summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml43
-rw-r--r--src/Values.ml10
2 files changed, 34 insertions, 19 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ee69a39d..fb98b516 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -40,6 +40,9 @@ let operand_to_string = Print.EvalCtxCfimAst.operand_to_string
let statement_to_string ctx =
Print.EvalCtxCfimAst.statement_to_string ctx "" " "
+let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
+ sv0.V.sv_id = sv1.V.sv_id
+
(* TODO: move *)
let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var
=
@@ -1046,29 +1049,30 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
TODO: detailed comments. See [apply_proj_borrows]
*)
let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t)
- (see : symbolic_expansion) (ty : T.rty) : V.typed_avalue =
+ (see : symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue =
(* Match *)
- let value : V.avalue =
- match (see, ty) with
- | SeConcrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv
+ let (value, ty) : V.avalue * T.rty =
+ match (see, original_sv_ty) with
+ | SeConcrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) ->
+ (V.AConcrete cv, original_sv_ty)
| SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) ->
(* Project over the field values *)
let field_values =
List.map mk_aproj_loans_from_proj_comp field_values
in
- V.AAdt { V.variant_id; field_values }
- | SeMutRef (bid, spc), T.Ref (r, _ref_ty, T.Mut) ->
+ (V.AAdt { V.variant_id; field_values }, original_sv_ty)
+ | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) ->
(* Apply the projector to the borrowed value *)
let child_av = mk_aproj_loans_from_proj_comp spc in
(* Check if the region is in the set of projected regions (note that
* we never project over static regions) *)
if region_in_set r regions then
(* In the set: keep *)
- V.ALoan (V.AMutLoan (bid, child_av))
+ (V.ALoan (V.AMutLoan (bid, child_av)), ref_ty)
else
(* Not in the set: ignore *)
- V.ALoan (V.AIgnoredMutLoan (bid, child_av))
- | SeSharedRef (bids, spc), T.Ref (r, _ref_ty, T.Shared) ->
+ (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty)
+ | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) ->
(* Apply the projector to the borrowed value *)
let child_av = mk_aproj_loans_from_proj_comp spc in
(* Check if the region is in the set of projected regions (note that
@@ -1076,9 +1080,10 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t)
if region_in_set r regions then
(* In the set: keep *)
let shared_value = mk_typed_value_from_proj_comp spc in
- V.ALoan (V.ASharedLoan (bids, shared_value, child_av))
- else (* Not in the set: ignore *)
- V.ALoan (V.AIgnoredSharedLoan child_av)
+ (V.ALoan (V.ASharedLoan (bids, shared_value, child_av)), ref_ty)
+ else
+ (* Not in the set: ignore *)
+ (V.ALoan (V.AIgnoredSharedLoan child_av), ref_ty)
| _ -> failwith "Unreachable"
in
{ V.value; V.ty }
@@ -2748,11 +2753,11 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
match (aproj, proj_kind) with
| V.AProjLoans sv, LoanProj ->
(* Check if this is the symbolic value we are looking for *)
- if sv = original_sv then
+ if same_symbolic_id sv original_sv then
(* Apply the projector *)
let projected_value =
apply_proj_loans_on_symbolic_expansion proj_regions expansion
- sv.V.sv_ty
+ original_sv.V.sv_ty
in
(* Replace *)
projected_value.V.value
@@ -2761,10 +2766,12 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
super#visit_ASymbolic (Some proj_regions) aproj
| V.AProjBorrows (sv, proj_ty), BorrowProj ->
(* Check if this is the symbolic value we are looking for *)
- if sv = original_sv then
+ if same_symbolic_id 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) *)
+ (* WARNING: we mustn't get there if the expansion is for a shared
+ * reference. *)
let expansion =
symbolic_expansion_non_shared_borrow_to_value original_sv
expansion
@@ -2825,7 +2832,7 @@ let replace_symbolic_values (at_most_once : bool)
inherit [_] C.map_eval_ctx as super
method! visit_Symbolic env spc =
- if spc.V.svalue = original_sv then replace ()
+ if same_symbolic_id spc.V.svalue original_sv then replace ()
else super#visit_Symbolic env spc
end
in
@@ -3037,7 +3044,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
* `None` otherwise *)
let reborrow_ashared proj_regions (sv : V.symbolic_value) (proj_ty : T.rty) :
V.abstract_shared_borrows option =
- if sv = original_sv then
+ if same_symbolic_id sv original_sv then
match proj_ty with
| T.Ref (r, ref_ty, T.Shared) ->
(* Projector over the shared value *)
@@ -3058,7 +3065,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
inherit [_] C.map_eval_ctx as super
method! visit_Symbolic env sv =
- if sv.V.svalue = original_sv then
+ if same_symbolic_id sv.V.svalue original_sv then
let bid = fresh_borrow () in
V.Borrow (V.SharedBorrow bid)
else super#visit_Symbolic env sv
diff --git a/src/Values.ml b/src/Values.ml
index a4dde6ea..e4eca156 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -47,7 +47,15 @@ type constant_value =
type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty }
[@@deriving show]
-(** Symbolic value *)
+(** Symbolic value.
+
+ TODO: a symbolic value may not always have the same type!!
+ For references:
+ - a projector on loans may see a symbolic value of id `sid` as having type `T`
+ - a projector on borrows may see it as having type `&mut T`
+ We need to make this clear and more consistant.
+ So [symbolic_value] is actually a projector. TODO: rename
+ *)
(** TODO: make it clear that complementary projectors are projectors on borrows *)
type symbolic_proj_comp = {