From 5020a5a07da3fd690f5d171a48d0c73ef48f9430 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 1 Mar 2013 15:32:13 +0000 Subject: Revised Stacking and Asmgen passes and Mach semantics: - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Mach.v | 247 ++++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 236 insertions(+), 11 deletions(-) (limited to 'backend/Mach.v') diff --git a/backend/Mach.v b/backend/Mach.v index 56c03699..12c6c9db 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -21,10 +21,14 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. +Require Import Memory. Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. Require Import Op. Require Import Locations. Require Import Conventions. +Require Stacklayout. (** * Abstract syntax *) @@ -89,13 +93,39 @@ Definition funsig (fd: fundef) := Definition genv := Genv.t fundef unit. -(** * Elements of dynamic semantics *) - -(** The operational semantics is in module [Machsem]. *) +(** * Operational semantics *) + +(** The semantics for Mach is close to that of [Linear]: they differ only + on the interpretation of stack slot accesses. In Mach, these + accesses are interpreted as memory accesses relative to the + stack pointer. More precisely: +- [Mgetstack ofs ty r] is a memory load at offset [ofs * 4] relative + to the stack pointer. +- [Msetstack r ofs ty] is a memory store at offset [ofs * 4] relative + to the stack pointer. +- [Mgetparam ofs ty r] is a memory load at offset [ofs * 4] + relative to the pointer found at offset 0 from the stack pointer. + The semantics maintain a linked structure of activation records, + with the current record containing a pointer to the record of the + caller function at offset 0. + +In addition to this linking of activation records, the +semantics also make provisions for storing a back link at offset +[f.(fn_link_ofs)] from the stack pointer, and a return address at +offset [f.(fn_retaddr_ofs)]. The latter stack location will be used +by the Asm code generated by [Asmgen] to save the return address into +the caller at the beginning of a function, then restore it and jump to +it at the end of a function. *) Definition chunk_of_type (ty: typ) := match ty with Tint => Mint32 | Tfloat => Mfloat64al32 end. +Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) := + Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)). + +Definition store_stack (m: mem) (sp: val) (ty: typ) (ofs: int) (v: val) := + Mem.storev (chunk_of_type ty) m (Val.add sp (Vint ofs)) v. + Module RegEq. Definition t := mreg. Definition eq := mreg_eq. @@ -170,15 +200,210 @@ Proof. destruct (is_label lbl a). inv H. auto with coqlib. eauto with coqlib. Qed. -Definition find_function_ptr - (ge: genv) (ros: mreg + ident) (rs: regset) : option block := +Section RELSEM. + +Variable ge: genv. + +Definition find_function (ros: mreg + ident) (rs: regset) : option fundef := match ros with - | inl r => - match rs r with - | Vptr b ofs => if Int.eq ofs Int.zero then Some b else None - | _ => None - end + | inl r => Genv.find_funct ge (rs r) | inr symb => - Genv.find_symbol ge symb + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end + end. + +(** Extract the values of the arguments to an external call. *) + +Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := + | extcall_arg_reg: forall rs m sp r, + extcall_arg rs m sp (R r) (rs r) + | extcall_arg_stack: forall rs m sp ofs ty v, + load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v -> + extcall_arg rs m sp (S (Outgoing ofs ty)) v. + +Definition extcall_arguments + (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := + list_forall2 (extcall_arg rs m sp) (loc_arguments sg) args. + +(** Extract the values of the arguments to an annotation. *) + +Inductive annot_arg: regset -> mem -> val -> annot_param -> val -> Prop := + | annot_arg_reg: forall rs m sp r, + annot_arg rs m sp (APreg r) (rs r) + | annot_arg_stack: forall rs m stk base chunk ofs v, + Mem.load chunk m stk (Int.unsigned base + ofs) = Some v -> + annot_arg rs m (Vptr stk base) (APstack chunk ofs) v. + +Definition annot_arguments + (rs: regset) (m: mem) (sp: val) (params: list annot_param) (args: list val) : Prop := + list_forall2 (annot_arg rs m sp) params args. + +(** Mach execution states. *) + +Inductive stackframe: Type := + | Stackframe: + forall (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (c: code), (**r program point in calling function *) + stackframe. + +Inductive state: Type := + | State: + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (sp: val) (**r stack pointer *) + (c: code) (**r current program point *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Callstate: + forall (stack: list stackframe) (**r call stack *) + (fd: fundef) (**r function to call *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Returnstate: + forall (stack: list stackframe) (**r call stack *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state. + +Definition parent_sp (s: list stackframe) : val := + match s with + | nil => Vptr Mem.nullptr Int.zero + | Stackframe f sp c :: s' => sp end. +Inductive step: state -> trace -> state -> Prop := + | exec_Mlabel: + forall s f sp lbl c rs m, + step (State s f sp (Mlabel lbl :: c) rs m) + E0 (State s f sp c rs m) + | exec_Mgetstack: + forall s f sp ofs ty dst c rs m v, + load_stack m sp ty ofs = Some v -> + step (State s f sp (Mgetstack ofs ty dst :: c) rs m) + E0 (State s f sp c (rs#dst <- v) m) + | exec_Msetstack: + forall s f sp src ofs ty c rs m m', + store_stack m sp ty ofs (rs src) = Some m' -> + step (State s f sp (Msetstack src ofs ty :: c) rs m) + E0 (State s f sp c (undef_setstack rs) m') + | exec_Mgetparam: + forall s f sp ofs ty dst c rs m v, + load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (parent_sp s) ty ofs = Some v -> + step (State s f sp (Mgetparam ofs ty dst :: c) rs m) + E0 (State s f sp c (rs # IT1 <- Vundef # dst <- v) m) + | exec_Mop: + forall s f sp op args res c rs m v, + eval_operation ge sp op rs##args m = Some v -> + step (State s f sp (Mop op args res :: c) rs m) + E0 (State s f sp c ((undef_op op rs)#res <- v) m) + | exec_Mload: + forall s f sp chunk addr args dst c rs m a v, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + step (State s f sp (Mload chunk addr args dst :: c) rs m) + E0 (State s f sp c ((undef_temps rs)#dst <- v) m) + | exec_Mstore: + forall s f sp chunk addr args src c rs m m' a, + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a (rs src) = Some m' -> + step (State s f sp (Mstore chunk addr args src :: c) rs m) + E0 (State s f sp c (undef_temps rs) m') + | exec_Mcall: + forall s f sp sig ros c rs m fd, + find_function ros rs = Some fd -> + step (State s f sp (Mcall sig ros :: c) rs m) + E0 (Callstate (Stackframe f sp c :: s) + fd rs m) + | exec_Mtailcall: + forall s f stk soff sig ros c rs m fd m' m'', + find_function ros rs = Some fd -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' -> + Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' -> + step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs m) + E0 (Callstate s fd rs m'') + | exec_Mbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge rs##args m t v m' -> + step (State s f sp (Mbuiltin ef args res :: b) rs m) + t (State s f sp b ((undef_temps rs)#res <- v) m') + | exec_Mannot: + forall s f sp rs m ef args b vargs t v m', + annot_arguments rs m sp args vargs -> + external_call ef ge vargs m t v m' -> + step (State s f sp (Mannot ef args :: b) rs m) + t (State s f sp b rs m') + | exec_Mgoto: + forall s f sp lbl c rs m c', + find_label lbl f.(fn_code) = Some c' -> + step (State s f sp (Mgoto lbl :: c) rs m) + E0 (State s f sp c' rs m) + | exec_Mcond_true: + forall s f sp cond args lbl c rs m c', + eval_condition cond rs##args m = Some true -> + find_label lbl f.(fn_code) = Some c' -> + step (State s f sp (Mcond cond args lbl :: c) rs m) + E0 (State s f sp c' (undef_temps rs) m) + | exec_Mcond_false: + forall s f sp cond args lbl c rs m, + eval_condition cond rs##args m = Some false -> + step (State s f sp (Mcond cond args lbl :: c) rs m) + E0 (State s f sp c (undef_temps rs) m) + | exec_Mjumptable: + forall s f sp arg tbl c rs m n lbl c', + rs arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some lbl -> + find_label lbl f.(fn_code) = Some c' -> + step (State s f sp (Mjumptable arg tbl :: c) rs m) + E0 (State s f sp c' (undef_temps rs) m) + | exec_Mreturn: + forall s f stk soff c rs m m' m'', + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' -> + Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' -> + step (State s f (Vptr stk soff) (Mreturn :: c) rs m) + E0 (Returnstate s rs m'') + | exec_function_internal: + forall s f rs m m1 m2 m3 stk, + Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> + Mem.free m1 stk (Int.unsigned f.(fn_retaddr_ofs)) (Int.unsigned f.(fn_retaddr_ofs) + 4) = Some m2 -> + let sp := Vptr stk Int.zero in + store_stack m2 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m3 -> + (4 | Int.unsigned f.(fn_retaddr_ofs)) -> + step (Callstate s (Internal f) rs m) + E0 (State s f sp f.(fn_code) (undef_temps rs) m3) + | exec_function_external: + forall s ef rs m t rs' args res m', + external_call ef ge args m t res m' -> + extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> + rs' = (rs#(loc_result (ef_sig ef)) <- res) -> + step (Callstate s (External ef) rs m) + t (Returnstate s rs' m') + | exec_return: + forall s f sp c rs m, + step (Returnstate (Stackframe f sp c :: s) rs m) + E0 (State s f sp c rs m). + +End RELSEM. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b fd m0, + 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 fd -> + initial_state p (Callstate nil fd (Regmap.init Vundef) m0). + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall rs m r, + rs (loc_result (mksignature nil (Some Tint))) = Vint r -> + final_state (Returnstate nil rs m) r. + +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). -- cgit