Simplify module Complements and add separate compilation (#121)

* Simplify the theorems about preservation of specifications (section 2)

There were three theorems, transf_c_program_preserves_spec, _safety_spec, and _liveness_spec) with the first being needlessly general and the last being hard to understand.  Plus, the "liveness" and "safety" terminology wasn't very good.

Replaced by two theorems:
- transf_c_program_preserves_spec, which is the theorem previously named _safety_spec and talks about specifications that exclude going-wrong behaviors;
- transf_c_program_preserves_initial_trace, which is an instance of the theorem previously named _liveness_spec, and now talks about a single initial trace of interest rather than a set of such traces.

Added named definitions for properties of interest.

Added more explanations.

* Added theorems that talk about separate compilation (section 3)

These are the theorems from section 1 and 2 but reformulated in terms of multiple C source compilation units being separately compiled to Asm units then linked together.

1 files changed, 172 insertions, 74 deletions

diff --git a/driver/Complements.v b/driver/Complements.v
index d1bea1b3..3660fff0 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -13,30 +13,20 @@
 (** Corollaries of the main semantic preservation theorem. *)
 
 Require Import Classical.
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Behaviors.
-Require Import Csyntax.
-Require Import Csem.
-Require Import Cstrategy.
-Require Import Clight.
-Require Import Cminor.
-Require Import RTL.
-Require Import Asm.
+Require Import Coqlib Errors.
+Require Import AST Linking Events Smallstep Behaviors.
+Require Import Csyntax Csem Cstrategy Asm.
 Require Import Compiler.
-Require Import Errors.
 
 (** * 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. *)
+  a behavior of the source C code.  The behavior [beh] of the assembly
+  code is either identical to the behavior [beh'] of the source C code
+  or ``improves upon'' [beh']  by replacing a ``going wrong'' behavior
+  with a more defined behavior. *)
 
 Theorem transf_c_program_preservation:
   forall p tp beh,
@@ -48,8 +38,9 @@ Proof.
   apply transf_c_program_correct; auto.
 Qed.
 
-(** 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. *)
+(** As a corollary, if the source C code cannot go wrong, i.e. is free of
+  undefined behaviors, the behavior of the generated assembly code is
+  one of the possible behaviors of the source C code. *)
 
 Theorem transf_c_program_is_refinement:
   forall p tp,
@@ -124,83 +115,190 @@ Qed.
 (** * 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),
+  of the source C program satisfies a given specification,
   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. *)
-
-Section SPECS_PRESERVED.
-
-Variable spec: program_behavior -> Prop.
+  this specification as well.  *)
+
+(** The specifications we consider here are sets of observable
+  behaviors, representing the good behaviors a program is expected
+  to have.  A specification can be as simple as
+  ``the program does not go wrong'' or as precise as
+  ``the program prints a prime number then terminates with code 0''.
+  As usual in Coq, sets of behaviors are represented as predicates
+  [program_behavior -> Prop]. *)
+
+Definition specification := program_behavior -> Prop.
+
+(** A program satisfies a specification if all its observable behaviors
+  are in the specification. *)
+
+Definition c_program_satisfies_spec (p: Csyntax.program) (spec: specification): Prop :=
+  forall beh,  program_behaves (Csem.semantics p) beh -> spec beh.
+Definition asm_program_satisfies_spec (p: Asm.program) (spec: specification): Prop :=
+  forall beh,  program_behaves (Asm.semantics p) beh -> spec beh.
+  
+(** It is not always the case that if the source program satisfies a
+  specification, then the generated assembly code satisfies it as
+  well.  For example, if the specification is ``the program goes wrong
+  on an undefined behavior'', a C source that goes wrong satisfies
+  this specification but can be compiled into Asm code that does not
+  go wrong and therefore does not satisfy the specification.
+
+  For this reason, we restrict ourselves to safety-enforcing specifications:
+  specifications that exclude ``going wrong'' behaviors and are satisfied
+  only by programs that execute safely. *)
+
+Definition safety_enforcing_specification (spec: specification): Prop :=
+  forall beh, spec beh -> not_wrong beh.
 
-Hypothesis spec_stable:
-  forall beh1 beh2, behavior_improves beh1 beh2 -> spec beh1 -> spec beh2.
+(** As the main result of this section, we show that CompCert
+  compilation preserves safety-enforcing specifications: 
+  any such specification that is satisfied by the source C program is
+  always satisfied by the generated assembly code. *)
 
 Theorem transf_c_program_preserves_spec:
