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 --- ia32/PrintAsm.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'ia32/PrintAsm.ml') diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index e4c2ea1d..e4de2a32 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 -- cgit