diff options
| -rw-r--r-- | src/Invariants.ml | 42 | ||||
| -rw-r--r-- | src/Logging.ml | 13 | ||||
| -rw-r--r-- | 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 |