-  forall p tp,
+  forall p tp spec,
   transf_c_program p = OK tp ->
-  (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) ->
-  (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh).
+  safety_enforcing_specification spec ->
+  c_program_satisfies_spec p spec ->
+  asm_program_satisfies_spec tp spec.
 Proof.
-  intros.
-  exploit transf_c_program_preservation; eauto. intros [beh' [A B]].
-  apply spec_stable with beh'; auto.
+  intros p tp spec TRANSF SES CSAT; red; intros beh AEXEC.
+  exploit transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR).
+  apply CSAT in CEXEC. destruct IMPR as [EQ | [t [A B]]].
+- congruence.
+- subst beh'. apply SES in CEXEC. contradiction. 
 Qed.
 
-End SPECS_PRESERVED.
+(** Safety-enforcing specifications are not the only good properties
+  of source programs that are preserved by compilation.  Another example
+  of a property that is preserved is the ``initial trace'' property:
+  all executions of the program start by producing an expected trace
+  of I/O actions, representing the good behavior expected from the program.
+  After that, the program may terminate, or continue running, or go wrong
+  on an undefined behavior.  What matters is that the program produced
+  the expected trace at the beginning of its execution.  This is a typical
+  liveness property, and it is preserved by compilation. *)
+
+Definition c_program_has_initial_trace (p: Csyntax.program) (t: trace): Prop :=
+  forall beh, program_behaves (Csem.semantics p) beh -> behavior_prefix t beh.
+Definition asm_program_has_initial_trace (p: Asm.program) (t: trace): Prop :=
+  forall beh, program_behaves (Asm.semantics p) beh -> behavior_prefix t beh.
+
+Theorem transf_c_program_preserves_initial_trace:
+  forall p tp t,
+  transf_c_program p = OK tp ->
+  c_program_has_initial_trace p t ->
+  asm_program_has_initial_trace tp t.
+Proof.
+  intros p tp t TRANSF CTRACE; red; intros beh AEXEC.
+  exploit transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR).
+  apply CTRACE in CEXEC. destruct IMPR as [EQ | [t' [A B]]].
+- congruence.
+- destruct CEXEC as (beh1' & EQ').
+  destruct B as (beh1 & EQ).
+  subst beh'. destruct beh1'; simpl in A; inv A. 
+  exists (behavior_app t0 beh1). apply behavior_app_assoc.
+Qed.
 
-(** As a corollary, we obtain preservation of safety specifications:
-  specifications that exclude "going wrong" behaviors. *)
+(** * Extension to separate compilation *)
 
-Section SAFETY_PRESERVED.
+(** The results above were given in terms of whole-program compilation.
+    They also extend to separate compilation followed by linking. *)
 
-Variable spec: program_behavior -> Prop.
+Section SEPARATE_COMPILATION.
 
-Hypothesis spec_safety:
-  forall beh, spec beh -> not_wrong beh.
+(** The source: a list of C compilation units *)
+Variable c_units: nlist Csyntax.program.
 
-Theorem transf_c_program_preserves_safety_spec:
-  forall p tp,
-  transf_c_program p = OK tp ->
-  (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) ->
-  (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh).
+(** The compiled code: a list of Asm compilation units, obtained by separate compilation *)
+Variable asm_units: nlist Asm.program.
+Hypothesis separate_compilation_succeeds: 
+  nlist_forall2 (fun cu tcu => transf_c_program cu = OK tcu) c_units asm_units.
+
+(** We assume that the source C compilation units can be linked together
+    to obtain a monolithic C program [c_program]. *)
+Variable c_program: Csyntax.program.
+Hypothesis source_linking: link_list c_units = Some c_program.
+
+(** Then, linking the Asm units obtained by separate compilation succeeds. *)
+Lemma compiled_linking_succeeds:
+  { asm_program | link_list asm_units = Some asm_program }.
 Proof.
-  intros. eapply transf_c_program_preserves_spec; eauto.
-  intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]].
-  subst beh1. elim (spec_safety _ H3).
+  destruct (link_list asm_units) eqn:E. 
+- exists p; auto.
+- exfalso. 
+  exploit separate_transf_c_program_correct; eauto. intros (a & P & Q).
+  congruence.
 Qed.
 
