From 6acc8ded7cd7e6605fcf27bdbd209d94571f45f4 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 3 Mar 2013 21:35:23 +0000 Subject: Partial backtracking on previous commit: the "hole in Mach stack frame" trick prevents a future mapping of the Mach/Asm call stack as a single block. IA32 is fixed, PowerPC and ARM remains to be done. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2136 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Mach.v | 137 ++++++++++++++++++++++++++++++++++----------------------- 1 file changed, 82 insertions(+), 55 deletions(-) (limited to 'backend/Mach.v') diff --git a/backend/Mach.v b/backend/Mach.v index 12c6c9db..0728c4df 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -115,7 +115,13 @@ semantics also make provisions for storing a back link at offset 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. *) +it at the end of a function. The Mach concrete semantics does not +attach any particular meaning to the pointer stored in this reserved +location, but makes sure that it is preserved during execution of a +function. The [return_address_offset] parameter is used to guess the +value of the return address that the Asm code generated later will +store in the reserved location. +*) Definition chunk_of_type (ty: typ) := match ty with Tint => Mint32 | Tfloat => Mfloat64al32 end. @@ -202,16 +208,20 @@ Qed. Section RELSEM. +Variable return_address_offset: function -> code -> int -> Prop. + Variable ge: genv. -Definition find_function (ros: mreg + ident) (rs: regset) : option fundef := +Definition find_function_ptr + (ge: genv) (ros: mreg + ident) (rs: regset) : option block := match ros with - | inl r => Genv.find_funct ge (rs r) - | inr symb => - match Genv.find_symbol ge symb with - | None => None - | Some b => Genv.find_funct_ptr ge b + | inl r => + match rs r with + | Vptr b ofs => if Int.eq ofs Int.zero then Some b else None + | _ => None end + | inr symb => + Genv.find_symbol ge symb end. (** Extract the values of the arguments to an external call. *) @@ -242,17 +252,20 @@ Definition annot_arguments (** Mach execution states. *) +(** Mach execution states. *) + Inductive stackframe: Type := | Stackframe: - forall (f: function) (**r calling function *) + forall (f: block) (**r pointer to calling function *) (sp: val) (**r stack pointer in calling function *) + (retaddr: val) (**r Asm return address 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 *) + (f: block) (**r pointer to current function *) (sp: val) (**r stack pointer *) (c: code) (**r current program point *) (rs: regset) (**r register state *) @@ -260,7 +273,7 @@ Inductive state: Type := state | Callstate: forall (stack: list stackframe) (**r call stack *) - (fd: fundef) (**r function to call *) + (f: block) (**r pointer to function to call *) (rs: regset) (**r register state *) (m: mem), (**r memory state *) state @@ -273,7 +286,13 @@ Inductive state: Type := Definition parent_sp (s: list stackframe) : val := match s with | nil => Vptr Mem.nullptr Int.zero - | Stackframe f sp c :: s' => sp + | Stackframe f sp ra c :: s' => sp + end. + +Definition parent_ra (s: list stackframe) : val := + match s with + | nil => Vzero + | Stackframe f sp ra c :: s' => ra end. Inductive step: state -> trace -> state -> Prop := @@ -292,11 +311,12 @@ Inductive step: state -> trace -> state -> Prop := 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, + forall s fb f sp ofs ty dst c rs m v, + Genv.find_funct_ptr ge fb = Some (Internal f) -> 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) + step (State s fb sp (Mgetparam ofs ty dst :: c) rs m) + E0 (State s fb 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 -> @@ -315,19 +335,22 @@ Inductive step: state -> trace -> state -> Prop := 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) + forall s fb sp sig ros c rs m f f' ra, + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + return_address_offset f c ra -> + step (State s fb sp (Mcall sig ros :: c) rs m) + E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) + f' rs m) | exec_Mtailcall: - forall s f stk soff sig ros c rs m fd m' m'', - find_function ros rs = Some fd -> + forall s fb stk soff sig ros c rs m f f' m', + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> 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'') + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) + E0 (Callstate s f' 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' -> @@ -340,70 +363,74 @@ Inductive step: state -> trace -> state -> Prop := 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', + forall s fb f sp lbl c rs m c', + Genv.find_funct_ptr ge fb = Some (Internal f) -> 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) + step (State s fb sp (Mgoto lbl :: c) rs m) + E0 (State s fb sp c' rs m) | exec_Mcond_true: - forall s f sp cond args lbl c rs m c', + forall s fb f sp cond args lbl c rs m c', eval_condition cond rs##args m = Some true -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> 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) + step (State s fb sp (Mcond cond args lbl :: c) rs m) + E0 (State s fb 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', + forall s fb f sp arg tbl c rs m n lbl c', rs arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some lbl -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> 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) + step (State s fb sp (Mjumptable arg tbl :: c) rs m) + E0 (State s fb sp c' (undef_temps rs) m) | exec_Mreturn: - forall s f stk soff c rs m m' m'', + forall s fb stk soff c rs m f m', + Genv.find_funct_ptr ge fb = Some (Internal f) -> 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'') + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s fb (Vptr stk soff) (Mreturn :: c) rs m) + E0 (Returnstate s rs m') | exec_function_internal: - forall s f rs m m1 m2 m3 stk, + forall s fb rs m f m1 m2 m3 stk, + Genv.find_funct_ptr ge fb = Some (Internal f) -> 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) + store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 -> + store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> + step (Callstate s fb rs m) + E0 (State s fb sp f.(fn_code) (undef_temps rs) m3) | exec_function_external: - forall s ef rs m t rs' args res m', + forall s fb rs m t rs' ef args res m', + Genv.find_funct_ptr ge fb = Some (External ef) -> 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) + step (Callstate s fb 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) + forall s f sp ra c rs m, + step (Returnstate (Stackframe f sp ra 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, + | initial_state_intro: forall fb 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). + Genv.find_symbol ge p.(prog_main) = Some fb -> + initial_state p (Callstate nil fb (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). +Definition semantics (rao: function -> code -> int -> Prop) (p: program) := + Semantics (step rao) (initial_state p) final_state (Genv.globalenv p). -- cgit