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: Alignement de la pile dans PrintPPC

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@606 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/PrintPPC.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'caml')

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) ->
-- 
cgit