From b221a8c63f4c5400c9584a46b257ff29afb8e05d Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 5 Dec 2023 17:15:25 -0800 Subject: [PATCH 01/21] Add a field for the number of parameters that should be understood to be const generics. This has no effect on the existing binder representation, transformation passes, or anything else whatsoever, and should only be useful for eurydice --- lib/Ast.ml | 37 +++++++++++---------- lib/AstToCFlat.ml | 18 ++++++----- lib/AstToCStar.ml | 16 +++++---- lib/AstToMiniRust.ml | 14 ++++---- lib/Builtin.ml | 62 +++++++++++++++++------------------ lib/Bundles.ml | 8 ++--- lib/Checker.ml | 16 +++++---- lib/DataTypes.ml | 72 ++++++++++++++++++++++------------------- lib/DeBruijn.ml | 69 +++++++++++++++++++++++++++++++++++++++ lib/Diagnostics.ml | 6 ++-- lib/GcTypes.ml | 2 +- lib/Helpers.ml | 3 +- lib/Inlining.ml | 36 ++++++++++----------- lib/InputAstToAst.ml | 14 ++++---- lib/Monomorphization.ml | 70 ++++++++++++++++++++------------------- lib/Output.ml | 2 +- lib/PrintAst.ml | 13 +++++--- lib/Simplify.ml | 57 ++++++++++++++++---------------- lib/SimplifyC89.ml | 4 +-- lib/SimplifyMerge.ml | 4 +-- lib/SimplifyWasm.ml | 2 +- lib/Structs.ml | 25 +++++++------- lib/UseAnalysis.ml | 10 +++--- 23 files changed, 330 insertions(+), 230 deletions(-) diff --git a/lib/Ast.ml b/lib/Ast.ml index e25c2cd8a..6cfe1add4 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -51,6 +51,8 @@ type typ = | TArray of typ * constant (** appears when we start hoisting buffer definitions to their enclosing * push frame *) + | TCgArray of typ * int + (** for monomorphization of stuff coming from Rust (eurydice) *) | TQualified of lident (** a reference to a type that has been introduced via a DType *) | TArrow of typ * typ @@ -189,7 +191,7 @@ type expr' = | EIgnore of expr | EApp of expr * expr list - | ETApp of expr * typ_wo list + | ETApp of expr * expr list * typ_wo list | EPolyComp of poly_comp * typ_wo | ELet of binder * expr * expr | EFun of binder list * expr * typ_wo @@ -416,12 +418,12 @@ and files = file list and decl = - | DFunction of calling_convention option * flag list * int * typ * lident * binders_w * expr_w + | DFunction of calling_convention option * flag list * int * int * typ * lident * binders_w * expr_w | DGlobal of flag list * lident * int * typ * expr_w | DExternal of calling_convention option * flag list * int * lident * typ * string list (** String list: only for pretty-printing purposes, names of the first few * known arguments. *) - | DType of lident * flag list * int * type_def + | DType of lident * flag list * int * int * type_def and binders_w = binder_w list @@ -496,14 +498,14 @@ class ['self] map = object (self: 'self) let e = self#visit_expr env e in bs, p, e - method! visit_DType env lid flags n d = + method! visit_DType env lid flags n_cg n d = let lid = self#visit_lident env lid in let flags = self#visit_flags env flags in let env = self#extend_tmany env n in let d = self#visit_type_def env d in - DType (lid, flags, n, d) + DType (lid, flags, n_cg, n, d) - method! visit_DFunction env cc flags n t lid bs e = + method! visit_DFunction env cc flags n_cg n t lid bs e = let cc = self#visit_calling_convention_option env cc in let flags = self#visit_flags env flags in let env = self#extend_tmany env n in @@ -512,13 +514,14 @@ class ['self] map = object (self: 'self) let bs = self#visit_binders_w env bs in let env = self#extend_many env bs in let e = self#visit_expr_w env e in - DFunction (cc, flags, n, t, lid, bs, e) + DFunction (cc, flags, n_cg, n, t, lid, bs, e) - method! visit_ETApp env e ts = + method! visit_ETApp env e es ts = let ts = List.map (self#visit_typ_wo env) ts in + let es = List.map (self#visit_expr env) es in let env = self#extend_tmany (fst env) (List.length ts) in let e = self#visit_expr_w env e in - ETApp (e, ts) + ETApp (e, es, ts) end class ['self] iter = object (self: 'self) @@ -551,13 +554,13 @@ class ['self] iter = object (self: 'self) self#visit_pattern env p; self#visit_expr env e - method! visit_DType env lid flags n d = + method! visit_DType env lid flags _n_cg n d = self#visit_lident env lid; self#visit_flags env flags; let env = self#extend_tmany env n in self#visit_type_def env d - method! visit_DFunction env cc flags n t lid bs e = + method! visit_DFunction env cc flags _n_cg n t lid bs e = self#visit_calling_convention_option env cc; self#visit_flags env flags; let env = self#extend_tmany env n in @@ -602,14 +605,14 @@ class virtual ['self] reduce = object (self: 'self) let e = self#visit_expr env e in KList.reduce self#plus [ bs'; p; e ] - method! visit_DType env lid flags n d = + method! visit_DType env lid flags _n_cg n d = let lid = self#visit_lident env lid in let flags = self#visit_flags env flags in let env = self#extend_tmany env n in let d = self#visit_type_def env d in KList.reduce self#plus [ lid; flags; d ] - method! visit_DFunction env cc flags n t lid bs e = + method! visit_DFunction env cc flags _n_cg n t lid bs e = let cc = self#visit_calling_convention_option env cc in let flags = self#visit_flags env flags in let env = self#extend_tmany env n in @@ -634,16 +637,16 @@ let with_type typ node = { typ; node } let lid_of_decl = function - | DFunction (_, _, _, _, lid, _, _) + | DFunction (_, _, _, _, _, lid, _, _) | DGlobal (_, lid, _, _, _) | DExternal (_, _, _, lid, _, _) - | DType (lid, _, _, _) -> + | DType (lid, _, _, _, _) -> lid let flags_of_decl = function - | DFunction (_, flags, _, _, _, _, _) + | DFunction (_, flags, _, _, _, _, _, _) | DGlobal (flags, _, _, _, _) - | DType (_, flags, _, _) + | DType (_, flags, _, _, _) | DExternal (_, flags, _, _, _, _) -> flags diff --git a/lib/AstToCFlat.ml b/lib/AstToCFlat.ml index 40fc613ca..8a70b0ec7 100644 --- a/lib/AstToCFlat.ml +++ b/lib/AstToCFlat.ml @@ -340,7 +340,7 @@ let name_flat_layouts = object (self) List.concat_map (fun d -> current_prefix <- fst (lid_of_decl d); let d = self#visit_decl () d in - let ds: decl list = List.map (fun (name, fields) -> DType (name, [], 0, Flat fields)) new_decls in + let ds: decl list = List.map (fun (name, fields) -> DType (name, [], 0, 0, Flat fields)) new_decls in new_decls <- []; List.rev_append ds [ d ] ) decls @@ -352,7 +352,7 @@ let populate env files = let env = List.fold_left (fun env (_, decls) -> List.fold_left (fun env decl -> match decl with - | DType (_, _, _, Enum idents) -> + | DType (_, _, _, _, Enum idents) -> KList.fold_lefti (fun i env ident -> assert (i < 256); { env with enums = LidMap.add ident i env.enums } @@ -369,9 +369,9 @@ let populate env files = let env = List.fold_left (fun env (_, decls) -> List.fold_left (fun env decl -> match decl with - | DType (lid, _, _, Enum _) -> + | DType (lid, _, _, _, Enum _) -> { env with layouts = LidMap.add lid LEnum env.layouts } - | DType (lid, _, _, Flat fields) -> + | DType (lid, _, _, _, Flat fields) -> (* Need to pass in the layout of previous structs *) begin try let l = flat_layout env (fields_of_struct fields) in @@ -723,13 +723,15 @@ and mk_expr (env: env) (locals: locals) (e: expr): locals * CF.expr = | EOpen _ -> invalid_arg "mk_expr (EOpen)" - | EApp ({ node = ETApp ({ node = EQualified (["LowStar"; "Ignore"],"ignore"); _ }, _); _ }, [ e ]) -> + | EApp ({ node = ETApp ({ node = EQualified (["LowStar"; "Ignore"],"ignore"); _ }, cgs, _); _ }, [ e ]) -> + assert (cgs = []); let locals, e = mk_expr env locals e in (* This is slightly ill-typed since everywhere else the result of intermediary sequence bits is units, but that's fine *) locals, CF.Sequence [ e; cflat_unit ] - | EApp ({ node = ETApp ({ node = EQualified (["Lib"; "Memzero0"],"memzero"); _ }, _); _ }, [ dst; len ]) -> + | EApp ({ node = ETApp ({ node = EQualified (["Lib"; "Memzero0"],"memzero"); _ }, cgs, _); _ }, [ dst; len ]) -> + assert (cgs = []); (* TODO: now that the C backend is generic for type applications, do the same here and have generic support for ETApp. Idea: reuse the JSON representation of a type (used for layouts) and pass that to the JS @@ -1026,8 +1028,8 @@ let mk_wrapper orig_name n_args locals = let mk_decl env (d: decl): env * CF.decl list = match d with - | DFunction (_, flags, n, ret, name, args, body) -> - assert (n = 0); + | DFunction (_, flags, n_cgs, n, ret, name, args, body) -> + assert (n = 0 && n_cgs = 0); let public = not (List.mem Common.Private flags) in let locals, env = List.fold_left (fun (locals, env) b -> let locals, _, env = extend env b locals in diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml index 4c55cf04e..193e59f54 100644 --- a/lib/AstToCStar.ml +++ b/lib/AstToCStar.ml @@ -358,10 +358,12 @@ and mk_expr env in_stmt e = | EConstant c -> CStar.Constant c - | EApp ({ node = ETApp (e, ts); _ }, es) when !Options.allow_tapps || whitelisted_tapp e -> + | EApp ({ node = ETApp (e, cgs, ts); _ }, es) when !Options.allow_tapps || whitelisted_tapp e -> + assert (cgs = []); unit_to_void env e es (List.map (fun t -> CStar.Type (mk_type env t)) ts) - | ETApp (e, ts) when !Options.allow_tapps || whitelisted_tapp e -> + | ETApp (e, cgs, ts) when !Options.allow_tapps || whitelisted_tapp e -> + assert (cgs = []); CStar.Call (mk_expr env e, List.map (fun t -> CStar.Type (mk_type env t)) ts) | EApp ({ node = EOp (op, w); _ }, [ _; _ ]) when is_arith op w -> @@ -802,6 +804,8 @@ and mk_return_type env = function fatal_error "Internal failure: TTuple not desugared here" | TAnonymous t -> mk_type_def env t + | TCgArray _ -> + fatal_error "Internal failure: TCgArray not desugared here" and mk_type env = function @@ -876,8 +880,8 @@ and mk_declaration m env d: (CStar.decl * _) option = in match d with - | DFunction (cc, flags, n, t, name, binders, body) -> - assert (n = 0); + | DFunction (cc, flags, n_cgs, n, t, name, binders, body) -> + assert (n = 0 && n_cgs = 0); let env = locate env (InTop name) in Some (wrap_throw (string_of_lident name) (lazy begin let t = mk_return_type env t in @@ -909,10 +913,10 @@ and mk_declaration m env d: (CStar.decl * _) option = in Some (CStar.External (name, add_cc (mk_type env t), flags, pp), []) - | DType (name, flags, _, Forward k) -> + | DType (name, flags, _, _, Forward k) -> Some (CStar.TypeForward (name, flags, k), [ GlobalNames.to_c_name m name ]) - | DType (name, flags, 0, def) -> + | DType (name, flags, 0, 0, def) -> Some (CStar.Type (name, mk_type_def env def, flags), [ GlobalNames.to_c_name m name ] ) | DType _ -> diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index eb8f30dd1..88406d506 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -398,6 +398,7 @@ let rec translate_type (env: env) (t: Ast.typ): MiniRust.typ = | TBound i -> Bound i | TTuple _ -> failwith "TODO: TTuple" | TAnonymous _ -> failwith "unexpected: we don't compile data types going to Rust" + | TCgArray _ -> failwith "Impossible: TCgArray" (* Expressions *) @@ -557,7 +558,8 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): Min | EApp ({ node = EQualified ([ "LowStar"; "BufferOps" ], s); _ }, e1 :: e2 :: _ ) when KString.starts_with s "op_Star_Equals__" -> Assign (Deref (translate_expr env e1), translate_expr env e2) - | EApp ({ node = ETApp (e, ts); _ }, es) -> + | EApp ({ node = ETApp (e, cgs, ts); _ }, es) -> + assert (cgs = []); let es = match es with | [ { typ = TUnit; node } ] -> assert (node = EUnit); [] @@ -571,7 +573,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): Min | _ -> es in Call (translate_expr env e, [], List.map (translate_expr env) es) - | ETApp (_, _) -> + | ETApp (_, _, _) -> failwith "TODO: ETApp" | EPolyComp _ -> failwith "unexpected: EPolyComp" @@ -780,11 +782,11 @@ let translate_decl env (d: Ast.decl) = false in match d with - | Ast.DFunction (_, _, _, _, lid, _, _) when is_handled_primitively lid -> + | Ast.DFunction (_, _, _, _, _, lid, _, _) when is_handled_primitively lid -> env, None - | Ast.DFunction (_cc, flags, type_parameters, t, lid, args, body) -> - assert (type_parameters = 0); + | Ast.DFunction (_cc, flags, n_cgs, type_parameters, t, lid, args, body) -> + assert (type_parameters = 0 && n_cgs = 0); if Options.debug "rs" then KPrint.bprintf "Ast.DFunction (%a)\n" PrintAst.Ops.plid lid; let args, body = @@ -826,7 +828,7 @@ let translate_decl env (d: Ast.decl) = let env = push_global env lid (name, make_poly (translate_type env t) type_parameters) in env, None - | Ast.DType (name, _, _, _) -> + | Ast.DType (name, _, _, _, _) -> Warn.failwith "TODO: Ast.DType (%a)\n" PrintAst.Ops.plid name let identify_path_components_rev filename = diff --git a/lib/Builtin.ml b/lib/Builtin.ml index 151b31143..5fcd46266 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -23,21 +23,21 @@ let prims: file = let mk_val = mk_val [ "Prims" ] in let dtuple10 = TApp ((["Prims"],"dtuple2"), [ TBound 1; TBound 0 ]) in "Prims", [ - DType ((["Prims"], "list"), [ Common.GcType ], 1, Variant [ + DType ((["Prims"], "list"), [ Common.GcType ], 0, 1, Variant [ "Nil", []; "Cons", [ "hd", (TBound 0, false); "tl", (TApp ((["Prims"],"list"), [ TBound 0 ]), false) ] ]); - DType ((["Prims"], "dtuple2"), [], 2, Variant [ + DType ((["Prims"], "dtuple2"), [], 0, 2, Variant [ "Mkdtuple2", [ "fst", (TBound 1, false); "snd", (TBound 0, false) ] ]); DFunction (None, - [ Common.Private ], 2, TBound 1, + [ Common.Private ], 0, 2, TBound 1, (["Prims"], "__proj__Mkdtuple2__item___1"), [ fresh_binder "pair" dtuple10 ], (* match pair with *) @@ -53,7 +53,7 @@ let prims: file = with_type (TBound 1) (EBound 0) ]))); DFunction (None, - [ Common.Private ], 2, TBound 0, + [ Common.Private ], 0, 2, TBound 0, (["Prims"], "__proj__Mkdtuple2__item___2"), [ fresh_binder "pair" dtuple10 ], (* match pair with *) @@ -82,8 +82,8 @@ let prims: file = mk_unop "abs"; mk_val "strcat" (TArrow (t_string, TArrow (t_string, t_string))); mk_val "string_of_int" (TArrow (TInt K.CInt, t_string)); - DType ((["Prims"], "prop"), [], 0, Abbrev TUnit); - DType ((["Prims"], "nat"), [ Common.Private ], 0, Abbrev (TQualified (["Prims"], "int"))) + DType ((["Prims"], "prop"), [], 0, 0, Abbrev TUnit); + DType ((["Prims"], "nat"), [ Common.Private ], 0, 0, Abbrev (TQualified (["Prims"], "int"))) ] (* JP: as a guiding principle: builtins that are from LowStar.Monotonic.Buffer @@ -104,7 +104,7 @@ let buffer: file = * break * ret *) - DFunction (None, [ ], 1, TBool, ([ "FStar"; "Buffer" ], "eqb"), + DFunction (None, [ ], 0, 1, TBool, ([ "FStar"; "Buffer" ], "eqb"), [ fresh_binder "b1" (TBuf (TBound 0, true)); fresh_binder "b2" (TBuf (TBound 0, true)); fresh_binder "len" uint32 ], @@ -128,7 +128,7 @@ let buffer: file = eunit)))); with_type TBool (EBound 0)])))); - DFunction (None, [ Common.MustDisappear ], 1, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 1, TUnit, ([ "FStar"; "Buffer" ], "recall"), [ fresh_binder "x" (TBuf (TBound 0, true)) ], eunit); @@ -136,47 +136,47 @@ let buffer: file = let monotonic_hs: file = "FStar_Monotonic_HyperStack", [ - DType (([ "FStar"; "Monotonic"; "HyperStack" ], "mem"), [], 0, Abbrev TUnit); + DType (([ "FStar"; "Monotonic"; "HyperStack" ], "mem"), [], 0, 0, Abbrev TUnit); DGlobal ([], ([ "FStar"; "Monotonic"; "HyperStack" ], "root"), 0, TUnit, eunit); ] let monotonic_hh: file = "FStar_Monotonic_HyperHeap", [ - DType (([ "FStar"; "Monotonic"; "HyperHeap" ], "rid"), [], 0, Abbrev TUnit) + DType (([ "FStar"; "Monotonic"; "HyperHeap" ], "rid"), [], 0, 0, Abbrev TUnit) ] let hs: file = "FStar_HyperStack_ST", [ - DFunction (None, [ Common.MustDisappear ], 0, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 0, TUnit, ([ "FStar"; "HyperStack"; "ST" ], "new_region"), [ fresh_binder "x" TUnit ], with_unit (EBound 0)); - DFunction (None, [ Common.MustDisappear ], 0, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 0, TUnit, ([ "FStar"; "HyperStack"; "ST" ], "new_colored_region"), [ fresh_binder "x" TUnit; fresh_binder "x" (TInt K.CInt) ], with_unit (EBound 1)); - DFunction (None, [ Common.MustDisappear ], 0, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 0, TUnit, ([ "FStar"; "HyperStack"; "ST" ], "recall"), [ fresh_binder "x" TAny ], eunit); - DFunction (None, [ Common.MustDisappear ], 0, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 0, TUnit, ([ "FStar"; "HyperStack"; "ST" ], "testify"), [ fresh_binder "x" TAny ], eunit); - DFunction (None, [ Common.MustDisappear ], 0, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 0, TUnit, ([ "FStar"; "HyperStack"; "ST" ], "testify_forall"), [ fresh_binder "x" TAny ], eunit); - DFunction (None, [ Common.MustDisappear ], 0, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 0, TUnit, ([ "FStar"; "HyperStack"; "ST" ], "testify_forall_region_contains_pred"), [ fresh_binder "x" TAny; fresh_binder "y" TAny ], eunit); - DFunction (None, [ Common.MustDisappear ], 0, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 0, TUnit, ([ "FStar"; "HyperStack"; "ST" ], "recall_region"), [ fresh_binder "x" TUnit ], with_unit (EBound 0)); - DFunction (None, [ Common.MustDisappear ], 0, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 0, TUnit, ([ "FStar"; "HyperStack"; "ST" ], "mr_witness"), [ fresh_binder "x" TUnit; @@ -186,15 +186,15 @@ let hs: file = fresh_binder "x" TUnit; ], eunit); - DType (([ "FStar"; "HyperStack"; "ST" ], "erid"), [], 0, Abbrev TUnit); - DType (([ "FStar"; "HyperStack"; "ST" ], "ex_rid"), [], 0, Abbrev TUnit); - DType (([ "FStar"; "HyperStack"; "ST" ], "witnessed"), [ Common.MustDisappear ], 1, Abbrev TUnit); + DType (([ "FStar"; "HyperStack"; "ST" ], "erid"), [], 0, 0, Abbrev TUnit); + DType (([ "FStar"; "HyperStack"; "ST" ], "ex_rid"), [], 0, 0, Abbrev TUnit); + DType (([ "FStar"; "HyperStack"; "ST" ], "witnessed"), [ Common.MustDisappear ], 0, 1, Abbrev TUnit); ] let dyn: file = let void_star = TBuf (TAny, false) in "FStar_Dyn", [ - DFunction (None, [], 1, void_star, + DFunction (None, [], 0, 1, void_star, ([ "FStar"; "Dyn" ], "mkdyn"), [ fresh_binder "x" (TBound 0) ], with_type void_star (ECast (with_type (TBound 0) (EBound 0), void_star))) @@ -226,15 +226,15 @@ let steel_arrayarith : file = let lowstar_monotonic_buffer: file = "LowStar_Monotonic_Buffer", [ - DFunction (None, [ Common.MustDisappear ], 3, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 3, TUnit, ([ "LowStar"; "Monotonic"; "Buffer" ], "recall"), [ fresh_binder "x" (TBuf (TBound 2, false)) ], eunit); - DFunction (None, [ Common.MustDisappear ], 3, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 3, TUnit, ([ "LowStar"; "Monotonic"; "Buffer" ], "frameOf"), [ fresh_binder "x" (TBuf (TBound 2, false)) ], eunit); - DType (([ "LowStar"; "Monotonic"; "Buffer" ], "loc_disjoint"), [ Common.MustDisappear ], 2, Abbrev TUnit); + DType (([ "LowStar"; "Monotonic"; "Buffer" ], "loc_disjoint"), [ Common.MustDisappear ], 0, 2, Abbrev TUnit); ] let lowstar_buffer: file = @@ -266,7 +266,7 @@ let lowstar_endianness: file = (* assume val store16_le: buffer uint8 -> uint16 -> unit *) mk_val (fst store_lid) (snd store_lid) store_t; (* let store16_le_i #_ #_ b i x = store16_le (b + i) x *) - DFunction (None, [ Common.MustDisappear ], 2, TUnit, + DFunction (None, [ Common.MustDisappear ], 0, 2, TUnit, store_i_lid, [ fresh_binder "b" buf8; fresh_binder "i" int32; fresh_binder "x" t ], with_unit (EApp (with_type store_t (EQualified store_lid), @@ -283,7 +283,7 @@ let lowstar_endianness: file = (* assume val load16_le: buffer uint8 -> uint16 *) mk_val (fst load_lid) (snd load_lid) load_t; (* let load16_le_i #_ #_ b i = load16_le (b + i) *) - DFunction (None, [ Common.MustDisappear ], 2, t, + DFunction (None, [ Common.MustDisappear ], 0, 2, t, load_i_lid, [ fresh_binder "b" buf8; fresh_binder "i" int32 ], with_type t (EApp (with_type load_t (EQualified load_lid), @@ -351,7 +351,7 @@ let addendum = [ ] let make_abstract_function_or_global = function - | DFunction (cc, flags, n, t, name, bs, _) -> + | DFunction (cc, flags, _, n, t, name, bs, _) -> let t = fold_arrow (List.map (fun b -> b.typ) bs) t in if n = 0 then Some (DExternal (cc, flags, 0, name, t, List.map (fun x -> x.node.name) bs)) @@ -362,9 +362,9 @@ let make_abstract_function_or_global = function Some (DExternal (None, flags, 0, name, t, [])) else None - | DType (name, flags, _, _) when List.mem Common.AbstractStruct flags -> + | DType (name, flags, _, _, _) when List.mem Common.AbstractStruct flags -> (* We assume the module doesn't lie and the CAbstractStruct will type-check in C. *) - Some (DType (name, List.filter ((<>) Common.AbstractStruct) flags, 0, Forward FStruct)) + Some (DType (name, List.filter ((<>) Common.AbstractStruct) flags, 0, 0, Forward FStruct)) | d -> Some d @@ -376,7 +376,7 @@ let make_abstract_function_or_global = function * - but we keep the gte_mask and eq_mask functions *) let make_abstract (name, decls) = name, KList.filter_map (function - | DType (_, _, _, Abbrev _) as t -> + | DType (_, _, _, _, Abbrev _) as t -> Some t | DType _ -> None diff --git a/lib/Bundles.ml b/lib/Bundles.ml index 60fa3bed8..f44c908aa 100644 --- a/lib/Bundles.ml +++ b/lib/Bundles.ml @@ -48,12 +48,12 @@ let make_one_bundle (bundle: Bundle.t) (files: file list) (used: (int * Bundle.t flags in function - | DFunction (cc, flags, n, typ, name, binders, body) -> - DFunction (cc, add_if name flags, n, typ, name, binders, body) + | DFunction (cc, flags, n_cgs, n, typ, name, binders, body) -> + DFunction (cc, add_if name flags, n_cgs, n, typ, name, binders, body) | DGlobal (flags, name, n, typ, body) -> DGlobal (add_if name flags, name, n, typ, body) - | DType (lid, flags, n, def) -> - DType (lid, add_if lid flags, n, def) + | DType (lid, flags, n_cgs, n, def) -> + DType (lid, add_if lid flags, n_cgs, n, def) | DExternal (cc, flags, n, lid, t, pp) -> DExternal (cc, add_if lid flags, n, lid, t, pp) in diff --git a/lib/Checker.ml b/lib/Checker.ml index f357a5617..7fb849e32 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -54,6 +54,8 @@ type env = { location: loc list; enums: lident M.t; warn: bool; + n_cgs: int; + (* Number of const generics, useful only for type-checking stuff coming in from Eurydice pre-monomorphization. *) } let empty: env = { @@ -62,7 +64,8 @@ let empty: env = { types = M.empty; location = []; enums = M.empty; - warn = false + warn = false; + n_cgs = 0 } let push env binder = @@ -109,7 +112,7 @@ let populate_env files = List.fold_left (fun env (_, decls) -> List.fold_left (fun env decl -> match decl with - | DType (lid, _, _, typ) -> + | DType (lid, _, _, _, typ) -> let env = match typ with | Enum tags -> List.fold_left (fun env tag -> @@ -122,7 +125,7 @@ let populate_env files = | DGlobal (_, lid, n, t, _) -> assert (n = 0); { env with globals = M.add lid t env.globals } - | DFunction (_, _, n, ret, lid, binders, _) -> + | DFunction (_, _, _, n, ret, lid, binders, _) -> if not !Options.allow_tapps && n <> 0 then Warn.fatal_error "%a is polymorphic\n" plid lid; let t = List.fold_right (fun b t2 -> TArrow (b.typ, t2)) binders ret in @@ -197,7 +200,7 @@ and check_decl env d = if Options.debug "checker" then KPrint.bprintf "checking %a\n" plid (lid_of_decl d); match d with - | DFunction (_, _, n, t, name, binders, body) -> + | DFunction (_, _, _n_cgs, n, t, name, binders, body) -> assert (!Options.allow_tapps || n = 0); let env = List.fold_left push env binders in let env = locate env (InTop name) in @@ -272,7 +275,7 @@ and check env t e = and check' env t e = let c t' = check_subtype env t' t in match e.node with - | ETApp (e, _) -> + | ETApp (e, _, _) -> (* JP: is this code even reachable? *) (* Equalities are type checked with Any *) (match e.node with EOp ((K.Eq | K.Neq), _) -> () | _ -> assert false); @@ -521,7 +524,7 @@ and best_buffer_type l t1 e2 = and infer' env e = match e.node with - | ETApp (e, ts) -> + | ETApp (e, cs, ts) -> begin match e.node with | EOp ((K.Eq | K.Neq), _) -> (* Special incorrect encoding of polymorphic equalities *) @@ -529,6 +532,7 @@ and infer' env e = TArrow (t, TArrow (t, TBool)) | _ -> let t = infer env e in + let t = DeBruijn.subst_ctn env.n_cgs cs t in DeBruijn.subst_tn ts t end diff --git a/lib/DataTypes.ml b/lib/DataTypes.ml index 337d45786..896e54b0f 100644 --- a/lib/DataTypes.ml +++ b/lib/DataTypes.ml @@ -35,9 +35,10 @@ let remove_unused_type_arguments files = let def_map = Helpers.build_map files (fun map d -> match d with - | DType (lid, _, n, d) -> + | DType (lid, _, _, n, d) -> + (* TODO: ignore unused const generics *) Hashtbl.add map lid (`Typ (n, d)) - | DFunction (_, _, n, t_ret, lid, bs, body) -> + | DFunction (_, _, _, n, t_ret, lid, bs, body) -> let ts = List.map (fun b -> b.typ) bs in Hashtbl.add map lid (`Fun (n, t_ret :: ts, body)) | _ -> () @@ -66,7 +67,8 @@ let remove_unused_type_arguments files = method! visit_TApp env lid args = self#visit_app env lid args - method! visit_ETApp env e args = + method! visit_ETApp env e _ args = + (* TODO: for now, we ignore unused const generics *) let lid = assert_elid e.node in self#visit_app (fst env) lid args end in @@ -94,7 +96,7 @@ let remove_unused_type_arguments files = (* Then, if the i-th type parameter is unused, we remove it from the type * definition... *) - method! visit_DType env lid flags n def = + method! visit_DType env lid flags n_cgs n def = let def = self#visit_type_def env def in let rec chop kept i def = if i = n then @@ -107,7 +109,7 @@ let remove_unused_type_arguments files = chop kept (i + 1) def in let n, def = chop 0 0 def in - DType (lid, flags, n, def) + DType (lid, flags, n_cgs, n, def) (* ... and also any use of it. *) method! visit_TApp env lid args = @@ -123,7 +125,7 @@ let remove_unused_type_arguments files = else TQualified lid - method! visit_DFunction env cc flags n ret lid binders def = + method! visit_DFunction env cc flags n_cgs n ret lid binders def = let binders = self#visit_binders_w env binders in let ret = self#visit_typ env ret in let def = self#visit_expr_w env def in @@ -140,9 +142,10 @@ let remove_unused_type_arguments files = chop kept (i + 1) (def, binders, ret) in let n, (def, binders, ret) = chop 0 0 (def, binders, ret) in - DFunction (cc, flags, n, ret, lid, binders, def) + DFunction (cc, flags, n_cgs, n, ret, lid, binders, def) - method! visit_ETApp env e args = + method! visit_ETApp env e cgs args = + assert (cgs = []); let lid = assert_elid e.node in let args = List.map (self#visit_typ_wo env) args in let args = KList.filter_mapi (fun i arg -> @@ -152,7 +155,7 @@ let remove_unused_type_arguments files = None ) args in if List.length args > 0 then - ETApp (e, args) + ETApp (e, [], args) else e.node end in @@ -192,7 +195,7 @@ let one_non_constant_branch branches = let build_scheme_map files = let map = build_map files (fun map -> function - | DType (lid, _, 0, Variant branches) -> + | DType (lid, _, _, 0, Variant branches) -> let _constant, non_constant = List.partition (fun (_, fields) -> List.length fields = 0 ) branches in @@ -211,7 +214,7 @@ let build_scheme_map files = | _ -> () end - | DType (lid, _, 0, Flat [ _, (t, _) ]) -> + | DType (lid, _, _, 0, Flat [ _, (t, _) ]) -> Hashtbl.add map lid (Eliminate t) | _ -> () @@ -221,7 +224,7 @@ let build_scheme_map files = * forward struct declaration is what allows us to compile these types. *) (object inherit [_] iter - method visit_DType _ lid _ _ d = + method visit_DType _ lid _ _ _ d = (* But if it turns out we can't eliminate, restore what otherwise would've * been the compilation scheme. (See OCaml doc for the behavior of add.) *) if Helpers.is_forward d then @@ -315,7 +318,7 @@ let allocate_tag enums preferred_lid tags = | exception Not_found -> Hashtbl.add enums tags preferred_lid; (* Private will be removed, if needed, by the cross-call analysis. *) - Fresh (DType (preferred_lid, [ Common.Private ], 0, Enum tags)) + Fresh (DType (preferred_lid, [ Common.Private ], 0, 0, Enum tags)) let field_for_tag = "tag" let field_for_union = "val" @@ -453,30 +456,31 @@ let compile_simple_matches (map, enums) = object(self) pending := decl :: !pending; preferred_lid - method! visit_DType env lid flags n def = + method! visit_DType env lid flags n_cgs n def = + assert (n_cgs = 0); let def = self#visit_type_def env def in match def with | Variant branches -> assert (n = 0); begin match Hashtbl.find map lid with | exception Not_found -> - DType (lid, flags, 0, Variant branches) + DType (lid, flags, 0, 0, Variant branches) | Eliminate t -> - DType (lid, flags, 0, Abbrev t) + DType (lid, flags, 0, 0, Abbrev t) | ToTaggedUnion _ -> ignore (self#allocate_enum_lid lid branches); - DType (lid, flags, 0, Variant branches) + DType (lid, flags, 0, 0, Variant branches) | ToEnum -> let tags = List.map (fun (cons, _fields) -> mk_tag_lid lid cons) branches in begin match allocate_tag enums lid tags with | Found other_lid -> - DType (lid, flags, 0, Abbrev (TQualified other_lid)) + DType (lid, flags, 0, 0, Abbrev (TQualified other_lid)) | Fresh decl -> decl end | ToFlat _ -> let fields = List.map (fun (f, t) -> Some f, t) (snd (List.hd branches)) in - DType (lid, flags, 0, Flat fields) + DType (lid, flags, 0, 0, Flat fields) | ToFlatTaggedUnion branches -> ignore (self#allocate_enum_lid lid branches); (* First field for the tag, then flatly, the fields of the only one @@ -484,20 +488,20 @@ let compile_simple_matches (map, enums) = object(self) let f_tag = field_for_tag, (TQualified (self#allocate_enum_lid lid branches), false) in let fields = snd (one_non_constant_branch branches) in let fields = List.map (fun (f, t) -> Some f, t) (f_tag :: fields) in - DType (lid, flags, 0, Flat fields) + DType (lid, flags, 0, 0, Flat fields) end | Flat fields -> assert (n = 0); begin match Hashtbl.find map lid with | exception Not_found -> - DType (lid, flags, 0, Flat fields) + DType (lid, flags, 0, 0, Flat fields) | Eliminate t -> - DType (lid, flags, 0, Abbrev t) + DType (lid, flags, 0, 0, Abbrev t) | _ -> assert false end | _ -> - DType (lid, flags, n, def) + DType (lid, flags, 0, n, def) (* Need the type to be mapped *after* the expression, so that we can examine * the old type. Maybe this should be the default? *) @@ -656,14 +660,14 @@ let remove_unit_fields = object (self) | TAny -> EAny | t -> Warn.fatal_error "default_value: %a" ptyp t - method! visit_DType _ lid flags n type_def = + method! visit_DType _ lid flags n_cgs n type_def = match type_def with | Variant branches -> - DType (lid, flags, n, self#rewrite_variant lid branches) + DType (lid, flags, n_cgs, n, self#rewrite_variant lid branches) | Flat fields -> - DType (lid, flags, n, Flat (self#rewrite_fields lid None (fun x -> x) fields)) + DType (lid, flags, n_cgs, n, Flat (self#rewrite_fields lid None (fun x -> x) fields)) | _ -> - DType (lid, flags, n, type_def) + DType (lid, flags, n_cgs, n, type_def) (* Modify type definitions so that fields of type unit and any are removed. * Remember in a table that they are removed. *) @@ -1006,12 +1010,12 @@ let compile_all_matches (map, enums) = object (self) in TQualified tag_lid, TAnonymous (Union structs) - method! visit_DType _ lid flags n type_def = + method! visit_DType _ lid flags n_cgs n type_def = match type_def with | Variant branches -> - DType (lid, flags, n, self#rewrite_variant lid branches) + DType (lid, flags, n_cgs, n, self#rewrite_variant lid branches) | _ -> - DType (lid, flags, n, type_def) + DType (lid, flags, n_cgs, n, type_def) (* A variant declaration is a struct declaration with two fields: * - [field_for_tag] is the field that holds the "tag" whose type is an @@ -1073,11 +1077,11 @@ let compile_all_matches (map, enums) = object (self) ) (* The match transformation is tricky: we open all binders. *) - method! visit_DFunction env cc flags n ret name binders expr = + method! visit_DFunction env cc flags n_cgs n ret name binders expr = let binders, expr = open_binders binders expr in let expr = self#visit_expr_w env expr in let expr = close_binders binders expr in - DFunction (cc, flags, n, ret, name, binders, expr) + DFunction (cc, flags, n_cgs, n, ret, name, binders, expr) method! visit_ELet _ binder e1 e2 = let e1 = self#visit_expr_w () e1 in @@ -1131,10 +1135,10 @@ let anonymous_unions (map, _) = object (self) method! visit_decl env d = match d with - | DType (lid, flags, 0, Flat [ Some f1, t1; Some f2, t2 ]) when + | DType (lid, flags, 0, 0, Flat [ Some f1, t1; Some f2, t2 ]) when f1 = field_for_tag && f2 = field_for_union && is_tagged_union map lid -> - DType (lid, flags, 0, Flat [ Some f1, t1; None, t2 ]) + DType (lid, flags, 0, 0, Flat [ Some f1, t1; None, t2 ]) | _ -> super#visit_decl env d diff --git a/lib/DeBruijn.ml b/lib/DeBruijn.ml index ee38dbfc1..769af2d3f 100644 --- a/lib/DeBruijn.ml +++ b/lib/DeBruijn.ml @@ -243,3 +243,72 @@ let open_branch bs pat expr = in b :: bs, pat, expr ) bs ([], pat, expr) + +(* ---------------------------------------------------------------------------- *) + +(* Const generic support *) + +class map_counting_cg = object + (* The environment [i] has type [int*int]. *) + inherit [_] map + (* The environment is a pair [i, i']. The first component [i] is the DeBruijn + index we are looking for, after entering ONLY the cg binders. It it set by + the caller and does not increase afterwards since the only cg binders are at + the function declaration level. The second component [i'] is the DeBruijn + index we are looking for, after entering ALL the binders. It is incremented + at each binder, in expressions. *) + method! extend ((i: int), i') (_: binder) = + i, i' + 1 +end + +let cg_of_expr n_cg (_, i') e = + match e.node with + | EBound k -> + let level = i' - k - 1 in + assert (n_cg - level - 1 >= 0); + `Var (n_cg - level - 1) + | EConstant (w, s) -> + `Const (w, s) + | _ -> + failwith "Unsuitable const generic" + +(* Substitute const generics *) +class subst_c (n_cg: int) (c: expr) = object (self) + inherit map_counting_cg + method! visit_TCgArray ((i, _) as env) t j = + let t = self#visit_typ env t in + match cg_of_expr n_cg env c with + | `Var v' -> + (* we substitute v' for i in [ t; j ] *) + if j = i then + (* lift i c boils down to this since we never cross any binders *) + TCgArray (t, v' + i) + else + TCgArray (t, if j < i then j else j-1) + | `Const (w, s) -> + TArray (t, (w, s)) + + method! visit_EBound ((_, i), _) j = + if j = i then + (lift i c).node + else + EBound (if j < i then j else j-1) +end + +let subst_ce n_cg c = (new subst_c n_cg c)#visit_expr_w +let subst_ct n_cg c = (new subst_c n_cg c)#visit_typ + +(*let subst_cen n_cg cs e = + let l = List.length cs in + KList.fold_lefti (fun i body arg -> + let k = l - i - 1 in + subst_ce n_cg arg k body + ) e cs*) + +let subst_ctn n_cg cs t = + let l = List.length cs in + KList.fold_lefti (fun i body arg -> + let k = l - i - 1 in + subst_ct n_cg arg (k, k) body + ) t cs + diff --git a/lib/Diagnostics.ml b/lib/Diagnostics.ml index d08e4625b..6adb92b99 100644 --- a/lib/Diagnostics.ml +++ b/lib/Diagnostics.ml @@ -9,7 +9,7 @@ open PrintAst.Ops let types_depth files = let def_map = Helpers.build_map files (fun map d -> match d with - | DType (lid, _, _, d) -> Hashtbl.add map lid d + | DType (lid, _, _, _, d) -> Hashtbl.add map lid d | _ -> () ) in @@ -38,7 +38,7 @@ let types_depth files = and depth_of_type p t = match t with | TArrow _ - | TInt _ | TBool | TUnit | TAny | TBuf _ | TArray _ -> + | TInt _ | TBool | TUnit | TAny | TBuf _ | TArray _ | TCgArray _ -> 0, List.rev p | TQualified lid -> begin try @@ -58,7 +58,7 @@ let types_depth files = (object (_) inherit [_] iter - method! visit_DType _ lid _ _ def = + method! visit_DType _ lid _ _ _ def = compute_depth lid def end)#visit_files () files; diff --git a/lib/GcTypes.ml b/lib/GcTypes.ml index 136895c02..1defd4d88 100644 --- a/lib/GcTypes.ml +++ b/lib/GcTypes.ml @@ -12,7 +12,7 @@ module C = Common let mk_table files = Helpers.build_map files (fun map -> function - | DType (lid, flags, _, _) when List.mem C.GcType flags -> + | DType (lid, flags, _, _, _) when List.mem C.GcType flags -> Hashtbl.add map lid () | _ -> () diff --git a/lib/Helpers.ml b/lib/Helpers.ml index c08a5a3be..bf1e334e1 100644 --- a/lib/Helpers.ml +++ b/lib/Helpers.ml @@ -336,7 +336,7 @@ class ['self] readonly_visitor = object (self: 'self) List.for_all (self#visit_expr_w ()) es | EQualified lid when is_readonly_builtin_lid lid -> List.for_all (self#visit_expr_w ()) es - | ETApp ({ node = EQualified lid; _ }, _) when is_readonly_builtin_lid lid -> + | ETApp ({ node = EQualified lid; _ }, _, _) when is_readonly_builtin_lid lid -> List.for_all (self#visit_expr_w ()) es | _ -> false @@ -737,6 +737,7 @@ let push_ignore = nest_in_return_pos TUnit (fun _ e -> ETApp ( with_type (TArrow (TBound 0, TUnit)) (EQualified (["LowStar"; "Ignore"], "ignore")), + [], [ e.typ ] )), [ e ]))) diff --git a/lib/Inlining.ml b/lib/Inlining.ml index ca61d57c3..af22646d0 100644 --- a/lib/Inlining.ml +++ b/lib/Inlining.ml @@ -16,7 +16,7 @@ let natural_arity = Hashtbl.create 43 let compute_natural_arity = object inherit [_] iter - method! visit_DFunction () _ _ _ _ name args _ = + method! visit_DFunction () _ _ _ _ _ name args _ = Hashtbl.add natural_arity name (List.length args) end @@ -36,7 +36,7 @@ let reparenthesize_applications = object (self) let es = List.map (self#visit_expr env) es in let e = self#visit_expr env e in match e.node with - | EQualified lid | ETApp ({ node = EQualified lid; _ }, _) -> + | EQualified lid | ETApp ({ node = EQualified lid; _ }, _, _) -> begin try let n = Hashtbl.find natural_arity lid in let first, last = KList.split n es in @@ -105,7 +105,7 @@ let mk_inliner files criterion = (* Build a map suitable for the [memoize_inline] combinator. *) let map = Helpers.build_map files (fun map -> function | DGlobal (_, name, _, _, body) - | DFunction (_, _, _, _, name, _, body) -> + | DFunction (_, _, _, _, _, name, _, body) -> Hashtbl.add map name (White, body) | _ -> () @@ -138,7 +138,7 @@ let mk_inliner files criterion = let inline_analysis files = let map = Helpers.build_map files (fun map -> function | DGlobal (flags, name, _, _, body) - | DFunction (_, flags, _, _, name, _, body) -> + | DFunction (_, flags, _, _, _, name, _, body) -> Hashtbl.add map name (White, flags, 0, body) | _ -> () @@ -400,7 +400,7 @@ let cross_call_analysis files = end in begin match d with - | DFunction (_, _, _, t, _, bs, e) -> + | DFunction (_, _, _, _, t, _, bs, e) -> (visit false)#visit_typ () t; (visit false)#visit_binders_w () bs; (visit true)#visit_expr_w () e @@ -412,7 +412,7 @@ let cross_call_analysis files = (visit true)#visit_expr_w () e | DExternal (_, _, _, _, t, _) -> (visit false)#visit_typ () t - | DType (_, flags, _, d) -> + | DType (_, flags, _, _, d) -> if not (List.mem Common.AbstractStruct flags) then (visit false)#visit_type_def () d end; @@ -461,14 +461,14 @@ let cross_call_analysis files = flags in match d with - | DFunction (cc, flags, n, t, name, bs, e) -> - DFunction (cc, adjust flags, n, t, name, bs, e) + | DFunction (cc, flags, n_cgs, n, t, name, bs, e) -> + DFunction (cc, adjust flags, n_cgs, n, t, name, bs, e) | DGlobal (flags, name, n, t, e) -> DGlobal (adjust flags, name, n, t, e) | DExternal (cc, flags, n, name, t, hints) -> DExternal (cc, adjust flags, n, name, t, hints) - | DType (name, flags, n, def) -> - DType (name, adjust flags, n, def) + | DType (name, flags, n_cgs, n, def) -> + DType (name, adjust flags, n_cgs, n, def) ) decls ) files in @@ -491,7 +491,7 @@ let cross_call_analysis files = val mutable new_decls = [] method! visit_DGlobal () flags name n t body = if (Hashtbl.find info_map name).wasm_needs_getter then begin - let d = DFunction (None, [], 0, + let d = DFunction (None, [], 0, 0, t, name_of_getter name, [ Helpers.fresh_binder "_" TUnit ], @@ -531,13 +531,13 @@ let inline files = * dropped accordingly. * *) let files = filter_decls (function - | DFunction (cc, flags, n, ret, name, binders, _) -> + | DFunction (cc, flags, n_cgs, n, ret, name, binders, _) -> if must_disappear name && not (always_live name) then begin if Options.debug "reachability" then KPrint.bprintf "REACHABILITY: %a must disappear\n" plid name; None end else - Some (DFunction (cc, flags, n, ret, name, binders, inline_one name)) + Some (DFunction (cc, flags, n_cgs, n, ret, name, binders, inline_one name)) | DGlobal (flags, name, n, t, _) -> (* Note: should we allow globals to marked as "must disappear"? *) Some (DGlobal (flags, name, n, t, inline_one name)) @@ -550,7 +550,7 @@ let inline files = let inline_type_abbrevs ?(just_auto_generated=false) files = let map = Helpers.build_map files (fun map -> function - | DType (lid, flags, _, Abbrev t) when + | DType (lid, flags, _, _, Abbrev t) when not just_auto_generated || just_auto_generated && List.mem AutoGenerated flags -> Hashtbl.add map lid (White, t) | _ -> () @@ -580,7 +580,7 @@ let inline_type_abbrevs ?(just_auto_generated=false) files = if just_auto_generated then filter_decls (fun d -> match d with - | DType (_, flags, _, Abbrev _) when List.mem AutoGenerated flags -> + | DType (_, flags, _, _, Abbrev _) when List.mem AutoGenerated flags -> None | _ -> Some d @@ -660,9 +660,9 @@ let mark_possibly_unused ifdefs files = end)#visit_files () files in (object inherit [_] map - method! visit_DFunction _ cc flags n t name binders body = + method! visit_DFunction _ cc flags n_cgs n t name binders body = if not (LidSet.mem name map) && List.mem Private flags then - DFunction (cc, MaybeUnused :: flags, n, t, name, binders, body) + DFunction (cc, MaybeUnused :: flags, n_cgs, n, t, name, binders, body) else - DFunction (cc, flags, n, t, name, binders, body) + DFunction (cc, flags, n_cgs, n, t, name, binders, body) end)#visit_files () files diff --git a/lib/InputAstToAst.ml b/lib/InputAstToAst.ml index 2a7400d5b..9395902cd 100644 --- a/lib/InputAstToAst.ml +++ b/lib/InputAstToAst.ml @@ -40,24 +40,24 @@ let rec mk_decl = function else mk_expr body in - DFunction (cc, flags, n, mk_typ t, name, mk_binders binders, body) + DFunction (cc, flags, 0, n, mk_typ t, name, mk_binders binders, body) | I.DTypeAlias (name, flags, n, t) -> - DType (name, flags, n, Abbrev (mk_typ t)) + DType (name, flags, 0, n, Abbrev (mk_typ t)) | I.DGlobal (flags, name, n, t, e) -> DGlobal (flags, name, n, mk_typ t, mk_expr e) | I.DTypeFlat (name, flags, n, fields) -> - DType (name, flags, n, Flat (mk_tfields_opt fields)) + DType (name, flags, 0, n, Flat (mk_tfields_opt fields)) | I.DExternal (cc, flags, name, t) -> DExternal (cc, flags, 0, name, mk_typ t, []) | I.DExternal2 (cc, flags, name, t, arg_names) -> DExternal (cc, flags, 0, name, mk_typ t, arg_names) | I.DTypeVariant (name, flags, n, branches) -> - DType (name, flags, n, + DType (name, flags, 0, n, Variant (List.map (fun (ident, fields) -> ident, mk_tfields fields) branches)) | I.DTypeAbstractStruct name -> - DType (name, [], 0, Forward FStruct) + DType (name, [], 0, 0, Forward FStruct) | I.DUntaggedUnion (name, flags, n, branches) -> - DType (name, flags, n, Union (List.map (fun (f, t) -> f, mk_typ t) branches)) + DType (name, flags, 0, n, Union (List.map (fun (f, t) -> f, mk_typ t) branches)) and mk_binders bs = List.map mk_binder bs @@ -160,7 +160,7 @@ and mk_expr = function let c = match op with K.Eq -> K.PEq | K.Neq -> K.PNeq | _ -> assert false in mk (EPolyComp (c, mk_typ t)) | I.ETApp (e, es) -> - mk (ETApp (mk_expr e, List.map mk_typ es)) + mk (ETApp (mk_expr e, [], List.map mk_typ es)) | I.ELet (b, e1, e2) -> mk (ELet (mk_binder b, mk_expr e1, mk_expr e2)) | I.EIfThenElse (e1, e2, e3) -> diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index 27f2a6534..55fecf33d 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -14,7 +14,7 @@ module K = Constant (* A whole-program map from type lids to their definitions. *) let build_def_map files = build_map files (fun map -> function - | DType (lid, flags, _, def) -> + | DType (lid, flags, _, _, def) -> Hashtbl.add map lid (flags, def) | _ -> () @@ -165,7 +165,7 @@ let monomorphize_data_types map = object(self) let args = List.map (self#visit_typ under_ref) args in (* For tuples, we immediately know how to generate a definition. *) let fields = List.mapi (fun i arg -> Some (self#field_at i), (arg, false)) args in - self#record (DType (chosen_lid, [ Common.Private ] @ flag, 0, Flat fields)); + self#record (DType (chosen_lid, [ Common.Private ] @ flag, 0, 0, Flat fields)); Hashtbl.replace state n (Black, chosen_lid) end else begin (* This specific node has not been visited yet. *) @@ -198,19 +198,19 @@ let monomorphize_data_types map = object(self) if Options.debug "data-types-traversal" then KPrint.bprintf "DEFERRING %a<%a>\n" plid (fst n) ptyps (snd n); if match def with Union _ -> true | _ -> false then - self#record (DType (chosen_lid, flags, 0, Forward FUnion)) + self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion)) else - self#record (DType (chosen_lid, flags, 0, Forward FStruct)); + self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct)); Hashtbl.add pending_monomorphizations (fst n) (snd n); Hashtbl.remove state n | flags, Variant branches -> let branches = List.map (fun (cons, fields) -> cons, subst fields) branches in let branches = self#visit_branches_t under_ref branches in - self#record (DType (chosen_lid, flag @ flags, 0, Variant branches)); + self#record (DType (chosen_lid, flag @ flags, 0, 0, Variant branches)); Hashtbl.replace state n (Black, chosen_lid) | flags, Flat fields -> let fields = self#visit_fields_t_opt under_ref (subst fields) in - self#record (DType (chosen_lid, flag @ flags, 0, Flat fields)); + self#record (DType (chosen_lid, flag @ flags, 0, 0, Flat fields)); Hashtbl.replace state n (Black, chosen_lid) | flags, Union fields -> let fields = List.map (fun (f, t) -> @@ -218,12 +218,12 @@ let monomorphize_data_types map = object(self) let t = self#visit_typ under_ref t in f, t ) fields in - self#record (DType (chosen_lid, flag @ flags, 0, Union fields)); + self#record (DType (chosen_lid, flag @ flags, 0, 0, Union fields)); Hashtbl.replace state n (Black, chosen_lid) | flags, Abbrev t -> let t = DeBruijn.subst_tn args t in let t = self#visit_typ under_ref t in - self#record (DType (chosen_lid, flag @ flags, 0, Abbrev t)); + self#record (DType (chosen_lid, flag @ flags, 0, 0, Abbrev t)); Hashtbl.replace state n (Black, chosen_lid) | _ -> Hashtbl.replace state n (Black, chosen_lid) @@ -237,9 +237,9 @@ let monomorphize_data_types map = object(self) | exception Not_found -> () | flags, Union _ -> - self#record (DType (chosen_lid, flags, 0, Forward FUnion)) + self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion)) | flags, _ -> - self#record (DType (chosen_lid, flags, 0, Forward FStruct)) + self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct)) end; chosen_lid | Black, chosen_lid -> @@ -257,7 +257,7 @@ let monomorphize_data_types map = object(self) if Options.debug "data-types-traversal" then KPrint.bprintf "decl %a\n" plid (lid_of_decl d); match d with - | DType (lid, _, n, Abbrev (TTuple args)) when n = 0 && not (Hashtbl.mem state (tuple_lid, args)) -> + | DType (lid, _, 0, 0, Abbrev (TTuple args)) when not (Hashtbl.mem state (tuple_lid, args)) -> Hashtbl.remove map lid; if Options.debug "monomorphization" then KPrint.bprintf "%a abbreviation for %a\n" plid lid ptyp (TApp (tuple_lid, args)); @@ -266,7 +266,7 @@ let monomorphize_data_types map = object(self) Hashtbl.add seen_declarations lid (); self#clear () - | DType (lid, _, n, Abbrev (TApp (hd, args) as t)) when n = 0 && not (Hashtbl.mem state (hd, args)) -> + | DType (lid, _, 0, 0, Abbrev (TApp (hd, args) as t)) when not (Hashtbl.mem state (hd, args)) -> (* We have not yet monomorphized this type, and conveniently, we have a type abbreviation that provides us with a name hint! We simply ditch the type abbreviation and replace it with a monomorphization @@ -293,12 +293,12 @@ let monomorphize_data_types map = object(self) GcTypes) into `typedef foobar foobar_gc *`. And mitlsffi.ci will be happy. *) if abbrev_for_gc_type then - self#record (DType (lid, [], 0, Abbrev (TQualified (fst lid, snd lid ^ "_gc")))); + self#record (DType (lid, [], 0, 0, Abbrev (TQualified (fst lid, snd lid ^ "_gc")))); Hashtbl.add seen_declarations lid (); self#clear () - | DType (lid, _, n, _) when n > 0 -> + | DType (lid, _, n_cgs, n, _) when n > 0 || n_cgs > 0 -> (* The type itself cannot be monomorphized, but we may have seen in the past monomorphic instances of this type that we ought to generate. *) @@ -310,9 +310,9 @@ let monomorphize_data_types map = object(self) Hashtbl.add seen_declarations lid (); self#clear () - | DType (lid, _, n, (Flat _ | Variant _ | Abbrev _ | Union _)) -> + | DType (lid, _, n_cgs, n, (Flat _ | Variant _ | Abbrev _ | Union _)) -> (* Re-inserted by visit_node... don't insert twice. *) - assert (n = 0); + assert (n = 0 && n_cgs = 0); (* FIXME: the logic here is quite twisted... it should be simplified. My understanding is we want to BOTH visit the body of the type in case it recursively needs to trigger monomorphizations, and @@ -403,9 +403,9 @@ end * application (caught via the visitor) generates an instance. *) let functions files = let map = Helpers.build_map files (fun map -> function - | DFunction (cc, flags, n, t, name, b, body) -> - if n > 0 then - Hashtbl.add map name (`Function (cc, flags, n, t, name, b, body)) + | DFunction (cc, flags, n_cgs, n, t, name, b, body) -> + if n > 0 || n_cgs > 0 then + Hashtbl.add map name (`Function (cc, flags, n_cgs, n, t, name, b, body)) | DGlobal (flags, name, n, t, body) -> if n > 0 then Hashtbl.add map name (`Global (flags, name, n, t, body)) @@ -424,12 +424,12 @@ let functions files = let file_name, decls = file in current_file <- file_name; file_name, KList.map_flatten (function - | DFunction (cc, flags, n, ret, name, binders, body) -> + | DFunction (cc, flags, n_cgs, n, ret, name, binders, body) -> if Hashtbl.mem map name then [] else - let d = DFunction (cc, flags, n, ret, name, binders, self#visit_expr_w () body) in - assert (n = 0); + let d = DFunction (cc, flags, n_cgs, n, ret, name, binders, self#visit_expr_w () body) in + assert (n = 0 && n_cgs = 0); Gen.clear () @ [ d ] | DGlobal (flags, name, n, t, body) -> if Hashtbl.mem map name then @@ -442,7 +442,8 @@ let functions files = [ d ] ) decls - method! visit_ETApp env e ts = + method! visit_ETApp env e cgs ts = + assert (cgs = []); match e.node with | EQualified lid -> begin try @@ -453,14 +454,17 @@ let functions files = | exception Not_found -> (* External function. Bail. *) if !Options.allow_tapps || AstToCStar.whitelisted_tapp e then - super#visit_ETApp env e ts + super#visit_ETApp env e cgs ts else (self#visit_expr env e).node - | `Function (cc, flags, n, ret, name, binders, body) -> + | `Function (cc, flags, n_cgs, n, ret, name, binders, body) -> (* Need to generate a new instance. *) if n <> List.length ts then begin KPrint.bprintf "%a is not fully type-applied!\n" plid lid; (self#visit_expr env e).node + end else if n_cgs <> List.length cgs then begin + KPrint.bprintf "%a is not fully cg-applied!\n" plid lid; + (self#visit_expr env e).node end else (* The thunk allows registering the name before visiting the * body, for polymorphic recursive functions. *) @@ -472,7 +476,7 @@ let functions files = ) binders in let body = DeBruijn.subst_ten ts body in let body = self#visit_expr env body in - DFunction (cc, flags, 0, ret, name, binders, body) + DFunction (cc, flags, 0, 0, ret, name, binders, body) in EQualified (Gen.register_def current_file lid ts name def) @@ -511,7 +515,7 @@ let equalities files = let types_map = Helpers.build_map files (fun map d -> match d with - | DType (lid, _, _, d) -> Hashtbl.add map lid d + | DType (lid, _, _, _, d) -> Hashtbl.add map lid d | _ -> () ) in @@ -544,7 +548,7 @@ let equalities files = let d = self#visit_decl env d in let equalities = Gen.clear () in let equalities = List.map (function - | DFunction (cc, flags, n, ret, name, binders, body) -> + | DFunction (cc, flags, n_cgs, n, ret, name, binders, body) -> (* This is a highly conservative criterion that is triggered by * any recursive type; we could be smarter and only break the * cycles by marking ONE declaration public. *) @@ -554,7 +558,7 @@ let equalities files = else flags in - DFunction (cc, flags, n, ret, name, binders, body) + DFunction (cc, flags, n_cgs, n, ret, name, binders, body) | d -> d ) equalities in @@ -600,7 +604,7 @@ let equalities files = EApp (with_type eq_typ' (self#generate_equality t K.PEq), [ with_type t' (EBound 0); with_type t' (EBound 1) ]))) in - DFunction (None, [ Common.Private ], 0, TBool, instance_lid, [ y; x ], body) + DFunction (None, [ Common.Private ], 0, 0, TBool, instance_lid, [ y; x ], body) in EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid def) | K.PEq -> @@ -684,7 +688,7 @@ let equalities files = (EField (with_type t (EBound 0), f)) (EField (with_type t (EBound 1), f)) ) fields in - DFunction (None, [ Common.Private ], 0, TBool, instance_lid, [ y; x ], + DFunction (None, [ Common.Private ], 0, 0, TBool, instance_lid, [ y; x ], mk_conj_or_disj sub_equalities) in EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid def) @@ -695,7 +699,7 @@ let equalities files = | K.PNeq -> etrue in (* let __eq__typ y x = *) - DFunction (None, [ Common.Private ], 0, TBool, instance_lid, [ y; x ], + DFunction (None, [ Common.Private ], 0, 0, TBool, instance_lid, [ y; x ], (* match *) with_type TBool (EMatch (Checked, (* x with *) @@ -768,7 +772,7 @@ let equalities files = let x = fresh_binder "x" t in let y = fresh_binder "y" t in EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid (fun _ -> - DFunction (None, [ Common.Private ], 0, TBool, instance_lid, [ y; x ], + DFunction (None, [ Common.Private ], 0, 0, TBool, instance_lid, [ y; x ], with_type TBool ( EApp (with_type eq_typ (EPolyComp (c, t)), [ with_type t (EBound 0); with_type t (EBound 1) ]))))) diff --git a/lib/Output.ml b/lib/Output.ml index b5a136162..e7d0d02dd 100644 --- a/lib/Output.ml +++ b/lib/Output.ml @@ -222,7 +222,7 @@ let write_def m c_files = (Filename.basename (Filename.chop_extension !Options.exe_name)); List.iter (fun (_, decls) -> List.iter (function - | Ast.DFunction (_, flags, _, _, name, _, _) + | Ast.DFunction (_, flags, _, _, _, name, _, _) when not (List.mem Common.Private flags) -> let name = GlobalNames.to_c_name m name in KPrint.bfprintf oc " %s\n" name diff --git a/lib/PrintAst.ml b/lib/PrintAst.ml index 5d0117c7c..27a77b1b2 100644 --- a/lib/PrintAst.ml +++ b/lib/PrintAst.ml @@ -24,10 +24,11 @@ let print_app f head g arguments = ) let rec print_decl = function - | DFunction (cc, flags, n, typ, name, binders, body) -> + | DFunction (cc, flags, n_cg, n, typ, name, binders, body) -> let cc = match cc with Some cc -> print_cc cc ^^ break1 | None -> empty in print_comment flags ^^ cc ^^ print_flags flags ^^ group (string "function" ^/^ string (string_of_lident name) ^/^ + langle ^^ string "cg: " ^^ int n_cg ^^ rangle ^^ langle ^^ int n ^^ rangle ^^ parens_with_nesting ( separate_map (comma ^^ break 1) print_binder binders @@ -46,10 +47,11 @@ let rec print_decl = function print_comment flags ^^ print_flags flags ^^ langle ^^ int n ^^ rangle ^^ print_typ typ ^^ space ^^ string (string_of_lident name) ^^ space ^^ equals ^/^ nest 2 (print_expr expr) - | DType (name, flags, n, def) -> + | DType (name, flags, n_cg, n, def) -> let args = KList.make n (fun i -> string ("t" ^ string_of_int i)) in let args = separate space args in group (string "type" ^/^ print_flags flags ^/^ string (string_of_lident name) ^/^ args ^/^ equals) ^^ + langle ^^ string "cg: " ^^ int n_cg ^^ rangle ^^ jump (print_type_def def) and print_comment flags = @@ -170,6 +172,7 @@ and print_typ = function | TInt w -> print_width w | TBuf (t, bool) -> (if bool then string "const" else empty) ^/^ print_typ t ^^ star | TArray (t, k) -> print_typ t ^^ lbracket ^^ print_constant k ^^ rbracket + | TCgArray (t, v) -> print_typ t ^^ lbracket ^^ int v ^^ rbracket | TUnit -> string "()" | TQualified name -> string (string_of_lident name) | TBool -> string "bool" @@ -221,8 +224,10 @@ and print_expr { node; typ } = dquote ^^ string s ^^ dquote | EApp (e, es) -> print_app print_expr e print_expr es - | ETApp (e, ts) -> - print_app print_expr e (fun t -> group (langle ^/^ print_typ t ^/^ rangle)) ts + | ETApp (e, es, ts) -> + print_app (fun (e, ts) -> + print_app print_expr e (fun t -> group (langle ^/^ print_typ t ^/^ rangle)) ts + ) (e, ts) print_expr es | ELet (binder, e1, e2) -> group (print_let_binding (binder, e1) ^/^ string "in") ^^ hardline ^^ group (print_expr e2) diff --git a/lib/Simplify.ml b/lib/Simplify.ml index f6b0ba7bf..ebd512f73 100644 --- a/lib/Simplify.ml +++ b/lib/Simplify.ml @@ -76,7 +76,7 @@ class ['self] safe_use = object (self: 'self) match e.node with | EOp _ -> super#visit_EApp env e es | EQualified lid when Helpers.is_readonly_builtin_lid lid -> super#visit_EApp env e es - | ETApp ({ node = EQualified lid; _ }, _) when Helpers.is_readonly_builtin_lid lid -> super#visit_EApp env e es + | ETApp ({ node = EQualified lid; _ }, _, _) when Helpers.is_readonly_builtin_lid lid -> super#visit_EApp env e es | _ -> self#unordered env (e :: es) method! visit_ELet env _ e1 e2 = self#sequential env e1 (Some e2) @@ -160,7 +160,7 @@ let unused_parameter_table = object (_) inherit [_] iter - method! visit_DFunction parameter_table _ flags _ _ name binders _ = + method! visit_DFunction parameter_table _ flags _ _ _ name binders _ = let is_private = List.mem Common.Private flags && not (Helpers.is_static_header name) in if is_private then let unused_vector = List.map (fun b -> !(b.node.mark)) binders in @@ -224,7 +224,7 @@ let remove_unused_parameters = object (self) method! extend (table, j) _ = table, j + 1 - method! visit_DFunction (parameter_table, _) cc flags n ret name binders body = + method! visit_DFunction (parameter_table, _) cc flags n_cgs n ret name binders body = current_lid <- name; (* Visit first: this may create more unused parameters and modify @@ -245,7 +245,7 @@ let remove_unused_parameters = object (self) body ) body (KList.make n_binders (fun i -> i)) in let binders = KList.filter_mapi (fun i b -> if unused i then None else Some b) binders in - DFunction (cc, flags, n, ret, name, binders, body) + DFunction (cc, flags, n_cgs, n, ret, name, binders, body) method! visit_DExternal (parameter_table, _ as env) cc flags n name t hints = let ret, args = flatten_arrow t in @@ -398,7 +398,7 @@ let remove_ignore_unit = object method! visit_EApp env hd args = match hd.node, args with - | ETApp ({ node = EQualified (["LowStar"; "Ignore"], "ignore"); _}, [ TUnit ]), [ { node = EUnit; _ } ] -> + | ETApp ({ node = EQualified (["LowStar"; "Ignore"], "ignore"); _}, _, [ TUnit ]), [ { node = EUnit; _ } ] -> EUnit | _ -> super#visit_EApp env hd args @@ -408,11 +408,11 @@ let remove_proj_is = object inherit [_] map - method! visit_DFunction _ cc flags n t name binders body = + method! visit_DFunction _ cc flags n_cgs n t name binders body = if KString.starts_with (snd name) "__proj__" || KString.starts_with (snd name) "__is__" then - DFunction (cc, Private :: flags, n, t, name, binders, body) + DFunction (cc, Private :: flags, n_cgs, n, t, name, binders, body) else - DFunction (cc, flags, n, t, name, binders, body) + DFunction (cc, flags, n_cgs, n, t, name, binders, body) end @@ -586,7 +586,7 @@ let functional_updates = object (self) (* The same object is called a second time with the mark_mut flag set to true * to mark those fields that now ought to be mutable *) - method! visit_DType mark_mut name flags n def = + method! visit_DType mark_mut name flags n_cgs n def = match def with | Flat fields when mark_mut -> let fields = List.map (fun (f, (t, m)) -> @@ -595,9 +595,9 @@ let functional_updates = object (self) else f, (t, m) ) fields in - DType (name, flags, n, Flat fields) + DType (name, flags, n_cgs, n, Flat fields) | _ -> - DType (name, flags, n, def) + DType (name, flags, n_cgs, n, def) end let mutated_types = Hashtbl.create 41 @@ -844,12 +844,12 @@ end let misc_cosmetic2 = object inherit [_] map - method! visit_DType () name flags n def = + method! visit_DType () name flags n_cgs n def = match def with | Flat fields when Hashtbl.mem mutated_types name -> - DType (name, flags, n, Flat (List.map (fun (f, (t, _)) -> f, (t, true)) fields)) + DType (name, flags, n_cgs, n, Flat (List.map (fun (f, (t, _)) -> f, (t, true)) fields)) | _ -> - DType (name, flags, n, def) + DType (name, flags, n_cgs, n, def) end (* No left-nested let-bindings ************************************************) @@ -1013,9 +1013,10 @@ and hoist_stmt loc e = and hoist_expr loc pos e = let mk node = { node; typ = e.typ } in match e.node with - | ETApp (e, ts) -> + | ETApp (e, cgs, ts) -> + assert (cgs = []); let lhs, e = hoist_expr loc Unspecified e in - lhs, mk (ETApp (e, ts)) + lhs, mk (ETApp (e, [], ts)) | EBufNull | EAbort _ @@ -1269,13 +1270,13 @@ let hoist = object method! visit_file loc file = super#visit_file Loc.(File (fst file) :: loc) file - method! visit_DFunction loc cc flags n ret name binders expr = + method! visit_DFunction loc cc flags n_cgs n ret name binders expr = let loc = Loc.(InTop name :: loc) in (* TODO: no nested let-bindings in top-level value declarations either *) let binders, expr = open_binders binders expr in let expr = hoist_stmt loc expr in let expr = close_binders binders expr in - DFunction (cc, flags, n, ret, name, binders, expr) + DFunction (cc, flags, n_cgs, n, ret, name, binders, expr) end @@ -1313,8 +1314,8 @@ let rec fixup_return_pos e = let fixup_hoist = object inherit [_] map - method visit_DFunction _ cc flags n ret name binders expr = - DFunction (cc, flags, n, ret, name, binders, fixup_return_pos expr) + method visit_DFunction _ cc flags n_cgs n ret name binders expr = + DFunction (cc, flags, n_cgs, n, ret, name, binders, fixup_return_pos expr) end @@ -1366,7 +1367,7 @@ let record_toplevel_names = object (self) method! visit_DGlobal env flags name _ _ _ = self#record env ~is_type:false ~is_external:false flags name - method! visit_DFunction env _ flags _ _ name _ _ = + method! visit_DFunction env _ flags _ _ _ name _ _ = self#record env ~is_type:false ~is_external:false flags name method! visit_DExternal env _ flags _ name _ _ = @@ -1374,7 +1375,7 @@ let record_toplevel_names = object (self) val forward = Hashtbl.create 41 - method! visit_DType env name flags _ def = + method! visit_DType env name flags _ _ def = if not (Hashtbl.mem forward name) then self#record env ~is_type:true ~is_external:false flags name; match def with @@ -1479,7 +1480,7 @@ let tail_calls = let tail_calls = object (_) inherit [_] map - method! visit_DFunction () cc flags n ret name binders body = + method! visit_DFunction () cc flags n_cgs n ret name binders body = try let x_args = List.map (fun b -> Helpers.fresh_binder ~mut:true b.node.name b.typ) binders in let x_args, body = DeBruijn.open_binders x_args body in @@ -1495,13 +1496,13 @@ let tail_calls = with_type ret (EAbort (None, Some "unreachable, returns inserted above")) ])) in - DFunction (cc, flags, n, ret, name, binders, body) + DFunction (cc, flags, n_cgs, n, ret, name, binders, body) with | T.NotTailCall -> Warn.(maybe_fatal_error ("", NotTailCall name)); - DFunction (cc, flags, n, ret, name, binders, body) + DFunction (cc, flags, n_cgs, n, ret, name, binders, body) | T.NothingToTailCall -> - DFunction (cc, flags, n, ret, name, binders, body) + DFunction (cc, flags, n_cgs, n, ret, name, binders, body) end in tail_calls#visit_files () @@ -1679,9 +1680,9 @@ let rec find_pushframe ifdefs (e: expr) = let hoist_bufcreate = object inherit [_] map - method visit_DFunction ifdefs cc flags n ret name binders expr = + method visit_DFunction ifdefs cc flags n_cgs n ret name binders expr = try - DFunction (cc, flags, n, ret, name, binders, find_pushframe ifdefs expr) + DFunction (cc, flags, n_cgs, n, ret, name, binders, find_pushframe ifdefs expr) with Fatal s -> KPrint.bprintf "Fatal error in %a:\n%s\n" plid name s; exit 151 diff --git a/lib/SimplifyC89.ml b/lib/SimplifyC89.ml index f6fc4487a..f38f7060d 100644 --- a/lib/SimplifyC89.ml +++ b/lib/SimplifyC89.ml @@ -30,9 +30,9 @@ let hoist_lets = object (self) ) !env in nest bs t e - method! visit_DFunction _ cc flags n ret name binders body = + method! visit_DFunction _ cc flags n_cg n ret name binders body = let body = self#scope_start ret body in - DFunction (cc, flags, n, ret, name, binders, body) + DFunction (cc, flags, n_cg, n, ret, name, binders, body) method! visit_EIfThenElse (_, t) e1 e2 e3 = (* No ELet's in e1 *) diff --git a/lib/SimplifyMerge.ml b/lib/SimplifyMerge.ml index 3b49d8292..19325deae 100644 --- a/lib/SimplifyMerge.ml +++ b/lib/SimplifyMerge.ml @@ -329,13 +329,13 @@ and merge_list env d u es = let merge_visitor = object(_) inherit [_] map - method! visit_DFunction () cc flags n ret name binders body = + method! visit_DFunction () cc flags n_cgs n ret name binders body = if debug then KPrint.bprintf "Variable merge: visiting %a\n%a\n" plid name ppexpr body; let binders, body = open_binders binders body in let _, _, body = merge [] S.empty body in let body = close_binders binders body in - DFunction (cc, flags, n, ret, name, binders, body) + DFunction (cc, flags, n_cgs, n, ret, name, binders, body) end (* Debug any intermediary AST as follows: *) diff --git a/lib/SimplifyWasm.ml b/lib/SimplifyWasm.ml index 3d0d43886..5310420c9 100644 --- a/lib/SimplifyWasm.ml +++ b/lib/SimplifyWasm.ml @@ -175,7 +175,7 @@ let eta_expand = object { node = EBound (n - i - 1); typ = t } ) targs) in let body = { node = EApp (body, args); typ = tret } in - DFunction (None, flags, 0, tret, name, binders, body) + DFunction (None, flags, 0, 0, tret, name, binders, body) | _ -> DGlobal (flags, name, n, t, body) end diff --git a/lib/Structs.ml b/lib/Structs.ml index 4b0936ffa..611cb512c 100644 --- a/lib/Structs.ml +++ b/lib/Structs.ml @@ -24,7 +24,7 @@ let mk_is_struct files = let map = Hashtbl.create 41 in List.iter (fun (_, decls) -> List.iter (function - | DType (lid, _, _, Flat _) -> + | DType (lid, _, _, _, Flat _) -> Hashtbl.add map lid true | _ -> () @@ -182,7 +182,7 @@ let pass_by_ref (should_rewrite: _ -> policy) = object (self) else Helpers.nest bs t (with_type t (EApp (e, args))) - method! visit_DFunction _ cc flags n ret lid binders body = + method! visit_DFunction _ cc flags n_cg n ret lid binders body = (* Step 0: parameters at function types get transformed, too. This has no * incidence on the result of is_struct. *) let binders = self#visit_binders_w [] binders in @@ -258,7 +258,7 @@ let pass_by_ref (should_rewrite: _ -> policy) = object (self) body in let body = DeBruijn.close_binders binders body in - DFunction (cc, flags, n, ret, lid, binders, body) + DFunction (cc, flags, n_cg, n, ret, lid, binders, body) method! visit_TArrow _ t1 t2 = let t = TArrow (t1, t2) in @@ -417,9 +417,9 @@ let pass_by_ref files = in let def_map = Helpers.build_map files (fun map d -> match d with - | DType (lid, _, _, (Flat fs)) -> + | DType (lid, _, _, _, (Flat fs)) -> Hashtbl.add map lid (List.map (fun (_, (t, _)) -> t) fs) - | DType (lid, _, _, (Union fs)) -> + | DType (lid, _, _, _, (Union fs)) -> Hashtbl.add map lid (List.map snd fs) | _ -> () @@ -489,14 +489,14 @@ let collect_initializers (files: Ast.file list) = end)#visit_files () files in if !initializers != [] then let file = "krmlinit", - [ DFunction (None, [ Common.Prologue hidden_visibility ], 0, TUnit, (["krmlinit"], "globals"), + [ DFunction (None, [ Common.Prologue hidden_visibility ], 0, 0, TUnit, (["krmlinit"], "globals"), [Helpers.fresh_binder "_" TUnit], with_type TUnit (ESequence (List.rev !initializers)))] in let files = files @ [ file ] in let found = ref false in let files = (object inherit [_] map - method! visit_DFunction _ cc flags n ret name binders body = + method! visit_DFunction _ cc flags n_cgs n ret name binders body = let body = if fst (GlobalNames.target_c_name ~attempt_shortening:false name) = "main" then begin found := true; @@ -509,7 +509,7 @@ let collect_initializers (files: Ast.file list) = end else body in - DFunction (cc, flags, n, ret, name, binders, body) + DFunction (cc, flags, n_cgs, n, ret, name, binders, body) end)#visit_files () files in if not !found then Warn.(maybe_fatal_error ("", MustCallKrmlInit)); @@ -579,9 +579,10 @@ let to_addr is_struct = not_struct (); w (EIgnore (to_addr false e)) - | ETApp (e, ts) -> + | ETApp (e, cgs, ts) -> + assert (cgs = []); not_struct (); - w (ETApp (to_addr false e, ts)) + w (ETApp (to_addr false e, [], ts)) | EApp (e, es) -> not_struct (); @@ -731,8 +732,8 @@ let to_addr is_struct = object inherit [_] map - method! visit_DFunction _ cc flags n ret lid binders body = - DFunction (cc, flags, n, ret, lid, binders, to_addr false body) + method! visit_DFunction _ cc flags n_cgs n ret lid binders body = + DFunction (cc, flags, n_cgs, n, ret, lid, binders, to_addr false body) end diff --git a/lib/UseAnalysis.ml b/lib/UseAnalysis.ml index 0d602171e..11d72c421 100644 --- a/lib/UseAnalysis.ml +++ b/lib/UseAnalysis.ml @@ -136,8 +136,8 @@ let build_usage_map_and_mark ifdefs = object(self) else self#plus map (self#visit_expr env e1) - method! visit_DFunction env cc flags n ret name binders body = - let map = super#visit_DFunction env cc flags n ret name binders body in + method! visit_DFunction env cc flags n_cgs n ret name binders body = + let map = super#visit_DFunction env cc flags n_cgs n ret name binders body in List.iteri (fun i b -> let v = match IntMap.find_opt i map with None -> zero | Some v -> v in b.node.mark := v @@ -217,13 +217,13 @@ let use_mark_to_remove_or_ignore final = object (self) (* Nothing to do *) self#remove_trivial_let (ELet (b, e1, e2)) - method! visit_DFunction env cc flags n ret name binders body = + method! visit_DFunction env cc flags n_cgs n ret name binders body = if not final then (* This is not the final phase, so we're still waiting for the removal of unused function parameters in private (non-externally visible) functions. This is done in a dedicated phase called `remove_unused` that relies on `unused_parameter_table`. *) - super#visit_DFunction env cc flags n ret name binders body + super#visit_DFunction env cc flags n_cgs n ret name binders body else let env = List.fold_left self#extend env binders in let body = self#visit_expr_w env body in @@ -246,7 +246,7 @@ let use_mark_to_remove_or_ignore final = object (self) with_type body.typ (ELet (b, i, DeBruijn.lift 1 body)) ) ignores body in - DFunction (cc, flags, n, ret, name, binders, body) + DFunction (cc, flags, n_cgs, n, ret, name, binders, body) end From 6156d7de783024149e867891ae69370665c11826 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 6 Dec 2023 20:23:19 -0800 Subject: [PATCH 02/21] Redo substitutions and binder representation for safer usage --- lib/Ast.ml | 6 +++--- lib/AstToCFlat.ml | 2 +- lib/AstToCStar.ml | 10 ++++------ lib/AstToMiniRust.ml | 2 +- lib/Builtin.ml | 11 ++++++----- lib/Bundles.ml | 4 ++-- lib/Checker.ml | 40 ++++++++++++++++++++++++++-------------- lib/DeBruijn.ml | 38 ++++++++++++++++++++++---------------- lib/Inlining.ml | 6 +++--- lib/InputAstToAst.ml | 4 ++-- lib/Monomorphization.ml | 16 +++++++++++++--- lib/PrintAst.ml | 14 +++++++++----- lib/Simplify.ml | 9 ++++----- 13 files changed, 96 insertions(+), 66 deletions(-) diff --git a/lib/Ast.ml b/lib/Ast.ml index 6cfe1add4..ed8bf3634 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -420,7 +420,7 @@ and files = and decl = | DFunction of calling_convention option * flag list * int * int * typ * lident * binders_w * expr_w | DGlobal of flag list * lident * int * typ * expr_w - | DExternal of calling_convention option * flag list * int * lident * typ * string list + | DExternal of calling_convention option * flag list * int * int * lident * typ * string list (** String list: only for pretty-printing purposes, names of the first few * known arguments. *) | DType of lident * flag list * int * int * type_def @@ -639,7 +639,7 @@ let with_type typ node = let lid_of_decl = function | DFunction (_, _, _, _, _, lid, _, _) | DGlobal (_, lid, _, _, _) - | DExternal (_, _, _, lid, _, _) + | DExternal (_, _, _, _, lid, _, _) | DType (lid, _, _, _, _) -> lid @@ -647,7 +647,7 @@ let flags_of_decl = function | DFunction (_, flags, _, _, _, _, _, _) | DGlobal (flags, _, _, _, _) | DType (_, flags, _, _, _) - | DExternal (_, flags, _, _, _, _) -> + | DExternal (_, flags, _, _, _, _, _) -> flags let tuple_lid = [ "K" ], "" diff --git a/lib/AstToCFlat.ml b/lib/AstToCFlat.ml index 8a70b0ec7..b45112cab 100644 --- a/lib/AstToCFlat.ml +++ b/lib/AstToCFlat.ml @@ -1078,7 +1078,7 @@ let mk_decl env (d: decl): env * CF.decl list = CF.Global (name, size, body, post_init, public) ] - | DExternal (_, _, _, lid, t, _) -> + | DExternal (_, _, _, _, lid, t, _) -> let name = GlobalNames.to_c_name env.names lid in match t with | TArrow _ -> diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml index 193e59f54..061fc5f2f 100644 --- a/lib/AstToCStar.ml +++ b/lib/AstToCStar.ml @@ -359,12 +359,10 @@ and mk_expr env in_stmt e = CStar.Constant c | EApp ({ node = ETApp (e, cgs, ts); _ }, es) when !Options.allow_tapps || whitelisted_tapp e -> - assert (cgs = []); - unit_to_void env e es (List.map (fun t -> CStar.Type (mk_type env t)) ts) + unit_to_void env e (cgs @ es) (List.map (fun t -> CStar.Type (mk_type env t)) ts) | ETApp (e, cgs, ts) when !Options.allow_tapps || whitelisted_tapp e -> - assert (cgs = []); - CStar.Call (mk_expr env e, List.map (fun t -> CStar.Type (mk_type env t)) ts) + unit_to_void env e cgs (List.map (fun t -> CStar.Type (mk_type env t)) ts) | EApp ({ node = EOp (op, w); _ }, [ _; _ ]) when is_arith op w -> fst (mk_arith env e) @@ -903,7 +901,7 @@ and mk_declaration m env d: (CStar.decl * _) option = mk_type env t, mk_expr env false body), []) - | DExternal (cc, flags, n, name, t, pp) -> + | DExternal (cc, flags, _, n, name, t, pp) -> if LidSet.mem name env.ifdefs || n > 0 then None else @@ -1006,7 +1004,7 @@ let mk_ifdefs_set files: LidSet.t = inherit [_] reduce as super method private zero = LidSet.empty method private plus = LidSet.union - method! visit_DExternal _env _cc (flags: flag list) _n (name: lident) _t _hints: LidSet.t = + method! visit_DExternal _env _cc (flags: flag list) _n_cg _n (name: lident) _t _hints: LidSet.t = if List.mem Common.IfDef flags then LidSet.singleton name else diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 88406d506..7ced9c77a 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -823,7 +823,7 @@ let translate_decl env (d: Ast.decl) = let env = push_global env lid (name, typ) in env, Some (MiniRust.Constant { name; typ; body; public }) - | Ast.DExternal (_, _, type_parameters, lid, t, _param_names) -> + | Ast.DExternal (_, _, _, type_parameters, lid, t, _param_names) -> let name = translate_unknown_lid lid in let env = push_global env lid (name, make_poly (translate_type env t) type_parameters) in env, None diff --git a/lib/Builtin.ml b/lib/Builtin.ml index 5fcd46266..613397a68 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -10,10 +10,10 @@ open Helpers let t_string = TQualified (["Prims"], "string") let mk_binop m n t = - DExternal (None, [ ], 0, (m, n), TArrow (t, TArrow (t, t)), [ "x"; "y" ]) + DExternal (None, [ ], 0, 0, (m, n), TArrow (t, TArrow (t, t)), [ "x"; "y" ]) let mk_val ?(flags=[]) ?(nvars=0) m n t = - DExternal (None, flags, nvars, (m, n), t, []) + DExternal (None, flags, 0, nvars, (m, n), t, []) let prims: file = let t = TInt K.CInt in @@ -351,15 +351,16 @@ let addendum = [ ] let make_abstract_function_or_global = function - | DFunction (cc, flags, _, n, t, name, bs, _) -> + | DFunction (cc, flags, n_cg, n, t, name, bs, _) -> let t = fold_arrow (List.map (fun b -> b.typ) bs) t in + assert (n_cg = 0); if n = 0 then - Some (DExternal (cc, flags, 0, name, t, List.map (fun x -> x.node.name) bs)) + Some (DExternal (cc, flags, 0, 0, name, t, List.map (fun x -> x.node.name) bs)) else None | DGlobal (flags, name, n, t, _) when not (List.mem Common.Macro flags) -> if n = 0 then - Some (DExternal (None, flags, 0, name, t, [])) + Some (DExternal (None, flags, 0, 0, name, t, [])) else None | DType (name, flags, _, _, _) when List.mem Common.AbstractStruct flags -> diff --git a/lib/Bundles.ml b/lib/Bundles.ml index f44c908aa..d3ad6adaf 100644 --- a/lib/Bundles.ml +++ b/lib/Bundles.ml @@ -54,8 +54,8 @@ let make_one_bundle (bundle: Bundle.t) (files: file list) (used: (int * Bundle.t DGlobal (add_if name flags, name, n, typ, body) | DType (lid, flags, n_cgs, n, def) -> DType (lid, add_if lid flags, n_cgs, n, def) - | DExternal (cc, flags, n, lid, t, pp) -> - DExternal (cc, add_if lid flags, n, lid, t, pp) + | DExternal (cc, flags, n_cg, n, lid, t, pp) -> + DExternal (cc, add_if lid flags, n_cg, n, lid, t, pp) in (* Match a file against the given list of patterns. *) diff --git a/lib/Checker.ml b/lib/Checker.ml index 7fb849e32..3d337fe5a 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -130,7 +130,7 @@ let populate_env files = Warn.fatal_error "%a is polymorphic\n" plid lid; let t = List.fold_right (fun b t2 -> TArrow (b.typ, t2)) binders ret in { env with globals = M.add lid t env.globals } - | DExternal (_, _, _, lid, typ, _) -> + | DExternal (_, _, _, _, lid, typ, _) -> { env with globals = M.add lid typ env.globals } ) env decls ) empty files @@ -523,17 +523,36 @@ and best_buffer_type l t1 e2 = and infer' env e = + let infer_app t es = + let t_ret, t_args = flatten_arrow t in + if List.length t_args = 0 then + checker_error env "This is not a function:\n%a" pexpr e; + if List.length es > List.length t_args then + checker_error env "Too many arguments for application:\n%a" pexpr e; + let t_args, t_remaining_args = KList.split (List.length es) t_args in + ignore (List.map2 (check_or_infer env) t_args es); + fold_arrow t_remaining_args t_ret + in + match e.node with - | ETApp (e, cs, ts) -> - begin match e.node with + | ETApp (e0, cs, ts) -> + begin match e0.node with | EOp ((K.Eq | K.Neq), _) -> (* Special incorrect encoding of polymorphic equalities *) let t = KList.one ts in TArrow (t, TArrow (t, TBool)) | _ -> - let t = infer env e in - let t = DeBruijn.subst_ctn env.n_cgs cs t in - DeBruijn.subst_tn ts t + let t = infer env e0 in + KPrint.bprintf "infer-cg: t=%a\n" ptyp t; + let diff = List.length env.locals - env.n_cgs in + let t = DeBruijn.subst_tn ts t in + KPrint.bprintf "infer-cg: subst_tn --> %a\n" ptyp t; + let t = DeBruijn.subst_ctn diff cs t in + KPrint.bprintf "infer-cg: subst_ctn --> %a\n" ptyp t; + (* Now type-check the application itself, after substitution *) + let t = infer_app t cs in + KPrint.bprintf "infer-cg: infer_app --> %a\n" ptyp t; + t end | EPolyComp (_, t) -> @@ -578,14 +597,7 @@ and infer' env e = let _ = List.map (infer env) es in TAny else - let t_ret, t_args = flatten_arrow t in - if List.length t_args = 0 then - checker_error env "This is not a function:\n%a" pexpr e; - if List.length es > List.length t_args then - checker_error env "Too many arguments for application:\n%a" pexpr e; - let t_args, t_remaining_args = KList.split (List.length es) t_args in - ignore (List.map2 (check_or_infer env) t_args es); - fold_arrow t_remaining_args t_ret + infer_app t es | ELet (binder, body, cont) -> let t = check_or_infer (locate env (In binder.node.name)) binder.typ body in diff --git a/lib/DeBruijn.ml b/lib/DeBruijn.ml index 769af2d3f..25512676a 100644 --- a/lib/DeBruijn.ml +++ b/lib/DeBruijn.ml @@ -261,28 +261,32 @@ class map_counting_cg = object i, i' + 1 end -let cg_of_expr n_cg (_, i') e = +(* Converting an expression into a suitable const generic usable in types, knowing + `diff = n_cg - n_binders`, where + - n_cg is the total number of const generics in the current function / type, + and + - n_binders is the total number of expression binders traversed (including + const generics) *) +let cg_of_expr diff e = match e.node with | EBound k -> - let level = i' - k - 1 in - assert (n_cg - level - 1 >= 0); - `Var (n_cg - level - 1) + assert (k - diff > 0); + `Var (k - diff) | EConstant (w, s) -> `Const (w, s) | _ -> failwith "Unsuitable const generic" (* Substitute const generics *) -class subst_c (n_cg: int) (c: expr) = object (self) +class subst_c (diff: int) (c: expr) = object (self) inherit map_counting_cg method! visit_TCgArray ((i, _) as env) t j = let t = self#visit_typ env t in - match cg_of_expr n_cg env c with + match cg_of_expr diff c with | `Var v' -> (* we substitute v' for i in [ t; j ] *) if j = i then - (* lift i c boils down to this since we never cross any binders *) - TCgArray (t, v' + i) + TCgArray (t, v' + i (* = lift_cg i v' *)) else TCgArray (t, if j < i then j else j-1) | `Const (w, s) -> @@ -295,20 +299,22 @@ class subst_c (n_cg: int) (c: expr) = object (self) EBound (if j < i then j else j-1) end -let subst_ce n_cg c = (new subst_c n_cg c)#visit_expr_w -let subst_ct n_cg c = (new subst_c n_cg c)#visit_typ +(* Both of these function receive a cg debruijn index, whereas the argument c is + an expression that is in the expression debruijn space -- hence the extra diff + parameter to go one the latter to the former. *) +let subst_ce diff c i = (new subst_c diff c)#visit_expr_w (i, i + diff) +let subst_ct diff c i = (new subst_c diff c)#visit_typ (i, i + diff) -(*let subst_cen n_cg cs e = +let subst_cen diff cs t = let l = List.length cs in KList.fold_lefti (fun i body arg -> let k = l - i - 1 in - subst_ce n_cg arg k body - ) e cs*) + subst_ce diff arg k body + ) t cs -let subst_ctn n_cg cs t = +let subst_ctn diff cs t = let l = List.length cs in KList.fold_lefti (fun i body arg -> let k = l - i - 1 in - subst_ct n_cg arg (k, k) body + subst_ct diff arg k body ) t cs - diff --git a/lib/Inlining.ml b/lib/Inlining.ml index af22646d0..3e5684ce4 100644 --- a/lib/Inlining.ml +++ b/lib/Inlining.ml @@ -410,7 +410,7 @@ let cross_call_analysis files = limited, this is still useful e.g. in the presence of function pointers. *) (visit true)#visit_expr_w () e - | DExternal (_, _, _, _, t, _) -> + | DExternal (_, _, _, _, _, t, _) -> (visit false)#visit_typ () t | DType (_, flags, _, _, d) -> if not (List.mem Common.AbstractStruct flags) then @@ -465,8 +465,8 @@ let cross_call_analysis files = DFunction (cc, adjust flags, n_cgs, n, t, name, bs, e) | DGlobal (flags, name, n, t, e) -> DGlobal (adjust flags, name, n, t, e) - | DExternal (cc, flags, n, name, t, hints) -> - DExternal (cc, adjust flags, n, name, t, hints) + | DExternal (cc, flags, n_cg, n, name, t, hints) -> + DExternal (cc, adjust flags, n_cg, n, name, t, hints) | DType (name, flags, n_cgs, n, def) -> DType (name, adjust flags, n_cgs, n, def) ) decls diff --git a/lib/InputAstToAst.ml b/lib/InputAstToAst.ml index 9395902cd..d17fd1bb7 100644 --- a/lib/InputAstToAst.ml +++ b/lib/InputAstToAst.ml @@ -48,9 +48,9 @@ let rec mk_decl = function | I.DTypeFlat (name, flags, n, fields) -> DType (name, flags, 0, n, Flat (mk_tfields_opt fields)) | I.DExternal (cc, flags, name, t) -> - DExternal (cc, flags, 0, name, mk_typ t, []) + DExternal (cc, flags, 0, 0, name, mk_typ t, []) | I.DExternal2 (cc, flags, name, t, arg_names) -> - DExternal (cc, flags, 0, name, mk_typ t, arg_names) + DExternal (cc, flags, 0, 0, name, mk_typ t, arg_names) | I.DTypeVariant (name, flags, n, branches) -> DType (name, flags, 0, n, Variant (List.map (fun (ident, fields) -> ident, mk_tfields fields) branches)) diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index 55fecf33d..7592031fb 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -443,7 +443,14 @@ let functions files = ) decls method! visit_ETApp env e cgs ts = - assert (cgs = []); + let fail_if () = + if cgs <> [] then + Warn.fatal_error "TODO: e=%a\ncgs=%a\nts=%a\n%a\n" + pexpr e + pexprs cgs + ptyps ts + pexpr (with_type TUnit (ETApp (e, cgs, ts))); + in match e.node with | EQualified lid -> begin try @@ -452,12 +459,14 @@ let functions files = with Not_found -> match Hashtbl.find map lid with | exception Not_found -> - (* External function. Bail. *) + (* External function. Bail. Leave cgs -- treated as normal + arguments when going to C. C'est la vie. *) if !Options.allow_tapps || AstToCStar.whitelisted_tapp e then super#visit_ETApp env e cgs ts else (self#visit_expr env e).node | `Function (cc, flags, n_cgs, n, ret, name, binders, body) -> + fail_if (); (* Need to generate a new instance. *) if n <> List.length ts then begin KPrint.bprintf "%a is not fully type-applied!\n" plid lid; @@ -481,6 +490,7 @@ let functions files = EQualified (Gen.register_def current_file lid ts name def) | `Global (flags, name, n, t, body) -> + fail_if (); if n <> List.length ts then begin KPrint.bprintf "%a is not fully type-applied!\n" plid lid; (self#visit_expr env e).node @@ -609,7 +619,7 @@ let equalities files = EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid def) | K.PEq -> (* assume val __eq__t: t -> t -> bool *) - let def () = DExternal (None, [], 0, instance_lid, eq_typ', [ "x"; "y" ]) in + let def () = DExternal (None, [], 0, 0, instance_lid, eq_typ', [ "x"; "y" ]) in EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid def) in diff --git a/lib/PrintAst.ml b/lib/PrintAst.ml index 27a77b1b2..6d9a1b825 100644 --- a/lib/PrintAst.ml +++ b/lib/PrintAst.ml @@ -13,16 +13,19 @@ open Common let arrow = string "->" let lambda = fancystring "λ" 1 -let print_app f head g arguments = +let print_app_ empty f head g arguments = group ( f head ^^ jump ( if List.length arguments = 0 then - utf8string "😱" + utf8string empty else separate_map (break 1) g arguments ) ) +let print_app x = print_app_ "😱" x +let print_cg_app x = print_app_ "□" x + let rec print_decl = function | DFunction (cc, flags, n_cg, n, typ, name, binders, body) -> let cc = match cc with Some cc -> print_cc cc ^^ break1 | None -> empty in @@ -36,11 +39,12 @@ let rec print_decl = function print_expr body ) - | DExternal (cc, flags, n, name, typ, _) -> + | DExternal (cc, flags, n_cg, n, name, typ, _) -> let cc = match cc with Some cc -> print_cc cc ^^ break1 | None -> empty in print_flags flags ^/^ group (cc ^^ string "external" ^/^ string (string_of_lident name) ^/^ langle ^^ int n ^^ rangle ^^ colon) ^^ + langle ^^ string "cg: " ^^ int n_cg ^^ rangle ^^ jump (print_typ typ) | DGlobal (flags, name, n, typ, expr) -> @@ -225,9 +229,9 @@ and print_expr { node; typ } = | EApp (e, es) -> print_app print_expr e print_expr es | ETApp (e, es, ts) -> - print_app (fun (e, ts) -> + print_cg_app (fun (e, ts) -> print_app print_expr e (fun t -> group (langle ^/^ print_typ t ^/^ rangle)) ts - ) (e, ts) print_expr es + ) (e, ts) (fun e -> brackets (brackets (print_expr e))) es | ELet (binder, e1, e2) -> group (print_let_binding (binder, e1) ^/^ string "in") ^^ hardline ^^ group (print_expr e2) diff --git a/lib/Simplify.ml b/lib/Simplify.ml index ebd512f73..fff1f2ed7 100644 --- a/lib/Simplify.ml +++ b/lib/Simplify.ml @@ -247,7 +247,7 @@ let remove_unused_parameters = object (self) let binders = KList.filter_mapi (fun i b -> if unused i then None else Some b) binders in DFunction (cc, flags, n_cgs, n, ret, name, binders, body) - method! visit_DExternal (parameter_table, _ as env) cc flags n name t hints = + method! visit_DExternal (parameter_table, _ as env) cc flags n_cg n name t hints = let ret, args = flatten_arrow t in let hints = KList.filter_mapi (fun i arg -> if unused parameter_table dummy_lid args i then @@ -263,7 +263,7 @@ let remove_unused_parameters = object (self) ) args in let ret = self#visit_typ env ret in let t = fold_arrow args ret in - DExternal (cc, flags, n, name, t, hints) + DExternal (cc, flags, n_cg, n, name, t, hints) method! visit_TArrow (parameter_table, _ as env) t1 t2 = (* Important: the only entries in `parameter_table` are those which are @@ -1014,9 +1014,8 @@ and hoist_expr loc pos e = let mk node = { node; typ = e.typ } in match e.node with | ETApp (e, cgs, ts) -> - assert (cgs = []); let lhs, e = hoist_expr loc Unspecified e in - lhs, mk (ETApp (e, [], ts)) + lhs, mk (ETApp (e, cgs, ts)) | EBufNull | EAbort _ @@ -1370,7 +1369,7 @@ let record_toplevel_names = object (self) method! visit_DFunction env _ flags _ _ _ name _ _ = self#record env ~is_type:false ~is_external:false flags name - method! visit_DExternal env _ flags _ name _ _ = + method! visit_DExternal env _ flags _ _ name _ _ = self#record env ~is_type:false ~is_external:true flags name val forward = Hashtbl.create 41 From 5e9dbace33c21224267fb578c9487ffd1edc08cd Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 6 Dec 2023 21:54:44 -0800 Subject: [PATCH 03/21] Debug, tweak --- lib/Checker.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/lib/Checker.ml b/lib/Checker.ml index 3d337fe5a..104897afd 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -543,15 +543,19 @@ and infer' env e = TArrow (t, TArrow (t, TBool)) | _ -> let t = infer env e0 in - KPrint.bprintf "infer-cg: t=%a\n" ptyp t; + if Options.debug "checker-cg" then + KPrint.bprintf "infer-cg: t=%a\n" ptyp t; let diff = List.length env.locals - env.n_cgs in let t = DeBruijn.subst_tn ts t in - KPrint.bprintf "infer-cg: subst_tn --> %a\n" ptyp t; + if Options.debug "checker-cg" then + KPrint.bprintf "infer-cg: subst_tn --> %a\n" ptyp t; let t = DeBruijn.subst_ctn diff cs t in - KPrint.bprintf "infer-cg: subst_ctn --> %a\n" ptyp t; + if Options.debug "checker-cg" then + KPrint.bprintf "infer-cg: subst_ctn --> %a\n" ptyp t; (* Now type-check the application itself, after substitution *) let t = infer_app t cs in - KPrint.bprintf "infer-cg: infer_app --> %a\n" ptyp t; + if Options.debug "checker-cg" then + KPrint.bprintf "infer-cg: infer_app --> %a\n" ptyp t; t end @@ -1046,6 +1050,8 @@ and subtype env t1 t2 = true | TArray (t1, (_, l1)), TArray (t2, (_, l2)) when subtype env t1 t2 && l1 = l2 -> true + | TCgArray (t1, l1), TCgArray (t2, l2) when subtype env t1 t2 && l1 = l2 -> + true | TArray (t1, _), TBuf (t2, _) when subtype env t1 t2 -> true | TBuf (t1, b1), TBuf (t2, b2) when subtype env t1 t2 && (b1 <= b2) -> From cfc4b0dd260de6b0b3b9c0d4c4cdd9b07ff9ef26 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 6 Dec 2023 22:17:58 -0800 Subject: [PATCH 04/21] Enable substitutions for const generics when monomorphizing functions --- lib/Monomorphization.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index 7592031fb..43966f9b9 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -415,7 +415,7 @@ let functions files = let monomorphize = object(self) - inherit [_] map as super + inherit DeBruijn.map_counting as super (* Current file, for warning purposes. *) val mutable current_file = "" @@ -428,21 +428,21 @@ let functions files = if Hashtbl.mem map name then [] else - let d = DFunction (cc, flags, n_cgs, n, ret, name, binders, self#visit_expr_w () body) in + let d = DFunction (cc, flags, n_cgs, n, ret, name, binders, self#visit_expr_w 0 body) in assert (n = 0 && n_cgs = 0); Gen.clear () @ [ d ] | DGlobal (flags, name, n, t, body) -> if Hashtbl.mem map name then [] else - let d = DGlobal (flags, name, n, t, self#visit_expr_w () body) in + let d = DGlobal (flags, name, n, t, self#visit_expr_w 0 body) in assert (n = 0); Gen.clear () @ [ d ] | d -> [ d ] ) decls - method! visit_ETApp env e cgs ts = + method! visit_ETApp ((diff, _) as env) e cgs ts = let fail_if () = if cgs <> [] then Warn.fatal_error "TODO: e=%a\ncgs=%a\nts=%a\n%a\n" @@ -466,7 +466,6 @@ let functions files = else (self#visit_expr env e).node | `Function (cc, flags, n_cgs, n, ret, name, binders, body) -> - fail_if (); (* Need to generate a new instance. *) if n <> List.length ts then begin KPrint.bprintf "%a is not fully type-applied!\n" plid lid; @@ -479,11 +478,13 @@ let functions files = * body, for polymorphic recursive functions. *) let name = Gen.gen_lid name ts in let def () = - let ret = DeBruijn.subst_tn ts ret in + let ret = DeBruijn.(subst_ctn diff cgs (subst_tn ts ret)) in + assert (List.length cgs = n_cgs); + let _, binders = KList.split (List.length cgs) binders in let binders = List.map (fun { node; typ } -> - { node; typ = DeBruijn.subst_tn ts typ } + { node; typ = DeBruijn.(subst_ctn diff cgs (subst_tn ts typ)) } ) binders in - let body = DeBruijn.subst_ten ts body in + let body = DeBruijn.(subst_cen (List.length binders) cgs (subst_ten ts body)) in let body = self#visit_expr env body in DFunction (cc, flags, 0, 0, ret, name, binders, body) in @@ -518,7 +519,7 @@ let functions files = end in - monomorphize#visit_files () files + monomorphize#visit_files 0 files let equalities files = From 73de315b7c3d6414e1fa04fe5d7c32bbba1c755d Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 6 Dec 2023 22:47:05 -0800 Subject: [PATCH 05/21] More missing cases in the checker --- lib/Checker.ml | 13 +++++++++---- lib/DeBruijn.ml | 2 +- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/lib/Checker.ml b/lib/Checker.ml index 104897afd..bf8940f1e 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -200,10 +200,11 @@ and check_decl env d = if Options.debug "checker" then KPrint.bprintf "checking %a\n" plid (lid_of_decl d); match d with - | DFunction (_, _, _n_cgs, n, t, name, binders, body) -> + | DFunction (_, _, n_cgs, n, t, name, binders, body) -> assert (!Options.allow_tapps || n = 0); let env = List.fold_left push env binders in let env = locate env (InTop name) in + let env = { env with n_cgs } in check env t body | DGlobal (_, name, n, t, body) -> assert (n = 0); @@ -542,16 +543,16 @@ and infer' env e = let t = KList.one ts in TArrow (t, TArrow (t, TBool)) | _ -> + let diff = List.length env.locals - env.n_cgs in let t = infer env e0 in if Options.debug "checker-cg" then - KPrint.bprintf "infer-cg: t=%a\n" ptyp t; - let diff = List.length env.locals - env.n_cgs in + KPrint.bprintf "infer-cg: t=%a, cs=%a, ts=%a, diff=%d\n" ptyp t pexprs cs ptyps ts diff; let t = DeBruijn.subst_tn ts t in if Options.debug "checker-cg" then KPrint.bprintf "infer-cg: subst_tn --> %a\n" ptyp t; let t = DeBruijn.subst_ctn diff cs t in if Options.debug "checker-cg" then - KPrint.bprintf "infer-cg: subst_ctn --> %a\n" ptyp t; + KPrint.bprintf "infer-cg: subst_ctn (diff=%d)--> %a\n" diff ptyp t; (* Now type-check the application itself, after substitution *) let t = infer_app t cs in if Options.debug "checker-cg" then @@ -1017,6 +1018,8 @@ and assert_buffer env t = t1, b | TArray (t1, _) -> t1, false + | TCgArray (t1, _) -> + t1, false | t -> checker_error env "This is not a buffer: %a" ptyp t @@ -1052,6 +1055,8 @@ and subtype env t1 t2 = true | TCgArray (t1, l1), TCgArray (t2, l2) when subtype env t1 t2 && l1 = l2 -> true + | TCgArray (t1, _), TBuf (t2, _) when subtype env t1 t2 -> + true | TArray (t1, _), TBuf (t2, _) when subtype env t1 t2 -> true | TBuf (t1, b1), TBuf (t2, b2) when subtype env t1 t2 && (b1 <= b2) -> diff --git a/lib/DeBruijn.ml b/lib/DeBruijn.ml index 25512676a..ee4131f9f 100644 --- a/lib/DeBruijn.ml +++ b/lib/DeBruijn.ml @@ -270,7 +270,7 @@ end let cg_of_expr diff e = match e.node with | EBound k -> - assert (k - diff > 0); + assert (k - diff >= 0); `Var (k - diff) | EConstant (w, s) -> `Const (w, s) From d1948039924d99644b66ec934279b4357630c8fb Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 6 Dec 2023 23:10:10 -0800 Subject: [PATCH 06/21] Proper name caching based on constant vlaues --- lib/Monomorphization.ml | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index 43966f9b9..b3bd11757 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -375,16 +375,17 @@ module Gen = struct let generated_lids = Hashtbl.create 41 let pending_defs = ref [] - let gen_lid lid ts = + let gen_lid lid ts cgs = let doc = let open PPrint in let open PrintAst in - separate_map underscore print_typ ts + separate_map underscore print_typ ts ^^ underscore ^^ + separate_map underscore print_expr cgs in fst lid, snd lid ^ KPrint.bsprintf "__%a" PrintCommon.pdoc doc - let register_def current_file original_lid ts lid def = - Hashtbl.add generated_lids (original_lid, ts) lid; + let register_def current_file original_lid cgs ts lid def = + Hashtbl.add generated_lids (original_lid, cgs, ts) lid; let d = def () in if Drop.file current_file then Warn.(maybe_fatal_error ("", DropDeclaration (lid_of_decl d, current_file))); @@ -455,7 +456,7 @@ let functions files = | EQualified lid -> begin try (* Already monomorphized? *) - EQualified (Hashtbl.find Gen.generated_lids (lid, ts)) + EQualified (Hashtbl.find Gen.generated_lids (lid, cgs, ts)) with Not_found -> match Hashtbl.find map lid with | exception Not_found -> @@ -476,7 +477,7 @@ let functions files = end else (* The thunk allows registering the name before visiting the * body, for polymorphic recursive functions. *) - let name = Gen.gen_lid name ts in + let name = Gen.gen_lid name ts cgs in let def () = let ret = DeBruijn.(subst_ctn diff cgs (subst_tn ts ret)) in assert (List.length cgs = n_cgs); @@ -488,7 +489,7 @@ let functions files = let body = self#visit_expr env body in DFunction (cc, flags, 0, 0, ret, name, binders, body) in - EQualified (Gen.register_def current_file lid ts name def) + EQualified (Gen.register_def current_file lid cgs ts name def) | `Global (flags, name, n, t, body) -> fail_if (); @@ -496,14 +497,14 @@ let functions files = KPrint.bprintf "%a is not fully type-applied!\n" plid lid; (self#visit_expr env e).node end else - let name = Gen.gen_lid name ts in + let name = Gen.gen_lid name ts [] in let def () = let t = DeBruijn.subst_tn ts t in let body = DeBruijn.subst_ten ts body in let body = self#visit_expr env body in DGlobal (flags, name, 0, t, body) in - EQualified (Gen.register_def current_file lid ts name def) + EQualified (Gen.register_def current_file lid [] ts name def) end @@ -598,7 +599,7 @@ let equalities files = | K.PEq -> [], "__eq" | K.PNeq -> [], "__neq" in - let instance_lid = Gen.gen_lid eq_lid [ t ] in + let instance_lid = Gen.gen_lid eq_lid [ t ] [] in let x = fresh_binder "x" t in let y = fresh_binder "y" t in @@ -617,11 +618,11 @@ let equalities files = in DFunction (None, [ Common.Private ], 0, 0, TBool, instance_lid, [ y; x ], body) in - EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid def) + EQualified (Gen.register_def current_file eq_lid [] [ t ] instance_lid def) | K.PEq -> (* assume val __eq__t: t -> t -> bool *) let def () = DExternal (None, [], 0, 0, instance_lid, eq_typ', [ "x"; "y" ]) in - EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid def) + EQualified (Gen.register_def current_file eq_lid [] [ t ] instance_lid def) in @@ -647,7 +648,7 @@ let equalities files = | TQualified lid when Hashtbl.mem types_map lid -> begin try (* Already monomorphized? *) - let existing_lid = Hashtbl.find Gen.generated_lids (eq_lid, [ t ]) in + let existing_lid = Hashtbl.find Gen.generated_lids (eq_lid, [], [ t ]) in let is_cycle = List.exists (fun d -> lid_of_decl d = existing_lid) !Gen.pending_defs in if is_cycle then has_cycle <- true; @@ -702,7 +703,7 @@ let equalities files = DFunction (None, [ Common.Private ], 0, 0, TBool, instance_lid, [ y; x ], mk_conj_or_disj sub_equalities) in - EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid def) + EQualified (Gen.register_def current_file eq_lid [] [ t ] instance_lid def) | Variant branches -> let def () = let fail_case = match op with @@ -752,13 +753,13 @@ let equalities files = with_type t PWild, fail_case ]))) in - EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid def) + EQualified (Gen.register_def current_file eq_lid [] [ t ] instance_lid def) end | _ -> try (* Already monomorphized? *) - EQualified (Hashtbl.find Gen.generated_lids (eq_lid, [ t ])) + EQualified (Hashtbl.find Gen.generated_lids (eq_lid, [], [ t ])) with Not_found -> (* External type without a definition. Comparison of function types? *) gen_poly () @@ -775,14 +776,14 @@ let equalities files = in try (* Already monomorphized? *) - let existing_lid = Hashtbl.find Gen.generated_lids (eq_lid, [ t ]) in + let existing_lid = Hashtbl.find Gen.generated_lids (eq_lid, [], [ t ]) in EQualified existing_lid with Not_found -> let eq_typ = TArrow (t, TArrow (t, TBool)) in - let instance_lid = Gen.gen_lid eq_lid [ t ] in + let instance_lid = Gen.gen_lid eq_lid [ t ] [] in let x = fresh_binder "x" t in let y = fresh_binder "y" t in - EQualified (Gen.register_def current_file eq_lid [ t ] instance_lid (fun _ -> + EQualified (Gen.register_def current_file eq_lid [] [ t ] instance_lid (fun _ -> DFunction (None, [ Common.Private ], 0, 0, TBool, instance_lid, [ y; x ], with_type TBool ( EApp (with_type eq_typ (EPolyComp (c, t)), [ From c5d0b7de27cf40d8470b00a1bb677fa5d4520988 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 6 Dec 2023 23:27:43 -0800 Subject: [PATCH 07/21] Preserve previous names --- lib/Monomorphization.ml | 4 ++-- test/.hints/Rust1.fst.hints | 14 +++++++------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index b3bd11757..d5aa81f33 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -379,8 +379,8 @@ module Gen = struct let doc = let open PPrint in let open PrintAst in - separate_map underscore print_typ ts ^^ underscore ^^ - separate_map underscore print_expr cgs + separate_map underscore print_typ ts ^^ + (if cgs = [] then empty else underscore ^^ separate_map underscore print_expr cgs) in fst lid, snd lid ^ KPrint.bsprintf "__%a" PrintCommon.pdoc doc diff --git a/test/.hints/Rust1.fst.hints b/test/.hints/Rust1.fst.hints index 9fcb1a1f7..d8f31467f 100644 --- a/test/.hints/Rust1.fst.hints +++ b/test/.hints/Rust1.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "5bb324f2cfa11752ab6a4b007bdd2ac9" + "d8d782168aeb290839dc8db99793893b" ], [ "Rust1.two", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "19af3f16124ed6131ebd118a1645f272" + "b977b9a8e679010dd7db6093c2b24d8a" ], [ "Rust1.zero", @@ -62,7 +62,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d085467eb557cb757d2b85c57ebf2d84" + "f86c73e1af7e81dadb23c04c7c9f2a29" ], [ "Rust1.doesnt_work", @@ -150,7 +150,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "91f166bd89ddce81d6c4629fdda8bac7" + "d6ead5099b52df6e78f527a435081340" ], [ "Rust1.does_work", @@ -238,7 +238,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "fe0681b3f23222e6fe18d1c809712105" + "15b8216a10f04a5bca9b51bdab9afc07" ], [ "Rust1.fully_static", @@ -327,7 +327,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "28f783251277dfe18bc75dccb61fd8a4" + "fc56150d57736c34acb5641ad70c2f88" ], [ "Rust1.main", @@ -416,7 +416,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "68a280be773e96f4eb3f61ae14d6c637" + "7a928ff143175d99fb65b5f56469a5e5" ] ] ] \ No newline at end of file From d433aac85b1faf83cf0521f397d6d69002b36357 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Thu, 7 Dec 2023 16:02:03 -0800 Subject: [PATCH 08/21] Fixup a tidbit in the pass by ref phase --- lib/Structs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Structs.ml b/lib/Structs.ml index 611cb512c..ccfc30e34 100644 --- a/lib/Structs.ml +++ b/lib/Structs.ml @@ -106,7 +106,7 @@ let pass_by_ref (should_rewrite: _ -> policy) = object (self) ) args args_policies in let ret, args = if ret_policy <> Never then - TUnit, args @ [ TBuf (ret, false) ] + TUnit, args @ [ if Helpers.is_array ret then ret else TBuf (ret, false) ] else ret, args in From b704a34243bea347e369b42f8e203329adfc58c1 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Thu, 7 Dec 2023 18:10:12 -0800 Subject: [PATCH 09/21] cg data type monomorphization --- lib/Ast.ml | 26 ++++++++++- lib/AstToCStar.ml | 2 + lib/AstToMiniRust.ml | 1 + lib/Checker.ml | 65 +++++++++++++++------------- lib/DeBruijn.ml | 66 +++++++++++++++++++++++----- lib/Diagnostics.ml | 2 +- lib/Monomorphization.ml | 83 ++++++++++++++++++++++-------------- lib/MonomorphizationState.ml | 2 +- lib/PrintAst.ml | 5 +++ 9 files changed, 178 insertions(+), 74 deletions(-) diff --git a/lib/Ast.ml b/lib/Ast.ml index ed8bf3634..9d2a82b54 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -37,8 +37,12 @@ and valuation = Mark.occurrence * Mark.usage [@ opaque] let dummy_lid = [], "" +type cg = + | CgVar of int + | CgConst of constant + (* The visitor of types composes with the misc. visitor. *) -type typ = +and typ = | TInt of width | TBool | TUnit @@ -59,6 +63,8 @@ type typ = (** t1 -> t2 *) | TApp of lident * typ list (** disappears after monomorphization *) + | TCgApp of typ * cg + (** typ is either TCgApp, TApp, or TQualified *) | TBound of int (** appears in type definitions... also disappears after monorphization *) | TTuple of typ list @@ -636,6 +642,24 @@ let map_decls f files = let with_type typ node = { typ; node } +let flatten_tapp t = + let rec flatten_tapp cgs t = + match t with + | TApp (lid, ts) -> + lid, ts, List.rev cgs + | TCgApp (t, cg) -> + flatten_tapp (cg :: cgs) t + | TQualified lid -> + lid, [], List.rev cgs + | _ -> + invalid_arg "flatten_tapp" + in + flatten_tapp [] t + +let fold_tapp (lid, ts, cgs) = + let t = if ts = [] then TQualified lid else TApp (lid, ts) in + List.fold_right (fun cg t -> TCgApp (t, cg)) cgs t + let lid_of_decl = function | DFunction (_, _, _, _, _, lid, _, _) | DGlobal (_, lid, _, _, _) diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml index 061fc5f2f..aa87e6a60 100644 --- a/lib/AstToCStar.ml +++ b/lib/AstToCStar.ml @@ -804,6 +804,8 @@ and mk_return_type env = function mk_type_def env t | TCgArray _ -> fatal_error "Internal failure: TCgArray not desugared here" + | TCgApp _ -> + fatal_error "Internal failure: TCgApp not desugared here" and mk_type env = function diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 7ced9c77a..ccf771b9c 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -399,6 +399,7 @@ let rec translate_type (env: env) (t: Ast.typ): MiniRust.typ = | TTuple _ -> failwith "TODO: TTuple" | TAnonymous _ -> failwith "unexpected: we don't compile data types going to Rust" | TCgArray _ -> failwith "Impossible: TCgArray" + | TCgApp _ -> failwith "Impossible: TCgApp" (* Expressions *) diff --git a/lib/Checker.ml b/lib/Checker.ml index bf8940f1e..922442515 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -428,31 +428,34 @@ and check' env t e = * typing comes into play. Indeed, a flat record is typed nominally (if * the context demands it) or structurally (default). TODO just type * structurally, and let the subtyping relation do the rest? *) - begin match expand_abbrev env t with - | TQualified lid when kind env lid = Some Record -> - let fieldtyps = assert_flat env (lookup_type env lid) in - check_fields_opt env fieldexprs fieldtyps - | TQualified lid when kind env lid = Some Union -> - let fieldtyps = assert_union env (lookup_type env lid) in - check_union env fieldexprs fieldtyps - | TApp (lid, ts) when kind env lid = Some Record -> + let t = expand_abbrev env t in + begin match flatten_tapp t with + | exception Invalid_argument _ -> + begin match t with + | TAnonymous (Flat fieldtyps) -> + check_fields_opt env fieldexprs fieldtyps + | TAnonymous (Union fieldtyps) -> + check_union env fieldexprs fieldtyps + | _ -> + checker_error env "Not a record %a" ptyp t + end + + | lid, ts, cgs when kind env lid = Some Record -> let fieldtyps = assert_flat env (lookup_type env lid) in let fieldtyps = List.map (fun (field, (typ, m)) -> - field, (DeBruijn.subst_tn ts typ, m) + field, (DeBruijn.subst_ctn' cgs (DeBruijn.subst_tn ts typ), m) ) fieldtyps in check_fields_opt env fieldexprs fieldtyps - | TApp (lid, ts) when kind env lid = Some Union -> + + | lid, ts, cgs when kind env lid = Some Union -> let fieldtyps = assert_union env (lookup_type env lid) in let fieldtyps = List.map (fun (field, typ) -> - field, DeBruijn.subst_tn ts typ + field, DeBruijn.subst_ctn' cgs (DeBruijn.subst_tn ts typ) ) fieldtyps in check_union env fieldexprs fieldtyps - | TAnonymous (Flat fieldtyps) -> - check_fields_opt env fieldexprs fieldtyps - | TAnonymous (Union fieldtyps) -> - check_union env fieldexprs fieldtyps + | _ -> - checker_error env "Not a record %a" ptyp t + checker_error env "Not a record (2) %a" ptyp t end | ESwitch (scrut, branches) -> @@ -818,16 +821,18 @@ and infer_and_check_eq: 'a. env -> ('a -> typ) -> 'a list -> typ = Option.must !t_base and find_field env t field = - match expand_abbrev env t with - | TQualified lid -> - Some (find_field_from_def env (lookup_type env lid) field) - | TApp (lid, ts) -> + let t = expand_abbrev env t in + match flatten_tapp t with + | exception Invalid_argument _ -> + begin match t with + | TAnonymous def -> + Some (find_field_from_def env def field) + | _ -> + None + end + | lid, ts, cgs -> let t, mut = find_field_from_def env (lookup_type env lid) field in - Some (DeBruijn.subst_tn ts t, mut) - | TAnonymous def -> - Some (find_field_from_def env def field) - | _ -> - None + Some (DeBruijn.(subst_ctn' cgs (subst_tn ts t), mut)) and find_field_from_def env def field = try begin match def with @@ -1079,6 +1084,8 @@ and subtype env t1 t2 = i = i' | TApp (lid, args), TApp (lid', args') -> lid = lid' && List.for_all2 (eqtype env) args args' + | TCgApp (lid, args), TCgApp (lid', args') -> + subtype env lid lid' && args = args' | TTuple ts1, TTuple ts2 -> List.length ts1 = List.length ts2 && List.for_all2 (subtype env) ts1 ts2 @@ -1116,11 +1123,11 @@ and subtype env t1 t2 = | TAnonymous (Flat [ Some f, (t, _) ]), TAnonymous (Union ts) -> List.exists (fun (f', t') -> f = f' && subtype env t t') ts - | TApp (lid, ts), _ when Hashtbl.mem MonomorphizationState.state (lid, ts) -> - subtype env (TQualified (snd (Hashtbl.find MonomorphizationState.state (lid, ts)))) t2 + | TApp (lid, ts), _ when Hashtbl.mem MonomorphizationState.state (lid, ts, []) -> + subtype env (TQualified (snd (Hashtbl.find MonomorphizationState.state (lid, ts, [])))) t2 - | _, TApp (lid, ts) when Hashtbl.mem MonomorphizationState.state (lid, ts) -> - subtype env t1 (TQualified (snd (Hashtbl.find MonomorphizationState.state (lid, ts)))) + | _, TApp (lid, ts) when Hashtbl.mem MonomorphizationState.state (lid, ts, []) -> + subtype env t1 (TQualified (snd (Hashtbl.find MonomorphizationState.state (lid, ts, [])))) | _ -> false diff --git a/lib/DeBruijn.ml b/lib/DeBruijn.ml index ee4131f9f..b3de41f2f 100644 --- a/lib/DeBruijn.ml +++ b/lib/DeBruijn.ml @@ -271,26 +271,63 @@ let cg_of_expr diff e = match e.node with | EBound k -> assert (k - diff >= 0); - `Var (k - diff) + CgVar (k - diff) | EConstant (w, s) -> - `Const (w, s) + CgConst (w, s) | _ -> failwith "Unsuitable const generic" (* Substitute const generics *) -class subst_c (diff: int) (c: expr) = object (self) - inherit map_counting_cg - method! visit_TCgArray ((i, _) as env) t j = +class subst_ct (c: cg) = object (self) + (* There are no const generic binders -- nothing to increment *) + inherit [_] map + method! visit_TCgArray (i as env) t j = let t = self#visit_typ env t in - match cg_of_expr diff c with - | `Var v' -> + (* We wish to replace i with c in [ t; j ] *) + match c with + | CgVar v' -> (* we substitute v' for i in [ t; j ] *) if j = i then TCgArray (t, v' + i (* = lift_cg i v' *)) else TCgArray (t, if j < i then j else j-1) - | `Const (w, s) -> - TArray (t, (w, s)) + | CgConst (w, s) -> + if j = i then + TArray (t, (w, s)) + else + TCgArray (t, if j < i then j else j-1) + + method! visit_TCgApp (i as env) t arg = + let t = self#visit_typ env t in + (* We are seeking to replace i with c in TCgApp (t, arg) *) + match arg with + | CgVar j -> + (* We are visiting a TCgApp that contains a variable: that variable (the + argument of the TCgApp) is a candidate for substitution. *) + begin match c with + | CgVar v' -> + (* We substitute v' for i in TCgApp (t, CgVar j) *) + if j = i then + TCgApp (t, CgVar (v' + i) (* = lift_cg i v' *)) + else + TCgApp (t, CgVar (if j < i then j else j-1)) + | CgConst _ -> + (* We substitute c for i in TCgApp (t, CgVar j) *) + if j = i then + TCgApp (t, c) + else + TCgApp (t, CgVar (if j < i then j else j-1)) + end + | _ -> + TCgApp (t, arg) +end + +(* Substitute const generics *) +class subst_c (diff: int) (c: expr) = object (_self) + inherit map_counting_cg + method! visit_typ ((i, _) as _env) t = + let c = cg_of_expr diff c in + (new subst_ct c)#visit_typ i t method! visit_EBound ((_, i), _) j = if j = i then @@ -309,7 +346,9 @@ let subst_cen diff cs t = let l = List.length cs in KList.fold_lefti (fun i body arg -> let k = l - i - 1 in - subst_ce diff arg k body + let body = subst_ce diff arg k body in + (* KPrint.bprintf "k=%d body=%a\n\n" k PrintAst.pexpr body; *) + body ) t cs let subst_ctn diff cs t = @@ -318,3 +357,10 @@ let subst_ctn diff cs t = let k = l - i - 1 in subst_ct diff arg k body ) t cs + +let subst_ctn' cs t = + let l = List.length cs in + KList.fold_lefti (fun i body arg -> + let k = l - i - 1 in + (new subst_ct arg)#visit_typ k body + ) t cs diff --git a/lib/Diagnostics.ml b/lib/Diagnostics.ml index 6adb92b99..241c335c5 100644 --- a/lib/Diagnostics.ml +++ b/lib/Diagnostics.ml @@ -38,7 +38,7 @@ let types_depth files = and depth_of_type p t = match t with | TArrow _ - | TInt _ | TBool | TUnit | TAny | TBuf _ | TArray _ | TCgArray _ -> + | TInt _ | TBool | TUnit | TAny | TBuf _ | TArray _ | TCgArray _ | TCgApp _ -> 0, List.rev p | TQualified lid -> begin try diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index d5aa81f33..0986a8378 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -60,6 +60,7 @@ let build_def_map files = include MonomorphizationState let has_variables = List.exists (function TBound _ -> assert !Options.allow_tapps; true | _ -> false) +let has_cg_variables = List.exists (function CgVar _ -> assert !Options.allow_tapps; true | _ -> false) let monomorphize_data_types map = object(self) @@ -73,15 +74,15 @@ let monomorphize_data_types map = object(self) (* Current file, for warning purposes. *) val mutable current_file = "" (* Possibly populated with something relevant *) - val mutable best_hint: node * lident = (dummy_lid, []), dummy_lid + val mutable best_hint: node * lident = (dummy_lid, [], []), dummy_lid (* For forward references, a map from lid to its pending monomorphizations (type arguments) *) - val pending_monomorphizations = Hashtbl.create 41 + val pending_monomorphizations: (lident, (typ list * cg list)) Hashtbl.t = Hashtbl.create 41 val seen_declarations = Hashtbl.create 41 method sanity_check () = - Hashtbl.iter (fun lid args -> - KPrint.bprintf "Missing monomorphization: %a<%a>\n" plid lid ptyps args + Hashtbl.iter (fun lid (ts, cgs) -> + KPrint.bprintf "Missing monomorphization: %a\n" ptyp (fold_tapp (lid, ts, cgs)) ) pending_monomorphizations; if Hashtbl.length pending_monomorphizations > 0 then Warn.fatal_error "Internal error: missing monomorphizations" @@ -107,7 +108,7 @@ let monomorphize_data_types map = object(self) (object inherit [_] map method! visit_TTuple () args = - match Hashtbl.find state (tuple_lid, args) with + match Hashtbl.find state (tuple_lid, args, []) with | exception Not_found -> let args = List.map (self#visit_typ false) args in TTuple args @@ -115,7 +116,7 @@ let monomorphize_data_types map = object(self) TQualified chosen_lid method! visit_TApp () lid args = - match Hashtbl.find state (lid, args) with + match Hashtbl.find state (lid, args, []) with | exception Not_found -> let args = List.map (self#visit_typ false) args in TApp (lid, args) @@ -125,18 +126,20 @@ let monomorphize_data_types map = object(self) (* Compute the name of a given node in the graph. *) method private lid_of (n: node) = - if List.length (snd n) = 0 then - fst n, [] + let lid, ts, cgs = n in + if ts = [] && cgs = [] then + lid, [] else if fst best_hint = n then snd best_hint, [] else - let lid, args = n in - let doc = PPrint.(separate_map underscore PrintAst.print_typ (List.map self#pretty args)) in + let doc = PPrint.(separate_map underscore PrintAst.print_typ (List.map self#pretty ts) ^^ + if cgs = [] then empty else underscore ^^ separate_map underscore PrintAst.print_cg cgs) + in let name = fst lid, KPrint.bsprintf "%s__%a" (snd lid) PrintCommon.pdoc doc in if Options.debug "monomorphization" then KPrint.bprintf "No hint provided for %a\n current best hint: %a -> %a\n picking: %a\n" - ptyp (TApp (lid, args)) - ptyp (TApp (fst (fst best_hint), snd (fst best_hint))) + ptyp (fold_tapp (lid, ts, [])) + ptyp (fold_tapp (fst best_hint)) plid (snd best_hint) plid name; name, [ Common.AutoGenerated ] @@ -153,12 +156,12 @@ let monomorphize_data_types map = object(self) * order declarations as they are needed, including that of the node we are * visiting. *) method private visit_node (under_ref: bool) (n: node) = - let lid, args = n in + let lid, args, cgs = n in (* White, gray or black? *) match Hashtbl.find state n with | exception Not_found -> if Options.debug "data-types-traversal" then - KPrint.bprintf "visiting %a<%a>: Not_found\n" plid (fst n) ptyps (snd n); + KPrint.bprintf "visiting %a: Not_found\n" ptyp (fold_tapp n); let chosen_lid, flag = self#lid_of n in if lid = tuple_lid then begin Hashtbl.add state n (Gray, chosen_lid); @@ -172,7 +175,7 @@ let monomorphize_data_types map = object(self) Hashtbl.add state n (Gray, chosen_lid); let subst fields = List.map (fun (field, (t, m)) -> - field, (DeBruijn.subst_tn args t, m) + field, (DeBruijn.subst_ctn' cgs (DeBruijn.subst_tn args t), m) ) fields in begin match Hashtbl.find map lid with | exception Not_found -> @@ -196,12 +199,12 @@ let monomorphize_data_types map = object(self) something we want to visit later (once we're done with this particular traversal)... *) if Options.debug "data-types-traversal" then - KPrint.bprintf "DEFERRING %a<%a>\n" plid (fst n) ptyps (snd n); + KPrint.bprintf "DEFERRING %a\n" ptyp (fold_tapp n); if match def with Union _ -> true | _ -> false then self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion)) else self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct)); - Hashtbl.add pending_monomorphizations (fst n) (snd n); + Hashtbl.add pending_monomorphizations lid (args, cgs); Hashtbl.remove state n | flags, Variant branches -> let branches = List.map (fun (cons, fields) -> cons, subst fields) branches in @@ -232,7 +235,7 @@ let monomorphize_data_types map = object(self) chosen_lid | Gray, chosen_lid -> if Options.debug "data-types-traversal" then - KPrint.bprintf "visiting %a<%a>: Gray\n" plid (fst n) ptyps (snd n); + KPrint.bprintf "visiting %a: Gray\n" ptyp (fold_tapp n); begin match Hashtbl.find map lid with | exception Not_found -> () @@ -244,7 +247,7 @@ let monomorphize_data_types map = object(self) chosen_lid | Black, chosen_lid -> if Options.debug "data-types-traversal" then - KPrint.bprintf "visiting %a<%a>: Black\n" plid (fst n) ptyps (snd n); + KPrint.bprintf "visiting %a: Black\n" ptyp (fold_tapp n); chosen_lid (* Top-level, non-parameterized declarations are root of our graph traversal. @@ -257,16 +260,16 @@ let monomorphize_data_types map = object(self) if Options.debug "data-types-traversal" then KPrint.bprintf "decl %a\n" plid (lid_of_decl d); match d with - | DType (lid, _, 0, 0, Abbrev (TTuple args)) when not (Hashtbl.mem state (tuple_lid, args)) -> + | DType (lid, _, 0, 0, Abbrev (TTuple args)) when not (Hashtbl.mem state (tuple_lid, args, [])) -> Hashtbl.remove map lid; if Options.debug "monomorphization" then KPrint.bprintf "%a abbreviation for %a\n" plid lid ptyp (TApp (tuple_lid, args)); - best_hint <- (tuple_lid, args), lid; - ignore (self#visit_node false (tuple_lid, args)); + best_hint <- (tuple_lid, args, []), lid; + ignore (self#visit_node false (tuple_lid, args, [])); Hashtbl.add seen_declarations lid (); self#clear () - | DType (lid, _, 0, 0, Abbrev (TApp (hd, args) as t)) when not (Hashtbl.mem state (hd, args)) -> + | DType (lid, _, 0, 0, Abbrev ((TApp _ | TCgApp _) as t)) when not (Hashtbl.mem state (flatten_tapp t)) -> (* We have not yet monomorphized this type, and conveniently, we have a type abbreviation that provides us with a name hint! We simply ditch the type abbreviation and replace it with a monomorphization @@ -275,6 +278,8 @@ let monomorphize_data_types map = object(self) if Options.debug "monomorphization" then KPrint.bprintf "%a abbreviation for %a\n" plid lid ptyp t; + let hd, args, cgs = flatten_tapp t in + (* miTLS backwards-compat strikes again: if the type is about to be GC'd (i.e. automatically rewritten to be heap-allocated to e.g. support lists "trivially" at the expense of a run-time GC)... then @@ -283,11 +288,11 @@ let monomorphize_data_types map = object(self) let abbrev_for_gc_type = Hashtbl.mem map hd && List.mem Common.GcType (fst (Hashtbl.find map hd)) in if abbrev_for_gc_type then - best_hint <- (hd, args), (fst lid, snd lid ^ "_gc") + best_hint <- (hd, args, cgs), (fst lid, snd lid ^ "_gc") else - best_hint <- (hd, args), lid; + best_hint <- (hd, args, cgs), lid; - ignore (self#visit_node false (hd, args)); + ignore (self#visit_node false (hd, args, cgs)); (* And a type abbreviation will automatically be rewritten (see GcTypes) into `typedef foobar foobar_gc *`. And mitlsffi.ci will be @@ -302,8 +307,8 @@ let monomorphize_data_types map = object(self) (* The type itself cannot be monomorphized, but we may have seen in the past monomorphic instances of this type that we ought to generate. *) - List.iter (fun args -> - ignore (self#visit_node false (lid, args)); + List.iter (fun (ts, cgs) -> + ignore (self#visit_node false (lid, ts, cgs)); Hashtbl.remove pending_monomorphizations lid ) (Hashtbl.find_all pending_monomorphizations lid); @@ -319,7 +324,7 @@ let monomorphize_data_types map = object(self) side-effectfully register the type as visited in our map for further uses (but why?). *) ignore (self#visit_decl false d); - ignore (self#visit_node false (lid, [])); + ignore (self#visit_node false (lid, [], [])); Hashtbl.add seen_declarations lid (); self#clear () @@ -343,17 +348,24 @@ let monomorphize_data_types map = object(self) PRecord (List.mapi (fun i p -> self#field_at i, self#visit_pattern under_ref p) pats) method! visit_TTuple under_ref ts = - TQualified (self#visit_node under_ref (tuple_lid, ts)) + TQualified (self#visit_node under_ref (tuple_lid, ts, [])) method! visit_TQualified under_ref lid = - TQualified (self#visit_node under_ref (lid, [])) + TQualified (self#visit_node under_ref (lid, [], [])) method! visit_TApp under_ref lid ts = if Hashtbl.mem map lid && not (has_variables ts) then - TQualified (self#visit_node under_ref (lid, ts)) + TQualified (self#visit_node under_ref (lid, ts, [])) else super#visit_TApp under_ref lid ts + method! visit_TCgApp under_ref t cg = + let lid, ts, cgs = flatten_tapp (TCgApp (t, cg)) in + if Hashtbl.mem map lid && not (has_variables ts) && not (has_cg_variables cgs) then + TQualified (self#visit_node under_ref (lid, ts, cgs)) + else + super#visit_TCgApp under_ref t cg + method! visit_TBuf _ t const = TBuf (self#visit_typ true t, const) end @@ -485,7 +497,14 @@ let functions files = let binders = List.map (fun { node; typ } -> { node; typ = DeBruijn.(subst_ctn diff cgs (subst_tn ts typ)) } ) binders in + (* KPrint.bprintf "about to substitute: e=%a\ncgs=%a\nts=%a\n%a\n" *) + (* pexpr e *) + (* pexprs cgs *) + (* ptyps ts *) + (* pexpr (with_type TUnit (ETApp (e, cgs, ts))); *) + (* KPrint.bprintf "after to substitute: body:%a\n\n" pexpr body; *) let body = DeBruijn.(subst_cen (List.length binders) cgs (subst_ten ts body)) in + (* KPrint.bprintf "after substitution: body:%a\n\n" pexpr body; *) let body = self#visit_expr env body in DFunction (cc, flags, 0, 0, ret, name, binders, body) in diff --git a/lib/MonomorphizationState.ml b/lib/MonomorphizationState.ml index a511cd8f3..c3e156330 100644 --- a/lib/MonomorphizationState.ml +++ b/lib/MonomorphizationState.ml @@ -1,4 +1,4 @@ open Ast -type node = lident * typ list +type node = lident * typ list * cg list type color = Gray | Black let state: (node, color * lident) Hashtbl.t = Hashtbl.create 41 diff --git a/lib/PrintAst.ml b/lib/PrintAst.ml index 6d9a1b825..182bf0d6a 100644 --- a/lib/PrintAst.ml +++ b/lib/PrintAst.ml @@ -172,11 +172,16 @@ and print_typ_paren = function | t -> print_typ t +and print_cg = function + | CgVar i -> int i + | CgConst c -> print_constant c + and print_typ = function | TInt w -> print_width w | TBuf (t, bool) -> (if bool then string "const" else empty) ^/^ print_typ t ^^ star | TArray (t, k) -> print_typ t ^^ lbracket ^^ print_constant k ^^ rbracket | TCgArray (t, v) -> print_typ t ^^ lbracket ^^ int v ^^ rbracket + | TCgApp (t, cg) -> print_typ t ^^ brackets (brackets (print_cg cg)) | TUnit -> string "()" | TQualified name -> string (string_of_lident name) | TBool -> string "bool" From 416d59a1d7be5c8a211e10493897d7b79650266d Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Fri, 8 Dec 2023 02:20:44 -0800 Subject: [PATCH 10/21] Various missing cases in checker, monomorphization, and fixing a type error in removing struct literals --- lib/AstToCStar.ml | 2 +- lib/Checker.ml | 17 ++++++++++++++++- lib/DeBruijn.ml | 9 ++++++--- lib/Helpers.ml | 2 +- lib/Monomorphization.ml | 37 ++++++++++++++++++++++++++++++++++--- lib/PrintAst.ml | 2 +- lib/PrintCommon.ml | 5 ++++- lib/Structs.ml | 10 +++++----- 8 files changed, 68 insertions(+), 16 deletions(-) diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml index aa87e6a60..58419d0a8 100644 --- a/lib/AstToCStar.ml +++ b/lib/AstToCStar.ml @@ -803,7 +803,7 @@ and mk_return_type env = function | TAnonymous t -> mk_type_def env t | TCgArray _ -> - fatal_error "Internal failure: TCgArray not desugared here" + CStar.Qualified (["Eurydice"], "error_t_cg_array") | TCgApp _ -> fatal_error "Internal failure: TCgApp not desugared here" diff --git a/lib/Checker.ml b/lib/Checker.ml index 922442515..186db1f00 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -161,7 +161,10 @@ let rec check_everything ?warn files: bool * file list = and check_program env r (name, decls) = let env = locate env (File name) in let by_lid = Hashtbl.create 41 in - let decls = KList.filter_map (fun d -> + let total = List.length decls in + let decls = KList.filter_mapi (fun i d -> + if Options.debug "checker" then + KPrint.bprintf "CHECKER PROGRESS: %d/%d\n" (i + 1) total; try check_decl env d; Some d @@ -1123,12 +1126,24 @@ and subtype env t1 t2 = | TAnonymous (Flat [ Some f, (t, _) ]), TAnonymous (Union ts) -> List.exists (fun (f', t') -> f = f' && subtype env t t') ts + | TTuple ts, _ when Hashtbl.mem MonomorphizationState.state (tuple_lid, ts, []) -> + subtype env (TQualified (snd (Hashtbl.find MonomorphizationState.state (tuple_lid, ts, [])))) t2 + + | _, TTuple ts when Hashtbl.mem MonomorphizationState.state (tuple_lid, ts, []) -> + subtype env t1 (TQualified (snd (Hashtbl.find MonomorphizationState.state (tuple_lid, ts, [])))) + | TApp (lid, ts), _ when Hashtbl.mem MonomorphizationState.state (lid, ts, []) -> subtype env (TQualified (snd (Hashtbl.find MonomorphizationState.state (lid, ts, [])))) t2 | _, TApp (lid, ts) when Hashtbl.mem MonomorphizationState.state (lid, ts, []) -> subtype env t1 (TQualified (snd (Hashtbl.find MonomorphizationState.state (lid, ts, [])))) + | TCgApp _, _ when Hashtbl.mem MonomorphizationState.state (flatten_tapp t1) -> + subtype env (TQualified (snd (Hashtbl.find MonomorphizationState.state (flatten_tapp t1)))) t2 + + | _, TCgApp _ when Hashtbl.mem MonomorphizationState.state (flatten_tapp t2) -> + subtype env t1 (TQualified (snd (Hashtbl.find MonomorphizationState.state (flatten_tapp t2)))) + | _ -> false diff --git a/lib/DeBruijn.ml b/lib/DeBruijn.ml index b3de41f2f..b75b1732b 100644 --- a/lib/DeBruijn.ml +++ b/lib/DeBruijn.ml @@ -250,7 +250,7 @@ let open_branch bs pat expr = class map_counting_cg = object (* The environment [i] has type [int*int]. *) - inherit [_] map + inherit [_] map as super (* The environment is a pair [i, i']. The first component [i] is the DeBruijn index we are looking for, after entering ONLY the cg binders. It it set by the caller and does not increase afterwards since the only cg binders are at @@ -259,6 +259,9 @@ class map_counting_cg = object at each binder, in expressions. *) method! extend ((i: int), i') (_: binder) = i, i' + 1 + + method! visit_ETApp ((i, i'), env) e cgs ts = + super#visit_ETApp ((i + List.length cgs, i'), env) e cgs ts end (* Converting an expression into a suitable const generic usable in types, knowing @@ -297,8 +300,8 @@ class subst_ct (c: cg) = object (self) else TCgArray (t, if j < i then j else j-1) - method! visit_TCgApp (i as env) t arg = - let t = self#visit_typ env t in + method! visit_TCgApp i t arg = + let t = self#visit_typ i t in (* We are seeking to replace i with c in TCgApp (t, arg) *) match arg with | CgVar j -> diff --git a/lib/Helpers.ml b/lib/Helpers.ml index bf1e334e1..dc56cca75 100644 --- a/lib/Helpers.ml +++ b/lib/Helpers.ml @@ -185,7 +185,7 @@ let fold_arrow ts t_ret = rather than a hardcoded list in krml *) let is_aligned_type = function ["Lib"; "IntVector"; "Intrinsics"], ("vec128"|"vec256"|"vec512") -> true | _ -> false -let is_array = function TArray _ -> true | _ -> false +let is_array = function TCgArray _ | TArray _ -> true | _ -> false let is_union = function TAnonymous (Union _) -> true | _ -> false diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index 0986a8378..b13d77746 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -59,7 +59,34 @@ let build_def_map files = include MonomorphizationState -let has_variables = List.exists (function TBound _ -> assert !Options.allow_tapps; true | _ -> false) +let has_variables ts= + let r = + (object + inherit [_] reduce + method zero = false + method plus = (||) + method! visit_TBound _ _ = + true + end)#visit_TApp () ([], "") ts + in + if r then + assert !Options.allow_tapps; + r + +let has_cg_array ts = + let r = + (object + inherit [_] reduce + method zero = false + method plus = (||) + method! visit_TCgArray _ _ _ = + true + end)#visit_TApp () ([], "") ts + in + if r then + assert !Options.allow_tapps; + r + let has_cg_variables = List.exists (function CgVar _ -> assert !Options.allow_tapps; true | _ -> false) let monomorphize_data_types map = object(self) @@ -177,6 +204,7 @@ let monomorphize_data_types map = object(self) let subst fields = List.map (fun (field, (t, m)) -> field, (DeBruijn.subst_ctn' cgs (DeBruijn.subst_tn args t), m) ) fields in + assert (not (Hashtbl.mem map lid) || not (has_variables args) && not (has_cg_variables cgs)); begin match Hashtbl.find map lid with | exception Not_found -> (* Unknown, external non-polymorphic lid, e.g. Prims.int *) @@ -348,13 +376,16 @@ let monomorphize_data_types map = object(self) PRecord (List.mapi (fun i p -> self#field_at i, self#visit_pattern under_ref p) pats) method! visit_TTuple under_ref ts = - TQualified (self#visit_node under_ref (tuple_lid, ts, [])) + if not (has_variables ts) && not (has_cg_array ts) then + TQualified (self#visit_node under_ref (tuple_lid, ts, [])) + else + super#visit_TTuple under_ref ts method! visit_TQualified under_ref lid = TQualified (self#visit_node under_ref (lid, [], [])) method! visit_TApp under_ref lid ts = - if Hashtbl.mem map lid && not (has_variables ts) then + if Hashtbl.mem map lid && not (has_variables ts) && not (has_cg_array ts) then TQualified (self#visit_node under_ref (lid, ts, [])) else super#visit_TApp under_ref lid ts diff --git a/lib/PrintAst.ml b/lib/PrintAst.ml index 182bf0d6a..6c34549c8 100644 --- a/lib/PrintAst.ml +++ b/lib/PrintAst.ml @@ -302,7 +302,7 @@ and print_expr { node; typ } = braces_with_nesting (print_expr e4) | EBufCreateL (l, es) -> print_lifetime l ^/^ - string "newbuf" ^/^ braces_with_nesting (separate_map (comma ^^ break1) print_expr es) + string "newbuf" ^/^ braces_with_nesting (flow (comma ^^ break1) (List.map print_expr es)) | ECons (ident, es) -> string ident ^/^ if List.length es > 0 then diff --git a/lib/PrintCommon.ml b/lib/PrintCommon.ml index 1ef8f1860..be3eef09f 100644 --- a/lib/PrintCommon.ml +++ b/lib/PrintCommon.ml @@ -78,8 +78,11 @@ let print_cc = function | StdCall -> string "__stdcall" | FastCall -> string "__fastcall" +let xstring s = + string (String.concat "␣" (KString.split_on_char ' ' s)) + let print_lident (idents, ident) = - separate_map dot string (idents @ [ ident ]) + separate_map dot xstring (idents @ [ ident ]) let print_program p decls = separate_map (hardline ^^ hardline) p decls diff --git a/lib/Structs.ml b/lib/Structs.ml index ccfc30e34..175515318 100644 --- a/lib/Structs.ml +++ b/lib/Structs.ml @@ -741,19 +741,19 @@ let to_addr is_struct = let remove_literals = object (self) inherit [_] map as super - method private mk_path (e: expr) (t: typ) (fields: ident list) = - List.fold_left (fun acc f -> with_type t (EField (acc, f))) e fields + method private mk_path (e: expr) (fields: (ident * typ) list) = + List.fold_left (fun acc (f, t) -> with_type t (EField (acc, f))) e fields - method private explode (acc: expr list) (path: ident list) (e: expr) (dst: expr) = + method private explode (acc: expr list) (path: (ident * typ) list) (e: expr) (dst: expr): expr list = match e.node with | EFlat fields -> List.fold_left (fun acc (f, e) -> let f = Option.must f in - self#explode acc (f :: path) e dst + self#explode acc ((f, e.typ) :: path) e dst ) acc fields | _ -> let e = self#visit_expr_w () e in - with_type TUnit (EAssign (self#mk_path dst e.typ (List.rev path), e)) :: acc + with_type TUnit (EAssign (self#mk_path dst (List.rev path), e)) :: acc method! visit_ELet ((_, t) as env) b e1 e2 = match e1.node with From f0b4a9a92b72fa4a60dab13d419cbab9e1f92032 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Fri, 8 Dec 2023 20:26:55 +0100 Subject: [PATCH 11/21] Missing recursive call to infer --- lib/Checker.ml | 19 ++++++++----------- lib/PrintAst.ml | 2 +- 2 files changed, 9 insertions(+), 12 deletions(-) diff --git a/lib/Checker.ml b/lib/Checker.ml index 186db1f00..8f5055a97 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -633,7 +633,8 @@ and infer' env e = end | EAssign (e1, e2) -> - let t = check_valid_assignment_lhs env e1 in + let t = infer env e1 in + check_valid_assignment_lhs env e1; check env t e2; TUnit @@ -862,28 +863,24 @@ and check_valid_assignment_lhs env e = | EBound i -> let binder = find env i in if not binder.node.mut then - checker_error env "%a (a.k.a. %s) is not a mutable binding" pexpr e binder.node.name; - binder.typ + checker_error env "%a (a.k.a. %s) is not a mutable binding" pexpr e binder.node.name | EField (e, f) -> let t1 = check_valid_path env e in begin match find_field env t1 f with - | Some (t2, mut) -> + | Some (_, mut) -> if not mut then - checker_error env "the field %s of type %a is not marked as mutable" f ptyp t1; - t2 + checker_error env "the field %s of type %a is not marked as mutable" f ptyp t1 | None -> checker_error env "field not found %s" f end - | EBufRead _ -> + | EBufRead _ (* Introduced by the wasm struct allocation phase. *) - e.typ - | EQualified _ -> + | EQualified _ (* Introduced when collecting global initializers. *) - e.typ | EApp ({ node = ETApp _; _ }, _) -> (* Will be emitted as a macro, optimistically assuming that's ok, the C compiler will bark if not. *) - e.typ + () | _ -> checker_error env "EAssign wants a lhs that's a mutable, local variable, or a \ path to a mutable field; got %a instead" pexpr e diff --git a/lib/PrintAst.ml b/lib/PrintAst.ml index 6c34549c8..1e0630a19 100644 --- a/lib/PrintAst.ml +++ b/lib/PrintAst.ml @@ -252,7 +252,7 @@ and print_expr { node; typ } = print_lifetime l ^^ space ^^ print_app string "newbuf" print_expr [e1; e2] | EBufRead (e1, e2) -> - print_expr e1 ^^ colon ^^ print_typ e1.typ ^^ lbracket ^^ print_expr e2 ^^ rbracket + parens (print_expr e1 ^^ colon ^^ print_typ e1.typ) ^^ lbracket ^^ print_expr e2 ^^ rbracket | EBufWrite (e1, e2, e3) -> print_expr e1 ^^ (*colon ^^ print_typ e1.typ ^^*) lbracket ^^ print_expr e2 ^^ rbracket ^/^ string "<-" ^/^ print_expr e3 From 6500a77cee8c89bed737f638c055457450ed9ed4 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Mon, 11 Dec 2023 12:51:33 +0100 Subject: [PATCH 12/21] Actually a better way of dealing with polymorphic externals --- lib/Checker.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/lib/Checker.ml b/lib/Checker.ml index 8f5055a97..f463e53d4 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -510,7 +510,17 @@ and infer env e = check_subtype env t e.typ; e.typ <- prefer_nominal t e.typ; if Options.debug "checker" then KPrint.bprintf "[infer, now] %a\n" ptyp e.typ; - t + + (* This is all because of external that retain their polymorphic + signatures. TODO: does this alleviate the need for those crappy checks in + subtype? *) + match Hashtbl.find_opt MonomorphizationState.state (flatten_tapp t) with + | exception Invalid_argument _ -> t + | Some (_, lid) -> + if Options.debug "checker" then + KPrint.bprintf "FOUND MONOMORPHIZATION %a\n" plid lid; + TQualified lid + | None -> t and prefer_nominal t1 t2 = match t1, t2 with @@ -528,7 +538,6 @@ and best_buffer_type l t1 e2 = | _ -> TBuf (t1, false) - and infer' env e = let infer_app t es = let t_ret, t_args = flatten_arrow t in @@ -914,6 +923,8 @@ and infer_branches env t_scrutinee branches = ) branches and check_pat env t_context pat = + (* KPrint.bprintf "Checking pattern: %a\n" ppat pat; *) + (* KPrint.bprintf "t_context:%a\n" ptyp t_context; *) match pat.node with | PWild -> pat.typ <- t_context From 092e417e03c358f90a2152cd9afe4be09a1e399d Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 12 Dec 2023 12:21:31 +0100 Subject: [PATCH 13/21] Add some class --- lib/Ast.ml | 4 ++-- lib/Structs.ml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/Ast.ml b/lib/Ast.ml index 9d2a82b54..d712dd3be 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -352,8 +352,8 @@ class ['self] map_expr_adapter = object (self: 'self) let node = f (env, typ) x.node in { node; typ } - method visit_expr_w = - self#lift_w self#visit_expr' + method visit_expr_w env e = + self#visit_expr (env, e.typ) e method visit_binder_w = self#lift_w self#visit_binder' diff --git a/lib/Structs.ml b/lib/Structs.ml index 175515318..76ec509d9 100644 --- a/lib/Structs.ml +++ b/lib/Structs.ml @@ -738,7 +738,7 @@ let to_addr is_struct = (* For C89 *) -let remove_literals = object (self) +class remove_literals = object (self) inherit [_] map as super method private mk_path (e: expr) (fields: (ident * typ) list) = @@ -777,7 +777,7 @@ let remove_literals = object (self) end let remove_literals files = - remove_literals#visit_files () files + (new remove_literals)#visit_files () files (* Debug any intermediary AST as follows: *) (* PPrint.(Print.(print (PrintAst.print_files files ^^ hardline))); *) From b329675d0f071d96455ed382901c67ec79aa6400 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 12 Dec 2023 13:33:29 +0100 Subject: [PATCH 14/21] Two missing cases in readonly analysis --- lib/Helpers.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/Helpers.ml b/lib/Helpers.ml index dc56cca75..c3e4cfde3 100644 --- a/lib/Helpers.ml +++ b/lib/Helpers.ml @@ -321,6 +321,8 @@ class ['self] readonly_visitor = object (self: 'self) method! visit_EBufFree _ _ = false method! visit_ESwitch _ _ _ = false method! visit_EReturn _ _ = false + method! visit_EContinue _ = false + method! visit_EAbort _ _ _ = false method! visit_EBreak _ = false method! visit_EFor _ _ _ _ _ _ = false method! visit_EWhile _ _ _ = false From 8e0595bdccd2035bb0cb6e014a227772565e2843 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 13 Dec 2023 09:48:53 +0100 Subject: [PATCH 15/21] tidbit --- lib/AstToCStar.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml index 58419d0a8..652e97428 100644 --- a/lib/AstToCStar.ml +++ b/lib/AstToCStar.ml @@ -954,6 +954,8 @@ and mk_program m name env decls = let n = string_of_lident (Ast.lid_of_decl d) in match mk_declaration m { env with type_names = names } d with | exception (Error e) -> + if Options.debug "backtraces" then + Printexc.print_backtrace stdout; Warn.maybe_fatal_error (fst e, Dropping (name ^ "/" ^ n, e)); decls, names | exception e -> From 1f52609c109dd46441f2bd769671f621fb628d31 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Mon, 18 Dec 2023 22:10:11 +0100 Subject: [PATCH 16/21] Expose a useful helper --- lib/Bundles.ml | 37 ++++++++++++++++++------------------- 1 file changed, 18 insertions(+), 19 deletions(-) diff --git a/lib/Bundles.ml b/lib/Bundles.ml index d3ad6adaf..0485fa448 100644 --- a/lib/Bundles.ml +++ b/lib/Bundles.ml @@ -16,6 +16,24 @@ let uniq = incr r; !r +let mark_private = + let add_if name flags = + let is_private = List.mem Common.Private flags in + if not is_private && not (Inlining.always_live name) then + Common.Private :: flags + else + flags + in + function + | DFunction (cc, flags, n_cgs, n, typ, name, binders, body) -> + DFunction (cc, add_if name flags, n_cgs, n, typ, name, binders, body) + | DGlobal (flags, name, n, typ, body) -> + DGlobal (add_if name flags, name, n, typ, body) + | DType (lid, flags, n_cgs, n, def) -> + DType (lid, add_if lid flags, n_cgs, n, def) + | DExternal (cc, flags, n_cg, n, lid, t, pp) -> + DExternal (cc, add_if lid flags, n_cg, n, lid, t, pp) + (** This collects all the files that match a given bundle specification, while * preserving their original dependency ordering within the bundle. If the * bundle is of the form Apis=Patterns, then the declarations from any of Apis @@ -39,25 +57,6 @@ let make_one_bundle (bundle: Bundle.t) (files: file list) (used: (int * Bundle.t List.mem name (List.map (String.concat "_") api) in - let mark_private = - let add_if name flags = - let is_private = List.mem Common.Private flags in - if not is_private && not (Inlining.always_live name) then - Common.Private :: flags - else - flags - in - function - | DFunction (cc, flags, n_cgs, n, typ, name, binders, body) -> - DFunction (cc, add_if name flags, n_cgs, n, typ, name, binders, body) - | DGlobal (flags, name, n, typ, body) -> - DGlobal (add_if name flags, name, n, typ, body) - | DType (lid, flags, n_cgs, n, def) -> - DType (lid, add_if lid flags, n_cgs, n, def) - | DExternal (cc, flags, n_cg, n, lid, t, pp) -> - DExternal (cc, add_if lid flags, n_cg, n, lid, t, pp) - in - (* Match a file against the given list of patterns. *) let match_file is_api patterns (used, found) (file: file) = List.fold_left (fun (used, found) pattern -> From 1152206421c227a7000aa1b4d3a0abe6c6dc42e2 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 19 Dec 2023 11:12:37 +0100 Subject: [PATCH 17/21] When emitting a polymorphic call, likely to be implemented as a macro, also pass the expected return type so that the macro can construct a compound literal if need be without having to do token concatenation, which is unaware of krml's naming choices. --- lib/AstToCStar.ml | 14 +++++++++----- lib/Checker.ml | 8 +------- lib/MonomorphizationState.ml | 6 ++++++ 3 files changed, 16 insertions(+), 12 deletions(-) diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml index 652e97428..4d0baa77e 100644 --- a/lib/AstToCStar.ml +++ b/lib/AstToCStar.ml @@ -358,11 +358,15 @@ and mk_expr env in_stmt e = | EConstant c -> CStar.Constant c - | EApp ({ node = ETApp (e, cgs, ts); _ }, es) when !Options.allow_tapps || whitelisted_tapp e -> - unit_to_void env e (cgs @ es) (List.map (fun t -> CStar.Type (mk_type env t)) ts) - - | ETApp (e, cgs, ts) when !Options.allow_tapps || whitelisted_tapp e -> - unit_to_void env e cgs (List.map (fun t -> CStar.Type (mk_type env t)) ts) + | EApp ({ node = ETApp (e0, cgs, ts); _ }, es) when !Options.allow_tapps || whitelisted_tapp e0 -> + (* Return type is oftentimes very useful when having to build a return value using e.g. a + compound literal *) + let ret_t = CStar.Type (mk_type env (MonomorphizationState.resolve e.typ)) in + unit_to_void env e0 (cgs @ es) (List.map (fun t -> CStar.Type (mk_type env t)) ts @ [ ret_t ]) + + | ETApp (e0, cgs, ts) when !Options.allow_tapps || whitelisted_tapp e0 -> + let ret_t = CStar.Type (mk_type env (MonomorphizationState.resolve e.typ)) in + unit_to_void env e0 cgs (List.map (fun t -> CStar.Type (mk_type env t)) ts @ [ ret_t ]) | EApp ({ node = EOp (op, w); _ }, [ _; _ ]) when is_arith op w -> fst (mk_arith env e) diff --git a/lib/Checker.ml b/lib/Checker.ml index f463e53d4..116589519 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -514,13 +514,7 @@ and infer env e = (* This is all because of external that retain their polymorphic signatures. TODO: does this alleviate the need for those crappy checks in subtype? *) - match Hashtbl.find_opt MonomorphizationState.state (flatten_tapp t) with - | exception Invalid_argument _ -> t - | Some (_, lid) -> - if Options.debug "checker" then - KPrint.bprintf "FOUND MONOMORPHIZATION %a\n" plid lid; - TQualified lid - | None -> t + MonomorphizationState.resolve t and prefer_nominal t1 t2 = match t1, t2 with diff --git a/lib/MonomorphizationState.ml b/lib/MonomorphizationState.ml index c3e156330..18f76e71e 100644 --- a/lib/MonomorphizationState.ml +++ b/lib/MonomorphizationState.ml @@ -2,3 +2,9 @@ open Ast type node = lident * typ list * cg list type color = Gray | Black let state: (node, color * lident) Hashtbl.t = Hashtbl.create 41 + +let resolve t = + match Hashtbl.find_opt state (flatten_tapp t) with + | exception Invalid_argument _ -> t + | Some (_, lid) -> TQualified lid + | None -> t From 22f275de48660a20cd7f4b4cd6c615ee2f5edb4e Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 20 Dec 2023 09:41:13 +0100 Subject: [PATCH 18/21] Fixup for new argument to macros --- lib/CStarToC11.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/lib/CStarToC11.ml b/lib/CStarToC11.ml index 5a302653a..a41c13e64 100644 --- a/lib/CStarToC11.ml +++ b/lib/CStarToC11.ml @@ -548,7 +548,7 @@ and mk_stmt m (stmt: stmt): C.stmt list = to double-ignore, since C does it for us automatically, and C compilers treat this as 100% normal UNLESS the programmer uses extensions like `__attribute__((nodiscard))`. *) - | Ignore (Call (Qualified ([ "LowStar"; "Ignore" ], "ignore"), [ arg; _ ])) when is_call arg -> + | Ignore (Call (Qualified ([ "LowStar"; "Ignore" ], "ignore"), [ arg; _; _ ])) when is_call arg -> [ Expr (mk_expr m arg) ] | Ignore e -> @@ -849,13 +849,13 @@ and mk_expr m (e: expr): C.expr = | Comma (e1, e2) -> Op2 (K.Comma, mk_expr m e1, mk_expr m e2) - | Call (Qualified ([ "LowStar"; "Ignore" ], "ignore"), [ _ ]) -> + | Call (Qualified ([ "LowStar"; "Ignore" ], "ignore"), [ arg; _; _ ]) -> + mk_ignore (is_var arg) (mk_expr m arg) + + | Call (Qualified ([ "LowStar"; "Ignore" ], "ignore"), _) -> (* Only one argument because of unit-to-void elimination -- should not happen. *) failwith "`ignore ()` should have been removed earlier on" - | Call (Qualified ([ "LowStar"; "Ignore" ], "ignore"), [ arg; _ ]) -> - mk_ignore (is_var arg) (mk_expr m arg) - | Call (Qualified ([ "C"; "Nullity" ], s), [ e1 ]) when KString.starts_with s "op_Bang_Star__" -> mk_deref m e1 From 0eda808be7c8470a451f9533355810a3f145dcfe Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 20 Dec 2023 09:41:58 +0100 Subject: [PATCH 19/21] tidbit --- test/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Makefile b/test/Makefile index d0d5bad92..e7f7e31f5 100644 --- a/test/Makefile +++ b/test/Makefile @@ -34,7 +34,7 @@ BROKEN = \ HigherOrder6.fst ForwardDecl.fst BlitNull.fst \ Ctypes1.fst Ctypes2.fst Ctypes3.fst Ctypes4.fst \ AbstractStructAbstract.fst MonomorphizationSeparate1.fst \ - Layered.fst GlobalInit2.fst Rust1.fst + Layered.fst GlobalInit2.fst $(wildcard Rust*.fst) # Lowlevel is not really broken, but its test shouldn't be run since it's a # special file and doesn't have a main. From 41612c692294d6c1cb8fe40cfc76788ae31f9f09 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 20 Dec 2023 19:17:16 +0100 Subject: [PATCH 20/21] omg --- lib/Builtin.ml | 4 ++-- lib/Checker.ml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/Builtin.ml b/lib/Builtin.ml index 613397a68..3f8fb229a 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -437,8 +437,8 @@ let prepare files = F* PR: References to module C can now occur even when the module is not in the scope. If so, we add the definition that is needed as a builtin, since it will be rewritten during C code generation *) - if List.mem_assoc "C" files then [] else [c_deref] @ - if List.mem_assoc "LowStar_Ignore" files then [] else [lowstar_ignore] @ + (if List.mem_assoc "C" files then [] else [c_deref]) @ + (if List.mem_assoc "LowStar_Ignore" files then [] else [lowstar_ignore]) @ [] let make_libraries files = diff --git a/lib/Checker.ml b/lib/Checker.ml index 116589519..35cf0afbf 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -536,9 +536,9 @@ and infer' env e = let infer_app t es = let t_ret, t_args = flatten_arrow t in if List.length t_args = 0 then - checker_error env "This is not a function:\n%a" pexpr e; + checker_error env "This is not a function type:\n%a a.k.a. %s\n" ptyp t (show_typ t); if List.length es > List.length t_args then - checker_error env "Too many arguments for application:\n%a" pexpr e; + checker_error env "Too many arguments for application:\n%a" pexprs es; let t_args, t_remaining_args = KList.split (List.length es) t_args in ignore (List.map2 (check_or_infer env) t_args es); fold_arrow t_remaining_args t_ret From 0eebaa9a545a09116a8204f62025ecb37f7a9015 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Thu, 21 Dec 2023 19:46:11 -0800 Subject: [PATCH 21/21] tidbit --- lib/Builtin.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Builtin.ml b/lib/Builtin.ml index cb7e82903..9b95eaf25 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -376,7 +376,7 @@ let make_abstract_function_or_global = function * - lets are replaced by vals * - but we keep the gte_mask and eq_mask functions *) let make_abstract (name, decls) = - name, List.map (function + name, List.filter_map (function | DType (_, _, _, _, Abbrev _) as t -> Some t | DType _ ->