From 213bf38509f4f92545d4c5749c25a55b9a9dda36 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 3 Aug 2009 15:32:27 +0000 Subject: Transition semantics for Clight and Csharpminor git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csem.v | 975 +++++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 876 insertions(+), 99 deletions(-) (limited to 'cfrontend/Csem.v') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 248192cc..fb8b8e1a 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -355,7 +355,7 @@ Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int := | I8, Unsigned => Int.zero_ext 8 i | I16, Signed => Int.sign_ext 16 i | I16, Unsigned => Int.zero_ext 16 i - | I32 , _ => i + | I32, _ => i end. Definition cast_int_float (si : signedness) (i: int) : float := @@ -422,49 +422,6 @@ Definition env := PTree.t block. (* map variable -> location *) Definition empty_env: env := (PTree.empty block). -(** 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 -> 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'), ty => ty <> Tvoid /\ v'=v - | _, _ => False - end. - -(** Selection of the appropriate case of a [switch], given the value [n] - of the selector expression. *) - -Fixpoint select_switch (n: int) (sl: labeled_statements) - {struct sl}: labeled_statements := - match sl with - | LSdefault _ => sl - | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' - end. - (** [load_value_of_type ty m b ofs] computes the value of a datum of type [ty] residing in memory [m] at block [b], offset [ofs]. If the type [ty] indicates an access by value, the corresponding @@ -491,24 +448,23 @@ Definition store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) end. (** Allocation of function-local variables. - [alloc_variables e1 m1 vars e2 m2 bl] allocates one memory block + [alloc_variables e1 m1 vars e2 m2] allocates one memory block for each variable declared in [vars], and associates the variable name with this block. [e1] and [m1] are the initial local environment and memory state. [e2] and [m2] are the final local environment - and memory state. The list [bl] collects the references to all - the blocks that were allocated. *) + and memory state. *) Inductive alloc_variables: env -> mem -> list (ident * type) -> - env -> mem -> list block -> Prop := + env -> mem -> Prop := | alloc_variables_nil: forall e m, - alloc_variables e m nil e m nil + alloc_variables e m nil e m | alloc_variables_cons: - forall e m id ty vars m1 b1 m2 e2 lb, + forall e m id ty vars m1 b1 m2 e2, Mem.alloc m 0 (sizeof ty) = (m1, b1) -> - alloc_variables (PTree.set id b1 e) m1 vars e2 m2 lb -> - alloc_variables e m ((id, ty) :: vars) e2 m2 (b1 :: lb). + alloc_variables (PTree.set id b1 e) m1 vars e2 m2 -> + alloc_variables e m ((id, ty) :: vars) e2 m2. (** Initialization of local variables that are parameters to a function. [bind_parameters e m1 params args m2] stores the values [args] @@ -528,10 +484,35 @@ Inductive bind_parameters: env -> bind_parameters e m1 params vl m2 -> bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. -Section RELSEM. +(** Return the list of blocks in the codomain of [e]. *) + +Definition blocks_of_env (e: env) : list block := + List.map (@snd ident block) (PTree.elements e). + +(** Selection of the appropriate case of a [switch], given the value [n] + of the selector expression. *) + +Fixpoint select_switch (n: int) (sl: labeled_statements) + {struct sl}: labeled_statements := + match sl with + | LSdefault _ => sl + | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' + end. + +(** Turn a labeled statement into a sequence *) + +Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement := + match sl with + | LSdefault s => s + | LScase c s sl' => Ssequence s (seq_of_labeled_statement sl') + end. + +Section SEMANTICS. Variable ge: genv. +(** ** Evaluation of expressions *) + Section EXPR. Variable e: env. @@ -640,6 +621,322 @@ Inductive eval_exprlist: list expr -> list val -> Prop := End EXPR. +(** ** Transition semantics for statements and functions *) + +(** Continuations *) + +Inductive cont: Type := + | Kstop: cont + | Kseq: statement -> cont -> cont + (* [Kseq s2 k] = after [s1] in [s1;s2] *) + | Kwhile: expr -> statement -> cont -> cont + (* [Kwhile e s k] = after [s] in [while (e) s] *) + | Kdowhile: expr -> statement -> cont -> cont + (* [Kdowhile e s k] = after [s] in [do s while (e)] *) + | Kfor2: expr -> statement -> statement -> cont -> cont + (* [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *) + | Kfor3: expr -> statement -> statement -> cont -> cont + (* [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *) + | Kswitch: cont -> cont + (* catches [break] statements arising out of [switch] *) + | Kcall: option (block * int * type) -> (* where to store result *) + function -> (* calling function *) + env -> (* local env of calling function *) + cont -> cont. + +(** Pop continuation until a call or stop *) + +Fixpoint call_cont (k: cont) : cont := + match k with + | Kseq s k => call_cont k + | Kwhile e s k => call_cont k + | Kdowhile e s k => call_cont k + | Kfor2 e2 e3 s k => call_cont k + | Kfor3 e2 e3 s k => call_cont k + | Kswitch k => call_cont k + | _ => k + end. + +Definition is_call_cont (k: cont) : Prop := + match k with + | Kstop => True + | Kcall _ _ _ _ => True + | _ => False + end. + +(** States *) + +Inductive state: Type := + | State + (f: function) + (s: statement) + (k: cont) + (e: env) + (m: mem) : state + | Callstate + (fd: fundef) + (args: list val) + (k: cont) + (m: mem) : state + | Returnstate + (res: val) + (k: cont) + (m: mem) : state. + +(** Find the statement and manufacture the continuation + corresponding to a label *) + +Fixpoint find_label (lbl: label) (s: statement) (k: cont) + {struct s}: option (statement * cont) := + match s with + | Ssequence s1 s2 => + match find_label lbl s1 (Kseq s2 k) with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Sifthenelse a s1 s2 => + match find_label lbl s1 k with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Swhile a s1 => + find_label lbl s1 (Kwhile a s1 k) + | Sdowhile a s1 => + find_label lbl s1 (Kdowhile a s1 k) + | Sfor a1 a2 a3 s1 => + match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with + | Some sk => Some sk + | None => + match find_label lbl s1 (Kfor2 a2 a3 s1 k) with + | Some sk => Some sk + | None => find_label lbl a3 (Kfor3 a2 a3 s1 k) + end + end + | Sswitch e sl => + find_label_ls lbl sl (Kswitch k) + | Slabel lbl' s' => + if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k + | _ => None + end + +with find_label_ls (lbl: label) (sl: labeled_statements) (k: cont) + {struct sl}: option (statement * cont) := + match sl with + | LSdefault s => find_label lbl s k + | LScase _ s sl' => + match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with + | Some sk => Some sk + | None => find_label_ls lbl sl' k + end + end. + +(** Transition relation *) + +Inductive step: state -> trace -> state -> Prop := + + | step_assign: forall f a1 a2 k e m loc ofs v2 m', + eval_lvalue e m a1 loc ofs -> + eval_expr e m a2 v2 -> + store_value_of_type (typeof a1) m loc ofs v2 = Some m' -> + step (State f (Sassign a1 a2) k e m) + E0 (State f Sskip k e m') + + | step_call_none: forall f a al k e m vf vargs fd, + eval_expr e m a vf -> + eval_exprlist e m al vargs -> + Genv.find_funct ge vf = Some fd -> + type_of_fundef fd = typeof a -> + step (State f (Scall None a al) k e m) + E0 (Callstate fd vargs (Kcall None f e k) m) + + | step_call_some: forall f lhs a al k e m loc ofs vf vargs fd, + eval_lvalue e m lhs loc ofs -> + eval_expr e m a vf -> + eval_exprlist e m al vargs -> + Genv.find_funct ge vf = Some fd -> + type_of_fundef fd = typeof a -> + step (State f (Scall (Some lhs) a al) k e m) + E0 (Callstate fd vargs (Kcall (Some(loc, ofs, typeof lhs)) f e k) m) + + | step_seq: forall f s1 s2 k e m, + step (State f (Ssequence s1 s2) k e m) + E0 (State f s1 (Kseq s2 k) e m) + | step_skip_seq: forall f s k e m, + step (State f Sskip (Kseq s k) e m) + E0 (State f s k e m) + | step_continue_seq: forall f s k e m, + step (State f Scontinue (Kseq s k) e m) + E0 (State f Scontinue k e m) + | step_break_seq: forall f s k e m, + step (State f Sbreak (Kseq s k) e m) + E0 (State f Sbreak k e m) + + | step_ifthenelse_true: forall f a s1 s2 k e m v1, + eval_expr e m a v1 -> + is_true v1 (typeof a) -> + step (State f (Sifthenelse a s1 s2) k e m) + E0 (State f s1 k e m) + | step_ifthenelse_false: forall f a s1 s2 k e m v1, + eval_expr e m a v1 -> + is_false v1 (typeof a) -> + step (State f (Sifthenelse a s1 s2) k e m) + E0 (State f s2 k e m) + + | step_while_false: forall f a s k e m v, + eval_expr e m a v -> + is_false v (typeof a) -> + step (State f (Swhile a s) k e m) + E0 (State f Sskip k e m) + | step_while_true: forall f a s k e m v, + eval_expr e m a v -> + is_true v (typeof a) -> + step (State f (Swhile a s) k e m) + E0 (State f s (Kwhile a s k) e m) + | step_skip_or_continue_while: forall f x a s k e m, + x = Sskip \/ x = Scontinue -> + step (State f x (Kwhile a s k) e m) + E0 (State f (Swhile a s) k e m) + | step_break_while: forall f a s k e m, + step (State f Sbreak (Kwhile a s k) e m) + E0 (State f Sskip k e m) + + | step_dowhile: forall f a s k e m, + step (State f (Sdowhile a s) k e m) + E0 (State f s (Kdowhile a s k) e m) + | step_skip_or_continue_dowhile_false: forall f x a s k e m v, + x = Sskip \/ x = Scontinue -> + eval_expr e m a v -> + is_false v (typeof a) -> + step (State f x (Kdowhile a s k) e m) + E0 (State f Sskip k e m) + | step_skip_or_continue_dowhile_true: forall f x a s k e m v, + x = Sskip \/ x = Scontinue -> + eval_expr e m a v -> + is_true v (typeof a) -> + step (State f x (Kdowhile a s k) e m) + E0 (State f (Sdowhile a s) k e m) + | step_break_dowhile: forall f a s k e m, + step (State f Sbreak (Kdowhile a s k) e m) + E0 (State f Sskip k e m) + + | step_for_start: forall f a1 a2 a3 s k e m, + a1 <> Sskip -> + step (State f (Sfor a1 a2 a3 s) k e m) + E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) + | step_for_false: forall f a2 a3 s k e m v, + eval_expr e m a2 v -> + is_false v (typeof a2) -> + step (State f (Sfor Sskip a2 a3 s) k e m) + E0 (State f Sskip k e m) + | step_for_true: forall f a2 a3 s k e m v, + eval_expr e m a2 v -> + is_true v (typeof a2) -> + step (State f (Sfor Sskip a2 a3 s) k e m) + E0 (State f s (Kfor2 a2 a3 s k) e m) + | step_skip_or_continue_for2: forall f x a2 a3 s k e m, + x = Sskip \/ x = Scontinue -> + step (State f x (Kfor2 a2 a3 s k) e m) + E0 (State f a3 (Kfor3 a2 a3 s k) e m) + | step_break_for2: forall f a2 a3 s k e m, + step (State f Sbreak (Kfor2 a2 a3 s k) e m) + E0 (State f Sskip k e m) + | step_skip_for3: forall f a2 a3 s k e m, + step (State f Sskip (Kfor3 a2 a3 s k) e m) + E0 (State f (Sfor Sskip a2 a3 s) k e m) + + | step_return_0: forall f k e m, + f.(fn_return) = Tvoid -> + step (State f (Sreturn None) k e m) + E0 (Returnstate Vundef (call_cont k) (Mem.free_list m (blocks_of_env e))) + | step_return_1: forall f a k e m v, + f.(fn_return) <> Tvoid -> + eval_expr e m a v -> + step (State f (Sreturn (Some a)) k e m) + E0 (Returnstate v (call_cont k) (Mem.free_list m (blocks_of_env e))) + | step_skip_call: forall f k e m, + is_call_cont k -> + f.(fn_return) = Tvoid -> + step (State f Sskip k e m) + E0 (Returnstate Vundef k (Mem.free_list m (blocks_of_env e))) + + | step_switch: forall f a sl k e m n, + eval_expr e m a (Vint n) -> + step (State f (Sswitch a sl) k e m) + E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m) + | step_skip_break_switch: forall f x k e m, + x = Sskip \/ x = Sbreak -> + step (State f x (Kswitch k) e m) + E0 (State f Sskip k e m) + | step_continue_switch: forall f k e m, + step (State f Scontinue (Kswitch k) e m) + E0 (State f Scontinue k e m) + + | step_label: forall f lbl s k e m, + step (State f (Slabel lbl s) k e m) + E0 (State f s k e m) + + | step_goto: forall f lbl k e m s' k', + find_label lbl f.(fn_body) (call_cont k) = Some (s', k') -> + step (State f (Sgoto lbl) k e m) + E0 (State f s' k' e m) + + | step_internal_function: forall f vargs k m e m1 m2, + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> + bind_parameters e m1 f.(fn_params) vargs m2 -> + step (Callstate (Internal f) vargs k m) + E0 (State f f.(fn_body) k e m2) + + | step_external_function: forall id targs tres vargs k m vres t, + event_match (external_function id targs tres) vargs t vres -> + step (Callstate (External id targs tres) vargs k m) + t (Returnstate vres k m) + + | step_returnstate_0: forall v f e k m, + step (Returnstate v (Kcall None f e k) m) + E0 (State f Sskip k e m) + + | step_returnstate_1: forall v f e k m m' loc ofs ty, + store_value_of_type ty m loc ofs v = Some m' -> + step (Returnstate v (Kcall (Some(loc, ofs, ty)) f e k) m) + E0 (State f Sskip k e 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 -> 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'), ty => ty <> Tvoid /\ v'=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. @@ -778,44 +1075,29 @@ Inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop (t1 ** t2 ** t3) m3 out | exec_Sswitch: forall e m a t n sl m1 out, eval_expr e m a (Vint n) -> - exec_lblstmts e m (select_switch n sl) t m1 out -> + exec_stmt e m (seq_of_labeled_statement (select_switch n sl)) t m1 out -> exec_stmt e m (Sswitch a sl) t m1 (outcome_switch out) -(** [exec_lblstmts ge e m1 ls t m2 out] is a variant of [exec_stmt] - that executes in sequence all statements in the list of labeled - statements [ls]. *) - -with exec_lblstmts: env -> mem -> labeled_statements -> trace -> mem -> outcome -> Prop := - | exec_LSdefault: forall e m s t m1 out, - exec_stmt e m s t m1 out -> - exec_lblstmts e m (LSdefault s) t m1 out - | exec_LScase_fallthrough: forall e m n s ls t1 m1 t2 m2 out, - exec_stmt e m s t1 m1 Out_normal -> - exec_lblstmts e m1 ls t2 m2 out -> - exec_lblstmts e m (LScase n s ls) (t1 ** t2) m2 out - | exec_LScase_stop: forall e m n s ls t m1 out, - exec_stmt e m s t m1 out -> out <> Out_normal -> - exec_lblstmts e m (LScase n s ls) t m1 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 m f vargs t e m1 lb m2 m3 out vres, - alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 lb -> + | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres, + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters e m1 f.(fn_params) vargs m2 -> exec_stmt e m2 f.(fn_body) t m3 out -> outcome_result_value out f.(fn_return) vres -> - eval_funcall m (Internal f) vargs t (Mem.free_list m3 lb) vres + eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres | eval_funcall_external: forall m id targs tres vargs t vres, event_match (external_function id targs tres) vargs t vres -> eval_funcall m (External id targs tres) vargs t m vres. -Scheme exec_stmt_ind3 := Minimality for exec_stmt Sort Prop - with exec_lblstmts_ind3 := Minimality for exec_lblstmts Sort Prop - with eval_funcall_ind3 := Minimality for eval_funcall Sort Prop. +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] @@ -823,13 +1105,21 @@ Scheme exec_stmt_ind3 := Minimality for exec_stmt Sort Prop trace of observable events performed during the execution. *) CoInductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop := - | execinf_Scall: forall e m lhs a al vf vargs f t, + | execinf_Scall_none: forall e m a al vf vargs f t, + eval_expr e m a vf -> + eval_exprlist e m al vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = typeof a -> + evalinf_funcall m f vargs t -> + execinf_stmt e m (Scall None a al) t + | execinf_Scall_some: forall e m lhs a al loc ofs vf vargs f t, + eval_lvalue e m lhs loc ofs -> eval_expr e m a vf -> eval_exprlist e m al vargs -> Genv.find_funct ge vf = Some f -> type_of_fundef f = typeof a -> evalinf_funcall m f vargs t -> - execinf_stmt e m (Scall lhs a al) t + execinf_stmt e m (Scall (Some lhs) a al) t | execinf_Sseq_1: forall e m s1 s2 t, execinf_stmt e m s1 t -> execinf_stmt e m (Ssequence s1 s2) t @@ -899,51 +1189,538 @@ CoInductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3) | execinf_Sswitch: forall e m a t n sl, eval_expr e m a (Vint n) -> - execinf_lblstmts e m (select_switch n sl) t -> + execinf_stmt e m (seq_of_labeled_statement (select_switch n sl)) t -> execinf_stmt e m (Sswitch a sl) t -with execinf_lblstmts: env -> mem -> labeled_statements -> traceinf -> Prop := - | execinf_LSdefault: forall e m s t, - execinf_stmt e m s t -> - execinf_lblstmts e m (LSdefault s) t - | execinf_LScase_body: forall e m n s ls t, - execinf_stmt e m s t -> - execinf_lblstmts e m (LScase n s ls) t - | execinf_LScase_fallthrough: forall e m n s ls t1 m1 t2, - exec_stmt e m s t1 m1 Out_normal -> - execinf_lblstmts e m1 ls t2 -> - execinf_lblstmts e m (LScase n s ls) (t1 *** t2) - (** [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 lb m2, - alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 lb -> + | evalinf_funcall_internal: forall m f vargs t e m1 m2, + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters e m1 f.(fn_params) vargs m2 -> execinf_stmt e m2 f.(fn_body) t -> evalinf_funcall m (Internal f) vargs t. -End RELSEM. +End SEMANTICS. + +(** * Whole-program semantics *) -(** Execution of a whole program. [exec_program p beh] holds +(** Execution of whole programs are described as sequences of transitions + from an initial state to a final state. An initial state is a [Callstate] + corresponding to the invocation of the ``main'' function of the program + without arguments and with an empty continuation. *) + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b f, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + initial_state p (Callstate f nil Kstop m0). + +(** A final state is a [Returnstate] with an empty continuation. *) + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall r m, + final_state (Returnstate (Vint r) Kstop m) r. + +(** Execution of a whole program: [exec_program p beh] + holds if the application of [p]'s main function to no arguments + in the initial memory state for [p] has [beh] as observable + behavior. *) + +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. + [exec_program_bigstep p beh] holds if the application of [p]'s main function to no arguments in the initial memory state for [p] executes without errors and produces the observable behaviour [beh]. *) -Inductive exec_program (p: program): program_behavior -> Prop := +Inductive exec_program_bigstep (p: program): program_behavior -> Prop := | program_terminates: forall b f m1 t r, let ge := Genv.globalenv p in let m0 := Genv.init_mem p in Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> eval_funcall ge m0 f nil t m1 (Vint r) -> - exec_program p (Terminates t r) + exec_program_bigstep p (Terminates t r) | program_diverges: forall b f t, let ge := Genv.globalenv p in let m0 := Genv.init_mem p in Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> evalinf_funcall ge m0 f nil t -> - exec_program p (Diverges t). - + exec_program_bigstep p (Diverges 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 -> mem -> statement -> trace -> mem -> outcome -> Prop) + (PF: 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) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := + | osm_normal: + outcome_state_match e m f k Out_normal (State f Sskip k e m) + | osm_break: + outcome_state_match e m f k Out_break (State f Sbreak k e m) + | osm_continue: + outcome_state_match e m f k Out_continue (State f Scontinue k e m) + | osm_return_none: forall k', + call_cont k' = call_cont k -> + outcome_state_match e m f k + (Out_return None) (State f (Sreturn None) k' e m) + | osm_return_some: forall a v k', + call_cont k' = call_cont k -> + eval_expr ge e m a v -> + outcome_state_match e m f k + (Out_return (Some v)) (State f (Sreturn (Some a)) k' e 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 m s t m' out, + exec_stmt ge e m s t m' out -> + forall f k, exists S, + star step ge (State f s k e m) t S + /\ outcome_state_match e 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_eval_funcall_ind; intros. + +(* skip *) + econstructor; split. apply star_refl. constructor. + +(* assign *) + econstructor; split. apply star_one. econstructor; eauto. constructor. + +(* call none *) + econstructor; split. + eapply star_left. econstructor; eauto. + eapply star_right. apply H4. 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 m1 + | Out_continue => State f Scontinue k e 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 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 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 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 start *) + destruct (H1 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]. inv B1. + destruct (H3 f k) as [S2 [A2 B2]]. + exists S2; split. + eapply star_left. apply step_for_start; auto. + eapply star_trans. eexact A1. + eapply star_left. constructor. 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 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 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 m1 + | Out_break => State f Sskip k e m1 + | Out_continue => State f Scontinue k e 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 (H2 f k) as [S1 [A1 B1]]. + eapply star_left. eapply step_internal_function; eauto. + eapply star_right. eexact A1. + inv B1; simpl in H3; try contradiction. + (* Out_normal *) + assert (fn_return f = Tvoid /\ vres = Vundef). + destruct (fn_return f); auto || contradiction. + 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 H6. subst vres. + rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. + apply step_return_0; auto. + (* Out_return Some *) + destruct H3. subst vres. + rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. + eapply step_return_1; eauto. + reflexivity. traceEq. + +(* call external *) + apply star_one. apply step_external_function; auto. +Qed. + +Lemma exec_stmt_steps: + forall e m s t m' out, + exec_stmt ge e m s t m' out -> + forall f k, exists S, + star step ge (State f s k e m) t S + /\ outcome_state_match e 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 m s T f k, + execinf_stmt ge e m s T -> + forever_N step order ge tt (State f s k e m) T). + cofix CIH_STMT. + intros. inv H. + +(* call none *) + eapply forever_N_plus. + apply plus_one. eapply step_call_none; eauto. + apply CIH_FUN. eauto. traceEq. +(* call some *) + eapply forever_N_plus. + apply plus_one. eapply step_call_some; eauto. + apply 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 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 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 start 1 *) + assert (a1 <> Sskip). red; intros; subst. inv H0. + eapply forever_N_plus. + eapply plus_one. apply step_for_start; auto. + apply CIH_STMT; eauto. + traceEq. + +(* for start 2 *) + destruct (exec_stmt_steps _ _ _ _ _ _ H1 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]]. + inv B1. + eapply forever_N_plus. + eapply plus_left. eapply step_for_start; eauto. + eapply star_right. eexact A1. + apply step_skip_seq. + 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 exec_program_bigstep_transition: + forall beh, + exec_program_bigstep prog beh -> + exec_program prog beh. +Proof. + intros. inv H. + (* termination *) + econstructor. + econstructor. eauto. eauto. + apply eval_funcall_steps. eauto. red; auto. + econstructor. + (* divergence *) + econstructor. + econstructor. eauto. eauto. + eapply forever_N_forever with (order := order). + red; intros. constructor; intros. red in H. elim H. + apply evalinf_funcall_forever. auto. +Qed. +*) + +End BIGSTEP_TO_TRANSITIONS. + + + + + + -- cgit