diff options
Diffstat (limited to 'extraction/extraction.vexpand')
| -rw-r--r-- | extraction/extraction.vexpand | 250 |
1 files changed, 250 insertions, 0 deletions
diff --git a/extraction/extraction.vexpand b/extraction/extraction.vexpand new file mode 100644 index 00000000..568b1b46 --- /dev/null +++ b/extraction/extraction.vexpand @@ -0,0 +1,250 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import ZArith PeanoNat. +Require Coqlib. +Require Wfsimpl. +Require DecidableClass Decidableplus. +Require AST. +Require Iteration. +Require Floats. +Require SelectLong. +Require Selection. +Require RTLgen. +Require Inlining. +Require ValueDomain. +Require Tailcall. +Require Allocation. +Require Bounds. +Require Ctypes. +Require Csyntax. +Require Ctyping. +Require Clight. +Require Compiler. +Require Parser. +Require Initializers. +Require Asmaux. + +Require CSE3. +Require CSE3analysis. + +(* Standard lib *) +Require Import ExtrOcamlBasic. +Require Import ExtrOcamlString. + +(* Coqlib *) +Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". + +(* Datatypes *) +Extract Inlined Constant Datatypes.fst => "fst". +Extract Inlined Constant Datatypes.snd => "snd". + +(* Decidable *) + +Extraction Inline DecidableClass.Decidable_witness DecidableClass.decide + Decidableplus.Decidable_and Decidableplus.Decidable_or + Decidableplus.Decidable_not Decidableplus.Decidable_implies. + +(* Wfsimpl *) +Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. + +(* Memory - work around an extraction bug. *) +Extraction NoInline Memory.Mem.valid_pointer. + +(* Errors *) +Extraction Inline Errors.bind Errors.bind2. + +(* Iteration *) + +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". + +(* Selection *) + +Extract Constant Selection.compile_switch => "Switchaux.compile_switch". +Extract Constant Selection.if_conversion_heuristic => "Selectionaux.if_conversion_heuristic". + +(* RTLgen *) +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". +Extract Inlined Constant Inlining.inlining_info => "Inliningaux.inlining_info". +Extract Inlined Constant Inlining.inlining_analysis => "Inliningaux.inlining_analysis". +Extraction Inline Inlining.ret Inlining.bind. + +(* Loop invariant code motion *) +Extract Inlined Constant LICM.gen_injections => "LICMaux.gen_injections". + +(* Allocation *) +Extract Constant Allocation.regalloc => "Regalloc.regalloc". + +(* Linearize *) +Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". + +(* SimplExpr *) +Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident". +Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. + +(* Compopts *) +Extract Constant Compopts.optim_for_size => + "fun _ -> !Clflags.option_Osize". +Extract Constant Compopts.va_strict => + "fun _ -> false". +Extract Constant Compopts.propagate_float_constants => + "fun _ -> !Clflags.option_ffloatconstprop >= 1". +Extract Constant Compopts.generate_float_constants => + "fun _ -> !Clflags.option_ffloatconstprop >= 2". +Extract Constant Compopts.optim_tailcalls => + "fun _ -> !Clflags.option_ftailcalls". +Extract Constant Compopts.optim_constprop => + "fun _ -> !Clflags.option_fconstprop". +Extract Constant Compopts.optim_CSE => + "fun _ -> !Clflags.option_fcse". +Extract Constant Compopts.optim_CSE2 => + "fun _ -> !Clflags.option_fcse2". +Extract Constant Compopts.optim_CSE3 => + "fun _ -> !Clflags.option_fcse3". +Extract Constant Compopts.optim_CSE3_alias_analysis => + "fun _ -> !Clflags.option_fcse3_alias_analysis". +Extract Constant Compopts.optim_CSE3_across_calls => + "fun _ -> !Clflags.option_fcse3_across_calls". +Extract Constant Compopts.optim_CSE3_across_merges => + "fun _ -> !Clflags.option_fcse3_across_merges". +Extract Constant Compopts.optim_CSE3_glb => + "fun _ -> !Clflags.option_fcse3_glb". +Extract Constant Compopts.optim_CSE3_trivial_ops => + "fun _ -> !Clflags.option_fcse3_trivial_ops". +Extract Constant Compopts.optim_move_loop_invariants => + "fun _ -> !Clflags.option_fmove_loop_invariants". + +Extract Constant Compopts.optim_redundancy => + "fun _ -> !Clflags.option_fredundancy". +Extract Constant Compopts.optim_postpass => + "fun _ -> !Clflags.option_fpostpass". +Extract Constant Compopts.thumb => + "fun _ -> !Clflags.option_mthumb". +Extract Constant Compopts.debug => + "fun _ -> !Clflags.option_g". +Extract Constant Compopts.optim_globaladdrtmp => + "fun _ -> !Clflags.option_fglobaladdrtmp". +Extract Constant Compopts.optim_globaladdroffset => + "fun _ -> !Clflags.option_fglobaladdroffset". +Extract Constant Compopts.optim_xsaddr => + "fun _ -> !Clflags.option_fxsaddr". +Extract Constant Compopts.optim_addx => + "fun _ -> !Clflags.option_faddx". +Extract Constant Compopts.optim_madd => + "fun _ -> !Clflags.option_fmadd". +Extract Constant Compopts.optim_coalesce_mem => + "fun _ -> !Clflags.option_fcoalesce_mem". +Extract Constant Compopts.optim_forward_moves => + "fun _ -> !Clflags.option_fforward_moves". +Extract Constant Compopts.va_strict => + "fun _ -> false". +Extract Constant Compopts.all_loads_nontrap => + "fun _ -> !Clflags.option_all_loads_nontrap". +Extract Constant Compopts.profile_arcs => +"fun _ -> !Clflags.option_profile_arcs". +Extract Constant Compopts.branch_probabilities => + "fun _ -> !Clflags.option_fbranch_probabilities". + +(* Compiler *) +Extract Constant Compiler.print_Clight => "PrintClight.print_if". +Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". +Extract Constant Compiler.print_RTL => "PrintRTL.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". +Extract Constant Compiler.time => "Timing.time_coq". +Extract Constant Compopts.time => "Timing.time_coq". +(*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) + +(* Profiling *) +Extract Constant AST.profiling_id => "Digest.t". +Extract Constant AST.profiling_id_eq => "Digest.equal". +Extract Constant Profiling.function_id => "Profilingaux.function_id". +Extract Constant Profiling.branch_id => "Profilingaux.branch_id". +Extract Constant ProfilingExploit.function_id => "Profilingaux.function_id". +Extract Constant ProfilingExploit.branch_id => "Profilingaux.branch_id". +Extract Constant ProfilingExploit.condition_oracle => "Profilingaux.condition_oracle". + +(* Cabs *) +Extract Constant Cabs.loc => +"{ lineno : int; + filename: string; + byteno: int; + ident : int; + }". +Extract Inlined Constant Cabs.string => "String.t". +Extract Constant Cabs.char_code => "int64". + +Extract Inlined Constant CSE3.preanalysis => "CSE3analysisaux.preanalysis". + +Extract Inductive HashedSet.PSet_internals.pset => "HashedSetaux.pset" [ "HashedSetaux.empty" "HashedSetaux.node" ] "HashedSetaux.pset_match". + +Extract Inlined Constant HashedSet.PSet_internals.pset_eq => "(==)" (* "HashedSetaux.eq" *). + +(* Processor-specific extraction directives *) + +Load extractionMachdep. + +(* Avoid name clashes *) +Extraction Blacklist List String Int. + +(* Cutting the dependency to R. *) +Extract Inlined Constant Defs.F2R => "fun _ -> assert false". +Extract Inlined Constant Binary.FF2R => "fun _ -> assert false". +Extract Inlined Constant Binary.B2R => "fun _ -> assert false". +Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". +Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". + +(* Needed in Coq 8.4 to avoid problems with Function definitions. *) +Set Extraction AccessOpaque. + +(* Go! *) + +Cd "extraction". + +Separate Extraction + Z.ldiff Z.lnot Nat.leb + CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem + Compiler.transf_c_program Compiler.transf_cminor_program + Cexec.do_initial_state Cexec.do_step Cexec.at_final_state + Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env + Initializers.transl_init Initializers.constval + Csyntax.Eindex Csyntax.Epreincr Csyntax.Eselection + Ctyping.typecheck_program + Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr + Ctyping.eselection + Ctypes.make_program + Clight.type_of_function + Conventions1.callee_save_type Conventions1.is_float_reg + Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs + Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs + 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 Machregs.is_stack_reg + Machregs.destroyed_at_indirect_call + AST.signature_main Asmaux + Floats.Float32.from_parsed Floats.Float.from_parsed + Globalenvs.Senv.invert_symbol + Parser.translation_unit_file + Compopts.optim_postpass + Archi.has_notrap_loads |