[PATCH] D64215: Add a transform pass to make the executable semantics of poison explicit in the IR

[Sanjoy Das via Phabricator via llvm-commits]

sanjoy added inline comments.


================
Comment at: lib/Transforms/Instrumentation/PoisonChecking.cpp:41
+//   are well defined on the specific input used.
+// - Finding/confirming poison specific miscompiles by checking the poison
+//   status of an input/IR pair is the same before and after an optimization
----------------
reames wrote:
> reames wrote:
> > sanjoy wrote:
> > > This will have false positives as long as `undef` is a thing right?  Unless the instrumentation added by this pass will produce poison if *any* value of `undef` produces poison (naively it seems this would require calling into a SAT solver at runtime)?
> > I don't actually follow what you're trying to say.  Can you maybe rephrase w/an example which concerns you?  
> > 
> > For context, I'm focusing on poison for the moment, but I think a completely reasonable thing would be to have a parallel approach for undef (1 bit per bit of original value), and then cross propagate if needed.  I have a much weaker understanding of the undef rules, so I started with poison since that seemed a bit more clearly specified and recently discussed.  
> > 
> For context, the part which has me confused was your claim of a false positive.  I definitely see how undef can cause a false negative if not accounted for in the poison tracking.
By "false positive" I meant "incorrectly concluding that an optimization is buggy because this pass fails to detect poison before the optimization but is able to detect poison after the optimization".

Say you have this program:

```
int c = INT_SMAX +nsw undef;
```

IIUC you'll instrument this to:

```
int c, bool ov = add_with_overflow(INT_SMAX, undef)
if (ov) trap();
```

which will for only some values of `undef`.  In particular, it may be (depending on the phase of the moon) that running this program does not trap.

But a pass can legitimately transform the program to:

```
int c = INT_SMAX +nsw 1;  // fold undef to 1
```

which will deterministically trap after instrumentation.

So if we are unlucky it will "look like" the transformation has a bug -- before the xform the instrumented IR did not trap, but after the xform it traps.


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

https://reviews.llvm.org/D64215