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

19 files changed, 125 insertions, 134 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index e7d9995..ae86ee8 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -797,11 +797,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  RTL.exec_program prog beh -> LTL.exec_program tprog beh.
+  forward_simulation (RTL.semantics prog) (LTL.semantics tprog).
 Proof.
-  unfold RTL.exec_program, LTL.exec_program; intros.
-  eapply simulation_step_preservation; eauto.
+  eapply forward_simulation_step.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact transl_step_correct. 
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 53576ad..77da538 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -968,11 +968,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  exec_program prog beh -> exec_program tprog beh.
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
 Proof.
-  unfold exec_program; intros.
-  eapply simulation_step_preservation; eauto.
+  eapply forward_simulation_step.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact transf_step_correct. 
diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v
index ab04d0e..0afc208 100644
--- a/backend/CastOptimproof.v
+++ b/backend/CastOptimproof.v
@@ -560,15 +560,13 @@ Proof.
 Qed.
 
 (** The preservation of the observable behavior of the program then
-  follows, using the generic preservation theorem
-  [Smallstep.simulation_step_preservation]. *)
+  follows. *)
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  exec_program prog beh -> exec_program tprog beh.
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
 Proof.
-  unfold exec_program; intros.
-  eapply simulation_step_preservation; eauto.
+  eapply forward_simulation_step.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact transf_step_correct. 
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index abd2581..a7a60f6 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -324,11 +324,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  exec_program prog beh -> LTLin.exec_program tprog beh.
+  forward_simulation (LTLin.semantics prog) (LTLin.semantics tprog).
 Proof.
-  unfold exec_program; intros.
-  eapply simulation_opt_preservation; eauto.
+  eapply forward_simulation_opt.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   eexact transf_step_correct.
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 45e060d..45efdf9 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -529,13 +529,26 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate (Vint r) Kstop m) r.
 
-(** Execution of a whole program: [exec_program p beh]
-  holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] has [beh] as observable
-  behavior. *)
+(** The corresponding small-step semantics. *)
 
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
+
+(** This semantics is receptive to changes in events. *)
+
+Lemma semantics_receptive:
+  forall (p: program), receptive (semantics p).
+Proof.
+  intros. constructor; simpl; intros.
+(* receptiveness *)
+  assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2).
+    intros. subst. inv H0. exists s1; auto.
+  inversion H; subst; auto.
+  exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
+  exists (Returnstate vres2 k m2). econstructor; eauto.
+(* trace length *)
+  inv H; simpl; try omega. eapply external_call_trace_length; eauto.
+Qed.
 
 (** * Alternate operational semantics (big-step) *)
 
@@ -697,17 +710,6 @@ Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop
 Combined Scheme eval_funcall_exec_stmt_ind2 
   from eval_funcall_ind2, exec_stmt_ind2.
 
-(*
-Definition eval_funcall_exec_stmt_ind2 
-  (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop)
-  (P2: val -> env -> mem -> stmt -> trace ->
-              env -> mem -> outcome -> Prop) :=
-  fun a b c d e f g h i j k l m n o p q =>
-  conj
-    (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q)
-    (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q).
-*)
-
 (** Coinductive semantics for divergence.
   [evalinf_funcall ge m f args t]
   means that the function [f] diverges when applied to the arguments [args] in
@@ -804,6 +806,9 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
       evalinf_funcall ge m0 f nil t ->
       bigstep_program_diverges p t.
 
+Definition bigstep_semantics (p: program) :=
+  Bigstep_semantics (bigstep_program_terminates p) (bigstep_program_diverges p).
+
 (** ** Correctness of the big-step semantics with respect to the transition semantics *)
 
 Section BIGSTEP_TO_TRANSITION.
@@ -1102,32 +1107,20 @@ Proof.
   traceEq.
 Qed.
 
-Theorem bigstep_program_terminates_exec:
-  forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
+Theorem bigstep_semantics_sound:
+  bigstep_sound (bigstep_semantics prog) (semantics prog).
 Proof.
-  intros. inv H.
-  econstructor.
-  econstructor; eauto. 
-  apply eval_funcall_steps. eauto. red; auto. 
+  constructor; intros.
+(* termination *)
+  inv H. econstructor; econstructor.
+  split. econstructor; eauto. 
+  split. apply eval_funcall_steps. eauto. red; auto. 
   econstructor.
-Qed.
-
-Theorem bigstep_program_diverges_exec:
-  forall T, bigstep_program_diverges prog T ->
-  exec_program prog (Reacts T) \/
-  exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T.
-Proof.
-  intros. inv H.
-  set (st := Callstate f nil Kstop m0).
-  assert (forever step ge0 st T). 
-    eapply forever_plus_forever.
-    eapply evalinf_funcall_forever; eauto. 
-  destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
-  as [A | [t [s' [T' [B [C D]]]]]]. 
-  left. econstructor. econstructor; eauto. auto.
-  right. exists t. split.
-  econstructor. econstructor; eauto. eauto. auto.  
-  subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
+(* divergence *)
+  inv H. econstructor.
+  split. econstructor; eauto. 
+  eapply forever_plus_forever.
+  eapply evalinf_funcall_forever; eauto.
 Qed.
 
 End BIGSTEP_TO_TRANSITION.
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 8a82c42..84b47f3 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -384,8 +384,8 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate (Vint r) Kstop m) r.
 
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
 
 Hint Constructors eval_expr eval_condexpr eval_exprlist: evalexpr.
 
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index d534c75..058d68e 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -468,15 +468,13 @@ Proof.
 Qed.
 
 (** The preservation of the observable behavior of the program then
-  follows, using the generic preservation theorem
-  [Smallstep.simulation_step_preservation]. *)
+  follows. *)
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  exec_program prog beh -> exec_program tprog beh.
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
 Proof.
