[PATCH] D85345: [BuildLibCalls] Add noundef to standard I/O functions

Mon Aug 10 00:49:12 PDT 2020

aqjune added a comment.

In D85345#2205745 <https://reviews.llvm.org/D85345#2205745>, @jdoerfert wrote:

> In D85345#2205712 <https://reviews.llvm.org/D85345#2205712>, @aqjune wrote:
>
>> What about undef or poison is given to malloc? If it should raise UB, the size argument and returned pointer should be noundef.
>
> It is unclear to me if we want to forbid undef to be passed to malloc. It makes practical sense but not from a semantic perspective.
> However, even if you pass undef you should not get undef back. So the return should never be undef for sure. If it doesn, how could you ever deal with it, given that a branch on the result would be UB :D

Makes sense.... and labeling the returned pointer of malloc as noundef will be useful in various places, e.g. proving safety of loop unswitching on `icmp(malloc(p), null)`.
Give me some time, because I'd like to play with this by implementing this on Alive2 and see how it goes when running unit tests.

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D85345/new/

https://reviews.llvm.org/D85345