From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/.depend | 194 +++++++++++++++++++++++++----------------------- extraction/Makefile | 13 ++-- extraction/extraction.v | 18 ++++- 3 files changed, 124 insertions(+), 101 deletions(-) (limited to 'extraction') diff --git a/extraction/.depend b/extraction/.depend index 9d6895d..20f0876 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -1,14 +1,9 @@ -../caml/Allocationaux.cmi: Locations.cmi Datatypes.cmi ../caml/CMlexer.cmi: ../caml/CMparser.cmi ../caml/CMparser.cmi: Cminor.cmi AST.cmi ../caml/CMtypecheck.cmi: Cminor.cmi ../caml/Coloringaux.cmi: Registers.cmi RTLtyping.cmi RTL.cmi Locations.cmi \ InterfGraph.cmi ../caml/PrintPPC.cmi: PPC.cmi -../caml/Allocationaux.cmo: Locations.cmi Datatypes.cmi ../caml/Camlcoq.cmo \ - CList.cmi AST.cmi ../caml/Allocationaux.cmi -../caml/Allocationaux.cmx: Locations.cmx Datatypes.cmx ../caml/Camlcoq.cmx \ - CList.cmx AST.cmx ../caml/Allocationaux.cmi ../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CList.cmi BinPos.cmi \ BinInt.cmi ../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CList.cmx BinPos.cmx \ @@ -17,24 +12,24 @@ ../caml/CMlexer.cmi ../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \ ../caml/CMlexer.cmi -../caml/CMparser.cmo: Op.cmi Integers.cmi Datatypes.cmi Cminor.cmi \ +../caml/CMparser.cmo: Op.cmi Integers.cmi Int.cmi Datatypes.cmi Cminor.cmi \ Cmconstr.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ ../caml/CMparser.cmi -../caml/CMparser.cmx: Op.cmx Integers.cmx Datatypes.cmx Cminor.cmx \ +../caml/CMparser.cmx: Op.cmx Integers.cmx Int.cmx Datatypes.cmx Cminor.cmx \ Cmconstr.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ ../caml/CMparser.cmi -../caml/CMtypecheck.cmo: Op.cmi Datatypes.cmi Cminor.cmi ../caml/Camlcoq.cmo \ - CList.cmi AST.cmi ../caml/CMtypecheck.cmi -../caml/CMtypecheck.cmx: Op.cmx Datatypes.cmx Cminor.cmx ../caml/Camlcoq.cmx \ - CList.cmx AST.cmx ../caml/CMtypecheck.cmi +../caml/CMtypecheck.cmo: Op.cmi Integers.cmi Datatypes.cmi Cminor.cmi \ + ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/CMtypecheck.cmi +../caml/CMtypecheck.cmx: Op.cmx Integers.cmx Datatypes.cmx Cminor.cmx \ + ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/CMtypecheck.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/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo +../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx ../caml/Main2.cmo: ../caml/PrintPPC.cmi Main.cmi Datatypes.cmi \ ../caml/CMtypecheck.cmi ../caml/CMparser.cmi ../caml/CMlexer.cmi ../caml/Main2.cmx: ../caml/PrintPPC.cmx Main.cmx Datatypes.cmx \ @@ -45,18 +40,23 @@ AST.cmx ../caml/PrintPPC.cmi ../caml/RTLgenaux.cmo: Cminor.cmi ../caml/RTLgenaux.cmx: Cminor.cmx +../caml/RTLtypingaux.cmo: Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \ + ../caml/Camlcoq.cmo CList.cmi AST.cmi +../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \ + ../caml/Camlcoq.cmx CList.cmx AST.cmx Allocation.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \ Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi LTL.cmi Datatypes.cmi \ Conventions.cmi Coloring.cmi CList.cmi BinPos.cmi AST.cmi -AST.cmi: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi +AST.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ + CList.cmi BinPos.cmi BinInt.cmi BinInt.cmi: Datatypes.cmi BinPos.cmi BinNat.cmi -BinNat.cmi: Datatypes.cmi BinPos.cmi +BinNat.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinPos.cmi: Peano.cmi Datatypes.cmi Bool.cmi: Specif.cmi Datatypes.cmi CList.cmi: Specif.cmi Datatypes.cmi Cmconstr.cmi: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi -Cminorgen.cmi: Zmin.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \ +Cminorgen.cmi: Zmax.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \ Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi Cmconstr.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Cminor.cmi: Values.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ @@ -67,43 +67,45 @@ Coloring.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \ Compare_dec.cmi: Specif.cmi Datatypes.cmi Constprop.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ Floats.cmi Datatypes.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi -Conventions.cmi: Locations.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ - AST.cmi +Conventions.cmi: Locations.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ + BinInt.cmi AST.cmi Coqlib.cmi: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \ BinPos.cmi BinInt.cmi CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi -Csharpminor.cmi: Zmin.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ +Csharpminor.cmi: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ Globalenvs.cmi Floats.cmi Datatypes.cmi CList.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 FSetInterface.cmi \ +Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi +FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi \ Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi FSetBridge.cmi: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi FSetInterface.cmi: Specif.cmi Datatypes.cmi CList.cmi -FSetList.cmi: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi +FSetList.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi Globalenvs.cmi: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Integers.cmi: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi -InterfGraph.cmi: Specif.cmi Registers.cmi Locations.cmi FSetInterface.cmi \ - Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi -Kildall.cmi: Wf.cmi Specif.cmi Maps.cmi Lattice.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi + CList.cmi Bool.cmi BinPos.cmi BinInt.cmi +InterfGraph.cmi: Specif.cmi Registers.cmi OrderedType.cmi Locations.cmi \ + Int.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi +Int.cmi: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi +Iteration.cmi: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi +Kildall.cmi: Specif.cmi Maps.cmi Lattice.cmi Iteration.cmi Datatypes.cmi \ + Coqlib.cmi CList.cmi BinPos.cmi Lattice.cmi: Specif.cmi Maps.cmi Datatypes.cmi BinPos.cmi Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Linear.cmi Lattice.cmi LTL.cmi \ Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi Linear.cmi: Values.cmi Specif.cmi Op.cmi Locations.cmi Integers.cmi \ Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi -Lineartyping.cmi: Zmin.cmi Locations.cmi Linear.cmi Datatypes.cmi \ +Lineartyping.cmi: Zmax.cmi Locations.cmi Linear.cmi Datatypes.cmi \ Conventions.cmi CList.cmi BinPos.cmi BinInt.cmi AST.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 Integers.cmi \ Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi BinPos.cmi \ BinInt.cmi AST.cmi -Mach.cmi: Zmin.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi \ +Mach.cmi: Zmax.cmi Zdiv.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 Main.cmi: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \ @@ -111,14 +113,15 @@ Main.cmi: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \ Cminor.cmi CSE.cmi Allocation.cmi AST.cmi Maps.cmi: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \ BinInt.cmi -Mem.cmi: Values.cmi Specif.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ +Mem.cmi: Zmax.cmi Values.cmi Specif.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Op.cmi: Values.cmi Specif.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ Datatypes.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi -Ordered.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Coqlib.cmi \ +Ordered.cmi: Specif.cmi OrderedType.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi -Parallelmove.cmi: Wf.cmi Values.cmi Specif.cmi Peano.cmi Locations.cmi \ - LTL.cmi Datatypes.cmi CList.cmi AST.cmi +OrderedType.cmi: Specif.cmi Datatypes.cmi +Parallelmove.cmi: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi +Parmov.cmi: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi Peano.cmi: Datatypes.cmi PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \ Datatypes.cmi Coqlib.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi @@ -130,8 +133,8 @@ RTLgen.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ Datatypes.cmi Coqlib.cmi Cminor.cmi CList.cmi BinPos.cmi AST.cmi RTL.cmi: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi -RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \ - Coqlib.cmi CList.cmi BinPos.cmi AST.cmi +RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Locations.cmi \ + Datatypes.cmi Coqlib.cmi Conventions.cmi CList.cmi AST.cmi Sets.cmi: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi Specif.cmi: Datatypes.cmi Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Lineartyping.cmi \ @@ -148,6 +151,7 @@ Zbool.cmi: Zeven.cmi ZArith_dec.cmi Sumbool.cmi Specif.cmi Datatypes.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 +Zmax.cmi: Datatypes.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 @@ -159,14 +163,14 @@ Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx \ Parallelmove.cmx Op.cmx Maps.cmx Locations.cmx LTL.cmx Kildall.cmx \ Datatypes.cmx Conventions.cmx Coloring.cmx CList.cmx BinPos.cmx AST.cmx \ Allocation.cmi -AST.cmo: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ - AST.cmi -AST.cmx: Specif.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \ - AST.cmi +AST.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ + CList.cmi BinPos.cmi BinInt.cmi AST.cmi +AST.cmx: Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx \ + CList.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 +BinNat.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinNat.cmi +BinNat.cmx: Specif.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 @@ -177,10 +181,10 @@ Cmconstr.cmo: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Cmconstr.cmi Cmconstr.cmx: Specif.cmx Op.cmx Integers.cmx Datatypes.cmx Compare_dec.cmx \ Cminor.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Cmconstr.cmi -Cminorgen.cmo: Zmin.cmi Specif.cmi Sets.cmi Op.cmi Mem.cmi Maps.cmi \ +Cminorgen.cmo: Zmax.cmi Specif.cmi Sets.cmi Op.cmi Mem.cmi Maps.cmi \ Integers.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi \ Cmconstr.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Cminorgen.cmi -Cminorgen.cmx: Zmin.cmx Specif.cmx Sets.cmx Op.cmx Mem.cmx Maps.cmx \ +Cminorgen.cmx: Zmax.cmx Specif.cmx Sets.cmx Op.cmx Mem.cmx Maps.cmx \ Integers.cmx Datatypes.cmx Csharpminor.cmx Coqlib.cmx Cminor.cmx \ Cmconstr.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Cminorgen.cmi Cminor.cmo: Values.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ @@ -201,10 +205,10 @@ Constprop.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Lattice.cmi \ Constprop.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Lattice.cmx \ Kildall.cmx Integers.cmx Floats.cmx Datatypes.cmx CList.cmx Bool.cmx \ BinPos.cmx BinInt.cmx AST.cmx Constprop.cmi -Conventions.cmo: Locations.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ - AST.cmi Conventions.cmi -Conventions.cmx: Locations.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx \ - AST.cmx Conventions.cmi +Conventions.cmo: Locations.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ + BinInt.cmi AST.cmi Conventions.cmi +Conventions.cmx: Locations.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \ + BinInt.cmx AST.cmx Conventions.cmi Coqlib.cmo: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \ BinPos.cmi BinInt.cmi Coqlib.cmi Coqlib.cmx: Zdiv.cmx ZArith_dec.cmx Wf.cmx Specif.cmx Datatypes.cmx CList.cmx \ @@ -215,52 +219,54 @@ CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \ CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Kildall.cmx \ Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \ AST.cmx CSE.cmi -Csharpminor.cmo: Zmin.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ +Csharpminor.cmo: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi Csharpminor.cmi -Csharpminor.cmx: Zmin.cmx Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx \ +Csharpminor.cmx: Zmax.cmx Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx \ Globalenvs.cmx Floats.cmx Datatypes.cmx CList.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.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 FSetList.cmi \ - FSetInterface.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ - FSetAVL.cmi -FSetAVL.cmx: ZArith_dec.cmx Wf.cmx Specif.cmx Peano.cmx FSetList.cmx \ - FSetInterface.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx \ - FSetAVL.cmi + Floats.cmi +FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi FSetList.cmi \ + Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi +FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx Int.cmx FSetList.cmx \ + Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx FSetAVL.cmi FSetBridge.cmo: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi \ FSetBridge.cmi FSetBridge.cmx: Specif.cmx FSetInterface.cmx Datatypes.cmx CList.cmx \ FSetBridge.cmi FSetInterface.cmo: Specif.cmi Datatypes.cmi CList.cmi FSetInterface.cmi FSetInterface.cmx: Specif.cmx Datatypes.cmx CList.cmx FSetInterface.cmi -FSetList.cmo: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi \ - FSetList.cmi -FSetList.cmx: Specif.cmx FSetInterface.cmx Datatypes.cmx CList.cmx \ - FSetList.cmi +FSetList.cmo: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi FSetList.cmi +FSetList.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx FSetList.cmi Globalenvs.cmo: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Globalenvs.cmi Globalenvs.cmx: Values.cmx Mem.cmx Maps.cmx Integers.cmx Datatypes.cmx \ CList.cmx BinPos.cmx BinInt.cmx AST.cmx Globalenvs.cmi Integers.cmo: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Integers.cmi + CList.cmi Bool.cmi BinPos.cmi BinInt.cmi Integers.cmi Integers.cmx: Zpower.cmx Zdiv.cmx Specif.cmx Datatypes.cmx Coqlib.cmx \ - CList.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx Integers.cmi -InterfGraph.cmo: Specif.cmi Registers.cmi Ordered.cmi Locations.cmi \ - FSetInterface.cmi FSetBridge.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi BinInt.cmi InterfGraph.cmi -InterfGraph.cmx: Specif.cmx Registers.cmx Ordered.cmx Locations.cmx \ - FSetInterface.cmx FSetBridge.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx \ - CList.cmx BinPos.cmx BinInt.cmx InterfGraph.cmi -Kildall.cmo: Wf.cmi Specif.cmi Maps.cmi Lattice.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi Kildall.cmi -Kildall.cmx: Wf.cmx Specif.cmx Maps.cmx Lattice.cmx Datatypes.cmx Coqlib.cmx \ - CList.cmx BinPos.cmx Kildall.cmi + CList.cmx Bool.cmx BinPos.cmx BinInt.cmx Integers.cmi +InterfGraph.cmo: Specif.cmi Registers.cmi OrderedType.cmi Ordered.cmi \ + Locations.cmi Int.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi CList.cmi \ + BinPos.cmi BinInt.cmi InterfGraph.cmi +InterfGraph.cmx: Specif.cmx Registers.cmx OrderedType.cmx Ordered.cmx \ + Locations.cmx Int.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx CList.cmx \ + BinPos.cmx BinInt.cmx InterfGraph.cmi +Int.cmo: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi Int.cmi +Int.cmx: Zmax.cmx ZArith_dec.cmx Specif.cmx BinPos.cmx BinInt.cmx Int.cmi +Iteration.cmo: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ + Iteration.cmi +Iteration.cmx: Wf.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \ + Iteration.cmi +Kildall.cmo: Specif.cmi Maps.cmi Lattice.cmi Iteration.cmi Datatypes.cmi \ + Coqlib.cmi CList.cmi BinPos.cmi Kildall.cmi +Kildall.cmx: Specif.cmx Maps.cmx Lattice.cmx Iteration.cmx Datatypes.cmx \ + Coqlib.cmx CList.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 Linear.cmi Lattice.cmi LTL.cmi \ @@ -275,9 +281,9 @@ Linear.cmo: Values.cmi Specif.cmi Op.cmi Locations.cmi Integers.cmi \ Linear.cmx: Values.cmx Specif.cmx Op.cmx Locations.cmx Integers.cmx \ Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \ AST.cmx Linear.cmi -Lineartyping.cmo: Zmin.cmi Locations.cmi Linear.cmi Datatypes.cmi \ +Lineartyping.cmo: Zmax.cmi Locations.cmi Linear.cmi Datatypes.cmi \ Conventions.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Lineartyping.cmi -Lineartyping.cmx: Zmin.cmx Locations.cmx Linear.cmx Datatypes.cmx \ +Lineartyping.cmx: Zmax.cmx Locations.cmx Linear.cmx Datatypes.cmx \ Conventions.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Lineartyping.cmi Locations.cmo: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ BinInt.cmi AST.cmi Locations.cmi @@ -291,10 +297,10 @@ LTL.cmo: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi Integers.cmi \ LTL.cmx: Values.cmx Specif.cmx Op.cmx Maps.cmx Locations.cmx Integers.cmx \ Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.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 \ +Mach.cmo: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi \ Locations.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi \ CList.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 \ +Mach.cmx: Zmax.cmx Zdiv.cmx Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx \ Locations.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx Coqlib.cmx \ CList.cmx BinPos.cmx BinInt.cmx AST.cmx Mach.cmi Main.cmo: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \ @@ -307,22 +313,26 @@ Maps.cmo: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \ BinInt.cmi Maps.cmi Maps.cmx: Specif.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinNat.cmx \ BinInt.cmx Maps.cmi -Mem.cmo: Values.cmi Specif.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ +Mem.cmo: Zmax.cmi Values.cmi Specif.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Mem.cmi -Mem.cmx: Values.cmx Specif.cmx Integers.cmx Datatypes.cmx Coqlib.cmx \ +Mem.cmx: Zmax.cmx Values.cmx Specif.cmx Integers.cmx Datatypes.cmx Coqlib.cmx \ CList.cmx BinPos.cmx BinInt.cmx AST.cmx Mem.cmi Op.cmo: Values.cmi Specif.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ Datatypes.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Op.cmi Op.cmx: Values.cmx Specif.cmx Integers.cmx Globalenvs.cmx Floats.cmx \ Datatypes.cmx CList.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx Op.cmi -Ordered.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Coqlib.cmi \ +Ordered.cmo: Specif.cmi OrderedType.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi Ordered.cmi -Ordered.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Coqlib.cmx \ +Ordered.cmx: Specif.cmx OrderedType.cmx Maps.cmx Datatypes.cmx Coqlib.cmx \ BinPos.cmx Ordered.cmi -Parallelmove.cmo: Wf.cmi Values.cmi Specif.cmi Peano.cmi Locations.cmi \ - LTL.cmi Datatypes.cmi CList.cmi AST.cmi Parallelmove.cmi -Parallelmove.cmx: Wf.cmx Values.cmx Specif.cmx Peano.cmx Locations.cmx \ - LTL.cmx Datatypes.cmx CList.cmx AST.cmx Parallelmove.cmi +OrderedType.cmo: Specif.cmi Datatypes.cmi OrderedType.cmi +OrderedType.cmx: Specif.cmx Datatypes.cmx OrderedType.cmi +Parallelmove.cmo: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi \ + Parallelmove.cmi +Parallelmove.cmx: Parmov.cmx Locations.cmx Datatypes.cmx CList.cmx AST.cmx \ + Parallelmove.cmi +Parmov.cmo: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi Parmov.cmi +Parmov.cmx: Specif.cmx Peano.cmx Datatypes.cmx CList.cmx Parmov.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 Integers.cmi \ @@ -351,12 +361,12 @@ RTL.cmo: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi RTL.cmi RTL.cmx: Values.cmx Registers.cmx Op.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx RTL.cmi -RTLtyping.cmo: union_find.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi \ - Maps.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi \ - RTLtyping.cmi -RTLtyping.cmx: union_find.cmx Specif.cmx Registers.cmx RTL.cmx Op.cmx \ - Maps.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx AST.cmx \ - RTLtyping.cmi +RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \ + Op.cmi Maps.cmi Locations.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ + CList.cmi AST.cmi RTLtyping.cmi +RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \ + Op.cmx Maps.cmx Locations.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \ + CList.cmx AST.cmx RTLtyping.cmi Sets.cmo: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi Sets.cmi Sets.cmx: Specif.cmx Maps.cmx Datatypes.cmx CList.cmx Sets.cmi Specif.cmo: Datatypes.cmi Specif.cmi @@ -393,6 +403,8 @@ 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 +Zmax.cmo: Datatypes.cmi BinInt.cmi Zmax.cmi +Zmax.cmx: Datatypes.cmx BinInt.cmx Zmax.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 diff --git a/extraction/Makefile b/extraction/Makefile index 687c5c5..6ae8e35 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -1,19 +1,20 @@ FILES=\ Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml \ Bool.ml CList.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 \ + ZArith_dec.ml Zeven.ml Zmax.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \ + Int.ml OrderedType.ml FSetList.ml FSetAVL.ml \ + Coqlib.ml Maps.ml Sets.ml AST.ml Iteration.ml Integers.ml \ + ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.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 \ + Locations.ml Conventions.ml \ + ../caml/RTLtypingaux.ml RTLtyping.ml \ Lattice.ml Kildall.ml \ Constprop.ml CSE.ml \ - Locations.ml Conventions.ml LTL.ml \ + LTL.ml \ Ordered.ml InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \ Parallelmove.ml Allocation.ml \ Tunneling.ml Linear.ml Lineartyping.ml Linearize.ml \ diff --git a/extraction/extraction.v b/extraction/extraction.v index 1717882..47c6f36 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -1,9 +1,8 @@ +Require Iteration. Require Floats. -Require Kildall. Require RTLgen. Require Coloring. Require Allocation. -Require Cmconstr. Require Main. (* Standard lib *) @@ -28,9 +27,22 @@ 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". +(* Iteration *) +Extract Constant Iteration.dependent_description' => + "fun x -> assert false". + +Extract Constant Iteration.GenIter.iterate => + "let rec iter f a = + match f a with Coq_inl b -> Some b | Coq_inr a' -> iter f a' + in iter". + + (* RTLgen *) Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". +(* RTLtyping *) +Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_environment". + (* Coloring *) Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". @@ -49,5 +61,3 @@ Extract Constant PPC.preg_eq => "fun (x: preg) (y: preg) -> x = y". (* Go! *) Recursive Extraction Library Main. -(*Extraction Library Compare_dec. - Extraction Library Cmconstr.*) -- cgit v1.2.3