The Vellvm project seeks to provide a formal framework for developing machine-checkable proofs about LLVM IR programs and translation passes. While the traditional SSA control-flow-graph representation used by this IR enforces rich invariants, reasoning about program equivalence of such CFGs can be difficult. In contrast, functional programming languages come with equational theories, allowing for program transformations to be proved without having to build manually a simulation.

In the Vellvm (Verified LLVM) project, we have been experimenting with representing SSA control-flow-graphs using terms of Levy’s call-by-push-value (CBPV) variant of the lambda calculus. CBPV offers the benefits of a good equational theory based on the usual notions of beta-equivalence. By relating the operational semantics of the CBPV language to that of the SSA-control-flow graphs, we can transport reasoning and program transformations from one level to another, thereby allowing for very simple proofs of the correctness of many low-level optimizations such as function inlining. This talk will give a high level overview of the ongoing work we are conducting to formalize this connection between SSA CFGs and CBPV.

This is joing work with: Dmitri Garbuzov, William Mansky, Christine Rizkallah, and Steve Zdancewic.