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

2 files changed, 46 insertions, 29 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index fb8b8e1a..e0d05f21 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -1233,27 +1233,25 @@ Inductive final_state: state -> int -> Prop :=
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
   program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
 
-(** Big-step execution of a whole program.  
-  [exec_program_bigstep p beh] holds
-  if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] executes without errors and produces
-  the observable behaviour [beh]. *)
-
-Inductive exec_program_bigstep (p: program): program_behavior -> Prop :=
-  | program_terminates: forall b f m1 t r,
+(** Big-step execution of a whole program.  *)
+
+Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
+  | bigstep_program_terminates_intro: forall b f m1 t r,
       let ge := Genv.globalenv p in 
       let m0 := Genv.init_mem p in
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       eval_funcall ge m0 f nil t m1 (Vint r) ->
-      exec_program_bigstep p (Terminates t r)
-  | program_diverges: forall b f t,
+      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
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       evalinf_funcall ge m0 f nil t ->
-      exec_program_bigstep p (Diverges t).
+      bigstep_program_diverges p t.
 
 (** * Implication from big-step semantics to transition semantics *)
 
@@ -1696,26 +1694,34 @@ 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 *)
+  intros. inv H. unfold ge0, m0 in *. 
   econstructor.
   econstructor. eauto. eauto.
   apply eval_funcall_steps. eauto. red; auto. 
-  econstructor. 
-  (* divergence *)
   econstructor.
-  econstructor. eauto. eauto. 
-  eapply forever_N_forever with (order := order).
-  red; intros. constructor; intros. red in H. elim H.
-  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_N_forever with (order := order).
+    red; intros. constructor; intros. red in H. elim H.
+    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.
+  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_TRANSITIONS.
 
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 6a8b676f..836f1e4b 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -1661,6 +1661,8 @@ Theorem transl_program_correct:
   Csharpminor.exec_program tprog beh.
 Proof.
   set (order := fun (S1 S2: Csem.state) => False).
+  assert (WF: well_founded order).
+  unfold order; red. intros. constructor; intros. contradiction.
   assert (transl_step':
      forall S1 t S2, Csem.step ge S1 t S2 ->
      forall T1, match_states S1 T1 ->
@@ -1670,21 +1672,30 @@ Proof.
   intros. exploit transl_step; eauto. intros [T2 [A B]].
   exists T2; split. auto. auto.
   intros. inv H0.
+(* Terminates *)
   assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1).
   inv H3. inv H2. inv H1. exists t1; exists s2; auto.
   destruct H0 as [t1 [s1 ST]].
   exploit transl_initial_states; eauto. intros [R [A B]].
   exploit simulation_star_star; eauto. intros [R' [C D]]. 
   econstructor; eauto. eapply transl_final_states; eauto.
+(* Diverges *)
   assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1).
-  inv H2. exists t; exists s2; auto.
+  inv H2. inv H3. exists E0; exists s2; auto. exists t1; exists s2; auto.
   destruct H0 as [t1 [s1 ST]].
   exploit transl_initial_states; eauto. intros [R [A B]].
-  exploit simulation_star_forever; eauto.
-  unfold order; red. intros. constructor; intros. contradiction.
+  exploit simulation_star_star; eauto. intros [R' [C D]]. 
+  econstructor; eauto. eapply simulation_star_forever_silent; eauto.
+(* Reacts *)
+  assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1).
+  inv H2. inv H0. congruence. exists t1; exists s0; auto.
+  destruct H0 as [t1 [s1 ST]].
+  exploit transl_initial_states; eauto. intros [R [A B]].
+  exploit simulation_star_forever_reactive; eauto.
   intro C.
   econstructor; eauto.
-  contradiction.
+(* Goes wrong *)
+  contradiction. contradiction.
 Qed.
 
 End CORRECTNESS.