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
- Errors: the Error monad.
- AST: identifiers, whole programs and other
common elements of abstract syntaxes.
- Values: run-time values.
- Values_symbolictype: type of symbolic values together with their typechecking functions.
- Values_symbolic: the counterpart of Values for symbolic values.
- Events: observable events and traces.
- Memtype: memory model (interface).
See also: Memory (implementation of the memory model).
See also: Memdata (in-memory representation of data).
- Globalenvs: global execution environments.
- Smallstep: tools for small-step semantics.
- Behaviors: from small-step semantics to observable behaviors of programs.
- Determinism: determinism properties of small-step semantics.
- Unityping: a solver for atomic unification constraints.
New modules introduced to cope with symbolic expressions
- NormaliseSpec: specification of the normalisation, in particular definitions of compatible memory layouts, and notions of correctness and completeness for the normalisation.
- Normalise: collection of useful theorems about the normalisation
- Alloc: allocation algorithm and theorems about it. This is needed because we model an allocation that can fail when there is no memeory left.
- Equivalences: definition of equivalences of symbolic expressions, equivalence of memories, and proofs that primitive memory operations commute with these equivalences.
- ClightEquivalences: proofs that Clight memory operations commute with memory equivalences.
Source, intermediate and target languages: syntax and semantics
The languages that have been adapted to symbolic values.
||Source & target
|Pulling side-effects out of expressions;
fixing an evaluation order
|CompCert C to Clight
|Pulling non-adressable scalar local variables out of memory
||Clight to Clight
|Simplification of control structures;
explication of type-dependent computations
|Clight to Csharpminor
|Stack allocation of local variables
whose address is taken;
simplification of switch statements
|Csharpminor to Cminor
- Compiler: composing the passes together;
whole-compiler semantic preservation theorems. This has been adapted to generate Cminor code instead of assembly code.
- Complements: interesting consequences of the semantic preservation theorems.