Fix various issues

5 files changed, 22 insertions, 5 deletions

diff --git a/TODO.md b/TODO.md
index 1632a3ca..b9ae7934 100644
--- a/TODO.md
+++ b/TODO.md
@@ -56,6 +56,13 @@
   Then, once we collected all the borrows, we would convert it to:
   `AEndedProjLoans of (mvalue * aproj) list`
   If the list is empty, it means the value was not modified.
+
+9. The way we currently give back symbolic values to symbolic values (inside
+   abstractions) is wrong.
+   We get things like :
+   `AProjLoans (s0 <: &'a mut T) [AProjBorrows (s1 <: &'a mut T)]`
+   while in the case of `s1` we should ignore the outer borrow (we
+   gave back something because this borrow ended...).
   
 * write a function to check that the code we are about to synthesize is in the proper
   subset. In particular:
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