Authors
Yuting Wang
Pierre Wilke
Zhong Shao
Abstract
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.
Published
In
Proc. 46th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL'19), Lisbon, Portugal, January 2019.
Published as
Proc. ACM Program. Lang. 3, POPL, Article 62 (January 2019), 30 pages.