Merge of branch new-semantics: revised and strengthened top-level statements of semantic preservation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 130 insertions, 174 deletions

diff --git a/driver/Complements.v b/driver/Complements.v
index e6b0095d..1b7e9744 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -20,223 +20,179 @@ Require Import Values.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
-Require Import Determinism.
+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 Compiler.
 Require Import Errors.
 
-(** * Integrating a deterministic external world *)
+(** * Preservation of whole-program behaviors *)
 
-(** We now integrate a deterministic external world in the semantics
-  of Compcert C and Asm. *)
+(** 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. *)
 
-Section WORLD.
-
-Variable initial_world: world.
-
-Definition exec_C_program (p: Csyntax.program) (beh: program_behavior) : Prop :=
-  wprogram_behaves _ _
-      Csem.step (Csem.initial_state p) Csem.final_state
-      initial_world (Genv.globalenv p) beh.
-
-Definition exec_asm_program (p: Asm.program) (beh: program_behavior) : Prop :=
-  wprogram_behaves _ _
-      Asm.step (Asm.initial_state p) Asm.final_state
-      initial_world (Genv.globalenv p) beh.
-
-(** ** Safety of C programs. *)
+Theorem transf_c_program_preservation:
+  forall p tp beh,
+  transf_c_program p = OK tp ->
+  program_behaves (Asm.semantics tp) beh ->
+  exists beh', program_behaves (Csem.semantics p) beh' /\ behavior_improves beh' beh.
+Proof.
+  intros. eapply backward_simulation_behavior_improves; eauto. 
+  apply transf_c_program_correct; auto.
+Qed.
 
-(** We show that a C program is safe (in the sense of [Cstrategy.safeprog])
-  if it cannot go wrong in the world-aware semantics. *)
+(** 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. *)
 
-Lemma notwrong_safeprog:
-  forall p,
-  (forall beh, exec_C_program p beh -> not_wrong beh) ->
-  Cstrategy.safeprog p initial_world.
+Theorem transf_c_program_is_refinement:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  (forall beh, program_behaves (Csem.semantics p) beh -> not_wrong beh) ->
+  (forall beh, program_behaves (Asm.semantics tp) beh -> program_behaves (Csem.semantics p) beh).
 Proof.
