From 7137e0733650e0ce37eff4ff805c95543f2c1161 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 17:44:17 +0100
Subject: Remove the symbolic_proj_comp def and make the set of ended regions a
 field in the eval_ctx struct

---
 src/Contexts.ml               |  1 +
 src/Interpreter.ml            |  1 +
 src/InterpreterBorrows.ml     | 80 +++++++------------------------------------
 src/InterpreterExpansion.ml   | 77 +++++++++++++++++------------------------
 src/InterpreterExpressions.ml |  6 ++--
 src/InterpreterPaths.ml       |  5 ++-
 src/InterpreterProjectors.ml  | 33 +++++++++---------
 src/InterpreterStatements.ml  | 29 ++++++----------
 src/InterpreterUtils.ml       | 78 ++++++++++++-----------------------------
 src/Invariants.ml             |  4 +--
 src/Print.ml                  | 12 +++----
 src/Values.ml                 | 45 ++++++------------------
 12 files changed, 116 insertions(+), 255 deletions(-)

(limited to 'src')

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 89056680..5225645c 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -67,6 +67,7 @@ type eval_ctx = {
   fun_context : fun_def list;
   type_vars : type_var list;
   env : env;
+  ended_regions : RegionId.set_t;
   symbolic_counter : SymbolicValueId.generator;
   (* TODO: make this global? *)
   borrow_counter : BorrowId.generator;
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 384e0a11..54911d85 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -30,6 +30,7 @@ module Test = struct
       C.fun_context = fun_defs;
       C.type_vars;
       C.env = [];
+      C.ended_regions = T.RegionId.Set.empty;
       C.symbolic_counter = V.SymbolicValueId.generator_zero;
       C.borrow_counter = V.BorrowId.generator_zero;
       C.region_counter = T.RegionId.generator_zero;
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index fbd958ef..3cfa78e0 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -626,13 +626,7 @@ let convert_avalue_to_value (av : V.typed_avalue) (ctx : C.eval_ctx) :
   (* Generate the fresh a symbolic value *)
   let ctx, sv_id = C.fresh_symbolic_value_id ctx in
   let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in
-  let value : V.symbolic_proj_comp =
-    (* Note that the set of ended regions is empty: we shouldn't have to take
-     * into account any ended regions at this point, otherwise we would be in
-     * the first case where we should return ⊥ *)
-    { V.svalue; V.rset_ended = T.RegionId.Set.empty }
-  in
-  let value = V.Symbolic value in
+  let value = V.Symbolic svalue in
   (ctx, { V.value; V.ty })
 
 (** End a borrow identified by its borrow id in a context
@@ -759,8 +753,15 @@ and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id)
   let ctx = end_abstraction_loans config abs_id ctx in
   (* End the abstraction itself by redistributing the borrows it contains *)
   let ctx = end_abstraction_borrows config abs_id ctx in
-  (* End the regions owned by the abstraction *)
-  let ctx = end_abstraction_regions config abs_id ctx in
+  (* End the regions owned by the abstraction - note that we don't need to
+   * relookup the abstraction: the set of regions in an abstraction never
+   * changes... *)
+  let ctx =
+    {
+      ctx with
+      ended_regions = T.RegionId.Set.union ctx.ended_regions abs.V.regions;
+    }
+  in
   (* Remove all the references to the id of the current abstraction, and remove
    * the abstraction itself *)
   end_abstraction_remove_from_context config abs_id ctx
@@ -911,63 +912,6 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
     (* Reexplore *)
     end_abstraction_borrows config abs_id ctx
 
-(** Update the symbolic values in a context to register the regions in the
-    abstraction we are ending as already ended.
-    Note that this function also checks that no symbolic value in an abstraction
-    contains regions which we are ending.
-    Of course, we ignore the abstraction we are currently ending...
- *)
-and end_abstraction_regions (_config : C.config) (abs_id : V.AbstractionId.id)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Lookup the abstraction to retrieve the set of owned regions *)
-  let abs = C.ctx_lookup_abs ctx abs_id in
-  let ended_regions = abs.V.regions in
-  (* Update all the symbolic values in the context *)
-  let obj =
-    object
-      inherit [_] C.map_eval_ctx as super
-
-      method! visit_Symbolic _ sproj =
-        let sproj =
-          {
-            sproj with
-            V.rset_ended = T.RegionId.Set.union sproj.V.rset_ended ended_regions;
-          }
-        in
-        V.Symbolic sproj
-
-      method! visit_aproj (abs_regions : T.RegionId.set_t option) aproj =
-        (* Sanity check *)
-        (match aproj with
-        | V.AProjLoans _ -> ()
-        | V.AProjBorrows (sv, ty) -> (
-            match abs_regions with
-            | None -> failwith "Unexpected"
-            | Some abs_regions ->
-                assert (
-                  not
-                    (projections_intersect sv.V.sv_ty ended_regions ty
-                       abs_regions))));
-        (* Return - nothing to update *)
-        aproj
-
-      method! visit_abs (regions : T.RegionId.set_t option) abs =
-        if abs.V.abs_id = abs_id then abs
-        else (
-          assert (Option.is_none regions);
-          (* Check that we don't project over already ended regions *)
-          assert (T.RegionId.Set.disjoint ended_regions abs.V.regions);
-          (* Remember the set of regions owned by the abstraction *)
-          let regions = Some abs.V.regions in
-          super#visit_abs regions abs)
-      (** Whenever we dive in an abstraction, we need to keep track of the
-          set of regions owned by the abstraction.
-          Also: we don't dive in the abstraction we are currently ending... *)
-    end
-  in
-  (* Update the context *)
-  obj#visit_eval_ctx None ctx
-
 (** Remove an abstraction from the context, as well as all its references *)
 and end_abstraction_remove_from_context (_config : C.config)
     (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx =
@@ -1022,7 +966,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
          to do a sanity check. *)
       assert (not (loans_in_value sv));
       (* Check there isn't [Bottom] (this is actually an invariant *)
-      assert (not (bottom_in_value sv));
+      assert (not (bottom_in_value ctx.ended_regions sv));
       (* Check there aren't inactivated borrows *)
       assert (not (inactivated_in_value sv));
       (* Update the loan content *)
@@ -1094,7 +1038,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
               ("activate_inactivated_mut_borrow: resulting value:\n"
              ^ V.show_typed_value sv));
           assert (not (loans_in_value sv));
-          assert (not (bottom_in_value sv));
+          assert (not (bottom_in_value ctx.ended_regions sv));
           assert (not (inactivated_in_value sv));
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 7366a819..24ec018e 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -152,7 +152,7 @@ let replace_symbolic_values (at_most_once : bool)
       inherit [_] C.map_eval_ctx as super
 
       method! visit_Symbolic env spc =
-        if same_symbolic_id spc.V.svalue original_sv then replace ()
+        if same_symbolic_id spc original_sv then replace ()
         else super#visit_Symbolic env spc
     end
   in
@@ -190,9 +190,9 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
-    (ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id)
-    (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (ctx : C.eval_ctx) : (C.eval_ctx * symbolic_expansion) list =
+    (def_id : T.TypeDefId.id) (regions : T.RegionId.id T.region list)
+    (types : T.rty list) (ctx : C.eval_ctx) :
+    (C.eval_ctx * symbolic_expansion) list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = C.ctx_lookup_type_def ctx def_id in
@@ -210,8 +210,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
       C.eval_ctx * symbolic_expansion =
     let ctx, field_values =
       List.fold_left_map
-        (fun ctx (ty : T.rty) ->
-          mk_fresh_symbolic_proj_comp ended_regions ty ctx)
+        (fun ctx (ty : T.rty) -> mk_fresh_symbolic_value ty ctx)
         ctx field_types
     in
     let see = SeAdt (variant_id, field_values) in
@@ -220,32 +219,29 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
   (* Initialize all the expanded values of all the variants *)
   List.map (initialize ctx) variants_fields_types
 
-let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t)
-    (field_types : T.rty list) (ctx : C.eval_ctx) :
-    C.eval_ctx * symbolic_expansion =
+let compute_expanded_symbolic_tuple_value (field_types : T.rty list)
+    (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion =
   (* Generate the field values *)
   let ctx, field_values =
     List.fold_left_map
-      (fun ctx sv_ty -> mk_fresh_symbolic_proj_comp ended_regions sv_ty ctx)
+      (fun ctx sv_ty -> mk_fresh_symbolic_value sv_ty ctx)
       ctx field_types
   in
   let variant_id = None in
   let see = SeAdt (variant_id, field_values) in
   (ctx, see)
 
-let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t)
-    (boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion =
+let compute_expanded_symbolic_box_value (boxed_ty : T.rty) (ctx : C.eval_ctx) :
+    C.eval_ctx * symbolic_expansion =
   (* Introduce a fresh symbolic value *)
-  let ctx, boxed_value =
-    mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx
-  in
+  let ctx, boxed_value = mk_fresh_symbolic_value boxed_ty ctx in
   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)
-    (ref_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx =
-  (* First, replace the projectors on borrows (AProjBorrow and proj_comp)
+    (original_sv : V.symbolic_value) (ref_ty : T.rty) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  (* First, replace the projectors on borrows.
    * 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.
@@ -285,7 +281,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
       inherit [_] C.map_eval_ctx as super
 
       method! visit_Symbolic env sv =
-        if same_symbolic_id sv.V.svalue original_sv then
+        if same_symbolic_id sv original_sv then
           let bid = fresh_borrow () in
           V.Borrow (V.SharedBorrow bid)
         else super#visit_Symbolic env sv
@@ -326,7 +322,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   (* Finally, replace the projectors on loans *)
   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 ctx, shared_sv = mk_fresh_symbolic_value ref_ty ctx in
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
@@ -339,17 +335,16 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   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)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+    (original_sv : V.symbolic_value) (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 *)
-  assert (not (region_in_set region ended_regions));
+  assert (not (region_in_set region ctx.ended_regions));
   (* Match on the reference kind *)
   match rkind with
   | T.Mut ->
       (* Simple case: simply create a fresh symbolic value and a fresh
        * borrow id *)
-      let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in
+      let ctx, sv = mk_fresh_symbolic_value ref_ty ctx in
       let ctx, bid = C.fresh_borrow_id ctx in
       let see = SeMutRef (bid, sv) in
       (* Expand the symbolic values - we simply perform a substitution (and
@@ -370,8 +365,7 @@ let expand_symbolic_value_borrow (config : C.config)
       (* Return *)
       ctx
   | T.Shared ->
-      expand_symbolic_value_shared_borrow config original_sv ended_regions
-        ref_ty ctx
+      expand_symbolic_value_shared_borrow config original_sv ref_ty ctx
 
 (** Expand a symbolic value which is not an enumeration with several variants
     (i.e., in a situation where it doesn't lead to branching).
@@ -379,13 +373,12 @@ let expand_symbolic_value_borrow (config : C.config)
     This function is used when exploring paths.
  *)
 let expand_symbolic_value_no_branching (config : C.config)
-    (pe : E.projection_elem) (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) :
+    (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) :
     C.eval_ctx =
   (* Compute the expanded value - note that when doing so, we may introduce
    * fresh symbolic values in the context (which thus gets updated) *)
-  let original_sv = sp.V.svalue in
+  let original_sv = sp in
   let rty = original_sv.V.sv_ty in
-  let ended_regions = sp.V.rset_ended in
   let ctx =
     match (pe, rty) with
     (* "Regular" ADTs *)
@@ -396,8 +389,8 @@ let expand_symbolic_value_no_branching (config : C.config)
          * don't allow to expand enumerations with strictly more than one variant *)
         let expand_enumerations = false in
         match
-          compute_expanded_symbolic_adt_value expand_enumerations ended_regions
-            def_id regions types ctx
+          compute_expanded_symbolic_adt_value expand_enumerations def_id regions
+            types ctx
         with
         | [ (ctx, see) ] ->
             (* Apply in the context *)
@@ -413,9 +406,7 @@ let expand_symbolic_value_no_branching (config : C.config)
     | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
         assert (arity = List.length tys);
         (* Generate the field values *)
-        let ctx, see =
-          compute_expanded_symbolic_tuple_value ended_regions tys ctx
-        in
+        let ctx, see = compute_expanded_symbolic_tuple_value tys ctx in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -426,9 +417,7 @@ let expand_symbolic_value_no_branching (config : C.config)
         ctx
     (* Boxes *)
     | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
-        let ctx, see =
-          compute_expanded_symbolic_box_value ended_regions boxed_ty ctx
-        in
+        let ctx, see = compute_expanded_symbolic_box_value boxed_ty ctx in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -439,8 +428,7 @@ let expand_symbolic_value_no_branching (config : C.config)
         ctx
     (* Borrows *)
     | Deref, T.Ref (region, ref_ty, rkind) ->
-        expand_symbolic_value_borrow config original_sv ended_regions region
-          ref_ty rkind ctx
+        expand_symbolic_value_borrow config original_sv region ref_ty rkind ctx
     | _ ->
         failwith
           ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
@@ -454,13 +442,12 @@ let expand_symbolic_value_no_branching (config : C.config)
 
     This might lead to branching.
  *)
-let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp)
+let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
     (ctx : C.eval_ctx) : C.eval_ctx list =
   (* Compute the expanded value - note that when doing so, we may introduce
    * fresh symbolic values in the context (which thus gets updated) *)
-  let original_sv = sp.V.svalue in
+  let original_sv = sp in
   let rty = original_sv.V.sv_ty in
-  let ended_regions = sp.V.rset_ended in
   match rty with
   (*  The value should be a "regular" ADTs *)
   | T.Adt (T.AdtId def_id, regions, types) ->
@@ -468,8 +455,8 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp)
        * don't allow to expand enumerations with strictly more than one variant *)
       let expand_enumerations = true in
       let res =
-        compute_expanded_symbolic_adt_value expand_enumerations ended_regions
-          def_id regions types ctx
+        compute_expanded_symbolic_adt_value expand_enumerations def_id regions
+          types ctx
       in
       (* Update the synthesized program *)
       let seel = List.map (fun (_, x) -> x) res in
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index e379eacd..f9b1ab3c 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -87,7 +87,7 @@ let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
         let access = Move in
         prepare_rplace config access p ctx
   in
-  assert (not (bottom_in_value v));
+  assert (not (bottom_in_value ctx.ended_regions v));
   (ctx, v)
 
 (** Evaluate an operand. *)
@@ -109,7 +109,7 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
       let ctx, v = prepare_rplace config access p ctx in
       (* Copy the value *)
       L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v));
-      assert (not (bottom_in_value v));
+      assert (not (bottom_in_value ctx.ended_regions v));
       let allow_adt_copy = false in
       copy_value allow_adt_copy config ctx v
   | Expressions.Move p -> (
@@ -118,7 +118,7 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
       let ctx, v = prepare_rplace config access p ctx in
       (* Move the value *)
       L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v));
-      assert (not (bottom_in_value v));
+      assert (not (bottom_in_value ctx.ended_regions v));
       let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
       match write_place config access p bottom ctx with
       | Error _ -> failwith "Unreachable"
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 80725bab..bfe877ab 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -28,7 +28,7 @@ type path_fail_kind =
   | FailInactivatedMutBorrow of V.BorrowId.id
       (** Failure because we couldn't go inside an inactivated mutable borrow
           (which should get activated) *)
-  | FailSymbolic of (E.projection_elem * V.symbolic_proj_comp)
+  | FailSymbolic of (E.projection_elem * V.symbolic_value)
       (** Failure because we need to enter a symbolic value (and thus need to expand it) *)
   (* TODO: Remove the parentheses *)
   | FailBottom of (int * E.projection_elem * T.ety)
@@ -774,8 +774,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
        * Note that in the general case, copy is a trait: copying values
        * thus requires calling the proper function. Here, we copy values
        * for very simple types such as integers, shared borrows, etc. *)
-      assert (
-        type_is_primitively_copyable (Subst.erase_regions sp.V.svalue.V.sv_ty));
+      assert (type_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty));
       (* If the type is copyable, we simply return the current value. Side
        * remark: what is important to look at when copying symbolic values
        * is symbolic expansion. The important subcase is the expansion of shared
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index ada1a89a..21c9e034 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -13,9 +13,9 @@ open InterpreterBorrowsCore
 (** A symbolic expansion *)
 type symbolic_expansion =
   | SeConcrete of V.constant_value
-  | SeAdt of (T.VariantId.id option * V.symbolic_proj_comp list)
-  | SeMutRef of V.BorrowId.id * V.symbolic_proj_comp
-  | SeSharedRef of V.BorrowId.set_t * V.symbolic_proj_comp
+  | SeAdt of (T.VariantId.id option * V.symbolic_value list)
+  | SeMutRef of V.BorrowId.id * V.symbolic_value
+  | SeSharedRef of V.BorrowId.set_t * V.symbolic_value
 
 (** Auxiliary function.
 
@@ -92,8 +92,9 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
       asb
   | V.Loan _, _ -> failwith "Unreachable"
   | V.Symbolic s, _ ->
-      assert (not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions));
-      [ V.AsbProjReborrows (s.V.svalue, ty) ]
+      (* Check that the projection doesn't contain ended regions *)
+      assert (not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions));
+      [ V.AsbProjReborrows (s, ty) ]
   | _ -> failwith "Unreachable"
 
 (** Apply (and reduce) a projector over borrows to a value.
@@ -212,12 +213,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
           V.ABorrow bc
     | V.Loan _, _ -> failwith "Unreachable"
     | V.Symbolic s, _ ->
-        (* Check that the symbolic value doesn't contain already ended regions,
+        (* Check that the projection doesn't contain already ended regions,
          * if necessary *)
         if check_symbolic_no_ended then
           assert (
-            not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions));
-        V.ASymbolic (V.AProjBorrows (s.V.svalue, ty))
+            not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions));
+        V.ASymbolic (V.AProjBorrows (s, ty))
     | _ -> failwith "Unreachable"
   in
   { V.value; V.ty }
@@ -231,7 +232,7 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
     | SeConcrete cv -> V.Concrete cv
     | SeAdt (variant_id, field_values) ->
         let field_values =
-          List.map mk_typed_value_from_proj_comp field_values
+          List.map mk_typed_value_from_symbolic_value field_values
         in
         V.Adt { V.variant_id; V.field_values }
     | SeMutRef (_, _) | SeSharedRef (_, _) ->
@@ -250,7 +251,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
   match see with
   | SeMutRef (bid, bv) ->
       let ty = Subst.erase_regions sv.V.sv_ty in
-      let bv = mk_typed_value_from_proj_comp bv in
+      let bv = mk_typed_value_from_symbolic_value bv in
       let value = V.Borrow (V.MutBorrow (bid, bv)) in
       { V.value; ty }
   | SeSharedRef (_, _) ->
@@ -271,14 +272,14 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t)
     | 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
