reopt-vcg

Reopt VCG is a companion-tool to Reopt, designed to demonstrate functional equivalence between Reopt-generated LLVM bitcode and the original binary. This is done by simulating execution of each in tandem, block-by-block, and generating verification conditions which are dispatched to an external SMT solver (CVC4) intended to prove their behavioral equivalence.

Reopt VCG relies on an annotations file generated by Reopt for the binary in question (see Reopt's --annotations flag). This annotations file contains the locations of the original binary and generated LLVM bitcode files along with annotations intended to provide context for basic blocks which assist verification condition generation.

By default Reopt VCG will generate verification conditions and dispatch them to CVC4 to verify them. The --export flag can be used to instead emit each verification condition as an .smt2 file for manual inspection/verification.

Example usage:

$ reopt-vcg test_fib_diet_reopt.ann
Generating verification conditions for LLVM module...
.............................................................................
.............................................................................
.....
All 2 functions were assigned verification conditions without error.

====================== GOAL VERIFICATION SUMMARY =======================
All 159 generated verification goals successfully proven.

Note: on non-trivial binaries, some verification conditions may fail to be proven. This does not necessarily indicate that the lifting to LLVM was erroneous, as some verification conditions are inherently difficult to prove in practice. E.g., they may rely on non-trivial semantic properties which are under active development/research (e.g., invariants regarding memory safety, memory layout, pointer semantics, etc). Manual inspection of failed verification conditions can be useful in these instances.

Verification Conditions

The verification conditions generated for checking the equivalence of a binary basic block and the corresponding LLVM bitcode generated by reopt fall into one of the following categories, focusing on the equivalence of externally observable events that occur during execution:

1. Machine code reads/writes only from unreserved stack space.
2. LLVM writes targets intended allocation.
3. Machine code write targets intended allocation.
4. Read heap address not in stack space.
5. Block is unreachable.
6. Instruction pointer is expected value.
7. Reopt-infered pre/post-condition holds.
8. LLVM and machine code read from same allocation offset.
9. LLVM and machine code load from same heap address.
10. LLVM and machine code store to same heap address.
11. LLVM and machine code store the same value to the heap.
12. LLVM and machine code branch to the same function address.
13. Stack height preserved.
14. Return address preserved.
15. Register value preserved.
16. Return address is next instruction.
17. LLVM and machine code return values match.
18. Argument matches register.
19. Direction flag is expected value.

Example programs

add, fib, and nweb have been the running examples this tool was developed against. Annotations files for these live in the test-programs directory of this repository.