From f746abf4c631a860d8dafc83c47d569574bdc245 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 10:24:47 +0100
Subject: Fix a mistake in convert_avalue_to_value

---
 src/Interpreter.ml | 62 ++++++++++++++++++++++++------------------------------
 1 file changed, 27 insertions(+), 35 deletions(-)

(limited to 'src/Interpreter.ml')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index a123f046..192dfe25 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1267,38 +1267,34 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
 (** Convert an [avalue] to a [value].
 
     This function is used when ending abstractions: whenever we end a borrow
-    in an abstraction, we converted the borrowed [avalue] to a [value], then give
-    back this [value] to the context.
-    
-    There are two possibilities:
-    - either the borrowed [avalue] contains ended regions, in which case we return ⊥
-    - or it doesn't contain ⊥, in which case we simply return a newly introduced
-      symbolic value.
-    We return a new context because we may have to introduce a symbolic value.
-    
-    The `ended_regions` parameter is for the regions contained in the current
-    abstraction.
+    in an abstraction, we converted the borrowed [avalue] to a fresh symbolic
+    [value], then give back this [value] to the context.
+ 
+    Note that some regions may have ended in the symbolic value we generate.
+    For instance, consider the following function signature:
+    ```
+    fn f<'a>(x : &'a mut &'a mut u32);
+    ```
+    When ending the abstraction, the value given back for the outer borrow
+    should be ⊥. In practice, we will give back a symbolic value which can't
+    be expanded (because expanding this symbolic value would require expanding
+    a reference whose region has already ended).
  *)
-let convert_avalue_to_value (ended_regions : T.RegionId.set_t)
-    (av : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+let convert_avalue_to_value (av : V.typed_avalue) (ctx : C.eval_ctx) :
+    C.eval_ctx * V.typed_value =
   (* Convert the type *)
   let ty = Subst.erase_regions av.V.ty in
-  (* Check if the avalue contains ended regions *)
-  if rty_regions_intersect av.V.ty ended_regions then
-    (* Contains ended regions: return ⊥ *)
-    (ctx, { V.value = V.Bottom; V.ty })
-  else
-    (* Doesn't contain ended regions: return 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
-    (ctx, { V.value; V.ty })
+  (* 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
+  (ctx, { V.value; V.ty })
 
 (** End a borrow identified by its borrow id in a context
     
@@ -1564,12 +1560,8 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
     let ctx =
       match bc with
       | V.AMutBorrow (bid, av) ->
-          (* First, convert the avalue to a value (by introducing the proper
-           * symbolic values). Note that we should probably use the regions owned
-           * by the abstraction for the ended_regions parameter, but for safety
-           * I'm using the accumulated regions (which include the ancestors'
-           * regions). Think a bit about that... *)
-          let ctx, v = convert_avalue_to_value abs.acc_regions av ctx in
+          (* First, convert the avalue to a (fresh symbolic) value *)
+          let ctx, v = convert_avalue_to_value av ctx in
           give_back_value config bid v ctx
       | V.ASharedBorrow bid -> give_back_shared config bid ctx
       | V.AProjSharedBorrow _ ->
-- 
cgit v1.2.3