Propagate changes to EBufSub

FStarLang · Dec 11, 2023 · adf14e6 · adf14e6
1 parent fab3b03
commit adf14e6
Show file tree

Hide file tree

Showing 11 changed files with 37 additions and 23 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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))