Library Stacklayout
Machine- and ABI-dependent layout information for activation records.
Require Import Coqlib.
Require Import Bounds.
The general shape of activation records is as follows,
from bottom (lowest offsets) to top:
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
- 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 : Type := 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 let oics := oil + 4 * b.(bound_int_local) in let oendi := oics + 4 * b.(bound_int_callee_save) in
let ofl := align oendi 8 in let ofcs := ofl + 8 * b.(bound_float_local) in let sz := ofcs + 8 * b.(bound_float_callee_save) in mk_frame_env sz 0 12
oil oics b.(bound_int_callee_save)
ofl ofcs b.(bound_float_callee_save).
Remark align_float_part:
forall b,
24 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <=
align (24 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8.