Merge pull request #7 from AeneasVerif/protz_config

Several improvements in support of Kyber.

bin/main.ml

@@ -127,33 +127,27 @@ Supported options:|}
   let files = Krml.Simplify.fixup_hoist#visit_files () files in
   let files = Krml.Simplify.misc_cosmetic#visit_files () files in
   let files = Krml.Simplify.let_to_sequence#visit_files () files in
+  Eurydice.Logging.log "Phase2.5" "%a" pfiles files;
   let files = Krml.Inlining.cross_call_analysis files in
   let files = Krml.Simplify.remove_unused files in
+  (* Macros stemming from globals *)
   let files, macros = Eurydice.Cleanup2.build_macros files in
 
   Eurydice.Logging.log "Phase3" "%a" pfiles files;
   let errors, files = Krml.Checker.check_everything ~warn:true files in
   if errors then
     exit 1;
 
+  let scope_env = Krml.Simplify.allocate_c_env files in
+  let files = Eurydice.Cleanup3.decay_cg_externals#visit_files (scope_env, false) files in
   let macros =
-    Krml.Idents.LidSet.union
-      macros
-      ((object(self)
-        inherit [_] Krml.Ast.reduce
-        method private zero = Krml.Idents.LidSet.empty
-        method private plus = Krml.Idents.LidSet.union
-        method! visit_DExternal _ _ _ n_cgs n name _ _ =
-          if n > 0 || n_cgs > 0 then
-            Krml.Idents.LidSet.singleton name
-          else
-            self#zero
-      end)#visit_files () files)
+    let cg_macros = Eurydice.Cleanup3.build_cg_macros#visit_files () files in
+    Krml.Idents.LidSet.(union (union macros cg_macros) Eurydice.Builtin.macros)
   in
-  let macros = Krml.Idents.LidSet.union macros Eurydice.Builtin.macros in
+  let c_name_map = Krml.GlobalNames.mapping (fst scope_env) in
+
   let open Krml in
   let file_of_map = Bundle.mk_file_of files in
-  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

lib/Bundles.ml

@@ -18,7 +18,6 @@ type config = file list
 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
@@ -64,8 +63,21 @@ let parse_file (v: Yaml.value): file =
         | Some (`A private_) -> List.map parse_pattern private_
         | Some _ -> parsing_error "private not a list"
       in
+      let include_ =
+        match lookup "include_in_h" with
+        | None -> []
+        | Some (`A include_) -> List.map (function `String s -> Krml.Options.HeaderOnly name, s | _ -> parsing_error "include_in_h must be a string") include_
+        | Some _ -> parsing_error "include_in_h must be a list"
+      in
+      let c_include_ =
+        match lookup "include_in_c" with
+        | None -> []
+        | Some (`A include_) -> List.map (function `String s -> Krml.Options.COnly name, s | _ -> parsing_error "include_in_c must be a string") include_
+        | Some _ -> parsing_error "include_in_c must be a list"
+      in
       if !count < List.length ls then
         parsing_error "extraneous fields in file";
+      Krml.Options.(add_include := include_ @ c_include_ @ !add_include);
       { name; api; private_ }
   | _ ->
       parsing_error "file must be an object"
@@ -115,11 +127,11 @@ let bundle (files: file list) (c: config): files =
             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);
+              (* 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);
+              (* Krml.(KPrint.bprintf "%a goes (private) into %s\n" PrintAst.Ops.plid lid name); *)
               bundle name (Krml.Bundles.mark_private decl);
               true
             end else

lib/Cleanup3.ml

@@ -0,0 +1,84 @@
+(* Administrative cleanups that do not get checked. *)
+
+(* CG-polymorphic external signatures generally cannot be implemented with C functions, and Eurydice
+   expects those to be hand-written using macros. There is one exception, though:
+   - all of the const generics appear in positions that would anyhow decay to pointers (e.g.,
+     void f<N>(int x[N]) can be replaced by void f(int *x) -- it's the same in C)
+   - the return type is unit -- the implementation doesn't need to receive the return type as an
+     argument
+*)
+
+open Krml
+open Ast
+
+let decay_cg_externals = object(self)
+  inherit [_] Krml.Ast.map as super
+
+  (* Since we allocate new names, we reuse the C name allocation facility *)
+  inherit Simplify.scope_helpers
+
+  method! visit_file env f =
+    current_file <- fst f;
+    super#visit_file env f
+
+  method! visit_TCgArray (env, under_external) t n =
+    if under_external then
+      raise Exit
+    else
+      super#visit_TCgArray (env, under_external) t n
+
+  method! visit_TCgApp (env, under_external) t n =
+    if under_external then
+      raise Exit
+    else
+      super#visit_TCgApp (env, under_external) t n
+
+  method! visit_DExternal (scope_env, _) cc flags n_cgs n name t hints =
+    let t_ret, t_args = Helpers.flatten_arrow t in
+    if t_ret = TUnit && n_cgs > 0 then
+      let t_args = List.map (function
+        | TCgArray (t, _) -> TBuf (t, false)
+        | t -> t
+      ) t_args in
+      try
+        (* This throws and aborts if there are some const generics left. *)
+        let t_args = List.map (self#visit_typ (scope_env, true)) t_args in
+
+        (* We're good. Find the allocated C name for our declaration, and allocate a new C name for
+           the extra declaration *)
+        let c_name = Option.get (GlobalNames.lookup (fst scope_env) name) in
+        let new_name = fst name, snd name ^ "_" in
+        self#record scope_env ~is_type:false ~is_external:true flags new_name;
+        let new_c_name = Option.get (GlobalNames.lookup (fst scope_env) new_name) in
+
+        (* We build: #define <<c_name>>(x0, ..., xn, _ret_t) \
+           <<new_c_name>>(x0, ..., xn) *)
+        let prelude =
+          (* Names of the arguments *)
+          let names =
+            if List.length hints = List.length t_args then
+              hints
+            else
+              List.init (List.length t_args) (fun i -> KPrint.bsprintf "x_%d" i)
+          in
+          KPrint.bsprintf "#define %s(%s) %s(%s)"
+            c_name (String.concat ", " (names @ [ "_ret_t" ]))
+            new_c_name (String.concat ", " names)
+        in
+        DExternal (cc, [ Common.Prologue prelude ] @ flags, 0, n, new_name, Helpers.fold_arrow t_args t_ret, hints)
+      with Exit ->
+        DExternal (cc, flags, n_cgs, n, name, t, hints)
+    else
+      DExternal (cc, flags, n_cgs, n, name, t, hints)
+end
+
+let build_cg_macros = object(self)
+  inherit [_] Krml.Ast.reduce
+  method private zero = Krml.Idents.LidSet.empty
+  method private plus = Krml.Idents.LidSet.union
+  method! visit_DExternal () _ _ n_cgs n name _ _ =
+    if n > 0 || n_cgs > 0 then
+      Krml.Idents.LidSet.singleton name
+    else
+      self#zero
+end