From 3c733ce1d82c8d31ec8cf3f10955d210e6b45a3e Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 18 Sep 2024 16:21:10 -0700 Subject: [PATCH] down to four errors in HACL --- lib/AstToMiniRust.ml | 8 ++++++-- lib/OptimizeMiniRust.ml | 26 ++++++++++++++++++-------- lib/PrintMiniRust.ml | 15 ++++++++++++++- 3 files changed, 38 insertions(+), 11 deletions(-) diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 95648f87..6dd6eb76 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -494,6 +494,10 @@ let translate_lid env lid = else allocate name +let translate_binder_name (b: Ast.binder) = + let open Ast in + if snd !(b.node.mark) = AtMost 0 then "_" ^ b.node.name else b.node.name + (* Trying to compile a *reference* to variable, who originates from a split of `v_base`, and whose original path in the tree is `path`. *) @@ -948,7 +952,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env let env, e = translate_expr env e in let branches = List.map (fun (binders, pat, e) -> let binders = List.map (fun (b: Ast.binder) -> - { MiniRust.name = b.node.name; typ = translate_type env b.typ; mut = false; ref = false } + { MiniRust.name = translate_binder_name b; typ = translate_type env b.typ; mut = false; ref = false } ) binders in let env = List.fold_left push env binders in let pat = translate_pat env pat in @@ -1236,7 +1240,7 @@ let translate_decl env (d: Ast.decl): MiniRust.decl option = | _ -> failwith "impossible" in let body, args = if parameters = [] then DeBruijn.subst Helpers.eunit 0 body, [] else body, args in - let parameters = List.map2 (fun typ a -> { MiniRust.mut = false; name = a.Ast.node.Ast.name; typ; ref = false }) parameters args in + let parameters = List.map2 (fun typ a -> { MiniRust.mut = false; name = translate_binder_name a; typ; ref = false }) parameters args in let env = List.fold_left push env parameters in let _, body = translate_expr_with_type env body return_type in let meta = translate_meta flags in diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml index f203548f..4fb9dbe8 100644 --- a/lib/OptimizeMiniRust.ml +++ b/lib/OptimizeMiniRust.ml @@ -146,13 +146,13 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr | Let (b, e1, e2) -> (* KPrint.bprintf "[infer-mut,let] %a\n" pexpr e; *) let a, e2 = open_ b e2 in - (* KPrint.bprintf "[infer-mut,let] opened %s[%s]\n" b.name (show_atom_t a); *) + KPrint.bprintf "[infer-mut,let] opened %s[%s]\n" b.name (show_atom_t a); let known, e2 = infer env expected known e2 in let mut_var = want_mut_var a known in let mut_borrow = want_mut_borrow a known in - (* KPrint.bprintf "[infer-mut,let-done-e2] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name + KPrint.bprintf "[infer-mut,let-done-e2] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name (show_atom_t a) - ptyp b.typ mut_var mut_borrow; *) + ptyp b.typ mut_var mut_borrow; let t1 = if mut_borrow then make_mut_borrow b.typ else b.typ in let known, e1 = infer env t1 known e1 in known, Let ({ b with mut = mut_var; typ = t1 }, e1, close a (Var 0) (lift 1 e2)) @@ -365,9 +365,9 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr in known. *) known, e - | Match (e, t, arms) as e_match -> + | Match (e_scrut, t, arms) as e_match -> (* We have the expected type of the scrutinee: recurse *) - let known, e = infer env t known e in + let known, e = infer env t known e_scrut in let known, arms = List.fold_left_map (fun known ((bs, _, _) as branch) -> let atoms, pat, e = open_branch branch in let known, e = infer env expected known e in @@ -428,13 +428,19 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr | OpenP open_var -> let { atom; _ } = open_var in let mut = VarSet.mem atom known.r in - let ref = match typ with Ref _ -> true | _ -> false in + let ref = match typ with Ref _ -> true | _ -> mut (* something mutated relying on an implicit conversion to ref *) in KPrint.bprintf "In match:\n%a\nPattern variable %s: mut=%b, ref=%b\n" pexpr e_match open_var.name mut ref; (* i., above *) let known = if mut then add_mut_field (Some t) f known else known in (* ii.b. *) - let known = match e with Open { atom; _ } when mut -> add_mut_var atom known | _ -> known in + let known = match e_scrut with + | Open { atom; _ } when mut -> add_mut_var atom known + | Deref (Open { atom; _ }) when mut -> add_mut_borrow atom known + | _ -> + KPrint.bprintf "%a is not open or deref\n" pexpr e; + known + in (* ii.a *) let known = if ref then { known with p = VarSet.add atom known.p } else known in known, (f, OpenP open_var) :: fieldpats @@ -454,7 +460,11 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr | _ -> Warn.failwith "TODO: Match %a" ppat pat in let known, pat = update_fields known pat t in - let bs = List.map2 (fun a b -> if VarSet.mem a known.p then { b with ref = true } else b) atoms bs in + let bs = List.map2 (fun a b -> + let ref = VarSet.mem a known.p in + let mut = VarSet.mem a known.r in + { b with ref; mut } + ) atoms bs in let branch = close_branch atoms (bs, pat, e) in known, branch ) known arms in diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml index 9b92ae84..84c5864e 100644 --- a/lib/PrintMiniRust.ml +++ b/lib/PrintMiniRust.ml @@ -225,6 +225,16 @@ let print_op = function | Constant.BNot -> string "!" | op -> print_op op +let rec is_ignored_pattern env = function + | Wildcard -> true + | VarP v -> + begin match lookup env v with + | Bound b -> b.name.[0] = '_' + | _ -> failwith "incorrect bound var in pattern" + end + | StructP (_, fields) -> List.for_all (fun (_, p) -> is_ignored_pattern env p) fields + | _ -> false + (* print a block *and* the expression within it *) let rec print_block_expression env e = braces_with_nesting (print_statements env e) @@ -479,10 +489,13 @@ and print_pat env (p: pat) = | Literal c -> print_constant c | Wildcard -> underscore | StructP (name, fields) -> + (* Not printing those ignored patterns makes a semantic difference! It prevents move-outs... *) + let ignored, fields = List.partition (fun (_, p) -> is_ignored_pattern env p) fields in + let trailing = if ignored <> [] then comma ^/^ dot ^^ dot else empty in print_name env name ^^ braces_with_nesting ( separate_map (comma ^^ break1) (fun (name, pat) -> group (group (string name ^^ colon) ^/^ group (print_pat env pat)) - ) fields + ) fields ^^ trailing ) | VarP v -> begin match lookup env v with