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.