diff options
Diffstat (limited to 'backend/Machconcr.v')
| -rw-r--r-- | backend/Machconcr.v | 55 |
1 files changed, 28 insertions, 27 deletions
diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 2eb3d478..0cfd8f11 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -41,17 +41,17 @@ Require PPCgenretaddr. caller function at offset 0. In addition to this linking of activation records, the concrete -semantics also make provisions for storing a return address -at offset 12 from the stack pointer. This stack location will -be used by the PPC code generated by [PPCgen] 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. 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] predicate -from module [PPCgenretaddr] is used to guess the value of the return -address that the PPC code generated later will store in the -reserved location. +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 PPC code generated by [PPCgen] 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. 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] predicate from module +[PPCgenretaddr] is used to guess the value of the return address that +the PPC code generated later will store in the reserved location. *) Definition chunk_of_type (ty: typ) := @@ -146,11 +146,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 rs m') | exec_Mgetparam: - forall s f sp parent ofs ty dst c rs m v, - load_stack m sp Tint (Int.repr 0) = Some parent -> + forall s fb f sp parent 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 -> load_stack m parent ty ofs = Some v -> - step (State s f sp (Mgetparam ofs ty dst :: c) rs m) - E0 (State s f sp c (rs#dst <- v) m) + step (State s fb sp (Mgetparam ofs ty dst :: c) rs m) + E0 (State s fb sp c (rs#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 -> @@ -177,10 +178,11 @@ Inductive step: state -> trace -> state -> Prop := E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' rs m) | exec_Mtailcall: - forall s fb stk soff sig ros c rs m f', + forall s fb stk soff sig ros c rs m f f', find_function_ptr ge ros rs = Some f' -> - load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) E0 (Callstate s f' rs (Mem.free m stk)) | exec_Malloc: @@ -210,20 +212,19 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Mcond cond args lbl :: c) rs m) E0 (State s f sp c rs m) | exec_Mreturn: - forall s f stk soff c rs m, - load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) -> - step (State s f (Vptr stk soff) (Mreturn :: c) rs m) + forall s fb stk soff c rs m 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) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + step (State s fb (Vptr stk soff) (Mreturn :: c) rs m) E0 (Returnstate s rs (Mem.free m stk)) | exec_function_internal: forall s fb rs m f m1 m2 m3 stk, Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mem.alloc m (- f.(fn_framesize)) - (align_16_top (- f.(fn_framesize)) f.(fn_stacksize)) - = (m1, stk) -> + Mem.alloc m (- f.(fn_framesize)) f.(fn_stacksize) = (m1, stk) -> let sp := Vptr stk (Int.repr (-f.(fn_framesize))) in - store_stack m1 sp Tint (Int.repr 0) (parent_sp s) = Some m2 -> - store_stack m2 sp Tint (Int.repr 12) (parent_ra s) = Some 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) rs m3) | exec_function_external: |