From fccd14d21ad7d4848fad1e11ec56ee28486b08af Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 14 Oct 2012 14:01:15 +0000 Subject: Clight: split off the big step semantics in ClightBigstep. Cstrategy: updated the big-step semantics with Eseqand and Eseqor. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2062 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 1 + Makefile | 2 +- cfrontend/Clight.v | 554 ------------------------------------------- cfrontend/ClightBigstep.v | 583 ++++++++++++++++++++++++++++++++++++++++++++++ cfrontend/Cstrategy.v | 118 +++++++++- 5 files changed, 695 insertions(+), 563 deletions(-) create mode 100644 cfrontend/ClightBigstep.v diff --git a/.depend b/.depend index 1c6d223..5fd67ab 100644 --- a/.depend +++ b/.depend @@ -110,6 +110,7 @@ cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqli cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo +cfrontend/ClightBigstep.vo cfrontend/ClightBigstep.glob: cfrontend/ClightBigstep.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo common/Smallstep.vo diff --git a/Makefile b/Makefile index 9e011fa..844697d 100644 --- a/Makefile +++ b/Makefile @@ -93,7 +93,7 @@ BACKEND=\ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Cstrategy.v Cexec.v \ Initializers.v Initializersproof.v \ SimplExpr.v SimplExprspec.v SimplExprproof.v \ - Clight.v Cshmgen.v Cshmgenproof.v \ + Clight.v ClightBigstep.v Cshmgen.v Cshmgenproof.v \ Csharpminor.v Cminorgen.v Cminorgenproof.v # Putting everything together (in driver/) diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index f95cbe6..d1ab673 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -673,557 +673,3 @@ Proof. eapply external_call_trace_length; eauto. Qed. -(** * Alternate big-step semantics *) - -Section BIGSTEP. - -Variable ge: genv. - -(** ** 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 /\ sem_cast v' t' t = Some 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 ge e le m a1 loc ofs -> - eval_expr ge e le m a2 v2 -> - sem_cast v2 (typeof a2) (typeof a1) = Some v -> - assign_loc (typeof a1) m loc ofs v 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 ge e le m a v -> - exec_stmt e le m (Sset id a) - E0 (PTree.set id v le) m Out_normal - | exec_Scall: forall e le m optid a al tyargs tyres vf vargs f t m' vres, - classify_fun (typeof a) = fun_case_f tyargs tyres -> - eval_expr ge e le m a vf -> - eval_exprlist ge e le m al tyargs vargs -> - Genv.find_funct ge vf = Some f -> - type_of_fundef f = Tfunction tyargs tyres -> - eval_funcall m f vargs t m' vres -> - exec_stmt e le m (Scall optid a al) - t (set_opttemp optid vres le) m' Out_normal - | exec_Sbuiltin: forall e le m optid ef al tyargs vargs t m' vres, - eval_exprlist ge e le m al tyargs vargs -> - external_call ef ge vargs m t vres m' -> - exec_stmt e le m (Sbuiltin optid ef tyargs al) - t (set_opttemp optid 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: forall e le m a s1 s2 v1 b t le' m' out, - eval_expr ge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> - exec_stmt e le m (if b then s1 else 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 ge 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_Sloop_stop1: forall e le m s1 s2 t le' m' out' out, - exec_stmt e le m s1 t le' m' out' -> - out_break_or_return out' out -> - exec_stmt e le m (Sloop s1 s2) - t le' m' out - | exec_Sloop_stop2: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 out2 out, - exec_stmt e le m s1 t1 le1 m1 out1 -> - out_normal_or_continue out1 -> - exec_stmt e le1 m1 s2 t2 le2 m2 out2 -> - out_break_or_return out2 out -> - exec_stmt e le m (Sloop s1 s2) - (t1**t2) le2 m2 out - | exec_Sloop_loop: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 t3 le3 m3 out, - exec_stmt e le m s1 t1 le1 m1 out1 -> - out_normal_or_continue out1 -> - exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal -> - exec_stmt e le2 m2 (Sloop s1 s2) t3 le3 m3 out -> - exec_stmt e le m (Sloop s1 s2) - (t1**t2**t3) le3 m3 out - | exec_Sswitch: forall e le m a t n sl le1 m1 out, - eval_expr ge 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: 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 (create_undef_temps f.(fn_temps)) 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 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 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. -Combined Scheme exec_stmt_funcall_ind from exec_stmt_ind2, eval_funcall_ind2. - -(** ** 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: forall e le m optid a al vf tyargs tyres vargs f t, - classify_fun (typeof a) = fun_case_f tyargs tyres -> - eval_expr ge e le m a vf -> - eval_exprlist ge e le m al tyargs vargs -> - Genv.find_funct ge vf = Some f -> - type_of_fundef f = Tfunction tyargs tyres -> - evalinf_funcall m f vargs t -> - execinf_stmt e le m (Scall optid 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: forall e le m a s1 s2 v1 b t, - eval_expr ge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> - execinf_stmt e le m (if b then s1 else s2) t -> - execinf_stmt e le m (Sifthenelse a s1 s2) t - | execinf_Sloop_body1: forall e le m s1 s2 t, - execinf_stmt e le m s1 t -> - execinf_stmt e le m (Sloop s1 s2) t - | execinf_Sloop_body2: forall e le m s1 s2 t1 le1 m1 out1 t2, - exec_stmt e le m s1 t1 le1 m1 out1 -> - out_normal_or_continue out1 -> - execinf_stmt e le1 m1 s2 t2 -> - execinf_stmt e le m (Sloop s1 s2) (t1***t2) - | execinf_Sloop_loop: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 t3, - exec_stmt e le m s1 t1 le1 m1 out1 -> - out_normal_or_continue out1 -> - exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal -> - execinf_stmt e le2 m2 (Sloop s1 s2) t3 -> - execinf_stmt e le m (Sloop s1 s2) (t1***t2***t3) - | execinf_Sswitch: forall e le m a t n sl, - eval_expr ge 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: 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 (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t -> - evalinf_funcall m (Internal f) vargs t. - -End BIGSTEP. - -(** 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 type_int32s -> - eval_funcall ge 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 type_int32s -> - 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. - -Variable prog: program. -Let ge : genv := Genv.globalenv prog. - -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 m fd args t m' res, - eval_funcall ge 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_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 *) - econstructor; split. - eapply star_left. econstructor; eauto. - eapply star_right. apply H5. simpl; auto. econstructor. reflexivity. traceEq. - constructor. - -(* builtin *) - econstructor; split. apply star_one. econstructor; eauto. 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 *) - destruct (H2 f k) as [S1 [A1 B1]]. - exists S1; split. - eapply star_left. 2: eexact A1. eapply step_ifthenelse; eauto. 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. - -(* loop stop 1 *) - destruct (H0 f (Kloop1 s1 s2 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_loop. - 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. - -(* loop stop 2 *) - destruct (H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]]. - destruct (H3 f (Kloop2 s1 s2 k)) as [S2 [A2 B2]]. - set (S3 := - match out2 with - | Out_break => State f Sskip k e le2 m2 - | _ => S2 - end). - exists S3; split. - eapply star_left. eapply step_loop. - eapply star_trans. eexact A1. - eapply star_left with (s2 := State f s2 (Kloop2 s1 s2 k) e le1 m1). - inv H1; inv B1; constructor; auto. - eapply star_trans. eexact A2. - unfold S3. inversion H4; subst. - inv B2. apply star_one. constructor. apply star_refl. - reflexivity. reflexivity. reflexivity. traceEq. - unfold S3. inversion H4; subst. constructor. inv B2; econstructor; eauto. - -(* loop loop *) - destruct (H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]]. - destruct (H3 f (Kloop2 s1 s2 k)) as [S2 [A2 B2]]. - destruct (H5 f k) as [S3 [A3 B3]]. - exists S3; split. - eapply star_left. eapply step_loop. - eapply star_trans. eexact A1. - eapply star_left with (s2 := State f s2 (Kloop2 s1 s2 k) e le1 m1). - inv H1; inv B1; constructor; auto. - eapply star_trans. eexact A2. - eapply star_left with (s2 := State f (Sloop s1 s2) k e le2 m2). - inversion H4; subst; inv B2; constructor; auto. - 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 m fd args t m' res, - eval_funcall ge 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 m fd args T k, - evalinf_funcall ge 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 *) - 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 *) - eapply forever_N_plus. - apply plus_one. eapply step_ifthenelse with (b := b); eauto. - apply CIH_STMT; eauto. traceEq. - -(* loop body 1 *) - eapply forever_N_plus. - eapply plus_one. constructor. - apply CIH_STMT; eauto. traceEq. -(* loop body 2 *) - destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]]. - eapply forever_N_plus with (s2 := State f s2 (Kloop2 s1 s2 k) e le1 m1). - eapply plus_left. constructor. - eapply star_right. eexact A1. - inv H1; inv B1; constructor; auto. - reflexivity. reflexivity. - apply CIH_STMT; eauto. traceEq. -(* loop loop *) - destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]]. - destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H2 f (Kloop2 s1 s2 k)) as [S2 [A2 B2]]. - eapply forever_N_plus with (s2 := State f (Sloop s1 s2) k e le2 m2). - eapply plus_left. constructor. - eapply star_trans. eexact A1. - eapply star_left. inv H1; inv B1; constructor; auto. - eapply star_right. eexact A2. - inv B2. 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_semantics_sound: - bigstep_sound (bigstep_semantics prog) (semantics prog). -Proof. - constructor; simpl; intros. -(* termination *) - inv H. econstructor; econstructor. - split. econstructor; eauto. - split. eapply eval_funcall_steps. eauto. red; auto. - econstructor. -(* 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. - diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v new file mode 100644 index 0000000..7603b6b --- /dev/null +++ b/cfrontend/ClightBigstep.v @@ -0,0 +1,583 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** A big-step semantics for the Clight language. *) + +Require Import Coqlib. +Require Import Errors. +Require Import Maps. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import AST. +Require Import Memory. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Ctypes. +Require Import Cop. +Require Import Clight. + +Section BIGSTEP. + +Variable ge: genv. + +(** ** 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 /\ sem_cast v' t' t = Some 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 ge e le m a1 loc ofs -> + eval_expr ge e le m a2 v2 -> + sem_cast v2 (typeof a2) (typeof a1) = Some v -> + assign_loc (typeof a1) m loc ofs v 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 ge e le m a v -> + exec_stmt e le m (Sset id a) + E0 (PTree.set id v le) m Out_normal + | exec_Scall: forall e le m optid a al tyargs tyres vf vargs f t m' vres, + classify_fun (typeof a) = fun_case_f tyargs tyres -> + eval_expr ge e le m a vf -> + eval_exprlist ge e le m al tyargs vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = Tfunction tyargs tyres -> + eval_funcall m f vargs t m' vres -> + exec_stmt e le m (Scall optid a al) + t (set_opttemp optid vres le) m' Out_normal + | exec_Sbuiltin: forall e le m optid ef al tyargs vargs t m' vres, + eval_exprlist ge e le m al tyargs vargs -> + external_call ef ge vargs m t vres m' -> + exec_stmt e le m (Sbuiltin optid ef tyargs al) + t (set_opttemp optid 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: forall e le m a s1 s2 v1 b t le' m' out, + eval_expr ge e le m a v1 -> + bool_val v1 (typeof a) = Some b -> + exec_stmt e le m (if b then s1 else 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 ge 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_Sloop_stop1: forall e le m s1 s2 t le' m' out' out, + exec_stmt e le m s1 t le' m' out' -> + out_break_or_return out' out -> + exec_stmt e le m (Sloop s1 s2) + t le' m' out + | exec_Sloop_stop2: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 out2 out, + exec_stmt e le m s1 t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + exec_stmt e le1 m1 s2 t2 le2 m2 out2 -> + out_break_or_return out2 out -> + exec_stmt e le m (Sloop s1 s2) + (t1**t2) le2 m2 out + | exec_Sloop_loop: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 t3 le3 m3 out, + exec_stmt e le m s1 t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal -> + exec_stmt e le2 m2 (Sloop s1 s2) t3 le3 m3 out -> + exec_stmt e le m (Sloop s1 s2) + (t1**t2**t3) le3 m3 out + | exec_Sswitch: forall e le m a t n sl le1 m1 out, + eval_expr ge 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: 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 (create_undef_temps f.(fn_temps)) 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 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 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. +Combined Scheme exec_stmt_funcall_ind from exec_stmt_ind2, eval_funcall_ind2. + +(** ** 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: forall e le m optid a al vf tyargs tyres vargs f t, + classify_fun (typeof a) = fun_case_f tyargs tyres -> + eval_expr ge e le m a vf -> + eval_exprlist ge e le m al tyargs vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = Tfunction tyargs tyres -> + evalinf_funcall m f vargs t -> + execinf_stmt e le m (Scall optid 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: forall e le m a s1 s2 v1 b t, + eval_expr ge e le m a v1 -> + bool_val v1 (typeof a) = Some b -> + execinf_stmt e le m (if b then s1 else s2) t -> + execinf_stmt e le m (Sifthenelse a s1 s2) t + | execinf_Sloop_body1: forall e le m s1 s2 t, + execinf_stmt e le m s1 t -> + execinf_stmt e le m (Sloop s1 s2) t + | execinf_Sloop_body2: forall e le m s1 s2 t1 le1 m1 out1 t2, + exec_stmt e le m s1 t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + execinf_stmt e le1 m1 s2 t2 -> + execinf_stmt e le m (Sloop s1 s2) (t1***t2) + | execinf_Sloop_loop: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 t3, + exec_stmt e le m s1 t1 le1 m1 out1 -> + out_normal_or_continue out1 -> + exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal -> + execinf_stmt e le2 m2 (Sloop s1 s2) t3 -> + execinf_stmt e le m (Sloop s1 s2) (t1***t2***t3) + | execinf_Sswitch: forall e le m a t n sl, + eval_expr ge 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: 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 (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t -> + evalinf_funcall m (Internal f) vargs t. + +End BIGSTEP. + +(** 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 type_int32s -> + eval_funcall ge 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 type_int32s -> + 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. + +Variable prog: program. +Let ge : genv := Genv.globalenv prog. + +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 m fd args t m' res, + eval_funcall ge 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_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 *) + econstructor; split. + eapply star_left. econstructor; eauto. + eapply star_right. apply H5. simpl; auto. econstructor. reflexivity. traceEq. + constructor. + +(* builtin *) + econstructor; split. apply star_one. econstructor; eauto. 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 *) + destruct (H2 f k) as [S1 [A1 B1]]. + exists S1; split. + eapply star_left. 2: eexact A1. eapply step_ifthenelse; eauto. 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. + +(* loop stop 1 *) + destruct (H0 f (Kloop1 s1 s2 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_loop. + 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. + +(* loop stop 2 *) + destruct (H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]]. + destruct (H3 f (Kloop2 s1 s2 k)) as [S2 [A2 B2]]. + set (S3 := + match out2 with + | Out_break => State f Sskip k e le2 m2 + | _ => S2 + end). + exists S3; split. + eapply star_left. eapply step_loop. + eapply star_trans. eexact A1. + eapply star_left with (s2 := State f s2 (Kloop2 s1 s2 k) e le1 m1). + inv H1; inv B1; constructor; auto. + eapply star_trans. eexact A2. + unfold S3. inversion H4; subst. + inv B2. apply star_one. constructor. apply star_refl. + reflexivity. reflexivity. reflexivity. traceEq. + unfold S3. inversion H4; subst. constructor. inv B2; econstructor; eauto. + +(* loop loop *) + destruct (H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]]. + destruct (H3 f (Kloop2 s1 s2 k)) as [S2 [A2 B2]]. + destruct (H5 f k) as [S3 [A3 B3]]. + exists S3; split. + eapply star_left. eapply step_loop. + eapply star_trans. eexact A1. + eapply star_left with (s2 := State f s2 (Kloop2 s1 s2 k) e le1 m1). + inv H1; inv B1; constructor; auto. + eapply star_trans. eexact A2. + eapply star_left with (s2 := State f (Sloop s1 s2) k e le2 m2). + inversion H4; subst; inv B2; constructor; auto. + 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 m fd args t m' res, + eval_funcall ge 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 m fd args T k, + evalinf_funcall ge 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 *) + 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 *) + eapply forever_N_plus. + apply plus_one. eapply step_ifthenelse with (b := b); eauto. + apply CIH_STMT; eauto. traceEq. + +(* loop body 1 *) + eapply forever_N_plus. + eapply plus_one. constructor. + apply CIH_STMT; eauto. traceEq. +(* loop body 2 *) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]]. + eapply forever_N_plus with (s2 := State f s2 (Kloop2 s1 s2 k) e le1 m1). + eapply plus_left. constructor. + eapply star_right. eexact A1. + inv H1; inv B1; constructor; auto. + reflexivity. reflexivity. + apply CIH_STMT; eauto. traceEq. +(* loop loop *) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]]. + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H2 f (Kloop2 s1 s2 k)) as [S2 [A2 B2]]. + eapply forever_N_plus with (s2 := State f (Sloop s1 s2) k e le2 m2). + eapply plus_left. constructor. + eapply star_trans. eexact A1. + eapply star_left. inv H1; inv B1; constructor; auto. + eapply star_right. eexact A2. + inv B2. 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_semantics_sound: + bigstep_sound (bigstep_semantics prog) (semantics prog). +Proof. + constructor; simpl; intros. +(* termination *) + inv H. econstructor; econstructor. + split. econstructor; eauto. + split. eapply eval_funcall_steps. eauto. red; auto. + econstructor. +(* 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. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 179361d..0d2f235 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -1607,9 +1607,7 @@ Proof. intros. subst s1. exists s2'; split; auto. apply step_simulation; auto. Qed. -(** * A big-step semantics implementing the reduction strategy. *) - -(** TODO: update with seqand / seqor *) +(** * A big-step semantics for CompCert C implementing the reduction strategy. *) Section BIGSTEP. @@ -1692,8 +1690,29 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := | eval_cast: forall e m a t m' a' ty, eval_expr e m RV a t m' a' -> eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty) + | eval_seqand_true: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v' v, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> + bool_val v1 (typeof a1) = Some true -> + eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> + sem_cast v2 (typeof a2) type_bool = Some v' -> + sem_cast v' type_bool ty = Some v -> + eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty) + | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> + bool_val v1 (typeof a1) = Some false -> + eval_expr e m RV (Eseqand a1 a2 ty) t1 m' (Eval (Vint Int.zero) ty) + | eval_seqor_false: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v' v, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> + bool_val v1 (typeof a1) = Some false -> + eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> + sem_cast v2 (typeof a2) type_bool = Some v' -> + sem_cast v' type_bool ty = Some v -> + eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty) + | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> + bool_val v1 (typeof a1) = Some true -> + eval_expr e m RV (Eseqor a1 a2 ty) t1 m' (Eval (Vint Int.one) ty) | eval_condition: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a' v' b v, - simple a2 = false \/ simple a3 = false -> eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) = Some b -> eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' -> @@ -1926,11 +1945,26 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := | evalinf_cast: forall e m a t ty, evalinf_expr e m RV a t -> evalinf_expr e m RV (Ecast a ty) t + | evalinf_seqand: forall e m a1 a2 ty t1, + evalinf_expr e m RV a1 t1 -> + evalinf_expr e m RV (Eseqand a1 a2 ty) t1 + | evalinf_seqand_2: forall e m a1 a2 ty t1 m' a1' v1 t2, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> + bool_val v1 (typeof a1) = Some true -> + evalinf_expr e m' RV a2 t2 -> + evalinf_expr e m RV (Eseqand a1 a2 ty) (t1***t2) + | evalinf_seqor: forall e m a1 a2 ty t1, + evalinf_expr e m RV a1 t1 -> + evalinf_expr e m RV (Eseqor a1 a2 ty) t1 + | evalinf_seqor_2: forall e m a1 a2 ty t1 m' a1' v1 t2, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> + bool_val v1 (typeof a1) = Some false -> + evalinf_expr e m' RV a2 t2 -> + evalinf_expr e m RV (Eseqor a1 a2 ty) (t1***t2) | evalinf_condition: forall e m a1 a2 a3 ty t1, evalinf_expr e m RV a1 t1 -> evalinf_expr e m RV (Econdition a1 a2 a3 ty) t1 | evalinf_condition_2: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b, - simple a2 = false \/ simple a3 = false -> eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) = Some b -> evalinf_expr e m' RV (if b then a2 else a3) t2 -> @@ -2220,10 +2254,52 @@ Proof. exploit (H0 (fun x => C(Ecast x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. simpl; intuition; eauto. +(* seqand true *) + exploit (H0 (fun x => C(Eseqand x a2 ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + exploit (H4 (fun x => C(Eparen (Eparen x type_bool) ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. + simpl; intuition. eapply star_trans. eexact D. + eapply star_left. left; eapply step_seqand_true; eauto. rewrite B; auto. + eapply star_trans. eexact G. + set (C' := fun x => C (Eparen x ty)). + change (C (Eparen (Eparen a2' type_bool) ty)) with (C' (Eparen a2' type_bool)). + eapply star_two. + left; eapply step_paren; eauto. unfold C'; eapply leftcontext_compose; eauto. repeat constructor. + rewrite F; eauto. + unfold C'. left; eapply step_paren; eauto. constructor. + eauto. eauto. eauto. traceEq. +(* seqand false *) + exploit (H0 (fun x => C(Eseqand x a2 ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition. eapply star_right. eexact D. + left; eapply step_seqand_false; eauto. rewrite B; auto. + traceEq. +(* seqor false *) + exploit (H0 (fun x => C(Eseqor x a2 ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + exploit (H4 (fun x => C(Eparen (Eparen x type_bool) ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. + simpl; intuition. eapply star_trans. eexact D. + eapply star_left. left; eapply step_seqor_false; eauto. rewrite B; auto. + eapply star_trans. eexact G. + set (C' := fun x => C (Eparen x ty)). + change (C (Eparen (Eparen a2' type_bool) ty)) with (C' (Eparen a2' type_bool)). + eapply star_two. + left; eapply step_paren; eauto. unfold C'; eapply leftcontext_compose; eauto. repeat constructor. + rewrite F; eauto. + unfold C'. left; eapply step_paren; eauto. constructor. + eauto. eauto. eauto. traceEq. +(* seqor true *) + exploit (H0 (fun x => C(Eseqor x a2 ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition. eapply star_right. eexact D. + left; eapply step_seqor_true; eauto. rewrite B; auto. + traceEq. (* condition *) - exploit (H1 (fun x => C(Econdition x a2 a3 ty))). + exploit (H0 (fun x => C(Econdition x a2 a3 ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - exploit (H5 (fun x => C(Eparen x ty))). + exploit (H4 (fun x => C(Eparen x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. simpl. split; auto. split; auto. eapply star_trans. eexact D. @@ -2720,12 +2796,38 @@ Proof. eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. eapply COE with (C := fun x => C(Ecast x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* seqand left *) + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Eseqand x a2 ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* seqand 2 *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eseqand x a2 ty)) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + eapply forever_N_plus. eapply plus_right. eexact R. + left; eapply step_seqand_true; eauto. rewrite Q; eauto. + reflexivity. + eapply COE with (C := fun x => (C (Eparen (Eparen x type_bool) ty))). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* seqor left *) + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Eseqor x a2 ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* seqor 2 *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eseqor x a2 ty)) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + eapply forever_N_plus. eapply plus_right. eexact R. + left; eapply step_seqor_false; eauto. rewrite Q; eauto. + reflexivity. + eapply COE with (C := fun x => (C (Eparen (Eparen x type_bool) ty))). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition top *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition *) - destruct (eval_expr_to_steps _ _ _ _ _ _ _ H2 (fun x => C(Econdition x a2 a3 ty)) f k) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Econdition x a2 a3 ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. eapply forever_N_plus. eapply plus_right. eexact R. -- cgit v1.2.3