diff options
| -rw-r--r-- | src/InterpreterBorrows.ml | 29 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 3 | ||||
| -rw-r--r-- | src/Invariants.ml | 2 | ||||
| -rw-r--r-- | src/Logging.ml | 10 | ||||
| -rw-r--r-- | src/main.ml | 3 |
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 |