Skip to content

Commit

Permalink
A special-case support for contained types that need to be wrapper in…
Browse files Browse the repository at this point in the history
… an outer container that outlives the containee
  • Loading branch information
msprotz committed Oct 30, 2024
1 parent e1441f8 commit ce37b9b
Show file tree
Hide file tree
Showing 5 changed files with 21 additions and 5 deletions.
15 changes: 14 additions & 1 deletion lib/AstToMiniRust.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1254,6 +1254,9 @@ let compute_derives heap_structs pointer_holding_structs files =

F.lfp equations

let is_contained t =
let t = KList.last t in
List.exists (fun t' -> KString.starts_with t t') !Options.contained

(* In Rust, like in C, all the declarations from the current module are in
* scope immediately. This requires us to duplicate a little bit of work. *)
Expand All @@ -1278,7 +1281,11 @@ let bind_decl env trait_valuation (d: Ast.decl): env =
let config = { default_config with lifetime } in

let parameters = List.map (fun (b: Ast.binder) ->
translate_type_with_config env config b.typ
match translate_type_with_config env config b.typ with
| Ref (_, m, (Slice (Name (t, _ :: _)) as slice_t)) when is_contained t ->
MiniRust.Ref (Some (Label "b"), m, slice_t)
| t ->
t
) args in
let is_likely_heap_allocation =
KString.exists (snd lid) "new" ||
Expand Down Expand Up @@ -1416,6 +1423,12 @@ let translate_decl env (d: Ast.decl): MiniRust.decl option =
| name, Function (_, parameters, return_type) -> name, parameters, return_type
| _ -> failwith "impossible"
in
let generic_params =
if List.exists (function MiniRust.Ref (l, _, _) when l <> lifetime -> true | _ -> false) parameters then
MiniRust.Lifetime (Label "b") :: generic_params
else
generic_params
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 env = List.fold_left push env parameters in
Expand Down
4 changes: 2 additions & 2 deletions lib/MiniRust.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(* A minimalistic representation of Rust *)

module Name = struct
type t = string list
type t = string list [@@ deriving show ]
let compare = compare
end

Expand All @@ -12,7 +12,7 @@ type borrow_kind = borrow_kind_ [@ opaque ]
and constant = Constant.t [@ opaque ]
and width = Constant.width [@ opaque ]
and op = Constant.op [@ opaque ]
and name = Name.t [@ opaque ]
and name = Name.t [@ visitors.opaque ]

(* Some design choices.
- We don't intend to perform any deep semantic transformations on this Rust
Expand Down
4 changes: 2 additions & 2 deletions lib/OptimizeMiniRust.ml
Original file line number Diff line number Diff line change
Expand Up @@ -498,7 +498,7 @@ let rec infer_expr (env: env) valuation (expected: typ) (known: known) (e: expr)
the struct type (provided by the context t) needs to be mutable --
this is the same as when we see x.f[0] = 1 -- field f needs to be
mutable (but not x!)
ii. if the pattern contains f = x *and* x is a borrow, then this is
ii. if the pattern contains f = x *and* x is a /mutable/ borrow, then this is
going to be a move-out -- this is not the same behavior as a
let-binding. Since borrows do not implement Copy, we need to do
some extra work. Consider this example:
Expand Down Expand Up @@ -547,7 +547,7 @@ let rec infer_expr (env: env) valuation (expected: typ) (known: known) (e: expr)
let { atom; _ } = open_var in
let mut = VarSet.mem atom known.r in
let ref = match typ with
| App (Name (["Box"], []), [_]) | Vec _ | Ref _ ->
| App (Name (["Box"], []), [_]) | Vec _ | Ref (_, Mut, _) ->
true (* prevent a move-out, again *)
| _ ->
mut (* something mutated relying on an implicit conversion to ref *)
Expand Down
1 change: 1 addition & 0 deletions lib/Options.ml
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ let backend = ref C
let wasm () = !backend = Wasm
let rust () = !backend = Rust
let no_box = ref false
let contained: string list ref = ref []

let static_header: Bundle.pat list ref = ref []
let minimal = ref false
Expand Down
2 changes: 2 additions & 0 deletions src/Karamel.ml
Original file line number Diff line number Diff line change
Expand Up @@ -288,6 +288,8 @@ Supported options:|}
"-by-ref", Arg.String (fun s -> prepend Options.by_ref (Parsers.lid s)), " \
pass the given struct type by reference, always";
"-fno-box", Arg.Set Options.no_box, " don't generate Box (Rust only)";
"-fcontained-type", Arg.String (fun s -> Options.contained := s :: !Options.contained), " \
type passed by reference with a different lifetime";
"-fbuiltin-uint128", Arg.Set Options.builtin_uint128, " target compiler \
supports arithmetic operators for uint128 -- this is NON PORTABLE, \
works only with GCC/Clang";
Expand Down

0 comments on commit ce37b9b

Please sign in to comment.