From 8efa0f736dcf17cd2e26213ca3f0b329d768d868 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 13 Feb 2024 16:09:20 -0800 Subject: [PATCH 1/3] Feature: add support for configuration files to control how declarations are grouped within various C files --- bin/main.ml | 30 ++++++++++++++++++++---------- dune-project | 2 +- eurydice.opam | 1 + lib/Options.ml | 1 + lib/dune | 2 +- 5 files changed, 24 insertions(+), 12 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index 8639c7d..97557ea 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -16,6 +16,7 @@ Supported options:|} "--log", Arg.Set_string O.log_level, " log level, use * for everything"; "--debug", Arg.String debug, " debug options, to be passed to krml"; "--output", Arg.Set_string Krml.Options.tmpdir, " output directory in which to write files"; + "--config", Arg.Set_string O.config, " YAML configuration file"; ] in let spec = Arg.align spec in let files = ref [] in @@ -87,15 +88,16 @@ Supported options:|} Printf.printf "2️⃣ Cleanup\n"; let files = - (* Custom bundling, for now -- since our bundling operates based on - declaration lids, not their original file. *) - let prefix, (f, decls) = Krml.KList.split_at_last files in - let core, decls = List.fold_left (fun (core, decls) decl -> - match Krml.Ast.lid_of_decl decl with - | "core" :: _, _ -> Krml.Bundles.mark_private decl :: core, decls - | _ -> core, decl :: decls - ) ([], []) decls in - prefix @ [ "core", List.rev core; f, List.rev decls ] + if !O.config = "" then + files + else + let config = Eurydice.Bundles.load_config !O.config in + let config = Eurydice.Bundles.parse_config config in + let files = Eurydice.Bundles.bundle files config in + let files = Krml.Bundles.topological_sort files in + Krml.KPrint.bprintf "File order after topological sort: %s\n" + (String.concat ", " (List.map fst files)); + files in let files = Eurydice.Cleanup1.cleanup files in @@ -154,10 +156,18 @@ Supported options:|} let c_name_map = Simplify.allocate_c_names files in let deps = Bundles.direct_dependencies_with_internal files file_of_map in let files = List.map (fun (f, ds) -> + let is_fine = function + | ["LowStar"; "Ignore"], "ignore" + | "Eurydice" :: _, _ -> + (* | "core" :: _, _ -> *) + true + | _ -> + false + in f, List.filter_map (fun d -> match d with | Krml.Ast.DExternal (_, _, _, _, lid, t, _) when Krml.Monomorphization.( - has_variables [ t ] || has_cg_array [ t ] + (has_variables [ t ] || has_cg_array [ t ]) && not (is_fine lid) ) -> KPrint.bprintf "Warning: %a is a type/const-polymorphic assumed function, \ must be implemented with a macro, dropping it\n" Krml.PrintAst.Ops.plid lid; diff --git a/dune-project b/dune-project index 42c0875..a571420 100644 --- a/dune-project +++ b/dune-project @@ -18,6 +18,6 @@ (synopsis "A Rust to C translator") (description "Eurydice builds upon Charon to take existing Rust code and translate it to C") - (depends ocaml dune terminal)) + (depends ocaml dune terminal yaml)) (using menhir 2.1) diff --git a/eurydice.opam b/eurydice.opam index bd16911..aaf5e18 100644 --- a/eurydice.opam +++ b/eurydice.opam @@ -13,6 +13,7 @@ depends: [ "ocaml" "dune" {>= "3.7"} "terminal" + "yaml" "odoc" {with-doc} ] build: [ diff --git a/lib/Options.ml b/lib/Options.ml index 7ad910a..dd36298 100644 --- a/lib/Options.ml +++ b/lib/Options.ml @@ -1 +1,2 @@ let log_level = ref "" +let config = ref "" diff --git a/lib/dune b/lib/dune index 9d22e42..754ee4f 100644 --- a/lib/dune +++ b/lib/dune @@ -1,3 +1,3 @@ (library (name eurydice) - (libraries charon krml)) + (libraries charon krml yaml)) From dfe1c7fa8fc045449d374b120e9f93c72aa63f17 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 13 Feb 2024 16:13:15 -0800 Subject: [PATCH 2/3] missing file --- lib/Bundles.ml | 147 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 lib/Bundles.ml diff --git a/lib/Bundles.ml b/lib/Bundles.ml new file mode 100644 index 0000000..cd844fd --- /dev/null +++ b/lib/Bundles.ml @@ -0,0 +1,147 @@ +(* A more modern version of the krml facility that matches on lids (instead of file names), and + relies on a YAML file for configuration (rather than the cryptic syntax). *) + +type pattern = + | Prefix of string list + | Exact of string list + +type file = { + name: string; + api: pattern list; + private_: pattern list; +} + +type config = file list + +(** Loading & parsing *) + +let load_config (path: string): Yaml.value = + (* TODO: library not found: Yaml_unix *) + let contents = Krml.Utils.file_get_contents path in + print_endline contents; + match Yaml.of_string contents with + | Error (`Msg s) -> + Krml.Warn.fatal_error "Issue reading configuration file: %s" s + | Ok v -> + v + +let parsing_error f = Krml.Warn.fatal_error ("Issue parsing configuration file: " ^^ f) + +let parse_pattern (v: Yaml.value): pattern = + match v with + | `A vs -> + let rec parse acc = function + | (`String "*") :: [] -> Prefix (List.rev acc) + | (`String "*") :: _ -> parsing_error "wildcards only allowed at the end" + | (`String s) :: tl -> parse (s :: acc) tl + | _ :: _ -> parsing_error "only strings in patterns" + | [] -> Exact (List.rev acc) + in + parse [] vs + | _ -> + parsing_error "pattern not a list" + +let parse_file (v: Yaml.value): file = + match v with + | `O ls -> + let count = ref 0 in + let lookup k = try let r = List.assoc k ls in incr count; Some r with Not_found -> None in + let name = + match lookup "name" with + | Some (`String name) -> name + | Some _ -> parsing_error "name not a string" + | None -> parsing_error "missing name" + in + let api = + match lookup "api" with + | None -> [] + | Some (`A api) -> List.map parse_pattern api + | Some _ -> parsing_error "api not a list" + in + let private_ = + match lookup "private" with + | None -> [] + | Some (`A private_) -> List.map parse_pattern private_ + | Some _ -> parsing_error "private not a list" + in + if !count < List.length ls then + parsing_error "extraneous fields in file"; + { name; api; private_ } + | _ -> + parsing_error "file must be an object" + +let parse_config (v: Yaml.value): config = + match v with + | `O [ "files", `A files ] -> + List.map parse_file files + | `O [ "files", _ ] -> + parsing_error "files is not a sequence" + | `O _ -> + parsing_error "top-level object must be made of a single entry: files" + | _ -> + parsing_error "YAML file must be an object with key files" + +open Krml.Ast + +(** Constructing bundles *) + +let starts_with l prefix = + List.length prefix <= List.length l && + fst (Krml.KList.split (List.length prefix) l) = prefix + +(* `lid` matches pattern `p` *) +let matches lid p = + match p with + | Exact m -> + m = fst lid + | Prefix prefix -> + starts_with (fst lid) prefix + +let bundle (files: file list) (c: config): files = + let bundled = Hashtbl.create 137 in + let bundle name decl = + if Hashtbl.mem bundled name then + Hashtbl.replace bundled name (decl :: Hashtbl.find bundled name) + else + Hashtbl.add bundled name [ decl ] + in + let files = List.map (fun (filename, decls) -> + filename, List.filter_map (fun decl -> + let lid = lid_of_decl decl in + let rec find files = + match files with + | [] -> + Krml.(KPrint.bprintf "%a doesn't go anywhere\n" PrintAst.Ops.plid lid); + false + | { name; api; private_ } :: files -> + if List.exists (matches lid) api then begin + Krml.(KPrint.bprintf "%a goes (api) into %s\n" PrintAst.Ops.plid lid name); + bundle name decl; + true + end else if List.exists (matches lid) private_ then begin + Krml.(KPrint.bprintf "%a goes (private) into %s\n" PrintAst.Ops.plid lid name); + bundle name (Krml.Bundles.mark_private decl); + true + end else + find files + in + if find c then + None + else + Some decl + ) decls + ) files in + let files = List.filter (fun (filename, decls) -> + (* Collision between the original crate name (e.g. libcrux_kyber) and the destination bundle + (e.g. libcrux_kyber). *) + if Hashtbl.mem bundled filename then begin + List.iter (bundle filename) decls; + false + end else + true + ) files in + Hashtbl.fold (fun filename decls acc -> + (filename, List.rev decls) :: acc + ) bundled (List.filter (fun (_, decls) -> decls <> []) files) + + From efb65f5e668d9cb424f0e4eda0d2ad7069931f62 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 13 Feb 2024 16:14:29 -0800 Subject: [PATCH 3/3] Praying to the nix gods --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 529cb9d..708eb2e 100644 --- a/flake.nix +++ b/flake.nix @@ -49,7 +49,7 @@ nativeBuildInputs = [gnugrep]; - propagatedBuildInputs = [krml charon-ml ocamlPackages.terminal]; + propagatedBuildInputs = [krml charon-ml ocamlPackages.terminal ocamlPackages.yaml]; passthru = { tests = stdenv.mkDerivation {