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

[Nuno Lopes via Phabricator via llvm-commits]

nlopes added a comment.

Just a shameless plug :)
We've been half secretly working on Alive2 (https://github.com/AliveToolkit/alive2), which includes a plugin for `opt` that can check if an optimization is correct or not. Alive2 also has a standalone tool that accepts 2 IR files instead.
This tool implements the semantics of poison for many LLVM instructions, and already has some support for memory (which is quite hard to handle).
Of course, what this patch does is not the same. This patch is more executable, while Alive2 requires Z3 to reason about the semantics (though it can also execute code very slowly).

I guess this is more a FYI.  If you want to support a significant chunk of LLVM, it's going to be a lot of work. Alive2 already has ~1 year of development, and has already found a few bugs in LLVM.


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

https://reviews.llvm.org/D64215