From b1105c75ea54f38155ca86c62711082ce0bc325d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jan 2022 23:20:54 +0100
Subject: Fix various issues

---
 src/InterpreterBorrows.ml |  1 +
 src/Invariants.ml         | 11 ++++++++++-
 src/Print.ml              |  4 ++--
 src/main.ml               |  4 ++--
 4 files changed, 15 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index b231722d..d2964c90 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -454,6 +454,7 @@ let give_back_symbolic_value (_config : C.config)
           V.AProjBorrows (nsv, sv.V.sv_ty)
       | _ -> failwith "Unreachable"
     in
+    (* TODO: this actually doesn't work, or at least there is something subtle... *)
     V.AProjLoans (sv, (mv, child_proj) :: local_given_back)
   in
   update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx
diff --git a/src/Invariants.ml b/src/Invariants.ml
index ee58a1a3..2d26404d 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -595,13 +595,22 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.ASymbolic aproj, ty -> (
             let ty1 = Subst.erase_regions ty in
             match aproj with
-            | V.AProjLoans (sv, _) | V.AProjBorrows (sv, _) ->
+            | V.AProjLoans (sv, _) ->
                 let ty2 = Subst.erase_regions sv.V.sv_ty in
                 assert (ty1 = ty2);
                 (* Also check that the symbolic values contain regions of interest -
                  * otherwise they should have been reduced to `_` *)
                 let abs = Option.get info in
+                log#ldebug (lazy (symbolic_value_to_string ctx sv));
                 assert (ty_has_regions_in_set abs.regions sv.V.sv_ty)
+            | V.AProjBorrows (sv, proj_ty) ->
+                let ty2 = Subst.erase_regions sv.V.sv_ty in
+                assert (ty1 = ty2);
+                (* Also check that the symbolic values contain regions of interest -
+                 * otherwise they should have been reduced to `_` *)
+                let abs = Option.get info in
+                log#ldebug (lazy (symbolic_value_to_string ctx sv));
+                assert (ty_has_regions_in_set abs.regions proj_ty)
             | V.AEndedProjLoans (_msv, given_back_ls) ->
                 List.iter
                   (fun (_, proj) ->
diff --git a/src/Print.ml b/src/Print.ml
index da6158b5..e1834ca6 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -317,9 +317,9 @@ module Values = struct
             let given_back = List.map (aproj_to_string fmt) given_back in
             " (" ^ String.concat "," given_back ^ ") "
         in
-        "["
+        "⌊"
         ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv
-        ^ given_back ^ "]"
+        ^ given_back ^ "⌋"
     | AProjBorrows (sv, rty) ->
         "(" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
     | AEndedProjLoans (_, given_back) ->
diff --git a/src/main.ml b/src/main.ml
index 2e1e552e..e803c49c 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.Warning;
+  invariants_log#set_level EL.Debug;
   (* Load the module *)
   let json = Yojson.Basic.from_file !filename in
   match cfim_module_of_json json with
@@ -68,7 +68,7 @@ let () =
       let config =
         {
           C.check_invariants = true;
-          greedy_expand_symbolics_with_borrows = false;
+          greedy_expand_symbolics_with_borrows = true;
         }
       in
 
-- 
cgit v1.2.3