Distinguish two kinds of nonterminating behaviors: silent divergence

and reactive divergence.  As a consequence:
- Removed the Enilinf constructor from traceinf (values of traceinf
  type are always infinite traces).
- Traces are now uniquely defined.
- Adapted proofs big step -> small step for Clight and Cminor accordingly.
- Strengthened results in driver/Complements accordingly.
- Added common/Determinism to collect generic results about
  deterministic semantics.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 28 insertions, 19 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index b48db2d6..8cc2185d 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -755,13 +755,10 @@ with execinf_stmt:
 
 End NATURALSEM.
 
-(** Execution of a whole program: [exec_program p beh]
-  holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] has [beh] as observable
-  behavior. *)
+(** Big-step execution of a whole program *)
 
-Inductive exec_program_bigstep (p: program): program_behavior -> Prop :=
-  | program_terminates:
+Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
+  | bigstep_program_terminates_intro:
       forall b f t m r,
       let ge := Genv.globalenv p in
       let m0 := Genv.init_mem p in
@@ -769,8 +766,10 @@ Inductive exec_program_bigstep (p: program): program_behavior -> Prop :=
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
       eval_funcall ge m0 f nil t m (Vint r) ->
-      exec_program_bigstep p (Terminates t r)
-  | program_diverges:
+      bigstep_program_terminates p t r.
+
+Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
+  | bigstep_program_diverges_intro:
       forall b f t,
       let ge := Genv.globalenv p in
       let m0 := Genv.init_mem p in
@@ -778,7 +777,7 @@ Inductive exec_program_bigstep (p: program): program_behavior -> Prop :=
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
       evalinf_funcall ge m0 f nil t ->
-      exec_program_bigstep p (Diverges t).
+      bigstep_program_diverges p t.
 
 (** ** Correctness of the big-step semantics with respect to the transition semantics *)
 
@@ -1087,22 +1086,32 @@ Proof.
   traceEq.
 Qed.
 
-Theorem exec_program_bigstep_transition:
-  forall beh,
-  exec_program_bigstep prog beh ->
-  exec_program prog beh.
+Theorem bigstep_program_terminates_exec:
+  forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
 Proof.
   intros. inv H.
-  (* termination *)
   econstructor.
   econstructor. eauto. eauto. auto. 
   apply eval_funcall_steps. eauto. red; auto. 
-  econstructor. 
-  (* divergence *)
   econstructor.
-  econstructor. eauto. eauto. auto. 
-  apply forever_plus_forever. 
-  apply evalinf_funcall_forever. auto.
+Qed.
+
+Theorem bigstep_program_diverges_exec:
+  forall T, bigstep_program_diverges prog T ->
+  exec_program prog (Reacts T) \/
+  exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T.
+Proof.
+  intros. inv H.
+  set (st := Callstate f nil Kstop m0).
+  assert (forever step ge0 st T). 
+    eapply forever_plus_forever.
+    eapply evalinf_funcall_forever; eauto. 
+  destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
+  as [A | [t [s' [T' [B [C D]]]]]]. 
+  left. econstructor. econstructor. eauto. eauto. auto. auto.
+  right. exists t. split.
+  econstructor. econstructor; eauto. eauto. auto.  
+  subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
 Qed.
 
 End BIGSTEP_TO_TRANSITION.