From 3358c5ebecf24aec90df610b0cd46585d6af70ca Mon Sep 17 00:00:00 2001 From: Lélio Brun Date: Thu, 30 Jun 2016 17:05:58 +0200 Subject: Semantics parametrized by function entry --- cfrontend/ClightBigstep.v | 89 ++++++++++++++++++++++++++++------------------- 1 file changed, 53 insertions(+), 36 deletions(-) diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index 92457586..2bccf60a 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -74,6 +74,8 @@ Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem): Prop [t] is the trace of input/output events performed during this evaluation. *) +Variable function_entry: function -> list val -> mem -> env -> temp_env -> mem -> Prop. + Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> mem -> outcome -> Prop := | exec_Sskip: forall e le m, exec_stmt e le m Sskip @@ -163,14 +165,12 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> by the call. *) with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := - | eval_funcall_internal: forall le m f vargs t e m1 m2 m3 out vres m4, - alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> - list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - bind_parameters ge e m1 f.(fn_params) vargs m2 -> - exec_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t le m3 out -> - outcome_result_value out f.(fn_return) vres m3 -> - Mem.free_list m3 (blocks_of_env ge e) = Some m4 -> - eval_funcall m (Internal f) vargs t m4 vres + | eval_funcall_internal: forall m f vargs t e le1 le2 m1 m2 out vres m3, + function_entry f vargs m e le1 m1 -> + exec_stmt e le1 m1 f.(fn_body) t le2 m2 out -> + outcome_result_value out f.(fn_return) vres m2 -> + Mem.free_list m2 (blocks_of_env ge e) = Some m3 -> + eval_funcall m (Internal f) vargs t m3 vres | eval_funcall_external: forall m ef targs tres cconv vargs t vres m', external_call ef ge vargs m t vres m' -> eval_funcall m (External ef targs tres cconv) vargs t m' vres. @@ -231,17 +231,19 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro [fd] on arguments [args] diverges, with observable trace [t]. *) with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := - | evalinf_funcall_internal: forall m f vargs t e m1 m2, - alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> - list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - bind_parameters ge e m1 f.(fn_params) vargs m2 -> - execinf_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t -> + | evalinf_funcall_internal: forall m f vargs t e m1 le1, + function_entry f vargs m e le1 m1 -> + execinf_stmt e le1 m1 f.(fn_body) t -> evalinf_funcall m (Internal f) vargs t. End BIGSTEP. (** Big-step execution of a whole program. *) +Section ENTRY. + +Variable function_entry: genv -> function -> list val -> mem -> env -> temp_env -> mem -> Prop. + Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := | bigstep_program_terminates_intro: forall b f m0 m1 t r, let ge := globalenv p in @@ -249,7 +251,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> type_of_fundef f = Tfunction Tnil type_int32s cc_default -> - eval_funcall ge m0 f nil t m1 (Vint r) -> + eval_funcall ge (function_entry ge) m0 f nil t m1 (Vint r) -> bigstep_program_terminates p t r. Inductive bigstep_program_diverges (p: program): traceinf -> Prop := @@ -259,12 +261,14 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> type_of_fundef f = Tfunction Tnil type_int32s cc_default -> - evalinf_funcall ge m0 f nil t -> + evalinf_funcall ge (function_entry 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). +End ENTRY. + (** * Implication from big-step semantics to transition semantics *) Section BIGSTEP_TO_TRANSITIONS. @@ -296,18 +300,31 @@ Proof. destruct k; simpl; intros; contradiction || auto. Qed. +Variable function_entry: genv -> function -> list val -> mem -> env -> temp_env -> mem -> Prop. + +Definition exec_stmt_fe (ge: genv) := exec_stmt ge (function_entry ge). +Definition eval_funcall_fe (ge: genv) := eval_funcall ge (function_entry ge). +Definition execinf_stmt_fe (ge: genv) := execinf_stmt ge (function_entry ge). +Definition evalinf_funcall_fe (ge: genv) := evalinf_funcall ge (function_entry ge). +Definition bigstep_semantics_fe := bigstep_semantics function_entry. + +Definition step_fe (ge: genv) := step ge (function_entry ge). +Definition semantics_fe (p: program) := + let ge := globalenv p in + Semantics_gen step_fe (initial_state p) final_state ge ge. + Lemma exec_stmt_eval_funcall_steps: (forall e le m s t le' m' out, - exec_stmt ge e le m s t le' m' out -> + exec_stmt_fe ge e le m s t le' m' out -> forall f k, exists S, - star step1 ge (State f s k e le m) t S + star step_fe ge (State f s k e le m) t S /\ outcome_state_match e le' m' f k out S) /\ (forall m fd args t m' res, - eval_funcall ge m fd args t m' res -> + eval_funcall_fe ge m fd args t m' res -> forall k, is_call_cont k -> - star step1 ge (Callstate fd args k m) t (Returnstate res k m')). + star step_fe ge (Callstate fd args k m) t (Returnstate res k m')). Proof. apply exec_stmt_funcall_ind; intros. @@ -450,23 +467,23 @@ Proof. unfold S2. inv B1; simpl; econstructor; eauto. (* call internal *) - destruct (H3 f k) as [S1 [A1 B1]]. - eapply star_left. eapply step_internal_function; eauto. econstructor; eauto. + destruct (H1 f k) as [S1 [A1 B1]]. + eapply star_left. eapply step_internal_function; eauto. eapply star_right. eexact A1. inv B1; simpl in H4; try contradiction. (* Out_normal *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. - destruct H7. subst vres. apply step_skip_call; auto. + destruct H5. subst vres. apply step_skip_call; auto. (* Out_return None *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. - destruct H8. subst vres. - rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. + destruct H6. subst vres. + rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. apply step_return_0; auto. (* Out_return Some *) - destruct H4. - rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. + destruct H2. + rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. eapply step_return_1; eauto. reflexivity. traceEq. @@ -476,31 +493,31 @@ Qed. Lemma exec_stmt_steps: forall e le m s t le' m' out, - exec_stmt ge e le m s t le' m' out -> + exec_stmt_fe ge e le m s t le' m' out -> forall f k, exists S, - star step1 ge (State f s k e le m) t S + star step_fe ge (State f s k e le m) t S /\ outcome_state_match e le' m' f k out S. Proof (proj1 exec_stmt_eval_funcall_steps). Lemma eval_funcall_steps: forall m fd args t m' res, - eval_funcall ge m fd args t m' res -> + eval_funcall_fe ge m fd args t m' res -> forall k, is_call_cont k -> - star step1 ge (Callstate fd args k m) t (Returnstate res k m'). + star step_fe ge (Callstate fd args k m) t (Returnstate res k m'). Proof (proj2 exec_stmt_eval_funcall_steps). Definition order (x y: unit) := False. Lemma evalinf_funcall_forever: forall m fd args T k, - evalinf_funcall ge m fd args T -> - forever_N step1 order ge tt (Callstate fd args k m) T. + evalinf_funcall_fe ge m fd args T -> + forever_N step_fe order ge tt (Callstate fd args k m) T. Proof. cofix CIH_FUN. assert (forall e le m s T f k, - execinf_stmt ge e le m s T -> - forever_N step1 order ge tt (State f s k e le m) T). + execinf_stmt_fe ge e le m s T -> + forever_N step_fe order ge tt (State f s k e le m) T). cofix CIH_STMT. intros. inv H. @@ -559,13 +576,13 @@ Proof. (* call internal *) intros. inv H0. eapply forever_N_plus. - eapply plus_one. econstructor; eauto. econstructor; eauto. + eapply plus_one. econstructor; eauto. apply H; eauto. traceEq. Qed. Theorem bigstep_semantics_sound: - bigstep_sound (bigstep_semantics prog) (semantics1 prog). + bigstep_sound (bigstep_semantics_fe prog) (semantics_fe prog). Proof. constructor; simpl; intros. (* termination *) -- cgit