diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-31 18:32:31 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-31 18:32:31 +0000 |
commit | 7cf9ed0e3fd92110cc8531829d03ba40beab76d1 (patch) | |
tree | ec33d42fab2f0db5cd965fc8f2ca1c0e1354a17a /powerpc/eabi/Stacklayout.v | |
parent | 831c5fdf1158c6d55641ea479936f7beabf2221e (diff) | |
download | compcert-7cf9ed0e3fd92110cc8531829d03ba40beab76d1.tar.gz compcert-7cf9ed0e3fd92110cc8531829d03ba40beab76d1.zip |
Continuation of PowerPC/EABI port
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@933 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/eabi/Stacklayout.v')
-rw-r--r-- | powerpc/eabi/Stacklayout.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/powerpc/eabi/Stacklayout.v b/powerpc/eabi/Stacklayout.v index f641847e..48e26a76 100644 --- a/powerpc/eabi/Stacklayout.v +++ b/powerpc/eabi/Stacklayout.v @@ -19,10 +19,13 @@ Require Import Bounds. the general shape of activation records is as follows, from bottom (lowest offsets) to top: - 8 reserved bytes. The first 4 bytes hold the back pointer to the - activation record of the caller. The next 4 bytes hold the - return address. + activation record of the caller. The next 4 bytes are reserved + for called functions to store their return addresses. + Since we would rather store our return address in our own + frame, we will not use these 4 bytes, and just reserve them. - Space for outgoing arguments to function calls. - Local stack slots of integer type. +- Saved return address into caller. - 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. @@ -59,20 +62,21 @@ Record frame_env : Set := mk_frame_env { Definition make_env (b: bounds) := let oil := 8 + 4 * b.(bound_outgoing) in (* integer locals *) - let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *) + let ora := oil + 4 * b.(bound_int_local) in (* saved return address *) + let oics := ora + 4 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 4 + mk_frame_env sz 0 ora oil oics b.(bound_int_callee_save) ofl ofcs b.(bound_float_callee_save). Remark align_float_part: forall b, - 8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <= - align (8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8. + 8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 + 4 * bound_int_callee_save b <= + align (8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 + 4 * bound_int_callee_save b) 8. Proof. intros. apply align_le. omega. Qed. |