Add logging information for borrows

5 files changed, 40 insertions, 7 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 1dd4d247..c9637f46 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -743,12 +743,30 @@ and end_borrows (config : C.config) (io : inner_outer)
 
 and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id)
     (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Remember the original context for printing purposes *)
+  let ctx0 = ctx in
+  log#ldebug
+    (lazy
+      ("end_abstraction: "
+      ^ V.AbstractionId.to_string abs_id
+      ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0));
   (* Lookup the abstraction *)
   let abs = C.ctx_lookup_abs ctx abs_id in
   (* End the parent abstractions first *)
   let ctx = end_abstractions config abs.parents ctx in
+  log#ldebug
+    (lazy
+      ("end_abstraction: "
+      ^ V.AbstractionId.to_string abs_id
+      ^ "\n- context after parent abstractions ended:\n"
+      ^ eval_ctx_to_string ctx));
   (* End the loans inside the abstraction *)
   let ctx = end_abstraction_loans config abs_id ctx in
+  log#ldebug
+    (lazy
+      ("end_abstraction: "
+      ^ V.AbstractionId.to_string abs_id
+      ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx));
   (* End the abstraction itself by redistributing the borrows it contains *)
   let ctx = end_abstraction_borrows config abs_id ctx in
   (* End the regions owned by the abstraction - note that we don't need to
@@ -762,7 +780,16 @@ and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id)
   in
   (* Remove all the references to the id of the current abstraction, and remove
    * the abstraction itself *)
-  end_abstraction_remove_from_context config abs_id ctx
+  let ctx = end_abstraction_remove_from_context config abs_id ctx in
+  (* Debugging *)
+  log#ldebug
+    (lazy
+      ("end_abstraction: "
+      ^ V.AbstractionId.to_string abs_id
+      ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0
+      ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx));
+  (* Return *)
+  ctx
 
 and end_abstractions (config : C.config) (abs_ids : V.AbstractionId.set_t)
     (ctx : C.eval_ctx) : C.eval_ctx =
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index bc2f5971..aaab18cb 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -9,6 +9,9 @@ module Subst = Substitute
 module L = Logging
 open InterpreterUtils
 
+(** The local logger *)
+let log = L.borrows_log
+
 (** TODO: cleanup this a bit, once we have a better understanding about
     what we need.
     TODO: I'm not sure in which file this should be moved... *)
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 65a74c31..3c5d24e3 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -36,7 +36,7 @@ let set_outer_mut (info : outer_borrow_info) : outer_borrow_info =
 let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info =
   { outer_borrow = true; outer_shared = true }
 
-(* TODO: we need to factorize print functions for strings *)
+(* TODO: we need to factorize print functions for sets *)
 let ids_reprs_to_string (indent : string)
     (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
   let bindings = V.BorrowId.Map.bindings reprs in
diff --git a/src/Logging.ml b/src/Logging.ml
index b0eeadb7..2759854c 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -15,12 +15,14 @@ let interpreter_log = L.get_logger "MainLogger.Interpreter"
 (** Logger for InterpreterStatements *)
 let statements_log = L.get_logger "MainLogger.Interpreter.Statements"
 
+(** Logger for InterpreterExpressions *)
+let expressions_log = L.get_logger "MainLogger.Interpreter.Expressions"
+
 (** Logger for InterpreterExpansion *)
-let expansion_log = L.get_logger "MainLogger.Interpreter.Statements.Expansion"
+let expansion_log = L.get_logger "MainLogger.Interpreter.Expansion"
 
-(** Logger for InterpreterExpressions *)
-let expressions_log =
-  L.get_logger "MainLogger.Interpreter.Statements.Expressions"
+(** Logger for InterpreterBorrows *)
+let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"
 
 (** Logger for Invariants *)
 let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants"
diff --git a/src/main.ml b/src/main.ml
index b151cce7..da1b333e 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -43,8 +43,9 @@ let () =
   (* Set up the logging - for now we use default values - TODO: use the
    * command-line arguments *)
   statements_log#set_level EL.Debug;
-  expansion_log#set_level EL.Debug;
   expressions_log#set_level EL.Warning;
+  expansion_log#set_level EL.Debug;
+  borrows_log#set_level EL.Debug;
   invariants_log#set_level EL.Warning;
   (* Load the module *)
   let json = Yojson.Basic.from_file !filename in