From 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Aug 2009 12:53:19 +0000 Subject: 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 --- cfrontend/Csem.v | 56 ++++++++++++++++++++++++++--------------------- cfrontend/Cshmgenproof3.v | 19 ++++++++++++---- 2 files changed, 46 insertions(+), 29 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index fb8b8e1..e0d05f2 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 6a8b676..836f1e4 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. -- cgit v1.2.3