+          List.map mk_aproj_loans_from_symbolic_value field_values
         in
         (V.AAdt { V.variant_id; field_values }, original_sv_ty)
     | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) ->
         (* Sanity check *)
-        assert (spc.V.svalue.V.sv_ty = ref_ty);
+        assert (spc.V.sv_ty = ref_ty);
         (* Apply the projector to the borrowed value *)
-        let child_av = mk_aproj_loans_from_proj_comp spc in
+        let child_av = mk_aproj_loans_from_symbolic_value 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
@@ -289,14 +290,14 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t)
           (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty)
     | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) ->
         (* Sanity check *)
-        assert (spc.V.svalue.V.sv_ty = ref_ty);
+        assert (spc.V.sv_ty = ref_ty);
         (* Apply the projector to the borrowed value *)
-        let child_av = mk_aproj_loans_from_proj_comp spc in
+        let child_av = mk_aproj_loans_from_symbolic_value 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 *)
-          let shared_value = mk_typed_value_from_proj_comp spc in
+          let shared_value = mk_typed_value_from_symbolic_value spc in
           (V.ALoan (V.ASharedLoan (bids, shared_value, child_av)), ref_ty)
         else
           (* Not in the set: ignore *)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 5eee5296..c4bbdf23 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -74,10 +74,8 @@ let eval_assertion (config : C.config) (ctx : C.eval_ctx)
        * `true` *)
       S.synthesize_assert v;
       let see = SeConcrete (V.Bool true) in
