summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Identifiers.ml1
-rw-r--r--src/Interpreter.ml46
2 files changed, 45 insertions, 2 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 04f6c1b8..345ce058 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -18,6 +18,7 @@ module type Id = sig
(* TODO: this is stateful! - but we may want to be able to duplicate contexts... *)
val fresh : generator -> id * generator
+ (* TODO: change the order of the returned types *)
val to_string : id -> string
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 0e88be2d..8c2ebb63 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1422,7 +1422,7 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool)
(* The function to generate and register fresh reborrows *)
let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id =
if allow_reborrows then (
- let bid', cnt' = V.BorrowId.fresh ctx.borrow_counter in
+ let bid', cnt' = V.BorrowId.fresh !borrow_counter in
borrow_counter := cnt';
reborrows := (bid, bid') :: !reborrows;
bid')
@@ -3001,6 +3001,46 @@ 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_shared_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 =
+ (* First, replace the symbolic values. The important point is that the
+ * symbolic value to expand may appear several times, if it has been
+ * copied. In this case, we need to introduce one fresh borrow id per
+ * instance.
+ *)
+ let borrows = ref V.BorrowId.Set.empty in
+ let borrow_counter = ref ctx.C.borrow_counter in
+ let fresh_borrow () =
+ let bid', cnt' = V.BorrowId.fresh !borrow_counter in
+ borrow_counter := cnt';
+ borrows := V.BorrowId.Set.add bid' !borrows;
+ bid'
+ in
+ (* Visitor to replace the symbolic values *)
+ let obj =
+ object
+ inherit [_] C.map_eval_ctx as super
+
+ method! visit_Symbolic env sv =
+ if sv.V.svalue = original_sv then
+ let bid = fresh_borrow () in
+ V.Borrow (V.SharedBorrow bid)
+ else super#visit_Symbolic env sv
+ end
+ in
+ (* Call the visitor *)
+ let ctx = obj#visit_eval_ctx () ctx in
+ let ctx = { ctx with C.borrow_counter = !borrow_counter } in
+ (* Finally, replace the symbolic avalues *)
+ let bids = !borrows in
+ assert (not (V.BorrowId.Set.is_empty bids));
+ let ctx, shared_sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in
+ let see = SeSharedRef (bids, shared_sv) in
+ let allow_reborrows = true in
+ apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see ctx
+
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)
@@ -3026,7 +3066,9 @@ let expand_symbolic_value_borrow (config : C.config)
let allow_reborrows = true in
apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
ctx
- | T.Shared -> raise Unimplemented
+ | T.Shared ->
+ expand_symbolic_value_shared_borrow config original_sv ended_regions
+ region ref_ty rkind ctx
(** Expand a symbolic value which is not an enumeration with several variants.