A Witnessing Compiler: A Proof of Concept - Runtime Verification - page 340

A Witnessing Compiler: A Proof of Concept
Kedar S. Namjoshi 1 , Giacomo Tagliabue 2 , and Lenore D. Zuck 2
1 Bell Laboratories, Alcatel-Lucent
[e-mail]
2 University of Illinois at Chicago
[e-mail], [e-mail]
Abstract. In prior work we proposed a mechanism of “witness genera-
tion and propagation” to construct proofs of the correctness of program
transformations. Here we present a simpler theory, and describe our ex-
perience with an initial implementation based on the LLVM open-source
compiler and the Z3 SMT solver.
1 Introduction
Ensuring the correctness of an optimizing compiler is a classic question in com-
puting. Compilers are very large programs - for instance, GCC is over 7 million
lines of code, and LLVM is near a million - and they carry out the essential task
of transforming other programs (often themselves large) into executable machine
code. Ensuring the correctness of compiler transformations is thus a critical ques-
tion; however, manual inspection is impossible,whichhasledtomuchworkon
the construction of automated proofs of correctness.
In [7] we proposed a methodology for creating such a proof. There, each
optimization procedure in the compiler is augmented with an auxiliary witness
generator . For every instance of optimization, the generator constructs, at run
time ,a witness relation between its target and source programs. The conditions
for a relation to be a proper witness are checked off-line, using an automated
theorem prover. Thus, when a witnessing compiler is used on a source program,
it generates a chain of witnesses, one for each optimization, which connects the
source program with the final target program. Each link of the chain may be
verified independently of the compiler code.
Witness generation can be positioned in-between two well known methods
of compiler verification: machine-checked proofs of correctness (e.g., [5]) and
Translation Validation (TV) (e.g., [10]). It is substantially simpler to define
a witness generation procedure than to prove an optimization correct, as the
definition does not require one to show (or assume) the correctness of the analysis
phase of an optimization. Moreover, as the generating procedure is written with
full knowledge of the optimization, one avoids the heuristic constructions which
limit the scope of translation validation. The potential drawback to witness
generation is the run-time overhead of generation and checking.
In this paper, we report on early experiments with witness generation. The im-
plementation is carried out using the LLVM compiler framework [4]. It currently