From 93b89122000e42ac57abc39734fdf05d3a89e83c Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Jul 2011 08:26:16 +0000 Subject: Merge of branch new-semantics: revised and strengthened top-level statements of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Clight.v | 66 +++++++++++++++++++++++++++++------------------------- 1 file changed, 35 insertions(+), 31 deletions(-) (limited to 'cfrontend/Clight.v') diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index da8f668f..a61d7067 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -906,13 +906,26 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate (Vint r) Kstop m) r. -(** 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. *) +(** Wrapping up these definitions in a small-step semantics. *) -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + +(** This semantics is receptive to changes in events. *) + +Lemma semantics_receptive: + forall (p: program), receptive (semantics p). +Proof. + intros. constructor; simpl; intros. +(* receptiveness *) + assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2). + intros. subst. inv H0. exists s1; auto. + inversion H; subst; auto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (Returnstate vres2 k m2). econstructor; eauto. +(* trace length *) + inv H; simpl; try omega. eapply external_call_trace_length; eauto. +Qed. (** Big-step execution of a whole program. *) @@ -936,6 +949,9 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. +Definition bigstep_semantics (p: program) := + Bigstep_semantics (bigstep_program_terminates p) (bigstep_program_diverges p). + (** * Implication from big-step semantics to transition semantics *) Section BIGSTEP_TO_TRANSITIONS. @@ -1352,33 +1368,21 @@ Proof. traceEq. Qed. -Theorem bigstep_program_terminates_exec: - forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). +Theorem bigstep_semantics_sound: + bigstep_sound (bigstep_semantics prog) (semantics prog). Proof. - intros. inv H. + constructor; simpl; intros. +(* termination *) + inv H. econstructor; econstructor. + split. econstructor; eauto. + split. eapply eval_funcall_steps. eauto. red; auto. econstructor. - econstructor. eauto. eauto. eauto. auto. - eapply eval_funcall_steps. eauto. red; auto. - econstructor. -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. - right. exists t. split. - econstructor. econstructor; eauto. eauto. auto. - subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor. +(* divergence *) + inv H. econstructor. + split. econstructor; eauto. + eapply forever_N_forever with (order := order). + red; intros. constructor; intros. red in H. elim H. + eapply evalinf_funcall_forever; eauto. Qed. End BIGSTEP_TO_TRANSITIONS. -- cgit