An abstract stack based approach to verified compositional compilation to machine code
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 02, 2019
- Source ID
- 10.1145/3290375
Entities
People
- Pierre Wilke
- Yuting Wang
- Zhong Shao
Organizations
- Defense Advanced Research Projects Agency
- National Science Foundation
- Yale University