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

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

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


Cool!
Is true that Alive2 doesn't support loops yet; that's in the todo list. It can handle branches and Phi nodes well, though.
Memory is being implemented ATM. Proofs with undef are quite hard. We don't have a fast-path for identical IR yet, it always goes to the expensive proof algorithm.
You can increase the timeout. With, say, a 10 seconds timeout it's very unlikely there's a bug since the SMT solver would very likely find it in that time.

Please keep me in the loop for these bugs you are seeing. I'm happy to help debug and/or just being in the loop of what happened if this might be an issue with IR semantics or simply a misunderstanding in the semantics. Thank you!


Repository:
  rL LLVM

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

https://reviews.llvm.org/D64215