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

[Philip Reames via Phabricator via llvm-commits]

reames added a comment.

In D64215#1572285 <https://reviews.llvm.org/D64215#1572285>, @nlopes wrote:

> 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.


One thought on sharing.

>From what I can tell from a quick look at the code you mentioned, it looks like you're parsing IR into an expression language, then rewriting the expressions to propagate poison - in a fairly similar manner to this code, but over your expression language - and then translating that expression language to SMT.  Is that a good high level summary?

If you used this framework (not necessarily the pass, but the utilities) to rewrite the IR so as to make poison semantics explicit before converting to your expression language, you might be able to factor out a good portion of the poison reasoning from Alive2.  It'd be a fairly major design though, so not sure if that's worth it to you or not.


Repository:
  rL LLVM

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

https://reviews.llvm.org/D64215