diff options
| -rw-r--r-- | src/Assumed.ml | 21 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 5 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 6 |
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 |