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

Sat Jul 6 03:37:52 PDT 2019

nlopes added a comment.

In D64215#1572070 <https://reviews.llvm.org/D64215#1572070>, @reames wrote:

> In D64215#1571424 <https://reviews.llvm.org/D64215#1571424>, @nlopes wrote:
>
> > 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.
>
>
> I'd tried playing with Alive2 a while ago, and had trouble getting it to work.  Could you maybe update the readme (or other docs) with some instructions on how to use the standalone tool you mentioned?  I'd very much like to play with this.

I've just added a short description to the README file: https://github.com/AliveToolkit/alive2#running-standalone-translation-validation-tool-alive-tv
It's fairly simple: it just takes 2 LLVM IR files. Let me know if you have questions or if you find bugs :)

>> 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'd love to explore options for sharing the semantics here.  What form does Alive2 express them in?

That's still a unsolved research problem. No one really knows how to share semantics still.
The semantics in Alive2 are written in C++, using an embedded expression language. While it is potentially possible to reuse that somewhere else, it isn't trivial. See e.g. the ir/instr.cpp file.

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

https://reviews.llvm.org/D64215