-End SAFETY_PRESERVED.
+(** Let asm_program be the result of linking the Asm units. *)
+Let asm_program: Asm.program := proj1_sig compiled_linking_succeeds.
+Let compiled_linking: link_list asm_units = Some asm_program := proj2_sig compiled_linking_succeeds.
+
+(** Then, [asm_program] preserves the semantics and the specifications of
+  [c_program], in the following sense.
+  First, every behavior of [asm_program] improves upon one of the possible
+  behaviors of [c_program]. *)
 
-(** We also have preservation of liveness specifications:
-  specifications that assert the existence of a prefix of the observable
-  trace satisfying some conditions. *)
+Theorem separate_transf_c_program_preservation:
+  forall beh,
+  program_behaves (Asm.semantics asm_program) beh ->
+  exists beh', program_behaves (Csem.semantics c_program) beh' /\ behavior_improves beh' beh.
+Proof.
+  intros. exploit separate_transf_c_program_correct; eauto. intros (a & P & Q).
+  assert (a = asm_program) by congruence. subst a. 
+  eapply backward_simulation_behavior_improves; eauto.
+Qed.
 
-Section LIVENESS_PRESERVED.
+(** As a corollary, if [c_program] is free of undefined behaviors, 
+  the behavior of [asm_program] is one of the possible behaviors of [c_program]. *)
 
-Variable spec: trace -> Prop.
+Theorem separate_transf_c_program_is_refinement:
+  (forall beh, program_behaves (Csem.semantics c_program) beh -> not_wrong beh) ->
+  (forall beh, program_behaves (Asm.semantics asm_program) beh -> program_behaves (Csem.semantics c_program) beh).
+Proof.
+  intros. exploit separate_transf_c_program_preservation; eauto. intros (beh' & P & Q).
+  assert (not_wrong beh') by auto.
+  inv Q.
+- auto.
+- destruct H2 as (t & U & V). subst beh'. elim H1. 
+Qed.
 
-Definition liveness_spec_satisfied (b: program_behavior) : Prop :=
-  exists t, behavior_prefix t b /\ spec t.
+(** We now show that if all executions of [c_program] satisfy a specification,
+  then all executions of [asm_program] also satisfy the specification, provided
+  the specification is of the safety-enforcing kind. *)
 
-Theorem transf_c_program_preserves_liveness_spec:
-  forall p tp,
-  transf_c_program p = OK tp ->
-  (forall beh, program_behaves (Csem.semantics p) beh -> liveness_spec_satisfied beh) ->
-  (forall beh, program_behaves (Asm.semantics tp) beh -> liveness_spec_satisfied beh).
+Theorem separate_transf_c_program_preserves_spec:
+  forall spec,
+  safety_enforcing_specification spec ->
+  c_program_satisfies_spec c_program spec ->
+  asm_program_satisfies_spec asm_program spec.
 Proof.
-  intros. eapply transf_c_program_preserves_spec; eauto.
-  intros. destruct H3 as [t1 [A B]]. destruct H2.
-  subst. exists t1; auto.
-  destruct H2 as [t [C D]]. subst.
-  destruct A as [b1 E]. destruct D as [b2 F].
-  destruct b1; simpl in E; inv E.
-  exists t1; split; auto.
-  exists (behavior_app t0 b2); apply behavior_app_assoc.
+  intros spec SES CSAT; red; intros beh AEXEC.
+  exploit separate_transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR).
+  apply CSAT in CEXEC. destruct IMPR as [EQ | [t [A B]]].
+- congruence.
+- subst beh'. apply SES in CEXEC. contradiction. 
 Qed.
 
-End LIVENESS_PRESERVED.
+(** As another corollary of [separate_transf_c_program_preservation],
+  if all executions of [c_program] have a trace [t] as initial trace,
+  so do all executions of [asm_program]. *)
+
+Theorem separate_transf_c_program_preserves_initial_trace:
+  forall t,
+  c_program_has_initial_trace c_program t ->
+  asm_program_has_initial_trace asm_program t.
+Proof.
+  intros t CTRACE; red; intros beh AEXEC.
+  exploit separate_transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR).
+  apply CTRACE in CEXEC. destruct IMPR as [EQ | [t' [A B]]].
+- congruence.
+- destruct CEXEC as (beh1' & EQ').
+  destruct B as (beh1 & EQ).
+  subst beh'. destruct beh1'; simpl in A; inv A. 
+  exists (behavior_app t0 beh1). apply behavior_app_assoc.
+Qed.
 
+End SEPARATE_COMPILATION.