-      let ctx =
-        apply_symbolic_expansion_non_borrow config sv.V.svalue see ctx
-      in
-      S.synthesize_symbolic_expansion_no_branching sv.V.svalue see;
+      let ctx = apply_symbolic_expansion_non_borrow config sv see ctx in
+      S.synthesize_symbolic_expansion_no_branching sv see;
       (* We can finally fully evaluate the operand *)
       let ctx, _ = eval_operand config ctx assertion.cond in
       Ok ctx
@@ -641,15 +639,13 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets)
           else eval_statement config ctx st2
       | V.Symbolic sv ->
           (* Synthesis *)
-          S.synthesize_symbolic_expansion_if_branching sv.V.svalue;
+          S.synthesize_symbolic_expansion_if_branching sv;
           (* Expand the symbolic value to true or false *)
           let see_true = SeConcrete (V.Bool true) in
           let see_false = SeConcrete (V.Bool false) in
           let expand_and_execute see st =
             (* Apply the symbolic expansion *)
-            let ctx =
-              apply_symbolic_expansion_non_borrow config sv.V.svalue see ctx
-            in
+            let ctx = apply_symbolic_expansion_non_borrow config sv see ctx in
             (* Evaluate the operand *)
             let ctx, _ = eval_operand config ctx op in
             (* Evaluate the branch *)
