Merge of branch "unsigned-offsets":

- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int.
  (Fixes issue with wrong comparison of pointers across 0x8000_0000)
- Revised Stacking pass to not use negative SP offsets.
- Add pointer validity checks to Cminor ... Mach
  to support the use of memory injections in Stacking.
- Cleaned up Stacklayout modules.
- IA32: improved code generation for Mgetparam.
- ARM: improved code generation for op-immediate instructions.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 9 deletions

diff --git a/.depend b/.depend
index 8cf28b2..941c6d7 100644
--- a/.depend
+++ b/.depend
@@ -22,7 +22,7 @@ common/Smallstep.vo common/Smallstep.glob: common/Smallstep.v lib/Coqlib.vo comm
 common/Determinism.vo common/Determinism.glob: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo
 common/Switch.vo common/Switch.glob: common/Switch.v lib/Coqlib.vo lib/Integers.vo lib/Ordered.vo
 backend/Cminor.vo backend/Cminor.glob: 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 lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Globalenvs.vo
+$(ARCH)/Op.vo $(ARCH)/Op.glob: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Globalenvs.vo common/Events.vo
 backend/CminorSel.vo backend/CminorSel.glob: backend/CminorSel.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 backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo
 $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob: $(ARCH)/SelectOp.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo
 backend/Selection.vo backend/Selection.glob: backend/Selection.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
@@ -66,21 +66,19 @@ backend/Linearize.vo backend/Linearize.glob: backend/Linearize.v lib/Coqlib.vo l
 backend/Linearizeproof.vo backend/Linearizeproof.glob: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo lib/Lattice.vo
 backend/Linearizetyping.vo backend/Linearizetyping.glob: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo backend/Conventions.vo
 backend/Linear.vo backend/Linear.glob: backend/Linear.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo
-backend/Lineartyping.vo backend/Lineartyping.glob: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo
+backend/Lineartyping.vo backend/Lineartyping.glob: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Conventions.vo
 backend/Parallelmove.vo backend/Parallelmove.glob: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo common/Values.vo common/Events.vo common/AST.vo backend/Locations.vo backend/Conventions.vo
 backend/Reload.vo backend/Reload.glob: backend/Reload.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo backend/Parallelmove.vo backend/Linear.vo
 backend/Reloadproof.vo backend/Reloadproof.glob: backend/Reloadproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Parallelmove.vo backend/Reload.vo
 backend/Reloadtyping.vo backend/Reloadtyping.glob: backend/Reloadtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Parallelmove.vo backend/Reload.vo backend/Reloadproof.vo
-backend/Mach.vo backend/Mach.glob: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo
-backend/Machabstr.vo backend/Machabstr.glob: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo
-backend/Machtyping.vo backend/Machtyping.glob: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machabstr.vo
+backend/Mach.vo backend/Mach.glob: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo
+backend/Machtyping.vo backend/Machtyping.glob: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo
 backend/Bounds.vo backend/Bounds.glob: backend/Bounds.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo
 $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob: $(ARCH)/$(VARIANT)/Stacklayout.v lib/Coqlib.vo backend/Bounds.vo
 backend/Stacking.vo backend/Stacking.glob: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo
-backend/Stackingproof.vo backend/Stackingproof.glob: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machabstr.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo
+backend/Stackingproof.vo backend/Stackingproof.glob: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machconcr.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo
 backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingproof.vo
 backend/Machconcr.vo backend/Machconcr.glob: backend/Machconcr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo
-backend/Machabstr2concr.vo backend/Machabstr2concr.glob: backend/Machabstr2concr.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/Machabstr.vo backend/Machconcr.vo backend/Conventions.vo $(ARCH)/Asmgenretaddr.vo
 $(ARCH)/Asm.vo $(ARCH)/Asm.glob: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo
 $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
 $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo 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
@@ -90,7 +88,7 @@ cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo c
 cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo
 cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
 cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
-cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo
+cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo
 cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo
 cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo
 cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo 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/Smallstep.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo
@@ -100,5 +98,5 @@ cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v
 cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.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 backend/Cminor.vo common/Smallstep.vo
 cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo
 cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo
-driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo
+driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo
 driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo