diff options
| -rw-r--r-- | .depend | 20 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backend/Allocation.v | 117 | ||||
| -rw-r--r-- | backend/Allocproof.v | 254 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 708 | ||||
| -rw-r--r-- | backend/Locations.v | 24 | ||||
| -rw-r--r-- | backend/RTLtyping.v | 428 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 206 | ||||
| -rw-r--r-- | common/Unityping.v | 435 |
9 files changed, 672 insertions, 1522 deletions
@@ -27,7 +27,7 @@ common/Smallstep.vo common/Smallstep.glob common/Smallstep.v.beautified: common/ common/Behaviors.vo common/Behaviors.glob common/Behaviors.v.beautified: common/Behaviors.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo common/Switch.vo common/Switch.glob common/Switch.v.beautified: common/Switch.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo common/Determinism.vo common/Determinism.glob common/Determinism.v.beautified: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo -common/Unityping.vo common/Unityping.glob common/Unityping.v.beautified: common/Unityping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo +common/Subtyping.vo common/Subtyping.glob common/Subtyping.v.beautified: common/Subtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo backend/Cminor.vo backend/Cminor.glob backend/Cminor.v.beautified: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo $(ARCH)/Op.vo $(ARCH)/Op.glob $(ARCH)/Op.v.beautified: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/CminorSel.vo backend/CminorSel.glob backend/CminorSel.v.beautified: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo @@ -35,7 +35,7 @@ $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH) backend/SelectDiv.vo backend/SelectDiv.glob backend/SelectDiv.v.beautified: backend/SelectDiv.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo common/Errors.vo backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo -$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDivproof.vo backend/SelectDivproof.glob backend/SelectDivproof.v.beautified: backend/SelectDivproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectDiv.vo backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectDivproof.vo backend/SelectLongproof.vo @@ -51,7 +51,7 @@ backend/Inliningspec.vo backend/Inliningspec.glob backend/Inliningspec.v.beautif backend/Inliningproof.vo backend/Inliningproof.glob backend/Inliningproof.v.beautified: backend/Inliningproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/Inlining.vo backend/Inliningspec.vo backend/RTL.vo backend/Renumber.vo backend/Renumber.glob backend/Renumber.v.beautified: backend/Renumber.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo backend/RTL.vo backend/Renumberproof.vo backend/Renumberproof.glob backend/Renumberproof.v.beautified: backend/Renumberproof.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Renumber.vo -backend/RTLtyping.vo backend/RTLtyping.glob backend/RTLtyping.v.beautified: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo common/Unityping.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo lib/Integers.vo common/Memory.vo common/Events.vo backend/RTL.vo backend/Conventions.vo +backend/RTLtyping.vo backend/RTLtyping.glob backend/RTLtyping.v.beautified: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo common/Subtyping.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo lib/Integers.vo common/Memory.vo common/Events.vo backend/RTL.vo backend/Conventions.vo backend/Kildall.vo backend/Kildall.glob backend/Kildall.v.beautified: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo backend/Liveness.vo backend/Liveness.glob backend/Liveness.v.beautified: backend/Liveness.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueDomain.glob backend/ValueDomain.v.beautified: backend/ValueDomain.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo backend/RTL.vo @@ -59,18 +59,18 @@ $(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH) backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/Liveness.vo lib/Axioms.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/ValueDomain.vo backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo -$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo +$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.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/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo backend/CSEdomain.vo backend/CSEdomain.glob backend/CSEdomain.v.beautified: backend/CSEdomain.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob $(ARCH)/CombineOp.v.beautified: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/CSEdomain.vo backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: backend/CSE.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 $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/CSEdomain.vo backend/Kildall.vo $(ARCH)/CombineOp.vo -$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo +$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo backend/CSEproof.vo backend/CSEproof.glob backend/CSEproof.v.beautified: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo backend/NeedDomain.vo backend/NeedDomain.glob backend/NeedDomain.v.beautified: backend/NeedDomain.v lib/Coqlib.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Registers.vo backend/ValueDomain.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/NeedOp.vo $(ARCH)/NeedOp.glob $(ARCH)/NeedOp.v.beautified: $(ARCH)/NeedOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/NeedDomain.vo backend/RTL.vo backend/Deadcode.vo backend/Deadcode.glob backend/Deadcode.v.beautified: backend/Deadcode.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memory.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcodeproof.vo backend/Deadcodeproof.glob backend/Deadcodeproof.v.beautified: backend/Deadcodeproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcode.vo -$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo +$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: backend/Locations.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo $(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob $(ARCH)/$(VARIANT)/Conventions1.v.beautified: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo @@ -80,7 +80,7 @@ backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: b backend/Tunneling.vo backend/Tunneling.glob backend/Tunneling.v.beautified: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo backend/LTL.vo backend/Tunnelingproof.vo backend/Tunnelingproof.glob backend/Tunnelingproof.v.beautified: 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/Linear.vo backend/Linear.glob backend/Linear.v.beautified: backend/Linear.v lib/Coqlib.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.glob backend/Lineartyping.v.beautified: backend/Lineartyping.v lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo lib/Iteration.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo $(ARCH)/Op.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Linear.vo common/Globalenvs.vo common/Memory.vo +backend/Lineartyping.vo backend/Lineartyping.glob backend/Lineartyping.v.beautified: backend/Lineartyping.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo backend/Linearize.glob backend/Linearize.v.beautified: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Errors.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Kildall.vo lib/Lattice.vo backend/Linearizeproof.vo backend/Linearizeproof.glob backend/Linearizeproof.v.beautified: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo lib/Lattice.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/Linear.vo backend/Linearize.vo backend/CleanupLabels.vo backend/CleanupLabels.glob backend/CleanupLabels.v.beautified: backend/CleanupLabels.v lib/Coqlib.vo lib/Ordered.vo backend/Linear.vo @@ -91,10 +91,10 @@ $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob $(ARCH)/$( backend/Stacking.vo backend/Stacking.glob backend/Stacking.v.beautified: backend/Stacking.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Lineartyping.vo backend/Stackingproof.vo backend/Stackingproof.glob backend/Stackingproof.v.beautified: backend/Stackingproof.v lib/Coqlib.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/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo $(ARCH)/Asm.vo $(ARCH)/Asm.glob $(ARCH)/Asm.v.beautified: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo -$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo +$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo -$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/Errors.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 backend/Conventions.vo backend/Asmgenproof0.vo -$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(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 $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.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/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo $(ARCH)/Archi.vo cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo @@ -71,7 +71,7 @@ LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ # Parts common to the front-ends and the back-end (in common/) COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \ - Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Unityping.v + Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Subtyping.v # Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT)) diff --git a/backend/Allocation.v b/backend/Allocation.v index f4fcd6e..f830d79 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -368,7 +368,7 @@ End IndexedEqKind. Module OrderedEqKind := OrderedIndexed(IndexedEqKind). -(** This is an order over equations that is lexicographic on [ereg], then +(** This is an order over equations that is lexicgraphic on [ereg], then [eloc], then [ekind]. *) Module OrderedEquation <: OrderedType. @@ -609,6 +609,20 @@ Definition subst_loc (l1 l2: loc) (e: eqs) : option eqs := (EqSet2.elements_between (select_loc_l l1) (select_loc_h l1) (eqs2 e)) (Some e). +(** [loc_type_compat env l e] checks that for all equations [r = l] in [e], + the type [env r] of [r] is compatible with the type of [l]. *) + +Definition sel_type (k: equation_kind) (ty: typ) : typ := + match k with + | Full => ty + | Low | High => Tint + end. + +Definition loc_type_compat (env: regenv) (l: loc) (e: eqs) : bool := + EqSet2.for_all_between + (fun q => subtype (sel_type (ekind q) (env (ereg q))) (Loc.type l)) + (select_loc_l l) (select_loc_h l) (eqs2 e). + (** [add_equations [r1...rN] [m1...mN] e] adds to [e] the [N] equations [ri = R mi [Full]]. Return [None] if the two lists have different lengths. *) @@ -759,18 +773,25 @@ Definition destroyed_by_move (src dst: loc) := | _, _ => destroyed_by_op Omove end. +Definition well_typed_move (env: regenv) (dst: loc) (e: eqs) : bool := + match dst with + | R r => true + | S sl ofs ty => loc_type_compat env dst e + end. + (** Simulate the effect of a sequence of moves [mv] on a set of equations [e]. The set [e] is the equations that must hold after the sequence of moves. Return the set of equations that must hold before the sequence of moves. Return [None] if the set of equations [e] cannot hold after the sequence of moves. *) -Fixpoint track_moves (mv: moves) (e: eqs) : option eqs := +Fixpoint track_moves (env: regenv) (mv: moves) (e: eqs) : option eqs := match mv with | nil => Some e | (src, dst) :: mv => - do e1 <- track_moves mv e; + do e1 <- track_moves env mv e; assertion (can_undef_except dst (destroyed_by_move src dst)) e1; + assertion (well_typed_move env dst e1); subst_loc dst src e1 end. @@ -803,89 +824,89 @@ Definition kind_second_word := if Archi.big_endian then Low else High. equations that must hold "before" these instructions, or [None] if impossible. *) -Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option eqs := +Definition transfer_aux (f: RTL.function) (env: regenv) (shape: block_shape) (e: eqs) : option eqs := match shape with | BSnop mv s => - track_moves mv e + track_moves env mv e | BSmove src dst mv s => - track_moves mv (subst_reg dst src e) + track_moves env mv (subst_reg dst src e) | BSmakelong src1 src2 dst mv s => let e1 := subst_reg_kind dst High src1 Full e in let e2 := subst_reg_kind dst Low src2 Full e1 in assertion (reg_unconstrained dst e2); - track_moves mv e2 + track_moves env mv e2 | BSlowlong src dst mv s => let e1 := subst_reg_kind dst Full src Low e in assertion (reg_unconstrained dst e1); - track_moves mv e1 + track_moves env mv e1 | BShighlong src dst mv s => let e1 := subst_reg_kind dst Full src High e in assertion (reg_unconstrained dst e1); - track_moves mv e1 + track_moves env mv e1 | BSop op args res mv1 args' res' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; do e2 <- transfer_use_def args res args' res' (destroyed_by_op op) e1; - track_moves mv1 e2 + track_moves env mv1 e2 | BSopdead op args res mv s => assertion (reg_unconstrained res e); - track_moves mv e + track_moves env mv e | BSload chunk addr args dst mv1 args' dst' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1; - track_moves mv1 e2 + track_moves env mv1 e2 | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => - do e1 <- track_moves mv3 e; + do e1 <- track_moves env mv3 e; let e2 := remove_equation (Eq kind_second_word dst (R dst2')) e1 in assertion (loc_unconstrained (R dst2') e2); assertion (can_undef (destroyed_by_load Mint32 addr') e2); do e3 <- add_equations args args2' e2; - do e4 <- track_moves mv2 e3; + do e4 <- track_moves env mv2 e3; let e5 := remove_equation (Eq kind_first_word dst (R dst1')) e4 in assertion (loc_unconstrained (R dst1') e5); assertion (can_undef (destroyed_by_load Mint32 addr) e5); assertion (reg_unconstrained dst e5); do e6 <- add_equations args args1' e5; - track_moves mv1 e6 + track_moves env mv1 e6 | BSload2_1 addr args dst mv1 args' dst' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; let e2 := remove_equation (Eq kind_first_word dst (R dst')) e1 in assertion (reg_loc_unconstrained dst (R dst') e2); assertion (can_undef (destroyed_by_load Mint32 addr) e2); do e3 <- add_equations args args' e2; - track_moves mv1 e3 + track_moves env mv1 e3 | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; let e2 := remove_equation (Eq kind_second_word dst (R dst')) e1 in assertion (reg_loc_unconstrained dst (R dst') e2); assertion (can_undef (destroyed_by_load Mint32 addr') e2); do e3 <- add_equations args args' e2; - track_moves mv1 e3 + track_moves env mv1 e3 | BSloaddead chunk addr args dst mv s => assertion (reg_unconstrained dst e); - track_moves mv e + track_moves env mv e | BSstore chunk addr args src mv args' src' s => assertion (can_undef (destroyed_by_store chunk addr) e); do e1 <- add_equations (src :: args) (src' :: args') e; - track_moves mv e1 + track_moves env mv e1 | BSstore2 addr addr' args src mv1 args1' src1' mv2 args2' src2' s => assertion (can_undef (destroyed_by_store Mint32 addr') e); do e1 <- add_equations args args2' (add_equation (Eq kind_second_word src (R src2')) e); - do e2 <- track_moves mv2 e1; + do e2 <- track_moves env mv2 e1; assertion (can_undef (destroyed_by_store Mint32 addr) e2); do e3 <- add_equations args args1' (add_equation (Eq kind_first_word src (R src1')) e2); - track_moves mv1 e3 + track_moves env mv1 e3 | BScall sg ros args res mv1 ros' mv2 s => let args' := loc_arguments sg in let res' := map R (loc_result sg) in - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; do e2 <- remove_equations_res res (sig_res sg) res' e1; assertion (forallb (fun l => reg_loc_unconstrained res l e2) res'); assertion (no_caller_saves e2); do e3 <- add_equation_ros ros ros' e2; do e4 <- add_equations_args args (sig_args sg) args' e3; - track_moves mv1 e4 + track_moves env mv1 e4 | BStailcall sg ros args mv1 ros' => let args' := loc_arguments sg in assertion (tailcall_is_possible sg); @@ -893,9 +914,9 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option assertion (ros_compatible_tailcall ros'); do e1 <- add_equation_ros ros ros' empty_eqs; do e2 <- add_equations_args args (sig_args sg) args' e1; - track_moves mv1 e2 + track_moves env mv1 e2 | BSbuiltin ef args res mv1 args' res' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; let args' := map R args' in let res' := map R res' in do e2 <- remove_equations_res res (sig_res (ef_sig ef)) res' e1; @@ -903,23 +924,23 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option assertion (forallb (fun l => loc_unconstrained l e2) res'); assertion (can_undef (destroyed_by_builtin ef) e2); do e3 <- add_equations_args args (sig_args (ef_sig ef)) args' e2; - track_moves mv1 e3 + track_moves env mv1 e3 | BSannot txt typ args res mv1 args' s => do e1 <- add_equations_args args (annot_args_typ typ) args' e; - track_moves mv1 e1 + track_moves env mv1 e1 | BScond cond args mv args' s1 s2 => assertion (can_undef (destroyed_by_cond cond) e); do e1 <- add_equations args args' e; - track_moves mv e1 + track_moves env mv e1 | BSjumptable arg mv arg' tbl => assertion (can_undef destroyed_by_jumptable e); - track_moves mv (add_equation (Eq Full arg (R arg')) e) + track_moves env mv (add_equation (Eq Full arg (R arg')) e) | BSreturn None mv => - track_moves mv empty_eqs + track_moves env mv empty_eqs | BSreturn (Some arg) mv => let arg' := map R (loc_result (RTL.fn_sig f)) in do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs; - track_moves mv e1 + track_moves env mv e1 end. (** The main transfer function for the dataflow analysis. Like [transfer_aux], @@ -927,7 +948,7 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option equations that must hold "after". It also handles error propagation and reporting. *) -Definition transfer (f: RTL.function) (shapes: PTree.t block_shape) +Definition transfer (f: RTL.function) (env: regenv) (shapes: PTree.t block_shape) (pc: node) (after: res eqs) : res eqs := match after with | Error _ => after @@ -935,7 +956,7 @@ Definition transfer (f: RTL.function) (shapes: PTree.t block_shape) match shapes!pc with | None => Error(MSG "At PC " :: POS pc :: MSG ": unmatched block" :: nil) | Some shape => - match transfer_aux f shape e with + match transfer_aux f env shape e with | None => Error(MSG "At PC " :: POS pc :: MSG ": invalid register allocation" :: nil) | Some e' => OK e' end @@ -1083,8 +1104,8 @@ Definition successors_block_shape (bsh: block_shape) : list node := | BSreturn optarg mv => nil end. -Definition analyze (f: RTL.function) (bsh: PTree.t block_shape) := - DS.fixpoint_allnodes bsh successors_block_shape (transfer f bsh). +Definition analyze (f: RTL.function) (env: regenv) (bsh: PTree.t block_shape) := + DS.fixpoint_allnodes bsh successors_block_shape (transfer f env bsh). (** * Validating and translating functions and programs *) @@ -1118,9 +1139,9 @@ Function compat_entry (rparams: list reg) (tys: list typ) (lparams: list loc) (e and stack size. *) Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function) - (e1: eqs) : option unit := + (env: regenv) (e1: eqs) : option unit := do mv <- pair_entrypoints rtl ltl; - do e2 <- track_moves mv e1; + do e2 <- track_moves env mv e1; assertion (compat_entry (RTL.fn_params rtl) (sig_args (RTL.fn_sig rtl)) (loc_parameters (RTL.fn_sig rtl)) e2); @@ -1133,10 +1154,10 @@ Local Close Scope option_monad_scope. Local Open Scope error_monad_scope. Definition check_entrypoints (rtl: RTL.function) (ltl: LTL.function) - (bsh: PTree.t block_shape) + (env: regenv) (bsh: PTree.t block_shape) (a: PMap.t LEq.t): res unit := - do e1 <- transfer rtl bsh (RTL.fn_entrypoint rtl) a!!(RTL.fn_entrypoint rtl); - match check_entrypoints_aux rtl ltl e1 with + do e1 <- transfer rtl env bsh (RTL.fn_entrypoint rtl) a!!(RTL.fn_entrypoint rtl); + match check_entrypoints_aux rtl ltl env e1 with | None => Error (msg "invalid register allocation at entry point") | Some _ => OK tt end. @@ -1145,11 +1166,11 @@ Definition check_entrypoints (rtl: RTL.function) (ltl: LTL.function) a source RTL function and an LTL function generated by the external register allocator. *) -Definition check_function (rtl: RTL.function) (ltl: LTL.function) : res unit := +Definition check_function (rtl: RTL.function) (ltl: LTL.function) (env: regenv) : res unit := let bsh := pair_codes rtl ltl in - match analyze rtl bsh with + match analyze rtl env bsh with | None => Error (msg "allocation analysis diverges") - | Some a => check_entrypoints rtl ltl bsh a + | Some a => check_entrypoints rtl ltl env bsh a end. (** [regalloc] is the external register allocator. It is written in OCaml @@ -1165,7 +1186,7 @@ Definition transf_function (f: RTL.function) : res LTL.function := | OK env => match regalloc f with | Error m => Error m - | OK tf => do x <- check_function f tf; OK tf + | OK tf => do x <- check_function f tf env; OK tf end end. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 9303878..4c39fee 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -451,7 +451,7 @@ Lemma add_equations_args_lessdef: forall rs ls rl tyl ll e e', add_equations_args rl tyl ll e = Some e' -> satisf rs ls e' -> - Val.has_type_list (rs##rl) (normalize_list tyl) -> + Val.has_type_list (rs##rl) tyl -> Val.lessdef_list (rs##rl) (decode_longs tyl (map ls ll)). Proof. intros until e'. functional induction (add_equations_args rl tyl ll e); simpl; intros. @@ -648,7 +648,7 @@ Lemma loc_unconstrained_satisf: Proof. intros; red; intros. destruct (OrderedEquation.eq_dec q (Eq k r l)). - subst q; simpl. unfold l; rewrite Locmap.gss. auto. + subst q; simpl. unfold l; rewrite Locmap.gss_reg. auto. assert (EqSet.In q (remove_equation (Eq k r l) e)). simpl. ESD.fsetdec. rewrite Locmap.gso. apply H; auto. eapply loc_unconstrained_sound; eauto. @@ -674,7 +674,7 @@ Lemma parallel_assignment_satisf: Proof. intros; red; intros. destruct (OrderedEquation.eq_dec q (Eq k r l)). - subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss; auto. + subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss_reg; auto. assert (EqSet.In q (remove_equation {| ekind := k; ereg := r; eloc := l |} e)). simpl. ESD.fsetdec. exploit reg_loc_unconstrained_sound; eauto. intros [A B]. @@ -702,11 +702,11 @@ Proof. rewrite <- H5 in H2. simpl in H2. InvBooleans. simpl. destruct (OrderedEquation.eq_dec q (Eq Low res l2)). subst q; simpl. rewrite Regmap.gss. - destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss. + destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg. apply Val.loword_lessdef; auto. destruct (OrderedEquation.eq_dec q (Eq High res l1)). subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto. - destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss. + destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg. apply Val.hiword_lessdef; auto. assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. rewrite Regmap.gso. rewrite ! Locmap.gso. auto. @@ -719,7 +719,7 @@ Proof. set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *. destruct (OrderedEquation.eq_dec q (Eq Full res l1)). subst q; simpl. rewrite Regmap.gss. - destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss. + destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg. auto. assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec. simpl. rewrite Regmap.gso. rewrite Locmap.gso. auto. @@ -969,7 +969,6 @@ Proof. split. apply eqs_same; auto. auto. Qed. -(* Lemma loc_type_compat_charact: forall env l e q, loc_type_compat env l e = true -> @@ -1009,8 +1008,7 @@ Proof. destruct (rs#r); exact I. eelim Loc.diff_not_eq. eexact A. auto. Qed. -*) -(* + Remark val_lessdef_normalize: forall v v' ty, Val.has_type v ty -> Val.lessdef v v' -> @@ -1018,19 +1016,23 @@ Remark val_lessdef_normalize: Proof. intros. inv H0. rewrite Val.load_result_same; auto. auto. Qed. -*) Lemma subst_loc_satisf: forall env src dst rs ls e e', subst_loc dst src e = Some e' -> - (*well_typed_move env dst e = true ->*) + well_typed_move env dst e = true -> wt_regset env rs -> satisf rs ls e' -> satisf rs (Locmap.set dst (ls src) ls) e. Proof. intros; red; intros. exploit in_subst_loc; eauto. intros [[A B] | [A B]]. - subst dst. rewrite Locmap.gss. apply (H1 _ B). + subst dst. rewrite Locmap.gss. + destruct q as [k r l]; simpl in *. + exploit well_typed_move_charact; eauto. + destruct l as [mr | sl ofs ty]; intros. + apply (H2 _ B). + apply val_lessdef_normalize; auto. apply (H2 _ B). rewrite Locmap.gso; auto. Qed. @@ -1077,18 +1079,22 @@ Proof. Qed. Lemma subst_loc_undef_satisf: - forall src dst rs ls ml e e', + forall env src dst rs ls ml e e', subst_loc dst src e = Some e' -> - (*well_typed_move env dst e = true ->*) + well_typed_move env dst e = true -> can_undef_except dst ml e = true -> - (*wt_regset env rs ->*) + wt_regset env rs -> satisf rs ls e' -> satisf rs (Locmap.set dst (ls src) (undef_regs ml ls)) e. Proof. intros; red; intros. exploit in_subst_loc; eauto. intros [[A B] | [A B]]. subst dst. rewrite Locmap.gss. - destruct q as [k r l]; simpl in *. apply (H1 _ B). + destruct q as [k r l]; simpl in *. + exploit well_typed_move_charact; eauto. + destruct l as [mr | sl ofs ty]; intros. + apply (H3 _ B). + apply val_lessdef_normalize; auto. apply (H3 _ B). rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto. eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto. Qed. @@ -1330,27 +1336,27 @@ Qed. (** * Properties of the dataflow analysis *) Lemma analyze_successors: - forall f bsh an pc bs s e, - analyze f bsh = Some an -> + forall f env bsh an pc bs s e, + analyze f env bsh = Some an -> bsh!pc = Some bs -> In s (successors_block_shape bs) -> an!!pc = OK e -> - exists e', transfer f bsh s an!!s = OK e' /\ EqSet.Subset e' e. + exists e', transfer f env bsh s an!!s = OK e' /\ EqSet.Subset e' e. Proof. unfold analyze; intros. exploit DS.fixpoint_allnodes_solution; eauto. - rewrite H2. unfold DS.L.ge. destruct (transfer f bsh s an#s); intros. + rewrite H2. unfold DS.L.ge. destruct (transfer f env bsh s an#s); intros. exists e0; auto. contradiction. Qed. Lemma satisf_successors: - forall f bsh an pc bs s e rs ls, - analyze f bsh = Some an -> + forall f env bsh an pc bs s e rs ls, + analyze f env bsh = Some an -> bsh!pc = Some bs -> In s (successors_block_shape bs) -> an!!pc = OK e -> satisf rs ls e -> - exists e', transfer f bsh s an!!s = OK e' /\ satisf rs ls e'. + exists e', transfer f env bsh s an!!s = OK e' /\ satisf rs ls e'. Proof. intros. exploit analyze_successors; eauto. intros [e' [A B]]. exists e'; split; auto. eapply satisf_incr; eauto. @@ -1360,12 +1366,13 @@ Qed. Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop := | transf_function_spec_intro: - forall an mv k e1 e2, - analyze f (pair_codes f tf) = Some an -> + forall env an mv k e1 e2, + wt_function f env -> + analyze f env (pair_codes f tf) = Some an -> (LTL.fn_code tf)!(LTL.fn_entrypoint tf) = Some(expand_moves mv (Lbranch (RTL.fn_entrypoint f) :: k)) -> wf_moves mv -> - transfer f (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 -> - track_moves mv e1 = Some e2 -> + transfer f env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 -> + track_moves env mv e1 = Some e2 -> compat_entry (RTL.fn_params f) (sig_args (RTL.fn_sig f)) (loc_parameters (fn_sig tf)) e2 = true -> can_undef destroyed_at_function_entry e2 = true -> RTL.fn_stacksize f = LTL.fn_stacksize tf -> @@ -1380,33 +1387,36 @@ Proof. unfold transf_function; intros. destruct (type_function f) as [env|] eqn:TY; try discriminate. destruct (regalloc f); try discriminate. - destruct (check_function f f0) as [] eqn:?; inv H. + destruct (check_function f f0 env) as [] eqn:?; inv H. unfold check_function in Heqr. - destruct (analyze f (pair_codes f tf)) as [an|] eqn:?; try discriminate. + destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate. monadInv Heqr. - destruct (check_entrypoints_aux f tf x) as [y|] eqn:?; try discriminate. + destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate. unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv. exploit extract_moves_sound; eauto. intros [A B]. subst b. exploit check_succ_sound; eauto. intros [k EQ1]. subst b0. - econstructor; eauto. congruence. + econstructor; eauto. eapply type_function_correct; eauto. congruence. Qed. Lemma invert_code: - forall f tf pc i opte e, + forall f env tf pc i opte e, + wt_function f env -> (RTL.fn_code f)!pc = Some i -> - transfer f (pair_codes f tf) pc opte = OK e -> + transfer f env (pair_codes f tf) pc opte = OK e -> exists eafter, exists bsh, exists bb, opte = OK eafter /\ (pair_codes f tf)!pc = Some bsh /\ (LTL.fn_code tf)!pc = Some bb /\ expand_block_shape bsh i bb /\ - transfer_aux f bsh eafter = Some e. + transfer_aux f env bsh eafter = Some e /\ + wt_instr f env i. Proof. - intros. destruct opte as [eafter|]; simpl in H0; try discriminate. exists eafter. + intros. destruct opte as [eafter|]; simpl in H1; try discriminate. exists eafter. destruct (pair_codes f tf)!pc as [bsh|] eqn:?; try discriminate. exists bsh. exploit matching_instr_block; eauto. intros [bb [A B]]. - destruct (transfer_aux f bsh eafter) as [e1|] eqn:?; inv H0. - exists bb. tauto. + destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H1. + exists bb. exploit wt_instr_at; eauto. + tauto. Qed. (** * Semantic preservation *) @@ -1480,10 +1490,11 @@ Proof. Qed. Lemma exec_moves: - forall mv rs s f sp bb m e e' ls, - track_moves mv e = Some e' -> + forall mv env rs s f sp bb m e e' ls, + track_moves env mv e = Some e' -> wf_moves mv -> satisf rs ls e' -> + wt_regset env rs -> exists ls', star step tge (Block s f sp (expand_moves mv bb) ls m) E0 (Block s f sp bb ls' m) @@ -1495,7 +1506,7 @@ Opaque destroyed_by_op. - unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. auto. (* step *) - destruct a as [src dst]. unfold expand_moves. simpl. - destruct (track_moves mv e) as [e1|] eqn:?; MonadInv. + destruct (track_moves env mv e) as [e1|] eqn:?; MonadInv. assert (wf_moves mv). red; intros. apply H0; auto with coqlib. destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst]. (* reg-reg *) @@ -1521,13 +1532,17 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa sg.(sig_res) = Some Tint -> match_stackframes nil nil sg | match_stackframes_cons: - forall res f sp pc rs s tf bb ls ts sg an e + forall res f sp pc rs s tf bb ls ts sg an e env (STACKS: match_stackframes s ts (fn_sig tf)) (FUN: transf_function f = OK tf) - (ANL: analyze f (pair_codes f tf) = Some an) - (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e) + (ANL: analyze f env (pair_codes f tf) = Some an) + (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e) + (WTF: wt_function f env) + (WTRS: wt_regset env rs) + (WTRES: subtype (proj_sig_res sg) (env res) = true) (STEPS: forall v ls1 m, Val.lessdef_list (encode_long (sig_res sg) v) (map ls1 (map R (loc_result sg))) -> + Val.has_type v (env res) -> agree_callee_save ls ls1 -> exists ls2, star LTL.step tge (Block ts tf sp bb ls1 m) @@ -1540,13 +1555,15 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa Inductive match_states: RTL.state -> LTL.state -> Prop := | match_states_intro: - forall s f sp pc rs m ts tf ls m' an e + forall s f sp pc rs m ts tf ls m' an e env (STACKS: match_stackframes s ts (fn_sig tf)) (FUN: transf_function f = OK tf) - (ANL: analyze f (pair_codes f tf) = Some an) - (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e) + (ANL: analyze f env (pair_codes f tf) = Some an) + (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e) (SAT: satisf rs ls e) - (MEM: Mem.extends m m'), + (MEM: Mem.extends m m') + (WTF: wt_function f env) + (WTRS: wt_regset env rs), match_states (RTL.State s f sp pc rs m) (LTL.State ts tf sp pc ls m') | match_states_call: @@ -1555,7 +1572,8 @@ Inductive match_states: RTL.state -> LTL.state -> Prop := (FUN: transf_fundef f = OK tf) (ARGS: Val.lessdef_list args (decode_longs (sig_args (funsig tf)) (map ls (loc_arguments (funsig tf))))) (AG: agree_callee_save (parent_locset ts) ls) - (MEM: Mem.extends m m'), + (MEM: Mem.extends m m') + (WTARGS: Val.has_type_list args (sig_args (funsig tf))), match_states (RTL.Callstate s f args m) (LTL.Callstate ts tf ls m') | match_states_return: @@ -1563,7 +1581,8 @@ Inductive match_states: RTL.state -> LTL.state -> Prop := (STACKS: match_stackframes s ts sg) (RES: Val.lessdef_list (encode_long (sig_res sg) res) (map ls (map R (loc_result sg)))) (AG: agree_callee_save (parent_locset ts) ls) - (MEM: Mem.extends m m'), + (MEM: Mem.extends m m') + (WTRES: Val.has_type res (proj_sig_res sg)), match_states (RTL.Returnstate s res m) (LTL.Returnstate ts ls m'). @@ -1576,13 +1595,14 @@ Proof. intros. inv H. constructor. congruence. econstructor; eauto. + unfold proj_sig_res in *. rewrite H0; auto. intros. unfold loc_result in H; rewrite H0 in H; eauto. Qed. Ltac UseShape := match goal with - | [ CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ = OK _ |- _ ] => - destruct (invert_code _ _ _ _ _ _ CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR); + | [ WT: wt_function _ _, CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ _ = OK _ |- _ ] => + destruct (invert_code _ _ _ _ _ _ _ WT CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI); inv EBS; unfold transfer_aux in TR; MonadInv end. @@ -1599,8 +1619,10 @@ Proof. { generalize args (type_of_addressing addr) H0 H1 H5. induction args0; simpl; intros. contradiction. - destruct l. discriminate. inv H4. - destruct H2. subst a. apply H3; auto with coqlib. + destruct l. discriminate. InvBooleans. + destruct H2. subst a. + assert (t = Tint) by auto with coqlib. subst t. + destruct (env r); auto || discriminate. eauto with coqlib. } red; intros; subst r. rewrite H in H8; discriminate. @@ -1610,11 +1632,11 @@ Qed. "plus" kind. *) Lemma step_simulation: - forall S1 t S2, RTL.step ge S1 t S2 -> wt_state S1 -> + forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> exists S2', plus LTL.step tge S1' t S2' /\ match_states S2 S2'. Proof. - induction 1; intros WT S1' MS; inv MS; try UseShape. + induction 1; intros S1' MS; inv MS; try UseShape. (* nop *) exploit exec_moves; eauto. intros [ls1 [X Y]]. @@ -1626,7 +1648,8 @@ Proof. econstructor; eauto. (* op move *) -- simpl in H0. inv H0. +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + simpl in H0. inv H0. exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -1637,7 +1660,8 @@ Proof. econstructor; eauto. (* op makelong *) -- simpl in H0. inv H0. +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + simpl in H0. inv H0. exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -1649,7 +1673,8 @@ Proof. econstructor; eauto. (* op lowlong *) -- simpl in H0. inv H0. +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + simpl in H0. inv H0. exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -1661,7 +1686,8 @@ Proof. econstructor; eauto. (* op highlong *) -- simpl in H0. inv H0. +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + simpl in H0. inv H0. exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -1673,7 +1699,8 @@ Proof. econstructor; eauto. (* op regular *) -- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. exploit transfer_use_def_satisf; eauto. intros [X Y]. exploit eval_operation_lessdef; eauto. intros [v' [F G]]. exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. @@ -1697,9 +1724,11 @@ Proof. eapply reg_unconstrained_satisf; eauto. intros [enext [U V]]. econstructor; eauto. + eapply wt_exec_Iop; eauto. (* load regular *) -- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. exploit transfer_use_def_satisf; eauto. intros [X Y]. exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. exploit Mem.loadv_extends; eauto. intros [v' [P Q]]. @@ -1715,7 +1744,8 @@ Proof. econstructor; eauto. (* load pair *) -- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. + exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. @@ -1736,8 +1766,7 @@ Proof. assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')). { replace (rs##args) with ((rs#dst<-v)##args). eapply add_equations_lessdef; eauto. - apply list_map_exten; intros. rewrite Regmap.gso; auto. - exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). + apply list_map_exten; intros. rewrite Regmap.gso; auto. eapply addressing_not_long; eauto. } exploit eval_addressing_lessdef. eexact LD3. @@ -1769,7 +1798,8 @@ Proof. econstructor; eauto. (* load first word of a pair *) -- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. + exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. @@ -1799,7 +1829,8 @@ Proof. econstructor; eauto. (* load second word of a pair *) -- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. + exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. @@ -1839,6 +1870,7 @@ Proof. eapply reg_unconstrained_satisf; eauto. intros [enext [U V]]. econstructor; eauto. + eapply wt_exec_Iload; eauto. (* store *) - exploit exec_moves; eauto. intros [ls1 [X Y]]. @@ -1918,19 +1950,21 @@ Proof. exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]]. econstructor; eauto. econstructor; eauto. + inv WTI. rewrite SIG. auto. intros. exploit (exec_moves mv2). eauto. eauto. eapply function_return_satisf with (v := v) (ls_before := ls1) (ls_after := ls0); eauto. eapply add_equation_ros_satisf; eauto. eapply add_equations_args_satisf; eauto. congruence. + apply wt_regset_assign; auto. intros [ls2 [A2 B2]]. exists ls2; split. eapply star_right. eexact A2. constructor. traceEq. apply satisf_incr with eafter; auto. rewrite SIG. eapply add_equations_args_lessdef; eauto. - exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). - inv WTI. rewrite <- H7. apply wt_regset_list; auto. + inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. simpl. red; auto. + inv WTI. rewrite SIG. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. (* tailcall *) - set (sg := RTL.funsig fd) in *. @@ -1951,16 +1985,16 @@ Proof. eapply match_stackframes_change_sig; eauto. rewrite SIG. rewrite e0. decEq. destruct (transf_function_inv _ _ FUN); auto. rewrite SIG. rewrite return_regs_arg_values; auto. eapply add_equations_args_lessdef; eauto. - exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). - inv WTI. rewrite <- H6. apply wt_regset_list; auto. + inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. apply return_regs_agree_callee_save. + rewrite SIG. inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. (* builtin *) -- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. +- assert (WTRS': wt_regset env (rs#res <- v)) by (eapply wt_exec_Ibuiltin; eauto). + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto. - exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). - inv WTI. rewrite <- H4. apply wt_regset_list; auto. + inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. intros [v' [m'' [F [G [J K]]]]]. assert (E: map ls1 (map R args') = reglist ls1 args'). { unfold reglist. rewrite list_map_compose. auto. } @@ -1990,8 +2024,7 @@ Proof. (* annot *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto. - exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). - inv WTI. simpl in H4. rewrite <- H4. apply wt_regset_list; auto. + inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. intros [v' [m'' [F [G [J K]]]]]. assert (v = Vundef). red in H0; inv H0. auto. econstructor; split. @@ -2009,6 +2042,7 @@ Proof. econstructor; eauto. change (destroyed_by_builtin (EF_annot txt typ)) with (@nil mreg). simpl. subst v. assumption. + apply wt_regset_assign; auto. subst v. constructor. (* cond *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. @@ -2040,43 +2074,45 @@ Proof. (* return *) - destruct (transf_function_inv _ _ FUN). - exploit Mem.free_parallel_extends; eauto. rewrite H9. intros [m'' [P Q]]. - destruct or as [r|]; MonadInv. + exploit Mem.free_parallel_extends; eauto. rewrite H10. intros [m'' [P Q]]. + inv WTI; MonadInv. + (* without an argument *) ++ exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact A1. + econstructor. eauto. eauto. traceEq. + simpl. econstructor; eauto. + unfold encode_long, loc_result. rewrite <- H11; rewrite H13. simpl; auto. + apply return_regs_agree_callee_save. + constructor. (* with an argument *) + exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact A1. econstructor. eauto. eauto. traceEq. - simpl. econstructor; eauto. rewrite <- H10. + simpl. econstructor; eauto. rewrite <- H11. replace (map (return_regs (parent_locset ts) ls1) (map R (loc_result (RTL.fn_sig f)))) with (map ls1 (map R (loc_result (RTL.fn_sig f)))). eapply add_equations_res_lessdef; eauto. rewrite !list_map_compose. apply list_map_exten; intros. unfold return_regs. apply pred_dec_true. eapply loc_result_caller_save; eauto. apply return_regs_agree_callee_save. - - (* without an argument *) -+ assert (SG: f.(RTL.fn_sig).(sig_res) = None). - { exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). - inv WTI; auto. } - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact A1. - econstructor. eauto. eauto. traceEq. - simpl. econstructor; eauto. - unfold encode_long, loc_result. rewrite <- H10. rewrite SG. simpl; auto. - apply return_regs_agree_callee_save. + unfold proj_sig_res. rewrite <- H11; rewrite H13. + eapply Val.has_subtype; eauto. (* internal function *) - monadInv FUN. simpl in *. destruct (transf_function_inv _ _ EQ). - exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H7; apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H8; apply Zle_refl. intros [m'' [U V]]. + assert (WTRS: wt_regset env (init_regs args (fn_params f))). + { apply wt_init_regs. inv H0. eapply Val.has_subtype_list; eauto. congruence. } exploit (exec_moves mv). eauto. eauto. eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto. - rewrite call_regs_param_values. rewrite H8. eexact ARGS. + rewrite call_regs_param_values. rewrite H9. eexact ARGS. + exact WTRS. intros [ls1 [A B]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -2108,13 +2144,15 @@ Proof. exploit list_in_map_inv; eauto. intros [r [A B]]; subst l'. destruct l; simpl; auto. red; intros; subst r0; elim H0. eapply loc_result_caller_save; eauto. + simpl. eapply external_call_well_typed; eauto. (* return *) - inv STACKS. - exploit STEPS; eauto. intros [ls2 [A B]]. + exploit STEPS; eauto. eapply Val.has_subtype; eauto. intros [ls2 [A B]]. econstructor; split. eapply plus_left. constructor. eexact A. traceEq. econstructor; eauto. + apply wt_regset_assign; auto. eapply Val.has_subtype; eauto. Qed. Lemma initial_states_simulation: @@ -2135,6 +2173,7 @@ Proof. rewrite SIG; rewrite H3; simpl; auto. red; auto. apply Mem.extends_refl. + rewrite SIG; rewrite H3; simpl; auto. Qed. Lemma final_states_simulation: @@ -2146,31 +2185,14 @@ Proof. unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. inv H3; auto. Qed. -Lemma wt_prog: wt_program prog. -Proof. - red; intros. exploit transform_partial_program_succeeds; eauto. - intros [tfd TF]. destruct f; simpl in *. -- monadInv TF. unfold transf_function in EQ. - destruct (type_function f) as [env|] eqn:TF; try discriminate. - econstructor. eapply type_function_correct; eauto. -- constructor. -Qed. - Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (LTL.semantics tprog). Proof. - set (ms := fun s s' => wt_state s /\ match_states s s'). - eapply forward_simulation_plus with (match_states := ms). -- exact symbols_preserved. -- intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. - exists st2; split; auto. split; auto. - apply wt_initial_state with (p := prog); auto. exact wt_prog. -- intros. destruct H. eapply final_states_simulation; eauto. -- intros. destruct H0. - exploit step_simulation; eauto. intros [s2' [A B]]. - exists s2'; split. exact A. split. - eapply subject_reduction; eauto. eexact wt_prog. eexact H. - auto. + eapply forward_simulation_plus. + eexact symbols_preserved. + eexact initial_states_simulation. + eexact final_states_simulation. + exact step_simulation. Qed. End PRESERVATION. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index f1e3d41..73c5453 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -10,26 +10,20 @@ (* *) (* *********************************************************************) -(** Type-checking Linear code. *) +(** Typing rules for Linear. *) -Require Import FSets. -Require FSetAVL. Require Import Coqlib. -Require Import Ordered. -Require Import Maps. -Require Import Iteration. Require Import AST. Require Import Integers. Require Import Values. Require Import Events. Require Import Op. -Require Import Machregs. Require Import Locations. Require Import Conventions. Require Import LTL. Require Import Linear. -(** The typechecker for Linear enforce several properties useful for +(** The typing rules for Linear enforce several properties useful for the proof of the [Stacking] pass: - for each instruction, the type of the result register or slot agrees with the type of values produced by the instruction; @@ -37,120 +31,13 @@ Require Import Linear. accessed through [Lgetstack] and [Lsetstack] Linear instructions. *) -(** * Tracking the flow of single-precision floats *) - -(** At each program point, we infer a set of machine registers - that are guaranteed to contain single-precision floats. - The inference is a simple forward dataflow analysis, iterating on the - list of instructions until a fixpoint is reached. The result of - the analysis is a map from labels to sets of machine registers - containing single-precision floats. *) - -Module OrderedMreg := OrderedIndexed(IndexedMreg). -Module Regset := FSetAVL.Make(OrderedMreg). - -Definition setreg (fs: Regset.t) (r: mreg) (t: typ) := - if typ_eq t Tsingle then Regset.add r fs else Regset.remove r fs. - -Fixpoint setregs (fs: Regset.t) (rl: list mreg) (tl: list typ) := - match rl, tl with - | nil, nil => fs - | r1 :: rs, t1 :: ts => setregs (setreg fs r1 t1) rs ts - | _, _ => fs - end. - -Definition copyreg (fs: Regset.t) (rd rs: mreg) := - if Regset.mem rs fs then Regset.add rd fs else Regset.remove rd fs. - -Definition allregs := - List.fold_right Regset.add Regset.empty - (float_caller_save_regs ++ float_callee_save_regs). - -Definition destroyed_at_call_regs := - List.fold_right Regset.add Regset.empty destroyed_at_call. - -Definition callregs (fs: Regset.t) := - Regset.diff fs destroyed_at_call_regs. - -Definition labelmap := PMap.t Regset.t. - -Definition update_label (lbl: label) (fs: Regset.t) (lm: labelmap) : Regset.t * labelmap * bool := - let fs1 := PMap.get lbl lm in - if Regset.subset fs1 fs - then (fs1, lm, false) - else let fs2 := Regset.inter fs fs1 in (fs2, PMap.set lbl fs2 lm, true). - -Fixpoint update_labels (lbls: list label) (fs: Regset.t) (lm: labelmap): labelmap * bool := - match lbls with - | nil => (lm, false) - | lbl1 :: lbls => - let '(fs1, lm1, changed1) := update_label lbl1 fs lm in - let '(lm2, changed2) := update_labels lbls fs lm1 in - (lm2, changed1 || changed2) - end. - -Fixpoint ana_code (lm: labelmap) (ch: bool) (fs: Regset.t) (c: code) : labelmap * bool := - match c with - | nil => (lm, ch) - | Lgetstack sl ofs ty rd :: c => - ana_code lm ch (setreg fs rd ty) c - | Lsetstack rs sl ofs ty :: c => - ana_code lm ch fs c - | Lop op args dst :: c => - match is_move_operation op args with - | Some src => ana_code lm ch (copyreg fs dst src) c - | None => ana_code lm ch (setreg fs dst (snd (type_of_operation op))) c - end - | Lload chunk addr args dst :: c => - ana_code lm ch (setreg fs dst (type_of_chunk chunk)) c - | Lstore chunk addr args src :: c => - ana_code lm ch fs c - | Lcall sg ros :: c => - ana_code lm ch (callregs fs) c - | Ltailcall sg ros :: c => - ana_code lm ch allregs c - | Lbuiltin ef args res :: c => - ana_code lm ch (setregs fs res (proj_sig_res' (ef_sig ef))) c - | Lannot ef args :: c => - ana_code lm ch fs c - | Llabel lbl :: c => - let '(fs1, lm1, ch1) := update_label lbl fs lm in - ana_code lm1 (ch || ch1) fs1 c - | Lgoto lbl :: c => - let '(fs1, lm1, ch1) := update_label lbl fs lm in - ana_code lm1 (ch || ch1) allregs c - | Lcond cond args lbl :: c => - let '(fs1, lm1, ch1) := update_label lbl fs lm in - ana_code lm1 (ch || ch1) fs c - | Ljumptable r lbls :: c => - let '(lm1, ch1) := update_labels lbls fs lm in - ana_code lm1 (ch || ch1) allregs c - | Lreturn :: c => - ana_code lm ch allregs c - end. - -Definition ana_iter (c: code) (lm: labelmap) : labelmap + labelmap := - let '(lm1, ch) := ana_code lm false Regset.empty c in - if ch then inr _ lm1 else inl _ lm. - -Definition ana_function (f: function): option (PMap.t Regset.t) := - PrimIter.iterate _ _ (ana_iter f.(fn_code)) (PMap.init allregs). - -(** * The type-checker *) - -(** The typing rules are presented as boolean-valued functions so that we +(** The rules are presented as boolean-valued functions so that we get an executable type-checker for free. *) Section WT_INSTR. Variable funct: function. -Variable lm: labelmap. - -Definition reg_type (fs: Regset.t) (r: mreg) := - let ty := mreg_type r in - if typ_eq ty Tfloat && Regset.mem r fs then Tsingle else ty. - Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool := match sl with | Local => zle 0 ofs @@ -176,579 +63,116 @@ Definition loc_valid (l: loc) : bool := | S _ _ _ => false end. -Fixpoint wt_code (fs: Regset.t) (c: code) : bool := - match c with - | nil => true - | Lgetstack sl ofs ty rd :: c => - subtype ty (mreg_type rd) && slot_valid sl ofs ty && - wt_code (setreg fs rd ty) c - | Lsetstack rs sl ofs ty :: c => - subtype (reg_type fs rs) ty && - slot_valid sl ofs ty && slot_writable sl && - wt_code fs c - | Lop op args dst :: c => +Definition wt_instr (i: instruction) : bool := + match i with + | Lgetstack sl ofs ty r => + subtype ty (mreg_type r) && slot_valid sl ofs ty + | Lsetstack r sl ofs ty => + slot_valid sl ofs ty && slot_writable sl + | Lop op args res => match is_move_operation op args with - | Some src => - typ_eq (mreg_type src) (mreg_type dst) && - wt_code (copyreg fs dst src) c - | None => - let (ty_args, ty_res) := type_of_operation op in - subtype ty_res (mreg_type dst) && - wt_code (setreg fs dst ty_res) c + | Some arg => + subtype (mreg_type arg) (mreg_type res) + | None => + let (targs, tres) := type_of_operation op in + subtype tres (mreg_type res) end - | Lload chunk addr args dst :: c => - subtype (type_of_chunk chunk) (mreg_type dst) && - wt_code (setreg fs dst (type_of_chunk chunk)) c - | Lstore chunk addr args src :: c => - wt_code fs c - | Lcall sg ros :: c => - wt_code (callregs fs) c - | Ltailcall sg ros :: c => - zeq (size_arguments sg) 0 && - wt_code allregs c - | Lbuiltin ef args res :: c => - let ty_res := proj_sig_res' (ef_sig ef) in - subtype_list ty_res (map mreg_type res) && - wt_code (setregs fs res ty_res) c - | Lannot ef args :: c => - forallb loc_valid args && - wt_code fs c - | Llabel lbl :: c => - let fs1 := PMap.get lbl lm in - Regset.subset fs1 fs && wt_code fs1 c - | Lgoto lbl :: c => - let fs1 := PMap.get lbl lm in - Regset.subset fs1 fs && wt_code allregs c - | Lcond cond args lbl :: c => - let fs1 := PMap.get lbl lm in - Regset.subset fs1 fs && wt_code fs c - | Ljumptable r lbls :: c => - forallb (fun lbl => Regset.subset (PMap.get lbl lm) fs) lbls && - wt_code allregs c - | Lreturn :: c => - wt_code allregs c + | Lload chunk addr args dst => + subtype (type_of_chunk chunk) (mreg_type dst) + | Ltailcall sg ros => + zeq (size_arguments sg) 0 + | Lbuiltin ef args res => + subtype_list (proj_sig_res' (ef_sig ef)) (map mreg_type res) + | Lannot ef args => + forallb loc_valid args + | _ => + true end. -Remark wt_code_cons: - forall fs i c, - wt_code fs (i :: c) = true -> exists fs', wt_code fs' c = true. -Proof. - simpl; intros. destruct i; InvBooleans; try (econstructor; eassumption). - destruct (is_move_operation o l). - InvBooleans; econstructor; eassumption. - destruct (type_of_operation o). InvBooleans; econstructor; eassumption. -Qed. - -Lemma wt_find_label: - forall lbl c' c fs, - find_label lbl c = Some c' -> - wt_code fs c = true -> - wt_code (PMap.get lbl lm) c' = true. -Proof. - induction c; intros. -- discriminate. -- simpl in H. specialize (is_label_correct lbl a). destruct (is_label lbl a); intros IL. - + subst a. simpl in H0. inv H. InvBooleans. auto. - + destruct (wt_code_cons _ _ _ H0) as [fs' WT]. eauto. -Qed. - End WT_INSTR. -Definition wt_funcode (f: function) (lm: labelmap) : bool := - wt_code f lm Regset.empty f.(fn_code). +Definition wt_code (f: function) (c: code) : bool := + forallb (wt_instr f) c. Definition wt_function (f: function) : bool := - match ana_function f with - | None => false - | Some lm => wt_funcode f lm - end. + wt_code f f.(fn_code). -(** * Soundness of the type system *) +(** Typing the run-time state. These definitions are used in [Stackingproof]. *) Require Import Values. -Require Import Globalenvs. -Require Import Memory. -Module RSF := FSetFacts.Facts(Regset). - -(** ** Typing the run-time state *) - -Definition loc_type (fs: Regset.t) (l: loc): typ := - match l with - | R r => reg_type fs r - | S sl ofs ty => ty - end. - -Definition wt_locset (fs: Regset.t) (ls: locset) : Prop := - forall l, Val.has_type (ls l) (loc_type fs l). - -Remark subtype_refl: - forall ty, subtype ty ty = true. -Proof. - destruct ty; reflexivity. -Qed. - -Remark reg_type_sub: - forall fs r, subtype (reg_type fs r) (mreg_type r) = true. -Proof. - intros. unfold reg_type. destruct (typ_eq (mreg_type r) Tfloat); simpl. - rewrite e. destruct (Regset.mem r fs); auto. - apply subtype_refl. -Qed. - -Lemma wt_mreg: - forall fs ls r, wt_locset fs ls -> Val.has_type (ls (R r)) (mreg_type r). -Proof. - intros. eapply Val.has_subtype. apply reg_type_sub with (fs := fs). apply H. -Qed. - -Lemma wt_locset_empty: - forall ls, - (forall l, Val.has_type (ls l) (Loc.type l)) -> - wt_locset Regset.empty ls. -Proof. - intros; red; intros. destruct l; simpl. -- unfold reg_type. change (Regset.mem r Regset.empty) with false. - rewrite andb_false_r. apply H. -- apply H. -Qed. - -Remark reg_type_mon: - forall fs1 fs2 r, Regset.Subset fs2 fs1 -> subtype (reg_type fs1 r) (reg_type fs2 r) = true. -Proof. - intros. unfold reg_type. destruct (typ_eq (mreg_type r) Tfloat); simpl. - rewrite e. destruct (Regset.mem r fs2) eqn:E. - rewrite Regset.mem_1. auto. apply H. apply Regset.mem_2; auto. - destruct (Regset.mem r fs1); auto. - apply subtype_refl. -Qed. - -Lemma wt_locset_mon: - forall fs1 fs2 ls, - Regset.Subset fs2 fs1 -> wt_locset fs1 ls -> wt_locset fs2 ls. -Proof. - intros; red; intros. apply Val.has_subtype with (loc_type fs1 l); auto. - unfold loc_type. destruct l. apply reg_type_mon; auto. apply subtype_refl. -Qed. +Definition wt_locset (ls: locset) : Prop := + forall l, Val.has_type (ls l) (Loc.type l). Lemma wt_setreg: - forall fs ls r v ty, - Val.has_type v ty -> subtype ty (mreg_type r) = true -> wt_locset fs ls -> - wt_locset (setreg fs r ty) (Locmap.set (R r) v ls). + forall ls r v, + Val.has_type v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls). Proof. intros; red; intros. - unfold Locmap.set. destruct (Loc.eq (R r) l). -- subst l. simpl. unfold reg_type, setreg. - destruct (typ_eq (mreg_type r) Tfloat && - Regset.mem r - (if typ_eq ty Tsingle then Regset.add r fs else Regset.remove r fs)) eqn:E. -+ InvBooleans. destruct (typ_eq ty Tsingle). - congruence. - rewrite RSF.remove_b in H3. unfold RSF.eqb in H3. rewrite dec_eq_true in H3. - simpl in H3. rewrite andb_false_r in H3. discriminate. -+ eapply Val.has_subtype; eauto. -- destruct (Loc.diff_dec (R r) l). -+ replace (loc_type (setreg fs r ty) l) with (loc_type fs l). - apply H1. - unfold loc_type, setreg. destruct l; auto. destruct (typ_eq ty Tsingle). - unfold reg_type. rewrite RSF.add_neq_b. auto. congruence. - unfold reg_type. rewrite RSF.remove_neq_b. auto. congruence. -+ red; auto. -Qed. - -Lemma wt_copyreg: - forall fs ls src dst v, - mreg_type src = mreg_type dst -> - wt_locset fs ls -> - Val.has_type v (reg_type fs src) -> - wt_locset (copyreg fs dst src) (Locmap.set (R dst) v ls). -Proof. - intros; red; intros. - unfold Locmap.set. destruct (Loc.eq (R dst) l). -- subst l. simpl. unfold reg_type, copyreg. - unfold reg_type in H1. rewrite H in H1. - destruct (Regset.mem src fs) eqn:SRC. - rewrite RSF.add_b. unfold RSF.eqb. rewrite dec_eq_true. simpl. auto. - rewrite RSF.remove_b. unfold RSF.eqb. rewrite dec_eq_true. simpl. rewrite ! andb_false_r. - rewrite andb_false_r in H1. auto. -- destruct (Loc.diff_dec (R dst) l). -+ replace (loc_type (copyreg fs dst src) l) with (loc_type fs l). - apply H0. - unfold loc_type, copyreg. destruct l; auto. destruct (Regset.mem src fs). - unfold reg_type. rewrite RSF.add_neq_b. auto. congruence. - unfold reg_type. rewrite RSF.remove_neq_b. auto. congruence. -+ red; auto. + unfold Locmap.set. + destruct (Loc.eq (R r) l). + subst l; auto. + destruct (Loc.diff_dec (R r) l). auto. red. auto. Qed. Lemma wt_setstack: - forall fs ls sl ofs ty v, - Val.has_type v ty -> wt_locset fs ls -> - wt_locset fs (Locmap.set (S sl ofs ty) v ls). + forall ls sl ofs ty v, + wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls). Proof. intros; red; intros. unfold Locmap.set. destruct (Loc.eq (S sl ofs ty) l). - subst l. simpl. auto. + subst l. simpl. + generalize (Val.load_result_type (chunk_of_type ty) v). + replace (type_of_chunk (chunk_of_type ty)) with ty. auto. + destruct ty; reflexivity. destruct (Loc.diff_dec (S sl ofs ty) l). auto. red. auto. Qed. -Lemma wt_undef: - forall fs ls l, wt_locset fs ls -> wt_locset fs (Locmap.set l Vundef ls). -Proof. - intros; red; intros. unfold Locmap.set. - destruct (Loc.eq l l0). red; auto. - destruct (Loc.diff_dec l l0); auto. red; auto. -Qed. - Lemma wt_undef_regs: - forall fs rs ls, wt_locset fs ls -> wt_locset fs (undef_regs rs ls). + forall rs ls, wt_locset ls -> wt_locset (undef_regs rs ls). Proof. - induction rs; simpl; intros. auto. apply wt_undef; auto. + induction rs; simpl; intros. auto. apply wt_setreg; auto. red; auto. Qed. Lemma wt_call_regs: - forall fs ls, wt_locset fs ls -> wt_locset Regset.empty (call_regs ls). + forall ls, wt_locset ls -> wt_locset (call_regs ls). Proof. - intros; red; intros. unfold call_regs. destruct l. - eapply Val.has_subtype; eauto. unfold loc_type. apply reg_type_mon. - red; intros. eelim Regset.empty_1; eauto. + intros; red; intros. unfold call_regs. destruct l. auto. destruct sl. red; auto. - change (loc_type Regset.empty (S Incoming pos ty)) - with (loc_type fs (S Outgoing pos ty)). auto. + change (Loc.type (S Incoming pos ty)) with (Loc.type (S Outgoing pos ty)). auto. red; auto. Qed. -Remark set_from_list: - forall r l, Regset.In r (List.fold_right Regset.add Regset.empty l) <-> In r l. -Proof. - induction l; simpl. -- rewrite RSF.empty_iff. tauto. -- rewrite RSF.add_iff. rewrite IHl. tauto. -Qed. - Lemma wt_return_regs: - forall fs caller callee, - wt_locset fs caller -> wt_locset Regset.empty callee -> - wt_locset (callregs fs) (return_regs caller callee). + forall caller callee, + wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee). Proof. intros; red; intros. - unfold return_regs. destruct l. -- destruct (in_dec mreg_eq r destroyed_at_call). -+ unfold loc_type. replace (reg_type (callregs fs) r) with (mreg_type r). - eapply Val.has_subtype. eapply reg_type_sub. apply (H0 (R r)). - unfold reg_type, callregs. rewrite RSF.diff_b. - rewrite (@Regset.mem_1 destroyed_at_call_regs). - rewrite ! andb_false_r. auto. - unfold destroyed_at_call_regs; apply set_from_list; auto. -+ unfold loc_type, reg_type, callregs. rewrite RSF.diff_b. - destruct (Regset.mem r destroyed_at_call_regs) eqn:E. - elim n. apply set_from_list. apply Regset.mem_2; auto. - rewrite andb_true_r. apply H. -- unfold loc_type. apply H. + unfold return_regs. destruct l; auto. + destruct (in_dec mreg_eq r destroyed_at_call); auto. Qed. Lemma wt_init: - forall fs, wt_locset fs (Locmap.init Vundef). + wt_locset (Locmap.init Vundef). Proof. red; intros. unfold Locmap.init. red; auto. Qed. -Lemma wt_setregs: - forall vl tyl rl fs rs, - Val.has_type_list vl tyl -> - subtype_list tyl (map mreg_type rl) = true -> - wt_locset fs rs -> - wt_locset (setregs fs rl tyl) (Locmap.setlist (map R rl) vl rs). -Proof. - induction vl; simpl; intros. -- destruct tyl; try contradiction. destruct rl; try discriminate. - simpl. auto. -- destruct tyl as [ | ty tyl]; try contradiction. destruct H. - destruct rl as [ | r rl]; simpl in H0; try discriminate. InvBooleans. - simpl. eapply IHvl; eauto. eapply wt_setreg; eauto. -Qed. - -Lemma wt_setregs_result: - forall sg fs v rl rs, +Lemma wt_setlist_result: + forall sg v rs, Val.has_type v (proj_sig_res sg) -> - subtype_list (proj_sig_res' sg) (map mreg_type rl) = true -> - wt_locset fs rs -> - wt_locset (setregs fs rl (proj_sig_res' sg)) - (Locmap.setlist (map R rl) (encode_long (sig_res sg) v) rs). -Proof. - intros. eapply wt_setregs; eauto. - unfold proj_sig_res in H. unfold encode_long, proj_sig_res'. - destruct (sig_res sg) as [[] | ]; simpl; intuition. - destruct v; simpl; auto. - destruct v; simpl; auto. -Qed. - -Remark in_setreg_other: - forall fs r ty r', - r' <> r -> (Regset.In r' (setreg fs r ty) <-> Regset.In r' fs). -Proof. - intros. unfold setreg. destruct (typ_eq ty Tsingle). - rewrite RSF.add_iff. intuition. - rewrite RSF.remove_iff. intuition. -Qed. - -Remark in_setregs_other: - forall r rl fs tyl, - ~In r rl -> (Regset.In r (setregs fs rl tyl) <-> Regset.In r fs). -Proof. - induction rl; simpl; intros. -- destruct tyl; tauto. -- destruct tyl. tauto. rewrite IHrl by tauto. apply in_setreg_other. intuition. -Qed. - -Remark callregs_setregs_result: - forall sg fs, - Regset.Subset (callregs fs) (setregs fs (loc_result sg) (proj_sig_res' sg)). -Proof. - red; unfold callregs; intros. rewrite RSF.diff_iff in H. destruct H. - apply in_setregs_other; auto. - red; intros; elim H0. apply set_from_list. eapply loc_result_caller_save; eauto. -Qed. - -Definition wt_fundef (fd: fundef) := - match fd with - | Internal f => wt_function f = true - | External ef => True - end. - -Inductive wt_callstack: list stackframe -> Regset.t -> Prop := - | wt_callstack_nil: forall fs, - wt_callstack nil fs - | wt_callstack_cons: forall f sp rs c s fs lm fs0 fs1 - (WTSTK: wt_callstack s fs0) - (WTF: wt_funcode f lm = true) - (WTC: wt_code f lm (callregs fs1) c = true) - (WTRS: wt_locset fs rs) - (INCL: Regset.Subset (callregs fs1) (callregs fs)), - wt_callstack (Stackframe f sp rs c :: s) fs. - -Lemma wt_parent_locset: - forall s fs, wt_callstack s fs -> wt_locset fs (parent_locset s). -Proof. - induction 1; simpl. -- apply wt_init. -- auto. -Qed. - -Lemma wt_callstack_change_fs: - forall s fs, wt_callstack s fs -> wt_callstack s (callregs fs). -Proof. - induction 1. -- constructor. -- econstructor; eauto. - apply wt_locset_mon with fs; auto. - unfold callregs; red; intros. eapply Regset.diff_1; eauto. - red; intros. exploit INCL; eauto. unfold callregs. rewrite ! RSF.diff_iff. - tauto. -Qed. - -Inductive wt_state: state -> Prop := - | wt_regular_state: forall s f sp c rs m lm fs fs0 - (WTSTK: wt_callstack s fs0) - (WTF: wt_funcode f lm = true) - (WTC: wt_code f lm fs c = true) - (WTRS: wt_locset fs rs), - wt_state (State s f sp c rs m) - | wt_call_state: forall s fd rs m fs - (WTSTK: wt_callstack s fs) - (WTFD: wt_fundef fd) - (WTRS: wt_locset fs rs), - wt_state (Callstate s fd rs m) - | wt_return_state: forall s rs m fs - (WTSTK: wt_callstack s fs) - (WTRS: wt_locset (callregs fs) rs), - wt_state (Returnstate s rs m). - -(** ** Preservation of state typing by transitions *) - -Section SOUNDNESS. - -Variable prog: program. -Let ge := Genv.globalenv prog. - -Hypothesis wt_prog: - forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd. - -Lemma wt_find_function: - forall ros rs f, find_function ge ros rs = Some f -> wt_fundef f. -Proof. - intros. - assert (X: exists i, In (i, Gfun f) prog.(prog_defs)). - { - destruct ros as [r | s]; simpl in H. - eapply Genv.find_funct_inversion; eauto. - destruct (Genv.find_symbol ge s) as [b|]; try discriminate. - eapply Genv.find_funct_ptr_inversion; eauto. - } - destruct X as [i IN]. eapply wt_prog; eauto. -Qed. - -Theorem step_type_preservation: - forall S1 t S2, step ge S1 t S2 -> wt_state S1 -> wt_state S2. -Proof. - induction 1; intros WTS; inv WTS. -- (* getstack *) - simpl in WTC; InvBooleans. - econstructor; eauto. - apply wt_setreg; auto. apply (WTRS (S sl ofs ty)). apply wt_undef_regs; auto. -- (* setstack *) - simpl in WTC; InvBooleans. - econstructor; eauto. - apply wt_setstack; auto. eapply Val.has_subtype; eauto. apply WTRS. - apply wt_undef_regs; auto. -- (* op *) - simpl in WTC. destruct (is_move_operation op args) as [src | ] eqn:ISMOVE. - + (* move *) - InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst. - simpl in H. inv H. - econstructor; eauto. - apply wt_copyreg. auto. apply wt_undef_regs; auto. apply WTRS. - + (* other ops *) - destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans. - econstructor; eauto. - apply wt_setreg; auto. - change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. - eapply type_of_operation_sound; eauto. - red; intros; subst op. simpl in ISMOVE. - destruct args; try discriminate. destruct args; discriminate. - apply wt_undef_regs; auto. -- (* load *) - simpl in WTC; InvBooleans. - econstructor; eauto. - apply wt_setreg. - destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto. - auto. - apply wt_undef_regs; auto. -- (* store *) - simpl in WTC; InvBooleans. - econstructor; eauto. - apply wt_undef_regs; auto. -- (* call *) - simpl in WTC; InvBooleans. - econstructor; eauto. econstructor; eauto. - red; auto. - eapply wt_find_function; eauto. -- (* tailcall *) - simpl in WTC; InvBooleans. - econstructor. apply wt_callstack_change_fs; eauto. - eapply wt_find_function; eauto. - apply wt_return_regs. apply wt_parent_locset; auto. - eapply wt_locset_mon; eauto. red; intros. eelim Regset.empty_1; eauto. -- (* builtin *) - simpl in WTC; InvBooleans. inv H. - econstructor; eauto. - apply wt_setregs_result; auto. - eapply external_call_well_typed; eauto. - apply wt_undef_regs; auto. -- (* annot *) - simpl in WTC; InvBooleans. - econstructor; eauto. -- (* label *) - simpl in WTC; InvBooleans. - econstructor; eauto. - eapply wt_locset_mon; eauto. apply Regset.subset_2; auto. -- (* goto *) - simpl in WTC; InvBooleans. - econstructor. eauto. eauto. - eapply wt_find_label; eauto. - eapply wt_locset_mon; eauto. apply Regset.subset_2; auto. -- (* cond branch, taken *) - simpl in WTC; InvBooleans. - econstructor. eauto. eauto. - eapply wt_find_label; eauto. - eapply wt_locset_mon. apply Regset.subset_2; eauto. - apply wt_undef_regs; auto. -- (* cond branch, not taken *) - simpl in WTC; InvBooleans. - econstructor. eauto. eauto. eauto. - apply wt_undef_regs; auto. -- (* jumptable *) - simpl in WTC; InvBooleans. - econstructor. eauto. eauto. - eapply wt_find_label; eauto. - apply wt_locset_mon with fs. - apply Regset.subset_2. rewrite List.forallb_forall in H2. apply H2. - eapply list_nth_z_in; eauto. - apply wt_undef_regs; auto. -- (* return *) - econstructor. eauto. - apply wt_return_regs. - apply wt_parent_locset; auto. - apply wt_locset_mon with fs; auto. red; intros. eelim Regset.empty_1; eauto. -- (* internal function *) - simpl in WTFD. unfold wt_function in WTFD. destruct (ana_function f) as [lm|]; try discriminate. - econstructor. eauto. eauto. eexact WTFD. - apply wt_undef_regs. eapply wt_call_regs; eauto. -- (* external function *) - inv H0. - econstructor. eauto. - eapply wt_locset_mon. 2: eapply wt_setregs_result; eauto. - apply callregs_setregs_result. - eapply external_call_well_typed; eauto. - unfold proj_sig_res', loc_result. destruct (sig_res (ef_sig ef) )as [[] | ]; auto. -- (* return *) - inv WTSTK. econstructor; eauto. - apply wt_locset_mon with (callregs fs); auto. -Qed. - -Theorem wt_initial_state: - forall S, initial_state prog S -> wt_state S. -Proof. - induction 1. econstructor. - apply wt_callstack_nil with (fs := Regset.empty). - unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto. - intros [id IN]. eapply wt_prog; eauto. - apply wt_init. -Qed. - -End SOUNDNESS. - -(** Properties of well-typed states that are used in [Stackingproof]. *) - -Lemma wt_state_getstack: - forall s f sp sl ofs ty rd c rs m, - wt_state (State s f sp (Lgetstack sl ofs ty rd :: c) rs m) -> - slot_valid f sl ofs ty = true. -Proof. - intros. inv H. simpl in WTC; InvBooleans. auto. -Qed. - -Lemma wt_state_setstack: - forall s f sp sl ofs ty r c rs m, - wt_state (State s f sp (Lsetstack r sl ofs ty :: c) rs m) -> - Val.has_type (rs (R r)) ty /\ slot_valid f sl ofs ty = true /\ slot_writable sl = true. -Proof. - intros. inv H. simpl in WTC; InvBooleans. intuition. - eapply Val.has_subtype; eauto. apply WTRS. -Qed. - -Lemma wt_state_tailcall: - forall s f sp sg ros c rs m, - wt_state (State s f sp (Ltailcall sg ros :: c) rs m) -> - size_arguments sg = 0. -Proof. - intros. inv H. simpl in WTC; InvBooleans. auto. -Qed. - -Lemma wt_state_annot: - forall s f sp ef args c rs m, - wt_state (State s f sp (Lannot ef args :: c) rs m) -> - forallb (loc_valid f) args = true. -Proof. - intros. inv H. simpl in WTC; InvBooleans. auto. -Qed. - -Lemma wt_callstate_wt_locset: - forall s f rs m, - wt_state (Callstate s f rs m) -> wt_locset Regset.empty rs. -Proof. - intros. inv H. apply wt_locset_mon with fs; auto. - red; intros; eelim Regset.empty_1; eauto. + wt_locset rs -> + wt_locset (Locmap.setlist (map R (loc_result sg)) (encode_long (sig_res sg) v) rs). +Proof. + unfold loc_result, encode_long, proj_sig_res; intros. + destruct (sig_res sg) as [[] | ]; simpl. +- apply wt_setreg; auto. +- apply wt_setreg; auto. +- destruct v; simpl in H; try contradiction; + simpl; apply wt_setreg; auto; apply wt_setreg; auto. +- apply wt_setreg; auto. apply Val.has_subtype with Tsingle; auto. +- apply wt_setreg; auto. Qed. diff --git a/backend/Locations.v b/backend/Locations.v index 96f1eba..43ce210 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -301,16 +301,29 @@ Module Locmap. Definition set (l: loc) (v: val) (m: t) : t := fun (p: loc) => - if Loc.eq l p then v - else if Loc.diff_dec l p then m p + if Loc.eq l p then + match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end + else if Loc.diff_dec l p then + m p else Vundef. Lemma gss: forall l v m, - (set l v m) l = v. + (set l v m) l = + match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end. Proof. intros. unfold set. apply dec_eq_true. Qed. + Lemma gss_reg: forall r v m, (set (R r) v m) (R r) = v. + Proof. + intros. unfold set. rewrite dec_eq_true. auto. + Qed. + + Lemma gss_typed: forall l v m, Val.has_type v (Loc.type l) -> (set l v m) l = v. + Proof. + intros. rewrite gss. destruct l. auto. apply Val.load_result_same; auto. + Qed. + Lemma gso: forall l v m p, Loc.diff l p -> (set l v m) p = m p. Proof. intros. unfold set. destruct (Loc.eq l p). @@ -336,10 +349,11 @@ Module Locmap. Proof. assert (P: forall ll l m, m l = Vundef -> (undef ll m) l = Vundef). induction ll; simpl; intros. auto. apply IHll. - unfold set. destruct (Loc.eq a l). auto. + unfold set. destruct (Loc.eq a l). + destruct a. auto. destruct ty; reflexivity. destruct (Loc.diff_dec a l); auto. induction ll; simpl; intros. contradiction. - destruct H. apply P. subst a. apply gss. + destruct H. apply P. subst a. apply gss_typed. exact I. auto. Qed. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index e8ae7ae..24f8d7b 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -14,7 +14,7 @@ Require Import Coqlib. Require Import Errors. -Require Import Unityping. +Require Import Subtyping. Require Import Maps. Require Import AST. Require Import Op. @@ -36,8 +36,7 @@ Require Import Conventions. is very simple, consisting of the four types [Tint] (for integers and pointers), [Tfloat] (for double-precision floats), [Tlong] (for 64-bit integers) and [Tsingle] (for single-precision floats). - At the RTL level, we simplify things further by equating [Tsingle] - with [Tfloat]. + The only subtlety is that [Tsingle] is a subtype of [Tfloat]. Additionally, we impose that each pseudo-register has the same type throughout the function. This requirement helps with register allocation, @@ -57,11 +56,6 @@ Require Import Conventions. which can work over both integers and floats. *) -Definition normalize (ty: typ) : typ := - match ty with Tsingle => Tfloat | _ => ty end. - -Definition normalize_list (tyl: list typ) : list typ := map normalize tyl. - Definition regenv := reg -> typ. Section WT_INSTR. @@ -79,57 +73,57 @@ Inductive wt_instr : instruction -> Prop := wt_instr (Inop s) | wt_Iopmove: forall r1 r s, - env r = env r1 -> + subtype (env r1) (env r) = true -> valid_successor s -> wt_instr (Iop Omove (r1 :: nil) r s) | wt_Iop: forall op args res s, op <> Omove -> - map env args = fst (type_of_operation op) -> - env res = normalize (snd (type_of_operation op)) -> + subtype_list (map env args) (fst (type_of_operation op)) = true -> + subtype (snd (type_of_operation op)) (env res) = true -> valid_successor s -> wt_instr (Iop op args res s) | wt_Iload: forall chunk addr args dst s, - map env args = type_of_addressing addr -> - env dst = normalize (type_of_chunk chunk) -> + subtype_list (map env args) (type_of_addressing addr) = true -> + subtype (type_of_chunk chunk) (env dst) = true -> valid_successor s -> wt_instr (Iload chunk addr args dst s) | wt_Istore: forall chunk addr args src s, - map env args = type_of_addressing addr -> - env src = type_of_chunk_use chunk -> + subtype_list (map env args) (type_of_addressing addr) = true -> + subtype (env src) (type_of_chunk_use chunk) = true -> valid_successor s -> wt_instr (Istore chunk addr args src s) | wt_Icall: forall sig ros args res s, - match ros with inl r => env r = Tint | inr s => True end -> - map env args = normalize_list sig.(sig_args) -> - env res = normalize (proj_sig_res sig) -> + match ros with inl r => subtype (env r) Tint = true | inr s => True end -> + subtype_list (map env args) sig.(sig_args) = true -> + subtype (proj_sig_res sig) (env res) = true -> valid_successor s -> wt_instr (Icall sig ros args res s) | wt_Itailcall: forall sig ros args, - match ros with inl r => env r = Tint | inr s => True end -> - map env args = normalize_list sig.(sig_args) -> + match ros with inl r => subtype (env r) Tint = true | inr s => True end -> sig.(sig_res) = funct.(fn_sig).(sig_res) -> + subtype_list (map env args) sig.(sig_args) = true -> tailcall_possible sig -> wt_instr (Itailcall sig ros args) | wt_Ibuiltin: forall ef args res s, - map env args = normalize_list (ef_sig ef).(sig_args) -> - env res = normalize (proj_sig_res (ef_sig ef)) -> + subtype_list (map env args) (ef_sig ef).(sig_args) = true -> + subtype (proj_sig_res (ef_sig ef)) (env res) = true -> valid_successor s -> wt_instr (Ibuiltin ef args res s) | wt_Icond: forall cond args s1 s2, - map env args = type_of_condition cond -> + subtype_list (map env args) (type_of_condition cond) = true -> valid_successor s1 -> valid_successor s2 -> wt_instr (Icond cond args s1 s2) | wt_Ijumptable: forall arg tbl, - env arg = Tint -> + subtype (env arg) Tint = true -> (forall s, In s tbl -> valid_successor s) -> list_length_z tbl * 4 <= Int.max_unsigned -> wt_instr (Ijumptable arg tbl) @@ -139,7 +133,7 @@ Inductive wt_instr : instruction -> Prop := | wt_Ireturn_some: forall arg ty, funct.(fn_sig).(sig_res) = Some ty -> - env arg = normalize ty -> + subtype (env arg) ty = true -> wt_instr (Ireturn (Some arg)). End WT_INSTR. @@ -152,7 +146,7 @@ End WT_INSTR. Record wt_function (f: function) (env: regenv): Prop := mk_wt_function { wt_params: - map env f.(fn_params) = normalize_list f.(fn_sig).(sig_args); + subtype_list f.(fn_sig).(sig_args) (map env f.(fn_params)) = true; wt_norepet: list_norepet f.(fn_params); wt_instrs: @@ -174,8 +168,8 @@ Definition wt_program (p: program): Prop := (** * Type inference *) -(** Type inference reuses the generic solver for unification constraints - defined in module [Unityping]. *) +(** Type inference reuses the generic solver for subtyping constraints + defined in module [Subtyping]. *) Module RTLtypes <: TYPE_ALGEBRA. @@ -183,9 +177,122 @@ Definition t := typ. Definition eq := typ_eq. Definition default := Tint. +Definition sub (t1 t2: typ): Prop := subtype t1 t2 = true. + +Lemma sub_refl: forall ty, sub ty ty. +Proof. unfold sub; destruct ty; auto. Qed. + +Lemma sub_trans: forall ty1 ty2 ty3, sub ty1 ty2 -> sub ty2 ty3 -> sub ty1 ty3. +Proof. + unfold sub; intros. destruct ty1; destruct ty2; try discriminate; destruct ty3; auto; discriminate. +Qed. + +Definition sub_dec: forall ty1 ty2, {sub ty1 ty2} + {~sub ty1 ty2}. +Proof. + unfold sub; intros. destruct (subtype ty1 ty2). left; auto. right; congruence. +Defined. + +Definition lub (ty1 ty2: typ) := + match ty1, ty2 with + | Tint, Tint => Tint + | Tlong, Tlong => Tlong + | Tfloat, Tfloat => Tfloat + | Tsingle, Tsingle => Tsingle + | Tfloat, Tsingle => Tfloat + | Tsingle, Tfloat => Tfloat + | _, _ => default + end. + +Lemma lub_left: forall x y z, sub x z -> sub y z -> sub x (lub x y). +Proof. + unfold sub, lub; intros. destruct x; destruct y; auto; destruct z; discriminate. +Qed. + +Lemma lub_right: forall x y z, sub x z -> sub y z -> sub y (lub x y). +Proof. + unfold sub, lub; intros. destruct x; destruct y; auto; destruct z; discriminate. +Qed. + +Lemma lub_min: forall x y z, sub x z -> sub y z -> sub (lub x y) z. +Proof. + unfold sub, lub; intros. destruct x; destruct z; try discriminate; destruct y; auto; discriminate. +Qed. + +Definition glb (ty1 ty2: typ) := + match ty1, ty2 with + | Tint, Tint => Tint + | Tlong, Tlong => Tlong + | Tfloat, Tfloat => Tfloat + | Tsingle, Tsingle => Tsingle + | Tfloat, Tsingle => Tsingle + | Tsingle, Tfloat => Tsingle + | _, _ => default + end. + +Lemma glb_left: forall x y z, sub z x -> sub z y -> sub (glb x y) x. +Proof. + unfold sub, glb; intros. destruct x; destruct y; auto; destruct z; discriminate. +Qed. + +Lemma glb_right: forall x y z, sub z x -> sub z y -> sub (glb x y) y. +Proof. + unfold sub, glb; intros. destruct x; destruct y; auto; destruct z; discriminate. +Qed. + +Lemma glb_max: forall x y z, sub z x -> sub z y -> sub z (glb x y). +Proof. + unfold sub, glb; intros. destruct x; destruct z; try discriminate; destruct y; auto; discriminate. +Qed. + +Definition low_bound (ty: typ) := + match ty with Tfloat => Tsingle | _ => ty end. + +Definition high_bound (ty: typ) := + match ty with Tsingle => Tfloat | _ => ty end. + +Lemma low_bound_sub: forall t, sub (low_bound t) t. +Proof. + unfold sub; destruct t0; auto. +Qed. + +Lemma low_bound_minorant: forall x y, sub x y -> sub (low_bound y) x. +Proof. + unfold sub; intros. destruct x; destruct y; auto; discriminate. +Qed. + +Lemma high_bound_sub: forall t, sub t (high_bound t). +Proof. + unfold sub; destruct t0; auto. +Qed. + +Lemma high_bound_majorant: forall x y, sub x y -> sub y (high_bound x). +Proof. + unfold sub; intros. destruct x; destruct y; auto; discriminate. +Qed. + +Definition weight (t: typ) := + match t with Tfloat => 1%nat | _ => 0%nat end. + +Definition max_weight := 1%nat. + +Lemma weight_range: forall t, (weight t <= max_weight)%nat. +Proof. + unfold max_weight; destruct t0; simpl; omega. +Qed. + +Lemma weight_sub: forall x y, sub x y -> (weight x <= weight y)%nat. +Proof. + unfold sub; intros. destruct x; destruct y; simpl; discriminate || omega. +Qed. + +Lemma weight_sub_strict: forall x y, sub x y -> x <> y -> (weight x < weight y)%nat. +Proof. + unfold sub, subtype; intros. destruct x; destruct y; simpl; congruence || omega. +Qed. + End RTLtypes. -Module S := UniSolver(RTLtypes). +Module S := SubSolver(RTLtypes). Section INFERENCE. @@ -211,7 +318,7 @@ Fixpoint check_successors (sl: list node): res unit := Definition type_ros (e: S.typenv) (ros: reg + ident) : res S.typenv := match ros with - | inl r => S.set e r Tint + | inl r => S.type_use e r Tint | inr s => OK e end. @@ -226,28 +333,28 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := do x <- check_successor s; if is_move op then match args with - | arg :: nil => do (changed, e') <- S.move e res arg; OK e' + | arg :: nil => do (changed, e') <- S.type_move e arg res; OK e' | _ => Error (msg "ill-formed move") end else (let (targs, tres) := type_of_operation op in - do e1 <- S.set_list e args targs; S.set e1 res (normalize tres)) + do e1 <- S.type_uses e args targs; S.type_def e1 res tres) | Iload chunk addr args dst s => do x <- check_successor s; - do e1 <- S.set_list e args (type_of_addressing addr); - S.set e1 dst (normalize (type_of_chunk chunk)) + do e1 <- S.type_uses e args (type_of_addressing addr); + S.type_def e1 dst (type_of_chunk chunk) | Istore chunk addr args src s => do x <- check_successor s; - do e1 <- S.set_list e args (type_of_addressing addr); - S.set e1 src (type_of_chunk_use chunk) + do e1 <- S.type_uses e args (type_of_addressing addr); + S.type_use e1 src (type_of_chunk_use chunk) | Icall sig ros args res s => do x <- check_successor s; do e1 <- type_ros e ros; - do e2 <- S.set_list e1 args (normalize_list sig.(sig_args)); - S.set e2 res (normalize (proj_sig_res sig)) + do e2 <- S.type_uses e1 args sig.(sig_args); + S.type_def e2 res (proj_sig_res sig) | Itailcall sig ros args => do e1 <- type_ros e ros; - do e2 <- S.set_list e1 args (normalize_list sig.(sig_args)); + do e2 <- S.type_uses e1 args sig.(sig_args); if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then if tailcall_is_possible sig then OK e2 @@ -256,48 +363,45 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := | Ibuiltin ef args res s => let sig := ef_sig ef in do x <- check_successor s; - do e1 <- S.set_list e args (normalize_list sig.(sig_args)); - S.set e1 res (normalize (proj_sig_res sig)) - | Icond cond args s1 s2 => + do e1 <- S.type_uses e args sig.(sig_args); + S.type_def e1 res (proj_sig_res sig) + | Icond cond args s1 s2 => do x1 <- check_successor s1; do x2 <- check_successor s2; - S.set_list e args (type_of_condition cond) - | Ijumptable arg tbl => + S.type_uses e args (type_of_condition cond) + | Ijumptable arg tbl => do x <- check_successors tbl; - do e1 <- S.set e arg Tint; - if zle (list_length_z tbl * 4) Int.max_unsigned - then OK e1 - else Error(msg "jumptable too big") + do e1 <- S.type_use e arg Tint; + if zle (list_length_z tbl * 4) Int.max_unsigned then OK e1 else Error(msg "jumptable too big") | Ireturn optres => match optres, f.(fn_sig).(sig_res) with | None, None => OK e - | Some r, Some t => S.set e r (normalize t) + | Some r, Some t => S.type_use e r t | _, _ => Error(msg "bad return") end end. Definition type_code (e: S.typenv): res S.typenv := - PTree.fold (fun re pc i => - match re with - | Error _ => re - | OK e => - match type_instr e i with - | Error msg => Error(MSG "At PC " :: POS pc :: MSG ": " :: msg) - | OK e' => OK e' - end - end) - f.(fn_code) (OK e). + PTree.fold + (fun re pc i => + match re with + | Error _ => re + | OK e => + match type_instr e i with + | Error msg => Error(MSG "At PC " :: POS pc :: MSG ": " :: msg) + | OK e' => OK e' + end + end) + f.(fn_code) (OK e). (** Solve remaining constraints *) -Definition check_params_norepet (params: list reg): res unit := - if list_norepet_dec Reg.eq params - then OK tt - else Error(msg "duplicate parameters"). +Definition check_params_norepet (params: list reg): res unit := + if list_norepet_dec Reg.eq params then OK tt else Error(msg "duplicate parameters"). Definition type_function : res regenv := do e1 <- type_code S.initial; - do e2 <- S.set_list e1 f.(fn_params) (normalize_list f.(fn_sig).(sig_args)); + do e2 <- S.type_defs e1 f.(fn_params) f.(fn_sig).(sig_args); do te <- S.solve e2; do x1 <- check_params_norepet f.(fn_params); do x2 <- check_successor f.(fn_entrypoint); @@ -315,10 +419,10 @@ Hint Resolve type_ros_incr: ty. Lemma type_ros_sound: forall e ros e' te, type_ros e ros = OK e' -> S.satisf te e' -> - match ros with inl r => te r = Tint | inr s => True end. + match ros with inl r => subtype (te r) Tint = true | inr s => True end. Proof. unfold type_ros; intros. destruct ros. - eapply S.set_sound; eauto. + eapply S.type_use_sound; eauto. auto. Qed. @@ -339,6 +443,17 @@ Proof. monadInv H. destruct H0. subst a; eauto with ty. eauto. Qed. +Remark subtype_list_charact: + forall tyl1 tyl2, + subtype_list tyl1 tyl2 = true <-> list_forall2 RTLtypes.sub tyl1 tyl2. +Proof. + unfold RTLtypes.sub; intros; split; intros. + revert tyl1 tyl2 H. induction tyl1; destruct tyl2; simpl; intros; try discriminate. + constructor. + InvBooleans. constructor; auto. + revert tyl1 tyl2 H. induction 1; simpl. auto. rewrite H; rewrite IHlist_forall2; auto. +Qed. + Lemma type_instr_incr: forall e i e' te, type_instr e i = OK e' -> S.satisf te e' -> S.satisf te e. @@ -374,56 +489,56 @@ Proof. + assert (o = Omove) by (unfold is_move in ISMOVE; destruct o; congruence). subst o. destruct l; try discriminate. destruct l; monadInv EQ0. - constructor. eapply S.move_sound; eauto. eauto with ty. + constructor. eapply S.type_move_sound; eauto. eauto with ty. + destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0. apply wt_Iop. unfold is_move in ISMOVE; destruct o; congruence. - rewrite TYOP. eapply S.set_list_sound; eauto with ty. - rewrite TYOP. eapply S.set_sound; eauto with ty. + rewrite TYOP. rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + rewrite TYOP. eapply S.type_def_sound; eauto with ty. eauto with ty. - (* load *) constructor. - eapply S.set_list_sound; eauto with ty. - eapply S.set_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + eapply S.type_def_sound; eauto with ty. eauto with ty. - (* store *) constructor. - eapply S.set_list_sound; eauto with ty. - eapply S.set_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + eapply S.type_use_sound; eauto with ty. eauto with ty. - (* call *) constructor. eapply type_ros_sound; eauto with ty. - eapply S.set_list_sound; eauto with ty. - eapply S.set_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + eapply S.type_def_sound; eauto with ty. eauto with ty. - (* tailcall *) destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2. constructor. eapply type_ros_sound; eauto with ty. - eapply S.set_list_sound; eauto with ty. auto. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. apply tailcall_is_possible_correct; auto. - (* builtin *) constructor. - eapply S.set_list_sound; eauto with ty. - eapply S.set_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + eapply S.type_def_sound; eauto with ty. eauto with ty. - (* cond *) constructor. - eapply S.set_list_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. eauto with ty. eauto with ty. - (* jumptable *) destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2. constructor. - eapply S.set_sound; eauto. + eapply S.type_use_sound; eauto. eapply check_successors_sound; eauto. auto. - (* return *) simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate. - econstructor. eauto. eapply S.set_sound; eauto with ty. + econstructor. eauto. eapply S.type_use_sound; eauto with ty. inv H. constructor. auto. Qed. @@ -460,7 +575,7 @@ Proof. assert (SAT1: S.satisf env x) by (eauto with ty). constructor. - (* type of parameters *) - eapply S.set_list_sound; eauto. + rewrite subtype_list_charact. eapply S.type_defs_sound; eauto. - (* parameters are unique *) unfold check_params_norepet in EQ2. destruct (list_norepet_dec Reg.eq (fn_params f)); inv EQ2; auto. @@ -475,11 +590,11 @@ Qed. Lemma type_ros_complete: forall te ros e, S.satisf te e -> - match ros with inl r => te r = Tint | inr s => True end -> + match ros with inl r => subtype (te r) Tint = true | inr s => True end -> exists e', type_ros e ros = OK e' /\ S.satisf te e'. Proof. intros; destruct ros; simpl. - eapply S.set_complete; eauto. + eapply S.type_use_complete; eauto. exists e; auto. Qed. @@ -500,60 +615,67 @@ Proof. - (* nop *) econstructor; split. rewrite check_successor_complete; simpl; eauto. auto. - (* move *) - exploit S.move_complete; eauto. intros (changed & e' & A & B). + exploit S.type_move_complete; eauto. intros (changed & e' & A & B). exists e'; split. rewrite check_successor_complete by auto; simpl. rewrite A; auto. auto. - (* other op *) destruct (type_of_operation op) as [targ tres]. simpl in *. - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_complete. eexact B. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H1. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_def_complete. eexact B. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. replace (is_move op) with false. rewrite A; simpl; rewrite C; auto. destruct op; reflexivity || congruence. - (* load *) - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_complete. eexact B. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H0. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_def_complete. eexact B. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; auto. - (* store *) - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_complete. eexact B. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H0. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_use_complete. eexact B. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; auto. - (* call *) exploit type_ros_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_list_complete. eauto. eauto. intros [e2 [C D]]. - exploit S.set_complete. eexact D. eauto. intros [e3 [E F]]. + rewrite subtype_list_charact in H1. + exploit S.type_uses_complete. eauto. eauto. intros [e2 [C D]]. + exploit S.type_def_complete. eexact D. eauto. intros [e3 [E F]]. exists e3; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; simpl; rewrite E; auto. - (* tailcall *) exploit type_ros_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_list_complete. eauto. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H2. + exploit S.type_uses_complete. eauto. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite A; simpl; rewrite C; simpl. - rewrite H2; rewrite dec_eq_true. + rewrite H1; rewrite dec_eq_true. replace (tailcall_is_possible sig) with true; auto. revert H3. unfold tailcall_possible, tailcall_is_possible. generalize (loc_arguments sig). induction l; simpl; intros. auto. exploit (H3 a); auto. intros. destruct a; try contradiction. apply IHl. intros; apply H3; auto. - (* builtin *) - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_complete. eexact B. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H0. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_def_complete. eexact B. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; auto. - (* cond *) - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. + rewrite subtype_list_charact in H0. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. exists e1; split; auto. rewrite check_successor_complete by auto; simpl. rewrite check_successor_complete by auto; simpl. auto. - (* jumptbl *) - exploit S.set_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_use_complete. eauto. eauto. intros [e1 [A B]]. exists e1; split; auto. replace (check_successors tbl) with (OK tt). simpl. rewrite A; simpl. apply zle_true; auto. @@ -563,7 +685,7 @@ Proof. - (* return none *) rewrite H0. exists e; auto. - (* return some *) - rewrite H0. apply S.set_complete; auto. + rewrite H0. apply S.type_use_complete; auto. Qed. Lemma type_code_complete: @@ -597,7 +719,8 @@ Proof. intros. destruct H. destruct (type_code_complete te S.initial) as (e1 & A & B). auto. apply S.satisf_initial. - destruct (S.set_list_complete te f.(fn_params) (normalize_list f.(fn_sig).(sig_args)) e1) as (e2 & C & D); auto. + destruct (S.type_defs_complete te f.(fn_params) f.(fn_sig).(sig_args) e1) as (e2 & C & D); auto. + rewrite <- subtype_list_charact; auto. destruct (S.solve_complete te e2) as (te' & E); auto. exists te'; unfold type_function. rewrite A; simpl. rewrite C; simpl. rewrite E; simpl. @@ -637,23 +760,6 @@ Proof. apply H. Qed. -Lemma normalize_subtype: - forall ty, subtype ty (normalize ty) = true. -Proof. - intros. destruct ty; reflexivity. -Qed. - -Lemma wt_regset_assign2: - forall env rs v r ty, - wt_regset env rs -> - Val.has_type v ty -> - env r = normalize ty -> - wt_regset env (rs#r <- v). -Proof. - intros. eapply wt_regset_assign; eauto. - rewrite H1. eapply Val.has_subtype; eauto. apply normalize_subtype. -Qed. - Lemma wt_regset_list: forall env rs, wt_regset env rs -> @@ -682,11 +788,11 @@ Lemma wt_exec_Iop: wt_regset env (rs#res <- v). Proof. intros. inv H. - simpl in H0. inv H0. apply wt_regset_assign; auto. - rewrite H4; auto. - eapply wt_regset_assign2; auto. + simpl in H0. inv H0. apply wt_regset_assign; auto. + eapply Val.has_subtype; eauto. + apply wt_regset_assign; auto. + eapply Val.has_subtype; eauto. eapply type_of_operation_sound; eauto. - auto. Qed. Lemma wt_exec_Iload: @@ -697,7 +803,8 @@ Lemma wt_exec_Iload: wt_regset env (rs#dst <- v). Proof. intros. destruct a; simpl in H0; try discriminate. inv H. - eapply wt_regset_assign2; eauto. + apply wt_regset_assign; auto. + eapply Val.has_subtype; eauto. eapply Mem.load_type; eauto. Qed. @@ -709,7 +816,8 @@ Lemma wt_exec_Ibuiltin: wt_regset env (rs#res <- vres). Proof. intros. inv H. - eapply wt_regset_assign2; eauto. + apply wt_regset_assign; auto. + eapply Val.has_subtype; eauto. eapply external_call_well_typed; eauto. Qed. @@ -720,46 +828,36 @@ Proof. intros. inv H. eauto. Qed. -Inductive wt_stackframes: list stackframe -> signature -> Prop := - | wt_stackframes_nil: forall sg, - sg.(sig_res) = Some Tint -> - wt_stackframes nil sg +Inductive wt_stackframes: list stackframe -> option typ -> Prop := + | wt_stackframes_nil: + wt_stackframes nil (Some Tint) | wt_stackframes_cons: - forall s res f sp pc rs env sg, + forall s res f sp pc rs env tyres, wt_function f env -> wt_regset env rs -> - env res = normalize (proj_sig_res sg) -> - wt_stackframes s (fn_sig f) -> - wt_stackframes (Stackframe res f sp pc rs :: s) sg. + subtype (match tyres with None => Tint | Some t => t end) (env res) = true -> + wt_stackframes s (sig_res (fn_sig f)) -> + wt_stackframes (Stackframe res f sp pc rs :: s) tyres. Inductive wt_state: state -> Prop := | wt_state_intro: forall s f sp pc rs m env - (WT_STK: wt_stackframes s (fn_sig f)) + (WT_STK: wt_stackframes s (sig_res (fn_sig f))) (WT_FN: wt_function f env) (WT_RS: wt_regset env rs), wt_state (State s f sp pc rs m) | wt_state_call: forall s f args m, - wt_stackframes s (funsig f) -> + wt_stackframes s (sig_res (funsig f)) -> wt_fundef f -> - Val.has_type_list args (normalize_list (sig_args (funsig f))) -> + Val.has_type_list args (sig_args (funsig f)) -> wt_state (Callstate s f args m) | wt_state_return: - forall s v m sg, - wt_stackframes s sg -> - Val.has_type v (normalize (proj_sig_res sg)) -> + forall s v m tyres, + wt_stackframes s tyres -> + Val.has_type v (match tyres with None => Tint | Some t => t end) -> wt_state (Returnstate s v m). -Remark wt_stackframes_change_sig: - forall s sg1 sg2, - sg1.(sig_res) = sg2.(sig_res) -> wt_stackframes s sg1 -> wt_stackframes s sg2. -Proof. - intros. inv H0. -- constructor; congruence. -- econstructor; eauto. rewrite H3. unfold proj_sig_res. rewrite H. auto. -Qed. - Section SUBJECT_REDUCTION. Variable p: program. @@ -793,7 +891,7 @@ Proof. discriminate. econstructor; eauto. econstructor; eauto. inv WTI; auto. - inv WTI. rewrite <- H8. apply wt_regset_list. auto. + inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list. auto. (* Itailcall *) assert (wt_fundef fd). destruct ros; simpl in H0. @@ -804,8 +902,8 @@ Proof. exact wt_p. exact H0. discriminate. econstructor; eauto. - inv WTI. apply wt_stackframes_change_sig with (fn_sig f); auto. - inv WTI. rewrite <- H7. apply wt_regset_list. auto. + inv WTI. rewrite H7; auto. + inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list. auto. (* Ibuiltin *) econstructor; eauto. eapply wt_exec_Ibuiltin; eauto. (* Icond *) @@ -814,40 +912,18 @@ Proof. econstructor; eauto. (* Ireturn *) econstructor; eauto. - inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. rewrite <- H3. auto. + inv WTI; simpl. auto. rewrite H2. eapply Val.has_subtype; eauto. (* internal function *) simpl in *. inv H5. econstructor; eauto. - inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto. + inv H1. apply wt_init_regs; auto. eapply Val.has_subtype_list; eauto. (* external function *) econstructor; eauto. simpl. - change (Val.has_type res (normalize (proj_sig_res (ef_sig ef)))). - eapply Val.has_subtype. apply normalize_subtype. + change (Val.has_type res (proj_sig_res (ef_sig ef))). eapply external_call_well_typed; eauto. (* return *) inv H1. econstructor; eauto. - apply wt_regset_assign; auto. rewrite H10; auto. -Qed. - -Lemma wt_initial_state: - forall S, initial_state p S -> wt_state S. -Proof. - intros. inv H. constructor. constructor. rewrite H3; auto. - pattern f. apply Genv.find_funct_ptr_prop with fundef unit p b. - exact wt_p. exact H2. - rewrite H3. constructor. -Qed. - -Lemma wt_instr_inv: - forall s f sp pc rs m i, - wt_state (State s f sp pc rs m) -> - f.(fn_code)!pc = Some i -> - exists env, wt_instr f env i /\ wt_regset env rs. -Proof. - intros. inv H. exists env; split; auto. - inv WT_FN. eauto. + apply wt_regset_assign; auto. eapply Val.has_subtype; eauto. Qed. End SUBJECT_REDUCTION. - - diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index cea2e0b..9b144cb 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -664,12 +664,17 @@ Record agree_frame (j: meminj) (ls ls0: locset) (** Permissions on the frame part of the Mach stack block *) agree_perm: - frame_perm_freeable m' sp' + frame_perm_freeable m' sp'; + + (** Current locset is well-typed *) + agree_wt_ls: + wt_locset ls }. Hint Resolve agree_unused_reg agree_locals agree_outgoing agree_incoming agree_link agree_retaddr agree_saved_int agree_saved_float - agree_valid_linear agree_valid_mach agree_perm: stacking. + agree_valid_linear agree_valid_mach agree_perm + agree_wt_ls: stacking. (** Auxiliary predicate used at call points *) @@ -788,16 +793,19 @@ Lemma agree_frame_set_reg: forall j ls ls0 m sp m' sp' parent ra r v, agree_frame j ls ls0 m sp m' sp' parent ra -> mreg_within_bounds b r -> + Val.has_type v (Loc.type (R r)) -> agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent ra. Proof. intros. inv H; constructor; auto; intros. rewrite Locmap.gso. auto. red. intuition congruence. + apply wt_setreg; auto. Qed. Lemma agree_frame_set_regs: forall j ls0 m sp m' sp' parent ra rl vl ls, agree_frame j ls ls0 m sp m' sp' parent ra -> (forall r, In r rl -> mreg_within_bounds b r) -> + Val.has_type_list vl (map Loc.type (map R rl)) -> agree_frame j (Locmap.setlist (map R rl) vl ls) ls0 m sp m' sp' parent ra. Proof. induction rl; destruct vl; simpl; intros; intuition. @@ -813,7 +821,7 @@ Lemma agree_frame_undef_regs: Proof. induction regs; simpl; intros. auto. - apply agree_frame_set_reg; auto. + apply agree_frame_set_reg; auto. red; auto. Qed. Lemma caller_save_reg_within_bounds: @@ -844,18 +852,17 @@ Lemma agree_frame_set_local: forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', agree_frame j ls ls0 m sp m' sp' parent retaddr -> slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true -> - Val.has_type v ty -> val_inject j v v' -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' -> agree_frame j (Locmap.set (S Local ofs ty) v ls) ls0 m sp m'' sp' parent retaddr. Proof. intros. inv H. - change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H4. + change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3. constructor; auto; intros. (* local *) unfold Locmap.set. destruct (Loc.eq (S Local ofs ty) (S Local ofs0 ty0)). - inv e. eapply gss_index_contains_inj; eauto with stacking. + inv e. eapply gss_index_contains_inj'; eauto with stacking. destruct (Loc.diff_dec (S Local ofs ty) (S Local ofs0 ty0)). eapply gso_index_contains_inj. eauto. eauto with stacking. eauto. simpl. simpl in d. intuition. @@ -876,6 +883,8 @@ Proof. eauto with mem. (* perm *) red; intros. eapply Mem.perm_store_1; eauto. +(* wt *) + apply wt_setstack; auto. Qed. (** Preservation by assignment to outgoing slot *) @@ -884,20 +893,19 @@ Lemma agree_frame_set_outgoing: forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', agree_frame j ls ls0 m sp m' sp' parent retaddr -> slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true -> - Val.has_type v ty -> val_inject j v v' -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' -> agree_frame j (Locmap.set (S Outgoing ofs ty) v ls) ls0 m sp m'' sp' parent retaddr. Proof. intros. inv H. - change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H4. + change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3. constructor; auto; intros. (* local *) rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking. red; auto. red; left; congruence. (* outgoing *) unfold Locmap.set. destruct (Loc.eq (S Outgoing ofs ty) (S Outgoing ofs0 ty0)). - inv e. eapply gss_index_contains_inj; eauto with stacking. + inv e. eapply gss_index_contains_inj'; eauto with stacking. destruct (Loc.diff_dec (S Outgoing ofs ty) (S Outgoing ofs0 ty0)). eapply gso_index_contains_inj; eauto with stacking. red. red in d. intuition. @@ -915,6 +923,8 @@ Proof. eauto with mem stacking. (* perm *) red; intros. eapply Mem.perm_store_1; eauto. +(* wt *) + apply wt_setstack; auto. Qed. (** General invariance property with respect to memory changes. *) @@ -1041,6 +1051,7 @@ Lemma agree_frame_return: forall j ls ls0 m sp m' sp' parent retaddr ls', agree_frame j ls ls0 m sp m' sp' parent retaddr -> agree_callee_save ls' ls -> + wt_locset ls' -> agree_frame j ls' ls0 m sp m' sp' parent retaddr. Proof. intros. red in H0. inv H; constructor; auto; intros. @@ -1236,7 +1247,7 @@ Hypothesis csregs_typ: Hypothesis ls_temp_undef: forall r, In r (destroyed_by_setstack ty) -> ls (R r) = Vundef. -Hypothesis wt_ls: wt_locset Regset.empty ls. +Hypothesis wt_ls: wt_locset ls. Lemma save_callee_save_regs_correct: forall l k rs m, @@ -1293,8 +1304,7 @@ Proof. simpl in H3. destruct (mreg_eq a r). subst r. assert (index_contains_inj j m1 sp (mkindex (number a)) (ls (R a))). eapply gss_index_contains_inj; eauto. - rewrite mkindex_typ. rewrite <- (csregs_typ a). eapply wt_mreg; eauto. - auto with coqlib. + rewrite mkindex_typ. rewrite <- (csregs_typ a). apply wt_ls. auto with coqlib. destruct H5 as [v' [P Q]]. exists v'; split; auto. apply C; auto. intros. apply mkindex_inj. apply number_inj; auto with coqlib. @@ -1344,7 +1354,7 @@ Qed. Lemma save_callee_save_correct: forall j ls0 rs sp cs fb k m, let ls := LTL.undef_regs destroyed_at_function_entry ls0 in - agree_regs j ls rs -> wt_locset Regset.empty ls -> + agree_regs j ls rs -> wt_locset ls -> frame_perm_freeable m sp -> exists rs', exists m', star step tge @@ -1470,7 +1480,7 @@ Lemma function_prologue_correct: forall j ls ls0 ls1 rs rs1 m1 m1' m2 sp parent ra cs fb k, agree_regs j ls rs -> agree_callee_save ls ls0 -> - wt_locset Regset.empty ls -> + wt_locset ls -> ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) -> rs1 = undef_regs destroyed_at_function_entry rs -> Mem.inject j m1 m1' -> @@ -1530,7 +1540,7 @@ Proof. instantiate (1 := rs1). instantiate (1 := call_regs ls). instantiate (1 := j'). subst rs1. apply agree_regs_undef_regs. apply agree_regs_call_regs. eapply agree_regs_inject_incr; eauto. - apply wt_undef_regs. eapply wt_call_regs. eauto. + apply wt_undef_regs. apply wt_call_regs. auto. eexact PERM4. rewrite <- LS1. intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]]. @@ -1612,6 +1622,8 @@ Proof. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite dec_eq_true. auto. (* perms *) auto. + (* wt *) + rewrite LS1. apply wt_undef_regs. apply wt_call_regs; auto. (* incr *) split. auto. (* separated *) @@ -1854,6 +1866,7 @@ Inductive match_stacks (j: meminj) (m m': mem): match_stacks j m m' nil nil sg bound bound' | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg bound bound' trf (TAIL: is_tail c (Linear.fn_code f)) + (WTF: wt_function f = true) (FINDF: Genv.find_funct_ptr tge fb = Some (Internal trf)) (TRF: transf_function f = OK trf) (TRC: transl_code (make_env (function_bounds f)) c = c') @@ -2042,6 +2055,16 @@ Qed. (** Typing properties of [match_stacks]. *) +Lemma match_stacks_wt_locset: + forall j m m' cs cs' sg bound bound', + match_stacks j m m' cs cs' sg bound bound' -> + wt_locset (parent_locset cs). +Proof. + induction 1; simpl. + unfold Locmap.init; red; intros; red; auto. + inv FRM; auto. +Qed. + Lemma match_stacks_type_sp: forall j m m' cs cs' sg bound bound', match_stacks j m m' cs cs' sg bound bound' -> @@ -2434,6 +2457,7 @@ Inductive match_states: Linear.state -> Mach.state -> Prop := (STACKS: match_stacks j m m' cs cs' f.(Linear.fn_sig) sp sp') (TRANSL: transf_function f = OK tf) (FIND: Genv.find_funct_ptr tge fb = Some (Internal tf)) + (WTF: wt_function f = true) (AGREGS: agree_regs j ls rs) (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs')) (TAIL: is_tail c (Linear.fn_code f)), @@ -2445,6 +2469,7 @@ Inductive match_states: Linear.state -> Mach.state -> Prop := (STACKS: match_stacks j m m' cs cs' (Linear.funsig f) (Mem.nextblock m) (Mem.nextblock m')) (TRANSL: transf_fundef f = OK tf) (FIND: Genv.find_funct_ptr tge fb = Some tf) + (WTLS: wt_locset ls) (AGREGS: agree_regs j ls rs) (AGLOCS: agree_callee_save ls (parent_locset cs)), match_states (Linear.Callstate cs f ls m) @@ -2453,6 +2478,7 @@ Inductive match_states: Linear.state -> Mach.state -> Prop := forall cs ls m cs' rs m' j sg (MINJ: Mem.inject j m m') (STACKS: match_stacks j m m' cs cs' sg (Mem.nextblock m) (Mem.nextblock m')) + (WTLS: wt_locset ls) (AGREGS: agree_regs j ls rs) (AGLOCS: agree_callee_save ls (parent_locset cs)), match_states (Linear.Returnstate cs ls m) @@ -2460,40 +2486,37 @@ Inductive match_states: Linear.state -> Mach.state -> Prop := Theorem transf_step_correct: forall s1 t s2, Linear.step ge s1 t s2 -> - forall (WTS: wt_state s1) s1' (MS: match_states s1 s1'), + forall s1' (MS: match_states s1 s1'), exists s2', plus step tge s1' t s2' /\ match_states s2 s2'. Proof. -(* assert (USEWTF: forall f i c, wt_function f = true -> is_tail (i :: c) (Linear.fn_code f) -> wt_instr f i = true). intros. unfold wt_function, wt_code in H. rewrite forallb_forall in H. apply H. eapply is_tail_in; eauto. -*) induction 1; intros; try inv MS; try rewrite transl_code_eq; + try (generalize (USEWTF _ _ _ WTF TAIL); intro WTI; simpl in WTI; InvBooleans); try (generalize (function_is_within_bounds f _ (is_tail_in TAIL)); intro BOUND; simpl in BOUND); unfold transl_instr. -- (* Lgetstack *) - destruct BOUND. - exploit wt_state_getstack; eauto. intros SV. - unfold destroyed_by_getstack; destruct sl. -+ (* Lgetstack, local *) + (* Lgetstack *) + destruct BOUND. unfold destroyed_by_getstack; destruct sl. + (* Lgetstack, local *) exploit agree_locals; eauto. intros [v [A B]]. econstructor; split. apply plus_one. apply exec_Mgetstack. eapply index_contains_load_stack; eauto. econstructor; eauto with coqlib. apply agree_regs_set_reg; auto. - apply agree_frame_set_reg; auto. -+ (* Lgetstack, incoming *) - unfold slot_valid in SV. InvBooleans. + apply agree_frame_set_reg; auto. simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto. + (* Lgetstack, incoming *) + unfold slot_valid in H0. InvBooleans. exploit incoming_slot_in_parameters; eauto. intros IN_ARGS. inversion STACKS; clear STACKS. - elim (H6 _ IN_ARGS). + elim (H7 _ IN_ARGS). subst bound bound' s cs'. exploit agree_outgoing. eexact FRM. eapply ARGS; eauto. exploit loc_arguments_acceptable; eauto. intros [A B]. @@ -2514,7 +2537,8 @@ Proof. eapply agree_frame_set_reg; eauto. eapply agree_frame_set_reg; eauto. apply caller_save_reg_within_bounds. apply temp_for_parent_frame_caller_save. -+ (* Lgetstack, outgoing *) + simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto. + (* Lgetstack, outgoing *) exploit agree_outgoing; eauto. intros [v [A B]]. econstructor; split. apply plus_one. apply exec_Mgetstack. @@ -2522,55 +2546,66 @@ Proof. econstructor; eauto with coqlib. apply agree_regs_set_reg; auto. apply agree_frame_set_reg; auto. + simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto. -- (* Lsetstack *) - exploit wt_state_setstack; eauto. intros (VTY & SV & SW). + (* Lsetstack *) set (idx := match sl with | Local => FI_local ofs ty | Incoming => FI_link (*dummy*) | Outgoing => FI_arg ofs ty end). assert (index_valid f idx). - { unfold idx; destruct sl. + unfold idx; destruct sl. apply index_local_valid; auto. red; auto. - apply index_arg_valid; auto. } + apply index_arg_valid; auto. exploit store_index_succeeds; eauto. eapply agree_perm; eauto. instantiate (1 := rs0 src). intros [m1' STORE]. econstructor; split. - apply plus_one. destruct sl; simpl in SW. + apply plus_one. destruct sl; simpl in H0. econstructor. eapply store_stack_succeeds with (idx := idx); eauto. eauto. discriminate. econstructor. eapply store_stack_succeeds with (idx := idx); eauto. auto. econstructor. eapply Mem.store_outside_inject; eauto. intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta. - rewrite size_type_chunk in H2. + rewrite size_type_chunk in H4. exploit offset_of_index_disj_stack_data_2; eauto. exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. omega. apply match_stacks_change_mach_mem with m'; auto. - eauto with mem. eauto with mem. intros. rewrite <- H1; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. + eauto with mem. eauto with mem. intros. rewrite <- H3; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. eauto. eauto. auto. apply agree_regs_set_slot. apply agree_regs_undef_regs; auto. destruct sl. - + eapply agree_frame_set_local. eapply agree_frame_undef_locs; eauto. - apply destroyed_by_setstack_caller_save. auto. auto. auto. apply AGREGS. + eapply agree_frame_set_local. eapply agree_frame_undef_locs; eauto. + apply destroyed_by_setstack_caller_save. auto. auto. apply AGREGS. + assumption. + simpl in H0; discriminate. + eapply agree_frame_set_outgoing. eapply agree_frame_undef_locs; eauto. + apply destroyed_by_setstack_caller_save. auto. auto. apply AGREGS. assumption. - + simpl in SW; discriminate. - + eapply agree_frame_set_outgoing. eapply agree_frame_undef_locs; eauto. - apply destroyed_by_setstack_caller_save. auto. auto. auto. apply AGREGS. - assumption. - + eauto with coqlib. + eauto with coqlib. -- (* Lop *) + (* Lop *) + assert (Val.has_type v (mreg_type res)). + destruct (is_move_operation op args) as [arg|] eqn:?. + exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst op args. + eapply Val.has_subtype; eauto. simpl in H; inv H. eapply agree_wt_ls; eauto. + destruct (type_of_operation op) as [targs tres] eqn:TYOP. + eapply Val.has_subtype; eauto. + replace tres with (snd (type_of_operation op)). + eapply type_of_operation_sound; eauto. + red; intros. subst op. simpl in Heqo. + destruct args; simpl in H. discriminate. destruct args. discriminate. simpl in H. discriminate. + rewrite TYOP; auto. assert (exists v', eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v' /\ val_inject j v v'). eapply eval_operation_inject; eauto. eapply match_stacks_preserves_globals; eauto. eapply agree_inj; eauto. eapply agree_reglist; eauto. - destruct H0 as [v' [A B]]. + destruct H1 as [v' [A B]]. econstructor; split. apply plus_one. econstructor. instantiate (1 := v'). rewrite <- A. apply eval_operation_preserved. @@ -2581,7 +2616,7 @@ Proof. apply agree_frame_set_reg; auto. apply agree_frame_undef_locs; auto. apply destroyed_by_op_caller_save. -- (* Lload *) + (* Lload *) assert (exists a', eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' /\ val_inject j a a'). @@ -2598,8 +2633,9 @@ Proof. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. apply agree_frame_set_reg. apply agree_frame_undef_locs; auto. apply destroyed_by_load_caller_save. auto. + simpl. eapply Val.has_subtype; eauto. destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto. -- (* Lstore *) + (* Lstore *) assert (exists a', eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' /\ val_inject j a a'). @@ -2620,7 +2656,7 @@ Proof. eapply agree_frame_parallel_stores; eauto. apply destroyed_by_store_caller_save. -- (* Lcall *) + (* Lcall *) exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. exploit is_tail_transf_function; eauto. intros IST. rewrite transl_code_eq in IST. simpl in IST. @@ -2636,9 +2672,10 @@ Proof. apply loc_arguments_bounded; auto. eapply agree_valid_linear; eauto. eapply agree_valid_mach; eauto. + eapply agree_wt_ls; eauto. simpl; red; auto. -- (* Ltailcall *) + (* Ltailcall *) exploit function_epilogue_correct; eauto. intros [rs1 [m1' [P [Q [R [S [T [U V]]]]]]]]. exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. @@ -2651,13 +2688,14 @@ Proof. apply match_stacks_change_mach_mem with m'0. auto. eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; apply Plt_ne; auto. - intros. rewrite <- H1. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. + intros. rewrite <- H3. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. eauto with mem. intros. eapply Mem.perm_free_3; eauto. apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. - apply zero_size_arguments_tailcall_possible. eapply wt_state_tailcall; eauto. + apply zero_size_arguments_tailcall_possible; auto. + apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. -- (* Lbuiltin *) + (* Lbuiltin *) exploit external_call_mem_inject'; eauto. eapply match_stacks_preserves_globals; eauto. eapply agree_reglist; eauto. @@ -2679,9 +2717,12 @@ Proof. intros. inv H; eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto. eapply external_call_valid_block'; eauto. eapply agree_valid_mach; eauto. + simpl. rewrite list_map_compose. + change (fun x => Loc.type (R x)) with mreg_type. + eapply Val.has_subtype_list; eauto. eapply external_call_well_typed'; eauto. -- (* Lannot *) - exploit transl_annot_params_correct; eauto. eapply wt_state_annot; eauto. + (* Lannot *) + exploit transl_annot_params_correct; eauto. intros [vargs' [P Q]]. exploit external_call_mem_inject'; eauto. eapply match_stacks_preserves_globals; eauto. @@ -2702,49 +2743,49 @@ Proof. eapply external_call_valid_block'; eauto. eapply agree_valid_mach; eauto. -- (* Llabel *) + (* Llabel *) econstructor; split. apply plus_one; apply exec_Mlabel. econstructor; eauto with coqlib. -- (* Lgoto *) + (* Lgoto *) econstructor; split. apply plus_one; eapply exec_Mgoto; eauto. apply transl_find_label; eauto. econstructor; eauto. eapply find_label_tail; eauto. -- (* Lcond, true *) + (* Lcond, true *) econstructor; split. apply plus_one. eapply exec_Mcond_true; eauto. eapply eval_condition_inject; eauto. eapply agree_reglist; eauto. eapply transl_find_label; eauto. - econstructor. eauto. eauto. eauto. eauto. + econstructor. eauto. eauto. eauto. eauto. eauto. apply agree_regs_undef_regs; auto. apply agree_frame_undef_locs; auto. apply destroyed_by_cond_caller_save. eapply find_label_tail; eauto. -- (* Lcond, false *) + (* Lcond, false *) econstructor; split. apply plus_one. eapply exec_Mcond_false; eauto. eapply eval_condition_inject; eauto. eapply agree_reglist; eauto. - econstructor. eauto. eauto. eauto. eauto. + econstructor. eauto. eauto. eauto. eauto. eauto. apply agree_regs_undef_regs; auto. apply agree_frame_undef_locs; auto. apply destroyed_by_cond_caller_save. eauto with coqlib. -- (* Ljumptable *) + (* Ljumptable *) assert (rs0 arg = Vint n). - { generalize (AGREGS arg). rewrite H. intro IJ; inv IJ; auto. } + generalize (AGREGS arg). rewrite H. intro IJ; inv IJ; auto. econstructor; split. apply plus_one; eapply exec_Mjumptable; eauto. apply transl_find_label; eauto. - econstructor. eauto. eauto. eauto. eauto. + econstructor. eauto. eauto. eauto. eauto. eauto. apply agree_regs_undef_regs; auto. apply agree_frame_undef_locs; auto. apply destroyed_by_jumptable_caller_save. eapply find_label_tail; eauto. -- (* Lreturn *) + (* Lreturn *) exploit function_epilogue_correct; eauto. intros [rs1 [m1' [P [Q [R [S [T [U V]]]]]]]]. econstructor; split. @@ -2760,12 +2801,13 @@ Proof. eauto with mem. intros. eapply Mem.perm_free_3; eauto. apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. + apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. -- (* internal function *) + (* internal function *) revert TRANSL. unfold transf_fundef, transf_partial_fundef. caseEq (transf_function f); simpl; try congruence. intros tfn TRANSL EQ. inversion EQ; clear EQ; subst tf. - exploit function_prologue_correct; eauto. eapply wt_callstate_wt_locset; eauto. + exploit function_prologue_correct; eauto. eapply match_stacks_type_sp; eauto. eapply match_stacks_type_retaddr; eauto. intros [j' [rs' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]]. @@ -2786,9 +2828,10 @@ Proof. intros. eapply stores_in_frame_perm; eauto with mem. intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto. eapply Mem.load_alloc_unchanged; eauto. red. congruence. + eapply transf_function_well_typed; eauto. auto with coqlib. -- (* external function *) + (* external function *) simpl in TRANSL. inversion TRANSL; subst tf. exploit transl_external_arguments; eauto. intros [vl [ARGS VINJ]]. exploit external_call_mem_inject'; eauto. @@ -2803,10 +2846,11 @@ Proof. inv H0; inv A. eapply match_stack_change_extcall; eauto. apply Ple_refl. apply Ple_refl. eapply external_call_nextblock'; eauto. eapply external_call_nextblock'; eauto. + inv H0. apply wt_setlist_result. eapply external_call_well_typed; eauto. auto. apply agree_regs_set_regs; auto. apply agree_regs_inject_incr with j; auto. apply agree_callee_save_set_result; auto. -- (* return *) + (* return *) inv STACKS. simpl in AGLOCS. econstructor; split. apply plus_one. apply exec_return. @@ -2835,6 +2879,7 @@ Proof. intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto. intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto. rewrite H3. red; intros. contradiction. + apply wt_init. unfold Locmap.init. red; intros; auto. unfold parent_locset. red; auto. Qed. @@ -2848,31 +2893,14 @@ Proof. econstructor; eauto. Qed. -Lemma wt_prog: - forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd. -Proof. - intros. exploit transform_partial_program_succeeds; eauto. - intros [tfd TF]. destruct fd; simpl in *. -- monadInv TF. unfold transf_function in EQ. - destruct (wt_function f). auto. discriminate. -- auto. -Qed. - Theorem transf_program_correct: forward_simulation (Linear.semantics prog) (Mach.semantics return_address_offset tprog). Proof. - set (ms := fun s s' => wt_state s /\ match_states s s'). - eapply forward_simulation_plus with (match_states := ms). -- exact symbols_preserved. -- intros. exploit transf_initial_states; eauto. intros [st2 [A B]]. - exists st2; split; auto. split; auto. - apply wt_initial_state with (prog := prog); auto. exact wt_prog. -- intros. destruct H. eapply transf_final_states; eauto. -- intros. destruct H0. - exploit transf_step_correct; eauto. intros [s2' [A B]]. - exists s2'; split. exact A. split. - eapply step_type_preservation; eauto. eexact wt_prog. eexact H. - auto. + eapply forward_simulation_plus. + eexact symbols_preserved. + eexact transf_initial_states. + eexact transf_final_states. + eexact transf_step_correct. Qed. End PRESERVATION. diff --git a/common/Unityping.v b/common/Unityping.v deleted file mode 100644 index d108c87..0000000 --- a/common/Unityping.v +++ /dev/null @@ -1,435 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(* A solver for unification constraints. *) - -Require Import Recdef Coqlib Maps Errors. - -Local Open Scope nat_scope. -Local Open Scope error_monad_scope. - -(** This module provides a solver for sets of unification constraints of the - following kinds: [T(x) = base-type] or [T(x) = T(y)]. - The unknowns are the types [T(x)] of every identifier [x]. *) - -(** The interface for base types. *) - -Module Type TYPE_ALGEBRA. - -Variable t: Type. -Variable eq: forall (x y: t), {x=y} + {x<>y}. -Variable default: t. - -End TYPE_ALGEBRA. - -(** The constraint solver. *) - -Module UniSolver (T: TYPE_ALGEBRA). - -(* The current set of constraints is represented by a record with two components: -- [te_typ]: a partial map from variables to types -- [te_equ]: a list of pairs [(x,y)] of variables, indicating that - the type of [x] must be equal to the type of [y]. -*) - -Definition constraint : Type := (positive * positive)%type. - -Record typenv : Type := Typenv { - te_typ: PTree.t T.t; (**r mapping var -> typ *) - te_equ: list constraint (**r additional equality constraints *) -}. - -Definition initial : typenv := {| te_typ := PTree.empty _; te_equ := nil |}. - -(** Add the constraint [T(x) = ty]. *) - -Definition set (e: typenv) (x: positive) (ty: T.t) : res typenv := - match e.(te_typ)!x with - | None => - OK {| te_typ := PTree.set x ty e.(te_typ); - te_equ := e.(te_equ) |} - | Some ty' => - if T.eq ty ty' - then OK e - else Error (MSG "bad definition/use of variable " :: POS x :: nil) - end. - -Fixpoint set_list (e: typenv) (rl: list positive) (tyl: list T.t) {struct rl}: res typenv := - match rl, tyl with - | nil, nil => OK e - | r1::rs, ty1::tys => do e1 <- set e r1 ty1; set_list e1 rs tys - | _, _ => Error (msg "arity mismatch") - end. - -(** Add the constraint [T(x) = T(y)]. - The boolean result is [true] if the types of [x] or [y] could be - made more precise. Otherwise, [te_typ] does not change and - [false] is returned. *) - -Definition move (e: typenv) (r1 r2: positive) : res (bool * typenv) := - if peq r1 r2 then OK (false, e) else - match e.(te_typ)!r1, e.(te_typ)!r2 with - | None, None => - OK (false, {| te_typ := e.(te_typ); te_equ := (r1, r2) :: e.(te_equ) |}) - | Some ty1, None => - OK (true, {| te_typ := PTree.set r2 ty1 e.(te_typ); te_equ := e.(te_equ) |}) - | None, Some ty2 => - OK (true, {| te_typ := PTree.set r1 ty2 e.(te_typ); te_equ := e.(te_equ) |}) - | Some ty1, Some ty2 => - if T.eq ty1 ty2 - then OK (false, e) - else Error(MSG "ill-typed move from " :: POS r1 :: MSG " to " :: POS r2 :: nil) - end. - -(** Solve the remaining subtyping constraints by iteration. *) - -Fixpoint solve_rec (e: typenv) (changed: bool) (q: list constraint) : res (typenv * bool) := - match q with - | nil => - OK (e, changed) - | (r1, r2) :: q' => - do (changed1, e1) <- move e r1 r2; solve_rec e1 (changed || changed1) q' - end. - -(** Measuring the state *) - -Lemma move_shape: - forall e r1 r2 changed e', - move e r1 r2 = OK (changed, e') -> - (e'.(te_equ) = e.(te_equ) \/ e'.(te_equ) = (r1, r2) :: e.(te_equ)) - /\ (changed = true -> e'.(te_equ) = e.(te_equ)). -Proof. - unfold move; intros. - destruct (peq r1 r2). inv H. auto. - destruct e.(te_typ)!r1 as [ty1|]; destruct e.(te_typ)!r2 as [ty2|]; inv H; simpl. - destruct (T.eq ty1 ty2); inv H1. auto. - auto. - auto. - split. auto. intros. discriminate. -Qed. - -Lemma length_move: - forall e r1 r2 changed e', - move e r1 r2 = OK (changed, e') -> - length e'.(te_equ) + (if changed then 1 else 0) <= S(length e.(te_equ)). -Proof. - unfold move; intros. - destruct (peq r1 r2). inv H. omega. - destruct e.(te_typ)!r1 as [ty1|]; destruct e.(te_typ)!r2 as [ty2|]; inv H; simpl. - destruct (T.eq ty1 ty2); inv H1. omega. - omega. - omega. - omega. -Qed. - -Lemma length_solve_rec: - forall q e ch e' ch', - solve_rec e ch q = OK (e', ch') -> - length e'.(te_equ) + (if ch' && negb ch then 1 else 0) <= length e.(te_equ) + length q. -Proof. - induction q; simpl; intros. -- inv H. replace (ch' && negb ch') with false. omega. destruct ch'; auto. -- destruct a as [r1 r2]; monadInv H. rename x0 into e0. rename x into ch0. - exploit IHq; eauto. intros A. - exploit length_move; eauto. intros B. - set (X := (if ch' && negb (ch || ch0) then 1 else 0)) in *. - set (Y := (if ch0 then 1 else 0)) in *. - set (Z := (if ch' && negb ch then 1 else 0)) in *. - cut (Z <= X + Y). intros. omega. - unfold X, Y, Z. destruct ch'; destruct ch; destruct ch0; simpl; auto. -Qed. - -Definition weight_typenv (e: typenv) : nat := length e.(te_equ). - - -(** Iterative solving of the remaining constraints *) - -Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv := - match solve_rec {| te_typ := e.(te_typ); te_equ := nil |} false e.(te_equ) with - | OK(e', false) => OK e (**r no more changes, fixpoint reached *) - | OK(e', true) => solve_constraints e' (**r one more iteration *) - | Error msg => Error msg - end. -Proof. - intros. exploit length_solve_rec; eauto. simpl. intros. - unfold weight_typenv. omega. -Qed. - -Definition typassign := positive -> T.t. - -Definition makeassign (e: typenv) : typassign := - fun x => match e.(te_typ)!x with Some ty => ty | None => T.default end. - -Definition solve (e: typenv) : res typassign := - do e' <- solve_constraints e; OK(makeassign e'). - -(** What it means to be a solution *) - -Definition satisf (te: typassign) (e: typenv) : Prop := - (forall x ty, e.(te_typ)!x = Some ty -> te x = ty) -/\ (forall x y, In (x, y) e.(te_equ) -> te x = te y). - -Lemma satisf_initial: forall te, satisf te initial. -Proof. - unfold initial; intros; split; simpl; intros. - rewrite PTree.gempty in H; discriminate. - contradiction. -Qed. - -(** Soundness proof *) - -Lemma set_incr: - forall te x ty e e', set e x ty = OK e' -> satisf te e' -> satisf te e. -Proof. - unfold set; intros. destruct (te_typ e)!x as [ty'|] eqn:E. -- destruct (T.eq ty ty'); inv H. auto. -- inv H. destruct H0 as [A B]; simpl in *. red; split; intros; auto. - apply A. rewrite PTree.gso by congruence. auto. -Qed. - -Hint Resolve set_incr: ty. - -Lemma set_sound: - forall te x ty e e', set e x ty = OK e' -> satisf te e' -> te x = ty. -Proof. - unfold set; intros. destruct H0 as [P Q]. - destruct (te_typ e)!x as [ty'|] eqn:E. -- destruct (T.eq ty ty'); inv H. eauto. -- inv H. simpl in P. apply P. apply PTree.gss. -Qed. - -Lemma set_list_incr: - forall te xl tyl e e', set_list e xl tyl = OK e' -> satisf te e' -> satisf te e. -Proof. - induction xl; destruct tyl; simpl; intros; monadInv H; eauto with ty. -Qed. - -Hint Resolve set_list_incr: ty. - -Lemma set_list_sound: - forall te xl tyl e e', set_list e xl tyl = OK e' -> satisf te e' -> map te xl = tyl. -Proof. - induction xl; destruct tyl; simpl; intros; monadInv H. - auto. - f_equal. eapply set_sound; eauto with ty. eauto. -Qed. - -Lemma move_incr: - forall te e r1 r2 e' changed, - move e r1 r2 = OK(changed, e') -> satisf te e' -> satisf te e. -Proof. - unfold move; intros. destruct H0 as [P Q]. - destruct (peq r1 r2). inv H; split; auto. - destruct (te_typ e)!r1 as [ty1|] eqn:E1; - destruct (te_typ e)!r2 as [ty2|] eqn:E2. -- destruct (T.eq ty1 ty2); inv H. split; auto. -- inv H; simpl in *; split; auto. intros. apply P. - rewrite PTree.gso by congruence. auto. -- inv H; simpl in *; split; auto. intros. apply P. - rewrite PTree.gso by congruence. auto. -- inv H; simpl in *; split; auto. -Qed. - -Hint Resolve move_incr: ty. - -Lemma move_sound: - forall te e r1 r2 e' changed, - move e r1 r2 = OK(changed, e') -> satisf te e' -> te r1 = te r2. -Proof. - unfold move; intros. destruct H0 as [P Q]. - destruct (peq r1 r2). congruence. - destruct (te_typ e)!r1 as [ty1|] eqn:E1; - destruct (te_typ e)!r2 as [ty2|] eqn:E2. -- destruct (T.eq ty1 ty2); inv H. erewrite ! P by eauto. auto. -- inv H; simpl in *. rewrite (P r1 ty1). rewrite (P r2 ty1). auto. - apply PTree.gss. rewrite PTree.gso by congruence. auto. -- inv H; simpl in *. rewrite (P r1 ty2). rewrite (P r2 ty2). auto. - rewrite PTree.gso by congruence. auto. apply PTree.gss. -- inv H; simpl in *. apply Q; auto. -Qed. - -Lemma solve_rec_incr: - forall te q e changed e' changed', - solve_rec e changed q = OK(e', changed') -> satisf te e' -> satisf te e. -Proof. - induction q; simpl; intros. -- inv H. auto. -- destruct a as [r1 r2]; monadInv H. eauto with ty. -Qed. - -Lemma solve_rec_sound: - forall te r1 r2 q e changed e' changed', - solve_rec e changed q = OK(e', changed') -> In (r1, r2) q -> satisf te e' -> - te r1 = te r2. -Proof. - induction q; simpl; intros. -- contradiction. -- destruct a as [r3 r4]; monadInv H. destruct H0. - + inv H. eapply move_sound; eauto. eapply solve_rec_incr; eauto. - + eapply IHq; eauto with ty. -Qed. - -Lemma move_false: - forall e r1 r2 e', - move e r1 r2 = OK(false, e') -> - te_typ e' = te_typ e /\ makeassign e r1 = makeassign e r2. -Proof. - unfold move; intros. - destruct (peq r1 r2). inv H. split; auto. - unfold makeassign; - destruct (te_typ e)!r1 as [ty1|] eqn:E1; - destruct (te_typ e)!r2 as [ty2|] eqn:E2. -- destruct (T.eq ty1 ty2); inv H. auto. -- discriminate. -- discriminate. -- inv H. split; auto. -Qed. - -Lemma solve_rec_false: - forall r1 r2 q e changed e', - solve_rec e changed q = OK(e', false) -> - changed = false /\ - (In (r1, r2) q -> makeassign e r1 = makeassign e r2). -Proof. - induction q; simpl; intros. -- inv H. tauto. -- destruct a as [r3 r4]; monadInv H. - exploit IHq; eauto. intros [P Q]. - destruct changed; try discriminate. destruct x; try discriminate. - exploit move_false; eauto. intros [U V]. - split. auto. intros [A|A]. inv A. auto. exploit Q; auto. - unfold makeassign; rewrite U; auto. -Qed. - -Lemma solve_constraints_incr: - forall te e e', solve_constraints e = OK e' -> satisf te e' -> satisf te e. -Proof. - intros te e; functional induction (solve_constraints e); intros. -- inv H. auto. -- exploit solve_rec_incr; eauto. intros [A B]. - split; auto. intros; eapply solve_rec_sound; eauto. -- discriminate. -Qed. - -Lemma solve_constraints_sound: - forall e e', solve_constraints e = OK e' -> satisf (makeassign e') e'. -Proof. - intros e0; functional induction (solve_constraints e0); intros. -- inv H. split; intros. - unfold makeassign; rewrite H. split; auto with ty. - exploit solve_rec_false. eauto. intros [A B]. eapply B; eauto. -- eauto. -- discriminate. -Qed. - -Theorem solve_sound: - forall e te, solve e = OK te -> satisf te e. -Proof. - unfold solve; intros. monadInv H. - eapply solve_constraints_incr. eauto. eapply solve_constraints_sound; eauto. -Qed. - -(** Completeness proof *) - -Lemma set_complete: - forall te e x ty, - satisf te e -> te x = ty -> exists e', set e x ty = OK e' /\ satisf te e'. -Proof. - unfold set; intros. generalize H; intros [P Q]. - destruct (te_typ e)!x as [ty1|] eqn:E. -- replace ty1 with ty. rewrite dec_eq_true. exists e; auto. - exploit P; eauto. congruence. -- econstructor; split; eauto. split; simpl; intros; auto. - rewrite PTree.gsspec in H1. destruct (peq x0 x). congruence. eauto. -Qed. - -Lemma set_list_complete: - forall te xl tyl e, - satisf te e -> map te xl = tyl -> - exists e', set_list e xl tyl = OK e' /\ satisf te e'. -Proof. - induction xl; intros; inv H0; simpl. - econstructor; eauto. - exploit (set_complete te e a (te a)); auto. intros (e1 & P & Q). - exploit (IHxl (map te xl) e1); auto. intros (e2 & U & V). - exists e2; split; auto. rewrite P; auto. -Qed. - -Lemma move_complete: - forall te e r1 r2, - satisf te e -> te r1 = te r2 -> - exists changed e', move e r1 r2 = OK(changed, e') /\ satisf te e'. -Proof. - unfold move; intros. elim H; intros P Q. - assert (Q': forall x y, In (x, y) ((r1, r2) :: te_equ e) -> te x = te y). - { intros. destruct H1; auto. congruence. } - destruct (peq r1 r2). econstructor; econstructor; eauto. - destruct (te_typ e)!r1 as [ty1|] eqn:E1; - destruct (te_typ e)!r2 as [ty2|] eqn:E2. -- replace ty2 with ty1. rewrite dec_eq_true. econstructor; econstructor; eauto. - exploit (P r1); eauto. exploit (P r2); eauto. congruence. -- econstructor; econstructor; split; eauto. - split; simpl; intros; auto. rewrite PTree.gsspec in H1. destruct (peq x r2). - inv H1. rewrite <- H0. eauto. - eauto. -- econstructor; econstructor; split; eauto. - split; simpl; intros; auto. rewrite PTree.gsspec in H1. destruct (peq x r1). - inv H1. rewrite H0. eauto. - eauto. -- econstructor; econstructor; split; eauto. - split; eauto. -Qed. - -Lemma solve_rec_complete: - forall te q e changed, - satisf te e -> - (forall r1 r2, In (r1, r2) q -> te r1 = te r2) -> - exists e' changed', solve_rec e changed q = OK(e', changed') /\ satisf te e'. -Proof. - induction q; simpl; intros. -- econstructor; econstructor; eauto. -- destruct a as [r1 r2]. - exploit (move_complete te e r1 r2); auto. intros (changed1 & e1 & A & B). - exploit (IHq e1 (changed || changed1)); auto. intros (e' & changed' & C & D). - exists e'; exists changed'. rewrite A; simpl; rewrite C; auto. -Qed. - -Lemma solve_constraints_complete: - forall te e, satisf te e -> exists e', solve_constraints e = OK e' /\ satisf te e'. -Proof. - intros te e. functional induction (solve_constraints e); intros. -- exists e; auto. -- exploit (solve_rec_complete te (te_equ e) {| te_typ := te_typ e; te_equ := nil |} false). - destruct H; split; auto. simpl; tauto. - destruct H; auto. - intros (e1 & changed1 & P & Q). - apply IHr. congruence. -- exploit (solve_rec_complete te (te_equ e) {| te_typ := te_typ e; te_equ := nil |} false). - destruct H; split; auto. simpl; tauto. - destruct H; auto. - intros (e1 & changed1 & P & Q). - congruence. -Qed. - -Lemma solve_complete: - forall te e, satisf te e -> exists te', solve e = OK te'. -Proof. - intros. unfold solve. - destruct (solve_constraints_complete te e H) as (e' & P & Q). - econstructor. rewrite P. simpl. eauto. -Qed. - -End UniSolver. - |