@@ -674,7 +670,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets)
           | Some (_, tgt) -> eval_statement config ctx tgt)
       | V.Symbolic sv ->
           (* Synthesis *)
-          S.synthesize_symbolic_expansion_switch_int_branching sv.V.svalue;
+          S.synthesize_symbolic_expansion_switch_int_branching sv;
           (* For all the branches of the switch, we expand the symbolic value
            * to the value given by the branch and execute the branch statement.
            * For the otherwise branch, we leave the symbolic value as it is
@@ -685,9 +681,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets)
           let exec_branch (switch_value, branch_st) =
             let see = SeConcrete (V.Scalar switch_value) in
             (* Apply the symbolic expansion *)
-            let ctx =
-              apply_symbolic_expansion_non_borrow config sv.V.svalue see ctx
-            in
+            let ctx = apply_symbolic_expansion_non_borrow config sv see ctx in
             (* Evaluate the operand *)
             let ctx, _ = eval_operand config ctx op in
             (* Evaluate the branch *)
@@ -810,11 +804,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     (args : E.operand list) (dest : E.place) : C.eval_ctx =
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.A.output in
-  let ctx, ret_spc =
-    mk_fresh_symbolic_proj_comp T.RegionId.Set.empty ret_sv_ty ctx
-  in
-  let ret_value = mk_typed_value_from_proj_comp ret_spc in
-  let ret_av = mk_aproj_loans_from_symbolic_value ret_spc.V.svalue in
+  let ctx, ret_spc = mk_fresh_symbolic_value ret_sv_ty ctx in
+  let ret_value = mk_typed_value_from_symbolic_value ret_spc in
+  let ret_av = mk_aproj_loans_from_symbolic_value ret_spc in
   (* Evaluate the input operands *)
   let ctx, args = eval_operands config ctx args in
   let args_with_rtypes = List.combine args inst_sg.A.inputs in
