From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 36 +++++++++++++++++++++++++++++++----- 1 file changed, 31 insertions(+), 5 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 1397416..804ccef 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -11,13 +11,14 @@ (* *********************************************************************) Require Wfsimpl. +Require AST. Require Iteration. Require Floats. +Require SelectLong. Require RTLgen. Require Inlining. Require ConstpropOp. Require Constprop. -Require Coloring. Require Allocation. Require Compiler. @@ -28,6 +29,10 @@ Require Import ExtrOcamlString. (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. +(* AST *) +Extract Constant AST.ident_of_string => + "fun s -> Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s)". + (* Memdata *) Extract Constant Memdata.big_endian => "Memdataaux.big_endian". @@ -44,6 +49,15 @@ Extract Constant Iteration.GenIter.iterate => match f a with Coq_inl b -> Some b | Coq_inr a' -> iter f a' in iter". +(* Selection *) + +Extract Constant SelectLong.get_helper => + "fun ge s sg -> + Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". +Extract Constant SelectLong.get_builtin => + "fun s sg -> + Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". + (* RTLgen *) Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch". Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". @@ -59,8 +73,15 @@ Extract Constant ConstpropOp.propagate_float_constants => Extract Constant Constprop.generate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 2". -(* Coloring *) -Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". +(* Allocation *) +Extract Constant Allocation.eq_operation => "(=)". +Extract Constant Allocation.eq_addressing => "(=)". +Extract Constant Allocation.eq_opt_addressing => "(=)". +Extract Constant Allocation.eq_condition => "(=)". +Extract Constant Allocation.eq_chunk => "(=)". +Extract Constant Allocation.eq_external_function => "(=)". +Extract Constant Allocation.eq_signature => "(=)". +Extract Constant Allocation.regalloc => "Regalloc.regalloc". (* Linearize *) Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". @@ -77,7 +98,7 @@ 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". +Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) @@ -106,5 +127,10 @@ Separate Extraction Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Initializers.transl_init Initializers.constval - Csyntax.Eindex Csyntax.Epreincr. + Csyntax.Eindex Csyntax.Epreincr + Conventions1.dummy_int_reg Conventions1.dummy_float_reg + RTL.instr_defs RTL.instr_uses + Machregs.mregs_for_operation Machregs.mregs_for_builtin + Machregs.two_address_op. + -- cgit v1.2.3