A Formal Semantics of Intermediate Compiler
Representations in Isabelle/HOL
Sabine Glesner and Andreas Humbert
Technical University of Berlin, Germany
The correctness of compilers is crucial for the entire software
construction process. Especially optimizing transformations in
compilers are error-prone. In this paper, we define a formal semantics
for SSA intermediate compiler representations by a structural
operational semantics and semantic equivalence based on bisimulations
within the Isabelle/HOL theorem prover. Our formalization is generic
in the sense that it abstracts from a concrete individual SSA form and
instead introduces variables (representing e.g. types or certain
arithmetic operations) that can be instantiated when dealing with a
specific compiler. In this way, we not only simplify the formalization
itself but moreover allow for its reuse in further verifications of
similar (not only compiler) transformations. As an application, we
have verified a partial redundancy elimination.