Corollaries of the main semantic preservation theorem.

CompCertX:test-compcert-param-memory We create section WITHMEM and associated contexts to parameterize the proof over the memory model. We also parameterize over mmatch_inj, the proof that matching a concrete memory state with an abstract representation yields a memory that injects into itself. We also parameterize over magree_spec, the specification of memory matching for dead code elimination (a weaker form of memory extension.) CompCertX:test-compcert-param-extcall Actually, we also need to parameterize over external functions. To this end, we created a CompilerConfiguration class (cf. Events) which is designed to be the single class on which the whole CompCert is to be parameterized. It includes all operations and properties on which CompCert depends: memory model, semantics of external functions and their preservation through compilation. But it does not include mmatch_inj nor magree_spec (because their specification are too specific to the optimizations) CompCertX:test-compcert-param-i64-helpers Because of the axiom get_helpers_correct, we need to instantiate those classes now. It does not matter for whole programs.

Preservation of whole-program behaviors

From the simulation diagrams proved in file Compiler. it follows that whole-program observable behaviors are preserved in the following sense. First, every behavior of the generated assembly code is matched by a behavior of the source C code.

As a corollary, if the source C code cannot go wrong, the behavior of the generated assembly code is one of the possible behaviors of the source C code.

If we consider the C evaluation strategy implemented by the compiler, we get stronger preservation results.

We can also use the alternate big-step semantics for Cstrategy to establish behaviors of the generated assembly code.

Satisfaction of specifications

The second additional results shows that if all executions of the source C program satisfies a given specification (a predicate on the observable behavior of the program), then all executions of the produced Asm program satisfy this specification as well. We first show this result for specifications that are stable under the behavior_improves relation.

As a corollary, we obtain preservation of safety specifications: specifications that exclude "going wrong" behaviors.

We also have preservation of liveness specifications: specifications that assert the existence of a prefix of the observable trace satisfying some conditions.