From c48b9097201dc9a1e326acdbce491fe16cab01e6 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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 +++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 66 insertions(+), 7 deletions(-)

(limited to 'common/Complements.v')

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.
-- 
cgit