CompCert with symbolic values

This page presents the Coq development associated with our extension of CompCert with symbolic values, including the adapted proofs of the memory model and the frontend.

Table of contents

Definitions and theorems used in many parts of the development

New modules introduced to cope with symbolic expressions

Source, intermediate and target languages: syntax and semantics

The languages that have been adapted to symbolic values.

Compiler passes

Pass Source & target Compiler code Correctness proof
Pulling side-effects out of expressions;
fixing an evaluation order
CompCert C to Clight SimplExpr SimplExprspec
SimplExprproof
Pulling non-adressable scalar local variables out of memory Clight to Clight SimplLocals SimplLocalsproof
Simplification of control structures;
explication of type-dependent computations
Clight to Csharpminor Cshmgen Cshmgenproof
Stack allocation of local variables
whose address is taken;
simplification of switch statements
Csharpminor to Cminor Cminorgen Cminorgenproof

All together