diff --git a/.vscode/settings.json b/.vscode/settings.json index 1eaf5245f..706b220ac 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -2,5 +2,18 @@ "lldb.displayFormat": "auto", "lldb.showDisassembly": "auto", "lldb.dereferencePointers": false, - "lldb.consoleMode": "commands" + "lldb.consoleMode": "commands", + "files.exclude": { + "**/*.vo": true, + "**/*.vok": true, + "**/*.vos": true, + "**/*.aux": true, + "**/*.glob": true, + "**/.git": true, + "**/.svn": true, + "**/.hg": true, + "**/CVS": true, + "**/.DS_Store": true, + "**/Thumbs.db": true + } } \ No newline at end of file diff --git a/Makefile b/Makefile index b7005fcc8..d887706b4 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -.PHONY: all submodules plugin cplugin install clean bootstrap +.PHONY: all submodules runtime plugin cplugin install clean bootstrap all theories/Extraction/extraction.vo: theories/Makefile libraries/Makefile @@ -11,14 +11,13 @@ theories/Makefile: theories/_CoqProject libraries/Makefile: libraries/_CoqProject cd libraries;coq_makefile -f _CoqProject -o Makefile - submodules: git submodule update ./make_submodules.sh plugins: plugin cplugin -plugin: all plugin/CertiCoq.vo +plugin: all runtime plugin/CertiCoq.vo plugin/Makefile: plugin/_CoqProject cd plugin ; coq_makefile -f _CoqProject -o Makefile @@ -27,7 +26,7 @@ plugin/CertiCoq.vo: all plugin/Makefile theories/Extraction/extraction.vo bash ./make_plugin.sh plugin -cplugin: all cplugin/CertiCoq.vo +cplugin: all runtime cplugin/CertiCoq.vo cplugin/Makefile: cplugin/_CoqProject cd cplugin ; coq_makefile -f _CoqProject -o Makefile @@ -41,6 +40,7 @@ bootstrap: plugin cplugin install: plugin cplugin bootstrap $(MAKE) -C libraries install $(MAKE) -C theories install + $(MAKE) -C runtime install $(MAKE) -C plugin install $(MAKE) -C cplugin install $(MAKE) -C bootstrap install @@ -55,10 +55,14 @@ mrproper: theories/Makefile libraries/Makefile plugin/Makefile cplugin/Makefile clean: theories/Makefile libraries/Makefile plugin/Makefile cplugin/Makefile $(MAKE) -C libraries clean $(MAKE) -C theories clean + $(MAKE) -C runtime clean $(MAKE) -C plugin clean $(MAKE) -C cplugin clean $(MAKE) -C bootstrap clean rm -f `find theories -name "*.ml*"` rm -rf plugin/extraction rm -rf cplugin/extraction - $(MAKE) mrproper \ No newline at end of file + $(MAKE) mrproper + +runtime: runtime/Makefile + $(MAKE) -C runtime diff --git a/benchmarks/Makefile b/benchmarks/Makefile index 3e818122c..5f5cdddc5 100644 --- a/benchmarks/Makefile +++ b/benchmarks/Makefile @@ -7,7 +7,7 @@ TESTS=$(shell cat TESTS) CFILES=$(patsubst %, CertiCoq.Benchmarks.tests.%_cps.c, $(TESTS)) $(patsubst %, CertiCoq.Benchmarks.tests.%.c, $(TESTS)) # Names of the generated executables EXEC=$(TESTS) $(patsubst %, %_cps, $(TESTS)) $(patsubst %, %_cps_opt, $(TESTS)) $(patsubst %, %_opt, $(TESTS)) -INCLUDE=../plugin/runtime +INCLUDE=../runtime all: lib tests exec run default: exec run diff --git a/benchmarks/metacoq_erasure/Makefile b/benchmarks/metacoq_erasure/Makefile index 4a9113961..a6a34ace8 100644 --- a/benchmarks/metacoq_erasure/Makefile +++ b/benchmarks/metacoq_erasure/Makefile @@ -11,7 +11,7 @@ COQOPTS = -Q ../../theories/Codegen CertiCoq.Codegen -Q ../../libraries CertiCoq -Q ../../theories/Compiler CertiCoq.Compiler -Q ../../theories/common CertiCoq.Common \ -Q ../../theories/LambdaBoxMut CertiCoq.LambdaBoxMut -Q .. CertiCoq.Benchmarks -RUNTIME_DIR = ../../plugin/runtime +RUNTIME_DIR = ../../runtime RUNTIME_FILES = ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_int63.o plugin: metacoq_erasure.vo Loader.vo diff --git a/bootstrap/certicoqc/Makefile b/bootstrap/certicoqc/Makefile index 2b804e7ad..b73738933 100644 --- a/bootstrap/certicoqc/Makefile +++ b/bootstrap/certicoqc/Makefile @@ -60,7 +60,7 @@ OCAMLOPTS = -package coq-metacoq-template-ocaml.plugin -open Metacoq_template_pl GENCFILES = glue.c CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c CFILES = certicoqc_wrapper.c $(GENCFILES) -RUNTIME_DIR = ../../plugin/runtime +RUNTIME_DIR = ../../runtime RUNTIME_FILES = $(RUNTIME_DIR)/gc_stack.o $(RUNTIME_DIR)/prim_floats.o $(RUNTIME_DIR)/prim_int63.o $(RUNTIME_DIR)/coq_c_ffi.o VFILES = theories/Loader.v theories/PrimInt63.v theories/PrimFloats.v theories/CertiCoqC.v diff --git a/bootstrap/certicoqc/g_certicoqc.mlg b/bootstrap/certicoqc/g_certicoqc.mlg index edd3ff67d..88d9cb72c 100644 --- a/bootstrap/certicoqc/g_certicoqc.mlg +++ b/bootstrap/certicoqc/g_certicoqc.mlg @@ -10,6 +10,7 @@ open Stdarg open Pcoq.Prim open Plugin_utils open Certicoq +open Tacarg open G_certicoq_vanilla } @@ -58,3 +59,32 @@ VERNAC COMMAND EXTEND CertiCoqCCompile CLASSIFIED AS QUERY Feedback.msg_info (str help_msg) } END + + +VERNAC COMMAND EXTEND CertiCoqC_Eval CLASSIFIED AS SIDEFF +| [ "CertiCoqC" "Eval" vanilla_cargs_list(l) global(gr) "Extract" "Constants" "[" vanilla_extract_cnst_list_sep(cs, ",") "]" "Include" "[" vanilla_cinclude_list_sep(imps, ",") "]" ] -> { + let gr = Nametab.global gr in + let opts = Certicoq.make_options l cs (get_name gr) in + let result = Certicoq.eval_gr opts gr imps in + Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result) + } +| [ "CertiCoqC" "Eval" vanilla_cargs_list(l) global(gr) ] -> { + let gr = Nametab.global gr in + let opts = Certicoq.make_options l [] (get_name gr) in + let result = Certicoq.eval_gr opts gr [] in + Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result) + } +END + +TACTIC EXTEND CertiCoqc_eval +| [ "certicoqc_eval" vanilla_cargs_list(l) constr(c) tactic(tac) ] -> + { (* quote and evaluate the given term, unquote, pass the result to t *) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let opts = Certicoq.make_options l [] "goal" in + let opts = Certicoq.{ opts with toplevel_name = "goal" } in + let c' = Certicoq.eval opts env sigma c [] in + ltac_apply tac (List.map to_ltac_val [EConstr.of_constr c']) + end } +END diff --git a/bootstrap/certicoqc/test.v b/bootstrap/certicoqc/test.v index 4ba1a014d..320c4d8d0 100644 --- a/bootstrap/certicoqc/test.v +++ b/bootstrap/certicoqc/test.v @@ -38,7 +38,12 @@ Definition certicoqc (opts : Options) (p : Template.Ast.Env.program) := Set Warnings "-primitive-turned-into-axiom". -Definition demo1 := [1; 0; 1]. +(* Definition demo1 := show [1; 0; 1]. + +CertiCoqC Eval demo1. + +Definition demo2 := if false then false else true. +CertiCoqC Eval demo2. *) (* Time CertiCoqC Compile -build_dir "tests" -time -O 1 demo1. *) diff --git a/bootstrap/certicoqc/theories/CertiCoqC.v b/bootstrap/certicoqc/theories/CertiCoqC.v index cdcab9b7f..82397a5da 100644 --- a/bootstrap/certicoqc/theories/CertiCoqC.v +++ b/bootstrap/certicoqc/theories/CertiCoqC.v @@ -13,8 +13,8 @@ Section Pipeline. (prims : list (Kernames.kername * string * bool * nat * positive)) (debug : bool). - Definition CertiCoq_pipeline econf (p : Ast.Env.program) := - p <- compile_LambdaBoxMut econf p ;; + Definition CertiCoq_pipeline econf im (p : Ast.Env.program) := + p <- compile_LambdaBoxMut econf im p ;; p <- compile_LambdaBoxLocal prims p ;; p <- compile_LambdaANF_ANF next_id prims p ;; (* if debug then compile_LambdaANF_debug next_id p For debugging intermediate states of the λanf pipeline else *) @@ -28,7 +28,7 @@ Definition pipeline (p : Template.Ast.Env.program) := let genv := fst p in o <- get_options ;; '(prs, next_id) <- register_prims next_id genv.(Ast.Env.declarations) ;; - p' <- CertiCoq_pipeline next_id prs o.(erasure_config) p ;; + p' <- CertiCoq_pipeline next_id prs o.(erasure_config) o.(inductives_mapping) p ;; compile_Clight prs p'. Definition compile (opts : Options) (p : Template.Ast.Env.program) := diff --git a/bootstrap/certicoqchk/META b/bootstrap/certicoqchk/META deleted file mode 100644 index 048bb7ced..000000000 --- a/bootstrap/certicoqchk/META +++ /dev/null @@ -1,9 +0,0 @@ - -package "plugin" ( - requires = "coq-core.plugins.ltac coq-metacoq-template-ocaml.plugin coq-certicoq-vanilla.plugin stdlib-shims" - archive(byte) = "certicoqchk_plugin.cma" - archive(native) = "certicoqchk_plugin.cmxa" - plugin(byte) = "certicoqchk_plugin.cma" - plugin(native) = "certicoqchk_plugin.cmxs" -) - diff --git a/bootstrap/certicoqchk/Makefile b/bootstrap/certicoqchk/Makefile index 5bf14916f..205acf59c 100644 --- a/bootstrap/certicoqchk/Makefile +++ b/bootstrap/certicoqchk/Makefile @@ -36,7 +36,7 @@ OCAMLOPTS = -package coq-metacoq-template-ocaml.plugin -open Metacoq_template_pl GENCFILES = glue.c CertiCoq.CertiCoqCheck.compile.certicoqchk.c CFILES = certicoqchk_wrapper.c ${GENCFILES} -RUNTIME_DIR = ../../plugin/runtime +RUNTIME_DIR = ../../runtime RUNTIME_FILES = ${RUNTIME_DIR}/gc_stack.o ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_int63.o ${RUNTIME_DIR}/coq_ffi.o CCOMPILEROPTS = -fPIC -g -c -I . -I ${RUNTIME_DIR} -I ${OCAMLLIB} -w -Wno-everything -O2 diff --git a/bootstrap/certicoqchk/certicoqchk.ml b/bootstrap/certicoqchk/certicoqchk.ml index 87cb51f45..b4eecf872 100644 --- a/bootstrap/certicoqchk/certicoqchk.ml +++ b/bootstrap/certicoqchk/certicoqchk.ml @@ -21,6 +21,4 @@ let check gr = (* Quote Coq term *) let p = quote gr in let b = Certicoqchk_plugin_wrapper.check (Obj.magic p) (* Go through a type equality *) in - match b with - | Datatypes.Coq_true -> () - | Datatypes.Coq_false -> CErrors.user_err Pp.(str"The program does not typecheck") + if b then () else CErrors.user_err Pp.(str"The program does not typecheck") diff --git a/bootstrap/certicoqchk/certicoqchk_plugin_wrapper.ml b/bootstrap/certicoqchk/certicoqchk_plugin_wrapper.ml index 948050b14..1d6aad786 100644 --- a/bootstrap/certicoqchk/certicoqchk_plugin_wrapper.ml +++ b/bootstrap/certicoqchk/certicoqchk_plugin_wrapper.ml @@ -6,7 +6,7 @@ open Ast0 open Toplevel2 open Pipeline_utils -external certicoqchk_wrapper : Ast0.Env.program -> Datatypes.bool = "certicoqchk_wrapper" +external certicoqchk_wrapper : Ast0.Env.program -> bool = "certicoqchk_wrapper" let info s = Feedback.msg_info (Pp.str s) let msg_info s = diff --git a/bootstrap/certicoqchk/certicoqchk_plugin_wrapper.mli b/bootstrap/certicoqchk/certicoqchk_plugin_wrapper.mli index 231722fa6..0f3ed64bb 100644 --- a/bootstrap/certicoqchk/certicoqchk_plugin_wrapper.mli +++ b/bootstrap/certicoqchk/certicoqchk_plugin_wrapper.mli @@ -1 +1 @@ -val check : Ast0.Env.program -> Datatypes.bool +val check : Ast0.Env.program -> bool diff --git a/cplugin/Loader.v b/cplugin/Loader.v index 6f01f196b..95595d5d9 100644 --- a/cplugin/Loader.v +++ b/cplugin/Loader.v @@ -1 +1,3 @@ -Declare ML Module "coq-certicoq-vanilla.plugin". \ No newline at end of file +Declare ML Module "coq-certicoq-vanilla.plugin". + +CertiCoq Extract Inductives [ bool => "bool" [ 1 0 ]]. \ No newline at end of file diff --git a/cplugin/Makefile.local b/cplugin/Makefile.local index 668244e4f..ca96bceec 100644 --- a/cplugin/Makefile.local +++ b/cplugin/Makefile.local @@ -15,7 +15,4 @@ merlin-hook:: $(HIDE)echo 'PKG coq-metacoq-template-ocaml.plugin' >> .merlin $(HIDE)echo 'PKG stdlib-shims' >> .merlin -get_ordinal.o: get_ordinal.c - $(CC) -c -o $@ -I runtime $< - -certicoq_plugin.cmxs: get_ordinal.o \ No newline at end of file +certicoq_plugin.cmxs: ../runtime/get_ordinal.o \ No newline at end of file diff --git a/cplugin/Makefile.local-late b/cplugin/Makefile.local-late index da418b424..b4ce6e94e 100644 --- a/cplugin/Makefile.local-late +++ b/cplugin/Makefile.local-late @@ -1,4 +1,2 @@ -# CAMLOPTLINK = "$(OCAMLFIND)" opt -linkall get_ordinal.o - -certicoq_vanilla_plugin.cmxa: certicoq_vanilla_plugin.cmx get_ordinal.o - $(HIDE)$(TIMER) $(CAMLOPTLINK) get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< +certicoq_vanilla_plugin.cmxa: certicoq_vanilla_plugin.cmx ../runtime/get_ordinal.o + $(HIDE)$(TIMER) $(CAMLOPTLINK) ../runtime/get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< diff --git a/cplugin/_CoqProject b/cplugin/_CoqProject index b9d0cb388..5ccdc7ba4 100644 --- a/cplugin/_CoqProject +++ b/cplugin/_CoqProject @@ -21,8 +21,6 @@ PrimInt63.v PrimFloats.v CertiCoqVanilla.v -static/caml_bool.mli -static/caml_bool.ml static/caml_option.mli static/caml_option.ml static/caml_nat.mli diff --git a/cplugin/certicoq.ml b/cplugin/certicoq.ml index 632e97a5a..312fab696 100644 --- a/cplugin/certicoq.ml +++ b/cplugin/certicoq.ml @@ -9,133 +9,6 @@ open ExceptionMonad open AstCommon open Plugin_utils -module FixRepr = -struct - -(** The ML value representation of an erased quoted program does not directly match - the one expected by CertiCoq erase function as singleton inductive types are unboxed, - we use Obj.t surgery to transform the value. - - This involves the transformation of universes sets, constraints sets and the representation - of universe values. - *) - -let fix_set u = - let block = Obj.new_block 0 1 in - Obj.set_field block 0 (Obj.magic u); - block - -let fix_universe u = - let open Universes0.Sort in - let fix_ues ues : Obj.t = - let block = Obj.new_block 0 1 in - Obj.set_field block 0 (Obj.magic ues); - block - in - let fix_neues neues : Obj.t = - let ues = fix_ues neues in - let block = Obj.new_block 0 1 in - Obj.set_field block 0 ues; - block - in - match u with - | Coq_sProp -> Coq_sProp - | Coq_sSProp -> Coq_sSProp - | Coq_sType neues -> Coq_sType (Obj.magic (fix_neues neues)) - -let fix_term (p : Ast0.term) : Ast0.term = - let open Ast0 in - let open BasicAst in - let open List in - let rec aux p = - match p with - | Coq_tRel _ | Coq_tVar _ | Coq_tConst _ | Coq_tInd _ | Coq_tConstruct _ -> p - | Coq_tEvar (k, l) -> Coq_tEvar (k, map aux l) - | Coq_tSort u -> Coq_tSort (fix_universe u) - | Coq_tCast (t, k, t') -> Coq_tCast (aux t, k, aux t') - | Coq_tProd (na, t, t') -> Coq_tProd (na, aux t, aux t') - | Coq_tLambda (na, t, t') -> Coq_tLambda (na, aux t, aux t') - | Coq_tLetIn (na, t, b, t') -> Coq_tLetIn (na, aux t, aux b, aux t') - | Coq_tApp (t, l) -> Coq_tApp (aux t, map aux l) - | Coq_tCase (ci, p, c, brs) -> Coq_tCase (ci, aux_pred p, aux c, map aux_branch brs) - | Coq_tProj (p, t) -> Coq_tProj (p, aux t) - | Coq_tFix (mfix, i) -> Coq_tFix (map aux_def mfix, i) - | Coq_tCoFix (mfix, i) -> Coq_tCoFix (map aux_def mfix, i) - | Coq_tInt i -> p - | Coq_tFloat f -> p - | Coq_tArray (u, v, def, ty) -> Coq_tArray (u, map aux v, aux def, aux ty) - and aux_pred { puinst = puinst; pparams = pparams; pcontext = pcontext; preturn = preturn } = - { puinst; pparams = map aux pparams; pcontext; preturn = aux preturn } - and aux_branch { bcontext = bcontext; bbody = bbody } = - { bcontext; bbody = aux bbody } - and aux_def { dname = dname; dtype = dtype; dbody = dbody; rarg = rarg } = - { dname; dtype = aux dtype; dbody = aux dbody; rarg } - in aux p - -let option_map f (x : 'a option) = - match x with - | None -> Datatypes.None - | Some x -> Datatypes.Some (f x) - -let fix_rel_context ctx = - let open BasicAst in - let fix_decl {decl_name; decl_body; decl_type} = - {decl_name; decl_body = option_map fix_term (Obj.magic decl_body); decl_type = fix_term decl_type} - in - List.map fix_decl ctx - -open Ast0 -open Universes0 - -let fix_universes_decl = function - | Monomorphic_ctx -> Monomorphic_ctx - | Polymorphic_ctx (names, set) -> Polymorphic_ctx (names, Obj.magic (fix_set set)) - -let fix_universes (levels, cstrs) = - (Obj.magic (fix_set levels), Obj.magic (fix_set cstrs)) - -let fix_declarations decls = - let open Ast0.Env in - let fix_constructor {cstr_name; cstr_args; cstr_indices; cstr_type; cstr_arity} = - {cstr_name; cstr_args = fix_rel_context cstr_args; - cstr_indices = List.map fix_term cstr_indices; - cstr_type = fix_term cstr_type; - cstr_arity} - in - let fix_projection {proj_name; proj_relevance; proj_type} = - { proj_name; proj_relevance; proj_type = fix_term proj_type } - in - let fix_ind_body {ind_name; ind_indices; ind_sort; ind_type; ind_kelim; ind_ctors; ind_projs; ind_relevance} = - {ind_name; ind_indices = fix_rel_context ind_indices; ind_sort = fix_universe ind_sort; - ind_type = fix_term ind_type; ind_kelim; - ind_ctors = List.map fix_constructor ind_ctors; - ind_projs = List.map fix_projection ind_projs; - ind_relevance} - in - let fix_decl (kn, decl) = - let decl' = match decl with - | Ast0.Env.ConstantDecl {cst_type; cst_body; cst_universes; cst_relevance} -> - Ast0.Env.ConstantDecl { cst_type = fix_term cst_type; cst_body = option_map fix_term (Obj.magic cst_body); - cst_universes = fix_universes_decl cst_universes; cst_relevance } - | Ast0.Env.InductiveDecl { ind_finite; ind_npars; ind_params; ind_bodies; ind_universes; ind_variance} -> - Ast0.Env.InductiveDecl { ind_finite; ind_npars; ind_params = fix_rel_context ind_params; - ind_bodies = List.map fix_ind_body ind_bodies; - ind_universes = fix_universes_decl ind_universes; - ind_variance} - in (kn, decl') - in - List.map fix_decl decls - -let fix_quoted_program (p : Ast0.Env.program) = - let ({ Ast0.Env.universes = universes; declarations = declarations; retroknowledge = retro }, term) = p in - let term = fix_term term in - let universes = fix_universes universes in - let declarations = fix_declarations declarations in - { Ast0.Env.universes = universes; declarations; retroknowledge = retro }, term - -end - - let get_stringopt_option key = let open Goptions in match get_option_value key with @@ -182,7 +55,7 @@ let increment_subscript id = end in String.of_bytes (add (len-1)) -let debug_reify = CDebug.create ~name:"certicoq-vanilla-reify" () +let debug_reify = CDebug.create ~name:"certicoq-reify" () external get_unboxed_ordinal : Obj.t -> int = "get_unboxed_ordinal" [@@noalloc] @@ -208,11 +81,11 @@ let debug_msg (flag : bool) (s : string) = (* Separate registration of primitive extraction *) -type prim = ((Kernames.kername * Kernames.ident) * Datatypes.bool) +type prim = ((Kernames.kername * Kernames.ident) * bool) let global_registers = - Summary.ref (([], []) : prim list * import list) ~name:"CertiCoq Vanilla Registration" + Summary.ref (([], []) : prim list * import list) ~name:"CertiCoq Registration" -let global_registers_name = "certicoq-vanilla-registration" +let global_registers_name = "certicoq-registration" let cache_registers (prims, imports) = let (prims', imports') = !global_registers in @@ -236,14 +109,39 @@ let register (prims : prim list) (imports : import list) : unit = let get_global_prims () = fst !global_registers let get_global_includes () = snd !global_registers +(* Extract Inductive *) +type inductive_mapping = Kernames.inductive * (string * int list) (* Target inductive type and mapping of constructor names to constructor tags *) +type inductives_mapping = inductive_mapping list + +let global_inductive_registers = + Summary.ref ([] : inductives_mapping) ~name:"CertiCoq Extract Inductive Registration" + +let global_inductive_registers_name = "certicoq-extract-inductive-registration" + +let cache_inductive_registers inds = + let inds' = !global_inductive_registers in + global_inductive_registers := inds @ inds' + +let global_inductive_registers_input = + let open Libobject in + declare_object + (global_object_nodischarge global_inductive_registers_name + ~cache:(fun r -> cache_inductive_registers r) + ~subst:None) + +let register_inductives (inds : inductives_mapping) : unit = + Lib.add_leaf (global_inductive_registers_input inds) + +let get_global_inductives_mapping () = !global_inductive_registers + (* Support for dynamically-linked certicoq-compiled programs *) type certicoq_run_function = unit -> Obj.t let certicoq_run_functions = - Summary.ref ~name:"CertiCoq Vanilla Run Functions Table" + Summary.ref ~name:"CertiCoq Run Functions Table" (CString.Map.empty : certicoq_run_function CString.Map.t) -let certicoq_run_functions_name = "certicoq-vanilla-run-functions-registration" +let certicoq_run_functions_name = "certicoq-run-functions-registration" let all_run_functions = ref CString.Set.empty @@ -300,7 +198,6 @@ let _ = Callback.register "coq_user_error" coq_user_error type command_args = | TYPED_ERASURE - | FAST_ERASURE | UNSAFE_ERASURE | BYPASS_QED | CPS @@ -319,7 +216,6 @@ type command_args = type options = { typed_erasure : bool; - fast_erasure : bool; unsafe_erasure : bool; bypass_qed : bool; cps : bool; @@ -335,7 +231,8 @@ type options = dev : int; prefix : string; toplevel_name : string; - prims : ((Kernames.kername * Kernames.ident) * Datatypes.bool) list; + prims : ((Kernames.kername * Kernames.ident) * bool) list; + inductives_mapping : inductives_mapping; } let check_build_dir d = @@ -351,7 +248,6 @@ let check_build_dir d = let default_options () : options = { typed_erasure = false; - fast_erasure = false; unsafe_erasure = false; bypass_qed = false; cps = false; @@ -368,14 +264,14 @@ let default_options () : options = prefix = ""; toplevel_name = "body"; prims = []; + inductives_mapping = get_global_inductives_mapping (); } -let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ident) * Datatypes.bool) list) (fname : string) : options = +let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ident) * bool) list) (fname : string) : options = let rec aux (o : options) l = match l with | [] -> o | TYPED_ERASURE :: xs -> aux {o with typed_erasure = true} xs - | FAST_ERASURE :: xs -> aux {o with fast_erasure = true} xs | UNSAFE_ERASURE :: xs -> aux {o with unsafe_erasure = true} xs | BYPASS_QED :: xs -> aux {o with bypass_qed = true} xs | CPS :: xs -> aux {o with cps = true} xs @@ -398,43 +294,42 @@ let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ide let o = aux opts l in {o with prims = pr} - let make_unsafe_passes b = let open Erasure0 in - let b = Caml_bool.to_coq b in { cofix_to_lazy = b; - reorder_constructors = b; inlining = b; unboxing = b; betared = b } + let all_unsafe_passes = make_unsafe_passes true let no_unsafe_passes = make_unsafe_passes false - + +let quote_inductives_mapping l = + List.map (fun (hd, (na, cstrs)) -> (hd, (bytestring_of_string na, List.map (fun i -> coq_nat_of_int i) cstrs))) l let make_pipeline_options (opts : options) = let erasure_config = Erasure0.({ - enable_typed_erasure = Caml_bool.to_coq opts.typed_erasure; + enable_typed_erasure = opts.typed_erasure; enable_unsafe = if opts.unsafe_erasure then all_unsafe_passes else no_unsafe_passes; - enable_fast_remove_params = Caml_bool.to_coq opts.fast_erasure; - dearging_config = default_dearging_config; (* FIXME *) - inductives_mapping = []; - inlined_constants = Obj.magic (FixRepr.fix_set Kernames.KernameSet.empty) + dearging_config = default_dearging_config; + inlined_constants = Kernames.KernameSet.empty }) in - let cps = Caml_bool.to_coq opts.cps in + let cps = opts.cps in let args = coq_nat_of_int opts.args in let olevel = coq_nat_of_int opts.olevel in - let timing = Caml_bool.to_coq opts.time in - let timing_anf = Caml_bool.to_coq opts.time_anf in - let debug = Caml_bool.to_coq opts.debug in + let timing = opts.time in + let timing_anf = opts.time_anf in + let debug = opts.debug in let anfc = coq_nat_of_int opts.anf_conf in let dev = coq_nat_of_int opts.dev in let prefix = bytestring_of_string opts.prefix in let toplevel_name = bytestring_of_string opts.toplevel_name in let prims = get_global_prims () @ opts.prims in + let inductives_mapping = quote_inductives_mapping opts.inductives_mapping in (* Feedback.msg_debug Pp.(str"Prims: " ++ prlist_with_sep spc (fun ((x, y), wt) -> str (string_of_bytestring y)) prims); *) - Pipeline.make_opts erasure_config cps args anfc olevel timing timing_anf debug dev prefix toplevel_name prims + Pipeline.make_opts erasure_config inductives_mapping cps args anfc olevel timing timing_anf debug dev prefix toplevel_name prims (** Main Compilation Functions *) @@ -454,7 +349,7 @@ let quote_term opts env sigma c = let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass env sigma (EConstr.to_constr sigma c) in let time = (Unix.gettimeofday() -. time) in debug_msg debug (Printf.sprintf "Finished quoting in %f s.. compiling to L7." time); - Obj.magic term + term let quote opts gr = let env = Global.env () in @@ -477,11 +372,144 @@ module type CompilerInterface = sig end + +module FixRepr = +struct + +(** The ML value representation of an erased quoted program does not directly match + the one expected by CertiCoq erase function as singleton inductive types are unboxed, + we use Obj.t surgery to transform the value. + + This involves the transformation of universes sets, constraints sets and the representation + of universe values. + *) + +let fix_set u = + let block = Obj.new_block 0 1 in + Obj.set_field block 0 (Obj.magic u); + block + +let fix_universe u = + let open Universes0.Sort in + let fix_ues ues : Obj.t = + let block = Obj.new_block 0 1 in + Obj.set_field block 0 (Obj.magic ues); + block + in + let fix_neues neues : Obj.t = + let ues = fix_ues neues in + let block = Obj.new_block 0 1 in + Obj.set_field block 0 ues; + block + in + match u with + | Coq_sProp -> Coq_sProp + | Coq_sSProp -> Coq_sSProp + | Coq_sType neues -> Coq_sType (Obj.magic (fix_neues neues)) + +let fix_term (p : Ast0.term) : Ast0.term = + let open Ast0 in + let open BasicAst in + let open List in + let rec aux p = + match p with + | Coq_tRel _ | Coq_tVar _ | Coq_tConst _ | Coq_tInd _ | Coq_tConstruct _ -> p + | Coq_tEvar (k, l) -> Coq_tEvar (k, map aux l) + | Coq_tSort u -> Coq_tSort (fix_universe u) + | Coq_tCast (t, k, t') -> Coq_tCast (aux t, k, aux t') + | Coq_tProd (na, t, t') -> Coq_tProd (na, aux t, aux t') + | Coq_tLambda (na, t, t') -> Coq_tLambda (na, aux t, aux t') + | Coq_tLetIn (na, t, b, t') -> Coq_tLetIn (na, aux t, aux b, aux t') + | Coq_tApp (t, l) -> Coq_tApp (aux t, map aux l) + | Coq_tCase (ci, p, c, brs) -> Coq_tCase (ci, aux_pred p, aux c, map aux_branch brs) + | Coq_tProj (p, t) -> Coq_tProj (p, aux t) + | Coq_tFix (mfix, i) -> Coq_tFix (map aux_def mfix, i) + | Coq_tCoFix (mfix, i) -> Coq_tCoFix (map aux_def mfix, i) + | Coq_tInt i -> p + | Coq_tFloat f -> p + | Coq_tArray (u, v, def, ty) -> Coq_tArray (u, map aux v, aux def, aux ty) + and aux_pred { puinst = puinst; pparams = pparams; pcontext = pcontext; preturn = preturn } = + { puinst; pparams = map aux pparams; pcontext; preturn = aux preturn } + and aux_branch { bcontext = bcontext; bbody = bbody } = + { bcontext; bbody = aux bbody } + and aux_def { dname = dname; dtype = dtype; dbody = dbody; rarg = rarg } = + { dname; dtype = aux dtype; dbody = aux dbody; rarg } + in aux p + +let option_map f (x : 'a option) = + match x with + | None -> Datatypes.None + | Some x -> Datatypes.Some (f x) + +let fix_rel_context ctx = + let open BasicAst in + let fix_decl {decl_name; decl_body; decl_type} = + {decl_name; decl_body = option_map fix_term (Obj.magic decl_body); decl_type = fix_term decl_type} + in + List.map fix_decl ctx + +open Ast0 +open Universes0 + +let fix_universes_decl = function + | Monomorphic_ctx -> Monomorphic_ctx + | Polymorphic_ctx (names, set) -> Polymorphic_ctx (names, Obj.magic (fix_set set)) + +let fix_universes (levels, cstrs) = + (Obj.magic (fix_set levels), Obj.magic (fix_set cstrs)) + +let fix_declarations decls = + let open Ast0.Env in + let fix_constructor {cstr_name; cstr_args; cstr_indices; cstr_type; cstr_arity} = + {cstr_name; cstr_args = fix_rel_context cstr_args; + cstr_indices = List.map fix_term cstr_indices; + cstr_type = fix_term cstr_type; + cstr_arity} + in + let fix_projection {proj_name; proj_relevance; proj_type} = + { proj_name; proj_relevance; proj_type = fix_term proj_type } + in + let fix_ind_body {ind_name; ind_indices; ind_sort; ind_type; ind_kelim; ind_ctors; ind_projs; ind_relevance} = + {ind_name; ind_indices = fix_rel_context ind_indices; ind_sort = fix_universe ind_sort; + ind_type = fix_term ind_type; ind_kelim; + ind_ctors = List.map fix_constructor ind_ctors; + ind_projs = List.map fix_projection ind_projs; + ind_relevance} + in + let fix_decl (kn, decl) = + let decl' = match decl with + | Ast0.Env.ConstantDecl {cst_type; cst_body; cst_universes; cst_relevance} -> + Ast0.Env.ConstantDecl { cst_type = fix_term cst_type; cst_body = option_map fix_term (Obj.magic cst_body); + cst_universes = fix_universes_decl cst_universes; cst_relevance } + | Ast0.Env.InductiveDecl { ind_finite; ind_npars; ind_params; ind_bodies; ind_universes; ind_variance} -> + Ast0.Env.InductiveDecl { ind_finite; ind_npars; ind_params = fix_rel_context ind_params; + ind_bodies = List.map fix_ind_body ind_bodies; + ind_universes = fix_universes_decl ind_universes; + ind_variance} + in (kn, decl') + in + List.map fix_decl decls + +let fix_quoted_program (p : Ast0.Env.program) = + let ({ Ast0.Env.universes = universes; declarations = declarations; retroknowledge = retro }, term) = p in + let term = fix_term term in + let universes = fix_universes universes in + let declarations = fix_declarations declarations in + { Ast0.Env.universes = universes; declarations; retroknowledge = retro }, term + +end + +let fix_opts opts = + Pipeline_utils.{ opts with erasure_config = + { opts.erasure_config with Erasure0.inlined_constants = Obj.magic (FixRepr.fix_set opts.erasure_config.Erasure0.inlined_constants) } } + module MLCompiler : CompilerInterface with type name_env = BasicAst.name Cps.M.t = struct type name_env = BasicAst.name Cps.M.t - let compile opt prg = Pipeline.compile opt (FixRepr.fix_quoted_program prg) + let compile opts prg = + let opts = fix_opts opts in + Pipeline.compile opts (FixRepr.fix_quoted_program prg) let printProg prog names (dest : string) (imports : import list) = let imports' = List.map (fun i -> match i with | FromRelativePath s -> "#include \"" ^ s ^ "\"" @@ -490,8 +518,12 @@ module MLCompiler : CompilerInterface with failwith "Import with absolute path should have been filled") imports in PrintClight.print_dest_names_imports prog (Cps.M.elements names) dest imports' - let generate_glue opts decls = Glue.generate_glue opts (FixRepr.fix_declarations decls) - let generate_ffi opts prg = Ffi.generate_ffi opts (FixRepr.fix_quoted_program prg) + let generate_glue opts decls = + let opts = fix_opts opts in + Glue.generate_glue opts (FixRepr.fix_declarations decls) + let generate_ffi opts prg = + let opts = fix_opts opts in + Ffi.generate_ffi opts (FixRepr.fix_quoted_program prg) end @@ -500,6 +532,53 @@ module CompileFunctor (CI : CompilerInterface) = struct let make_fname opts str = Filename.concat opts.build_dir str + type line = + | EOF + | Info of string + | Error of string + + let read_line stdout stderr = + try Info (input_line stdout) + with End_of_file -> + try Error (input_line stderr) + with End_of_file -> EOF + + let push_line buf line = + Buffer.add_string buf line; + Buffer.add_string buf "\n" + + let string_of_buffer buf = Bytes.to_string (Buffer.to_bytes buf) + + let execute cmd = + debug Pp.(fun () -> str "Executing: " ++ str cmd ++ str " in environemt: " ++ + prlist_with_sep spc str (Array.to_list (Unix.environment ()))); + let (stdout, stdin, stderr) = Unix.open_process_full cmd (Unix.environment ()) in + let continue = ref true in + let outbuf, errbuf = Buffer.create 100, Buffer.create 100 in + let push_info = push_line outbuf in + let push_error = push_line errbuf in + while !continue do + match read_line stdout stderr with + | EOF -> debug Pp.(fun () -> str "Program terminated"); continue := false + | Info s -> push_info s + | Error s -> push_error s + done; + let status = Unix.close_process_full (stdout, stdin, stderr) in + status, string_of_buffer outbuf, string_of_buffer errbuf + + let execute ?loc cmd = + let status, out, err = execute cmd in + match status with + | Unix.WEXITED 0 -> out, err + | Unix.WEXITED n -> + CErrors.user_err ?loc Pp.(str"Command" ++ spc () ++ str cmd ++ spc () ++ + str"exited with code " ++ int n ++ str "." ++ fnl () ++ + str"stdout: " ++ spc () ++ str out ++ fnl () ++ str "stderr: " ++ str err) + | Unix.WSIGNALED n | Unix.WSTOPPED n -> + CErrors.user_err ?loc Pp.(str"Command" ++ spc () ++ str cmd ++ spc () ++ + str"was signaled with code " ++ int n ++ str"." ++ fnl () ++ + str"stdout: " ++ spc () ++ str out ++ fnl () ++ str "stderr: " ++ str err) + let compile opts term imports = let debug = opts.debug in let options = make_pipeline_options opts in @@ -600,11 +679,6 @@ module CompileFunctor (CI : CompilerInterface) = struct | None -> find_executable debug "which ocamlfind" | Some s -> s - type line = - | EOF - | Info of string - | Error of string - let read_line stdout stderr = try Info (input_line stdout) with End_of_file -> @@ -619,7 +693,8 @@ module CompileFunctor (CI : CompilerInterface) = struct | EOF -> debug_msg debug ("Program terminated"); continue := false | Info s -> Feedback.msg_notice Pp.(str prog ++ str": " ++ str s) | Error s -> Feedback.msg_warning Pp.(str prog ++ str": " ++ str s) - done + done; + ignore (Unix.close_process_full (stdout, stdin, stderr)) let runtime_dir () = let open Boot in @@ -746,8 +821,28 @@ module CompileFunctor (CI : CompilerInterface) = struct let time = Unix.gettimeofday () -. start in Feedback.msg_notice Pp.(msg ++ str (Printf.sprintf " executed in %f sec" time)); res - - let reify env sigma ty v : Constr.t = + + let apply_reordering hd m cstrs = + try + let find_ind_ord (ind, (na, tags)) = + if Kernames.eq_inductive_def ind hd then + Some (Array.of_list (List.map (fun i -> cstrs.(i)) tags)) + else None + in + CList.find_map_exn find_ind_ord m + with Not_found -> cstrs + + let find_reverse_mapping hd m cstr = + try + let find_ind_ord (ind, (na, tags)) = + if Kernames.eq_inductive_def ind hd then + Some (CList.index0 Int.equal cstr tags) + else None + in + CList.find_map_exn find_ind_ord m + with Not_found -> cstr + + let reify im env sigma ty v : Constr.t = let open Declarations in let debug s = debug_reify Pp.(fun () -> str s) in let rec aux ty v = @@ -757,11 +852,13 @@ module CompileFunctor (CI : CompilerInterface) = struct | IsInductive (hd, u, args) -> let open Inductive in let open Inductiveops in + let qhd = match Metacoq_template_plugin.Ast_quoter.quote_global_reference (IndRef hd) with Metacoq_template_plugin.Kernames.IndRef i -> (Obj.magic i : Kernames.inductive) | _ -> assert false in let spec = lookup_mind_specif env hd in let npars = inductive_params spec in let params, _indices = CList.chop npars args in let indfam = make_ind_family ((hd, u), params) in let cstrs = get_constructors env indfam in + let cstrs = apply_reordering qhd im cstrs in if Obj.is_block v then let ord = get_boxed_ordinal v in let () = debug (Printf.sprintf "Reifying constructor block of tag %i" ord) in @@ -770,6 +867,7 @@ module CompileFunctor (CI : CompilerInterface) = struct with Not_found -> ill_formed env sigma ty in let cstr = cstrs.(coqidx) in + let coqidx = find_reverse_mapping qhd im coqidx in let ctx = Vars.smash_rel_context cstr.cs_args in let vargs = List.init (List.length ctx) (Obj.field v) in let args' = List.map2 (fun decl v -> @@ -784,6 +882,7 @@ module CompileFunctor (CI : CompilerInterface) = struct try find_nth_constant ord cstrs with Not_found -> ill_formed env sigma ty in + let coqidx = find_reverse_mapping qhd im coqidx in let () = debug (Printf.sprintf "Reifying constant constructor: %i is %i in Coq" ord coqidx) in Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) params | IsPrimitive (c, u, _args) -> @@ -797,8 +896,8 @@ module CompileFunctor (CI : CompilerInterface) = struct in aux ty v let reify opts env sigma tyinfo result = - if opts.time then time ~msg:(Pp.str "Reification") (fun () -> reify env sigma tyinfo result) - else reify env sigma tyinfo result + if opts.time then time ~msg:(Pp.str "Reification") (fun () -> reify opts.inductives_mapping env sigma tyinfo result) + else reify opts.inductives_mapping env sigma tyinfo result let template name = Printf.sprintf "\nvalue %s ()\n { struct thread_info* tinfo = make_tinfo(); return %s_body(tinfo); }\n" name name @@ -869,32 +968,25 @@ module CompileFunctor (CI : CompilerInterface) = struct "coq-core.interp"; "coq-core.kernel"; "coq-core.library"] in let pkgs = String.concat "," packages in let dontlink = "str,unix,dynlink,threads,zarith,coq-core,coq-core.plugins.ltac,coq-core.interp" in - match Unix.system cmd with - | Unix.WEXITED 0 -> - let shared_lib = make_fname opts opts.filename ^ suff ^ ".cmxs" in - let linkcmd = - Printf.sprintf "%s ocamlopt -shared -linkpkg -dontlink %s -thread -rectypes -package %s \ - -I %s -I plugin -o %s %s %s %s %s" - ocamlfind dontlink pkgs opts.build_dir shared_lib ocaml_driver gc_stack_o - (make_fname opts opts.filename ^ ".o") importso - in - debug_msg debug (Printf.sprintf "Executing command: %s" linkcmd); - (match Unix.system linkcmd with - | Unix.WEXITED 0 -> - debug_msg debug (Printf.sprintf "Compilation ran fine, linking compiled code for %s" global_id); - Dynlink.loadfile_private shared_lib; - debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" global_id); - let result = - if opts.time then time ~msg:(Pp.str id) (run_certicoq_run global_id) - else run_certicoq_run global_id () - in - debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); - reify opts env sigma tyinfo result - | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str linkcmd) - | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n)) - | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str cmd) - | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n ++ str" while running " ++ str cmd) - + let () = ignore (execute cmd) in + let shared_lib = make_fname opts opts.filename ^ suff ^ ".cmxs" in + let linkcmd = + Printf.sprintf "%s ocamlopt -shared -linkpkg -dontlink %s -thread -rectypes -package %s \ + -I %s -I cplugin -o %s %s %s %s %s" + ocamlfind dontlink pkgs opts.build_dir shared_lib ocaml_driver gc_stack_o + (make_fname opts opts.filename ^ ".o") importso + in + debug_msg debug (Printf.sprintf "Executing command: %s" linkcmd); + let _out, _err = execute linkcmd in + Dynlink.loadfile_private shared_lib; + debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" global_id); + let result = + if opts.time then time ~msg:(Pp.str id) (run_certicoq_run global_id) + else run_certicoq_run global_id () + in + debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); + reify opts env sigma tyinfo result + let next_string_away_from s bad = let rec name_rec s = if bad s then name_rec (increment_subscript s) else s in name_rec s @@ -948,6 +1040,7 @@ module CompileFunctor (CI : CompilerInterface) = struct Printf.fprintf f "%s\n" s; close_out f + let show_ir opts gr = let term = quote opts gr in let debug = opts.debug in diff --git a/cplugin/certicoq.mli b/cplugin/certicoq.mli index ae0650271..3085364bb 100644 --- a/cplugin/certicoq.mli +++ b/cplugin/certicoq.mli @@ -2,7 +2,6 @@ open Plugin_utils type command_args = | TYPED_ERASURE - | FAST_ERASURE | UNSAFE_ERASURE | BYPASS_QED | CPS @@ -19,28 +18,31 @@ type command_args = | TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *) | FILENAME of string (* Name of the generated file *) - type options = - { typed_erasure : bool; - fast_erasure : bool; - unsafe_erasure : bool; - bypass_qed : bool; - cps : bool; - time : bool; - time_anf : bool; - olevel : int; - debug : bool; - args : int; - anf_conf : int; - build_dir : string; - filename : string; - ext : string; - dev : int; - prefix : string; - toplevel_name : string; - prims : ((Kernames.kername * Kernames.ident) * Datatypes.bool) list; - } +type inductive_mapping = Kernames.inductive * (string * int list) (* Target inductive type and mapping of constructor names to constructor tags *) +type inductives_mapping = inductive_mapping list +type prim = ((Kernames.kername * Kernames.ident) * bool) -type prim = ((Kernames.kername * Kernames.ident) * Datatypes.bool) + +type options = + { typed_erasure : bool; + unsafe_erasure : bool; + bypass_qed : bool; + cps : bool; + time : bool; + time_anf : bool; + olevel : int; + debug : bool; + args : int; + anf_conf : int; + build_dir : string; + filename : string; + ext : string; + dev : int; + prefix : string; + toplevel_name : string; + prims : prim list; + inductives_mapping : inductives_mapping; + } val default_options : unit -> options val make_options : command_args list -> prim list -> string -> options @@ -48,7 +50,19 @@ val make_options : command_args list -> prim list -> string -> options (* Register primitive operations and associated include file *) val register : prim list -> import list -> unit +val register_inductives : inductives_mapping -> unit + val get_name : Names.GlobRef.t -> string + +(* Support for running dynamically linked certicoq-compiled programs *) +type certicoq_run_function = unit -> Obj.t + +(* [register_certicoq_run global_id fresh_name function]. A same global_id + can be compiled multiple times with different definitions, fresh_name indicates + the version used this time *) +val register_certicoq_run : string -> string -> certicoq_run_function -> unit +val run_certicoq_run : string -> certicoq_run_function + module type CompilerInterface = sig type name_env val compile : Pipeline_utils.coq_Options -> Ast0.Env.program -> ((name_env * Clight.program) * Clight.program) CompM.error * Bytestring.String.t @@ -58,8 +72,7 @@ module type CompilerInterface = sig (((name_env * Clight.program) * Clight.program) * Bytestring.String.t list) CompM.error val generate_ffi : - Pipeline_utils.coq_Options -> Ast0.Env.program -> (((name_env * Clight.program) * Clight.program) * Bytestring.String.t list) CompM.error - + Pipeline_utils.coq_Options -> Ast0.Env.program -> (((name_env * Clight.program) * Clight.program) * Bytestring.String.t list) CompM.error end module CompileFunctor (CI : CompilerInterface) : sig @@ -69,22 +82,15 @@ module CompileFunctor (CI : CompilerInterface) : sig val show_ir : options -> Names.GlobRef.t -> unit val ffi_command : options -> Names.GlobRef.t -> unit val glue_command : options -> Names.GlobRef.t list -> unit + val eval_gr : options -> Names.GlobRef.t -> import list -> Constr.t + val eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t end val compile_only : options -> Names.GlobRef.t -> import list -> unit val generate_glue_only : options -> Names.GlobRef.t -> unit val compile_C : options -> Names.GlobRef.t -> import list -> unit -val eval_gr : options -> Names.GlobRef.t -> import list -> Constr.t val show_ir : options -> Names.GlobRef.t -> unit val ffi_command : options -> Names.GlobRef.t -> unit val glue_command : options -> Names.GlobRef.t list -> unit -val eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t - -(* Support for running dynamically linked certicoq-compiled programs *) -type certicoq_run_function = unit -> Obj.t - -(* [register_certicoq_run global_id fresh_name function]. A same global_id - can be compiled multiple times with different definitions, fresh_name indicates - the version used this time *) -val register_certicoq_run : string -> string -> certicoq_run_function -> unit -val run_certicoq_run : string -> certicoq_run_function +val eval_gr : options -> Names.GlobRef.t -> import list -> Constr.t +val eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t \ No newline at end of file diff --git a/cplugin/certicoq_vanilla_plugin.mlpack b/cplugin/certicoq_vanilla_plugin.mlpack index 3b87bd4e2..738163aad 100644 --- a/cplugin/certicoq_vanilla_plugin.mlpack +++ b/cplugin/certicoq_vanilla_plugin.mlpack @@ -4,7 +4,6 @@ Tm_util Datatypes Caml_nat -Caml_bool Caml_option Caml_comparison DecidableClass diff --git a/cplugin/g_certicoq_vanilla.mlg b/cplugin/g_certicoq_vanilla.mlg index eddffe4a0..8f5694619 100644 --- a/cplugin/g_certicoq_vanilla.mlg +++ b/cplugin/g_certicoq_vanilla.mlg @@ -39,11 +39,25 @@ let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = let to_ltac_val c = Tacinterp.Value.of_constr c +let globref_of_qualid ?loc (gr : Libnames.qualid) : Names.GlobRef.t = + match Constrintern.locate_reference gr with + | None -> CErrors.user_err ?loc Pp.(Libnames.pr_qualid gr ++ str " not found.") + | Some g -> g + +let quoted_globref_of_qualid ~loc (gr : Libnames.qualid) : Metacoq_template_plugin.Kernames.global_reference = + Metacoq_template_plugin.Ast_quoter.quote_global_reference (globref_of_qualid ~loc gr) + +let inductive_of_qualid ~loc (gr : Libnames.qualid) : Kernames.inductive = + let open Metacoq_template_plugin in + match quoted_globref_of_qualid ~loc gr with + | Kernames.ConstRef kn -> CErrors.user_err ~loc Pp.(str "Expected an inductive name but found a constant.") + | Kernames.VarRef(v) -> CErrors.user_err ~loc Pp.(str "Expected an inductive name but found a variable.") + | Kernames.IndRef(i) -> (Obj.magic i) + | Kernames.ConstructRef(_, _) -> CErrors.user_err ~loc Pp.(str "Expected an inductive name but found a constructor.") } ARGUMENT EXTEND vanilla_cargs | [ "-typed-erasure" ] -> { TYPED_ERASURE } -| [ "-fast-erasure" ] -> { FAST_ERASURE } | [ "-unsafe-erasure" ] -> { UNSAFE_ERASURE } | [ "-bypass_qed" ] -> { BYPASS_QED } | [ "-cps" ] -> { CPS } @@ -63,8 +77,8 @@ END VERNAC ARGUMENT EXTEND vanilla_extract_cnst -| [ reference(gr) "=>" string(str) ] -> { (extract_constant (Option.get (Constrintern.locate_reference gr)) str, Datatypes.Coq_false) } -| [ reference(gr) "=>" string(str) "with" "tinfo" ] -> { (extract_constant (Option.get (Constrintern.locate_reference gr)) str, Datatypes.Coq_true) } +| [ reference(gr) "=>" string(str) ] -> { (extract_constant (Option.get (Constrintern.locate_reference gr)) str, false) } +| [ reference(gr) "=>" string(str) "with" "tinfo" ] -> { (extract_constant (Option.get (Constrintern.locate_reference gr)) str, true) } END @@ -86,12 +100,22 @@ VERNAC ARGUMENT EXTEND vanilla_cinclude | [ "Library" string(str) string_opt(str') ] -> { FromLibrary (str, str') } END + +VERNAC ARGUMENT EXTEND vanilla_certiCoq_Register_extract_inductive +| [ reference(gr) "=>" string(ty) "[" natural_list(cstrs) "]" ] -> + { ((inductive_of_qualid ~loc gr), (ty, cstrs)) } +END + VERNAC COMMAND EXTEND CertiCoq_Register CLASSIFIED AS SIDEFF | [ "CertiCoq" "Register" "[" vanilla_extract_cnst_list_sep(l, ",") "]" "Include" "[" vanilla_cinclude_list_sep(imps, ",") "]" ] -> { - Certicoq.register l imps + Certicoq.register l imps } +| [ "CertiCoq" "Extract" "Inductives" "[" vanilla_certiCoq_Register_extract_inductive_list_sep(inds, ",") "]" ] -> { + Certicoq.register_inductives inds +} END + VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY | [ "CertiCoq" "Compile" vanilla_cargs_list(l) global(gr) ] -> { let gr = Nametab.global gr in diff --git a/cplugin/plugin_utils.ml b/cplugin/plugin_utils.ml index fbf46a160..6a7c4833a 100644 --- a/cplugin/plugin_utils.ml +++ b/cplugin/plugin_utils.ml @@ -69,7 +69,6 @@ Valid options:\n\ -time_anf : Time λanf optimizations\n\ -unsafe-erasure : Allow to use unsafe passes in the MetaCoq Erasure pipeline. This currently includes the cofixpoint-to-fixpoint translation.\n\ -typed-erasure : Uses the typed erasure and de-arging phase of the MetaCoq Erasure pipeline.\n\ --fast-erasure : Uses an alternative function to remove parameters of constructors in the MetaCoq Erasure pipeline.\n\ \n\n\ To compile Gallina constants to specific C functions use:\n\ CertiCoqC Compile Extract Constants [ constant1 => \"c_function1\", ... , constantN => \"c_functionN\" ] Include [ \"file1.h\", ... , \"fileM.h\" ]." diff --git a/cplugin/runtime/Makefile b/cplugin/runtime/Makefile deleted file mode 100644 index 9626fc490..000000000 --- a/cplugin/runtime/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -SRC = gc_stack.c certicoq_run_main.c coq_c_ffi.c prim_int63.c prim_floats.c -HEADERS = config.h values.h gc_stack.h certicoq_run_main.h coq_c_ffi.h prim_int63.h prim_floats.h -TARGETS = ${SRC:.c=.o} - -COQLIB = `coqc -where` -DST = ${COQLIB}/user-contrib/CertiCoq/Plugin/runtime - -all: ${TARGETS} - -%.o: %.c - gcc -I . -O2 -g -fomit-frame-pointer -c -o $@ $+ - -install: all - install -d ${DST} - install -m 0644 ${HEADERS} ${DST} - install -m 0644 ${SRC} ${DST} - install -m 0644 ${TARGETS} ${DST} diff --git a/cplugin/runtime/certicoq_run_main.c b/cplugin/runtime/certicoq_run_main.c deleted file mode 100644 index 1aecfdccd..000000000 --- a/cplugin/runtime/certicoq_run_main.c +++ /dev/null @@ -1,32 +0,0 @@ -#include -#include -#include "gc_stack.h" -#include - -extern void body(struct thread_info *); - -extern value args[]; - -_Bool is_ptr(value s) { - return (_Bool) Is_block(s); -} - -int main(int argc, char *argv[]) { - // value val; - struct thread_info* tinfo; - clock_t start, end; - double msec, sec; - - start = clock(); - tinfo = make_tinfo(); - body(tinfo); - end = clock(); - - // val = tinfo -> args[1]; - - sec = (double)(end - start)/CLOCKS_PER_SEC; - msec = 1000*sec; - printf("Time taken %f seconds %f milliseconds\n", sec, msec); - - return 0; -} diff --git a/cplugin/runtime/prim_floats.c b/cplugin/runtime/prim_floats.c deleted file mode 100644 index 3d4502ca1..000000000 --- a/cplugin/runtime/prim_floats.c +++ /dev/null @@ -1,265 +0,0 @@ -#include -#include -#include -#include -#include "gc_stack.h" -#include "prim_int63.h" - -typedef value primfloat; -typedef value primfloatintpair; -typedef value primfloat_comparison; -typedef value primfloat_class; - -#define trace(...) printf(__VA_ARGS__) -#define Double_block (Double_tag & (1 << 10)) - -primfloat mk_float (struct thread_info *tinfo, double x) { - trace("Calling mk_float with %a, %f\n", x, x); - register value *$alloc; - register value *$limit; - $limit = (*tinfo).limit; - $alloc = (*tinfo).alloc; - if (!(2LLU <= $limit - $alloc)) { - /*skip*/; - (*tinfo).nalloc = 2LLU; - garbage_collect(tinfo); - /*skip*/; - $alloc = (*tinfo).alloc; - $limit = (*tinfo).limit; - } - *($alloc + 0LLU) = Double_block; - *((double*) ($alloc + 1LLU)) = x; - (*tinfo).alloc = (*tinfo).alloc + 2LLU; - // trace ("mk_float return adress: %p\n", (void*)(((unsigned long long *) $alloc) + 1LLU)); - // trace ("mk_float return value: %f\n", Double_val ((double*)(((unsigned long long *) $alloc) + 1LLU))); - return (value) ((unsigned long long *) $alloc + 1LLU); -} - -#define FEq 1U -#define FLt 3U -#define FGt 5U -#define FNotComparable 7U - -primfloat_comparison prim_float_compare(primfloat x, primfloat y) { - double xv = Double_val(x); - double yv = Double_val(y); - trace ("Comparing floats: %f and %f\n", xv, yv); - if (x < y) return FLt; - else if (x > y) return FGt; - else if (x == y) return FEq; - else return FNotComparable; -} - -primbool prim_float_eqb(primfloat x, primfloat y) { - double xv = Double_val(x); - double yv = Double_val(y); - trace ("Comparing floats for equality: %f and %f\n", xv, yv); - return (mk_bool (xv == yv)); -} - -primbool prim_float_equal(primfloat x, primfloat y) { - double xv = Double_val(x); - double yv = Double_val(y); - trace ("Comparing floats for equality: %f and %f\n", xv, yv); - switch (fpclassify(xv)) - { case FP_NORMAL: - case FP_SUBNORMAL: - case FP_INFINITE: - printf("%i\n", xv == yv); - return (mk_bool (xv == yv)); - - case FP_NAN: - return (mk_bool (isnan (yv))); - - case FP_ZERO: - printf("%i\n", (xv == yv && ((1 / xv) == (1 / yv)))); - return (mk_bool (xv == yv && ((1 / xv) == (1 / yv)))); - - default: - exit (1); // Should not happen - } - // return (mk_bool (xv == yv)); -} - -primbool prim_float_ltb(primfloat x, primfloat y) { - double xv = Double_val(x); - double yv = Double_val(y); - trace ("prim_float_ltb %f and %f\n", xv, yv); - return (mk_bool (xv < yv)); -} - -primbool prim_float_leb(primfloat x, primfloat y) { - double xv = Double_val(x); - double yv = Double_val(y); - return (mk_bool (xv <= yv)); -} - -// let eshift = 2101 (* 2*emax + prec *) -unsigned long long eshift = 2101; - -primfloatintpair prim_float_frshiftexp(struct thread_info *tinfo, primfloat x) { - double xv = Double_val(x); - int e = 0; - value frac; - trace ("prim_float_frshiftexp %f\n", xv); - switch (fpclassify(xv)) - { - case FP_NAN: - case FP_INFINITE: - case FP_ZERO: - return (mk_pair(tinfo, x, Val_long(0))); - - case FP_NORMAL: - case FP_SUBNORMAL: - trace ("prim_float_frshiftexp frexp %f\n", frexp(xv, &e)); - frac = mk_float(tinfo, frexp(xv, &e)); - trace ("prim_float_frshiftexp result %f, %llu\n", Double_val(frac), (e + eshift)); - - return (mk_pair(tinfo, frac, Val_long(e + eshift))); - - default: - exit(1); // Should not happen - } -} - -primfloat prim_float_ldshiftexp(struct thread_info *tinfo, primfloat x, primint y) { - //todo fix - double xv = Double_val(x); - int e = 0; - value frac; - trace ("prim_float_ldshiftexp %f\n", xv); - switch (fpclassify(xv)) - { - case FP_NAN: - case FP_INFINITE: - case FP_ZERO: - return (mk_pair(tinfo, x, Val_long(0))); - - case FP_NORMAL: - case FP_SUBNORMAL: - frac = mk_float(tinfo, frexp(xv, &e)); - return (mk_pair(tinfo, frac, Val_long(e + eshift))); - - default: - exit(1); // Should not happen - } -} - -int prec = 53; - -primint prim_float_normfr_mantissa(primfloat x) { - double xv = Double_val(x); - double f = fabs(xv); - trace ("prim_float_normfr_mantissa %f, abs: %f, ldexp: %f, %llu\n", xv, f, ldexp(f, prec), - ((unsigned long long) ldexp(f, prec))); - if (f >= 0.5 && f < 1.0) - { return (Val_long ((unsigned long long) (ldexp(f, prec)))); } - else return (Val_long(0)); -} - -primfloat_class prim_float_classify(primfloat x) { - double xv = Double_val(x); - trace ("prim_float_classify %f\n", xv); - switch (fpclassify(xv)) - { - case FP_NAN: return ((8 << 1) + 1); - case FP_INFINITE: return (signbit(xv) ? (7 << 1) + 1 : (6 << 1) + 1); - case FP_ZERO: return (signbit(xv) ? (5 << 1) + 1 : (4 << 1) + 1); - case FP_SUBNORMAL: return (signbit(xv) ? (3 << 1) + 1 : (2 << 1) + 1); - case FP_NORMAL: return (signbit(xv) ? (1 << 1) + 1 : 1); - default: exit (1); // impossible - } -} - -primfloat prim_float_abs(struct thread_info *tinfo, primfloat x) { - double xv = Double_val(x); - trace ("prim_float_abs %f\n", xv); - return (mk_float (tinfo, fabs(xv))); -} - -primfloat prim_float_sqrt(struct thread_info *tinfo, primfloat x) { - double xv = Double_val(x); - trace ("prim_float_sqrt %f\n", xv); - return (mk_float (tinfo, sqrt(xv))); -} - -primfloat prim_float_opp(struct thread_info *tinfo, primfloat x) { - double xv = Double_val(x); - trace ("prim_float_opp %f\n", xv); - return (mk_float (tinfo, - xv)); -} - -primfloat prim_float_div(struct thread_info *tinfo, primfloat x, primfloat y) { - double xv = Double_val(x); - double yv = Double_val(y); - trace ("prim_float_div %f and %f\n", xv, yv); - return (mk_float (tinfo, xv / yv)); -} - -primfloat prim_float_mul(struct thread_info *tinfo, primfloat x, primfloat y) { - double xv = Double_val(x); - double yv = Double_val(y); - trace ("prim_float_mul %f and %f\n", xv, yv); - return (mk_float (tinfo, xv * yv)); -} - -primfloat prim_float_add(struct thread_info *tinfo, primfloat x, primfloat y) { - double xv = Double_val(x); - double yv = Double_val(y); - trace ("prim_float_add %f and %f\n", xv, yv); - return (mk_float (tinfo, xv + yv)); -} - -primfloat prim_float_sub(struct thread_info *tinfo, primfloat x, primfloat y) { - double xv = Double_val(x); - double yv = Double_val(y); - trace ("prim_float_sub %f and %f\n", xv, yv); - return (mk_float (tinfo, xv - yv)); -} - -primfloat prim_float_of_uint63(struct thread_info * tinfo, primint x) { - double xv = (double) (Long_val(x)); - trace ("prim_float_of_uint63 %f\n", xv); - return (mk_float (tinfo, xv)); -} - - -union double_bits { - double d; - uint64_t u; -}; - -static double next_up(double x) { - union double_bits bits; - trace ("prim_float_nextup %f\n", x); - - if (!(x < INFINITY)) return x; // x is +oo or NaN - bits.d = x; - int64_t i = bits.u; - if (i >= 0) ++bits.u; // x >= +0.0, go away from zero - else if (bits.u + bits.u == 0) bits.u = 1; // x is -0.0, should almost never happen - else --bits.u; // x < 0.0, go toward zero - return bits.d; -} - -static double next_down(double x) { - union double_bits bits; - trace ("prim_float_nextdown %f\n", x); - if (!(x > -INFINITY)) return x; // x is -oo or NaN - bits.d = x; - int64_t i = bits.u; - if (i == 0) bits.u = INT64_MIN + 1; // x is +0.0 - else if (i < 0) ++bits.u; // x <= -0.0, go away from zero - else --bits.u; // x > 0.0, go toward zero - return bits.d; -} - -primfloat prim_float_next_up(struct thread_info * ti, primfloat x) { - double xv = Double_val(x); - return (mk_float (ti, next_up(xv))); -} - -primfloat prim_float_next_down(struct thread_info * ti, primfloat x) { - double xv = Double_val(x); - return (mk_float (ti, next_down(xv))); -} diff --git a/cplugin/runtime/prim_int63.c b/cplugin/runtime/prim_int63.c deleted file mode 100644 index 7fec5e5bd..000000000 --- a/cplugin/runtime/prim_int63.c +++ /dev/null @@ -1,382 +0,0 @@ -#include -#include -#include "gc_stack.h" - -typedef value primint; -typedef value primbool; -typedef value primintcarry; -typedef value primintpair; - -#define trace(...) printf(__VA_ARGS__) - -#define maxuint63 0x7FFFFFFFFFFFFFFF - -primint prim_int63_add(primint x, primint y) -{ - // trace("Calling prim_int63_add\n"); - return (Val_long (Unsigned_long_val(x) + Unsigned_long_val(y))); -} - -primint prim_int63_sub(primint x, primint y) -{ - unsigned long long xr = Unsigned_long_val(x); - unsigned long long yr = Unsigned_long_val(y); - trace("Calling prim_int63_sub on %llu and %llu: %llu\n", xr, yr, xr - yr); - return (Val_long (xr - yr)); -} - -primint prim_int63_mul(primint x, primint y) -{ - trace("Calling prim_int63_mul\n"); - return (Val_long (Unsigned_long_val(x) * Unsigned_long_val(y))); -} - -primint prim_int63_mod(primint x, primint y) -{ - trace("Calling prim_int63_mod\n"); - return (Val_long (Unsigned_long_val(x) % Unsigned_long_val(y))); -} - -primint prim_int63_div(primint x, primint y) -{ - trace("Calling prim_int63_div\n"); - return (Val_long (Unsigned_long_val(x) / Unsigned_long_val(y))); -} - -primint prim_int63_land(primint x, primint y) -{ - unsigned long long xr = Unsigned_long_val(x); - unsigned long long yr = Unsigned_long_val(y); - trace("Calling prim_int63_land on %llu (%p) and %llu (%p): %llu, %llu \n", xr, (void*)x, yr, (void*)y, xr & yr, (unsigned long long) (x & y)); - return (Val_long (xr & yr)); -} -primint prim_int63_lsl(primint x, primint y) -{ - unsigned long long xr = Unsigned_long_val(x); - unsigned long long yr = Unsigned_long_val(y); - trace("Calling prim_int63_lsl on %llu and %llu: %llu \n", xr, yr, xr << yr); - return (Val_long ((xr << yr))); -} - -primint prim_int63_lsr(primint x, primint y) -{ - unsigned long long xr = Unsigned_long_val(x); - unsigned long long yr = Unsigned_long_val(y); - trace("Calling prim_int63_lsr on %llu and %llu: %llu \n", xr, yr, xr >> yr); - return (Val_long (xr >> yr)); -} - -primint prim_int63_lor(primint x, primint y) -{ - trace("Calling prim_int63_lor\n"); - return (Val_long (Unsigned_long_val(x) | Unsigned_long_val(y))); -} -primint prim_int63_lxor(primint x, primint y) -{ - trace("Calling prim_int63_lxor\n"); - return (Val_long (Unsigned_long_val(x) ^ Unsigned_long_val(y))); -} - -primint prim_int63_head0(primint init) -{ - unsigned long long r = 0; - unsigned long long x = Unsigned_long_val (init); - if ((x & 0x7FFFFFFF00000000) == 0) { r = r + 31; } - else { x = x >> 31; } - if ((x & 0xFFFF0000) == 0) { x = (x << 16) & maxuint63; r = r + 16; }; - if ((x & 0xFF000000) == 0) { x = (x << 8) & maxuint63; r = r + 8; }; - if ((x & 0xF0000000) == 0) { x = (x << 4) & maxuint63; r = r + 4; }; - if ((x & 0xC0000000) == 0) { x = (x << 2) & maxuint63; r = r + 2; }; - if ((x & 0x80000000) == 0) { x = (x << 1) & maxuint63; r = r + 1; }; - if ((x & 0x80000000) == 0) { r = r + 1; }; - trace("Calling prim_int63_head0 on %llu: %llu\n", x, r); - return Val_long(r); -} - -primint prim_int63_tail0(primint init) -{ - trace("Calling prim_int63_tail0\n"); - unsigned long long r = 0; - unsigned long long x = Unsigned_long_val (init); - if ((x & 0xFFFFFFFF) == 0) { x = x >> 32; r = r + 32; }; - if ((x & 0xFFFF) == 0) { x = x >> 16; r = r + 16; }; - if ((x & 0xFF) == 0) { x = x >> 8; r = r + 8; }; - if ((x & 0xF) == 0) { x = x >> 4; r = r + 4; }; - if ((x & 0x3) == 0) { x = x >> 2; r = r + 2; }; - if ((x & 0x1) == 0) { r = r + 1; }; - return Val_long(r); -} - -primbool mk_bool(int b) -{ - if (b) return 1; - else return 3; -} - -primbool prim_int63_eqb(primint x, primint y) -{ - unsigned long long xr = Unsigned_long_val(x); - unsigned long long yr = Unsigned_long_val(y); - trace("Calling prim_int63_eqb on %llu and %llu: %i, %i \n", xr, yr, xr == yr, x == y); - return (mk_bool (xr == yr)); -} -primbool prim_int63_leb(primint x, primint y) -{ - trace("Calling prim_int63_leb\n"); - return (mk_bool (x <= y)); -} -primbool prim_int63_ltb(primint x, primint y) -{ - trace("Calling prim_int63_ltb\n"); - return (mk_bool (x < y)); -} - -value prim_int63_compare(primint x, primint y) -{ - register signed long long xr = Unsigned_long_val(x); - register signed long long yr = Unsigned_long_val(y); - register signed long long result = xr - yr; - trace("Calling prim_int63_compare\n"); - trace("Calling prim_int63_compare on %llu and %llu: %lli \n", xr, yr, result); - if (result == 0) return 1; - else if (result < 0) return 3; - else return 5; -} - -unsigned long long prim_int63_make_Coq_Numbers_Cyclic_Abstract_CarryType_carry_C0(unsigned long long $arg0, unsigned long long *$argv) -{ - *((unsigned long long *) $argv + 0LLU) = 1024LLU; - *((unsigned long long *) $argv + 1LLU) = $arg0; - return ((unsigned long long) $argv) + 1LLU; -} - -value prim_int63_alloc_make_Coq_Numbers_Cyclic_Abstract_CarryType_carry_C0(struct thread_info *$tinfo, unsigned long long $arg0) -{ - // trace("Calling mkC0 with %llu (%p)\n", Unsigned_long_val($arg0), (void*)$arg0); - register value *$alloc; - register value *$limit; - $limit = (*$tinfo).limit; - $alloc = (*$tinfo).alloc; - if (!(2LLU <= $limit - $alloc)) { - /*skip*/; - (*$tinfo).nalloc = 2LLU; - garbage_collect($tinfo); - /*skip*/; - $alloc = (*$tinfo).alloc; - $limit = (*$tinfo).limit; - } - *($alloc + 0LLU) = 1024LLU; - *($alloc + 1LLU) = $arg0; - (*$tinfo).alloc = (*$tinfo).alloc + 2LLU; - // trace ("addc returns adress: %p", (void*)(((unsigned long long *) $alloc) + 1LLU)); - return (value) ((unsigned long long *) $alloc + 1LLU); -} - -value prim_int63_make_Coq_Numbers_Cyclic_Abstract_CarryType_carry_C1(unsigned long long $arg0, unsigned long long *$argv) -{ - *((unsigned long long *) $argv + 0LLU) = 1025LLU; - *((unsigned long long *) $argv + 1LLU) = $arg0; - return ((unsigned long long) $argv) + 1LLU; -} - -value prim_int63_alloc_make_Coq_Numbers_Cyclic_Abstract_CarryType_carry_C1(struct thread_info *$tinfo, unsigned long long $arg0) -{ - // trace("Calling mkC1\n"); - register value *$alloc; - register value *$limit; - $limit = (*$tinfo).limit; - $alloc = (*$tinfo).alloc; - if (!(2LLU <= $limit - $alloc)) { - (*$tinfo).nalloc = 2LLU; - garbage_collect($tinfo); - $alloc = (*$tinfo).alloc; - $limit = (*$tinfo).limit; - } - *($alloc + 0LLU) = 1025LLU; - *($alloc + 1LLU) = $arg0; - (*$tinfo).alloc = (*$tinfo).alloc + 2LLU; - return (value) ($alloc + 1LLU); -} - -primintcarry mk_C0(struct thread_info *ti, primint x) -{ - return prim_int63_alloc_make_Coq_Numbers_Cyclic_Abstract_CarryType_carry_C0(ti, x); -} - -primintcarry mk_C1(struct thread_info *ti, primint x) -{ - return prim_int63_alloc_make_Coq_Numbers_Cyclic_Abstract_CarryType_carry_C1(ti, x); -} - -value prim_int63_make_Coq_Init_Datatypes_prod_pair(unsigned long long $arg0, unsigned long long $arg1, value *$argv) -{ - *($argv + 0LLU) = 2048LLU; - *($argv + 1LLU) = $arg0; - *($argv + 2LLU) = $arg1; - return (value) ($argv + 1LLU); -} - -value prim_int63_alloc_make_Coq_Init_Datatypes_prod_pair(struct thread_info *$tinfo, unsigned long long $arg0, unsigned long long $arg1) -{ - register value *$argv; - $argv = (*$tinfo).alloc; - *($argv + 0LLU) = 2048LLU; - *($argv + 1LLU) = $arg0; - *($argv + 2LLU) = $arg1; - (*$tinfo).alloc = (*$tinfo).alloc + 3LLU; - return (value) ($argv + 1LLU); -} - -primintpair mk_pair(struct thread_info *ti, primint x, primint y) -{ - // trace("Calling prim_int63_mk_pair on %lu and %lu\n", Unsigned_long_val(x), Unsigned_long_val(y)); - return prim_int63_alloc_make_Coq_Init_Datatypes_prod_pair(ti, x, y); -} - -primintcarry prim_int63_addc(struct thread_info *ti, primint x, primint y) -{ - unsigned long long xr = Unsigned_long_val(x); - unsigned long long yr = Unsigned_long_val(y); - trace("Calling prim_int63_addc on %llu and %llu\n", xr, yr); - register unsigned long long r = xr + yr; - trace("Result: %llu\n", r); - if (r < xr) { return mk_C1(ti, Val_long (r)); } - else { return mk_C0(ti, Val_long (r)); } -} - -primintcarry prim_int63_addcarryc(struct thread_info *ti, primint x, primint y) -{ - trace("Calling prim_int63_addcarryc\n"); - register primint r = (Unsigned_long_val(x) + Unsigned_long_val(y) + 1); - if (r <= x) { return mk_C1(ti, Val_long(r)); } - else { return mk_C0(ti, Val_long(r)); } -} - -primintcarry prim_int63_subc(struct thread_info *ti, primint x, primint y) -{ - unsigned long long xr = Unsigned_long_val(x); - unsigned long long yr = Unsigned_long_val(y); - register unsigned long long r = xr - yr; - trace("Calling prim_int63_subc on %llu and %llu: %llu\n", xr, yr, r); - if (y <= x) { return mk_C0(ti, Val_long(r)); } - else { return mk_C1(ti, Val_long(r)); } -} - -primintcarry prim_int63_subcarryc(struct thread_info *ti, primint x, primint y) -{ - trace("Calling prim_int63_subccarryc\n"); - register primint r = (Unsigned_long_val(x) - Unsigned_long_val(y) - 1); - if (y < x) { return mk_C0(ti, Val_long(r)); } - else { return mk_C1(ti, Val_long(r)); } -} - -#define maxuint31 0x7FFFFFFF - -// precondiition : (x lsr 62 = 0 || y lsr 62 = 0) -primintpair mulc_aux(struct thread_info *ti, unsigned long long x, unsigned long long y) { - unsigned long lx = x & maxuint31; - unsigned long ly = y & maxuint31; - unsigned long hx = x >> 31; - unsigned long hy = y >> 31; - // trace("Multiplication mulc_aux lx = %lu, ly = %lu, hx = %lu, hy = %lu)\n", lx, ly, hx, hy); - // hx and hy are 32 bits value but at most one is 32 - unsigned long long hxy = hx * hy; // 63 bits - unsigned long long hxly = hx * ly; // 63 bits - unsigned long long lxhy = lx * hy; // 63 bits - unsigned long long lxy = lx * ly; // 62 bits - unsigned long long l = lxy | (hxy << 62); // 63 bits - unsigned long long h = hxy >> 1; // 62 bits - unsigned long long hl = hxly + lxhy; // We can have a carry - if (hl < hxly) h = h + (1ULL << 31); - unsigned long long hl2 = (hl << 31) & maxuint63; - l = l + hl2; - if (l < hl2) h = h + 1; - h = h + (hl >> 32); - trace("Multiplication mulc_aux gives: (%llu, %llu)\n", h, l); - return mk_pair (ti, Val_long(h),Val_long(l)); -} - -primintpair prim_int63_mulc (struct thread_info *ti, primint xp, primint yp) { - unsigned long long x = Unsigned_long_val(xp); - unsigned long long y = Unsigned_long_val(yp); - trace("Calling prim_int63_mulc on %llu (%p) and %llu (%p)\n", x, (void*)xp, y, (void*)yp); - if (x >> 62 == 0 || y >> 62 == 0) - return (mulc_aux(ti, x, y)); - else { - unsigned long long yl = y ^ (1ULL << 62); - value p = mulc_aux(ti,x,yl); - unsigned long long h = Unsigned_long_val(((unsigned long long*) p + 0)); - unsigned long long l = Unsigned_long_val(((unsigned long long*) p + 1)); - /* h << 63 + l = x * yl - x * y = x * (1 << 62 + yl) = - x << 62 + x*yl = x << 62 + h << 63 + l */ - unsigned long long l2 = l + (x << 62); - if (l2 < l) h = h + 1; - h = h + (x >> 1); - trace("Multiplication gives: (%llu, %llu)\n", h, l2); - return (mk_pair (ti, Val_long(h), Val_long(l2))); - } -} - -/* [div21 xh xl y] returns [q % 2^63, r] - s.t. [xh * 2^63 + xl = q * y + r] and [r < y]. - When [y] is [0], returns [0, 0]. */ - -/* division of two numbers by one - precondition: xh < y *) - outputs: q, r s.t. x = q * y + r, r < y */ - -primintpair prim_int63_diveucl_21_long(struct thread_info *ti, unsigned long long xh, unsigned long long xl, - unsigned long long y) -{ - trace("Calling prim_int63_diveucl_21 with %llu, %llu and %llu\n", xh, xl, y); - /* nh might temporarily grow as large as 2*y - 1 in the loop body, - so we store it as a 64-bit unsigned integer */ - unsigned long long nh = xh & maxuint63; - unsigned long long nl = xl & maxuint63; - unsigned long long q = 0; - unsigned int i = 0; - if (((nh & (1LLU << 63)) != 0)) trace("msb is set\n"); - for (i = 0; i < 63; i++) { - /* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^63, - (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl */ - nh = (nh << 1) | (nl >> 62); - nl = (nl << 1) & maxuint63; - q = q << 1; - if (nh >= y) { q = q | 1LLU; nh = nh - y; } - } - trace("Result: %llu, %llu\n", q, nh & 18446744073709551615ULL); - return mk_pair(ti, Val_long(q), Val_long(nh & 18446744073709551615ULL)); -} - -primintpair prim_int63_diveucl_21(struct thread_info *ti, primint xh, primint xl, primint y) { - unsigned long long xhl = Unsigned_long_val(xh); - unsigned long long xll = Unsigned_long_val(xl); - unsigned long long yl = Unsigned_long_val(y); - if (yl <= xhl) return mk_pair (ti, Val_long(0), Val_long(0)); - else - return prim_int63_diveucl_21_long(ti, xhl, xll, yl); -} - -primintpair prim_int63_diveucl(struct thread_info *ti, primint xp, primint yp) -{ - unsigned long long x = Unsigned_long_val(xp); - unsigned long long y = Unsigned_long_val(yp); - trace("Calling prim_int63_diveucl\n"); - if (y == 0) return (mk_pair (ti, Val_long(0), Val_long(0))); - else - return (mk_pair (ti, Val_long(x / y), Val_long(x % y))); -} - -#define uint_size 63 - -primint prim_int63_addmuldiv(primint pp, primint xp, primint yp) -{ - trace("Calling prim_int63_addmuldiv\n"); - unsigned long long p = Unsigned_long_val(pp); - unsigned long long x = Unsigned_long_val(xp); - unsigned long long y = Unsigned_long_val(yp); - unsigned long long r = ((x << p) & maxuint63) | y >> (uint_size - p); - trace("Calling addmuldiv with %llu, %llu and %llu: %llu\n", p, x, y, r); - return Val_long(r); -} diff --git a/cplugin/static/caml_bool.ml b/cplugin/static/caml_bool.ml deleted file mode 100644 index c7ac2892d..000000000 --- a/cplugin/static/caml_bool.ml +++ /dev/null @@ -1,8 +0,0 @@ - -let of_coq = function - | Datatypes.Coq_true -> true - | Datatypes.Coq_false -> false - -let to_coq = function - | true -> Datatypes.Coq_true - | false -> Datatypes.Coq_false \ No newline at end of file diff --git a/cplugin/static/caml_bool.mli b/cplugin/static/caml_bool.mli deleted file mode 100644 index 101e26819..000000000 --- a/cplugin/static/caml_bool.mli +++ /dev/null @@ -1,2 +0,0 @@ -val of_coq : Datatypes.bool -> bool -val to_coq : bool -> Datatypes.bool diff --git a/cplugin/static/printCsyntax.ml b/cplugin/static/printCsyntax.ml index 236a881c5..50045d52c 100644 --- a/cplugin/static/printCsyntax.ml +++ b/cplugin/static/printCsyntax.ml @@ -72,7 +72,7 @@ let name_longtype sg = let attributes a = let open Datatypes in - let s1 = if Caml_bool.of_coq a.attr_volatile then " volatile" else "" in + let s1 = if a.attr_volatile then " volatile" else "" in match a.attr_alignas with | None -> s1 | Some l -> @@ -134,7 +134,7 @@ let rec name_cdecl id ty = if not first then Buffer.add_string b ", "; Buffer.add_string b (name_cdecl "" t1); add_args false tl in - if not (Caml_bool.of_coq cconv.cc_unproto) then add_args true args; + if not cconv.cc_unproto then add_args true args; Buffer.add_char b ')'; name_cdecl (Buffer.contents b) res | Tstruct(name, a) -> @@ -515,7 +515,7 @@ let re_string_literal = Str.regexp "__stringlit_[0-9]+" let print_globvar p id v = let name1 = extern_atom id in - let name2 = if Caml_bool.of_coq v.gvar_readonly then "const " ^ name1 else name1 in + let name2 = if v.gvar_readonly then "const " ^ name1 else name1 in match v.gvar_init with | [] -> fprintf p "extern %s;@ @ " @@ -540,7 +540,7 @@ let print_globvar p id v = let print_globvardecl p id v = let name = extern_atom id in - let name = if Caml_bool.of_coq v.gvar_readonly then "const "^name else name in + let name = if v.gvar_readonly then "const "^name else name in let linkage = "extern" in fprintf p "%s %s;@ @ " linkage (name_cdecl name v.gvar_info) diff --git a/plugin/CertiCoq.v b/plugin/CertiCoq.v index 70eddd518..ca9fefeb7 100644 --- a/plugin/CertiCoq.v +++ b/plugin/CertiCoq.v @@ -1,2 +1,2 @@ -From CertiCoq.Plugin Require Import Loader. +From CertiCoq.Plugin Require Export Loader. From CertiCoq.Plugin Require Export CoqMsgFFI PrimInt63 PrimFloats. \ No newline at end of file diff --git a/plugin/Loader.v b/plugin/Loader.v index c28f43c6f..e40713540 100644 --- a/plugin/Loader.v +++ b/plugin/Loader.v @@ -1,2 +1,4 @@ Set Debug "backtrace". -Declare ML Module "coq-certicoq.plugin". \ No newline at end of file +Declare ML Module "coq-certicoq.plugin". + +CertiCoq Extract Inductives [ bool => "bool" [ 1 0 ] ]. \ No newline at end of file diff --git a/plugin/Makefile.local b/plugin/Makefile.local index c7d05f3d8..9ab1b9fd3 100644 --- a/plugin/Makefile.local +++ b/plugin/Makefile.local @@ -15,10 +15,4 @@ merlin-hook:: $(HIDE)echo 'PKG coq-metacoq-template-ocaml.plugin' >> .merlin $(HIDE)echo 'PKG stdlib-shims' >> .merlin -get_ordinal.o: get_ordinal.c - $(CC) -c -o $@ -I runtime $< - -certicoq_vanilla_plugin.cmxs: get_ordinal.o - -install-extra:: - make -C runtime install \ No newline at end of file +certicoq_vanilla_plugin.cmxs: ../runtime/get_ordinal.o diff --git a/plugin/Makefile.local-late b/plugin/Makefile.local-late index 253507c58..02baa1b3d 100644 --- a/plugin/Makefile.local-late +++ b/plugin/Makefile.local-late @@ -1,4 +1,2 @@ -# CAMLOPTLINK = "$(OCAMLFIND)" opt -linkall get_ordinal.o - -certicoq_plugin.cmxa: certicoq_plugin.cmx get_ordinal.o - $(HIDE)$(TIMER) $(CAMLOPTLINK) get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< +certicoq_plugin.cmxa: certicoq_plugin.cmx ../runtime/get_ordinal.o + $(HIDE)$(TIMER) $(CAMLOPTLINK) ../runtime/get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index 5a700f29b..998791685 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -109,6 +109,31 @@ let register (prims : prim list) (imports : import list) : unit = let get_global_prims () = fst !global_registers let get_global_includes () = snd !global_registers +(* Extract Inductive *) +type inductive_mapping = Kernames.inductive * (string * int list) (* Target inductive type and mapping of constructor names to constructor tags *) +type inductives_mapping = inductive_mapping list + +let global_inductive_registers = + Summary.ref ([] : inductives_mapping) ~name:"CertiCoq Extract Inductive Registration" + +let global_inductive_registers_name = "certicoq-extract-inductive-registration" + +let cache_inductive_registers inds = + let inds' = !global_inductive_registers in + global_inductive_registers := inds @ inds' + +let global_inductive_registers_input = + let open Libobject in + declare_object + (global_object_nodischarge global_inductive_registers_name + ~cache:(fun r -> cache_inductive_registers r) + ~subst:None) + +let register_inductives (inds : inductives_mapping) : unit = + Lib.add_leaf (global_inductive_registers_input inds) + +let get_global_inductives_mapping () = !global_inductive_registers + (* Support for dynamically-linked certicoq-compiled programs *) type certicoq_run_function = unit -> Obj.t @@ -173,7 +198,6 @@ let _ = Callback.register "coq_user_error" coq_user_error type command_args = | TYPED_ERASURE - | FAST_ERASURE | UNSAFE_ERASURE | BYPASS_QED | CPS @@ -192,7 +216,6 @@ type command_args = type options = { typed_erasure : bool; - fast_erasure : bool; unsafe_erasure : bool; bypass_qed : bool; cps : bool; @@ -209,6 +232,7 @@ type options = prefix : string; toplevel_name : string; prims : ((Kernames.kername * Kernames.ident) * bool) list; + inductives_mapping : inductives_mapping; } let check_build_dir d = @@ -224,7 +248,6 @@ let check_build_dir d = let default_options () : options = { typed_erasure = false; - fast_erasure = false; unsafe_erasure = false; bypass_qed = false; cps = false; @@ -241,6 +264,7 @@ let default_options () : options = prefix = ""; toplevel_name = "body"; prims = []; + inductives_mapping = get_global_inductives_mapping (); } let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ident) * bool) list) (fname : string) : options = @@ -248,7 +272,6 @@ let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ide match l with | [] -> o | TYPED_ERASURE :: xs -> aux {o with typed_erasure = true} xs - | FAST_ERASURE :: xs -> aux {o with fast_erasure = true} xs | UNSAFE_ERASURE :: xs -> aux {o with unsafe_erasure = true} xs | BYPASS_QED :: xs -> aux {o with bypass_qed = true} xs | CPS :: xs -> aux {o with cps = true} xs @@ -274,7 +297,6 @@ let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ide let make_unsafe_passes b = let open Erasure0 in { cofix_to_lazy = b; - reorder_constructors = b; inlining = b; unboxing = b; betared = b } @@ -282,14 +304,15 @@ let make_unsafe_passes b = let all_unsafe_passes = make_unsafe_passes true let no_unsafe_passes = make_unsafe_passes false +let quote_inductives_mapping l = + List.map (fun (hd, (na, cstrs)) -> (hd, (bytestring_of_string na, List.map (fun i -> coq_nat_of_int i) cstrs))) l + let make_pipeline_options (opts : options) = let erasure_config = Erasure0.({ enable_typed_erasure = opts.typed_erasure; enable_unsafe = if opts.unsafe_erasure then all_unsafe_passes else no_unsafe_passes; - enable_fast_remove_params = opts.fast_erasure; dearging_config = default_dearging_config; - inductives_mapping = []; inlined_constants = Kernames.KernameSet.empty }) in @@ -304,8 +327,9 @@ let make_pipeline_options (opts : options) = let prefix = bytestring_of_string opts.prefix in let toplevel_name = bytestring_of_string opts.toplevel_name in let prims = get_global_prims () @ opts.prims in + let inductives_mapping = quote_inductives_mapping opts.inductives_mapping in (* Feedback.msg_debug Pp.(str"Prims: " ++ prlist_with_sep spc (fun ((x, y), wt) -> str (string_of_bytestring y)) prims); *) - Pipeline.make_opts erasure_config cps args anfc olevel timing timing_anf debug dev prefix toplevel_name prims + Pipeline.make_opts erasure_config inductives_mapping cps args anfc olevel timing timing_anf debug dev prefix toplevel_name prims (** Main Compilation Functions *) @@ -659,8 +683,28 @@ module CompileFunctor (CI : CompilerInterface) = struct let time = Unix.gettimeofday () -. start in Feedback.msg_notice Pp.(msg ++ str (Printf.sprintf " executed in %f sec" time)); res - - let reify env sigma ty v : Constr.t = + + let apply_reordering hd m cstrs = + try + let find_ind_ord (ind, (na, tags)) = + if Kernames.eq_inductive_def ind hd then + Some (Array.of_list (List.map (fun i -> cstrs.(i)) tags)) + else None + in + CList.find_map_exn find_ind_ord m + with Not_found -> cstrs + + let find_reverse_mapping hd m cstr = + try + let find_ind_ord (ind, (na, tags)) = + if Kernames.eq_inductive_def ind hd then + Some (CList.index0 Int.equal cstr tags) + else None + in + CList.find_map_exn find_ind_ord m + with Not_found -> cstr + + let reify im env sigma ty v : Constr.t = let open Declarations in let debug s = debug_reify Pp.(fun () -> str s) in let rec aux ty v = @@ -670,11 +714,13 @@ module CompileFunctor (CI : CompilerInterface) = struct | IsInductive (hd, u, args) -> let open Inductive in let open Inductiveops in + let qhd = match Metacoq_template_plugin.Ast_quoter.quote_global_reference (IndRef hd) with Metacoq_template_plugin.Kernames.IndRef i -> (Obj.magic i : Kernames.inductive) | _ -> assert false in let spec = lookup_mind_specif env hd in let npars = inductive_params spec in let params, _indices = CList.chop npars args in let indfam = make_ind_family ((hd, u), params) in let cstrs = get_constructors env indfam in + let cstrs = apply_reordering qhd im cstrs in if Obj.is_block v then let ord = get_boxed_ordinal v in let () = debug (Printf.sprintf "Reifying constructor block of tag %i" ord) in @@ -683,6 +729,7 @@ module CompileFunctor (CI : CompilerInterface) = struct with Not_found -> ill_formed env sigma ty in let cstr = cstrs.(coqidx) in + let coqidx = find_reverse_mapping qhd im coqidx in let ctx = Vars.smash_rel_context cstr.cs_args in let vargs = List.init (List.length ctx) (Obj.field v) in let args' = List.map2 (fun decl v -> @@ -697,6 +744,7 @@ module CompileFunctor (CI : CompilerInterface) = struct try find_nth_constant ord cstrs with Not_found -> ill_formed env sigma ty in + let coqidx = find_reverse_mapping qhd im coqidx in let () = debug (Printf.sprintf "Reifying constant constructor: %i is %i in Coq" ord coqidx) in Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) params | IsPrimitive (c, u, _args) -> @@ -710,8 +758,8 @@ module CompileFunctor (CI : CompilerInterface) = struct in aux ty v let reify opts env sigma tyinfo result = - if opts.time then time ~msg:(Pp.str "Reification") (fun () -> reify env sigma tyinfo result) - else reify env sigma tyinfo result + if opts.time then time ~msg:(Pp.str "Reification") (fun () -> reify opts.inductives_mapping env sigma tyinfo result) + else reify opts.inductives_mapping env sigma tyinfo result let template name = Printf.sprintf "\nvalue %s ()\n { struct thread_info* tinfo = make_tinfo(); return %s_body(tinfo); }\n" name name diff --git a/plugin/certicoq.mli b/plugin/certicoq.mli index f0115298d..3085364bb 100644 --- a/plugin/certicoq.mli +++ b/plugin/certicoq.mli @@ -2,7 +2,6 @@ open Plugin_utils type command_args = | TYPED_ERASURE - | FAST_ERASURE | UNSAFE_ERASURE | BYPASS_QED | CPS @@ -19,9 +18,13 @@ type command_args = | TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *) | FILENAME of string (* Name of the generated file *) +type inductive_mapping = Kernames.inductive * (string * int list) (* Target inductive type and mapping of constructor names to constructor tags *) +type inductives_mapping = inductive_mapping list +type prim = ((Kernames.kername * Kernames.ident) * bool) + + type options = { typed_erasure : bool; - fast_erasure : bool; unsafe_erasure : bool; bypass_qed : bool; cps : bool; @@ -37,19 +40,29 @@ type options = dev : int; prefix : string; toplevel_name : string; - prims : ((Kernames.kername * Kernames.ident) * bool) list; + prims : prim list; + inductives_mapping : inductives_mapping; } -type prim = ((Kernames.kername * Kernames.ident) * bool) - val default_options : unit -> options val make_options : command_args list -> prim list -> string -> options (* Register primitive operations and associated include file *) val register : prim list -> import list -> unit +val register_inductives : inductives_mapping -> unit + val get_name : Names.GlobRef.t -> string +(* Support for running dynamically linked certicoq-compiled programs *) +type certicoq_run_function = unit -> Obj.t + +(* [register_certicoq_run global_id fresh_name function]. A same global_id + can be compiled multiple times with different definitions, fresh_name indicates + the version used this time *) +val register_certicoq_run : string -> string -> certicoq_run_function -> unit +val run_certicoq_run : string -> certicoq_run_function + module type CompilerInterface = sig type name_env val compile : Pipeline_utils.coq_Options -> Ast0.Env.program -> ((name_env * Clight.program) * Clight.program) CompM.error * Bytestring.String.t @@ -59,8 +72,7 @@ module type CompilerInterface = sig (((name_env * Clight.program) * Clight.program) * Bytestring.String.t list) CompM.error val generate_ffi : - Pipeline_utils.coq_Options -> Ast0.Env.program -> (((name_env * Clight.program) * Clight.program) * Bytestring.String.t list) CompM.error - + Pipeline_utils.coq_Options -> Ast0.Env.program -> (((name_env * Clight.program) * Clight.program) * Bytestring.String.t list) CompM.error end module CompileFunctor (CI : CompilerInterface) : sig @@ -70,22 +82,15 @@ module CompileFunctor (CI : CompilerInterface) : sig val show_ir : options -> Names.GlobRef.t -> unit val ffi_command : options -> Names.GlobRef.t -> unit val glue_command : options -> Names.GlobRef.t list -> unit + val eval_gr : options -> Names.GlobRef.t -> import list -> Constr.t + val eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t end val compile_only : options -> Names.GlobRef.t -> import list -> unit val generate_glue_only : options -> Names.GlobRef.t -> unit val compile_C : options -> Names.GlobRef.t -> import list -> unit -val eval_gr : options -> Names.GlobRef.t -> import list -> Constr.t val show_ir : options -> Names.GlobRef.t -> unit val ffi_command : options -> Names.GlobRef.t -> unit val glue_command : options -> Names.GlobRef.t list -> unit -val eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t - -(* Support for running dynamically linked certicoq-compiled programs *) -type certicoq_run_function = unit -> Obj.t - -(* [register_certicoq_run global_id fresh_name function]. A same global_id - can be compiled multiple times with different definitions, fresh_name indicates - the version used this time *) -val register_certicoq_run : string -> string -> certicoq_run_function -> unit -val run_certicoq_run : string -> certicoq_run_function +val eval_gr : options -> Names.GlobRef.t -> import list -> Constr.t +val eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t \ No newline at end of file diff --git a/plugin/g_certicoq.mlg b/plugin/g_certicoq.mlg index 5fbea6c3d..b59a2d4eb 100644 --- a/plugin/g_certicoq.mlg +++ b/plugin/g_certicoq.mlg @@ -40,11 +40,26 @@ let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = let to_ltac_val c = Tacinterp.Value.of_constr c +let globref_of_qualid ?loc (gr : Libnames.qualid) : Names.GlobRef.t = + match Constrintern.locate_reference gr with + | None -> CErrors.user_err ?loc Pp.(Libnames.pr_qualid gr ++ str " not found.") + | Some g -> g + +let quoted_globref_of_qualid ~loc (gr : Libnames.qualid) : Metacoq_template_plugin.Kernames.global_reference = + Metacoq_template_plugin.Ast_quoter.quote_global_reference (globref_of_qualid ~loc gr) + +let inductive_of_qualid ~loc (gr : Libnames.qualid) : Kernames.inductive = + let open Metacoq_template_plugin in + match quoted_globref_of_qualid ~loc gr with + | Kernames.ConstRef kn -> CErrors.user_err ~loc Pp.(str "Expected an inductive name but found a constant.") + | Kernames.VarRef(v) -> CErrors.user_err ~loc Pp.(str "Expected an inductive name but found a variable.") + | Kernames.IndRef(i) -> (Obj.magic i) + | Kernames.ConstructRef(_, _) -> CErrors.user_err ~loc Pp.(str "Expected an inductive name but found a constructor.") + } ARGUMENT EXTEND cargs | [ "-typed-erasure" ] -> { TYPED_ERASURE } -| [ "-fast-erasure" ] -> { FAST_ERASURE } | [ "-unsafe-erasure" ] -> { UNSAFE_ERASURE } | [ "-bypass_qed" ] -> { BYPASS_QED } | [ "-cps" ] -> { CPS } @@ -90,10 +105,18 @@ VERNAC ARGUMENT EXTEND cinclude | [ "Absolute" string(str) ] -> { FromAbsolutePath str } END +VERNAC ARGUMENT EXTEND certiCoq_Register_extract_inductive +| [ reference(gr) "=>" string(ty) "[" natural_list(cstrs) "]" ] -> + { ((inductive_of_qualid ~loc gr), (ty, cstrs)) } +END + VERNAC COMMAND EXTEND CertiCoq_Register CLASSIFIED AS SIDEFF | [ "CertiCoq" "Register" "[" extract_cnst_list_sep(l, ",") "]" "Include" "[" cinclude_list_sep(imps, ",") "]" ] -> { Certicoq.register l imps } +| [ "CertiCoq" "Extract" "Inductives" "[" certiCoq_Register_extract_inductive_list_sep(inds, ",") "]" ] -> { + Certicoq.register_inductives inds +} END VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY diff --git a/plugin/plugin_utils.ml b/plugin/plugin_utils.ml index 067234fcc..b80d97cd7 100644 --- a/plugin/plugin_utils.ml +++ b/plugin/plugin_utils.ml @@ -71,7 +71,6 @@ Valid options:\n\ -time_anf : Time λanf optimizations\n\ -unsafe-erasure : Allow to use unsafe passes in the MetaCoq Erasure pipeline. This currently includes the cofixpoint-to-fixpoint translation.\n\ -typed-erasure : Uses the typed erasure and de-arging phase of the MetaCoq Erasure pipeline.\n\ --fast-erasure : Uses an alternative function to remove parameters of constructors in the MetaCoq Erasure pipeline.\n\ \n\n\ To compile Gallina constants to specific C functions use:\n\ CertiCoq Compile Extract Constants [ constant1 => \"c_function1\", ... , constantN => \"c_functionN\" ] Include [ \"file1.h\" , Library \"runtime_header.h\", ... , Absolute \"fileM.h\" ].\n\ diff --git a/plugin/runtime/certicoq_run_main.h b/plugin/runtime/certicoq_run_main.h deleted file mode 100644 index 4b085bb79..000000000 --- a/plugin/runtime/certicoq_run_main.h +++ /dev/null @@ -1,3 +0,0 @@ - - -extern int main (int, char**) \ No newline at end of file diff --git a/plugin/runtime/config.h b/plugin/runtime/config.h deleted file mode 100644 index 4dc007181..000000000 --- a/plugin/runtime/config.h +++ /dev/null @@ -1,148 +0,0 @@ -/**************************************************************************/ -/* */ -/* OCaml */ -/* */ -/* Xavier Leroy and Damien Doligez, INRIA Rocquencourt */ -/* */ -/* Copyright 1996 Institut National de Recherche en Informatique et */ -/* en Automatique. */ -/* */ -/* All rights reserved. This file is distributed under the terms of */ -/* the GNU Lesser General Public License version 2.1, with the */ -/* special exception on linking described in the file LICENSE. */ -/* */ -/**************************************************************************/ - -#ifndef CONFIG_H -#define CONFIG_H - -#include "m.h" - -#if SIZEOF_PTR > 0 -#else -#error "Oops! SIZEOF_PTR is not defined" -#endif - -#if SIZEOF_PTR == SIZEOF_LONG -/* Standard models: ILP32 or I32LP64 */ -typedef long intnat; -typedef unsigned long uintnat; -#define ARCH_INTNAT_PRINTF_FORMAT "l" -#elif SIZEOF_PTR == SIZEOF_INT -/* Hypothetical IP32L64 model */ -typedef int intnat; -typedef unsigned int uintnat; -#define ARCH_INTNAT_PRINTF_FORMAT "" -#elif SIZEOF_PTR == 8 -/* Win64 model: IL32P64 */ -typedef int64_t intnat; -typedef uint64_t uintnat; -#define ARCH_INTNAT_PRINTF_FORMAT ARCH_INT64_PRINTF_FORMAT -#else -#error "No integer type available to represent pointers" -#endif - -/* Endianness of floats */ - -/* ARCH_FLOAT_ENDIANNESS encodes the byte order of doubles as follows: - the value [0xabcdefgh] means that the least significant byte of the - float is at byte offset [a], the next lsb at [b], ..., and the - most significant byte at [h]. */ - -#if defined(__arm__) && !defined(__ARM_EABI__) -#define ARCH_FLOAT_ENDIANNESS 0x45670123 -#elif defined(ARCH_BIG_ENDIAN) -#define ARCH_FLOAT_ENDIANNESS 0x76543210 -#else -#define ARCH_FLOAT_ENDIANNESS 0x01234567 -#endif - - -/* We use threaded code interpretation if the compiler provides labels - as first-class values (GCC 2.x). */ - -#if defined(__GNUC__) && __GNUC__ >= 2 && !defined(DEBUG) \ - && !defined (SHRINKED_GNUC) && !defined(CAML_JIT) -#define THREADED_CODE -#endif - - -/* Memory model parameters */ - -/* The size of a page for memory management (in bytes) is [1 << Page_log]. - [Page_size] must be a multiple of [sizeof (value)]. - [Page_log] must be be >= 8 and <= 20. - Do not change the definition of [Page_size]. */ -#define Page_log 12 /* A page is 4 kilobytes. */ -#define Page_size (1 << Page_log) - -/* Initial size of stack (bytes). */ -#define Stack_size (4096 * sizeof(value)) - -/* Minimum free size of stack (bytes); below that, it is reallocated. */ -#define Stack_threshold (256 * sizeof(value)) - -/* Default maximum size of the stack (words). */ -#define Max_stack_def (1024 * 1024) - - -/* Maximum size of a block allocated in the young generation (words). */ -/* Must be > 4 */ -#define Max_young_wosize 256 -#define Max_young_whsize (Whsize_wosize (Max_young_wosize)) - - -/* Minimum size of the minor zone (words). - This must be at least [2 * Max_young_whsize]. */ -#define Minor_heap_min 4096 - -/* Maximum size of the minor zone (words). - Must be greater than or equal to [Minor_heap_min]. -*/ -#define Minor_heap_max (1 << 28) - -/* Default size of the minor zone. (words) */ -#define Minor_heap_def 262144 - - -/* Minimum size increment when growing the heap (words). - Must be a multiple of [Page_size / sizeof (value)]. */ -#define Heap_chunk_min (15 * Page_size) - -/* Default size increment when growing the heap. - If this is <= 1000, it's a percentage of the current heap size. - If it is > 1000, it's a number of words. */ -#define Heap_chunk_def 2048 /* 15 (original value) */ - -/* Default initial size of the major heap (words); - Must be a multiple of [Page_size / sizeof (value)]. */ -#define Init_heap_def (31 * Page_size) -/* (about 512 kB for a 32-bit platform, 1 MB for a 64-bit platform.) */ - - -/* Default speed setting for the major GC. The heap will grow until - the dead objects and the free list represent this percentage of the - total size of live objects. */ -#define Percent_free_def 80 - -/* Default setting for the compacter: 500% - (i.e. trigger the compacter when 5/6 of the heap is free or garbage) - This can be set quite high because the overhead is over-estimated - when fragmentation occurs. - */ -#define Max_percent_free_def 500 - -/* Default setting for the major GC slice smoothing window: 1 - (i.e. no smoothing) -*/ -#define Major_window_def 1 - -/* Maximum size of the major GC slice smoothing window. */ -#define Max_major_window 50 - - -/* Default size of the heap in words */ -#define Heap_def 8192 - - -#endif /* CONFIG_H */ diff --git a/plugin/runtime/coq_c_ffi.c b/plugin/runtime/coq_c_ffi.c deleted file mode 100644 index cb9187700..000000000 --- a/plugin/runtime/coq_c_ffi.c +++ /dev/null @@ -1,62 +0,0 @@ -#include -#include -#include "coq_c_ffi.h" -#include "gc_stack.h" -#include "values.h" - -unsigned long long length_of_coq_string(value s) { - unsigned long long ptr = s; - register unsigned long long len = 0; - while (Is_block(ptr)) { - len += 1; - ptr = (*((unsigned long long *) ptr + 1)); - } - return len; -} - -char* string_of_coq_string(value s) { - register unsigned long long len = 0; - unsigned long long ptr = s; - unsigned long long chr; - char * str; - size_t size = (length_of_coq_string(s) + 1) * sizeof(char); - str = (char *) malloc(size); - if (str == NULL) - fprintf(stderr, "malloc of %lu bytes failed:", size); - while (Is_block(ptr)) { - chr = (*((unsigned long long *) ptr)); - *(str + len) = (char) (chr >> 1LLU); - len += 1; - ptr = *((unsigned long long *) ptr + 1); - } - str[len] = '\0'; - return str; -} - -value coq_msg_info(value msg) { - char *str = string_of_coq_string(msg); - puts(str); - free(str); - return 1; -} - -value coq_user_error(value msg) { - char *str = string_of_coq_string(msg); - fputs(str, stderr); - free(str); - exit(1); -} - -value coq_msg_debug(value msg) { - char *str = string_of_coq_string(msg); - fputs(str, stdout); - free(str); - return 1; -} - -value coq_msg_notice(value msg) { - char *str = string_of_coq_string(msg); - fputs(str, stdout); - free(str); - return 1; -} diff --git a/plugin/runtime/coq_c_ffi.h b/plugin/runtime/coq_c_ffi.h deleted file mode 100644 index 895efe331..000000000 --- a/plugin/runtime/coq_c_ffi.h +++ /dev/null @@ -1,6 +0,0 @@ -#include "values.h" - -extern value coq_msg_debug(value msg); -extern value coq_msg_info(value msg); -extern value coq_msg_notice(value msg); -extern value coq_user_error(value msg); diff --git a/plugin/runtime/gc.h b/plugin/runtime/gc.h deleted file mode 100644 index 46c6e6a4e..000000000 --- a/plugin/runtime/gc.h +++ /dev/null @@ -1,155 +0,0 @@ -#include "values.h" - -/* EXPLANATION OF THE CERTICOQ GENERATIONAL GARBAGE COLLECTOR. - Andrew W. Appel, September 2016 - -The current Certicoq code generator uses Ocaml object formats, -as described in Chapter 20 of Real World Ocaml by Minsky et al. -https://realworldocaml.org/v1/en/html/memory-representation-of-values.html - -That is: - - 31 10 9 8 7 0 - +-------+---------+----------+ - | size | color | tag byte | - +-------+---------+----------+ -v --> | value[0] | - +----------------------------+ - | value[1] | - +----------------------------+ - | . | - | . | - | . | - +----------------------------+ - | value[size-1] | - +----------------------------+ - -This works for 32-bit or 64-bit words; -if 64-bit words, substitute "63" for "31" in the diagram above. -At present we'll assume 32-bit words. - -The header file "values.h", from the OCaml distribution, -has macros (etc.) for accessing these fields and headers. - -The header file "config.h", from the OCaml distribution, defines -typedef "intnat", the "natural integer type" for this compiler/machine, -and "uintnat", the "natural unsigned integer type". -Config.h also defines (BUT WE DO NOT USE) parameters for the Ocaml -generational garbage collector. - -The important definitions we use from values.h are: - -Is_block(v) : tests whether v is a pointer (even number) -Hd_val(v) : contents of the header word, i.e., just before where v points to -Field(v,i) : the i'th field of object v -Tag_hd(h) : If h is a header-word, get the constructor-tag -Wosize_hd(h): If h is a header-word, get size of the object in words - -We define the following ourselves, following Ocaml's format: - -No_scan(t) : If t is a constructor-tag, true if none of the object's - data words are to be interpreted as pointers. - (For example, character-string data) - -CALLING THE GARBAGE COLLECTOR (this part is NOT standard Ocaml): - -The mutator runs in this environment: - - NURSERY OLDER GENERATIONS - +-------------+ start---->+-------------+ +-------------+ - | args[0] | | | | | - +-------------+ | <-\ | /-->| | - | args[1] *----\ | | *---/ | | - +-------------+ \-----> | *-/ | | | - | . | +-+ | | | | - | . | alloc|*-->+-------------+ | | - | . | +-+ | | | | - +-------------+ | | | | - | args[argc-1]| +-+ | | | | - +-------------+ limit|*-->+-------------+ | | - +-+ +-------------+ - -There is a global "args" array. Certain words in "args" may -point into the heap (either the nursery or into older generations). -The nursery may point within itself, or into older generations. -Older generations may not point into the nursery. -The heap may not point into the args array. - -The mutator creates a new object by using the N+1 words (including header) -starting at "alloc", and then adding N+1 to alloc. This is only -permitted if alloc+N+1 <= limit. Otherwise, the mutator must -first call the garbage collector. - -The variables "alloc" and "limit" are owned by the mutator. -The "start" value is not actually a variable of the mutator, -but it was the value of "alloc" immediately after the most -recent collection. - -To call the garbage collector, the mutator passes a fun_info and -a thread_info, as follows. */ - -typedef const uintnat *fun_info; -/* fi[0]: How many words the function might allocate - fi[1]: How many slots of the args array contain live roots - fi[2..(fi[1]-2)]: Indices of the live roots in the args array -*/ - -struct heap; /* abstract, opaque */ - -#define MAX_ARGS 1024 - -struct thread_info { - value *alloc; /* alloc pointer */ - value *limit; /* limit pointer */ - struct heap *heap; /* Description of the generations in the heap */ - value args[MAX_ARGS]; /* the args array */ -}; - -struct thread_info *make_tinfo(void); - -void garbage_collect(fun_info fi, struct thread_info *ti); -/* Performs one garbage collection; - or if ti->heap==NULL, initializes the heap. - - The returns in a state where - (1) the "after" graph of nodes reachable from args[indices[0..num_args]] - is isomorphic to the "before" graph; and - (2) the alloc pointer points to N words of unallocated heap space - (where N>=num_allocs), such that limit-alloc=N. -*/ - -void free_heap(struct heap *h); -/* Deallocates all heap data associated with h, and returns the - * memory to the operating system (via the malloc/free system). - * After calling this function, h is a dangling pointer and should not be used. - */ - -void reset_heap(struct heap *h); -/* Empties the heap without freeing its storage. - * After a complete execution of the mutator, - * and after whoever invoked the mutator copies whatever result they want - * out of the heap, one can call this function before starting - * another mutator execution. This saves the operating-system overhead of - * free_heap() followed by the implicit create_heap that would have been - * done in the first garbage_collect() call of the next execution. - */ - -/* which slot of the args array has the answer of a certicoq program */ -#define answer_index 1 - -value* extract_answer(struct thread_info *ti); -/* y=extract_answer(x,ti) copies the dag rooted at ti->args[answer_index] - into a compact data structure starting at y[1], outside the heap, - in a single malloc'ed (therefore freeable) object at address y. - All within-the-heap pointers will now be within the object y. - If (the answer within) the heap pointed to records outside - the heap, then those will point at their original locations - outside the object y. - - Note that the start is *(y+1), not (y+1); that is, there's an - extra wrapper-record round the object. That's so that the - root-within-the-heap and the root-outside-the-heap (or root-unboxed) - can be treated uniformly by the caller of extract_answer(). -*/ - -void* export(struct thread_info *ti); diff --git a/plugin/runtime/gc_stack.c b/plugin/runtime/gc_stack.c deleted file mode 100644 index 0ef06be37..000000000 --- a/plugin/runtime/gc_stack.c +++ /dev/null @@ -1,554 +0,0 @@ -#include -#include -#include -#include "m.h" /* use printm.c to create m.h */ -#include "config.h" -#include "values.h" -#include "gc_stack.h" - -/* A version of GC that scans a stack in order to find the roots. It is useful - * when compiling direct-style programs - */ - - -/* The following 5 functions should (in practice) compile correctly in CompCert, - but the CompCert correctness specification does not _require_ that - they compile correctly: their semantics is "undefined behavior" in - CompCert C (and in C11), but in practice they will work in any compiler. */ - -int test_int_or_ptr (value x) /* returns 1 if int, 0 if aligned ptr */ { - return (int)(((intnat)x)&1); -} - -intnat int_or_ptr_to_int (value x) /* precondition: is int */ { - return (intnat)x; -} - -void * int_or_ptr_to_ptr (value x) /* precond: is aligned ptr */ { - return (void *)x; -} - -value int_to_int_or_ptr(intnat x) /* precondition: is odd */ { - return (value)x; -} - -value ptr_to_int_or_ptr(void *x) /* precondition: is aligned */ { - return (value)x; -} - -int is_ptr(value x) { - return test_int_or_ptr(x) == 0; -} - -/* A "space" describes one generation of the generational collector. -struct space { - value *start, *next, *limit, *rem_limit; - };*/ -/* Either start==NULL (meaning that this generation has not yet been created), - or start <= next <= limit. The words in start..next are allocated - and initialized, and the words from next..limit are available to allocate. */ - -#ifndef RATIO -#define RATIO 2 /* size of generation i+1 / size of generation i */ -/* Using RATIO=2 is faster than larger ratios, empirically */ -#endif - -/* Rationale for LOG_NURSERY_SIZE = 16: - The size of generation 0 (the "nursery") should approximately match the - size of the level-2 cache of the machine, according to: - Cache Performance of Fast-Allocating Programs, - by Marcelo J. R. Goncalves and Andrew W. Appel. - 7th Int'l Conf. on Functional Programming and Computer Architecture, - pp. 293-305, ACM Press, June 1995. - We estimate this as 256 kilobytes - (which is the size of the Intel Core i7 per-core L2 cache). - http://www.tomshardware.com/reviews/Intel-i7-nehalem-cpu,2041-10.html - https://en.wikipedia.org/wiki/Nehalem_(microarchitecture) - Empirical measurements on Intel Core i7 in 32-bit mode show that NURSERY_SIZE=64k 4-byte words works well - (or anything in the range from 32k to 128k). - Some machines are radically different, however: - Mac M2 "big" core has 64-bit words, L1 cache 128kB, shared L2 cache 16MB - Mac M2 "small" core has 64-bit words, L1 cache 64kB, shared L2 cache 4MB - On such machines the Goncalves rule of thumb may not apply; would be worth measuring - performance with different nursery sizes, on realistic workloads. - -*/ - - -/* The definition of MAX_SPACES allows the largest generation to be as big - as half the entire address space. - Here's the math: 8*sizeof(value) is the number of bits per word. - Counting the nursery as generation 0, the largest generation is MAX_SPACES-1, - and generation i+1 is twice as big as generation i. - Therefore the number of bytes in the largest generation is, - WORDSIZE*2^(MAX_SPACES-1)*NURSERY_SIZE - = 2^(LOG_WORDSIZE + MAX_SPACES-1 + LOG_NURSERY_SIZE) - = 2^(LOG_WORDSIZE + 8*WORDSIZE - (2+LOG_WORDDSIZE+LOG_NURSERY_SIZE) + LOG_NURSERY_SIZE) - = 2^(8*WORDSIZE - 2) - On a 64-bit machine this is 2^(64-2) = 2^62; on a 32-bit machine it is 4*2^26 = 2^30. - - On a 32-bit machine, that's actually a problem! We would like the largest generation - to be as big as 2^31, so the sum of all the generations could approach 2^32, and we use - the entire address space. To make that work, we would have to reason more carefully - about pointer subtractions; see NOTE-POINTER-ARITH below. This could probably be done. -*/ - -#ifndef DEPTH -#define DEPTH 0 /* how much depth-first search to do */ -#endif - -#ifdef DEBUG - -int in_heap(struct heap *h, value v) { - int i; - for (i=0; ispaces[i].start != NULL) - if (h->spaces[i].start <= (value*)v && - (value *)v <= h->spaces[i].limit) - return 1; - return 0; -} - -void printtree(FILE *f, struct heap *h, value v) { - if(is_ptr(v)) - if (in_heap(h,v)) { - header_t hd = Field(v,-1); - int sz = Wosize_hd(hd); - int i; - fprintf(f,"%d(", Tag_hd(hd)); - for(i=0; i>1); -} - -// XXX todo update for roots arrays -/* void printroots (FILE *f, struct heap *h, */ -/* fun_info fi, /\* which args contain live roots? *\/ */ -/* struct thread_info *ti) /\* where's the args array? *\/ */ -/* { */ -/* value *args; int n; uintnat i, *roots; */ -/* roots = fi+2; */ -/* n = fi[1]; */ -/* args = ti->args; */ - -/* for(i = 0; i < n; i++) { */ -/* fprintf(f,"%d[%8x]:",roots[i],args[roots[i]]); */ -/* printtree(f, h, args[roots[i]]); */ -/* fprintf(f,"\n"); */ -/* } */ -/* fprintf(f,"\n"); */ -/* } */ - -#endif - -void abort_with(char *s) { - fprintf(stderr, "%s", s); - exit(1); -} - -int Is_from(value* from_start, value * from_limit, value * v) { - return (from_start <= v && v < from_limit); -} -/* Assuming v is a pointer (is_ptr(v)), tests whether v points - somewhere into the "from-space" defined by from_start and from_limit */ - -void forward (value *from_start, /* beginning of from-space */ - value *from_limit, /* end of from-space */ - value **next, /* next available spot in to-space */ - value *p, /* location of word to forward */ - int depth) /* how much depth-first search to do */ -/* What it does: If *p is a pointer, AND it points into from-space, - then make *p point at the corresponding object in to-space. - If such an object did not already exist, create it at address *next - (and increment *next by the size of the object). - If *p is not a pointer into from-space, then leave it alone. - - The depth parameter may be set to 0 for ordinary breadth-first - collection. Setting depth to a small integer (perhaps 10) - may improve the cache locality of the copied graph. -*/ -{ - value * v; - value va = *p; - if(is_ptr(va)) { - v = (value*)int_or_ptr_to_ptr(va); - /* printf("Start: %lld end"" %lld word %lld \n", from_start, from_limit, v); */ - /* if (v == 4360698480) printf ("Found it\n"); */ - if(Is_from(from_start, from_limit, v)) { - /* printf("Moving\n"); */ - header_t hd = Hd_val(v); - if(hd == 0) { /* already forwarded */ - *p = Field(v,0); - } else { - intnat i; - intnat sz; - value *newv; - sz = Wosize_hd(hd); - newv = *next+1; - *next = newv+sz; - /* if (sz > 50) printf("Moving value %p with tag %ld with %d fields\n", (void*)v, hd, sz); */ - Hd_val(newv) = hd; - for(i = 0; i < sz; i++) { - /* printf("Moving field %d\n", i); */ - Field(newv, i) = Field(v, i); - } - Hd_val(v) = 0; - Field(v, 0) = ptr_to_int_or_ptr((void *)newv); - *p = ptr_to_int_or_ptr((void *)newv); - /* printf("New %lld\n", newv); */ - /* if (*p == 73832) printf("Found it\n"); */ - if (depth>0) - if (!No_scan(Tag_hd(hd))) - for (i=0; istart, *from_limit=from->limit, *from_rem_limit=from->rem_limit; - value *q = from_limit; - assert (from_rem_limit-from_limit <= to->limit-to->start); - while (q != from_rem_limit) { - value *p = *(value**)q; - if (!(from_start <= p && p < from_limit)) { - value oldp= *p, newp; - forward(from_start, from_limit, next, p, DEPTH); - newp= *p; - if (oldp!=newp) - *(--to->limit) = (value)p; - } - q++; - } -} - -void forward_roots (value *from_start, /* beginning of from-space */ - value *from_limit, /* end of from-space */ - value **next, /* next available spot in to-space */ - struct stack_frame *frames) /* data structure to find the roots */ -/* Forward each live root in the stack */ - { - struct stack_frame *frame = frames; - value *start; size_t i, limit; - /* Scan the stack by traversing the stack pointers */ - - while (frame != NULL) { - start = frame->root; - limit = frame->next - start; /* See NOTE-POINTER-ARITH below */ - frame = frame->prev; - for (i=0; inext; - /* assert(from->next-from->start + from->rem_limit-from->limit <= to->limit-to->next); */ - forward_remset(from, to, &to->next); - forward_roots(from->start, from->limit, &to->next, fr); - do_scan(from->start, from->limit, p, &to->next); - #ifdef CERTICOQ_DEBUG_GC - fprintf(stderr,"%5.3f%% occupancy\n", - (to->next-p)/(double)(from->next-from->start)); - #endif - from->next=from->start; - from->limit=from->rem_limit; -} - -#if 0 -/* This "gensize" function is only useful if the desired ratio is >2, - but empirical measurements show that ratio=2 is better than ratio>2. */ -uintnat gensize(uintnat words) -/* words is size of one generation; calculate size of the next generation */ -{ - uintnat maxint = 0u-1u; - uintnat n,d; - /* The next few lines calculate a value "n" that's at least words*2, - preferably words*RATIO, and without overflowing the size of an - unsigned integer. */ - /* minor bug: this assumes sizeof(uintnat)==sizeof(void*)==sizeof(value) */ - if (words > maxint/(2*sizeof(value))) - abort_with("Next generation would be too big for address space\n"); - d = maxint/RATIO; - if (words= 2*words); - return n; -} -#endif - -void create_space(struct space *s, /* which generation to create */ - uintnat n) /* size of the generation */ - /* malloc an array of words for generation "s", and - set s->start and s->next to the beginning, and s->limit to the end. - */ - - { - value *p; - p = (value *)malloc(n * sizeof(value)); - if (p==NULL) - abort_with ("Could not create the next generation\n"); - /* fprintf(stderr, "Created a generation of %d words\n", n); */ - s->start=p; - s->next=p; - s->limit = p+n; - s->rem_limit = s->limit; -} - -struct heap *create_heap() -/* To create a heap, first malloc the array of space-descriptors, - then create only generation 0. */ -{ - int i; - struct heap *h = (struct heap *)malloc(sizeof (struct heap)); - if (h==NULL) - abort_with("Could not create the heap\n"); - create_space(h->spaces+0, NURSERY_SIZE); - for(i=1; ispaces[i].start = NULL; - h->spaces[i].next = NULL; - h->spaces[i].limit = NULL; - h->spaces[i].rem_limit = NULL; - } - return h; -} - -struct thread_info *make_tinfo(void) { - struct heap *h; - struct thread_info *tinfo; - h = create_heap(); - tinfo = (struct thread_info *)malloc(sizeof(struct thread_info)); - if (!tinfo) - abort_with("Could not allocate thread_info struct\n"); - - tinfo->heap=h; - tinfo->alloc=h->spaces[0].start; - tinfo->limit=h->spaces[0].limit; - tinfo->fp=NULL; /* the initial stack pointer is NULL */ - tinfo->nalloc=0; - tinfo->odata=NULL; - return tinfo; -} - -void resume(struct thread_info *ti) -/* When the garbage collector is all done, inform the mutator - of the new values for the alloc and limit pointers, - and check that enough space has been freed (ti->nalloc words). -*/ - { - struct heap *h = ti->heap; - value *lo, *hi; - uintnat num_allocs = ti->nalloc; - assert (h); - lo = h->spaces[0].start; - hi = h->spaces[0].limit; - if (hi-lo < num_allocs) /* See NOTE-POINTER-ARITH below */ - abort_with ("Nursery is too small for function's num_allocs\n"); - ti->alloc = lo; - ti->limit = hi; - /* printf ("end gc\n"); */ -} - -void garbage_collect(struct thread_info *ti) -/* See the header file for the interface-spec of this function. */ -{ - struct heap *h = ti->heap; - /* printf("In GC\n"); */ - int i; - h->spaces[0].limit = ti->limit; - h->spaces[0].next = ti->alloc; /* this line is probably unnecessary */ - for (i=0; ispaces[i+1].start==NULL) { - intnat w = h->spaces[i].rem_limit-h->spaces[i].start; /* See NOTE-POINTER-ARITH below */ - create_space(h->spaces+(i+1), RATIO*w); - } - /* Copy all the objects in generation i, into generation i+1 */ - #ifdef CERTICOQ_DEBUG_GC - fprintf(stderr, "Generation %d: ", i); - #endif - do_generation(h->spaces+i, h->spaces+(i+1), ti->fp); - /* If there's enough space in gen i+1 to guarantee that the - NEXT collection into i+1 will succeed, we can stop here. - We need enough space in the (unlikely) scenario where - * all the data in gen i is live ([i].limit-[i].start), and - * all the remembered set in i is preserved ([i].rem_limit-[i].limit). - */ - if (h->spaces[i].rem_limit - h->spaces[i].start /* See NOTE-POINTER-ARITH below */ - <= h->spaces[i+1].limit - h->spaces[i+1].next) { - resume(ti); - return; - } - } - - /* If we get to i==MAX_SPACES, that's bad news */ - /* assert (MAX_SPACES == i); */ - abort_with("Ran out of generations\n"); -} - -/* REMARK. The generation-management policy in the garbage_collect function - has a potential flaw. Whenever a record is copied, it is promoted to - a higher generation. This is generally a good idea. But there is - a bounded number of generations. A useful improvement would be: - when it's time to collect the oldest generation (and we can tell - it's the oldest, at least because create_space() fails), do some - reorganization instead of failing. -*/ - -void reset_heap (struct heap *h) { - fprintf(stderr, "Debug: in reset_heap\n"); - int i; - for (i=0; ispaces[i].next = h->spaces[i].start; -} - - -void free_heap (struct heap *h) { - fprintf(stderr, "Debug: in free_heap\n"); - int i; - for (i=0; ispaces[i].start; - if (p!=NULL) - free(p); - } - free (h); -} - -int garbage_collect_all(struct thread_info *ti) { - struct heap *h = ti->heap; - if (h==NULL) { - h = create_heap(); - ti->heap = h; - } - int i; - - h->spaces[0].limit = ti->limit; - h->spaces[0].next = ti->alloc; /* this line more necessary here than perhaps in garbage_collect() */ - for (i=0; i < MAX_SPACES - 1 && h->spaces[i+1].start != NULL; i++) - do_generation(h->spaces+i, h->spaces+(i+1), ti->fp); - - return i; -} - -/* export_heap (deep copy if boxed) from the given root */ -void *export_heap(struct thread_info *ti, value root) { - - - /* This block of 7 lines is new (appel 2023/06/27) and untested */ - struct stack_frame frame; - value roots[1]; - roots[0]=root; - frame.root=roots; - frame.next=roots+1; - frame.prev=NULL; - ti->fp= &frame; - - /* if root is unboxed, return it */ - if(!is_ptr(root)) - return (void *)root; - - /* otherwise collect all that is reachable from it to the last generation, then compact it into value_sp */ - int gen_level = garbage_collect_all(ti); - struct space* sp = ti->heap->spaces+gen_level; - struct space* fake_sp = (struct space*)malloc(sizeof(struct space)); - - create_space(fake_sp, sp->next - sp->start); - do_generation(sp, fake_sp, ti->fp); - - struct space* value_sp = (struct space*)malloc(sizeof(struct space)); - create_space(value_sp, fake_sp->next - fake_sp->start); - do_generation(fake_sp, value_sp, ti->fp); - - /* offset start by the header */ - void* result_block = (void *)(value_sp->start +1); - - free(fake_sp->start); - free(fake_sp); - free(value_sp); - - return result_block; -} - -/* mutable write barrier */ -void certicoq_modify(struct thread_info *ti, value *p_cell, value p_val) { - assert (ti->alloc < ti->limit); - *p_cell = p_val; - if (is_ptr(p_val)) { - *(value **)(--ti->limit) = p_cell; - } -} - -void print_heapsize(struct thread_info *ti) { - for (int i = 0; i < MAX_SPACES; i++) { - int allocated = (int)(ti->heap->spaces[i].next - ti->heap->spaces[i].start); - int remembered = (int)(ti->heap->spaces[i].rem_limit - ti->heap->spaces[i].limit); - if (!(allocated || remembered)) { - continue; - } - printf("generation %d:\n", i); - printf(" size: %d\n", (int)(ti->heap->spaces[i].rem_limit - ti->heap->spaces[i].start)); - printf(" allocated: %d\n", allocated); - printf(" remembered: %d\n", remembered); - } -} - -/* NOTE-POINTER-ARITH: In a few places, we do a pointer subtraction, such as - h->spaces[i].limit - h->spaces[i].start. - When p and q have type *foo, then this is much like ((int)p-(int)q)/sizeof(foo). - But note this is a SIGNED division, which makes it quite dangerous if ((int)p-(int)q) - can be larger than the maximum signed integer. So we have to be quite careful in - the program and the proof, especially when (on a 32-bit machines) our largest generation - might be similar in size to the entire address space. -*/ - - - diff --git a/plugin/runtime/gc_stack.h b/plugin/runtime/gc_stack.h deleted file mode 100644 index a7e33a3d1..000000000 --- a/plugin/runtime/gc_stack.h +++ /dev/null @@ -1,195 +0,0 @@ -#ifndef CERTICOQ_GC_STACK_H -#define CERTICOQ_GC_STACK_H - -#include "values.h" - -/* EXPLANATION OF THE CERTICOQ GENERATIONAL GARBAGE COLLECTOR. - Andrew W. Appel, September 2016 - -The current Certicoq code generator uses Ocaml object formats, -as described in Chapter 20 of Real World Ocaml by Minsky et al. -https://realworldocaml.org/v1/en/html/memory-representation-of-values.html - -That is: - - 31 10 9 8 7 0 - +-------+---------+----------+ - | size | color | tag byte | - +-------+---------+----------+ -v --> | value[0] | - +----------------------------+ - | value[1] | - +----------------------------+ - | . | - | . | - | . | - +----------------------------+ - | value[size-1] | - +----------------------------+ - -This works for 32-bit or 64-bit words; -if 64-bit words, substitute "63" for "31" in the diagram above. -At present we'll assume 32-bit words. - -The header file "values.h", from the OCaml distribution, -has macros (etc.) for accessing these fields and headers. - -The header file "config.h", from the OCaml distribution, defines -typedef "intnat", the "natural integer type" for this compiler/machine, -and "uintnat", the "natural unsigned integer type". -Config.h also defines (BUT WE DO NOT USE) parameters for the Ocaml -generational garbage collector. - -The important definitions we use from values.h are: - -Is_block(v) : tests whether v is a pointer (even number) -Hd_val(v) : contents of the header word, i.e., just before where v points to -Field(v,i) : the i'th field of object v -Tag_hd(h) : If h is a header-word, get the constructor-tag -Wosize_hd(h): If h is a header-word, get size of the object in words - -We define the following ourselves, following Ocaml's format: - -No_scan(t) : If t is a constructor-tag, true if none of the object's - data words are to be interpreted as pointers. - (For example, character-string data) - -CALLING THE GARBAGE COLLECTOR (this part is NOT standard Ocaml): - -The mutator runs in this environment: - - NURSERY OLDER GENERATIONS - +-------------+ start---->+-------------+ +-------------+ - | args[0] | | | | | - +-------------+ | <-\ | /-->| | - | args[1] *----\ | | *---/ | | - +-------------+ \-----> | *-/ | | | - | . | +-+ | | | | - | . | alloc|*-->+-------------+ | | - | . | +-+ | | | | - +-------------+ | | | | - | args[argc-1]| +-+ | | | | - +-------------+ limit|*-->+-------------+ | | - +-+ +-------------+ - -There is a global "args" array. Certain words in "args" may -point into the heap (either the nursery or into older generations). -The nursery may point within itself, or into older generations. -Older generations may not point into the nursery. -The heap may not point into the args array. - -The mutator creates a new object by using the N+1 words (including header) -starting at "alloc", and then adding N+1 to alloc. This is only -permitted if alloc+N+1 <= limit. Otherwise, the mutator must -first call the garbage collector. - -The variables "alloc" and "limit" are owned by the mutator. -The "start" value is not actually a variable of the mutator, -but it was the value of "alloc" immediately after the most -recent collection. - -To call the garbage collector, the mutator passes a fun_info and -a thread_info, as follows. */ - -#define No_scan_tag 251 -#define No_scan(t) ((t) >= No_scan_tag) - -typedef const uintnat *fun_info; -/* fi[0]: How many words the function might allocate - fi[1]: How many slots of the args array contain live roots - fi[2..(fi[1]-2)]: Indices of the live roots in the args array -*/ - -/* ideally struct heap should be more abstract (opaque) - struct heap; - and ideally, the following definitions should live in gc_stack.c rather than gc_stack.h: -*/ -#if SIZEOF_PTR == 8 -#define LOG_WORDSIZE 3 -#endif -#if SIZEOF_PTR == 4 -#define LOG_WORDSIZE 2 -#endif -#define LOG_NURSERY_SIZE 16 -#define NURSERY_SIZE (1<heap==NULL, initializes the heap. - - The returns in a state where - (1) the "after" graph of nodes reachable from args[indices[0..num_args]] - is isomorphic to the "before" graph; and - (2) the alloc pointer points to N words of unallocated heap space - (where N>=num_allocs), such that limit-alloc=N. -*/ - -void free_heap(struct heap *h); -/* Deallocates all heap data associated with h, and returns the - * memory to the operating system (via the malloc/free system). - * After calling this function, h is a dangling pointer and should not be used. - */ - -void reset_heap(struct heap *h); -/* Empties the heap without freeing its storage. - * After a complete execution of the mutator, - * and after whoever invoked the mutator copies whatever result they want - * out of the heap, one can call this function before starting - * another mutator execution. This saves the operating-system overhead of - * free_heap() followed by the implicit create_heap that would have been - * done in the first garbage_collect() call of the next execution. - */ - -/* which slot of the args array has the answer of a certicoq program */ -#define answer_index 1 - -value* extract_answer(struct thread_info *ti); -/* y=extract_answer(x,ti) copies the dag rooted at ti->args[answer_index] - into a compact data structure starting at y[1], outside the heap, - in a single malloc'ed (therefore freeable) object at address y. - All within-the-heap pointers will now be within the object y. - If (the answer within) the heap pointed to records outside - the heap, then those will point at their original locations - outside the object y. - - Note that the start is *(y+1), not (y+1); that is, there's an - extra wrapper-record round the object. That's so that the - root-within-the-heap and the root-outside-the-heap (or root-unboxed) - can be treated uniformly by the caller of extract_answer(). -*/ - -void* export_heap(struct thread_info *ti, value root); - -/* mutable write barrier */ -void certicoq_modify(struct thread_info *ti, value *p_cell, value p_val); - -void print_heapsize(struct thread_info *ti); - -#endif /* CERTICOQ_GC_STACK_H */ diff --git a/plugin/runtime/m.h b/plugin/runtime/m.h deleted file mode 100644 index 1c509a54b..000000000 --- a/plugin/runtime/m.h +++ /dev/null @@ -1,3 +0,0 @@ -#define SIZEOF_PTR 8 -#define SIZEOF_LONG 8 -#define SIZEOF_INT 4 diff --git a/plugin/runtime/prim_floats.h b/plugin/runtime/prim_floats.h deleted file mode 100644 index a5d538463..000000000 --- a/plugin/runtime/prim_floats.h +++ /dev/null @@ -1,37 +0,0 @@ -#include "values.h" -#include "prim_int63.h" -#include - -#ifndef PRIM_FLOATS_H -#define PRIM_FLOATS_H 1 - -typedef value primfloat; -typedef value primfloatintpair; -typedef value primfloat_class; -typedef value primfloat_comparison; - -// #define inf INFINITY // OCaml name for infinity - -extern primfloat_comparison prim_float_compare(primfloat x, primfloat y); -extern primbool prim_float_eqb(primfloat x, primfloat y); -extern primbool prim_float_ltb(primfloat x, primfloat y); -extern primbool prim_float_leb(primfloat x, primfloat y); - -extern primfloatintpair prim_float_frshiftexp(struct thread_info *ti, primfloat x); -extern primfloat prim_float_ldshiftexp(struct thread_info *ti, primfloat x, primint exp); - -extern primint prim_float_normfr_mantissa(primfloat x); -extern primfloat_class prim_float_classify(primfloat x); - -extern primfloat prim_float_div(struct thread_info *ti, primfloat x, primfloat y); -extern primfloat prim_float_abs(struct thread_info *ti, primfloat x); -extern primfloat prim_float_sqrt(struct thread_info *ti, primfloat x); -extern primfloat prim_float_opp(struct thread_info *ti, primfloat x); -extern primfloat prim_float_mul(struct thread_info *ti, primfloat x, primfloat y); -extern primfloat prim_float_add(struct thread_info *ti, primfloat x, primfloat y); -extern primfloat prim_float_sub(struct thread_info *ti, primfloat x, primfloat y); -extern primfloat prim_float_of_uint63(struct thread_info *, primint); -extern primfloat prim_float_next_up(struct thread_info *, primfloat); -extern primfloat prim_float_next_down(struct thread_info *, primfloat); - -#endif // PRIM_FLOATS_H \ No newline at end of file diff --git a/plugin/runtime/prim_int63.h b/plugin/runtime/prim_int63.h deleted file mode 100644 index 8dd751dc6..000000000 --- a/plugin/runtime/prim_int63.h +++ /dev/null @@ -1,48 +0,0 @@ -#include "values.h" - -#ifndef PRIM_INT63_H -#define PRIM_INT63_H - -typedef value primint; -typedef value primbool; -typedef value primintcarry; -typedef value primintpair; - -extern primbool mk_bool(int); -extern value mk_pair(struct thread_info *ti, value x, value y); - -extern primint prim_int63_add(primint x, primint y); -extern primint prim_int63_sub(primint x, primint y); -extern primint prim_int63_mul(primint x, primint y); -extern primint prim_int63_mod(primint x, primint y); -extern primint prim_int63_div(primint x, primint y); - -extern primint prim_int63_land(primint x, primint y); -extern primint prim_int63_lsl(primint x, primint y); -extern primint prim_int63_lsr(primint x, primint y); -extern primint prim_int63_lor(primint x, primint y); -extern primint prim_int63_lxor(primint x, primint y); - -extern primint prim_int63_head0(primint x); -extern primint prim_int63_tail0(primint x); - -extern primbool prim_int63_eqb(primint x, primint y); -extern primbool prim_int63_leb(primint x, primint y); -extern primbool prim_int63_ltb(primint x, primint y); -extern value prim_int63_compare(primint x, primint y); - -extern primintcarry prim_int63_addc(struct thread_info *, primint x, primint y); -extern primintcarry prim_int63_addcarryc(struct thread_info *, primint x, primint y); -extern primintcarry prim_int63_subc(struct thread_info *, primint x, primint y); -extern primintcarry prim_int63_subcarryc(struct thread_info *, primint x, primint y); -extern primintpair prim_int63_mulc(struct thread_info *, primint x, primint y); - -/* [div21 xh xl y] returns [q % 2^63, r] - s.t. [xh * 2^63 + xl = q * y + r] and [r < y]. - When [y] is [0], returns [0, 0]. */ -extern primintpair prim_int63_diveucl_21(struct thread_info *, primint x, primint y, primint z); -extern primintpair prim_int63_diveucl(struct thread_info *, primint x, primint y); - -extern primint prim_int63_addmuldiv(primint x, primint y, primint z); - -#endif /* PRIM_INT63_H */ \ No newline at end of file diff --git a/plugin/runtime/values.h b/plugin/runtime/values.h deleted file mode 100644 index aeefec1fc..000000000 --- a/plugin/runtime/values.h +++ /dev/null @@ -1,224 +0,0 @@ -/**************************************************************************/ -/* */ -/* OCaml */ -/* */ -/* Xavier Leroy and Damien Doligez, INRIA Rocquencourt */ -/* */ -/* Copyright 1996 Institut National de Recherche en Informatique et */ -/* en Automatique. */ -/* */ -/* All rights reserved. This file is distributed under the terms of */ -/* the GNU Lesser General Public License version 2.1, with the */ -/* special exception on linking described in the file LICENSE. */ -/* */ -/**************************************************************************/ - -#ifndef VALUES_H -#define VALUES_H - -#include "config.h" - -#ifdef __cplusplus -extern "C" { -#endif - -/* Definitions - - word: Four bytes on 32 and 16 bit architectures, - eight bytes on 64 bit architectures. - long: A C integer having the same number of bytes as a word. - val: The ML representation of something. A long or a block or a pointer - outside the heap. If it is a block, it is the (encoded) address - of an object. If it is a long, it is encoded as well. - block: Something allocated. It always has a header and some - fields or some number of bytes (a multiple of the word size). - field: A word-sized val which is part of a block. - bp: Pointer to the first byte of a block. (a char *) - op: Pointer to the first field of a block. (a value *) - hp: Pointer to the header of a block. (a char *) - int32_t: Four bytes on all architectures. - int64_t: Eight bytes on all architectures. - - Remark: A block size is always a multiple of the word size, and at least - one word plus the header. - - bosize: Size (in bytes) of the "bytes" part. - wosize: Size (in words) of the "fields" part. - bhsize: Size (in bytes) of the block with its header. - whsize: Size (in words) of the block with its header. - - hd: A header. - tag: The value of the tag field of the header. - color: The value of the color field of the header. - This is for use only by the GC. -*/ - - -/* -CHANGE BY THE CERTICOQ/VERIFFI TEAM: -We do this for CertiCoq's FFI system because for technical reasons related to -VST's program logic type system, we need the value type to be void* with this -attribute. On the other hand, standard OCaml wants the value to be intnat. -*/ -#ifdef VERIFFI - typedef void * value - #ifdef COMPCERT - __attribute((aligned(_Alignof(void *)))) - #endif - ; -#else - typedef intnat value; -#endif -/* because of VST's restrictions. */ -typedef uintnat header_t; -typedef uintnat mlsize_t; -typedef unsigned int tag_t; /* Actually, an unsigned char */ -typedef uintnat color_t; -typedef uintnat mark_t; - -/* Longs vs blocks. */ -#define Is_long(x) (((x) & 1) != 0) -/* CHANGE BY THE CERTICOQ/VERIFFI TEAM: */ -#ifdef VERIFFI - #define Is_block(x) (((int)(((intnat) x) & 1)) == 0) -#else - #define Is_block(x) (((x) & 1) == 0) -#endif - -/* Conversion macro names are always of the form "to_from". */ -/* Example: Val_long as in "Val from long" or "Val of long". */ -#define Val_long(x) ((intnat) (((uintnat)(x) << 1)) + 1) -#define Long_val(x) ((x) >> 1) -#define Max_long (((intnat)1 << (8 * sizeof(value) - 2)) - 1) -#define Min_long (-((intnat)1 << (8 * sizeof(value) - 2))) -#define Val_int(x) Val_long(x) -#define Int_val(x) ((int) Long_val(x)) -#define Unsigned_long_val(x) ((uintnat)(x) >> 1) -#define Unsigned_int_val(x) ((int) Unsigned_long_val(x)) - -/* Structure of the header: - -For 16-bit and 32-bit architectures: - +--------+-------+-----+ - | wosize | color | tag | - +--------+-------+-----+ -bits 31 10 9 8 7 0 - -For 64-bit architectures: - - +--------+-------+-----+ - | wosize | color | tag | - +--------+-------+-----+ -bits 63 10 9 8 7 0 - -For x86-64 with Spacetime profiling: - P = PROFINFO_WIDTH (as set by "configure", currently 26 bits, giving a - maximum block size of just under 4Gb) - +----------------+----------------+-------------+ - | profiling info | wosize | color | tag | - +----------------+----------------+-------------+ -bits 63 (64-P) (63-P) 10 9 8 7 0 - -*/ - -#define PROFINFO_SHIFT (64 - PROFINFO_WIDTH) -#define PROFINFO_MASK ((1ull << PROFINFO_WIDTH) - 1ull) - -#define Tag_hd(hd) ((tag_t) ((hd) & 0xFF)) -#ifdef WITH_SPACETIME -#define Hd_no_profinfo(hd) ((hd) & ~(PROFINFO_MASK << PROFINFO_SHIFT)) -#define Wosize_hd(hd) ((mlsize_t) ((Hd_no_profinfo(hd)) >> 10)) -#else -#define Wosize_hd(hd) ((mlsize_t) ((hd) >> 10)) -#endif /* SPACETIME */ -#ifdef ARCH_SIXTYFOUR -/* [Profinfo_hd] is used when the compiler is not configured for Spacetime - (e.g. when decoding profiles). */ -#define Profinfo_hd(hd) (((mlsize_t) ((hd) >> PROFINFO_SHIFT)) & PROFINFO_MASK) -#else -#define Profinfo_hd(hd) ((hd) & 0) -#endif /* ARCH_SIXTYFOUR */ - -#define Hd_val(val) (((header_t *) (val)) [-1]) /* Also an l-value. */ -#define Hd_op(op) (Hd_val (op)) /* Also an l-value. */ -#define Hd_bp(bp) (Hd_val (bp)) /* Also an l-value. */ -#define Hd_hp(hp) (* ((header_t *) (hp))) /* Also an l-value. */ -#define Hp_val(val) (((header_t *) (val)) - 1) -#define Hp_op(op) (Hp_val (op)) -#define Hp_bp(bp) (Hp_val (bp)) -#define Val_op(op) ((value) (op)) -#define Val_hp(hp) ((value) (((header_t *) (hp)) + 1)) -#define Op_hp(hp) ((value *) Val_hp (hp)) -#define Bp_hp(hp) ((char *) Val_hp (hp)) - -#define Num_tags (1 << 8) -#ifdef ARCH_SIXTYFOUR -#ifdef WITH_SPACETIME -#define Max_wosize (((intnat)1 << (54-PROFINFO_WIDTH)) - 1) -#else -#define Max_wosize (((intnat)1 << 54) - 1) -#endif -#else -#define Max_wosize ((1 << 22) - 1) -#endif - -#define Wosize_val(val) (Wosize_hd (Hd_val (val))) -#define Wosize_op(op) (Wosize_val (op)) -#define Wosize_bp(bp) (Wosize_val (bp)) -#define Wosize_hp(hp) (Wosize_hd (Hd_hp (hp))) -#define Whsize_wosize(sz) ((sz) + 1) -#define Wosize_whsize(sz) ((sz) - 1) -#define Wosize_bhsize(sz) ((sz) / sizeof (value) - 1) -#define Bsize_wsize(sz) ((sz) * sizeof (value)) -#define Wsize_bsize(sz) ((sz) / sizeof (value)) -#define Bhsize_wosize(sz) (Bsize_wsize (Whsize_wosize (sz))) -#define Bhsize_bosize(sz) ((sz) + sizeof (header_t)) -#define Bosize_val(val) (Bsize_wsize (Wosize_val (val))) -#define Bosize_op(op) (Bosize_val (Val_op (op))) -#define Bosize_bp(bp) (Bosize_val (Val_bp (bp))) -#define Bosize_hd(hd) (Bsize_wsize (Wosize_hd (hd))) -#define Whsize_hp(hp) (Whsize_wosize (Wosize_hp (hp))) -#define Whsize_val(val) (Whsize_hp (Hp_val (val))) -#define Whsize_bp(bp) (Whsize_val (Val_bp (bp))) -#define Whsize_hd(hd) (Whsize_wosize (Wosize_hd (hd))) -#define Bhsize_hp(hp) (Bsize_wsize (Whsize_hp (hp))) -#define Bhsize_hd(hd) (Bsize_wsize (Whsize_hd (hd))) -#define Bhsize_val(val) (Bsize_wsize (Whsize_val (val))) - -#define Profinfo_val(val) (Profinfo_hd (Hd_val (val))) - -#ifdef ARCH_BIG_ENDIAN -#define Tag_val(val) (((unsigned char *) (val)) [-1]) - /* Also an l-value. */ -#define Tag_hp(hp) (((unsigned char *) (hp)) [sizeof(value)-1]) - /* Also an l-value. */ -#else -#define Tag_val(val) (((unsigned char *) (val)) [-sizeof(value)]) - /* Also an l-value. */ -#define Tag_hp(hp) (((unsigned char *) (hp)) [0]) - /* Also an l-value. */ -#endif - -/* Pointer to the first field. */ -#define Op_val(x) ((value *) (x)) -/* Fields are numbered from 0. */ -#define Field(x, i) (((value *)(x)) [i]) /* Also an l-value. */ - -/* Pointer to the first byte */ -#define Bp_val(v) ((char *) (v)) -#define Val_bp(p) ((value) (p)) -/* Bytes are numbered from 0. */ -#define Byte(x, i) (((char *) (x)) [i]) /* Also an l-value. */ -#define Byte_u(x, i) (((unsigned char *) (x)) [i]) /* Also an l-value. */ - -#ifdef __cplusplus -} -#endif - -/* Floating-point numbers. */ -#define Double_tag 253 -#define Double_wosize ((sizeof(double) / sizeof(value))) -#define Double_val(v) (* (double *)(v)) -#define Store_double_val(v,d) (* (double *)(v) = (d)) - -#endif /* VALUES_H */ diff --git a/plugin/test_certicoq_eval.v b/plugin/test_certicoq_eval.v index 5d39b82cb..0c5997447 100644 --- a/plugin/test_certicoq_eval.v +++ b/plugin/test_certicoq_eval.v @@ -14,6 +14,9 @@ Definition string_of_bool b := if (b : bool) then "true" else "false". #[export] Instance bool_show : Show bool := string_of_bool. +Definition test := true. +CertiCoq Eval -time -debug test. + #[export] Instance list_show {A} {SA : Show A} : Show (list A) := string_of_list show. From MetaCoq.Common Require Import Primitive. From Coq Require Import PrimFloat PrimInt63. diff --git a/plugin/runtime/Makefile b/runtime/Makefile similarity index 84% rename from plugin/runtime/Makefile rename to runtime/Makefile index 4a99d72aa..835dcd907 100644 --- a/plugin/runtime/Makefile +++ b/runtime/Makefile @@ -1,5 +1,5 @@ -SRC = gc_stack.c certicoq_run_main.c coq_c_ffi.c coq_ffi.c prim_int63.c prim_floats.c -HEADERS = m.h config.h values.h gc_stack.h certicoq_run_main.h coq_c_ffi.h coq_ffi.h prim_int63.h prim_floats.h +SRC = gc_stack.c certicoq_run_main.c coq_c_ffi.c coq_ffi.c prim_int63.c prim_floats.c get_ordinal.c +HEADERS = m.h config.h values.h gc_stack.h certicoq_run_main.h coq_c_ffi.h coq_ffi.h prim_int63.h prim_floats.h get_ordinal.h LINKOPTS = -linkpkg -dontlink str,unix,dynlink,threads,zarith TARGETS = ${SRC:.c=.o} diff --git a/plugin/runtime/certicoq_run_main.c b/runtime/certicoq_run_main.c similarity index 100% rename from plugin/runtime/certicoq_run_main.c rename to runtime/certicoq_run_main.c diff --git a/cplugin/runtime/certicoq_run_main.h b/runtime/certicoq_run_main.h similarity index 100% rename from cplugin/runtime/certicoq_run_main.h rename to runtime/certicoq_run_main.h diff --git a/cplugin/runtime/config.h b/runtime/config.h similarity index 100% rename from cplugin/runtime/config.h rename to runtime/config.h diff --git a/cplugin/runtime/coq_c_ffi.c b/runtime/coq_c_ffi.c similarity index 100% rename from cplugin/runtime/coq_c_ffi.c rename to runtime/coq_c_ffi.c diff --git a/cplugin/runtime/coq_c_ffi.h b/runtime/coq_c_ffi.h similarity index 100% rename from cplugin/runtime/coq_c_ffi.h rename to runtime/coq_c_ffi.h diff --git a/plugin/runtime/coq_ffi.c b/runtime/coq_ffi.c similarity index 100% rename from plugin/runtime/coq_ffi.c rename to runtime/coq_ffi.c diff --git a/plugin/runtime/coq_ffi.h b/runtime/coq_ffi.h similarity index 100% rename from plugin/runtime/coq_ffi.h rename to runtime/coq_ffi.h diff --git a/cplugin/runtime/gc.h b/runtime/gc.h similarity index 100% rename from cplugin/runtime/gc.h rename to runtime/gc.h diff --git a/cplugin/runtime/gc_stack.c b/runtime/gc_stack.c similarity index 100% rename from cplugin/runtime/gc_stack.c rename to runtime/gc_stack.c diff --git a/cplugin/runtime/gc_stack.h b/runtime/gc_stack.h similarity index 100% rename from cplugin/runtime/gc_stack.h rename to runtime/gc_stack.h diff --git a/plugin/get_ordinal.c b/runtime/get_ordinal.c similarity index 100% rename from plugin/get_ordinal.c rename to runtime/get_ordinal.c diff --git a/plugin/get_ordinal.h b/runtime/get_ordinal.h similarity index 100% rename from plugin/get_ordinal.h rename to runtime/get_ordinal.h diff --git a/cplugin/runtime/m.h b/runtime/m.h similarity index 100% rename from cplugin/runtime/m.h rename to runtime/m.h diff --git a/plugin/runtime/prim_floats.c b/runtime/prim_floats.c similarity index 100% rename from plugin/runtime/prim_floats.c rename to runtime/prim_floats.c diff --git a/cplugin/runtime/prim_floats.h b/runtime/prim_floats.h similarity index 100% rename from cplugin/runtime/prim_floats.h rename to runtime/prim_floats.h diff --git a/plugin/runtime/prim_int63.c b/runtime/prim_int63.c similarity index 99% rename from plugin/runtime/prim_int63.c rename to runtime/prim_int63.c index 34b9542a7..9dd891ba0 100644 --- a/plugin/runtime/prim_int63.c +++ b/runtime/prim_int63.c @@ -123,8 +123,8 @@ primint prim_int63_tail0(primint init) primbool mk_bool(int b) { - if (b) return 1; - else return 3; + if (b) return 3; + else return 1; } primbool prim_int63_eqb(primint x, primint y) diff --git a/cplugin/runtime/prim_int63.h b/runtime/prim_int63.h similarity index 100% rename from cplugin/runtime/prim_int63.h rename to runtime/prim_int63.h diff --git a/cplugin/runtime/values.h b/runtime/values.h similarity index 100% rename from cplugin/runtime/values.h rename to runtime/values.h diff --git a/submodules/metacoq b/submodules/metacoq index 13dc7ce5b..b1b6be23e 160000 --- a/submodules/metacoq +++ b/submodules/metacoq @@ -1 +1 @@ -Subproject commit 13dc7ce5b1526ee783722ff4985249951704116d +Subproject commit b1b6be23e00fefba6a03c153a458e72acb463daa diff --git a/theories/Compiler/pipeline.v b/theories/Compiler/pipeline.v index 788c38893..d24d451b4 100644 --- a/theories/Compiler/pipeline.v +++ b/theories/Compiler/pipeline.v @@ -110,7 +110,7 @@ Section Pipeline. Definition CertiCoq_pipeline (p : Ast.Env.program) := o <- get_options ;; - p <- compile_LambdaBoxMut o.(erasure_config) p ;; + p <- compile_LambdaBoxMut o.(erasure_config) o.(inductives_mapping) p ;; check_axioms p ;; p <- compile_LambdaBoxLocal prims p ;; p <- (if direct o then compile_LambdaANF_ANF next_id prims p else compile_LambdaANF_CPS next_id prims p) ;; @@ -134,6 +134,7 @@ Definition pipeline (p : Template.Ast.Env.program) := Definition default_opts : Options := {| erasure_config := Erasure.default_erasure_config; + inductives_mapping := []; direct := false; c_args := 5; anf_conf := 0; @@ -150,6 +151,7 @@ Definition default_opts : Options := Definition make_opts (erasure_config : Erasure.erasure_configuration) + (im : EProgram.inductives_mapping) (cps : bool) (* CPS or direct *) (args : nat) (* number of C args *) (conf : nat) (* λ_ANF configuration *) @@ -162,6 +164,7 @@ Definition make_opts (prims : list (kername * string * bool)) (* list of extracted constants *) : Options := {| erasure_config := erasure_config; + inductives_mapping := im; direct := negb cps; c_args := args; anf_conf := conf; diff --git a/theories/ExtractionVanilla/VanillaExtrOCamlFloats.v b/theories/ExtractionVanilla/VanillaExtrOCamlFloats.v index 4993a9fa9..c73d1b361 100644 --- a/theories/ExtractionVanilla/VanillaExtrOCamlFloats.v +++ b/theories/ExtractionVanilla/VanillaExtrOCamlFloats.v @@ -44,9 +44,9 @@ Extract Constant PrimFloat.classify => "Float64.classify". Extract Constant PrimFloat.abs => "Float64.abs". Extract Constant PrimFloat.sqrt => "Float64.sqrt". Extract Constant PrimFloat.opp => "Float64.opp". -Extract Constant PrimFloat.eqb => "fun x y -> Caml_bool.to_coq (Float64.eq x y)". -Extract Constant PrimFloat.ltb => "fun x y -> Caml_bool.to_coq (Float64.lt x y)". -Extract Constant PrimFloat.leb => "fun x y -> Caml_bool.to_coq (Float64.le x y)". +Extract Constant PrimFloat.eqb => "Float64.eq". +Extract Constant PrimFloat.ltb => "Float64.lt". +Extract Constant PrimFloat.leb => "Float64.le". Extract Constant PrimFloat.compare => "Float64.compare". Extract Constant PrimFloat.mul => "Float64.mul". Extract Constant PrimFloat.add => "Float64.add". diff --git a/theories/ExtractionVanilla/VanillaExtrOCamlInt63.v b/theories/ExtractionVanilla/VanillaExtrOCamlInt63.v index 776ad336b..805bce661 100644 --- a/theories/ExtractionVanilla/VanillaExtrOCamlInt63.v +++ b/theories/ExtractionVanilla/VanillaExtrOCamlInt63.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Extraction to OCaml of native 63-bit machine integers. *) +(** Extraction to OCaml of native 63-bit machine integers. The only difference with the regular OCaml Int63 interface is due to comparisons. *) From Coq Require Uint63 Sint63 Extraction. @@ -39,11 +39,11 @@ Extract Constant Sint63.div => "Uint63.divs". Extract Constant Sint63.rem => "Uint63.rems". -Extract Constant Uint63.eqb => "fun x y -> Caml_bool.to_coq (Uint63.equal x y)". -Extract Constant Uint63.ltb => "fun x y -> Caml_bool.to_coq (Uint63.lt x y)". -Extract Constant Uint63.leb => "fun x y -> Caml_bool.to_coq (Uint63.le x y)". -Extract Constant Sint63.ltb => "fun x y -> Caml_bool.to_coq (Uint63.lts x y)". -Extract Constant Sint63.leb => "fun x y -> Caml_bool.to_coq (Uint63.les x y)". +Extract Constant Uint63.eqb => "Uint63.equal". +Extract Constant Uint63.ltb => "Uint63.lt". +Extract Constant Uint63.leb => "Uint63.le". +Extract Constant Sint63.ltb => "Uint63.lts". +Extract Constant Sint63.leb => "Uint63.les". Extract Constant Uint63.addc => "Uint63.addc". Extract Constant Uint63.addcarryc => "Uint63.addcarryc". diff --git a/theories/ExtractionVanilla/extraction.v b/theories/ExtractionVanilla/extraction.v index e1efa6ecf..ecb6f5311 100644 --- a/theories/ExtractionVanilla/extraction.v +++ b/theories/ExtractionVanilla/extraction.v @@ -23,6 +23,7 @@ Require Import VanillaExtrOCamlInt63 VanillaExtrOCamlFloats. E.g. no constructor swapping allowed. *) +Extract Inductive bool => bool [ true false ]. (* Swaps the constructors *) Extract Inductive unit => unit [ "()" ]. Extract Inductive list => list [ "[]" "( :: )" ]. Extract Inductive prod => "( * )" [ "" ]. @@ -35,8 +36,8 @@ Extract Inductive prod => "( * )" [ "" ]. (if ... then ... else false) and (if ... then true else ...). *) -Extract Inlined Constant andb => "(fun x y -> match x with Coq_true -> Coq_true | _ -> y)". -Extract Inlined Constant orb => "(fun x y -> match x with Coq_false -> y | Coq_true -> x)". +Extract Inlined Constant andb => "(&&)". +Extract Inlined Constant orb => "(||)". Require Import ZArith NArith. @@ -84,13 +85,6 @@ Extraction Blacklist config List String Nat Int Ast Universes UnivSubst Typing R Instances Classes Term Monad Coqlib Errors Compile Checker Eq Classes0 Numeral Uint63 Number Values. -(* Cutting the dependency to R. -Extract Inlined Constant Fcore_defs.F2R => "fun _ -> assert false". -Extract Inlined Constant Fappli_IEEE.FF2R => "fun _ -> assert false". -Extract Inlined Constant Fappli_IEEE.B2R => "fun _ -> assert false". -Extract Inlined Constant Fappli_IEEE.round_mode => "fun _ -> assert false". -Extract Inlined Constant Fcalc_bracket.inbetween_loc => "fun _ -> assert false". *) - Set Warnings "-extraction-reserved-identifier". Set Warnings "-extraction-opaque-accessed". diff --git a/theories/LambdaBoxMut/compile.v b/theories/LambdaBoxMut/compile.v index 220f205ec..f83ea6f9c 100644 --- a/theories/LambdaBoxMut/compile.v +++ b/theories/LambdaBoxMut/compile.v @@ -441,10 +441,14 @@ Fixpoint compile_ctx (t : global_context) := (n, compile_global_decl decl) :: compile_ctx rest end. -Program Definition compile_program econf (p : Ast.Env.program) : Program Term := - let p := run_erase_program econf p _ in +Axiom assume_wellformed_inductives_mapping : forall Σ (ip : EProgram.inductives_mapping), is_true (wf_template_inductives_mapping Σ ip). + +Program Definition compile_program (econf : erasure_configuration) imap (p : Ast.Env.program) : Program Term := + let p := run_erase_program econf (imap, p) _ in {| main := compile (snd p) ; env := compile_ctx (fst p) |}. Next Obligation. + split. + now eapply assume_wellformed_inductives_mapping. split. now eapply assume_that_we_only_erase_on_welltyped_programs. cbv [PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn]. @@ -452,5 +456,5 @@ Next Obligation. split; typeclasses eauto. Qed. -Definition program_Program econf (p: Ast.Env.program) : Program Term := - compile_program econf p. +Definition program_Program econf ip (p: Ast.Env.program) : Program Term := + compile_program econf ip p. diff --git a/theories/LambdaBoxMut/stripEvalCommute.v b/theories/LambdaBoxMut/stripEvalCommute.v index 9a57fa57d..5da241b76 100644 --- a/theories/LambdaBoxMut/stripEvalCommute.v +++ b/theories/LambdaBoxMut/stripEvalCommute.v @@ -547,7 +547,7 @@ Proof. rewrite tlength_hom. apply eqb_eq in lenargs. lia. - destruct args => //. now constructor. solve_all. clear -crctΣ H1; induction H1; cbn; constructor; auto. repeat apply p. - - destruct lookup_inductive as [[mdecl idecl]|] eqn:hl => //. + - rewrite /wf_brs in H0. destruct lookup_inductive as [[mdecl idecl]|] eqn:hl => //. econstructor. eapply compile_crctInd; tea. eauto. repeat toAll. clear -wfΣ crctΣ H1. diff --git a/theories/LambdaBoxMut/toplevel.v b/theories/LambdaBoxMut/toplevel.v index 36b165526..4ea74708c 100644 --- a/theories/LambdaBoxMut/toplevel.v +++ b/theories/LambdaBoxMut/toplevel.v @@ -29,8 +29,8 @@ Import MonadNotation. BigStep := fun s sv => WcbvEval (env s) (main s) sv }. -Definition compile_LambdaBoxMut econf +Definition compile_LambdaBoxMut econf ip : CertiCoqTrans (Ast.Env.program) (Program LambdaBoxMut.compile.Term) := fun src => debug_msg "Translating from L1g to L1k" ;; - (LiftCertiCoqTrans "LambdaBoxMut" (compile_program econf) src). + (LiftCertiCoqTrans "LambdaBoxMut" (compile_program econf ip) src). diff --git a/theories/common/Pipeline_utils.v b/theories/common/Pipeline_utils.v index 8b708e2d5..42dcc63c1 100644 --- a/theories/common/Pipeline_utils.v +++ b/theories/common/Pipeline_utils.v @@ -19,6 +19,7 @@ Open Scope bs_scope. (* Compiler options *) Record Options := { erasure_config : erasure_configuration; + inductives_mapping : EProgram.inductives_mapping; (* Mapping for inductives, set by global declarations in the plugin *) direct : bool; (* direct or CPS code *) c_args : nat; (* numbers of C arguments *) anf_conf : nat; (* for different ANF pipeline configs. For development purposes *)