summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml75
1 files changed, 51 insertions, 24 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index c871d530..0e88be2d 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2787,34 +2787,51 @@ let apply_symbolic_expansion_to_avalues (config : C.config)
let ctx = apply_expansion BorrowProj ctx in
ctx
-(** Apply a symbolic expansion to a context, by replacing the original
- symbolic value with its expanded value. Is valid only if the expansion
- is not a borrow (i.e., an adt...).
+(** Auxiliary function.
+
+ Simply replace the symbolic values (*not avalues*) in the context with
+ a given value. Will break invariants if not used properly.
*)
-let apply_symbolic_expansion_non_borrow (config : C.config)
- (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
- (ctx : C.eval_ctx) : C.eval_ctx =
- (* Convert the expansion to a value *)
- let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
- (* Visitor to apply the expansion to *non-abstraction* values *)
+let replace_symbolic_values (config : C.config) (at_most_once : bool)
+ (original_sv : V.symbolic_value) (nv : V.value) (ctx : C.eval_ctx) :
+ C.eval_ctx =
+ (* Count *)
+ let replaced = ref false in
+ let replace () =
+ if at_most_once then assert (not !replaced);
+ replaced := true;
+ nv
+ in
+ (* Visitor to apply the substitution *)
let obj =
object
inherit [_] C.map_eval_ctx as super
method! visit_Symbolic env spc =
- if spc.V.svalue = original_sv then nv.V.value
+ if spc.V.svalue = original_sv then replace ()
else super#visit_Symbolic env spc
- (** Replace a symbolic value with its expansion.
- Note that there may be several references to the same symbolic value
- in the context, if the value has been copied. Expansion is then a bit
- subtle in the case we expand shared borrows, in which case we need to
- introduce a unique borrow identifier for every borrow (this is not
- the case here: this function should NOT be used to expand borrows).
- *)
end
in
- (* Apply the expansion to non-abstraction values *)
+ (* Apply the substitution *)
let ctx = obj#visit_eval_ctx None ctx in
+ (* Check that we substituted *)
+ assert !replaced;
+ (* Return *)
+ ctx
+
+(** Apply a symbolic expansion to a context, by replacing the original
+ symbolic value with its expanded value. Is valid only if the expansion
+ is not a borrow (i.e., an adt...).
+*)
+let apply_symbolic_expansion_non_borrow (config : C.config)
+ (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
+ (ctx : C.eval_ctx) : C.eval_ctx =
+ (* Apply the expansion to non-abstraction values *)
+ let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
+ let at_most_once = false in
+ let ctx =
+ replace_symbolic_values config at_most_once original_sv nv.V.value ctx
+ in
(* Apply the expansion to abstraction values *)
let allow_reborrows = false in
apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
@@ -2984,7 +3001,8 @@ let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t)
let see = SeAdt (None, [ boxed_value ]) in
(ctx, see)
-let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
+let expand_symbolic_value_borrow (config : C.config)
+ (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t)
(region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind)
(ctx : C.eval_ctx) : C.eval_ctx =
(* Check that we are allowed to expand the reference *)
@@ -2996,7 +3014,18 @@ let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
* 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
+ let see = SeMutRef (bid, sv) in
+ (* Expand the symbolic values - we simply perform a substitution (and
+ * check that we perform exactly one substitution) *)
+ let nv = symbolic_expansion_to_value_with_borrows original_sv see in
+ let at_most_once = true in
+ let ctx =
+ replace_symbolic_values config at_most_once original_sv nv.V.value ctx
+ in
+ (* Expand the symbolic avalues *)
+ let allow_reborrows = true in
+ apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
+ ctx
| T.Shared -> raise Unimplemented
(** Expand a symbolic value which is not an enumeration with several variants.
@@ -3043,10 +3072,8 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
(* Borrows *)
| Deref, T.Ref (region, ref_ty, rkind) ->
- let _ =
- expand_symbolic_value_borrow ended_regions region ref_ty rkind ctx
- in
- raise Unimplemented
+ expand_symbolic_value_borrow config sp.V.svalue ended_regions region
+ ref_ty rkind ctx
| _ ->
failwith
("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)