From bf11d4d993b3dce15ae61bb54caac4bae1bbe27a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 27 Jan 2022 00:07:14 +0100
Subject: Implement the borrow_content case of end_abstraction_borrows

---
 src/InterpreterBorrows.ml | 36 +++++++++++++++++++++++++++++++-----
 src/main.ml               |  2 +-
 2 files changed, 32 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 487e308a..24521335 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1063,7 +1063,7 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
         | V.AIgnoredSharedLoan _ ->
             super#visit_aloan_content env lc
 
-      method! visit_loan_content env lc =
+      method! visit_loan_content _ lc =
         match lc with
         | V.MutLoan _ ->
             (* The mut loan linked to the mutable borrow present in a shared
@@ -1159,9 +1159,12 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
             ());
         super#visit_aproj env sproj
 
-      method! visit_borrow_content env bc =
-        (* TODO: this happens because of shared values *)
-        raise Errors.Unimplemented
+      method! visit_borrow_content _ bc =
+        match bc with
+        | V.SharedBorrow (_, _) | V.MutBorrow (_, _) ->
+            raise (FoundBorrowContent bc)
+        | V.InactivatedMutBorrow _ -> failwith "Unreachable"
+      (** We may need to end borrows in "regular" values, because of shared values *)
     end
   in
   (* Lookup the abstraction *)
@@ -1172,7 +1175,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
     (* No borrows: nothing to update *)
     cf ctx
   with
-  (* There are concrete borrows: end them, then reexplore *)
+  (* There are concrete (i.e., not symbolic) borrows: end them, then reexplore *)
   | FoundABorrowContent bc ->
       let ctx =
         match bc with
@@ -1233,6 +1236,29 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
       in
       (* Reexplore *)
       end_abstraction_borrows config chain abs_id cf ctx
+  (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *)
+  | FoundBorrowContent bc ->
+      let ctx =
+        match bc with
+        | V.SharedBorrow (_, bid) -> (
+            (* Replace the shared borrow with bottom *)
+            match end_borrow_get_borrow (Some abs_id) bid ctx with
+            | Error _ -> failwith "Unreachable"
+            | Ok (ctx, _) ->
+                (* Give back *)
+                give_back_shared config bid ctx)
+        | V.MutBorrow (bid, v) -> (
+            (* Replace the mut borrow with bottom *)
+            match end_borrow_get_borrow (Some abs_id) bid ctx with
+            | Error _ -> failwith "Unreachable"
+            | Ok (ctx, _) ->
+                (* Give the value back - note that the mut borrow was below a
+                 * shared borrow: the value is thus unchanged *)
+                give_back_value config bid v ctx)
+        | V.InactivatedMutBorrow _ -> failwith "Unreachable"
+      in
+      (* Reexplore *)
+      end_abstraction_borrows config chain abs_id cf ctx
 
 (** Remove an abstraction from the context, as well as all its references *)
 and end_abstraction_remove_from_context (_config : C.config)
diff --git a/src/main.ml b/src/main.ml
index e803c49c..ea4ab23f 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -55,7 +55,7 @@ let () =
   expressions_log#set_level EL.Debug;
   expansion_log#set_level EL.Debug;
   borrows_log#set_level EL.Debug;
-  invariants_log#set_level EL.Debug;
+  invariants_log#set_level EL.Warning;
   (* Load the module *)
   let json = Yojson.Basic.from_file !filename in
   match cfim_module_of_json json with
-- 
cgit v1.2.3