diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-06-29 08:27:14 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-06-29 08:27:14 +0000 |
| commit | 9c7c84cc40eaacc1e2c13091165785cddecba5ad (patch) | |
| tree | 65eafe51ad284d88fd5a949e1b2a54cd272f9f91 | |
| parent | f4b416882955d9d91bca60f3eb35b95f4124a5be (diff) | |
| download | compcert-kvx-9c7c84cc40eaacc1e2c13091165785cddecba5ad.tar.gz compcert-kvx-9c7c84cc40eaacc1e2c13091165785cddecba5ad.zip | |
Support for inlined built-ins.
AST: add ef_inline flag to external functions.
Selection: recognize calls to inlined built-ins and inline them as Sbuiltin.
CminorSel to Asm: added Sbuiltin/Ibuiltin instruction.
PrintAsm: adapted expansion of builtins.
C2Clight: adapted detection of builtins.
Conventions: refactored in a machine-independent part (backend/Conventions)
and a machine-dependent part (ARCH/SYS/Conventions1).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
77 files changed, 1228 insertions, 1302 deletions
@@ -32,9 +32,9 @@ backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Intege backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgenspec.vo: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenproof.vo: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo common/Switch.vo backend/Registers.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenspec.vo common/Errors.vo -backend/Tailcall.vo: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo -backend/Tailcallproof.vo: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Tailcall.vo -backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo common/Memory.vo lib/Integers.vo common/Events.vo common/Smallstep.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo +backend/Tailcall.vo: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo +backend/Tailcallproof.vo: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Tailcall.vo +backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo common/Memory.vo lib/Integers.vo common/Events.vo common/Smallstep.vo backend/RTL.vo backend/Conventions.vo backend/Kildall.vo: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Ordered.vo $(ARCH)/ConstpropOp.vo: $(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.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 @@ -44,44 +44,45 @@ backend/CSE.vo: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Intege backend/CSEproof.vo: 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 $(ARCH)/Machregs.vo: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Locations.vo: backend/Locations.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo -$(ARCH)/$(VARIANT)/Conventions.vo: $(ARCH)/$(VARIANT)/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo -backend/LTL.vo: backend/LTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo -backend/LTLtyping.vo: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo $(ARCH)/$(VARIANT)/Conventions.vo +$(ARCH)/$(VARIANT)/Conventions1.vo: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo +backend/Conventions.vo: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo +backend/LTL.vo: backend/LTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo +backend/LTLtyping.vo: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo backend/InterfGraph.vo: backend/InterfGraph.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo -backend/Coloring.vo: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/InterfGraph.vo -backend/Coloringproof.vo: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo -backend/Allocation.vo: backend/Allocation.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Coloring.vo backend/LTL.vo -backend/Allocproof.vo: backend/Allocproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/LTL.vo -backend/Alloctyping.vo: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo $(ARCH)/$(VARIANT)/Conventions.vo +backend/Coloring.vo: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo +backend/Coloringproof.vo: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo +backend/Allocation.vo: backend/Allocation.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/LTL.vo +backend/Allocproof.vo: backend/Allocproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/LTL.vo +backend/Alloctyping.vo: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Conventions.vo backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/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/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo $(ARCH)/$(VARIANT)/Conventions.vo -backend/LTLintyping.vo: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/LTLtyping.vo $(ARCH)/$(VARIANT)/Conventions.vo +backend/LTLin.vo: backend/LTLin.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/LTL.vo backend/Conventions.vo +backend/LTLintyping.vo: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/LTLtyping.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 $(ARCH)/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/Memory.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo $(ARCH)/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 $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo $(ARCH)/$(VARIANT)/Conventions.vo -backend/Linear.vo: backend/Linear.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/LTL.vo $(ARCH)/$(VARIANT)/Conventions.vo -backend/Lineartyping.vo: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo $(ARCH)/$(VARIANT)/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 $(ARCH)/$(VARIANT)/Conventions.vo -backend/Reload.vo: backend/Reload.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Parallelmove.vo backend/Linear.vo -backend/Reloadproof.vo: backend/Reloadproof.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 $(ARCH)/$(VARIANT)/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 $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Lineartyping.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Parallelmove.vo backend/Reload.vo backend/Reloadproof.vo +backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/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/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/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 lib/Integers.vo common/Memdata.vo $(ARCH)/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 +backend/Reload.vo: backend/Reload.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo backend/Parallelmove.vo backend/Linear.vo +backend/Reloadproof.vo: backend/Reloadproof.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/Allocproof.vo backend/RTLtyping.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 $(ARCH)/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/Memory.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo -backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo -backend/Machtyping.vo: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Mach.vo backend/Machabstr.vo -backend/Bounds.vo: backend/Bounds.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo $(ARCH)/$(VARIANT)/Conventions.vo +backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.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 +backend/Machtyping.vo: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo $(ARCH)/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 $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo: $(ARCH)/$(VARIANT)/Stacklayout.v lib/Coqlib.vo backend/Bounds.vo -backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.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 $(ARCH)/Op.vo common/Memory.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 $(ARCH)/$(VARIANT)/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.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 $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.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/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo -backend/Machabstr2concr.vo: backend/Machabstr2concr.v lib/Axioms.vo 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/Mach.vo backend/Machtyping.vo backend/Machabstr.vo backend/Machconcr.vo $(ARCH)/Asmgenretaddr.vo -$(ARCH)/Asm.vo: $(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 $(ARCH)/$(VARIANT)/Conventions.vo +backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.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 $(ARCH)/Op.vo common/Memory.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 $(ARCH)/$(VARIANT)/Stacklayout.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 $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.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/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 +backend/Machabstr2concr.vo: backend/Machabstr2concr.v lib/Axioms.vo 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/Mach.vo backend/Machtyping.vo backend/Machabstr.vo backend/Machconcr.vo backend/Conventions.vo $(ARCH)/Asmgenretaddr.vo +$(ARCH)/Asm.vo: $(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.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.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.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/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/$(VARIANT)/Conventions.vo -$(ARCH)/Asmgenproof.vo: $(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/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgenproof1.vo: $(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/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo: $(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/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csem.vo: 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/Ctyping.vo: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo cfrontend/Csyntax.vo @@ -16,7 +16,7 @@ DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver INCLUDES=$(patsubst %,-I %, $(DIRS)) -COQC=coqc $(INCLUDES) +COQC=coqc -q $(INCLUDES) COQDEP=coqdep $(INCLUDES) COQDOC=coqdoc COQEXEC=coqtop $(INCLUDES) -batch -load-vernac-source @@ -53,7 +53,7 @@ BACKEND=\ Kildall.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ CSE.v CSEproof.v \ - Machregs.v Locations.v Conventions.v LTL.v LTLtyping.v \ + Machregs.v Locations.v Conventions1.v Conventions.v LTL.v LTLtyping.v \ InterfGraph.v Coloring.v Coloringproof.v \ Allocation.v Allocproof.v Alloctyping.v \ Tunneling.v Tunnelingproof.v Tunnelingtyping.v \ @@ -24,7 +24,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Locations. Require Stacklayout. -Require Conventions. +Require Import Conventions. (** * Abstract syntax *) @@ -65,6 +65,28 @@ Inductive crbit: Type := Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}. Proof. decide equality. Defined. +(** We model the following registers of the ARM architecture. *) + +Inductive preg: Type := + | IR: ireg -> preg (**r integer registers *) + | FR: freg -> preg (**r float registers *) + | CR: crbit -> preg (**r bits in the condition register *) + | PC: preg. (**r program counter *) + +Coercion IR: ireg >-> preg. +Coercion FR: freg >-> preg. +Coercion CR: crbit >-> preg. + +Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. +Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined. + +Module PregEq. + Definition t := preg. + Definition eq := preg_eq. +End PregEq. + +Module Pregmap := EMap(PregEq). + (** The instruction set. Most instructions correspond exactly to actual instructions of the PowerPC processor. See the PowerPC reference manuals for more details. Some instructions, @@ -149,7 +171,8 @@ Inductive instruction : Type := | Pfreeframe: Z -> Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *) - | Pbtbl: ireg -> list label -> instruction. (**r N-way branch through a jump table *) + | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) + | Pbuiltin: external_function -> list preg -> preg -> instruction. (**r built-in *) (** The pseudo-instructions are the following: @@ -204,28 +227,6 @@ Definition program := AST.program fundef unit. (** * Operational semantics *) -(** We model the following registers of the ARM architecture. *) - -Inductive preg: Type := - | IR: ireg -> preg (**r integer registers *) - | FR: freg -> preg (**r float registers *) - | CR: crbit -> preg (**r bits in the condition register *) - | PC: preg. (**r program counter *) - -Coercion IR: ireg >-> preg. -Coercion FR: freg >-> preg. -Coercion CR: crbit >-> preg. - -Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined. - -Module PregEq. - Definition t := preg. - Definition eq := preg_eq. -End PregEq. - -Module Pregmap := EMap(PregEq). - (** The semantics operates over a single mapping from registers (type [preg]) to values. We maintain (but do not enforce) the convention that integer registers are mapped to values of @@ -532,6 +533,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome else Error | _ => Error end + | Pbuiltin ef args res => Error (**r treated specially below *) end. (** Translation of the LTL/Linear/Mach view of machine registers @@ -594,10 +596,10 @@ Inductive extcall_args (rs: regset) (m: mem): list loc -> list val -> Prop := Definition extcall_arguments (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := - extcall_args rs m (Conventions.loc_arguments sg) args. + extcall_args rs m (loc_arguments sg) args. Definition loc_external_result (sg: signature) : preg := - preg_of (Conventions.loc_result sg). + preg_of (loc_result sg). (** Execution of the instruction at [rs#PC]. *) @@ -612,13 +614,20 @@ Inductive step: state -> trace -> state -> Prop := find_instr (Int.unsigned ofs) c = Some i -> exec_instr c i rs m = OK rs' m' -> step (State rs m) E0 (State rs' m') + | exec_step_builtin: + forall b ofs c ef args res rs m t v m', + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal c) -> + find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) -> + external_call ef ge (map rs args) m t v m' -> + step (State rs m) t (State (nextinstr(rs # res <- v)) m') | exec_step_external: forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> - extcall_arguments rs m ef.(ef_sig) args -> - rs' = (rs#(loc_external_result ef.(ef_sig)) <- res + extcall_arguments rs m (ef_sig ef) args -> + rs' = (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs IR14)) -> step (State rs m) t (State rs' m'). diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 2a3b3f36..775bb37f 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -55,7 +55,7 @@ Definition is_immed_mem_float (x: int) : bool := Int.eq (Int.and x (Int.repr 3)) Int.zero && Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x. -(** Smart constructor for integer immediate arguments. *) +(** Smart constructors for integer immediate arguments. *) Definition loadimm (r: ireg) (n: int) (k: code) := if is_immed_arith n then @@ -479,6 +479,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := loadind_int IR13 f.(fn_retaddr_ofs) IR14 (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb :: k) + | Mbuiltin ef args res => + Pbuiltin ef (map preg_of args) (preg_of res) :: k | Mlabel lbl => Plabel lbl :: k | Mgoto lbl => diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 99759720..cc4d7ac5 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -25,6 +25,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Op. Require Import Locations. +Require Import Conventions. Require Import Mach. Require Import Machconcr. Require Import Machtyping. @@ -896,6 +897,37 @@ Lemma exec_Mtailcall_prop:
forall (s : list stackframe) (fb stk : block) (soff intros. rewrite Pregmap.gso; auto. Qed. +Lemma exec_Mbuiltin_prop: + forall (s : list stackframe) (f : block) (sp : val) + (ms : Mach.regset) (m : mem) (ef : external_function) + (args : list mreg) (res : mreg) (b : list Mach.instruction) + (t : trace) (v : val) (m' : mem), + external_call ef ge ms ## args m t v m' -> + exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t + (Machconcr.State s f sp b (Regmap.set res v ms) m'). +Proof. + intros; red; intros; inv MS. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI. inv WTI. + inv AT. simpl in H3. + generalize (functions_transl _ _ FIND); intro FN. + generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. + left. econstructor; split. apply plus_one. + eapply exec_step_builtin. eauto. eauto. + eapply find_instr_tail; eauto. + replace (rs##(preg_of##args)) with (ms##args). + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + rewrite list_map_compose. apply list_map_exten. intros. + symmetry. eapply preg_val; eauto. + econstructor; eauto with coqlib. + unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. + rewrite <- H0. simpl. constructor; auto. + eapply code_tail_next_int; eauto. + apply sym_not_equal. auto with ppcgen. + auto with ppcgen. +Qed. + Lemma exec_Mgoto_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) @@ -1145,7 +1177,7 @@ Lemma exec_function_external_prop: Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef ge args m t0 res m' -> Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> - ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> + ms' = Regmap.set (loc_result (ef_sig ef)) res ms -> exec_instr_prop (Machconcr.Callstate s fb ms m) t0 (Machconcr.Returnstate s ms' m'). Proof. @@ -1187,6 +1219,7 @@ Proof exec_Mstore_prop exec_Mcall_prop exec_Mtailcall_prop + exec_Mbuiltin_prop exec_Mgoto_prop exec_Mcond_true_prop exec_Mcond_false_prop @@ -24,6 +24,7 @@ syntax and dynamic semantics of the Cminor language. *) +Require Import Axioms. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -132,7 +133,7 @@ Proof. generalize Int.eq_dec; intro. assert (forall (x y: shift_amount), {x=y}+{x<>y}). destruct x as [x Px]. destruct y as [y Py]. destruct (H x y). - subst x. rewrite (proof_irrelevance _ Px Py). left; auto. + subst x. rewrite (proof_irr Px Py). left; auto. right. red; intro. elim n. inversion H0. auto. decide equality. Qed. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 3184d92f..b3f49cd6 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -188,7 +188,53 @@ let call_helper oc fn dst arg1 arg2 = (* ... for a total of at most 7 instructions *) 7 -(* Built-in functions *) +(* Built-ins. They come in two flavors: + - inlined by the compiler: take their arguments in arbitrary + registers; preserve all registers except IR14 + - inlined while printing asm code; take their arguments in + locations dictated by the calling conventions; preserve + callee-save regs only. *) + +let print_builtin_inlined oc name args res = + fprintf oc "%s begin %s\n" comment name; + let n = match name, args, res with + (* Volatile reads *) + | "__builtin_volatile_read_int8unsigned", [IR addr], IR res -> + fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 + | "__builtin_volatile_read_int8signed", [IR addr], IR res -> + fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 + | "__builtin_volatile_read_int16unsigned", [IR addr], IR res -> + fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 + | "__builtin_volatile_read_int16signed", [IR addr], IR res -> + fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 + | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res -> + fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 + | "__builtin_volatile_read_float32", [IR addr], FR res -> + fprintf oc " ldfs %a, [%a, #0]\n" freg res ireg addr; + fprintf oc " mvfd %a, %a\n" freg res freg res; 2 + | "__builtin_volatile_read_float64", [IR addr], FR res -> + fprintf oc " ldfd %a, [%a, #0]\n" freg res ireg addr; 1 + (* Volatile writes *) + | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ -> + fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1 + | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ -> + fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 + | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ -> + fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 + | "__builtin_volatile_write_float32", [IR addr; FR src], _ -> + fprintf oc " mvfs %a, %a\n" freg FR2 freg src; + fprintf oc " stfs %a, [%a, #0]\n" freg FR2 ireg addr; 2 + | "__builtin_volatile_write_float64", [IR addr; FR src], _ -> + fprintf oc " stfd %a, [%a, #0]\n" freg src ireg addr; 1 + (* Float arithmetic *) + | "__builtin_fabs", [FR a1], FR res -> + fprintf oc " absd %a, %a\n" freg res freg a1; 1 + (* Catch-all *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + in + fprintf oc "%s end %s\n" comment name; + n let re_builtin_function = Str.regexp "__builtin_" @@ -200,38 +246,6 @@ let print_builtin_function oc s = (* int args: IR0-IR3 float args: FR0, FR1 int res: IR0 float res: FR0 *) let n = match extern_atom s with - (* Volatile reads *) - | "__builtin_volatile_read_int8unsigned" -> - fprintf oc " ldrb %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_int8signed" -> - fprintf oc " ldrsb %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_int16unsigned" -> - fprintf oc " ldrh %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_int16signed" -> - fprintf oc " ldrsh %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_int32" - | "__builtin_volatile_read_pointer" -> - fprintf oc " ldr %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_float32" -> - fprintf oc " ldfs %a, [%a, #0]\n" freg FR0 ireg IR0; - fprintf oc " mvfd %a, %a\n" freg FR0 freg FR0; 2 - | "__builtin_volatile_read_float64" -> - fprintf oc " ldfd %a, [%a, #0]\n" freg FR0 ireg IR0; 1 - (* Volatile writes *) - | "__builtin_volatile_write_int8unsigned" - | "__builtin_volatile_write_int8signed" -> - fprintf oc " strb %a, [%a, #0]\n" ireg IR1 ireg IR0; 1 - | "__builtin_volatile_write_int16unsigned" - | "__builtin_volatile_write_int16signed" -> - fprintf oc " strh %a, [%a, #0]\n" ireg IR1 ireg IR0; 1 - | "__builtin_volatile_write_int32" - | "__builtin_volatile_write_pointer" -> - fprintf oc " str %a, [%a, #0]\n" ireg IR1 ireg IR0; 1 - | "__builtin_volatile_write_float32" -> - fprintf oc " mvfs %a, %a\n" freg FR0 freg FR0; - fprintf oc " stfs %a, [%a, #0]\n" freg FR0 ireg IR0; 2 - | "__builtin_volatile_write_float64" -> - fprintf oc " stfd %a, [%a, #0]\n" freg FR0 ireg IR0; 1 (* Block copy *) | "__builtin_memcpy" -> let lbl1 = new_label() in @@ -252,7 +266,7 @@ let print_builtin_function oc s = fprintf oc " subnes %a, %a, #1\n" ireg IR2 ireg IR2; fprintf oc " bne %a\n" label lbl *) - | "__builtin_memcpy_word" -> + | "__builtin_memcpy_words" -> let lbl1 = new_label() in let lbl2 = new_label() in fprintf oc " movs %a, %a, lsr #2\n" ireg IR2 ireg IR2; @@ -467,6 +481,8 @@ let print_instruction oc labels = function (fun l -> fprintf oc " .word %a\n" print_label l) tbl; 2 + List.length tbl + | Pbuiltin(ef, args, res) -> + print_builtin_inlined oc (extern_atom ef.ef_id) args res let no_fallthrough = function | Pb _ -> true diff --git a/arm/linux/Conventions.v b/arm/linux/Conventions1.v index a35162c2..703dc12d 100644 --- a/arm/linux/Conventions.v +++ b/arm/linux/Conventions1.v @@ -222,65 +222,6 @@ Proof. unfold float_callee_save_regs; NoRepet. Qed. -(** * Acceptable locations for register allocation *) - -(** The following predicate describes the locations that can be assigned - to an RTL pseudo-register during register allocation: a non-temporary - machine register or a [Local] stack slot are acceptable. *) - -Definition loc_acceptable (l: loc) : Prop := - match l with - | R r => ~(In l temporaries) - | S (Local ofs ty) => ofs >= 0 - | S (Incoming _ _) => False - | S (Outgoing _ _) => False - end. - -Definition locs_acceptable (ll: list loc) : Prop := - forall l, In l ll -> loc_acceptable l. - -Lemma temporaries_not_acceptable: - forall l, loc_acceptable l -> Loc.notin l temporaries. -Proof. - unfold loc_acceptable; destruct l. - simpl. intuition congruence. - destruct s; try contradiction. - intro. simpl. tauto. -Qed. -Hint Resolve temporaries_not_acceptable: locs. - -Lemma locs_acceptable_disj_temporaries: - forall ll, locs_acceptable ll -> Loc.disjoint ll temporaries. -Proof. - intros. apply Loc.notin_disjoint. intros. - apply temporaries_not_acceptable. auto. -Qed. - -Lemma loc_acceptable_noteq_diff: - forall l1 l2, - loc_acceptable l1 -> l1 <> l2 -> Loc.diff l1 l2. -Proof. - unfold loc_acceptable, Loc.diff; destruct l1; destruct l2; - try (destruct s); try (destruct s0); intros; auto; try congruence. - case (zeq z z0); intro. - compare t t0; intro. - subst z0; subst t0; tauto. - tauto. tauto. - contradiction. contradiction. -Qed. - -Lemma loc_acceptable_notin_notin: - forall r ll, - loc_acceptable r -> - ~(In r ll) -> Loc.notin r ll. -Proof. - induction ll; simpl; intros. - auto. - split. apply loc_acceptable_noteq_diff. assumption. - apply sym_not_equal. tauto. - apply IHll. assumption. tauto. -Qed. - (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -326,40 +267,18 @@ Proof. reflexivity. Qed. -(** The result location is acceptable. *) - -Lemma loc_result_acceptable: - forall sig, loc_acceptable (R (loc_result sig)). -Proof. - intros. unfold loc_acceptable. red. - unfold loc_result. destruct (sig_res sig). - destruct t; simpl; NotOrEq. - simpl; NotOrEq. -Qed. - -(** The result location is a caller-save register. *) +(** The result location is a caller-save register or a temporary *) Lemma loc_result_caller_save: - forall (s: signature), In (R (loc_result s)) destroyed_at_call. + forall (s: signature), + In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries. Proof. - intros; unfold loc_result. + intros; unfold loc_result. left; destruct (sig_res s). destruct t; simpl; OrEq. simpl; OrEq. Qed. -(** The result location is not a callee-save register. *) - -Lemma loc_result_not_callee_save: - forall (s: signature), - ~(In (loc_result s) int_callee_save_regs \/ In (loc_result s) float_callee_save_regs). -Proof. - intros. generalize (loc_result_caller_save s). - generalize (int_callee_save_not_destroyed (loc_result s)). - generalize (float_callee_save_not_destroyed (loc_result s)). - tauto. -Qed. - (** ** Location of function arguments *) (** We use the following calling conventions, adapted from the ARM ABI: @@ -449,13 +368,6 @@ Fixpoint size_arguments_rec Definition size_arguments (s: signature) : Z := size_arguments_rec s.(sig_args) int_param_regs float_param_regs 0. -(** A tail-call is possible for a signature if the corresponding - arguments are all passed in registers. *) - -Definition tailcall_possible (s: signature) : Prop := - forall l, In l (loc_arguments s) -> - match l with R _ => True | S _ => False end. - (** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -685,24 +597,6 @@ Proof. ElimOrEq; intuition. Qed. -(** Callee-save registers do not overlap with argument locations. *) - -Lemma arguments_not_preserved: - forall sig l, - Loc.notin l destroyed_at_call -> loc_acceptable l -> - Loc.notin l (loc_arguments sig). -Proof. - intros. unfold loc_arguments. destruct l. - apply loc_arguments_rec_notin_reg. - generalize (Loc.notin_not_in _ _ H). intro; red; intro. - apply H1. generalize H2. simpl. ElimOrEq; OrEq. - generalize (Loc.notin_not_in _ _ H). intro; red; intro. - apply H1. generalize H2. simpl. ElimOrEq; OrEq. - destruct s; simpl in H0; try contradiction. - apply loc_arguments_rec_notin_local. -Qed. -Hint Resolve arguments_not_preserved: locs. - (** Argument locations agree in number with the function signature. *) Lemma loc_arguments_length: @@ -748,107 +642,3 @@ Proof. intro; simpl. ElimOrEq; reflexivity. Qed. -(** There is no partial overlap between an argument location and an - acceptable location: they are either identical or disjoint. *) - -Lemma no_overlap_arguments: - forall args sg, - locs_acceptable args -> - Loc.no_overlap args (loc_arguments sg). -Proof. - unfold Loc.no_overlap; intros. - generalize (H r H0). - generalize (loc_arguments_acceptable _ _ H1). - destruct s; destruct r; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; auto. - intros. right. auto. - destruct s; try tauto. destruct s0; tauto. -Qed. - -(** Decide whether a tailcall is possible. *) - -Definition tailcall_is_possible (sg: signature) : bool := - let fix tcisp (l: list loc) := - match l with - | nil => true - | R _ :: l' => tcisp l' - | S _ :: l' => false - end - in tcisp (loc_arguments sg). - -Lemma tailcall_is_possible_correct: - forall s, tailcall_is_possible s = true -> tailcall_possible s. -Proof. - intro s. unfold tailcall_is_possible, tailcall_possible. - generalize (loc_arguments s). induction l; simpl; intros. - elim H0. - destruct a. - destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate. -Qed. - -(** ** Location of function parameters *) - -(** A function finds the values of its parameter in the same locations - where its caller stored them, except that the stack-allocated arguments, - viewed as [Outgoing] slots by the caller, are accessed via [Incoming] - slots (at the same offsets and types) in the callee. *) - -Definition parameter_of_argument (l: loc) : loc := - match l with - | S (Outgoing n ty) => S (Incoming n ty) - | _ => l - end. - -Definition loc_parameters (s: signature) := - List.map parameter_of_argument (loc_arguments s). - -Lemma loc_parameters_type: - forall sig, List.map Loc.type (loc_parameters sig) = sig.(sig_args). -Proof. - intros. unfold loc_parameters. - rewrite list_map_compose. - rewrite <- loc_arguments_type. - apply list_map_exten. - intros. destruct x; simpl. auto. - destruct s; reflexivity. -Qed. - -Lemma loc_parameters_length: - forall sg, List.length (loc_parameters sg) = List.length sg.(sig_args). -Proof. - intros. unfold loc_parameters. rewrite list_length_map. - apply loc_arguments_length. -Qed. - -Lemma loc_parameters_not_temporaries: - forall sig, Loc.disjoint (loc_parameters sig) temporaries. -Proof. - intro; red; intros. - unfold loc_parameters in H. - elim (list_in_map_inv _ _ _ H). intros y [EQ IN]. - generalize (loc_arguments_not_temporaries sig y x2 IN H0). - subst x1. destruct x2. - destruct y; simpl. auto. destruct s; auto. - byContradiction. generalize H0. simpl. NotOrEq. -Qed. - -Lemma no_overlap_parameters: - forall params sg, - locs_acceptable params -> - Loc.no_overlap (loc_parameters sg) params. -Proof. - unfold Loc.no_overlap; intros. - unfold loc_parameters in H0. - elim (list_in_map_inv _ _ _ H0). intros t [EQ IN]. - rewrite EQ. - generalize (loc_arguments_acceptable _ _ IN). - generalize (H s H1). - destruct s; destruct t; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; simpl; auto. - intros; right; auto. - destruct s; try tauto. destruct s0; try tauto. - intros; simpl. tauto. -Qed. - diff --git a/backend/Allocation.v b/backend/Allocation.v index b802f4ac..69fb32fa 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -101,6 +101,8 @@ Definition transfer (reg_sum_live ros (reg_dead res after)) | Itailcall sig ros args => reg_list_live args (reg_sum_live ros Regset.empty) + | Ibuiltin ef args res s => + reg_list_live args (reg_dead res after) | Icond cond args ifso ifnot => reg_list_live args after | Ijumptable arg tbl => @@ -167,6 +169,8 @@ Definition transf_instr (assign res) s | Itailcall sig ros args => Ltailcall sig (sum_left_map assign ros) (List.map assign args) + | Ibuiltin ef args res s => + Lbuiltin ef (List.map assign args) (assign res) s | Icond cond args ifso ifnot => Lcond cond (List.map assign args) ifso ifnot | Ijumptable arg tbl => diff --git a/backend/Allocproof.v b/backend/Allocproof.v index c5d6adc3..d06c26fa 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -330,7 +330,7 @@ Lemma agree_postcall: forall live args ros res rs v (ls: locset), (forall r, Regset.In r live -> r <> res -> - ~(In (assign r) Conventions.destroyed_at_call)) -> + ~(In (assign r) destroyed_at_call)) -> (forall r, Regset.In r live -> r <> res -> assign r <> assign res) -> agree (reg_list_live args (reg_sum_live ros (reg_dead res live))) rs ls -> @@ -676,6 +676,19 @@ Proof. rewrite (sig_function_translated _ _ TF). eauto. rewrite H1. econstructor; eauto. + (* Ibuiltin *) + econstructor; split. + eapply exec_Lbuiltin; eauto. TranslInstr. + replace (map ls (@map reg loc assign args)) with (rs##args). + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + eapply agree_eval_regs; eauto. + generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). + unfold correct_alloc_instr. intro CORR. + MatchStates. + eapply agree_assign_live; eauto. + eapply agree_reg_list_live; eauto. + (* Icond, true *) assert (COND: eval_condition cond (map ls (map assign args)) = Some true). replace (map ls (map assign args)) with (rs##args). auto. diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index 260297f2..a6536831 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -139,6 +139,8 @@ Proof. split. autorewrite with allocty; auto. split. auto with allocty. auto. rewrite transf_unroll; auto. + (* builtin *) + WT. (* cond *) WT. (* jumptable *) diff --git a/backend/Bounds.v b/backend/Bounds.v index 15468c57..514895be 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -72,6 +72,7 @@ Definition instr_within_bounds (i: instruction) := | Lop op args res => mreg_within_bounds res | Lload chunk addr args dst => mreg_within_bounds dst | Lcall sig ros => size_arguments sig <= bound_outgoing b + | Lbuiltin ef args res => mreg_within_bounds res | _ => True end. @@ -103,6 +104,7 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil + | Lbuiltin ef args res => res :: nil | Llabel lbl => nil | Lgoto lbl => nil | Lcond cond args lbl => nil diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 84202096..1cd245ec 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -352,9 +352,7 @@ proc: fn_stackspace = $8; fn_body = $10 }) } | EXTERN STRINGLIT COLON signature - { Coq_pair($2, - External { ef_id = $2; - ef_sig = $4 }) } + { Coq_pair($2, External({ef_id = $2; ef_sig = $4; ef_inline = false})) } ; signature: diff --git a/backend/CSE.v b/backend/CSE.v index ff79be54..dab8fc31 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -189,7 +189,7 @@ Definition add_load (n: numbering) (rd: reg) (** [add_unknown n rd] returns a numbering where [rd] is mapped to a fresh value number, and no equations are added. This is useful - to model instructions with unpredictable results such as [Ialloc]. *) + to model instructions with unpredictable results such as [Ibuiltin]. *) Definition add_unknown (n: numbering) (rd: reg) := mknumbering (Psucc n.(num_next)) @@ -348,6 +348,8 @@ Definition transfer (f: function) (pc: node) (before: numbering) := empty_numbering | Itailcall sig ros args => empty_numbering + | Ibuiltin ef args res s => + add_unknown (kill_loads before) res | Icond cond args ifso ifnot => before | Ijumptable arg tbl => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 445c1af9..c5670e8d 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -232,7 +232,7 @@ Proof. apply wf_kill_loads; auto. apply wf_empty_numbering. apply wf_empty_numbering. -(* apply wf_add_unknown; auto. *) + apply wf_add_unknown. apply wf_kill_loads; auto. Qed. (** As a consequence, the numberings computed by the static analysis @@ -582,21 +582,16 @@ Proof. Qed. Lemma kill_load_satisfiable: - forall n rs chunk addr v m', - Mem.storev chunk m addr v = Some m' -> + forall n rs m', numbering_satisfiable ge sp rs m n -> numbering_satisfiable ge sp rs m' (kill_loads n). Proof. - intros. inversion H0. inversion H1. - generalize (kill_load_eqs_incl n.(num_eqs)). intro. + intros. inv H. destruct H0. generalize (kill_load_eqs_incl n.(num_eqs)). intro. exists x. split; intros. - generalize (H2 _ _ (H4 _ H5)). - generalize (kill_load_eqs_ops _ _ _ H5). - destruct rh; simpl. - intros. destruct addr; simpl in H; try discriminate. - auto. - tauto. - apply H3. assumption. + generalize (H _ _ (H1 _ H2)). + generalize (kill_load_eqs_ops _ _ _ H2). + destruct rh; simpl; tauto. + apply H0. auto. Qed. (** Correctness of [reg_valnum]: if it returns a register [r], @@ -902,7 +897,18 @@ Proof. econstructor; split. eapply exec_Itailcall; eauto. apply sig_preserved. - econstructor; eauto. + econstructor; eauto. + + (* Ibuiltin *) + econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + apply add_unknown_satisfiable. apply wf_kill_loads. apply wf_analyze. + eapply kill_load_satisfiable; eauto. (* Icond true *) econstructor; split. diff --git a/backend/Cminor.v b/backend/Cminor.v index bdfb379a..4e57d3ce 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -133,8 +133,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. (** * Operational semantics (small-step) *) diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 1e87419f..29f7178e 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -70,6 +70,7 @@ Inductive stmt : Type := | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt | Scall : option ident -> signature -> expr -> exprlist -> stmt | Stailcall: signature -> expr -> exprlist -> stmt + | Sbuiltin : option ident -> external_function -> exprlist -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -93,8 +94,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. (** * Operational semantics *) @@ -297,6 +298,12 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) m') + | step_builtin: forall f optid ef al k sp e m vl t v m', + eval_exprlist sp e m nil al vl -> + external_call ef ge vl m t v m' -> + step (State f (Sbuiltin optid ef al) k sp e m) + t (State f Sskip k sp (set_optvar optid v e) m') + | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) diff --git a/backend/Coloring.v b/backend/Coloring.v index 67824ae3..28626cba 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.v @@ -183,6 +183,8 @@ Definition add_edges_instr let largs := loc_arguments sig in add_prefs_call args largs (add_interf_call ros largs g) + | Ibuiltin ef args res s => + add_interf_op res live g | Ireturn (Some r) => add_pref_mreg r (loc_result sig) g | _ => g diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index d17229ea..63f21906 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -22,6 +22,7 @@ open Locations open RTL open RTLtyping open InterfGraph +open Conventions1 open Conventions (* George-Appel graph coloring *) @@ -202,13 +203,13 @@ let rec remove_reserved = function let init_regs() = caller_save_registers.(0) <- - Array.of_list (remove_reserved Conventions.int_caller_save_regs); + Array.of_list (remove_reserved int_caller_save_regs); caller_save_registers.(1) <- - Array.of_list (remove_reserved Conventions.float_caller_save_regs); + Array.of_list (remove_reserved float_caller_save_regs); callee_save_registers.(0) <- - Array.of_list (remove_reserved Conventions.int_callee_save_regs); + Array.of_list (remove_reserved int_callee_save_regs); callee_save_registers.(1) <- - Array.of_list (remove_reserved Conventions.float_callee_save_regs); + Array.of_list (remove_reserved float_callee_save_regs); for i = 0 to num_register_classes - 1 do num_available_registers.(i) <- Array.length caller_save_registers.(i) @@ -789,6 +790,7 @@ let spill_costs f = | Istore(chunk, addr, args, src, _) -> incr_list args; incr src | Icall(sg, ros, args, res, _) -> incr_ros ros; incr_list args; incr res | Itailcall(sg, ros, args) -> incr_ros ros; incr_list args + | Ibuiltin(ef, args, res, _) -> incr_list args; incr res | Icond(cond, args, _, _) -> incr_list args | Ijumptable(arg, _) -> incr arg | Ireturn(Some r) -> incr r diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index 92ac0676..5f035b40 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -384,6 +384,7 @@ Proof. apply add_interf_destroyed_incl. eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. apply add_interfs_call_incl. + apply add_interf_op_incl. destruct o. apply add_pref_mreg_incl. apply graph_incl_refl. @@ -433,6 +434,10 @@ Definition correct_interf_instr interfere_mreg rfun mr g | inr idfun => True end + | Ibuiltin ef args res s => + forall r, + Regset.In r live -> + r <> res -> interfere r res g | _ => True end. @@ -453,7 +458,8 @@ Proof. split. intros. eapply interfere_mreg_incl; eauto. split. intros. eapply interfere_incl; eauto. destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. - destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. + destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. + intros. eapply interfere_incl; eauto. Qed. Lemma add_edges_instr_correct: @@ -500,38 +506,9 @@ Proof. eapply interfere_mreg_incl. apply add_prefs_call_incl. apply add_interfs_call_correct. auto. -Qed. - -Lemma add_edges_instrs_incl_aux: - forall sig live instrs g, - graph_incl g - (fold_left - (fun (a : graph) (p : positive * instruction) => - add_edges_instr sig (snd p) live !! (fst p) a) - instrs g). -Proof. - induction instrs; simpl; intros. - apply graph_incl_refl. - eapply graph_incl_trans; [idtac|eauto]. - apply add_edges_instr_incl. -Qed. -Lemma add_edges_instrs_correct_aux: - forall sig live instrs g pc i, - In (pc, i) instrs -> - correct_interf_instr live!!pc i - (fold_left - (fun (a : graph) (p : positive * instruction) => - add_edges_instr sig (snd p) live !! (fst p) a) - instrs g). -Proof. - induction instrs; simpl; intros. - elim H. - elim H; intro. - subst a; simpl. eapply correct_interf_instr_incl. - apply add_edges_instrs_incl_aux. - apply add_edges_instr_correct. - auto. + (* Ibuiltin *) + intros. apply add_interf_op_correct; auto. Qed. Lemma add_edges_instrs_correct: @@ -539,11 +516,20 @@ Lemma add_edges_instrs_correct: f.(fn_code)!pc = Some i -> correct_interf_instr live!!pc i (add_edges_instrs f live). Proof. - intros. - unfold add_edges_instrs. - rewrite PTree.fold_spec. - apply add_edges_instrs_correct_aux. - apply PTree.elements_correct. auto. + intros f live. + set (P := fun (c: code) g => + forall pc i, c!pc = Some i -> correct_interf_instr live#pc i g). + set (F := (fun (g : graph) (pc0 : positive) (i0 : instruction) => + add_edges_instr (fn_sig f) i0 live # pc0 g)). + change (P f.(fn_code) (PTree.fold F f.(fn_code) empty_graph)). + apply PTree_Properties.fold_rec; unfold P; intros. + apply H0. rewrite H. auto. + rewrite PTree.gempty in H. congruence. + rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. unfold F. apply add_edges_instr_correct. + apply correct_interf_instr_incl with a. + unfold F; apply add_edges_instr_incl. + apply H1; auto. Qed. (** Here are the three correctness properties of the generated @@ -783,7 +769,7 @@ Definition correct_alloc_instr (forall r, Regset.In r live!!pc -> r <> res -> - ~(In (alloc r) Conventions.destroyed_at_call)) + ~(In (alloc r) destroyed_at_call)) /\ (forall r, Regset.In r live!!pc -> r <> res -> alloc r <> alloc res) @@ -796,6 +782,10 @@ Definition correct_alloc_instr | inl rfun => ~(In (alloc rfun) (loc_arguments sig)) | inr idfun => True end) + | Ibuiltin ef args res s => + forall r, + Regset.In r live!!pc -> + r <> res -> alloc r <> alloc res | _ => True end. @@ -877,14 +867,14 @@ Proof. generalize (ALL2 _ _ H2). contradiction. split. auto. destruct s0; auto. red; intros. - generalize (ALL3 r0). generalize (Conventions.loc_arguments_acceptable _ _ H). + generalize (ALL3 r0). generalize (loc_arguments_acceptable _ _ H). unfold loc_argument_acceptable, loc_acceptable. caseEq (alloc r0). intros. elim (ALL2 r0 m). apply C; auto. congruence. auto. destruct s0; auto. (* Itailcall *) destruct s0; auto. red; intros. - generalize (ALL3 r). generalize (Conventions.loc_arguments_acceptable _ _ H0). + generalize (ALL3 r). generalize (loc_arguments_acceptable _ _ H0). unfold loc_argument_acceptable, loc_acceptable. caseEq (alloc r). intros. elim (ALL2 r m). apply H; auto. congruence. auto. diff --git a/backend/Constprop.v b/backend/Constprop.v index e1ab2e9c..03966cdd 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -128,6 +128,8 @@ Definition transfer (f: function) (pc: node) (before: D.t) := D.set dst Unknown before | Icall sig ros args res s => D.set res Unknown before + | Ibuiltin ef args res s => + D.set res Unknown before | _ => before end diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 16f839fc..714468aa 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -355,6 +355,17 @@ Proof. eapply exec_Itailcall; eauto. apply sig_function_translated; auto. constructor; auto. + (* Ibuiltin *) + TransfInstr. intro. + exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split. + eapply exec_Ibuiltin; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. + eapply analyze_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. simpl; auto. + (* Icond, true *) exists (State s' (transf_function f) sp ifso rs m); split. caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); diff --git a/backend/LTL.v b/backend/LTL.v index a44f3fa4..e1222a52 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -41,6 +41,7 @@ Inductive instruction: Type := | Lstore: memory_chunk -> addressing -> list loc -> loc -> node -> instruction | Lcall: signature -> loc + ident -> list loc -> loc -> node -> instruction | Ltailcall: signature -> loc + ident -> list loc -> instruction + | Lbuiltin: external_function -> list loc -> loc -> node -> instruction | Lcond: condition -> list loc -> node -> node -> instruction | Ljumptable: loc -> list node -> instruction | Lreturn: option loc -> instruction. @@ -61,8 +62,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. (** * Operational semantics *) @@ -91,9 +92,9 @@ Definition postcall_locs (ls: locset) : locset := fun (l: loc) => match l with | R r => - if In_dec Loc.eq (R r) Conventions.temporaries then + if In_dec Loc.eq (R r) temporaries then Vundef - else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then + else if In_dec Loc.eq (R r) destroyed_at_call then Vundef else ls (R r) @@ -196,6 +197,12 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) pc rs m) E0 (Callstate s f' (List.map rs args) m') + | exec_Lbuiltin: + forall s f sp pc rs m ef args res pc' t v m', + (fn_code f)!pc = Some(Lbuiltin ef args res pc') -> + external_call ef ge (map rs args) m t v m' -> + step (State s f sp pc rs m) + t (State s f sp pc' (Locmap.set res v rs) m') | exec_Lcond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> @@ -272,6 +279,7 @@ Definition successors_instr (i: instruction) : list node := | Lstore chunk addr args src s => s :: nil | Lcall sig ros args res s => s :: nil | Ltailcall sig ros args => nil + | Lbuiltin ef args res s => s :: nil | Lcond cond args ifso ifnot => ifso :: ifnot :: nil | Ljumptable arg tbl => tbl | Lreturn optarg => nil diff --git a/backend/LTLin.v b/backend/LTLin.v index 806a7aa9..ee4cb943 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -47,6 +47,7 @@ Inductive instruction: Type := | Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction | Lcall: signature -> loc + ident -> list loc -> loc -> instruction | Ltailcall: signature -> loc + ident -> list loc -> instruction + | Lbuiltin: external_function -> list loc -> loc -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list loc -> label -> instruction @@ -68,8 +69,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. Definition genv := Genv.t fundef unit. @@ -186,6 +187,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m) E0 (Callstate s f' (List.map rs args) m') + | exec_Lbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge (map rs args) m t v m' -> + step (State s f sp (Lbuiltin ef args res :: b) rs m) + t (State s f sp b (Locmap.set res v rs) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 69422e0c..ad3ad644 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -67,8 +67,15 @@ Inductive wt_instr : instruction -> Prop := LTLtyping.call_loc_acceptable sig ros -> locs_acceptable args -> sig.(sig_res) = funsig.(sig_res) -> - Conventions.tailcall_possible sig -> + tailcall_possible sig -> wt_instr (Ltailcall sig ros args) + | wt_Lbuiltin: + forall ef args res, + List.map Loc.type args = (ef_sig ef).(sig_args) -> + Loc.type res = proj_sig_res (ef_sig ef) -> + arity_ok (ef_sig ef).(sig_args) = true -> + locs_acceptable args -> loc_acceptable res -> + wt_instr (Lbuiltin ef args res) | wt_Llabel: forall lbl, wt_instr (Llabel lbl) | wt_Lgoto: forall lbl, diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index e1e43f56..7afae2db 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -88,8 +88,16 @@ Inductive wt_instr : instruction -> Prop := call_loc_acceptable sig ros -> locs_acceptable args -> sig.(sig_res) = funct.(fn_sig).(sig_res) -> - Conventions.tailcall_possible sig -> + tailcall_possible sig -> wt_instr (Ltailcall sig ros args) + | wt_Lbuiltin: + forall ef args res s, + List.map Loc.type args = (ef_sig ef).(sig_args) -> + Loc.type res = proj_sig_res (ef_sig ef) -> + arity_ok (ef_sig ef).(sig_args) = true -> + locs_acceptable args -> loc_acceptable res -> + valid_successor s -> + wt_instr (Lbuiltin ef args res s) | wt_Lcond: forall cond args s1 s2, List.map Loc.type args = type_of_condition cond -> diff --git a/backend/Linear.v b/backend/Linear.v index 71310a97..0f44206d 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -43,6 +43,7 @@ Inductive instruction: Type := | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction + | Lbuiltin: external_function -> list mreg -> mreg -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -63,8 +64,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. Definition genv := Genv.t fundef unit. @@ -153,9 +154,9 @@ Definition return_regs (caller callee: locset) : locset := fun (l: loc) => match l with | R r => - if In_dec Loc.eq (R r) Conventions.temporaries then + if In_dec Loc.eq (R r) temporaries then callee (R r) - else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then + else if In_dec Loc.eq (R r) destroyed_at_call then callee (R r) else caller (R r) @@ -275,6 +276,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m) E0 (Callstate s f' (return_regs (parent_locset s) rs) m') + | exec_Lbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge (reglist rs args) m t v m' -> + step (State s f sp (Lbuiltin ef args res :: b) rs m) + t (State s f sp b (Locmap.set (R res) v rs) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -315,8 +321,8 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s ef args res rs1 rs2 m t m', external_call ef ge args m t res m' -> - args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) -> - rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 -> + args = List.map rs1 (loc_arguments (ef_sig ef)) -> + rs2 = Locmap.set (R (loc_result (ef_sig ef))) res rs1 -> step (Callstate s (External ef) rs1 m) t (Returnstate s rs2 m') | exec_return: @@ -337,7 +343,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs (R (Conventions.loc_result (mksignature nil (Some Tint)))) = Vint r -> + rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := diff --git a/backend/Linearize.v b/backend/Linearize.v index 31d0318c..fd350c71 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -185,6 +185,8 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code := Lcall sig ros args res :: add_branch s k | LTL.Ltailcall sig ros args => Ltailcall sig ros args :: k + | LTL.Lbuiltin ef args res s => + Lbuiltin ef args res :: add_branch s k | LTL.Lcond cond args s1 s2 => if starts_with s1 k then Lcond (negate_condition cond) args s2 :: add_branch s1 k diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 1f4e5fac..ce7788f4 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -94,6 +94,7 @@ let basic_blocks f joins = | Lstore (chunk, addr, args, src, s) -> next_in_block blk minpc s | Lcall (sig0, ros, args, res, s) -> next_in_block blk minpc s | Ltailcall (sig0, ros, args) -> end_block blk minpc + | Lbuiltin (ef, args, res, s) -> next_in_block blk minpc s | Lcond (cond, args, ifso, ifnot) -> end_block blk minpc; start_block ifso; start_block ifnot | Ljumptable(arg, tbl) -> diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 5f0a2a4e..df750008 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -612,6 +612,23 @@ Proof. destruct (Genv.find_symbol ge i); try discriminate. eapply Genv.find_funct_ptr_prop; eauto. + (* Lbuiltin *) + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!pc' = true). + eapply reachable_successors; eauto. simpl; auto. + exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + econstructor; split. + eapply plus_left'. + eapply exec_Lbuiltin. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + eapply add_branch_correct; eauto. + eapply is_tail_add_branch. eapply is_tail_cons_left. + eapply is_tail_find_label. eauto. + traceEq. + econstructor; eauto. + (* Lcond true *) destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index 716b66f1..7393535d 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -55,6 +55,7 @@ Proof. apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. apply wt_add_instr. constructor; auto. auto. + apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. destruct (starts_with s1 k); apply wt_add_instr. constructor; auto. rewrite H. destruct cond; auto. apply wt_add_branch; auto. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 028e1200..4ea2ea95 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -87,6 +87,12 @@ Inductive wt_instr : instruction -> Prop := tailcall_possible sig -> match ros with inl r => r = IT1 | _ => True end -> wt_instr (Ltailcall sig ros) + | wt_Lbuiltin: + forall ef args res, + List.map mreg_type args = (ef_sig ef).(sig_args) -> + mreg_type res = proj_sig_res (ef_sig ef) -> + arity_ok (ef_sig ef).(sig_args) = true -> + wt_instr (Lbuiltin ef args res) | wt_Llabel: forall lbl, wt_instr (Llabel lbl) diff --git a/backend/Locations.v b/backend/Locations.v index 295df281..c2fda9c2 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -173,6 +173,18 @@ Module Loc. destruct s; destruct s0; intuition auto. Qed. + Lemma diff_reg_right: + forall l r, l <> R r -> diff (R r) l. + Proof. + intros. simpl. destruct l. congruence. auto. + Qed. + + Lemma diff_reg_left: + forall l r, l <> R r -> diff l (R r). + Proof. + intros. apply diff_sym. apply diff_reg_right. auto. + Qed. + (** [Loc.overlap l1 l2] returns [false] if [l1] and [l2] are different and non-overlapping, and [true] otherwise: either [l1 = l2] or they partially overlap. *) @@ -290,6 +302,14 @@ Module Loc. auto. Qed. + Lemma reg_notin: + forall r ll, ~(In (R r) ll) -> notin (R r) ll. + Proof. + induction ll; simpl; intros. auto. + split. destruct a; auto. intuition congruence. + apply IHll. intuition. + Qed. + (** [Loc.disjoint l1 l2] is true if the locations in list [l1] are different from all locations in list [l2]. *) @@ -352,6 +372,9 @@ Module Loc. | norepet_cons: forall hd tl, notin hd tl -> norepet tl -> norepet (hd :: tl). +(** [Loc.no_overlap l1 l2] holds if elements of [l1] never overlap partially + with elements of [l2]. *) + Definition no_overlap (l1 l2 : list loc) := forall r, In r l1 -> forall s, In s l2 -> r = s \/ Loc.diff r s. diff --git a/backend/Mach.v b/backend/Mach.v index e89ff3b1..2ec312e4 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -58,6 +58,7 @@ Inductive instruction: Type := | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Mcall: signature -> mreg + ident -> instruction | Mtailcall: signature -> mreg + ident -> instruction + | Mbuiltin: external_function -> list mreg -> mreg -> instruction | Mlabel: label -> instruction | Mgoto: label -> instruction | Mcond: condition -> list mreg -> label -> instruction @@ -80,8 +81,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. Definition genv := Genv.t fundef unit. diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 060c6c2b..291a4682 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -24,7 +24,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Op. Require Import Locations. -Require Conventions. +Require Import Conventions. Require Import Mach. Require Stacklayout. @@ -148,7 +148,7 @@ Inductive extcall_args: regset -> frame -> list loc -> list val -> Prop := Definition extcall_arguments (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop := - extcall_args rs fr (Conventions.loc_arguments sg) args. + extcall_args rs fr (loc_arguments sg) args. End FRAME_ACCESSES. @@ -267,6 +267,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m) E0 (Callstate s f' rs m') + | exec_Mbuiltin: + forall s f sp rs fr m ef args res b t v m', + external_call ef ge rs##args m t v m' -> + step (State s f sp (Mbuiltin ef args res :: b) rs fr m) + t (State s f sp b (rs#res <- v) fr m') | exec_Mgoto: forall s f sp lbl c rs fr m c', find_label lbl f.(fn_code) = Some c' -> @@ -304,8 +309,8 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s ef args res rs1 rs2 m t m', external_call ef ge args m t res m' -> - extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args -> - rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> + extcall_arguments (parent_function s) rs1 (parent_frame s) (ef_sig ef) args -> + rs2 = (rs1#(loc_result (ef_sig ef)) <- res) -> step (Callstate s (External ef) rs1 m) t (Returnstate s rs2 m') | exec_return: @@ -325,7 +330,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs (Conventions.loc_result (mksignature nil (Some Tint))) = Vint r -> + rs (loc_result (mksignature nil (Some Tint))) = Vint r -> final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 125cd57a..1a97dda5 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -28,6 +28,7 @@ Require Import Mach. Require Import Machtyping. Require Import Machabstr. Require Import Machconcr. +Require Import Conventions. Require Import Asmgenretaddr. (** Two semantics were defined for the Mach intermediate language: @@ -911,7 +912,7 @@ Lemma transl_extcall_arguments: /\ Val.lessdef_list args targs. Proof. unfold Machabstr.extcall_arguments, extcall_arguments; intros. - generalize (Conventions.loc_arguments sg) args H. + generalize (loc_arguments sg) args H. induction l; intros; inv H2. exists (@nil val); split; constructor. exploit IHl; eauto. intros [targs [A B]]. @@ -1023,6 +1024,16 @@ Proof. eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto. econstructor; eauto. eapply match_stacks_free; eauto. + (* Mbuiltin *) + exploit external_call_mem_extends; eauto. eapply regset_lessdef_list; eauto. + intros [v' [ms' [A [B [C D]]]]]. + econstructor; split. + eapply exec_Mbuiltin. eauto. + econstructor; eauto with coqlib. + eapply match_stacks_external_call; eauto. + eapply frame_match_external_call; eauto. + apply regset_lessdef_set; eauto. + (* Mgoto *) econstructor; split. eapply exec_Mgoto; eauto. @@ -1104,7 +1115,7 @@ Lemma equiv_final_states: Proof. intros. inv H0. destruct H. inv H. inv STACKS. constructor. - generalize (RLD (Conventions.loc_result (mksignature nil (Some Tint)))). + generalize (RLD (loc_result (mksignature nil (Some Tint)))). rewrite H1. intro LD. inv LD. auto. Qed. diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 5b63fa8f..b736c8f7 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -23,7 +23,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Op. Require Import Locations. -Require Conventions. +Require Import Conventions. Require Import Mach. Require Stacklayout. Require Asmgenretaddr. @@ -82,7 +82,7 @@ Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop := Definition extcall_arguments (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := - extcall_args rs m sp (Conventions.loc_arguments sg) args. + extcall_args rs m sp (loc_arguments sg) args. (** Mach execution states. *) @@ -187,6 +187,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) E0 (Callstate s f' rs m') + | exec_Mbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge rs##args m t v m' -> + step (State s f sp (Mbuiltin ef args res :: b) rs m) + t (State s f sp b (rs#res <- v) m') | exec_Mgoto: forall s fb f sp lbl c rs m c', Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -234,8 +239,8 @@ Inductive step: state -> trace -> state -> Prop := forall s fb rs m t rs' ef args res m', Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef ge args m t res m' -> - extcall_arguments rs m (parent_sp s) ef.(ef_sig) args -> - rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) -> + extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> + rs' = (rs#(loc_result (ef_sig ef)) <- res) -> step (Callstate s fb rs m) t (Returnstate s rs' m') | exec_return: @@ -254,7 +259,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs (Conventions.loc_result (mksignature nil (Some Tint))) = Vint r -> + rs (loc_result (mksignature nil (Some Tint))) = Vint r -> final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := diff --git a/backend/Machtyping.v b/backend/Machtyping.v index b0673ca8..7013e296 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -23,7 +23,7 @@ Require Import Events. Require Import Globalenvs. Require Import Op. Require Import Locations. -Require Conventions. +Require Import Conventions. Require Import Mach. (** * Typing rules *) @@ -69,9 +69,14 @@ Inductive wt_instr : instruction -> Prop := wt_instr (Mcall sig ros) | wt_Mtailcall: forall sig ros, - Conventions.tailcall_possible sig -> + tailcall_possible sig -> match ros with inl r => mreg_type r = Tint | inr s => True end -> wt_instr (Mtailcall sig ros) + | wt_Mbuiltin: + forall ef args res, + List.map mreg_type args = (ef_sig ef).(sig_args) -> + mreg_type res = proj_sig_res (ef_sig ef) -> + wt_instr (Mbuiltin ef args res) | wt_Mgoto: forall lbl, wt_instr (Mgoto lbl) @@ -273,7 +278,7 @@ Proof. apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H). econstructor; eauto. -(* apply wt_setreg; auto. exact I. *) + inv H0. apply wt_setreg; auto. rewrite H5. eapply external_call_well_typed; eauto. apply is_tail_find_label with lbl; congruence. apply is_tail_find_label with lbl; congruence. @@ -286,7 +291,7 @@ Proof. econstructor; eauto. apply wt_setreg; auto. generalize (external_call_well_typed _ _ _ _ _ _ _ H). - unfold proj_sig_res, Conventions.loc_result. + unfold proj_sig_res, loc_result. destruct (sig_res (ef_sig ef)). destruct t0; simpl; auto. simpl; auto. diff --git a/backend/RTL.v b/backend/RTL.v index a17c74ee..1c309a0c 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -70,6 +70,10 @@ Inductive instruction: Type := | Itailcall: signature -> reg + ident -> list reg -> instruction (** [Itailcall sig fn args] performs a function invocation in tail-call position. *) + | Ibuiltin: external_function -> list reg -> reg -> node -> instruction + (** [Ibuiltin ef args dest succ] calls the built-in function + identified by [ef], giving it the values of [args] as arguments. + It stores the return value in [dest] and branches to [succ]. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -109,8 +113,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. (** * Operational semantics *) @@ -245,6 +249,12 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) pc rs m) E0 (Callstate s fd rs##args m') + | exec_Ibuiltin: + forall s f sp pc rs m ef args res pc' t v m', + (fn_code f)!pc = Some(Ibuiltin ef args res pc') -> + external_call ef ge rs##args m t v m' -> + step (State s f sp pc rs m) + t (State s f sp pc' (rs#res <- v) m') | exec_Icond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> @@ -351,6 +361,7 @@ Definition successors_instr (i: instruction) : list node := | Istore chunk addr args src s => s :: nil | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil + | Ibuiltin ef args res s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ijumptable arg tbl => tbl | Ireturn optarg => nil diff --git a/backend/RTLgen.v b/backend/RTLgen.v index ff4f81c5..aec2c867 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -546,6 +546,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do n1 <- add_instr (Itailcall sig (inl _ rf) rargs); do n2 <- transl_exprlist map cl rargs n1; transl_expr map b rf n2 + | Sbuiltin optid ef al => + do rargs <- alloc_regs map al; + do r <- new_reg; + do n1 <- store_optvar map r optid nd; + do n2 <- add_instr (Ibuiltin ef rargs r n1); + transl_exprlist map al rargs n2 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index a96dfbfd..a1bd6618 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1213,6 +1213,22 @@ Proof. rewrite H2; eauto. traceEq. rewrite G. constructor; auto. + + (* builtin *) + inv TS. + exploit transl_exprlist_correct; eauto. + intros [rs' [E [F [G J]]]]. + exploit tr_store_optvar_correct. eauto. eauto. + apply match_env_update_temp. eexact F. eauto. + intros [rs'' [A B]]. + econstructor; split. + left. eapply star_plus_trans. eexact E. eapply plus_left. + eapply exec_Ibuiltin. eauto. rewrite G. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + eexact A. reflexivity. traceEq. + econstructor; eauto. constructor. rewrite Regmap.gss in B. auto. + (* seq *) inv TS. econstructor; split. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 5690bb29..0b18a99b 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -816,6 +816,12 @@ Inductive tr_stmt (c: code) (map: mapping): tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Itailcall sig (inl _ rf) rargs) -> tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret + | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 n2 rargs, + tr_exprlist c map nil al ns n1 rargs -> + c!n1 = Some (Ibuiltin ef rargs rd n2) -> + tr_store_optvar c map rd optid n2 nd -> + ~reg_in_map map rd -> + tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> @@ -1228,6 +1234,11 @@ Proof. eapply transl_expr_charact; eauto 3 with rtlg. apply tr_exprlist_incr with s4; auto. eapply transl_exprlist_charact; eauto 4 with rtlg. + (* Sbuiltin *) + econstructor; eauto 4 with rtlg. + eapply transl_exprlist_charact; eauto 3 with rtlg. + apply tr_store_optvar_incr with s2; auto. + eapply store_optvar_charact; eauto with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 68f38c0d..533c47a9 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -25,7 +25,7 @@ Require Import Integers. Require Import Events. Require Import Smallstep. Require Import RTL. -Require Conventions. +Require Import Conventions. (** * The type system *) @@ -104,8 +104,15 @@ Inductive wt_instr : instruction -> Prop := match ros with inl r => env r = Tint | inr s => True end -> sig.(sig_res) = funct.(fn_sig).(sig_res) -> List.map env args = sig.(sig_args) -> - Conventions.tailcall_possible sig -> + tailcall_possible sig -> wt_instr (Itailcall sig ros args) + | wt_Ibuiltin: + forall ef args res s, + List.map env args = (ef_sig ef).(sig_args) -> + env res = proj_sig_res (ef_sig ef) -> + arity_ok (ef_sig ef).(sig_args) = true -> + valid_successor s -> + wt_instr (Ibuiltin ef args res s) | wt_Icond: forall cond args s1 s2, List.map env args = type_of_condition cond -> @@ -225,7 +232,12 @@ Definition check_instr (i: instruction) : bool := match ros with inl r => check_reg r Tint | inr s => true end && check_regs args sig.(sig_args) && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res) - && Conventions.tailcall_is_possible sig + && tailcall_is_possible sig + | Ibuiltin ef args res s => + check_regs args (ef_sig ef).(sig_args) + && check_reg res (proj_sig_res (ef_sig ef)) + && arity_ok (ef_sig ef).(sig_args) + && check_successor s | Icond cond args s1 s2 => check_regs args (type_of_condition cond) && check_successor s1 @@ -331,7 +343,13 @@ Proof. destruct s0; auto. apply check_reg_correct; auto. eapply proj_sumbool_true; eauto. apply check_regs_correct; auto. - apply Conventions.tailcall_is_possible_correct; auto. + apply tailcall_is_possible_correct; auto. + (* builtin *) + constructor. + apply check_regs_correct; auto. + apply check_reg_correct; auto. + auto. + apply check_successor_correct; auto. (* cond *) constructor. apply check_regs_correct; auto. apply check_successor_correct; auto. @@ -541,6 +559,10 @@ Proof. econstructor; eauto. rewrite H6; auto. rewrite <- H7. apply wt_regset_list. auto. + (* Ibuiltin *) + econstructor; eauto. + apply wt_regset_assign. auto. + rewrite H6. eapply external_call_well_typed; eauto. (* Icond *) econstructor; eauto. econstructor; eauto. diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index 868fb8df..657c4daa 100644 --- a/backend/RTLtypingaux.ml +++ b/backend/RTLtypingaux.ml @@ -86,6 +86,17 @@ let type_instr retty (Coq_pair(pc, i)) = raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s" name msg)) end + | Ibuiltin(ef, args, res, _) -> + begin try + let sg = ef_sig ef in + set_types args sg.sig_args; + set_type res (match sg.sig_res with None -> Tint | Some ty -> ty); + if not (Conventions.arity_ok sg.sig_args) then + raise(Type_error "wrong arity") + with Type_error msg -> + raise(Type_error (Printf.sprintf "type mismatch in Ibuiltin(%s): %s" + (extern_atom ef.ef_id) msg)) + end | Icond(cond, args, _, _) -> set_types args (type_of_condition cond) | Ijumptable(arg, _) -> diff --git a/backend/Reload.v b/backend/Reload.v index 5728a628..81b61998 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -235,6 +235,11 @@ Definition transf_instr parallel_move args largs (Ltailcall sig (inr _ id) :: k) end + | LTLin.Lbuiltin ef args dst => + let rargs := regs_for args in + let rdst := reg_for dst in + add_reloads args rargs + (Lbuiltin ef rargs rdst :: add_spill rdst dst k) | LTLin.Llabel lbl => Llabel lbl :: k | LTLin.Lgoto lbl => diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 155f7b1b..286a266d 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -25,6 +25,7 @@ Require Import Op. Require Import Locations. Require Import Conventions. Require Import Allocproof. +Require Import RTLtyping. Require Import LTLin. Require Import LTLintyping. Require Import Linear. @@ -33,33 +34,10 @@ Require Import Reload. (** * Exploitation of the typing hypothesis *) -(** Reloading is applied to LTLin code that is well-typed in - the sense of [LTLintyping]. We exploit this hypothesis to obtain information on - the number of temporaries required for reloading the arguments. *) - -Fixpoint temporaries_ok_rec (tys: list typ) (itmps ftmps: list mreg) - {struct tys} : bool := - match tys with - | nil => true - | Tint :: ts => - match itmps with - | nil => false - | it1 :: its => temporaries_ok_rec ts its ftmps - end - | Tfloat :: ts => - match ftmps with - | nil => false - | ft1 :: fts => temporaries_ok_rec ts itmps fts - end - end. - -Definition temporaries_ok (tys: list typ) := - temporaries_ok_rec tys int_temporaries float_temporaries. - -Remark temporaries_ok_rec_incr_1: +Remark arity_ok_rec_incr_1: forall tys it itmps ftmps, - temporaries_ok_rec tys itmps ftmps = true -> - temporaries_ok_rec tys (it :: itmps) ftmps = true. + arity_ok_rec tys itmps ftmps = true -> + arity_ok_rec tys (it :: itmps) ftmps = true. Proof. induction tys; intros until ftmps; simpl. tauto. @@ -68,10 +46,10 @@ Proof. destruct ftmps. congruence. auto. Qed. -Remark temporaries_ok_rec_incr_2: +Remark arity_ok_rec_incr_2: forall tys ft itmps ftmps, - temporaries_ok_rec tys itmps ftmps = true -> - temporaries_ok_rec tys itmps (ft :: ftmps) = true. + arity_ok_rec tys itmps ftmps = true -> + arity_ok_rec tys itmps (ft :: ftmps) = true. Proof. induction tys; intros until ftmps; simpl. tauto. @@ -80,37 +58,37 @@ Proof. destruct ftmps. congruence. auto. Qed. -Remark temporaries_ok_rec_decr: +Remark arity_ok_rec_decr: forall tys ty itmps ftmps, - temporaries_ok_rec (ty :: tys) itmps ftmps = true -> - temporaries_ok_rec tys itmps ftmps = true. + arity_ok_rec (ty :: tys) itmps ftmps = true -> + arity_ok_rec tys itmps ftmps = true. Proof. intros until ftmps. simpl. destruct ty. - destruct itmps. congruence. intros. apply temporaries_ok_rec_incr_1; auto. - destruct ftmps. congruence. intros. apply temporaries_ok_rec_incr_2; auto. + destruct itmps. congruence. intros. apply arity_ok_rec_incr_1; auto. + destruct ftmps. congruence. intros. apply arity_ok_rec_incr_2; auto. Qed. -Lemma temporaries_ok_enough_rec: +Lemma arity_ok_enough_rec: forall locs itmps ftmps, - temporaries_ok_rec (List.map Loc.type locs) itmps ftmps = true -> + arity_ok_rec (List.map Loc.type locs) itmps ftmps = true -> enough_temporaries_rec locs itmps ftmps = true. Proof. induction locs; intros until ftmps. simpl. auto. simpl enough_temporaries_rec. simpl map. - destruct a. intros. apply IHlocs. eapply temporaries_ok_rec_decr; eauto. + destruct a. intros. apply IHlocs. eapply arity_ok_rec_decr; eauto. simpl. destruct (slot_type s). destruct itmps; auto. destruct ftmps; auto. Qed. -Lemma temporaries_ok_enough: +Lemma arity_ok_enough: forall locs, - temporaries_ok (List.map Loc.type locs) = true -> + arity_ok (List.map Loc.type locs) = true -> enough_temporaries locs = true. Proof. - unfold temporaries_ok, enough_temporaries. intros. - apply temporaries_ok_enough_rec; auto. + unfold arity_ok, enough_temporaries. intros. + apply arity_ok_enough_rec; auto. Qed. Lemma enough_temporaries_op_args: @@ -118,7 +96,7 @@ Lemma enough_temporaries_op_args: (List.map Loc.type args, Loc.type res) = type_of_operation op -> enough_temporaries args = true. Proof. - intros. apply temporaries_ok_enough. + intros. apply arity_ok_enough. replace (map Loc.type args) with (fst (type_of_operation op)). destruct op; try (destruct c); compute; reflexivity. rewrite <- H. auto. @@ -129,7 +107,7 @@ Lemma enough_temporaries_cond: List.map Loc.type args = type_of_condition cond -> enough_temporaries args = true. Proof. - intros. apply temporaries_ok_enough. rewrite H. + intros. apply arity_ok_enough. rewrite H. destruct cond; compute; reflexivity. Qed. @@ -138,15 +116,15 @@ Lemma enough_temporaries_addr: List.map Loc.type args = type_of_addressing addr -> enough_temporaries args = true. Proof. - intros. apply temporaries_ok_enough. rewrite H. + intros. apply arity_ok_enough. rewrite H. destruct addr; compute; reflexivity. Qed. -Lemma temporaries_ok_rec_length: +Lemma arity_ok_rec_length: forall tys itmps ftmps, (length tys <= length itmps)%nat -> (length tys <= length ftmps)%nat -> - temporaries_ok_rec tys itmps ftmps = true. + arity_ok_rec tys itmps ftmps = true. Proof. induction tys; intros until ftmps; simpl. auto. @@ -159,8 +137,8 @@ Lemma enough_temporaries_length: forall args, (length args <= 2)%nat -> enough_temporaries args = true. Proof. - intros. apply temporaries_ok_enough. unfold temporaries_ok. - apply temporaries_ok_rec_length. + intros. apply arity_ok_enough. unfold arity_ok. + apply arity_ok_rec_length. rewrite list_length_map. simpl. omega. rewrite list_length_map. simpl. omega. Qed. @@ -690,7 +668,7 @@ Proof. intros. unfold return_regs. destruct (In_dec Loc.eq (R (loc_result sig)) temporaries). auto. destruct (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call). auto. - elim n0. apply loc_result_caller_save. + generalize (loc_result_caller_save sig). tauto. Qed. (** * Preservation of labels and gotos *) @@ -885,7 +863,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop := | match_states_call: forall s f args m s' ls tm (STACKS: match_stackframes s s' (LTLin.funsig f)) - (AG: Val.lessdef_list args (map ls (Conventions.loc_arguments (LTLin.funsig f)))) + (AG: Val.lessdef_list args (map ls (loc_arguments (LTLin.funsig f)))) (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call -> ls l = parent_locset s' l) (WT: wt_fundef f) @@ -895,7 +873,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop := | match_states_return: forall s res m s' ls tm sig (STACKS: match_stackframes s s' sig) - (AG: Val.lessdef res (ls (R (Conventions.loc_result sig)))) + (AG: Val.lessdef res (ls (R (loc_result sig)))) (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call -> ls l = parent_locset s' l) (MMD: Mem.extends m tm), @@ -1216,6 +1194,29 @@ Proof. rewrite return_regs_arguments; auto. congruence. exact (return_regs_preserve (parent_locset s') ls3). + (* Lbuiltin *) + ExploitWT; inv WTI. + exploit add_reloads_correct. + instantiate (1 := args). apply arity_ok_enough. rewrite H3. auto. + apply locs_acceptable_disj_temporaries; auto. + intros [ls2 [A [B C]]]. + exploit external_call_mem_extends; eauto. + apply agree_locs; eauto. + intros [v' [tm' [P [Q [R S]]]]]. + exploit add_spill_correct. + intros [ls3 [D [E F]]]. + left; econstructor; split. + eapply star_plus_trans. eauto. + eapply plus_left. eapply exec_Lbuiltin. rewrite B. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + eauto. reflexivity. traceEq. + econstructor; eauto with coqlib. + apply agree_set with ls; auto. + rewrite E. rewrite Locmap.gss. auto. + intros. rewrite F; auto. rewrite Locmap.gso. auto. + apply reg_for_diff; auto. + (* Llabel *) left; econstructor; split. apply plus_one. apply exec_Llabel. @@ -1319,7 +1320,8 @@ Proof. econstructor; eauto. simpl. rewrite Locmap.gss. auto. intros. rewrite Locmap.gso. auto. - simpl. destruct l; auto. red; intro. elim H1. subst m0. apply loc_result_caller_save. + simpl. destruct l; auto. red; intro. elim H1. subst m0. + generalize (loc_result_caller_save (ef_sig ef)). tauto. (* return *) inv STACKS. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index df0715ee..1bb462dc 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -34,7 +34,7 @@ Require Import Reloadproof. given sufficient typing and well-formedness hypotheses over the locations involved. *) Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove - wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall + wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lbuiltin wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty. Remark wt_code_cons: @@ -292,6 +292,13 @@ Proof. auto 10 with reloadty. assert (map mreg_type (regs_for args) = map Loc.type args). + apply wt_regs_for. apply arity_ok_enough. congruence. + assert (mreg_type (reg_for res) = Loc.type res). eauto with reloadty. + auto with reloadty. + + + + assert (map mreg_type (regs_for args) = map Loc.type args). eauto with reloadty. auto with reloadty. diff --git a/backend/Selection.v b/backend/Selection.v index e822fdf7..ebdad8a2 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -167,46 +167,73 @@ Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist := | a :: bl => Econs (sel_expr a) (sel_exprlist bl) end. +(** Recognition of calls to built-in functions that should be inlined *) + +Definition expr_is_addrof_ident (e: Cminor.expr) : option ident := + match e with + | Cminor.Econst (Cminor.Oaddrsymbol id ofs) => + if Int.eq ofs Int.zero then Some id else None + | _ => None + end. + +Definition expr_is_addrof_builtin (ge: Cminor.genv) (e: Cminor.expr) : option external_function := + match expr_is_addrof_ident e with + | None => None + | Some id => + match Genv.find_symbol ge id with + | None => None + | Some b => + match Genv.find_funct_ptr ge b with + | Some(External ef) => if ef.(ef_inline) then Some ef else None + | _ => None + end + end + end. + (** Conversion from Cminor statements to Cminorsel statements. *) -Fixpoint sel_stmt (s: Cminor.stmt) : stmt := +Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt := match s with | Cminor.Sskip => Sskip | Cminor.Sassign id e => Sassign id (sel_expr e) | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs) | Cminor.Scall optid sg fn args => - Scall optid sg (sel_expr fn) (sel_exprlist args) + match expr_is_addrof_builtin ge fn with + | None => Scall optid sg (sel_expr fn) (sel_exprlist args) + | Some ef => Sbuiltin optid ef (sel_exprlist args) + end | Cminor.Stailcall sg fn args => Stailcall sg (sel_expr fn) (sel_exprlist args) - | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) + | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2) | Cminor.Sifthenelse e ifso ifnot => Sifthenelse (condexpr_of_expr (sel_expr e)) - (sel_stmt ifso) (sel_stmt ifnot) - | Cminor.Sloop body => Sloop (sel_stmt body) - | Cminor.Sblock body => Sblock (sel_stmt body) + (sel_stmt ge ifso) (sel_stmt ge ifnot) + | Cminor.Sloop body => Sloop (sel_stmt ge body) + | Cminor.Sblock body => Sblock (sel_stmt ge body) | Cminor.Sexit n => Sexit n | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl | Cminor.Sreturn None => Sreturn None | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e)) - | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body) + | Cminor.Slabel lbl body => Slabel lbl (sel_stmt ge body) | Cminor.Sgoto lbl => Sgoto lbl end. (** Conversion of functions and programs. *) -Definition sel_function (f: Cminor.function) : function := +Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : function := mkfunction f.(Cminor.fn_sig) f.(Cminor.fn_params) f.(Cminor.fn_vars) f.(Cminor.fn_stackspace) - (sel_stmt f.(Cminor.fn_body)). + (sel_stmt ge f.(Cminor.fn_body)). -Definition sel_fundef (f: Cminor.fundef) : fundef := - transf_fundef sel_function f. +Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : fundef := + transf_fundef (sel_function ge) f. Definition sel_program (p: Cminor.program) : program := - transform_program sel_fundef p. + let ge := Genv.globalenv p in + transform_program (sel_fundef ge) p. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index e03085a9..cb9f4fc5 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -275,6 +275,36 @@ Qed. End CMCONSTR. +(** Recognition of calls to built-in functions *) + +Lemma expr_is_addrof_ident_correct: + forall e id, + expr_is_addrof_ident e = Some id -> + e = Cminor.Econst (Cminor.Oaddrsymbol id Int.zero). +Proof. + intros e id. unfold expr_is_addrof_ident. + destruct e; try congruence. + destruct c; try congruence. + predSpec Int.eq Int.eq_spec i0 Int.zero; congruence. +Qed. + +Lemma expr_is_addrof_builtin_correct: + forall ge sp e m a v ef fd, + expr_is_addrof_builtin ge a = Some ef -> + Cminor.eval_expr ge sp e m a v -> + Genv.find_funct ge v = Some fd -> + fd = External ef. +Proof. + intros until fd; unfold expr_is_addrof_builtin. + case_eq (expr_is_addrof_ident a); intros; try congruence. + exploit expr_is_addrof_ident_correct; eauto. intro EQ; subst a. + inv H1. inv H4. + destruct (Genv.find_symbol ge i); try congruence. + inv H3. rewrite Genv.find_funct_find_funct_ptr in H2. rewrite H2 in H0. + destruct fd; try congruence. + destruct (ef_inline e0); congruence. +Qed. + (** * Semantic preservation for instruction selection. *) Section PRESERVATION. @@ -297,24 +327,24 @@ Qed. Lemma functions_translated: forall (v: val) (f: Cminor.fundef), Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (sel_fundef f). + Genv.find_funct tge v = Some (sel_fundef ge f). Proof. intros. - exact (Genv.find_funct_transf sel_fundef _ _ H). + exact (Genv.find_funct_transf (sel_fundef ge) _ _ H). Qed. Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (sel_fundef f). + Genv.find_funct_ptr tge b = Some (sel_fundef ge f). Proof. intros. - exact (Genv.find_funct_ptr_transf sel_fundef _ _ H). + exact (Genv.find_funct_ptr_transf (sel_fundef ge) _ _ H). Qed. Lemma sig_function_translated: forall f, - funsig (sel_fundef f) = Cminor.funsig f. + funsig (sel_fundef ge f) = Cminor.funsig f. Proof. intros. destruct f; reflexivity. Qed. @@ -369,29 +399,40 @@ Hint Resolve sel_exprlist_correct: evalexpr. Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont := match k with | Cminor.Kstop => Kstop - | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1) + | Cminor.Kseq s1 k1 => Kseq (sel_stmt ge s1) (sel_cont k1) | Cminor.Kblock k1 => Kblock (sel_cont k1) | Cminor.Kcall id f sp e k1 => - Kcall id (sel_function f) sp e (sel_cont k1) + Kcall id (sel_function ge f) sp e (sel_cont k1) end. Inductive match_states: Cminor.state -> CminorSel.state -> Prop := | match_state: forall f s k s' k' sp e m, - s' = sel_stmt s -> + s' = sel_stmt ge s -> k' = sel_cont k -> match_states (Cminor.State f s k sp e m) - (State (sel_function f) s' k' sp e m) + (State (sel_function ge f) s' k' sp e m) | match_callstate: forall f args k k' m, k' = sel_cont k -> match_states (Cminor.Callstate f args k m) - (Callstate (sel_fundef f) args k' m) + (Callstate (sel_fundef ge f) args k' m) | match_returnstate: forall v k k' m, k' = sel_cont k -> match_states (Cminor.Returnstate v k m) - (Returnstate v k' m). + (Returnstate v k' m) + | match_builtin_1: forall ef args optid f sp e k m al k', + k' = sel_cont k -> + eval_exprlist tge sp e m nil al args -> + match_states + (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) + (State (sel_function ge f) (Sbuiltin optid ef al) k' sp e m) + | match_builtin_2: forall v optid f sp e k m k', + k' = sel_cont k -> + match_states + (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m) + (State (sel_function ge f) Sskip k' sp (set_optvar optid v e) m). Remark call_cont_commut: forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k). @@ -401,19 +442,20 @@ Qed. Remark find_label_commut: forall lbl s k, - find_label lbl (sel_stmt s) (sel_cont k) = - option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk))) + find_label lbl (sel_stmt ge s) (sel_cont k) = + option_map (fun sk => (sel_stmt ge (fst sk), sel_cont (snd sk))) (Cminor.find_label lbl s k). Proof. induction s; intros; simpl; auto. unfold store. destruct (addressing m (sel_expr e)); auto. - change (Kseq (sel_stmt s2) (sel_cont k)) + destruct (expr_is_addrof_builtin ge e); auto. + change (Kseq (sel_stmt ge s2) (sel_cont k)) with (sel_cont (Cminor.Kseq s2 k)). rewrite IHs1. rewrite IHs2. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto. rewrite IHs1. rewrite IHs2. destruct (Cminor.find_label lbl s1 k); auto. - change (Kseq (Sloop (sel_stmt s)) (sel_cont k)) + change (Kseq (Sloop (sel_stmt ge s)) (sel_cont k)) with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)). auto. change (Kblock (sel_cont k)) @@ -423,64 +465,79 @@ Proof. destruct (ident_eq lbl l); auto. Qed. +Definition measure (s: Cminor.state) : nat := + match s with + | Cminor.Callstate _ _ _ _ => 0%nat + | Cminor.State _ _ _ _ _ _ => 1%nat + | Cminor.Returnstate _ _ _ => 2%nat + end. + Lemma sel_step_correct: forall S1 t S2, Cminor.step ge S1 t S2 -> forall T1, match_states S1 T1 -> - exists T2, step tge T1 t T2 /\ match_states S2 T2. + (exists T2, step tge T1 t T2 /\ match_states S2 T2) + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat. Proof. induction 1; intros T1 ME; inv ME; simpl; - try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). + try (left; econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). (* skip call *) - econstructor; split. + left; econstructor; split. econstructor. destruct k; simpl in H; simpl; auto. rewrite <- H0; reflexivity. simpl. eauto. constructor; auto. -(* - (* assign *) - exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split. - constructor. auto with evalexpr. - constructor; auto. -*) (* store *) - econstructor; split. + left; econstructor; split. eapply eval_store; eauto with evalexpr. constructor; auto. (* Scall *) - econstructor; split. + case_eq (expr_is_addrof_builtin ge a). + (* Scall turned into Sbuiltin *) + intros ef EQ. exploit expr_is_addrof_builtin_correct; eauto. intro EQ1. subst fd. + right; split. omega. split. auto. + econstructor; eauto with evalexpr. + (* Scall preserved *) + intro EQ. left; econstructor; split. econstructor; eauto with evalexpr. apply functions_translated; eauto. apply sig_function_translated. constructor; auto. (* Stailcall *) - econstructor; split. + left; econstructor; split. econstructor; eauto with evalexpr. apply functions_translated; eauto. apply sig_function_translated. constructor; auto. apply call_cont_commut. (* Sifthenelse *) - exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split. + left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) (sel_cont k) sp e m); split. constructor. eapply eval_condition_of_expr; eauto with evalexpr. constructor; auto. destruct b; auto. (* Sreturn None *) - econstructor; split. + left; econstructor; split. econstructor. simpl; eauto. constructor; auto. apply call_cont_commut. (* Sreturn Some *) - econstructor; split. + left; econstructor; split. econstructor. simpl. eauto with evalexpr. simpl; eauto. constructor; auto. apply call_cont_commut. (* Sgoto *) - econstructor; split. + left; econstructor; split. econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. rewrite H. simpl. reflexivity. constructor; auto. (* external call *) - econstructor; split. + left; econstructor; split. econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. constructor; auto. + (* external call turned into a Sbuiltin *) + left; econstructor; split. + econstructor. eauto. eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + constructor; auto. + (* return of an external call turned into a Sbuiltin *) + right; split. omega. split. auto. constructor; auto. Qed. Lemma sel_initial_states: @@ -509,10 +566,10 @@ Theorem transf_program_correct: Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. Proof. unfold CminorSel.exec_program, Cminor.exec_program; intros. - eapply simulation_step_preservation; eauto. + eapply simulation_opt_preservation; eauto. eexact sel_initial_states. eexact sel_final_states. - exact sel_step_correct. + eexact sel_step_correct. Qed. End PRESERVATION. diff --git a/backend/Stacking.v b/backend/Stacking.v index 5d9cf374..f289793e 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -179,6 +179,8 @@ Definition transl_instr | Ltailcall sig ros => restore_callee_save fe (Mtailcall sig ros :: k) + | Lbuiltin ef args dst => + Mbuiltin ef args dst :: k | Llabel lbl => Mlabel lbl :: k | Lgoto lbl => diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 4406187f..68d179a6 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -650,7 +650,7 @@ Qed. Lemma agree_callee_save_set_result: forall ls1 ls2 v sg, agree_callee_save ls1 ls2 -> - agree_callee_save (Locmap.set (R (Conventions.loc_result sg)) v ls1) ls2. + agree_callee_save (Locmap.set (R (loc_result sg)) v ls1) ls2. Proof. intros; red; intros. rewrite H; auto. symmetry; apply Locmap.gso. destruct l; simpl; auto. @@ -1501,7 +1501,17 @@ Proof. econstructor; eauto. intros; symmetry; eapply agree_return_regs; eauto. intros. inv WTI. generalize (H4 _ H0). tauto. - apply agree_callee_save_return_regs. + apply agree_callee_save_return_regs. + + (* Lbuiltin *) + exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) (rs0#res <- v) fr m'); split. + apply plus_one. apply exec_Mbuiltin. + change mreg with RegEq.t. + rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto with coqlib. + apply agree_set_reg; auto. (* Llabel *) econstructor; split. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index 8ba5caed..6ef86690 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -176,6 +176,9 @@ Proof. apply wt_restore_callee_save. apply wt_instrs_cons; auto. constructor; auto. destruct s0; auto. rewrite H5; auto. + (* builtin *) + apply wt_instrs_cons; auto. + constructor; auto. (* label *) apply wt_instrs_cons; auto. constructor. diff --git a/backend/Tailcall.v b/backend/Tailcall.v index 809a6a13..158002e8 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -19,7 +19,7 @@ Require Import Globalenvs. Require Import Registers. Require Import Op. Require Import RTL. -Require Conventions. +Require Import Conventions. (** An [Icall] instruction that stores its result in register [rreg] can be turned into a tail call if: @@ -88,7 +88,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) := match instr with | Icall sig ros args res s => if is_return niter f s res - && Conventions.tailcall_is_possible sig + && tailcall_is_possible sig && opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then Itailcall sig ros args else instr diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 2eed6e8d..11e6be20 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -24,7 +24,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Registers. Require Import RTL. -Require Conventions. +Require Import Conventions. Require Import Tailcall. (** * Syntactic properties of the code transformation *) @@ -168,7 +168,7 @@ Lemma transf_instr_charact: transf_instr_spec f instr (transf_instr f pc instr). Proof. intros. unfold transf_instr. destruct instr; try constructor. - caseEq (is_return niter f n r && Conventions.tailcall_is_possible s && + caseEq (is_return niter f n r && tailcall_is_possible s && opt_typ_eq (sig_res s) (sig_res (fn_sig f))); intros. destruct (andb_prop _ _ H0). destruct (andb_prop _ _ H1). eapply transf_instr_tailcall; eauto. @@ -497,6 +497,17 @@ Proof. rewrite stacksize_preserved; auto. constructor. auto. apply regset_get_list; auto. auto. +(* builtin *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. + exploit external_call_mem_extends; eauto. + intros [v' [m'1 [A [B [C D]]]]]. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'1); split. + eapply exec_Ibuiltin; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. apply regset_set; auto. + (* cond true *) TransfInstr. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifso rs' m'); split. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 3ad8c4d0..6646f11f 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -104,6 +104,8 @@ Definition tunnel_instr (uf: U.t) (b: instruction) : instruction := Lcall sig ros args res (U.repr uf s) | Ltailcall sig ros args => Ltailcall sig ros args + | Lbuiltin ef args res s => + Lbuiltin ef args res (U.repr uf s) | Lcond cond args s1 s2 => Lcond cond args (U.repr uf s1) (U.repr uf s2) | Ljumptable arg tbl => diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 774ce853..9a14158f 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -308,6 +308,14 @@ Proof. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. + (* Lbuiltin *) + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. + left; econstructor; split. + eapply exec_Lbuiltin; eauto. + rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. (* cond *) generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml index 2f61d53c..035840b1 100644 --- a/cfrontend/C2Clight.ml +++ b/cfrontend/C2Clight.ml @@ -3,6 +3,7 @@ open Printf open Cparser open Cparser.C open Cparser.Env +open Cparser.Builtins open Camlcoq open AST @@ -37,6 +38,72 @@ let warning msg = eprintf "%aWarning: %s\n" Cutil.printloc !currentLocation msg +(** ** The builtin environment *) + +let builtins_generic = { + typedefs = [ + (* keeps GCC-specific headers happy, harmless for others *) + "__builtin_va_list", C.TPtr(C.TVoid [], []) + ]; + functions = [ + (* Floating-point absolute value *) + "__builtin_fabs", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (* The volatile read/volatile write functions *) + "__builtin_volatile_read_int8unsigned", + (TInt(IUChar, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int8signed", + (TInt(ISChar, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int16unsigned", + (TInt(IUShort, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int16signed", + (TInt(IShort, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int32", + (TInt(IInt, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_float32", + (TFloat(FFloat, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_float64", + (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_pointer", + (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_write_int8unsigned", + (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false); + "__builtin_volatile_write_int8signed", + (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false); + "__builtin_volatile_write_int16unsigned", + (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false); + "__builtin_volatile_write_int16signed", + (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false); + "__builtin_volatile_write_int32", + (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false); + "__builtin_volatile_write_float32", + (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false); + "__builtin_volatile_write_float64", + (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false); + "__builtin_volatile_write_pointer", + (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false); + (* Block copy *) + "__builtin_memcpy", + (TVoid [], + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, [])], + false); + "__builtin_memcpy_words", + (TVoid [], + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, [])], + false) + ] +} + +(* Add processor-dependent builtins *) + +let builtins = + { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; + functions = builtins_generic.functions @ CBuiltins.builtins.functions } + (** ** Functions used to handle string literals *) let stringNum = ref 0 (* number of next global for string literals *) @@ -104,7 +171,10 @@ let declare_stub_function stub_name stub_type = match stub_type with | Tfunction(targs, tres) -> Datatypes.Coq_pair(intern_string stub_name, - External(intern_string stub_name, targs, tres)) + External({ ef_id = intern_string stub_name; + ef_sig = signature_of_type targs tres; + ef_inline = false }, + targs, tres)) | _ -> assert false let declare_stub_functions k = @@ -370,6 +440,8 @@ let volatile_write_fun ty = let convertTopExpr env e = match e.edesc with | C.EBinop(C.Oassign, lhs, {edesc = C.ECall(fn, args)}, _) -> + convertFuncall env (Some (convertExpr env lhs)) fn args +(**** (* Recognize __builtin_fabs and turn it into Clight operator *) begin match fn, args with | {edesc = C.EVar {name = "__builtin_fabs"}}, [arg1] -> @@ -378,6 +450,7 @@ let convertTopExpr env e = | _ -> convertFuncall env (Some (convertExpr env lhs)) fn args end +*****) | C.EBinop(C.Oassign, lhs, rhs, _) -> if Cutil.is_composite_type env lhs.etyp then unsupported "assignment between structs or between unions"; @@ -535,13 +608,23 @@ let convertFundef env fd = (** External function declaration *) +let noninlined_builtin_functions = [ + "__builtin_memcpy"; + "__builtin_memcpy_words" +] + let convertFundecl env (sto, id, ty, optinit) = - match convertTyp env ty with - | Tfunction(args, res) -> - let id' = intern_string id.name in - Datatypes.Coq_pair(id', External(id', args, res)) - | _ -> - assert false + let (args, res) = + match convertTyp env ty with + | Tfunction(args, res) -> (args, res) + | _ -> assert false in + let id' = intern_string id.name in + let ef = + { ef_id = id'; + ef_sig = signature_of_type args res; + ef_inline = List.mem_assoc id.name builtins.functions + && not (List.mem id.name noninlined_builtin_functions) } in + Datatypes.Coq_pair(id', External(ef, args, res)) (** Initializers *) @@ -816,70 +899,3 @@ let atom_alignof a = with Not_found -> None -(** ** The builtin environment *) - -open Cparser.Builtins - -let builtins_generic = { - typedefs = [ - (* keeps GCC-specific headers happy, harmless for others *) - "__builtin_va_list", C.TPtr(C.TVoid [], []) - ]; - functions = [ - (* Floating-point absolute value *) - "__builtin_fabs", - (TFloat(FDouble, []), [TFloat(FDouble, [])], false); - (* The volatile read/volatile write functions *) - "__builtin_volatile_read_int8unsigned", - (TInt(IUChar, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int8signed", - (TInt(ISChar, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int16unsigned", - (TInt(IUShort, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int16signed", - (TInt(IShort, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int32", - (TInt(IInt, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_float32", - (TFloat(FFloat, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_float64", - (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_pointer", - (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_write_int8unsigned", - (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false); - "__builtin_volatile_write_int8signed", - (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false); - "__builtin_volatile_write_int16unsigned", - (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false); - "__builtin_volatile_write_int16signed", - (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false); - "__builtin_volatile_write_int32", - (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false); - "__builtin_volatile_write_float32", - (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false); - "__builtin_volatile_write_float64", - (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false); - "__builtin_volatile_write_pointer", - (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false); - (* Block copy *) - "__builtin_memcpy", - (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); - TInt(Cutil.size_t_ikind, [])], - false); - "__builtin_memcpy_words", - (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); - TInt(Cutil.size_t_ikind, [])], - false) - ] -} - -(* Add processor-dependent builtins *) - -let builtins = - { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; - functions = builtins_generic.functions @ CBuiltins.builtins.functions } diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 42884091..212c2add 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -900,9 +900,9 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k e m2) - | step_external_function: forall id targs tres vargs k m vres t m', - external_call (external_function id targs tres) ge vargs m t vres m' -> - step (Callstate (External id targs tres) vargs k m) + | step_external_function: forall ef targs tres vargs k m vres t m', + external_call ef ge vargs m t vres m' -> + step (Callstate (External ef targs tres) vargs k m) t (Returnstate vres k m') | step_returnstate_0: forall v f e k m, @@ -1105,9 +1105,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := outcome_result_value out f.(fn_return) vres -> Mem.free_list m3 (blocks_of_env e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres - | eval_funcall_external: forall m id targs tres vargs t vres m', - external_call (external_function id targs tres) ge vargs m t vres m' -> - eval_funcall m (External id targs tres) vargs t m' vres. + | eval_funcall_external: forall m ef targs tres vargs t vres m', + external_call ef ge vargs m t vres m' -> + eval_funcall m (External ef targs tres) vargs t m' vres. Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index cc81d0f4..56bef553 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -620,8 +620,8 @@ Definition transl_fundef (f: Csyntax.fundef) : res fundef := match f with | Csyntax.Internal g => do tg <- transl_function g; OK(AST.Internal tg) - | Csyntax.External id args res => - OK(AST.External (external_function id args res)) + | Csyntax.External ef args res => + OK(AST.External ef) end. (** ** Translation of programs *) diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index ebc188e8..73a38246 100644 --- a/cfrontend/Cshmgenproof1.v +++ b/cfrontend/Cshmgenproof1.v @@ -55,27 +55,30 @@ Proof. Qed. Lemma transl_fundef_sig1: - forall f tf args res, + forall tenv f tf args res, + wt_fundef tenv f -> transl_fundef f = OK tf -> classify_fun (type_of_fundef f) = fun_case_f args res -> funsig tf = signature_of_type args res. Proof. - intros. destruct f; monadInv H. + intros. inv H; monadInv H0. monadInv EQ. simpl. - simpl in H0. inversion H0. + simpl in H1. inversion H1. unfold fn_sig; simpl. unfold signature_of_type. f_equal. apply transl_params_types; auto. - simpl. simpl in H0. congruence. + simpl. simpl in H1. inv H1. destruct (ef_sig ef); simpl in *. + unfold signature_of_type. congruence. Qed. Lemma transl_fundef_sig2: - forall f tf args res, + forall tenv f tf args res, + wt_fundef tenv f -> transl_fundef f = OK tf -> type_of_fundef f = Tfunction args res -> funsig tf = signature_of_type args res. Proof. intros. eapply transl_fundef_sig1; eauto. - rewrite H0; reflexivity. + rewrite H1; reflexivity. Qed. Lemma var_kind_by_value: diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index fb1edbe3..0e9e5b13 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -1249,7 +1249,8 @@ Proof. apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. exploit transl_exprlist_correct; eauto. - eapply transl_fundef_sig1; eauto. congruence. + eapply transl_fundef_sig1; eauto. eapply functions_well_typed; eauto. + congruence. econstructor; eauto. eapply functions_well_typed; eauto. econstructor; eauto. simpl. auto. @@ -1263,7 +1264,8 @@ Proof. apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. exploit transl_exprlist_correct; eauto. - eapply transl_fundef_sig1; eauto. congruence. + eapply transl_fundef_sig1; eauto. eapply functions_well_typed; eauto. + congruence. econstructor; eauto. eapply functions_well_typed; eauto. econstructor; eauto. simpl; auto. @@ -1595,10 +1597,15 @@ Proof. eapply Genv.find_funct_ptr_symbol_inversion; eauto. destruct H as [targs D]. assert (targs = Tnil). - inv H0. inv H10. simpl in D. unfold type_of_function in D. rewrite <- H5 in D. + inv H0. + (* internal function *) + inv H10. simpl in D. unfold type_of_function in D. rewrite <- H5 in D. simpl in D. congruence. + (* external function *) simpl in D. inv D. - exploit external_call_arity; eauto. destruct targs; simpl; congruence. + exploit external_call_arity; eauto. intro ARITY. + exploit function_ptr_well_typed; eauto. intro WT. inv WT. + rewrite H5 in ARITY. destruct targs; simpl in ARITY; congruence. subst targs. assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)). eapply transl_fundef_sig2; eauto. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index c82aa9ea..9d0791e7 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -210,7 +210,7 @@ Record function : Type := mkfunction { Inductive fundef : Type := | Internal: function -> fundef - | External: ident -> typelist -> type -> fundef. + | External: external_function -> typelist -> type -> fundef. (** ** Programs *) @@ -639,7 +639,3 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := Definition signature_of_type (args: typelist) (res: type) : signature := mksignature (typlist_of_typelist args) (opttyp_of_type res). - -Definition external_function - (id: ident) (targs: typelist) (tres: type) : AST.external_function := - mkextfun id (signature_of_type targs tres). diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index b147fbda..8e089f16 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -155,8 +155,10 @@ Inductive wt_fundef: typenv -> fundef -> Prop := | wt_fundef_Internal: forall env f, wt_function env f -> wt_fundef env (Internal f) - | wt_fundef_External: forall env id args res, - wt_fundef env (External id args res). + | wt_fundef_External: forall env ef args res, + (ef_sig ef).(sig_args) = typlist_of_typelist args -> + (ef_sig ef).(sig_res) = opttyp_of_type res -> + wt_fundef env (External ef args res). Definition add_global_var (env: typenv) (id_v: ident * globvar type) : typenv := @@ -410,8 +412,12 @@ Qed. Definition typecheck_fundef (main: ident) (env: typenv) (id_fd: ident * fundef) : bool := let (id, fd) := id_fd in match fd with - | Internal f => typecheck_function env f - | External _ _ _ => true + | Internal f => + typecheck_function env f + | External ef targs tres => + let s := ef_sig ef in + list_eq_dec typ_eq s.(sig_args) (typlist_of_typelist targs) + && opt_typ_eq s.(sig_res) (opttyp_of_type tres) end && if ident_eq id main then match type_of_fundef fd with @@ -430,8 +436,8 @@ Proof. intros. unfold typecheck_fundef in H; TrueInv. split. destruct fd. - constructor. apply typecheck_function_correct; auto. - constructor. + constructor. apply typecheck_function_correct; auto. + TrueInv. constructor; eapply proj_sumbool_true; eauto. intro. destruct (ident_eq id main). destruct (type_of_fundef fd); try discriminate. exists t; decEq; auto. apply eq_type_correct; auto. diff --git a/common/AST.v b/common/AST.v index 861795cc..bca0535b 100644 --- a/common/AST.v +++ b/common/AST.v @@ -82,6 +82,19 @@ Inductive memory_chunk : Type := | Mfloat32 : memory_chunk (**r 32-bit single-precision float *) | Mfloat64 : memory_chunk. (**r 64-bit double-precision float *) +(** The type (integer/pointer or float) of a chunk. *) + +Definition type_of_chunk (c: memory_chunk) : typ := + match c with + | Mint8signed => Tint + | Mint8unsigned => Tint + | Mint16signed => Tint + | Mint16unsigned => Tint + | Mint32 => Tint + | Mfloat32 => Tfloat + | Mfloat64 => Tfloat + end. + (** Initialization data for global variables. *) Inductive init_data: Type := @@ -390,9 +403,12 @@ Qed. Record external_function : Type := mkextfun { ef_id: ident; - ef_sig: signature + ef_sig: signature; + ef_inline: bool }. +(** Function definitions are the union of internal and external functions. *) + Inductive fundef (F: Type): Type := | Internal: F -> fundef F | External: external_function -> fundef F. diff --git a/common/Events.v b/common/Events.v index 329f31c2..a5c82d09 100644 --- a/common/Events.v +++ b/common/Events.v @@ -400,7 +400,7 @@ End EVENTVAL_INV. (** Each external function is of one of the following kinds: *) Inductive extfun_kind: signature -> Type := - | EF_syscall (sg: signature) (name: ident): extfun_kind sg + | EF_syscall (name: ident) (sg: signature): extfun_kind sg (** A system call. Takes integer-or-float arguments, produces a result that is an integer or a float, does not modify the memory, and produces an [Event_syscall] event in the trace. *) @@ -985,7 +985,7 @@ This predicate is used in the semantics of all CompCert languages. *) Definition external_call (ef: external_function): extcall_sem := match classify_external_function ef with - | EF_syscall sg name => extcall_io_sem name sg + | EF_syscall name sg => extcall_io_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk | EF_malloc => extcall_malloc_sem @@ -994,7 +994,7 @@ Definition external_call (ef: external_function): extcall_sem := Theorem external_call_spec: forall ef, - extcall_properties (external_call ef) (ef.(ef_sig)). + extcall_properties (external_call ef) (ef_sig ef). Proof. intros. unfold external_call. destruct (classify_external_function ef). apply extcall_io_ok. diff --git a/common/Memdata.v b/common/Memdata.v index 94a99176..20c0b105 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -103,19 +103,6 @@ Proof. destruct chunk1; destruct chunk2; simpl; congruence. Qed. -(** The type (integer/pointer or float) of a chunk. *) - -Definition type_of_chunk (c: memory_chunk) : typ := - match c with - | Mint8signed => Tint - | Mint8unsigned => Tint - | Mint16signed => Tint - | Mint16unsigned => Tint - | Mint32 => Tint - | Mfloat32 => Tfloat - | Mfloat64 => Tfloat - end. - (** * Memory values *) (** A ``memory value'' is a byte-sized quantity that describes the current diff --git a/common/Memory.v b/common/Memory.v index 4d65c5c9..1fb78166 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -80,9 +80,7 @@ Lemma mkmem_ext: mkmem cont1 acc1 bound1 next1 a1 b1 c1 d1 = mkmem cont2 acc2 bound2 next2 a2 b2 c2 d2. Proof. -intros. -subst. -f_equal; apply proof_irr. + intros. subst. f_equal; apply proof_irr. Qed. (** * Validity of blocks and accesses *) @@ -1699,78 +1697,78 @@ Hint Local Resolve valid_block_free_1 valid_block_free_2 Lemma mem_access_ext: forall m1 m2, perm m1 = perm m2 -> mem_access m1 = mem_access m2. Proof. -intros. -apply extensionality; intro b. -apply extensionality; intro ofs. -case_eq (mem_access m1 b ofs); case_eq (mem_access m2 b ofs); intros; auto. -assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). -assert (perm m1 b ofs p0 <-> perm m2 b ofs p0) by (rewrite H; intuition). -unfold perm, perm_order' in H2,H3. -rewrite H0 in H2,H3; rewrite H1 in H2,H3. -f_equal. -assert (perm_order p p0 -> perm_order p0 p -> p0=p) by - (clear; intros; inv H; inv H0; auto). -intuition. -assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). -unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. -assert (perm_order p p) by auto with mem. -intuition. -assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). -unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. -assert (perm_order p p) by auto with mem. -intuition. + intros. + apply extensionality; intro b. + apply extensionality; intro ofs. + case_eq (mem_access m1 b ofs); case_eq (mem_access m2 b ofs); intros; auto. + assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). + assert (perm m1 b ofs p0 <-> perm m2 b ofs p0) by (rewrite H; intuition). + unfold perm, perm_order' in H2,H3. + rewrite H0 in H2,H3; rewrite H1 in H2,H3. + f_equal. + assert (perm_order p p0 -> perm_order p0 p -> p0=p) by + (clear; intros; inv H; inv H0; auto). + intuition. + assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). + unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. + assert (perm_order p p) by auto with mem. + intuition. + assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). + unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. + assert (perm_order p p) by auto with mem. + intuition. Qed. Lemma mem_ext': forall m1 m2, - mem_access m1 = mem_access m2 -> - nextblock m1 = nextblock m2 -> - (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> - (forall b ofs, perm_order' (mem_access m1 b ofs) Readable -> - mem_contents m1 b ofs = mem_contents m2 b ofs) -> - m1 = m2. + mem_access m1 = mem_access m2 -> + nextblock m1 = nextblock m2 -> + (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> + (forall b ofs, perm_order' (mem_access m1 b ofs) Readable -> + mem_contents m1 b ofs = mem_contents m2 b ofs) -> + m1 = m2. Proof. -intros. -destruct m1; destruct m2; simpl in *. -destruct H; subst. -apply mkmem_ext; auto. -apply extensionality; intro b. -apply extensionality; intro ofs. -destruct (perm_order'_dec (mem_access0 b ofs) Readable). -auto. -destruct (noread_undef0 b ofs); try contradiction. -destruct (noread_undef1 b ofs); try contradiction. -congruence. -apply extensionality; intro b. -destruct (nextblock_noaccess0 b); auto. -destruct (nextblock_noaccess1 b); auto. -congruence. + intros. + destruct m1; destruct m2; simpl in *. + destruct H; subst. + apply mkmem_ext; auto. + apply extensionality; intro b. + apply extensionality; intro ofs. + destruct (perm_order'_dec (mem_access0 b ofs) Readable). + auto. + destruct (noread_undef0 b ofs); try contradiction. + destruct (noread_undef1 b ofs); try contradiction. + congruence. + apply extensionality; intro b. + destruct (nextblock_noaccess0 b); auto. + destruct (nextblock_noaccess1 b); auto. + congruence. Qed. Theorem mem_ext: - forall m1 m2, - perm m1 = perm m2 -> - nextblock m1 = nextblock m2 -> - (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> - (forall b ofs, loadbytes m1 b ofs 1 = loadbytes m2 b ofs 1) -> - m1 = m2. + forall m1 m2, + perm m1 = perm m2 -> + nextblock m1 = nextblock m2 -> + (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> + (forall b ofs, loadbytes m1 b ofs 1 = loadbytes m2 b ofs 1) -> + m1 = m2. Proof. -intros. -generalize (mem_access_ext _ _ H); clear H; intro. -apply mem_ext'; auto. -intros. -specialize (H2 b ofs). -unfold loadbytes in H2; simpl in H2. -destruct (range_perm_dec m1 b ofs (ofs+1)). -destruct (range_perm_dec m2 b ofs (ofs+1)). -inv H2; auto. -contradict n. -intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. -unfold perm, perm_order'. - rewrite <- H; destruct (mem_access m1 b ofs); try destruct p; intuition. -contradict n. -intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. -unfold perm. destruct (mem_access m1 b ofs); try destruct p; intuition. + intros. + generalize (mem_access_ext _ _ H); clear H; intro. + apply mem_ext'; auto. + intros. + specialize (H2 b ofs). + unfold loadbytes in H2; simpl in H2. + destruct (range_perm_dec m1 b ofs (ofs+1)). + destruct (range_perm_dec m2 b ofs (ofs+1)). + inv H2; auto. + contradict n. + intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. + unfold perm, perm_order'. + rewrite <- H; destruct (mem_access m1 b ofs); try destruct p; intuition. + contradict n. + intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. + unfold perm. destruct (mem_access m1 b ofs); try destruct p; intuition. Qed. (** * Generic injections *) diff --git a/driver/Compiler.v b/driver/Compiler.v index 1580fcd6..09a6c52e 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -103,7 +103,7 @@ Notation "a @@ b" := RTL, then to LTL, etc, all the way to Asm, and iterates this transformation for every function. The second translates the whole Cminor program to a RTL program, then to an LTL program, etc. - Between Cminor and Asm, we follow the first approach because it has + Between CminorSel and Asm, we follow the first approach because it has lower memory requirements. The translation from Clight to Asm follows the second approach. @@ -121,11 +121,10 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := @@@ Stacking.transf_fundef @@@ Asmgen.transf_fundef. -(* Here is the translation of a Cminor function to an Asm function. *) +(* Here is the translation of a CminorSel function to an Asm function. *) -Definition transf_cminor_fundef (f: Cminor.fundef) : res Asm.fundef := +Definition transf_cminorsel_fundef (f: CminorSel.fundef) : res Asm.fundef := OK f - @@ Selection.sel_fundef @@@ RTLgen.transl_fundef @@@ transf_rtl_fundef. @@ -135,7 +134,9 @@ Definition transf_rtl_program (p: RTL.program) : res Asm.program := transform_partial_program transf_rtl_fundef p. Definition transf_cminor_program (p: Cminor.program) : res Asm.program := - transform_partial_program transf_cminor_fundef p. + OK p + @@ Selection.sel_program + @@@ transform_partial_program transf_cminorsel_fundef. Definition transf_c_program (p: Csyntax.program) : res Asm.program := match Ctyping.typecheck_program p with @@ -284,16 +285,15 @@ Theorem transf_cminor_program_correct: Cminor.exec_program p beh -> Asm.exec_program tp beh. Proof. - intros. unfold transf_cminor_program, transf_cminor_fundef in H. + intros. unfold transf_cminor_program, transf_cminorsel_fundef in H. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [X3 P3]]. clear H. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X3) as [p2 [X2 P2]]. clear X3. - destruct (transform_program_compose _ _ _ _ _ _ _ _ X2) as [p1 [X1 P1]]. - generalize (transform_partial_program_identity _ _ _ _ X1). clear X1. intro. subst p1. + generalize (transform_partial_program_identity _ _ _ _ X2). clear X2. intro. subst p2. apply transf_rtl_program_correct with p3; auto. - apply RTLgenproof.transf_program_correct with p2; auto. - rewrite <- P1. apply Selectionproof.transf_program_correct; auto. + apply RTLgenproof.transf_program_correct with (Selection.sel_program p); auto. + apply Selectionproof.transf_program_correct; auto. Qed. Theorem transf_c_program_correct: @@ -306,7 +306,7 @@ Proof. intros until beh; unfold transf_c_program; simpl. caseEq (Ctyping.typecheck_program p); try congruence; intro. caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. - caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. + caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. intros EQ3 NOTW SEM. eapply transf_cminor_program_correct; eauto. eapply Cminorgenproof.transl_program_correct; eauto. diff --git a/driver/Complements.v b/driver/Complements.v index 7389d291..3f32cc63 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -59,7 +59,14 @@ Proof. assert (i0 = i) by congruence. assert (rs'0 = rs') by congruence. assert (m'0 = m') by congruence. - subst. auto. + subst. auto. + replace i with (Pbuiltin ef args res) in H5 by congruence. simpl in H5. inv H5. + congruence. + replace i with (Pbuiltin ef args res) in H12 by congruence. simpl in H12. inv H12. + rewrite H2 in H7; inv H7. rewrite H3 in H8; inv H8. rewrite H4 in H9; inv H9. + exploit external_call_determ. eexact H5. eexact H12. auto. + intros [A [B C]]. subst. auto. + congruence. congruence. congruence. assert (ef0 = ef) by congruence. subst ef0. @@ -82,7 +89,8 @@ Lemma final_state_not_step: Proof. unfold nostep. intros. red; intros. inv H. inv H0. unfold Vzero in H1. congruence. - unfold Vzero in H1. congruence. + unfold Vzero in H1. congruence. + unfold Vzero in H1. congruence. Qed. Lemma final_state_deterministic: diff --git a/lib/Axioms.v b/lib/Axioms.v index 0d82ed4b..52a7fffa 100644 --- a/lib/Axioms.v +++ b/lib/Axioms.v @@ -1,27 +1,59 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** This file collects some axioms used throughout the CompCert development. *) + Require ClassicalFacts. -(* We use just 2 axioms of extensionality: +(** * Extensionality axioms *) + +(** The following [Require Export] gives us functional extensionality for dependent function types: +<< +Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, + forall (f g : forall x : A, B x), + (forall x, f x = g x) -> f = g. +>> +and, as a corollary, functional extensionality for non-dependent functions: +<< +Lemma functional_extensionality {A B} (f g : A -> B) : + (forall x, f x = g x) -> f = g. +>> +*) +Require Export FunctionalExtensionality. -1. Functional extensionality for dependent functions - (FunctionalExtensionality.functional_extensionality_dep) - forall {A} {B : A -> Type}, forall (f g : forall x : A, B x), (forall x, f x = g x) -> f = g. +(** For compatibility with earlier developments, [extensionality] + is an alias for [functional_extensionality]. *) -2. Propositional extensionality (forall A B:Prop, (A <-> B) -> A = B.) +Lemma extensionality: + forall (A B: Type) (f g : A -> B), (forall x, f x = g x) -> f = g. +Proof. intros; apply functional_extensionality. auto. Qed. -*) +Implicit Arguments extensionality. -Require Export FunctionalExtensionality. (* Contains one Axiom *) +(** We also assert propositional extensionality. *) Axiom prop_ext: ClassicalFacts.prop_extensionality. Implicit Arguments prop_ext. +(** * Proof irrelevance *) + +(** We also use proof irrelevance, which is a consequence of propositional + extensionality. *) + Lemma proof_irr: ClassicalFacts.proof_irrelevance. Proof. -exact (ClassicalFacts.ext_prop_dep_proof_irrel_cic prop_ext). + exact (ClassicalFacts.ext_prop_dep_proof_irrel_cic prop_ext). Qed. Implicit Arguments proof_irr. - -Lemma extensionality: - forall (A B: Type) (f g : A -> B), (forall x, f x = g x) -> f = g. -Proof. intros; apply functional_extensionality. auto. Qed. -Implicit Arguments extensionality. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 21c237e6..9da58710 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -24,7 +24,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Locations. Require Stacklayout. -Require Conventions. +Require Import Conventions. (** * Abstract syntax *) @@ -56,6 +56,34 @@ Proof. decide equality. Defined. Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. Proof. decide equality. Defined. +(** The PowerPC has a great many registers, some general-purpose, some very + specific. We model only the following registers: *) + +Inductive preg: Type := + | IR: ireg -> preg (**r integer registers *) + | FR: freg -> preg (**r float registers *) + | PC: preg (**r program counter *) + | LR: preg (**r link register (return address) *) + | CTR: preg (**r count register, used for some branches *) + | CARRY: preg (**r carry bit of the status register *) + | CR0_0: preg (**r bit 0 of the condition register *) + | CR0_1: preg (**r bit 1 of the condition register *) + | CR0_2: preg (**r bit 2 of the condition register *) + | CR0_3: preg. (**r bit 3 of the condition register *) + +Coercion IR: ireg >-> preg. +Coercion FR: freg >-> preg. + +Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. +Proof. decide equality. apply ireg_eq. apply freg_eq. Defined. + +Module PregEq. + Definition t := preg. + Definition eq := preg_eq. +End PregEq. + +Module Pregmap := EMap(PregEq). + (** Symbolic constants. Immediate operands to an arithmetic instruction or an indexed memory access can be either integer literals, or the low or high 16 bits of a symbolic reference (the address @@ -188,7 +216,8 @@ Inductive instruction : Type := | Pxor: ireg -> ireg -> ireg -> instruction (**r bitwise xor *) | Pxori: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate *) | Pxoris: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate high *) - | Plabel: label -> instruction. (**r define a code label *) + | Plabel: label -> instruction (**r define a code label *) + | Pbuiltin: external_function -> list preg -> preg -> instruction. (**r built-in *) (** The pseudo-instructions are the following: @@ -313,34 +342,6 @@ Definition program := AST.program fundef unit. (** * Operational semantics *) -(** The PowerPC has a great many registers, some general-purpose, some very - specific. We model only the following registers: *) - -Inductive preg: Type := - | IR: ireg -> preg (**r integer registers *) - | FR: freg -> preg (**r float registers *) - | PC: preg (**r program counter *) - | LR: preg (**r link register (return address) *) - | CTR: preg (**r count register, used for some branches *) - | CARRY: preg (**r carry bit of the status register *) - | CR0_0: preg (**r bit 0 of the condition register *) - | CR0_1: preg (**r bit 1 of the condition register *) - | CR0_2: preg (**r bit 2 of the condition register *) - | CR0_3: preg. (**r bit 3 of the condition register *) - -Coercion IR: ireg >-> preg. -Coercion FR: freg >-> preg. - -Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. apply freg_eq. Defined. - -Module PregEq. - Definition t := preg. - Definition eq := preg_eq. -End PregEq. - -Module Pregmap := EMap(PregEq). - (** The semantics operates over a single mapping from registers (type [preg]) to values. We maintain (but do not enforce) the convention that integer registers are mapped to values of @@ -788,6 +789,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#rd <- (Val.xor rs#r1 (const_high cst)))) m | Plabel lbl => OK (nextinstr rs) m + | Pbuiltin ef args res => + Error (**r treated specially below *) end. (** Translation of the LTL/Linear/Mach view of machine registers @@ -859,10 +862,10 @@ Inductive extcall_args (rs: regset) (m: mem): list loc -> list val -> Prop := Definition extcall_arguments (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := - extcall_args rs m (Conventions.loc_arguments sg) args. + extcall_args rs m (loc_arguments sg) args. Definition loc_external_result (sg: signature) : preg := - preg_of (Conventions.loc_result sg). + preg_of (loc_result sg). (** Execution of the instruction at [rs#PC]. *) @@ -877,13 +880,20 @@ Inductive step: state -> trace -> state -> Prop := find_instr (Int.unsigned ofs) c = Some i -> exec_instr c i rs m = OK rs' m' -> step (State rs m) E0 (State rs' m') + | exec_step_builtin: + forall b ofs c ef args res rs m t v m', + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal c) -> + find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) -> + external_call ef ge (map rs args) m t v m' -> + step (State rs m) t (State (nextinstr(rs # res <- v)) m') | exec_step_external: forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> - extcall_arguments rs m ef.(ef_sig) args -> - rs' = (rs#(loc_external_result ef.(ef_sig)) <- res + extcall_arguments rs m (ef_sig ef) args -> + rs' = (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs LR)) -> step (State rs m) t (State rs' m'). diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index ca42d563..b1b1245b 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -494,6 +494,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pmtlr GPR12 :: Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbs symb :: k + | Mbuiltin ef args res => + Pbuiltin ef (map preg_of args) (preg_of res) :: k | Mlabel lbl => Plabel lbl :: k | Mgoto lbl => diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index fcbbbd73..ee2867e6 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -25,6 +25,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Op. Require Import Locations. +Require Import Conventions. Require Import Mach. Require Import Machconcr. Require Import Machtyping. @@ -1063,6 +1064,37 @@ Proof. unfold rs5; auto with ppcgen. Qed. +Lemma exec_Mbuiltin_prop: + forall (s : list stackframe) (f : block) (sp : val) + (ms : Mach.regset) (m : mem) (ef : external_function) + (args : list mreg) (res : mreg) (b : list Mach.instruction) + (t : trace) (v : val) (m' : mem), + external_call ef ge ms ## args m t v m' -> + exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t + (Machconcr.State s f sp b (Regmap.set res v ms) m'). +Proof. + intros; red; intros; inv MS. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI. inv WTI. + inv AT. simpl in H3. + generalize (functions_transl _ _ FIND); intro FN. + generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. + left. econstructor; split. apply plus_one. + eapply exec_step_builtin. eauto. eauto. + eapply find_instr_tail; eauto. + replace (rs##(preg_of##args)) with (ms##args). + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + rewrite list_map_compose. apply list_map_exten. intros. + symmetry. eapply preg_val; eauto. + econstructor; eauto with coqlib. + unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. + rewrite <- H0. simpl. constructor; auto. + eapply code_tail_next_int; eauto. + apply sym_not_equal. auto with ppcgen. + auto with ppcgen. +Qed. + Lemma exec_Mgoto_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) @@ -1345,7 +1377,7 @@ Lemma exec_function_external_prop: Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef ge args m t0 res m' -> Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> - ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> + ms' = Regmap.set (loc_result (ef_sig ef)) res ms -> exec_instr_prop (Machconcr.Callstate s fb ms m) t0 (Machconcr.Returnstate s ms' m'). Proof. @@ -1387,6 +1419,7 @@ Proof exec_Mstore_prop exec_Mcall_prop exec_Mtailcall_prop + exec_Mbuiltin_prop exec_Mgoto_prop exec_Mcond_true_prop exec_Mcond_false_prop diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 60c49690..5ebde633 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -27,7 +27,7 @@ Require Import Machconcr. Require Import Machtyping. Require Import Asm. Require Import Asmgen. -Require Conventions. +Require Import Conventions. (** * Properties of low half/high half decomposition *) diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 62e4536b..b3ccb20b 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -178,6 +178,11 @@ let creg oc r = | MacOS|Diab -> fprintf oc "cr%d" r | Linux -> fprintf oc "%d" r +let preg oc = function + | IR r -> ireg oc r + | FR r -> freg oc r + | _ -> assert false + (* Names of sections *) let name_of_section_MacOS = function @@ -256,7 +261,90 @@ let rec log2 n = assert (n > 0); if n = 1 then 0 else 1 + log2 (n lsr 1) -(* Built-in functions *) +(* Built-ins. They come in two flavors: + - inlined by the compiler: take their arguments in arbitrary + registers; preserve all registers except GPR12 and FPR13 + - inlined while printing asm code; take their arguments in + locations dictated by the calling conventions; preserve + callee-save regs only. *) + +let print_builtin_inlined oc name args res = + fprintf oc "%s begin builtin %s\n" comment name; + (* Can use as temporaries: GPR12, FPR13 *) + begin match name, args, res with + (* Volatile reads *) + | "__builtin_volatile_read_int8unsigned", [IR addr], IR res -> + fprintf oc " lbz %a, 0(%a)\n" ireg res ireg addr + | "__builtin_volatile_read_int8signed", [IR addr], IR res -> + fprintf oc " lbz %a, 0(%a)\n" ireg res ireg addr; + fprintf oc " extsb %a, %a\n" ireg res ireg res + | "__builtin_volatile_read_int16unsigned", [IR addr], IR res -> + fprintf oc " lhz %a, 0(%a)\n" ireg res ireg addr + | "__builtin_volatile_read_int16signed", [IR addr], IR res -> + fprintf oc " lha %a, 0(%a)\n" ireg res ireg addr + | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res -> + fprintf oc " lwz %a, 0(%a)\n" ireg res ireg addr + | "__builtin_volatile_read_float32", [IR addr], FR res -> + fprintf oc " lfs %a, 0(%a)\n" freg res ireg addr + | "__builtin_volatile_read_float64", [IR addr], FR res -> + fprintf oc " lfd %a, 0(%a)\n" freg res ireg addr + (* Volatile writes *) + | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ -> + fprintf oc " stb %a, 0(%a)\n" ireg src ireg addr + | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ -> + fprintf oc " sth %a, 0(%a)\n" ireg src ireg addr + | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ -> + fprintf oc " stw %a, 0(%a)\n" ireg src ireg addr + | "__builtin_volatile_write_float32", [IR addr; FR src], _ -> + fprintf oc " frsp %a, %a\n" freg FPR13 freg src; + fprintf oc " stfs %a, 0(%a)\n" freg FPR13 ireg addr + | "__builtin_volatile_write_float64", [IR addr; FR src], _ -> + fprintf oc " stfd %a, 0(%a)\n" freg src ireg addr + (* Integer arithmetic *) + | "__builtin_mulhw", [IR a1; IR a2], IR res -> + fprintf oc " mulhw %a, %a, %a\n" ireg res ireg a1 ireg a2 + | "__builtin_mulhwu", [IR a1; IR a2], IR res -> + fprintf oc " mulhwu %a, %a, %a\n" ireg res ireg a1 ireg a2 + | "__builtin_cntlzw", [IR a1], IR res -> + fprintf oc " cntlzw %a, %a\n" ireg res ireg a1 + (* Float arithmetic *) + | "__builtin_fmadd", [FR a1; FR a2; FR a3], FR res -> + fprintf oc " fmadd %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 + | "__builtin_fmsub", [FR a1; FR a2; FR a3], FR res -> + fprintf oc " fmsub %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 + | "__builtin_fabs", [FR a1], FR res -> + fprintf oc " fabs %a, %a\n" freg res freg a1 + | "__builtin_fsqrt", [FR a1], FR res -> + fprintf oc " fsqrt %a, %a\n" freg res freg a1 + | "__builtin_frsqrte", [FR a1], FR res -> + fprintf oc " frsqrte %a, %a\n" freg res freg a1 + | "__builtin_fres", [FR a1], FR res -> + fprintf oc " fres %a, %a\n" freg res freg a1 + | "__builtin_fsel", [FR a1; FR a2; FR a3], FR res -> + fprintf oc " fsel %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 + (* Memory accesses *) + | "__builtin_read_int16_reversed", [IR a1], IR res -> + fprintf oc " lhbrx %a, %a, %a\n" ireg res ireg_or_zero GPR0 ireg a1 + | "__builtin_read_int32_reversed", [IR a1], IR res -> + fprintf oc " lwbrx %a, %a, %a\n" ireg res ireg_or_zero GPR0 ireg a1 + | "__builtin_write_int16_reversed", [IR a1; IR a2], _ -> + fprintf oc " sthbrx %a, %a, %a\n" ireg a2 ireg_or_zero GPR0 ireg a1 + | "__builtin_write_int32_reversed", [IR a1; IR a2], _ -> + fprintf oc " stwbrx %a, %a, %a\n" ireg a2 ireg_or_zero GPR0 ireg a1 + (* Synchronization *) + | "__builtin_eieio", [], _ -> + fprintf oc " eieio\n" + | "__builtin_sync", [], _ -> + fprintf oc " sync\n" + | "__builtin_isync", [], _ -> + fprintf oc " isync\n" + | "__builtin_trap", [], _ -> + fprintf oc " trap\n" + (* Catch-all *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + end; + fprintf oc "%s end builtin %s\n" comment name let re_builtin_function = Str.regexp "__builtin_" @@ -264,121 +352,42 @@ let is_builtin_function s = Str.string_match re_builtin_function (extern_atom s) 0 let print_builtin_function oc s = - fprintf oc "%s begin builtin %s\n" comment (extern_atom s); - (* int args: GPR3, GPR4 float args: FPR1, FPR2, FPR3 - int res: GPR3 float res: FPR1 + fprintf oc "%s begin builtin function %s\n" comment (extern_atom s); + (* int args: GPR3, GPR4, GPR5 float args: FPR1, FPR2, FPR3 + int res: GPR3 float res: FPR1 Watch out for MacOSX/EABI incompatibility: functions that take some floats then some ints. There are none here. *) - begin match extern_atom s with - (* Volatile reads *) - | "__builtin_volatile_read_int8unsigned" -> - fprintf oc " lbz %a, 0(%a)\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_int8signed" -> - fprintf oc " lbz %a, 0(%a)\n" ireg GPR3 ireg GPR3; - fprintf oc " extsb %a, %a\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_int16unsigned" -> - fprintf oc " lhz %a, 0(%a)\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_int16signed" -> - fprintf oc " lha %a, 0(%a)\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_int32" - | "__builtin_volatile_read_pointer" -> - fprintf oc " lwz %a, 0(%a)\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_float32" -> - fprintf oc " lfs %a, 0(%a)\n" freg FPR1 ireg GPR3 - | "__builtin_volatile_read_float64" -> - fprintf oc " lfd %a, 0(%a)\n" freg FPR1 ireg GPR3 - (* Volatile writes *) - | "__builtin_volatile_write_int8unsigned" - | "__builtin_volatile_write_int8signed" -> - fprintf oc " stb %a, 0(%a)\n" ireg GPR4 ireg GPR3 - | "__builtin_volatile_write_int16unsigned" - | "__builtin_volatile_write_int16signed" -> - fprintf oc " sth %a, 0(%a)\n" ireg GPR4 ireg GPR3 - | "__builtin_volatile_write_int32" - | "__builtin_volatile_write_pointer" -> - fprintf oc " stw %a, 0(%a)\n" ireg GPR4 ireg GPR3 - | "__builtin_volatile_write_float32" -> - fprintf oc " frsp %a, %a\n" freg FPR1 freg FPR1; - fprintf oc " stfs %a, 0(%a)\n" freg FPR1 ireg GPR3 - | "__builtin_volatile_write_float64" -> - fprintf oc " stfd %a, 0(%a)\n" freg FPR1 ireg GPR3 (* Block copy *) + begin match extern_atom s with | "__builtin_memcpy" -> let lbl1 = new_label() in let lbl2 = new_label() in - fprintf oc " cmplwi %a, %a, 0\n" creg 0 ireg GPR5; - fprintf oc " beq %a, %a\n" creg 0 label lbl1; - fprintf oc " mtctr %a\n" ireg GPR5; - fprintf oc " addi %a, %a, -1\n" ireg GPR3 ireg GPR3; - fprintf oc " addi %a, %a, -1\n" ireg GPR4 ireg GPR4; - fprintf oc "%a: lbzu %a, 1(%a)\n" label lbl2 ireg GPR0 ireg GPR4; - fprintf oc " stbu %a, 1(%a)\n" ireg GPR0 ireg GPR3; - fprintf oc " bdnz %a\n" label lbl2; + fprintf oc " cmplwi %a, %a, 0\n" creg 0 ireg GPR5; + fprintf oc " beq %a, %a\n" creg 0 label lbl1; + fprintf oc " mtctr %a\n" ireg GPR5; + fprintf oc " addi %a, %a, -1\n" ireg GPR3 ireg GPR3; + fprintf oc " addi %a, %a, -1\n" ireg GPR4 ireg GPR4; + fprintf oc "%a: lbzu %a, 1(%a)\n" label lbl2 ireg GPR0 ireg GPR4; + fprintf oc " stbu %a, 1(%a)\n" ireg GPR0 ireg GPR3; + fprintf oc " bdnz %a\n" label lbl2; fprintf oc "%a:\n" label lbl1 | "__builtin_memcpy_words" -> let lbl1 = new_label() in let lbl2 = new_label() in - fprintf oc " rlwinm. %a, %a, 30, 2, 31\n" ireg GPR5 ireg GPR5; - fprintf oc " beq %a, %a\n" creg 0 label lbl1; - fprintf oc " mtctr %a\n" ireg GPR5; - fprintf oc " addi %a, %a, -4\n" ireg GPR3 ireg GPR3; - fprintf oc " addi %a, %a, -4\n" ireg GPR4 ireg GPR4; - fprintf oc "%a: lwzu %a, 4(%a)\n" label lbl2 ireg GPR0 ireg GPR4; - fprintf oc " stwu %a, 4(%a)\n" ireg GPR0 ireg GPR3; - fprintf oc " bdnz %a\n" label lbl2; + fprintf oc " rlwinm. %a, %a, 30, 2, 31\n" ireg GPR5 ireg GPR5; + fprintf oc " beq %a, %a\n" creg 0 label lbl1; + fprintf oc " mtctr %a\n" ireg GPR5; + fprintf oc " addi %a, %a, -4\n" ireg GPR3 ireg GPR3; + fprintf oc " addi %a, %a, -4\n" ireg GPR4 ireg GPR4; + fprintf oc "%a: lwzu %a, 4(%a)\n" label lbl2 ireg GPR0 ireg GPR4; + fprintf oc " stwu %a, 4(%a)\n" ireg GPR0 ireg GPR3; + fprintf oc " bdnz %a\n" label lbl2; fprintf oc "%a:\n" label lbl1 - (* Integer arithmetic *) - | "__builtin_mulhw" -> - fprintf oc " mulhw %a, %a, %a\n" ireg GPR3 ireg GPR3 ireg GPR4 - | "__builtin_mulhwu" -> - fprintf oc " mulhwu %a, %a, %a\n" ireg GPR3 ireg GPR3 ireg GPR4 - | "__builtin_cntlzw" -> - fprintf oc " cntlzw %a, %a\n" ireg GPR3 ireg GPR3 - (* Float arithmetic *) - | "__builtin_fmadd" -> - fprintf oc " fmadd %a, %a, %a, %a\n" - freg FPR1 freg FPR1 freg FPR2 freg FPR3 - | "__builtin_fmsub" -> - fprintf oc " fmsub %a, %a, %a, %a\n" - freg FPR1 freg FPR1 freg FPR2 freg FPR3 - | "__builtin_fabs" -> - fprintf oc " fabs %a, %a\n" freg FPR1 freg FPR1 - | "__builtin_fsqrt" -> - fprintf oc " fsqrt %a, %a\n" freg FPR1 freg FPR1 - | "__builtin_frsqrte" -> - fprintf oc " frsqrte %a, %a\n" freg FPR1 freg FPR1 - | "__builtin_fres" -> - fprintf oc " fres %a, %a\n" freg FPR1 freg FPR1 - | "__builtin_fsel" -> - fprintf oc " fsel %a, %a, %a, %a\n" - freg FPR1 freg FPR1 freg FPR2 freg FPR3 - (* Memory accesses *) - | "__builtin_read_int16_reversed" -> - fprintf oc " lhbrx %a, %a, %a\n" - ireg GPR3 ireg_or_zero GPR0 ireg GPR3 - | "__builtin_read_int32_reversed" -> - fprintf oc " lwbrx %a, %a, %a\n" - ireg GPR3 ireg_or_zero GPR0 ireg GPR3 - | "__builtin_write_int16_reversed" -> - fprintf oc " sthbrx %a, %a, %a\n" - ireg GPR4 ireg_or_zero GPR0 ireg GPR3 - | "__builtin_write_int32_reversed" -> - fprintf oc " stwbrx %a, %a, %a\n" - ireg GPR4 ireg_or_zero GPR0 ireg GPR3 - (* Synchronization *) - | "__builtin_eieio" -> - fprintf oc " eieio\n" - | "__builtin_sync" -> - fprintf oc " sync\n" - | "__builtin_isync" -> - fprintf oc " isync\n" - | "__builtin_trap" -> - fprintf oc " trap\n" (* Catch-all *) | s -> invalid_arg ("unrecognized builtin function " ^ s) end; - fprintf oc "%s end builtin %s\n" comment (extern_atom s) + fprintf oc "%s end builtin function %s\n" comment (extern_atom s) (* Printing of instructions *) @@ -450,10 +459,7 @@ let print_instruction oc labels = function fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12; fprintf oc " mtctr %a\n" ireg GPR12; fprintf oc " bctr\n"; - fprintf oc "%a:" label lbl; - List.iter - (fun l -> fprintf oc " .long %a\n" label (transl_label l)) - tbl; + jumptables := (lbl, tbl) :: !jumptables; fprintf oc "%s end pseudoinstr btbl\n" comment | Pcmplw(r1, r2) -> fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 @@ -660,6 +666,8 @@ let print_instruction oc labels = function | Plabel lbl -> if Labelset.mem lbl labels then fprintf oc "%a:\n" label (transl_label lbl) + | Pbuiltin(ef, args, res) -> + print_builtin_inlined oc (extern_atom ef.ef_id) args res let print_literal oc (lbl, n) = let nlo = Int64.to_int32 n @@ -814,7 +822,7 @@ let stub_function oc name ef = fprintf oc " .align 2\n"; fprintf oc "L%s$stub:\n" name; if Str.string_match re_variadic_stub name 0 - then variadic_stub oc name (Str.matched_group 1 name) ef.ef_sig.sig_args + then variadic_stub oc name (Str.matched_group 1 name) (ef_sig ef).sig_args else non_variadic_stub oc name let function_needs_stub name = true @@ -839,7 +847,7 @@ let stub_function oc name ef = let name = extern_atom name in (* Only variadic functions need a stub *) if Str.string_match re_variadic_stub name 0 - then variadic_stub oc name (Str.matched_group 1 name) ef.ef_sig.sig_args + then variadic_stub oc name (Str.matched_group 1 name) (ef_sig ef).sig_args let function_needs_stub name = Str.string_match re_variadic_stub (extern_atom name) 0 @@ -858,13 +866,15 @@ let stub_function = let print_fundef oc (Coq_pair(name, defn)) = match defn with - | Internal code -> print_function oc name code - | External ef -> if not(is_builtin_function name) then stub_function oc name ef + | Internal code -> + print_function oc name code + | External ef -> + if not (is_builtin_function name) then stub_function oc name ef let record_extfun (Coq_pair(name, defn)) = match defn with | Internal _ -> () - | External _ -> + | External _ -> if function_needs_stub name && not (is_builtin_function name) then stubbed_functions := IdentSet.add name !stubbed_functions diff --git a/powerpc/eabi/Conventions.v b/powerpc/eabi/Conventions1.v index fd3a4ebe..60eaaa5e 100644 --- a/powerpc/eabi/Conventions.v +++ b/powerpc/eabi/Conventions1.v @@ -229,65 +229,6 @@ Proof. unfold float_callee_save_regs; NoRepet. Qed. -(** * Acceptable locations for register allocation *) - -(** The following predicate describes the locations that can be assigned - to an RTL pseudo-register during register allocation: a non-temporary - machine register or a [Local] stack slot are acceptable. *) - -Definition loc_acceptable (l: loc) : Prop := - match l with - | R r => ~(In l temporaries) - | S (Local ofs ty) => ofs >= 0 - | S (Incoming _ _) => False - | S (Outgoing _ _) => False - end. - -Definition locs_acceptable (ll: list loc) : Prop := - forall l, In l ll -> loc_acceptable l. - -Lemma temporaries_not_acceptable: - forall l, loc_acceptable l -> Loc.notin l temporaries. -Proof. - unfold loc_acceptable; destruct l. - simpl. intuition congruence. - destruct s; try contradiction. - intro. simpl. tauto. -Qed. -Hint Resolve temporaries_not_acceptable: locs. - -Lemma locs_acceptable_disj_temporaries: - forall ll, locs_acceptable ll -> Loc.disjoint ll temporaries. -Proof. - intros. apply Loc.notin_disjoint. intros. - apply temporaries_not_acceptable. auto. -Qed. - -Lemma loc_acceptable_noteq_diff: - forall l1 l2, - loc_acceptable l1 -> l1 <> l2 -> Loc.diff l1 l2. -Proof. - unfold loc_acceptable, Loc.diff; destruct l1; destruct l2; - try (destruct s); try (destruct s0); intros; auto; try congruence. - case (zeq z z0); intro. - compare t t0; intro. - subst z0; subst t0; tauto. - tauto. tauto. - contradiction. contradiction. -Qed. - -Lemma loc_acceptable_notin_notin: - forall r ll, - loc_acceptable r -> - ~(In r ll) -> Loc.notin r ll. -Proof. - induction ll; simpl; intros. - auto. - split. apply loc_acceptable_noteq_diff. assumption. - apply sym_not_equal. tauto. - apply IHll. assumption. tauto. -Qed. - (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -333,40 +274,18 @@ Proof. reflexivity. Qed. -(** The result location is acceptable. *) - -Lemma loc_result_acceptable: - forall sig, loc_acceptable (R (loc_result sig)). -Proof. - intros. unfold loc_acceptable. red. - unfold loc_result. destruct (sig_res sig). - destruct t; simpl; NotOrEq. - simpl; NotOrEq. -Qed. - -(** The result location is a caller-save register. *) +(** The result location is a caller-save register or a temporary *) Lemma loc_result_caller_save: - forall (s: signature), In (R (loc_result s)) destroyed_at_call. + forall (s: signature), + In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries. Proof. - intros; unfold loc_result. + intros; unfold loc_result. left; destruct (sig_res s). destruct t; simpl; OrEq. simpl; OrEq. Qed. -(** The result location is not a callee-save register. *) - -Lemma loc_result_not_callee_save: - forall (s: signature), - ~(In (loc_result s) int_callee_save_regs \/ In (loc_result s) float_callee_save_regs). -Proof. - intros. generalize (loc_result_caller_save s). - generalize (int_callee_save_not_destroyed (loc_result s)). - generalize (float_callee_save_not_destroyed (loc_result s)). - tauto. -Qed. - (** ** Location of function arguments *) (** The PowerPC EABI states the following convention for passing arguments @@ -635,24 +554,6 @@ Proof. ElimOrEq; intuition. Qed. -(** Callee-save registers do not overlap with argument locations. *) - -Lemma arguments_not_preserved: - forall sig l, - Loc.notin l destroyed_at_call -> loc_acceptable l -> - Loc.notin l (loc_arguments sig). -Proof. - intros. unfold loc_arguments. destruct l. - apply loc_arguments_rec_notin_reg. - generalize (Loc.notin_not_in _ _ H). intro; red; intro. - apply H1. generalize H2. simpl. ElimOrEq; OrEq. - generalize (Loc.notin_not_in _ _ H). intro; red; intro. - apply H1. generalize H2. simpl. ElimOrEq; OrEq. - destruct s; simpl in H0; try contradiction. - apply loc_arguments_rec_notin_local. -Qed. -Hint Resolve arguments_not_preserved: locs. - (** Argument locations agree in number with the function signature. *) Lemma loc_arguments_length: @@ -687,108 +588,3 @@ Proof. intro; simpl. ElimOrEq; reflexivity. intro; simpl. ElimOrEq; reflexivity. Qed. - -(** There is no partial overlap between an argument location and an - acceptable location: they are either identical or disjoint. *) - -Lemma no_overlap_arguments: - forall args sg, - locs_acceptable args -> - Loc.no_overlap args (loc_arguments sg). -Proof. - unfold Loc.no_overlap; intros. - generalize (H r H0). - generalize (loc_arguments_acceptable _ _ H1). - destruct s; destruct r; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; auto. - intros. right. auto. - destruct s; try tauto. destruct s0; tauto. -Qed. - -(** Decide whether a tailcall is possible. *) - -Definition tailcall_is_possible (sg: signature) : bool := - let fix tcisp (l: list loc) := - match l with - | nil => true - | R _ :: l' => tcisp l' - | S _ :: l' => false - end - in tcisp (loc_arguments sg). - -Lemma tailcall_is_possible_correct: - forall s, tailcall_is_possible s = true -> tailcall_possible s. -Proof. - intro s. unfold tailcall_is_possible, tailcall_possible. - generalize (loc_arguments s). induction l; simpl; intros. - elim H0. - destruct a. - destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate. -Qed. - -(** ** Location of function parameters *) - -(** A function finds the values of its parameter in the same locations - where its caller stored them, except that the stack-allocated arguments, - viewed as [Outgoing] slots by the caller, are accessed via [Incoming] - slots (at the same offsets and types) in the callee. *) - -Definition parameter_of_argument (l: loc) : loc := - match l with - | S (Outgoing n ty) => S (Incoming n ty) - | _ => l - end. - -Definition loc_parameters (s: signature) := - List.map parameter_of_argument (loc_arguments s). - -Lemma loc_parameters_type: - forall sig, List.map Loc.type (loc_parameters sig) = sig.(sig_args). -Proof. - intros. unfold loc_parameters. - rewrite list_map_compose. - rewrite <- loc_arguments_type. - apply list_map_exten. - intros. destruct x; simpl. auto. - destruct s; reflexivity. -Qed. - -Lemma loc_parameters_length: - forall sg, List.length (loc_parameters sg) = List.length sg.(sig_args). -Proof. - intros. unfold loc_parameters. rewrite list_length_map. - apply loc_arguments_length. -Qed. - -Lemma loc_parameters_not_temporaries: - forall sig, Loc.disjoint (loc_parameters sig) temporaries. -Proof. - intro; red; intros. - unfold loc_parameters in H. - elim (list_in_map_inv _ _ _ H). intros y [EQ IN]. - generalize (loc_arguments_not_temporaries sig y x2 IN H0). - subst x1. destruct x2. - destruct y; simpl. auto. destruct s; auto. - byContradiction. generalize H0. simpl. NotOrEq. -Qed. - -Lemma no_overlap_parameters: - forall params sg, - locs_acceptable params -> - Loc.no_overlap (loc_parameters sg) params. -Proof. - unfold Loc.no_overlap; intros. - unfold loc_parameters in H0. - elim (list_in_map_inv _ _ _ H0). intros t [EQ IN]. - rewrite EQ. - generalize (loc_arguments_acceptable _ _ IN). - generalize (H s H1). - destruct s; destruct t; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; simpl; auto. - intros; right; auto. - destruct s; try tauto. destruct s0; try tauto. - intros; simpl. tauto. -Qed. - diff --git a/powerpc/macosx/Conventions.v b/powerpc/macosx/Conventions1.v index 1954c912..a5741e1c 100644 --- a/powerpc/macosx/Conventions.v +++ b/powerpc/macosx/Conventions1.v @@ -229,65 +229,6 @@ Proof. unfold float_callee_save_regs; NoRepet. Qed. -(** * Acceptable locations for register allocation *) - -(** The following predicate describes the locations that can be assigned - to an RTL pseudo-register during register allocation: a non-temporary - machine register or a [Local] stack slot are acceptable. *) - -Definition loc_acceptable (l: loc) : Prop := - match l with - | R r => ~(In l temporaries) - | S (Local ofs ty) => ofs >= 0 - | S (Incoming _ _) => False - | S (Outgoing _ _) => False - end. - -Definition locs_acceptable (ll: list loc) : Prop := - forall l, In l ll -> loc_acceptable l. - -Lemma temporaries_not_acceptable: - forall l, loc_acceptable l -> Loc.notin l temporaries. -Proof. - unfold loc_acceptable; destruct l. - simpl. intuition congruence. - destruct s; try contradiction. - intro. simpl. tauto. -Qed. -Hint Resolve temporaries_not_acceptable: locs. - -Lemma locs_acceptable_disj_temporaries: - forall ll, locs_acceptable ll -> Loc.disjoint ll temporaries. -Proof. - intros. apply Loc.notin_disjoint. intros. - apply temporaries_not_acceptable. auto. -Qed. - -Lemma loc_acceptable_noteq_diff: - forall l1 l2, - loc_acceptable l1 -> l1 <> l2 -> Loc.diff l1 l2. -Proof. - unfold loc_acceptable, Loc.diff; destruct l1; destruct l2; - try (destruct s); try (destruct s0); intros; auto; try congruence. - case (zeq z z0); intro. - compare t t0; intro. - subst z0; subst t0; tauto. - tauto. tauto. - contradiction. contradiction. -Qed. - -Lemma loc_acceptable_notin_notin: - forall r ll, - loc_acceptable r -> - ~(In r ll) -> Loc.notin r ll. -Proof. - induction ll; simpl; intros. - auto. - split. apply loc_acceptable_noteq_diff. assumption. - apply sym_not_equal. tauto. - apply IHll. assumption. tauto. -Qed. - (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -333,40 +274,18 @@ Proof. reflexivity. Qed. -(** The result location is acceptable. *) - -Lemma loc_result_acceptable: - forall sig, loc_acceptable (R (loc_result sig)). -Proof. - intros. unfold loc_acceptable. red. - unfold loc_result. destruct (sig_res sig). - destruct t; simpl; NotOrEq. - simpl; NotOrEq. -Qed. - -(** The result location is a caller-save register. *) +(** The result location is a caller-save register or a temporary *) Lemma loc_result_caller_save: - forall (s: signature), In (R (loc_result s)) destroyed_at_call. + forall (s: signature), + In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries. Proof. - intros; unfold loc_result. + intros; unfold loc_result. left; destruct (sig_res s). destruct t; simpl; OrEq. simpl; OrEq. Qed. -(** The result location is not a callee-save register. *) - -Lemma loc_result_not_callee_save: - forall (s: signature), - ~(In (loc_result s) int_callee_save_regs \/ In (loc_result s) float_callee_save_regs). -Proof. - intros. generalize (loc_result_caller_save s). - generalize (int_callee_save_not_destroyed (loc_result s)). - generalize (float_callee_save_not_destroyed (loc_result s)). - tauto. -Qed. - (** ** Location of function arguments *) (** The PowerPC ABI states the following convention for passing arguments @@ -439,13 +358,6 @@ Fixpoint size_arguments_rec Definition size_arguments (s: signature) : Z := size_arguments_rec s.(sig_args) int_param_regs float_param_regs 8. -(** A tail-call is possible for a signature if the corresponding - arguments are all passed in registers. *) - -Definition tailcall_possible (s: signature) : Prop := - forall l, In l (loc_arguments s) -> - match l with R _ => True | S _ => False end. - (** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -641,24 +553,6 @@ Proof. ElimOrEq; intuition. Qed. -(** Callee-save registers do not overlap with argument locations. *) - -Lemma arguments_not_preserved: - forall sig l, - Loc.notin l destroyed_at_call -> loc_acceptable l -> - Loc.notin l (loc_arguments sig). -Proof. - intros. unfold loc_arguments. destruct l. - apply loc_arguments_rec_notin_reg. - generalize (Loc.notin_not_in _ _ H). intro; red; intro. - apply H1. generalize H2. simpl. ElimOrEq; OrEq. - generalize (Loc.notin_not_in _ _ H). intro; red; intro. - apply H1. generalize H2. simpl. ElimOrEq; OrEq. - destruct s; simpl in H0; try contradiction. - apply loc_arguments_rec_notin_local. -Qed. -Hint Resolve arguments_not_preserved: locs. - (** Argument locations agree in number with the function signature. *) Lemma loc_arguments_length: @@ -696,107 +590,3 @@ Proof. intro; simpl. ElimOrEq; reflexivity. Qed. -(** There is no partial overlap between an argument location and an - acceptable location: they are either identical or disjoint. *) - -Lemma no_overlap_arguments: - forall args sg, - locs_acceptable args -> - Loc.no_overlap args (loc_arguments sg). -Proof. - unfold Loc.no_overlap; intros. - generalize (H r H0). - generalize (loc_arguments_acceptable _ _ H1). - destruct s; destruct r; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; auto. - intros. right. auto. - destruct s; try tauto. destruct s0; tauto. -Qed. - -(** Decide whether a tailcall is possible. *) - -Definition tailcall_is_possible (sg: signature) : bool := - let fix tcisp (l: list loc) := - match l with - | nil => true - | R _ :: l' => tcisp l' - | S _ :: l' => false - end - in tcisp (loc_arguments sg). - -Lemma tailcall_is_possible_correct: - forall s, tailcall_is_possible s = true -> tailcall_possible s. -Proof. - intro s. unfold tailcall_is_possible, tailcall_possible. - generalize (loc_arguments s). induction l; simpl; intros. - elim H0. - destruct a. - destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate. -Qed. - -(** ** Location of function parameters *) - -(** A function finds the values of its parameter in the same locations - where its caller stored them, except that the stack-allocated arguments, - viewed as [Outgoing] slots by the caller, are accessed via [Incoming] - slots (at the same offsets and types) in the callee. *) - -Definition parameter_of_argument (l: loc) : loc := - match l with - | S (Outgoing n ty) => S (Incoming n ty) - | _ => l - end. - -Definition loc_parameters (s: signature) := - List.map parameter_of_argument (loc_arguments s). - -Lemma loc_parameters_type: - forall sig, List.map Loc.type (loc_parameters sig) = sig.(sig_args). -Proof. - intros. unfold loc_parameters. - rewrite list_map_compose. - rewrite <- loc_arguments_type. - apply list_map_exten. - intros. destruct x; simpl. auto. - destruct s; reflexivity. -Qed. - -Lemma loc_parameters_length: - forall sg, List.length (loc_parameters sg) = List.length sg.(sig_args). -Proof. - intros. unfold loc_parameters. rewrite list_length_map. - apply loc_arguments_length. -Qed. - -Lemma loc_parameters_not_temporaries: - forall sig, Loc.disjoint (loc_parameters sig) temporaries. -Proof. - intro; red; intros. - unfold loc_parameters in H. - elim (list_in_map_inv _ _ _ H). intros y [EQ IN]. - generalize (loc_arguments_not_temporaries sig y x2 IN H0). - subst x1. destruct x2. - destruct y; simpl. auto. destruct s; auto. - byContradiction. generalize H0. simpl. NotOrEq. -Qed. - -Lemma no_overlap_parameters: - forall params sg, - locs_acceptable params -> - Loc.no_overlap (loc_parameters sg) params. -Proof. - unfold Loc.no_overlap; intros. - unfold loc_parameters in H0. - elim (list_in_map_inv _ _ _ H0). intros t [EQ IN]. - rewrite EQ. - generalize (loc_arguments_acceptable _ _ IN). - generalize (H s H1). - destruct s; destruct t; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; simpl; auto. - intros; right; auto. - destruct s; try tauto. destruct s0; try tauto. - intros; simpl. tauto. -Qed. - |