summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-03 19:51:58 +0100
committerSon Ho2022-01-03 19:51:58 +0100
commit191c1eec8d3da6c2559280e085f1dc0c80296a57 (patch)
treeace4d4f5d039c1dc142bb8bc9b970f4c281b67ff /src
parent0e241434a0a5c895fe43c8e9e54862f2ece09ab7 (diff)
Implement compute_expanded_symbolic_box_value
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml50
1 files changed, 35 insertions, 15 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 0352a80d..02d9aff5 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -49,6 +49,26 @@ let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var
let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
{ var_id; projection = [] }
+(** Deconstruct a type of the form `Box<T>` to retrieve the `T` inside *)
+let ty_get_box (box_ty : T.ety) : T.ety =
+ match box_ty with
+ | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> boxed_ty
+ | _ -> failwith "Not a boxed type"
+
+(** Deconstruct a type of the form `&T` or `&mut T` to retrieve the `T` (and
+ the borrow kind, etc.)
+ *)
+let ty_get_ref (ty : T.ety) : T.erased_region * T.ety * T.ref_kind =
+ match ty with
+ | T.Ref (r, ty, ref_kind) -> (r, ty, ref_kind)
+ | _ -> failwith "Not a ref type"
+
+(** Box a value *)
+let mk_box_value (v : V.typed_value) : V.typed_value =
+ let box_ty = T.Adt (T.Assumed T.Box, [], [ v.V.ty ]) in
+ let box_v = V.Adt { variant_id = None; field_values = [ v ] } in
+ mk_typed_value box_ty box_v
+
(** TODO: change the name *)
type eval_error = Panic
@@ -2662,6 +2682,19 @@ let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t)
let ty = T.Adt (T.Tuple, [], field_types) in
(ctx, { V.value = v; V.ty })
+let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t)
+ (boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+ (* Introduce a fresh symbolic value *)
+ let ctx, boxed_sv_id = C.fresh_symbolic_value_id ctx in
+ let boxed_sv = { V.sv_id = boxed_sv_id; V.sv_ty = boxed_ty } in
+ let boxed_sv = { V.svalue = boxed_sv; rset_ended = ended_regions } in
+ let boxed_value = V.Symbolic boxed_sv in
+ let boxed_value : V.typed_value =
+ { V.value = boxed_value; V.ty = Subst.erase_regions boxed_ty }
+ in
+ let box_value = mk_box_value boxed_value in
+ (ctx, box_value)
+
(** Expand a symbolic value.
Note that we return a list of contexts because when expanding enumerations
@@ -2695,7 +2728,8 @@ let expand_symbolic_value (config : C.config) (expand_enumerations : bool)
(* Borrows *)
| Deref, T.Ref (_, _, _) -> raise Unimplemented
(* Boxes *)
- | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> raise Unimplemented
+ | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
+ compute_expanded_symbolic_box_value sp.V.rset_ended boxed_ty ctx
| _ ->
failwith
("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
@@ -3554,20 +3588,6 @@ let eval_box_new (config : C.config) (region_params : T.erased_region list)
Ok ctx
| _ -> failwith "Inconsistent state"
-(** Deconstruct a type of the form `Box<T>` to retrieve the `T` inside *)
-let ty_get_box (box_ty : T.ety) : T.ety =
- match box_ty with
- | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> boxed_ty
- | _ -> failwith "Not a boxed type"
-
-(** Deconstruct a type of the form `&T` or `&mut T` to retrieve the `T` (and
- the borrow kind, etc.)
- *)
-let ty_get_ref (ty : T.ety) : T.erased_region * T.ety * T.ref_kind =
- match ty with
- | T.Ref (r, ty, ref_kind) -> (r, ty, ref_kind)
- | _ -> failwith "Not a ref type"
-
(** Auxiliary function which factorizes code to evaluate `std::Deref::deref`
and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *)
let eval_box_deref_mut_or_shared (config : C.config)