Introduce AEndedSharedBorrow so as not to introduce ABottom when

ending shared aborrows

6 files changed, 21 insertions, 13 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index ad7b5b2c..e7031d4c 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -187,7 +187,8 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
         | V.AIgnoredMutBorrow (_, _)
         | V.AEndedMutBorrow _
         | V.AEndedIgnoredMutBorrow
-            { given_back_loans_proj = _; child = _; given_back_meta = _ } ->
+            { given_back_loans_proj = _; child = _; given_back_meta = _ }
+        | V.AEndedSharedBorrow ->
             (* Nothing special to do *)
             super#visit_ABorrow outer bc
         | V.AProjSharedBorrow asb ->
@@ -753,8 +754,8 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       (* Update the context *)
       give_back_shared config l ctx
   | Abstract
-      (V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _)
-    ->
+      ( V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _
+      | V.AEndedSharedBorrow ) ->
       failwith "Unreachable"
 
 (** Convert an [avalue] to a [value].
@@ -1158,7 +1159,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
             then raise (FoundABorrowContent bc)
             else ()
         | V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _
-        | V.AEndedIgnoredMutBorrow _ ->
+        | V.AEndedIgnoredMutBorrow _ | V.AEndedSharedBorrow ->
             (* Nothing to do for ignored borrows *)
             ()
 
@@ -1202,8 +1203,9 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
             let v = mk_typed_value_from_symbolic_value v in
             give_back_value config bid v ctx
         | V.ASharedBorrow bid ->
-            (* Replace the shared borrow with bottom *)
-            let ctx = update_aborrow ek_all bid V.ABottom ctx in
+            (* Replace the shared borrow to account for the fact it ended *)
+            let ended_borrow = V.ABorrow V.AEndedSharedBorrow in
+            let ctx = update_aborrow ek_all bid ended_borrow ctx in
             (* Give back *)
             give_back_shared config bid ctx
         | V.AProjSharedBorrow asb ->
@@ -1230,7 +1232,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
             (* Continue *)
             ctx
         | V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _
-        | V.AEndedIgnoredMutBorrow _ ->
+        | V.AEndedIgnoredMutBorrow _ | V.AEndedSharedBorrow ->
             failwith "Unexpected"
       in
       (* Reexplore *)
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index b4ab7706..941ac140 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -434,7 +434,8 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
         | V.AIgnoredMutBorrow (_, _)
         | V.AEndedMutBorrow _
         | V.AEndedIgnoredMutBorrow
-            { given_back_loans_proj = _; child = _; given_back_meta = _ } ->
+            { given_back_loans_proj = _; child = _; given_back_meta = _ }
+        | V.AEndedSharedBorrow ->
             super#visit_aborrow_content env bc
         | V.AProjSharedBorrow asb ->
             if borrow_in_asb l asb then
@@ -548,7 +549,7 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue)
         | V.ASharedBorrow bid ->
             if bid = l then update ()
             else V.ABorrow (super#visit_ASharedBorrow env bid)
-        | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
+        | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ | V.AEndedSharedBorrow
         | V.AEndedIgnoredMutBorrow _ ->
             super#visit_ABorrow env bc
         | V.AProjSharedBorrow asb ->
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 522f2ffa..fe1b5e82 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -257,7 +257,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
           | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
           | V.AIgnoredMutBorrow (None, _)
           | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _
-          | V.AProjSharedBorrow _ ->
+          | V.AEndedSharedBorrow | V.AProjSharedBorrow _ ->
               (* Do nothing *)
               ()
         in
@@ -361,7 +361,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
         let info =
           match bc with
           | V.AMutBorrow (_, _, _) -> set_outer_mut info
-          | V.ASharedBorrow _ -> set_outer_shared info
+          | V.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info
           | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
           | V.AEndedIgnoredMutBorrow _ ->
               set_outer_mut info
diff --git a/src/Print.ml b/src/Print.ml
index 69feeb6c..78a826bf 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -440,6 +440,7 @@ module Values = struct
         ^ "; "
         ^ typed_avalue_to_string fmt given_back_loans_proj
         ^ ")"
+    | AEndedSharedBorrow -> "@ended_shared_borrow"
     | AProjSharedBorrow sb ->
         "@ignored_shared_borrow("
         ^ abstract_shared_borrows_to_string fmt sb
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 1985bfd3..80d08ac4 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -678,7 +678,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) :
   | AEndedIgnoredMutBorrow _ ->
       (* This happens with nested borrows: we need to dive in *)
       raise Unimplemented
-  | AProjSharedBorrow _ ->
+  | AEndedSharedBorrow | AProjSharedBorrow _ ->
       (* Ignore *)
       None
 
@@ -784,7 +784,7 @@ and aborrow_content_to_given_back (bc : V.aborrow_content) (ctx : bs_ctx) :
   | AEndedIgnoredMutBorrow _ ->
       (* This happens with nested borrows: we need to dive in *)
       raise Unimplemented
-  | AProjSharedBorrow _ ->
+  | AEndedSharedBorrow | AProjSharedBorrow _ ->
       (* Ignore *)
       (ctx, None)
 
diff --git a/src/Values.ml b/src/Values.ml
index 57d188da..25d354fb 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -681,6 +681,10 @@ and aborrow_content =
           in practice the child value should only contain ended borrows, ignored
           values, bottom values, etc.
        *)
+  | AEndedSharedBorrow
+      (** We don't really need [AEndedSharedBorrow]: we simply want to be
+          precise, and not insert ⊥ when ending borrows.
+       *)
   | AEndedIgnoredMutBorrow of {
       child : typed_avalue;
       given_back_loans_proj : typed_avalue;