PV1 ⊧ AliveInLeanverifies its own expectations of a given compiler optimisation

Application domain/field

• Compilers
• Compiler optimizations

Type of tool

Compiler optimization verifier

Expected input

Optimization pattern. This pattern describes what 'pattern' should be matched in the LLVM, and what the result should be (i.e. how it should be rewritten). Example (Source: "AliveInLean: A Verified LLVM Peephole Optimization Verifier" by J. Lee et al. (2019)):

Format:

Domain-specific language

Expected output

Whether the compiler optimization is correct

Internals

Has been verified/implemented with the Lean theorem prover. Uses a verification condition (VC) generator. The VCs are discharged using an SMT solver (Z3). The correctness of the optimization is checked by the following 3 things:

1. The target is defined when the source is defined
2. The target is poison-free when the source is poison-free
3. The source and target produce the same result when the source is defined and poison-free

Comments

Goal of the tool: Developers can check the correctness of compiler optimizations.