summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.depend20
-rw-r--r--Makefile2
-rw-r--r--backend/Allocation.v117
-rw-r--r--backend/Allocproof.v254
-rw-r--r--backend/Lineartyping.v708
-rw-r--r--backend/Locations.v24
-rw-r--r--backend/RTLtyping.v428
-rw-r--r--backend/Stackingproof.v206
-rw-r--r--common/Unityping.v435
9 files changed, 672 insertions, 1522 deletions
diff --git a/.depend b/.depend
index 7307c32..bcddfbc 100644
--- a/.depend
+++ b/.depend
@@ -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
diff --git a/Makefile b/Makefile
index 87a4977..d206461 100644
--- a/Makefile
+++ b/Makefile
@@ -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.
-