Skip to content

Commit

Permalink
Merge branch 'master' into protz_hoist
Browse files Browse the repository at this point in the history
  • Loading branch information
@msprotz
msprotz authored Sep 9, 2024
2 parents 960b290 + 97ced77 commit 0894e0c
Show file tree
Hide file tree
Showing 3 changed files with 56 additions and 32 deletions.
34 changes: 19 additions & 15 deletions lib/AstToMiniRust.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -431,8 +431,8 @@ let rec translate_type_with_config (env: env) (config: config) (t: Ast.typ): Min
| TAny -> failwith "unexpected: [type] no casts in Low* -> Rust"
| TBuf (t, b) ->
if config.box then
(* MiniRust.box (Slice (translate_type_with_config env config t)) *)
Vec (translate_type_with_config env config t)
MiniRust.box (Slice (translate_type_with_config env config t))
(* Vec (translate_type_with_config env config t) *)
else
Ref (config.lifetime, borrow_kind_of_bool b, Slice (translate_type_with_config env config t))
| TArray (t, c) -> Array (translate_type_with_config env config t, int_of_string (snd c))
Expand Down Expand Up @@ -542,12 +542,6 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr
| Heap -> false
in

let optimize_size_one = function
| MiniRust.Repeat(e_init, Constant (_, "1")) -> MiniRust.VecNew (List [e_init])
| e_init ->
VecNew e_init
in

match init.node with
| EBufCreate (lifetime, e_init, len) ->
let t = translate_type env (Helpers.assert_tbuf_or_tarray init.typ) in
Expand All @@ -557,7 +551,7 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr
if to_array lifetime && H.is_const len then
env, Array e_init, Array (t, H.assert_const len)
else
env, optimize_size_one e_init, Vec t
MiniRust.(env, box_new e_init, box (Slice t))
| EBufCreateL (lifetime, es) ->
let t = translate_type env (Helpers.assert_tbuf_or_tarray init.typ) in
let l = List.length es in
Expand All @@ -566,21 +560,24 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr
if to_array lifetime then
env, Array e_init, Array (t, l)
else
env, optimize_size_one e_init, Vec t
MiniRust.(env, box_new e_init, box (Slice t))
| _ ->
Warn.fatal_error "unexpected: non-bufcreate expression, got %a" PrintAst.Ops.pexpr init

(* 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; *)

let erase_lifetime_info = (object(self)
inherit [_] MiniRust.DeBruijn.map
method! visit_Ref env _ bk t = Ref (None, bk, self#visit_typ env t)
method! visit_tname _ n _ = Name (n, [])
end)#visit_typ ()
in

(* KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e; *)
(* Possibly convert expression x, known to have type t (per Rust), into
expected type t_ret (captured variable). *)
let possibly_convert (x: MiniRust.expr) t: MiniRust.expr =
(* KPrint.bprintf "possibly_convert: %a: %a <: %a\n" *)
(* PrintMiniRust.pexpr x *)
Expand All @@ -598,20 +595,26 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
(* The type annotations coming from Ast do not feature polymorphic binders in types, but we
do retain them in our Function type -- so we need to relax the comparison here *)
x

(* More conversions due to box-ing types. *)
| _, App (Name (["Box"], _), [Slice _]), Ref (_, k, Slice _) ->
Borrow (k, Deref x)
Borrow (k, x)
| _, Ref (_, _, Slice _), App (Name (["Box"], _), [Slice _]) ->
(* COPY *)
MethodCall (Borrow (Shared, Deref x), ["into"], [])
(* | _, Ref (_, Shared, Slice _), App (Name (["Box"], _), [Slice _]) -> *)
(* MethodCall (x, ["into"], []) *)
| _, Vec _, App (Name (["Box"], _), [Slice _]) ->
(* DEAD CODE -- no method try_into on Vec *)
MethodCall (MethodCall (x, ["try_into"], []), ["unwrap"], [])
| _, Array _, App (Name (["Box"], _), [Slice _]) ->
(* COPY *)
Call (Name ["Box"; "new"], [], [x])

(* More conversions due to vec-ing types *)
| _, Ref (_, _, Slice _), Vec _ ->
(* COPY *)
MethodCall (x, ["to_vec"], [])
| _, Array _, Vec _ ->
(* COPY *)
Call (Name ["Vec"; "from"], [], [x])

| _, Name (n, _), Name (n', _) when n = n' ->
Expand Down Expand Up @@ -910,6 +913,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
[ "copy_from_slice" ],
[ Borrow (Shared, Index (src, H.range_with_len src_index len)) ])
| EBufFill (dst, elt, len) ->
(* let t = translate_type env elt.typ in *)
let env, dst = translate_expr env dst in
let env, elt = translate_expr env elt in
let env, len = translate_expr_with_type env len (Constant SizeT) in
Expand All @@ -922,7 +926,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
env, MethodCall (
Index (dst, H.range_with_len (Constant (SizeT, "0")) len),
[ "copy_from_slice" ],
[ Borrow (Shared, VecNew (Repeat (elt, len))) ])
[ Borrow (Shared, MiniRust.(box_new (Repeat (elt, len)))) ])
| EBufFree _ ->
(* Rather than error out, we do nothing, as some functions may allocate then free. *)
env, Unit
Expand Down
15 changes: 15 additions & 0 deletions lib/MiniRust.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ and generic_param =
and lifetime =
| Label of string

