From adf14e6544383f4fe9f3cd56a785ad279b5dbdad Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 11 Dec 2023 09:59:53 +0100 Subject: [PATCH] Propagate changes to EBufSub --- lib/AstToCFlat.ml | 2 +- lib/AstToCStar.ml | 2 +- lib/AstToMiniRust.ml | 6 ++++-- lib/Builtin.ml | 4 ++-- lib/Checker.ml | 8 +++++--- lib/DataTypes.ml | 4 ++-- lib/InputAst.ml | 4 ++-- lib/InputAstToAst.ml | 4 ++-- lib/Simplify.ml | 13 +++++++++---- lib/SimplifyMerge.ml | 9 +++++++-- lib/Structs.ml | 4 ++-- 11 files changed, 37 insertions(+), 23 deletions(-) diff --git a/lib/AstToCFlat.ml b/lib/AstToCFlat.ml index 40fc613ca..8350afbe0 100644 --- a/lib/AstToCFlat.ml +++ b/lib/AstToCFlat.ml @@ -805,7 +805,7 @@ and mk_expr (env: env) (locals: locals) (e: expr): locals * CF.expr = locals, mk_add32 e1 (mk_uint32 ofs) | EAddrOf ({ node = EBufRead (e1, e2); _ }) - | EBufSub (e1, e2) -> + | EBufSub (e1, e2, _) -> let mult, base_size = cell_size env (assert_buf e.typ) in let locals, e1 = mk_expr env locals e1 in let locals, e2 = mk_expr env locals e2 in diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml index 4c55cf04e..b9a4c4e4d 100644 --- a/lib/AstToCStar.ml +++ b/lib/AstToCStar.ml @@ -387,7 +387,7 @@ and mk_expr env in_stmt e = CStar.BufCreateL (l, List.map (mk_expr env) es) | EBufRead (e1, e2) -> CStar.BufRead (mk_expr env e1, mk_expr env e2) - | EBufSub (e1, e2) -> + | EBufSub (e1, e2, _) -> CStar.BufSub (mk_expr env e1, mk_expr env e2) | EBufDiff (e1, e2) -> CStar.Call (CStar.Op K.Sub, [mk_expr env e1; mk_expr env e2]) diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index eb8f30dd1..08119117b 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -576,7 +576,8 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): Min | EPolyComp _ -> failwith "unexpected: EPolyComp" - | ELet (b, ({ node = EBufSub ({ node = EBound v_base; _ } as e_base, e_ofs); _ } as e1), e2) -> + | ELet (b, ({ node = EBufSub ({ node = EBound v_base; _ } as e_base, e_ofs, _); _ } as e1), e2) -> + (* TODO (AF): Do not ignore the length of the slice *) if Options.debug "rs-splits" then begin KPrint.bprintf "Translating: let %a = %a\n" PrintAst.Ops.pbind b PrintAst.Ops.pexpr e1; debug env @@ -664,10 +665,11 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): Min let e2 = translate_expr_with_type env e2 (Constant SizeT) in let e3 = translate_expr env e3 in Assign (Index (e1, e2), e3) - | EBufSub (e1, e2) -> + | EBufSub (e1, e2, _) -> (* This is a fallback for the analysis above. Happens if, for instance, the pointer arithmetic appears in subexpression position (like, function call), in which case there's a chance this might still work! *) + (* TODO (AF): Handle the length of the slice *) let e1 = translate_expr env e1 in let e2 = translate_expr_with_type env e2 (Constant SizeT) in Borrow (Mut, Index (e1, Range (Some e2, None, false))) diff --git a/lib/Builtin.ml b/lib/Builtin.ml index 151b31143..e4c356f1f 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -270,7 +270,7 @@ let lowstar_endianness: file = 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), - [ with_type buf8 (EBufSub (with_type buf8 (EBound 2), with_type int32 (EBound 1))); + [ with_type buf8 (EBufSub (with_type buf8 (EBound 2), with_type int32 (EBound 1), None)); with_type t (EBound 0) ]))); ] @@ -287,7 +287,7 @@ let lowstar_endianness: file = load_i_lid, [ fresh_binder "b" buf8; fresh_binder "i" int32 ], with_type t (EApp (with_type load_t (EQualified load_lid), - [ with_type buf8 (EBufSub (with_type buf8 (EBound 1), with_type int32 (EBound 0)))]))); + [ with_type buf8 (EBufSub (with_type buf8 (EBound 1), with_type int32 (EBound 0), None))]))); ] in let mk_conv s t = [ diff --git a/lib/Checker.ml b/lib/Checker.ml index f357a5617..73c32f0c9 100644 --- a/lib/Checker.ml +++ b/lib/Checker.ml @@ -360,9 +360,10 @@ and check' env t e = check_mut env "write" c1; c TUnit - | EBufSub (e1, e2) -> + | EBufSub (e1, e2, oe3) -> check_array_index env e2; - check_buffer env t e1 + check_buffer env t e1; + (match oe3 with | None -> () | Some e3 -> check_array_index env e3) | EBufDiff (e1, e2) -> let t1 = infer env e1 in @@ -626,8 +627,9 @@ and infer' env e = check env t1 e3; TUnit - | EBufSub (e1, e2) -> + | EBufSub (e1, e2, oe3) -> check_array_index env e2; + (match oe3 with | None -> () | Some e3 -> check_array_index env e3); let t1, c = infer_buffer env e1 in TBuf (t1, c) diff --git a/lib/DataTypes.ml b/lib/DataTypes.ml index 337d45786..59c51b71f 100644 --- a/lib/DataTypes.ml +++ b/lib/DataTypes.ml @@ -594,12 +594,12 @@ let remove_unit_buffers = object (self) | _ -> super#visit_EBufWrite env e1 e2 e3 - method! visit_EBufSub env e1 e2 = + method! visit_EBufSub env e1 e2 e3 = match e1.typ with | TBuf ((TUnit (* | TAny *)), _) -> EUnit | _ -> - super#visit_EBufSub env e1 e2 + super#visit_EBufSub env e1 e2 e3 method! visit_EBufDiff env e1 e2 = match e1.typ with diff --git a/lib/InputAst.ml b/lib/InputAst.ml index 8c91297fd..1edf529c4 100644 --- a/lib/InputAst.ml +++ b/lib/InputAst.ml @@ -68,8 +68,8 @@ and expr = (** e1[e2] *) | EBufWrite of (expr * expr * expr) (** e1[e2] <- e3 *) - | EBufSub of (expr * expr) - (** e1 + e2 *) + | EBufSub of (expr * expr * expr option) + (** e1 + e2, e3 optional length of the slice*) | EBufBlit of (expr * expr * expr * expr * expr) (** e1, index; e2, index; len *) | EMatch of (expr * branches) diff --git a/lib/InputAstToAst.ml b/lib/InputAstToAst.ml index 2a7400d5b..8dd0315b3 100644 --- a/lib/InputAstToAst.ml +++ b/lib/InputAstToAst.ml @@ -183,8 +183,8 @@ and mk_expr = function mk (EBufWrite (mk_expr e1, mk_expr e2, mk_expr e3)) | I.EBufFill (e1, e2, e3) -> mk (EBufFill (mk_expr e1, mk_expr e2, mk_expr e3)) - | I.EBufSub (e1, e2) -> - mk (EBufSub (mk_expr e1, mk_expr e2)) + | I.EBufSub (e1, e2, oe3) -> + mk (EBufSub (mk_expr e1, mk_expr e2, Option.map mk_expr oe3)) | I.EBufDiff (e1, e2) -> mk (EBufDiff (mk_expr e1, mk_expr e2)) | I.EBufBlit (e1, e2, e3, e4, e5) -> diff --git a/lib/Simplify.ml b/lib/Simplify.ml index f6b0ba7bf..2e568d0f8 100644 --- a/lib/Simplify.ml +++ b/lib/Simplify.ml @@ -817,14 +817,14 @@ let misc_cosmetic = object (self) | _ -> EBufWrite (e1, e2, e3) - method! visit_EBufSub env e1 e2 = + method! visit_EBufSub env e1 e2 e3 = (* AstToCStar emits BufSub (e, 0) as just e, so we need the value * check to be in agreement on both sides. *) match e2.node with | EConstant (_, "0") when not (Options.rust ()) -> (self#visit_expr env e1).node | _ -> - EBufSub (self#visit_expr env e1, self#visit_expr env e2) + EBufSub (self#visit_expr env e1, self#visit_expr env e2, Option.map (self#visit_expr env) e3) (* renumber uu's to have a stable numbering scheme that minimizes the diff * from one code generation to another *) @@ -1205,10 +1205,15 @@ and hoist_expr loc pos e = let b = { b with node = { b.node with meta = Some MetaSequence }} in lhs @ [ b, mk (EBufFree e) ], mk EUnit - | EBufSub (e1, e2) -> + | EBufSub (e1, e2, oe3) -> let lhs1, e1 = hoist_expr loc Unspecified e1 in let lhs2, e2 = hoist_expr loc Unspecified e2 in - lhs1 @ lhs2, mk (EBufSub (e1, e2)) + (match oe3 with + | None -> lhs1 @ lhs2, mk (EBufSub (e1, e2, None)) + | Some e3 -> + let lhs3, e3 = hoist_expr loc Unspecified e3 in + lhs1 @ lhs2 @ lhs3, mk (EBufSub (e1, e2, Some e3)) + ) | EBufDiff (e1, e2) -> let lhs1, e1 = hoist_expr loc Unspecified e1 in diff --git a/lib/SimplifyMerge.ml b/lib/SimplifyMerge.ml index 3b49d8292..e78ef8172 100644 --- a/lib/SimplifyMerge.ml +++ b/lib/SimplifyMerge.ml @@ -230,10 +230,15 @@ let rec merge' (env: env) (u: S.t) (e: expr): S.t * S.t * expr = let d3, u, e3 = merge env u e3 in S.inter (S.inter d1 d2) d3, u, w (EBufWrite (e1, e2, e3)) - | EBufSub (e1, e2) -> + | EBufSub (e1, e2, oe3) -> let d1, u, e1 = merge env u e1 in let d2, u, e2 = merge env u e2 in - S.inter d1 d2, u, w (EBufSub (e1, e2)) + (match oe3 with + | None -> S.inter d1 d2, u, w (EBufSub (e1, e2, None)) + | Some e3 -> + let d3, u, e2 = merge env u e3 in + S.inter (S.inter d1 d2) d3, u, w (EBufSub (e1, e2, Some e3)) + ) | EBufDiff (e1, e2) -> let d1, u, e1 = merge env u e1 in diff --git a/lib/Structs.ml b/lib/Structs.ml index 4b0936ffa..87be51f59 100644 --- a/lib/Structs.ml +++ b/lib/Structs.ml @@ -684,8 +684,8 @@ let to_addr is_struct = | EAddrOf e -> w (EAddrOf (to_addr false e)) - | EBufSub (e1, e2) -> - w (EBufSub (e1, e2)) + | EBufSub (e1, e2, oe3) -> + w (EBufSub (e1, e2, oe3)) | EBufDiff (e1, e2) -> w (EBufDiff (e1, e2))