-  intros; red.
-  assert (exists beh1, exec_C_program p beh1).
-    unfold exec_C_program. apply program_behaves_exists. 
-  destruct H0 as [beh1 A].
-  assert (B: not_wrong beh1) by auto.
-  split.
-  inv A; simpl in B.
-  destruct H0. exists (fst s); auto.
-  destruct H0. exists (fst s); auto.
-  destruct H0. exists (fst s); auto.
-  contradiction.
-  contradiction.
-  intros; red; intros.
-  destruct (classic (exists r, Csem.final_state s' r)).
-  (* 1. Final state.  This is immsafe. *)
-  destruct H3 as [r F]. eapply immsafe_final; eauto. 
-  (* 2. Not a final state. *)
-  destruct (classic (nostep (wstep _ _ Csem.step) (Genv.globalenv p) (s', w'))).
-  (* 2.1 No step possible -> going wrong *)
-  elim (H (Goes_wrong t)). 
-  eapply program_goes_wrong.
-  instantiate (1 := (s, initial_world)). split; auto.
-  instantiate (1 := (s', w')). apply Determinism.inject_star; auto. 
-  auto.
-  intros; red; intros. elim H3. exists r; auto. 
-  (* 2.2 One step possible -> this is immsafe *)
-  unfold nostep in H4. 
-  generalize (not_all_ex_not _ _ H4). clear H4. intros [t' P].
-  generalize (not_all_ex_not _ _ P). clear P. intros [s'' Q].
-  generalize (NNPP _ Q). clear Q. intros R. destruct R as [R1 R2]. simpl in *.
-  eapply immsafe_step. eauto. eauto. 
+  intros. eapply backward_simulation_same_safe_behavior; eauto.
+  apply transf_c_program_correct; auto.
 Qed.
 
-(** ** Determinism of Asm semantics *)
+(** If we consider the C evaluation strategy implemented by the compiler,
+  we get stronger preservation results. *)
 
-Remark extcall_arguments_deterministic:
-  forall rs m sg args args',
-  extcall_arguments rs m sg args ->
-  extcall_arguments rs m sg args' -> args = args'.
+Theorem transf_cstrategy_program_preservation:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  (forall beh, program_behaves (Cstrategy.semantics p) beh ->
+     exists beh', program_behaves (Asm.semantics tp) beh' /\ behavior_improves beh beh')
+/\(forall beh, program_behaves (Asm.semantics tp) beh ->
+     exists beh', program_behaves (Cstrategy.semantics p) beh' /\ behavior_improves beh' beh)
+/\(forall beh, not_wrong beh ->
+     program_behaves (Cstrategy.semantics p) beh -> program_behaves (Asm.semantics tp) beh)
+/\(forall beh,
+     (forall beh', program_behaves (Cstrategy.semantics p) beh' -> not_wrong beh') ->
+     program_behaves (Asm.semantics tp) beh ->
+     program_behaves (Cstrategy.semantics p) beh).
 Proof.
-  unfold extcall_arguments; intros. 
-  revert args H args' H0. generalize (Conventions1.loc_arguments sg); induction 1; intros.
-  inv H0; auto.
-  inv H1; decEq; auto. inv H; inv H4; congruence. 
+  intros. intuition.
+  eapply forward_simulation_behavior_improves; eauto. 
+    apply (fst (transf_cstrategy_program_correct _ _ H)).
+  eapply backward_simulation_behavior_improves; eauto. 
+    apply (snd (transf_cstrategy_program_correct _ _ H)).
+  eapply forward_simulation_same_safe_behavior; eauto.
+    apply (fst (transf_cstrategy_program_correct _ _ H)).
+  eapply backward_simulation_same_safe_behavior; eauto.
+    apply (snd (transf_cstrategy_program_correct _ _ H)).
 Qed.
 
-Remark annot_arguments_deterministic:
-  forall rs m pl args args',
-  annot_arguments rs m pl args ->
-  annot_arguments rs m pl args' -> args = args'.
+(** We can also use the alternate big-step semantics for [Cstrategy]
+  to establish behaviors of the generated assembly code. *)
+
+Theorem bigstep_cstrategy_preservation:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  (forall t r,
+     Cstrategy.bigstep_program_terminates p t r ->
+     program_behaves (Asm.semantics tp) (Terminates t r))
+/\(forall T,
+     Cstrategy.bigstep_program_diverges p T ->
+       program_behaves (Asm.semantics tp) (Reacts T)
+    \/ exists t, program_behaves (Asm.semantics tp) (Diverges t) /\ traceinf_prefix t T).
 Proof.
-  unfold annot_arguments; intros. 
-  revert pl args H args' H0. induction 1; intros.
-  inv H0; auto.
-  inv H1; decEq; auto. inv H; inv H4; congruence. 
+  intuition.
+  apply transf_cstrategy_program_preservation with p; auto. red; auto.
+  apply behavior_bigstep_terminates with (Cstrategy.bigstep_semantics p); auto.
+  apply Cstrategy.bigstep_semantics_sound.
+  exploit (behavior_bigstep_diverges (Cstrategy.bigstep_semantics_sound p)). eassumption.
+  intros [A | [t [A B]]]. 
+  left. apply transf_cstrategy_program_preservation with p; auto. red; auto.
+  right; exists t; split; auto. apply transf_cstrategy_program_preservation with p; auto. red; auto.
 Qed.
 
-Lemma step_internal_deterministic:
-  forall ge s t1 s1 t2 s2,
-  Asm.step ge s t1 s1 -> Asm.step ge s t2 s2 -> matching_traces t1 t2 ->
-  s1 = s2 /\ t1 = t2.
-Proof.
+(** * Satisfaction of specifications *)
 
-Ltac InvEQ :=
-  match goal with
-  | [ H1: ?x = ?y, H2: ?x = ?z |- _ ] => rewrite H1 in H2; inv H2; InvEQ
-  | _ => idtac
-  end.
-
-  intros. inv H; inv H0; InvEQ.
-(* regular, regular *)
-  split; congruence.
-(* regular, builtin *)
-  simpl in H5; inv H5.
-(* regular, annot *)
-  simpl in H5; inv H5.
-(* builtin, regular *)
-  simpl in H12; inv H12.
-(* builtin, builtin *)
-  exploit external_call_determ. eexact H5. eexact H12. auto. intros [A [B C]]. subst.
-  auto.
-(* annot, regular *)
-  simpl in H13. inv H13.
-(* annot, annot *)
-  exploit annot_arguments_deterministic. eexact H5. eexact H11. intros EQ; subst. 
-  exploit external_call_determ. eexact H6. eexact H14. auto. intros [A [B C]]. subst.
-  auto.
-(* extcall, extcall *)
-  exploit extcall_arguments_deterministic. eexact H5. eexact H10. intros EQ; subst.
-  exploit external_call_determ. eexact H4. eexact H9. auto. intros [A [B C]]. subst.
-  auto.
-Qed.
+(** 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.  
 
-Lemma initial_state_deterministic:
-  forall p s1 s2,
-  initial_state p s1 -> initial_state p s2 -> s1 = s2.
-Proof.
-  intros. inv H; inv H0. f_equal. congruence.
-Qed.
+  We first show this result for specifications that are stable
+  under the [behavior_improves] relation. *) 
 
-Lemma final_state_not_step:
-  forall ge st r, final_state st r -> nostep step ge st.
-Proof.
-  unfold nostep. intros. red; intros. inv H. inv H0; unfold Vzero in H1; congruence.
-Qed.
+Section SPECS_PRESERVED.
 
-Lemma final_state_deterministic:
-  forall st r1 r2, final_state st r1 -> final_state st r2 -> r1 = r2.
-Proof.
-  intros. inv H; inv H0. congruence.
-Qed.
+Variable spec: program_behavior -> Prop.
+
+Hypothesis spec_stable:
+  forall beh1 beh2, behavior_improves beh1 beh2 -> spec beh1 -> spec beh2.
 
-Theorem asm_exec_program_deterministic:
-  forall p beh1 beh2,
-  exec_asm_program p beh1 -> exec_asm_program p beh2 ->
-  beh1 = beh2.
+Theorem transf_c_program_preserves_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).
 Proof.
-  intros. hnf in H; hnf in H0.
-  eapply (program_behaves_deterministic _ _
-             (wstep _ _ step)
-             (winitial_state _ (initial_state p) initial_world)
-             (wfinal_state _ final_state));
-  eauto.
-  apply wstep_deterministic. apply step_internal_deterministic.
-  apply winitial_state_determ. apply initial_state_deterministic.
-  apply wfinal_state_determ. apply final_state_deterministic.
-  apply wfinal_state_nostep. apply final_state_not_step.
+  intros.
+  exploit transf_c_program_preservation; eauto. intros [beh' [A B]].
+  apply spec_stable with beh'; auto. 
 Qed.
 
-(** * Additional semantic preservation property *)
+End SPECS_PRESERVED.
+
+(** As a corollary, we obtain preservation of safety specifications:
+  specifications that exclude "going wrong" behaviors. *)
 
-(** Combining the semantic preservation theorem from module [Compiler]
-  with the determinism of Asm executions, we easily obtain
-  additional, stronger semantic preservation properties.
-  The first property states that, when compiling a Compcert C
-  program that has well-defined semantics, all possible executions
-  of the resulting Asm code correspond to an execution of
-  the source program. *)
+Section SAFETY_PRESERVED.
 
-Theorem transf_c_program_is_refinement:
+Variable spec: program_behavior -> Prop.
+
+Hypothesis spec_safety:
+  forall beh, spec beh -> not_wrong beh.
+
+Theorem transf_c_program_preserves_safety_spec:
   forall p tp,
   transf_c_program p = OK tp ->
-  (forall beh, exec_C_program p beh -> not_wrong beh) ->
-  (forall beh, exec_asm_program tp beh -> exec_C_program p beh).
+  (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) ->
+  (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh).
 Proof.
-  intros. 
-  exploit Cstrategy.strategy_behavior.
-  apply notwrong_safeprog. eauto. 
-  intros [beh1 [A [B [C D]]]].
-  assert (Asm.exec_program tp beh1).
-    eapply transf_c_program_correct; eauto.
-  assert (exec_asm_program tp beh1).
-    red. apply inject_behaviors; auto.
-  assert (beh = beh1). eapply asm_exec_program_deterministic; eauto.
-  subst beh.
-  red. apply inject_behaviors; auto.
+  intros. eapply transf_c_program_preserves_spec; eauto. 
+  intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]]. 
+  subst beh1. elim (spec_safety _ H3). 
 Qed.
 
-Section SPECS_PRESERVED.
+End SAFETY_PRESERVED.
 
-(** The second additional results shows that if one execution
-  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 also have preservation of liveness specifications:
+  specifications that assert the existence of a prefix of the observable
+  trace satisfying some conditions. *)
 
-Variable spec: program_behavior -> Prop.
+Section LIVENESS_PRESERVED.
 
-Hypothesis spec_not_wrong: forall b, spec b -> not_wrong b.
+Variable spec: trace -> Prop.
 
-Theorem transf_c_program_preserves_spec:
+Definition liveness_spec_satisfied (b: program_behavior) : Prop :=
+  exists t, behavior_prefix t b /\ spec t.
+
+Theorem transf_c_program_preserves_liveness_spec:
   forall p tp,
   transf_c_program p = OK tp ->
-  (forall beh, exec_C_program p beh -> spec beh) ->
-  (forall beh, exec_asm_program tp beh -> spec beh).
+  (forall beh, program_behaves (Csem.semantics p) beh -> liveness_spec_satisfied beh) ->
+  (forall beh, program_behaves (Asm.semantics tp) beh -> liveness_spec_satisfied beh).
 Proof.
-  intros. apply H0. apply transf_c_program_is_refinement with tp; auto. 
+  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. 
 Qed.
 
-End SPECS_PRESERVED.
-
-End WORLD.
+End LIVENESS_PRESERVED.