Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG

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

4 files changed, 19 insertions, 35 deletions

diff --git a/extraction/.depend b/extraction/.depend
index 6ed07d8..60534fd 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -42,10 +42,10 @@
     ../caml/CMlexer.cmx 
 ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo 
 ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx 
-../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
-    ../caml/Camlcoq.cmo CList.cmi AST.cmi 
-../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
-    ../caml/Camlcoq.cmx CList.cmx AST.cmx 
+../caml/Linearizeaux.cmo: Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
+    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi 
+../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTLin.cmx LTL.cmx \
+    Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx 
 ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
     CList.cmi AST.cmi 
 ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
@@ -129,8 +129,9 @@ Kildall.cmi: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \
     BinPos.cmi BinInt.cmi 
 Lattice.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
     BinPos.cmi 
-Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
+Linearize.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \
+    Lattice.cmi LTLin.cmi LTL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
+    CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
 Linear.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
     Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi 
@@ -351,12 +352,14 @@ Lattice.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
     BinPos.cmi Lattice.cmi 
 Lattice.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Bool.cmx \
     BinPos.cmx Lattice.cmi 
-Linearize.cmo: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
-    Kildall.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi \
-    Linearize.cmi 
-Linearize.cmx: Specif.cmx Op.cmx Maps.cmx Lattice.cmx LTLin.cmx LTL.cmx \
-    Kildall.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx AST.cmx \
-    Linearize.cmi 
+Linearize.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \
+    ../caml/Linearizeaux.cmo Lattice.cmi LTLin.cmi LTL.cmi Kildall.cmi \
+    FSetAVL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi \
+    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Linearize.cmi 
+Linearize.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Op.cmx Maps.cmx \
+    ../caml/Linearizeaux.cmx Lattice.cmx LTLin.cmx LTL.cmx Kildall.cmx \
+    FSetAVL.cmx Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx \
+    BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx Linearize.cmi 
 Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
     Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi Linear.cmi 
diff --git a/extraction/Linearize.ml.patch b/extraction/Linearize.ml.patch
deleted file mode 100644
index 47b6cc9..0000000
--- a/extraction/Linearize.ml.patch
+++ /dev/null
@@ -1,22 +0,0 @@
-*** Linearize.ml.orig	2006-02-09 11:47:55.000000000 +0100
---- Linearize.ml	2006-02-09 11:58:42.000000000 +0100
-***************
-*** 28,35 ****
-  (** val enumerate : LTL.coq_function -> node list **)
-  
-  let enumerate f =
-    positive_rec Coq_nil (fun pc nodes ->
-!     match Maps.PMap.get pc (reachable f) with
-        | true -> Coq_cons (pc, nodes)
-        | false -> nodes) (coq_Psucc f.fn_entrypoint)
-  
---- 28,36 ----
-  (** val enumerate : LTL.coq_function -> node list **)
-  
-  let enumerate f =
-+   let reach = reachable f in
-    positive_rec Coq_nil (fun pc nodes ->
-!     match Maps.PMap.get pc reach with
-        | true -> Coq_cons (pc, nodes)
-        | false -> nodes) (coq_Psucc f.fn_entrypoint)
-  
diff --git a/extraction/Makefile b/extraction/Makefile
index 4274e8e..513577c 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -23,7 +23,7 @@ FILES=\
   LTL.ml LTLin.ml \
   InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \
   Allocation.ml  \
-  Tunneling.ml Linear.ml Linearize.ml \
+  Tunneling.ml Linear.ml ../caml/Linearizeaux.ml Linearize.ml \
   Parallelmove.ml Reload.ml \
   Mach.ml Bounds.ml Stacking.ml \
   PPC.ml PPCgen.ml \
diff --git a/extraction/extraction.v b/extraction/extraction.v
index cc33c98..e0f965d 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -47,6 +47,9 @@ Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_en
 (* Coloring *)
 Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring".
 
+(* Linearize *)
+Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
+
 (* PPC *)
 Extract Constant PPC.low_half_signed => "fun _ -> assert false".
 Extract Constant PPC.high_half_signed => "fun _ -> assert false".