@@ -857,8 +849,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
   (* Move the return value to its destination *)
   let ctx = assign_to_place config ctx ret_value dest in
   (* Synthesis *)
-  S.synthesize_function_call fid region_params type_params args dest
-    ret_spc.V.svalue;
+  S.synthesize_function_call fid region_params type_params args dest ret_spc;
   (* Return *)
   ctx
 
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 458c11b4..fcc6050f 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -51,51 +51,19 @@ let mk_fresh_symbolic_value (ty : T.rty) (ctx : C.eval_ctx) :
   let svalue = { V.sv_id; V.sv_ty = ty } in
   (ctx, svalue)
 
-(** Create a fresh symbolic proj comp *)
-let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty)
-    (ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp =
-  let ctx, svalue = mk_fresh_symbolic_value ty ctx in
-  let sv = { V.svalue; rset_ended = ended_regions } in
-  (ctx, sv)
-
-(** Create a fresh symbolic value (as a complementary projector) *)
-let mk_fresh_symbolic_proj_comp_value (ended_regions : T.RegionId.set_t)
-    (ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
-  let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ty ctx in
-  let value : V.value = V.Symbolic sv in
-  let ty : T.ety = Subst.erase_regions ty in
-  let sv : V.typed_value = { V.value; ty } in
-  (ctx, sv)
-
-let mk_typed_value_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_value =
-  let ty = Subst.erase_regions sv.V.svalue.V.sv_ty in
-  let value = V.Symbolic sv in
-  { V.value; ty }
-
-(** Create a typed value from a symbolic value.
-
-    Initializes the set of ended regions with `empty`.
- *)
+(** Create a typed value from a symbolic value. *)
 let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
     V.typed_value =
-  let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in
-  mk_typed_value_from_proj_comp spc
-
-let mk_aproj_loans_from_proj_comp (spc : V.symbolic_proj_comp) : V.typed_avalue
-    =
-  let ty = spc.V.svalue.V.sv_ty in
-  let proj = V.AProjLoans spc.V.svalue in
-  let value = V.ASymbolic proj in
-  { V.value; ty }
-
-(** Create a Loans projector from a symbolic value.
+  let av = V.Symbolic svalue in
+  let av : V.typed_value =
+    { V.value = av; V.ty = Subst.erase_regions svalue.V.sv_ty }
+  in
+  av
 
-    Initializes the set of ended regions with `empty`.
- *)
+(** Create a loans projector from a symbolic value. *)
 let mk_aproj_loans_from_symbolic_value (svalue : V.symbolic_value) :
     V.typed_avalue =
-  let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in
-  let av = V.ASymbolic (V.AProjLoans spc.V.svalue) in
+  let av = V.ASymbolic (V.AProjLoans svalue) in
   let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in
   av
 
@@ -162,7 +130,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
       inherit [_] C.iter_eval_ctx
 
       method! visit_Symbolic _ sv =
-        if sv.V.svalue.V.sv_id = sv_id then raise Found else ()
+        if sv.V.sv_id = sv_id then raise Found else ()
 
       method! visit_ASymbolic _ aproj =
         match aproj with
@@ -228,36 +196,33 @@ let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t)
       || projections_intersect ty1 rset1 ty2 rset2
   | _ -> failwith "Unreachable"
 
-(** Check if the ended regions of a comp projector over a symbolic value
-    intersect the regions listed in another projection *)
-let symbolic_proj_comp_ended_regions_intersect_proj (s : V.symbolic_proj_comp)
-    (ty : T.rty) (regions : T.RegionId.set_t) : bool =
-  projections_intersect s.V.svalue.V.sv_ty s.V.rset_ended ty regions
-
 (** Check that a symbolic value doesn't contain ended regions.
 
     Note that we don't check that the set of ended regions is empty: we
     check that the set of ended regions doesn't intersect the set of
     regions used in the type (this is more general).
 *)
-let symbolic_proj_comp_ended_regions (s : V.symbolic_proj_comp) : bool =
-  let regions = rty_regions s.V.svalue.V.sv_ty in
-  not (T.RegionId.Set.disjoint regions s.rset_ended)
+let symbolic_value_has_ended_regions (ended_regions : T.RegionId.set_t)
+    (s : V.symbolic_value) : bool =
+  let regions = rty_regions s.V.sv_ty in
+  not (T.RegionId.Set.disjoint regions ended_regions)
 
 (** Check if a [value] contains ⊥.
 
     Note that this function is very general: it also checks wether
     symbolic values contain already ended regions.
  *)
-let bottom_in_value (v : V.typed_value) : bool =
+let bottom_in_value (ended_regions : T.RegionId.set_t) (v : V.typed_value) :
+    bool =
   let obj =
     object
       inherit [_] V.iter_typed_value
 
       method! visit_Bottom _ = raise Found
 
-      method! visit_symbolic_proj_comp _ s =
-        if symbolic_proj_comp_ended_regions s then raise Found else ()
+      method! visit_symbolic_value _ s =
+        if symbolic_value_has_ended_regions ended_regions s then raise Found
+        else ()
     end
   in
   (* We use exceptions *)
@@ -273,7 +238,7 @@ let bottom_in_value (v : V.typed_value) : bool =
     
     TODO: remove?
 *)
