From 795ae4b8a7e95aa8fb850d109ad38f5c5cc21673 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 13 Apr 2008 09:43:01 +0000
Subject: [PATCH] Alignement de la pile dans PrintPPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@606 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
.depend | 12 ++++++------
caml/PrintPPC.ml | 16 ++++++++++------
2 files changed, 16 insertions(+), 12 deletions(-)
diff --git a/.depend b/.depend
index 3a2036e6f..cf24f7f7d 100644
--- a/.depend
+++ b/.depend
@@ -47,9 +47,9 @@ backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo co
backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo
backend/LTLin.vo: backend/LTLin.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo
backend/LTLintyping.vo: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo
-backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLin.vo backend/Kildall.vo lib/Lattice.vo
-backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo lib/Lattice.vo
-backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo backend/Conventions.vo
+backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Errors.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLin.vo backend/Kildall.vo lib/Lattice.vo
+backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo lib/Lattice.vo
+backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo backend/Conventions.vo
backend/Linear.vo: backend/Linear.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo
backend/Lineartyping.vo: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo
backend/Parallelmove.vo: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo common/Values.vo common/Events.vo common/AST.vo backend/Locations.vo backend/Conventions.vo
@@ -57,14 +57,14 @@ backend/Reload.vo: backend/Reload.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/
backend/Reloadproof.vo: backend/Reloadproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Allocproof.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Parallelmove.vo backend/Reload.vo
backend/Reloadtyping.vo: backend/Reloadtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Parallelmove.vo backend/Reload.vo backend/Reloadproof.vo
backend/Mach.vo: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo
-backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Mem.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo
+backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Mem.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Stacking.vo
backend/Machtyping.vo: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Mem.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machabstr.vo
backend/Bounds.vo: backend/Bounds.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo
backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo
backend/Stackingproof.vo: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo backend/Op.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machabstr.vo backend/Bounds.vo backend/Conventions.vo backend/Stacking.vo
backend/Stackingtyping.vo: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo backend/Stacking.vo backend/Stackingproof.vo
-backend/Machconcr.vo: backend/Machconcr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/PPCgenretaddr.vo
-backend/Machabstr2concr.vo: backend/Machabstr2concr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/Machabstr.vo backend/Machconcr.vo backend/Stackingproof.vo backend/PPCgenretaddr.vo
+backend/Machconcr.vo: backend/Machconcr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Stacking.vo backend/PPCgenretaddr.vo
+backend/Machabstr2concr.vo: backend/Machabstr2concr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/Machabstr.vo backend/Machconcr.vo backend/PPCgenretaddr.vo
backend/PPC.vo: backend/PPC.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo
backend/PPCgen.vo: backend/PPCgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/PPC.vo
backend/PPCgenretaddr.vo: backend/PPCgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/PPC.vo backend/PPCgen.vo
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index 3d247e10c..311a71f3e 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) ->
--
GitLab