asking for advice about putting alive2 on compiler explorer

[John Regehr]

Hello!

I'm one of the developers of Alive2, a formal methods tool for reasoning about LLVM IR. We are very interested in making Alive2 available on CE, either on Matt's main instance or else on a custom instance that we would run, and are looking for advice. Alas, none of the Alive2 folks are good at JS so my questions may be very basic.

There are multiple ways to use Alive2, but the one that seems most likely to fit into Compiler Explorer's world view is one that takes a single IR file as input, optimizes it, and then checks if the optimization was OK.

For example, here we use Alive2 to find an LLVM optimization bug (not sure if the bug is still there, but it had not been fixed on the release/10.x branch as of early February 2020):

$ cat foo.ll
define i3 @foo(i3) {
  %x1 = sub i3 0, %0
  %x2 = icmp ne i3 %0, 0
  %x3 = zext i1 %x2 to i3
  %x4 = lshr i3 %x1, %x3
  %x5 = lshr i3 %x4, %x3
  ret i3 %x5
}
$ ./alive-tv foo.ll

----------------------------------------
define i3 @foo(i3 %0) {
  %x1 = sub i3 0, %0
  %x2 = icmp ne i3 %0, 0
  %x3 = zext i1 %x2 to i3
  %x4 = lshr i3 %x1, %x3
  %x5 = lshr i3 %x4, %x3
  ret i3 %x5
}
=>
define i3 @foo(i3 %0) {
  %x1 = sub i3 0, %0
  ret i3 %x1
}
Transformation doesn't verify!
ERROR: Value mismatch

Example:
i3 %0 = #x5 (5, -3)

Source:
i3 %x1 = #x3 (3)
i1 %x2 = #x1 (1)
i3 %x3 = #x1 (1)
i3 %x4 = #x1 (1)
i3 %x5 = #x0 (0)

Target:
i3 %x1 = #x3 (3)
Source value: #x0 (0)
Target value: #x3 (3)

Summary:
  0 correct transformations
  1 incorrect transformations
  0 errors

The goal, of course, is to allow someone to paste some LLVM IR into Compiler Explorer, and see the output above. Does this seem reasonably straightforward, and is there perhaps interest in hosting this tool in the main CE instance, if we do the legwork to package up alive2 appropriately?

Our code is here, in case that's helpful:

  https://github.com/AliveToolkit/alive2

Thanks,

John

[Rubén Rincón Blanco]

Hi John, sorry that we missed this for as long as we did

Is this something you're still interested in?

[John Regehr]

Hi! I managed to resolve my issues and the site is working fine, thank you!

http://volta.cs.utah.edu:8080/

John

On Wed, Apr 1, 2020 at 3:10 AM Rubén Rincón Blanco <rubr...@gmail.com> wrote:

Hi John, sorry that we missed this for as long as we did

Is this something you're still interested in?

--
You received this message because you are subscribed to the Google Groups "Compiler Explorer Discussion" group.
To unsubscribe from this group and stop receiving emails from it, send an email to compiler-explorer-di...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/compiler-explorer-discussion/aec722dc-6228-4b2d-8d3f-f3fbe3efddef%40googlegroups.com.

[an...@ajdurant.co.uk]

Hi John,

I'm interested in setting up something similar, are you able to share any information on how you got it set up or what your configuration is for CE?

Thanks,

Andy

On Friday, 3 April 2020 18:10:08 UTC+1, John Regehr wrote:

Hi! I managed to resolve my issues and the site is working fine, thank you!

http://volta.cs.utah.edu:8080/

John

On Wed, Apr 1, 2020 at 3:10 AM Rubén Rincón Blanco <rubr...@gmail.com> wrote:

Hi John, sorry that we missed this for as long as we did

Is this something you're still interested in?

--
You received this message because you are subscribed to the Google Groups "Compiler Explorer Discussion" group.

To unsubscribe from this group and stop receiving emails from it, send an email to compiler-explorer-discussion+unsub...@googlegroups.com.

[John Regehr]

hi!

my branch is here:

https://github.com/regehr/compiler-explorer/tree/alive2-compiler

let me know if you have any questions, this has been running happily on one of my machines for a month or so

John

On Thu, Apr 30, 2020 at 7:17 AM <an...@ajdurant.co.uk> wrote:

Hi John,

I'm interested in setting up something similar, are you able to share any information on how you got it set up or what your configuration is for CE?

Thanks,

Andy

On Friday, 3 April 2020 18:10:08 UTC+1, John Regehr wrote:

Hi! I managed to resolve my issues and the site is working fine, thank you!

http://volta.cs.utah.edu:8080/

John

On Wed, Apr 1, 2020 at 3:10 AM Rubén Rincón Blanco <rubr...@gmail.com> wrote:

Hi John, sorry that we missed this for as long as we did

Is this something you're still interested in?

--
You received this message because you are subscribed to the Google Groups "Compiler Explorer Discussion" group.

To unsubscribe from this group and stop receiving emails from it, send an email to compiler-explorer-di...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/compiler-explorer-discussion/aec722dc-6228-4b2d-8d3f-f3fbe3efddef%40googlegroups.com.

--

You received this message because you are subscribed to the Google Groups "Compiler Explorer Discussion" group.

To unsubscribe from this group and stop receiving emails from it, send an email to compiler-explorer-di...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/compiler-explorer-discussion/a9a806ce-351d-4d6e-b901-1c1b83990717%40googlegroups.com.