From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 4861ff9..1156d04 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -10,9 +10,12 @@ (* *) (* *********************************************************************) +Require Wfsimpl. Require Iteration. Require Floats. Require RTLgen. +Require Inlining. +Require Constprop. Require Coloring. Require Allocation. Require Compiler. @@ -22,6 +25,9 @@ Require Initializers. Require Import ExtrOcamlBasic. Require Import ExtrOcamlString. +(* Wfsimpl *) +Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. + (* Float *) Extract Inlined Constant Floats.float => "float". Extract Constant Floats.Float.zero => "0.". @@ -53,8 +59,6 @@ Extraction NoInline Memory.Mem.valid_pointer. Extraction Inline Errors.bind Errors.bind2. (* Iteration *) -Extract Constant Iteration.dependent_description' => - "fun x -> assert false". Extract Constant Iteration.GenIter.iterate => "let rec iter f a = @@ -66,9 +70,19 @@ Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch". Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2. +(* Inlining *) +Extract Inlined Constant Inlining.should_inline => "Inliningaux.should_inline". +Extraction Inline Inlining.ret Inlining.bind. + (* RTLtyping *) Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_environment". +(* Constprop *) +Extract Constant ConstpropOp.propagate_float_constants => + "fun _ -> !Clflags.option_ffloatconstprop >= 1". +Extract Constant Constprop.generate_float_constants => + "fun _ -> !Clflags.option_ffloatconstprop >= 2". + (* Coloring *) Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". @@ -83,6 +97,7 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_rtl". Extract Constant Compiler.print_RTL_tailcall => "PrintRTL.print_tailcall". +Extract Constant Compiler.print_RTL_inline => "PrintRTL.print_inlining". Extract Constant Compiler.print_RTL_constprop => "PrintRTL.print_constprop". Extract Constant Compiler.print_RTL_cse => "PrintRTL.print_cse". Extract Constant Compiler.print_LTLin => "PrintLTLin.print_if". -- cgit v1.2.3