summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Interpreter.ml7
-rw-r--r--src/InterpreterBorrows.ml2
-rw-r--r--src/InterpreterPaths.ml11
-rw-r--r--src/InterpreterStatements.ml15
-rw-r--r--src/Logging.ml12
-rw-r--r--src/main.ml7
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 02:33:42 +0000