From 0f0ad1ff17d226b4bd6832f6bf8bacc7dcdd09f0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 29 Jan 2024 17:19:04 +0100 Subject: [PATCH 01/11] Implement dynamic linking of compiled certicoq code --- .gitignore | 1 + .vscode/CertiCoq.code-workspace | 6 +- benchmarks/test_primfloat.v | 6 +- benchmarks/test_primitive.v | 3 +- cplugin/_CoqProject | 2 - plugin/CoqMsgFFI.v | 2 +- plugin/Makefile.local | 10 +- plugin/Makefile.local-late | 4 + plugin/certicoq.ml | 546 +++++++++++++++++++++++- plugin/certicoq.mli | 7 + plugin/g_certicoq.mlg | 12 + plugin/get_ordinal.c | 12 + plugin/get_ordinal.h | 4 + plugin/runtime/Makefile | 22 +- plugin/runtime/certicoq_run.c | 27 ++ plugin/runtime/certicoq_run.h | 3 + plugin/runtime/certicoq_run_main.c | 4 - plugin/runtime/certicoq_run_wrapper.ml | 17 + plugin/runtime/certicoq_run_wrapper.mli | 2 + plugin/runtime/coq_ffi.c | 61 +++ plugin/runtime/coq_ffi.h | 6 + plugin/test_certicoq_eval.v | 46 ++ 22 files changed, 765 insertions(+), 38 deletions(-) create mode 100644 plugin/Makefile.local-late create mode 100644 plugin/get_ordinal.c create mode 100644 plugin/get_ordinal.h create mode 100644 plugin/runtime/certicoq_run.c create mode 100644 plugin/runtime/certicoq_run.h create mode 100644 plugin/runtime/certicoq_run_wrapper.ml create mode 100644 plugin/runtime/certicoq_run_wrapper.mli create mode 100644 plugin/runtime/coq_ffi.c create mode 100644 plugin/runtime/coq_ffi.h create mode 100644 plugin/test_certicoq_eval.v diff --git a/.gitignore b/.gitignore index 8927ccd8..f240986b 100644 --- a/.gitignore +++ b/.gitignore @@ -130,3 +130,4 @@ bootstrap/certicoqc/META bootstrap/certicoqchk/META bootstrap/certicoqc*/glue.c bootstrap/certicoqc*/glue.h +plugin/.merlin diff --git a/.vscode/CertiCoq.code-workspace b/.vscode/CertiCoq.code-workspace index 9391c9c3..c5c7712c 100644 --- a/.vscode/CertiCoq.code-workspace +++ b/.vscode/CertiCoq.code-workspace @@ -6,6 +6,10 @@ ], "settings": { "coqtop.binPath": "_opam/bin", - "coqtop.args": [] + "coqtop.args": [], + "ocaml.sandbox": { + "kind": "opam", + "switch": "coq817" + } } } diff --git a/benchmarks/test_primfloat.v b/benchmarks/test_primfloat.v index d1c64539..bfd6023a 100644 --- a/benchmarks/test_primfloat.v +++ b/benchmarks/test_primfloat.v @@ -1,6 +1,6 @@ From CertiCoq.Plugin Require Import CertiCoq. -From MetaCoq Require Import utils. +From MetaCoq.Utils Require Import utils. From CertiCoq.Common Require Import Pipeline_utils. Open Scope bs_scope. @@ -14,7 +14,7 @@ Definition string_of_bool b := #[export] Instance bool_show : Show bool := string_of_bool. #[export] Instance list_show {A} {SA : Show A} : Show (list A) := string_of_list show. -From MetaCoq Require Import Primitive. +From MetaCoq.Common Require Import Primitive. From Coq Require Import PrimFloat PrimInt63. #[export] Instance float_show : Show PrimFloat.float := string_of_float. #[export] Instance prim_int_show : Show PrimInt63.int := string_of_prim_int. @@ -39,4 +39,6 @@ Definition certicoqc2 := coq_msg_info (show (0%float == (-0)%float)). Time Eval compute in certicoqc2. + +Set Warnings "-primitive-turned-into-axiom". Time CertiCoq Run certicoqc2. \ No newline at end of file diff --git a/benchmarks/test_primitive.v b/benchmarks/test_primitive.v index fb63bd20..1450347b 100644 --- a/benchmarks/test_primitive.v +++ b/benchmarks/test_primitive.v @@ -1,4 +1,5 @@ -From MetaCoq Require Import bytestring MCString Primitive. +From MetaCoq.Utils Require Import bytestring MCString. +From MetaCoq.Common Require Import Primitive. From CertiCoq.Plugin Require Import CertiCoq. From Coq Require Import Uint63 ZArith. Open Scope bs. diff --git a/cplugin/_CoqProject b/cplugin/_CoqProject index 7e557737..382a2724 100644 --- a/cplugin/_CoqProject +++ b/cplugin/_CoqProject @@ -468,5 +468,3 @@ extraction/zbool.ml extraction/zbool.mli extraction/zpower.ml extraction/zpower.mli -extraction/optionMonad.mli -extraction/optionMonad.ml diff --git a/plugin/CoqMsgFFI.v b/plugin/CoqMsgFFI.v index 445a02c8..e246416d 100644 --- a/plugin/CoqMsgFFI.v +++ b/plugin/CoqMsgFFI.v @@ -11,4 +11,4 @@ CertiCoq Register [ coq_msg_notice => "coq_msg_notice", coq_msg_debug => "coq_msg_debug", coq_user_error => "coq_user_error" ] -Include [ "coq_c_ffi.h" as library ]. +Include [ "coq_ffi.h" as library ]. diff --git a/plugin/Makefile.local b/plugin/Makefile.local index 70c4d4ce..08f2550c 100644 --- a/plugin/Makefile.local +++ b/plugin/Makefile.local @@ -8,8 +8,14 @@ CAMLFLAGS+=-w -39 # Unused rec flagss CAMLFLAGS+=-w -20 # Unused arguments CAMLFLAGS+=-w -60 # Unused functor arguments CAMLFLAGS+=-w -8 # Non-exhaustive matches produced by extraction +CAMLFLAGS+=-w -37 # Unused constructor -CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims +CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims,inspect + +CC=$(shell which gcc || which clang-11) merlin-hook:: - $(HIDE)echo 'FLG $(OPENS)' >> .merlin \ No newline at end of file + $(HIDE)echo 'FLG $(OPENS)' >> .merlin + +get_ordinal.o: get_ordinal.c + $(CC) -c -o $@ -I runtime $< diff --git a/plugin/Makefile.local-late b/plugin/Makefile.local-late new file mode 100644 index 00000000..6c6f7343 --- /dev/null +++ b/plugin/Makefile.local-late @@ -0,0 +1,4 @@ +# CAMLOPTLINK = "$(OCAMLFIND)" opt -linkall get_ordinal.o + +certicoq_plugin.cmxa: certicoq_plugin.cmx + $(HIDE)$(TIMER) $(CAMLOPTLINK) get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index 8ab0fba1..a21a3c48 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -3,16 +3,318 @@ (* Copyright (c) 2017 *) (**********************************************************************) -open Pp open Printer open Metacoq_template_plugin.Ast_quoter open ExceptionMonad open AstCommon open Plugin_utils +external get_unboxed_ordinal : Obj.t -> int = "get_unboxed_ordinal" +external get_boxed_ordinal : Obj.t -> int = "get_boxed_ordinal" + +module Value = struct + open Printf + +type t = Obj.t + +let compare = compare +let equal = (==) +let hash = Hashtbl.hash + +type tag = + | Lazy + | Closure + | Object + | Infix + | Forward + | Block + | Abstract + | String + | Double + | Double_array + | Custom + | Int + | Out_of_heap + | Unaligned + +type custom = + | Custom_nativeint of nativeint + | Custom_int32 of int32 + | Custom_int64 of int64 + | Custom_bigarray + | Custom_channel + | Custom_unknown + | Not_custom + +(* external bits : t -> nativeint = "inspect_bits" *) + +let hex_digits = "0123456789ABCDEF" + +let dec_of_bits v = + sprintf "%nd" v + +let hex_of_bits v = + let (lsr) = Nativeint.shift_right in + let (land) = Nativeint.logand in + let ndig = Nativeint.size / 4 in + let b = Buffer.create (2 + ndig + 1) in + Buffer.add_string b "0x"; + for i = ndig - 1 downto 0 do + let d = (v lsr (i * 4)) land 0xFn in + Buffer.add_char b hex_digits.[Nativeint.to_int d] + done; + Buffer.contents b + +let bin_of_bits v = + let (lsr) = Nativeint.shift_right in + let (land) = Nativeint.logand in + let ndig = Nativeint.size in + let b = Buffer.create (2 + ndig + 1) in + (* three seems reasonable, prefix and maybe null? *) + Buffer.add_string b "0b"; + for i = Sys.word_size - 1 downto 0 do + let d = (v lsr i) land 1n in + Buffer.add_string b (if d = 1n then "1" else "0") + done; + Buffer.contents b + +(* let bits_to_string ?(base=`Hex) v = + let bs = bits v in + match base with + | `Dec -> dec_of_bits bs + | `Hex -> hex_of_bits bs + | `Bin -> bin_of_bits bs *) + +(* external custom_identifier : t -> string = "inspect_custom_id" + +external custom_has_finalize : t -> bool = "inspect_custom_has_finalize" +external custom_has_compare : t -> bool = "inspect_custom_has_compare" +external custom_has_hash : t -> bool = "inspect_custom_has_hash" +external custom_has_serialize : t -> bool = "inspect_custom_has_serialize" +external custom_has_deserialize : t -> bool = "inspect_custom_has_deserialize" *) + +(* let custom_ops_info r = + sprintf "%c%c%c%c%c" + (if custom_has_finalize r then 'F' else '-') + (if custom_has_compare r then 'C' else '-') + (if custom_has_hash r then 'H' else '-') + (if custom_has_serialize r then 'S' else '-') + (if custom_has_deserialize r then 'D' else '-') *) + +let nativeint_id = "_n" +let int32_id = "_i" +let int64_id = "_j" +let bigarray_id = "_bigarray" +let channel_id = "_chan" + +module TagSet = +struct + include Set.Make(struct type t = tag let compare = compare end) + + let of_list tlist = + List.fold_left (fun s t -> add t s) empty tlist + + let all = + of_list [ + Lazy; + Closure; + Object; + Infix; + Forward; + Block; + Abstract; + String; + Double; + Double_array; + Custom; + Int; + Out_of_heap; + Unaligned; + ] +end + +(* Make sure the known custom identifiers are in sync. *) +let _ = + let rnat = Obj.repr 0n and ri32 = Obj.repr 0l and ri64 = Obj.repr 0L in + assert (Obj.tag rnat = Obj.custom_tag); + assert (Obj.tag ri32 = Obj.custom_tag); + assert (Obj.tag ri64 = Obj.custom_tag); + (* assert (nativeint_id = custom_identifier rnat); + assert (int32_id = custom_identifier ri32); + assert (int64_id = custom_identifier ri64); + (* assert (bigarray_id = custom_identifier ...); *) + assert (channel_id = custom_identifier (Obj.repr stdout)); *) + () + +let custom_value r = + if Obj.tag r = Obj.custom_tag then ( + + Custom_unknown + ) + else + Not_custom + +let custom_is_int r = + match custom_value r with + | Custom_nativeint _ -> false + | Custom_int32 _ -> true + | Custom_int64 _ -> true + | _ -> false + +(* Matching an integer value should be faster than a series of if + statements. + That's why all these assertions are here, to make sure + that the integer literals used in the match statement actually + correspond to the tags defined by the Obj module. *) +let _ = + assert (Obj.lazy_tag = 246); + assert (Obj.closure_tag = 247); + assert (Obj.object_tag = 248); + assert (Obj.infix_tag = 249); + assert (Obj.forward_tag = 250); + assert (Obj.no_scan_tag = 251); + assert (Obj.abstract_tag = 251); + assert (Obj.string_tag = 252); + assert (Obj.double_tag = 253); + assert (Obj.double_array_tag = 254); + assert (Obj.custom_tag = 255); + assert (Obj.int_tag = 1000); + assert (Obj.out_of_heap_tag = 1001); + assert (Obj.unaligned_tag = 1002); + () + +(* Slower and safer. +let value_tag r = + match tag r with + | x when x = lazy_tag -> Lazy + | x when x = closure_tag -> Closure + | x when x = object_tag -> Object + | x when x = infix_tag -> Infix + | x when x = forward_tag -> Forward + | x when x < no_scan_tag -> Block + | x when x = abstract_tag -> Abstract + | x when x = string_tag -> String + | x when x = double_tag -> Double + | x when x = double_array_tag -> Double_array + | x when x = custom_tag -> Custom + | x when x = int_tag -> Int + | x when x = out_of_heap_tag -> Out_of_heap + | x when x = unaligned_tag -> Unaligned + | x -> failwith (sprintf "OCaml value with unknown tag = %d" x) +*) + +(* Faster but more dangerous *) +let tag r = + match Obj.tag r with + | x when x < 246 -> Block + | 246 -> Lazy + | 247 -> Closure + | 248 -> Object + | 249 -> Infix + | 250 -> Forward + | 251 -> Abstract + | 252 -> String + | 253 -> Double + | 254 -> Double_array + | 255 -> Custom + | 1000 -> Int + | 1001 -> Out_of_heap + | 1002 -> Unaligned + | x -> failwith (sprintf "OCaml value with unknown tag = %d" x) + +(* Slower? and safer +let is_in_heap r = + let x = Obj.tag r in + not (x = Obj.int_tag || x = Obj.out_of_heap_tag || x = Obj.unaligned_tag) +*) + +(* Faster but more dangerous *) +let is_in_heap r = + let x = Obj.tag r in + x < 1000 || 1002 < x + +let heap_words r = + if is_in_heap r then Obj.size r else 0 + +let mnemonic r = + match tag r with + | Lazy -> "LAZY" + | Closure -> "CLOS" + | Object -> "OBJ" + | Infix -> "INFX" + | Forward -> "FWD" + | Block -> "BLK" + | Abstract -> "ABST" + | String -> "STR" + | Double -> "DBL" + | Double_array -> "DBLA" + | Custom -> "CUST" + | Int -> "INT" + | Out_of_heap -> "OADR" + | Unaligned -> "UADR" + +let mnemonic_unknown = + "????" + +let abbrev r = + match tag r with + | Lazy + | Closure + | Object + | Infix + | Forward + | Block + | Double_array + | String + | Abstract -> sprintf "%s#%d" (mnemonic r) (heap_words r) + | Double -> sprintf "%g" (Obj.magic r : float) + | Custom -> ( + match custom_value r with + | Custom_nativeint n -> sprintf "%ndn" n + | Custom_int32 i -> sprintf "%ldl" i + | Custom_int64 i -> sprintf "%LdL" i + | Custom_bigarray -> "Bigarray" + | Custom_channel -> "Channel" + | Custom_unknown -> sprintf "Unknown" + | Not_custom -> failwith "Value.description: should be a custom value" + ) + | Int -> string_of_int (Obj.magic r : int) + | Out_of_heap -> "Out_of_heap" + | Unaligned -> "Unaligned" + +let description r = + match tag r with + | Lazy -> "Lazy: #" ^ string_of_int (Obj.size r) + | Closure -> "Closure: #" ^ string_of_int (Obj.size r) + | Object -> "Object: #" ^ string_of_int (Obj.size r) + | Infix -> "Infix: #" ^ string_of_int (Obj.size r) + | Forward -> "Forward: #" ^ string_of_int (Obj.size r) + | Block -> sprintf "Block(%d): #%d" (Obj.tag r) (Obj.size r) + | Abstract -> "Abstract: #" ^ string_of_int (Obj.size r) + | String -> + let len = String.length (Obj.magic r : string) in + sprintf "String: %d char%s" len (if len > 1 then "s" else "") + | Double -> sprintf "Double: %g" (Obj.magic r : float) + | Double_array -> sprintf "Double_array: %d floats" (Array.length (Obj.magic r : float array)) + | Custom -> ( + match custom_value r with + | Custom_nativeint n -> sprintf "Nativeint: %nd" n + | Custom_int32 i -> sprintf "Int32: %ld" i + | Custom_int64 i -> sprintf "Int64: %Ld" i + | Custom_bigarray -> "Bigarray" + | Custom_channel -> "Channel" + | Custom_unknown -> sprintf "Custom:" + | Not_custom -> failwith "Value.description: should be a custom value" + ) + | Int -> sprintf "Int: %d" (Obj.magic r : int) + | Out_of_heap -> sprintf "Out_of_heap " + | Unaligned -> sprintf "Unaligned " + +end + (** Various Utils *) -let pr_string s = str (Caml_bytestring.caml_string_of_bytestring s) +let pr_string s = Pp.str (Caml_bytestring.caml_string_of_bytestring s) (* remove duplicates but preserve order, keep the leftmost element *) let nub (xs : 'a list) : 'a list = @@ -25,7 +327,7 @@ let rec coq_nat_of_int x = let debug_msg (flag : bool) (s : string) = if flag then - Feedback.msg_debug (str s) + Feedback.msg_debug (Pp.str s) else () (* Separate registration of primitive extraction *) @@ -58,6 +360,56 @@ let register (prims : prim list) (imports : import list) : unit = let get_global_prims () = fst !global_registers let get_global_includes () = snd !global_registers +(* Support for dynamically-linked certicoq-compiled programs *) +type certicoq_run_function = Ast0.Env.global_env -> typ:Ast0.term -> Obj.t + +let certicoq_run_functions = + Summary.ref ~name:"CertiCoq Run Functions Table" + (CString.Map.empty : certicoq_run_function CString.Map.t) + +let certicoq_run_functions_name = "certicoq-run-functions-registration" + +let cache_certicoq_run_function (s, fn) = + let fns = !certicoq_run_functions in + certicoq_run_functions := CString.Map.add s fn fns + +let certicoq_run_function_input = + let open Libobject in + declare_object + (global_object_nodischarge certicoq_run_functions_name + ~cache:(fun r -> cache_certicoq_run_function r) + ~subst:None) + +let register_certicoq_run s fn = + Lib.add_leaf (certicoq_run_function_input (s, fn)) + +let run_certicoq_run s = + try CString.Map.find s !certicoq_run_functions + with Not_found -> CErrors.user_err Pp.(str"Could not find certicoq run function associated to " ++ str s) + +(** Coq FFI: message channels and raising user errors. *) + +let coq_msg_info s = + let s = Caml_bytestring.caml_string_of_bytestring s in + Feedback.msg_info (Pp.str s) + +let _ = Callback.register "coq_msg_info" coq_msg_info + +let coq_msg_debug s = + Feedback.msg_debug Pp.(str (Caml_bytestring.caml_string_of_bytestring s)) + +let _ = Callback.register "coq_msg_debug" coq_msg_debug + +let coq_msg_notice s = + Feedback.msg_notice Pp.(str (Caml_bytestring.caml_string_of_bytestring s)) + +let _ = Callback.register "coq_msg_notice" coq_msg_notice + +let coq_user_error s = + CErrors.user_err Pp.(str (Caml_bytestring.caml_string_of_bytestring s)) + +let _ = Callback.register "coq_user_error" coq_user_error + (** Compilation Command Arguments *) type command_args = @@ -114,12 +466,10 @@ let check_build_dir d = let isdir = try Unix.((stat d).st_kind = S_DIR) with Unix.Unix_error (Unix.ENOENT, _, _) -> - CErrors.user_err ~hdr:"pipeline" - Pp.(str "Could not compile: build directory " ++ str d ++ str " not found.") + CErrors.user_err Pp.(str "Could not compile: build directory " ++ str d ++ str " not found.") in if not isdir then - CErrors.user_err ~hdr:"pipeline" - Pp.(str "Could not compile: " ++ str d ++ str " is not a directory.") + CErrors.user_err Pp.(str "Could not compile: " ++ str d ++ str " is not a directory.") else d let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ident) * bool) list) (fname : string) : options = @@ -166,7 +516,7 @@ let make_pipeline_options (opts : options) = let get_name (gr : Names.GlobRef.t) : string = match gr with | Names.GlobRef.ConstRef c -> Names.KerName.to_string (Names.Constant.canonical c) - | _ -> CErrors.user_err ~hdr:"template-coq" (Printer.pr_global gr ++ str " is not a constant definition") + | _ -> CErrors.user_err Pp.(Printer.pr_global gr ++ str " is not a constant definition") (* Quote Coq term *) @@ -255,13 +605,13 @@ module CompileFunctor (CI : CompilerInterface) = struct | (CompM.Err s, dbg) -> debug_msg debug "Pipeline debug:"; debug_msg debug (string_of_bytestring dbg); - CErrors.user_err ~hdr:"pipeline" (str "Could not compile: " ++ (pr_string s) ++ str "\n") + CErrors.user_err Pp.(str "Could not compile: " ++ (pr_string s) ++ str "\n") (* Generate glue code for the compiled program *) let generate_glue (standalone : bool) opts globs = if standalone && opts.filename = "" then - CErrors.user_err ~hdr:"glue-code" (str "You need to provide a file name with the -file option.") + CErrors.user_err Pp.(str "You need to provide a file name with the -file option.") else let debug = opts.debug in let options = make_pipeline_options opts in @@ -287,7 +637,7 @@ module CompileFunctor (CI : CompilerInterface) = struct let time = (Unix.gettimeofday() -. time) in debug_msg debug (Printf.sprintf "Printed glue code to file %s in %f s.." cstr time) | CompM.Err s -> - CErrors.user_err ~hdr:"glue-code" (str "Could not generate glue code: " ++ pr_string s)) + CErrors.user_err Pp.(str "Could not generate glue code: " ++ pr_string s)) let compile_only (opts : options) (gr : Names.GlobRef.t) (imports : import list) : unit = let term = quote opts gr in @@ -297,8 +647,8 @@ module CompileFunctor (CI : CompilerInterface) = struct let term = quote opts gr in generate_glue true opts (Ast0.Env.declarations (fst (Obj.magic term))) - let compiler_executable debug = - let whichcmd = Unix.open_process_in "which gcc || which clang-11" in + let find_executable debug cmd = + let whichcmd = Unix.open_process_in cmd in let result = try Stdlib.input_line whichcmd with End_of_file -> "" @@ -310,6 +660,8 @@ module CompileFunctor (CI : CompilerInterface) = struct result | _ -> failwith "Compiler not found" + let compiler_executable debug = find_executable debug "which gcc || which clang-11" + type line = | EOF | Info of string @@ -359,10 +711,10 @@ module CompileFunctor (CI : CompilerInterface) = struct in let imports' = List.concat (List.map (fun i -> match i with - | FromAbsolutePath s -> [s] - | FromRelativePath s -> [s] - | _ -> []) imports) in - let l = make_rt_file "certicoq_run_main.o" :: List.map oname imports' in + | FromAbsolutePath s -> [oname s] + | FromRelativePath s -> [oname s] + | FromLibrary s -> [make_rt_file (oname s)]) imports) in + let l = make_rt_file "certicoq_run_main.o" :: imports' in String.concat " " l in let gc_stack_o = make_rt_file "gc_stack.o" in @@ -383,6 +735,158 @@ module CompileFunctor (CI : CompilerInterface) = struct | 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 ocamlfind_executable _debug = + "_opam/bin/ocamlfind" + (* find_executable debug "which ocamlfind" *) + + type reifyable_type = + | IsInductive of Names.inductive * Univ.Instance.t * Constr.t list + | IsPrimitive of Names.Constant.t * Univ.Instance.t + + let find_nth_constant n ar = + let open Inductiveops in + let rec aux i const = + if Array.length ar <= i then raise Not_found + else if CList.is_empty ar.(i).cs_args then (* FIXME lets in constructors *) + if const = n then i + else aux (i + 1) (const + 1) + else aux (i + 1) const + in aux 0 0 + + let find_nth_non_constant n ar = + let open Inductiveops in + let rec aux i nconst = + if Array.length ar <= i then raise Not_found + else if not (CList.is_empty ar.(i).cs_args) then + if nconst = n then i + else aux (i + 1) (nconst + 1) + else aux (i + 1) nconst + in aux 0 0 + + let check_reifyable env sigma ty = + (* We might have bound universes though. It's fine! *) + try let (hd, u), args = Inductiveops.find_inductive env sigma ty in + IsInductive (hd, EConstr.EInstance.kind sigma u, args) + with Not_found -> + match EConstr.kind sigma (Reductionops.whd_all env sigma ty) with + | Const (c, u) when Environ.is_primitive_type env c -> + IsPrimitive (c, EConstr.EInstance.kind sigma u) + | _ -> CErrors.user_err + Pp.(str"Cannot reify values of non-inductive or non-primitive type: " ++ + Printer.pr_econstr_env env sigma ty) + + let reify debug env sigma ty v : Constr.t = + let open Declarations in + let rec aux ty v = + match ty with + | IsInductive (hd, u, args) -> + let open Inductive in + let open Inductiveops in + let spec = lookup_mind_specif env hd in + let indfam = make_ind_family ((hd, u), args) in + let npars = inductive_params spec in + let params, _indices = CList.chop npars args in + let cstrs = get_constructors env indfam in + let () = debug_msg true (Printf.sprintf "Reifying inductive value") in + if Obj.is_block v then + let () = debug_msg true (Printf.sprintf "Reifying constructor block") in + let ord = get_boxed_ordinal v in + (*if not (0 <= otag && otag < Obj.no_scan_tag) thenm + CErrors.user_err Pp.(str "reify: Unexpected value tag: " ++ int otag); *) + let () = debug_msg debug (Printf.sprintf "Reifying constructor block of tag %i" ord) in + let coqidx = find_nth_non_constant ord cstrs in + let cstr = cstrs.(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 -> + let argty = check_reifyable env sigma + (EConstr.of_constr (Context.Rel.Declaration.get_type decl)) in + aux argty v) (List.rev ctx) vargs in + Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) (params @ args') + else (* Constant constructor *) + let () = debug_msg debug (Printf.sprintf "Reifying constant constructor") in + let ord = (Obj.magic v : int) in + let () = debug_msg debug (Printf.sprintf "Reifying constant constructor: %i" ord) in + let coqidx = find_nth_constant ord cstrs in + let () = debug_msg 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) -> + if Environ.is_array_type env c then + CErrors.user_err Pp.(str "Primitive arrays are not supported yet") + else if Environ.is_float64_type env c then + Constr.mkFloat (Obj.magic v) + else if Environ.is_int63_type env c then + Constr.mkInt (Obj.magic v) + else CErrors.user_err Pp.(str "Unsupported primitive type") + in aux ty v + + let compile_shared_C opts gr imports = + let prog = quote opts gr in + let env = Global.env () in + let sigma, tyinfo = + let sigma = Evd.from_env env in + let sigma, frgr = Evd.fresh_global env sigma gr in + let sigma, ty = Typing.type_of env sigma frgr in + assert (Evd.is_empty sigma); + sigma, check_reifyable env sigma ty + in + let () = compile opts (Obj.magic prog) imports in + let () = compile_only opts gr imports in + let imports = get_global_includes () @ imports in + let debug = opts.debug in + let fname = opts.filename in + let suff = opts.ext in + let name = make_fname opts (fname ^ suff) in + let compiler = compiler_executable debug in + let ocamlfind = ocamlfind_executable debug in + let rt_dir = runtime_dir () in + let cmd = + Printf.sprintf "%s -Wno-everything -g -I %s -I %s -c -o %s %s" + compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) (name ^ ".o") (name ^ ".c") + in + let importso = + let oname s = + assert (CString.is_suffix ".h" s); + String.sub s 0 (String.length s - 2) ^ ".o" + in + let imports' = List.concat (List.map (fun i -> + match i with + | FromAbsolutePath s -> [oname s] + | FromRelativePath s -> [oname s] + | FromLibrary s -> [make_rt_file (oname s)]) imports) in + let l = make_rt_file "certicoq_run.o" :: imports' in + String.concat " " l + in + let gc_stack_o = make_rt_file "gc_stack.o" in + debug_msg debug (Printf.sprintf "Executing command: %s" cmd); + let packages = ["coq-core"; "coq-core.plugins.ltac"; "coq-metacoq-template-ocaml"; + "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 = name ^ ".cmxs" in + let linkcmd = + Printf.sprintf "%s ocamlopt -shared -linkpkg -dontlink %s -thread -rectypes -package %s \ + -I . -I %s -o %s %s %s %s %s" + ocamlfind dontlink pkgs opts.build_dir shared_lib (make_rt_file "certicoq_run_wrapper.cmx") gc_stack_o (name ^ ".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" name); + Dynlink.loadfile_private shared_lib; + debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" name); + let result = run_certicoq_run "certicoq_run" (fst (Obj.magic prog)) ~typ:(snd (Obj.magic prog)) (* FIXME we should get the type*) in + debug_msg debug (Printf.sprintf "Running they dynamic linked program succeeded, reifying result"); + reify debug 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 print_to_file (s : string) (file : string) = let f = open_out file in Printf.fprintf f "%s\n" s; @@ -408,7 +912,7 @@ module CompileFunctor (CI : CompilerInterface) = struct | (CompM.Err s, dbg) -> debug_msg debug "Pipeline debug:"; debug_msg debug (string_of_bytestring dbg); - CErrors.user_err ~hdr:"show-ir" (str "Could not compile: " ++ (pr_string s) ++ str "\n") + CErrors.user_err Pp.(str "Could not compile: " ++ (pr_string s) ++ str "\n") (* Quote Coq inductive type *) @@ -421,8 +925,8 @@ module CompileFunctor (CI : CompilerInterface) = struct | Names.GlobRef.IndRef i -> let (mut, _) = i in Names.KerName.to_string (Names.MutInd.canonical mut) - | _ -> CErrors.user_err ~hdr:"template-coq" - (Printer.pr_global gr ++ str " is not an inductive type") in + | _ -> CErrors.user_err + Pp.(Printer.pr_global gr ++ str " is not an inductive type") in debug_msg debug "Quoting"; let time = Unix.gettimeofday() in let term = quote_term_rec ~bypass:true env sigma (EConstr.to_constr sigma c) in @@ -452,7 +956,7 @@ module CompileFunctor (CI : CompilerInterface) = struct let time = (Unix.gettimeofday() -. time) in debug_msg debug (Printf.sprintf "Printed FFI glue code to file in %f s.." time) | CompM.Err s -> - CErrors.user_err ~hdr:"ffi-glue-code" (str "Could not generate FFI glue code: " ++ pr_string s)) + CErrors.user_err Pp.(str "Could not generate FFI glue code: " ++ pr_string s)) let glue_command opts grs = let terms = grs |> List.rev diff --git a/plugin/certicoq.mli b/plugin/certicoq.mli index 68bdae6c..936e4c7d 100644 --- a/plugin/certicoq.mli +++ b/plugin/certicoq.mli @@ -67,6 +67,13 @@ 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 compile_shared_C : 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 + +(* Support for running dynamically linked certicoq-compiled programs *) +type certicoq_run_function = Ast0.Env.global_env -> typ:Ast0.term -> Obj.t + +val register_certicoq_run : string -> certicoq_run_function -> unit +val run_certicoq_run : string -> certicoq_run_function diff --git a/plugin/g_certicoq.mlg b/plugin/g_certicoq.mlg index 4c7ec4fe..e22b55d7 100644 --- a/plugin/g_certicoq.mlg +++ b/plugin/g_certicoq.mlg @@ -80,6 +80,18 @@ VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY let opts = Certicoq.make_options l [] (get_name gr) in Certicoq.compile_C opts gr [] } +| [ "CertiCoq" "Eval" cargs_list(l) global(gr) "Extract" "Constants" "[" extract_cnst_list_sep(cs, ",") "]" "Include" "[" cinclude_list_sep(imps, ",") "]" ] -> { + let gr = Nametab.global gr in + let opts = Certicoq.make_options l cs (get_name gr) in + let result = Certicoq.compile_shared_C opts gr imps in + Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result) + } +| [ "CertiCoq" "Eval" cargs_list(l) global(gr) ] -> { + let gr = Nametab.global gr in + let opts = Certicoq.make_options l [] (get_name gr) in + let result = Certicoq.compile_shared_C opts gr [] in + Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result) + } | [ "CertiCoq" "Show" "IR" cargs_list(l) global(gr) ] -> { let gr = Nametab.global gr in let opts = Certicoq.make_options l [] (get_name gr) in diff --git a/plugin/get_ordinal.c b/plugin/get_ordinal.c new file mode 100644 index 00000000..2aa6d73b --- /dev/null +++ b/plugin/get_ordinal.c @@ -0,0 +1,12 @@ +#include "gc_stack.h" + +value get_unboxed_ordinal(value $v) +{ + return Val_long($v); + // >> 1LLU); +} + +value get_boxed_ordinal(value $v) +{ + return Val_long(*((unsigned long long *) $v + 18446744073709551615LLU) & 255LLU); +} diff --git a/plugin/get_ordinal.h b/plugin/get_ordinal.h new file mode 100644 index 00000000..2e200c67 --- /dev/null +++ b/plugin/get_ordinal.h @@ -0,0 +1,4 @@ +#include "values.h" + +extern value get_unboxed_ordinal (value); +extern value get_boxed_ordinal (value); \ No newline at end of file diff --git a/plugin/runtime/Makefile b/plugin/runtime/Makefile index 9626fc49..944a1490 100644 --- a/plugin/runtime/Makefile +++ b/plugin/runtime/Makefile @@ -1,17 +1,31 @@ -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} +SRC = gc_stack.c certicoq_run_main.c certicoq_run.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 certicoq_run.h coq_c_ffi.h coq_ffi.h prim_int63.h prim_floats.h +LINKOPTS = -linkpkg -dontlink str,unix,dynlink,threads,zarith +MLIFILES = certicoq_run_wrapper.mli +MLFILES = certicoq_run_wrapper.ml + +TARGETS = ${SRC:.c=.o} ${MLFILES:.ml=.cmx} COQLIB = `coqc -where` DST = ${COQLIB}/user-contrib/CertiCoq/Plugin/runtime all: ${TARGETS} %.o: %.c - gcc -I . -O2 -g -fomit-frame-pointer -c -o $@ $+ + gcc -I . -I `ocamlc -where` -O2 -g -fomit-frame-pointer -c -o $@ $+ + +%.cmx: %.ml %.mli + ocamlfind ocamlopt -thread -rectypes -package coq-core,coq-core.plugins.ltac,coq-metacoq-template-ocaml,coq-certicoq.plugin -open Metacoq_template_plugin ${<:.ml=.mli} + ocamlfind ocamlopt -thread -rectypes ${LINKOPTS} -package coq-core,coq-core.plugins.ltac,coq-metacoq-template-ocaml,coq-certicoq.plugin -open Metacoq_template_plugin -I .. -c $< install: all install -d ${DST} install -m 0644 ${HEADERS} ${DST} install -m 0644 ${SRC} ${DST} + install -m 0644 ${MLFILES} ${MLIFILES} ${MLFILES:.ml=.o} ${DST} install -m 0644 ${TARGETS} ${DST} + +clean: + rm -f *.o *.cmx *.cmi + +.PHONY: certicoq_run_wrapper.cmi \ No newline at end of file diff --git a/plugin/runtime/certicoq_run.c b/plugin/runtime/certicoq_run.c new file mode 100644 index 00000000..312dc804 --- /dev/null +++ b/plugin/runtime/certicoq_run.c @@ -0,0 +1,27 @@ +#include +#include +#include "gc_stack.h" +#include +#include + +extern value body(struct thread_info *); + +extern value args[]; + +value certicoq_run() { + value val; + struct thread_info* tinfo; + clock_t start, end; + double msec, sec; + + start = clock(); + tinfo = make_tinfo(); + val = body(tinfo); + end = clock(); + + sec = (double)(end - start)/CLOCKS_PER_SEC; + msec = 1000*sec; + printf("Time taken %f seconds %f milliseconds\n", sec, msec); + + return val; +} diff --git a/plugin/runtime/certicoq_run.h b/plugin/runtime/certicoq_run.h new file mode 100644 index 00000000..7436ef24 --- /dev/null +++ b/plugin/runtime/certicoq_run.h @@ -0,0 +1,3 @@ +#include "values.h" + +extern value certicoq_run (); diff --git a/plugin/runtime/certicoq_run_main.c b/plugin/runtime/certicoq_run_main.c index 1aecfdcc..3f60ca24 100644 --- a/plugin/runtime/certicoq_run_main.c +++ b/plugin/runtime/certicoq_run_main.c @@ -7,10 +7,6 @@ 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; diff --git a/plugin/runtime/certicoq_run_wrapper.ml b/plugin/runtime/certicoq_run_wrapper.ml new file mode 100644 index 00000000..edf687e1 --- /dev/null +++ b/plugin/runtime/certicoq_run_wrapper.ml @@ -0,0 +1,17 @@ +open Tm_util +open Pp +open Universes0 +open BasicAst +open Ast0 + +external certicoq_run : unit -> Obj.t = "certicoq_run" + +let info s = Feedback.msg_info (Pp.str s) + +(** Run a program knowing it returns a value of the given type, + and reify the return value at that type. *) + +let run (env : Ast0.Env.global_env) ~(typ : Ast0.term) : Obj.t = + certicoq_run () + +let _ = Certicoq_plugin.Certicoq.register_certicoq_run "certicoq_run" (Obj.magic run) \ No newline at end of file diff --git a/plugin/runtime/certicoq_run_wrapper.mli b/plugin/runtime/certicoq_run_wrapper.mli new file mode 100644 index 00000000..86971341 --- /dev/null +++ b/plugin/runtime/certicoq_run_wrapper.mli @@ -0,0 +1,2 @@ + +val run : Ast0.Env.global_env -> typ:Ast0.term -> Obj.t diff --git a/plugin/runtime/coq_ffi.c b/plugin/runtime/coq_ffi.c new file mode 100644 index 00000000..8f6e6757 --- /dev/null +++ b/plugin/runtime/coq_ffi.c @@ -0,0 +1,61 @@ +#include + +void call_coq_msg_info(value msg) +{ + static const value * closure_f = NULL; + if (closure_f == NULL) { + /* First time around, look up by name */ + closure_f = caml_named_value("coq_msg_info"); + } + caml_callback(*closure_f, msg); +} + +value coq_msg_info(value msg) { + call_coq_msg_info(msg); + return Val_unit; +} + +void call_coq_user_error(value msg) +{ + static const value * closure_f = NULL; + if (closure_f == NULL) { + /* First time around, look up by name */ + closure_f = caml_named_value("coq_user_error"); + } + caml_callback(*closure_f, msg); +} + +value coq_user_error(value msg) { + call_coq_user_error(msg); + return Val_unit; +} + +void call_coq_msg_debug(value msg) +{ + static const value * closure_f = NULL; + if (closure_f == NULL) { + /* First time around, look up by name */ + closure_f = caml_named_value("coq_msg_debug"); + } + caml_callback(*closure_f, msg); +} + +value coq_msg_debug(value msg) { + call_coq_msg_debug(msg); + return Val_unit; +} + +void call_coq_msg_notice(value msg) +{ + static const value * closure_f = NULL; + if (closure_f == NULL) { + /* First time around, look up by name */ + closure_f = caml_named_value("coq_msg_notice"); + } + caml_callback(*closure_f, msg); +} + +value coq_msg_notice(value msg) { + call_coq_msg_notice(msg); + return Val_unit; +} diff --git a/plugin/runtime/coq_ffi.h b/plugin/runtime/coq_ffi.h new file mode 100644 index 00000000..895efe33 --- /dev/null +++ b/plugin/runtime/coq_ffi.h @@ -0,0 +1,6 @@ +#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/test_certicoq_eval.v b/plugin/test_certicoq_eval.v new file mode 100644 index 00000000..aef46b3f --- /dev/null +++ b/plugin/test_certicoq_eval.v @@ -0,0 +1,46 @@ + +From CertiCoq.Plugin Require Import CertiCoq. +From MetaCoq.Utils Require Import utils. + +Open Scope bs_scope. + +Class Show (A : Type) := show : A -> string. + +#[export] Instance nat_show : Show nat := string_of_nat. +Local Open Scope bs. +Definition string_of_bool b := + if (b : bool) then "true" else "false". +#[export] Instance bool_show : Show bool := string_of_bool. + +#[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. +#[export] Instance float_show : Show PrimFloat.float := string_of_float. +#[export] Instance prim_int_show : Show PrimInt63.int := string_of_prim_int. +Eval compute in 5.0%float. +(* Definition certicoqc2 := coq_msg_info (show 5%int63). *) +Import SpecFloat. +Definition string_of_specfloat (f : SpecFloat.spec_float) := + match f with + | S754_zero sign => if sign then "-0" else "0" + | S754_infinity sign => if sign then "-infinity" else "infinity" + | S754_nan => "nan" + | S754_finite sign p z => + let num := string_of_positive p ++ "p" ++ string_of_Z z in + if sign then "-" ++ num else num + end. + +#[export] Instance show_specfloat : Show SpecFloat.spec_float := string_of_specfloat. +#[export] Instance show_positive : Show positive := string_of_positive. +#[export] Instance show_Z : Show Z := string_of_Z. + +Definition certicoqc2 := 5. +Definition certicoqc3 := coq_msg_notice ("Hello world! " ++ show 100%nat). + (* show (0%float == (-0)%float)). *) + +Definition certicoqc4 := show (List.map S [26; 20]). + +Time Eval compute in certicoqc4. +Set Warnings "-primitive-turned-into-axiom". +Set Warnings "backtrace". +CertiCoq Eval -time certicoqc4. \ No newline at end of file From c91717e1908baa5c8fce21b8f904d6b40bca42e2 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 30 Jan 2024 16:50:05 +0100 Subject: [PATCH 02/11] Better setup for dynamic linking, generating the wrapper code on the fly. Avoid issue of loading multiple times the same module name dynamically, not supported by ocaml. We use a gensym to get fresh names. Also add an option to choose the name of "body" in the generated C code for added flexibility. --- .gitignore | 1 + plugin/certicoq.ml | 502 ++++++------------- plugin/certicoq.mli | 5 +- plugin/g_certicoq.mlg | 46 +- plugin/runtime/Makefile | 14 +- plugin/runtime/certicoq_run.c | 27 - plugin/runtime/certicoq_run.h | 3 - plugin/runtime/certicoq_run_wrapper.ml | 17 - plugin/runtime/certicoq_run_wrapper.mli | 2 - plugin/test_certicoq_eval.v | 11 +- theories/Codegen/LambdaANF_to_Clight.v | 5 +- theories/Codegen/LambdaANF_to_Clight_stack.v | 5 +- theories/Codegen/toplevel.v | 16 +- theories/Compiler/pipeline.v | 3 + theories/common/Pipeline_utils.v | 1 + 15 files changed, 233 insertions(+), 425 deletions(-) delete mode 100644 plugin/runtime/certicoq_run.c delete mode 100644 plugin/runtime/certicoq_run.h delete mode 100644 plugin/runtime/certicoq_run_wrapper.ml delete mode 100644 plugin/runtime/certicoq_run_wrapper.mli diff --git a/.gitignore b/.gitignore index f240986b..7f5b32f0 100644 --- a/.gitignore +++ b/.gitignore @@ -131,3 +131,4 @@ bootstrap/certicoqchk/META bootstrap/certicoqc*/glue.c bootstrap/certicoqc*/glue.h plugin/.merlin +_build \ No newline at end of file diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index a21a3c48..135ce8b1 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -9,309 +9,37 @@ open ExceptionMonad open AstCommon open Plugin_utils +(* Taken from Coq's increment_subscript, but works on strings rather than idents *) +let increment_subscript id = + let len = String.length id in + let rec add carrypos = + let c = id.[carrypos] in + if Util.is_digit c then + if Int.equal (Char.code c) (Char.code '9') then begin + assert (carrypos>0); + add (carrypos-1) + end + else begin + let newid = Bytes.of_string id in + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid carrypos (Char.chr (Char.code c + 1)); + newid + end + else begin + let newid = Bytes.of_string (id^"0") in + if carrypos < len-1 then begin + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid (carrypos+1) '1' + end; + newid + end + in String.of_bytes (add (len-1)) + +let debug_reify = CDebug.create ~name:"certicoq-reify" () + external get_unboxed_ordinal : Obj.t -> int = "get_unboxed_ordinal" external get_boxed_ordinal : Obj.t -> int = "get_boxed_ordinal" -module Value = struct - open Printf - -type t = Obj.t - -let compare = compare -let equal = (==) -let hash = Hashtbl.hash - -type tag = - | Lazy - | Closure - | Object - | Infix - | Forward - | Block - | Abstract - | String - | Double - | Double_array - | Custom - | Int - | Out_of_heap - | Unaligned - -type custom = - | Custom_nativeint of nativeint - | Custom_int32 of int32 - | Custom_int64 of int64 - | Custom_bigarray - | Custom_channel - | Custom_unknown - | Not_custom - -(* external bits : t -> nativeint = "inspect_bits" *) - -let hex_digits = "0123456789ABCDEF" - -let dec_of_bits v = - sprintf "%nd" v - -let hex_of_bits v = - let (lsr) = Nativeint.shift_right in - let (land) = Nativeint.logand in - let ndig = Nativeint.size / 4 in - let b = Buffer.create (2 + ndig + 1) in - Buffer.add_string b "0x"; - for i = ndig - 1 downto 0 do - let d = (v lsr (i * 4)) land 0xFn in - Buffer.add_char b hex_digits.[Nativeint.to_int d] - done; - Buffer.contents b - -let bin_of_bits v = - let (lsr) = Nativeint.shift_right in - let (land) = Nativeint.logand in - let ndig = Nativeint.size in - let b = Buffer.create (2 + ndig + 1) in - (* three seems reasonable, prefix and maybe null? *) - Buffer.add_string b "0b"; - for i = Sys.word_size - 1 downto 0 do - let d = (v lsr i) land 1n in - Buffer.add_string b (if d = 1n then "1" else "0") - done; - Buffer.contents b - -(* let bits_to_string ?(base=`Hex) v = - let bs = bits v in - match base with - | `Dec -> dec_of_bits bs - | `Hex -> hex_of_bits bs - | `Bin -> bin_of_bits bs *) - -(* external custom_identifier : t -> string = "inspect_custom_id" - -external custom_has_finalize : t -> bool = "inspect_custom_has_finalize" -external custom_has_compare : t -> bool = "inspect_custom_has_compare" -external custom_has_hash : t -> bool = "inspect_custom_has_hash" -external custom_has_serialize : t -> bool = "inspect_custom_has_serialize" -external custom_has_deserialize : t -> bool = "inspect_custom_has_deserialize" *) - -(* let custom_ops_info r = - sprintf "%c%c%c%c%c" - (if custom_has_finalize r then 'F' else '-') - (if custom_has_compare r then 'C' else '-') - (if custom_has_hash r then 'H' else '-') - (if custom_has_serialize r then 'S' else '-') - (if custom_has_deserialize r then 'D' else '-') *) - -let nativeint_id = "_n" -let int32_id = "_i" -let int64_id = "_j" -let bigarray_id = "_bigarray" -let channel_id = "_chan" - -module TagSet = -struct - include Set.Make(struct type t = tag let compare = compare end) - - let of_list tlist = - List.fold_left (fun s t -> add t s) empty tlist - - let all = - of_list [ - Lazy; - Closure; - Object; - Infix; - Forward; - Block; - Abstract; - String; - Double; - Double_array; - Custom; - Int; - Out_of_heap; - Unaligned; - ] -end - -(* Make sure the known custom identifiers are in sync. *) -let _ = - let rnat = Obj.repr 0n and ri32 = Obj.repr 0l and ri64 = Obj.repr 0L in - assert (Obj.tag rnat = Obj.custom_tag); - assert (Obj.tag ri32 = Obj.custom_tag); - assert (Obj.tag ri64 = Obj.custom_tag); - (* assert (nativeint_id = custom_identifier rnat); - assert (int32_id = custom_identifier ri32); - assert (int64_id = custom_identifier ri64); - (* assert (bigarray_id = custom_identifier ...); *) - assert (channel_id = custom_identifier (Obj.repr stdout)); *) - () - -let custom_value r = - if Obj.tag r = Obj.custom_tag then ( - - Custom_unknown - ) - else - Not_custom - -let custom_is_int r = - match custom_value r with - | Custom_nativeint _ -> false - | Custom_int32 _ -> true - | Custom_int64 _ -> true - | _ -> false - -(* Matching an integer value should be faster than a series of if - statements. - That's why all these assertions are here, to make sure - that the integer literals used in the match statement actually - correspond to the tags defined by the Obj module. *) -let _ = - assert (Obj.lazy_tag = 246); - assert (Obj.closure_tag = 247); - assert (Obj.object_tag = 248); - assert (Obj.infix_tag = 249); - assert (Obj.forward_tag = 250); - assert (Obj.no_scan_tag = 251); - assert (Obj.abstract_tag = 251); - assert (Obj.string_tag = 252); - assert (Obj.double_tag = 253); - assert (Obj.double_array_tag = 254); - assert (Obj.custom_tag = 255); - assert (Obj.int_tag = 1000); - assert (Obj.out_of_heap_tag = 1001); - assert (Obj.unaligned_tag = 1002); - () - -(* Slower and safer. -let value_tag r = - match tag r with - | x when x = lazy_tag -> Lazy - | x when x = closure_tag -> Closure - | x when x = object_tag -> Object - | x when x = infix_tag -> Infix - | x when x = forward_tag -> Forward - | x when x < no_scan_tag -> Block - | x when x = abstract_tag -> Abstract - | x when x = string_tag -> String - | x when x = double_tag -> Double - | x when x = double_array_tag -> Double_array - | x when x = custom_tag -> Custom - | x when x = int_tag -> Int - | x when x = out_of_heap_tag -> Out_of_heap - | x when x = unaligned_tag -> Unaligned - | x -> failwith (sprintf "OCaml value with unknown tag = %d" x) -*) - -(* Faster but more dangerous *) -let tag r = - match Obj.tag r with - | x when x < 246 -> Block - | 246 -> Lazy - | 247 -> Closure - | 248 -> Object - | 249 -> Infix - | 250 -> Forward - | 251 -> Abstract - | 252 -> String - | 253 -> Double - | 254 -> Double_array - | 255 -> Custom - | 1000 -> Int - | 1001 -> Out_of_heap - | 1002 -> Unaligned - | x -> failwith (sprintf "OCaml value with unknown tag = %d" x) - -(* Slower? and safer -let is_in_heap r = - let x = Obj.tag r in - not (x = Obj.int_tag || x = Obj.out_of_heap_tag || x = Obj.unaligned_tag) -*) - -(* Faster but more dangerous *) -let is_in_heap r = - let x = Obj.tag r in - x < 1000 || 1002 < x - -let heap_words r = - if is_in_heap r then Obj.size r else 0 - -let mnemonic r = - match tag r with - | Lazy -> "LAZY" - | Closure -> "CLOS" - | Object -> "OBJ" - | Infix -> "INFX" - | Forward -> "FWD" - | Block -> "BLK" - | Abstract -> "ABST" - | String -> "STR" - | Double -> "DBL" - | Double_array -> "DBLA" - | Custom -> "CUST" - | Int -> "INT" - | Out_of_heap -> "OADR" - | Unaligned -> "UADR" - -let mnemonic_unknown = - "????" - -let abbrev r = - match tag r with - | Lazy - | Closure - | Object - | Infix - | Forward - | Block - | Double_array - | String - | Abstract -> sprintf "%s#%d" (mnemonic r) (heap_words r) - | Double -> sprintf "%g" (Obj.magic r : float) - | Custom -> ( - match custom_value r with - | Custom_nativeint n -> sprintf "%ndn" n - | Custom_int32 i -> sprintf "%ldl" i - | Custom_int64 i -> sprintf "%LdL" i - | Custom_bigarray -> "Bigarray" - | Custom_channel -> "Channel" - | Custom_unknown -> sprintf "Unknown" - | Not_custom -> failwith "Value.description: should be a custom value" - ) - | Int -> string_of_int (Obj.magic r : int) - | Out_of_heap -> "Out_of_heap" - | Unaligned -> "Unaligned" - -let description r = - match tag r with - | Lazy -> "Lazy: #" ^ string_of_int (Obj.size r) - | Closure -> "Closure: #" ^ string_of_int (Obj.size r) - | Object -> "Object: #" ^ string_of_int (Obj.size r) - | Infix -> "Infix: #" ^ string_of_int (Obj.size r) - | Forward -> "Forward: #" ^ string_of_int (Obj.size r) - | Block -> sprintf "Block(%d): #%d" (Obj.tag r) (Obj.size r) - | Abstract -> "Abstract: #" ^ string_of_int (Obj.size r) - | String -> - let len = String.length (Obj.magic r : string) in - sprintf "String: %d char%s" len (if len > 1 then "s" else "") - | Double -> sprintf "Double: %g" (Obj.magic r : float) - | Double_array -> sprintf "Double_array: %d floats" (Array.length (Obj.magic r : float array)) - | Custom -> ( - match custom_value r with - | Custom_nativeint n -> sprintf "Nativeint: %nd" n - | Custom_int32 i -> sprintf "Int32: %ld" i - | Custom_int64 i -> sprintf "Int64: %Ld" i - | Custom_bigarray -> "Bigarray" - | Custom_channel -> "Channel" - | Custom_unknown -> sprintf "Custom:" - | Not_custom -> failwith "Value.description: should be a custom value" - ) - | Int -> sprintf "Int: %d" (Obj.magic r : int) - | Out_of_heap -> sprintf "Out_of_heap " - | Unaligned -> sprintf "Unaligned " - -end - (** Various Utils *) let pr_string s = Pp.str (Caml_bytestring.caml_string_of_bytestring s) @@ -361,7 +89,7 @@ let get_global_prims () = fst !global_registers let get_global_includes () = snd !global_registers (* Support for dynamically-linked certicoq-compiled programs *) -type certicoq_run_function = Ast0.Env.global_env -> typ:Ast0.term -> Obj.t +type certicoq_run_function = unit -> Obj.t let certicoq_run_functions = Summary.ref ~name:"CertiCoq Run Functions Table" @@ -369,8 +97,11 @@ let certicoq_run_functions = let certicoq_run_functions_name = "certicoq-run-functions-registration" +let all_run_functions = ref CString.Set.empty + let cache_certicoq_run_function (s, fn) = let fns = !certicoq_run_functions in + all_run_functions := CString.Set.add s !all_run_functions; certicoq_run_functions := CString.Map.add s fn fns let certicoq_run_function_input = @@ -381,6 +112,7 @@ let certicoq_run_function_input = ~subst:None) let register_certicoq_run s fn = + Feedback.msg_debug Pp.(str"Registering function " ++ str s ++ str " in certicoq_run"); Lib.add_leaf (certicoq_run_function_input (s, fn)) let run_certicoq_run s = @@ -425,6 +157,7 @@ type command_args = | EXT of string (* Filename extension to be appended to the file name *) | DEV of int (* For development purposes *) | PREFIX of string (* Prefix to add to the generated FFI fns, avoids clashes with C fns *) + | TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *) | FILENAME of string (* Name of the generated file *) type options = @@ -441,6 +174,7 @@ type options = ext : string; dev : int; prefix : string; + toplevel_name : string; prims : ((Kernames.kername * Kernames.ident) * bool) list; } @@ -458,6 +192,7 @@ let default_options : options = ext = ""; dev = 0; prefix = ""; + toplevel_name = "body"; prims = []; } @@ -490,6 +225,7 @@ let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ide | EXT s :: xs -> aux {o with ext = s} xs | DEV n :: xs -> aux {o with dev = n} xs | PREFIX s :: xs -> aux {o with prefix = s} xs + | TOPLEVEL_NAME s :: xs -> aux {o with toplevel_name = s} xs | FILENAME s :: xs -> aux {o with filename = s} xs in let opts = { default_options with filename = fname } in @@ -506,9 +242,10 @@ let make_pipeline_options (opts : options) = 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 (* Feedback.msg_debug Pp.(str"Prims: " ++ prlist_with_sep spc (fun ((x, y), wt) -> str (string_of_bytestring y)) prims); *) - Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix prims + Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix toplevel_name prims (** Main Compilation Functions *) @@ -520,12 +257,9 @@ let get_name (gr : Names.GlobRef.t) : string = (* Quote Coq term *) -let quote opts gr = +let quote_term opts env sigma c = let debug = opts.debug in let bypass = opts.bypass_qed in - let env = Global.env () in - let sigma = Evd.from_env env in - let sigma, c = Evd.fresh_global env sigma gr in debug_msg debug "Quoting"; let time = Unix.gettimeofday() in let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass env sigma (EConstr.to_constr sigma c) in @@ -533,6 +267,12 @@ let quote opts gr = debug_msg debug (Printf.sprintf "Finished quoting in %f s.. compiling to L7." time); term +let quote opts gr = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + quote_term opts env sigma c + (* Compile Quoted term with CertiCoq *) module type CompilerInterface = sig @@ -742,8 +482,15 @@ module CompileFunctor (CI : CompilerInterface) = struct type reifyable_type = | IsInductive of Names.inductive * Univ.Instance.t * Constr.t list - | IsPrimitive of Names.Constant.t * Univ.Instance.t + | IsPrimitive of Names.Constant.t * Univ.Instance.t * Constr.t list + + let type_of_reifyable_type = function + | IsInductive (hd, u, args) -> Term.applistc (Constr.mkIndU ((hd, u))) args + | IsPrimitive (c, u, args) -> Term.applistc (Constr.mkConstU ((c, u))) args + let pr_reifyable_type env sigma ty = + Printer.pr_constr_env env sigma (type_of_reifyable_type ty) + let find_nth_constant n ar = let open Inductiveops in let rec aux i const = @@ -769,15 +516,30 @@ module CompileFunctor (CI : CompilerInterface) = struct try let (hd, u), args = Inductiveops.find_inductive env sigma ty in IsInductive (hd, EConstr.EInstance.kind sigma u, args) with Not_found -> - match EConstr.kind sigma (Reductionops.whd_all env sigma ty) with + let hnf = Reductionops.whd_all env sigma ty in + let hd, args = EConstr.decompose_app sigma hnf in + match EConstr.kind sigma hd with | Const (c, u) when Environ.is_primitive_type env c -> - IsPrimitive (c, EConstr.EInstance.kind sigma u) + IsPrimitive (c, EConstr.EInstance.kind sigma u, List.map EConstr.Unsafe.to_constr args) | _ -> CErrors.user_err Pp.(str"Cannot reify values of non-inductive or non-primitive type: " ++ Printer.pr_econstr_env env sigma ty) - let reify debug env sigma ty v : Constr.t = + let ill_formed env sigma ty = + match ty with + | IsInductive _ -> + CErrors.anomaly ~label:"certicoq-reify-ill-formed" + Pp.(str "Ill-formed inductive value representation in CertiCoq's reification for type " ++ + pr_reifyable_type env sigma ty) + | IsPrimitive _ -> + CErrors.anomaly ~label:"certicoq-reify-ill-formed" + Pp.(str "Ill-formed primitive value representation in CertiCoq's reification for type " ++ + pr_reifyable_type env sigma ty) + + + let reify 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 = match ty with | IsInductive (hd, u, args) -> @@ -788,14 +550,15 @@ module CompileFunctor (CI : CompilerInterface) = struct let npars = inductive_params spec in let params, _indices = CList.chop npars args in let cstrs = get_constructors env indfam in - let () = debug_msg true (Printf.sprintf "Reifying inductive value") in + let () = debug (Printf.sprintf "Reifying inductive value") in if Obj.is_block v then - let () = debug_msg true (Printf.sprintf "Reifying constructor block") in + let () = debug (Printf.sprintf "Reifying constructor block") in let ord = get_boxed_ordinal v in - (*if not (0 <= otag && otag < Obj.no_scan_tag) thenm - CErrors.user_err Pp.(str "reify: Unexpected value tag: " ++ int otag); *) - let () = debug_msg debug (Printf.sprintf "Reifying constructor block of tag %i" ord) in - let coqidx = find_nth_non_constant ord cstrs in + let () = debug (Printf.sprintf "Reifying constructor block of tag %i" ord) in + let coqidx = + try find_nth_non_constant ord cstrs + with Not_found -> ill_formed env sigma ty + in let cstr = cstrs.(coqidx) in let ctx = Vars.smash_rel_context cstr.cs_args in let vargs = List.init (List.length ctx) (Obj.field v) in @@ -805,13 +568,16 @@ module CompileFunctor (CI : CompilerInterface) = struct aux argty v) (List.rev ctx) vargs in Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) (params @ args') else (* Constant constructor *) - let () = debug_msg debug (Printf.sprintf "Reifying constant constructor") in + let () = debug (Printf.sprintf "Reifying constant constructor") in let ord = (Obj.magic v : int) in - let () = debug_msg debug (Printf.sprintf "Reifying constant constructor: %i" ord) in - let coqidx = find_nth_constant ord cstrs in - let () = debug_msg debug (Printf.sprintf "Reifying constant constructor: %i is %i in Coq" ord coqidx) in + let () = debug (Printf.sprintf "Reifying constant constructor: %i" ord) in + let coqidx = + try find_nth_constant ord cstrs + with Not_found -> ill_formed env sigma ty + 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) -> + | IsPrimitive (c, u, _args) -> if Environ.is_array_type env c then CErrors.user_err Pp.(str "Primitive arrays are not supported yet") else if Environ.is_float64_type env c then @@ -821,29 +587,55 @@ module CompileFunctor (CI : CompilerInterface) = struct else CErrors.user_err Pp.(str "Unsupported primitive type") in aux ty v - let compile_shared_C opts gr imports = - let prog = quote opts gr in - let env = Global.env () in - let sigma, tyinfo = - let sigma = Evd.from_env env in - let sigma, frgr = Evd.fresh_global env sigma gr in - let sigma, ty = Typing.type_of env sigma frgr in - assert (Evd.is_empty sigma); - sigma, check_reifyable env sigma ty + let template name = + Printf.sprintf "\nvalue %s ()\n { struct thread_info* tinfo = make_tinfo(); return %s_body(tinfo); }\n" name name + let template_header name = + Printf.sprintf "#include \nextern value %s ();\n" name + + let write_c_driver opts name = + let fname = make_fname opts (name ^ ".c") in + let fhname = make_fname opts (name ^ ".h") in + let fd = Unix.(openfile fname [O_CREAT; O_APPEND; O_WRONLY] 0o640) in + let chan = Unix.out_channel_of_descr fd in + output_string chan (template name); + flush chan; + close_out chan; + let chan = open_out fhname in + output_string chan (template_header name); + flush chan; close_out chan; + fname + + let template_ocaml name = + Printf.sprintf "external %s : unit -> Obj.t = \"%s\"\nlet _ = Certicoq_plugin.Certicoq.register_certicoq_run \"%s\" (Obj.magic %s)" name name name name + + let write_ocaml_driver opts name = + let fname = make_fname opts (name ^ "_wrapper.ml") in + let chan = open_out fname in + output_string chan (template_ocaml name); + flush chan; close_out chan; fname + + let certicoq_eval_named opts env sigma id c imports = + let prog = quote_term opts env sigma c in + let tyinfo = + let ty = Retyping.get_type_of env sigma c in + (* assert (Evd.is_empty sigma); *) + check_reifyable env sigma ty in let () = compile opts (Obj.magic prog) imports in - let () = compile_only opts gr imports in + (* Write wrapping code *) + let c_driver = write_c_driver opts id in + let ocaml_driver = write_ocaml_driver opts id in let imports = get_global_includes () @ imports in let debug = opts.debug in - let fname = opts.filename in let suff = opts.ext in - let name = make_fname opts (fname ^ suff) in + let name = make_fname opts (id ^ suff) in let compiler = compiler_executable debug in let ocamlfind = ocamlfind_executable debug in let rt_dir = runtime_dir () in + let cmd = Printf.sprintf "%s -Wno-everything -g -I %s -I %s -c -o %s %s" - compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) (name ^ ".o") (name ^ ".c") + compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) (Filename.remove_extension c_driver ^ ".o") c_driver in let importso = let oname s = @@ -855,7 +647,7 @@ module CompileFunctor (CI : CompilerInterface) = struct | FromAbsolutePath s -> [oname s] | FromRelativePath s -> [oname s] | FromLibrary s -> [make_rt_file (oname s)]) imports) in - let l = make_rt_file "certicoq_run.o" :: imports' in + let l = imports' in String.concat " " l in let gc_stack_o = make_rt_file "gc_stack.o" in @@ -865,28 +657,48 @@ module CompileFunctor (CI : CompilerInterface) = struct 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 = name ^ ".cmxs" in + | Unix.WEXITED 0 -> + let shared_lib = name ^ ".cmxs" in let linkcmd = Printf.sprintf "%s ocamlopt -shared -linkpkg -dontlink %s -thread -rectypes -package %s \ - -I . -I %s -o %s %s %s %s %s" - ocamlfind dontlink pkgs opts.build_dir shared_lib (make_rt_file "certicoq_run_wrapper.cmx") gc_stack_o (name ^ ".o") importso + -I %s -I plugin -o %s %s %s %s %s" + ocamlfind dontlink pkgs opts.build_dir shared_lib ocaml_driver gc_stack_o (name ^ ".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" name); + debug_msg debug (Printf.sprintf "Compilation ran fine, linking compiled code for %s" id); Dynlink.loadfile_private shared_lib; - debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" name); - let result = run_certicoq_run "certicoq_run" (fst (Obj.magic prog)) ~typ:(snd (Obj.magic prog)) (* FIXME we should get the type*) in - debug_msg debug (Printf.sprintf "Running they dynamic linked program succeeded, reifying result"); - reify debug env sigma tyinfo result + debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" id); + let result = run_certicoq_run id () in + debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); + reify 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 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 + + let find_fresh s map = + Feedback.msg_debug Pp.(str "Looking for fresh " ++ str s ++ str " in " ++ prlist_with_sep spc str (CString.Set.elements map)); + let freshs = next_string_away_from s (fun s -> CString.Set.mem s map) in + Feedback.msg_debug Pp.(str "Found " ++ str freshs); + freshs + + let certicoq_eval opts env sigma c imports = + let fresh_name = find_fresh opts.filename !all_run_functions in + let opts = { opts with toplevel_name = fresh_name ^ "_body"; filename = fresh_name } in + certicoq_eval_named opts env sigma fresh_name c imports + + let compile_shared_C opts gr = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + certicoq_eval opts env sigma c + let print_to_file (s : string) (file : string) = let f = open_out file in Printf.fprintf f "%s\n" s; diff --git a/plugin/certicoq.mli b/plugin/certicoq.mli index 936e4c7d..b2c4996a 100644 --- a/plugin/certicoq.mli +++ b/plugin/certicoq.mli @@ -13,6 +13,7 @@ type command_args = | EXT of string (* Filename extension to be appended to the file name *) | DEV of int | PREFIX of string (* Prefix to add to the generated FFI fns, avoids clashes with C fns *) +| TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *) | FILENAME of string (* Name of the generated file *) type options = @@ -29,6 +30,7 @@ type options = ext : string; dev : int; prefix : string; + toplevel_name : string; prims : ((Kernames.kername * Kernames.ident) * bool) list; } @@ -71,9 +73,10 @@ val compile_shared_C : 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 certicoq_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 = Ast0.Env.global_env -> typ:Ast0.term -> Obj.t +type certicoq_run_function = unit -> Obj.t val register_certicoq_run : string -> certicoq_run_function -> unit val run_certicoq_run : string -> certicoq_run_function diff --git a/plugin/g_certicoq.mlg b/plugin/g_certicoq.mlg index e22b55d7..a7e6c9fb 100644 --- a/plugin/g_certicoq.mlg +++ b/plugin/g_certicoq.mlg @@ -3,16 +3,46 @@ DECLARE PLUGIN "coq-certicoq.plugin" { +open Names open Pp open Certicoq open Ltac_plugin open Stdarg open Pcoq.Prim open Plugin_utils +open Tacexpr +open Tacinterp +open Stdarg +open Tacarg +open Genredexpr + +(** Calling Ltac **) + +let ltac_lcall tac args = + let (location, name) = Loc.tag (Names.Id.of_string tac) + (* Loc.tag @@ Names.Id.of_string tac *) + in + CAst.make ?loc:location (Tacexpr.TacArg(Tacexpr.TacCall + (CAst.make (Locus.ArgVar (CAst.make ?loc:location name),args)))) + + +let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = + let fold arg (i, vars, lfun) = + let id = Names.Id.of_string ("x" ^ string_of_int i) in + let (l,n) = (Loc.tag id) in + let x = Reference (Locus.ArgVar (CAst.make ?loc:l n)) in + (succ i, x :: vars, Id.Map.add id arg lfun) + in + let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in + let lfun = Id.Map.add (Id.of_string "F") f lfun in + let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in + Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args) + +let to_ltac_val c = Tacinterp.Value.of_constr c } -VERNAC ARGUMENT EXTEND cargs +ARGUMENT EXTEND cargs | [ "-bypass_qed" ] -> { BYPASS_QED } | [ "-cps" ] -> { CPS } | [ "-time" ] -> { TIME } @@ -26,9 +56,9 @@ VERNAC ARGUMENT EXTEND cargs | [ "-dev" natural(n) ] -> { DEV(n) } | [ "-ext" string(s) ] -> { EXT(s) } | [ "-file" string(s) ] -> { FILENAME(s) } +| [ "-toplevel_name" string(s) ] -> { TOPLEVEL_NAME(s) } END - VERNAC ARGUMENT EXTEND extract_cnst | [ 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) } @@ -116,3 +146,15 @@ VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY Feedback.msg_info (str help_msg) } END + +TACTIC EXTEND CertiCoq_eval +| [ "certicoq_eval" 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 c' = Certicoq.certicoq_eval opts env sigma c [] in + ltac_apply tac (List.map to_ltac_val [EConstr.of_constr c']) + end } +END diff --git a/plugin/runtime/Makefile b/plugin/runtime/Makefile index 944a1490..3446532f 100644 --- a/plugin/runtime/Makefile +++ b/plugin/runtime/Makefile @@ -2,10 +2,7 @@ SRC = gc_stack.c certicoq_run_main.c certicoq_run.c coq_c_ffi.c coq_ffi.c prim_i HEADERS = m.h config.h values.h gc_stack.h certicoq_run_main.h certicoq_run.h coq_c_ffi.h coq_ffi.h prim_int63.h prim_floats.h LINKOPTS = -linkpkg -dontlink str,unix,dynlink,threads,zarith -MLIFILES = certicoq_run_wrapper.mli -MLFILES = certicoq_run_wrapper.ml - -TARGETS = ${SRC:.c=.o} ${MLFILES:.ml=.cmx} +TARGETS = ${SRC:.c=.o} COQLIB = `coqc -where` DST = ${COQLIB}/user-contrib/CertiCoq/Plugin/runtime @@ -14,18 +11,11 @@ all: ${TARGETS} %.o: %.c gcc -I . -I `ocamlc -where` -O2 -g -fomit-frame-pointer -c -o $@ $+ -%.cmx: %.ml %.mli - ocamlfind ocamlopt -thread -rectypes -package coq-core,coq-core.plugins.ltac,coq-metacoq-template-ocaml,coq-certicoq.plugin -open Metacoq_template_plugin ${<:.ml=.mli} - ocamlfind ocamlopt -thread -rectypes ${LINKOPTS} -package coq-core,coq-core.plugins.ltac,coq-metacoq-template-ocaml,coq-certicoq.plugin -open Metacoq_template_plugin -I .. -c $< - install: all install -d ${DST} install -m 0644 ${HEADERS} ${DST} install -m 0644 ${SRC} ${DST} - install -m 0644 ${MLFILES} ${MLIFILES} ${MLFILES:.ml=.o} ${DST} install -m 0644 ${TARGETS} ${DST} clean: - rm -f *.o *.cmx *.cmi - -.PHONY: certicoq_run_wrapper.cmi \ No newline at end of file + rm -f *.o diff --git a/plugin/runtime/certicoq_run.c b/plugin/runtime/certicoq_run.c deleted file mode 100644 index 312dc804..00000000 --- a/plugin/runtime/certicoq_run.c +++ /dev/null @@ -1,27 +0,0 @@ -#include -#include -#include "gc_stack.h" -#include -#include - -extern value body(struct thread_info *); - -extern value args[]; - -value certicoq_run() { - value val; - struct thread_info* tinfo; - clock_t start, end; - double msec, sec; - - start = clock(); - tinfo = make_tinfo(); - val = body(tinfo); - end = clock(); - - sec = (double)(end - start)/CLOCKS_PER_SEC; - msec = 1000*sec; - printf("Time taken %f seconds %f milliseconds\n", sec, msec); - - return val; -} diff --git a/plugin/runtime/certicoq_run.h b/plugin/runtime/certicoq_run.h deleted file mode 100644 index 7436ef24..00000000 --- a/plugin/runtime/certicoq_run.h +++ /dev/null @@ -1,3 +0,0 @@ -#include "values.h" - -extern value certicoq_run (); diff --git a/plugin/runtime/certicoq_run_wrapper.ml b/plugin/runtime/certicoq_run_wrapper.ml deleted file mode 100644 index edf687e1..00000000 --- a/plugin/runtime/certicoq_run_wrapper.ml +++ /dev/null @@ -1,17 +0,0 @@ -open Tm_util -open Pp -open Universes0 -open BasicAst -open Ast0 - -external certicoq_run : unit -> Obj.t = "certicoq_run" - -let info s = Feedback.msg_info (Pp.str s) - -(** Run a program knowing it returns a value of the given type, - and reify the return value at that type. *) - -let run (env : Ast0.Env.global_env) ~(typ : Ast0.term) : Obj.t = - certicoq_run () - -let _ = Certicoq_plugin.Certicoq.register_certicoq_run "certicoq_run" (Obj.magic run) \ No newline at end of file diff --git a/plugin/runtime/certicoq_run_wrapper.mli b/plugin/runtime/certicoq_run_wrapper.mli deleted file mode 100644 index 86971341..00000000 --- a/plugin/runtime/certicoq_run_wrapper.mli +++ /dev/null @@ -1,2 +0,0 @@ - -val run : Ast0.Env.global_env -> typ:Ast0.term -> Obj.t diff --git a/plugin/test_certicoq_eval.v b/plugin/test_certicoq_eval.v index aef46b3f..a8cfacc8 100644 --- a/plugin/test_certicoq_eval.v +++ b/plugin/test_certicoq_eval.v @@ -1,4 +1,4 @@ - +From CertiCoq.Plugin Require Import Loader. From CertiCoq.Plugin Require Import CertiCoq. From MetaCoq.Utils Require Import utils. @@ -17,8 +17,7 @@ From MetaCoq.Common Require Import Primitive. From Coq Require Import PrimFloat PrimInt63. #[export] Instance float_show : Show PrimFloat.float := string_of_float. #[export] Instance prim_int_show : Show PrimInt63.int := string_of_prim_int. -Eval compute in 5.0%float. -(* Definition certicoqc2 := coq_msg_info (show 5%int63). *) + Import SpecFloat. Definition string_of_specfloat (f : SpecFloat.spec_float) := match f with @@ -43,4 +42,8 @@ Definition certicoqc4 := show (List.map S [26; 20]). Time Eval compute in certicoqc4. Set Warnings "-primitive-turned-into-axiom". Set Warnings "backtrace". -CertiCoq Eval -time certicoqc4. \ No newline at end of file +(* CertiCoq Eval -time certicoqc4. *) + +Goal True. + intros. + certicoq_eval -build_dir "_build" certicoqc4 ltac:(fun c => assert (certicoqc4 = c) by reflexivity). \ No newline at end of file diff --git a/theories/Codegen/LambdaANF_to_Clight.v b/theories/Codegen/LambdaANF_to_Clight.v index b7e8ad6b..15099837 100644 --- a/theories/Codegen/LambdaANF_to_Clight.v +++ b/theories/Codegen/LambdaANF_to_Clight.v @@ -36,6 +36,7 @@ Variable (limitIdent : ident). Variable (gcIdent : ident). Variable (mainIdent : ident). Variable (bodyIdent : ident). +Variable (bodyName : string). Variable (threadInfIdent : ident). Variable (tinfIdent : ident). Variable (heapInfIdent : ident). @@ -1068,7 +1069,7 @@ Fixpoint make_extern_decls Definition body_external_decl : positive * globdef Clight.fundef type := let params := type_of_params ((tinfIdent, threadInf) :: nil) in - (bodyIdent, Gfun (External (EF_external (String.to_string "body") + (bodyIdent, Gfun (External (EF_external (String.to_string bodyName) (signature_of_type params Tvoid cc_default)) params Tvoid cc_default)). @@ -1352,7 +1353,7 @@ Definition add_inf_vars (nenv : name_env) : name_env := M.set limitIdent (nNamed "limit"%bs) ( M.set gcIdent (nNamed "garbage_collect"%bs) ( M.set mainIdent (nNamed "main"%bs) ( - M.set bodyIdent (nNamed "body"%bs) ( + M.set bodyIdent (nNamed bodyName%bs) ( M.set threadInfIdent (nNamed "thread_info"%bs) ( M.set tinfIdent (nNamed "tinfo"%bs) ( M.set heapInfIdent (nNamed "heap"%bs) ( diff --git a/theories/Codegen/LambdaANF_to_Clight_stack.v b/theories/Codegen/LambdaANF_to_Clight_stack.v index c7085e9d..952a4ace 100644 --- a/theories/Codegen/LambdaANF_to_Clight_stack.v +++ b/theories/Codegen/LambdaANF_to_Clight_stack.v @@ -43,6 +43,7 @@ Variable (limitIdent : ident). Variable (gcIdent : ident). Variable (mainIdent : ident). Variable (bodyIdent : ident). +Variable (bodyName : string). Variable (threadInfIdent : ident). Variable (tinfIdent : ident). Variable (heapInfIdent : ident). @@ -1066,7 +1067,7 @@ Fixpoint make_extern_decls Definition body_external_decl : positive * globdef Clight.fundef type := let params := type_of_params ((tinfIdent, threadInf) :: nil) in - (bodyIdent, Gfun (External (EF_external (String.to_string ("body"%bs)) + (bodyIdent, Gfun (External (EF_external (String.to_string bodyName) (signature_of_type params val cc_default)) params val cc_default)). @@ -1266,7 +1267,7 @@ Definition inf_vars := (limitIdent, (nNamed "limit"%bs)) :: (gcIdent, (nNamed "garbage_collect"%bs)) :: (mainIdent, (nNamed "main"%bs)) :: - (bodyIdent, (nNamed "body"%bs)) :: + (bodyIdent, (nNamed bodyName)) :: (threadInfIdent, (nNamed "thread_info"%bs)) :: (tinfIdent, (nNamed "tinfo"%bs)) :: (heapInfIdent, (nNamed "heap"%bs)) :: diff --git a/theories/Codegen/toplevel.v b/theories/Codegen/toplevel.v index b4f59ccd..46b8d2c0 100644 --- a/theories/Codegen/toplevel.v +++ b/theories/Codegen/toplevel.v @@ -38,10 +38,10 @@ Definition add_prim_names (prims : list (kername * string * bool * nat * positiv List.fold_left (fun map '(k, s, b, ar, p) => cps.M.set p (nNamed s) map) prims nenv. -Definition Clight_trans (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram := +Definition Clight_trans (bodyName : string) (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram := let '(_, p_env, cenv, ctag, itag, nenv, fenv, _, prog) := t in let p := LambdaANF_to_Clight.compile - argsIdent allocIdent limitIdent gcIdent mainIdent bodyIdent threadInfIdent + argsIdent allocIdent limitIdent gcIdent mainIdent bodyIdent bodyName threadInfIdent tinfIdent heapInfIdent numArgsIdent isptrIdent caseIdent args p_env prog cenv nenv in match p with @@ -52,19 +52,19 @@ Definition Clight_trans (prims : list (kername * string * bool * nat * positive) (* TODO unify with the one above, propagate errors *) -Definition Clight_trans_fast (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram := +Definition Clight_trans_fast (bodyName : string) (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram := let '(_, p_env, cenv, ctag, itag, nenv, fenv, _, prog) := t in let '(nenv, prog, head) := LambdaANF_to_Clight.compile_fast - argsIdent allocIdent limitIdent gcIdent mainIdent bodyIdent threadInfIdent + argsIdent allocIdent limitIdent gcIdent mainIdent bodyIdent bodyName threadInfIdent tinfIdent heapInfIdent numArgsIdent isptrIdent caseIdent args p_env prog cenv nenv in Ret (add_prim_names prims nenv, stripOption mainIdent prog, stripOption mainIdent head). -Definition Clight_trans_ANF (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram * string := +Definition Clight_trans_ANF bodyName (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram * string := let '(_, pr_env, cenv, ctag, itag, nenv, fenv, _, prog) := t in let '(p, str) := LambdaANF_to_Clight_stack.compile - argsIdent allocIdent nallocIdent limitIdent gcIdent mainIdent bodyIdent threadInfIdent + argsIdent allocIdent nallocIdent limitIdent gcIdent mainIdent bodyIdent bodyName threadInfIdent tinfIdent heapInfIdent numArgsIdent isptrIdent caseIdent resultIdent args pr_env @@ -85,6 +85,6 @@ Definition compile_Clight (prims : list (kername * string * bool * nat * positiv let args := c_args opts in let cps := negb (direct opts) in if cps then - LiftErrorCertiCoqTrans "Codegen" (Clight_trans prims args) s + LiftErrorCertiCoqTrans "Codegen" (Clight_trans opts.(body_name) prims args) s else - LiftErrorLogCertiCoqTrans "Codegen" (Clight_trans_ANF prims args) s. + LiftErrorLogCertiCoqTrans "Codegen" (Clight_trans_ANF opts.(body_name) prims args) s. diff --git a/theories/Compiler/pipeline.v b/theories/Compiler/pipeline.v index 761ad7fd..b877e2d3 100644 --- a/theories/Compiler/pipeline.v +++ b/theories/Compiler/pipeline.v @@ -143,6 +143,7 @@ Definition default_opts : Options := debug := false; dev := 0; Pipeline_utils.prefix := ""; + Pipeline_utils.body_name := "body"; prims := []; |}. @@ -155,6 +156,7 @@ Definition make_opts (debug : bool) (* Debug log *) (dev : nat) (* Extra flag for development purposes *) (prefix : string) (* Prefix for the FFI. Check why is this needed in the pipeline and not just the plugin *) + (toplevel_name : string) (* Name of the toplevel function ("body" by default) *) (prims : list (kername * string * bool)) (* list of extracted constants *) : Options := {| direct := negb cps; @@ -167,6 +169,7 @@ Definition make_opts debug := debug; dev := dev; Pipeline_utils.prefix := prefix; + Pipeline_utils.body_name := toplevel_name; prims := prims |}. diff --git a/theories/common/Pipeline_utils.v b/theories/common/Pipeline_utils.v index 2555cd35..da7a69a6 100644 --- a/theories/common/Pipeline_utils.v +++ b/theories/common/Pipeline_utils.v @@ -30,6 +30,7 @@ Record Options := dev : nat; (* for development purposes *) prefix : string; (* prefix to generated FFI *) + body_name : string; (* Name of the toplevel function *) prims : list (kername * string * bool); (* List of constants that are realized in the target code. * kername: constant name, string: name of target primitive *) From 27d5b635fae7ba2e09d2d7f3e3b937c6e5359cdd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 30 Jan 2024 17:16:27 +0100 Subject: [PATCH 03/11] Fix path handling --- plugin/certicoq.ml | 15 +++++++++------ plugin/test_certicoq_eval.v | 9 ++++++--- 2 files changed, 15 insertions(+), 9 deletions(-) diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index 135ce8b1..6f9905a5 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -593,8 +593,8 @@ module CompileFunctor (CI : CompilerInterface) = struct Printf.sprintf "#include \nextern value %s ();\n" name let write_c_driver opts name = - let fname = make_fname opts (name ^ ".c") in - let fhname = make_fname opts (name ^ ".h") in + let fname = make_fname opts (opts.filename ^ ".c") in + let fhname = make_fname opts (opts.filename ^ ".h") in let fd = Unix.(openfile fname [O_CREAT; O_APPEND; O_WRONLY] 0o640) in let chan = Unix.out_channel_of_descr fd in output_string chan (template name); @@ -609,7 +609,7 @@ module CompileFunctor (CI : CompilerInterface) = struct Printf.sprintf "external %s : unit -> Obj.t = \"%s\"\nlet _ = Certicoq_plugin.Certicoq.register_certicoq_run \"%s\" (Obj.magic %s)" name name name name let write_ocaml_driver opts name = - let fname = make_fname opts (name ^ "_wrapper.ml") in + let fname = make_fname opts (opts.filename ^ "_wrapper.ml") in let chan = open_out fname in output_string chan (template_ocaml name); flush chan; close_out chan; fname @@ -662,7 +662,8 @@ module CompileFunctor (CI : CompilerInterface) = struct 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 (name ^ ".o") importso + 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 @@ -693,11 +694,13 @@ module CompileFunctor (CI : CompilerInterface) = struct let opts = { opts with toplevel_name = fresh_name ^ "_body"; filename = fresh_name } in certicoq_eval_named opts env sigma fresh_name c imports - let compile_shared_C opts gr = + let compile_shared_C opts gr imports = let env = Global.env () in let sigma = Evd.from_env env in let sigma, c = Evd.fresh_global env sigma gr in - certicoq_eval opts env sigma c + let fresh_name = find_fresh (Names.Id.to_string (Nametab.basename_of_global gr)) !all_run_functions in + let opts = { opts with toplevel_name = fresh_name ^ "_body"; } in + certicoq_eval_named opts env sigma fresh_name c imports let print_to_file (s : string) (file : string) = let f = open_out file in diff --git a/plugin/test_certicoq_eval.v b/plugin/test_certicoq_eval.v index a8cfacc8..10b13e2d 100644 --- a/plugin/test_certicoq_eval.v +++ b/plugin/test_certicoq_eval.v @@ -37,13 +37,16 @@ Definition certicoqc2 := 5. Definition certicoqc3 := coq_msg_notice ("Hello world! " ++ show 100%nat). (* show (0%float == (-0)%float)). *) -Definition certicoqc4 := show (List.map S [26; 20]). +Definition certicoqc4 := (List.map S [26; 20]). Time Eval compute in certicoqc4. Set Warnings "-primitive-turned-into-axiom". Set Warnings "backtrace". -(* CertiCoq Eval -time certicoqc4. *) +CertiCoq Eval -time certicoqc4. Goal True. intros. - certicoq_eval -build_dir "_build" certicoqc4 ltac:(fun c => assert (certicoqc4 = c) by reflexivity). \ No newline at end of file + certicoq_eval -build_dir "_build" certicoqc4 ltac:(fun c => assert (certicoqc4 = c) by reflexivity). + exact I. +Qed. + From 5e00c439540bccc38e8a0a220133e773b21a0399 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 6 Feb 2024 12:13:57 +0100 Subject: [PATCH 04/11] Tests for CertiCoq Eval --- benchmarks/certicoq_eval.v | 97 ++++++++++++++++++++++++++++++++ benchmarks/certicoq_eval_issue.v | 45 +++++++++++++++ 2 files changed, 142 insertions(+) create mode 100644 benchmarks/certicoq_eval.v create mode 100644 benchmarks/certicoq_eval_issue.v diff --git a/benchmarks/certicoq_eval.v b/benchmarks/certicoq_eval.v new file mode 100644 index 00000000..67900810 --- /dev/null +++ b/benchmarks/certicoq_eval.v @@ -0,0 +1,97 @@ +From Equations Require Import Equations. +From Coq Require Import Uint63 Wf_nat ZArith Lia Arith. +From CertiCoq Require Import CertiCoq. + +(* This warns about uses of primitive operations, but we compile them fine *) +Set Warnings "-primitive-turned-into-axiom". + + +Definition inspect {A} (a : A) : {b | a = b} := + exist _ a eq_refl. +Notation " x 'eqn:' H " := (exist _ x H) (at level 20, only parsing). + +Section FactPrim. + Local Open Scope Z_scope. + + Equations fact (n : int) : int + by wf (Z.to_nat (to_Z n)) lt := + | n with inspect (Uint63.eqb n 0) := + | true eqn:_ => 1 + | false eqn:heq => n * fact (pred n). + Next Obligation. + pose proof (to_Z_bounded n). + pose proof (to_Z_bounded (pred n)). + red. + eapply Uint63.eqb_false_spec in heq. + rewrite <- Z2Nat.inj_succ. + assert (φ (n)%uint63 <> 0). intros hq. + pose proof (of_to_Z n). rewrite hq in H1. cbn in H1. congruence. + 2:lia. + rewrite pred_spec in H0 |- *. + assert (to_Z n - 1 < wB)%Z. lia. + eapply Z2Nat.inj_le. lia. lia. + rewrite Z.mod_small. 2:lia. lia. + Qed. +End FactPrim. +From CertiCoq.Benchmarks Require Import sha256. +From Coq Require Import String. +Definition test := "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching."%string. + +Definition sha := sha256.SHA_256 (sha256.str_to_bytes test). + +Definition sha_fast := sha256.SHA_256' (sha256.str_to_bytes test). + +Definition sha_fast_noproofs := let x := sha_fast in tt. + +Time Eval vm_compute in sha_fast_noproofs. +(* Executed in 0.004 sec *) + +CertiCoq Eval -time sha_fast_noproofs. +(* Executed in 0.037175 sec *) + +Time CertiCoq Eval sha_fast_noproofs. +(* Finished transaction in 0.06 sec *) + +CertiCoq Eval -time sha_fast_noproofs. +(* Executed in 0.045 sec *) +CertiCoq Eval -time sha_fast_noproofs. + + +From CertiCoq.Benchmarks Require Import Color. + +Time Eval vm_compute in Color.main. + +From CertiCoq.Benchmarks Require Import vs. +Import VeriStar. + +Definition vs_easy := + (fix loop (n : nat) (res : veristar_result) := + match n with + | 0%nat => + match res with + | Valid => true + | _ => false + end + | S n => + let res := check_entailment example_ent in + loop n res + end) 100 Valid. + +Definition vs_hard := + match vs.main_h with + | vs.VeriStar.Valid => true + | _ => false + end. + +(* +(* Blows up *) Time Eval vm_compute in vs_easy. +(* Blows up *) Time Eval vm_compute in vs_hard. +*) + +CertiCoq Eval -time vs_hard. +(* Executed in 0.06s *) +CertiCoq Eval -time vs_hard. + +CertiCoq Eval -time vs_easy. +(* Executed in 0.007s *) + diff --git a/benchmarks/certicoq_eval_issue.v b/benchmarks/certicoq_eval_issue.v new file mode 100644 index 00000000..2385a79a --- /dev/null +++ b/benchmarks/certicoq_eval_issue.v @@ -0,0 +1,45 @@ + +From Coq Require Import List Arith Extraction Lia. +Notation "( x ; p )" := (exist _ x p). +Example nth {A} (l : list A) : {n : nat | n < length l} -> A. +Proof. + intros n. + induction l as [|l' Hl']. + - destruct n as [n Hn]. + simpl in Hn. + apply False_rect. + inversion Hn. + Set Printing Notations. + - destruct n as [n Hn]. + destruct n as [|n']. + + (* 0 *) + exact l'. + + (* S n' *) + apply IHHl'. + exists n'. + simpl in Hn. + apply Nat.succ_lt_mono. apply Hn. +Defined. + +Print nth. + +Extraction nth. + +From CertiCoq.Plugin Require Import CertiCoq. + +Import ListNotations. +Definition l : list nat := map (fun x => x * x) (repeat 3 45000). + +Lemma nth_l : 30000 < length l. +Proof. unfold l. rewrite map_length. rewrite repeat_length. Admitted. + +Definition test : nat := (nth l (30000; nth_l)). +(* Time Eval vm_compute in test. *) +(* 30 seconds, includes cost of building the intermediate n < length proofs *) +(* Stack overflowing? *) +(* CertiCoq Eval -debug -time test. *) +Definition largenat := 45000. +(* Stack overflowing? *) + +Definition llength := length l. +CertiCoq Eval -debug -time llength. From 5ef7f714dcb7d9ebd02dfed0f623e532a8ea5a10 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 6 Feb 2024 12:14:46 +0100 Subject: [PATCH 05/11] Implement caching of previously compiled references (beware, not playing great with backtracking yet). --- plugin/certicoq.ml | 47 +++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 42 insertions(+), 5 deletions(-) diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index 6f9905a5..21c0c10c 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -115,6 +115,9 @@ let register_certicoq_run s fn = Feedback.msg_debug Pp.(str"Registering function " ++ str s ++ str " in certicoq_run"); Lib.add_leaf (certicoq_run_function_input (s, fn)) +let exists_certicoq_run s = + CString.Map.find_opt s !certicoq_run_functions + let run_certicoq_run s = try CString.Map.find s !certicoq_run_functions with Not_found -> CErrors.user_err Pp.(str"Could not find certicoq run function associated to " ++ str s) @@ -614,6 +617,14 @@ module CompileFunctor (CI : CompilerInterface) = struct output_string chan (template_ocaml name); flush chan; close_out chan; fname + + let time f = + let start = Unix.gettimeofday() in + let res = f () in + let time = Unix.gettimeofday () -. start in + Feedback.msg_notice (Pp.str (Printf.sprintf "Executed in %f sec" time)); + res + let certicoq_eval_named opts env sigma id c imports = let prog = quote_term opts env sigma c in let tyinfo = @@ -671,7 +682,10 @@ module CompileFunctor (CI : CompilerInterface) = struct debug_msg debug (Printf.sprintf "Compilation ran fine, linking compiled code for %s" id); Dynlink.loadfile_private shared_lib; debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" id); - let result = run_certicoq_run id () in + let result = + if opts.time then time (run_certicoq_run id) + else run_certicoq_run id () + in debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); reify env sigma tyinfo result | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str linkcmd) @@ -693,20 +707,43 @@ module CompileFunctor (CI : CompilerInterface) = struct let fresh_name = find_fresh opts.filename !all_run_functions in let opts = { opts with toplevel_name = fresh_name ^ "_body"; filename = fresh_name } in certicoq_eval_named opts env sigma fresh_name c imports - + + let run_existing opts env sigma c run = + let tyinfo = + let ty = Retyping.get_type_of env sigma c in + check_reifyable env sigma ty + in + let result = + if opts.time then time run + else run () + in + debug_msg opts.debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); + reify env sigma tyinfo result + + let certicoq_eval opts env sigma c imports = + match exists_certicoq_run opts.filename with + | None -> certicoq_eval opts env sigma c imports + | Some run -> + debug_msg opts.debug (Printf.sprintf "Retrieved earlier compiled code for %s" opts.filename); + run_existing opts env sigma c run + let compile_shared_C opts gr imports = let env = Global.env () in let sigma = Evd.from_env env in let sigma, c = Evd.fresh_global env sigma gr in - let fresh_name = find_fresh (Names.Id.to_string (Nametab.basename_of_global gr)) !all_run_functions in - let opts = { opts with toplevel_name = fresh_name ^ "_body"; } in - certicoq_eval_named opts env sigma fresh_name c imports + let name = Names.Id.to_string (Nametab.basename_of_global gr) in + match exists_certicoq_run name with + | None -> + let opts = { opts with toplevel_name = name ^ "_body"; } in + certicoq_eval_named opts env sigma name c imports + | Some run -> run_existing opts env sigma c run let print_to_file (s : string) (file : string) = let f = open_out file in 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 From 1f580a2a4d3a21628e401273876cbf44a25b24aa Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 7 Feb 2024 10:47:22 +0100 Subject: [PATCH 06/11] Remove spurious opam dependency --- plugin/Makefile.local | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugin/Makefile.local b/plugin/Makefile.local index 08f2550c..87147a2b 100644 --- a/plugin/Makefile.local +++ b/plugin/Makefile.local @@ -10,7 +10,7 @@ CAMLFLAGS+=-w -60 # Unused functor arguments CAMLFLAGS+=-w -8 # Non-exhaustive matches produced by extraction CAMLFLAGS+=-w -37 # Unused constructor -CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims,inspect +CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims CC=$(shell which gcc || which clang-11) From 1f87c26fee301a5f03ac8109c6a980a42beab2ff Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 7 Feb 2024 11:51:51 +0100 Subject: [PATCH 07/11] Fix plugin Makefile --- plugin/Makefile.local | 2 ++ 1 file changed, 2 insertions(+) diff --git a/plugin/Makefile.local b/plugin/Makefile.local index 87147a2b..1b4fec03 100644 --- a/plugin/Makefile.local +++ b/plugin/Makefile.local @@ -19,3 +19,5 @@ merlin-hook:: get_ordinal.o: get_ordinal.c $(CC) -c -o $@ -I runtime $< + +certicoq_plugin.cmxs: get_ordinal.o \ No newline at end of file From 2a876bcfa40a712f591dc71161b99dce2cf13f93 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 7 Feb 2024 13:52:34 +0100 Subject: [PATCH 08/11] Attributes on external calls --- plugin/certicoq.ml | 5 +++-- plugin/get_ordinal.c | 5 ++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index 21c0c10c..cd8616f4 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -37,8 +37,9 @@ let increment_subscript id = let debug_reify = CDebug.create ~name:"certicoq-reify" () -external get_unboxed_ordinal : Obj.t -> int = "get_unboxed_ordinal" -external get_boxed_ordinal : Obj.t -> int = "get_boxed_ordinal" +external get_unboxed_ordinal : Obj.t -> int = "get_unboxed_ordinal" [@@noalloc] + +external get_boxed_ordinal : Obj.t -> (int [@untagged]) = "get_boxed_ordinal" "get_boxed_ordinal" [@@noalloc] (** Various Utils *) diff --git a/plugin/get_ordinal.c b/plugin/get_ordinal.c index 2aa6d73b..6855d32f 100644 --- a/plugin/get_ordinal.c +++ b/plugin/get_ordinal.c @@ -3,10 +3,9 @@ value get_unboxed_ordinal(value $v) { return Val_long($v); - // >> 1LLU); } -value get_boxed_ordinal(value $v) +intnat get_boxed_ordinal(value $v) { - return Val_long(*((unsigned long long *) $v + 18446744073709551615LLU) & 255LLU); + return (*((unsigned long long *) $v + 18446744073709551615LLU) & 255LLU); } From fa27de80abc2c2af36a9165faa7dc5b0c0994dc5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 7 Feb 2024 14:11:00 +0100 Subject: [PATCH 09/11] Minor fixes in get_ordinal interface --- plugin/certicoq.ml | 30 ++++++++++++++++++++++-------- plugin/get_ordinal.c | 3 ++- plugin/test_certicoq_eval.v | 20 ++++++++++++++++++-- 3 files changed, 42 insertions(+), 11 deletions(-) diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index cd8616f4..593b498a 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -540,6 +540,15 @@ module CompileFunctor (CI : CompilerInterface) = struct Pp.(str "Ill-formed primitive value representation in CertiCoq's reification for type " ++ pr_reifyable_type env sigma ty) + let ocaml_get_boxed_ordinal v = + (* tag is the header of the object *) + let tag = Array.unsafe_get (Obj.magic v : Obj.t array) (-1) in + (* We turn it into an ocaml int usable for arithmetic operations *) + let tag_int = (Stdlib.Int.shift_left (Obj.magic (Obj.repr tag)) 1) + 1 in + Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml tag: %i" (Obj.tag tag))); + Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml get_boxed_ordinal int: %u" tag_int)); + Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml get_boxed_ordinal ordinal: %u" (tag_int land 255))); + tag_int land 255 let reify env sigma ty v : Constr.t = let open Declarations in @@ -558,6 +567,10 @@ module CompileFunctor (CI : CompilerInterface) = struct if Obj.is_block v then let () = debug (Printf.sprintf "Reifying constructor block") in let ord = get_boxed_ordinal v in + let ord' = ocaml_get_boxed_ordinal v in + let () = if ord == ord' then () else + Feedback.msg_debug (Pp.str (Printf.sprintf "C get_boxed_ordinal = %i, OCaml get_boxed_ordinale = %i" ord ord')) + in let () = debug (Printf.sprintf "Reifying constructor block of tag %i" ord) in let coqidx = try find_nth_non_constant ord cstrs @@ -619,11 +632,11 @@ module CompileFunctor (CI : CompilerInterface) = struct flush chan; close_out chan; fname - let time f = + let time ~(msg:Pp.t) f = let start = Unix.gettimeofday() in let res = f () in let time = Unix.gettimeofday () -. start in - Feedback.msg_notice (Pp.str (Printf.sprintf "Executed in %f sec" time)); + Feedback.msg_notice Pp.(msg ++ str (Printf.sprintf " executed in %f sec" time)); res let certicoq_eval_named opts env sigma id c imports = @@ -684,11 +697,12 @@ module CompileFunctor (CI : CompilerInterface) = struct Dynlink.loadfile_private shared_lib; debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" id); let result = - if opts.time then time (run_certicoq_run id) + if opts.time then time ~msg:(Pp.str id) (run_certicoq_run id) else run_certicoq_run id () in debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); - reify 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 | 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) @@ -709,13 +723,13 @@ module CompileFunctor (CI : CompilerInterface) = struct let opts = { opts with toplevel_name = fresh_name ^ "_body"; filename = fresh_name } in certicoq_eval_named opts env sigma fresh_name c imports - let run_existing opts env sigma c run = + let run_existing opts env sigma c id run = let tyinfo = let ty = Retyping.get_type_of env sigma c in check_reifyable env sigma ty in let result = - if opts.time then time run + if opts.time then time ~msg:Pp.(str"Running " ++ id) run else run () in debug_msg opts.debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); @@ -726,7 +740,7 @@ module CompileFunctor (CI : CompilerInterface) = struct | None -> certicoq_eval opts env sigma c imports | Some run -> debug_msg opts.debug (Printf.sprintf "Retrieved earlier compiled code for %s" opts.filename); - run_existing opts env sigma c run + run_existing opts env sigma c (Pp.str opts.filename) run let compile_shared_C opts gr imports = let env = Global.env () in @@ -737,7 +751,7 @@ module CompileFunctor (CI : CompilerInterface) = struct | None -> let opts = { opts with toplevel_name = name ^ "_body"; } in certicoq_eval_named opts env sigma name c imports - | Some run -> run_existing opts env sigma c run + | Some run -> run_existing opts env sigma c (Pp.str name) run let print_to_file (s : string) (file : string) = let f = open_out file in diff --git a/plugin/get_ordinal.c b/plugin/get_ordinal.c index 6855d32f..b2cdfe5b 100644 --- a/plugin/get_ordinal.c +++ b/plugin/get_ordinal.c @@ -1,4 +1,5 @@ #include "gc_stack.h" +#include value get_unboxed_ordinal(value $v) { @@ -7,5 +8,5 @@ value get_unboxed_ordinal(value $v) intnat get_boxed_ordinal(value $v) { - return (*((unsigned long long *) $v + 18446744073709551615LLU) & 255LLU); + return *((unsigned long long *) $v + 18446744073709551615LLU) & 255LLU; } diff --git a/plugin/test_certicoq_eval.v b/plugin/test_certicoq_eval.v index 10b13e2d..a52e38d8 100644 --- a/plugin/test_certicoq_eval.v +++ b/plugin/test_certicoq_eval.v @@ -37,16 +37,32 @@ Definition certicoqc2 := 5. Definition certicoqc3 := coq_msg_notice ("Hello world! " ++ show 100%nat). (* show (0%float == (-0)%float)). *) +Inductive three_ind := One | Two | Three. +Definition one := One. +Definition two := Two. +Definition three := Three. + Definition certicoqc4 := (List.map S [26; 20]). Time Eval compute in certicoqc4. Set Warnings "-primitive-turned-into-axiom". Set Warnings "backtrace". -CertiCoq Eval -time certicoqc4. +CertiCoq Eval -time -debug certicoqc4. + +Definition largertag := S754_finite true xH 0%Z. +Definition otherlargertag := S754_infinity true. +CertiCoq Eval -time -debug otherlargertag. + +Set Debug "certicoq-reify". +Time CertiCoq Eval -time one. +CertiCoq Eval -time two. +CertiCoq Eval -time -debug three. +Time CertiCoq Eval -time -debug three. +(* Goal True. intros. certicoq_eval -build_dir "_build" certicoqc4 ltac:(fun c => assert (certicoqc4 = c) by reflexivity). exact I. -Qed. +Qed. *) From c6ae751d044e8def94ab9dbaa5699ef1284754a5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 7 Feb 2024 14:35:09 +0100 Subject: [PATCH 10/11] Add a CertiCoq Build Directory coq option to set the build directory globally --- plugin/certicoq.ml | 73 +++++++++++++++++++------------------ plugin/certicoq.mli | 2 +- plugin/test_certicoq_eval.v | 2 + 3 files changed, 40 insertions(+), 37 deletions(-) diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index 593b498a..de2b039e 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -9,6 +9,11 @@ open ExceptionMonad open AstCommon open Plugin_utils +let get_build_dir_opt = + Goptions.declare_stringopt_option_and_ref + ~key:["CertiCoq"; "Build"; "Directory"] + ~depr:false + (* Taken from Coq's increment_subscript, but works on strings rather than idents *) let increment_subscript id = let len = String.length id in @@ -182,7 +187,18 @@ type options = prims : ((Kernames.kername * Kernames.ident) * bool) list; } -let default_options : options = +let check_build_dir d = + if d = "" then "." else + let isdir = + try Unix.((stat d).st_kind = S_DIR) + with Unix.Unix_error (Unix.ENOENT, _, _) -> + CErrors.user_err Pp.(str "Could not compile: build directory " ++ str d ++ str " not found.") + in + if not isdir then + CErrors.user_err Pp.(str "Could not compile: " ++ str d ++ str " is not a directory.") + else d + +let default_options () : options = { bypass_qed = false; cps = false; time = false; @@ -191,7 +207,7 @@ let default_options : options = debug = false; args = 5; anf_conf = 0; - build_dir = "."; + build_dir = (match get_build_dir_opt () with None -> "." | Some s -> check_build_dir s); filename = ""; ext = ""; dev = 0; @@ -200,17 +216,6 @@ let default_options : options = prims = []; } -let check_build_dir d = - if d = "" then "." else - let isdir = - try Unix.((stat d).st_kind = S_DIR) - with Unix.Unix_error (Unix.ENOENT, _, _) -> - CErrors.user_err Pp.(str "Could not compile: build directory " ++ str d ++ str " not found.") - in - if not isdir then - CErrors.user_err Pp.(str "Could not compile: " ++ str d ++ str " is not a directory.") - else d - 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 @@ -232,7 +237,7 @@ let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ide | TOPLEVEL_NAME s :: xs -> aux {o with toplevel_name = s} xs | FILENAME s :: xs -> aux {o with filename = s} xs in - let opts = { default_options with filename = fname } in + let opts = { (default_options ()) with filename = fname } in let o = aux opts l in {o with prims = pr} @@ -540,7 +545,7 @@ module CompileFunctor (CI : CompilerInterface) = struct Pp.(str "Ill-formed primitive value representation in CertiCoq's reification for type " ++ pr_reifyable_type env sigma ty) - let ocaml_get_boxed_ordinal v = + (* let ocaml_get_boxed_ordinal v = (* tag is the header of the object *) let tag = Array.unsafe_get (Obj.magic v : Obj.t array) (-1) in (* We turn it into an ocaml int usable for arithmetic operations *) @@ -548,8 +553,16 @@ module CompileFunctor (CI : CompilerInterface) = struct Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml tag: %i" (Obj.tag tag))); Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml get_boxed_ordinal int: %u" tag_int)); Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml get_boxed_ordinal ordinal: %u" (tag_int land 255))); - tag_int land 255 + tag_int land 255 *) + + let time ~(msg:Pp.t) f = + let start = Unix.gettimeofday() in + let res = f () in + 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 open Declarations in let debug s = debug_reify Pp.(fun () -> str s) in @@ -563,14 +576,8 @@ module CompileFunctor (CI : CompilerInterface) = struct let npars = inductive_params spec in let params, _indices = CList.chop npars args in let cstrs = get_constructors env indfam in - let () = debug (Printf.sprintf "Reifying inductive value") in if Obj.is_block v then - let () = debug (Printf.sprintf "Reifying constructor block") in let ord = get_boxed_ordinal v in - let ord' = ocaml_get_boxed_ordinal v in - let () = if ord == ord' then () else - Feedback.msg_debug (Pp.str (Printf.sprintf "C get_boxed_ordinal = %i, OCaml get_boxed_ordinale = %i" ord ord')) - in let () = debug (Printf.sprintf "Reifying constructor block of tag %i" ord) in let coqidx = try find_nth_non_constant ord cstrs @@ -585,7 +592,6 @@ module CompileFunctor (CI : CompilerInterface) = struct aux argty v) (List.rev ctx) vargs in Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) (params @ args') else (* Constant constructor *) - let () = debug (Printf.sprintf "Reifying constant constructor") in let ord = (Obj.magic v : int) in let () = debug (Printf.sprintf "Reifying constant constructor: %i" ord) in let coqidx = @@ -596,14 +602,18 @@ module CompileFunctor (CI : CompilerInterface) = struct Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) params | IsPrimitive (c, u, _args) -> if Environ.is_array_type env c then - CErrors.user_err Pp.(str "Primitive arrays are not supported yet") + CErrors.user_err Pp.(str "Primitive arrays are not supported yet in CertiCoq reification") else if Environ.is_float64_type env c then Constr.mkFloat (Obj.magic v) else if Environ.is_int63_type env c then Constr.mkInt (Obj.magic v) - else CErrors.user_err Pp.(str "Unsupported primitive type") + else CErrors.user_err Pp.(str "Unsupported primitive type in CertiCoq reification") 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 + let template name = Printf.sprintf "\nvalue %s ()\n { struct thread_info* tinfo = make_tinfo(); return %s_body(tinfo); }\n" name name let template_header name = @@ -631,14 +641,6 @@ module CompileFunctor (CI : CompilerInterface) = struct output_string chan (template_ocaml name); flush chan; close_out chan; fname - - let time ~(msg:Pp.t) f = - let start = Unix.gettimeofday() in - let res = f () in - let time = Unix.gettimeofday () -. start in - Feedback.msg_notice Pp.(msg ++ str (Printf.sprintf " executed in %f sec" time)); - res - let certicoq_eval_named opts env sigma id c imports = let prog = quote_term opts env sigma c in let tyinfo = @@ -701,8 +703,7 @@ module CompileFunctor (CI : CompilerInterface) = struct else run_certicoq_run id () in debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); - if opts.time then time ~msg:(Pp.str "reification") (fun () -> reify env sigma tyinfo result) - else reify env sigma tyinfo 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) @@ -733,7 +734,7 @@ module CompileFunctor (CI : CompilerInterface) = struct else run () in debug_msg opts.debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); - reify env sigma tyinfo result + reify opts env sigma tyinfo result let certicoq_eval opts env sigma c imports = match exists_certicoq_run opts.filename with diff --git a/plugin/certicoq.mli b/plugin/certicoq.mli index b2c4996a..494c98b0 100644 --- a/plugin/certicoq.mli +++ b/plugin/certicoq.mli @@ -36,7 +36,7 @@ type options = type prim = ((Kernames.kername * Kernames.ident) * bool) -val default_options : options +val default_options : unit -> options val make_options : command_args list -> prim list -> string -> options (* Register primitive operations and associated include file *) diff --git a/plugin/test_certicoq_eval.v b/plugin/test_certicoq_eval.v index a52e38d8..5d39b82c 100644 --- a/plugin/test_certicoq_eval.v +++ b/plugin/test_certicoq_eval.v @@ -2,6 +2,8 @@ From CertiCoq.Plugin Require Import Loader. From CertiCoq.Plugin Require Import CertiCoq. From MetaCoq.Utils Require Import utils. +Set CertiCoq Build Directory "_build". + Open Scope bs_scope. Class Show (A : Type) := show : A -> string. From 68c7aff26bc8254df742491eac9bcfbcd3d1bac6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 7 Feb 2024 15:07:28 +0100 Subject: [PATCH 11/11] Fix certicoq.ml in cplugin, compiles with -O2 -fomit-frame-pointer in standard plugin --- cplugin/certicoq.ml | 3 ++- plugin/certicoq.ml | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/cplugin/certicoq.ml b/cplugin/certicoq.ml index 1ab88c3f..859c5546 100644 --- a/cplugin/certicoq.ml +++ b/cplugin/certicoq.ml @@ -280,8 +280,9 @@ let make_pipeline_options (opts : options) = let dev = coq_nat_of_int opts.dev in let prefix = bytestring_of_string opts.prefix in let prims = get_global_prims () @ opts.prims in + let name = bytestring_of_string "body" in (* Feedback.msg_debug Pp.(str"Prims: " ++ prlist_with_sep spc (fun ((x, y), wt) -> str (string_of_bytestring y)) prims); *) - Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix prims + Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix name prims (** Main Compilation Functions *) diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index de2b039e..fabd6ca5 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -450,7 +450,7 @@ module CompileFunctor (CI : CompilerInterface) = struct let compiler = compiler_executable debug in let rt_dir = runtime_dir () in let cmd = - Printf.sprintf "%s -Wno-everything -g -I %s -I %s -c -o %s %s" + Printf.sprintf "%s -Wno-everything -O2 -fomit-frame-pointer -g -I %s -I %s -c -o %s %s" compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) (name ^ ".o") (name ^ ".c") in let importso =