Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


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

1 files changed, 8 insertions, 11 deletions

diff --git a/Makefile b/Makefile
index fed2660..0db4118 100644
--- a/Makefile
+++ b/Makefile
@@ -55,7 +55,7 @@ FLOCQ=$(FLOCQ_CORE) $(FLOCQ_PROP) $(FLOCQ_CALC) $(FLOCQ_APPLI)
 
 LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
   Iteration.v Integers.v Floats.v Parmov.v UnionFind.v Wfsimpl.v \
-  Postorder.v
+  Postorder.v FSetAVLplus.v
 
 # Parts common to the front-ends and the back-end (in common/)
 
@@ -66,7 +66,8 @@ COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \
 
 BACKEND=\
   Cminor.v Op.v CminorSel.v \
-  SelectOp.v Selection.v SelectOpproof.v Selectionproof.v \
+  SelectOp.v SelectLong.v Selection.v \
+  SelectOpproof.v SelectLongproof.v Selectionproof.v \
   Registers.v RTL.v \
   RTLgen.v RTLgenspec.v RTLgenproof.v \
   Tailcall.v Tailcallproof.v \
@@ -76,16 +77,12 @@ BACKEND=\
   Kildall.v Liveness.v \
   ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
   CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
-  Machregs.v Locations.v Conventions1.v Conventions.v LTL.v LTLtyping.v \
-  InterfGraph.v Coloring.v Coloringproof.v \
-  Allocation.v Allocproof.v Alloctyping.v \
-  Tunneling.v Tunnelingproof.v Tunnelingtyping.v \
-  LTLin.v LTLintyping.v \
-  Linearize.v Linearizeproof.v Linearizetyping.v \
-  CleanupLabels.v CleanupLabelsproof.v CleanupLabelstyping.v \
+  Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \
+  Allocation.v Allocproof.v \
+  Tunneling.v Tunnelingproof.v \
   Linear.v Lineartyping.v \
-  Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \
-  RRE.v RREproof.v RREtyping.v \
+  Linearize.v Linearizeproof.v \
+  CleanupLabels.v CleanupLabelsproof.v \
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
   Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v