From ed975ca89e79ea8b046365a8ef7a2f3557b126c0 Mon Sep 17 00:00:00 2001 From: blazy Date: Wed, 25 May 2011 06:35:11 +0000 Subject: Ajout big-step Clight et preuve big-step -> small-step git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1659 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Clight.v | 770 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 769 insertions(+), 1 deletion(-) (limited to 'cfrontend/Clight.v') diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index f183ade8..6d675b32 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -531,7 +531,7 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sreturn None) k e le m) E0 (Returnstate Vundef (call_cont k) m') | step_return_1: forall f a k e le m v v' m', - eval_expr e le m a v -> + eval_expr e le m a v -> cast v (typeof a) f.(fn_return) v' -> Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn (Some a)) k e le m) @@ -583,6 +583,305 @@ Inductive step: state -> trace -> state -> Prop := step (Returnstate v (Kcall (Some id) f e le k) m) E0 (State f Sskip k e (PTree.set id v le) m). + +(** * Alternate big-step semantics *) + +(** ** Big-step semantics for terminating statements and functions *) + +(** The execution of a statement produces an ``outcome'', indicating + how the execution terminated: either normally or prematurely + through the execution of a [break], [continue] or [return] statement. *) + +Inductive outcome: Type := + | Out_break: outcome (**r terminated by [break] *) + | Out_continue: outcome (**r terminated by [continue] *) + | Out_normal: outcome (**r terminated normally *) + | Out_return: option (val * type) -> outcome. (**r terminated by [return] *) + +Inductive out_normal_or_continue : outcome -> Prop := + | Out_normal_or_continue_N: out_normal_or_continue Out_normal + | Out_normal_or_continue_C: out_normal_or_continue Out_continue. + +Inductive out_break_or_return : outcome -> outcome -> Prop := + | Out_break_or_return_B: out_break_or_return Out_break Out_normal + | Out_break_or_return_R: forall ov, + out_break_or_return (Out_return ov) (Out_return ov). + +Definition outcome_switch (out: outcome) : outcome := + match out with + | Out_break => Out_normal + | o => o + end. + +Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := + match out, t with + | Out_normal, Tvoid => v = Vundef + | Out_return None, Tvoid => v = Vundef + | Out_return (Some (v',t')), ty => ty <> Tvoid /\ cast v' t' t v + | _, _ => False + end. + +(** [exec_stmt ge e m1 s t m2 out] describes the execution of + the statement [s]. [out] is the outcome for this execution. + [m1] is the initial memory state, [m2] the final memory state. + [t] is the trace of input/output events performed during this + evaluation. *) + +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 + E0 le m Out_normal + | exec_Sassign: forall e le m a1 a2 loc ofs v2 v m', + eval_lvalue e le m a1 loc ofs -> + eval_expr e le m a2 v2 -> + cast v2 (typeof a2) (typeof a1) v -> + store_value_of_type (typeof a1) m loc ofs v = Some m' -> + exec_stmt e le m (Sassign a1 a2) + E0 le m' Out_normal + | exec_Sset: forall e le m id a v, + eval_expr e le m a v -> + exec_stmt e le m (Sset id a) + E0 (PTree.set id v le) m Out_normal + | exec_Scall_none: forall e le m a al tyargs tyres vf vargs f t m' vres, + typeof a = Tfunction tyargs tyres -> + eval_expr e le m a vf -> + eval_exprlist e le m al tyargs vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = typeof a -> + eval_funcall le m f vargs t m' vres -> + exec_stmt e le m (Scall None a al) + t le m' Out_normal + | exec_Scall_some: forall e le m id a al tyargs tyres vf vargs f t m' vres, + typeof a = Tfunction tyargs tyres -> + eval_expr e le m a vf -> + eval_exprlist e le m al tyargs vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = typeof a -> + eval_funcall le m f vargs t m' vres -> + exec_stmt e le m (Scall (Some id) a al) + t (PTree.set id vres le) m' Out_normal + | exec_Sseq_1: forall e le m s1 s2 t1 le1 m1 t2 le2 m2 out, + exec_stmt e le m s1 t1 le1 m1 Out_normal -> + exec_stmt e le1 m1 s2 t2 le2 m2 out -> + exec_stmt e le m (Ssequence s1 s2) + (t1 ** t2) le2 m2 out + | exec_Sseq_2: forall e le m s1 s2 t1 le1 m1 out, + exec_stmt e le m s1 t1 le1 m1 out -> + out <> Out_normal -> + exec_stmt e le m (Ssequence s1 s2) + t1 le1 m1 out + | exec_Sifthenelse_true: forall e le m a s1 s2 v1 t le' m' out, + eval_expr e le m a v1 -> + is_true v1 (typeof a) -> + exec_stmt e le m s1 t le' m' out -> + exec_stmt e le m (Sifthenelse a s1 s2) + t le' m' out + | exec_Sifthenelse_false: forall e le m a s1 s2 v1 t le' m' out, + eval_expr e le m a v1 -> + is_false v1 (typeof a) -> + exec_stmt e le m s2 t le' m' out -> + exec_stmt e le m (Sifthenelse a s1 s2) + t le' m' out + | exec_Sreturn_none: forall e le m, + exec_stmt e le m (Sreturn None) + E0 le m (Out_return None) + | exec_Sreturn_some: forall e le m a v, + eval_expr e le m a v -> + exec_stmt e le m (Sreturn (Some a)) + E0 le m (Out_return (Some (v, typeof a))) + | exec_Sbreak: forall e le m, + exec_stmt e le m Sbreak + E0 le m Out_break + | exec_Scontinue: forall e le m, + exec_stmt e le m Scontinue + E0 le m Out_continue + | exec_Swhile_false: forall e le m a s v, + eval_expr e le m a v -> + is_false v (typeof a) -> + exec_stmt e le m (Swhile a s) + E0 le m Out_normal + | exec_Swhile_stop: forall e le m a v s t le' m' out' out, + eval_expr e le m a v -> + is_true v (typeof a) -> + exec_stmt e le m s t le' m' out' -> + out_break_or_return out' out -> + exec_stmt e le m (Swhile a s) + t le' m' out + | exec_Swhile_loop: forall e le m a s v t1 le1 m1 out1 t2 le2 m2 out, + eval_expr e le m a v -> + is_true v (typeof a) -> + exec_stmt e le m s t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + exec_stmt e le1 m1 (Swhile a s) t2 le2 m2 out -> + exec_stmt e le m (Swhile a s) + (t1 ** t2) le2 m2 out + | exec_Sdowhile_false: forall e le m s a t le1 m1 out1 v, + exec_stmt e le m s t le1 m1 out1 -> + out_normal_or_continue out1 -> + eval_expr e le1 m1 a v -> + is_false v (typeof a) -> + exec_stmt e le m (Sdowhile a s) + t le1 m1 Out_normal + | exec_Sdowhile_stop: forall e le m s a t le1 m1 out1 out, + exec_stmt e le m s t le1 m1 out1 -> + out_break_or_return out1 out -> + exec_stmt e le m (Sdowhile a s) + t le1 m1 out + | exec_Sdowhile_loop: forall e le m s a le1 m1 le2 m2 t1 t2 out out1 v, + exec_stmt e le m s t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + eval_expr e le1 m1 a v -> + is_true v (typeof a) -> + exec_stmt e le1 m1 (Sdowhile a s) t2 le2 m2 out -> + exec_stmt e le m (Sdowhile a s) + (t1 ** t2) le2 m2 out + + | exec_Sfor_false: forall e le m s a2 a3 v, + eval_expr e le m a2 v -> + is_false v (typeof a2) -> + exec_stmt e le m (Sfor' a2 a3 s) + E0 le m Out_normal + | exec_Sfor_stop: forall e le m s a2 a3 v le1 m1 t out1 out, + eval_expr e le m a2 v -> + is_true v (typeof a2) -> + exec_stmt e le m s t le1 m1 out1 -> + out_break_or_return out1 out -> + exec_stmt e le m (Sfor' a2 a3 s) + t le1 m1 out + | exec_Sfor_loop: forall e le m s a2 a3 v le1 m1 le2 m2 le3 m3 t1 t2 t3 out1 out, + eval_expr e le m a2 v -> + is_true v (typeof a2) -> + exec_stmt e le m s t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + exec_stmt e le1 m1 a3 t2 le2 m2 Out_normal -> + exec_stmt e le2 m2 (Sfor' a2 a3 s) t3 le3 m3 out -> + exec_stmt e le m (Sfor' a2 a3 s) + (t1 ** t2 ** t3) le3 m3 out + | exec_Sswitch: forall e le m a t n sl le1 m1 out, + eval_expr e le m a (Vint n) -> + exec_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t le1 m1 out -> + exec_stmt e le m (Sswitch a sl) + t le1 m1 (outcome_switch out) + +(** [eval_funcall m1 fd args t m2 res] describes the invocation of + function [fd] with arguments [args]. [res] is the value returned + by the call. *) + +with eval_funcall: temp_env -> 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 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 e m1 f.(fn_params) vargs m2 -> + exec_stmt e (PTree.empty val) m2 f.(fn_body) t le m3 out -> + outcome_result_value out f.(fn_return) vres -> + Mem.free_list m3 (blocks_of_env e) = Some m4 -> + eval_funcall (PTree.empty val) m (Internal f) vargs t m4 vres + | eval_funcall_external: forall m ef targs tres vargs t vres m', + external_call ef ge vargs m t vres m' -> + eval_funcall (PTree.empty val) m (External ef targs tres) vargs t m' vres. + +Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop + with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop. + +(** ** Big-step semantics for diverging statements and functions *) + +(** Coinductive semantics for divergence. + [execinf_stmt ge e m s t] holds if the execution of statement [s] + diverges, i.e. loops infinitely. [t] is the possibly infinite + trace of observable events performed during the execution. *) + +CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Prop := + | execinf_Scall_none: forall e le m a al vf tyargs tyres vargs f t, + typeof a = Tfunction tyargs tyres -> + eval_expr e le m a vf -> + eval_exprlist e le m al tyargs vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = typeof a -> + evalinf_funcall le m f vargs t -> + execinf_stmt e le m (Scall None a al) t + | execinf_Scall_some: forall e le m id a al vf tyargs tyres vargs f t, + typeof a = Tfunction tyargs tyres -> + eval_expr e le m a vf -> + eval_exprlist e le m al tyargs vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = typeof a -> + evalinf_funcall le m f vargs t -> + execinf_stmt e le m (Scall (Some id) a al) t + | execinf_Sseq_1: forall e le m s1 s2 t, + execinf_stmt e le m s1 t -> + execinf_stmt e le m (Ssequence s1 s2) t + | execinf_Sseq_2: forall e le m s1 s2 t1 le1 m1 t2, + exec_stmt e le m s1 t1 le1 m1 Out_normal -> + execinf_stmt e le1 m1 s2 t2 -> + execinf_stmt e le m (Ssequence s1 s2) (t1 *** t2) + | execinf_Sifthenelse_true: forall e le m a s1 s2 v1 t, + eval_expr e le m a v1 -> + is_true v1 (typeof a) -> + execinf_stmt e le m s1 t -> + execinf_stmt e le m (Sifthenelse a s1 s2) t + | execinf_Sifthenelse_false: forall e le m a s1 s2 v1 t, + eval_expr e le m a v1 -> + is_false v1 (typeof a) -> + execinf_stmt e le m s2 t -> + execinf_stmt e le m (Sifthenelse a s1 s2) t + | execinf_Swhile_body: forall e le m a v s t, + eval_expr e le m a v -> + is_true v (typeof a) -> + execinf_stmt e le m s t -> + execinf_stmt e le m (Swhile a s) t + | execinf_Swhile_loop: forall e le m a s v t1 le1 m1 out1 t2, + eval_expr e le m a v -> + is_true v (typeof a) -> + exec_stmt e le m s t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + execinf_stmt e le1 m1 (Swhile a s) t2 -> + execinf_stmt e le m (Swhile a s) (t1 *** t2) + | execinf_Sdowhile_body: forall e le m s a t, + execinf_stmt e le m s t -> + execinf_stmt e le m (Sdowhile a s) t + | execinf_Sdowhile_loop: forall e le m s a le1 m1 t1 t2 out1 v, + exec_stmt e le m s t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + eval_expr e le1 m1 a v -> + is_true v (typeof a) -> + execinf_stmt e le1 m1 (Sdowhile a s) t2 -> + execinf_stmt e le m (Sdowhile a s) (t1 *** t2) + | execinf_Sfor_body: forall e le m s a2 a3 v t, + eval_expr e le m a2 v -> + is_true v (typeof a2) -> + execinf_stmt e le m s t -> + execinf_stmt e le m (Sfor' a2 a3 s) t + | execinf_Sfor_next: forall e le m s a2 a3 v le1 m1 t1 t2 out1, + eval_expr e le m a2 v -> + is_true v (typeof a2) -> + exec_stmt e le m s t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + execinf_stmt e le1 m1 a3 t2 -> + execinf_stmt e le m (Sfor' a2 a3 s) (t1 *** t2) + | execinf_Sfor_loop: forall e le m s a2 a3 v le1 m1 le2 m2 t1 t2 t3 out1, + eval_expr e le m a2 v -> + is_true v (typeof a2) -> + exec_stmt e le m s t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + exec_stmt e le1 m1 a3 t2 le2 m2 Out_normal -> + execinf_stmt e le2 m2 (Sfor' a2 a3 s) t3 -> + execinf_stmt e le m (Sfor' a2 a3 s) (t1 *** t2 *** t3) + | execinf_Sswitch: forall e le m a t n sl, + eval_expr e le m a (Vint n) -> + execinf_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t -> + execinf_stmt e le m (Sswitch a sl) t + +(** [evalinf_funcall ge m fd args t] holds if the invocation of function + [fd] on arguments [args] diverges, with observable trace [t]. *) + +with evalinf_funcall:temp_env -> mem -> fundef -> list val -> traceinf -> Prop := + | evalinf_funcall_internal: forall m f vargs t e m1 m2, + alloc_variables 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 e m1 f.(fn_params) vargs m2 -> + execinf_stmt e (PTree.empty val) m2 f.(fn_body) t -> + evalinf_funcall (PTree.empty val) m (Internal f) vargs t. + End SEMANTICS. (** * Whole-program semantics *) @@ -614,3 +913,472 @@ 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. *) + +Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := + | bigstep_program_terminates_intro: forall b f m0 m1 t r, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + type_of_fundef f = Tfunction Tnil (Tint I32 Signed) -> + eval_funcall ge (PTree.empty val) m0 f nil t m1 (Vint r) -> + bigstep_program_terminates p t r. + +Inductive bigstep_program_diverges (p: program): traceinf -> Prop := + | bigstep_program_diverges_intro: forall b f m0 t, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + type_of_fundef f = Tfunction Tnil (Tint I32 Signed) -> + evalinf_funcall ge (PTree.empty val) m0 f nil t -> + bigstep_program_diverges p t. + +(** * Implication from big-step semantics to transition semantics *) + +Section BIGSTEP_TO_TRANSITIONS. + +Variable prog: program. +Let ge : genv := Genv.globalenv prog. + +Definition exec_stmt_eval_funcall_ind + (PS: env -> temp_env -> mem -> statement -> trace -> temp_env -> mem -> outcome -> Prop) + (PF: temp_env -> mem -> fundef -> list val -> trace -> mem -> val -> Prop) := + fun a b c d e f g h i j k l m n o p q r s t u v w x y => + conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y) + (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y). + +Inductive outcome_state_match + (e: env) (le: temp_env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := + | osm_normal: + outcome_state_match e le m f k Out_normal (State f Sskip k e le m) + | osm_break: + outcome_state_match e le m f k Out_break (State f Sbreak k e le m) + | osm_continue: + outcome_state_match e le m f k Out_continue (State f Scontinue k e le m) + | osm_return_none: forall k', + call_cont k' = call_cont k -> + outcome_state_match e le m f k + (Out_return None) (State f (Sreturn None) k' e le m) + | osm_return_some: forall a v k', + call_cont k' = call_cont k -> + eval_expr ge e le m a v -> + outcome_state_match e le m f k + (Out_return (Some (v,typeof a))) (State f (Sreturn (Some a)) k' e le m). + +Lemma is_call_cont_call_cont: + forall k, is_call_cont k -> call_cont k = k. +Proof. + destruct k; simpl; intros; contradiction || auto. +Qed. + +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 -> + forall f k, exists S, + star step ge (State f s k e le m) t S + /\ outcome_state_match e le' m' f k out S) +/\ + (forall le m fd args t m' res, + eval_funcall ge le m fd args t m' res -> + forall k, + is_call_cont k -> + star step ge (Callstate fd args k m) t (Returnstate res k m')). +Proof. + apply exec_stmt_eval_funcall_ind; intros. + +(* skip *) + econstructor; split. apply star_refl. constructor. + +(* assign *) + econstructor; split. apply star_one. econstructor; eauto. constructor. + +(* set *) + econstructor; split. apply star_one. econstructor; eauto. constructor. + +(* call none *) + econstructor; split. + eapply star_left. econstructor; eauto. + eapply star_right. apply H5. simpl; auto. econstructor. reflexivity. traceEq. + constructor. + +(* call some *) + econstructor; split. + eapply star_left. econstructor; eauto. + eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq. + constructor. + +(* sequence 2 *) + destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1. + destruct (H2 f k) as [S2 [A2 B2]]. + econstructor; split. + eapply star_left. econstructor. + eapply star_trans. eexact A1. + eapply star_left. constructor. eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* sequence 1 *) + destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. + set (S2 := + match out with + | Out_break => State f Sbreak k e le1 m1 + | Out_continue => State f Scontinue k e le1 m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. econstructor. + eapply star_trans. eexact A1. + unfold S2; inv B1. + congruence. + apply star_one. apply step_break_seq. + apply star_one. apply step_continue_seq. + apply star_refl. + apply star_refl. + reflexivity. traceEq. + unfold S2; inv B1; congruence || econstructor; eauto. + +(* ifthenelse true *) + destruct (H2 f k) as [S1 [A1 B1]]. + exists S1; split. + eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq. + auto. + +(* ifthenelse false *) + destruct (H2 f k) as [S1 [A1 B1]]. + exists S1; split. + eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq. + auto. + +(* return none *) + econstructor; split. apply star_refl. constructor. auto. + +(* return some *) + econstructor; split. apply star_refl. econstructor; eauto. + +(* break *) + econstructor; split. apply star_refl. constructor. + +(* continue *) + econstructor; split. apply star_refl. constructor. + +(* while false *) + econstructor; split. + apply star_one. eapply step_while_false; eauto. + constructor. + +(* while stop *) + destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. + set (S2 := + match out' with + | Out_break => State f Sskip k e le' m' + | _ => S1 + end). + exists S2; split. + eapply star_left. eapply step_while_true; eauto. + eapply star_trans. eexact A1. + unfold S2. inversion H3; subst. + inv B1. apply star_one. constructor. + apply star_refl. + reflexivity. traceEq. + unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. + +(* while loop *) + destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. + destruct (H5 f k) as [S2 [A2 B2]]. + exists S2; split. + eapply star_left. eapply step_while_true; eauto. + eapply star_trans. eexact A1. + eapply star_left. + inv H3; inv B1; apply step_skip_or_continue_while; auto. + eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* dowhile false *) + destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. + exists (State f Sskip k e le1 m1); split. + eapply star_left. constructor. + eapply star_right. eexact A1. + inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto. + reflexivity. traceEq. + constructor. + +(* dowhile stop *) + destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. + set (S2 := + match out1 with + | Out_break => State f Sskip k e le1 m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. apply step_dowhile. + eapply star_trans. eexact A1. + unfold S2. inversion H1; subst. + inv B1. apply star_one. constructor. + apply star_refl. + reflexivity. traceEq. + unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto. + +(* dowhile loop *) + destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. + destruct (H5 f k) as [S2 [A2 B2]]. + exists S2; split. + eapply star_left. apply step_dowhile. + eapply star_trans. eexact A1. + eapply star_left. + inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. + eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* for false *) + econstructor; split. + eapply star_one. eapply step_for_false; eauto. + constructor. + +(* for stop *) + destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. + set (S2 := + match out1 with + | Out_break => State f Sskip k e le1 m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. eapply step_for_true; eauto. + eapply star_trans. eexact A1. + unfold S2. inversion H3; subst. + inv B1. apply star_one. constructor. + apply star_refl. + reflexivity. traceEq. + unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. + +(* for loop *) + destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. + destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2. + destruct (H7 f k) as [S3 [A3 B3]]. + exists S3; split. + eapply star_left. eapply step_for_true; eauto. + eapply star_trans. eexact A1. + eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e le1 m1). + inv H3; inv B1. + apply star_one. constructor. auto. + apply star_one. constructor. auto. + eapply star_trans. eexact A2. + eapply star_left. constructor. + eexact A3. + reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + auto. + +(* switch *) + destruct (H1 f (Kswitch k)) as [S1 [A1 B1]]. + set (S2 := + match out with + | Out_normal => State f Sskip k e le1 m1 + | Out_break => State f Sskip k e le1 m1 + | Out_continue => State f Scontinue k e le1 m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. eapply step_switch; eauto. + eapply star_trans. eexact A1. + unfold S2; inv B1. + apply star_one. constructor. auto. + apply star_one. constructor. auto. + apply star_one. constructor. + apply star_refl. + apply star_refl. + reflexivity. traceEq. + 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. + 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. + (* 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. + apply step_return_0; auto. + (* Out_return Some *) + destruct H4. + rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. + eapply step_return_1; eauto. + reflexivity. traceEq. + +(* call external *) + apply star_one. apply step_external_function; auto. +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 -> + forall f k, exists S, + star step 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 le m fd args t m' res, + eval_funcall ge le m fd args t m' res -> + forall k, + is_call_cont k -> + star step 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 le m fd args T k, + evalinf_funcall ge le m fd args T -> + forever_N step 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 step order ge tt (State f s k e le m) T). + cofix CIH_STMT. + intros. inv H. + +(* call none *) + eapply forever_N_plus. + apply plus_one. eapply step_call; eauto. + eapply CIH_FUN. eauto. traceEq. +(* call some *) + eapply forever_N_plus. + apply plus_one. eapply step_call; eauto. + eapply CIH_FUN. eauto. traceEq. + +(* seq 1 *) + eapply forever_N_plus. + apply plus_one. econstructor. + apply CIH_STMT; eauto. traceEq. +(* seq 2 *) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]]. + inv B1. + eapply forever_N_plus. + eapply plus_left. constructor. eapply star_trans. eexact A1. + apply star_one. constructor. reflexivity. reflexivity. + apply CIH_STMT; eauto. traceEq. + +(* ifthenelse true *) + eapply forever_N_plus. + apply plus_one. eapply step_ifthenelse_true; eauto. + apply CIH_STMT; eauto. traceEq. +(* ifthenelse false *) + eapply forever_N_plus. + apply plus_one. eapply step_ifthenelse_false; eauto. + apply CIH_STMT; eauto. traceEq. + +(* while body *) + eapply forever_N_plus. + eapply plus_one. eapply step_while_true; eauto. + apply CIH_STMT; eauto. traceEq. +(* while loop *) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]]. + eapply forever_N_plus with (s2 := State f (Swhile a s0) k e le1 m1). + eapply plus_left. eapply step_while_true; eauto. + eapply star_right. eexact A1. + inv H3; inv B1; apply step_skip_or_continue_while; auto. + reflexivity. reflexivity. + apply CIH_STMT; eauto. traceEq. + +(* dowhile body *) + eapply forever_N_plus. + eapply plus_one. eapply step_dowhile. + apply CIH_STMT; eauto. + traceEq. + +(* dowhile loop *) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]]. + eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e le1 m1). + eapply plus_left. eapply step_dowhile. + eapply star_right. eexact A1. + inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. + reflexivity. reflexivity. + apply CIH_STMT. eauto. + traceEq. + +(* for body *) + eapply forever_N_plus. + apply plus_one. eapply step_for_true; eauto. + apply CIH_STMT; eauto. + traceEq. + +(* for next *) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. + eapply forever_N_plus. + eapply plus_left. eapply step_for_true; eauto. + eapply star_trans. eexact A1. + apply star_one. + inv H3; inv B1; apply step_skip_or_continue_for2; auto. + reflexivity. reflexivity. + apply CIH_STMT; eauto. + traceEq. + +(* for body *) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]]. + inv B2. + eapply forever_N_plus. + eapply plus_left. eapply step_for_true; eauto. + eapply star_trans. eexact A1. + eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto. + eapply star_right. eexact A2. + constructor. + reflexivity. reflexivity. reflexivity. reflexivity. + apply CIH_STMT; eauto. + traceEq. + +(* switch *) + eapply forever_N_plus. + eapply plus_one. eapply step_switch; eauto. + apply CIH_STMT; eauto. + traceEq. + +(* call internal *) + intros. inv H0. + eapply forever_N_plus. + eapply plus_one. econstructor; eauto. + apply H; eauto. + traceEq. +Qed. + +Theorem bigstep_program_terminates_exec: + forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). +Proof. + intros. inv H. + 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. +Qed. + +End BIGSTEP_TO_TRANSITIONS. -- cgit