aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/Stacklayout.v
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/Stacklayout.v')
-rw-r--r--ia32/Stacklayout.v148
1 files changed, 0 insertions, 148 deletions
diff --git a/ia32/Stacklayout.v b/ia32/Stacklayout.v
deleted file mode 100644
index 44fd43b2..00000000
--- a/ia32/Stacklayout.v
+++ /dev/null
@@ -1,148 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-(** Machine- and ABI-dependent layout information for activation records. *)
-
-Require Import Coqlib.
-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.
-- Back link to parent frame
-- Saved values of integer callee-save registers used by the function.
-- Saved values of float callee-save registers used by the function.
-- Local stack slots.
-- Space for the stack-allocated data declared in Cminor
-- Return address.
-*)
-
-Definition fe_ofs_arg := 0.
-
-Definition make_env (b: bounds) : frame_env :=
- 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)) w in (* return address *)
- let sz := oretaddr + w in (* total size *)
- {| fe_size := sz;
- fe_ofs_link := olink;
- fe_ofs_retaddr := oretaddr;
- fe_ofs_local := ol;
- fe_ofs_callee_save := ocs;
- fe_stack_data := ostkdata;
- fe_used_callee_save := b.(used_callee_save) |}.
-
-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 + 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 (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)) 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 <= 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).
- assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega).
-(* Reorder as:
- outgoing
- back link
- callee-save
- local
- retaddr *)
- rewrite sep_swap12.
- rewrite sep_swap23.
- rewrite sep_swap45.
- rewrite sep_swap34.
-(* Apply range_split and range_split2 repeatedly *)
- unfold fe_ofs_arg.
- 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.
- rewrite sep_swap.
- apply range_drop_left with (ostkdata + bound_stack_data b). omega.
- rewrite sep_swap.
- exact H.
-Qed.
-
-Lemma frame_env_range:
- forall b,
- let fe := make_env b in
- 0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe.
-Proof.
- intros; simpl.
- 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)) 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 <= 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).
- assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega).
- split. omega. omega.
-Qed.
-
-Lemma frame_env_aligned:
- forall b,
- let fe := make_env b in
- (8 | fe_ofs_arg)
- /\ (8 | fe_ofs_local fe)
- /\ (8 | fe_stack_data fe)
- /\ (align_chunk Mptr | fe_ofs_link fe)
- /\ (align_chunk Mptr | fe_ofs_retaddr fe).
-Proof.
- intros; simpl.
- 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)) 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 align_divides; omega.
- apply align_divides; omega.
-Qed.
generated by cgit (git 2.34.1) at 2024-07-08 10:38:31 +0000