diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-15 08:26:16 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-15 08:26:16 +0000 |
commit | 93b89122000e42ac57abc39734fdf05d3a89e83c (patch) | |
tree | 43bbde048cff6f58ffccde99b862dce0891b641d /driver | |
parent | 5fccbcb628c5282cf1b13077d5eeccf497d58c38 (diff) | |
download | compcert-93b89122000e42ac57abc39734fdf05d3a89e83c.tar.gz compcert-93b89122000e42ac57abc39734fdf05d3a89e83c.zip |
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
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Compiler.v | 179 | ||||
-rw-r--r-- | driver/Complements.v | 304 |
2 files changed, 250 insertions, 233 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index d8810a4c..a51cd8ff 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -171,15 +171,19 @@ Definition transf_cminor_program (p: Cminor.program) : res Asm.program := @@ Selection.sel_program @@@ transform_partial_program transf_cminorsel_fundef. -Definition transf_c_program (p: Csyntax.program) : res Asm.program := +Definition transf_clight_program (p: Clight.program) : res Asm.program := OK p - @@ print print_Csyntax - @@@ SimplExpr.transl_program @@ print print_Clight @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ transf_cminor_program. +Definition transf_c_program (p: Csyntax.program) : res Asm.program := + OK p + @@ print print_Csyntax + @@@ SimplExpr.transl_program + @@@ transf_clight_program. + (** Force [Initializers] to be extracted as well. *) Definition transl_init := Initializers.transl_init. @@ -199,16 +203,18 @@ Lemma map_partial_compose: (f1: A -> res B) (f2: B -> res C) (pa: list (X * A)) (pc: list (X * C)), map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc -> - exists pb, map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc. + { pb | map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc }. Proof. induction pa; simpl. intros. inv H. econstructor; eauto. intro pc. destruct a as [x a]. - caseEq (f1 a); simpl; try congruence. intros b F1. - caseEq (f2 b); simpl; try congruence. intros c F2 EQ. - monadInv EQ. exploit IHpa; eauto. intros [pb [P Q]]. + destruct (f1 a) as [] _eqn; simpl; try congruence. + destruct (f2 b) as [] _eqn; simpl; try congruence. + destruct (map_partial ctx (fun f => f1 f @@@ f2) pa) as [] _eqn; simpl; try congruence. + intros. inv H. + destruct (IHpa l) as [pb [P Q]]; auto. rewrite P; simpl. - exists ((x, b) :: pb); split. auto. simpl. rewrite F2. rewrite Q. auto. + econstructor; split. eauto. simpl. rewrite Heqr0. rewrite Q. auto. Qed. Lemma transform_partial_program_compose: @@ -216,11 +222,13 @@ Lemma transform_partial_program_compose: (f1: A -> res B) (f2: B -> res C) (pa: program A V) (pc: program C V), transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc -> - exists pb, transform_partial_program f1 pa = OK pb /\ - transform_partial_program f2 pb = OK pc. + { pb | transform_partial_program f1 pa = OK pb /\ + transform_partial_program f2 pb = OK pc }. Proof. - intros. monadInv H. - exploit map_partial_compose; eauto. intros [xb [P Q]]. + intros. unfold transform_partial_program in H. + destruct (map_partial prefix_name (fun f : A => f1 f @@@ f2) (prog_funct pa)) as [] _eqn; + simpl in H; inv H. + destruct (map_partial_compose _ _ _ _ _ _ _ _ _ Heqr) as [xb [P Q]]. exists (mkprogram xb (prog_main pa) (prog_vars pa)); split. unfold transform_partial_program. rewrite P; auto. unfold transform_partial_program. simpl. rewrite Q; auto. @@ -240,14 +248,14 @@ Lemma transform_program_compose: (f1: A -> res B) (f2: B -> C) (pa: program A V) (pc: program C V), transform_partial_program (fun f => f1 f @@ f2) pa = OK pc -> - exists pb, transform_partial_program f1 pa = OK pb /\ - transform_program f2 pb = pc. + { pb | transform_partial_program f1 pa = OK pb /\ + transform_program f2 pb = pc }. Proof. intros. replace (fun f : A => f1 f @@ f2) with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H. - exploit transform_partial_program_compose; eauto. - intros [pb [X Y]]. exists pb; split. auto. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [pb [X Y]]. + exists pb; split. auto. apply transform_program_partial_program. auto. apply extensionality; intro. destruct(f1 x); auto. Qed. @@ -283,9 +291,17 @@ Qed. (** * Semantic preservation *) -(** We prove that the [transf_program] translations preserve semantics. - The proof composes the semantic preservation results for each pass. - This establishes the correctness of the whole compiler! *) +(** We prove that the [transf_program] translations preserve semantics + by constructing the following simulations: +- Forward simulations from [Cstrategy] / [Cminor] / [RTL] to [Asm] + (composition of the forward simulations for each pass). +- Backward simulations for the same languages + (derived from the forward simulation, using receptiveness of the source + language and determinacy of [Asm]). +- Backward simulation from [Csem] to [Asm] + (composition of two backward simulations). + +These results establish the correctness of the whole compiler! *) Ltac TransfProgInv := match goal with @@ -300,16 +316,17 @@ Ltac TransfProgInv := end. Theorem transf_rtl_program_correct: - forall p tp beh, + forall p tp, transf_rtl_program p = OK tp -> - not_wrong beh -> - RTL.exec_program p beh -> - Asm.exec_program tp beh. + forward_simulation (RTL.semantics p) (Asm.semantics tp) + * backward_simulation (RTL.semantics p) (Asm.semantics tp). Proof. - intros. unfold transf_rtl_program, transf_rtl_fundef in H. + intros. + assert (F: forward_simulation (RTL.semantics p) (Asm.semantics tp)). + unfold transf_rtl_program, transf_rtl_fundef in H. repeat TransfProgInv. repeat rewrite transform_program_print_identity in *. subst. - exploit transform_partial_program_identity; eauto. intro EQ. subst. + generalize (transform_partial_program_identity _ _ _ _ X0). intro EQ. subst. generalize Alloctyping.program_typing_preserved Tunnelingtyping.program_typing_preserved @@ -318,49 +335,93 @@ Proof. Reloadtyping.program_typing_preserved Stackingtyping.program_typing_preserved; intros. - eapply Asmgenproof.transf_program_correct; eauto 8. - eapply Stackingproof.transf_program_correct; eauto 6. - eapply Reloadproof.transf_program_correct; eauto. - eapply CleanupLabelsproof.transf_program_correct; eauto. - eapply Linearizeproof.transf_program_correct; eauto. - eapply Tunnelingproof.transf_program_correct; eauto. - eapply Allocproof.transf_program_correct; eauto. - eapply CSEproof.transf_program_correct; eauto. - eapply Constpropproof.transf_program_correct; eauto. - eapply CastOptimproof.transf_program_correct; eauto. - eapply Tailcallproof.transf_program_correct; eauto. + eapply compose_forward_simulation. apply Tailcallproof.transf_program_correct. + eapply compose_forward_simulation. apply CastOptimproof.transf_program_correct. + eapply compose_forward_simulation. apply Constpropproof.transf_program_correct. + eapply compose_forward_simulation. apply CSEproof.transf_program_correct. + eapply compose_forward_simulation. apply Allocproof.transf_program_correct. eassumption. + eapply compose_forward_simulation. apply Tunnelingproof.transf_program_correct. + eapply compose_forward_simulation. apply Linearizeproof.transf_program_correct. eassumption. eauto. + eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. + eapply compose_forward_simulation. apply Reloadproof.transf_program_correct. eauto. + eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. eassumption. eauto 8. + apply Asmgenproof.transf_program_correct; eauto 10. + split. auto. + apply forward_to_backward_simulation. auto. + apply RTL.semantics_receptive. + apply Asm.semantics_determinate. Qed. Theorem transf_cminor_program_correct: - forall p tp beh, + forall p tp, transf_cminor_program p = OK tp -> - not_wrong beh -> - Cminor.exec_program p beh -> - Asm.exec_program tp beh. + forward_simulation (Cminor.semantics p) (Asm.semantics tp) + * backward_simulation (Cminor.semantics p) (Asm.semantics tp). Proof. - intros. unfold transf_cminor_program, transf_cminorsel_fundef in H. + intros. + assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)). + unfold transf_cminor_program, transf_cminorsel_fundef in H. simpl in H. repeat TransfProgInv. - eapply transf_rtl_program_correct; eauto. - eapply RTLgenproof.transf_program_correct; eauto. - eapply Selectionproof.transf_program_correct; eauto. + eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. + eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption. + exact (fst (transf_rtl_program_correct _ _ P)). + + split. auto. + apply forward_to_backward_simulation. auto. + apply Cminor.semantics_receptive. + apply Asm.semantics_determinate. Qed. -Theorem transf_c_program_correct: - forall p tp beh, - transf_c_program p = OK tp -> - not_wrong beh -> - Cstrategy.exec_program p beh -> - Asm.exec_program tp beh. +Theorem transf_clight_program_correct: + forall p tp, + transf_clight_program p = OK tp -> + forward_simulation (Clight.semantics p) (Asm.semantics tp) + * backward_simulation (Clight.semantics p) (Asm.semantics tp). Proof. - intros until beh; unfold transf_c_program; simpl. - rewrite print_identity. - caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0. + intros. + assert (F: forward_simulation (Clight.semantics p) (Asm.semantics tp)). + revert H; unfold transf_clight_program; simpl. rewrite print_identity. - caseEq (Cshmgen.transl_program p0); simpl; try congruence; intros p1 EQ1. + caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. - intros EQ3 NOTW SEM. - eapply transf_cminor_program_correct; eauto. - eapply Cminorgenproof.transl_program_correct; eauto. - eapply Cshmgenproof.transl_program_correct; eauto. - eapply SimplExprproof.transl_program_correct; eauto. + intros EQ3. + eapply compose_forward_simulation. apply Cshmgenproof.transl_program_correct. eauto. + eapply compose_forward_simulation. apply Cminorgenproof.transl_program_correct. eauto. + exact (fst (transf_cminor_program_correct _ _ EQ3)). + + split. auto. + apply forward_to_backward_simulation. auto. + apply Clight.semantics_receptive. + apply Asm.semantics_determinate. +Qed. + +Theorem transf_cstrategy_program_correct: + forall p tp, + transf_c_program p = OK tp -> + forward_simulation (Cstrategy.semantics p) (Asm.semantics tp) + * backward_simulation (Cstrategy.semantics p) (Asm.semantics tp). +Proof. + intros. + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)). + revert H; unfold transf_c_program; simpl. rewrite print_identity. + caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0. + intros EQ1. + eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto. + exact (fst (transf_clight_program_correct _ _ EQ1)). + + split. auto. + apply forward_to_backward_simulation. auto. + apply Cstrategy.semantics_receptive. + apply Asm.semantics_determinate. +Qed. + +Theorem transf_c_program_correct: + forall p tp, + transf_c_program p = OK tp -> + backward_simulation (Csem.semantics p) (Asm.semantics tp). +Proof. + intros. + eapply compose_backward_simulation. + apply Cstrategy.strategy_simulation. + exact (snd (transf_cstrategy_program_correct _ _ H)). Qed. 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. |