## 1 Introduction

## 2 Overview

`(%a & %b) + (%a | %b)`

to `%a + %b`

, given 4-bits integers `%a`

and `%b`

. The last variable `%r`

, or root variable, is assumed to be the return value of the programs. AliveInLean encodes the behavior of each program and generates verification conditions (VCs). Finally, AliveInLean calls Z3 to discharge the VCs.`udiv`

(unsigned division) is never `poison`

^{1}if it did not raise undefined behavior (UB). The lemma below states this in Lean. This lemma says that the divisor

`val`

is never poison if the state `st’`

after executing the `udiv`

instruction (`step`

) has no UB.
`step`

function in the above example implements a specification of the LLVM IR, and it can be tested with respect to the behavior of the LLVM compiler. Another trust-base is the specification of SMT expressions, which defines a relation between expressions (with no free variable) and their corresponding concrete values.## 3 Verifying Optimizations

### 3.1 Semantics Encoder

`bool`

type of Lean or the `Bool`

SMT expression type. Given the type, Lean can automatically resolve which operations to use to update the state using typeclass resolution.### 3.2 Refinement Encoder

`poison`

when it is also `poison`

in the original program, and (3) variables’ values in the final states of the two programs are the same when no UB is triggered and the original value is not `poison`

.### 3.3 Parser and Z3 Backend

## 4 Correctness of AliveInLean

### 4.1 Semantics Encoding

`run`

, a semantics encoder `encoder`

is correct with respect to `run`

if for any IR program and input state, the final program state generated by `run`

and the symbolic state encoded by `encoder`

are equivalent.`encoder`

with respect to `run`

is defined as follows. It states that the result of `encoder`

is equivalent to the result of `run`

.### 4.2 Refinement Encoding

`check`

\((p_{src}, p_{tgt}, s_s)\) generates an SMT expression that encodes refinement between the source and target programs, respectively, \(p_{src}\) and \(p_{tgt}\).`check`

is stated as follows.`check`

\((p_{src}, p_{tgt}, s_s)]\!] \sim true \) for any \(\eta _0\), then for any environment \(\eta \) and initial state \(s_c\) s.t. \(\eta [\![ s_s ]\!] \sim s_c\), we have that \(\texttt {run}(p_{tgt}, s_c) \sqsubseteq \texttt {run}(p_{src}, s_c)\).`check`

evaluates to true in any environment, program \(p_{tgt}\) refines program \(p_{src}\).### 4.3 Validity of Trust-Base

`s1`

, `s2`

of a bit-vector type (`sbitvec`

) are equivalent to two concrete bit-vector values `b1`

, `b2`

in Lean (`bitvector`

), an add expression of `s1`

, `s2`

is equivalent to the result of adding `b1`

and `b2`

. Function `bitvector.add`

must be called in Lean, so its operands (`b1`

, `b2`

) are assigned random values in Lean. `sbitvec.add`

is translated to SMT’s `bvadd`

expression, and `s1`

and `s2`

are initialized as `BitVec`

variables in an SMT solver. The testing function generates an SMT expression with random inputs like the following:
`sz`

) is initialized to 4, and `b1`

, `b2`

were randomly initialized to 10 (`#xA`

) and 2 (`#x2`

). A specification is incorrect if the generated SMT expression is not valid.## 5 Evaluation

^{2}

^{3}consists of 11.9K lines of code. The optimization verifier consists of 2.2K LoC, the specification tester is 1.5K, and the proof has 8.1K lines. It took 3 person-months to implement the tool and prove its correctness.

## 6 Related Work

### 6.1 Compiler Verification

`poison`

and `undef`

value of LLVM is currently not consistent and thus it triggers miscompilations of some programs [10]. Therefore, compiler developers regularly test various `undef`

semantics with existing optimizations, which would be a non-trivial task if correctness proofs had to be manually updated.`C`

is a constant, `-C`

can be computed at compile time. However, this optimization is wrong only if `C`

is `INT_MIN`

. To show that compilation is fully correct, translation validation would need to be run for every combination of inputs.### 6.2 Solver-Aided Programming Languages

### 6.3 Semantics of Compiler IR

`poison`

and `undef`

values are inconsistent. [9] shows that the semantics of pointer\(\leftrightarrow \)integer casting is inconsistent. AliveInLean supports `poison`

but not `undef`

, following the suggestion from [10]. AliveInLean does not support memory-related operations including load, store, and pointer \(\leftrightarrow \) integer casting.