PV1 ⊧ Alive2formalises LLVM code and transformations and allows to analyse them

Collection of libraries and tools for the analysis and verification of LLVM code and transformations

Application domain/field

• Compiler
• Translation validation
• Bounded analysis
• Refinement

Type of tool

Translation validation tool for LLVM's IR

Expected input

Depends on the library/tool used.

Expected output

Depends on the library/tool used.

Internals

This framework has been made to find bugs in LLVM. Translation validation: A technique where an individual translation (e.g. a run of the compiler) is validated (i.e. verifies that the target code produced on this run correctly implements the submitted source program) instead of proving the correctness of the compiler beforehand. (Source: "Translation Validation" by A. Pnueli, M. Siegel and E. Singerman, TACAS 1998) It includes the following libraries:

• Alive2 IR
• Symbolic executor
• LLVM to Alive2 IR converter
• Refinement check (i.e. optimization verifier)
• SMT abstraction layer

It includes the following tools:

• Alive drop-in replacement
• Translation validation plugins for clang and LLVM's opt
• Standalone translation validation tool: alive-tv

Uses Z3.