(* Smart constructors *)
let box t =
App (Name (["Box"], []), [t])

Expand Down Expand Up @@ -125,6 +126,20 @@ and open_var = {

and atom_t = Atom.t [@ visitors.opaque]

(* Smart constructors *)
let box_new (e: array_expr) =
let optimize_size_one = function
| Repeat(e_init, Constant (_, "1")) ->
VecNew (List [e_init])
| e_init ->
VecNew e_init
in
MethodCall (optimize_size_one e, ["into_boxed_slice"], [])

(* e[..] *)
let slice_of_array e =
Index (Array e, Range (None, None, false))

type visibility = Pub | PubCrate

type meta = {
Expand Down
39 changes: 22 additions & 17 deletions lib/OptimizeMiniRust.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@
*)

open MiniRust
open PrintMiniRust

module NameMap = Map.Make(Name)
module VarSet = Set.Make(Atom)
Expand Down Expand Up @@ -90,6 +91,7 @@ let retrieve_pair_type = function
| _ -> failwith "impossible: retrieve_pair_type"

let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr =
KPrint.bprintf "[infer] %a @ %a\n" pexpr e ptyp expected;
match e with
| Borrow (k, e) ->
(* If we expect this borrow to be a mutable borrow, then we make it a mutable borrow
Expand Down Expand Up @@ -117,7 +119,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
add_mut_borrow atom known, Borrow (Mut, e)

| _ ->
KPrint.bprintf "[infer-mut, borrow] borrwing %a is not supported\n" PrintMiniRust.pexpr e;
KPrint.bprintf "[infer-mut, borrow] borrwing %a is not supported\n" pexpr e;
failwith "TODO: borrowing something other than a variable"
else
let known, e = infer env (assert_borrow expected) known e in
Expand All @@ -132,15 +134,15 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
known, e

| Let (b, e1, e2) ->
(* KPrint.bprintf "[infer-mut,let] %a\n" PrintMiniRust.pexpr e; *)
(* 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); *)
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
(show_atom_t a)
PrintMiniRust.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))
Expand All @@ -163,6 +165,9 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
argument. *)
let known, e = infer env (KList.one targs) known (KList.one es) in
known, Call (Name n, targs, [ e ])
else if n = ["Box"; "new"] then
let known, e = infer env (KList.one targs) known (KList.one es) in
known, Call (Name n, targs, [ e ])
else if n = [ "lib"; "memzero0"; "memzero" ] then (
(* Same as ignore above *)
assert (List.length es = 2);
Expand All @@ -183,7 +188,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
| Eq | Neq | Lt | Lte | Gt | Gte
| And | Or | Xor | Not -> known, e
| _ ->
KPrint.bprintf "[infer-mut,call] %a not supported\n" PrintMiniRust.pexpr e;
KPrint.bprintf "[infer-mut,call] %a not supported\n" pexpr e;
failwith "TODO: operator not supported"
end

Expand All @@ -192,7 +197,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr

(* atom = e3 *)
| Assign (Open { atom; _ }, e3, t) ->
(* KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e; *)
(* KPrint.bprintf "[infer-mut,assign] %a\n" pexpr e; *)
let known, e3 = infer env t known e3 in
add_mut_var atom known, e3

Expand All @@ -209,7 +214,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
| Assign (Index (Field (Open {atom;_}, "0", None) as e1, e2), e3, t)
(* atom.1[e2] = e3 *)
| Assign (Index (Field (Open {atom;_}, "1", None) as e1, e2), e3, t) ->
(* KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e; *)
(* KPrint.bprintf "[infer-mut,assign] %a\n" pexpr e; *)
let known = add_mut_borrow atom known in
let known, e2 = infer env usize known e2 in
let known, e3 = infer env t known e3 in
Expand All @@ -224,7 +229,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr

(* (&atom)[e2] = e3 *)
| Assign (Index (Borrow (_, (Open { atom; _ } as e1)), e2), e3, t) ->
(* KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e; *)
(* KPrint.bprintf "[infer-mut,assign] %a\n" pexpr e; *)
let known = add_mut_var atom known in
let known, e2 = infer env usize known e2 in
let known, e3 = infer env t known e3 in
Expand Down Expand Up @@ -257,7 +262,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
known, Assign (Index (Borrow (Mut, Index (Borrow (Mut, e1), e2)), e3), e4, t)

| Assign _ ->
KPrint.bprintf "[infer-mut,assign] %a unsupported\n" PrintMiniRust.pexpr e;
KPrint.bprintf "[infer-mut,assign] %a unsupported\n" pexpr e;
failwith "TODO: unknown assignment"

| AssignOp _ -> failwith "AssignOp nodes should only be introduced after mutability inference"
Expand Down Expand Up @@ -304,10 +309,10 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
AST node to indicate e.g. that the destination of `copy_from_slice` ought to be mutable, or
we just bake that knowledge in right here. *)
begin match m with
| [ "wrapping_add" ] | [ "wrapping_div" ] | [ "wrapping_mul" ]
| [ "wrapping_neg" ] | [ "wrapping_rem" ] | [ "wrapping_shl" ]
| [ "wrapping_shr" ] | [ "wrapping_sub" ]
| [ "to_vec" ] ->
| [ "wrapping_add" | "wrapping_div" | "wrapping_mul"
| "wrapping_neg" | "wrapping_rem" | "wrapping_shl"
| "wrapping_shr" | "wrapping_sub"
| "to_vec" | "into_boxed_slice" | "into" ] ->
known, MethodCall (e1, m, e2)
| ["split_at"] ->
assert (List.length e2 = 1);
Expand Down Expand Up @@ -335,7 +340,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
| _ -> failwith "TODO: push on complex expressions"
end
| _ ->
KPrint.bprintf "%a unsupported\n" PrintMiniRust.pexpr e;
KPrint.bprintf "%a unsupported\n" pexpr e;
failwith "TODO: MethodCall"
end