-let bottom_in_avalue (v : V.typed_avalue) (_abs_regions : T.RegionId.set_t) :
+let bottom_in_avalue (ended_regions : T.RegionId.set_t) (v : V.typed_avalue) :
     bool =
   let obj =
     object
@@ -281,8 +246,9 @@ let bottom_in_avalue (v : V.typed_avalue) (_abs_regions : T.RegionId.set_t) :
 
       method! visit_Bottom _ = raise Found
 
-      method! visit_symbolic_proj_comp _ sv =
-        if symbolic_proj_comp_ended_regions sv then raise Found else ()
+      method! visit_symbolic_value _ sv =
+        if symbolic_value_has_ended_regions ended_regions sv then raise Found
+        else ()
 
       method! visit_aproj _ ap =
         (* Nothing to do actually *)
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 11b00381..86fa3d46 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -433,8 +433,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 | Abstract (V.AMutBorrow (_, sv)) ->
                     assert (Subst.erase_regions sv.V.ty = ty)
                 | _ -> failwith "Inconsistent context"))
-        | V.Symbolic spc, ty ->
-            let ty' = Subst.erase_regions spc.V.svalue.V.sv_ty in
+        | V.Symbolic sv, ty ->
+            let ty' = Subst.erase_regions sv.V.sv_ty in
             assert (ty' = ty)
         | _ -> failwith "Erroneous typing");
         (* Continue exploring to inspect the subterms *)
