From 7dfb6a445266c6eaf963106e891db580020a24cc Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 14 Feb 2024 14:56:29 -0800 Subject: [PATCH 1/2] Several improvements in support of Kyber. - Rather than bailing when trying to emit external, const-generic functions, see first if we can anticipate on C's array decay rules to replace e.g. t[N] in the signature with t*, in the hope that doing so removes all occurrences of const-generic variables. If it does, then we can emit this prototype! (And then length of the arrays will be known since the actual value of the const generic argument is passed at runtime.) - For functions that do not pass this test, rely on an upstream fix to prop up the visibility of all the monomorphized type declarations that may be passed to the external at every call-site. This means that the external can now be implemented using a macro with the right type definitions in scope, which is essential for externals. - Extend the syntax of configuration files with two new keys: include_in_h, a list of extra headers to be included in the .h for this file; and include_in_c, which is pretty self-explanatory. This all allows removing a gigantic, sed-based hack for Kyber! --- bin/main.ml | 22 +++++-------- lib/Bundles.ml | 18 +++++++++-- lib/Cleanup3.ml | 84 +++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 107 insertions(+), 17 deletions(-) create mode 100644 lib/Cleanup3.ml diff --git a/bin/main.ml b/bin/main.ml index 97557ea..021e8ef 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -127,8 +127,10 @@ 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; @@ -136,24 +138,16 @@ Supported options:|} 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 diff --git a/lib/Bundles.ml b/lib/Bundles.ml index cd844fd..09e86e0 100644 --- a/lib/Bundles.ml +++ b/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" with + | None -> [] + | Some (`A include_) -> List.map (function `String s -> Krml.Options.HeaderOnly name, s | _ -> parsing_error "include must be a string") include_ + | Some _ -> parsing_error "include 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 diff --git a/lib/Cleanup3.ml b/lib/Cleanup3.ml new file mode 100644 index 0000000..7229e73 --- /dev/null +++ b/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(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 <>(x0, ..., xn, _ret_t) \ + <>(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 From 796e36d9cf58596371fe1fcce8df35ec9849a05c Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 14 Feb 2024 18:53:08 -0800 Subject: [PATCH 2/2] Update nix flake --- flake.lock | 6 +++--- lib/Bundles.ml | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/flake.lock b/flake.lock index e5680b0..d07613e 100644 --- a/flake.lock +++ b/flake.lock @@ -167,11 +167,11 @@ ] }, "locked": { - "lastModified": 1707785177, - "narHash": "sha256-DPUINtVtpTiK5fb01JKv6pFR28QCUsyzf47OegGrg7s=", + "lastModified": 1707954613, + "narHash": "sha256-UVixnlHYQYicZOpr9iQm47aFmsaMGFpG/q3L8sRuwck=", "owner": "FStarLang", "repo": "karamel", - "rev": "7cf2361746b4c26877bd7f1a2c48ffb889eeab12", + "rev": "08bfa78ae1df5639446e6c5897b07c9823fbf3b0", "type": "github" }, "original": { diff --git a/lib/Bundles.ml b/lib/Bundles.ml index 09e86e0..a5fe7e7 100644 --- a/lib/Bundles.ml +++ b/lib/Bundles.ml @@ -64,10 +64,10 @@ let parse_file (v: Yaml.value): file = | Some _ -> parsing_error "private not a list" in let include_ = - match lookup "include" with + match lookup "include_in_h" with | None -> [] - | Some (`A include_) -> List.map (function `String s -> Krml.Options.HeaderOnly name, s | _ -> parsing_error "include must be a string") include_ - | Some _ -> parsing_error "include must be a list" + | 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