diff options
Diffstat (limited to 'ia32/Stacklayout.v')
-rw-r--r-- | ia32/Stacklayout.v | 70 |
1 files changed, 38 insertions, 32 deletions
diff --git a/ia32/Stacklayout.v b/ia32/Stacklayout.v index f19f036c..44fd43b2 100644 --- a/ia32/Stacklayout.v +++ b/ia32/Stacklayout.v @@ -2,7 +2,7 @@ (* *) (* The Compcert verified compiler *) (* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Xavier Leroy, INRIA Paris *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -13,9 +13,11 @@ (** Machine- and ABI-dependent layout information for activation records. *) Require Import Coqlib. -Require Import Memory Separation. +Require Import AST Memory Separation. Require Import Bounds. +Local Open Scope sep_scope. + (** The general shape of activation records is as follows, from bottom (lowest offsets) to top: - Space for outgoing arguments to function calls. @@ -29,16 +31,14 @@ Require Import Bounds. Definition fe_ofs_arg := 0. -(** Computation of the frame environment from the bounds of the current - function. *) - Definition make_env (b: bounds) : frame_env := - let olink := 4 * b.(bound_outgoing) in (* back link *) - let ocs := olink + 4 in (* callee-saves *) + let w := if Archi.ptr64 then 8 else 4 in + let olink := align (4 * b.(bound_outgoing)) w in (* back link *) + let ocs := olink + w in (* callee-saves *) let ol := align (size_callee_save_area b ocs) 8 in (* locals *) let ostkdata := align (ol + 4 * b.(bound_local)) 8 in (* stack data *) - let oretaddr := align (ostkdata + b.(bound_stack_data)) 4 in (* return address *) - let sz := oretaddr + 4 in (* total size *) + let oretaddr := align (ostkdata + b.(bound_stack_data)) w in (* return address *) + let sz := oretaddr + w in (* total size *) {| fe_size := sz; fe_ofs_link := olink; fe_ofs_retaddr := oretaddr; @@ -47,31 +47,31 @@ Definition make_env (b: bounds) : frame_env := fe_stack_data := ostkdata; fe_used_callee_save := b.(used_callee_save) |}. -(** Separation property *) - -Local Open Scope sep_scope. - Lemma frame_env_separated: forall b sp m P, let fe := make_env b in m |= range sp 0 (fe_stack_data fe) ** range sp (fe_stack_data fe + bound_stack_data b) (fe_size fe) ** P -> m |= range sp (fe_ofs_local fe) (fe_ofs_local fe + 4 * bound_local b) ** range sp fe_ofs_arg (fe_ofs_arg + 4 * bound_outgoing b) - ** range sp (fe_ofs_link fe) (fe_ofs_link fe + 4) - ** range sp (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4) + ** range sp (fe_ofs_link fe) (fe_ofs_link fe + size_chunk Mptr) + ** range sp (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + size_chunk Mptr) ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. Local Opaque Z.add Z.mul sepconj range. intros; simpl. - set (olink := 4 * b.(bound_outgoing)). - set (ocs := olink + 4). + set (w := if Archi.ptr64 then 8 else 4). + set (olink := align (4 * b.(bound_outgoing)) w). + set (ocs := olink + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4). + set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). + replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto). + assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= olink) by (unfold olink; omega). - assert (olink + 4 <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by omega. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). + assert (olink + w <= ocs) by (unfold ocs; omega). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). @@ -88,7 +88,7 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap34. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split. omega. + apply range_split_2. fold olink. omega. omega. apply range_split. omega. apply range_split_2. fold ol. omega. omega. apply range_drop_right with ostkdata. omega. @@ -104,14 +104,17 @@ Lemma frame_env_range: 0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe. Proof. intros; simpl. - set (olink := 4 * b.(bound_outgoing)). - set (ocs := olink + 4). + set (w := if Archi.ptr64 then 8 else 4). + set (olink := align (4 * b.(bound_outgoing)) w). + set (ocs := olink + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4). + set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). + assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= olink) by (unfold olink; omega). - assert (olink + 4 <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by omega. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). + assert (olink + w <= ocs) by (unfold ocs; omega). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). @@ -125,18 +128,21 @@ Lemma frame_env_aligned: (8 | fe_ofs_arg) /\ (8 | fe_ofs_local fe) /\ (8 | fe_stack_data fe) - /\ (4 | fe_ofs_link fe) - /\ (4 | fe_ofs_retaddr fe). + /\ (align_chunk Mptr | fe_ofs_link fe) + /\ (align_chunk Mptr | fe_ofs_retaddr fe). Proof. intros; simpl. - set (olink := 4 * b.(bound_outgoing)). - set (ocs := olink + 4). + set (w := if Archi.ptr64 then 8 else 4). + set (olink := align (4 * b.(bound_outgoing)) w). + set (ocs := olink + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4). + set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). + assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). split. apply Zdivide_0. split. apply align_divides; omega. split. apply align_divides; omega. - split. apply Z.divide_factor_l. + split. apply align_divides; omega. apply align_divides; omega. Qed. |