From aaa49526068f528f2233de0dace43549432fba52 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 12 Apr 2008 12:55:21 +0000 Subject: Revu gestion retaddr et link dans Stacking git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Stacking.v | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) (limited to 'backend/Stacking.v') diff --git a/backend/Stacking.v b/backend/Stacking.v index 16595e54..a1310aa1 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -45,9 +45,8 @@ Require Import Conventions. To facilitate some of the proofs, the Cminor stack-allocated data starts at offset 0; the preceding areas in the activation record therefore have negative offsets. This part (with negative offsets) -is called the ``frame'' (see the [Machabstr] semantics for the Mach -language), by opposition with the ``Cminor stack data'' which is the part -with positive offsets. +is called the ``frame'', by opposition with the ``Cminor stack data'' +which is the part with positive offsets. The [frame_env] compilation environment records the positions of the boundaries between areas in the frame part. @@ -55,6 +54,8 @@ the boundaries between areas in the frame part. Record frame_env : Set := mk_frame_env { fe_size: Z; + fe_ofs_link: Z; + fe_ofs_retaddr: Z; fe_ofs_int_local: Z; fe_ofs_int_callee_save: Z; fe_num_int_callee_save: Z; @@ -67,19 +68,22 @@ Record frame_env : Set := mk_frame_env { function. *) Definition make_env (b: bounds) := - let oil := 4 * b.(bound_outgoing) in (* integer locals *) + let oil := 4 * b.(bound_outgoing) in (* integer locals *) let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *) let oendi := oics + 4 * b.(bound_int_callee_save) in let ofl := align oendi 8 in (* float locals *) let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *) let sz := ofcs + 8 * b.(bound_float_callee_save) in (* total frame size *) - mk_frame_env sz oil oics b.(bound_int_callee_save) + mk_frame_env sz 0 12 + oil oics b.(bound_int_callee_save) ofl ofcs b.(bound_float_callee_save). (** Computation the frame offset for the given component of the frame. The component is expressed by the following [frame_index] sum type. *) Inductive frame_index: Set := + | FI_link: frame_index + | FI_retaddr: frame_index | FI_local: Z -> typ -> frame_index | FI_arg: Z -> typ -> frame_index | FI_saved_int: Z -> frame_index @@ -87,6 +91,8 @@ Inductive frame_index: Set := Definition offset_of_index (fe: frame_env) (idx: frame_index) := match idx with + | FI_link => fe.(fe_ofs_link) + | FI_retaddr => fe.(fe_ofs_retaddr) | FI_local x Tint => fe.(fe_ofs_int_local) + 4 * x | FI_local x Tfloat => fe.(fe_ofs_float_local) + 8 * x | FI_arg x ty => 4 * x @@ -218,7 +224,8 @@ Definition transl_instr | Lcall sig ros => Mcall sig ros :: k | Ltailcall sig ros => - restore_callee_save fe (Mtailcall sig ros :: k) + restore_callee_save fe + (Mtailcall sig ros :: k) | Lalloc => Malloc :: k | Llabel lbl => @@ -228,7 +235,8 @@ Definition transl_instr | Lcond cond args lbl => Mcond cond args lbl :: k | Lreturn => - restore_callee_save fe (Mreturn :: k) + restore_callee_save fe + (Mreturn :: k) end. (** Translation of a function. Code that saves the values of used @@ -260,7 +268,9 @@ Definition transf_function (f: Linear.function) : res Mach.function := f.(Linear.fn_sig) (transl_body f fe) f.(Linear.fn_stacksize) - fe.(fe_size)). + fe.(fe_size) + (Int.repr fe.(fe_ofs_link)) + (Int.repr fe.(fe_ofs_retaddr))). Definition transf_fundef (f: Linear.fundef) : res Mach.fundef := AST.transf_partial_fundef transf_function f. -- cgit