From bdc7b815d033f84e5538a1c8db87d3c061b1ca4c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 5 Aug 2009 14:40:34 +0000
Subject: Added 'going wrong' behaviors

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Smallstep.v | 45 ++++++++++++++++++++++++++++++++++-----------
 1 file changed, 34 insertions(+), 11 deletions(-)

(limited to 'common/Smallstep.v')

diff --git a/common/Smallstep.v b/common/Smallstep.v
index f41fe4ed..9e9063b0 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -21,6 +21,7 @@
 
 Require Import Wf.
 Require Import Wf_nat.
+Require Import Classical.
 Require Import Coqlib.
 Require Import AST.
 Require Import Events.
@@ -281,18 +282,28 @@ Qed.
 
 (** * Outcomes for program executions *)
 
-(** The two valid outcomes for the execution of a program:
+(** The three possible outcomes for the execution of a program:
 - Termination, with a finite trace of observable events
   and an integer value that stands for the process exit code
   (the return value of the main function).
 - Divergence with an infinite trace of observable events.
   (The actual events generated by the execution can be a
    finite prefix of this trace, or the whole trace.)
+- Going wrong, with a finite trace of observable events
+  performed before the program gets stuck.
 *)
 
 Inductive program_behavior: Type :=
   | Terminates: trace -> int -> program_behavior
-  | Diverges: traceinf -> program_behavior.
+  | Diverges: traceinf -> program_behavior
+  | Goes_wrong: trace -> program_behavior.
+
+Definition not_wrong (beh: program_behavior) : Prop :=
+  match beh with
+  | Terminates _ _ => True
+  | Diverges _ => True
+  | Goes_wrong _ => False
+  end.
 
 (** Given a characterization of initial states and final states,
   [program_behaves] relates a program behaviour with the 
@@ -311,7 +322,13 @@ Inductive program_behaves (ge: genv): program_behavior -> Prop :=
   | program_diverges: forall s T,
       initial_state s ->
       forever ge s T ->
-      program_behaves ge (Diverges T).
+      program_behaves ge (Diverges T)
+  | program_goes_wrong: forall s t s',
+      initial_state s ->
+      star ge s t s' ->
+      (forall t1 s1, ~step ge s' t1 s1) ->
+      (forall r, ~final_state s' r) ->
+      program_behaves ge (Goes_wrong t).
 
 End CLOSURES.
 
@@ -418,16 +435,18 @@ Qed.
 
 Lemma simulation_star_wf_preservation:
   forall beh,
+  not_wrong beh ->
   program_behaves step1 initial_state1 final_state1 ge1 beh ->
   program_behaves step2 initial_state2 final_state2 ge2 beh.
 Proof.
-  intros. inversion H; subst.
-  destruct (match_initial_states H0) as [s2 [A B]].
-  destruct (simulation_star_star H1 B) as [s2' [C D]].
+  intros. inv H0; simpl in H. 
+  destruct (match_initial_states H1) as [s2 [A B]].
+  destruct (simulation_star_star H2 B) as [s2' [C D]].
   econstructor; eauto.
-  destruct (match_initial_states H0) as [s2 [A B]].
+  destruct (match_initial_states H1) as [s2 [A B]].
   econstructor; eauto.
   eapply simulation_star_forever; eauto.
+  contradiction. 
 Qed.
 
 End SIMULATION_STAR_WF.
@@ -448,16 +467,17 @@ Hypothesis simulation:
 
 Lemma simulation_star_preservation:
   forall beh,
+  not_wrong beh ->
   program_behaves step1 initial_state1 final_state1 ge1 beh ->
   program_behaves step2 initial_state2 final_state2 ge2 beh.
 Proof.
   intros.
   apply simulation_star_wf_preservation with (ltof _ measure).
   apply well_founded_ltof. intros.
-  destruct (simulation H0 H1) as [[st2' [A B]] | [A [B C]]].
+  destruct (simulation H1 H2) as [[st2' [A B]] | [A [B C]]].
   exists st2'; auto.
   exists st2; split. right; split. rewrite B. apply star_refl. auto. auto.
-  auto.
+  auto. auto.
 Qed.
 
 End SIMULATION_STAR.
@@ -474,6 +494,7 @@ Hypothesis simulation:
 
 Lemma simulation_step_preservation:
   forall beh,
+  not_wrong beh ->
   program_behaves step1 initial_state1 final_state1 ge1 beh ->
   program_behaves step2 initial_state2 final_state2 ge2 beh.
 Proof.
@@ -484,7 +505,7 @@ Proof.
   forall st2, match_states st1 st2 ->
   (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
   \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
-  intros. destruct (simulation H0 H1) as [st2' [A B]].
+  intros. destruct (simulation H1 H2) as [st2' [A B]].
   left; exists st2'; split. apply plus_one; auto. auto.
   eapply simulation_star_preservation; eauto.
 Qed.
@@ -503,6 +524,7 @@ Hypothesis simulation:
 
 Lemma simulation_plus_preservation:
   forall beh,
+  not_wrong beh ->
   program_behaves step1 initial_state1 final_state1 ge1 beh ->
   program_behaves step2 initial_state2 final_state2 ge2 beh.
 Proof.
@@ -513,7 +535,7 @@ Proof.
   forall st2, match_states st1 st2 ->
   (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
   \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
-  intros. destruct (simulation H0 H1) as [st2' [A B]].
+  intros. destruct (simulation H1 H2) as [st2' [A B]].
   left; exists st2'; auto.
   eapply simulation_star_preservation; eauto.
 Qed.
@@ -538,6 +560,7 @@ Hypothesis simulation:
 
 Lemma simulation_opt_preservation:
   forall beh,
+  not_wrong beh ->
   program_behaves step1 initial_state1 final_state1 ge1 beh ->
   program_behaves step2 initial_state2 final_state2 ge2 beh.
 Proof.
-- 
cgit