From 7c55573d4a6dd0f643295d52c391d33f7593064a Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 11 Mar 2010 12:22:26 +0000 Subject: Restored the big-step semantics for Cminor git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1287 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Cminor.v | 250 +++++++++++++++++++++++++++---------------------------- 1 file changed, 125 insertions(+), 125 deletions(-) (limited to 'backend/Cminor.v') diff --git a/backend/Cminor.v b/backend/Cminor.v index 094bef7..f2f03c5 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -536,9 +536,11 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop := (** * Alternate operational semantics (big-step) *) -(** In big-step style, just like expressions evaluate to values, - statements evaluate to``outcomes'' indicating how execution should - proceed afterwards. *) +(** We now define another semantics for Cminor without [goto] that follows + the ``big-step'' style of semantics, also known as natural semantics. + In this style, just like expressions evaluate to values, + statements evaluate to``outcomes'' indicating how execution should + proceed afterwards. *) Inductive outcome: Type := | Out_normal: outcome (**r continue in sequence *) @@ -570,10 +572,6 @@ Definition outcome_free_mem | _ => Mem.free m sp 0 sz = Some m' end. -(***** REVISE - PROBLEMS WITH free *) - -(****************************** - Section NATURALSEM. Variable ge: genv. @@ -591,7 +589,7 @@ Inductive eval_funcall: forall m f vargs m1 sp e t e2 m2 out vres m3, Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) -> set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> - exec_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out -> + exec_stmt f (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out -> outcome_result_value out f.(fn_sig).(sig_res) vres -> outcome_free_mem out m2 sp f.(fn_stackspace) m3 -> eval_funcall m (Internal f) vargs t m3 vres @@ -600,7 +598,7 @@ Inductive eval_funcall: external_call ef args m t res m' -> eval_funcall m (External ef) args t m' res -(** Execution of a statement: [exec_stmt ge sp e m s t e' m' out] +(** Execution of a statement: [exec_stmt ge f sp e m s t e' m' out] means that statement [s] executes with outcome [out]. [e] is the initial environment and [m] is the initial memory state. [e'] is the final environment, reflecting variable assignments performed @@ -609,89 +607,103 @@ Inductive eval_funcall: the execution. The other parameters are as in [eval_expr]. *) with exec_stmt: - val -> + function -> val -> env -> mem -> stmt -> trace -> env -> mem -> outcome -> Prop := | exec_Sskip: - forall sp e m, - exec_stmt sp e m Sskip E0 e m Out_normal + forall f sp e m, + exec_stmt f sp e m Sskip E0 e m Out_normal | exec_Sassign: - forall sp e m id a v, + forall f sp e m id a v, eval_expr ge sp e m a v -> - exec_stmt sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal + exec_stmt f sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal | exec_Sstore: - forall sp e m chunk addr a vaddr v m', + forall f sp e m chunk addr a vaddr v m', eval_expr ge sp e m addr vaddr -> eval_expr ge sp e m a v -> Mem.storev chunk m vaddr v = Some m' -> - exec_stmt sp e m (Sstore chunk addr a) E0 e m' Out_normal + exec_stmt f sp e m (Sstore chunk addr a) E0 e m' Out_normal | exec_Scall: - forall sp e m optid sig a bl vf vargs f t m' vres e', + forall f sp e m optid sig a bl vf vargs fd t m' vres e', eval_expr ge sp e m a vf -> eval_exprlist ge sp e m bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - eval_funcall m f vargs t m' vres -> + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + eval_funcall m fd vargs t m' vres -> e' = set_optvar optid vres e -> - exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal + exec_stmt f sp e m (Scall optid sig a bl) t e' m' Out_normal | exec_Sifthenelse: - forall sp e m a s1 s2 v b t e' m' out, + forall f sp e m a s1 s2 v b t e' m' out, eval_expr ge sp e m a v -> Val.bool_of_val v b -> - exec_stmt sp e m (if b then s1 else s2) t e' m' out -> - exec_stmt sp e m (Sifthenelse a s1 s2) t e' m' out + exec_stmt f sp e m (if b then s1 else s2) t e' m' out -> + exec_stmt f sp e m (Sifthenelse a s1 s2) t e' m' out | exec_Sseq_continue: - forall sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out, - exec_stmt sp e m s1 t1 e1 m1 Out_normal -> - exec_stmt sp e1 m1 s2 t2 e2 m2 out -> + forall f sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out, + exec_stmt f sp e m s1 t1 e1 m1 Out_normal -> + exec_stmt f sp e1 m1 s2 t2 e2 m2 out -> t = t1 ** t2 -> - exec_stmt sp e m (Sseq s1 s2) t e2 m2 out + exec_stmt f sp e m (Sseq s1 s2) t e2 m2 out | exec_Sseq_stop: - forall sp e m t s1 s2 e1 m1 out, - exec_stmt sp e m s1 t e1 m1 out -> + forall f sp e m t s1 s2 e1 m1 out, + exec_stmt f sp e m s1 t e1 m1 out -> out <> Out_normal -> - exec_stmt sp e m (Sseq s1 s2) t e1 m1 out + exec_stmt f sp e m (Sseq s1 s2) t e1 m1 out | exec_Sloop_loop: - forall sp e m s t t1 e1 m1 t2 e2 m2 out, - exec_stmt sp e m s t1 e1 m1 Out_normal -> - exec_stmt sp e1 m1 (Sloop s) t2 e2 m2 out -> + forall f sp e m s t t1 e1 m1 t2 e2 m2 out, + exec_stmt f sp e m s t1 e1 m1 Out_normal -> + exec_stmt f sp e1 m1 (Sloop s) t2 e2 m2 out -> t = t1 ** t2 -> - exec_stmt sp e m (Sloop s) t e2 m2 out + exec_stmt f sp e m (Sloop s) t e2 m2 out | exec_Sloop_stop: - forall sp e m t s e1 m1 out, - exec_stmt sp e m s t e1 m1 out -> + forall f sp e m t s e1 m1 out, + exec_stmt f sp e m s t e1 m1 out -> out <> Out_normal -> - exec_stmt sp e m (Sloop s) t e1 m1 out + exec_stmt f sp e m (Sloop s) t e1 m1 out | exec_Sblock: - forall sp e m s t e1 m1 out, - exec_stmt sp e m s t e1 m1 out -> - exec_stmt sp e m (Sblock s) t e1 m1 (outcome_block out) + forall f sp e m s t e1 m1 out, + exec_stmt f sp e m s t e1 m1 out -> + exec_stmt f sp e m (Sblock s) t e1 m1 (outcome_block out) | exec_Sexit: - forall sp e m n, - exec_stmt sp e m (Sexit n) E0 e m (Out_exit n) + forall f sp e m n, + exec_stmt f sp e m (Sexit n) E0 e m (Out_exit n) | exec_Sswitch: - forall sp e m a cases default n, + forall f sp e m a cases default n, eval_expr ge sp e m a (Vint n) -> - exec_stmt sp e m (Sswitch a cases default) + exec_stmt f sp e m (Sswitch a cases default) E0 e m (Out_exit (switch_target n default cases)) | exec_Sreturn_none: - forall sp e m, - exec_stmt sp e m (Sreturn None) E0 e m (Out_return None) + forall f sp e m, + exec_stmt f sp e m (Sreturn None) E0 e m (Out_return None) | exec_Sreturn_some: - forall sp e m a v, + forall f sp e m a v, eval_expr ge sp e m a v -> - exec_stmt sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v)) + exec_stmt f sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v)) | exec_Stailcall: - forall sp e m sig a bl vf vargs f t m' vres, + forall f sp e m sig a bl vf vargs fd t m' m'' vres, eval_expr ge (Vptr sp Int.zero) e m a vf -> eval_exprlist ge (Vptr sp Int.zero) e m bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - eval_funcall (Mem.free m sp) f vargs t m' vres -> - exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m' (Out_tailcall_return vres). + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> + eval_funcall m' fd vargs t m'' vres -> + exec_stmt f (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m'' (Out_tailcall_return vres). Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop. +Combined Scheme eval_funcall_exec_stmt_ind2 + from eval_funcall_ind2, exec_stmt_ind2. + +(* +Definition eval_funcall_exec_stmt_ind2 + (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop) + (P2: val -> env -> mem -> stmt -> trace -> + env -> mem -> outcome -> Prop) := + fun a b c d e f g h i j k l m n o p q => + conj + (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q) + (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q). +*) (** Coinductive semantics for divergence. [evalinf_funcall ge m f args t] @@ -706,7 +718,7 @@ CoInductive evalinf_funcall: forall m f vargs m1 sp e t, Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) -> set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> - execinf_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t -> + execinf_stmt f (Vptr sp Int.zero) e m1 f.(fn_body) t -> evalinf_funcall m (Internal f) vargs t (** [execinf_stmt ge sp e m s t] means that statement [s] diverges. @@ -714,53 +726,54 @@ CoInductive evalinf_funcall: and [t] the trace of observable events performed during the execution. *) with execinf_stmt: - val -> env -> mem -> stmt -> traceinf -> Prop := + function -> val -> env -> mem -> stmt -> traceinf -> Prop := | execinf_Scall: - forall sp e m optid sig a bl vf vargs f t, + forall f sp e m optid sig a bl vf vargs fd t, eval_expr ge sp e m a vf -> eval_exprlist ge sp e m bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - evalinf_funcall m f vargs t -> - execinf_stmt sp e m (Scall optid sig a bl) t + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + evalinf_funcall m fd vargs t -> + execinf_stmt f sp e m (Scall optid sig a bl) t | execinf_Sifthenelse: - forall sp e m a s1 s2 v b t, + forall f sp e m a s1 s2 v b t, eval_expr ge sp e m a v -> Val.bool_of_val v b -> - execinf_stmt sp e m (if b then s1 else s2) t -> - execinf_stmt sp e m (Sifthenelse a s1 s2) t + execinf_stmt f sp e m (if b then s1 else s2) t -> + execinf_stmt f sp e m (Sifthenelse a s1 s2) t | execinf_Sseq_1: - forall sp e m t s1 s2, - execinf_stmt sp e m s1 t -> - execinf_stmt sp e m (Sseq s1 s2) t + forall f sp e m t s1 s2, + execinf_stmt f sp e m s1 t -> + execinf_stmt f sp e m (Sseq s1 s2) t | execinf_Sseq_2: - forall sp e m t s1 t1 e1 m1 s2 t2, - exec_stmt sp e m s1 t1 e1 m1 Out_normal -> - execinf_stmt sp e1 m1 s2 t2 -> + forall f sp e m t s1 t1 e1 m1 s2 t2, + exec_stmt f sp e m s1 t1 e1 m1 Out_normal -> + execinf_stmt f sp e1 m1 s2 t2 -> t = t1 *** t2 -> - execinf_stmt sp e m (Sseq s1 s2) t + execinf_stmt f sp e m (Sseq s1 s2) t | execinf_Sloop_body: - forall sp e m s t, - execinf_stmt sp e m s t -> - execinf_stmt sp e m (Sloop s) t + forall f sp e m s t, + execinf_stmt f sp e m s t -> + execinf_stmt f sp e m (Sloop s) t | execinf_Sloop_loop: - forall sp e m s t t1 e1 m1 t2, - exec_stmt sp e m s t1 e1 m1 Out_normal -> - execinf_stmt sp e1 m1 (Sloop s) t2 -> + forall f sp e m s t t1 e1 m1 t2, + exec_stmt f sp e m s t1 e1 m1 Out_normal -> + execinf_stmt f sp e1 m1 (Sloop s) t2 -> t = t1 *** t2 -> - execinf_stmt sp e m (Sloop s) t + execinf_stmt f sp e m (Sloop s) t | execinf_Sblock: - forall sp e m s t, - execinf_stmt sp e m s t -> - execinf_stmt sp e m (Sblock s) t + forall f sp e m s t, + execinf_stmt f sp e m s t -> + execinf_stmt f sp e m (Sblock s) t | execinf_Stailcall: - forall sp e m sig a bl vf vargs f t, + forall f sp e m sig a bl vf vargs fd m' t, eval_expr ge (Vptr sp Int.zero) e m a vf -> eval_exprlist ge (Vptr sp Int.zero) e m bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - evalinf_funcall (Mem.free m sp) f vargs t -> - execinf_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t. + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> + evalinf_funcall m' fd vargs t -> + execinf_stmt f (Vptr sp Int.zero) e m (Stailcall sig a bl) t. End NATURALSEM. @@ -795,15 +808,6 @@ Section BIGSTEP_TO_TRANSITION. Variable prog: program. Let ge := Genv.globalenv prog. -Definition eval_funcall_exec_stmt_ind2 - (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop) - (P2: val -> env -> mem -> stmt -> trace -> - env -> mem -> outcome -> Prop) := - fun a b c d e f g h i j k l m n o p q => - conj - (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q) - (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q). - Inductive outcome_state_match (sp: val) (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := @@ -850,9 +854,9 @@ Lemma eval_funcall_exec_stmt_steps: is_call_cont k -> star step ge (Callstate fd args k m) t (Returnstate res k m')) -/\(forall sp e m s t e' m' out, - exec_stmt ge sp e m s t e' m' out -> - forall f k, +/\(forall f sp e m s t e' m' out, + exec_stmt ge f sp e m s t e' m' out -> + forall k, exists S, star step ge (State f s k sp e m) t S /\ outcome_state_match sp e' m' f k out S). @@ -860,7 +864,7 @@ Proof. apply eval_funcall_exec_stmt_ind2; intros. (* funcall internal *) - destruct (H2 f k) as [S [A B]]. + destruct (H2 k) as [S [A B]]. assert (call_cont k = k) by (apply call_cont_is_call_cont; auto). eapply star_left. econstructor; eauto. eapply star_trans. eexact A. @@ -868,22 +872,22 @@ Proof. (* Out normal *) assert (f.(fn_sig).(sig_res) = None /\ vres = Vundef). destruct f.(fn_sig).(sig_res). contradiction. auto. - destruct H6. subst vres. + destruct H7. subst vres. apply star_one. apply step_skip_call; auto. (* Out_return None *) assert (f.(fn_sig).(sig_res) = None /\ vres = Vundef). destruct f.(fn_sig).(sig_res). contradiction. auto. - destruct H7. subst vres. + destruct H8. subst vres. replace k with (call_cont k') by congruence. apply star_one. apply step_return_0; auto. (* Out_return Some *) assert (f.(fn_sig).(sig_res) <> None /\ vres = v). destruct f.(fn_sig).(sig_res). split; congruence. contradiction. - destruct H8. subst vres. + destruct H9. subst vres. replace k with (call_cont k') by congruence. apply star_one. eapply step_return_1; eauto. (* Out_tailcall_return *) - subst vres. rewrite H5. apply star_refl. + subst vres. red in H4. subst m3. rewrite H6. apply star_refl. reflexivity. traceEq. @@ -913,7 +917,7 @@ Proof. subst e'. constructor. (* ifthenelse *) - destruct (H2 f k) as [S [A B]]. + destruct (H2 k) as [S [A B]]. exists S; split. apply star_left with E0 (State f (if b then s1 else s2) k sp e m) t. econstructor; eauto. exact A. @@ -921,8 +925,8 @@ Proof. auto. (* seq continue *) - destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. - destruct (H2 f k) as [S2 [A2 B2]]. + destruct (H0 (Kseq s2 k)) as [S1 [A1 B1]]. + destruct (H2 k) as [S2 [A2 B2]]. inv B1. exists S2; split. eapply star_left. constructor. @@ -932,7 +936,7 @@ Proof. auto. (* seq stop *) - destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. + destruct (H0 (Kseq s2 k)) as [S1 [A1 B1]]. set (S2 := match out with | Out_exit n => State f (Sexit n) k sp e1 m1 @@ -946,8 +950,8 @@ Proof. unfold S2; inv B1; congruence || simpl; constructor; auto. (* loop loop *) - destruct (H0 f (Kseq (Sloop s) k)) as [S1 [A1 B1]]. - destruct (H2 f k) as [S2 [A2 B2]]. + destruct (H0 (Kseq (Sloop s) k)) as [S1 [A1 B1]]. + destruct (H2 k) as [S2 [A2 B2]]. inv B1. exists S2; split. eapply star_left. constructor. @@ -957,7 +961,7 @@ Proof. auto. (* loop stop *) - destruct (H0 f (Kseq (Sloop s) k)) as [S1 [A1 B1]]. + destruct (H0 (Kseq (Sloop s) k)) as [S1 [A1 B1]]. set (S2 := match out with | Out_exit n => State f (Sexit n) k sp e1 m1 @@ -971,7 +975,7 @@ Proof. unfold S2; inv B1; congruence || simpl; constructor; auto. (* block *) - destruct (H0 f (Kblock k)) as [S1 [A1 B1]]. + destruct (H0 (Kblock k)) as [S1 [A1 B1]]. set (S2 := match out with | Out_normal => State f Sskip k sp e1 m1 @@ -1005,8 +1009,8 @@ Proof. (* tailcall *) econstructor; split. eapply star_left. econstructor; eauto. - apply H4. apply is_call_cont_call_cont. traceEq. - constructor. + apply H5. apply is_call_cont_call_cont. traceEq. + econstructor. Qed. Lemma eval_funcall_steps: @@ -1019,9 +1023,9 @@ Lemma eval_funcall_steps: Proof (proj1 eval_funcall_exec_stmt_steps). Lemma exec_stmt_steps: - forall sp e m s t e' m' out, - exec_stmt ge sp e m s t e' m' out -> - forall f k, + forall f sp e m s t e' m' out, + exec_stmt ge f sp e m s t e' m' out -> + forall k, exists S, star step ge (State f s k sp e m) t S /\ outcome_state_match sp e' m' f k out S. @@ -1034,7 +1038,7 @@ Lemma evalinf_funcall_forever: Proof. cofix CIH_FUN. assert (forall sp e m s T f k, - execinf_stmt ge sp e m s T -> + execinf_stmt ge f sp e m s T -> forever_plus step ge (State f s k sp e m) T). cofix CIH_STMT. intros. inv H. @@ -1055,7 +1059,7 @@ Proof. apply CIH_STMT. eauto. traceEq. (* seq 2 *) - destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kseq s2 k)) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ _ H0 (Kseq s2 k)) as [S [A B]]. inv B. eapply forever_plus_intro. eapply plus_left. constructor. @@ -1069,7 +1073,7 @@ Proof. apply CIH_STMT. eauto. traceEq. (* loop loop *) - destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kseq (Sloop s0) k)) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ _ H0 (Kseq (Sloop s0) k)) as [S [A B]]. inv B. eapply forever_plus_intro. eapply plus_left. constructor. @@ -1100,7 +1104,7 @@ Theorem bigstep_program_terminates_exec: Proof. intros. inv H. econstructor. - econstructor. eauto. eauto. auto. + econstructor; eauto. apply eval_funcall_steps. eauto. red; auto. econstructor. Qed. @@ -1117,14 +1121,10 @@ Proof. 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. + left. econstructor. econstructor; 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_TRANSITION. - -***************************************************) - - -- cgit v1.2.3