summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-05-05 17:46:50 +0200
committerSon Ho2022-05-05 17:46:50 +0200
commit3b34326732183dac2f1e397e649c2b8e1bb74af7 (patch)
tree88867e6774bdff1f47b8e14e399f659dad5ff7c1
parentbb94d52be2d0ddb317577dc3cd468754646e4b64 (diff)
Make minor fixes
-rw-r--r--src/Assumed.ml21
-rw-r--r--src/InterpreterPaths.ml5
-rw-r--r--src/TypesUtils.ml6
3 files changed, 28 insertions, 4 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml
index 2cd83db5..b3128b9b 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -92,6 +92,17 @@ module Sig = struct
output = mk_box_ty tvar_0 (* Box<T> *);
}
+ (** `fn<T>(Box<T>) -> ()` *)
+ let box_free_sig : A.fun_sig =
+ {
+ region_params = [];
+ num_early_bound_regions = 0;
+ regions_hierarchy = [];
+ type_params = [ type_param_0 ] (* <T> *);
+ inputs = [ mk_box_ty tvar_0 (* Box<T> *) ];
+ output = mk_unit_ty (* () *);
+ }
+
(** Helper for `Box::deref_shared` and `Box::deref_mut`.
Returns:
`fn<'a, T>(&'a (mut) Box<T>) -> &'a (mut) T`
@@ -248,6 +259,10 @@ let assumed_infos : assumed_info list =
[
(A.Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]);
(BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]);
+ ( BoxFree,
+ Sig.box_free_sig,
+ false,
+ to_name [ "alloc"; "boxed"; "Box"; "free" ] );
( BoxDeref,
Sig.box_deref_shared_sig,
false,
@@ -271,7 +286,11 @@ let assumed_infos : assumed_info list =
]
let get_assumed_info (id : A.assumed_fun_id) : assumed_info =
- List.find (fun (id', _, _, _) -> id = id') assumed_infos
+ match List.find_opt (fun (id', _, _, _) -> id = id') assumed_infos with
+ | Some info -> info
+ | None ->
+ raise
+ (Failure ("get_assumed_info: not found: " ^ A.show_assumed_fun_id id))
let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig =
let _, sg, _, _ = get_assumed_info id in
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 1fd504d2..52742703 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -711,9 +711,10 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
| V.Adt av ->
(* Sanity check *)
(match v.V.ty with
- | T.Adt (T.Assumed _, _, _) -> failwith "Can't copy an assumed value"
+ | T.Adt (T.Assumed (T.Box | Vec), _, _) ->
+ failwith "Can't copy an assumed value other than Option"
| T.Adt (T.AdtId _, _, _) -> assert allow_adt_copy
- | T.Adt (T.Tuple, _, _) -> () (* Ok *)
+ | T.Adt ((T.Assumed Option | T.Tuple), _, _) -> () (* Ok *)
| _ -> failwith "Unreachable");
let ctx, fields =
List.fold_left_map
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 58bb4803..bee7956e 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -172,10 +172,14 @@ let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : rty) : bool =
* "primitively copyable" means that copying instances of this type doesn't
* require calling dedicated functions defined through the Copy trait. It
* is the case for types like integers, shared borrows, etc.
+ *
+ * Generally, ADTs are not copyable. However, some of the primitive ADTs are
+ * like `Option`.
*)
let rec ty_is_primitively_copyable (ty : 'r ty) : bool =
match ty with
- | Adt ((AdtId _ | Assumed _), _, _) -> false
+ | Adt (Assumed Option, _, tys) -> List.for_all ty_is_primitively_copyable tys
+ | Adt ((AdtId _ | Assumed (Box | Vec)), _, _) -> false
| Adt (Tuple, _, tys) -> List.for_all ty_is_primitively_copyable tys
| TypeVar _ | Never | Str | Array _ | Slice _ -> false
| Bool | Char | Integer _ -> true