From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Bounds.v | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'backend/Bounds.v') diff --git a/backend/Bounds.v b/backend/Bounds.v index 514895b..0415670 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Computation of resource bounds forr Linear code. *) +(** Computation of resource bounds for Linear code. *) Require Import Coqlib. Require Import Maps. @@ -36,11 +36,13 @@ Record bounds : Type := mkbounds { bound_int_callee_save: Z; bound_float_callee_save: Z; bound_outgoing: Z; + bound_stack_data: Z; bound_int_local_pos: bound_int_local >= 0; bound_float_local_pos: bound_float_local >= 0; bound_int_callee_save_pos: bound_int_callee_save >= 0; bound_float_callee_save_pos: bound_float_callee_save >= 0; - bound_outgoing_pos: bound_outgoing >= 0 + bound_outgoing_pos: bound_outgoing >= 0; + bound_stack_data_pos: bound_stack_data >= 0 }. (** The following predicates define the correctness of a set of bounds @@ -186,15 +188,19 @@ Program Definition function_bounds := (max_over_regs_of_funct float_callee_save) (Zmax (max_over_instrs outgoing_space) (max_over_slots_of_funct outgoing_slot)) + (Zmax f.(fn_stacksize) 0) (max_over_slots_of_funct_pos int_local) (max_over_slots_of_funct_pos float_local) (max_over_regs_of_funct_pos int_callee_save) (max_over_regs_of_funct_pos float_callee_save) - _. + _ _. Next Obligation. apply Zle_ge. eapply Zle_trans. 2: apply Zmax2. apply Zge_le. apply max_over_slots_of_funct_pos. Qed. +Next Obligation. + apply Zle_ge. apply Zmax2. +Qed. (** We now show the correctness of the inferred bounds. *) -- cgit v1.2.3