1 files changed, 3 insertions, 52 deletions
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 3f08daa..1cf010b 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -24,61 +24,12 @@ Require Import Linear.
 Require Import Bounds.
 Require Import Mach.
 Require Import Conventions.
+Require Import Stacklayout.
 
 (** * Layout of activation records *)
 
-(** The general shape of activation records is as follows,
-  from bottom (lowest offsets) to top:
-- 24 reserved bytes.  The first 4 bytes hold the back pointer to the
-  activation record of the caller.  We use the 4 bytes at offset 12
-  to store the return address.  (These are reserved by the PowerPC
-  application binary interface.)  The remaining bytes are unused.
-- Space for outgoing arguments to function calls.
-- Local stack slots of integer type.
-- Saved values of integer callee-save registers used by the function.
-- One word of padding, if necessary to align the following data
-  on a 8-byte boundary.
-- Local stack slots of float type.
-- Saved values of float callee-save registers used by the function.
-- Space for the stack-allocated data declared in Cminor.
-
-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'', 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.
-*)
-
-Definition fe_ofs_arg := 24.
-
-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;
-  fe_ofs_float_local: Z;
-  fe_ofs_float_callee_save: Z;
-  fe_num_float_callee_save: Z
-}.
-
-(** Computation of the frame environment from the bounds of the current
-  function. *)
-
-Definition make_env (b: bounds) :=
-  let oil := 24 + 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 0 12
-                  oil oics b.(bound_int_callee_save)
-                  ofl ofcs b.(bound_float_callee_save).
+(** The machine- and ABI-dependent aspects of the layout are defined
+  in module [Stacklayout]. *)
 
 (** Computation the frame offset for the given component of the frame.
   The component is expressed by the following [frame_index] sum type. *)