Merge pull request #6 from AeneasVerif/protz_config

Feature: add support for configuration files to control how declarati…

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;

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)

eurydice.opam

@@ -13,6 +13,7 @@ depends: [
   "ocaml"
   "dune" {>= "3.7"}
   "terminal"
+  "yaml"
   "odoc" {with-doc}
 ]
 build: [

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 {

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)
+
+

lib/Options.ml

@@ -1 +1,2 @@
 let log_level = ref ""
+let config = ref ""

lib/dune

@@ -1,3 +1,3 @@
 (library
  (name eurydice)
- (libraries charon krml))
+ (libraries charon krml yaml))