A First-Order Functional Intermediate Language for Veried Compilers
Sigurd Schneider, Gert Smolka, Sebastian Hack · arXiv (Cornell University) · 2015
We present the rst-order intermediate language IL for veried compilers. IL is a functional language with calls to a nondeterministic environment. We give IL terms a second, imperative semantic interpretation and obtain a register transfer language. For the imperative interpretation we establish a notion of live variables. Based on live variables, we formulate a decidable property called coherence ensuring that the functional and the imperative interpretation of a term coincide. We formulate a SSA-based register assignment algorithm for IL and prove its correctness. The algorithm translates a functional IL program into an equivalent imperative IL program. Correctness follows from the fact that the algorithm reaches a coherent program after consistently renaming local variables. We prove that the maximal number of live variables in the initial program bounds the number of dierent variables in the nal coherent program. The entire development is formalized in Coq.