Go Formal Translation Verification

[Ryan Berger]

Hello all,

I'm Ryan Berger, I'm a long time gopher and a previous student of John Regehr who worked on Alive2 (https://users.cs.utah.edu/~regehr/alive2-pldi21.pdf , https://github.com/alivetoolkit/alive2), CSmith, and a few other compiler tools.

As part of my senior thesis, we wrote a verifier to take ARM generated from LLVM's backend and validate that the generation was semantically correct using Alive2. Writing backend optimizations is hard to get right, and we caught quite a few bugs in LLVM's GlobalISel ARM backend through lots of fuzzing and verifying translation.

I've been wanting to extend this tool validate different forms of translation in Go, and asking around on the Gopher slack, there seems to be some initial interest from some well-known gophers who have contributed to the compiler.

There are two areas where I see this as helpful:

1. Verifying correctness of source to source rewrite rules for generic SSA rewrites.
2. Verifying correctness of ARM (soon to be other backends) code generation.

Doing either of these will allow for more fearless optimization work, and the ability to verify that rewrites are valid. Many of the folks over at LLVM who contribute have found great value in being able to test if their optimizations are correct without much thought.

To do this however, I would need access to the compile/internal/ssa package, and its ability to apply rewrite rules to a program. With that I would lift the unoptimized and optimized programs into Alive IR to verify the rewrite rule's correctness.

There is the the golang.org/x/tools/go/ssa package, but this only provides me an interface to turn an the program into an in-memory SSA data structure, but cannot apply any of the rewrite rules.

I was hoping to get a feel for sentiment on providing the generic (maybe even platform specific?) rewrite rules and passes as apart of the public golang.org/x/tools/go/ssa API (maybe in a sub-package called "rewrite"), or some other public facing API. Doing so would provide more advanced analysis capabilities for correctness work, makes hacking on optimizations easier, and could provide more tooling outside the ssa-html tool for visualization and understanding of optimizations.

Alternatively, the project could depend on the internal ssa package, accepting that it is internal and could break at any time, and that the Go team doesn't owe the project any consistency. I'm willing to do this, but was hoping to get some feedback before I get too deep into anything.

I'm happy to write up a more formal proposal or talk with anyone involved to help hash out details.

Thanks,

Ryan

[Keith Randall]

On Wed, Mar 15, 2023 at 11:09 AM Ryan Berger <ryanb...@gmail.com> wrote:

Hello all,

I'm Ryan Berger, I'm a long time gopher and a previous student of John Regehr who worked on Alive2 (https://users.cs.utah.edu/~regehr/alive2-pldi21.pdf , https://github.com/alivetoolkit/alive2), CSmith, and a few other compiler tools.

As part of my senior thesis, we wrote a verifier to take ARM generated from LLVM's backend and validate that the generation was semantically correct using Alive2. Writing backend optimizations is hard to get right, and we caught quite a few bugs in LLVM's GlobalISel ARM backend through lots of fuzzing and verifying translation.

I've been wanting to extend this tool validate different forms of translation in Go, and asking around on the Gopher slack, there seems to be some initial interest from some well-known gophers who have contributed to the compiler.

There are two areas where I see this as helpful:

1. Verifying correctness of source to source rewrite rules for generic SSA rewrites.
2. Verifying correctness of ARM (soon to be other backends) code generation.

Doing either of these will allow for more fearless optimization work, and the ability to verify that rewrites are valid. Many of the folks over at LLVM who contribute have found great value in being able to test if their optimizations are correct without much thought.

To do this however, I would need access to the compile/internal/ssa package, and its ability to apply rewrite rules to a program. With that I would lift the unoptimized and optimized programs into Alive IR to verify the rewrite rule's correctness.

There is the the golang.org/x/tools/go/ssa package, but this only provides me an interface to turn an the program into an in-memory SSA data structure, but cannot apply any of the rewrite rules.

I was hoping to get a feel for sentiment on providing the generic (maybe even platform specific?) rewrite rules and passes as apart of the public golang.org/x/tools/go/ssa API (maybe in a sub-package called "rewrite"), or some other public facing API. Doing so would provide more advanced analysis capabilities for correctness work, makes hacking on optimizations easier, and could provide more tooling outside the ssa-html tool for visualization and understanding of optimizations.

I don't think it is a good idea to expose the compiler internals like this. The general format of the SSA values (Blocks, Values, etc.) are pretty stable at this point, but we're still adding/modifying opcodes all the time.

Alternatively, the project could depend on the internal ssa package, accepting that it is internal and could break at any time, and that the Go team doesn't owe the project any consistency. I'm willing to do this, but was hoping to get some feedback before I get too deep into anything.

That would be fine, or you could just copy all that code into your own project. I think if you found bugs in a snapshot taken a few months ago that would still be useful info. As long as you didn't modify that code it would be pretty easy to pull in the latest version periodically.

I'm happy to write up a more formal proposal or talk with anyone involved to help hash out details.

Thanks,

Ryan

--
You received this message because you are subscribed to the Google Groups "golang-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-dev+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/golang-dev/dc7a062d-77a1-4f96-8bd4-cca14d7ac0b8n%40googlegroups.com.

[Michael McLoughlin]

Ryan,

This is awesome, thanks for sharing.

I had a similar idea and started down this road a while back, didn't get very far and my effort on it dwindled. That's not to say your project would go the same way, I just have a long trail of incomplete side projects.

I've made the repository public in case my limited progress is of any interest to you:

https://github.com/mmcloughlin/ssarules

Looking forward to seeing how you get on!

Mike

--

[Ryan Berger]

On Thursday, March 16, 2023 at 1:52:20 AM UTC-6 Michael McLoughlin wrote:

Ryan,

This is awesome, thanks for sharing.

I had a similar idea and started down this road a while back, didn't get very far and my effort on it dwindled. That's not to say your project would go the same way, I just have a long trail of incomplete side projects.

I've made the repository public in case my limited progress is of any interest to you:

https://github.com/mmcloughlin/ssarules

Looking forward to seeing how you get on!

Mike

Hey Mike! That does look quite similar to what I've been looking at doing.

Thankfully the SMT solver is hidden behind the abstraction of Alive2 and maintained by people much smarter than me :)

Also, I have a prototype!

https://github.com/ryan-berger/golang_tv

I ended up with going with Keith's advice and just copy pasting the Go SSA internals and hacking around on it. It mostly works, still working through figuring out some of the Go compiler internals so that I can deal with more complicated programs. Doesn't matter too much because there's now a prototype that can convert Go's SSA into Alive IR!

Cheers,

Ryan