Fix a few mistakes with symbolic values and their types

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 = {