Expand Down Expand Up @@ -741,22 +746,22 @@ let infer_mut_borrows files =
match decl with
| Function ({ name; body; return_type; parameters; _ } as f) ->
(* KPrint.bprintf "[infer-mut] visiting %s\n%a\n" (String.concat "." name)
PrintMiniRust.pdecl decl; *)
pdecl decl; *)
let atoms, body =
List.fold_right (fun binder (atoms, e) ->
let a, e = open_ binder e in
(* KPrint.bprintf "[infer-mut] opened %s[%s]\n%a\n" binder.name (show_atom_t a) PrintMiniRust.pexpr e; *)
(* KPrint.bprintf "[infer-mut] opened %s[%s]\n%a\n" binder.name (show_atom_t a) pexpr e; *)
a :: atoms, e
) parameters ([], body)
in
(* KPrint.bprintf "[infer-mut] done opening %s\n%a\n" (String.concat "." name)
PrintMiniRust.pexpr body; *)
pexpr body; *)
(* Start the analysis with the current state of struct mutability *)
let known, body = infer env return_type {known with structs = env.structs} body in
let parameters, body =
List.fold_left2 (fun (parameters, e) (binder: binding) atom ->
let e = close atom (Var 0) (lift 1 e) in
(* KPrint.bprintf "[infer-mut] closed %s[%s]\n%a\n" binder.name (show_atom_t atom) PrintMiniRust.pexpr e; *)
(* KPrint.bprintf "[infer-mut] closed %s[%s]\n%a\n" binder.name (show_atom_t atom) pexpr e; *)
let mut = want_mut_var atom known in
let typ = if want_mut_borrow atom known then make_mut_borrow binder.typ else binder.typ in
{ binder with mut; typ } :: parameters, e
Expand Down

0 comments on commit 0894e0c

Please sign in to comment.