[PATCH] D60047: [CaptureTracking] Don't let comparisons against null escape inbounds pointers

[Juneyoung Lee via Phabricator via llvm-commits]

aqjune added a comment.

Hello,

> One mode of reasoning that could invalidate this example is that p *could have been* something other than 2^64-4 which would invoke UB. This UB would both let us pretend that foo does not escape p, and also print 2^64-4 even though p was not 2^64-4 in the execution we chose. This seems a bit subtle though, and I'm not entirely sure this is sound reasoning.

(sorry for my sudden interruption :) I think this reasoning makes sense, but to say why it makes sense a few minor details should be explained.
We can say that there are two kinds of nondeterminisms -
First one is from an external input. After `scanf("%d", &x)`, we can say that the value of x is 'nondeterministically' chosen.
However, compiler cannot conveniently choose what `x` is; for example, it is invalid to assume that `x == 1` after `scanf` and optimize `printf("%d", x)` to `print("1")`.
Second one is the nondeterminism coming from the semantics of language. For example, given a C statement `f(e1, e2)` where e1 and e2 are expressions, the order of evaluation of `e1` and `e2` is nondeterministic. In this case, it is allowed for compiler to choose which one to execute.
This is why the statement 'a racy program has undefined behavior' makes sense. In languages like C, the order of interleaving of instructions is not given by an external identity (which would be something like a stream of `scanf` getting which thread to execute next from a process scheduler), but it is nondeterministic by its semantics. If there exists a racy execution among them, compiler can just choose the execution and say that 'the source program has undefined behavior, so I'm going to compile it into anything'.
I think the story is similar here. We can define that the address of allocation is nondeterministically chosen (like the case of a racy program), so LLVM can pick the most problematic one, and say that the source program already has undefined behavior. :)


Repository:
  rL LLVM

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

https://reviews.llvm.org/D60047