diff options
| -rw-r--r-- | .depend | 12 | ||||
| -rw-r--r-- | caml/PrintPPC.ml | 16 |
2 files changed, 16 insertions, 12 deletions
@@ -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 3d247e1..311a71f 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) -> |