diff --git a/src/Print.ml b/src/Print.ml
index 0b436f1a..f714e847 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -214,11 +214,6 @@ module Values = struct
       (sv : V.symbolic_value) : string =
     symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.rty_to_string fmt sv.sv_ty
 
-  let symbolic_proj_comp_to_string (fmt : PT.rtype_formatter)
-      (sp : V.symbolic_proj_comp) : string =
-    let regions = T.RegionId.set_to_string sp.rset_ended in
-    "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")"
-
   let symbolic_value_proj_to_string (fmt : value_formatter)
       (sv : V.symbolic_value) (rty : T.rty) : string =
     symbolic_value_id_to_string sv.sv_id
@@ -275,8 +270,7 @@ module Values = struct
     | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
     | Borrow bc -> borrow_content_to_string fmt bc
     | Loan lc -> loan_content_to_string fmt lc
-    | Symbolic s ->
-        symbolic_proj_comp_to_string (value_to_rtype_formatter fmt) s
+    | Symbolic s -> symbolic_value_to_string (value_to_rtype_formatter fmt) s
 
   and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) :
       string =
@@ -539,6 +533,7 @@ module Contexts = struct
 
   let eval_ctx_to_string (ctx : C.eval_ctx) : string =
     let fmt = eval_ctx_to_ctx_formatter ctx in
