From e882493e2c4b91024b42f0603ca6869e95695e85 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 27 Oct 2007 10:23:16 +0000 Subject: 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 --- extraction/.depend | 27 +++++++++++++++------------ extraction/Linearize.ml.patch | 22 ---------------------- extraction/Makefile | 2 +- extraction/extraction.v | 3 +++ 4 files changed, 19 insertions(+), 35 deletions(-) delete mode 100644 extraction/Linearize.ml.patch (limited to 'extraction') 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". -- cgit v1.2.3