diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index bd0ca184..79a06384 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -70,7 +70,7 @@ let mk_box_value (v : V.typed_value) : V.typed_value = mk_typed_value box_ty box_v (** Create a fresh symbolic value (as a complementary projector) *) -let mk_fresh_symbolic_comp_proj (ended_regions : T.RegionId.set_t) (ty : T.rty) +let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = let ctx, sv_id = C.fresh_symbolic_value_id ctx in let svalue = { V.sv_id; V.sv_ty = ty } in @@ -2697,7 +2697,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) let ctx, field_values = List.fold_left_map (fun ctx (ty : T.rty) -> - mk_fresh_symbolic_comp_proj ended_regions ty ctx) + mk_fresh_symbolic_proj_comp ended_regions ty ctx) ctx field_types in let av = V.Adt { variant_id; field_values } in @@ -2713,7 +2713,7 @@ let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t) (* Generate the field values *) let ctx, fields = List.fold_left_map - (fun ctx sv_ty -> mk_fresh_symbolic_comp_proj ended_regions sv_ty ctx) + (fun ctx sv_ty -> mk_fresh_symbolic_proj_comp ended_regions sv_ty ctx) ctx field_types in let v = V.Adt { variant_id = None; field_values = fields } in @@ -2725,15 +2725,25 @@ 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_value = - mk_fresh_symbolic_comp_proj ended_regions boxed_ty ctx + mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx in let box_value = mk_box_value boxed_value in (ctx, box_value) let compute_expanded_symbolic_ref_value (ended_regions : T.RegionId.set_t) - (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) : - C.eval_ctx * V.typed_value = - raise Unimplemented + (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) + (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + (* Check that we are allowed to expand the reference *) + assert (not (region_in_set region ended_regions)); + (* Match on the reference kind *) + match rkind with + | T.Mut -> + (* Simple case: simply create a fresh symbolic value and a fresh + * borrow id *) + let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in + let ctx, bid = C.fresh_borrow_id ctx in + raise Unimplemented + | T.Shared -> raise Unimplemented (** Expand a symbolic value which is not an enumeration with several variants. @@ -2768,6 +2778,7 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem) (* Borrows *) | Deref, T.Ref (region, ref_ty, rkind) -> compute_expanded_symbolic_ref_value ended_regions region ref_ty rkind + ctx (* Boxes *) | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> compute_expanded_symbolic_box_value ended_regions boxed_ty ctx |