diff options
| -rw-r--r-- | .depend | 8 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 12 |
3 files changed, 10 insertions, 12 deletions
@@ -40,7 +40,7 @@ backend/RTLtyping.vo backend/RTLtyping.glob: backend/RTLtyping.v lib/Coqlib.vo c backend/Kildall.vo backend/Kildall.glob: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo backend/Constprop.vo backend/Constprop.glob: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo -$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo +$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo backend/Constpropproof.vo backend/Constpropproof.glob: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo backend/CSE.vo backend/CSE.glob: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSEproof.vo backend/CSEproof.glob: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSE.vo @@ -86,9 +86,9 @@ backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v backend/Machsem.vo backend/Machsem.glob: backend/Machsem.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asm.vo $(ARCH)/Asm.glob: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo -$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo -$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo -$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo @@ -69,8 +69,6 @@ BACKEND=\ Machsem.v \ Asm.v Asmgen.v Asmgenretaddr.v Asmgenproof1.v Asmgenproof.v -# CastOptim.v CastOptimproof.v \ - # C front-end modules (in cfrontend/) CFRONTEND=Csyntax.v Csem.v Cstrategy.v Cexec.v \ diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index d79735a..1ce95f2 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -375,7 +375,7 @@ let print_builtin_memcpy oc sz al args = (* Handling of volatile reads and writes *) -let print_builtin_vload_shared oc chunk base offset res = +let print_builtin_vload_common oc chunk base offset res = match chunk, res with | Mint8unsigned, IR res -> fprintf oc " lbz %a, %a(%a)\n" ireg res constant offset ireg base @@ -399,7 +399,7 @@ let print_builtin_vload oc chunk args res = fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; begin match args with | [IR addr] -> - print_builtin_vload_shared oc chunk addr (Cint Integers.Int.zero) res + print_builtin_vload_common oc chunk addr (Cint Integers.Int.zero) res | _ -> assert false end; @@ -409,10 +409,10 @@ let print_builtin_vload_global oc chunk id ofs args res = fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; fprintf oc " addis %a, %a, %a\n" ireg GPR11 ireg_or_zero GPR0 constant (Csymbol_high(id, ofs)); - print_builtin_vload_shared oc chunk GPR11 (Csymbol_low(id, ofs)) res; + print_builtin_vload_common oc chunk GPR11 (Csymbol_low(id, ofs)) res; fprintf oc "%s end builtin __builtin_volatile_read\n" comment -let print_builtin_vstore_shared oc chunk base offset src = +let print_builtin_vstore_common oc chunk base offset src = match chunk, src with | (Mint8signed | Mint8unsigned), IR src -> fprintf oc " stb %a, %a(%a)\n" ireg src ireg base constant offset @@ -432,7 +432,7 @@ let print_builtin_vstore oc chunk args = fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; begin match args with | [IR addr; src] -> - print_builtin_vstore_shared oc chunk addr (Cint Integers.Int.zero) src + print_builtin_vstore_common oc chunk addr (Cint Integers.Int.zero) src | _ -> assert false end; @@ -445,7 +445,7 @@ let print_builtin_vstore_global oc chunk id ofs args = let tmp = if src = IR GPR11 then GPR12 else GPR11 in fprintf oc " addis %a, %a, %a\n" ireg tmp ireg_or_zero GPR0 constant (Csymbol_high(id, ofs)); - print_builtin_vstore_shared oc chunk tmp (Csymbol_low(id, ofs)) src + print_builtin_vstore_common oc chunk tmp (Csymbol_low(id, ofs)) src | _ -> assert false end; |