Formal Verification of an SSA-Based Middle-End for CompCert
Formal Verification of an SSA-Based Middle-End for CompCert
复制标题
DOI：
10.1145/2579080
复制
发表时间：
2014-03-01
影响因子：
1.3
通讯作者：
Pichardie, David
中科院分区：
文献类型：
--
作者：
Barthe, Gilles;Demange, Delphine;Pichardie, David
CompCert 是经过正式验证的编译器，可为 C 语言的大部分子集生成紧凑且高效的代码。然而，CompCert 放弃使用 SSA，这是许多编译器使用的一种中间表示形式，可以编写更简单、更快的优化器。事实上，正式验证基于 SSA 的编译器仍然是一个悬而未决的问题。我们报告了一个经过正式验证、基于 SSA 的 CompCert 中端。除了提供形式化验证的基于 SSA 的中端之外，我们还解决了 Leroy 在 [2009] 中提出的两个问题：为 SSA 提供直观的形式语义，并利用其全局属性在本地推理程序优化。
CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler, faster optimizers. In fact, it has remained an open problem to verify formally an SSA-based compiler. We report on a formally verified, SSA-based middle-end for CompCert. In addition to providing a formally verified SSA-based middle-end, we address two problems raised by Leroy in [2009]: giving an intuitive formal semantics to SSA, and leveraging its global properties to reason locally about program optimizations.