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, 10 insertions, 10 deletions

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index e4c2ea1..e4de2a3 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -165,12 +165,12 @@ let int32_align n a =
   then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a))
   else Int32.logand n (Int32.of_int (-a))
 
-let sp_adjustment lo hi =
-  let lo = camlint_of_coqint lo and hi = camlint_of_coqint hi in
-  let sz = Int32.sub hi lo in
-(* Enforce stack alignment, noting that 4 bytes are already allocated
-   by the call *)
-  let sz = Int32.sub (int32_align (Int32.add sz 4l) stack_alignment) 4l in
+let sp_adjustment sz =
+  let sz = camlint_of_coqint sz in
+  (* Preserve proper alignment of the stack *)
+  let sz = int32_align sz stack_alignment in
+  (* The top 4 bytes have already been allocated by the "call" instruction. *)
+  let sz = Int32.sub sz 4l in
   assert (sz >= 0l);
   sz
 
@@ -549,14 +549,14 @@ let print_instruction oc labels = function
   | Plabel(l) ->
       if Labelset.mem l labels then
         fprintf oc "%a:\n" label (transl_label l)
-  | Pallocframe(lo, hi, ofs_ra, ofs_link) ->
-      let sz = sp_adjustment lo hi in
+  | Pallocframe(sz, ofs_ra, ofs_link) ->
+      let sz = sp_adjustment sz in
       let ofs_link = camlint_of_coqint ofs_link in
       fprintf oc "	subl	$%ld, %%esp\n" sz;
       fprintf oc "	leal	%ld(%%esp), %%edx\n" (Int32.add sz 4l);
       fprintf oc "	movl	%%edx, %ld(%%esp)\n" ofs_link
-  | Pfreeframe(lo, hi, ofs_ra, ofs_link) ->
-      let sz = sp_adjustment lo hi in
+  | Pfreeframe(sz, ofs_ra, ofs_link) ->
+      let sz = sp_adjustment sz in
       fprintf oc "	addl	$%ld, %%esp\n" sz
   | Pbuiltin(ef, args, res) ->
       let name = extern_atom ef.ef_id in