From c48b9097201dc9a1e326acdbce491fe16cab01e6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 28 Aug 2007 12:57:58 +0000 Subject: Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Complements.v | 73 +++++++++++++++++++++++++++++++++++++++++++++++----- common/Events.v | 10 ++++--- common/Main.v | 14 +++++----- common/Smallstep.v | 31 ++++++++++++---------- 4 files changed, 98 insertions(+), 30 deletions(-) (limited to 'common') diff --git a/common/Complements.v b/common/Complements.v index 5280947b..2263f4ec 100644 --- a/common/Complements.v +++ b/common/Complements.v @@ -8,8 +8,11 @@ Require Import Values. Require Import Events. Require Import Globalenvs. Require Import Smallstep. +Require Import Csyntax. +Require Import Csem. Require Import PPC. Require Import Main. +Require Import Errors. (** * Determinism of PPC semantics *) @@ -555,22 +558,29 @@ Proof. auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl. Qed. -(** * Strong semantic preservation property *) +(** * Additional semantic preservation property *) -Require Import Errors. +(** Combining the semantic preservation theorem from module [Main] + with the determinism of PPC executions, we easily obtain + additional, stronger semantic preservation properties. + The first property states that, when compiling a Clight + program that has well-defined semantics, all possible executions + of the resulting PPC code correspond to an execution of + the source Clight program, in the sense of the [matching_behaviors] + predicate. *) -Theorem transf_rtl_program_correct_strong: +Theorem transf_c_program_correct_strong: forall p tp b w, - transf_rtl_program p = OK tp -> - RTL.exec_program p b -> + transf_c_program p = OK tp -> + Csem.exec_program p b -> possible_behavior w b -> (exists b', exec_program' tp w b') /\(forall b', exec_program' tp w b' -> - exists b0, RTL.exec_program p b0 /\ matching_behaviors b0 b'). + exists b0, Csem.exec_program p b0 /\ matching_behaviors b0 b'). Proof. intros. assert (PPC.exec_program tp b). - eapply transf_rtl_program_correct; eauto. + eapply transf_c_program_correct; eauto. exploit exec_program_program'; eauto. intros [b' [A B]]. split. exists b'; auto. @@ -578,3 +588,52 @@ Proof. apply matching_behaviors_same with b'. auto. eapply exec_program'_deterministic; eauto. Qed. + +Section SPECS_PRESERVED. + +(** The second additional results shows that if one execution + of the source Clight program satisfies a given specification + (a predicate on the observable behavior of the program), + then all executions of the produced PPC program satisfy + this specification as well. *) + +Variable spec: program_behavior -> Prop. + +(* Since the execution trace for a diverging Clight program + is not uniquely defined (the trace can contain events that + the program will never perform because it loops earlier), + this result holds only if the specification is closed under + prefixes in the case of diverging executions. This is the + case for all safety properties (some undesirable event never + occurs), but not for liveness properties (some desirable event + always occurs). *) + +Hypothesis spec_safety: + forall T T', traceinf_prefix T T' -> spec (Diverges T') -> spec (Diverges T). + +Theorem transf_c_program_preserves_spec: + forall p tp b w, + transf_c_program p = OK tp -> + Csem.exec_program p b -> + possible_behavior w b -> + spec b -> + (exists b', exec_program' tp w b') +/\(forall b', exec_program' tp w b' -> spec b'). +Proof. + intros. + assert (PPC.exec_program tp b). + eapply transf_c_program_correct; eauto. + exploit exec_program_program'; eauto. + intros [b' [A B]]. + split. exists b'; auto. + intros b'' EX. + assert (same_behaviors b' b''). eapply exec_program'_deterministic; eauto. + inv B; inv H4. + auto. + apply spec_safety with T1. + eapply traceinf_prefix_compat with T2 T1. + auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl. + auto. +Qed. + +End SPECS_PRESERVED. diff --git a/common/Events.v b/common/Events.v index 83a7a19b..e9070e16 100644 --- a/common/Events.v +++ b/common/Events.v @@ -66,14 +66,18 @@ Proof. intros. unfold E0, Eapp. rewrite <- app_nil_end. auto. Qed. Lemma Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3). Proof. intros. unfold Eapp, trace. apply app_ass. Qed. +Lemma E0_left_inf: forall T, E0 *** T = T. +Proof. auto. Qed. + Lemma Eappinf_assoc: forall t1 t2 T, (t1 ** t2) *** T = t1 *** (t2 *** T). Proof. induction t1; intros; simpl. auto. decEq; auto. Qed. -Hint Rewrite E0_left E0_right Eapp_assoc: trace_rewrite. +Hint Rewrite E0_left E0_right Eapp_assoc + E0_left_inf Eappinf_assoc: trace_rewrite. -Opaque trace E0 Eextcall Eapp. +Opaque trace E0 Eextcall Eapp Eappinf. (** The following [traceEq] tactic proves equalities between traces or infinite traces. *) @@ -251,7 +255,7 @@ Proof. inv H; inv H0; inv H1; constructor; eapply COINDHYP; eauto. Qed. -Transparent trace E0 Eapp. +Transparent trace E0 Eapp Eappinf. Lemma traceinf_prefix_app: forall T1 T2 t, diff --git a/common/Main.v b/common/Main.v index 33bc7830..db159298 100644 --- a/common/Main.v +++ b/common/Main.v @@ -258,10 +258,10 @@ Proof. Qed. Theorem transf_cminor_program_correct: - forall p tp t n, + forall p tp beh, transf_cminor_program p = OK tp -> - Cminor.exec_program p t (Vint n) -> - PPC.exec_program tp (Terminates t n). + Cminor.exec_program p beh -> + PPC.exec_program tp beh. Proof. intros. unfold transf_cminor_program, transf_cminor_fundef in H. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [H3 P3]]. @@ -276,12 +276,12 @@ Proof. Qed. Theorem transf_c_program_correct: - forall p tp t n, + forall p tp beh, transf_c_program p = OK tp -> - Csem.exec_program p t (Vint n) -> - PPC.exec_program tp (Terminates t n). + Csem.exec_program p beh -> + PPC.exec_program tp beh. Proof. - intros until n; unfold transf_c_program; simpl. + intros until beh; unfold transf_c_program; simpl. caseEq (Ctyping.typecheck_program p); try congruence; intro. caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. diff --git a/common/Smallstep.v b/common/Smallstep.v index f60746d3..8039ba43 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -172,12 +172,17 @@ Qed. for coinductive reasoning. *) CoInductive forever_N (ge: genv): nat -> state -> traceinf -> Prop := - | forever_N_star: forall s1 t s2 p q T, - star ge s1 t s2 -> (p < q)%nat -> forever_N ge p s2 T -> - forever_N ge q s1 (t *** T) - | forever_N_plus: forall s1 t s2 p q T, - plus ge s1 t s2 -> forever_N ge p s2 T -> - forever_N ge q s1 (t *** T). + | forever_N_star: forall s1 t s2 p q T1 T2, + star ge s1 t s2 -> + (p < q)%nat -> + forever_N ge p s2 T2 -> + T1 = t *** T2 -> + forever_N ge q s1 T1 + | forever_N_plus: forall s1 t s2 p q T1 T2, + plus ge s1 t s2 -> + forever_N ge p s2 T2 -> + T1 = t *** T2 -> + forever_N ge q s1 T1. Remark Peano_induction: forall (P: nat -> Prop), @@ -202,14 +207,14 @@ Proof. (* star case *) inv H1. (* no transition *) - change (E0 *** T0) with T0. apply H with p1. auto. auto. + change (E0 *** T2) with T2. apply H with p1. auto. auto. (* at least one transition *) - exists t1; exists s0; exists p0; exists (t2 *** T0). + exists t1; exists s0; exists p0; exists (t2 *** T2). split. auto. split. eapply forever_N_star; eauto. apply Eappinf_assoc. (* plus case *) inv H1. - exists t1; exists s0; exists (S p1); exists (t2 *** T0). + exists t1; exists s0; exists (S p1); exists (t2 *** T2). split. auto. split. eapply forever_N_star; eauto. apply Eappinf_assoc. Qed. @@ -348,12 +353,12 @@ Proof. forever_N step2 ge2 (measure st1) st2 T). cofix COINDHYP; intros. inversion H; subst. elim (simulation H1 H0). - intros [st2' [A B]]. apply forever_N_plus with st2' (measure s2). - auto. apply COINDHYP. assumption. assumption. + intros [st2' [A B]]. apply forever_N_plus with t st2' (measure s2) T0. + auto. apply COINDHYP. assumption. assumption. auto. intros [A [B C]]. - apply forever_N_star with st2 (measure s2). + apply forever_N_star with t st2 (measure s2) T0. rewrite B. apply star_refl. auto. - apply COINDHYP. assumption. auto. + apply COINDHYP. assumption. auto. auto. intros. eapply forever_N_forever; eauto. Qed. -- cgit