Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


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

1 files changed, 10 insertions, 3 deletions

diff --git a/.depend b/.depend
index 3d6e10c..1b50427 100644
--- a/.depend
+++ b/.depend
@@ -5,18 +5,20 @@ lib/Maps.vo lib/Maps.glob: lib/Maps.v lib/Coqlib.vo
 lib/Heaps.vo lib/Heaps.glob: lib/Heaps.v lib/Coqlib.vo lib/Ordered.vo
 lib/Lattice.vo lib/Lattice.glob: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo
 lib/Ordered.vo lib/Ordered.glob: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo
-lib/Iteration.vo lib/Iteration.glob: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo
+lib/Iteration.vo lib/Iteration.glob: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo lib/Wfsimpl.vo
 lib/Integers.vo lib/Integers.glob: lib/Integers.v lib/Axioms.vo lib/Coqlib.vo
 lib/Floats.vo lib/Floats.glob: lib/Floats.v lib/Coqlib.vo lib/Integers.vo
 lib/Parmov.vo lib/Parmov.glob: lib/Parmov.v lib/Axioms.vo lib/Coqlib.vo
 lib/UnionFind.vo lib/UnionFind.glob: lib/UnionFind.v lib/Coqlib.vo
+lib/Wfsimpl.vo lib/Wfsimpl.glob: lib/Wfsimpl.v lib/Axioms.vo
+lib/Postorder.vo lib/Postorder.glob: lib/Postorder.v lib/Coqlib.vo lib/Maps.vo lib/Iteration.vo
 common/Errors.vo common/Errors.glob: common/Errors.v lib/Coqlib.vo
 common/AST.vo common/AST.glob: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo
 common/Events.vo common/Events.glob: common/Events.v lib/Coqlib.vo lib/Intv.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Errors.vo
 common/Globalenvs.vo common/Globalenvs.glob: common/Globalenvs.v lib/Axioms.vo 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/Memdata.vo common/Memdata.glob: common/Memdata.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo
 common/Memtype.vo common/Memtype.glob: common/Memtype.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo
-common/Memory.vo common/Memory.glob: common/Memory.v lib/Axioms.vo lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo
+common/Memory.vo common/Memory.glob: common/Memory.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo lib/Intv.vo
 common/Values.vo common/Values.glob: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo
 common/Smallstep.vo common/Smallstep.glob: common/Smallstep.v lib/Coqlib.vo common/AST.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo
 common/Behaviors.vo common/Behaviors.glob: common/Behaviors.v lib/Coqlib.vo common/AST.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo
@@ -36,6 +38,11 @@ backend/RTLgenspec.vo backend/RTLgenspec.glob: backend/RTLgenspec.v lib/Coqlib.v
 backend/RTLgenproof.vo backend/RTLgenproof.glob: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo common/Switch.vo backend/Registers.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenspec.vo common/Errors.vo
 backend/Tailcall.vo backend/Tailcall.glob: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo
 backend/Tailcallproof.vo backend/Tailcallproof.glob: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Tailcall.vo
+backend/Inlining.vo backend/Inlining.glob: backend/Inlining.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo
+backend/Inliningspec.vo backend/Inliningspec.glob: backend/Inliningspec.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Inlining.vo
+backend/Inliningproof.vo backend/Inliningproof.glob: 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 lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo common/AST.vo backend/RTL.vo
+backend/Renumberproof.vo backend/Renumberproof.glob: backend/Renumberproof.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo common/AST.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 backend/Renumber.vo
 backend/RTLtyping.vo backend/RTLtyping.glob: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo common/Memory.vo lib/Integers.vo common/Events.vo common/Smallstep.vo backend/RTL.vo backend/Conventions.vo
 backend/Kildall.vo backend/Kildall.glob: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo
 $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo
@@ -104,5 +111,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 lib/Floats.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/Cexec.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 backend/Machsem.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/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/RRE.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/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/RREproof.vo backend/RREtyping.vo backend/Stackingproof.vo backend/Stackingtyping.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/Cexec.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 backend/Machsem.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/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/RRE.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/Inliningproof.vo backend/Renumberproof.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/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/RREproof.vo backend/RREtyping.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/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo