From 2ee5357216cc5a620dbe6d091b0081d419951a4e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 13:55:16 +0100 Subject: Make more modifications to logging --- src/Interpreter.ml | 7 +++++-- src/InterpreterBorrows.ml | 2 +- src/InterpreterPaths.ml | 11 +++++++---- src/InterpreterStatements.ml | 15 +++++++++------ src/Logging.ml | 12 ++++++++---- src/main.ml | 7 +++++-- 6 files changed, 35 insertions(+), 19 deletions(-) diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 9ac8149b..b938fe90 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -21,6 +21,9 @@ open InterpreterStatements (* TODO: remove the config parameters when they are useless *) +(** The local logger *) +let log = L.interpreter_log + module Test = struct let initialize_context (type_context : C.type_context) (fun_defs : A.fun_def list) (type_vars : T.type_var list) : C.eval_ctx = @@ -126,7 +129,7 @@ module Test = struct let fdef = A.FunDefId.nth fun_defs fid in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("test_unit_function: " ^ Print.Types.name_to_string fdef.A.name)); (* Sanity check - *) @@ -177,7 +180,7 @@ module Test = struct let fdef = A.FunDefId.nth fun_defs fid in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("test_function_symbolic: " ^ Print.Types.name_to_string fdef.A.name)); diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index b52454b1..c651e2f1 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -1130,7 +1130,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) | None -> (* No loan to end inside the value *) (* Some sanity checks *) - L.log#ldebug + log#ldebug (lazy ("activate_inactivated_mut_borrow: resulting value:\n" ^ V.show_typed_value sv)); diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 07c615a0..491e4c21 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -12,6 +12,9 @@ open InterpreterBorrowsCore open InterpreterBorrows open InterpreterExpansion +(** The local logger *) +let log = L.paths_log + (** Paths *) (** When we fail reading from or writing to a path, it might be because we @@ -76,7 +79,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) let nv = update v in (* Type checking *) if nv.ty <> v.ty then ( - L.log#lerror + log#lerror (lazy ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: " ^ T.show_ety v.ty)); @@ -244,7 +247,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) let pe = "- pe: " ^ E.show_projection_elem pe in let v = "- v:\n" ^ V.show_value v in let ty = "- ty:\n" ^ T.show_ety ty in - L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); + log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); failwith "Inconsistent projection") (** Generic function to access (read/write) the value at a given place. @@ -314,7 +317,7 @@ let read_place (config : C.config) (access : access_kind) (p : E.place) ^ C.show_env ctx1.env ^ "\n\nOld environment:\n" ^ C.show_env ctx.env in - L.log#serror msg; + log#serror msg; failwith "Unexpected environment update"); Ok read_value @@ -402,7 +405,7 @@ let expand_bottom_value_from_projection (config : C.config) (access : access_kind) (p : E.place) (remaining_pes : int) (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx = (* Debugging *) - L.log#ldebug + log#ldebug (lazy ("expand_bottom_value_from_projection:\n" ^ "pe: " ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty)); diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 82f95556..03940bb7 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -15,13 +15,16 @@ open InterpreterExpansion open InterpreterPaths open InterpreterExpressions +(** The local logger *) +let log = L.statements_log + (** Result of evaluating a statement *) type statement_eval_res = Unit | Break of int | Continue of int | Return (** Drop a value at a given place *) let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx = - L.log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); + log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); (* Prepare the place (by ending the loans, then the borrows) *) let ctx, v = prepare_lplace config p ctx in (* Replace the value with [Bottom] *) @@ -167,7 +170,7 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id) let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = (* Debug *) - L.log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx)); + log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx)); (* Eval *) let ret_vid = V.VarId.zero in (* List the local variables, but the return variable *) @@ -182,7 +185,7 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : in let locals = list_locals ctx.env in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("ctx_pop_frame: locals to drop: [" ^ String.concat "," (List.map V.VarId.to_string locals) @@ -194,7 +197,7 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : ctx locals in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("ctx_pop_frame: after dropping local variables:\n" ^ eval_ctx_to_string ctx)); @@ -514,7 +517,7 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) : (C.eval_ctx * statement_eval_res) eval_result list = (* Debugging *) - L.log#ldebug + log#ldebug (lazy ("\n**About to evaluate statement**: [\n" ^ statement_to_string_with_tab ctx st @@ -909,7 +912,7 @@ and eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : C.eval_ctx eval_result = (* Debug *) - L.log#ldebug + log#ldebug (lazy (let type_params = "[" diff --git a/src/Logging.ml b/src/Logging.ml index 2759854c..36ede236 100644 --- a/src/Logging.ml +++ b/src/Logging.ml @@ -4,7 +4,7 @@ module L = Easy_logging.Logging let _ = L.make_logger "MainLogger" Debug [ Cli Debug ] (** The main logger *) -let log = L.get_logger "MainLogger" +let main_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 *) @@ -18,6 +18,9 @@ let statements_log = L.get_logger "MainLogger.Interpreter.Statements" (** Logger for InterpreterExpressions *) let expressions_log = L.get_logger "MainLogger.Interpreter.Expressions" +(** Logger for InterpreterPaths *) +let paths_log = L.get_logger "MainLogger.Interpreter.Paths" + (** Logger for InterpreterExpansion *) let expansion_log = L.get_logger "MainLogger.Interpreter.Expansion" @@ -131,7 +134,7 @@ let format_tags (tags : string list) = "[" ^ elems_str ^ "] " (* Change the formatters *) -let _ = +let main_logger_handler = (* TODO: comes from easy_logging *) let formatter (item : L.log_item) : string = let item_level_fmt = @@ -147,5 +150,6 @@ let _ = item_msg_fmt in (* There should be exactly one handler *) - let handlers = log#get_handlers in - List.map (fun h -> H.set_formatter h formatter) handlers + let handlers = main_log#get_handlers in + List.iter (fun h -> H.set_formatter h formatter) handlers; + match handlers with [ handler ] -> handler | _ -> failwith "Unexpected" diff --git a/src/main.ml b/src/main.ml index da1b333e..da0b4a0a 100644 --- a/src/main.ml +++ b/src/main.ml @@ -42,6 +42,9 @@ let () = exit 1); (* Set up the logging - for now we use default values - TODO: use the * command-line arguments *) + Easy_logging.Handlers.set_level main_logger_handler EL.Debug; + main_log#set_level EL.Debug; + interpreter_log#set_level EL.Debug; statements_log#set_level EL.Debug; expressions_log#set_level EL.Warning; expansion_log#set_level EL.Debug; @@ -50,10 +53,10 @@ let () = (* Load the module *) let json = Yojson.Basic.from_file !filename in match cfim_module_of_json json with - | Error s -> log#error "error: %s\n" s + | Error s -> main_log#error "error: %s\n" s | Ok m -> (* Print the module *) - log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n")); + main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n")); (* Test the unit functions with the concrete interpreter *) I.Test.test_unit_functions m.types m.functions; -- cgit v1.2.3