-  unfold exec_program; intros.
-  eapply simulation_step_preservation; eauto.
+  eapply forward_simulation_step.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact transf_step_correct. 
diff --git a/backend/LTL.v b/backend/LTL.v
index 6e3effd..5ed0a8f 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -267,8 +267,8 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall n m,
       final_state (Returnstate nil (Vint n) m) n.
 
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
 
 (** * Operations over LTL *)
 
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 5f12390..390c4cf 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -254,8 +254,8 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall n m,
       final_state (Returnstate nil (Vint n) m) n.
 
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
 
 (** * Properties of the operational semantics *)
 
diff --git a/backend/Linear.v b/backend/Linear.v
index 23f0324..3553ced 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -367,5 +367,5 @@ Inductive final_state: state -> int -> Prop :=
       rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
       final_state (Returnstate nil rs m) r.
 
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index abc497e..2f96a09 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -743,11 +743,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  LTL.exec_program prog beh -> LTLin.exec_program tprog beh.
+  forward_simulation (LTL.semantics prog) (LTLin.semantics tprog).
 Proof.
-  unfold LTL.exec_program, exec_program; intros.
-  eapply simulation_plus_preservation; eauto.
+  eapply forward_simulation_plus.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   eexact transf_step_correct.
diff --git a/backend/Machsem.v b/backend/Machsem.v
index fe0ec37..853e8a7 100644
--- a/backend/Machsem.v
+++ b/backend/Machsem.v
@@ -272,5 +272,5 @@ Inductive final_state: state -> int -> Prop :=
       rs (loc_result (mksignature nil (Some Tint))) = Vint r ->
       final_state (Returnstate nil rs m) r.
 
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
diff --git a/backend/RTL.v b/backend/RTL.v
index 2cb2719..10d4a3f 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -345,8 +345,30 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate nil (Vint r) m) r.
 
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+(** The small-step semantics for a program. *)
+
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
+
+(** This semantics is receptive to changes in events. *)
+
+Lemma semantics_receptive:
+  forall (p: program), receptive (semantics p).
+Proof.
+  intros. constructor; simpl; intros.
+(* receptiveness *)
+  assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2).
+    intros. subst. inv H0. exists s1; auto.
+  inversion H; subst; auto.
+  exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
+  exists (State s0 f sp pc' (rs#res <- vres2) m2). eapply exec_Ibuiltin; eauto.
+  exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
+  exists (Returnstate s0 vres2 m2). econstructor; eauto.
+(* trace length *)
+  inv H; simpl; try omega.
+  eapply external_call_trace_length; eauto.
+  eapply external_call_trace_length; eauto.
+Qed.
 
 (** * Operations on RTL abstract syntax *)
 
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index e72b000..55cdd6b 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -906,21 +906,12 @@ Fixpoint size_cont (k: cont) : nat :=
 
 Definition measure_state (S: CminorSel.state) :=
   match S with
-  | CminorSel.State _ s k _ _ _ =>
-      existS (fun (x: nat) => nat)
-             (size_stmt s + size_cont k)
-             (size_stmt s)
-  | _ =>
-      existS (fun (x: nat) => nat) 0 0
+  | CminorSel.State _ s k _ _ _ => (size_stmt s + size_cont k, size_stmt s)
+  | _                           => (0, 0)
   end.
 
-Require Import Relations.
-Require Import Wellfounded.
-
 Definition lt_state (S1 S2: CminorSel.state) :=
-  lexprod nat (fun (x: nat) => nat)
-          lt (fun (x: nat) => lt)
-          (measure_state S1) (measure_state S2).
+  lex_ord lt lt (measure_state S1) (measure_state S2).
 
 Lemma lt_state_intro:
   forall f1 s1 k1 sp1 e1 m1 f2 s2 k2 sp2 e2 m2,
@@ -931,20 +922,20 @@ Lemma lt_state_intro:
            (CminorSel.State f2 s2 k2 sp2 e2 m2).
 Proof.
   intros. unfold lt_state. simpl. destruct H as [A | [A B]].
-  apply left_lex. auto.
-  rewrite A. apply right_lex. auto.
+  left. auto.
+  rewrite A. right. auto.
 Qed.
 
 Ltac Lt_state :=
   apply lt_state_intro; simpl; try omega.
 
-Require Import Wf_nat.
+Require Import Wellfounded.
 
 Lemma lt_state_wf:
   well_founded lt_state.
 Proof.
   unfold lt_state. apply wf_inverse_image with (f := measure_state).
-  apply wf_lexprod. apply lt_wf. intros. apply lt_wf. 
+  apply wf_lex_ord. apply lt_wf. apply lt_wf. 
 Qed.
 
 (** ** Semantic preservation for the translation of statements *)   
@@ -1345,11 +1336,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  CminorSel.exec_program prog beh -> RTL.exec_program tprog beh.
+  forward_simulation (CminorSel.semantics prog) (RTL.semantics tprog).
 Proof.
-  unfold CminorSel.exec_program, RTL.exec_program; intros.
-  eapply simulation_star_wf_preservation with (order := lt_state); eauto.
+  eapply forward_simulation_star_wf with (order := lt_state).
+  eexact symbols_preserved.
   eexact transl_initial_states.
   eexact transl_final_states.
   apply lt_state_wf. 
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 49640a3..f0a0b97 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -1431,11 +1431,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  LTLin.exec_program prog beh -> Linear.exec_program tprog beh.
+  forward_simulation (LTLin.semantics prog) (Linear.semantics tprog).
 Proof.
-  unfold LTLin.exec_program, Linear.exec_program; intros.
-  eapply simulation_star_preservation; eauto.
+  eapply forward_simulation_star.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   eexact transf_step_correct. 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index d475f26..d6c850a 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -565,11 +565,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh.
+  forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog).
 Proof.
