summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-07 11:06:56 +0100
committerSon Ho2022-01-07 11:06:56 +0100
commite41b8da810b80a3e42bd5289dedfdb7bf2f10550 (patch)
tree97f11203888cd10e3e7debddcbe019e020170a43 /src
parentdbbb01630190d999d3932fabd8a181b4f826f64f (diff)
Make more improvements to logging
Diffstat (limited to '')
-rw-r--r--src/Invariants.ml42
-rw-r--r--src/Logging.ml13
-rw-r--r--src/main.ml1
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