一句话：提出并集成到 CompCert 的翻译验证框架，借助优化给出的提示，可形式化验证 LCM、强度削减等多种优化。
CompCert 是首个具有机器检查正确性证明的工业级编译器，但优化能力仍较温和，缺少 gcc -O1 中的惰性代码外提（LCM）和强度削减（SR）等优化；同时为这些高效优化开发形式化证明仍是难题。本文重新审视并推广 Six 等人的翻译验证方法，在 CompCert 中集成了一个可验证更多优化的框架，包括增强的 superblock 调度、死代码消除、常量传播，以及 LCM 与 SR。与其他翻译验证不同，本文协同设计不可信优化与其验证器：优化以不变式或 CFG 态射等形式提供提示，使形式化验证器保持简单高效。该设计有望用于 CompCert 之外。
CompCert (ACM Software System Award 2021) is the first industrial-strength compiler with a mechanically checked proof of correctness. Yet, CompCert remains a moderately optimizing C compiler. Indeed, some optimizations of “gcc -O1” such as Lazy Code Motion (LCM) or Strength Reduction (SR) were still missing: developing these efficient optimizations together with their formal proofs remained a challenge. Cyril Six et al. have developed efficient formally verified translation validators for certifying the results of superblock schedulers and peephole optimizations. We revisit and generalize their approach into a framework (integrated into CompCert) able to validate many more optimizations: an enhanced superblock scheduler, but also Dead Code Elimination (DCE), Constant Propagation (CP), and more noticeably, LCM and SR. In contrast to other approaches to translation validation, we co-design our untrusted optimizations and their validators. Our optimizations provide hints, in the forms of invariants or CFG morphisms , that help keep the formally verified validators both simple and efficient. Such designs seem applicable beyond CompCert.
@article{paperbot1821,
title = {Formally Verifying Optimizations with Block Simulations},
author = {Léo Gourdin and Benjamin Bonneau and Sylvain Boulmé and David Monniaux and Alexandre Bérard},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622799}
}