From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/.depend | 395 ++++++++++++++++++++++++++++++++++++++++++ extraction/Kildall.ml.patch | 22 +++ extraction/Linearize.ml.patch | 22 +++ extraction/Makefile | 91 ++++++++++ extraction/extraction.v | 53 ++++++ extraction/uncapitalize | 6 + 6 files changed, 589 insertions(+) create mode 100644 extraction/.depend create mode 100644 extraction/Kildall.ml.patch create mode 100644 extraction/Linearize.ml.patch create mode 100644 extraction/Makefile create mode 100644 extraction/extraction.v create mode 100755 extraction/uncapitalize (limited to 'extraction') diff --git a/extraction/.depend b/extraction/.depend new file mode 100644 index 0000000..1067a0a --- /dev/null +++ b/extraction/.depend @@ -0,0 +1,395 @@ +../caml/Allocationaux.cmi: Locations.cmi List.cmi Datatypes.cmi +../caml/CMlexer.cmi: ../caml/CMparser.cmi +../caml/CMparser.cmi: Cminor.cmi AST.cmi +../caml/Coloringaux.cmi: Registers.cmi RTLtyping.cmi RTL.cmi Locations.cmi \ + InterfGraph.cmi +../caml/PrintPPC.cmi: PPC.cmi +../caml/Allocationaux.cmo: Locations.cmi List.cmi Datatypes.cmi \ + ../caml/Camlcoq.cmo AST.cmi ../caml/Allocationaux.cmi +../caml/Allocationaux.cmx: Locations.cmx List.cmx Datatypes.cmx \ + ../caml/Camlcoq.cmx AST.cmx ../caml/Allocationaux.cmi +../caml/Camlcoq.cmo: List.cmi Integers.cmi Datatypes.cmi BinPos.cmi \ + BinInt.cmi +../caml/Camlcoq.cmx: List.cmx Integers.cmx Datatypes.cmx BinPos.cmx \ + BinInt.cmx +../caml/CMlexer.cmo: ../caml/Camlcoq.cmo ../caml/CMparser.cmi \ + ../caml/CMlexer.cmi +../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \ + ../caml/CMlexer.cmi +../caml/CMparser.cmo: Op.cmi List.cmi Integers.cmi Datatypes.cmi Cminor.cmi \ + Cmconstr.cmi ../caml/Camlcoq.cmo BinPos.cmi BinInt.cmi AST.cmi \ + ../caml/CMparser.cmi +../caml/CMparser.cmx: Op.cmx List.cmx Integers.cmx Datatypes.cmx Cminor.cmx \ + Cmconstr.cmx ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx \ + ../caml/CMparser.cmi +../caml/Coloringaux.cmo: Registers.cmi RTLtyping.cmi RTL.cmi Maps.cmi \ + Locations.cmi InterfGraph.cmi Datatypes.cmi Conventions.cmi \ + ../caml/Camlcoq.cmo BinPos.cmi BinInt.cmi AST.cmi ../caml/Coloringaux.cmi +../caml/Coloringaux.cmx: Registers.cmx RTLtyping.cmx RTL.cmx Maps.cmx \ + Locations.cmx InterfGraph.cmx Datatypes.cmx Conventions.cmx \ + ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx ../caml/Coloringaux.cmi +../caml/Floataux.cmo: ../caml/Camlcoq.cmo AST.cmi +../caml/Floataux.cmx: ../caml/Camlcoq.cmx AST.cmx +../caml/Main2.cmo: ../caml/PrintPPC.cmi Main.cmi Datatypes.cmi \ + ../caml/CMparser.cmi ../caml/CMlexer.cmi +../caml/Main2.cmx: ../caml/PrintPPC.cmx Main.cmx Datatypes.cmx \ + ../caml/CMparser.cmx ../caml/CMlexer.cmx +../caml/PrintPPC.cmo: PPC.cmi List.cmi Datatypes.cmi ../caml/Camlcoq.cmo \ + AST.cmi ../caml/PrintPPC.cmi +../caml/PrintPPC.cmx: PPC.cmx List.cmx Datatypes.cmx ../caml/Camlcoq.cmx \ + AST.cmx ../caml/PrintPPC.cmi +../caml/RTLgenaux.cmo: Cminor.cmi +../caml/RTLgenaux.cmx: Cminor.cmx +Allocation.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \ + Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi List.cmi LTL.cmi \ + Datatypes.cmi Conventions.cmi Coloring.cmi BinPos.cmi AST.cmi +AST.cmi: Specif.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi +BinInt.cmi: Datatypes.cmi BinPos.cmi BinNat.cmi +BinNat.cmi: Datatypes.cmi BinPos.cmi +BinPos.cmi: Peano.cmi Datatypes.cmi +Bool.cmi: Specif.cmi Datatypes.cmi +Cmconstr.cmi: Specif.cmi Op.cmi List.cmi Integers.cmi Datatypes.cmi \ + Compare_dec.cmi Cminor.cmi BinPos.cmi BinInt.cmi AST.cmi +Cminorgen.cmi: Zmin.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi List.cmi \ + Integers.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi \ + Cmconstr.cmi BinPos.cmi BinInt.cmi AST.cmi +Cminor.cmi: Values.cmi Op.cmi Maps.cmi List.cmi Globalenvs.cmi Datatypes.cmi \ + BinInt.cmi AST.cmi +Coloring.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \ + Locations.cmi List.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi \ + Conventions.cmi BinInt.cmi AST.cmi +Compare_dec.cmi: Specif.cmi Datatypes.cmi +Constprop.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \ + Integers.cmi Floats.cmi Datatypes.cmi Bool.cmi BinPos.cmi BinInt.cmi \ + AST.cmi +Conventions.cmi: Locations.cmi List.cmi Datatypes.cmi BinPos.cmi BinInt.cmi \ + AST.cmi +Coqlib.cmi: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi List.cmi Datatypes.cmi \ + BinPos.cmi BinInt.cmi +CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \ + Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi +Csharpminor.cmi: Zmin.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi List.cmi \ + Integers.cmi Globalenvs.cmi Floats.cmi Datatypes.cmi BinPos.cmi \ + BinInt.cmi AST.cmi +Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi AST.cmi +FSetAVL.cmi: ZArith_dec.cmi Wf.cmi Specif.cmi Peano.cmi List.cmi \ + FSetInterface.cmi Datatypes.cmi BinPos.cmi BinInt.cmi +FSetBridge.cmi: Specif.cmi List.cmi FSetInterface.cmi Datatypes.cmi +FSetInterface.cmi: Specif.cmi List.cmi Datatypes.cmi +FSetList.cmi: Specif.cmi List.cmi FSetInterface.cmi Datatypes.cmi +Globalenvs.cmi: Values.cmi Mem.cmi Maps.cmi List.cmi Integers.cmi \ + Datatypes.cmi BinPos.cmi BinInt.cmi AST.cmi +Integers.cmi: Zpower.cmi Zdiv.cmi Specif.cmi List.cmi Datatypes.cmi \ + Coqlib.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi +InterfGraph.cmi: Specif.cmi Registers.cmi Locations.cmi List.cmi \ + FSetInterface.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi +Kildall.cmi: Wf.cmi Specif.cmi Maps.cmi List.cmi Lattice.cmi Datatypes.cmi \ + Coqlib.cmi BinPos.cmi +Lattice.cmi: Specif.cmi Maps.cmi Datatypes.cmi BinPos.cmi +Linearize.cmi: Specif.cmi Op.cmi Maps.cmi List.cmi Linear.cmi Lattice.cmi \ + LTL.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi +Linear.cmi: Values.cmi Specif.cmi Op.cmi Locations.cmi List.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi +Lineartyping.cmi: Zmin.cmi Locations.cmi List.cmi Linear.cmi Datatypes.cmi \ + Conventions.cmi BinPos.cmi BinInt.cmi AST.cmi +List.cmi: Specif.cmi Datatypes.cmi +Locations.cmi: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ + BinInt.cmi AST.cmi +LTL.cmi: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi List.cmi \ + Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi BinPos.cmi \ + BinInt.cmi AST.cmi +Mach.cmi: Zmin.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi \ + Locations.cmi List.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi \ + Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi +Main.cmi: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \ + Linearize.cmi Datatypes.cmi Csharpminor.cmi Constprop.cmi Cminorgen.cmi \ + Cminor.cmi CSE.cmi Allocation.cmi AST.cmi +Maps.cmi: Specif.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinNat.cmi \ + BinInt.cmi +Mem.cmi: Values.cmi Specif.cmi List.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ + BinPos.cmi BinInt.cmi AST.cmi +Op.cmi: Values.cmi Specif.cmi List.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ + Datatypes.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi +Ordered.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Coqlib.cmi \ + BinPos.cmi +Parallelmove.cmi: Wf.cmi Values.cmi Specif.cmi Peano.cmi Locations.cmi \ + List.cmi LTL.cmi Datatypes.cmi AST.cmi +Peano.cmi: Datatypes.cmi +PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi List.cmi \ + Integers.cmi Datatypes.cmi Coqlib.cmi Bool.cmi BinPos.cmi BinInt.cmi \ + AST.cmi +PPC.cmi: Values.cmi Specif.cmi Mem.cmi List.cmi Integers.cmi Globalenvs.cmi \ + Floats.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi +Registers.cmi: Specif.cmi Maps.cmi List.cmi Datatypes.cmi Coqlib.cmi \ + BinPos.cmi AST.cmi +RTLgen.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \ + Datatypes.cmi Coqlib.cmi Cminor.cmi BinPos.cmi AST.cmi +RTL.cmi: Values.cmi Registers.cmi Op.cmi Maps.cmi List.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi BinPos.cmi BinInt.cmi AST.cmi +RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \ + Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi +Sets.cmi: Specif.cmi Maps.cmi List.cmi Datatypes.cmi +Specif.cmi: Datatypes.cmi +Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi List.cmi \ + Lineartyping.cmi Linear.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ + Conventions.cmi BinPos.cmi BinInt.cmi AST.cmi +Sumbool.cmi: Specif.cmi Datatypes.cmi +Tunneling.cmi: Maps.cmi List.cmi LTL.cmi Datatypes.cmi AST.cmi +union_find.cmi: Wf.cmi Specif.cmi Datatypes.cmi +Values.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ + BinPos.cmi BinInt.cmi AST.cmi +ZArith_dec.cmi: Sumbool.cmi Specif.cmi Datatypes.cmi BinInt.cmi +Zbool.cmi: Zeven.cmi ZArith_dec.cmi Sumbool.cmi Specif.cmi Datatypes.cmi \ + BinInt.cmi +Zdiv.cmi: Zbool.cmi ZArith_dec.cmi Specif.cmi Datatypes.cmi BinPos.cmi \ + BinInt.cmi +Zeven.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi +Zmin.cmi: Datatypes.cmi BinInt.cmi +Zmisc.cmi: Datatypes.cmi BinPos.cmi BinInt.cmi +Zpower.cmi: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi +Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \ + Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi List.cmi LTL.cmi \ + Kildall.cmi Datatypes.cmi Conventions.cmi Coloring.cmi BinPos.cmi AST.cmi \ + Allocation.cmi +Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx \ + Parallelmove.cmx Op.cmx Maps.cmx Locations.cmx List.cmx LTL.cmx \ + Kildall.cmx Datatypes.cmx Conventions.cmx Coloring.cmx BinPos.cmx AST.cmx \ + Allocation.cmi +AST.cmo: Specif.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi \ + AST.cmi +AST.cmx: Specif.cmx List.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx BinInt.cmx \ + AST.cmi +BinInt.cmo: Datatypes.cmi BinPos.cmi BinNat.cmi BinInt.cmi +BinInt.cmx: Datatypes.cmx BinPos.cmx BinNat.cmx BinInt.cmi +BinNat.cmo: Datatypes.cmi BinPos.cmi BinNat.cmi +BinNat.cmx: Datatypes.cmx BinPos.cmx BinNat.cmi +BinPos.cmo: Peano.cmi Datatypes.cmi BinPos.cmi +BinPos.cmx: Peano.cmx Datatypes.cmx BinPos.cmi +Bool.cmo: Specif.cmi Datatypes.cmi Bool.cmi +Bool.cmx: Specif.cmx Datatypes.cmx Bool.cmi +Cmconstr.cmo: Specif.cmi Op.cmi List.cmi Integers.cmi Datatypes.cmi \ + Compare_dec.cmi Cminor.cmi BinPos.cmi BinInt.cmi AST.cmi Cmconstr.cmi +Cmconstr.cmx: Specif.cmx Op.cmx List.cmx Integers.cmx Datatypes.cmx \ + Compare_dec.cmx Cminor.cmx BinPos.cmx BinInt.cmx AST.cmx Cmconstr.cmi +Cminorgen.cmo: Zmin.cmi Specif.cmi Sets.cmi Op.cmi Mem.cmi Maps.cmi List.cmi \ + Integers.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi \ + Cmconstr.cmi BinPos.cmi BinInt.cmi AST.cmi Cminorgen.cmi +Cminorgen.cmx: Zmin.cmx Specif.cmx Sets.cmx Op.cmx Mem.cmx Maps.cmx List.cmx \ + Integers.cmx Datatypes.cmx Csharpminor.cmx Coqlib.cmx Cminor.cmx \ + Cmconstr.cmx BinPos.cmx BinInt.cmx AST.cmx Cminorgen.cmi +Cminor.cmo: Values.cmi Op.cmi Maps.cmi List.cmi Globalenvs.cmi Datatypes.cmi \ + BinInt.cmi AST.cmi Cminor.cmi +Cminor.cmx: Values.cmx Op.cmx Maps.cmx List.cmx Globalenvs.cmx Datatypes.cmx \ + BinInt.cmx AST.cmx Cminor.cmi +Coloring.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \ + Locations.cmi List.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi \ + Conventions.cmi ../caml/Coloringaux.cmi BinInt.cmi AST.cmi Coloring.cmi +Coloring.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx Op.cmx Maps.cmx \ + Locations.cmx List.cmx InterfGraph.cmx Datatypes.cmx Coqlib.cmx \ + Conventions.cmx ../caml/Coloringaux.cmx BinInt.cmx AST.cmx Coloring.cmi +Compare_dec.cmo: Specif.cmi Datatypes.cmi Compare_dec.cmi +Compare_dec.cmx: Specif.cmx Datatypes.cmx Compare_dec.cmi +Constprop.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \ + Lattice.cmi Kildall.cmi Integers.cmi Floats.cmi Datatypes.cmi Bool.cmi \ + BinPos.cmi BinInt.cmi AST.cmi Constprop.cmi +Constprop.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx List.cmx \ + Lattice.cmx Kildall.cmx Integers.cmx Floats.cmx Datatypes.cmx Bool.cmx \ + BinPos.cmx BinInt.cmx AST.cmx Constprop.cmi +Conventions.cmo: Locations.cmi List.cmi Datatypes.cmi BinPos.cmi BinInt.cmi \ + AST.cmi Conventions.cmi +Conventions.cmx: Locations.cmx List.cmx Datatypes.cmx BinPos.cmx BinInt.cmx \ + AST.cmx Conventions.cmi +Coqlib.cmo: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi List.cmi Datatypes.cmi \ + BinPos.cmi BinInt.cmi Coqlib.cmi +Coqlib.cmx: Zdiv.cmx ZArith_dec.cmx Wf.cmx Specif.cmx List.cmx Datatypes.cmx \ + BinPos.cmx BinInt.cmx Coqlib.cmi +CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \ + Kildall.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ + AST.cmi CSE.cmi +CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx List.cmx \ + Kildall.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \ + AST.cmx CSE.cmi +Csharpminor.cmo: Zmin.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi List.cmi \ + Integers.cmi Globalenvs.cmi Floats.cmi Datatypes.cmi BinPos.cmi \ + BinInt.cmi AST.cmi Csharpminor.cmi +Csharpminor.cmx: Zmin.cmx Values.cmx Specif.cmx Mem.cmx Maps.cmx List.cmx \ + Integers.cmx Globalenvs.cmx Floats.cmx Datatypes.cmx BinPos.cmx \ + BinInt.cmx AST.cmx Csharpminor.cmi +Datatypes.cmo: Datatypes.cmi +Datatypes.cmx: Datatypes.cmi +Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \ + AST.cmi Floats.cmi +Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \ + AST.cmx Floats.cmi +FSetAVL.cmo: ZArith_dec.cmi Wf.cmi Specif.cmi Peano.cmi List.cmi FSetList.cmi \ + FSetInterface.cmi Datatypes.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi +FSetAVL.cmx: ZArith_dec.cmx Wf.cmx Specif.cmx Peano.cmx List.cmx FSetList.cmx \ + FSetInterface.cmx Datatypes.cmx BinPos.cmx BinInt.cmx FSetAVL.cmi +FSetBridge.cmo: Specif.cmi List.cmi FSetInterface.cmi Datatypes.cmi \ + FSetBridge.cmi +FSetBridge.cmx: Specif.cmx List.cmx FSetInterface.cmx Datatypes.cmx \ + FSetBridge.cmi +FSetInterface.cmo: Specif.cmi List.cmi Datatypes.cmi FSetInterface.cmi +FSetInterface.cmx: Specif.cmx List.cmx Datatypes.cmx FSetInterface.cmi +FSetList.cmo: Specif.cmi List.cmi FSetInterface.cmi Datatypes.cmi \ + FSetList.cmi +FSetList.cmx: Specif.cmx List.cmx FSetInterface.cmx Datatypes.cmx \ + FSetList.cmi +Globalenvs.cmo: Values.cmi Mem.cmi Maps.cmi List.cmi Integers.cmi \ + Datatypes.cmi BinPos.cmi BinInt.cmi AST.cmi Globalenvs.cmi +Globalenvs.cmx: Values.cmx Mem.cmx Maps.cmx List.cmx Integers.cmx \ + Datatypes.cmx BinPos.cmx BinInt.cmx AST.cmx Globalenvs.cmi +Integers.cmo: Zpower.cmi Zdiv.cmi Specif.cmi List.cmi Datatypes.cmi \ + Coqlib.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Integers.cmi +Integers.cmx: Zpower.cmx Zdiv.cmx Specif.cmx List.cmx Datatypes.cmx \ + Coqlib.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx Integers.cmi +InterfGraph.cmo: Specif.cmi Registers.cmi Ordered.cmi Locations.cmi List.cmi \ + FSetInterface.cmi FSetBridge.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi \ + BinPos.cmi BinInt.cmi InterfGraph.cmi +InterfGraph.cmx: Specif.cmx Registers.cmx Ordered.cmx Locations.cmx List.cmx \ + FSetInterface.cmx FSetBridge.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx \ + BinPos.cmx BinInt.cmx InterfGraph.cmi +Kildall.cmo: Wf.cmi Specif.cmi Maps.cmi List.cmi Lattice.cmi Datatypes.cmi \ + Coqlib.cmi BinPos.cmi Kildall.cmi +Kildall.cmx: Wf.cmx Specif.cmx Maps.cmx List.cmx Lattice.cmx Datatypes.cmx \ + Coqlib.cmx BinPos.cmx Kildall.cmi +Lattice.cmo: Specif.cmi Maps.cmi Datatypes.cmi BinPos.cmi Lattice.cmi +Lattice.cmx: Specif.cmx Maps.cmx Datatypes.cmx BinPos.cmx Lattice.cmi +Linearize.cmo: Specif.cmi Op.cmi Maps.cmi List.cmi Linear.cmi Lattice.cmi \ + LTL.cmi Kildall.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi \ + Linearize.cmi +Linearize.cmx: Specif.cmx Op.cmx Maps.cmx List.cmx Linear.cmx Lattice.cmx \ + LTL.cmx Kildall.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx AST.cmx \ + Linearize.cmi +Linear.cmo: Values.cmi Specif.cmi Op.cmi Locations.cmi List.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi \ + Linear.cmi +Linear.cmx: Values.cmx Specif.cmx Op.cmx Locations.cmx List.cmx Integers.cmx \ + Globalenvs.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx BinInt.cmx AST.cmx \ + Linear.cmi +Lineartyping.cmo: Zmin.cmi Locations.cmi List.cmi Linear.cmi Datatypes.cmi \ + Conventions.cmi BinPos.cmi BinInt.cmi AST.cmi Lineartyping.cmi +Lineartyping.cmx: Zmin.cmx Locations.cmx List.cmx Linear.cmx Datatypes.cmx \ + Conventions.cmx BinPos.cmx BinInt.cmx AST.cmx Lineartyping.cmi +List.cmo: Specif.cmi Datatypes.cmi List.cmi +List.cmx: Specif.cmx Datatypes.cmx List.cmi +Locations.cmo: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ + BinInt.cmi AST.cmi Locations.cmi +Locations.cmx: Values.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \ + BinInt.cmx AST.cmx Locations.cmi +Logic.cmo: Logic.cmi +Logic.cmx: Logic.cmi +LTL.cmo: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi List.cmi \ + Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi BinPos.cmi \ + BinInt.cmi AST.cmi LTL.cmi +LTL.cmx: Values.cmx Specif.cmx Op.cmx Maps.cmx Locations.cmx List.cmx \ + Integers.cmx Globalenvs.cmx Datatypes.cmx Conventions.cmx BinPos.cmx \ + BinInt.cmx AST.cmx LTL.cmi +Mach.cmo: Zmin.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi \ + Locations.cmi List.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi \ + Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi Mach.cmi +Mach.cmx: Zmin.cmx Zdiv.cmx Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx \ + Locations.cmx List.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx \ + Coqlib.cmx BinPos.cmx BinInt.cmx AST.cmx Mach.cmi +Main.cmo: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \ + Linearize.cmi Datatypes.cmi Csharpminor.cmi Constprop.cmi Cminorgen.cmi \ + Cminor.cmi CSE.cmi Allocation.cmi AST.cmi Main.cmi +Main.cmx: Tunneling.cmx Stacking.cmx RTLgen.cmx PPCgen.cmx PPC.cmx \ + Linearize.cmx Datatypes.cmx Csharpminor.cmx Constprop.cmx Cminorgen.cmx \ + Cminor.cmx CSE.cmx Allocation.cmx AST.cmx Main.cmi +Maps.cmo: Specif.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinNat.cmi \ + BinInt.cmi Maps.cmi +Maps.cmx: Specif.cmx List.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx BinNat.cmx \ + BinInt.cmx Maps.cmi +Mem.cmo: Values.cmi Specif.cmi List.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ + BinPos.cmi BinInt.cmi AST.cmi Mem.cmi +Mem.cmx: Values.cmx Specif.cmx List.cmx Integers.cmx Datatypes.cmx Coqlib.cmx \ + BinPos.cmx BinInt.cmx AST.cmx Mem.cmi +Op.cmo: Values.cmi Specif.cmi List.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ + Datatypes.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Op.cmi +Op.cmx: Values.cmx Specif.cmx List.cmx Integers.cmx Globalenvs.cmx Floats.cmx \ + Datatypes.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx Op.cmi +Ordered.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Coqlib.cmi \ + BinPos.cmi Ordered.cmi +Ordered.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Coqlib.cmx \ + BinPos.cmx Ordered.cmi +Parallelmove.cmo: Wf.cmi Values.cmi Specif.cmi Peano.cmi Locations.cmi \ + List.cmi LTL.cmi Datatypes.cmi AST.cmi Parallelmove.cmi +Parallelmove.cmx: Wf.cmx Values.cmx Specif.cmx Peano.cmx Locations.cmx \ + List.cmx LTL.cmx Datatypes.cmx AST.cmx Parallelmove.cmi +Peano.cmo: Datatypes.cmi Peano.cmi +Peano.cmx: Datatypes.cmx Peano.cmi +PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi List.cmi \ + Integers.cmi Datatypes.cmi Coqlib.cmi Bool.cmi BinPos.cmi BinInt.cmi \ + AST.cmi PPCgen.cmi +PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx List.cmx \ + Integers.cmx Datatypes.cmx Coqlib.cmx Bool.cmx BinPos.cmx BinInt.cmx \ + AST.cmx PPCgen.cmi +PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi List.cmi Integers.cmi \ + Globalenvs.cmi Floats.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi \ + AST.cmi PPC.cmi +PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx List.cmx Integers.cmx \ + Globalenvs.cmx Floats.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx BinInt.cmx \ + AST.cmx PPC.cmi +Registers.cmo: Specif.cmi Sets.cmi Maps.cmi List.cmi Datatypes.cmi Coqlib.cmi \ + BinPos.cmi AST.cmi Registers.cmi +Registers.cmx: Specif.cmx Sets.cmx Maps.cmx List.cmx Datatypes.cmx Coqlib.cmx \ + BinPos.cmx AST.cmx Registers.cmi +RTLgen.cmo: Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi Op.cmi \ + Maps.cmi List.cmi Datatypes.cmi Coqlib.cmi Cminor.cmi BinPos.cmi AST.cmi \ + RTLgen.cmi +RTLgen.cmx: Specif.cmx Registers.cmx ../caml/RTLgenaux.cmx RTL.cmx Op.cmx \ + Maps.cmx List.cmx Datatypes.cmx Coqlib.cmx Cminor.cmx BinPos.cmx AST.cmx \ + RTLgen.cmi +RTL.cmo: Values.cmi Registers.cmi Op.cmi Maps.cmi List.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi BinPos.cmi BinInt.cmi AST.cmi RTL.cmi +RTL.cmx: Values.cmx Registers.cmx Op.cmx Maps.cmx List.cmx Integers.cmx \ + Globalenvs.cmx Datatypes.cmx BinPos.cmx BinInt.cmx AST.cmx RTL.cmi +RTLtyping.cmo: union_find.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi \ + Maps.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi \ + RTLtyping.cmi +RTLtyping.cmx: union_find.cmx Specif.cmx Registers.cmx RTL.cmx Op.cmx \ + Maps.cmx List.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx AST.cmx \ + RTLtyping.cmi +Sets.cmo: Specif.cmi Maps.cmi List.cmi Datatypes.cmi Sets.cmi +Sets.cmx: Specif.cmx Maps.cmx List.cmx Datatypes.cmx Sets.cmi +Specif.cmo: Datatypes.cmi Specif.cmi +Specif.cmx: Datatypes.cmx Specif.cmi +Stacking.cmo: Specif.cmi Op.cmi Mach.cmi Locations.cmi List.cmi \ + Lineartyping.cmi Linear.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ + Conventions.cmi BinPos.cmi BinInt.cmi AST.cmi Stacking.cmi +Stacking.cmx: Specif.cmx Op.cmx Mach.cmx Locations.cmx List.cmx \ + Lineartyping.cmx Linear.cmx Integers.cmx Datatypes.cmx Coqlib.cmx \ + Conventions.cmx BinPos.cmx BinInt.cmx AST.cmx Stacking.cmi +Sumbool.cmo: Specif.cmi Datatypes.cmi Sumbool.cmi +Sumbool.cmx: Specif.cmx Datatypes.cmx Sumbool.cmi +Tunneling.cmo: Maps.cmi List.cmi LTL.cmi Datatypes.cmi AST.cmi Tunneling.cmi +Tunneling.cmx: Maps.cmx List.cmx LTL.cmx Datatypes.cmx AST.cmx Tunneling.cmi +union_find.cmo: Wf.cmi Specif.cmi Datatypes.cmi union_find.cmi +union_find.cmx: Wf.cmx Specif.cmx Datatypes.cmx union_find.cmi +Values.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ + BinPos.cmi BinInt.cmi AST.cmi Values.cmi +Values.cmx: Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx \ + BinPos.cmx BinInt.cmx AST.cmx Values.cmi +Wf.cmo: Wf.cmi +Wf.cmx: Wf.cmi +ZArith_dec.cmo: Sumbool.cmi Specif.cmi Datatypes.cmi BinInt.cmi \ + ZArith_dec.cmi +ZArith_dec.cmx: Sumbool.cmx Specif.cmx Datatypes.cmx BinInt.cmx \ + ZArith_dec.cmi +Zbool.cmo: Zeven.cmi ZArith_dec.cmi Sumbool.cmi Specif.cmi Datatypes.cmi \ + BinInt.cmi Zbool.cmi +Zbool.cmx: Zeven.cmx ZArith_dec.cmx Sumbool.cmx Specif.cmx Datatypes.cmx \ + BinInt.cmx Zbool.cmi +Zdiv.cmo: Zbool.cmi ZArith_dec.cmi Specif.cmi Datatypes.cmi BinPos.cmi \ + BinInt.cmi Zdiv.cmi +Zdiv.cmx: Zbool.cmx ZArith_dec.cmx Specif.cmx Datatypes.cmx BinPos.cmx \ + BinInt.cmx Zdiv.cmi +Zeven.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zeven.cmi +Zeven.cmx: Specif.cmx Datatypes.cmx BinPos.cmx BinInt.cmx Zeven.cmi +Zmin.cmo: Datatypes.cmi BinInt.cmi Zmin.cmi +Zmin.cmx: Datatypes.cmx BinInt.cmx Zmin.cmi +Zmisc.cmo: Datatypes.cmi BinPos.cmi BinInt.cmi Zmisc.cmi +Zmisc.cmx: Datatypes.cmx BinPos.cmx BinInt.cmx Zmisc.cmi +Zpower.cmo: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zpower.cmi +Zpower.cmx: Zmisc.cmx Datatypes.cmx BinPos.cmx BinInt.cmx Zpower.cmi diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch new file mode 100644 index 0000000..a091385 --- /dev/null +++ b/extraction/Kildall.ml.patch @@ -0,0 +1,22 @@ +*** Kildall.ml.orig 2006-02-09 11:47:52.000000000 +0100 +--- Kildall.ml 2006-02-09 13:42:35.103321691 +0100 +*************** +*** 191,199 **** + Maps.PMap.t option **) + + let fixpoint successors topnode transf entrypoints = +! DS.fixpoint (fun s -> +! Maps.PMap.get s (make_predecessors successors topnode)) topnode transf +! entrypoints + end + + module type ORDERED_TYPE_WITH_TOP = +--- 191,198 ---- + Maps.PMap.t option **) + + let fixpoint successors topnode transf entrypoints = +! let pred = make_predecessors successors topnode in +! DS.fixpoint (fun s -> Maps.PMap.get s pred) topnode transf entrypoints + end + + module type ORDERED_TYPE_WITH_TOP = diff --git a/extraction/Linearize.ml.patch b/extraction/Linearize.ml.patch new file mode 100644 index 0000000..47b6cc9 --- /dev/null +++ b/extraction/Linearize.ml.patch @@ -0,0 +1,22 @@ +*** 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 new file mode 100644 index 0000000..038b3d0 --- /dev/null +++ b/extraction/Makefile @@ -0,0 +1,91 @@ +FILES=\ + Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml \ + Bool.ml List.ml Sumbool.ml BinPos.ml BinNat.ml BinInt.ml \ + ZArith_dec.ml Zeven.ml Zmin.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \ + FSetInterface.ml FSetBridge.ml FSetList.ml FSetAVL.ml \ + Coqlib.ml Maps.ml Sets.ml union_find.ml AST.ml Integers.ml \ + ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Values.ml \ + Mem.ml Globalenvs.ml \ + Op.ml Cminor.ml Cmconstr.ml \ + Csharpminor.ml Cminorgen.ml \ + Registers.ml RTL.ml \ + ../caml/RTLgenaux.ml RTLgen.ml \ + RTLtyping.ml \ + Lattice.ml Kildall.ml \ + Constprop.ml CSE.ml \ + Locations.ml Conventions.ml LTL.ml \ + Ordered.ml InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \ + Parallelmove.ml Allocation.ml \ + Tunneling.ml Linear.ml Lineartyping.ml Linearize.ml \ + Mach.ml Stacking.ml \ + PPC.ml PPCgen.ml \ + Main.ml \ + ../caml/CMparser.ml ../caml/CMlexer.ml \ + ../caml/PrintPPC.ml ../caml/Main2.ml + +EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES)) +GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli) + +CAMLINCL=-I ../caml +OCAMLC=ocamlc -g $(CAMLINCL) +OCAMLOPT=ocamlopt $(CAMLINCL) +OCAMLDEP=ocamldep $(CAMLINCL) + +COQINCL=-I ../lib -I ../backend +COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source + +../ccomp: $(FILES:.ml=.cmo) + $(OCAMLC) -o ../ccomp $(FILES:.ml=.cmo) + +../ccomp.opt: Pack.cmx + $(OCAMLOPT) -o ../ccomp.opt Pack.cmx + +Pack.cmx: $(FILES:.ml=.cmx) + $(OCAMLOPT) -pack -o Pack.cmx $(FILES:.ml=.cmx) + +extraction: + @rm -f $(GENFILES) + $(COQEXEC) extraction.v + @echo "Fixing file names..." + @for i in $(GENFILES); do \ + j=`./uncapitalize $$i`; \ + test -f $$i || (test -f $$j && mv $$j $$i); \ + done + @echo "Patching files..." + @for i in *.patch; do patch < $$i; done + +../caml/CMparser.ml ../caml/CMparser.mli: ../caml/CMparser.mly + ocamlyacc -v ../caml/CMparser.mly + +beforedepend:: ../caml/CMparser.ml ../caml/CMparser.mli +clean:: + rm -f ../caml/CMparser.ml ../caml/CMparser.mli ../caml/CMparser.output + +../caml/CMlexer.ml: ../caml/CMlexer.mll + ocamllex ../caml/CMlexer.mll + +beforedepend:: ../caml/CMlexer.ml +clean:: + rm -f ../caml/CMlexer.ml + +.SUFFIXES: .ml .mli .cmo .cmi .cmx + +.mli.cmi: + $(OCAMLC) -c $*.mli +.ml.cmo: + $(OCAMLC) -c $*.ml +.ml.cmx: + $(OCAMLOPT) -c $*.ml + +clean:: + rm -f $(GENFILES) + rm -f *.cm? *.o + cd ../caml && rm -f *.cm? *.o + rm -f ccomp + +depend: beforedepend + $(OCAMLDEP) ../caml/*.mli ../caml/*.ml *.mli *.ml > .depend + +include .depend + + diff --git a/extraction/extraction.v b/extraction/extraction.v new file mode 100644 index 0000000..1717882 --- /dev/null +++ b/extraction/extraction.v @@ -0,0 +1,53 @@ +Require Floats. +Require Kildall. +Require RTLgen. +Require Coloring. +Require Allocation. +Require Cmconstr. +Require Main. + +(* Standard lib *) +Extract Inductive unit => "unit" [ "()" ]. +Extract Inductive bool => "bool" [ "true" "false" ]. +Extract Inductive sumbool => "bool" [ "true" "false" ]. + +(* Float *) +Extract Inlined Constant Floats.float => "float". +Extract Constant Floats.Float.zero => "0.". +Extract Constant Floats.Float.one => "1.". +Extract Constant Floats.Float.neg => "( ~-. )". +Extract Constant Floats.Float.abs => "abs_float". +Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat". +Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat". +Extract Constant Floats.Float.floatofint => "Floataux.floatofint". +Extract Constant Floats.Float.floatofintu => "Floataux.floatofintu". +Extract Constant Floats.Float.add => "( +. )". +Extract Constant Floats.Float.sub => "( -. )". +Extract Constant Floats.Float.mul => "( *. )". +Extract Constant Floats.Float.div => "( /. )". +Extract Constant Floats.Float.cmp => "Floataux.cmp". +Extract Constant Floats.Float.eq_dec => "fun (x: float) (y: float) -> x = y". + +(* RTLgen *) +Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". + +(* Coloring *) +Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". + +(* PPC *) +Extract Constant PPC.low_half_signed => "fun _ -> assert false". +Extract Constant PPC.high_half_signed => "fun _ -> assert false". +Extract Constant PPC.low_half_unsigned => "fun _ -> assert false". +Extract Constant PPC.high_half_unsigned => "fun _ -> assert false". + +(* Suppression of stupidly big equality functions *) +Extract Constant CSE.eq_rhs => "fun (x: rhs) (y: rhs) -> x = y". +Extract Constant Locations.mreg_eq => "fun (x: mreg) (y: mreg) -> x = y". +Extract Constant PPC.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". +Extract Constant PPC.freg_eq => "fun (x: freg) (y: freg) -> x = y". +Extract Constant PPC.preg_eq => "fun (x: preg) (y: preg) -> x = y". + +(* Go! *) +Recursive Extraction Library Main. +(*Extraction Library Compare_dec. + Extraction Library Cmconstr.*) diff --git a/extraction/uncapitalize b/extraction/uncapitalize new file mode 100755 index 0000000..d724b8f --- /dev/null +++ b/extraction/uncapitalize @@ -0,0 +1,6 @@ +#!/bin/sh +echo $1 | sed -e 'h +s/\(.\).*/\1/ +y/ABCDEFGHIJKLMNOPQRSTUVWXYZ/abcdefghijklmnopqrstuvwxyz/ +G +s/\n.//' -- cgit v1.2.3