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/Csharpminor.v | 529 +++++++++++++++++++++++------------------------- 1 file changed, 249 insertions(+), 280 deletions(-) (limited to 'cfrontend/Csharpminor.v') diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 942cfd7..5cdbd84 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -59,6 +59,8 @@ Inductive expr : Type := [Sexit n] terminates prematurely the execution of the [n+1] enclosing [Sblock] statements. *) +Definition label := ident. + Inductive stmt : Type := | Sskip: stmt | Sassign : ident -> expr -> stmt @@ -69,8 +71,14 @@ Inductive stmt : Type := | Sloop: stmt -> stmt | Sblock: stmt -> stmt | Sexit: nat -> stmt - | Sswitch: expr -> list (int * nat) -> nat -> stmt - | Sreturn: option expr -> stmt. + | Sswitch: expr -> lbl_stmt -> stmt + | Sreturn: option expr -> stmt + | Slabel: label -> stmt -> stmt + | Sgoto: label -> stmt + +with lbl_stmt : Type := + | LSdefault: stmt -> lbl_stmt + | LScase: int -> stmt -> lbl_stmt -> lbl_stmt. (** The variables can be either scalar variables (whose type, size and signedness are given by a [memory_chunk] @@ -105,39 +113,6 @@ Definition funsig (fd: fundef) := (** * Operational semantics *) -(** The operational semantics for Csharpminor is given in big-step operational - style. Expressions evaluate to values, and statements evaluate to - ``outcomes'' indicating how execution should proceed afterwards. *) - -Inductive outcome: Type := - | Out_normal: outcome (**r continue in sequence *) - | Out_exit: nat -> outcome (**r terminate [n+1] enclosing blocks *) - | Out_return: option val -> outcome. (**r return immediately to caller *) - -Definition outcome_result_value - (out: outcome) (ot: option typ) (v: val) : Prop := - match out, ot with - | Out_normal, None => v = Vundef - | Out_return None, None => v = Vundef - | Out_return (Some v'), Some ty => v = v' - | _, _ => False - end. - -Definition outcome_block (out: outcome) : outcome := - match out with - | Out_normal => Out_normal - | Out_exit O => Out_normal - | Out_exit (S n) => Out_exit n - | Out_return optv => Out_return optv - end. - -Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat)) - {struct cases} : nat := - match cases with - | nil => dfl - | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem - end. - (** Three kinds of evaluation environments are involved: - [genv]: global environments, define symbols and functions; - [gvarenv]: map global variables to variable informations (type [var_kind]); @@ -167,10 +142,105 @@ Definition fn_params_names (f: function) := Definition fn_vars_names (f: function) := List.map (@fst ident var_kind) f.(fn_vars). -Definition global_var_env (p: program): gvarenv := - List.fold_left - (fun gve x => match x with (id, init, k) => PTree.set id k gve end) - p.(prog_vars) (PTree.empty var_kind). +(** Continuations *) + +Inductive cont: Type := + | Kstop: cont (**r stop program execution *) + | Kseq: stmt -> cont -> cont (**r execute stmt, then cont *) + | Kblock: cont -> cont (**r exit a block, then do cont *) + | Kcall: option ident -> function -> env -> cont -> cont. + (**r return to caller *) + +(** States *) + +Inductive state: Type := + | State: (**r Execution within a function *) + forall (f: function) (**r currently executing function *) + (s: stmt) (**r statement under consideration *) + (k: cont) (**r its continuation -- what to do next *) + (e: env) (**r current local environment *) + (m: mem), (**r current memory state *) + state + | Callstate: (**r Invocation of a function *) + forall (f: fundef) (**r function to invoke *) + (args: list val) (**r arguments provided by caller *) + (k: cont) (**r what to do next *) + (m: mem), (**r memory state *) + state + | Returnstate: (**r Return from a function *) + forall (v: val) (**r Return value *) + (k: cont) (**r what to do next *) + (m: mem), (**r memory state *) + state. + +(** Pop continuation until a call or stop *) + +Fixpoint call_cont (k: cont) : cont := + match k with + | Kseq s k => call_cont k + | Kblock k => call_cont k + | _ => k + end. + +Definition is_call_cont (k: cont) : Prop := + match k with + | Kstop => True + | Kcall _ _ _ _ => True + | _ => False + end. + +(** Resolve [switch] statements. *) + +Fixpoint select_switch (n: int) (sl: lbl_stmt) {struct sl} : lbl_stmt := + match sl with + | LSdefault _ => sl + | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' + end. + +Fixpoint seq_of_lbl_stmt (sl: lbl_stmt) : stmt := + match sl with + | LSdefault s => s + | LScase c s sl' => Sseq s (seq_of_lbl_stmt sl') + end. + +(** Find the statement and manufacture the continuation + corresponding to a label *) + +Fixpoint find_label (lbl: label) (s: stmt) (k: cont) + {struct s}: option (stmt * cont) := + match s with + | Sseq 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 + | Sloop s1 => + find_label lbl s1 (Kseq (Sloop s1) k) + | Sblock s1 => + find_label lbl s1 (Kblock k) + | Sswitch a sl => + find_label_ls lbl sl 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: lbl_stmt) (k: cont) + {struct sl}: option (stmt * cont) := + match sl with + | LSdefault s => find_label lbl s k + | LScase _ s sl' => + match find_label lbl s (Kseq (seq_of_lbl_stmt sl') k) with + | Some sk => Some sk + | None => find_label_ls lbl sl' k + end + end. + (** Evaluation of operator applications. *) @@ -199,15 +269,21 @@ Definition eval_binop (op: binary_operation) Inductive alloc_variables: env -> mem -> list (ident * var_kind) -> - 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 lv vars m1 b1 m2 e2 lb, + forall e m id lv vars m1 b1 m2 e2, Mem.alloc m 0 (sizeof lv) = (m1, b1) -> - alloc_variables (PTree.set id (b1, lv) e) m1 vars e2 m2 lb -> - alloc_variables e m ((id, lv) :: vars) e2 m2 (b1 :: lb). + alloc_variables (PTree.set id (b1, lv) e) m1 vars e2 m2 -> + alloc_variables e m ((id, lv) :: vars) e2 m2. + +(** List of blocks mentioned in an environment *) + +Definition blocks_of_env (e: env) : list block := + List.map (fun id_b_lv => match id_b_lv with (id, (b, lv)) => b end) + (PTree.elements e). (** Initialization of local variables that are parameters. The value of the corresponding argument is stored into the memory block @@ -228,8 +304,9 @@ Inductive bind_parameters: env -> Section RELSEM. -Variable prg: program. -Let ge := Genv.globalenv prg. +Variable globenv : genv * gvarenv. +Let ge := fst globenv. +Let gvare := snd globenv. (* Evaluation of the address of a variable: [eval_var_addr prg ge e id b] states that variable [id] @@ -260,7 +337,7 @@ Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop := forall e id b chunk, PTree.get id e = None -> Genv.find_symbol ge id = Some b -> - PTree.get id (global_var_env prg) = Some (Vscalar chunk) -> + PTree.get id gvare = Some (Vscalar chunk) -> eval_var_ref e id b chunk. (** Evaluation of an expression: [eval_expr prg e m a v] states @@ -331,256 +408,148 @@ Inductive exec_opt_assign: env -> mem -> option ident -> val -> mem -> Prop := exec_assign e m id v m' -> exec_opt_assign e m (Some id) v m'. -(** Evaluation of a function invocation: [eval_funcall prg m f args t m' res] - means that the function [f], applied to the arguments [args] in - memory state [m], returns the value [res] in modified memory state [m']. - [t] is the trace of observable events performed during the call. *) +(** One step of execution *) -Inductive eval_funcall: - mem -> fundef -> list val -> trace -> - mem -> val -> Prop := - | eval_funcall_internal: - forall m f vargs e m1 lb m2 t m3 out vres, - list_norepet (fn_params_names f ++ fn_vars_names f) -> - alloc_variables empty_env m (fn_variables f) e m1 lb -> - 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_sig).(sig_res) vres -> - eval_funcall m (Internal f) vargs t (Mem.free_list m3 lb) vres - | eval_funcall_external: - forall m ef vargs t vres, - event_match ef vargs t vres -> - eval_funcall m (External ef) vargs t m vres - -(** Execution of a statement: [exec_stmt prg e m s t m' out] - means that statement [s] executes with outcome [out]. - [m] is the initial memory state, [m'] the final memory state, - and [t] the trace of events performed. - The other parameters are as in [eval_expr]. *) - -with exec_stmt: - env -> - mem -> stmt -> trace -> - mem -> outcome -> Prop := - | exec_Sskip: - forall e m, - exec_stmt e m Sskip E0 m Out_normal - | exec_Sassign: - forall e m id a v m', +Inductive step: state -> trace -> state -> Prop := + + | 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_skip_block: forall f k e m, + step (State f Sskip (Kblock k) e m) + E0 (State f Sskip k e m) + | step_skip_call: forall f k e m, + is_call_cont k -> + f.(fn_sig).(sig_res) = None -> + step (State f Sskip k e m) + E0 (Returnstate Vundef k (Mem.free_list m (blocks_of_env e))) + + | step_assign: forall f id a k e m m' v, eval_expr e m a v -> exec_assign e m id v m' -> - exec_stmt e m (Sassign id a) E0 m' Out_normal - | exec_Sstore: - forall e m chunk a b v1 v2 m', - eval_expr e m a v1 -> - eval_expr e m b v2 -> - Mem.storev chunk m v1 v2 = Some m' -> - exec_stmt e m (Sstore chunk a b) E0 m' Out_normal - | exec_Scall: - forall e m optid sig a bl vf vargs f t m1 vres m2, + step (State f (Sassign id a) k e m) + E0 (State f Sskip k e m') + + | step_store: forall f chunk addr a k e m vaddr v m', + eval_expr e m addr vaddr -> + eval_expr e m a v -> + Mem.storev chunk m vaddr v = Some m' -> + step (State f (Sstore chunk addr a) k e m) + E0 (State f Sskip k e m') + + | step_call: forall f optid sig a bl k e m vf vargs fd, eval_expr e m a vf -> eval_exprlist e m bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - eval_funcall m f vargs t m1 vres -> - exec_opt_assign e m1 optid vres m2 -> - exec_stmt e m (Scall optid sig a bl) t m2 Out_normal - | exec_Sseq_continue: - forall e m s1 s2 t1 t2 m1 m2 t out, - exec_stmt e m s1 t1 m1 Out_normal -> - exec_stmt e m1 s2 t2 m2 out -> - t = t1 ** t2 -> - exec_stmt e m (Sseq s1 s2) t m2 out - | exec_Sseq_stop: - forall e m s1 s2 t1 m1 out, - exec_stmt e m s1 t1 m1 out -> - out <> Out_normal -> - exec_stmt e m (Sseq s1 s2) t1 m1 out - | exec_Sifthenelse: - forall e m a sl1 sl2 v vb t m' out, + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + step (State f (Scall optid sig a bl) k e m) + E0 (Callstate fd vargs (Kcall optid f e k) m) + + | step_seq: forall f s1 s2 k e m, + step (State f (Sseq s1 s2) k e m) + E0 (State f s1 (Kseq s2 k) e m) + + | step_ifthenelse: forall f a s1 s2 k e m v b, eval_expr e m a v -> - Val.bool_of_val v vb -> - exec_stmt e m (if vb then sl1 else sl2) t m' out -> - exec_stmt e m (Sifthenelse a sl1 sl2) t m' out - | exec_Sloop_loop: - forall e m sl t1 m1 t2 m2 out t, - exec_stmt e m sl t1 m1 Out_normal -> - exec_stmt e m1 (Sloop sl) t2 m2 out -> - t = t1 ** t2 -> - exec_stmt e m (Sloop sl) t m2 out - | exec_Sloop_stop: - forall e m sl t1 m1 out, - exec_stmt e m sl t1 m1 out -> - out <> Out_normal -> - exec_stmt e m (Sloop sl) t1 m1 out - | exec_Sblock: - forall e m sl t1 m1 out, - exec_stmt e m sl t1 m1 out -> - exec_stmt e m (Sblock sl) t1 m1 (outcome_block out) - | exec_Sexit: - forall e m n, - exec_stmt e m (Sexit n) E0 m (Out_exit n) - | exec_Sswitch: - forall e m a cases default n, + Val.bool_of_val v b -> + step (State f (Sifthenelse a s1 s2) k e m) + E0 (State f (if b then s1 else s2) k e m) + + | step_loop: forall f s k e m, + step (State f (Sloop s) k e m) + E0 (State f s (Kseq (Sloop s) k) e m) + + | step_block: forall f s k e m, + step (State f (Sblock s) k e m) + E0 (State f s (Kblock k) e m) + + | step_exit_seq: forall f n s k e m, + step (State f (Sexit n) (Kseq s k) e m) + E0 (State f (Sexit n) k e m) + | step_exit_block_0: forall f k e m, + step (State f (Sexit O) (Kblock k) e m) + E0 (State f Sskip k e m) + | step_exit_block_S: forall f n k e m, + step (State f (Sexit (S n)) (Kblock k) e m) + E0 (State f (Sexit n) k e m) + + | step_switch: forall f a cases k e m n, eval_expr e m a (Vint n) -> - exec_stmt e m (Sswitch a cases default) - E0 m (Out_exit (switch_target n default cases)) - | exec_Sreturn_none: - forall e m, - exec_stmt e m (Sreturn None) E0 m (Out_return None) - | exec_Sreturn_some: - forall e m a v, + step (State f (Sswitch a cases) k e m) + E0 (State f (seq_of_lbl_stmt (select_switch n cases)) k e m) + + | step_return_0: forall f k e m, + f.(fn_sig).(sig_res) = None -> + 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_sig).(sig_res) <> None -> eval_expr e m a v -> - exec_stmt e m (Sreturn (Some a)) E0 m (Out_return (Some v)). - -Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop - with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop. - -(** Coinductive semantics for divergence. *) - -Inductive block_seq_context: (stmt -> stmt) -> Prop := - | block_seq_context_base_1: - block_seq_context (fun x => Sblock x) - | block_seq_context_base_2: forall s, - block_seq_context (fun x => Sseq x s) - | block_seq_context_ctx_1: forall ctx, - block_seq_context ctx -> - block_seq_context (fun x => Sblock (ctx x)) - | block_seq_context_ctx_2: forall s ctx, - block_seq_context ctx -> - block_seq_context (fun x => Sseq (ctx x) s). - -CoInductive evalinf_funcall: - mem -> fundef -> list val -> traceinf -> Prop := - | evalinf_funcall_internal: - forall m f vargs e m1 lb m2 t, + step (State f (Sreturn (Some a)) k e m) + E0 (Returnstate v (call_cont k) + (Mem.free_list m (blocks_of_env e))) + + | 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 m1 m2 e, list_norepet (fn_params_names f ++ fn_vars_names f) -> - alloc_variables empty_env m (fn_variables f) e m1 lb -> + alloc_variables empty_env m (fn_variables f) 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 + step (Callstate (Internal f) vargs k m) + E0 (State f f.(fn_body) k e m2) -with execinf_stmt: - env -> mem -> stmt -> traceinf -> Prop := - | execinf_Scall: - forall e m optid sig a bl vf vargs f t, - eval_expr e m a vf -> - eval_exprlist e m bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - evalinf_funcall m f vargs t -> - execinf_stmt e m (Scall optid sig a bl) t - | execinf_Sseq_1: - forall e m s1 s2 t, - execinf_stmt e m s1 t -> - execinf_stmt e m (Sseq s1 s2) t - | execinf_Sseq_2: - forall e m s1 s2 t1 t2 m1 t, - exec_stmt e m s1 t1 m1 Out_normal -> - execinf_stmt e m1 s2 t2 -> - t = t1 *** t2 -> - execinf_stmt e m (Sseq s1 s2) t - | execinf_Sifthenelse: - forall e m a sl1 sl2 v vb t, - eval_expr e m a v -> - Val.bool_of_val v vb -> - execinf_stmt e m (if vb then sl1 else sl2) t -> - execinf_stmt e m (Sifthenelse a sl1 sl2) t - | execinf_Sloop_body: - forall e m sl t, - execinf_stmt e m sl t -> - execinf_stmt e m (Sloop sl) t - | execinf_Sloop_loop: - forall e m sl t1 m1 t2 t, - exec_stmt e m sl t1 m1 Out_normal -> - execinf_stmt e m1 (Sloop sl) t2 -> - t = t1 *** t2 -> - execinf_stmt e m (Sloop sl) t - | execinf_Sblock: - forall e m sl t, - execinf_stmt e m sl t -> - execinf_stmt e m (Sblock sl) t - | execinf_stutter: - forall n e m s t, - execinf_stmt_N n e m s t -> - execinf_stmt e m s t - | execinf_Sloop_block: - forall e m sl t1 m1 t2 t, - exec_stmt e m sl t1 m1 Out_normal -> - execinf_stmt e m1 (Sblock (Sloop sl)) t2 -> - t = t1 *** t2 -> - execinf_stmt e m (Sloop sl) t - -with execinf_stmt_N: - nat -> env -> mem -> stmt -> traceinf -> Prop := - | execinf_context: forall n e m s t ctx, - execinf_stmt e m s t -> block_seq_context ctx -> - execinf_stmt_N n e m (ctx s) t - | execinf_sleep: forall n e m s t, - execinf_stmt_N n e m s t -> - execinf_stmt_N (S n) e m s t. - -Lemma execinf_stmt_N_inv: - forall n e m s t, - execinf_stmt_N n e m s t -> - match s with - | Sblock s1 => execinf_stmt e m s1 t - | Sseq s1 s2 => execinf_stmt e m s1 t - | _ => False - end. -Proof. - assert (BASECASE: forall e m s t ctx, - execinf_stmt e m s t -> block_seq_context ctx -> - match ctx s with - | Sblock s1 => execinf_stmt e m s1 t - | Sseq s1 s2 => execinf_stmt e m s1 t - | _ => False - end). - intros. inv H0. - auto. - auto. - apply execinf_stutter with O. apply execinf_context; eauto. - apply execinf_stutter with O. apply execinf_context; eauto. - - induction n; intros; inv H. - apply BASECASE; auto. - apply BASECASE; auto. - eapply IHn; eauto. -Qed. - -Lemma execinf_Sblock_inv: - forall e m s t, - execinf_stmt e m (Sblock s) t -> - execinf_stmt e m s t. -Proof. - intros. inv H. - auto. - exact (execinf_stmt_N_inv _ _ _ _ _ H0). -Qed. + | step_external_function: forall ef vargs k m t vres, + event_match ef vargs t vres -> + step (Callstate (External ef) vargs k m) + t (Returnstate vres k m) + + | step_return: forall v optid f e k m m', + exec_opt_assign e m optid v m' -> + step (Returnstate v (Kcall optid f e k) m) + E0 (State f Sskip k e m'). End RELSEM. -(** 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. *) +(** 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 exec_program (p: program): program_behavior -> Prop := - | program_terminates: - forall b f t m r, +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 -> funsig f = mksignature nil (Some Tint) -> - eval_funcall p m0 f nil t m (Vint r) -> - exec_program 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 -> - funsig f = mksignature nil (Some Tint) -> - evalinf_funcall p m0 f nil t -> - exec_program p (Diverges t). + 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 global_var_env (p: program): gvarenv := + List.fold_left + (fun gve x => match x with (id, init, k) => PTree.set id k gve end) + p.(prog_vars) (PTree.empty var_kind). + +Definition exec_program (p: program) (beh: program_behavior) : Prop := + program_behaves step (initial_state p) final_state + (Genv.globalenv p, global_var_env p) beh. + + -- cgit v1.2.3