Modular, Correct Compilation with Automatic Soundness Proofs

Abstract

Formal verification of compiler correctness requires substantial effort. A particular challenge is lack of modularity and automation. Any change or update to the compiler can render existing proofs obsolete and cause considerable manual proof effort. We propose a framework for automatically proving the correctness of compilation rules based on simultaneous symbolic execution for the source and target language. The correctness of the whole system follows from the correctness of each compilation rule. To support a new source or target language it is sufficient to formalize that language in terms of symbolic execution, while the corresponding formalization of its counterpart can be re-used. The correctness of translation rules can be checked automatically. Our approach is based on a reduction of correctness assertions to formulas in a program logic capable of symbolic execution of abstract programs. We instantiate the framework for compilation from Java to LLVM IR and provide a symbolic execution system for a subset of LLVM IR.

This work was funded by the Hessian LOEWE initiative within the Software-Factory 4.0 project.

Appendices

Appendix

This appendix provides additional material for the reader, including a sketch of the integration of state merging techniques into our approach, an extended compilation example, and a proof of Theorem 1.

A State Merging

Our SE transition relation defined in Sect. 3 outputs tree structures: all states, but the root, have exactly one predecessor. State Merging [16] has originally been invented to mitigate the state explosion problem of SE. It permits to merge symbolic states with identical program counter as arising, for example, after the execution of the then and else branch of an statement, thus reducing the state space. Definition 2 can be extended to transition relations with state merging by applying the same conditions reversely for “merging” transitions:

Fig. 7.

State merging translation rule

Definition 8

(Soundness of SE with State Merging). Let $\delta _m$ be an SE transition relation with state merging (some states have more than one predecessor). We call $\delta _m$ sound iff the transition relation

$$ \begin{aligned} \delta ':=~&\{(i,o)\in \delta _m:\lnot \exists {}i'\ne {}i,(i',o)\in \delta _m\}\,\cup \\&\{(o,i):(i,o)\in \delta _m\wedge \exists {}i'\ne {}i,(i',o)\in \delta _m\} \end{aligned} $$

is sound in the sense of Definition 2.

Translation rule mergeTransl (Fig. 7) merges two branches with identical program counters. Without it, compiling programs with branching statements leads to duplicated code, for example, in rule ifElseTransl. The double horizontal line below the rule’s premise indicates its special status: it is the only rule with more than one conclusion. For constructing the merged symbolic store, there is more than one option [16]. In the simplest case, we create a fully precise value summary by means of an if-then-else term.

B Factorial Example

The program in Fig. 8 (p. x) computes the factorial of variable x, contained in variable res after termination. Figure 12 shows the SET of the dual SE states corresponding to the translation of the Java to LLVM IR code. Constructing the tree works by first symbolically executing the Java program. The Java SET has the same structure, without the LLVM IR parts and observable variables sets.

In the second phase, we apply translation rules from the leaves to the root, obtaining the dual SE states. The root of the tree contains the compiled LLVM IR program $q_ result$ depicted in Fig. 9 (with dropped loop scopes). The tree is slightly simplified: we sometimes abbreviate programs with “$\dots$” and combine several translation rules into one, for example, in the translation of Java’s , which in the course of SE would be simplified to SSA form first. Two subtrees have been factored out for better readability (Figures 10 and 11).

The example also shows an artifact occurring due to our rule-based compilation: The basic block with label is never reached since it is not targeted by jumps, and the block before jumps outside the loop (this is the translation of the instruction). The instruction has been added because of the general definition of the translation rule; if the else block did not jump out of the loop, it would also make sense. Removal of such dead code, as well as other optimizations, are subject to subsequent post-processing steps and not within the scope of this paper.

Fig. 8.

Factorial program in Java

Fig. 9.

Factorial program in LLVM IR

Fig. 10.

Subtree “then” for the example tree in Fig. 12

Fig. 11.

Subtree “else” for the example tree in Fig. 12

Fig. 12.

An example compilation tree (slightly simplified)

C Proofs

Proof

(Theorem 1). We must prove that a translation rule is sound (Definition 6) if $\mathcal {F}=\big (\bigwedge _{i=1,\dots ,m} F ' {( pr_i )}\big )\rightarrow F ' {(c)}$ is valid. By Proposition 1, a dual SE state is valid iff its justifying formula is valid, and the shape of $\mathcal {F}$ directly encodes Definition 6. Hence, it suffices to show that the validity of justifying formulas $F ' {(s')}$ for abstract states $s'$ implies the validity of $F {(s)}$ for all concrete instantiations s of $s'$. Let be an abstract SE state where , $C^a$ and are symbolic and $p_j^ abs$, $p_ IR ^ abs$ contain abstract placeholder symbols. An instantiation s has the shape , where $p_j$ and $p_ IR$ result from $p_j^ abs$ and $p_ IR ^ abs$ by replacing placeholders with concrete programs. We have to show the following implication:

Since the validity of implies the validity of , it suffices to show the following, stronger property:

Since abstract execution is sound (Observation 1), the premise of (*) holds for all concrete contracts substituted for the abstract ones induced by the placeholders in the programs; this means that in particular, we can substitute $p_j$/$p_ IR$ for $p_j^ abs$/$p_ IR ^ abs$. Let , be the updates resulting from SE of the concrete programs (if SE splits, we can obtain summaries by state merging, see Appendix A).

Now there are two possibilities: Either, is an atom, or it is a guarded conjunction (and s constitutes the conclusion of a dual SE rule application). We focus on the more complicated second case. Let be the (concrete) set of observable variables of s, $C_i$ the path conditions of the premisses of the rule that has s in its conclusion, and the variables occurring in any symbolic store or path condition of those premises. Then, after instantiation, (*) expands to:

Generally, can contain variables not occurring in , due to over-approximation. On the other hand, if contains variables not in , those are not in the scope of the currently investigated rule, and are therefore taken out of consideration here.² Additionally, we perform a strengthening by dropping the updates in the conclusion (this can be regarded as an abstraction step, since we discharge information). W.l.o.g., consider two different variables x, y and ; their right-hand sides in the updates and are , , etc. Under the assumption that x and y do not occur in the $C_i$ (see Remark 1), the problem simplifies to:

For simplicity, we assume that the terms do not contain program variables. The equivalence in ($\triangle$) is valid iff for all interpretations $\mathcal {I}$, it holds that

Let $\mathcal {I} _0$ be an arbitrary interpretation; we show that ($\Delta ^{ sem }$) holds for $\mathcal {I} _0$. All $C_i$ are mutually exclusive due to the restriction built into our semantics (Definition 2), i.e. $C_i\leftrightarrow \bigwedge _{k\ne i}\lnot C_k$ for all $i=1,\dots ,n$. Since ($\dagger$) is valid, for any interpretation $\mathcal {I}$ there is exactly one i such that

We choose an interpretation $\mathcal {I} _1$ that (i) interprets in the same way as $\mathcal {I} _0$, (ii) satisfies and, at the same time, (iii) satisfies ($\dagger ^{{sem}}$) for some i. By definition of $\mathcal {I} _1$ we have that implies , and, similarly, for , . Hence, ($\Delta ^{ sem }$) holds in $\mathcal {I} _0$.    $\square$