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

4 files changed, 98 insertions, 30 deletions

diff --git a/common/Complements.v b/common/Complements.v
index 5280947..2263f4e 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 83a7a19..e9070e1 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 33bc783..db15929 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 f60746d..8039ba4 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.