-  unfold CminorSel.exec_program, Cminor.exec_program; intros.
-  eapply simulation_opt_preservation; eauto.
+  eapply forward_simulation_opt.
+  eexact symbols_preserved.
   eexact sel_initial_states.
   eexact sel_final_states.
   eexact sel_step_correct. 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index fbe8882..a2c8ecd 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -2701,11 +2701,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  Linear.exec_program prog beh -> Machsem.exec_program tprog beh.
+  forward_simulation (Linear.semantics prog) (Machsem.semantics tprog).
 Proof.
-  unfold Linear.exec_program, Machsem.exec_program; intros.
-  eapply simulation_plus_preservation; eauto.
+  eapply forward_simulation_plus.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   eexact transf_step_correct. 
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index ca8e915..f3dd9ed 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -616,15 +616,13 @@ Qed.
 
 
 (** The preservation of the observable behavior of the program then
-  follows, using the generic preservation theorem
-  [Smallstep.simulation_opt_preservation]. *)
+  follows. *)
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  exec_program prog beh -> exec_program tprog beh.
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
 Proof.
-  unfold exec_program; intros.
-  eapply simulation_opt_preservation with (measure := measure); eauto.
+  eapply forward_simulation_opt with (measure := measure); eauto.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact transf_step_correct. 
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 9a14158..8ff7347 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -138,31 +138,31 @@ Qed.
 
 Section PRESERVATION.
 
-Variable p: program.
-Let tp := tunnel_program p.
-Let ge := Genv.globalenv p.
-Let tge := Genv.globalenv tp.
+Variable prog: program.
+Let tprog := tunnel_program prog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
 
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   Genv.find_funct tge v = Some (tunnel_fundef f).
-Proof (@Genv.find_funct_transf _ _ _ tunnel_fundef p).
+Proof (@Genv.find_funct_transf _ _ _ tunnel_fundef prog).
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   Genv.find_funct_ptr tge v = Some (tunnel_fundef f).
-Proof (@Genv.find_funct_ptr_transf _ _ _ tunnel_fundef p).
+Proof (@Genv.find_funct_ptr_transf _ _ _ tunnel_fundef prog).
 
 Lemma symbols_preserved:
   forall id,
   Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef p).
+Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef prog).
 
 Lemma varinfo_preserved:
   forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof (@Genv.find_var_info_transf _ _ _ tunnel_fundef p).
+Proof (@Genv.find_var_info_transf _ _ _ tunnel_fundef prog).
 
 Lemma sig_preserved:
   forall f, funsig (tunnel_fundef f) = funsig f.
@@ -358,14 +358,14 @@ Proof.
 Qed.
 
 Lemma transf_initial_states:
-  forall st1, initial_state p st1 ->
-  exists st2, initial_state tp st2 /\ match_states st1 st2.
+  forall st1, initial_state prog st1 ->
+  exists st2, initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. 
   exists (Callstate nil (tunnel_fundef f) nil m0); split.
   econstructor; eauto.
   apply Genv.init_mem_transf; auto.
-  change (prog_main tp) with (prog_main p).
+  change (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
   apply function_ptr_translated; auto.
   rewrite <- H3. apply sig_preserved. 
@@ -380,11 +380,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  exec_program p beh -> exec_program tp beh.
+  forward_simulation (LTL.semantics prog) (LTL.semantics tprog).
 Proof.
-  unfold exec_program; intros.
-  eapply simulation_opt_preservation; eauto.
+  eapply forward_simulation_opt.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   eexact tunnel_step_correct.