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

Mon Jul 8 15:01:11 PDT 2019

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 :)

I finally got it working, required a couple changes to the CMakeFiles and an LD_PRELOAD (for unclear reasons).  However, it doesn't look like the scope of the alive-tv tool is anywhere near wide enough for my purposes.

Correct me if I'm wrong, but it looks like it can't handle loops at all right?  And use of any memory seams to trigger timeouts?  (Even for trivially identical IR?)  Just making sure there's no error between keyboard and chair.  :)

The problems I'm looking at are definitely not single block problems, unfortunately.

Can I get an LGTM on this?  It seems like folks are interested in the approach, and it would be much easier to iterate in tree if needed.

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

https://reviews.llvm.org/D64215