+    let ended_regions = T.RegionId.set_to_string ctx.ended_regions in
     let frames = split_env_according_to_frames ctx.env in
     let num_frames = List.length frames in
     let frames =
@@ -547,7 +542,8 @@ module Contexts = struct
           "\n# Frame " ^ string_of_int i ^ ":\n" ^ env_to_string fmt f ^ "\n")
         frames
     in
-    "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames
+    "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames
+    ^ " frame(s)\n" ^ String.concat "" frames
 end
 
 module PC = Contexts (* local module *)
diff --git a/src/Values.ml b/src/Values.ml
index 47bdda23..b6bb414b 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -47,35 +47,7 @@ type constant_value =
 
 type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty }
 [@@deriving show]
-(** 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 to [symbolic_proj].
-    The kind of projector will then depend on the context.
-    Actually, maybe we shouldn't use this type. Or for abstractions we should
-    use different types. Something like:
-    - [proj_borrows] for values
-    - [aproj_loans], [aproj_borrows] for avalues
-  *)
-
-(** TODO: make it clear that complementary projectors are projectors on borrows.
- ** TODO: actually this is useless: the set of ended regions should be global!
- ** (and thus stored in the context) *)
-type symbolic_proj_comp = {
-  svalue : symbolic_value;  (** The symbolic value itself *)
-  rset_ended : RegionId.set_t;
-      (** The regions used in the symbolic value which have already ended *)
-}
-[@@deriving show]
-(** A complementary projector over a symbolic value.
-    
-    "Complementary" stands for the fact that it is a projector over all the
-    regions *but* the ones which are listed in the projector.
-*)
+(** A symbolic value *)
 
 (** Ancestor for [typed_value] iter visitor *)
 class ['self] iter_typed_value_base =
@@ -86,8 +58,7 @@ class ['self] iter_typed_value_base =
 
     method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
 
-    method visit_symbolic_proj_comp : 'env -> symbolic_proj_comp -> unit =
-      fun _ _ -> ()
+    method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> ()
 
     method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
   end
@@ -103,8 +74,7 @@ class ['self] map_typed_value_base =
     method visit_erased_region : 'env -> erased_region -> erased_region =
       fun _ r -> r
 
-    method visit_symbolic_proj_comp
-        : 'env -> symbolic_proj_comp -> symbolic_proj_comp =
+    method visit_symbolic_value : 'env -> symbolic_value -> symbolic_value =
       fun _ sv -> sv
 
     method visit_ety : 'env -> ety -> ety = fun _ ty -> ty
@@ -117,8 +87,13 @@ type value =
   | Bottom  (** No value (uninitialized or moved value) *)
   | Borrow of borrow_content  (** A borrowed value *)
   | Loan of loan_content  (** A loaned value *)
-  | Symbolic of symbolic_proj_comp
-      (** Unknown (symbolic) value. This is a projector on borrows (TODO: make this clearer). *)
+  | Symbolic of symbolic_value
+      (** Borrow projector over a symbolic value.
+      
+          Note that contrary to the abstraction-values case, symbolic values
+          appearing in regular values are interpreted as *borrow* projectors,
+          they can never be *loan* projectors.
+       *)
 
 and adt_value = {
   variant_id : (VariantId.id option[@opaque]);
-- 
cgit v1.2.3