summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml79
1 files changed, 57 insertions, 22 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 9faf8506..9c806e8f 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1015,6 +1015,20 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
in
{ V.value; V.ty }
+(** Convert a symbolic expansion to a value.
+
+ If the expansion is a reference expansion, it converts it to a borrow.
+ This function is meant to be used when reducing projectors over borrows,
+ during a symbolic expansion.
+ *)
+let symbolic_expansion_to_value_with_borrows (sv : V.symbolic_value)
+ (see : symbolic_expansion) : V.typed_value =
+ match see with
+ | SeMutRef (_, _) -> raise Unimplemented
+ | SeSharedRef (_, _) ->
+ raise Unimplemented failwith "Unexpected symbolic borrow expansion"
+ | _ -> symbolic_expansion_non_borrow_to_value sv see
+
(** Apply (and reduce) a projector over loans to a value.
TODO: detailed comments. See [apply_proj_borrows]
@@ -2852,19 +2866,23 @@ let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
type proj_kind = LoanProj | BorrowProj
(** Auxiliary function.
- Apply a symbolic expansion to avalues in a context.
+ Apply a symbolic expansion to avalues in a context, targetting a specific
+ kind of projectors.
[proj_kind] controls whether we apply the expansion to projectors
- on loans or projectors on borrows (when applying a symbolic expansion to
- a borrow value, we need two different expansion values: one for the loans
- and another for the borrows meaning we have to call this function twice
- with different parameters for [expansion]). For instance, if we expand
- a symbolic mutable ref to `s0`, we'll have to apply the loan projectors
- on a loan `mut_loan l` and the borrow projectors to a borrow `mut_borrow l s1`.
+ on loans or projectors on borrows.
+
+ When dealing with reference expansion, it is necessary to first apply the
+ expansion on loan projectors, then on borrow projectors. The reason is
+ that reducing the borrow projectors might require to perform some reborrows,
+ in which case we need to lookup the corresponding loans in the context.
+
+ [allow_reborrows] controls whether we allow reborrows or not. It is useful
+ only if we target borrow projectors.
*)
-let apply_symbolic_expansion_to_avalues (config : C.config)
+let apply_symbolic_expansion_to_target_avalues (config : C.config)
(allow_reborrows : bool) (proj_kind : proj_kind)
- (original_sv : V.symbolic_value) (expansion : V.typed_value)
+ (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
(ctx : C.eval_ctx) : C.eval_ctx =
(* Symbolic values contained in the expansion might contain already ended regions *)
let check_symbolic_no_ended = false in
@@ -2892,8 +2910,8 @@ let apply_symbolic_expansion_to_avalues (config : C.config)
if sv = original_sv then
(* Apply the projector *)
let projected_value =
- apply_proj_loans check_symbolic_no_ended ctx proj_regions
- expansion
+ apply_proj_loans_on_symbolic_expansion ctx proj_regions
+ expansion sv.V.sv_ty
in
(* Replace *)
projected_value.V.value
@@ -2903,6 +2921,12 @@ let apply_symbolic_expansion_to_avalues (config : C.config)
| V.AProjBorrows (sv, proj_ty), BorrowProj ->
(* Check if this is the symbolic value we are looking for *)
if sv = original_sv then
+ (* Convert the symbolic expansion to a value on which we can
+ * apply a projector (if the expansion is a reference expansion,
+ * convert it to a borrow) *)
+ let expansion =
+ symbolic_expansion_to_value_with_borrows original_sv expansion
+ in
(* Apply the projector *)
let projected_value =
apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
@@ -2923,6 +2947,21 @@ let apply_symbolic_expansion_to_avalues (config : C.config)
(* Apply the reborrows *)
apply_registered_reborrows ctx
+(** Auxiliary function.
+ Apply a symbolic expansion to avalues in a context.
+*)
+let apply_symbolic_expansion_to_avalues (config : C.config)
+ (allow_reborrows : bool) (original_sv : V.symbolic_value)
+ (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx =
+ let apply_expansion proj_kind ctx =
+ apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
+ original_sv expansion ctx
+ in
+ (* First target the loan projectors, then the borrow projectors *)
+ let ctx = apply_expansion LoanProj ctx in
+ 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...).
@@ -2930,13 +2969,15 @@ let apply_symbolic_expansion_to_avalues (config : C.config)
let apply_symbolic_expansion_non_borrow (config : C.config)
(original_sv : V.symbolic_value) (expansion : symbolic_expansion)
(ctx : C.eval_ctx) : C.eval_ctx =
- (* Visitor to apply the expansion to non-abstraction values *)
+ (* 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 obj =
object
inherit [_] C.map_eval_ctx as super
method! visit_Symbolic env spc =
- if spc.V.svalue = original_sv then expansion.V.value
+ if spc.V.svalue = original_sv then nv.V.value
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
@@ -2949,16 +2990,10 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
in
(* Apply the expansion to non-abstraction values *)
let ctx = obj#visit_eval_ctx None ctx in
- (* Apply the expansion to abstraction values, on loans then on borrows (the
- * order is arbitrary: we just can't do both at once because of the way the
- * function is written) *)
+ (* Apply the expansion to abstraction values *)
let allow_reborrows = false in
- let apply_to_avalues proj_kind ctx =
- apply_symbolic_expansion_to_avalues config allow_reborrows proj_kind
- original_sv expansion ctx
- in
- let ctx = apply_to_avalues LoanProj ctx in
- apply_to_avalues BorrowProj ctx
+ apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+ expansion ctx
(** Expand a symbolic value which is not an enumeration with several variants.