From 93b89122000e42ac57abc39734fdf05d3a89e83c Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Jul 2011 08:26:16 +0000 Subject: 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 --- backend/Allocproof.v | 7 ++--- backend/CSEproof.v | 7 ++--- backend/CastOptimproof.v | 10 +++--- backend/CleanupLabelsproof.v | 7 ++--- backend/Cminor.v | 75 ++++++++++++++++++++------------------------ backend/CminorSel.v | 4 +-- backend/Constpropproof.v | 10 +++--- backend/LTL.v | 4 +-- backend/LTLin.v | 4 +-- backend/Linear.v | 4 +-- backend/Linearizeproof.v | 7 ++--- backend/Machsem.v | 4 +-- backend/RTL.v | 26 +++++++++++++-- backend/RTLgenproof.v | 30 ++++++------------ backend/Reloadproof.v | 7 ++--- backend/Selectionproof.v | 7 ++--- backend/Stackingproof.v | 7 ++--- backend/Tailcallproof.v | 10 +++--- backend/Tunnelingproof.v | 29 +++++++++-------- 19 files changed, 125 insertions(+), 134 deletions(-) (limited to 'backend') 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. -- cgit v1.2.3