From adff86c007196e4389668c7935b7891c5b4217c7 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 17 Dec 2020 11:25:03 +0100 Subject: fix extraction of non-aarch64 targets --- extraction/extraction.v | 252 ------------------------------------------ extraction/extraction.vexpand | 250 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 250 insertions(+), 252 deletions(-) delete mode 100644 extraction/extraction.v create mode 100644 extraction/extraction.vexpand (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v deleted file mode 100644 index ffcebaaa..00000000 --- a/extraction/extraction.v +++ /dev/null @@ -1,252 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 - Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64 - Asmgen.Asmgen_expand.storeptr. 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 -- cgit