From e41b8da810b80a3e42bd5289dedfdb7bf2f10550 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 7 Jan 2022 11:06:56 +0100
Subject: Make more improvements to logging

---
 src/Invariants.ml | 42 +++++++++++++++++++++---------------------
 src/Logging.ml    | 13 ++++++++++---
 src/main.ml       |  1 +
 3 files changed, 32 insertions(+), 24 deletions(-)

diff --git a/src/Invariants.ml b/src/Invariants.ml
index e214e820..65a74c31 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -12,7 +12,8 @@ open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
 
-let debug_invariants : bool ref = ref false
+(** The local logger *)
+let log = L.invariants_log
 
 type borrow_info = {
   loan_kind : T.ref_kind;
@@ -36,19 +37,23 @@ 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 *)
-let ids_reprs_to_string (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
+let ids_reprs_to_string (indent : string)
+    (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
   let bindings = V.BorrowId.Map.bindings reprs in
   let bindings =
     List.map
       (fun (id, repr_id) ->
-        V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id)
+        indent ^ V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id)
       bindings
   in
   String.concat "\n" bindings
 
-let borrows_infos_to_string (infos : borrow_info V.BorrowId.Map.t) : string =
+let borrows_infos_to_string (indent : string)
+    (infos : borrow_info V.BorrowId.Map.t) : string =
   let bindings = V.BorrowId.Map.bindings infos in
-  let bindings = List.map (fun (_, info) -> show_borrow_info info) bindings in
+  let bindings =
+    List.map (fun (_, info) -> indent ^ show_borrow_info info) bindings
+  in
   String.concat "\n" bindings
 
 type borrow_kind = Mut | Shared | Inactivated
@@ -67,8 +72,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
   let borrows_infos : borrow_info V.BorrowId.Map.t ref =
     ref V.BorrowId.Map.empty
   in
+  let context_to_string () : string =
+    eval_ctx_to_string ctx ^ "- representants:\n"
+    ^ ids_reprs_to_string "  " !ids_reprs
+    ^ "\n- info:\n"
+    ^ borrows_infos_to_string "  " !borrows_infos
+  in
 
-  (* First, register all the loans *)
+  (* first, register all the loans *)
   (* Some utilities to register the loans *)
   let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.set_t) : unit
       =
@@ -178,13 +189,9 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     | None ->
         let err =
           "find_info: could not find the representant of borrow "
-          ^ V.BorrowId.to_string bid ^ "\n" ^ "\n- Context:\n"
-          ^ eval_ctx_to_string ctx ^ "\n- representants:\n"
-          ^ ids_reprs_to_string !ids_reprs
-          ^ "\n- info:\n"
-          ^ borrows_infos_to_string !borrows_infos
+          ^ V.BorrowId.to_string bid ^ "\n" ^ context_to_string ()
         in
-        L.log#serror err;
+        log#serror err;
         failwith err
   in
 
@@ -259,15 +266,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
   borrows_visitor#visit_eval_ctx () ctx;
 
   (* Debugging *)
-  if !debug_invariants then (
-    L.log#ldebug
-      (lazy
-        ("\nAbout to check context invariant:\n" ^ eval_ctx_to_string ctx ^ "\n"));
-    L.log#ldebug
-      (lazy
-        ("\nBorrows information:\n"
-        ^ borrows_infos_to_string !borrows_infos
-        ^ "\n")));
+  log#ldebug
+    (lazy ("\nAbout to check context invariant:\n" ^ context_to_string ()));
 
   (* Finally, check that everything is consistant *)
   V.BorrowId.Map.iter
diff --git a/src/Logging.ml b/src/Logging.ml
index ccf63d0d..b0eeadb7 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -9,14 +9,21 @@ let log = L.get_logger "MainLogger"
 (** Below, we create subgloggers for various submodules, so that we can precisely
     toggle logging on/off, depending on which information we need *)
 
+(** Logger for Interpreter *)
+let interpreter_log = L.get_logger "MainLogger.Interpreter"
+
 (** Logger for InterpreterStatements *)
-let statements_log = L.get_logger "MainLogger.Statements"
+let statements_log = L.get_logger "MainLogger.Interpreter.Statements"
 
 (** Logger for InterpreterExpansion *)
-let expansion_log = L.get_logger "MainLogger.Statements.Expansion"
+let expansion_log = L.get_logger "MainLogger.Interpreter.Statements.Expansion"
 
 (** Logger for InterpreterExpressions *)
-let expressions_log = L.get_logger "MainLogger.Statements.Expressions"
+let expressions_log =
+  L.get_logger "MainLogger.Interpreter.Statements.Expressions"
+
+(** Logger for Invariants *)
+let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants"
 
 (** Terminal colors - TODO: comes from easy_logging (did not manage to reuse the module directly) *)
 type color =
diff --git a/src/main.ml b/src/main.ml
index 326ba08e..b151cce7 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -45,6 +45,7 @@ let () =
   statements_log#set_level EL.Debug;
   expansion_log#set_level EL.Debug;
   expressions_log#set_level EL.Warning;
+  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