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

1 files changed, 8 insertions, 13 deletions

diff --git a/backend/Stacking.v b/backend/Stacking.v
index 2ea08beb..09d98d6c 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -118,19 +118,17 @@ Definition restore_callee_save (fe: frame_env) (k: Mach.code) :=
 (** * Code transformation. *)
 
 (** Translation of operations and addressing mode.
-  In Linear, the stack pointer has offset 0, i.e. points to the
-  beginning of the Cminor stack data block.  In Mach, the stack
-  pointer points to the bottom of the activation record,
-  at offset [- fe.(fe_size)] where [fe] is the frame environment.
+  The Cminor stack data block starts at offset 0 in Linear,
+  but at offset [fe.(fe_stack_data)] in Mach.
   Operations and addressing mode that are relative to the stack pointer
-  must therefore be offset by [fe.(fe_size)] to preserve their
+  must therefore be offset by [fe.(fe_stack_data)] to preserve their
   behaviour. *)
 
 Definition transl_op (fe: frame_env) (op: operation) :=
-  shift_stack_operation (Int.repr fe.(fe_size)) op.
+  shift_stack_operation (Int.repr fe.(fe_stack_data)) op.
 
 Definition transl_addr (fe: frame_env) (addr: addressing) :=
-  shift_stack_addressing (Int.repr fe.(fe_size)) addr.
+  shift_stack_addressing (Int.repr fe.(fe_stack_data)) addr.
 
 (** Translation of a Linear instruction.  Prepends the corresponding
   Mach instructions to the given list of instructions.
@@ -193,8 +191,8 @@ Definition transl_instr
   by the translation of the function body.
 
   Subtle point: the compiler must check that the frame is no
-  larger than [- Int.min_signed] bytes, otherwise arithmetic overflows
-  could occur during frame accesses using signed machine integers as
+  larger than [Int.max_unsigned] bytes, otherwise arithmetic overflows
+  could occur during frame accesses using unsigned machine integers as
   offsets. *)
 
 Definition transl_code
@@ -208,15 +206,12 @@ Open Local Scope string_scope.
 
 Definition transf_function (f: Linear.function) : res Mach.function :=
   let fe := make_env (function_bounds f) in
-  if zlt f.(Linear.fn_stacksize) 0 then
-    Error (msg "Stacking.transf_function") 
-  else if zlt (- Int.min_signed) fe.(fe_size) then
+  if zlt Int.max_unsigned fe.(fe_size) then
     Error (msg "Too many spilled variables, stack size exceeded")
   else
     OK (Mach.mkfunction
          f.(Linear.fn_sig)
          (transl_body f fe)
-         f.(Linear.fn_stacksize)
          fe.(fe_size)
          (Int.repr fe.(fe_ofs_link))
          (Int.repr fe.(fe_ofs_retaddr))).