diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-04-09 16:59:13 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-04-09 16:59:13 +0000 |
commit | abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 (patch) | |
tree | ae109a136508da283a9e2be5f039c5f9cca4f95c /ia32/PrintAsm.ml | |
parent | ffd6080f9e1e742c73ac38354b31c6fc4e3963ba (diff) | |
download | compcert-kvx-abe2bb5c40260a31ce5ee27b841bcbd647ff8b88.tar.gz compcert-kvx-abe2bb5c40260a31ce5ee27b841bcbd647ff8b88.zip |
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
Diffstat (limited to 'ia32/PrintAsm.ml')
-rw-r--r-- | ia32/PrintAsm.ml | 20 |
1 files changed, 10 insertions, 10 deletions
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 |