一句话：为 CompCert 内存模型引入抽象栈与细粒度栈权限，实现完整验证编译链并支持上下文组合编译。
CompCert 作为经过验证的 C 编译器，其成功关键之一是基于块的内存模型，但该模型缺少显式栈概念：目标汇编将运行时栈表示为无界内存块列表，难以进一步编译为具有有限连续栈的真实机器码；同时，组合式验证编译需要保护私有栈数据并允许修改公共栈分配数据，而原始 CompCert 缺乏这种机制，已有工作常遗漏尾调用识别、内联等显著改变栈块分配方式的优化。本文提出轻量且完整的解决方案：用抽象栈丰富 CompCert 内存模型，跟踪栈帧历史以限制栈消耗，并通过细粒度权限实施统一栈访问策略。该模型用于 CompCert 所有语言，重新证明了包含全部优化遍的完整编译链正确性，得到 Stack-Aware CompCert；进而构建 CompCertMC，首个编译到平坦内存空间低级语言的 CompCert 扩展；以及 Stack-Aware CompCertX，支持称为上下文编译的组合式编译。
A key ingredient contributing to the success of CompCert, the state-of-the-art verified compiler for C, is its block-based memory model, which is used uniformly for all of its languages and their verified compilation. However, CompCert's memory model lacks an explicit notion of stack. Its target assembly language represents the runtime stack as an unbounded list of memory blocks, making further compilation of CompCert assembly into more realistic machine code difficult since it is not possible to merge these blocks into a finite and continuous stack. Furthermore, various notions of verified compositional compilation rely on some kind of mechanism for protecting private stack data and enabling modification to the public stack-allocated data, which is lacking in the original CompCert. These problems have been investigated but not fully addressed before, in the sense that some advanced optimization passes that significantly change the ways stack blocks are (de-)allocated, such as tailcall recognition and inlining, are often omitted. We propose a lightweight and complete solution to the above problems. It is based on the enrichment of CompCert's memory model with an abstract stack that keeps track of the history of stack frames to bound the stack consumption and that enforces a uniform stack access policy by assigning fine-grained permissions to stack memory. Using this enriched memory model for all the languages of CompCert, we are able to reprove the correctness of the full compilation chain of CompCert, including all the optimization passes. In the end, we get Stack-Aware CompCert, a complete extension of CompCert that enforces the finiteness of the stack and fine-grained stack permissions. Based on Stack-Aware CompCert, we develop CompCertMC, the first extension of CompCert that compiles into a low-level language with flat memory spaces. Based on CompCertMC, we develop Stack-Aware CompCertX, a complete extension of CompCert that supports a notion of compositional compilation that we call contextual compilation by exploiting the uniform stack access policy provided by the abstract stack.
@article{paperbot682,
title = {An abstract stack based approach to verified compositional compilation to machine code},
author = {Yuting Wang and Pierre Wilke and Zhong Shao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290375}
}