From b9aae0202ab07bea7fc6be11178e5b420a1bfa0e Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Fri, 13 Sep 2024 15:50:49 -0700 Subject: [PATCH] Better handling of comments --- lib/Ast.ml | 13 +++++++++---- lib/AstToMiniRust.ml | 16 +++++++++------- lib/DataTypes.ml | 8 ++++---- lib/DeBruijn.ml | 4 ++-- lib/Helpers.ml | 20 ++++++++++---------- lib/InputAstToAst.ml | 12 ++++++------ lib/Monomorphization.ml | 4 ++-- lib/PrintAst.ml | 8 ++++++-- lib/PrintMiniRust.ml | 1 + lib/Simplify.ml | 20 ++++++++++---------- lib/SimplifyWasm.ml | 4 ++-- lib/UseAnalysis.ml | 2 +- 12 files changed, 62 insertions(+), 50 deletions(-) diff --git a/lib/Ast.ml b/lib/Ast.ml index 72118ec1..9542d85f 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -120,12 +120,17 @@ and branch_t = and fields_t = (ident * (typ * bool)) list +type node_meta = + | NodeComment of string + +and node_meta' = node_meta [@visitors.opaque] [@@deriving show] (* This type, by virtue of being separated from the recursive definition of expr * and pattern, generates no implementation. We provide our own below. *) type 'a with_type = { node: 'a; - mutable typ: typ + mutable typ: typ; + meta: node_meta' list; (** Filled in by [Checker] *) } [@@deriving show] @@ -163,7 +168,7 @@ class ['self] map_typ_adapter = object (self: 'self) fun f (env, _) x -> let typ = self#visit_typ env x.typ in let node = f (env, typ) x.node in - { node; typ } + { node; typ; meta = x.meta } end class ['self] iter_typ_adapter = object (self: 'self) @@ -381,7 +386,7 @@ class ['self] map_expr_adapter = object (self: 'self) fun f env x -> let typ = self#visit_typ env x.typ in let node = f (env, typ) x.node in - { node; typ } + { node; typ; meta = x.meta } method visit_expr_w env e = self#visit_expr (env, e.typ) e @@ -679,7 +684,7 @@ let map_decls f files = List.map (fun (file, decls) -> file, List.map f decls) files let with_type typ node = - { typ; node } + { typ; node; meta = [] } let flatten_tapp t = let rec flatten_tapp cgs t = diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 48693341..fb5c091e 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -567,7 +567,7 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr (* However, generally, we will have a type provided by the context that may necessitate the insertion of conversions *) and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env * MiniRust.expr = - (* KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e; *) + KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e; let erase_lifetime_info = (object(self) inherit [_] MiniRust.DeBruijn.map @@ -641,9 +641,10 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env if erase_lifetime_info t = erase_lifetime_info t_ret then x else - Warn.failwith "type mismatch;\n e=%a\n t=%a\n t_ret=%a\n x=%a" + Warn.failwith "type mismatch;\n e=%a\n t=%a (verbose: %s)\n t_ret=%a\n x=%a" PrintAst.Ops.pexpr e - PrintMiniRust.ptyp t PrintMiniRust.ptyp t_ret + PrintMiniRust.ptyp t (MiniRust.show_typ t) + PrintMiniRust.ptyp t_ret PrintMiniRust.pexpr x; end in @@ -721,7 +722,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env assert (cgs @ cgs' = []); let es = match es with - | [ { typ = TUnit; node } ] -> assert (node = EUnit); [] + | [ { typ = TUnit; node; _ } ] -> assert (node = EUnit); [] | _ -> es in let env, e = translate_expr env e in @@ -739,7 +740,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env | EApp (e0, es) -> let es = match es with - | [ { typ = TUnit; node } ] -> assert (node = EUnit); [] + | [ { typ = TUnit; node; _ } ] -> assert (node = EUnit); [] | _ -> es in let env, e0 = translate_expr env e0 in @@ -1132,9 +1133,10 @@ let bind_decl env (d: Ast.decl): env = (* These sets are mutually exclusive, so we don't box *and* introduce a lifetime at the same time *) let box = Idents.LidSet.mem lid env.heap_structs in - KPrint.bprintf "%a: lifetime=%b\n" PrintAst.Ops.plid lid (Idents.LidSet.mem lid env.pointer_holding_structs); + let lifetime = Idents.LidSet.mem lid env.pointer_holding_structs in + KPrint.bprintf "%a (FLAT): lifetime=%b box=%b\n" PrintAst.Ops.plid lid lifetime box; let lifetime = - if Idents.LidSet.mem lid env.pointer_holding_structs then + if lifetime then Some (MiniRust.Label "a") else None diff --git a/lib/DataTypes.ml b/lib/DataTypes.ml index dcdbddbb..e737a756 100644 --- a/lib/DataTypes.ml +++ b/lib/DataTypes.ml @@ -137,7 +137,7 @@ let remove_unused_type_arguments files = chop (kept + 1) (i + 1) (def, binders, ret) else let def = DeBruijn.subst_te TAny (n - i - 1) def in - let binders = List.map (fun { node; typ } -> { node; typ = DeBruijn.subst_t TAny (n - i - 1) typ }) binders in + let binders = List.map (fun { node; typ; _ } -> { node; typ = DeBruijn.subst_t TAny (n - i - 1) typ; meta = [] }) binders in let ret = DeBruijn.subst_t TAny (n - i - 1) ret in chop kept (i + 1) (def, binders, ret) in @@ -511,17 +511,17 @@ let compile_simple_matches (map, enums) = object(self) method! visit_expr_w env x = let node = self#visit_expr' (env, x.typ) x.node in let typ = self#visit_typ env x.typ in - { node; typ } + { node; typ; meta = [] } method! visit_pattern_w env x = let node = self#visit_pattern' (env, x.typ) x.node in let typ = self#visit_typ env x.typ in - { node; typ } + { node; typ; meta = [] } method! visit_with_type f (env, _) x = let node = f (env, x.typ) x.node in let typ = self#visit_typ env x.typ in - { node; typ } + { node; typ; meta = [] } method! visit_TQualified _ lid = match Hashtbl.find map lid with diff --git a/lib/DeBruijn.ml b/lib/DeBruijn.ml index 0ee14808..f9d83777 100644 --- a/lib/DeBruijn.ml +++ b/lib/DeBruijn.ml @@ -234,7 +234,7 @@ let close_branch bs p e = let opening_binder b = let a = Atom.fresh () in let b = { b with node = { b.node with atom = a } } in - b, subst { node = EOpen (b.node.name, a); typ = b.typ } 0 + b, subst { node = EOpen (b.node.name, a); typ = b.typ; meta = [] } 0 let open_binder b e1 = let b, f = opening_binder b in @@ -254,7 +254,7 @@ let open_branch bs pat expr = List.fold_right (fun binder (bs, pat, expr) -> let b, expr = open_binder binder expr in let pat = - subst_p { node = POpen (b.node.name, b.node.atom); typ = b.typ } 0 pat + subst_p { node = POpen (b.node.name, b.node.atom); typ = b.typ; meta = [] } 0 pat in b :: bs, pat, expr ) bs ([], pat, expr) diff --git a/lib/Helpers.ml b/lib/Helpers.ml index 1bc198a6..acf1cdc8 100644 --- a/lib/Helpers.ml +++ b/lib/Helpers.ml @@ -71,7 +71,7 @@ let pwild = with_type TAny PWild let mk_op op w = { node = EOp (op, w); - typ = type_of_op op w } + typ = type_of_op op w; meta = [] } (* @0 < *) let mk_lt w finish = @@ -160,13 +160,13 @@ let unused_binding = sequence_binding let mk_binding ?(mut=false) name t = let b = fresh_binder name t in { b with node = { b.node with mut } }, - { node = EOpen (b.node.name, b.node.atom); typ = t } + { node = EOpen (b.node.name, b.node.atom); typ = t; meta = [] } (** Generates "let [[name]]: [[t]] = [[e]] in [[name]]" *) let mk_named_binding name t e = let b, ref = mk_binding name t in b, - { node = e; typ = t }, + { node = e; typ = t; meta = [] }, ref @@ -411,7 +411,7 @@ let rec is_initializer_constant e = match e with | { node = EAddrOf { node = EQualified _; _ }; _ } -> true - | { node = EQualified _; typ = t } -> + | { node = EQualified _; typ = t; _ } -> is_address t | { node = EEnum _; _ } -> true @@ -688,7 +688,7 @@ let rec strip_cast e = let rec nest bs t e2 = match bs with | (b, e1) :: bs -> - { node = ELet (b, e1, close_binder b (nest bs t e2)); typ = t } + { node = ELet (b, e1, close_binder b (nest bs t e2)); typ = t; meta = [] } | [] -> e2 @@ -715,22 +715,22 @@ let rec nest_in_return_pos i typ f e = match e.node with | ELet (b, e1, e2) -> let e2 = nest_in_return_pos (i + 1) typ f e2 in - { node = ELet (b, e1, e2); typ } + { node = ELet (b, e1, e2); typ; meta = [] } | EIfThenElse (e1, e2, e3) -> let e2 = nest_in_return_pos i typ f e2 in let e3 = nest_in_return_pos i typ f e3 in - { node = EIfThenElse (e1, e2, e3); typ } + { node = EIfThenElse (e1, e2, e3); typ; meta = [] } | ESwitch (e, branches) -> let branches = List.map (fun (t, e) -> t, nest_in_return_pos i typ f e ) branches in - { node = ESwitch (e, branches); typ } + { node = ESwitch (e, branches); typ; meta = [] } | EMatch (c, e, branches) -> { node = EMatch (c, e, List.map (fun (bs, p, e) -> bs, p, nest_in_return_pos (i + List.length bs) typ f e ) branches); - typ } + typ; meta = [] } | ESequence es -> let l = List.length es in { node = ESequence (List.mapi (fun j e -> @@ -738,7 +738,7 @@ let rec nest_in_return_pos i typ f e = nest_in_return_pos i typ f e else e - ) es); typ } + ) es); typ; meta = [] } | _ -> f i e diff --git a/lib/InputAstToAst.ml b/lib/InputAstToAst.ml index 3a78ef2a..d60078b9 100644 --- a/lib/InputAstToAst.ml +++ b/lib/InputAstToAst.ml @@ -9,7 +9,7 @@ open Common module I = InputAst let mk (type a) (node: a): a with_type = - { node; typ = TAny } + { node; typ = TAny; meta = [] } let rec binders_of_pat p = let open I in @@ -147,13 +147,13 @@ and mk_expr = function | I.EApp (I.ETApp (I.EQualified ([ "Steel"; "Reference" ], "null"), [ t ]), [ I.EUnit ]) | I.EApp (I.ETApp (I.EQualified ([ "C"; "Nullity" ], "null"), [ t ]), [ I.EUnit ]) | I.EBufNull t -> - { node = EBufNull; typ = TBuf (mk_typ t, false) } + { node = EBufNull; typ = TBuf (mk_typ t, false); meta = [] } | I.EApp (I.ETApp (I.EQualified ( [ "LowStar"; "Monotonic"; "Buffer" ], "is_null"), [ t; _; _ ]), [ e ]) | I.EApp (I.ETApp (I.EQualified ( [ "Steel"; "Reference" ], "is_null"), [ t ]), [ e ]) -> mk (EApp (mk (EPolyComp (K.PEq, TBuf (mk_typ t, false))), [ mk_expr e; - { node = EBufNull; typ = TBuf (mk_typ t, false) }])) + { node = EBufNull; typ = TBuf (mk_typ t, false); meta = [] }])) | I.EApp (e, es) -> mk (EApp (mk_expr e, List.map mk_expr es)) @@ -211,18 +211,18 @@ and mk_expr = function | I.EAbortS s -> mk (EAbort (None, Some s)) | I.EAbortT (s, t) -> - { node = EAbort (Some (mk_typ t), Some s); typ = mk_typ t } + { node = EAbort (Some (mk_typ t), Some s); typ = mk_typ t; meta = [] } | I.EReturn e -> mk (EReturn (mk_expr e)) | I.EFlat (tname, fields) -> - { node = EFlat (mk_fields fields); typ = mk_typ tname } + { node = EFlat (mk_fields fields); typ = mk_typ tname; meta = [] } | I.EField (tname, e, field) -> let e = { (mk_expr e) with typ = mk_typ tname } in mk (EField (e, field)) | I.ETuple es -> mk (ETuple (List.map mk_expr es)) | I.ECons (lid, id, es) -> - { node = ECons (id, List.map mk_expr es); typ = mk_typ lid } + { node = ECons (id, List.map mk_expr es); typ = mk_typ lid; meta = [] } | I.EFun (bs, e, t) -> mk (EFun (mk_binders bs, mk_expr e, mk_typ t)) | I.EComment (before, e, after) -> diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index ec9d1032..78e386b4 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -612,8 +612,8 @@ let functions files = (* binders are the remaining binders after the cg-binders have been eliminated *) let diff = List.length binders - List.length cgs in let _cg_binders, binders = KList.split (List.length cgs + List.length cgs') binders in - let binders = List.map (fun { node; typ } -> - { node; typ = DeBruijn.(subst_ctn diff cgs (subst_tn ts typ)) } + let binders = List.map (fun { node; typ; _ } -> + { node; typ = DeBruijn.(subst_ctn diff cgs (subst_tn ts typ)); meta = [] } ) binders in (* KPrint.bprintf "about to substitute:\n e=%a\n cgs=%a\n cgs'=%a\n ts=%a\n head type=%a\n%a\n" *) (* pexpr e *) diff --git a/lib/PrintAst.ml b/lib/PrintAst.ml index 0d743ccf..40a4a2ae 100644 --- a/lib/PrintAst.ml +++ b/lib/PrintAst.ml @@ -156,7 +156,7 @@ and print_flag = function | Target s -> string ("__attribute__((target = "^s^"))") -and print_binder { typ; node = { name; mut; meta; mark; _ }} = +and print_binder { typ; node = { name; mut; meta; mark; _ }; _ } = let o, u = !mark in (if mut then string "mutable" ^^ break 1 else empty) ^^ group (group (string name ^^ lparen ^^ string (Mark.show_occurrence o) ^^ comma ^^ @@ -212,8 +212,12 @@ and print_let_binding (binder, e1) = group (group (string "let" ^/^ print_binder binder ^/^ equals) ^^ jump (print_expr e1)) -and print_expr { node; typ } = +and print_expr { node; typ; meta } = (* print_typ typ ^^ colon ^^ space ^^ parens @@ *) + begin match List.filter_map (function NodeComment s -> Some s (* | _ -> None*) ) meta with + | [] -> empty + | s -> string (String.concat "\n" s) ^^ break1 + end ^^ match node with | EComment (s, e, s') -> surround 2 1 (string s) (print_expr e) (string s') diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml index 743795e7..06315e1b 100644 --- a/lib/PrintMiniRust.ml +++ b/lib/PrintMiniRust.ml @@ -184,6 +184,7 @@ let rec print_typ env (t: typ): document = let env = push_n_type env n in group @@ group (parens (separate_map (comma ^^ break1) (print_typ env) ts)) ^/^ + minus ^^ rangle ^^ print_typ env t | Bound n -> begin try diff --git a/lib/Simplify.ml b/lib/Simplify.ml index 9a7daa18..8be00383 100644 --- a/lib/Simplify.ml +++ b/lib/Simplify.ml @@ -379,11 +379,11 @@ let wrapping_arithmetic = object (self) let e = mk_op (K.without_wrap op) unsigned_w in let e1 = self#visit_expr env e1 in let e2 = self#visit_expr env e2 in - let c e = { node = ECast (e, TInt unsigned_w); typ = TInt unsigned_w } in + let c e = { node = ECast (e, TInt unsigned_w); typ = TInt unsigned_w; meta = [] } in (** TODO: the second call to [c] is optional per the C semantics, but in * order to preserve typing, we have to insert it... maybe recognize * that pattern later on at the C emission level? *) - let unsigned_app = { node = EApp (e, [ c e1; c e2 ]); typ = TInt unsigned_w } in + let unsigned_app = { node = EApp (e, [ c e1; c e2 ]); typ = TInt unsigned_w; meta = [] } in ECast (unsigned_app, TInt w) | EOp (((K.AddW | K.SubW | K.MultW | K.DivW) as op), w), [ e1; e2 ] when K.is_unsigned w -> @@ -432,7 +432,7 @@ let sequence_to_let = object (self) match List.rev es with | last :: first_fews -> (List.fold_left (fun cont e -> - { node = ELet (sequence_binding (), e, lift 1 cont); typ = last.typ } + { node = ELet (sequence_binding (), e, lift 1 cont); typ = last.typ; meta = [] } ) last first_fews).node | [] -> failwith "[sequence_to_let]: impossible (empty sequence)" @@ -491,7 +491,7 @@ let let_if_to_assign = object (self) method private make_assignment lhs e1 = let nest_assign = nest_in_return_pos TUnit (fun i innermost -> { node = EAssign (DeBruijn.lift i lhs, innermost); - typ = TUnit + typ = TUnit; meta = [] }) in match e1.node with | EIfThenElse (cond, e_then, e_else) -> @@ -1122,7 +1122,7 @@ and hoist_stmt loc e = (* This function returns an expression that can be successfully translated as a * C* expression. *) and hoist_expr loc pos e = - let mk node = { node; typ = e.typ } in + let mk node = { node; typ = e.typ; meta = e.meta } in match e.node with | ETApp (e, cgs, cgs', ts) -> let lhs, e = hoist_expr loc Unspecified e in @@ -1657,7 +1657,7 @@ let tail_calls = let rec hoist_bufcreate ifdefs (e: expr) = let hoist_bufcreate = hoist_bufcreate ifdefs in let under_pushframe = under_pushframe ifdefs in - let mk node = { node; typ = e.typ } in + let mk node = { node; typ = e.typ; meta = e.meta } in match e.node with | EMatch _ -> failwith "expected to run after match compilation" @@ -1737,16 +1737,16 @@ let rec hoist_bufcreate ifdefs (e: expr) = and under_pushframe ifdefs (e: expr) = let hoist_bufcreate = hoist_bufcreate ifdefs in let under_pushframe = under_pushframe ifdefs in - let mk node = { node; typ = e.typ } in + let mk node = { node; typ = e.typ; meta = e.meta } in match e.node with - | ELet (b, { node = EIfThenElse ({ node = EQualified lid; _ } as e1, e2, e3); typ }, ek) + | ELet (b, { node = EIfThenElse ({ node = EQualified lid; _ } as e1, e2, e3); typ; meta = [] }, ek) when Idents.LidSet.mem lid ifdefs -> (* Do not hoist, since this if will turn into an ifdef which does NOT shorten the scope...! TODO this does not catch all ifdefs *) let e2 = under_pushframe e2 in let e3 = under_pushframe e3 in let ek = under_pushframe ek in - mk (ELet (b, { node = EIfThenElse (e1, e2, e3); typ }, ek)) + mk (ELet (b, { node = EIfThenElse (e1, e2, e3); typ; meta = [] }, ek)) | ELet (b, e1, e2) -> let b1, e1 = hoist_bufcreate e1 in let e2 = under_pushframe e2 in @@ -1775,7 +1775,7 @@ and under_pushframe ifdefs (e: expr) = * code. This recursive routine is smarter and preserves the sequence of * let-bindings starting from the beginning of the scope. *) let rec find_pushframe ifdefs (e: expr) = - let mk node = { node; typ = e.typ } in + let mk node = { node; typ = e.typ; meta = e.meta } in match e.node with | ELet (b, ({ node = EPushFrame; _ } as e1), e2) -> mk (ELet (b, e1, under_pushframe ifdefs e2)) diff --git a/lib/SimplifyWasm.ml b/lib/SimplifyWasm.ml index 49027ee5..2205c1cd 100644 --- a/lib/SimplifyWasm.ml +++ b/lib/SimplifyWasm.ml @@ -172,9 +172,9 @@ let eta_expand = object let n = List.length targs in let binders, args = List.split (List.mapi (fun i t -> with_type t { name = Printf.sprintf "x%d" i; mut = false; mark = ref Mark.default; meta = None; atom = Atom.fresh (); attempt_inline = false }, - { node = EBound (n - i - 1); typ = t } + { node = EBound (n - i - 1); typ = t; meta = [] } ) targs) in - let body = { node = EApp (body, args); typ = tret } in + let body = { node = EApp (body, args); typ = tret; meta = [] } in DFunction (None, flags, 0, 0, tret, name, binders, body) | _ -> DGlobal (flags, name, n, t, body) diff --git a/lib/UseAnalysis.ml b/lib/UseAnalysis.ml index ae606095..1689cb06 100644 --- a/lib/UseAnalysis.ml +++ b/lib/UseAnalysis.ml @@ -208,7 +208,7 @@ let use_mark_to_remove_or_ignore final = object (self) ...) -- this is a bad idea, as it'll force the hoisting phase to hoist the bufcreate back into a let-binding, which will then be named "buf". *) else if not (is_bufcreate e1) then - ELet ({ node = { b.node with meta = Some MetaSequence }; typ = TUnit}, + ELet ({ node = { b.node with meta = Some MetaSequence }; typ = TUnit; meta = []}, push_ignore e1, e2) (* Definitely unused, push an ignore at depth *)