Speaker
Description
Peephole rewriting forms the backbone of the LLVM optimizer, where over 10% of the size of the codebase of LLVM lives in InstCombine. It's of vital importance to ensure that these rewrites are correct, especially because the canonicalizer and peephole optimizer are run pervasively through the pass pipeline. Efforts such as Alive have brought the verification of peephole optimizations into the LLVM review cycle by providing a convenient user interface for verifying such transformations. However, Alive only checks these rewrites upto a fixed bitwidth (typically, 64), and therefore does not provably guarantee that these rewrites are valid for arbitrary bit-widths.
We take on the challenge of building algorithms that can prove bitvector rewrites correct for arbitrary bitwidths. In particular, these algorithms prove the correctness of any proposition over a fragment of the bitvector theory, with a proof for all bitwidths.
The algorithm is based on ideas from model checking and program deobfuscation. We take care to ensure scalability, and we implement, benchmark, and prove our algorithms correct in the Lean proof assistant. We also provide a user-facing tactic interface for ease of use. . We evaluate our tactic on rewrites from both Hacker’s Delight and the InstCombine test suite, as well as on equivalence checking problems for program obfuscation.
We hope to use our algorithm to simplify the many thousands of lines of proof in the Lean bitvector standard library, and more broadly, to provide effective proof automation for bitvector predicates that are true for all bitwidths.
Any other info we should know?
The audience will gain a broad understanding of how the Lean proof assistant can be used to prove bitvector identities for arbitrary bitwidths, especially in the context of compiler optimizations. The talk is technical in nature and will explain our algorithms and their applications to real-world rewrite verification. Attendees will also learn about decision procedures for bitvectors, model checking techniques, and how to interact with Lean through a user-facing tactic interface. The session will be interactive—audience questions about proof automation, decision procedures, and Lean are very welcome.
Session author's bio
Siddharth Bhat is a PhD student at the University of Cambridge who works on algorithms and decision procedures. He formally verifies these algorithms in the Lean proof assistant, and builds such tooling with an eye toward SAT and SMT-style problems that are profitable for compilers.
| Please confirm that there are included headshots of all speakers in their profiles | Yes |
|---|---|
| Agree to Privacy Policy and Notice | I agree |
| Level of Difficulty | Intermediate |
| In Person Attendance | Remote |