diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-04-13 09:43:01 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-04-13 09:43:01 +0000 |
commit | 795ae4b8a7e95aa8fb850d109ad38f5c5cc21673 (patch) | |
tree | 64c35ef484a7aa6ecce21f916c1c1fc0cd9e9c98 /caml | |
parent | 41ef4d52e3c328d930979115cb4fd388cda09440 (diff) | |
download | compcert-795ae4b8a7e95aa8fb850d109ad38f5c5cc21673.tar.gz compcert-795ae4b8a7e95aa8fb850d109ad38f5c5cc21673.zip |
Alignement de la pile dans PrintPPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@606 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml')
-rw-r--r-- | caml/PrintPPC.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index 3d247e10..311a71f3 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -120,11 +120,15 @@ let print_instruction oc labels = function fprintf oc " addze %a, %a\n" ireg r1 ireg r2 | Pallocblock -> fprintf oc " bl _compcert_alloc\n" - | Pallocframe(lo, hi) -> + | Pallocframe(lo, hi, ofs) -> let lo = camlint_of_coqint lo - and hi = camlint_of_coqint hi in - let nsz = Int32.neg (Int32.sub hi lo) in - fprintf oc " stwu r1, %ld(r1)\n" nsz + and hi = camlint_of_coqint hi + and ofs = camlint_of_coqint ofs in + let sz = Int32.sub hi lo in + (* Keep stack 16-aligned *) + let sz16 = Int32.logand (Int32.add sz 15l) 0xFFFF_FFF0l in + assert (ofs = 0l); + fprintf oc " stwu r1, %ld(r1)\n" (Int32.neg sz16) | Pand_(r1, r2, r3) -> fprintf oc " and. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pandc(r1, r2, r3) -> @@ -169,8 +173,8 @@ let print_instruction oc labels = function fprintf oc " extsb %a, %a\n" ireg r1 ireg r2 | Pextsh(r1, r2) -> fprintf oc " extsh %a, %a\n" ireg r1 ireg r2 - | Pfreeframe -> - fprintf oc " lwz r1, 0(r1)\n" + | Pfreeframe ofs -> + fprintf oc " lwz r1, %ld(r1)\n" (camlint_of_coqint ofs) | Pfabs(r1, r2) -> fprintf oc " fabs %a, %a\n" freg r1 freg r2 | Pfadd(r1, r2, r3) -> |