From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:06:55 +0000 Subject: Merge of branches/full-expr-4: - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Complements.v | 129 ++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 98 insertions(+), 31 deletions(-) (limited to 'driver/Complements.v') diff --git a/driver/Complements.v b/driver/Complements.v index 3f32cc63..334b9b04 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -23,15 +23,74 @@ Require Import Smallstep. Require Import Determinism. Require Import Csyntax. Require Import Csem. +Require Import Cstrategy. Require Import Asm. Require Import Compiler. Require Import Errors. -(** * Determinism of Asm semantics *) +(** * Integrating a deterministic external world *) -(** In this section, we show that the semantics for the Asm language - are deterministic, provided that the program is executed against a - deterministic world, as formalized in module [Determinism]. *) +(** We now integrate a deterministic external world in the semantics + of Compcert C and Asm. *) + +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. *) + +(** We show that a C program is safe (in the sense of [Cstrategy.safeprog]) + if it cannot go wrong in the world-aware semantics. *) + +Lemma notwrong_safeprog: + forall p, + (forall beh, exec_C_program p beh -> not_wrong beh) -> + Cstrategy.safeprog p initial_world. +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. +Qed. + +(** ** Determinism of Asm semantics *) Remark extcall_arguments_deterministic: forall rs m sg args args', @@ -100,17 +159,20 @@ Proof. Qed. Theorem asm_exec_program_deterministic: - forall p w beh1 beh2, - Asm.exec_program p beh1 -> Asm.exec_program p beh2 -> - possible_behavior w beh1 -> possible_behavior w beh2 -> + forall p beh1 beh2, + exec_asm_program p beh1 -> exec_asm_program p beh2 -> beh1 = beh2. Proof. - intros. - eapply (program_behaves_deterministic _ _ step (initial_state p) final_state); eauto. - exact step_internal_deterministic. - exact (initial_state_deterministic p). - exact final_state_deterministic. - exact final_state_not_step. + 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. Qed. (** * Additional semantic preservation property *) @@ -118,28 +180,34 @@ Qed. (** 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 Clight + 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 Clight program. *) + the source program. *) Theorem transf_c_program_is_refinement: - forall p tp w, + forall p tp, transf_c_program p = OK tp -> - (exists b, Csem.exec_program p b /\ possible_behavior w b /\ not_wrong b) -> - (forall b, Asm.exec_program tp b -> possible_behavior w b -> Csem.exec_program p b). + (forall beh, exec_C_program p beh -> not_wrong beh) -> + (forall beh, exec_asm_program tp beh -> exec_C_program p beh). Proof. - intros. destruct H0 as [b0 [A [B C]]]. - assert (Asm.exec_program tp b0). + 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 (b = b0). eapply asm_exec_program_deterministic; eauto. - subst b0. auto. + 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. Qed. Section SPECS_PRESERVED. (** The second additional results shows that if one execution - of the source Clight program satisfies a given specification + 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. *) @@ -149,16 +217,15 @@ Variable spec: program_behavior -> Prop. Hypothesis spec_not_wrong: forall b, spec b -> not_wrong b. Theorem transf_c_program_preserves_spec: - forall p tp w, + forall p tp, transf_c_program p = OK tp -> - (exists b, Csem.exec_program p b /\ possible_behavior w b /\ spec b) -> - (forall b, Asm.exec_program tp b -> possible_behavior w b -> spec b). + (forall beh, exec_C_program p beh -> spec beh) -> + (forall beh, exec_asm_program tp beh -> spec beh). Proof. - intros. destruct H0 as [b1 [A [B C]]]. - assert (Asm.exec_program tp b1). - eapply transf_c_program_correct; eauto. - assert (b1 = b). eapply asm_exec_program_deterministic; eauto. - subst b1. auto. + intros. apply H0. apply transf_c_program_is_refinement with tp; auto. Qed. End SPECS_PRESERVED. + +End WORLD. + -- cgit