From b1e37704aefc4d657c21fc746163c5f05fcca935 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 13:52:56 +0200 Subject: [PATCH 01/39] Add Logs prototype --- src/util/logs.ml | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 src/util/logs.ml diff --git a/src/util/logs.ml b/src/util/logs.ml new file mode 100644 index 0000000000..14bdbb86f2 --- /dev/null +++ b/src/util/logs.ml @@ -0,0 +1,46 @@ +module Pretty = GoblintCil.Pretty + +module type Kind = +sig + type b + type c + val log: ('a, b, c, unit) format4 -> 'a +end + +module PrettyKind = +struct + type b = unit + type c = Pretty.doc + let log fmt = + (* Pretty.eprintf returns doc instead of unit *) + let finish doc = + Pretty.fprint stderr ~width:max_int doc + in + Pretty.gprintf finish fmt +end + +module FormatKind = +struct + type b = Format.formatter + type c = unit + let log fmt = + Format.eprintf fmt +end + + +module MakeKind (Kind: Kind) = +struct + open Kind + + let log = log + + let debug = log + let info = log + let warn = log + let error = log +end + +module Pretty = MakeKind (PrettyKind) +module Format = MakeKind (FormatKind) + +include Pretty (* current default *) From f7d2d5b9b0195645ffde39ffd1cba31ed206f8b7 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 14:01:49 +0200 Subject: [PATCH 02/39] Add semgrep rule for printing --- .semgrep/logs.yml | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 .semgrep/logs.yml diff --git a/.semgrep/logs.yml b/.semgrep/logs.yml new file mode 100644 index 0000000000..e2f6aa2adf --- /dev/null +++ b/.semgrep/logs.yml @@ -0,0 +1,22 @@ +rules: + - id: print-not-logging + pattern-either: + - pattern: printf + - pattern: Printf.printf + - pattern: BatPrintf.printf + - pattern: Format.printf + - pattern: Pretty.printf + + - pattern: eprintf + - pattern: Printf.eprintf + - pattern: BatPrintf.eprintf + - pattern: Format.eprintf + - pattern: Pretty.eprintf + + - pattern: print_endline + - pattern: prerr_endline + - pattern: print_newline + - pattern: print_string + message: printing should be replaced with logging + languages: [ocaml] + severity: WARNING From 80125a7f77dac25e8ef197b578bf0791bd211685 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 14:50:14 +0200 Subject: [PATCH 03/39] Start using Logs --- .semgrep/logs.yml | 3 ++ src/analyses/threadId.ml | 12 ++--- src/autoTune.ml | 40 ++++++++--------- src/autoTune0.ml | 20 ++++----- src/framework/constraints.ml | 54 +++++++++++----------- src/framework/control.ml | 20 ++++----- src/incremental/makefileUtil.ml | 12 ++--- src/solvers/generic.ml | 10 ++--- src/solvers/postSolver.ml | 10 ++--- src/solvers/sLR.ml | 8 ++-- src/solvers/sLRphased.ml | 8 ++-- src/solvers/sLRterm.ml | 8 ++-- src/solvers/td3.ml | 60 ++++++++++++------------- src/solvers/topDown_space_cache_term.ml | 10 ++--- src/util/logs.ml | 4 +- src/util/loopUnrolling.ml | 28 ++++++------ 16 files changed, 155 insertions(+), 152 deletions(-) diff --git a/.semgrep/logs.yml b/.semgrep/logs.yml index e2f6aa2adf..07b2b8aa0f 100644 --- a/.semgrep/logs.yml +++ b/.semgrep/logs.yml @@ -17,6 +17,9 @@ rules: - pattern: prerr_endline - pattern: print_newline - pattern: print_string + paths: + exclude: + - bench/ message: printing should be replaced with logging languages: [ocaml] severity: WARNING diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index 970e4a0cd7..30857e781e 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -125,12 +125,12 @@ struct let non_uniques = List.filter_map (fun (a,b) -> if not (Thread.is_unique a) then Some a else None) tids in let uc = List.length uniques in let nc = List.length non_uniques in - Printf.printf "Encountered number of thread IDs (unique): %i (%i)\n" (uc+nc) uc; - Printf.printf "unique: "; - List.iter (fun tid -> Printf.printf " %s " (Thread.show tid)) uniques; - Printf.printf "\nnon-unique: "; - List.iter (fun tid -> Printf.printf " %s " (Thread.show tid)) non_uniques; - Printf.printf "\n" + Logs.debug "Encountered number of thread IDs (unique): %i (%i)\n" (uc+nc) uc; + Logs.debug "unique: "; + List.iter (fun tid -> Logs.debug " %s " (Thread.show tid)) uniques; + Logs.debug "\nnon-unique: "; + List.iter (fun tid -> Logs.debug " %s " (Thread.show tid)) non_uniques; + Logs.debug "\n" let finalize () = if GobConfig.get_bool "dbg.print_tids" then print_tid_info (); diff --git a/src/autoTune.ml b/src/autoTune.ml index c412af061a..469912cbc1 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -70,7 +70,7 @@ let findMallocWrappers () = |> FunctionCallMap.filter (fun f _ -> timesCalled f > 10) |> FunctionCallMap.bindings |> List.map (fun (v,_) -> v.vname) - |> List.iter (fun n -> print_endline ("malloc wrapper: " ^ n); GobConfig.set_auto "ana.malloc.wrappers[+]" n) + |> List.iter (fun n -> Logs.info "malloc wrapper: %s" n; GobConfig.set_auto "ana.malloc.wrappers[+]" n) (*Functions for determining if the congruence analysis should be enabled *) @@ -83,7 +83,7 @@ let rec setCongruenceRecursive fd depth neigbourFunction = fd.svar.vattr <- addAttributes (fd.svar.vattr) [Attr ("goblint_precision",[AStr "congruence"])]; FunctionSet.iter (fun vinfo -> - print_endline (" " ^ vinfo.vname); + Logs.info " %s" vinfo.vname; setCongruenceRecursive (Cilfacade.find_varinfo_fundec vinfo) (depth -1) neigbourFunction ) (FunctionSet.filter (*for extern and builtin functions there is no function definition in CIL*) @@ -129,7 +129,7 @@ let disableIntervalContextsInRecursiveFunctions () = ResettableLazy.force functionCallMaps |> fun (x,_,_) -> x |> FunctionCallMap.iter (fun f set -> (*detect direct recursion and recursion with one indirection*) if FunctionSet.mem f set || (not @@ FunctionSet.disjoint (calledFunctions f) (callingFunctions f)) then ( - print_endline ("function " ^ (f.vname) ^" is recursive, disable interval context"); + Logs.info "function %s is recursive, disable interval context" f.vname; f.vattr <- addAttributes (f.vattr) [Attr ("goblint_context",[AStr "base.no-interval"; AStr "relation.no-context"])]; ) ) @@ -152,8 +152,8 @@ let reduceThreadAnalyses () = | Some args -> match desc.special args with | ThreadCreate _ -> - print_endline @@ "thread created by " ^ var.vname ^ ", called by:"; - FunctionSet.iter ( fun c -> print_endline @@ " " ^ c.vname) callers; + Logs.debug "thread created by %s, called by:" var.vname; + FunctionSet.iter ( fun c -> Logs.debug " %s" c.vname) callers; true | _ -> false ) @@ -162,7 +162,7 @@ let reduceThreadAnalyses () = ) in if not @@ hasThreadCreate () then ( - print_endline @@ "no thread creation -> disabeling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; + Logs.info "no thread creation -> disabeling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses); let disableAnalysis = GobConfig.set_auto "ana.activated[-]" in List.iter disableAnalysis notNeccessaryThreadAnalyses; @@ -172,7 +172,7 @@ let focusOnSpecification () = match Svcomp.Specification.of_option () with | UnreachCall s -> () | NoDataRace -> (*enable all thread analyses*) - print_endline @@ "Specification: NoDataRace -> enabeling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; + Logs.info "Specification: NoDataRace -> enabeling thread analyses \"%s\n" (String.concat ", " notNeccessaryThreadAnalyses); let enableAnalysis = GobConfig.set_auto "ana.activated[+]" in List.iter enableAnalysis notNeccessaryThreadAnalyses; | NoOverflow -> (*We focus on integer analysis*) @@ -322,9 +322,9 @@ let congruenceOption factors file = let cost = (locals + globals) * (factors.instructions / 12) + 5 * factors.functionCalls in let value = 5 * locals + globals in let activate () = - print_endline @@ "Congruence: " ^ string_of_int cost; + Logs.debug "Congruence: %d" cost; set_bool "ana.int.congruence" true; - print_endline "Enabled congruence domain."; + Logs.info "Enabled congruence domain."; in { value; @@ -355,14 +355,14 @@ let apronOctagonOption factors file = let allVars = (selectedGlobals @ selectedLocals) in let cost = (Batteries.Int.pow (locals + globals) 3) * (factors.instructions / 70) in let activateVars () = - print_endline @@ "Octagon: " ^ string_of_int cost; + Logs.debug "Octagon: %d" cost; set_bool "annotation.goblint_relation_track" true; set_string "ana.apron.domain" "octagon"; set_auto "ana.activated[+]" "apron"; set_bool "ana.apron.threshold_widening" true; set_string "ana.apron.threshold_widening_constants" "comparisons"; - print_endline "Enabled octagon domain for:"; - print_endline @@ String.concat ", " @@ List.map (fun info -> info.vname) allVars; + Logs.info "Enabled octagon domain for:"; + Logs.info "%s" @@ String.concat ", " @@ List.map (fun info -> info.vname) allVars; List.iter (fun info -> info.vattr <- addAttribute (Attr("goblint_relation_track",[])) info.vattr) allVars in { @@ -379,10 +379,10 @@ let wideningOption factors file = value = amountConsts * (factors.loops * 5 + factors.controlFlowStatements); cost = cost; activate = fun () -> - print_endline @@ "Widening: " ^ string_of_int cost; + Logs.debug "Widening: %d" cost; set_bool "ana.int.interval_threshold_widening" true; set_string "ana.int.interval_threshold_widening_constants" "comparisons"; - print_endline "Enabled widening thresholds"; + Logs.info "Enabled widening thresholds"; } @@ -402,13 +402,13 @@ let chooseFromOptions costTarget options = let ratio o = Float.of_int o.value /. Float.of_int o.cost in let compareRatio o1 o2 = Float.compare (ratio o1) (ratio o2) in let rec takeFitting remainingTarget options = - if remainingTarget < 0 then (print_endline @@ "Total: " ^ string_of_int (totalTarget - remainingTarget); [] ) else match options with + if remainingTarget < 0 then (Logs.debug "Total: %d" (totalTarget - remainingTarget); [] ) else match options with | o::os -> if o.cost < remainingTarget + costTarget / 20 then (*because we are already estimating, we allow overshooting *) o::takeFitting (remainingTarget - o.cost) os else takeFitting (remainingTarget - o.cost) os - | [] -> print_endline @@ "Total: " ^ string_of_int (totalTarget - remainingTarget); [] + | [] -> Logs.debug "Total: %d" (totalTarget - remainingTarget); [] in takeFitting costTarget @@ List.sort compareRatio options @@ -418,11 +418,11 @@ let chooseConfig file = let factors = collectFactors visitCilFileSameGlobals file in let fileCompplexity = estimateComplexity factors file in - print_endline "Collected factors:"; + Logs.debug "Collected factors:"; printFactors factors; - print_endline ""; - print_endline "Complexity estimates:"; - print_endline @@ "File: " ^ string_of_int fileCompplexity; + Logs.debug ""; + Logs.debug "Complexity estimates:"; + Logs.debug "File: %d" fileCompplexity; if fileCompplexity < totalTarget && isActivated "congruence" then addModAttributes file; diff --git a/src/autoTune0.ml b/src/autoTune0.ml index 27dba37252..60a28c3f26 100644 --- a/src/autoTune0.ml +++ b/src/autoTune0.ml @@ -17,16 +17,16 @@ type complexityFactors = { } let printFactors f = - Printf.printf "functions: %d\n" f.functions; - Printf.printf "functionCalls: %d\n" f.functionCalls; - Printf.printf "loops: %d\n" f.loops; - Printf.printf "loopBreaks: %d\n" f.loopBreaks; - Printf.printf "controlFlowStatements: %d\n" f.controlFlowStatements; - Printf.printf "expressions: %d\n" f.expressions; - Printf.printf "instructions: %d\n" f.instructions; - Printf.printf "integralVars: (%d,%d)\n" (fst f.integralVars) (snd f.integralVars); - Printf.printf "arrayVars: (%d,%d)\n" (fst f.arrayVars) (snd f.arrayVars); - Printf.printf "pointerVars: (%d,%d)\n" (fst f.pointerVars) (snd f.pointerVars); + Logs.debug "functions: %d\n" f.functions; + Logs.debug "functionCalls: %d\n" f.functionCalls; + Logs.debug "loops: %d\n" f.loops; + Logs.debug "loopBreaks: %d\n" f.loopBreaks; + Logs.debug "controlFlowStatements: %d\n" f.controlFlowStatements; + Logs.debug "expressions: %d\n" f.expressions; + Logs.debug "instructions: %d\n" f.instructions; + Logs.debug "integralVars: (%d,%d)\n" (fst f.integralVars) (snd f.integralVars); + Logs.debug "arrayVars: (%d,%d)\n" (fst f.arrayVars) (snd f.arrayVars); + Logs.debug "pointerVars: (%d,%d)\n" (fst f.pointerVars) (snd f.pointerVars); flush stdout; diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 2364234580..5da3fe3507 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -827,25 +827,25 @@ struct | Some {changes; _} -> changes | None -> empty_change_info () in - List.(Printf.printf "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (length c.added) (length c.removed)); + List.(Logs.info "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (length c.added) (length c.removed)); let changed_funs = List.filter_map (function | {old = {def = Some (Fun f); _}; diff = None; _} -> - print_endline ("Completely changed function: " ^ f.svar.vname); + Logs.info "Completely changed function: %s" f.svar.vname; Some f | _ -> None ) c.changed in let part_changed_funs = List.filter_map (function | {old = {def = Some (Fun f); _}; diff = Some nd; _} -> - print_endline ("Partially changed function: " ^ f.svar.vname); + Logs.info "Partially changed function: %s" f.svar.vname; Some (f, nd.primObsoleteNodes, nd.unchangedNodes) | _ -> None ) c.changed in let removed_funs = List.filter_map (function | {def = Some (Fun f); _} -> - print_endline ("Removed function: " ^ f.svar.vname); + Logs.info "Removed function: %s" f.svar.vname; Some f | _ -> None ) c.removed @@ -1352,22 +1352,22 @@ struct f_eq () else if b1 then begin if get_bool "dbg.compare_runs.diff" then - ignore (Pretty.printf "Global %a is more precise using left:\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1)); + Logs.info "Global %a is more precise using left:\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1); f_le () end else if b2 then begin if get_bool "dbg.compare_runs.diff" then - ignore (Pretty.printf "Global %a is more precise using right:\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2)); + Logs.info "Global %a is more precise using right:\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2); f_gr () end else begin if get_bool "dbg.compare_runs.diff" then ( - ignore (Pretty.printf "Global %a is incomparable (diff):\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2)); - ignore (Pretty.printf "Global %a is incomparable (reverse diff):\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1)); + Logs.info "Global %a is incomparable (diff):\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2); + Logs.info "Global %a is incomparable (reverse diff):\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1); ); f_uk () end in GH.iter f g1; - Printf.printf "globals:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\n" !eq !le !gr !uk + Logs.info "globals:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\n" !eq !le !gr !uk let compare_locals h1 h2 = let eq, le, gr, uk = ref 0, ref 0, ref 0, ref 0 in @@ -1380,16 +1380,16 @@ struct incr eq else if b1 then begin if get_bool "dbg.compare_runs.diff" then - ignore (Pretty.printf "%a @@ %a is more precise using left:\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1)); + Logs.info "%a @@ %a is more precise using left:\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1); incr le end else if b2 then begin if get_bool "dbg.compare_runs.diff" then - ignore (Pretty.printf "%a @@ %a is more precise using right:\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2)); + Logs.info "%a @@ %a is more precise using right:\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2); incr gr end else begin if get_bool "dbg.compare_runs.diff" then ( - ignore (Pretty.printf "%a @@ %a is incomparable (diff):\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2)); - ignore (Pretty.printf "%a @@ %a is incomparable (reverse diff):\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1)); + Logs.info "%a @@ %a is incomparable (diff):\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2); + Logs.info "%a @@ %a is incomparable (reverse diff):\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1); ); incr uk end @@ -1399,8 +1399,8 @@ struct let k2 = Set.of_enum @@ PP.keys h2 in let o1 = Set.cardinal @@ Set.diff k1 k2 in let o2 = Set.cardinal @@ Set.diff k2 k1 in - Printf.printf "locals: \tequal = %d\tleft = %d[%d]\tright = %d[%d]\tincomparable = %d\n" !eq !le o1 !gr o2 !uk *) - Printf.printf "locals: \tequal = %d\tleft = %d\tright = %d\tincomparable = %d\n" !eq !le !gr !uk + Logs.info "locals: \tequal = %d\tleft = %d[%d]\tright = %d[%d]\tincomparable = %d\n" !eq !le o1 !gr o2 !uk *) + Logs.info "locals: \tequal = %d\tleft = %d\tright = %d\tincomparable = %d\n" !eq !le !gr !uk let compare_locals_ctx h1 h2 = let eq, le, gr, uk, no2, no1 = ref 0, ref 0, ref 0, ref 0, ref 0, ref 0 in @@ -1417,16 +1417,16 @@ struct f_eq () else if b1 then begin if get_bool "dbg.compare_runs.diff" then - ignore (Pretty.printf "%a is more precise using left:\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1)); + Logs.info "%a is more precise using left:\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1); f_le () end else if b2 then begin if get_bool "dbg.compare_runs.diff" then - ignore (Pretty.printf "%a is more precise using right:\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2)); + Logs.info "%a is more precise using right:\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2); f_gr () end else begin if get_bool "dbg.compare_runs.diff" then ( - ignore (Pretty.printf "%a is incomparable (diff):\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2)); - ignore (Pretty.printf "%a is incomparable (reverse diff):\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1)); + Logs.info "%a is incomparable (diff):\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2); + Logs.info "%a is incomparable (reverse diff):\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1); ); f_uk () end @@ -1440,7 +1440,7 @@ struct (* let k2 = Set.of_enum @@ PP.keys h2 in *) (* let o1 = Set.cardinal @@ Set.diff k1 k2 in *) (* let o2 = Set.cardinal @@ Set.diff k2 k1 in *) - Printf.printf "locals_ctx:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\tno_ctx_in_right = %d\tno_ctx_in_left = %d\n" !eq !le !gr !uk !no2 !no1 + Logs.info "locals_ctx:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\tno_ctx_in_right = %d\tno_ctx_in_left = %d\n" !eq !le !gr !uk !no2 !no1 let compare (name1,name2) (l1,g1) (l2,g2) = let one_ctx (n,_) v h = @@ -1452,7 +1452,7 @@ struct let h2 = PP.create 113 in let _ = LH.fold one_ctx l1 h1 in let _ = LH.fold one_ctx l2 h2 in - Printf.printf "\nComparing GlobConstrSys precision of %s (left) with %s (right):\n" name1 name2; + Logs.info "\nComparing GlobConstrSys precision of %s (left) with %s (right):\n" name1 name2; compare_globals g1 g2; compare_locals h1 h2; compare_locals_ctx l1 l2; @@ -1483,10 +1483,10 @@ struct module Compare = CompareHashtbl (Sys.Var) (Sys.Dom) (VH) let compare (name1, name2) vh1 vh2 = - Printf.printf "\nComparing EqConstrSys precision of %s (left) with %s (right):\n" name1 name2; + Logs.info "\nComparing EqConstrSys precision of %s (left) with %s (right):\n" name1 name2; let verbose = get_bool "dbg.compare_runs.diff" in let (_, msg) = Compare.compare ~verbose ~name1 vh1 ~name2 vh2 in - ignore (Pretty.printf "EqConstrSys comparison summary: %t\n" (fun () -> msg)); + Logs.info "EqConstrSys comparison summary: %t\n" (fun () -> msg); print_newline (); end @@ -1495,10 +1495,10 @@ struct module Compare = CompareHashtbl (GVar) (G) (GH) let compare (name1, name2) vh1 vh2 = - Printf.printf "\nComparing globals precision of %s (left) with %s (right):\n" name1 name2; + Logs.info "\nComparing globals precision of %s (left) with %s (right):\n" name1 name2; let verbose = get_bool "dbg.compare_runs.diff" in let (_, msg) = Compare.compare ~verbose ~name1 vh1 ~name2 vh2 in - ignore (Pretty.printf "Globals comparison summary: %t\n" (fun () -> msg)); + Logs.info "Globals comparison summary: %t\n" (fun () -> msg); print_newline (); end @@ -1524,12 +1524,12 @@ struct nh let compare (name1, name2) vh1 vh2 = - Printf.printf "\nComparing nodes precision of %s (left) with %s (right):\n" name1 name2; + Logs.info "\nComparing nodes precision of %s (left) with %s (right):\n" name1 name2; let vh1' = join_contexts vh1 in let vh2' = join_contexts vh2 in let verbose = get_bool "dbg.compare_runs.diff" in let (_, msg) = Compare.compare ~verbose ~name1 vh1' ~name2 vh2' in - ignore (Pretty.printf "Nodes comparison summary: %t\n" (fun () -> msg)); + Logs.info "Nodes comparison summary: %t\n" (fun () -> msg); print_newline (); end diff --git a/src/framework/control.ml b/src/framework/control.ml index 2d18814ad2..e8dc04388d 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -281,7 +281,7 @@ struct } in let edges = CfgTools.getGlobalInits file in - if (get_bool "dbg.verbose") then print_endline ("Executing "^string_of_int (List.length edges)^" assigns."); + if (get_bool "dbg.verbose") then Logs.debug "Executing %d assigns." (List.length edges); let funs = ref [] in (*let count = ref 0 in*) let transfer_func (st : Spec.D.t) (loc, edge) : Spec.D.t = @@ -348,21 +348,21 @@ struct let test_domain (module D: Lattice.S): unit = let module DP = DomainProperties.All (D) in - ignore (Pretty.printf "domain testing...: %s\n" (D.name ())); + Logs.debug "domain testing...: %s\n" (D.name ()); let errcode = QCheck_base_runner.run_tests DP.tests in if (errcode <> 0) then failwith "domain tests failed" in let _ = if (get_bool "dbg.test.domain") then ( - ignore (Pretty.printf "domain testing analysis...: %s\n" (Spec.name ())); + Logs.debug "domain testing analysis...: %s\n" (Spec.name ()); test_domain (module Spec.D); test_domain (module Spec.G); ) in let startstate, more_funs = - if (get_bool "dbg.verbose") then print_endline ("Initializing "^string_of_int (CfgTools.numGlobals file)^" globals."); + if (get_bool "dbg.verbose") then Logs.debug "Initializing %d globals." (CfgTools.numGlobals file); Timing.wrap "global_inits" do_global_inits file in @@ -456,7 +456,7 @@ struct ) else if compare_runs <> [] then ( match compare_runs with | d1::d2::[] -> (* the directories of the runs *) - if d1 = d2 then print_endline "Beware that you are comparing a run with itself! There should be no differences."; + if d1 = d2 then Logs.warn "Beware that you are comparing a run with itself! There should be no differences."; (* instead of rewriting Compare for EqConstrSys, just transform unmarshaled EqConstrSys solutions to GlobConstrSys soltuions *) let module Splitter = GlobConstrSolFromEqConstrSol (EQSys) (LHT) (GHT) in let module S2 = Splitter.S2 in @@ -503,7 +503,7 @@ struct | None -> None in if get_bool "dbg.verbose" then - print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ "."); + Logs.info "%s" ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ "."); Goblintutil.should_warn := get_string "warn_at" = "early" || gobview; let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global startvars') solver_data in if GobConfig.get_bool "incremental.save" then @@ -518,7 +518,7 @@ struct let warnings = Fpath.(save_run / "warnings.marshalled") in let stats = Fpath.(save_run / "stats.marshalled") in if get_bool "dbg.verbose" then ( - Format.printf "Saving the current configuration to %a, meta-data about this run to %a, and solver statistics to %a\n" Fpath.pp config Fpath.pp meta Fpath.pp solver_stats; + Logs.Format.info "Saving the current configuration to %a, meta-data about this run to %a, and solver statistics to %a\n" Fpath.pp config Fpath.pp meta Fpath.pp solver_stats; ); GobSys.mkdir_or_exists save_run; GobConfig.write_file config; @@ -531,7 +531,7 @@ struct Yojson.Safe.pretty_to_channel (Stdlib.open_out (Fpath.to_string meta)) Meta.json; (* the above is compact, this is pretty-printed *) if gobview then ( if get_bool "dbg.verbose" then ( - Format.printf "Saving the analysis table to %a, the CIL state to %a, the warning table to %a, and the runtime stats to %a\n" Fpath.pp analyses Fpath.pp cil Fpath.pp warnings Fpath.pp stats; + Logs.Format.info "Saving the analysis table to %a, the CIL state to %a, the warning table to %a, and the runtime stats to %a\n" Fpath.pp analyses Fpath.pp cil Fpath.pp warnings Fpath.pp stats; ); Serialize.marshal MCPRegistry.registered_name analyses; Serialize.marshal (file, Cabs2cil.environment) cil; @@ -711,7 +711,7 @@ struct if not (get_bool "server.enabled") then Serialize.Cache.store_data () ); - if get_bool "dbg.verbose" && get_string "result" <> "none" then print_endline ("Generating output: " ^ get_string "result"); + if get_bool "dbg.verbose" && get_string "result" <> "none" then Logs.info "Generating output: %s" (get_string "result"); Timing.wrap "result output" (Result.output (lazy local_xml) gh make_global_fast_xml) file end @@ -739,7 +739,7 @@ let compute_cfg file = (** The main function to perform the selected analyses. *) let analyze change_info (file: file) fs = - if (get_bool "dbg.verbose") then print_endline "Generating the control flow graph."; + if (get_bool "dbg.verbose") then Logs.debug "Generating the control flow graph."; let (module CFG) = compute_cfg file in MyCFG.current_cfg := (module CFG); analyze_loop (module CFG) file fs change_info diff --git a/src/incremental/makefileUtil.ml b/src/incremental/makefileUtil.ml index a262849156..790dbb8677 100644 --- a/src/incremental/makefileUtil.ml +++ b/src/incremental/makefileUtil.ml @@ -14,7 +14,7 @@ let exec_command ?path (command: string) = if Sys.file_exists path_str && Sys.is_directory path_str then Sys.chdir path_str else failwith ("Directory " ^ path_str ^ " does not exist!") | None -> ()); - if GobConfig.get_bool "dbg.verbose" then print_endline ("executing command `" ^ command ^ "` in " ^ Sys.getcwd ()); + if GobConfig.get_bool "dbg.verbose" then Logs.debug "%s" ("executing command `" ^ command ^ "` in " ^ Sys.getcwd ()); let (std_out, std_in) = open_process command in let output = Buffer.create buff_size in try @@ -50,7 +50,7 @@ let remove_comb_files path = try while true do let comb = Fpath.to_string (find_file_by_suffix path comb_suffix) in - if GobConfig.get_bool "dbg.verbose" then print_endline ("deleting " ^ comb); + if GobConfig.get_bool "dbg.verbose" then Logs.info "deleting %s" comb; Sys.remove comb; done with Failure e -> () @@ -66,7 +66,7 @@ let run_cilly (path: Fpath.t) ~all_cppflags = let cflags = if all_cppflags = [] then "" else " CFLAGS+=" ^ Filename.quote (String.join " " all_cppflags) in let (exit_code, output) = exec_command ~path ("make CC=\"cilly --gcc=" ^ gcc_path ^ " --merge --keepmerged\"" ^cflags ^ " " ^ "LD=\"cilly --gcc=" ^ gcc_path ^ " --merge --keepmerged\"") in - print_string output; + Logs.debug "%s" output; (* fail if make failed *) if exit_code <> WEXITED 0 then failwith ("Failed combining files. Make was " ^ (GobUnix.string_of_process_status exit_code) ^ ".") @@ -77,14 +77,14 @@ let generate_and_combine makefile ~all_cppflags = let makefile_str = Fpath.to_string makefile in (* make sure the Makefile exists or try to generate it *) if not (Sys.file_exists makefile_str) then ( - print_endline ("Given " ^ makefile_str ^ " does not exist! Try to generate it."); + Logs.error "Given %s does not exist! Try to generate it." makefile_str; let configure = ("configure", "./configure", Fpath.(path / "configure")) in let autogen = ("autogen", "sh autogen.sh && ./configure", Fpath.(path / "autogen.sh")) in let exception MakefileNotGenerated in let generate_makefile_with (name, command, file) = if Sys.file_exists (Fpath.to_string file) then ( - print_endline ("Trying to run " ^ name ^ " to generate Makefile"); + Logs.debug "Trying to run %s to generate Makefile" name; let exit_code, output = exec_command ~path command in - print_endline (command ^ " " ^ GobUnix.string_of_process_status exit_code ^ ". Output: " ^ output); + Logs.debug "%s" (command ^ " " ^ GobUnix.string_of_process_status exit_code ^ ". Output: " ^ output); if not (Sys.file_exists makefile_str) then raise MakefileNotGenerated ) else raise MakefileNotGenerated in try generate_makefile_with configure diff --git a/src/solvers/generic.ml b/src/solvers/generic.ml index 6dbbb486dd..2ae2c73689 100644 --- a/src/solvers/generic.ml +++ b/src/solvers/generic.ml @@ -96,11 +96,11 @@ struct (* ignore @@ Pretty.printf "max #contexts: %d for %s\n" n max_k; *) ncontexts := Hashtbl.fold (fun _ -> (+)) histo 0; let topn = 5 in - Printf.printf "Found %d contexts for %d functions. Top %d functions:\n" !ncontexts (Hashtbl.length histo) topn; + Logs.debug "Found %d contexts for %d functions. Top %d functions:\n" !ncontexts (Hashtbl.length histo) topn; Hashtbl.to_list histo |> List.sort (fun (_,n1) (_,n2) -> compare n2 n1) |> List.take topn - |> List.iter @@ fun (k,n) -> ignore @@ Pretty.printf "%d\tcontexts for %s\n" n k + |> List.iter @@ fun (k,n) -> Logs.debug "%d\tcontexts for %s\n" n k let stats_csv = let save_run_str = GobConfig.get_string "save_run" in @@ -115,9 +115,9 @@ struct let print_stats _ = print_newline (); (* print_endline "# Generic solver stats"; *) - Printf.printf "runtime: %s\n" (string_of_time ()); - Printf.printf "vars: %d, evals: %d\n" !Goblintutil.vars !Goblintutil.evals; - Option.may (fun v -> ignore @@ Pretty.printf "max updates: %d for var %a\n" !max_c Var.pretty_trace v) !max_var; + Logs.info "runtime: %s\n" (string_of_time ()); + Logs.info "vars: %d, evals: %d\n" !Goblintutil.vars !Goblintutil.evals; + Option.may (fun v -> ignore @@ Logs.info "max updates: %d for var %a\n" !max_c Var.pretty_trace v) !max_var; print_newline (); (* print_endline "# Solver specific stats"; *) !print_solver_stats (); diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml index fbdbc76df7..16cd30652a 100644 --- a/src/solvers/postSolver.ml +++ b/src/solvers/postSolver.ml @@ -62,7 +62,7 @@ module Prune: F = let finalize ~vh ~reachable = if get_bool "dbg.debug" then - print_endline "Pruning result"; + Logs.debug "Pruning result"; VH.filteri_inplace (fun x _ -> VH.mem reachable x @@ -80,11 +80,11 @@ module Verify: F = let complain_constraint x ~lhs ~rhs = Goblintutil.verified := Some false; - ignore (Pretty.printf "Fixpoint not reached at %a\n @[Solver computed:\n%a\nRight-Hand-Side:\n%a\nDifference: %a\n@]" S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs)) + Logs.error "Fixpoint not reached at %a\n @[Solver computed:\n%a\nRight-Hand-Side:\n%a\nDifference: %a\n@]" S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs) let complain_side x y ~lhs ~rhs = Goblintutil.verified := Some false; - ignore (Pretty.printf "Fixpoint not reached at %a\nOrigin: %a\n @[Solver computed:\n%a\nSide-effect:\n%a\nDifference: %a\n@]" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs)) + Logs.error "Fixpoint not reached at %a\nOrigin: %a\n @[Solver computed:\n%a\nSide-effect:\n%a\nDifference: %a\n@]" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs) let one_side ~vh ~x ~y ~d = let y_lhs = try VH.find vh y with Not_found -> S.Dom.bot () in @@ -129,7 +129,7 @@ module SaveRun: F = let save_run = Fpath.v save_run_str in let solver = Fpath.(save_run / solver_file) in if get_bool "dbg.verbose" then - Format.printf "Saving the solver result to %a\n" Fpath.pp solver; + Logs.Format.info "Saving the solver result to %a\n" Fpath.pp solver; GobSys.mkdir_or_exists save_run; Serialize.marshal vh solver end @@ -179,7 +179,7 @@ struct let post xs vs vh = if get_bool "dbg.verbose" then - print_endline "Postsolving\n"; + Logs.debug "Postsolving\n"; let module StartS = struct diff --git a/src/solvers/sLR.ml b/src/solvers/sLR.ml index 6f07f66e8f..243dcaa583 100644 --- a/src/solvers/sLR.ml +++ b/src/solvers/sLR.ml @@ -152,8 +152,8 @@ module SLR3 = stop_event (); if GobConfig.get_bool "dbg.print_wpoints" then ( - Printf.printf "\nWidening points:\n"; - HM.iter (fun k () -> ignore @@ Pretty.printf "%a\n" S.Var.pretty_trace k) wpoint; + Logs.debug "\nWidening points:\n"; + HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; print_newline (); ); @@ -446,8 +446,8 @@ module Make0 = let _ = loop () in if GobConfig.get_bool "dbg.print_wpoints" then ( - Printf.printf "\nWidening points:\n"; - HM.iter (fun k () -> ignore @@ Pretty.printf "%a\n" S.Var.pretty_trace k) wpoint; + Logs.debug "\nWidening points:\n"; + HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; print_newline (); ); diff --git a/src/solvers/sLRphased.ml b/src/solvers/sLRphased.ml index 760b4614d8..441666800b 100644 --- a/src/solvers/sLRphased.ml +++ b/src/solvers/sLRphased.ml @@ -135,10 +135,10 @@ module Make = HM.replace rho0 x d; HM.replace infl x VS.empty; if side then ( - print_endline @@ "Variable by side-effect " ^ S.Var.var_id x ^ " to " ^ string_of_int !count_side; + Logs.debug "%s" @@ "Variable by side-effect " ^ S.Var.var_id x ^ " to " ^ string_of_int !count_side; HM.replace key x !count_side; decr count_side ) else ( - print_endline @@ "Variable " ^ S.Var.var_id x ^ " to " ^ string_of_int !count; + Logs.debug "%s" @@ "Variable " ^ S.Var.var_id x ^ " to " ^ string_of_int !count; HM.replace key x !count; decr count ); do_var false x; @@ -188,8 +188,8 @@ module Make = stop_event (); if GobConfig.get_bool "dbg.print_wpoints" then ( - Printf.printf "\nWidening points:\n"; - HM.iter (fun k () -> ignore @@ Pretty.printf "%a\n" S.Var.pretty_trace k) wpoint; + Logs.debug "\nWidening points:\n"; + HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; print_newline (); ); diff --git a/src/solvers/sLRterm.ml b/src/solvers/sLRterm.ml index 0108af84a1..f709751bb4 100644 --- a/src/solvers/sLRterm.ml +++ b/src/solvers/sLRterm.ml @@ -48,11 +48,11 @@ module SLR3term = let count_side = ref (max_int - 1) in let () = print_solver_stats := fun () -> - Printf.printf "wpoint: %d, rho: %d, rho': %d, q: %d, count: %d, count_side: %d\n" (HM.length wpoint) (HM.length rho) (HPM.length rho') (H.size !q) (Int.neg !count) (max_int - !count_side); + Logs.info "wpoint: %d, rho: %d, rho': %d, q: %d, count: %d, count_side: %d\n" (HM.length wpoint) (HM.length rho) (HPM.length rho') (H.size !q) (Int.neg !count) (max_int - !count_side); let histo = Hashtbl.create 13 in (* histogram: node id -> number of contexts *) HM.iter (fun k _ -> Hashtbl.modify_def 1 (S.Var.var_id k) ((+)1) histo) rho; let vid,n = Hashtbl.fold (fun k v (k',v') -> if v > v' then k,v else k',v') histo (Obj.magic (), 0) in - ignore @@ Pretty.printf "max #contexts: %d for var_id %s\n" n vid + Logs.info "max #contexts: %d for var_id %s\n" n vid in let init ?(side=false) x = @@ -206,8 +206,8 @@ module SLR3term = stop_event (); if GobConfig.get_bool "dbg.print_wpoints" then ( - Printf.printf "\nWidening points:\n"; - HM.iter (fun k () -> ignore @@ Pretty.printf "%a\n" S.Var.pretty_trace k) wpoint; + Logs.debug "\nWidening points:\n"; + HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; print_newline (); ); diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 52915e18e8..c7bca63fea 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -76,7 +76,7 @@ module Base = let print_data data str = if GobConfig.get_bool "dbg.verbose" then ( - Printf.printf "%s:\n|rho|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d\n" + Logs.info "%s:\n|rho|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d\n" str (HM.length data.rho) (HM.length data.stable) (HM.length data.infl) (HM.length data.wpoint) (HM.length data.side_dep) (HM.length data.side_infl) (HM.length data.var_messages) (HM.length data.rho_write) (HM.length data.dep); Hooks.print_data () ) @@ -86,7 +86,7 @@ module Base = (* every variable in (pruned) rho should be stable *) HM.iter (fun x _ -> if not (HM.mem data.stable x) then ( - ignore (Pretty.printf "unstable in rho: %a\n" S.Var.pretty_trace x); + Logs.warn "unstable in rho: %a\n" S.Var.pretty_trace x; assert false ) ) data.rho @@ -193,7 +193,7 @@ module Base = match marshal with | Some data -> if not reuse_stable then ( - print_endline "Destabilizing everything!"; + Logs.info "Destabilizing everything!"; HM.clear data.stable; HM.clear data.infl ); @@ -241,7 +241,7 @@ module Base = let dep = data.dep in let () = print_solver_stats := fun () -> - Printf.printf "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d\n" + Logs.info "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d\n" (HM.length rho) (HM.length called) (HM.length stable) (HM.length infl) (HM.length wpoint) (HM.length side_dep) (HM.length side_infl) (HM.length var_messages) (HM.length rho_write) (HM.length dep); Hooks.print_data (); print_context_stats rho @@ -388,7 +388,7 @@ module Base = and side ?x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *) if tracing then trace "sol2" "side to %a (wpx: %b) from %a ## value: %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d; if Hooks.system y <> None then ( - ignore @@ Pretty.printf "side-effect to unknown w/ rhs: %a, contrib: %a\n" S.Var.pretty_trace y S.Dom.pretty d; + Logs.warn "side-effect to unknown w/ rhs: %a, contrib: %a\n" S.Var.pretty_trace y S.Dom.pretty d; ); assert (Hooks.system y = None); init y; @@ -496,7 +496,7 @@ module Base = let restart_leaf x = if tracing then trace "sol2" "Restarting to bot %a\n" S.Var.pretty_trace x; - ignore (Pretty.printf "Restarting to bot %a\n" S.Var.pretty_trace x); + Logs.debug "Restarting to bot %a\n" S.Var.pretty_trace x; HM.replace rho x (S.Dom.bot ()); (* HM.remove rho x; *) HM.remove wpoint x; (* otherwise gets immediately widened during resolve *) @@ -609,14 +609,14 @@ module Base = ); if sys_change.obsolete <> [] then - print_endline "Destabilizing changed functions and primary old nodes ..."; + Logs.debug "Destabilizing changed functions and primary old nodes ..."; List.iter (fun k -> if HM.mem stable k then destabilize k ) sys_change.obsolete; (* We remove all unknowns for program points in changed or removed functions from rho, stable, infl and wpoint *) - print_endline "Removing data for changed and removed functions..."; + Logs.debug "Removing data for changed and removed functions..."; let delete_marked s = List.iter (fun k -> HM.remove s k) sys_change.delete in delete_marked rho; delete_marked infl; (* TODO: delete from inner sets? *) @@ -627,10 +627,10 @@ module Base = (* destabilize_with_side doesn't have all infl to follow anymore, so should somewhat work with reluctant *) if restart_sided then ( (* restarts old copies of functions and their (removed) side effects *) - print_endline "Destabilizing sides of changed functions, primary old nodes and removed functions ..."; + Logs.debug "Destabilizing sides of changed functions, primary old nodes and removed functions ..."; List.iter (fun k -> if HM.mem stable k then ( - ignore (Pretty.printf "marked %a\n" S.Var.pretty_trace k); + Logs.debug "marked %a\n" S.Var.pretty_trace k; destabilize k ) ) sys_change.delete @@ -662,7 +662,7 @@ module Base = List.iter (fun v -> if Hooks.system v <> None then - ignore @@ Pretty.printf "Trying to restart non-leaf unknown %a. This has no effect.\n" S.Var.pretty_trace v + Logs.warn "Trying to restart non-leaf unknown %a. This has no effect.\n" S.Var.pretty_trace v else if HM.mem stable v then destabilize_leaf v ) sys_change.restart; @@ -681,7 +681,7 @@ module Base = if should_restart_start then ( match GobList.assoc_eq_opt S.Var.equal v data.st with | Some old_d when not (S.Dom.equal old_d d) -> - ignore (Pretty.printf "Destabilizing and restarting changed start var %a\n" S.Var.pretty_trace v); + Logs.debug "Destabilizing and restarting changed start var %a\n" S.Var.pretty_trace v; restart_and_destabilize v (* restart side effect from start *) | _ -> (* don't restart unchanged start global *) @@ -698,7 +698,7 @@ module Base = | None -> (* restart removed start global to allow it to be pruned from incremental solution *) (* this gets rid of its warnings and makes comparing with from scratch sensible *) - ignore (Pretty.printf "Destabilizing and restarting removed start var %a\n" S.Var.pretty_trace v); + Logs.debug "Destabilizing and restarting removed start var %a\n" S.Var.pretty_trace v; restart_and_destabilize v | _ -> () @@ -718,7 +718,7 @@ module Base = (* before delete_marked because we also want to restart write-only side effects from deleted nodes *) HM.iter (fun x w -> HM.iter (fun y d -> - ignore (Pretty.printf "Restarting write-only to bot %a\n" S.Var.pretty_trace y); + Logs.debug "Restarting write-only to bot %a\n" S.Var.pretty_trace y; HM.replace rho y (S.Dom.bot ()); ) w ) rho_write @@ -732,21 +732,21 @@ module Base = if reluctant then ( (* solve on the return node of changed functions. Only destabilize the function's return node if the analysis result changed *) - print_endline "Separately solving changed functions..."; + Logs.debug "Separately solving changed functions..."; HM.iter (fun x (old_rho, old_infl) -> HM.replace rho x old_rho; HM.replace infl x old_infl) old_ret; HM.iter (fun x (old_rho, old_infl) -> - ignore @@ Pretty.printf "test for %a\n" Node.pretty_trace (S.Var.node x); + Logs.debug "test for %a\n" Node.pretty_trace (S.Var.node x); solve x Widen; if not (S.Dom.equal (HM.find rho x) old_rho) then ( - print_endline "Further destabilization happened ..."; + Logs.debug "Further destabilization happened ..."; ) else ( - print_endline "Destabilization not required..."; + Logs.debug "Destabilization not required..."; reluctant_vs := x :: !reluctant_vs ) ) old_ret; - print_endline "Final solve..." + Logs.debug "Final solve..." ); ) else ( List.iter set_start st; @@ -763,8 +763,8 @@ module Base = if unstable_vs <> [] then ( if GobConfig.get_bool "dbg.verbose" then ( if !i = 1 then print_newline (); - Printf.printf "Unstable solver start vars in %d. phase:\n" !i; - List.iter (fun v -> ignore @@ Pretty.printf "\t%a\n" S.Var.pretty_trace v) unstable_vs; + Logs.debug "Unstable solver start vars in %d. phase:\n" !i; + List.iter (fun v -> Logs.debug "\t%a\n" S.Var.pretty_trace v) unstable_vs; print_newline (); flush_all (); ); @@ -784,12 +784,12 @@ module Base = HM.replace visited y (); let mem = HM.mem rho y in let d' = try HM.find rho y with Not_found -> S.Dom.bot () in - if not (S.Dom.leq d d') then ignore @@ Pretty.printf "TDFP Fixpoint not reached in restore step at side-effected variable (mem: %b) %a from %a: %a not leq %a\n" mem S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d S.Dom.pretty d' + if not (S.Dom.leq d d') then Logs.error "TDFP Fixpoint not reached in restore step at side-effected variable (mem: %b) %a from %a: %a not leq %a\n" mem S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d S.Dom.pretty d' in let rec eq check x = HM.replace visited x (); match Hooks.system x with - | None -> if HM.mem rho x then HM.find rho x else (ignore @@ Pretty.printf "TDFP Found variable %a w/o rhs and w/o value in rho\n" S.Var.pretty_trace x; S.Dom.bot ()) + | None -> if HM.mem rho x then HM.find rho x else (Logs.warn "TDFP Found variable %a w/o rhs and w/o value in rho\n" S.Var.pretty_trace x; S.Dom.bot ()) | Some f -> f (get ~check) (check_side x) and get ?(check=false) x = if HM.mem visited x then ( @@ -798,9 +798,9 @@ module Base = let d1 = HM.find rho x in let d2 = eq check x in (* just to reach unrestored variables *) if check then ( - if not (HM.mem stable x) && Hooks.system x <> None then ignore @@ Pretty.printf "TDFP Found an unknown in rho that should be stable: %a\n" S.Var.pretty_trace x; + if not (HM.mem stable x) && Hooks.system x <> None then Logs.error "TDFP Found an unknown in rho that should be stable: %a\n" S.Var.pretty_trace x; if not (S.Dom.leq d2 d1) then - ignore @@ Pretty.printf "TDFP Fixpoint not reached in restore step at %a\n @[Variable:\n%a\nRight-Hand-Side:\n%a\nCalculating one more step changes: %a\n@]" S.Var.pretty_trace x S.Dom.pretty d1 S.Dom.pretty d2 S.Dom.pretty_diff (d1,d2); + Logs.error "TDFP Fixpoint not reached in restore step at %a\n @[Variable:\n%a\nRight-Hand-Side:\n%a\nCalculating one more step changes: %a\n@]" S.Var.pretty_trace x S.Dom.pretty d1 S.Dom.pretty d2 S.Dom.pretty_diff (d1,d2); ); d1 ) else ( @@ -812,7 +812,7 @@ module Base = (* restore values for non-widening-points *) if space && GobConfig.get_bool "solvers.td3.space_restore" then ( if GobConfig.get_bool "dbg.verbose" then - print_endline ("Restoring missing values."); + Logs.debug "Restoring missing values."; let restore () = let get x = let d = get ~check:true x in @@ -822,7 +822,7 @@ module Base = HM.filteri_inplace (fun x _ -> HM.mem visited x) rho in Timing.wrap "restore" restore (); - if GobConfig.get_bool "dbg.verbose" then ignore @@ Pretty.printf "Solved %d vars. Total of %d vars after restore.\n" !Goblintutil.vars (HM.length rho); + if GobConfig.get_bool "dbg.verbose" then Logs.debug "Solved %d vars. Total of %d vars after restore.\n" !Goblintutil.vars (HM.length rho); let avg xs = if List.is_empty !cache_sizes then 0.0 else float_of_int (BatList.sum xs) /. float_of_int (List.length xs) in if tracing then trace "cache" "#caches: %d, max: %d, avg: %.2f\n" (List.length !cache_sizes) (List.max !cache_sizes) (avg !cache_sizes); ); @@ -831,8 +831,8 @@ module Base = print_data data "Data after solve completed"; if GobConfig.get_bool "dbg.print_wpoints" then ( - Printf.printf "\nWidening points:\n"; - HM.iter (fun k () -> ignore @@ Pretty.printf "%a\n" S.Var.pretty_trace k) wpoint; + Logs.debug "\nWidening points:\n"; + HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; print_newline (); ); @@ -1075,7 +1075,7 @@ module DepVals: GenericEqIncrSolver = module HM = HM let print_data () = - Printf.printf "|dep_vals|=%d\n" (HM.length !current_dep_vals) + Logs.info "|dep_vals|=%d\n" (HM.length !current_dep_vals) let system x = match S.system x with diff --git a/src/solvers/topDown_space_cache_term.ml b/src/solvers/topDown_space_cache_term.ml index 6c0ed9f36b..450235854c 100644 --- a/src/solvers/topDown_space_cache_term.ml +++ b/src/solvers/topDown_space_cache_term.ml @@ -142,7 +142,7 @@ module WP = let rec get x = if HM.mem visited x then ( if not (HM.mem rho x) then ( - ignore @@ Pretty.printf "Found an unknown that should be a widening point: %a\n" S.Var.pretty_trace x; + Logs.warn "Found an unknown that should be a widening point: %a\n" S.Var.pretty_trace x; S.Dom.top () ) else HM.find rho x @@ -150,7 +150,7 @@ module WP = HM.replace visited x (); let check_side y d = let d' = try HM.find rho y with Not_found -> S.Dom.bot () in - if not (S.Dom.leq d d') then ignore @@ Pretty.printf "Fixpoint not reached in restore step at side-effected variable %a: %a not leq %a\n" S.Var.pretty_trace y S.Dom.pretty d S.Dom.pretty d' + if not (S.Dom.leq d d') then Logs.error "Fixpoint not reached in restore step at side-effected variable %a: %a not leq %a\n" S.Var.pretty_trace y S.Dom.pretty d S.Dom.pretty d' in let eq x = match S.system x with @@ -161,7 +161,7 @@ module WP = let d1 = HM.find rho x in let d2 = eq x in if not (S.Dom.leq d2 d1) then - ignore @@ Pretty.printf "Fixpoint not reached in restore step at %a\n @[Variable:\n%a\nRight-Hand-Side:\n%a\nCalculating one more step changes: %a\n@]" S.Var.pretty_trace x S.Dom.pretty d1 S.Dom.pretty d2 S.Dom.pretty_diff (d1,d2); + Logs.error "Fixpoint not reached in restore step at %a\n @[Variable:\n%a\nRight-Hand-Side:\n%a\nCalculating one more step changes: %a\n@]" S.Var.pretty_trace x S.Dom.pretty d1 S.Dom.pretty d2 S.Dom.pretty_diff (d1,d2); d1 ) else ( let d = eq x in @@ -173,7 +173,7 @@ module WP = (* restore values for non-widening-points *) if GobConfig.get_bool "solvers.wp.restore" then ( if (GobConfig.get_bool "dbg.verbose") then - print_endline ("Restoring missing values."); + Logs.debug ("Restoring missing values."); let restore () = let get x = let d = get x in @@ -182,7 +182,7 @@ module WP = List.iter get vs in Timing.wrap "restore" restore (); - if (GobConfig.get_bool "dbg.verbose") then ignore @@ Pretty.printf "Solved %d vars. Total of %d vars after restore.\n" !Goblintutil.vars (HM.length rho); + if (GobConfig.get_bool "dbg.verbose") then Logs.debug "Solved %d vars. Total of %d vars after restore.\n" !Goblintutil.vars (HM.length rho); ); let avg xs = float_of_int (BatList.sum xs) /. float_of_int (List.length xs) in if tracing then trace "cache" "#caches: %d, max: %d, avg: %.2f\n" (List.length !cache_sizes) (List.max !cache_sizes) (avg !cache_sizes); diff --git a/src/util/logs.ml b/src/util/logs.ml index 14bdbb86f2..e9c51d60e6 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -1,5 +1,3 @@ -module Pretty = GoblintCil.Pretty - module type Kind = sig type b @@ -9,6 +7,8 @@ end module PrettyKind = struct + open GoblintCil + type b = unit type c = Pretty.doc let log fmt = diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index b62dec9440..c9fb573b3f 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -152,7 +152,7 @@ let constBefore var loop f = let targetLocation = loopLocation loop in let rec lastAssignmentToVarBeforeLoop (current: (Z.t option)) (statements: stmt list) = match statements with | st::stmts -> ( - let current' = if st.labels <> [] then (print_endline "has Label"; (None)) else current in + let current' = if st.labels <> [] then (Logs.debug "has Label"; (None)) else current in match st.skind with | Instr list -> ( match lastAssignToVar var list with @@ -272,25 +272,25 @@ let fixedLoopSize loopStatement func = else constBefore var loopStatement func >>= fun start -> assignmentDifference loopStatement var >>= fun diff -> - print_endline "comparison: "; + Logs.debug "comparison: "; Pretty.fprint stdout (dn_exp () comparison) ~width:max_int; - print_endline ""; - print_endline "variable: "; - print_endline var.vname; - print_endline "start:"; - print_endline @@ Z.to_string start; - print_endline "diff:"; - print_endline @@ Z.to_string diff; + Logs.debug ""; + Logs.debug "variable: "; + Logs.debug "%s" var.vname; + Logs.debug "start:"; + Logs.debug "%s" @@ Z.to_string start; + Logs.debug "diff:"; + Logs.debug "%s" @@ Z.to_string diff; let iterations = loopIterations start diff comparison in match iterations with - | None -> print_endline "iterations failed"; None + | None -> Logs.debug "iterations failed"; None | Some s -> try let s' = Z.to_int s in - print_endline "iterations:"; - print_endline @@ string_of_int s'; + Logs.debug "iterations:"; + Logs.debug "%d" s'; Some s' - with _ -> print_endline "iterations too big for integer"; None + with _ -> Logs.debug "iterations too big for integer"; None class arrayVisitor = object @@ -350,7 +350,7 @@ let loop_unrolling_factor loopStatement func totalLoops = (* Unroll at least 10 times if there are only few (17?) loops *) let unroll_min = if totalLoops < 17 && AutoTune0.isActivated "forceLoopUnrollForFewLoops" then 10 else 0 in match fixedLoop with - | Some i -> if i * loopStats.instructions < 100 then (print_endline "fixed loop size"; i) else max unroll_min (100 / loopStats.instructions) + | Some i -> if i * loopStats.instructions < 100 then (Logs.debug "fixed loop size"; i) else max unroll_min (100 / loopStats.instructions) | _ -> max unroll_min (targetInstructions / loopStats.instructions) else (* Don't unroll empty (= while(1){}) loops*) From aff84b18250ebd7b110b8179185e23ad0f36ed8d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 15:21:15 +0200 Subject: [PATCH 04/39] Add newline after logging --- src/util/logs.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/util/logs.ml b/src/util/logs.ml index e9c51d60e6..8242bcb878 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -14,7 +14,8 @@ struct let log fmt = (* Pretty.eprintf returns doc instead of unit *) let finish doc = - Pretty.fprint stderr ~width:max_int doc + Pretty.fprint stderr ~width:max_int doc; + prerr_newline () in Pretty.gprintf finish fmt end @@ -24,7 +25,10 @@ struct type b = Format.formatter type c = unit let log fmt = - Format.eprintf fmt + let finish ppf = + Format.fprintf ppf "\n%!" + in + Format.kfprintf finish Format.err_formatter fmt end From 72bf02f0a72ad74117548c2c560317d5a485795a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 15:58:24 +0200 Subject: [PATCH 05/39] Use more Logs --- .semgrep/logs.yml | 1 + src/analyses/apron/relationAnalysis.apron.ml | 2 +- src/analyses/extractPthread.ml | 6 +- src/domains/printable.ml | 4 +- src/framework/analyses.ml | 6 +- src/framework/cfgTools.ml | 2 +- src/goblint.ml | 8 +-- src/maingoblint.ml | 58 ++++++++++---------- src/messagesCompare.ml | 4 +- src/spec/specUtil.ml | 10 ++-- src/transform/expressionEvaluation.ml | 10 ++-- src/transform/transform.ml | 2 +- src/util/backtrace/goblint_backtrace.ml | 2 +- src/util/cilfacade.ml | 6 +- src/util/compilationDatabase.ml | 4 +- src/util/gobConfig.ml | 6 +- src/util/jsonSchema.ml | 4 +- src/util/logs.ml | 12 ++++ src/util/options.ml | 8 +-- src/util/precCompare.ml | 6 +- src/util/preprocessor.ml | 2 +- src/util/tracing.ml | 2 +- src/witness/violation.ml | 6 +- src/witness/witness.ml | 4 +- src/witness/z3/violationZ3.z3.ml | 8 +-- 25 files changed, 98 insertions(+), 85 deletions(-) diff --git a/.semgrep/logs.yml b/.semgrep/logs.yml index 07b2b8aa0f..800e600c8c 100644 --- a/.semgrep/logs.yml +++ b/.semgrep/logs.yml @@ -19,6 +19,7 @@ rules: - pattern: print_string paths: exclude: + - logs.ml - bench/ message: printing should be replaced with logging languages: [ocaml] diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index f30cbeb278..49d4b3ae58 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -709,7 +709,7 @@ struct let finalize () = let file = GobConfig.get_string "exp.relation.prec-dump" in if file <> "" then begin - Printf.printf "exp.relation.prec-dump is potentially costly (for domains other than octagons), do not use for performance data!\n"; + Logs.warn "exp.relation.prec-dump is potentially costly (for domains other than octagons), do not use for performance data!\n"; Timing.wrap "relation.prec-dump" store_data (Fpath.v file) end; Priv.finalize () diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml index efec236ede..d4312296e4 100644 --- a/src/analyses/extractPthread.ml +++ b/src/analyses/extractPthread.ml @@ -575,7 +575,7 @@ module Codegen = struct let dir = Goblintutil.create_dir (Fpath.v "pml-result") in let path = Fpath.to_string @@ Fpath.append dir (Fpath.v ("pthread." ^ ext)) in output_file ~filename:path ~text:content ; - print_endline @@ "saved " ^ desc ^ " as " ^ path + Logs.info "saved %s as %s" desc path end let tabulate = ( ^ ) "\t" @@ -611,7 +611,7 @@ module Codegen = struct let called_funs_done = ref Set.empty in let rec process_def res = - print_endline @@ Resource.show res ; + print_endline @@ Resource.show res ; (* nosemgrep: print-not-logging *) let res_type = Resource.res_type res in let res_name = Resource.res_name res in let is_thread = res_type = Resource.Thread in @@ -850,7 +850,7 @@ module Codegen = struct Writer.write "promela model" "pml" promela ; Writer.write "graph" "dot" dot_graph ; - print_endline + Logs.info "Copy spin/pthread_base.pml to same folder and then do: spin -a \ pthread.pml && cc -o pan pan.c && ./pan -a" end diff --git a/src/domains/printable.ml b/src/domains/printable.ml index c67c3c94a6..0a6e92a3e5 100644 --- a/src/domains/printable.ml +++ b/src/domains/printable.ml @@ -150,12 +150,12 @@ struct let equal_debug x y = (* This debug version checks if we call hashcons enough to have up-to-date tags. Comment out the equal below to use this. This will be even slower than with hashcons disabled! *) if x.BatHashcons.tag = y.BatHashcons.tag then ( (* x.BatHashcons.obj == y.BatHashcons.obj || *) if not (Base.equal x.BatHashcons.obj y.BatHashcons.obj) then - ignore @@ Pretty.printf "tags are equal but values are not for %a and %a\n" pretty x pretty y; + Logs.error "tags are equal but values are not for %a and %a\n" pretty x pretty y; assert (Base.equal x.BatHashcons.obj y.BatHashcons.obj); true ) else ( if Base.equal x.BatHashcons.obj y.BatHashcons.obj then - ignore @@ Pretty.printf "tags are not equal but values are for %a and %a\n" pretty x pretty y; + Logs.error "tags are not equal but values are for %a and %a\n" pretty x pretty y; assert (not (Base.equal x.BatHashcons.obj y.BatHashcons.obj)); false ) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index d834a6928a..8f17a3c11f 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -248,7 +248,7 @@ struct in let write_file f fn = Messages.xml_file_name := fn; - BatPrintf.printf "Writing xml to temp. file: %s\n%!" fn; + Logs.info "Writing xml to temp. file: %s\n%!" fn; BatPrintf.fprintf f ""; BatPrintf.fprintf f "%s" Goblintutil.command_line; BatPrintf.fprintf f ""; @@ -288,7 +288,7 @@ struct (*let p_fun f x = p_obj f [ "name", BatString.print, x; "nodes", p_list p_node, SH.find_all funs2node x ] in*) let p_file f x = fprintf f "{\n \"name\": \"%s\",\n \"path\": \"%s\",\n \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in let write_file f fn = - printf "Writing json to temp. file: %s\n%!" fn; + Logs.info "Writing json to temp. file: %s\n%!" fn; fprintf f "{\n \"parameters\": \"%s\",\n " Goblintutil.command_line; fprintf f "\"files\": %a,\n " (p_enum p_file) (SH.keys file2funs); fprintf f "\"results\": [\n %a\n]\n" printJson (Lazy.force table); @@ -303,7 +303,7 @@ struct write_file f (get_string "outfile") | "sarif" -> let open BatPrintf in - printf "Writing Sarif to file: %s\n%!" (get_string "outfile"); + Logs.info "Writing Sarif to file: %s\n%!" (get_string "outfile"); Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list)); | "json-messages" -> let json = `Assoc [ diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index 28ca8fab1b..0ce3c239a7 100644 --- a/src/framework/cfgTools.ml +++ b/src/framework/cfgTools.ml @@ -450,7 +450,7 @@ let createCFG (file: file) = ); if Messages.tracing then Messages.trace "cfg" "CFG building finished.\n\n"; if get_bool "dbg.verbose" then - ignore (Pretty.eprintf "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB)); + Logs.debug "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB); cfgF, cfgB let createCFG = Timing.wrap "createCFG" createCFG diff --git a/src/goblint.ml b/src/goblint.ml index 2b86d027e7..bd588b607b 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -37,8 +37,8 @@ let main () = GoblintDir.init (); if get_bool "dbg.verbose" then ( - print_endline (localtime ()); - print_endline Goblintutil.command_line; + Logs.debug "%s" (localtime ()); + Logs.debug "%s" Goblintutil.command_line; ); let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in if get_bool "server.enabled" then ( @@ -74,12 +74,12 @@ let main () = | Sys.Break -> (* raised on Ctrl-C if `Sys.catch_break true` *) do_stats (); (* Printexc.print_backtrace BatInnerIO.stderr *) - eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!")); + Logs.error "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!")); Goblint_timing.teardown_tef (); exit 131 (* same exit code as without `Sys.catch_break true`, otherwise 0 *) | Timeout -> do_stats (); - eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!")); + Logs.error "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!")); Goblint_timing.teardown_tef (); exit 124 diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 534c3e7f91..43245f2df5 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -10,16 +10,16 @@ let writeconffile = ref None (** Print version and bail. *) let print_version ch = - printf "Goblint version: %s\n" Version.goblint; - printf "Cil version: %s\n" Cil.cilVersion; - printf "Dune profile: %s\n" ConfigProfile.profile; - printf "OCaml version: %s\n" Sys.ocaml_version; - printf "OCaml flambda: %s\n" ConfigOcaml.flambda; + Logs.info "Goblint version: %s\n" Version.goblint; + Logs.info "Cil version: %s\n" Cil.cilVersion; + Logs.info "Dune profile: %s\n" ConfigProfile.profile; + Logs.info "OCaml version: %s\n" Sys.ocaml_version; + Logs.info "OCaml flambda: %s\n" ConfigOcaml.flambda; if get_bool "dbg.verbose" then ( - printf "Library versions:\n"; + Logs.debug "Library versions:\n"; List.iter (fun (name, version) -> let version = Option.default "[unknown]" version in - printf " %s: %s\n" name version + Logs.debug " %s: %s\n" name version ) Goblint_build_info.statically_linked_libraries ); exit 0 @@ -55,7 +55,7 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy ( let add_int l = let f str = l := str :: !l in Arg_complete.Int (f, Arg_complete.empty) in let set_trace sys = if Messages.tracing then Tracing.addsystem sys - else (prerr_endline "Goblint has been compiled without tracing, recompile in trace profile (./scripts/trace_on.sh)"; raise Exit) + else (Logs.error "Goblint has been compiled without tracing, recompile in trace profile (./scripts/trace_on.sh)"; raise Exit) in let configure_html () = if (get_string "outfile" = "") then @@ -104,7 +104,7 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy ( ; "-I" , Arg_complete.String (set_string "pre.includes[+]", Arg_complete.empty), "" ; "-IK" , Arg_complete.String (set_string "pre.kernel_includes[+]", Arg_complete.empty), "" ; "--set" , Arg_complete.Tuple [Arg_complete.Set_string (tmp_arg, complete_option); Arg_complete.String ((fun x -> set_auto !tmp_arg x), complete_last_option_value)], "" - ; "--sets" , Arg_complete.Tuple [Arg_complete.Set_string (tmp_arg, complete_option); Arg_complete.String ((fun x -> prerr_endline "--sets is deprecated, use --set instead."; set_string !tmp_arg x), complete_last_option_value)], "" + ; "--sets" , Arg_complete.Tuple [Arg_complete.Set_string (tmp_arg, complete_option); Arg_complete.String ((fun x -> Logs.warn "--sets is deprecated, use --set instead."; set_string !tmp_arg x), complete_last_option_value)], "" ; "--enable" , Arg_complete.String ((fun x -> set_bool x true), complete_bool_option), "" ; "--disable" , Arg_complete.String ((fun x -> set_bool x false), complete_bool_option), "" ; "--conf" , Arg_complete.String ((fun fn -> merge_file (Fpath.v fn)), Arg_complete.empty), "" @@ -125,7 +125,7 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy ( and rest_all_complete = lazy (Arg_complete.Rest_all_compat.create complete Arg_complete.empty_all) and complete args = Arg_complete.complete_argv args (Lazy.force option_spec_list) Arg_complete.empty - |> List.iter print_endline; + |> List.iter print_endline; (* nosemgrep: print-not-logging *) raise Exit let eprint_color m = eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr m) @@ -185,8 +185,8 @@ let parse_arguments () = end; handle_options (); if not (get_bool "server.enabled") && get_string_list "files" = [] then ( - prerr_endline "No files for Goblint?"; - prerr_endline "Try `goblint --help' for more information."; + Logs.error "No files for Goblint?"; + Logs.warn "Try `goblint --help' for more information."; raise Exit ) @@ -212,7 +212,7 @@ let basic_preprocess ~all_cppflags fname = (* Preprocess using cpp. *) let arguments = all_cppflags @ Fpath.to_string fname :: "-o" :: Fpath.to_string nname :: [] in let command = Filename.quote_command (Preprocessor.get_cpp ()) arguments in - if get_bool "dbg.verbose" then print_endline command; + if get_bool "dbg.verbose" then Logs.debug "%s" command; (nname, Some {ProcessPool.command; cwd = None}) (** Preprocess all files. Return list of preprocessed files and the temp directory name. *) @@ -247,14 +247,14 @@ let preprocess_files () = Goblint_sites.lib_stub_src in if get_bool "dbg.verbose" then ( - print_endline "Custom include dirs:"; + Logs.debug "Custom include dirs:"; List.iteri (fun i custom_include_dir -> - Format.printf " %d. %a (exists=%B)\n" (i + 1) Fpath.pp custom_include_dir (Sys.file_exists (Fpath.to_string custom_include_dir)) + Logs.Format.debug " %d. %a (exists=%B)\n" (i + 1) Fpath.pp custom_include_dir (Sys.file_exists (Fpath.to_string custom_include_dir)) ) custom_include_dirs ); let custom_include_dirs = List.filter (Sys.file_exists % Fpath.to_string) custom_include_dirs in if custom_include_dirs = [] then - print_endline "Warning, cannot find goblint's custom include files."; + Logs.warn "Warning, cannot find goblint's custom include files."; let find_custom_include subpath = let custom_include_opt = List.find_map_opt (fun custom_include_dir -> @@ -325,7 +325,7 @@ let preprocess_files () = let all_cppflags = !cppflags @ include_args in (* preprocess all the files *) - if get_bool "dbg.verbose" then print_endline "Preprocessing files."; + if get_bool "dbg.verbose" then Logs.info "Preprocessing files."; let rec preprocess_arg_file = function | filename when not (Sys.file_exists (Fpath.to_string filename)) -> @@ -376,7 +376,7 @@ let preprocess_files () = (** Parse preprocessed files *) let parse_preprocessed preprocessed = (* get the AST *) - if get_bool "dbg.verbose" then print_endline "Parsing files."; + if get_bool "dbg.verbose" then Logs.info "Parsing files."; let goblint_cwd = GobFpath.cwd () in let get_ast_and_record_deps (preprocessed_file, task_opt) = @@ -443,9 +443,9 @@ let preprocess_parse_merge () = let do_stats () = if get_bool "dbg.timing.enabled" then ( print_newline (); - ignore (Pretty.printf "vars = %d evals = %d narrow_reuses = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses); + Logs.info "vars = %d evals = %d narrow_reuses = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses; print_newline (); - print_string "Timings:\n"; + Logs.info "Timings:\n"; Timing.Default.print (Format.formatter_of_out_channel @@ Messages.get_out "timing" Legacy.stderr); flush_all () ) @@ -471,19 +471,19 @@ let do_analyze change_info merged_AST = Cilfacade.print merged_AST else ( (* we first find the functions to analyze: *) - if get_bool "dbg.verbose" then print_endline "And now... the Goblin!"; + if get_bool "dbg.verbose" then Logs.info "And now... the Goblin!"; let (stf,exf,otf as funs) = Cilfacade.getFuns merged_AST in if stf@exf@otf = [] then raise (FrontendError "no suitable function to start from"); - if get_bool "dbg.verbose" then ignore (Pretty.printf "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a\n" - L.pretty stf L.pretty exf L.pretty otf); + if get_bool "dbg.verbose" then Logs.debug "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a\n" + L.pretty stf L.pretty exf L.pretty otf; (* and here we run the analysis! *) let control_analyze ast funs = if get_bool "dbg.verbose" then ( let aa = String.concat ", " @@ get_string_list "ana.activated" in let at = String.concat ", " @@ get_string_list "trans.activated" in - print_endline @@ "Activated analyses: " ^ aa; - print_endline @@ "Activated transformations: " ^ at + Logs.info "Activated analyses: %s" aa; + Logs.info "Activated transformations: %s" at ); try Control.analyze change_info ast funs with e -> @@ -513,11 +513,11 @@ let do_html_output () = let command = "java -jar "^ jar ^" --num-threads " ^ (string_of_int (jobs ())) ^ " --dot-timeout 0 --result-dir "^ (get_string "outfile")^" "^ !Messages.xml_file_name in try match Timing.wrap "g2html" Unix.system command with | Unix.WEXITED 0 -> () - | _ -> eprintf "HTML generation failed! Command: %s\n" command + | _ -> Logs.error "HTML generation failed! Command: %s\n" command with Unix.Unix_error (e, f, a) -> - eprintf "%s at syscall %s with argument \"%s\".\n" (Unix.error_message e) f a + Logs.error "%s at syscall %s with argument \"%s\".\n" (Unix.error_message e) f a ) else - eprintf "Warning: jar file %s not found.\n" jar + Logs.error "Warning: jar file %s not found.\n" jar ) let do_gobview cilfile = @@ -562,7 +562,7 @@ let do_gobview cilfile = ) dist_files ) else - eprintf "Warning: Cannot locate GobView.\n" + Logs.error "Warning: Cannot locate GobView.\n" ) let handle_extraspecials () = diff --git a/src/messagesCompare.ml b/src/messagesCompare.ml index b4f43f8b10..1bad65c1ec 100644 --- a/src/messagesCompare.ml +++ b/src/messagesCompare.ml @@ -34,12 +34,12 @@ let () = let right_only_messages = MS.diff right_messages left_messages in if not (MS.is_empty left_only_messages) then ( - Printf.printf "Left-only messages (%d):\n" (MS.cardinal left_only_messages); + Logs.info "Left-only messages (%d):\n" (MS.cardinal left_only_messages); MS.iter (Messages.print) left_only_messages; ); print_newline (); if not (MS.is_empty right_only_messages) then ( - Printf.printf "Right-only messages (%d):\n" (MS.cardinal right_only_messages); + Logs.info "Right-only messages (%d):\n" (MS.cardinal right_only_messages); MS.iter (Messages.print) right_only_messages; ) | _ -> diff --git a/src/spec/specUtil.ml b/src/spec/specUtil.ml index 925cdbdfcd..6c7fbae904 100644 --- a/src/spec/specUtil.ml +++ b/src/spec/specUtil.ml @@ -18,14 +18,14 @@ let parse ?repl:(repl=false) ?print:(print=false) ?dot:(dot=false) cin = let result = SpecParser.file SpecLexer.token lexbuf in defs := !defs@[result]; incr line; - if print then (print_endline (SpecCore.def_to_string result); flush stdout) + if print then (Logs.debug "%s" (SpecCore.def_to_string result); flush stdout) with (* just an empty line -> don't print *) | SpecCore.Endl -> incr line (* somehow gets raised in some cases instead of SpecCore.Eof *) | BatInnerIO.Input_closed -> raise SpecCore.Eof (* catch and print in repl-mode *) - | e when repl -> print_endline (Printexc.to_string e) + | e when repl -> Logs.error "%s" (Printexc.to_string e) done; ([], []) (* never happens, but ocaml needs it for type *) with @@ -33,15 +33,15 @@ let parse ?repl:(repl=false) ?print:(print=false) ?dot:(dot=false) cin = | SpecCore.Eof -> let nodes = List.filter_map (function SpecCore.Node x -> Some x | _ -> None) !defs in let edges = List.filter_map (function SpecCore.Edge x -> Some x | _ -> None) !defs in - if print then Printf.printf "\n#Definitions: %i, #Nodes: %i, #Edges: %i\n" + if print then Logs.debug "\n#Definitions: %i, #Nodes: %i, #Edges: %i\n" (List.length !defs) (List.length nodes) (List.length edges); if save_dot && not dot then ( let dotgraph = SpecCore.to_dot_graph !defs in output_file ~filename:"result/graph.dot" ~text:dotgraph; - print_endline ("saved graph as "^Sys.getcwd ()^"/result/graph.dot"); + Logs.info "saved graph as %s/result/graph.dot" (Sys.getcwd ()); ); if dot then ( - print_endline (SpecCore.to_dot_graph !defs) + print_endline (SpecCore.to_dot_graph !defs) (* nosemgrep: print-not-logging *) ); (nodes, edges) (* stop on parsing error if not in REPL and include line number *) diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml index 791d42c30e..f29a9cc68b 100644 --- a/src/transform/expressionEvaluation.ml +++ b/src/transform/expressionEvaluation.ml @@ -153,7 +153,7 @@ struct Error ("ExpEval: Unable to parse JSON query file: \"" ^ name ^ "\" (" ^ message ^ ")") | Ok query -> if is_debug () then - print_endline ("Successfully parsed JSON query file: \"" ^ name ^ "\""); + Logs.debug "Successfully parsed JSON query file: \"%s\"" name; Ok query let string_of_location (location : Cil.location) = @@ -195,16 +195,16 @@ struct match res with | Some value -> if value then - print_endline (loc |> string_of_location) + Logs.info "%s" (loc |> string_of_location) else if is_debug () then - print_endline ((loc |> string_of_location) ^ " x") + Logs.debug "%s x" (loc |> string_of_location) | None -> if query.mode = `May || is_debug () then - print_endline ((loc |> string_of_location) ^ " ?") + Logs.info "%s ?" (loc |> string_of_location) in gv_results := results; List.iter print results - | Error e -> prerr_endline e + | Error e -> Logs.error "%s" e end diff --git a/src/transform/transform.ml b/src/transform/transform.ml index e366b5d2a6..344388c3f3 100644 --- a/src/transform/transform.ml +++ b/src/transform/transform.ml @@ -9,7 +9,7 @@ let h = Hashtbl.create 13 let register name (module T : S) = Hashtbl.add h name (module T : S) let run name = let module T = (val try Hashtbl.find h name with Not_found -> failwith @@ "Transformation "^name^" does not exist!") in - if GobConfig.get_bool "dbg.verbose" then print_endline @@ "Starting transformation " ^ name; + if GobConfig.get_bool "dbg.verbose" then Logs.debug "Starting transformation %s" name; T.transform module PartialEval = struct diff --git a/src/util/backtrace/goblint_backtrace.ml b/src/util/backtrace/goblint_backtrace.ml index 1ffcaf7db7..a4355ac921 100644 --- a/src/util/backtrace/goblint_backtrace.ml +++ b/src/util/backtrace/goblint_backtrace.ml @@ -70,7 +70,7 @@ let print_marktrace oc e = let () = Printexc.set_uncaught_exception_handler (fun e bt -> (* Copied & modified from Printexc.default_uncaught_exception_handler. *) - Printf.eprintf "Fatal error: exception %s\n" (Printexc.to_string e); + Printf.eprintf "Fatal error: exception %s\n" (Printexc.to_string e); (* nosemgrep: print-not-logging *) if Printexc.backtrace_status () then print_marktrace stderr e; Printexc.print_raw_backtrace stderr bt; diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index be478622cc..19f56c3c32 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -119,7 +119,7 @@ let callConstructors ast = !cons in let d_fundec () fd = Pretty.text fd.svar.vname in - if get_bool "dbg.verbose" then ignore (Pretty.printf "Constructors: %a\n" (Pretty.d_list ", " d_fundec) constructors); + if get_bool "dbg.verbose" then ignore (Logs.debug "Constructors: %a\n" (Pretty.d_list ", " d_fundec) constructors); visitCilFileSameGlobals (new addConstructors constructors) ast; ast @@ -144,9 +144,9 @@ let getFuns fileAST : startfuns = | GFun({svar={vname=mn; _}; _} as def,_) when List.mem mn (get_string_list "exitfun") -> add_exit def acc | GFun({svar={vname=mn; _}; _} as def,_) when List.mem mn (get_string_list "otherfun") -> add_other def acc | GFun({svar={vname=mn; vattr=attr; _}; _} as def, _) when get_bool "kernel" && is_init attr -> - Printf.printf "Start function: %s\n" mn; set_string "mainfun[+]" mn; add_main def acc + Logs.debug "Start function: %s\n" mn; set_string "mainfun[+]" mn; add_main def acc | GFun({svar={vname=mn; vattr=attr; _}; _} as def, _) when get_bool "kernel" && is_exit attr -> - Printf.printf "Cleanup function: %s\n" mn; set_string "exitfun[+]" mn; add_exit def acc + Logs.debug "Cleanup function: %s\n" mn; set_string "exitfun[+]" mn; add_exit def acc | GFun ({svar={vstorage=NoStorage; _}; _} as def, _) when (get_bool "nonstatic") -> add_other def acc | GFun ({svar={vattr; _}; _} as def, _) when get_bool "allfuns" && not (Cil.hasAttribute "goblint_stub" vattr) -> add_other def acc | _ -> acc diff --git a/src/util/compilationDatabase.ml b/src/util/compilationDatabase.ml index 8d3e098a87..a49dca3dab 100644 --- a/src/util/compilationDatabase.ml +++ b/src/util/compilationDatabase.ml @@ -69,7 +69,7 @@ let load_and_preprocess ~all_cppflags filename = let old_root = GobFpath.rem_find_prefix database_dir original_database_dir in let new_root = GobFpath.rem_find_prefix original_database_dir database_dir in if GobConfig.get_bool "dbg.verbose" then - Format.printf "Rerooting compilation database\n from %a\n to %a\n" Fpath.pp old_root Fpath.pp new_root; + Logs.Format.debug "Rerooting compilation database\n from %a\n to %a\n" Fpath.pp old_root Fpath.pp new_root; let reroot_path p = Fpath.append new_root (Option.get (Fpath.relativize ~root:old_root p)) in @@ -127,7 +127,7 @@ let load_and_preprocess ~all_cppflags filename = in let cwd = reroot_path obj.directory in if GobConfig.get_bool "dbg.verbose" then - Format.printf "Preprocessing %a\n to %a\n using %s\n in %a\n" Fpath.pp file Fpath.pp preprocessed_file preprocess_command Fpath.pp cwd; + Logs.Format.debug "Preprocessing %a\n to %a\n using %s\n in %a\n" Fpath.pp file Fpath.pp preprocessed_file preprocess_command Fpath.pp cwd; let preprocess_task = {ProcessPool.command = preprocess_command; cwd = Some cwd} in (* command/arguments might have paths relative to directory *) Some (preprocessed_file, Some preprocess_task) in diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index c3553431ac..55ea5536bd 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -178,7 +178,7 @@ struct else Select (fld, parse_path' pth) end with PathParseError -> - eprintf "Error: Couldn't parse the json path '%s'\n%!" s; + Logs.error "Error: Couldn't parse the json path '%s'\n%!" s; failwith "parsing" (** Here we store the actual configuration. *) @@ -301,7 +301,7 @@ struct if tracing then trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x; try f x with Yojson.Safe.Util.Type_error (s, _) -> - eprintf "The value for '%s' has the wrong type: %s\n" st s; + Logs.error "The value for '%s' has the wrong type: %s\n" st s; failwith "get_path_string" with ConfTypeError -> eprintf "Cannot find value '%s' in\n%t\nDid You forget to add default values to options.schema.json?\n" @@ -377,7 +377,7 @@ struct with Yojson.Json_error _ | TypeError _ -> set_string st s with e -> - eprintf "Cannot set %s to '%s'.\n" st s; + Logs.error "Cannot set %s to '%s'.\n" st s; raise e let merge json = diff --git a/src/util/jsonSchema.ml b/src/util/jsonSchema.ml index 63295eb126..9eaefc6549 100644 --- a/src/util/jsonSchema.ml +++ b/src/util/jsonSchema.ml @@ -104,7 +104,7 @@ let rec element_defaults ?additional_field (element: element): Yojson.Safe.t = (name, element_defaults ?additional_field field_element) ) object_specs.properties) | _ -> - Format.printf "%a\n" Json_schema.pp (create element); + Logs.Format.error "%a\n" Json_schema.pp (create element); failwith "element_defaults" end @@ -135,7 +135,7 @@ let rec element_require_all (element: element): element = in Object { object_specs with properties = properties' } | _ -> - Format.printf "%a\n" Json_schema.pp (create element); + Logs.Format.error "%a\n" Json_schema.pp (create element); failwith "element_require_all" in { element with kind = kind' } diff --git a/src/util/logs.ml b/src/util/logs.ml index 8242bcb878..65baa95731 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -31,6 +31,17 @@ struct Format.kfprintf finish Format.err_formatter fmt end +module BatteriesKind = +struct + type b = unit BatIO.output + type c = unit + let log fmt = + let finish out = + BatPrintf.fprintf out "\n%!" + in + BatPrintf.kfprintf finish BatIO.stderr fmt +end + module MakeKind (Kind: Kind) = struct @@ -46,5 +57,6 @@ end module Pretty = MakeKind (PrettyKind) module Format = MakeKind (FormatKind) +module Batteries = MakeKind (BatteriesKind) include Pretty (* current default *) diff --git a/src/util/options.ml b/src/util/options.ml index 7fb6cabae9..65ccb7e09f 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -27,7 +27,7 @@ let rec element_paths (element: element): string list = List.map (fun path -> name ^ "." ^ path) (element_paths field_element) ) object_specs.properties | _ -> - Format.printf "%a\n" Json_schema.pp (create element); + Logs.Format.error "%a\n" Json_schema.pp (create element); failwith "element_paths" let schema_paths (schema: schema): string list = @@ -69,7 +69,7 @@ let rec element_completions (element: element): (string * string list) list = List.map (fun (path, cs) -> (name ^ "." ^ path, cs)) (element_completions field_element) ) object_specs.properties | _ -> - Format.printf "%a\n" Json_schema.pp (create element); + Logs.Format.error "%a\n" Json_schema.pp (create element); failwith "element_completions" let schema_completions (schema: schema): (string * string list) list = @@ -110,7 +110,7 @@ let rec pp_options ~levels ppf (element: element) = failwith "pp_options" let print_options () = - Format.printf "%a\n" (pp_options ~levels:1) (root schema) + Format.printf "%a\n" (pp_options ~levels:1) (root schema) (* nosemgrep: print-not-logging *) let print_all_options () = - Format.printf "%a\n" (pp_options ~levels:max_int) (root schema) + Format.printf "%a\n" (pp_options ~levels:max_int) (root schema) (* nosemgrep: print-not-logging *) diff --git a/src/util/precCompare.ml b/src/util/precCompare.ml index dafa835f80..e2c9391dd5 100644 --- a/src/util/precCompare.ml +++ b/src/util/precCompare.ml @@ -79,7 +79,7 @@ struct match c with | {Comparison.more_precise = 0; less_precise = 0; incomparable = 0; _} -> () | _ -> - if verbose then ignore (Pretty.printf "%a: %t\n" K.pretty k (fun () -> msg)) + if verbose then Logs.debug "%a: %t\n" K.pretty k (fun () -> msg) ) compared; let c = KH.fold (fun _ (c, _) acc -> Comparison.aggregate_same c acc) compared Comparison.empty in let msg = Pretty.dprintf "%s %s %s (%s)" name1 (Comparison.to_string_infix c) name2 (Comparison.to_string_counts c) in @@ -127,6 +127,6 @@ struct |> List.filter (fun ((i1, _), (i2, _)) -> i1 <> i2) |> List.map (Tuple2.map snd snd) |> List.map (uncurry compare_dumps) - |> List.iter (fun (_, msg) -> ignore (Pretty.printf "%t\n" (fun () -> msg))); - ignore (Pretty.printf "\nTotal locations: %d\nTotal %s: %d\n" locations_count (Key.name ()) location_vars_count) + |> List.iter (fun (_, msg) -> Logs.info "%t\n" (fun () -> msg)); + Logs.info "\nTotal locations: %d\nTotal %s: %d\n" locations_count (Key.name ()) location_vars_count end diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index eb24e5c839..796085bf14 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -10,7 +10,7 @@ let is_bad name = | _ -> true in if GobConfig.get_bool "dbg.verbose" then - Printf.printf "Preprocessor %s: is_bad=%B\n" name r; + Logs.debug "Preprocessor %s: is_bad=%B\n" name r; r let compgen prefix = diff --git a/src/util/tracing.ml b/src/util/tracing.ml index ea1183ac98..ab56d9074b 100644 --- a/src/util/tracing.ml +++ b/src/util/tracing.ml @@ -25,7 +25,7 @@ let activate (sys:string) (subsys: string list): unit = activated := Strs.union !activated subs; Hashtbl.add active_dep sys subs let deactivate (sys:string): unit = - activated := Strs.diff !activated (try Hashtbl.find active_dep sys with Not_found -> print_endline ("WTF? " ^ sys); Strs.empty) + activated := Strs.diff !activated (try Hashtbl.find active_dep sys with Not_found -> Logs.error "WTF? %s" sys; Strs.empty) let indent_level = ref 0 let traceIndent () = indent_level := !indent_level + 2 diff --git a/src/witness/violation.ml b/src/witness/violation.ml index 9b85f854ff..9cb9b6c579 100644 --- a/src/witness/violation.ml +++ b/src/witness/violation.ml @@ -123,7 +123,7 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod print_path path; begin match Feasibility.check_path path with | Feasibility.Feasible -> - print_endline "feasible"; + Logs.debug "feasible"; let module PathArg = struct @@ -144,12 +144,12 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod in Feasible (module PathArg) | Feasibility.Infeasible subpath -> - print_endline "infeasible"; + Logs.debug "infeasible"; print_path subpath; Infeasible subpath | Feasibility.Unknown -> - print_endline "unknown"; + Logs.debug "unknown"; Unknown end | None -> diff --git a/src/witness/witness.ml b/src/witness/witness.ml index c7fd174fb5..93d72661c1 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -260,7 +260,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) let print_svcomp_result (s: string): unit = - Printf.printf "SV-COMP result: %s\n" s + Logs.info "SV-COMP result: %s\n" s let print_task_result (module TaskResult:TaskResult): unit = print_svcomp_result (Result.to_string TaskResult.result) @@ -272,7 +272,7 @@ let init (module FileCfg: MyCFG.FileCfg) = let specification = Svcomp.Specification.of_option () end in - Printf.printf "SV-COMP specification: %s\n" (Svcomp.Specification.to_string Task.specification); + Logs.info "SV-COMP specification: %s\n" (Svcomp.Specification.to_string Task.specification); Svcomp.task := Some (module Task) module Result (R: ResultQuery.SpecSysSol2) = diff --git a/src/witness/z3/violationZ3.z3.ml b/src/witness/z3/violationZ3.z3.ml index b0085b6044..bf6af6cdf6 100644 --- a/src/witness/z3/violationZ3.z3.ml +++ b/src/witness/z3/violationZ3.z3.ml @@ -152,16 +152,16 @@ struct end and do_assert revpath' i env' expr = - Printf.printf "%d: %s\n" i (Expr.to_string expr); + Logs.debug "%d: %s\n" i (Expr.to_string expr); let track_const = Boolean.mk_const ctx (Symbol.mk_int ctx i) in Solver.assert_and_track solver expr track_const; let status = Solver.check solver [] in - Printf.printf "%d: %s\n" i (Solver.string_of_status status); + Logs.debug "%d: %s\n" i (Solver.string_of_status status); match Solver.check solver [] with | Solver.SATISFIABLE -> - Printf.printf "%d: %s\n" i (Model.to_string (BatOption.get @@ Solver.get_model solver)); + Logs.info "%d: %s\n" i (Model.to_string (BatOption.get @@ Solver.get_model solver)); iter_wp revpath' (i - 1) env' | Solver.UNSATISFIABLE -> @@ -181,7 +181,7 @@ struct unsat_core_is |> List.map string_of_int |> String.concat " " - |> print_endline; + |> Logs.debug "%s"; let (mini, maxi) = BatList.min_max unsat_core_is in let unsat_path = BatList.filteri (fun i _ -> mini <= i && i <= maxi) path in (* TODO: optimize subpath *) From aa1e1123dc6639918eb2a67b0bffd8512703df14 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 16:03:18 +0200 Subject: [PATCH 06/39] Add Logs.newline --- .semgrep/logs.yml | 14 +++++++++++++- src/framework/constraints.ml | 8 ++++---- src/maingoblint.ml | 6 +++--- src/messagesCompare.ml | 2 +- src/solvers/generic.ml | 8 ++++---- src/solvers/sLR.ml | 4 ++-- src/solvers/sLRphased.ml | 2 +- src/solvers/sLRterm.ml | 2 +- src/solvers/td3.ml | 6 +++--- src/util/logs.ml | 2 ++ 10 files changed, 34 insertions(+), 20 deletions(-) diff --git a/.semgrep/logs.yml b/.semgrep/logs.yml index 800e600c8c..dad32adadf 100644 --- a/.semgrep/logs.yml +++ b/.semgrep/logs.yml @@ -15,7 +15,6 @@ rules: - pattern: print_endline - pattern: prerr_endline - - pattern: print_newline - pattern: print_string paths: exclude: @@ -24,3 +23,16 @@ rules: message: printing should be replaced with logging languages: [ocaml] severity: WARNING + + - id: print-newline-not-logging + pattern-either: + - pattern: print_newline + - pattern: prerr_newline + paths: + exclude: + - logs.ml + - bench/ + fix: Logs.newline + message: use Logs instead + languages: [ocaml] + severity: WARNING diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 5da3fe3507..b5fbbdb7b9 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -1456,7 +1456,7 @@ struct compare_globals g1 g2; compare_locals h1 h2; compare_locals_ctx l1 l2; - print_newline (); + Logs.newline (); end module CompareHashtbl (Var: VarType) (Dom: Lattice.S) (VH: Hashtbl.S with type key = Var.t) = @@ -1487,7 +1487,7 @@ struct let verbose = get_bool "dbg.compare_runs.diff" in let (_, msg) = Compare.compare ~verbose ~name1 vh1 ~name2 vh2 in Logs.info "EqConstrSys comparison summary: %t\n" (fun () -> msg); - print_newline (); + Logs.newline (); end module CompareGlobal (GVar: VarType) (G: Lattice.S) (GH: Hashtbl.S with type key = GVar.t) = @@ -1499,7 +1499,7 @@ struct let verbose = get_bool "dbg.compare_runs.diff" in let (_, msg) = Compare.compare ~verbose ~name1 vh1 ~name2 vh2 in Logs.info "Globals comparison summary: %t\n" (fun () -> msg); - print_newline (); + Logs.newline (); end module CompareNode (C: Printable.S) (D: Lattice.S) (LH: Hashtbl.S with type key = VarF (C).t) = @@ -1530,7 +1530,7 @@ struct let verbose = get_bool "dbg.compare_runs.diff" in let (_, msg) = Compare.compare ~verbose ~name1 vh1' ~name2 vh2' in Logs.info "Nodes comparison summary: %t\n" (fun () -> msg); - print_newline (); + Logs.newline (); end (** [EqConstrSys] where [current_var] indicates the variable whose right-hand side is currently being evaluated. *) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 43245f2df5..adae969257 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -442,9 +442,9 @@ let preprocess_parse_merge () = let do_stats () = if get_bool "dbg.timing.enabled" then ( - print_newline (); + Logs.newline (); Logs.info "vars = %d evals = %d narrow_reuses = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses; - print_newline (); + Logs.newline (); Logs.info "Timings:\n"; Timing.Default.print (Format.formatter_of_out_channel @@ Messages.get_out "timing" Legacy.stderr); flush_all () @@ -497,7 +497,7 @@ let do_analyze change_info merged_AST = (* trigger Generic.SolverStats...print_stats *) Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal"))); do_stats (); - print_newline (); + Logs.newline (); Printexc.raise_with_backtrace e backtrace (* re-raise with captured inner backtrace *) (* Cilfacade.current_file := ast'; *) in diff --git a/src/messagesCompare.ml b/src/messagesCompare.ml index 1bad65c1ec..beef0913d7 100644 --- a/src/messagesCompare.ml +++ b/src/messagesCompare.ml @@ -37,7 +37,7 @@ let () = Logs.info "Left-only messages (%d):\n" (MS.cardinal left_only_messages); MS.iter (Messages.print) left_only_messages; ); - print_newline (); + Logs.newline (); if not (MS.is_empty right_only_messages) then ( Logs.info "Right-only messages (%d):\n" (MS.cardinal right_only_messages); MS.iter (Messages.print) right_only_messages; diff --git a/src/solvers/generic.ml b/src/solvers/generic.ml index 2ae2c73689..207ce80512 100644 --- a/src/solvers/generic.ml +++ b/src/solvers/generic.ml @@ -113,19 +113,19 @@ struct (* print generic and specific stats *) let print_stats _ = - print_newline (); + Logs.newline (); (* print_endline "# Generic solver stats"; *) Logs.info "runtime: %s\n" (string_of_time ()); Logs.info "vars: %d, evals: %d\n" !Goblintutil.vars !Goblintutil.evals; Option.may (fun v -> ignore @@ Logs.info "max updates: %d for var %a\n" !max_c Var.pretty_trace v) !max_var; - print_newline (); + Logs.newline (); (* print_endline "# Solver specific stats"; *) !print_solver_stats (); - print_newline (); + Logs.newline (); (* Timing.print (M.get_out "timing" Legacy.stdout) "Timings:\n"; *) (* Gc.print_stat stdout; (* too verbose, slow and words instead of MB *) *) let gc = Goblintutil.print_gc_quick_stat Legacy.stdout in - print_newline (); + Logs.newline (); Option.may (write_csv [string_of_time (); string_of_int !Goblintutil.vars; string_of_int !Goblintutil.evals; string_of_int !ncontexts; string_of_int gc.Gc.top_heap_words]) stats_csv; (* print_string "Do you want to continue? [Y/n]"; *) flush stdout diff --git a/src/solvers/sLR.ml b/src/solvers/sLR.ml index 243dcaa583..2f93516530 100644 --- a/src/solvers/sLR.ml +++ b/src/solvers/sLR.ml @@ -154,7 +154,7 @@ module SLR3 = if GobConfig.get_bool "dbg.print_wpoints" then ( Logs.debug "\nWidening points:\n"; HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; - print_newline (); + Logs.newline (); ); HM.clear key ; @@ -448,7 +448,7 @@ module Make0 = if GobConfig.get_bool "dbg.print_wpoints" then ( Logs.debug "\nWidening points:\n"; HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; - print_newline (); + Logs.newline (); ); X.to_list () diff --git a/src/solvers/sLRphased.ml b/src/solvers/sLRphased.ml index 441666800b..b8570c42e9 100644 --- a/src/solvers/sLRphased.ml +++ b/src/solvers/sLRphased.ml @@ -190,7 +190,7 @@ module Make = if GobConfig.get_bool "dbg.print_wpoints" then ( Logs.debug "\nWidening points:\n"; HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; - print_newline (); + Logs.newline (); ); HM.clear key ; diff --git a/src/solvers/sLRterm.ml b/src/solvers/sLRterm.ml index f709751bb4..6db9d59aa3 100644 --- a/src/solvers/sLRterm.ml +++ b/src/solvers/sLRterm.ml @@ -208,7 +208,7 @@ module SLR3term = if GobConfig.get_bool "dbg.print_wpoints" then ( Logs.debug "\nWidening points:\n"; HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; - print_newline (); + Logs.newline (); ); HM.clear key ; diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index c7bca63fea..c3e35d4af4 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -762,10 +762,10 @@ module Base = let unstable_vs = List.filter (neg (HM.mem stable)) vs in if unstable_vs <> [] then ( if GobConfig.get_bool "dbg.verbose" then ( - if !i = 1 then print_newline (); + if !i = 1 then Logs.newline (); Logs.debug "Unstable solver start vars in %d. phase:\n" !i; List.iter (fun v -> Logs.debug "\t%a\n" S.Var.pretty_trace v) unstable_vs; - print_newline (); + Logs.newline (); flush_all (); ); List.iter (fun x -> solve x Widen) unstable_vs; @@ -833,7 +833,7 @@ module Base = if GobConfig.get_bool "dbg.print_wpoints" then ( Logs.debug "\nWidening points:\n"; HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; - print_newline (); + Logs.newline (); ); (* Prune other data structures than rho with reachable. diff --git a/src/util/logs.ml b/src/util/logs.ml index 65baa95731..db694532e0 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -53,6 +53,8 @@ struct let info = log let warn = log let error = log + + let newline () = () end module Pretty = MakeKind (PrettyKind) From 1aa91c1fda7a1a1d6bee1a45113b6506c9caa69f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 16:06:27 +0200 Subject: [PATCH 07/39] Use Logs everywhere --- src/maingoblint.ml | 5 +++-- src/util/gobConfig.ml | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index adae969257..9c3171376b 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -128,7 +128,8 @@ and complete args = |> List.iter print_endline; (* nosemgrep: print-not-logging *) raise Exit -let eprint_color m = eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr m) +(* TODO: remove *) +let eprint_color m = Logs.info "%s\n" (MessageUtil.colorize ~fd:Unix.stderr m) let check_arguments () = let fail m = (let m = "Option failure: " ^ m in eprint_color ("{red}"^m); failwith m) in(* unused now, but might be useful for future checks here *) @@ -617,4 +618,4 @@ let () = (* signal for printing backtrace; other signals in Generic.SolverStats let open Sys in (* whether interactive interrupt (ctrl-C) terminates the program or raises the Break exception which we use below to print a backtrace. https://ocaml.org/api/Sys.html#VALcatch_break *) catch_break true; - set_signal (Goblintutil.signal_of_string (get_string "dbg.backtrace-signal")) (Signal_handle (fun _ -> Printexc.get_callstack 999 |> Printexc.print_raw_backtrace Stdlib.stderr; print_endline "\n...\n")) (* e.g. `pkill -SIGUSR2 goblint`, or `kill`, `htop` *) + set_signal (Goblintutil.signal_of_string (get_string "dbg.backtrace-signal")) (Signal_handle (fun _ -> Printexc.get_callstack 999 |> Printexc.print_raw_backtrace Stdlib.stderr)) (* e.g. `pkill -SIGUSR2 goblint`, or `kill`, `htop` *) diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 55ea5536bd..6a4334d9d7 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -304,7 +304,7 @@ struct Logs.error "The value for '%s' has the wrong type: %s\n" st s; failwith "get_path_string" with ConfTypeError -> - eprintf "Cannot find value '%s' in\n%t\nDid You forget to add default values to options.schema.json?\n" + Logs.Batteries.error "Cannot find value '%s' in\n%t\nDid You forget to add default values to options.schema.json?\n" st print; failwith "get_path_string" let get_json : string -> Yojson.Safe.t = get_path_string Fun.id From 22d8963773e198c57195a8bf2694ab06ff9941c3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 16:16:13 +0200 Subject: [PATCH 08/39] Remove %! from Logs formats --- src/framework/analyses.ml | 6 +++--- src/util/gobConfig.ml | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 8f17a3c11f..16566a6e59 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -248,7 +248,7 @@ struct in let write_file f fn = Messages.xml_file_name := fn; - Logs.info "Writing xml to temp. file: %s\n%!" fn; + Logs.info "Writing xml to temp. file: %s\n" fn; BatPrintf.fprintf f ""; BatPrintf.fprintf f "%s" Goblintutil.command_line; BatPrintf.fprintf f ""; @@ -288,7 +288,7 @@ struct (*let p_fun f x = p_obj f [ "name", BatString.print, x; "nodes", p_list p_node, SH.find_all funs2node x ] in*) let p_file f x = fprintf f "{\n \"name\": \"%s\",\n \"path\": \"%s\",\n \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in let write_file f fn = - Logs.info "Writing json to temp. file: %s\n%!" fn; + Logs.info "Writing json to temp. file: %s\n" fn; fprintf f "{\n \"parameters\": \"%s\",\n " Goblintutil.command_line; fprintf f "\"files\": %a,\n " (p_enum p_file) (SH.keys file2funs); fprintf f "\"results\": [\n %a\n]\n" printJson (Lazy.force table); @@ -303,7 +303,7 @@ struct write_file f (get_string "outfile") | "sarif" -> let open BatPrintf in - Logs.info "Writing Sarif to file: %s\n%!" (get_string "outfile"); + Logs.info "Writing Sarif to file: %s\n" (get_string "outfile"); Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list)); | "json-messages" -> let json = `Assoc [ diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 6a4334d9d7..624cf748a4 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -178,7 +178,7 @@ struct else Select (fld, parse_path' pth) end with PathParseError -> - Logs.error "Error: Couldn't parse the json path '%s'\n%!" s; + Logs.error "Error: Couldn't parse the json path '%s'\n" s; failwith "parsing" (** Here we store the actual configuration. *) From 2d8678f32857d81482d7cc967517cdfdc305756e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 16:28:38 +0200 Subject: [PATCH 09/39] Remove newlines from log messages --- src/analyses/apron/relationAnalysis.apron.ml | 2 +- src/analyses/threadId.ml | 7 +-- src/autoTune.ml | 2 +- src/autoTune0.ml | 21 ++++---- src/domains/printable.ml | 4 +- src/framework/analyses.ml | 6 +-- src/framework/cfgTools.ml | 2 +- src/framework/constraints.ml | 52 +++++++++++--------- src/framework/control.ml | 8 +-- src/goblint.ml | 4 +- src/maingoblint.ml | 32 ++++++------ src/messagesCompare.ml | 4 +- src/solvers/generic.ml | 10 ++-- src/solvers/postSolver.ml | 4 +- src/solvers/sLR.ml | 10 ++-- src/solvers/sLRphased.ml | 5 +- src/solvers/sLRterm.ml | 9 ++-- src/solvers/td3.ml | 41 +++++++-------- src/solvers/topDown_space_cache_term.ml | 6 +-- src/spec/specUtil.ml | 7 ++- src/util/cilfacade.ml | 6 +-- src/util/compilationDatabase.ml | 4 +- src/util/gobConfig.ml | 8 +-- src/util/jsonSchema.ml | 4 +- src/util/options.ml | 4 +- src/util/precCompare.ml | 7 +-- src/util/preprocessor.ml | 2 +- src/witness/witness.ml | 4 +- src/witness/z3/violationZ3.z3.ml | 6 +-- 29 files changed, 147 insertions(+), 134 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 49d4b3ae58..eec66f90a9 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -709,7 +709,7 @@ struct let finalize () = let file = GobConfig.get_string "exp.relation.prec-dump" in if file <> "" then begin - Logs.warn "exp.relation.prec-dump is potentially costly (for domains other than octagons), do not use for performance data!\n"; + Logs.warn "exp.relation.prec-dump is potentially costly (for domains other than octagons), do not use for performance data!"; Timing.wrap "relation.prec-dump" store_data (Fpath.v file) end; Priv.finalize () diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index 30857e781e..6dbd35b0de 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -125,12 +125,13 @@ struct let non_uniques = List.filter_map (fun (a,b) -> if not (Thread.is_unique a) then Some a else None) tids in let uc = List.length uniques in let nc = List.length non_uniques in - Logs.debug "Encountered number of thread IDs (unique): %i (%i)\n" (uc+nc) uc; + Logs.debug "Encountered number of thread IDs (unique): %i (%i)" (uc+nc) uc; Logs.debug "unique: "; List.iter (fun tid -> Logs.debug " %s " (Thread.show tid)) uniques; - Logs.debug "\nnon-unique: "; + Logs.newline (); + Logs.debug "non-unique: "; List.iter (fun tid -> Logs.debug " %s " (Thread.show tid)) non_uniques; - Logs.debug "\n" + Logs.newline () let finalize () = if GobConfig.get_bool "dbg.print_tids" then print_tid_info (); diff --git a/src/autoTune.ml b/src/autoTune.ml index 469912cbc1..a8737c693b 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -172,7 +172,7 @@ let focusOnSpecification () = match Svcomp.Specification.of_option () with | UnreachCall s -> () | NoDataRace -> (*enable all thread analyses*) - Logs.info "Specification: NoDataRace -> enabeling thread analyses \"%s\n" (String.concat ", " notNeccessaryThreadAnalyses); + Logs.info "Specification: NoDataRace -> enabeling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses); let enableAnalysis = GobConfig.set_auto "ana.activated[+]" in List.iter enableAnalysis notNeccessaryThreadAnalyses; | NoOverflow -> (*We focus on integer analysis*) diff --git a/src/autoTune0.ml b/src/autoTune0.ml index 60a28c3f26..8f87256854 100644 --- a/src/autoTune0.ml +++ b/src/autoTune0.ml @@ -17,17 +17,16 @@ type complexityFactors = { } let printFactors f = - Logs.debug "functions: %d\n" f.functions; - Logs.debug "functionCalls: %d\n" f.functionCalls; - Logs.debug "loops: %d\n" f.loops; - Logs.debug "loopBreaks: %d\n" f.loopBreaks; - Logs.debug "controlFlowStatements: %d\n" f.controlFlowStatements; - Logs.debug "expressions: %d\n" f.expressions; - Logs.debug "instructions: %d\n" f.instructions; - Logs.debug "integralVars: (%d,%d)\n" (fst f.integralVars) (snd f.integralVars); - Logs.debug "arrayVars: (%d,%d)\n" (fst f.arrayVars) (snd f.arrayVars); - Logs.debug "pointerVars: (%d,%d)\n" (fst f.pointerVars) (snd f.pointerVars); - flush stdout; + Logs.debug "functions: %d" f.functions; + Logs.debug "functionCalls: %d" f.functionCalls; + Logs.debug "loops: %d" f.loops; + Logs.debug "loopBreaks: %d" f.loopBreaks; + Logs.debug "controlFlowStatements: %d" f.controlFlowStatements; + Logs.debug "expressions: %d" f.expressions; + Logs.debug "instructions: %d" f.instructions; + Logs.debug "integralVars: (%d,%d)" (fst f.integralVars) (snd f.integralVars); + Logs.debug "arrayVars: (%d,%d)" (fst f.arrayVars) (snd f.arrayVars); + Logs.debug "pointerVars: (%d,%d)" (fst f.pointerVars) (snd f.pointerVars) class collectComplexityFactorsVisitor(factors) = object diff --git a/src/domains/printable.ml b/src/domains/printable.ml index 0a6e92a3e5..0a907f2bb9 100644 --- a/src/domains/printable.ml +++ b/src/domains/printable.ml @@ -150,12 +150,12 @@ struct let equal_debug x y = (* This debug version checks if we call hashcons enough to have up-to-date tags. Comment out the equal below to use this. This will be even slower than with hashcons disabled! *) if x.BatHashcons.tag = y.BatHashcons.tag then ( (* x.BatHashcons.obj == y.BatHashcons.obj || *) if not (Base.equal x.BatHashcons.obj y.BatHashcons.obj) then - Logs.error "tags are equal but values are not for %a and %a\n" pretty x pretty y; + Logs.error "tags are equal but values are not for %a and %a" pretty x pretty y; assert (Base.equal x.BatHashcons.obj y.BatHashcons.obj); true ) else ( if Base.equal x.BatHashcons.obj y.BatHashcons.obj then - Logs.error "tags are not equal but values are for %a and %a\n" pretty x pretty y; + Logs.error "tags are not equal but values are for %a and %a" pretty x pretty y; assert (not (Base.equal x.BatHashcons.obj y.BatHashcons.obj)); false ) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 16566a6e59..26b5370cf8 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -248,7 +248,7 @@ struct in let write_file f fn = Messages.xml_file_name := fn; - Logs.info "Writing xml to temp. file: %s\n" fn; + Logs.info "Writing xml to temp. file: %s" fn; BatPrintf.fprintf f ""; BatPrintf.fprintf f "%s" Goblintutil.command_line; BatPrintf.fprintf f ""; @@ -288,7 +288,7 @@ struct (*let p_fun f x = p_obj f [ "name", BatString.print, x; "nodes", p_list p_node, SH.find_all funs2node x ] in*) let p_file f x = fprintf f "{\n \"name\": \"%s\",\n \"path\": \"%s\",\n \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in let write_file f fn = - Logs.info "Writing json to temp. file: %s\n" fn; + Logs.info "Writing json to temp. file: %s" fn; fprintf f "{\n \"parameters\": \"%s\",\n " Goblintutil.command_line; fprintf f "\"files\": %a,\n " (p_enum p_file) (SH.keys file2funs); fprintf f "\"results\": [\n %a\n]\n" printJson (Lazy.force table); @@ -303,7 +303,7 @@ struct write_file f (get_string "outfile") | "sarif" -> let open BatPrintf in - Logs.info "Writing Sarif to file: %s\n" (get_string "outfile"); + Logs.info "Writing Sarif to file: %s" (get_string "outfile"); Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list)); | "json-messages" -> let json = `Assoc [ diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index 0ce3c239a7..0f3047176d 100644 --- a/src/framework/cfgTools.ml +++ b/src/framework/cfgTools.ml @@ -450,7 +450,7 @@ let createCFG (file: file) = ); if Messages.tracing then Messages.trace "cfg" "CFG building finished.\n\n"; if get_bool "dbg.verbose" then - Logs.debug "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB); + Logs.debug "cfgF (%a), cfgB (%a)" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB); cfgF, cfgB let createCFG = Timing.wrap "createCFG" createCFG diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index b5fbbdb7b9..a89c088f9e 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -827,7 +827,7 @@ struct | Some {changes; _} -> changes | None -> empty_change_info () in - List.(Logs.info "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (length c.added) (length c.removed)); + List.(Logs.info "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }" (length c.unchanged) (length c.changed) (length c.added) (length c.removed)); let changed_funs = List.filter_map (function | {old = {def = Some (Fun f); _}; diff = None; _} -> @@ -1352,22 +1352,22 @@ struct f_eq () else if b1 then begin if get_bool "dbg.compare_runs.diff" then - Logs.info "Global %a is more precise using left:\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1); + Logs.info "Global %a is more precise using left:\n%a" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1); f_le () end else if b2 then begin if get_bool "dbg.compare_runs.diff" then - Logs.info "Global %a is more precise using right:\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2); + Logs.info "Global %a is more precise using right:\n%a" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2); f_gr () end else begin if get_bool "dbg.compare_runs.diff" then ( - Logs.info "Global %a is incomparable (diff):\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2); - Logs.info "Global %a is incomparable (reverse diff):\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1); + Logs.info "Global %a is incomparable (diff):\n%a" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2); + Logs.info "Global %a is incomparable (reverse diff):\n%a" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1); ); f_uk () end in GH.iter f g1; - Logs.info "globals:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\n" !eq !le !gr !uk + Logs.info "globals:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d" !eq !le !gr !uk let compare_locals h1 h2 = let eq, le, gr, uk = ref 0, ref 0, ref 0, ref 0 in @@ -1380,16 +1380,16 @@ struct incr eq else if b1 then begin if get_bool "dbg.compare_runs.diff" then - Logs.info "%a @@ %a is more precise using left:\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1); + Logs.info "%a @@ %a is more precise using left:\n%a" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1); incr le end else if b2 then begin if get_bool "dbg.compare_runs.diff" then - Logs.info "%a @@ %a is more precise using right:\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2); + Logs.info "%a @@ %a is more precise using right:\n%a" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2); incr gr end else begin if get_bool "dbg.compare_runs.diff" then ( - Logs.info "%a @@ %a is incomparable (diff):\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2); - Logs.info "%a @@ %a is incomparable (reverse diff):\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1); + Logs.info "%a @@ %a is incomparable (diff):\n%a" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2); + Logs.info "%a @@ %a is incomparable (reverse diff):\n%a" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1); ); incr uk end @@ -1399,8 +1399,8 @@ struct let k2 = Set.of_enum @@ PP.keys h2 in let o1 = Set.cardinal @@ Set.diff k1 k2 in let o2 = Set.cardinal @@ Set.diff k2 k1 in - Logs.info "locals: \tequal = %d\tleft = %d[%d]\tright = %d[%d]\tincomparable = %d\n" !eq !le o1 !gr o2 !uk *) - Logs.info "locals: \tequal = %d\tleft = %d\tright = %d\tincomparable = %d\n" !eq !le !gr !uk + Logs.info "locals: \tequal = %d\tleft = %d[%d]\tright = %d[%d]\tincomparable = %d" !eq !le o1 !gr o2 !uk *) + Logs.info "locals: \tequal = %d\tleft = %d\tright = %d\tincomparable = %d" !eq !le !gr !uk let compare_locals_ctx h1 h2 = let eq, le, gr, uk, no2, no1 = ref 0, ref 0, ref 0, ref 0, ref 0, ref 0 in @@ -1417,16 +1417,16 @@ struct f_eq () else if b1 then begin if get_bool "dbg.compare_runs.diff" then - Logs.info "%a is more precise using left:\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1); + Logs.info "%a is more precise using left:\n%a" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1); f_le () end else if b2 then begin if get_bool "dbg.compare_runs.diff" then - Logs.info "%a is more precise using right:\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2); + Logs.info "%a is more precise using right:\n%a" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2); f_gr () end else begin if get_bool "dbg.compare_runs.diff" then ( - Logs.info "%a is incomparable (diff):\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2); - Logs.info "%a is incomparable (reverse diff):\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1); + Logs.info "%a is incomparable (diff):\n%a" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2); + Logs.info "%a is incomparable (reverse diff):\n%a" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1); ); f_uk () end @@ -1440,7 +1440,7 @@ struct (* let k2 = Set.of_enum @@ PP.keys h2 in *) (* let o1 = Set.cardinal @@ Set.diff k1 k2 in *) (* let o2 = Set.cardinal @@ Set.diff k2 k1 in *) - Logs.info "locals_ctx:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\tno_ctx_in_right = %d\tno_ctx_in_left = %d\n" !eq !le !gr !uk !no2 !no1 + Logs.info "locals_ctx:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\tno_ctx_in_right = %d\tno_ctx_in_left = %d" !eq !le !gr !uk !no2 !no1 let compare (name1,name2) (l1,g1) (l2,g2) = let one_ctx (n,_) v h = @@ -1452,7 +1452,8 @@ struct let h2 = PP.create 113 in let _ = LH.fold one_ctx l1 h1 in let _ = LH.fold one_ctx l2 h2 in - Logs.info "\nComparing GlobConstrSys precision of %s (left) with %s (right):\n" name1 name2; + Logs.newline (); + Logs.info "Comparing GlobConstrSys precision of %s (left) with %s (right):" name1 name2; compare_globals g1 g2; compare_locals h1 h2; compare_locals_ctx l1 l2; @@ -1483,10 +1484,11 @@ struct module Compare = CompareHashtbl (Sys.Var) (Sys.Dom) (VH) let compare (name1, name2) vh1 vh2 = - Logs.info "\nComparing EqConstrSys precision of %s (left) with %s (right):\n" name1 name2; + Logs.newline (); + Logs.info "Comparing EqConstrSys precision of %s (left) with %s (right):" name1 name2; let verbose = get_bool "dbg.compare_runs.diff" in let (_, msg) = Compare.compare ~verbose ~name1 vh1 ~name2 vh2 in - Logs.info "EqConstrSys comparison summary: %t\n" (fun () -> msg); + Logs.info "EqConstrSys comparison summary: %t" (fun () -> msg); Logs.newline (); end @@ -1495,10 +1497,11 @@ struct module Compare = CompareHashtbl (GVar) (G) (GH) let compare (name1, name2) vh1 vh2 = - Logs.info "\nComparing globals precision of %s (left) with %s (right):\n" name1 name2; + Logs.newline (); + Logs.info "Comparing globals precision of %s (left) with %s (right):" name1 name2; let verbose = get_bool "dbg.compare_runs.diff" in let (_, msg) = Compare.compare ~verbose ~name1 vh1 ~name2 vh2 in - Logs.info "Globals comparison summary: %t\n" (fun () -> msg); + Logs.info "Globals comparison summary: %t" (fun () -> msg); Logs.newline (); end @@ -1524,12 +1527,13 @@ struct nh let compare (name1, name2) vh1 vh2 = - Logs.info "\nComparing nodes precision of %s (left) with %s (right):\n" name1 name2; + Logs.newline (); + Logs.info "Comparing nodes precision of %s (left) with %s (right):" name1 name2; let vh1' = join_contexts vh1 in let vh2' = join_contexts vh2 in let verbose = get_bool "dbg.compare_runs.diff" in let (_, msg) = Compare.compare ~verbose ~name1 vh1' ~name2 vh2' in - Logs.info "Nodes comparison summary: %t\n" (fun () -> msg); + Logs.info "Nodes comparison summary: %t" (fun () -> msg); Logs.newline (); end diff --git a/src/framework/control.ml b/src/framework/control.ml index e8dc04388d..8850957501 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -348,14 +348,14 @@ struct let test_domain (module D: Lattice.S): unit = let module DP = DomainProperties.All (D) in - Logs.debug "domain testing...: %s\n" (D.name ()); + Logs.debug "domain testing...: %s" (D.name ()); let errcode = QCheck_base_runner.run_tests DP.tests in if (errcode <> 0) then failwith "domain tests failed" in let _ = if (get_bool "dbg.test.domain") then ( - Logs.debug "domain testing analysis...: %s\n" (Spec.name ()); + Logs.debug "domain testing analysis...: %s" (Spec.name ()); test_domain (module Spec.D); test_domain (module Spec.G); ) @@ -518,7 +518,7 @@ struct let warnings = Fpath.(save_run / "warnings.marshalled") in let stats = Fpath.(save_run / "stats.marshalled") in if get_bool "dbg.verbose" then ( - Logs.Format.info "Saving the current configuration to %a, meta-data about this run to %a, and solver statistics to %a\n" Fpath.pp config Fpath.pp meta Fpath.pp solver_stats; + Logs.Format.info "Saving the current configuration to %a, meta-data about this run to %a, and solver statistics to %a" Fpath.pp config Fpath.pp meta Fpath.pp solver_stats; ); GobSys.mkdir_or_exists save_run; GobConfig.write_file config; @@ -531,7 +531,7 @@ struct Yojson.Safe.pretty_to_channel (Stdlib.open_out (Fpath.to_string meta)) Meta.json; (* the above is compact, this is pretty-printed *) if gobview then ( if get_bool "dbg.verbose" then ( - Logs.Format.info "Saving the analysis table to %a, the CIL state to %a, the warning table to %a, and the runtime stats to %a\n" Fpath.pp analyses Fpath.pp cil Fpath.pp warnings Fpath.pp stats; + Logs.Format.info "Saving the analysis table to %a, the CIL state to %a, the warning table to %a, and the runtime stats to %a" Fpath.pp analyses Fpath.pp cil Fpath.pp warnings Fpath.pp stats; ); Serialize.marshal MCPRegistry.registered_name analyses; Serialize.marshal (file, Cabs2cil.environment) cil; diff --git a/src/goblint.ml b/src/goblint.ml index bd588b607b..1925cd1795 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -74,12 +74,12 @@ let main () = | Sys.Break -> (* raised on Ctrl-C if `Sys.catch_break true` *) do_stats (); (* Printexc.print_backtrace BatInnerIO.stderr *) - Logs.error "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!")); + Logs.error "%s" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!")); Goblint_timing.teardown_tef (); exit 131 (* same exit code as without `Sys.catch_break true`, otherwise 0 *) | Timeout -> do_stats (); - Logs.error "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!")); + Logs.error "%s" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!")); Goblint_timing.teardown_tef (); exit 124 diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 9c3171376b..28aa65b2fe 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -10,16 +10,16 @@ let writeconffile = ref None (** Print version and bail. *) let print_version ch = - Logs.info "Goblint version: %s\n" Version.goblint; - Logs.info "Cil version: %s\n" Cil.cilVersion; - Logs.info "Dune profile: %s\n" ConfigProfile.profile; - Logs.info "OCaml version: %s\n" Sys.ocaml_version; - Logs.info "OCaml flambda: %s\n" ConfigOcaml.flambda; + Logs.info "Goblint version: %s" Version.goblint; + Logs.info "Cil version: %s" Cil.cilVersion; + Logs.info "Dune profile: %s" ConfigProfile.profile; + Logs.info "OCaml version: %s" Sys.ocaml_version; + Logs.info "OCaml flambda: %s" ConfigOcaml.flambda; if get_bool "dbg.verbose" then ( - Logs.debug "Library versions:\n"; + Logs.debug "Library versions:"; List.iter (fun (name, version) -> let version = Option.default "[unknown]" version in - Logs.debug " %s: %s\n" name version + Logs.debug " %s: %s" name version ) Goblint_build_info.statically_linked_libraries ); exit 0 @@ -129,7 +129,7 @@ and complete args = raise Exit (* TODO: remove *) -let eprint_color m = Logs.info "%s\n" (MessageUtil.colorize ~fd:Unix.stderr m) +let eprint_color m = Logs.info "%s" (MessageUtil.colorize ~fd:Unix.stderr m) let check_arguments () = let fail m = (let m = "Option failure: " ^ m in eprint_color ("{red}"^m); failwith m) in(* unused now, but might be useful for future checks here *) @@ -250,7 +250,7 @@ let preprocess_files () = if get_bool "dbg.verbose" then ( Logs.debug "Custom include dirs:"; List.iteri (fun i custom_include_dir -> - Logs.Format.debug " %d. %a (exists=%B)\n" (i + 1) Fpath.pp custom_include_dir (Sys.file_exists (Fpath.to_string custom_include_dir)) + Logs.Format.debug " %d. %a (exists=%B)" (i + 1) Fpath.pp custom_include_dir (Sys.file_exists (Fpath.to_string custom_include_dir)) ) custom_include_dirs ); let custom_include_dirs = List.filter (Sys.file_exists % Fpath.to_string) custom_include_dirs in @@ -444,9 +444,9 @@ let preprocess_parse_merge () = let do_stats () = if get_bool "dbg.timing.enabled" then ( Logs.newline (); - Logs.info "vars = %d evals = %d narrow_reuses = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses; + Logs.info "vars = %d evals = %d narrow_reuses = %d" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses; Logs.newline (); - Logs.info "Timings:\n"; + Logs.info "Timings:"; Timing.Default.print (Format.formatter_of_out_channel @@ Messages.get_out "timing" Legacy.stderr); flush_all () ) @@ -475,7 +475,7 @@ let do_analyze change_info merged_AST = if get_bool "dbg.verbose" then Logs.info "And now... the Goblin!"; let (stf,exf,otf as funs) = Cilfacade.getFuns merged_AST in if stf@exf@otf = [] then raise (FrontendError "no suitable function to start from"); - if get_bool "dbg.verbose" then Logs.debug "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a\n" + if get_bool "dbg.verbose" then Logs.debug "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a" L.pretty stf L.pretty exf L.pretty otf; (* and here we run the analysis! *) @@ -514,11 +514,11 @@ let do_html_output () = let command = "java -jar "^ jar ^" --num-threads " ^ (string_of_int (jobs ())) ^ " --dot-timeout 0 --result-dir "^ (get_string "outfile")^" "^ !Messages.xml_file_name in try match Timing.wrap "g2html" Unix.system command with | Unix.WEXITED 0 -> () - | _ -> Logs.error "HTML generation failed! Command: %s\n" command + | _ -> Logs.error "HTML generation failed! Command: %s" command with Unix.Unix_error (e, f, a) -> - Logs.error "%s at syscall %s with argument \"%s\".\n" (Unix.error_message e) f a + Logs.error "%s at syscall %s with argument \"%s\"." (Unix.error_message e) f a ) else - Logs.error "Warning: jar file %s not found.\n" jar + Logs.error "Warning: jar file %s not found." jar ) let do_gobview cilfile = @@ -563,7 +563,7 @@ let do_gobview cilfile = ) dist_files ) else - Logs.error "Warning: Cannot locate GobView.\n" + Logs.error "Warning: Cannot locate GobView." ) let handle_extraspecials () = diff --git a/src/messagesCompare.ml b/src/messagesCompare.ml index beef0913d7..d523737542 100644 --- a/src/messagesCompare.ml +++ b/src/messagesCompare.ml @@ -34,12 +34,12 @@ let () = let right_only_messages = MS.diff right_messages left_messages in if not (MS.is_empty left_only_messages) then ( - Logs.info "Left-only messages (%d):\n" (MS.cardinal left_only_messages); + Logs.info "Left-only messages (%d):" (MS.cardinal left_only_messages); MS.iter (Messages.print) left_only_messages; ); Logs.newline (); if not (MS.is_empty right_only_messages) then ( - Logs.info "Right-only messages (%d):\n" (MS.cardinal right_only_messages); + Logs.info "Right-only messages (%d):" (MS.cardinal right_only_messages); MS.iter (Messages.print) right_only_messages; ) | _ -> diff --git a/src/solvers/generic.ml b/src/solvers/generic.ml index 207ce80512..b724c71dc9 100644 --- a/src/solvers/generic.ml +++ b/src/solvers/generic.ml @@ -96,11 +96,11 @@ struct (* ignore @@ Pretty.printf "max #contexts: %d for %s\n" n max_k; *) ncontexts := Hashtbl.fold (fun _ -> (+)) histo 0; let topn = 5 in - Logs.debug "Found %d contexts for %d functions. Top %d functions:\n" !ncontexts (Hashtbl.length histo) topn; + Logs.debug "Found %d contexts for %d functions. Top %d functions:" !ncontexts (Hashtbl.length histo) topn; Hashtbl.to_list histo |> List.sort (fun (_,n1) (_,n2) -> compare n2 n1) |> List.take topn - |> List.iter @@ fun (k,n) -> Logs.debug "%d\tcontexts for %s\n" n k + |> List.iter @@ fun (k,n) -> Logs.debug "%d\tcontexts for %s" n k let stats_csv = let save_run_str = GobConfig.get_string "save_run" in @@ -115,9 +115,9 @@ struct let print_stats _ = Logs.newline (); (* print_endline "# Generic solver stats"; *) - Logs.info "runtime: %s\n" (string_of_time ()); - Logs.info "vars: %d, evals: %d\n" !Goblintutil.vars !Goblintutil.evals; - Option.may (fun v -> ignore @@ Logs.info "max updates: %d for var %a\n" !max_c Var.pretty_trace v) !max_var; + Logs.info "runtime: %s" (string_of_time ()); + Logs.info "vars: %d, evals: %d" !Goblintutil.vars !Goblintutil.evals; + Option.may (fun v -> ignore @@ Logs.info "max updates: %d for var %a" !max_c Var.pretty_trace v) !max_var; Logs.newline (); (* print_endline "# Solver specific stats"; *) !print_solver_stats (); diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml index 16cd30652a..209402a0bc 100644 --- a/src/solvers/postSolver.ml +++ b/src/solvers/postSolver.ml @@ -129,7 +129,7 @@ module SaveRun: F = let save_run = Fpath.v save_run_str in let solver = Fpath.(save_run / solver_file) in if get_bool "dbg.verbose" then - Logs.Format.info "Saving the solver result to %a\n" Fpath.pp solver; + Logs.Format.info "Saving the solver result to %a" Fpath.pp solver; GobSys.mkdir_or_exists save_run; Serialize.marshal vh solver end @@ -179,7 +179,7 @@ struct let post xs vs vh = if get_bool "dbg.verbose" then - Logs.debug "Postsolving\n"; + Logs.debug "Postsolving"; let module StartS = struct diff --git a/src/solvers/sLR.ml b/src/solvers/sLR.ml index 2f93516530..d3ee93751a 100644 --- a/src/solvers/sLR.ml +++ b/src/solvers/sLR.ml @@ -152,8 +152,9 @@ module SLR3 = stop_event (); if GobConfig.get_bool "dbg.print_wpoints" then ( - Logs.debug "\nWidening points:\n"; - HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; Logs.newline (); ); @@ -446,8 +447,9 @@ module Make0 = let _ = loop () in if GobConfig.get_bool "dbg.print_wpoints" then ( - Logs.debug "\nWidening points:\n"; - HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; Logs.newline (); ); diff --git a/src/solvers/sLRphased.ml b/src/solvers/sLRphased.ml index b8570c42e9..a347fc0bf8 100644 --- a/src/solvers/sLRphased.ml +++ b/src/solvers/sLRphased.ml @@ -188,8 +188,9 @@ module Make = stop_event (); if GobConfig.get_bool "dbg.print_wpoints" then ( - Logs.debug "\nWidening points:\n"; - HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; Logs.newline (); ); diff --git a/src/solvers/sLRterm.ml b/src/solvers/sLRterm.ml index 6db9d59aa3..a9fd5f5f4b 100644 --- a/src/solvers/sLRterm.ml +++ b/src/solvers/sLRterm.ml @@ -48,11 +48,11 @@ module SLR3term = let count_side = ref (max_int - 1) in let () = print_solver_stats := fun () -> - Logs.info "wpoint: %d, rho: %d, rho': %d, q: %d, count: %d, count_side: %d\n" (HM.length wpoint) (HM.length rho) (HPM.length rho') (H.size !q) (Int.neg !count) (max_int - !count_side); + Logs.info "wpoint: %d, rho: %d, rho': %d, q: %d, count: %d, count_side: %d" (HM.length wpoint) (HM.length rho) (HPM.length rho') (H.size !q) (Int.neg !count) (max_int - !count_side); let histo = Hashtbl.create 13 in (* histogram: node id -> number of contexts *) HM.iter (fun k _ -> Hashtbl.modify_def 1 (S.Var.var_id k) ((+)1) histo) rho; let vid,n = Hashtbl.fold (fun k v (k',v') -> if v > v' then k,v else k',v') histo (Obj.magic (), 0) in - Logs.info "max #contexts: %d for var_id %s\n" n vid + Logs.info "max #contexts: %d for var_id %s" n vid in let init ?(side=false) x = @@ -206,8 +206,9 @@ module SLR3term = stop_event (); if GobConfig.get_bool "dbg.print_wpoints" then ( - Logs.debug "\nWidening points:\n"; - HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; Logs.newline (); ); diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index c3e35d4af4..90f3faa6bb 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -76,7 +76,7 @@ module Base = let print_data data str = if GobConfig.get_bool "dbg.verbose" then ( - Logs.info "%s:\n|rho|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d\n" + Logs.info "%s:\n|rho|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d" str (HM.length data.rho) (HM.length data.stable) (HM.length data.infl) (HM.length data.wpoint) (HM.length data.side_dep) (HM.length data.side_infl) (HM.length data.var_messages) (HM.length data.rho_write) (HM.length data.dep); Hooks.print_data () ) @@ -86,7 +86,7 @@ module Base = (* every variable in (pruned) rho should be stable *) HM.iter (fun x _ -> if not (HM.mem data.stable x) then ( - Logs.warn "unstable in rho: %a\n" S.Var.pretty_trace x; + Logs.warn "unstable in rho: %a" S.Var.pretty_trace x; assert false ) ) data.rho @@ -241,7 +241,7 @@ module Base = let dep = data.dep in let () = print_solver_stats := fun () -> - Logs.info "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d\n" + Logs.info "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d" (HM.length rho) (HM.length called) (HM.length stable) (HM.length infl) (HM.length wpoint) (HM.length side_dep) (HM.length side_infl) (HM.length var_messages) (HM.length rho_write) (HM.length dep); Hooks.print_data (); print_context_stats rho @@ -388,7 +388,7 @@ module Base = and side ?x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *) if tracing then trace "sol2" "side to %a (wpx: %b) from %a ## value: %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d; if Hooks.system y <> None then ( - Logs.warn "side-effect to unknown w/ rhs: %a, contrib: %a\n" S.Var.pretty_trace y S.Dom.pretty d; + Logs.warn "side-effect to unknown w/ rhs: %a, contrib: %a" S.Var.pretty_trace y S.Dom.pretty d; ); assert (Hooks.system y = None); init y; @@ -496,7 +496,7 @@ module Base = let restart_leaf x = if tracing then trace "sol2" "Restarting to bot %a\n" S.Var.pretty_trace x; - Logs.debug "Restarting to bot %a\n" S.Var.pretty_trace x; + Logs.debug "Restarting to bot %a" S.Var.pretty_trace x; HM.replace rho x (S.Dom.bot ()); (* HM.remove rho x; *) HM.remove wpoint x; (* otherwise gets immediately widened during resolve *) @@ -630,7 +630,7 @@ module Base = Logs.debug "Destabilizing sides of changed functions, primary old nodes and removed functions ..."; List.iter (fun k -> if HM.mem stable k then ( - Logs.debug "marked %a\n" S.Var.pretty_trace k; + Logs.debug "marked %a" S.Var.pretty_trace k; destabilize k ) ) sys_change.delete @@ -662,7 +662,7 @@ module Base = List.iter (fun v -> if Hooks.system v <> None then - Logs.warn "Trying to restart non-leaf unknown %a. This has no effect.\n" S.Var.pretty_trace v + Logs.warn "Trying to restart non-leaf unknown %a. This has no effect." S.Var.pretty_trace v else if HM.mem stable v then destabilize_leaf v ) sys_change.restart; @@ -681,7 +681,7 @@ module Base = if should_restart_start then ( match GobList.assoc_eq_opt S.Var.equal v data.st with | Some old_d when not (S.Dom.equal old_d d) -> - Logs.debug "Destabilizing and restarting changed start var %a\n" S.Var.pretty_trace v; + Logs.debug "Destabilizing and restarting changed start var %a" S.Var.pretty_trace v; restart_and_destabilize v (* restart side effect from start *) | _ -> (* don't restart unchanged start global *) @@ -698,7 +698,7 @@ module Base = | None -> (* restart removed start global to allow it to be pruned from incremental solution *) (* this gets rid of its warnings and makes comparing with from scratch sensible *) - Logs.debug "Destabilizing and restarting removed start var %a\n" S.Var.pretty_trace v; + Logs.debug "Destabilizing and restarting removed start var %a" S.Var.pretty_trace v; restart_and_destabilize v | _ -> () @@ -718,7 +718,7 @@ module Base = (* before delete_marked because we also want to restart write-only side effects from deleted nodes *) HM.iter (fun x w -> HM.iter (fun y d -> - Logs.debug "Restarting write-only to bot %a\n" S.Var.pretty_trace y; + Logs.debug "Restarting write-only to bot %a" S.Var.pretty_trace y; HM.replace rho y (S.Dom.bot ()); ) w ) rho_write @@ -735,7 +735,7 @@ module Base = Logs.debug "Separately solving changed functions..."; HM.iter (fun x (old_rho, old_infl) -> HM.replace rho x old_rho; HM.replace infl x old_infl) old_ret; HM.iter (fun x (old_rho, old_infl) -> - Logs.debug "test for %a\n" Node.pretty_trace (S.Var.node x); + Logs.debug "test for %a" Node.pretty_trace (S.Var.node x); solve x Widen; if not (S.Dom.equal (HM.find rho x) old_rho) then ( Logs.debug "Further destabilization happened ..."; @@ -763,8 +763,8 @@ module Base = if unstable_vs <> [] then ( if GobConfig.get_bool "dbg.verbose" then ( if !i = 1 then Logs.newline (); - Logs.debug "Unstable solver start vars in %d. phase:\n" !i; - List.iter (fun v -> Logs.debug "\t%a\n" S.Var.pretty_trace v) unstable_vs; + Logs.debug "Unstable solver start vars in %d. phase:" !i; + List.iter (fun v -> Logs.debug "\t%a" S.Var.pretty_trace v) unstable_vs; Logs.newline (); flush_all (); ); @@ -784,12 +784,12 @@ module Base = HM.replace visited y (); let mem = HM.mem rho y in let d' = try HM.find rho y with Not_found -> S.Dom.bot () in - if not (S.Dom.leq d d') then Logs.error "TDFP Fixpoint not reached in restore step at side-effected variable (mem: %b) %a from %a: %a not leq %a\n" mem S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d S.Dom.pretty d' + if not (S.Dom.leq d d') then Logs.error "TDFP Fixpoint not reached in restore step at side-effected variable (mem: %b) %a from %a: %a not leq %a" mem S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d S.Dom.pretty d' in let rec eq check x = HM.replace visited x (); match Hooks.system x with - | None -> if HM.mem rho x then HM.find rho x else (Logs.warn "TDFP Found variable %a w/o rhs and w/o value in rho\n" S.Var.pretty_trace x; S.Dom.bot ()) + | None -> if HM.mem rho x then HM.find rho x else (Logs.warn "TDFP Found variable %a w/o rhs and w/o value in rho" S.Var.pretty_trace x; S.Dom.bot ()) | Some f -> f (get ~check) (check_side x) and get ?(check=false) x = if HM.mem visited x then ( @@ -798,7 +798,7 @@ module Base = let d1 = HM.find rho x in let d2 = eq check x in (* just to reach unrestored variables *) if check then ( - if not (HM.mem stable x) && Hooks.system x <> None then Logs.error "TDFP Found an unknown in rho that should be stable: %a\n" S.Var.pretty_trace x; + if not (HM.mem stable x) && Hooks.system x <> None then Logs.error "TDFP Found an unknown in rho that should be stable: %a" S.Var.pretty_trace x; if not (S.Dom.leq d2 d1) then Logs.error "TDFP Fixpoint not reached in restore step at %a\n @[Variable:\n%a\nRight-Hand-Side:\n%a\nCalculating one more step changes: %a\n@]" S.Var.pretty_trace x S.Dom.pretty d1 S.Dom.pretty d2 S.Dom.pretty_diff (d1,d2); ); @@ -822,7 +822,7 @@ module Base = HM.filteri_inplace (fun x _ -> HM.mem visited x) rho in Timing.wrap "restore" restore (); - if GobConfig.get_bool "dbg.verbose" then Logs.debug "Solved %d vars. Total of %d vars after restore.\n" !Goblintutil.vars (HM.length rho); + if GobConfig.get_bool "dbg.verbose" then Logs.debug "Solved %d vars. Total of %d vars after restore." !Goblintutil.vars (HM.length rho); let avg xs = if List.is_empty !cache_sizes then 0.0 else float_of_int (BatList.sum xs) /. float_of_int (List.length xs) in if tracing then trace "cache" "#caches: %d, max: %d, avg: %.2f\n" (List.length !cache_sizes) (List.max !cache_sizes) (avg !cache_sizes); ); @@ -831,8 +831,9 @@ module Base = print_data data "Data after solve completed"; if GobConfig.get_bool "dbg.print_wpoints" then ( - Logs.debug "\nWidening points:\n"; - HM.iter (fun k () -> Logs.debug "%a\n" S.Var.pretty_trace k) wpoint; + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; Logs.newline (); ); @@ -1075,7 +1076,7 @@ module DepVals: GenericEqIncrSolver = module HM = HM let print_data () = - Logs.info "|dep_vals|=%d\n" (HM.length !current_dep_vals) + Logs.info "|dep_vals|=%d" (HM.length !current_dep_vals) let system x = match S.system x with diff --git a/src/solvers/topDown_space_cache_term.ml b/src/solvers/topDown_space_cache_term.ml index 450235854c..1767dffafc 100644 --- a/src/solvers/topDown_space_cache_term.ml +++ b/src/solvers/topDown_space_cache_term.ml @@ -142,7 +142,7 @@ module WP = let rec get x = if HM.mem visited x then ( if not (HM.mem rho x) then ( - Logs.warn "Found an unknown that should be a widening point: %a\n" S.Var.pretty_trace x; + Logs.warn "Found an unknown that should be a widening point: %a" S.Var.pretty_trace x; S.Dom.top () ) else HM.find rho x @@ -150,7 +150,7 @@ module WP = HM.replace visited x (); let check_side y d = let d' = try HM.find rho y with Not_found -> S.Dom.bot () in - if not (S.Dom.leq d d') then Logs.error "Fixpoint not reached in restore step at side-effected variable %a: %a not leq %a\n" S.Var.pretty_trace y S.Dom.pretty d S.Dom.pretty d' + if not (S.Dom.leq d d') then Logs.error "Fixpoint not reached in restore step at side-effected variable %a: %a not leq %a" S.Var.pretty_trace y S.Dom.pretty d S.Dom.pretty d' in let eq x = match S.system x with @@ -182,7 +182,7 @@ module WP = List.iter get vs in Timing.wrap "restore" restore (); - if (GobConfig.get_bool "dbg.verbose") then Logs.debug "Solved %d vars. Total of %d vars after restore.\n" !Goblintutil.vars (HM.length rho); + if (GobConfig.get_bool "dbg.verbose") then Logs.debug "Solved %d vars. Total of %d vars after restore." !Goblintutil.vars (HM.length rho); ); let avg xs = float_of_int (BatList.sum xs) /. float_of_int (List.length xs) in if tracing then trace "cache" "#caches: %d, max: %d, avg: %.2f\n" (List.length !cache_sizes) (List.max !cache_sizes) (avg !cache_sizes); diff --git a/src/spec/specUtil.ml b/src/spec/specUtil.ml index 6c7fbae904..0c0fc16fd7 100644 --- a/src/spec/specUtil.ml +++ b/src/spec/specUtil.ml @@ -33,8 +33,11 @@ let parse ?repl:(repl=false) ?print:(print=false) ?dot:(dot=false) cin = | SpecCore.Eof -> let nodes = List.filter_map (function SpecCore.Node x -> Some x | _ -> None) !defs in let edges = List.filter_map (function SpecCore.Edge x -> Some x | _ -> None) !defs in - if print then Logs.debug "\n#Definitions: %i, #Nodes: %i, #Edges: %i\n" - (List.length !defs) (List.length nodes) (List.length edges); + if print then ( + Logs.newline (); + Logs.debug "#Definitions: %i, #Nodes: %i, #Edges: %i" + (List.length !defs) (List.length nodes) (List.length edges) + ); if save_dot && not dot then ( let dotgraph = SpecCore.to_dot_graph !defs in output_file ~filename:"result/graph.dot" ~text:dotgraph; diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index 19f56c3c32..3b2fc41544 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -119,7 +119,7 @@ let callConstructors ast = !cons in let d_fundec () fd = Pretty.text fd.svar.vname in - if get_bool "dbg.verbose" then ignore (Logs.debug "Constructors: %a\n" (Pretty.d_list ", " d_fundec) constructors); + if get_bool "dbg.verbose" then ignore (Logs.debug "Constructors: %a" (Pretty.d_list ", " d_fundec) constructors); visitCilFileSameGlobals (new addConstructors constructors) ast; ast @@ -144,9 +144,9 @@ let getFuns fileAST : startfuns = | GFun({svar={vname=mn; _}; _} as def,_) when List.mem mn (get_string_list "exitfun") -> add_exit def acc | GFun({svar={vname=mn; _}; _} as def,_) when List.mem mn (get_string_list "otherfun") -> add_other def acc | GFun({svar={vname=mn; vattr=attr; _}; _} as def, _) when get_bool "kernel" && is_init attr -> - Logs.debug "Start function: %s\n" mn; set_string "mainfun[+]" mn; add_main def acc + Logs.debug "Start function: %s" mn; set_string "mainfun[+]" mn; add_main def acc | GFun({svar={vname=mn; vattr=attr; _}; _} as def, _) when get_bool "kernel" && is_exit attr -> - Logs.debug "Cleanup function: %s\n" mn; set_string "exitfun[+]" mn; add_exit def acc + Logs.debug "Cleanup function: %s" mn; set_string "exitfun[+]" mn; add_exit def acc | GFun ({svar={vstorage=NoStorage; _}; _} as def, _) when (get_bool "nonstatic") -> add_other def acc | GFun ({svar={vattr; _}; _} as def, _) when get_bool "allfuns" && not (Cil.hasAttribute "goblint_stub" vattr) -> add_other def acc | _ -> acc diff --git a/src/util/compilationDatabase.ml b/src/util/compilationDatabase.ml index a49dca3dab..586d39f3b7 100644 --- a/src/util/compilationDatabase.ml +++ b/src/util/compilationDatabase.ml @@ -69,7 +69,7 @@ let load_and_preprocess ~all_cppflags filename = let old_root = GobFpath.rem_find_prefix database_dir original_database_dir in let new_root = GobFpath.rem_find_prefix original_database_dir database_dir in if GobConfig.get_bool "dbg.verbose" then - Logs.Format.debug "Rerooting compilation database\n from %a\n to %a\n" Fpath.pp old_root Fpath.pp new_root; + Logs.Format.debug "Rerooting compilation database\n from %a\n to %a" Fpath.pp old_root Fpath.pp new_root; let reroot_path p = Fpath.append new_root (Option.get (Fpath.relativize ~root:old_root p)) in @@ -127,7 +127,7 @@ let load_and_preprocess ~all_cppflags filename = in let cwd = reroot_path obj.directory in if GobConfig.get_bool "dbg.verbose" then - Logs.Format.debug "Preprocessing %a\n to %a\n using %s\n in %a\n" Fpath.pp file Fpath.pp preprocessed_file preprocess_command Fpath.pp cwd; + Logs.Format.debug "Preprocessing %a\n to %a\n using %s\n in %a" Fpath.pp file Fpath.pp preprocessed_file preprocess_command Fpath.pp cwd; let preprocess_task = {ProcessPool.command = preprocess_command; cwd = Some cwd} in (* command/arguments might have paths relative to directory *) Some (preprocessed_file, Some preprocess_task) in diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 624cf748a4..865de4d704 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -178,7 +178,7 @@ struct else Select (fld, parse_path' pth) end with PathParseError -> - Logs.error "Error: Couldn't parse the json path '%s'\n" s; + Logs.error "Error: Couldn't parse the json path '%s'" s; failwith "parsing" (** Here we store the actual configuration. *) @@ -301,10 +301,10 @@ struct if tracing then trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x; try f x with Yojson.Safe.Util.Type_error (s, _) -> - Logs.error "The value for '%s' has the wrong type: %s\n" st s; + Logs.error "The value for '%s' has the wrong type: %s" st s; failwith "get_path_string" with ConfTypeError -> - Logs.Batteries.error "Cannot find value '%s' in\n%t\nDid You forget to add default values to options.schema.json?\n" + Logs.Batteries.error "Cannot find value '%s' in\n%t\nDid You forget to add default values to options.schema.json?" st print; failwith "get_path_string" let get_json : string -> Yojson.Safe.t = get_path_string Fun.id @@ -377,7 +377,7 @@ struct with Yojson.Json_error _ | TypeError _ -> set_string st s with e -> - Logs.error "Cannot set %s to '%s'.\n" st s; + Logs.error "Cannot set %s to '%s'." st s; raise e let merge json = diff --git a/src/util/jsonSchema.ml b/src/util/jsonSchema.ml index 9eaefc6549..0b4c6479b2 100644 --- a/src/util/jsonSchema.ml +++ b/src/util/jsonSchema.ml @@ -104,7 +104,7 @@ let rec element_defaults ?additional_field (element: element): Yojson.Safe.t = (name, element_defaults ?additional_field field_element) ) object_specs.properties) | _ -> - Logs.Format.error "%a\n" Json_schema.pp (create element); + Logs.Format.error "%a" Json_schema.pp (create element); failwith "element_defaults" end @@ -135,7 +135,7 @@ let rec element_require_all (element: element): element = in Object { object_specs with properties = properties' } | _ -> - Logs.Format.error "%a\n" Json_schema.pp (create element); + Logs.Format.error "%a" Json_schema.pp (create element); failwith "element_require_all" in { element with kind = kind' } diff --git a/src/util/options.ml b/src/util/options.ml index 65ccb7e09f..74583af2f1 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -27,7 +27,7 @@ let rec element_paths (element: element): string list = List.map (fun path -> name ^ "." ^ path) (element_paths field_element) ) object_specs.properties | _ -> - Logs.Format.error "%a\n" Json_schema.pp (create element); + Logs.Format.error "%a" Json_schema.pp (create element); failwith "element_paths" let schema_paths (schema: schema): string list = @@ -69,7 +69,7 @@ let rec element_completions (element: element): (string * string list) list = List.map (fun (path, cs) -> (name ^ "." ^ path, cs)) (element_completions field_element) ) object_specs.properties | _ -> - Logs.Format.error "%a\n" Json_schema.pp (create element); + Logs.Format.error "%a" Json_schema.pp (create element); failwith "element_completions" let schema_completions (schema: schema): (string * string list) list = diff --git a/src/util/precCompare.ml b/src/util/precCompare.ml index e2c9391dd5..bfb7031f51 100644 --- a/src/util/precCompare.ml +++ b/src/util/precCompare.ml @@ -79,7 +79,7 @@ struct match c with | {Comparison.more_precise = 0; less_precise = 0; incomparable = 0; _} -> () | _ -> - if verbose then Logs.debug "%a: %t\n" K.pretty k (fun () -> msg) + if verbose then Logs.debug "%a: %t" K.pretty k (fun () -> msg) ) compared; let c = KH.fold (fun _ (c, _) acc -> Comparison.aggregate_same c acc) compared Comparison.empty in let msg = Pretty.dprintf "%s %s %s (%s)" name1 (Comparison.to_string_infix c) name2 (Comparison.to_string_counts c) in @@ -127,6 +127,7 @@ struct |> List.filter (fun ((i1, _), (i2, _)) -> i1 <> i2) |> List.map (Tuple2.map snd snd) |> List.map (uncurry compare_dumps) - |> List.iter (fun (_, msg) -> Logs.info "%t\n" (fun () -> msg)); - Logs.info "\nTotal locations: %d\nTotal %s: %d\n" locations_count (Key.name ()) location_vars_count + |> List.iter (fun (_, msg) -> Logs.info "%t" (fun () -> msg)); + Logs.newline (); + Logs.info "Total locations: %d\nTotal %s: %d" locations_count (Key.name ()) location_vars_count end diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index 796085bf14..a11609983e 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -10,7 +10,7 @@ let is_bad name = | _ -> true in if GobConfig.get_bool "dbg.verbose" then - Logs.debug "Preprocessor %s: is_bad=%B\n" name r; + Logs.debug "Preprocessor %s: is_bad=%B" name r; r let compgen prefix = diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 93d72661c1..025005b52e 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -260,7 +260,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) let print_svcomp_result (s: string): unit = - Logs.info "SV-COMP result: %s\n" s + Logs.info "SV-COMP result: %s" s let print_task_result (module TaskResult:TaskResult): unit = print_svcomp_result (Result.to_string TaskResult.result) @@ -272,7 +272,7 @@ let init (module FileCfg: MyCFG.FileCfg) = let specification = Svcomp.Specification.of_option () end in - Logs.info "SV-COMP specification: %s\n" (Svcomp.Specification.to_string Task.specification); + Logs.info "SV-COMP specification: %s" (Svcomp.Specification.to_string Task.specification); Svcomp.task := Some (module Task) module Result (R: ResultQuery.SpecSysSol2) = diff --git a/src/witness/z3/violationZ3.z3.ml b/src/witness/z3/violationZ3.z3.ml index bf6af6cdf6..81d48e10f3 100644 --- a/src/witness/z3/violationZ3.z3.ml +++ b/src/witness/z3/violationZ3.z3.ml @@ -152,16 +152,16 @@ struct end and do_assert revpath' i env' expr = - Logs.debug "%d: %s\n" i (Expr.to_string expr); + Logs.debug "%d: %s" i (Expr.to_string expr); let track_const = Boolean.mk_const ctx (Symbol.mk_int ctx i) in Solver.assert_and_track solver expr track_const; let status = Solver.check solver [] in - Logs.debug "%d: %s\n" i (Solver.string_of_status status); + Logs.debug "%d: %s" i (Solver.string_of_status status); match Solver.check solver [] with | Solver.SATISFIABLE -> - Logs.info "%d: %s\n" i (Model.to_string (BatOption.get @@ Solver.get_model solver)); + Logs.info "%d: %s" i (Model.to_string (BatOption.get @@ Solver.get_model solver)); iter_wp revpath' (i - 1) env' | Solver.UNSATISFIABLE -> From 3dcf4924fd87655325ed62922eb9a66e2b31c50a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 16:31:01 +0200 Subject: [PATCH 10/39] Implement Logs.newline --- src/util/logs.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/util/logs.ml b/src/util/logs.ml index db694532e0..cce0d8fa21 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -54,7 +54,8 @@ struct let warn = log let error = log - let newline () = () + let newline () = + prerr_newline () end module Pretty = MakeKind (PrettyKind) From 9c4d1b8aa29900ef3531d3090bd3676872591235 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 16:43:56 +0200 Subject: [PATCH 11/39] Extract GobPretty.igprintf from Tracing --- src/util/gobPretty.ml | 51 ++++++++++++++++++++++++++++++++++++++++++ src/util/messages.ml | 6 ++--- src/util/tracing.ml | 52 +------------------------------------------ 3 files changed, 55 insertions(+), 54 deletions(-) create mode 100644 src/util/gobPretty.ml diff --git a/src/util/gobPretty.ml b/src/util/gobPretty.ml new file mode 100644 index 0000000000..92e3a9e75e --- /dev/null +++ b/src/util/gobPretty.ml @@ -0,0 +1,51 @@ +open GoblintCil.Pretty + +(* Parses a format string to generate a nop-function of the correct type. *) +let igprintf (finish: 'b) (format : ('a, unit, doc, 'b) format4) : 'a = + let format = string_of_format format in + let flen = String.length format in + let fget = String.unsafe_get format in + let rec literal acc i = + let rec skipChars j = + if j >= flen || (match fget j with '%' | '@' | '\n' -> true | _ -> false) then + collect nil j + else + skipChars (succ j) + in + skipChars (succ i) + and collect (acc: doc) (i: int) = + if i >= flen then begin + Obj.magic finish + end else begin + let c = fget i in + if c = '%' then begin + let j = skip_args (succ i) in + match fget j with + '%' -> literal acc j + | ',' -> collect acc (succ j) + | 's' | 'c' | 'd' | 'i' | 'o' | 'x' | 'X' | 'u' + | 'f' | 'e' | 'E' | 'g' | 'G' | 'b' | 'B' -> + Obj.magic(fun b -> collect nil (succ j)) + | 'L' | 'l' | 'n' -> Obj.magic(fun n -> collect nil (succ (succ j))) + | 'a' -> Obj.magic(fun pprinter arg -> collect nil (succ j)) + | 't' -> Obj.magic(fun pprinter -> collect nil (succ j)) + | c -> invalid_arg ("dprintf: unknown format %s" ^ String.make 1 c) + end else if c = '@' then begin + if i + 1 < flen then begin + match fget (succ i) with + '[' | ']' | '!' | '?' | '^' | '@' -> collect nil (i + 2) + | '<' | '>' -> collect nil (i + 1) + | c -> invalid_arg ("dprintf: unknown format @" ^ String.make 1 c) + end else + invalid_arg "dprintf: incomplete format @" + end else if c = '\n' then begin + collect nil (i + 1) + end else + literal acc i + end + and skip_args j = + match String.unsafe_get format j with + '0' .. '9' | ' ' | '.' | '-' -> skip_args (succ j) + | c -> j + in + collect nil 0 diff --git a/src/util/messages.ml b/src/util/messages.ml index 0d05d97236..fb4fba81e6 100644 --- a/src/util/messages.ml +++ b/src/util/messages.ml @@ -260,7 +260,7 @@ let msg severity ?loc ?(tags=[]) ?(category=Category.Unknown) fmt = Pretty.gprintf finish fmt ) else - Tracing.mygprintf () fmt + GobPretty.igprintf () fmt let msg_noloc severity ?(tags=[]) ?(category=Category.Unknown) fmt = if !GU.should_warn && Severity.should_warn severity && (Category.should_warn category || Tags.should_warn tags) then ( @@ -271,7 +271,7 @@ let msg_noloc severity ?(tags=[]) ?(category=Category.Unknown) fmt = Pretty.gprintf finish fmt ) else - Tracing.mygprintf () fmt + GobPretty.igprintf () fmt let msg_group severity ?(tags=[]) ?(category=Category.Unknown) fmt = if !GU.should_warn && Severity.should_warn severity && (Category.should_warn category || Tags.should_warn tags) then ( @@ -286,7 +286,7 @@ let msg_group severity ?(tags=[]) ?(category=Category.Unknown) fmt = Pretty.gprintf finish fmt ) else - Tracing.mygprintf (fun msgs -> ()) fmt + GobPretty.igprintf (fun msgs -> ()) fmt (* must eta-expand to get proper (non-weak) polymorphism for format *) let warn ?loc = msg Warning ?loc diff --git a/src/util/tracing.ml b/src/util/tracing.ml index ab56d9074b..0c884b45f8 100644 --- a/src/util/tracing.ml +++ b/src/util/tracing.ml @@ -31,56 +31,6 @@ let indent_level = ref 0 let traceIndent () = indent_level := !indent_level + 2 let traceOutdent () = indent_level := !indent_level - 2 -(* Parses a format string to generate a nop-function of the correct type. *) -let mygprintf (finish: 'b) (format : ('a, unit, doc, 'b) format4) : 'a = - let format = string_of_format format in - let flen = String.length format in - let fget = String.unsafe_get format in - let rec literal acc i = - let rec skipChars j = - if j >= flen || (match fget j with '%' | '@' | '\n' -> true | _ -> false) then - collect nil j - else - skipChars (succ j) - in - skipChars (succ i) - and collect (acc: doc) (i: int) = - if i >= flen then begin - Obj.magic finish - end else begin - let c = fget i in - if c = '%' then begin - let j = skip_args (succ i) in - match fget j with - '%' -> literal acc j - | ',' -> collect acc (succ j) - | 's' | 'c' | 'd' | 'i' | 'o' | 'x' | 'X' | 'u' - | 'f' | 'e' | 'E' | 'g' | 'G' | 'b' | 'B' -> - Obj.magic(fun b -> collect nil (succ j)) - | 'L' | 'l' | 'n' -> Obj.magic(fun n -> collect nil (succ (succ j))) - | 'a' -> Obj.magic(fun pprinter arg -> collect nil (succ j)) - | 't' -> Obj.magic(fun pprinter -> collect nil (succ j)) - | c -> invalid_arg ("dprintf: unknown format %s" ^ String.make 1 c) - end else if c = '@' then begin - if i + 1 < flen then begin - match fget (succ i) with - '[' | ']' | '!' | '?' | '^' | '@' -> collect nil (i + 2) - | '<' | '>' -> collect nil (i + 1) - | c -> invalid_arg ("dprintf: unknown format @" ^ String.make 1 c) - end else - invalid_arg "dprintf: incomplete format @" - end else if c = '\n' then begin - collect nil (i + 1) - end else - literal acc i - end - and skip_args j = - match String.unsafe_get format j with - '0' .. '9' | ' ' | '.' | '-' -> skip_args (succ j) - | c -> j - in - collect nil 0 - let traceTag (sys : string) : Pretty.doc = let rec ind (i : int) : string = if (i <= 0) then "" else " " ^ (ind (i-1)) in (text ((ind !indent_level) ^ "%%% " ^ sys ^ ": ")) @@ -104,7 +54,7 @@ let gtrace always f sys var ?loc do_subsys fmt = do_subsys (); gprintf (f sys) fmt end else - mygprintf () fmt + GobPretty.igprintf () fmt let trace sys ?var fmt = gtrace true printtrace sys var ignore fmt From 67441e0708cd26ccb0db6646af7013ff05ff2877 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 16:44:08 +0200 Subject: [PATCH 12/39] Add logging levels --- src/util/logs.ml | 51 +++++++++++++++++++++++++++++++++++++----------- 1 file changed, 40 insertions(+), 11 deletions(-) diff --git a/src/util/logs.ml b/src/util/logs.ml index cce0d8fa21..9d3da447a1 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -1,8 +1,27 @@ +module Level = +struct + type t = + | Debug + | Info + | Warning + | Error + [@@deriving eq, hash, show { with_path = false }, enum] + (* TODO: fix ord Error: https://github.com/ocaml-ppx/ppx_deriving/issues/254 *) + + let compare x y = Stdlib.compare (to_enum x) (to_enum y) + + let current = ref Warning + + let should_log l = + compare l !current >= 0 +end + + module type Kind = sig type b type c - val log: ('a, b, c, unit) format4 -> 'a + val log: Level.t -> ('a, b, c, unit) format4 -> 'a end module PrettyKind = @@ -11,35 +30,44 @@ struct type b = unit type c = Pretty.doc - let log fmt = + let log level fmt = (* Pretty.eprintf returns doc instead of unit *) let finish doc = Pretty.fprint stderr ~width:max_int doc; prerr_newline () in - Pretty.gprintf finish fmt + if Level.should_log level then + Pretty.gprintf finish fmt + else + GobPretty.igprintf () fmt end module FormatKind = struct type b = Format.formatter type c = unit - let log fmt = + let log level fmt = let finish ppf = Format.fprintf ppf "\n%!" in - Format.kfprintf finish Format.err_formatter fmt + if Level.should_log level then + Format.kfprintf finish Format.err_formatter fmt + else + Format.ifprintf Format.err_formatter fmt end module BatteriesKind = struct type b = unit BatIO.output type c = unit - let log fmt = + let log level fmt = let finish out = BatPrintf.fprintf out "\n%!" in - BatPrintf.kfprintf finish BatIO.stderr fmt + if Level.should_log level then + BatPrintf.kfprintf finish BatIO.stderr fmt + else + BatPrintf.ifprintf BatIO.stderr fmt end @@ -49,10 +77,11 @@ struct let log = log - let debug = log - let info = log - let warn = log - let error = log + (* must eta-expand to get proper (non-weak) polymorphism for format *) + let debug fmt = log Debug fmt + let info fmt = log Info fmt + let warn fmt = log Warning fmt + let error fmt = log Error fmt let newline () = prerr_newline () From 5cd82af9c6ec2e8d388c6580ce6f6ede24c43b92 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 17:02:05 +0200 Subject: [PATCH 13/39] Use Logs where semgrep missed --- src/analyses/basePriv.ml | 8 ++++---- src/analyses/mCP.ml | 2 +- src/analyses/raceAnalysis.ml | 2 +- src/analyses/termination.ml | 2 +- src/autoTune.ml | 6 +++--- src/cdomains/valueDomain.ml | 2 +- src/domains/mapDomain.ml | 2 +- src/framework/control.ml | 2 +- src/solvers/generic.ml | 10 +++++----- src/solvers/sLR.ml | 12 ++++++------ src/solvers/td3.ml | 4 ++-- src/spec/specUtil.ml | 2 +- src/transform/expressionEvaluation.ml | 10 +++++----- src/transform/transform.ml | 6 +++--- src/util/cilfacade.ml | 2 +- src/util/loopUnrolling.ml | 2 +- src/witness/violation.ml | 6 +++--- 17 files changed, 40 insertions(+), 40 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index bc20df011d..f0722d5739 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -226,7 +226,7 @@ struct CPA.find x st.cpa (* let read_global ask getg cpa x = let (cpa', v) as r = read_global ask getg cpa x in - ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" d_varinfo x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v); + Logs.debug "READ GLOBAL %a (%a, %B) = %a" d_varinfo x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v; r *) let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v = let cpa' = CPA.add x v st.cpa in @@ -236,7 +236,7 @@ struct {st with cpa = cpa'} (* let write_global ask getg sideg cpa x v = let cpa' = write_global ask getg sideg cpa x v in - ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" d_varinfo x VD.pretty v CPA.pretty cpa'); + Logs.debug "WRITE GLOBAL %a %a = %a" d_varinfo x VD.pretty v CPA.pretty cpa'; cpa' *) let lock ask getg (st: BaseComponents (D).t) m = @@ -331,7 +331,7 @@ struct {st with cpa = cpa'} (* let write_global ask getg sideg cpa x v = let cpa' = write_global ask getg sideg cpa x v in - ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" d_varinfo x VD.pretty v CPA.pretty cpa'); + Logs.debug "WRITE GLOBAL %a %a = %a" d_varinfo x VD.pretty v CPA.pretty cpa'; cpa' *) let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m = @@ -1638,7 +1638,7 @@ struct let dump () = let f = open_out_bin (get_string "exp.priv-prec-dump") in (* LVH.iter (fun (l, x) v -> - ignore (Pretty.printf "%a %a = %a\n" CilType.Location.pretty l d_varinfo x VD.pretty v) + Logs.debug "%a %a = %a" CilType.Location.pretty l d_varinfo x VD.pretty v ) lvh; *) Marshal.output f ({name = get_string "ana.base.privatization"; results = lvh}: result); close_out_noerr f diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index 7864737ab7..88ebc78b22 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -55,7 +55,7 @@ struct let y = find_id yn in if not (exists (fun (y',_) -> y=y') xs) then begin let xn = find_spec_name x in - Legacy.Printf.eprintf "Activated analysis '%s' depends on '%s' and '%s' is not activated.\n" xn yn yn; + Logs.error "Activated analysis '%s' depends on '%s' and '%s' is not activated.\n" xn yn yn; raise Exit end in diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index bfff9ce4e3..7d8d1c0d21 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -76,7 +76,7 @@ struct let g: V.t = Obj.obj g in begin match g with | `Left g' -> (* accesses *) - (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *) + (* Logs.debug "WarnGlobal %a" CilType.Varinfo.pretty g; *) let accs = G.access (ctx.global g) in let (lv, ty) = g' in let mem_loc_str = Pretty.sprint ~width:max_int (Access.d_memo () (ty, lv)) in diff --git a/src/analyses/termination.ml b/src/analyses/termination.ml index 4dc7ee74c7..c47c66e75b 100644 --- a/src/analyses/termination.ml +++ b/src/analyses/termination.ml @@ -139,7 +139,7 @@ class loopInstrVisitor (fd : fundec) = object(self) | _ -> ()); s | Loop (b, loc, eloc, Some continue, Some break) -> - print_endline @@ "WARN: Could not determine loop variable for loop at " ^ CilType.Location.show loc; + Logs.warn "WARN: Could not determine loop variable for loop at %a" CilType.Location.pretty loc; s | _ when Hashtbl.mem loopBreaks s.sid -> (* after a loop, we check that t is bounded/positive (no overflow happened) *) let loc = Hashtbl.find loopBreaks s.sid in diff --git a/src/autoTune.ml b/src/autoTune.ml index a8737c693b..f36d4783c8 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -110,10 +110,10 @@ class modFunctionAnnotatorVisitor = object let thisVisitor = new modVisitor in try ignore (visitCilFunction thisVisitor fd) with | ModFound -> - print_endline ("function " ^ (CilType.Fundec.show fd) ^" uses mod, enable congruence domain recursively for:"); - print_endline (" \"down\":"); + Logs.info "function %a uses mod, enable congruence domain recursively for:" CilType.Fundec.pretty fd; + Logs.info " \"down\":"; setCongruenceRecursive fd 6 calledFunctions; - print_endline (" \"up\":"); + Logs.info " \"up\":"; setCongruenceRecursive fd 3 callingFunctions; ; SkipChildren diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 1a4de9cd91..ea8b08402e 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -460,7 +460,7 @@ struct let warn_type op x y = if GobConfig.get_bool "dbg.verbose" then - ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name x) (tag_name y) CilType.Location.pretty !Tracing.current_loc pretty x pretty y + Logs.debug "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name x) (tag_name y) CilType.Location.pretty !Tracing.current_loc pretty x pretty y let rec leq x y = match (x,y) with diff --git a/src/domains/mapDomain.ml b/src/domains/mapDomain.ml index a2319df60e..942c782264 100644 --- a/src/domains/mapDomain.ml +++ b/src/domains/mapDomain.ml @@ -179,7 +179,7 @@ struct ) (* uncomment to easily check pretty's grouping during a normal run, e.g. ./regtest 01 01: *) - (* let add k v m = let _ = Pretty.printf "%a\n" pretty m in M.add k v m *) + (* let add k v m = let _ = Logs.debug "%a" pretty m in M.add k v m *) let arbitrary () = QCheck.always M.empty (* S TODO: non-empty map *) end diff --git a/src/framework/control.ml b/src/framework/control.ml index 8850957501..15ffbcd36a 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -656,7 +656,7 @@ struct CfgTools.dead_code_cfg (module FileCfg) liveness; let warn_global g v = - (* ignore (Pretty.printf "warn_global %a %a\n" EQSys.GVar.pretty_trace g EQSys.G.pretty v); *) + (* Logs.debug "warn_global %a %a" EQSys.GVar.pretty_trace g EQSys.G.pretty v; *) match g with | `Left g -> (* Spec global *) R.ask_global (WarnGlobal (Obj.repr g)) diff --git a/src/solvers/generic.ml b/src/solvers/generic.ml index b724c71dc9..29d2e9221d 100644 --- a/src/solvers/generic.ml +++ b/src/solvers/generic.ml @@ -73,7 +73,7 @@ struct let eval_rhs_event x = if full_trace then trace "sol" "(Re-)evaluating %a\n" Var.pretty_trace x; incr Goblintutil.evals; - if (get_bool "dbg.solver-progress") then (incr stack_d; print_int !stack_d; flush stdout) + if (get_bool "dbg.solver-progress") then (incr stack_d; Logs.debug "%d" !stack_d) let update_var_event x o n = if tracing then increase x; @@ -93,7 +93,7 @@ struct let is_fun k = match S.Var.node k with FunctionEntry _ -> true | _ -> false in (* only count function entries since other nodes in function will have leq number of contexts *) HM.iter (fun k _ -> if is_fun k then Hashtbl.modify_def 0 (str k) ((+)1) histo) rho; (* let max_k, n = Hashtbl.fold (fun k v (k',v') -> if v > v' then k,v else k',v') histo (Obj.magic (), 0) in *) - (* ignore @@ Pretty.printf "max #contexts: %d for %s\n" n max_k; *) + (* Logs.debug "max #contexts: %d for %s" n max_k; *) ncontexts := Hashtbl.fold (fun _ -> (+)) histo 0; let topn = 5 in Logs.debug "Found %d contexts for %d functions. Top %d functions:" !ncontexts (Hashtbl.length histo) topn; @@ -124,11 +124,11 @@ struct Logs.newline (); (* Timing.print (M.get_out "timing" Legacy.stdout) "Timings:\n"; *) (* Gc.print_stat stdout; (* too verbose, slow and words instead of MB *) *) - let gc = Goblintutil.print_gc_quick_stat Legacy.stdout in + let gc = Goblintutil.print_gc_quick_stat Legacy.stderr in Logs.newline (); - Option.may (write_csv [string_of_time (); string_of_int !Goblintutil.vars; string_of_int !Goblintutil.evals; string_of_int !ncontexts; string_of_int gc.Gc.top_heap_words]) stats_csv; + Option.may (write_csv [string_of_time (); string_of_int !Goblintutil.vars; string_of_int !Goblintutil.evals; string_of_int !ncontexts; string_of_int gc.Gc.top_heap_words]) stats_csv (* print_string "Do you want to continue? [Y/n]"; *) - flush stdout + (* flush stdout *) (* if read_line () = "n" then raise Break *) let () = diff --git a/src/solvers/sLR.ml b/src/solvers/sLR.ml index d3ee93751a..22b452e694 100644 --- a/src/solvers/sLR.ml +++ b/src/solvers/sLR.ml @@ -329,13 +329,13 @@ module Make0 = let _ = P.rem_item stable x in if k >= sk then () else let _ = X.set_value x (D.bot ()) in - (* ignore @@ Pretty.printf " also restarting %d: %a\n" k S.Var.pretty_trace x; *) + (* Logs.debug " also restarting %d: %a" k S.Var.pretty_trace x; *) (* flush_all (); *) let w = L.sub infl x in let _ = L.rem_item infl x in List.iter handle_one w in - (* ignore @@ Pretty.printf "restarting %d: %a\n" sk S.Var.pretty_trace x; *) + (* Logs.debug "restarting %d: %a" sk S.Var.pretty_trace x; *) (* flush_all (); *) let w = L.sub infl x in let _ = L.rem_item infl x in @@ -355,7 +355,7 @@ module Make0 = and side x y d = let yk, ynonfresh = X.get_index y in if X.get_key x > yk then begin - (* ignore @@ Pretty.printf "wrong order: %d > %d\n\n" (X.get_key x) yk; *) + (* Logs.warn "wrong order: %d > %d" (X.get_key x) yk; *) () end; @@ -368,9 +368,9 @@ module Make0 = in let old = XY.get_value (x,y) in - (* ignore @@ Pretty.printf "key: %a -> %a\nold: %a\n\nd: %a\n\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old S.Dom.pretty d; *) + (* Logs.debug "key: %a -> %a\nold: %a\n\nd: %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old S.Dom.pretty d; *) let tmp = d in - (* ignore @@ Pretty.printf "tmp: %a\n\n" S.Dom.pretty tmp; *) + (* Logs.debug "tmp: %a" S.Dom.pretty tmp; *) if not (D.eq tmp old) then begin let _ = XY.set_value (x,y) tmp in @@ -387,7 +387,7 @@ module Make0 = | None -> a | Some p -> let xs = P.to_list p in - (* ignore (Pretty.printf "%d var %a\n\n" (List.length list) S.Var.pretty_trace x); *) + (* Logs.debug "%d var %a" (List.length list) S.Var.pretty_trace x); *) List.fold_left (fun a z -> D.cup a (XY.get_value (z,x))) a xs and solve x = diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 90f3faa6bb..02c3302dc5 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -969,7 +969,7 @@ module Base = HM.iter (fun x w -> HM.iter (fun y d -> let old_d = try HM.find rho y with Not_found -> S.Dom.bot () in - (* ignore (Pretty.printf "rho_write retrigger %a %a %a %a\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old_d S.Dom.pretty d); *) + (* Logs.debug "rho_write retrigger %a %a %a %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old_d S.Dom.pretty d; *) HM.replace rho y (S.Dom.join old_d d); HM.replace init_reachable y (); HM.replace stable y (); (* make stable just in case, so following incremental load would have in superstable *) @@ -979,7 +979,7 @@ module Base = let one_side ~vh ~x ~y ~d = if S.Var.is_write_only y then ( - (* ignore (Pretty.printf "rho_write collect %a %a %a\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty d); *) + (* Logs.debug "rho_write collect %a %a %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty d; *) HM.replace stable y (); (* make stable just in case, so following incremental load would have in superstable *) let w = try diff --git a/src/spec/specUtil.ml b/src/spec/specUtil.ml index 0c0fc16fd7..4091c4820f 100644 --- a/src/spec/specUtil.ml +++ b/src/spec/specUtil.ml @@ -18,7 +18,7 @@ let parse ?repl:(repl=false) ?print:(print=false) ?dot:(dot=false) cin = let result = SpecParser.file SpecLexer.token lexbuf in defs := !defs@[result]; incr line; - if print then (Logs.debug "%s" (SpecCore.def_to_string result); flush stdout) + if print then Logs.debug "%s" (SpecCore.def_to_string result) with (* just an empty line -> don't print *) | SpecCore.Endl -> incr line diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml index f29a9cc68b..2f3839bb4a 100644 --- a/src/transform/expressionEvaluation.ml +++ b/src/transform/expressionEvaluation.ml @@ -81,7 +81,7 @@ struct match ~? (fun () -> Formatcil.cExp expression_string (local_variables @ global_variables)) with (* Expression unparseable at this location *) | None -> - if is_debug () then print_endline "| (Unparseable)"; + if is_debug () then Logs.debug "| (Unparseable)"; Some false (* Successfully parsed expression *) | Some expression -> @@ -89,7 +89,7 @@ struct match self#try_ask location expression with (* Dead code or not listed as part of the control flow *) | None -> - if is_debug () then print_endline "| (Unreachable)"; + if is_debug () then Logs.debug "| (Unreachable)"; Some false (* Valid location *) | Some value_before -> @@ -115,14 +115,14 @@ struct | None -> if is_debug () then begin - print_endline ("| /*" ^ (value_before |> string_of_evaluation_result) ^ "*/" ^ (statement |> string_of_statement)) + Logs.debug "%s" ("| /*" ^ (value_before |> string_of_evaluation_result) ^ "*/" ^ (statement |> string_of_statement)) end; value_before | Some value_after -> if is_debug () then begin - print_endline ("| " ^ (statement |> string_of_statement) ^ "/*" ^ (value_after |> string_of_evaluation_result) ^ "*/"); - print_endline ("| " ^ (~! !succeeding_statement |> string_of_statement)) + Logs.debug "%s" ("| " ^ (statement |> string_of_statement) ^ "/*" ^ (value_after |> string_of_evaluation_result) ^ "*/"); + Logs.debug "%s" ("| " ^ (~! !succeeding_statement |> string_of_statement)) end; value_after diff --git a/src/transform/transform.ml b/src/transform/transform.ml index 344388c3f3..dc2f1ac093 100644 --- a/src/transform/transform.ml +++ b/src/transform/transform.ml @@ -18,16 +18,16 @@ module PartialEval = struct inherit nopCilVisitor method! vstmt s = loc := Cilfacade.get_stmtLoc s; - (* ignore @@ Pretty.printf "Set loc at stmt %a to %a\n" d_stmt s CilType.Location.pretty !loc; *) + (* Logs.debug "Set loc at stmt %a to %a" d_stmt s CilType.Location.pretty !loc; *) DoChildren method! vexpr e = let eval e = match Queries.ID.to_int ((ask !loc).Queries.f (Queries.EvalInt e)) with | Some i -> let e' = integer @@ IntOps.BigIntOps.to_int i in - ignore @@ Pretty.printf "Replacing non-constant expression %a with %a at %a\n" d_exp e d_exp e' CilType.Location.pretty !loc; + Logs.debug "Replacing non-constant expression %a with %a at %a" d_exp e d_exp e' CilType.Location.pretty !loc; e' | None -> - ignore @@ Pretty.printf "Can't replace expression %a at %a\n" d_exp e CilType.Location.pretty !loc; e + Logs.error "Can't replace expression %a at %a" d_exp e CilType.Location.pretty !loc; e in match e with | Const _ -> SkipChildren diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index 3b2fc41544..ffbd1e91ed 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -79,7 +79,7 @@ class addConstructors cons = object val mutable cons1 = cons method! vfunc fd = if List.mem fd.svar.vname (get_string_list "mainfun") then begin - if get_bool "dbg.verbose" then ignore (Pretty.printf "Adding constructors to: %s\n" fd.svar.vname); + if get_bool "dbg.verbose" then Logs.debug "Adding constructors to: %s" fd.svar.vname; let loc = match fd.sbody.bstmts with | s :: _ -> get_stmtLoc s | [] -> locUnknown diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index c9fb573b3f..e81d455b53 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -273,7 +273,7 @@ let fixedLoopSize loopStatement func = constBefore var loopStatement func >>= fun start -> assignmentDifference loopStatement var >>= fun diff -> Logs.debug "comparison: "; - Pretty.fprint stdout (dn_exp () comparison) ~width:max_int; + Pretty.fprint stderr (dn_exp () comparison) ~width:max_int; Logs.debug ""; Logs.debug "variable: "; Logs.debug "%s" var.vname; diff --git a/src/witness/violation.ml b/src/witness/violation.ml index 9cb9b6c579..268b934f5c 100644 --- a/src/witness/violation.ml +++ b/src/witness/violation.ml @@ -68,9 +68,9 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod let rec trace_path next_nodes node2 = if NHT.mem next_nodes node2 then begin - (* ignore (Pretty.printf "PATH: %s\n" (Arg.Node.to_string node2)); *) + (* Logs.debug "PATH: %s" (Arg.Node.to_string node2); *) let (edge, next_node) = NHT.find next_nodes node2 in - (* ignore (Pretty.printf " %a\n" MyCFG.pretty_edge edge); *) + (* Logs.debug " %a" MyCFG.pretty_edge edge; *) (node2, edge, next_node) :: trace_path next_nodes next_node end else @@ -79,7 +79,7 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod let print_path path = List.iter (fun (n1, e, n2) -> - ignore (GoblintCil.Pretty.printf " %s =[%s]=> %s\n" (Arg.Node.to_string n1) (Arg.Edge.to_string e) (Arg.Node.to_string n2)) + Logs.info " %s =[%s]=> %s" (Arg.Node.to_string n1) (Arg.Edge.to_string e) (Arg.Node.to_string n2) ) path in From 61646c5621167a098ec91369abfd729c9146efc0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 17:46:09 +0200 Subject: [PATCH 14/39] Add colors to Logs --- src/util/ansiColors.ml | 10 ++++++++++ src/util/gobFormat.ml | 4 ++-- src/util/logs.ml | 26 ++++++++++++++++++++++---- src/util/messageUtil.ml | 17 +++++++---------- 4 files changed, 41 insertions(+), 16 deletions(-) create mode 100644 src/util/ansiColors.ml diff --git a/src/util/ansiColors.ml b/src/util/ansiColors.ml new file mode 100644 index 0000000000..5330c61ce5 --- /dev/null +++ b/src/util/ansiColors.ml @@ -0,0 +1,10 @@ +let table = + let open GobList.Syntax in + let colors = [("gray", "30"); ("red", "31"); ("green", "32"); ("yellow", "33"); ("blue", "34"); + ("violet", "35"); ("turquoise", "36"); ("white", "37"); ("reset", "0;00")] in + let modes = [(Fun.id, "0" (* normal *)); (String.uppercase_ascii, "1" (* bold *))] in + let+ (color, color_code) = colors + and+ (mode_fn, mode_code) = modes in + (mode_fn color, Format.sprintf "\027[%s;%sm" mode_code color_code) + +let stderr = ref true (* matches schema default *) diff --git a/src/util/gobFormat.ml b/src/util/gobFormat.ml index a489e92a88..698db9d4cb 100644 --- a/src/util/gobFormat.ml +++ b/src/util/gobFormat.ml @@ -3,13 +3,13 @@ let pp_set_ansi_color_tags ppf = let stag_functions = Format.pp_get_formatter_stag_functions ppf () in let mark_open_stag = function | Format.String_tag s -> - begin match List.assoc_opt s MessageUtil.ansi_color_table with + begin match List.assoc_opt s AnsiColors.table with | Some code -> code | None -> Format.sprintf "{%s}" s end | _ -> "" in - let reset_code = List.assoc "reset" MessageUtil.ansi_color_table in (* assoc only once *) + let reset_code = List.assoc "reset" AnsiColors.table in (* assoc only once *) let mark_close_stag = function | Format.String_tag _ -> reset_code | _ -> "" diff --git a/src/util/logs.ml b/src/util/logs.ml index 9d3da447a1..0f3638055b 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -14,6 +14,12 @@ struct let should_log l = compare l !current >= 0 + + let stag = function + | Error -> "red" + | Warning -> "yellow" + | Info -> "blue" + | Debug -> "white" (* non-bright white is actually some gray *) end @@ -34,10 +40,15 @@ struct (* Pretty.eprintf returns doc instead of unit *) let finish doc = Pretty.fprint stderr ~width:max_int doc; + if !AnsiColors.stderr then + prerr_string (List.assoc "reset" AnsiColors.table); prerr_newline () in - if Level.should_log level then + if Level.should_log level then ( + if !AnsiColors.stderr then + prerr_string (List.assoc (Level.stag level) AnsiColors.table); Pretty.gprintf finish fmt + ) else GobPretty.igprintf () fmt end @@ -48,10 +59,12 @@ struct type c = unit let log level fmt = let finish ppf = - Format.fprintf ppf "\n%!" + Format.fprintf ppf "@}\n%!" in - if Level.should_log level then + if Level.should_log level then ( + Format.eprintf "@{<%s>" (Level.stag level); Format.kfprintf finish Format.err_formatter fmt + ) else Format.ifprintf Format.err_formatter fmt end @@ -62,10 +75,15 @@ struct type c = unit let log level fmt = let finish out = + if !AnsiColors.stderr then + prerr_string (List.assoc "reset" AnsiColors.table); BatPrintf.fprintf out "\n%!" in - if Level.should_log level then + if Level.should_log level then ( + if !AnsiColors.stderr then + prerr_string (List.assoc (Level.stag level) AnsiColors.table); BatPrintf.kfprintf finish BatIO.stderr fmt + ) else BatPrintf.ifprintf BatIO.stderr fmt end diff --git a/src/util/messageUtil.ml b/src/util/messageUtil.ml index e1edc2d5be..b92cb8ea8d 100644 --- a/src/util/messageUtil.ml +++ b/src/util/messageUtil.ml @@ -1,22 +1,19 @@ open GobConfig -let ansi_color_table = - let open GobList.Syntax in - let colors = [("gray", "30"); ("red", "31"); ("green", "32"); ("yellow", "33"); ("blue", "34"); - ("violet", "35"); ("turquoise", "36"); ("white", "37"); ("reset", "0;00")] in - let modes = [(Fun.id, "0" (* normal *)); (String.uppercase_ascii, "1" (* bold *))] in - let+ (color, color_code) = colors - and+ (mode_fn, mode_code) = modes in - (mode_fn color, Format.sprintf "\027[%s;%sm" mode_code color_code) - let colors_on fd = (* use colors? *) let c = get_string "colors" in c = "always" || c = "auto" && Unix.(isatty fd) +let () = AfterConfig.register (fun () -> + AnsiColors.stderr := colors_on Unix.stderr; + if !AnsiColors.stderr then + GobFormat.pp_set_ansi_color_tags Format.err_formatter + ) + let colorize ~fd msg = let on = colors_on fd in let replace (color,code) = Str.global_replace (Str.regexp ("{"^color^"}")) (if on then code else "") in - let msg = List.fold_right replace ansi_color_table msg in + let msg = List.fold_right replace AnsiColors.table msg in msg^(if on then "\027[0;0;00m" else "") (* reset at end *) From 06972347815e6dde2a11391e40bc429c795c3f3b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 26 Jul 2023 13:45:56 +0300 Subject: [PATCH 15/39] Use Logs.info in longjmp autotune --- src/autoTune.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index f8d7448203..cec01a4e2f 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -206,7 +206,7 @@ let activateLongjmpAnalysesWhenRequired () = | _ -> false in if hasFunction isLongjmp then ( - print_endline @@ "longjmp -> enabling longjmp analyses \"" ^ (String.concat ", " longjmpAnalyses) ^ "\""; + Logs.info "longjmp -> enabling longjmp analyses \"%s\"" (String.concat ", " longjmpAnalyses); enableAnalyses longjmpAnalyses; ) From 23a14b057b21f419c26251c904b1f4b0ab93a5a4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 26 Jul 2023 13:49:24 +0300 Subject: [PATCH 16/39] Remove unused Printf opens --- src/framework/analyses.ml | 1 - src/goblint.ml | 1 - 2 files changed, 2 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 48ee1d9b7e..d7566b42a3 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -306,7 +306,6 @@ struct let f = BatIO.output_channel out in write_file f (get_string "outfile") | "sarif" -> - let open BatPrintf in Logs.info "Writing Sarif to file: %s" (get_string "outfile"); Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list)); | "json-messages" -> diff --git a/src/goblint.ml b/src/goblint.ml index 32f05241b7..02935c783e 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -1,7 +1,6 @@ open Goblint_lib open GobConfig open Maingoblint -open Printf (** the main function *) let main () = From d2377cdc99ff41c080741e8334c64194809ab826 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 26 Jul 2023 14:02:15 +0300 Subject: [PATCH 17/39] Fix d_varinfo mismerge --- src/analyses/basePriv.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 1ffa45198b..97db67acbd 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -230,7 +230,7 @@ struct CPA.find x st.cpa (* let read_global ask getg cpa x = let (cpa', v) as r = read_global ask getg cpa x in - Logs.debug "READ GLOBAL %a (%a, %B) = %a" d_varinfo x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v; + Logs.debug "READ GLOBAL %a (%a, %B) = %a" CilType.Varinfo.pretty x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v; r *) let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v = let cpa' = CPA.add x v st.cpa in @@ -240,7 +240,7 @@ struct {st with cpa = cpa'} (* let write_global ask getg sideg cpa x v = let cpa' = write_global ask getg sideg cpa x v in - Logs.debug "WRITE GLOBAL %a %a = %a" d_varinfo x VD.pretty v CPA.pretty cpa'; + Logs.debug "WRITE GLOBAL %a %a = %a" CilType.Varinfo.pretty x VD.pretty v CPA.pretty cpa'; cpa' *) let lock ask getg (st: BaseComponents (D).t) m = @@ -335,7 +335,7 @@ struct {st with cpa = cpa'} (* let write_global ask getg sideg cpa x v = let cpa' = write_global ask getg sideg cpa x v in - Logs.debug "WRITE GLOBAL %a %a = %a" d_varinfo x VD.pretty v CPA.pretty cpa'; + Logs.debug "WRITE GLOBAL %a %a = %a" CilType.Varinfo.pretty x VD.pretty v CPA.pretty cpa'; cpa' *) let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m = From b836978211c651a81a2cca3819c51b94da38361e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Aug 2023 12:28:51 +0300 Subject: [PATCH 18/39] Add dbg.level option --- src/maingoblint.ml | 1 + src/util/logs.ml | 9 ++++++++- src/util/options.schema.json | 7 +++++++ 3 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 6b76348152..7021745b5f 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -183,6 +183,7 @@ let handle_flags () = set_string "outfile" "" let handle_options () = + Logs.Level.current := Logs.Level.of_string (get_string "dbg.level"); check_arguments (); AfterConfig.run (); Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *) diff --git a/src/util/logs.ml b/src/util/logs.ml index 0f3638055b..2c303a07d3 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -10,7 +10,14 @@ struct let compare x y = Stdlib.compare (to_enum x) (to_enum y) - let current = ref Warning + let of_string = function + | "debug" -> Debug + | "info" -> Info + | "warning" -> Warning + | "error" -> Error + | _ -> invalid_arg "Logs.Level.of_string" + + let current = ref Debug let should_log l = compare l !current >= 0 diff --git a/src/util/options.schema.json b/src/util/options.schema.json index efa1dfabb8..9c3fb74b59 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1768,6 +1768,13 @@ "description": "Debugging options", "type": "object", "properties": { + "level": { + "title": "dbg.level", + "description": "Logging level.", + "type": "string", + "enum": ["debug", "info", "warning", "error"], + "default": "warning" + }, "verbose": { "title": "dbg.verbose", "description": "Prints some status information.", From 16344cc5e72f3f3c83471b25aee277b45bc1a2c4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Aug 2023 12:29:02 +0300 Subject: [PATCH 19/39] Remove Maingoblint.eprint_color --- src/maingoblint.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 7021745b5f..eae8309068 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -127,12 +127,12 @@ and complete args = |> List.iter print_endline; (* nosemgrep: print-not-logging *) raise Stdlib.Exit -(* TODO: remove *) -let eprint_color m = Logs.info "%s" (MessageUtil.colorize ~fd:Unix.stderr m) - let check_arguments () = - let fail m = (let m = "Option failure: " ^ m in eprint_color ("{red}"^m); failwith m) in - let warn m = eprint_color ("{yellow}Option warning: "^m) in + let fail m = + Logs.error "%s" m; + failwith "Option error" + in + let warn m = Logs.warn "%s" m in if get_bool "allfuns" && not (get_bool "exp.earlyglobs") then (set_bool "exp.earlyglobs" true; warn "allfuns enables exp.earlyglobs.\n"); if not @@ List.mem "escape" @@ get_string_list "ana.activated" then warn "Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!"; if List.mem "malloc_null" @@ get_string_list "ana.activated" && not @@ get_bool "sem.malloc.fail" then (set_bool "sem.malloc.fail" true; warn "The malloc_null analysis enables sem.malloc.fail."); @@ -626,7 +626,7 @@ let handle_extraspecials () = let diff_and_rename current_file = (* Create change info, either from old results, or from scratch if there are no previous results. *) let change_info: Analyses.increment_data option = - let warn m = eprint_color ("{yellow}Warning: "^m) in + let warn m = Logs.warn "%s" m in if GobConfig.get_bool "incremental.load" && not (Serialize.results_exist ()) then begin warn "incremental.load is activated but no data exists that can be loaded." end; From e673d9d3aecabc69ee9244bb7b21a2a69e19f90a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Aug 2023 12:38:29 +0300 Subject: [PATCH 20/39] Add log message level printing --- src/util/logs.ml | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/src/util/logs.ml b/src/util/logs.ml index 2c303a07d3..c9aa67b9c6 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -44,16 +44,17 @@ struct type b = unit type c = Pretty.doc let log level fmt = - (* Pretty.eprintf returns doc instead of unit *) - let finish doc = - Pretty.fprint stderr ~width:max_int doc; - if !AnsiColors.stderr then - prerr_string (List.assoc "reset" AnsiColors.table); - prerr_newline () - in if Level.should_log level then ( if !AnsiColors.stderr then prerr_string (List.assoc (Level.stag level) AnsiColors.table); + Printf.eprintf "[%s] " (Level.show level); + (* Pretty.eprintf returns doc instead of unit *) + let finish doc = + Pretty.fprint stderr ~width:max_int doc; + if !AnsiColors.stderr then + prerr_string (List.assoc "reset" AnsiColors.table); + prerr_newline () + in Pretty.gprintf finish fmt ) else @@ -65,11 +66,11 @@ struct type b = Format.formatter type c = unit let log level fmt = - let finish ppf = - Format.fprintf ppf "@}\n%!" - in if Level.should_log level then ( - Format.eprintf "@{<%s>" (Level.stag level); + Format.eprintf "@{<%s>[%a] " (Level.stag level) Level.pp level; + let finish ppf = + Format.fprintf ppf "@}\n%!" + in Format.kfprintf finish Format.err_formatter fmt ) else @@ -81,14 +82,15 @@ struct type b = unit BatIO.output type c = unit let log level fmt = - let finish out = - if !AnsiColors.stderr then - prerr_string (List.assoc "reset" AnsiColors.table); - BatPrintf.fprintf out "\n%!" - in if Level.should_log level then ( if !AnsiColors.stderr then prerr_string (List.assoc (Level.stag level) AnsiColors.table); + BatPrintf.eprintf "[%s] " (Level.show level); + let finish out = + if !AnsiColors.stderr then + prerr_string (List.assoc "reset" AnsiColors.table); + BatPrintf.fprintf out "\n%!" + in BatPrintf.kfprintf finish BatIO.stderr fmt ) else From ec1eeb5db9e25db7fbdc5bae73b283b66be8d485 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Aug 2023 12:48:58 +0300 Subject: [PATCH 21/39] Fix log output in cram tests --- src/util/options.schema.json | 2 +- tests/incremental/04-var-rename/01-rename_and_shuffle.t | 4 ++-- tests/incremental/04-var-rename/02-rename_with_usage.t | 4 ++-- tests/incremental/04-var-rename/04-renamed_param.t | 4 ++-- .../04-var-rename/05-renamed_param_usage_changed.t | 4 ++-- tests/incremental/05-method-rename/00-simple_rename.t | 4 ++-- tests/incremental/05-method-rename/01-dependent_rename.t | 4 ++-- .../05-method-rename/02-cyclic_rename_dependency.t | 4 ++-- tests/incremental/05-method-rename/03-cyclic_with_swap.t | 4 ++-- tests/incremental/05-method-rename/04-deep_change.t | 4 ++-- tests/incremental/05-method-rename/05-common_rename.t | 4 ++-- tests/incremental/05-method-rename/06-recursive_rename.t | 4 ++-- tests/incremental/06-glob-var-rename/00-simple_rename.t | 4 ++-- .../06-glob-var-rename/01-duplicate_local_global.t | 4 ++-- tests/incremental/06-glob-var-rename/02-add_new_gvar.t | 4 ++-- tests/regression/70-transform/01-ordering.t | 4 ++-- 16 files changed, 31 insertions(+), 31 deletions(-) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 9c3fb74b59..383e3e807a 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1773,7 +1773,7 @@ "description": "Logging level.", "type": "string", "enum": ["debug", "info", "warning", "error"], - "default": "warning" + "default": "info" }, "verbose": { "title": "dbg.verbose", diff --git a/tests/incremental/04-var-rename/01-rename_and_shuffle.t b/tests/incremental/04-var-rename/01-rename_and_shuffle.t index 8f3b57f797..657ba64836 100644 --- a/tests/incremental/04-var-rename/01-rename_and_shuffle.t +++ b/tests/incremental/04-var-rename/01-rename_and_shuffle.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 01-rename_and_shuffle.json --enable incremental.load 01-rename_and_shuffle.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 1 (with unchangedHeader = 1); added = 0; removed = 0 + $ goblint --conf 01-rename_and_shuffle.json --enable incremental.load 01-rename_and_shuffle.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 1 (with unchangedHeader = 1); added = 0; removed = 0 diff --git a/tests/incremental/04-var-rename/02-rename_with_usage.t b/tests/incremental/04-var-rename/02-rename_with_usage.t index 1e2818ed4d..d509d6f0ad 100644 --- a/tests/incremental/04-var-rename/02-rename_with_usage.t +++ b/tests/incremental/04-var-rename/02-rename_with_usage.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 02-rename_with_usage.json --enable incremental.load 02-rename_with_usage.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 + $ goblint --conf 02-rename_with_usage.json --enable incremental.load 02-rename_with_usage.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 diff --git a/tests/incremental/04-var-rename/04-renamed_param.t b/tests/incremental/04-var-rename/04-renamed_param.t index 9da6d5e888..f9ee692948 100644 --- a/tests/incremental/04-var-rename/04-renamed_param.t +++ b/tests/incremental/04-var-rename/04-renamed_param.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 04-renamed_param.json --enable incremental.load 04-renamed_param.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 + $ goblint --conf 04-renamed_param.json --enable incremental.load 04-renamed_param.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 diff --git a/tests/incremental/04-var-rename/05-renamed_param_usage_changed.t b/tests/incremental/04-var-rename/05-renamed_param_usage_changed.t index a465b2b6f2..ec3a4d43e9 100644 --- a/tests/incremental/04-var-rename/05-renamed_param_usage_changed.t +++ b/tests/incremental/04-var-rename/05-renamed_param_usage_changed.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 05-renamed_param_usage_changed.json --enable incremental.load 05-renamed_param_usage_changed.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 1 (with unchangedHeader = 1); added = 0; removed = 0 + $ goblint --conf 05-renamed_param_usage_changed.json --enable incremental.load 05-renamed_param_usage_changed.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 1 (with unchangedHeader = 1); added = 0; removed = 0 diff --git a/tests/incremental/05-method-rename/00-simple_rename.t b/tests/incremental/05-method-rename/00-simple_rename.t index 1855b903eb..8695911616 100644 --- a/tests/incremental/05-method-rename/00-simple_rename.t +++ b/tests/incremental/05-method-rename/00-simple_rename.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 00-simple_rename.json --enable incremental.load 00-simple_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 + $ goblint --conf 00-simple_rename.json --enable incremental.load 00-simple_rename.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 diff --git a/tests/incremental/05-method-rename/01-dependent_rename.t b/tests/incremental/05-method-rename/01-dependent_rename.t index bb0628447b..143a35982b 100644 --- a/tests/incremental/05-method-rename/01-dependent_rename.t +++ b/tests/incremental/05-method-rename/01-dependent_rename.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 01-dependent_rename.json --enable incremental.load 01-dependent_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 1 (with unchangedHeader = 1); added = 2; removed = 2 + $ goblint --conf 01-dependent_rename.json --enable incremental.load 01-dependent_rename.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 1 (with unchangedHeader = 1); added = 2; removed = 2 diff --git a/tests/incremental/05-method-rename/02-cyclic_rename_dependency.t b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.t index de9aa48e6c..37bb6383d9 100644 --- a/tests/incremental/05-method-rename/02-cyclic_rename_dependency.t +++ b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 02-cyclic_rename_dependency.json --enable incremental.load 02-cyclic_rename_dependency.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 1 (with unchangedHeader = 1); added = 2; removed = 2 + $ goblint --conf 02-cyclic_rename_dependency.json --enable incremental.load 02-cyclic_rename_dependency.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 1 (with unchangedHeader = 1); added = 2; removed = 2 diff --git a/tests/incremental/05-method-rename/03-cyclic_with_swap.t b/tests/incremental/05-method-rename/03-cyclic_with_swap.t index d2e8dd6d97..b9410a8aa9 100644 --- a/tests/incremental/05-method-rename/03-cyclic_with_swap.t +++ b/tests/incremental/05-method-rename/03-cyclic_with_swap.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 03-cyclic_with_swap.json --enable incremental.load 03-cyclic_with_swap.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 1 (with unchangedHeader = 1); added = 3; removed = 2 + $ goblint --conf 03-cyclic_with_swap.json --enable incremental.load 03-cyclic_with_swap.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 1 (with unchangedHeader = 1); added = 3; removed = 2 diff --git a/tests/incremental/05-method-rename/04-deep_change.t b/tests/incremental/05-method-rename/04-deep_change.t index 1adcb56276..67597ffbcc 100644 --- a/tests/incremental/05-method-rename/04-deep_change.t +++ b/tests/incremental/05-method-rename/04-deep_change.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 04-deep_change.json --enable incremental.load 04-deep_change.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 1 (with unchangedHeader = 1); added = 0; removed = 0 + $ goblint --conf 04-deep_change.json --enable incremental.load 04-deep_change.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 1 (with unchangedHeader = 1); added = 0; removed = 0 diff --git a/tests/incremental/05-method-rename/05-common_rename.t b/tests/incremental/05-method-rename/05-common_rename.t index 62e99c6c80..99264f84e9 100644 --- a/tests/incremental/05-method-rename/05-common_rename.t +++ b/tests/incremental/05-method-rename/05-common_rename.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 05-common_rename.json --enable incremental.load 05-common_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 + $ goblint --conf 05-common_rename.json --enable incremental.load 05-common_rename.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 diff --git a/tests/incremental/05-method-rename/06-recursive_rename.t b/tests/incremental/05-method-rename/06-recursive_rename.t index dce0894ff1..a7f9f2e693 100644 --- a/tests/incremental/05-method-rename/06-recursive_rename.t +++ b/tests/incremental/05-method-rename/06-recursive_rename.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 06-recursive_rename.json --enable incremental.load 06-recursive_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 + $ goblint --conf 06-recursive_rename.json --enable incremental.load 06-recursive_rename.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 diff --git a/tests/incremental/06-glob-var-rename/00-simple_rename.t b/tests/incremental/06-glob-var-rename/00-simple_rename.t index 1855b903eb..8695911616 100644 --- a/tests/incremental/06-glob-var-rename/00-simple_rename.t +++ b/tests/incremental/06-glob-var-rename/00-simple_rename.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 00-simple_rename.json --enable incremental.load 00-simple_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 + $ goblint --conf 00-simple_rename.json --enable incremental.load 00-simple_rename.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 diff --git a/tests/incremental/06-glob-var-rename/01-duplicate_local_global.t b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.t index cd2c5c0fea..d7880d803b 100644 --- a/tests/incremental/06-glob-var-rename/01-duplicate_local_global.t +++ b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 01-duplicate_local_global.json --enable incremental.load 01-duplicate_local_global.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 + $ goblint --conf 01-duplicate_local_global.json --enable incremental.load 01-duplicate_local_global.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 0 (with unchangedHeader = 0); added = 0; removed = 0 diff --git a/tests/incremental/06-glob-var-rename/02-add_new_gvar.t b/tests/incremental/06-glob-var-rename/02-add_new_gvar.t index c71cd6808f..cc65c9af88 100644 --- a/tests/incremental/06-glob-var-rename/02-add_new_gvar.t +++ b/tests/incremental/06-glob-var-rename/02-add_new_gvar.t @@ -10,5 +10,5 @@ Apply patch Run Goblint incrementally on new program version and check the change detection result - $ goblint --conf 02-add_new_gvar.json --enable incremental.load 02-add_new_gvar.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' - changed = 1 (with unchangedHeader = 1); added = 1; removed = 0 + $ goblint --conf 02-add_new_gvar.json --enable incremental.load 02-add_new_gvar.c 2>&1 | grep 'change_info' | sed -r 's/change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/' + [Info] changed = 1 (with unchangedHeader = 1); added = 1; removed = 0 diff --git a/tests/regression/70-transform/01-ordering.t b/tests/regression/70-transform/01-ordering.t index abf499c392..cd7ec8e36a 100644 --- a/tests/regression/70-transform/01-ordering.t +++ b/tests/regression/70-transform/01-ordering.t @@ -1,5 +1,5 @@ Check that assert transform is not allowed to happen after dead code removal $ ./transform.sh --stderr remove_dead_code assert -- 01-empty.c - Option failure: trans.activated: the 'assert' transform may not occur after the 'remove_dead_code' transform - Fatal error: exception Failure("Option failure: trans.activated: the 'assert' transform may not occur after the 'remove_dead_code' transform") + [Error] trans.activated: the 'assert' transform may not occur after the 'remove_dead_code' transform + Fatal error: exception Failure("Option error") [2] From ea809cfc06004867f08e7c296cb36e542d33ffe7 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Aug 2023 12:55:44 +0300 Subject: [PATCH 22/39] Revert --version to normal stdout printing This is needed to preserve compatibility with version checks, e.g. in BenchExec. --- src/maingoblint.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index eae8309068..c869782ea6 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -9,16 +9,16 @@ let writeconffile = ref None (** Print version and bail. *) let print_version ch = - Logs.info "Goblint version: %s" Version.goblint; - Logs.info "Cil version: %s" Cil.cilVersion; - Logs.info "Dune profile: %s" ConfigProfile.profile; - Logs.info "OCaml version: %s" Sys.ocaml_version; - Logs.info "OCaml flambda: %s" ConfigOcaml.flambda; + printf "Goblint version: %s\n" Version.goblint; (* nosemgrep: print-not-logging *) + printf "Cil version: %s\n" Cil.cilVersion; (* nosemgrep: print-not-logging *) + printf "Dune profile: %s\n" ConfigProfile.profile; (* nosemgrep: print-not-logging *) + printf "OCaml version: %s\n" Sys.ocaml_version; (* nosemgrep: print-not-logging *) + printf "OCaml flambda: %s\n" ConfigOcaml.flambda; (* nosemgrep: print-not-logging *) if get_bool "dbg.verbose" then ( - Logs.debug "Library versions:"; + printf "Library versions:\n"; (* nosemgrep: print-not-logging *) List.iter (fun (name, version) -> let version = Option.default "[unknown]" version in - Logs.debug " %s: %s" name version + printf " %s: %s\n" name version (* nosemgrep: print-not-logging *) ) Goblint_build_info.statically_linked_libraries ); exit 0 From d3283ea0d46648abd28f3eaa60749abf171a9415 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Aug 2023 13:37:44 +0300 Subject: [PATCH 23/39] Use Logs.debug instead of dbg.verbose conditional in most places --- src/cdomains/valueDomain.ml | 3 +-- src/framework/cfgTools.ml | 3 +-- src/framework/control.ml | 19 ++++++---------- src/goblint.ml | 6 ++--- src/incremental/makefileUtil.ml | 4 ++-- src/maingoblint.ml | 30 +++++++++++-------------- src/solvers/postSolver.ml | 9 +++----- src/solvers/td3.ml | 5 ++--- src/solvers/topDown_space_cache_term.ml | 5 ++--- src/util/cilfacade.ml | 4 ++-- src/util/compilationDatabase.ml | 6 ++--- src/util/preprocessor.ml | 3 +-- 12 files changed, 38 insertions(+), 59 deletions(-) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index de462c7e3f..4f95c5418c 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -501,8 +501,7 @@ struct let warn_type op x y = - if GobConfig.get_bool "dbg.verbose" then - Logs.debug "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Tracing.current_loc pretty x pretty y + Logs.debug "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Tracing.current_loc pretty x pretty y let rec leq x y = match (x,y) with diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index 454ac71387..532958cf9f 100644 --- a/src/framework/cfgTools.ml +++ b/src/framework/cfgTools.ml @@ -474,8 +474,7 @@ let createCFG (file: file) = | _ -> () ); if Messages.tracing then Messages.trace "cfg" "CFG building finished.\n\n"; - if get_bool "dbg.verbose" then - Logs.debug "cfgF (%a), cfgB (%a)" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB); + Logs.debug "cfgF (%a), cfgB (%a)" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB); cfgF, cfgB, skippedByEdge let createCFG = Timing.wrap "createCFG" createCFG diff --git a/src/framework/control.ml b/src/framework/control.ml index 751998542b..7e16f2783f 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -286,7 +286,7 @@ struct } in let edges = CfgTools.getGlobalInits file in - if (get_bool "dbg.verbose") then Logs.debug "Executing %d assigns." (List.length edges); + Logs.debug "Executing %d assigns." (List.length edges); let funs = ref [] in (*let count = ref 0 in*) let transfer_func (st : Spec.D.t) (loc, edge) : Spec.D.t = @@ -367,7 +367,7 @@ struct in let startstate, more_funs = - if (get_bool "dbg.verbose") then Logs.debug "Initializing %d globals." (CfgTools.numGlobals file); + Logs.debug "Initializing %d globals." (CfgTools.numGlobals file); Timing.wrap "global_inits" do_global_inits file in @@ -507,8 +507,7 @@ struct Some solver_data | None -> None in - if get_bool "dbg.verbose" then - Logs.info "%s" ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ "."); + Logs.debug "%s" ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ "."); AnalysisState.should_warn := get_string "warn_at" = "early" || gobview; let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global startvars') solver_data in if GobConfig.get_bool "incremental.save" then @@ -522,9 +521,7 @@ struct let cil = Fpath.(save_run / "cil.marshalled") in let warnings = Fpath.(save_run / "warnings.marshalled") in let stats = Fpath.(save_run / "stats.marshalled") in - if get_bool "dbg.verbose" then ( - Logs.Format.info "Saving the current configuration to %a, meta-data about this run to %a, and solver statistics to %a" Fpath.pp config Fpath.pp meta Fpath.pp solver_stats; - ); + Logs.Format.debug "Saving the current configuration to %a, meta-data about this run to %a, and solver statistics to %a" Fpath.pp config Fpath.pp meta Fpath.pp solver_stats; GobSys.mkdir_or_exists save_run; GobConfig.write_file config; let module Meta = struct @@ -535,9 +532,7 @@ struct (* Yojson.Safe.to_file meta Meta.json; *) Yojson.Safe.pretty_to_channel (Stdlib.open_out (Fpath.to_string meta)) Meta.json; (* the above is compact, this is pretty-printed *) if gobview then ( - if get_bool "dbg.verbose" then ( - Logs.Format.info "Saving the analysis table to %a, the CIL state to %a, the warning table to %a, and the runtime stats to %a" Fpath.pp analyses Fpath.pp cil Fpath.pp warnings Fpath.pp stats; - ); + Logs.Format.debug "Saving the analysis table to %a, the CIL state to %a, the warning table to %a, and the runtime stats to %a" Fpath.pp analyses Fpath.pp cil Fpath.pp warnings Fpath.pp stats; Serialize.marshal MCPRegistry.registered_name analyses; Serialize.marshal (file, Cabs2cil.environment) cil; Serialize.marshal !Messages.Table.messages_list warnings; @@ -766,7 +761,7 @@ struct if not (get_bool "server.enabled") then Serialize.Cache.store_data () ); - if get_bool "dbg.verbose" && get_string "result" <> "none" then Logs.info "Generating output: %s" (get_string "result"); + if get_string "result" <> "none" then Logs.debug "Generating output: %s" (get_string "result"); Messages.finalize (); Timing.wrap "result output" (Result.output (lazy local_xml) gh make_global_fast_xml) file @@ -798,7 +793,7 @@ let compute_cfg = fst % compute_cfg_skips (** The main function to perform the selected analyses. *) let analyze change_info (file: file) fs = - if (get_bool "dbg.verbose") then Logs.debug "Generating the control flow graph."; + Logs.debug "Generating the control flow graph."; let (module CFG), skippedByEdge = compute_cfg_skips file in MyCFG.current_cfg := (module CFG); analyze_loop (module CFG) file fs change_info skippedByEdge diff --git a/src/goblint.ml b/src/goblint.ml index 02935c783e..1266a1aeae 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -33,10 +33,8 @@ let main () = handle_extraspecials (); GoblintDir.init (); - if get_bool "dbg.verbose" then ( - Logs.debug "%s" (GobUnix.localtime ()); - Logs.debug "%s" GobSys.command_line; - ); + Logs.debug "%s" (GobUnix.localtime ()); + Logs.debug "%s" GobSys.command_line; let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in if get_bool "server.enabled" then ( let file = diff --git a/src/incremental/makefileUtil.ml b/src/incremental/makefileUtil.ml index 007dc711e4..9a17122f5e 100644 --- a/src/incremental/makefileUtil.ml +++ b/src/incremental/makefileUtil.ml @@ -15,7 +15,7 @@ let exec_command ?path (command: string) = if Sys.file_exists path_str && Sys.is_directory path_str then Sys.chdir path_str else failwith ("Directory " ^ path_str ^ " does not exist!") | None -> ()); - if GobConfig.get_bool "dbg.verbose" then Logs.debug "%s" ("executing command `" ^ command ^ "` in " ^ Sys.getcwd ()); + Logs.debug "%s" ("executing command `" ^ command ^ "` in " ^ Sys.getcwd ()); let (std_out, std_in) = open_process command in let output = Buffer.create buff_size in try @@ -51,7 +51,7 @@ let remove_comb_files path = try while true do let comb = Fpath.to_string (find_file_by_suffix path comb_suffix) in - if GobConfig.get_bool "dbg.verbose" then Logs.info "deleting %s" comb; + Logs.debug "deleting %s" comb; Sys.remove comb; done with Failure e -> () diff --git a/src/maingoblint.ml b/src/maingoblint.ml index c869782ea6..443bd0abb6 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -240,7 +240,7 @@ let basic_preprocess ?preprocess ~all_cppflags fname = let nname = Fpath.append (GoblintDir.preprocessed ()) (Fpath.add_ext ".i" unique_name) in let arguments = all_cppflags @ Fpath.to_string fname :: "-o" :: Fpath.to_string nname :: [] in let command = Filename.quote_command (Preprocessor.get_cpp ()) arguments in - if get_bool "dbg.verbose" then Logs.debug "%s" command; + Logs.debug "%s" command; (nname, Some {ProcessPool.command; cwd = None}) ) else @@ -277,12 +277,10 @@ let preprocess_files () = List.map (fun p -> Fpath.(p / "stub" / "src")) source_lib_dirs @ Goblint_sites.lib_stub_src in - if get_bool "dbg.verbose" then ( - Logs.debug "Custom include dirs:"; - List.iteri (fun i custom_include_dir -> - Logs.Format.debug " %d. %a (exists=%B)" (i + 1) Fpath.pp custom_include_dir (Sys.file_exists (Fpath.to_string custom_include_dir)) - ) custom_include_dirs - ); + Logs.debug "Custom include dirs:"; + List.iteri (fun i custom_include_dir -> + Logs.Format.debug " %d. %a (exists=%B)" (i + 1) Fpath.pp custom_include_dir (Sys.file_exists (Fpath.to_string custom_include_dir)) + ) custom_include_dirs; let custom_include_dirs = List.filter (Sys.file_exists % Fpath.to_string) custom_include_dirs in if custom_include_dirs = [] then Logs.warn "Warning, cannot find goblint's custom include files."; @@ -356,7 +354,7 @@ let preprocess_files () = let all_cppflags = !cppflags @ include_args in (* preprocess all the files *) - if get_bool "dbg.verbose" then Logs.info "Preprocessing files."; + Logs.debug "Preprocessing files."; let rec preprocess_arg_file ?preprocess = function | filename when not (Sys.file_exists (Fpath.to_string filename)) -> @@ -415,7 +413,7 @@ let preprocess_files () = (** Parse preprocessed files *) let parse_preprocessed preprocessed = (* get the AST *) - if get_bool "dbg.verbose" then Logs.info "Parsing files."; + Logs.debug "Parsing files."; let goblint_cwd = GobFpath.cwd () in let get_ast_and_record_deps (preprocessed_file, task_opt) = @@ -518,20 +516,18 @@ let do_analyze change_info merged_AST = Cilfacade.print merged_AST else ( (* we first find the functions to analyze: *) - if get_bool "dbg.verbose" then Logs.info "And now... the Goblin!"; + Logs.debug "And now... the Goblin!"; let (stf,exf,otf as funs) = Cilfacade.getFuns merged_AST in if stf@exf@otf = [] then raise (FrontendError "no suitable function to start from"); - if get_bool "dbg.verbose" then Logs.debug "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a" + Logs.debug "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a" L.pretty stf L.pretty exf L.pretty otf; (* and here we run the analysis! *) let control_analyze ast funs = - if get_bool "dbg.verbose" then ( - let aa = String.concat ", " @@ get_string_list "ana.activated" in - let at = String.concat ", " @@ get_string_list "trans.activated" in - Logs.info "Activated analyses: %s" aa; - Logs.info "Activated transformations: %s" at - ); + let aa = String.concat ", " @@ get_string_list "ana.activated" in + let at = String.concat ", " @@ get_string_list "trans.activated" in + Logs.debug "Activated analyses: %s" aa; + Logs.debug "Activated transformations: %s" at; try Control.analyze change_info ast funs with e -> let backtrace = Printexc.get_raw_backtrace () in (* capture backtrace immediately, otherwise the following loses it (internal exception usage without raise_notrace?) *) diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml index 030127b89d..0bd251f336 100644 --- a/src/solvers/postSolver.ml +++ b/src/solvers/postSolver.ml @@ -63,8 +63,7 @@ module Prune: F = include Unit (S) (VH) let finalize ~vh ~reachable = - if get_bool "dbg.verbose" then - Logs.debug "Pruning result"; + Logs.debug "Pruning result"; VH.filteri_inplace (fun x _ -> VH.mem reachable x @@ -130,8 +129,7 @@ module SaveRun: F = let save_run_str = let o = get_string "save_run" in if o = "" then (if gobview then "run" else "") else o in let save_run = Fpath.v save_run_str in let solver = Fpath.(save_run / solver_file) in - if get_bool "dbg.verbose" then - Logs.Format.info "Saving the solver result to %a" Fpath.pp solver; + Logs.Format.debug "Saving the solver result to %a" Fpath.pp solver; GobSys.mkdir_or_exists save_run; Serialize.marshal vh solver end @@ -180,8 +178,7 @@ struct module VH = PS.VH let post xs vs vh = - if get_bool "dbg.verbose" then - Logs.debug "Postsolving"; + Logs.debug "Postsolving"; let module StartS = struct diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 6117cf5bee..743b36c126 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -831,8 +831,7 @@ module Base = in (* restore values for non-widening-points *) if space && GobConfig.get_bool "solvers.td3.space_restore" then ( - if GobConfig.get_bool "dbg.verbose" then - Logs.debug "Restoring missing values."; + Logs.debug "Restoring missing values."; let restore () = let get x = let d = get ~check:true x in @@ -842,7 +841,7 @@ module Base = HM.filteri_inplace (fun x _ -> HM.mem visited x) rho in Timing.wrap "restore" restore (); - if GobConfig.get_bool "dbg.verbose" then Logs.debug "Solved %d vars. Total of %d vars after restore." !SolverStats.vars (HM.length rho); + Logs.debug "Solved %d vars. Total of %d vars after restore." !SolverStats.vars (HM.length rho); let avg xs = if List.is_empty !cache_sizes then 0.0 else float_of_int (BatList.sum xs) /. float_of_int (List.length xs) in if tracing && cache then trace "cache" "#caches: %d, max: %d, avg: %.2f\n" (List.length !cache_sizes) (List.max !cache_sizes) (avg !cache_sizes); ); diff --git a/src/solvers/topDown_space_cache_term.ml b/src/solvers/topDown_space_cache_term.ml index 32f89bb92c..13a2032c7a 100644 --- a/src/solvers/topDown_space_cache_term.ml +++ b/src/solvers/topDown_space_cache_term.ml @@ -172,8 +172,7 @@ module WP = in (* restore values for non-widening-points *) if GobConfig.get_bool "solvers.wp.restore" then ( - if (GobConfig.get_bool "dbg.verbose") then - Logs.debug ("Restoring missing values."); + Logs.debug "Restoring missing values."; let restore () = let get x = let d = get x in @@ -182,7 +181,7 @@ module WP = List.iter get vs in Timing.wrap "restore" restore (); - if (GobConfig.get_bool "dbg.verbose") then Logs.debug "Solved %d vars. Total of %d vars after restore." !SolverStats.vars (HM.length rho); + Logs.debug "Solved %d vars. Total of %d vars after restore." !SolverStats.vars (HM.length rho); ); let avg xs = float_of_int (BatList.sum xs) /. float_of_int (List.length xs) in if tracing then trace "cache" "#caches: %d, max: %d, avg: %.2f\n" (List.length !cache_sizes) (List.max !cache_sizes) (avg !cache_sizes); diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index 45df200f7b..06ea05d8e6 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -99,7 +99,7 @@ class addConstructors cons = object val mutable cons1 = cons method! vfunc fd = if List.mem fd.svar.vname (get_string_list "mainfun") then begin - if get_bool "dbg.verbose" then Logs.debug "Adding constructors to: %s" fd.svar.vname; + Logs.debug "Adding constructors to: %s" fd.svar.vname; let loc = match fd.sbody.bstmts with | s :: _ -> get_stmtLoc s | [] -> locUnknown @@ -139,7 +139,7 @@ let callConstructors ast = !cons in let d_fundec () fd = Pretty.text fd.svar.vname in - if get_bool "dbg.verbose" then ignore (Logs.debug "Constructors: %a" (Pretty.d_list ", " d_fundec) constructors); + Logs.debug "Constructors: %a" (Pretty.d_list ", " d_fundec) constructors; visitCilFileSameGlobals (new addConstructors constructors) ast; ast diff --git a/src/util/compilationDatabase.ml b/src/util/compilationDatabase.ml index 192b058b5a..e088cb5e76 100644 --- a/src/util/compilationDatabase.ml +++ b/src/util/compilationDatabase.ml @@ -70,8 +70,7 @@ let load_and_preprocess ~all_cppflags filename = let original_database_dir = Fpath.parent original_path in let old_root = GobFpath.rem_find_prefix database_dir original_database_dir in let new_root = GobFpath.rem_find_prefix original_database_dir database_dir in - if GobConfig.get_bool "dbg.verbose" then - Logs.Format.debug "Rerooting compilation database\n from %a\n to %a" Fpath.pp old_root Fpath.pp new_root; + Logs.Format.debug "Rerooting compilation database\n from %a\n to %a" Fpath.pp old_root Fpath.pp new_root; let reroot_path p = Fpath.append new_root (Option.get (Fpath.relativize ~root:old_root p)) in @@ -128,8 +127,7 @@ let load_and_preprocess ~all_cppflags filename = failwith ("CompilationDatabase.preprocess: neither command nor arguments specified for " ^ Fpath.to_string file) in let cwd = reroot_path obj.directory in - if GobConfig.get_bool "dbg.verbose" then - Logs.Format.debug "Preprocessing %a\n to %a\n using %s\n in %a" Fpath.pp file Fpath.pp preprocessed_file preprocess_command Fpath.pp cwd; + Logs.Format.debug "Preprocessing %a\n to %a\n using %s\n in %a" Fpath.pp file Fpath.pp preprocessed_file preprocess_command Fpath.pp cwd; let preprocess_task = {ProcessPool.command = preprocess_command; cwd = Some cwd} in (* command/arguments might have paths relative to directory *) Some (preprocessed_file, Some preprocess_task) in diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index 15cb4be54b..cbd12b8f24 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -11,8 +11,7 @@ let is_bad name = | exception Not_found -> false | _ -> true in - if GobConfig.get_bool "dbg.verbose" then - Logs.debug "Preprocessor %s: is_bad=%B" name r; + Logs.debug "Preprocessor %s: is_bad=%B" name r; r let compgen prefix = From 4c463c7a771d1d157e576a56c76547c0cf5f6bf9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Aug 2023 17:25:51 +0300 Subject: [PATCH 24/39] Remove dbg.verbose option --- conf/incremental.json | 2 +- conf/minimal_incremental.json | 2 +- src/incremental/serialize.ml | 2 +- src/maingoblint.ml | 6 ++-- src/solvers/generic.ml | 2 +- src/solvers/td3.ml | 28 +++++++++---------- src/transform/expressionEvaluation.ml | 28 +++++++------------ src/util/options.schema.json | 6 ---- .../regression/68-longjmp/42-poison-reduced.c | 2 +- tests/regression/68-longjmp/47-more-reduced.c | 2 +- 10 files changed, 33 insertions(+), 47 deletions(-) diff --git a/conf/incremental.json b/conf/incremental.json index a9c5fcd152..6c8f7c3c2b 100644 --- a/conf/incremental.json +++ b/conf/incremental.json @@ -24,7 +24,7 @@ "earlyglobs": true }, "dbg": { - "verbose": true, + "level": "debug", "trace": { "context": true }, diff --git a/conf/minimal_incremental.json b/conf/minimal_incremental.json index 4eb9f8289a..c6ae08b1ce 100644 --- a/conf/minimal_incremental.json +++ b/conf/minimal_incremental.json @@ -23,7 +23,7 @@ "earlyglobs": true }, "dbg": { - "verbose": true, + "level": "debug", "trace": { "context": true }, diff --git a/src/incremental/serialize.ml b/src/incremental/serialize.ml index bddf3aa383..2b1b04bc3f 100644 --- a/src/incremental/serialize.ml +++ b/src/incremental/serialize.ml @@ -27,7 +27,7 @@ let marshal obj fileName = close_out chan let unmarshal fileName = - if GobConfig.get_bool "dbg.verbose" then + if Logs.Level.should_log Debug then (* Do NOT replace with Printf because of GobView: https://github.com/goblint/gobview/issues/10 *) print_endline ("Unmarshalling " ^ Fpath.to_string fileName ^ "... If type of content changed, this will result in a segmentation fault!"); Marshal.input (open_in_bin (Fpath.to_string fileName)) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 443bd0abb6..1dc2890fb8 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -14,7 +14,7 @@ let print_version ch = printf "Dune profile: %s\n" ConfigProfile.profile; (* nosemgrep: print-not-logging *) printf "OCaml version: %s\n" Sys.ocaml_version; (* nosemgrep: print-not-logging *) printf "OCaml flambda: %s\n" ConfigOcaml.flambda; (* nosemgrep: print-not-logging *) - if get_bool "dbg.verbose" then ( + if Logs.Level.should_log Debug then ( printf "Library versions:\n"; (* nosemgrep: print-not-logging *) List.iter (fun (name, version) -> let version = Option.default "[unknown]" version in @@ -98,7 +98,7 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy ( complete_option_value !last_complete_option s in [ "-o" , Arg_complete.String (set_string "outfile", Arg_complete.empty), "" - ; "-v" , Arg_complete.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "dbg.timing.enabled" true), "" + ; "-v" , Arg_complete.Unit (fun () -> set_string "dbg.level" "debug"; set_bool "dbg.timing.enabled" true), "" ; "-j" , Arg_complete.Int (set_int "jobs", Arg_complete.empty), "" ; "-I" , Arg_complete.String (set_string "pre.includes[+]", Arg_complete.empty), "" ; "-IK" , Arg_complete.String (set_string "pre.kernel_includes[+]", Arg_complete.empty), "" @@ -164,7 +164,7 @@ let check_arguments () = (** Initialize some globals in other modules. *) let handle_flags () = - if get_bool "dbg.verbose" then ( + if Logs.Level.should_log Debug then ( Printexc.record_backtrace true; Errormsg.debugFlag := true; Errormsg.verboseFlag := true diff --git a/src/solvers/generic.ml b/src/solvers/generic.ml index ef5bd85016..ec5e60c88e 100644 --- a/src/solvers/generic.ml +++ b/src/solvers/generic.ml @@ -12,7 +12,7 @@ module LoadRunSolver: GenericEqSolver = let solver_file = "solver.marshalled" in let load_run = Fpath.v (get_string "load_run") in let solver = Fpath.(load_run / solver_file) in - if get_bool "dbg.verbose" then + if Logs.Level.should_log Debug then (* Do NOT replace with Printf because of GobView: https://github.com/goblint/gobview/issues/10 *) print_endline ("Loading the solver result of a saved run from " ^ (Fpath.to_string solver)); let vh: S.d VH.t = Serialize.unmarshal solver in diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 743b36c126..cddeb6c3d4 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -81,21 +81,21 @@ module Base = } let print_data data = - Logs.info "|rho|=%d" (HM.length data.rho); - Logs.info "|stable|=%d" (HM.length data.stable); - Logs.info "|infl|=%d" (HM.length data.infl); - Logs.info "|wpoint|=%d" (HM.length data.wpoint); - Logs.info "|sides|=%d" (HM.length data.sides); - Logs.info "|side_dep|=%d" (HM.length data.side_dep); - Logs.info "|side_infl|=%d" (HM.length data.side_infl); - Logs.info "|var_messages|=%d" (HM.length data.var_messages); - Logs.info "|rho_write|=%d" (HM.length data.rho_write); - Logs.info "|dep|=%d" (HM.length data.dep); + Logs.debug "|rho|=%d" (HM.length data.rho); + Logs.debug "|stable|=%d" (HM.length data.stable); + Logs.debug "|infl|=%d" (HM.length data.infl); + Logs.debug "|wpoint|=%d" (HM.length data.wpoint); + Logs.debug "|sides|=%d" (HM.length data.sides); + Logs.debug "|side_dep|=%d" (HM.length data.side_dep); + Logs.debug "|side_infl|=%d" (HM.length data.side_infl); + Logs.debug "|var_messages|=%d" (HM.length data.var_messages); + Logs.debug "|rho_write|=%d" (HM.length data.rho_write); + Logs.debug "|dep|=%d" (HM.length data.dep); Hooks.print_data () let print_data_verbose data str = - if GobConfig.get_bool "dbg.verbose" then ( - Logs.info "%s:" str; + if Logs.Level.should_log Debug then ( + Logs.debug "%s:" str; print_data data ) @@ -781,7 +781,7 @@ module Base = incr i; let unstable_vs = List.filter (neg (HM.mem stable)) vs in if unstable_vs <> [] then ( - if GobConfig.get_bool "dbg.verbose" then ( + if Logs.Level.should_log Debug then ( if !i = 1 then Logs.newline (); Logs.debug "Unstable solver start vars in %d. phase:" !i; List.iter (fun v -> Logs.debug "\t%a" S.Var.pretty_trace v) unstable_vs; @@ -1095,7 +1095,7 @@ module DepVals: GenericEqIncrSolver = module HM = HM let print_data () = - Logs.info "|dep_vals|=%d" (HM.length !current_dep_vals) + Logs.debug "|dep_vals|=%d" (HM.length !current_dep_vals) let system x = match S.system x with diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml index f2e8ea0a28..9c7fd478b4 100644 --- a/src/transform/expressionEvaluation.ml +++ b/src/transform/expressionEvaluation.ml @@ -37,9 +37,6 @@ struct | Some value -> value | None -> raise Stdlib.Exit - let is_debug () = - GobConfig.get_bool "dbg.verbose" - let string_of_evaluation_result evaluation_result = match evaluation_result with | Some value -> if value then "TRUE" else "FALSE" @@ -84,7 +81,7 @@ struct match ~? (fun () -> Formatcil.cExp expression_string (local_variables @ global_variables)) with (* Expression unparseable at this location *) | None -> - if is_debug () then Logs.debug "| (Unparseable)"; + Logs.debug "| (Unparseable)"; Some false (* Successfully parsed expression *) | Some expression -> @@ -92,7 +89,7 @@ struct match self#try_ask location expression with (* Dead code or not listed as part of the control flow *) | None -> - if is_debug () then Logs.debug "| (Unreachable)"; + Logs.debug "| (Unreachable)"; Some false (* Valid location *) | Some value_before -> @@ -116,17 +113,11 @@ struct (* Prefer successor evaluation *) match successor_evaluation with | None -> - if is_debug () then - begin - Logs.debug "%s" ("| /*" ^ (value_before |> string_of_evaluation_result) ^ "*/" ^ (statement |> string_of_statement)) - end; + Logs.debug "%s" ("| /*" ^ (value_before |> string_of_evaluation_result) ^ "*/" ^ (statement |> string_of_statement)); value_before | Some value_after -> - if is_debug () then - begin - Logs.debug "%s" ("| " ^ (statement |> string_of_statement) ^ "/*" ^ (value_after |> string_of_evaluation_result) ^ "*/"); - Logs.debug "%s" ("| " ^ (~! !succeeding_statement |> string_of_statement)) - end; + Logs.debug "%s" ("| " ^ (statement |> string_of_statement) ^ "/*" ^ (value_after |> string_of_evaluation_result) ^ "*/"); + Logs.debug "%s" ("| " ^ (~! !succeeding_statement |> string_of_statement)); value_after method private try_ask location expression = @@ -155,8 +146,7 @@ struct | Error message -> Error ("ExpEval: Unable to parse JSON query file: \"" ^ name ^ "\" (" ^ message ^ ")") | Ok query -> - if is_debug () then - Logs.debug "Successfully parsed JSON query file: \"%s\"" name; + Logs.debug "Successfully parsed JSON query file: \"%s\"" name; Ok query let string_of_location (location : Cil.location) = @@ -199,11 +189,13 @@ struct | Some value -> if value then Logs.info "%s" (loc |> string_of_location) - else if is_debug () then + else Logs.debug "%s x" (loc |> string_of_location) | None -> - if query.mode = `May || is_debug () then + if query.mode = `May then Logs.info "%s ?" (loc |> string_of_location) + else + Logs.debug "%s ?" (loc |> string_of_location) in gv_results := results; List.iter print results diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 383e3e807a..b63069e79f 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1775,12 +1775,6 @@ "enum": ["debug", "info", "warning", "error"], "default": "info" }, - "verbose": { - "title": "dbg.verbose", - "description": "Prints some status information.", - "type": "boolean", - "default": false - }, "timing": { "title": "dbg.timing", "type": "object", diff --git a/tests/regression/68-longjmp/42-poison-reduced.c b/tests/regression/68-longjmp/42-poison-reduced.c index a3ef050b35..b0e9bdfed1 100644 --- a/tests/regression/68-longjmp/42-poison-reduced.c +++ b/tests/regression/68-longjmp/42-poison-reduced.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --enable dbg.verbose --disable exp.volatiles_are_top --enable ana.int.interval +// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --disable exp.volatiles_are_top --enable ana.int.interval #include jmp_buf env_buffer; struct c { diff --git a/tests/regression/68-longjmp/47-more-reduced.c b/tests/regression/68-longjmp/47-more-reduced.c index ff85a229e5..be0e4a34cf 100644 --- a/tests/regression/68-longjmp/47-more-reduced.c +++ b/tests/regression/68-longjmp/47-more-reduced.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --enable dbg.verbose --disable exp.volatiles_are_top --enable ana.int.interval +// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --disable exp.volatiles_are_top --enable ana.int.interval #include jmp_buf env_buffer; From bb7d5048bcf1de4aee9e368cea39e6159d0fae79 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Aug 2023 17:26:59 +0300 Subject: [PATCH 25/39] Fix dbg.verbose in gobview --- gobview | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobview b/gobview index c3dcfaba97..4530c543e5 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit c3dcfaba97a1df72f027e5dad317e2c201ce5e4b +Subproject commit 4530c543e5f6722abd3a9b480b1a4bffe22889ea From bf4cb3149dbd504aa2d574dcb26373903b19dbd9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Aug 2023 17:51:24 +0300 Subject: [PATCH 26/39] Document logging --- docs/developer-guide/debugging.md | 29 +++++++++++++++++------------ docs/developer-guide/messaging.md | 3 ++- src/util/logs.ml | 2 ++ src/util/messages.ml | 2 +- 4 files changed, 22 insertions(+), 14 deletions(-) diff --git a/docs/developer-guide/debugging.md b/docs/developer-guide/debugging.md index 7875a9b01e..5278a756ba 100644 --- a/docs/developer-guide/debugging.md +++ b/docs/developer-guide/debugging.md @@ -1,39 +1,44 @@ # Debugging -## Printing -Goblint extensively uses [CIL's `Pretty`](https://people.eecs.berkeley.edu/~necula/cil/api/Pretty.html) module for printing due to many non-primitive values. +## Logging +Instead of debug printing directly to `stdout`, all logging should be done using the `Logs` module. +This allows for consistent pretty terminal output, as well as avoiding interference with server mode. +There are four logging levels: error, warning, info and debug. +Log output is controlled by the `dbg.level` option, which defaults to "info". -* Printing CIL values (e.g. an expression `exp`) using the corresponding pretty-printer `d_exp` from `Cil` module: +Goblint extensively uses [CIL's `Pretty`](https://people.eecs.berkeley.edu/~necula/cil/api/Pretty.html) module for output due to many non-primitive values. + +* Logging CIL values (e.g. an expression `exp`) using the corresponding pretty-printer `d_exp` from `Cil` module: ```ocaml -ignore (Pretty.printf "A CIL exp: %a\n" d_exp exp); +Logs.debug "A CIL exp: %a\n" d_exp exp; ``` -* Printing Goblint's `Printable` values (e.g. a domain `D` element `d`) using the corresponding pretty-printer `D.pretty`: +* Logging Goblint's `Printable` values (e.g. a domain `D` element `d`) using the corresponding pretty-printer `D.pretty`: ```ocaml -ignore (Pretty.printf "A domain element: %a\n" D.pretty d); +Logs.debug "A domain element: %a\n" D.pretty d; ``` -* Printing primitives (e.g. OCaml ints, strings, etc) using the standard [OCaml `Printf`](https://ocaml.org/api/Printf.html) specifiers: +* Logging primitives (e.g. OCaml ints, strings, etc) using the standard [OCaml `Printf`](https://ocaml.org/api/Printf.html) specifiers: ```ocaml -ignore (Pretty.printf "An int and a string: %d %s\n" 42 "magic"); +Logs.debug "An int and a string: %d %s\n" 42 "magic"; ``` -* Printing lists of pretty-printables (e.g. expressions list `exps`) using `d_list`: +* Logging lists of pretty-printables (e.g. expressions list `exps`) using `d_list`: ```ocaml -ignore (Pretty.printf "Some expressions: %a\n" (d_list ", " d_exp) exps); +Logs.debug "Some expressions: %a\n" (d_list ", " d_exp) exps; ``` ## Tracing -Tracing is a nicer alternative to debug printing, because it can be disabled for best performance and it can be used to only see relevant tracing output. +Tracing is a nicer alternative to some logging, because it can be disabled for best performance and it can be used to only see relevant tracing output. Recompile with tracing enabled: `./scripts/trace_on.sh`. -Instead of debug printing use a tracing function from the `Messages` module, which is often aliased to just `M` (and pick a relevant name instead of `mything`): +Instead of logging use a tracing function from the `Messages` module, which is often aliased to just `M` (and pick a relevant name instead of `mything`): ```ocaml if M.tracing then M.trace "mything" "A domain element: %a\n" D.pretty d; ``` diff --git a/docs/developer-guide/messaging.md b/docs/developer-guide/messaging.md index 28f24bc49c..a8ada2c261 100644 --- a/docs/developer-guide/messaging.md +++ b/docs/developer-guide/messaging.md @@ -1,7 +1,8 @@ # Messaging -The message system in `Messages` module should be used for outputting all (non-[tracing](./debugging.md#tracing)) information instead of printing them directly to `stdout`. +The message system in `Messages` module should be used for outputting all analysis results of the program to the user, instead of printing them directly to `stdout`. This allows for consistent pretty terminal output, as well as export to Goblint result viewers and IDEs. +For other kinds of (debug) output, see [Debugging](./debugging.md). ## Message structure diff --git a/src/util/logs.ml b/src/util/logs.ml index c9aa67b9c6..ccca18ca19 100644 --- a/src/util/logs.ml +++ b/src/util/logs.ml @@ -1,3 +1,5 @@ +(** Logging, which isn't for presenting analysis results. *) + module Level = struct type t = diff --git a/src/util/messages.ml b/src/util/messages.ml index a06a183eee..7718a1c3ca 100644 --- a/src/util/messages.ml +++ b/src/util/messages.ml @@ -1,4 +1,4 @@ -(** Messages (e.g. warnings) from the analysis. *) +(** Messages (e.g. warnings) presented to the user about the program from the analysis. *) module Pretty = GoblintCil.Pretty From a354ce37065122f9fce4dc951df2cd8be9a69c55 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 10 Jan 2024 16:31:51 +0200 Subject: [PATCH 27/39] Replace merged direct printing with Logs --- src/autoTune.ml | 14 +++++++------- src/util/loopUnrolling.ml | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 75b3589635..637a61c2f1 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -216,23 +216,23 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) = match spec with | ValidFree -> (* Enable the useAfterFree analysis *) let uafAna = ["useAfterFree"] in - print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\""; + Logs.info "Specification: ValidFree -> enabling useAfterFree analysis \"%s\"" (String.concat ", " uafAna); enableAnalyses uafAna | ValidDeref -> (* Enable the memOutOfBounds analysis *) let memOobAna = ["memOutOfBounds"] in set_bool "ana.arrayoob" true; - print_endline "Setting \"cil.addNestedScopeAttr\" to true"; + Logs.info "Setting \"cil.addNestedScopeAttr\" to true"; set_bool "cil.addNestedScopeAttr" true; - print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\""; + Logs.info "Specification: ValidDeref -> enabling memOutOfBounds analysis \"%s\"" (String.concat ", " memOobAna); enableAnalyses memOobAna; | ValidMemtrack | ValidMemcleanup -> (* Enable the memLeak analysis *) let memLeakAna = ["memLeak"] in if (get_int "ana.malloc.unique_address_count") < 1 then ( - print_endline "Setting \"ana.malloc.unique_address_count\" to 5"; + Logs.info "Setting \"ana.malloc.unique_address_count\" to 5"; set_int "ana.malloc.unique_address_count" 5; ); - print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\""; + Logs.info "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"%s\"" (String.concat ", " memLeakAna); enableAnalyses memLeakAna | _ -> () @@ -243,7 +243,7 @@ let focusOnTermination (spec: Svcomp.Specification.t) = match spec with | Termination -> let terminationAnas = ["termination"; "threadflag"; "apron"] in - print_endline @@ "Specification: Termination -> enabling termination analyses \"" ^ (String.concat ", " terminationAnas) ^ "\""; + Logs.info "Specification: Termination -> enabling termination analyses \"%s\"" (String.concat ", " terminationAnas); enableAnalyses terminationAnas; set_string "sem.int.signed_overflow" "assume_none"; set_bool "ana.int.interval" true; @@ -482,7 +482,7 @@ let activateTmpSpecialAnalysis () = in let hasMathFunctions = hasFunction isMathFun in if hasMathFunctions then ( - print_endline @@ "math function -> enabling tmpSpecial analysis and floating-point domain"; + Logs.info "math function -> enabling tmpSpecial analysis and floating-point domain"; enableAnalyses ["tmpSpecial"]; set_bool "ana.float.interval" true; ) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index bf5358142b..56163475c2 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -449,7 +449,7 @@ class loopUnrollingVisitor(func, totalLoops) = object let duplicate_and_rem_labels s = let factor = loop_unrolling_factor s func totalLoops in if(factor > 0) then ( - print_endline @@ "unrolling loop at " ^ CilType.Location.show loc ^" with factor " ^ string_of_int factor; + Logs.info "unrolling loop at %a with factor %d" CilType.Location.pretty loc factor; annotateArrays b; match s.skind with | Loop (b,loc, loc2, break , continue) -> From bbc360fc145c71ed32f679aca55bf32560047524 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 10 Jan 2024 17:44:21 +0200 Subject: [PATCH 28/39] Add Result log level to stdout --- src/util/logs/logs.ml | 58 ++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 55 insertions(+), 3 deletions(-) diff --git a/src/util/logs/logs.ml b/src/util/logs/logs.ml index ccca18ca19..496a4182fe 100644 --- a/src/util/logs/logs.ml +++ b/src/util/logs/logs.ml @@ -7,6 +7,7 @@ struct | Info | Warning | Error + | Result [@@deriving eq, hash, show { with_path = false }, enum] (* TODO: fix ord Error: https://github.com/ocaml-ppx/ppx_deriving/issues/254 *) @@ -17,6 +18,7 @@ struct | "info" -> Info | "warning" -> Warning | "error" -> Error + | "result" -> Result | _ -> invalid_arg "Logs.Level.of_string" let current = ref Debug @@ -29,6 +31,12 @@ struct | Warning -> "yellow" | Info -> "blue" | Debug -> "white" (* non-bright white is actually some gray *) + | Result -> "reset" +end + +module Result = +struct + let use_stdout = ref true (* TODO: disable in server mode *) end @@ -116,8 +124,52 @@ struct prerr_newline () end -module Pretty = MakeKind (PrettyKind) -module Format = MakeKind (FormatKind) -module Batteries = MakeKind (BatteriesKind) +module Pretty = +struct + include MakeKind (PrettyKind) + + open GoblintCil + + let result fmt = + if !Result.use_stdout then ( + let finish doc = + Pretty.fprint stdout ~width:max_int doc; + print_newline () + in + Pretty.gprintf finish fmt + ) + else + log Result fmt +end + +module Format = +struct + include MakeKind (FormatKind) + + let result fmt = + if !Result.use_stdout then ( + let finish ppf = + Format.fprintf ppf "\n%!" + in + Format.kfprintf finish Format.std_formatter fmt + ) + else + log Result fmt +end + +module Batteries = +struct + include MakeKind (BatteriesKind) + + let result fmt = + if !Result.use_stdout then ( + let finish out = + BatPrintf.fprintf out "\n%!" + in + BatPrintf.kfprintf finish BatIO.stdout fmt + ) + else + log Result fmt +end include Pretty (* current default *) From 68d1d1a4e13234eadd23c66ad23184a2ee88b299 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 10 Jan 2024 17:49:14 +0200 Subject: [PATCH 29/39] Use Logs.result --- src/analyses/extractPthread.ml | 2 +- src/framework/analysisResult.ml | 2 +- src/maingoblint.ml | 14 +++++++------- src/util/precCompare.ml | 4 ++-- src/witness/witness.ml | 2 +- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml index 8bd3ab416b..6cc347d511 100644 --- a/src/analyses/extractPthread.ml +++ b/src/analyses/extractPthread.ml @@ -850,7 +850,7 @@ module Codegen = struct Writer.write "promela model" "pml" promela ; Writer.write "graph" "dot" dot_graph ; - Logs.info + Logs.result "Copy spin/pthread_base.pml to same folder and then do: spin -a \ pthread.pml && cc -o pan pan.c && ./pan -a" end diff --git a/src/framework/analysisResult.ml b/src/framework/analysisResult.ml index 34536b9cab..1907346924 100644 --- a/src/framework/analysisResult.ml +++ b/src/framework/analysisResult.ml @@ -166,7 +166,7 @@ struct let f = BatIO.output_channel out in write_file f (get_string "outfile") | "sarif" -> - Logs.info "Writing Sarif to file: %s" (get_string "outfile"); + Logs.result "Writing Sarif to file: %s" (get_string "outfile"); Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list)); | "json-messages" -> let json = `Assoc [ diff --git a/src/maingoblint.ml b/src/maingoblint.ml index c661a3b66e..2af5091382 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -9,16 +9,16 @@ let writeconffile = ref None (** Print version and bail. *) let print_version ch = - printf "Goblint version: %s\n" Goblint_build_info.version; (* nosemgrep: print-not-logging *) - printf "Cil version: %s\n" Cil.cilVersion; (* nosemgrep: print-not-logging *) - printf "Dune profile: %s\n" Goblint_build_info.dune_profile; (* nosemgrep: print-not-logging *) - printf "OCaml version: %s\n" Sys.ocaml_version; (* nosemgrep: print-not-logging *) - printf "OCaml flambda: %s\n" Goblint_build_info.ocaml_flambda; (* nosemgrep: print-not-logging *) + Logs.result "Goblint version: %s" Goblint_build_info.version; + Logs.result "Cil version: %s" Cil.cilVersion; + Logs.result "Dune profile: %s" Goblint_build_info.dune_profile; + Logs.result "OCaml version: %s" Sys.ocaml_version; + Logs.result "OCaml flambda: %s" Goblint_build_info.ocaml_flambda; if Logs.Level.should_log Debug then ( - printf "Library versions:\n"; (* nosemgrep: print-not-logging *) + Logs.result "Library versions:"; List.iter (fun (name, version) -> let version = Option.default "[unknown]" version in - printf " %s: %s\n" name version (* nosemgrep: print-not-logging *) + Logs.result " %s: %s" name version ) Goblint_build_info.statically_linked_libraries ); exit 0 diff --git a/src/util/precCompare.ml b/src/util/precCompare.ml index 826901be35..a04e395e83 100644 --- a/src/util/precCompare.ml +++ b/src/util/precCompare.ml @@ -129,7 +129,7 @@ struct |> List.filter (fun ((i1, _), (i2, _)) -> i1 <> i2) |> List.map (Tuple2.map snd snd) |> List.map (uncurry compare_dumps) - |> List.iter (fun (_, msg) -> Logs.info "%t" (fun () -> msg)); + |> List.iter (fun (_, msg) -> Logs.result "%t" (fun () -> msg)); Logs.newline (); - Logs.info "Total locations: %d\nTotal %s: %d" locations_count (Key.name ()) location_vars_count + Logs.result "Total locations: %d\nTotal %s: %d" locations_count (Key.name ()) location_vars_count end diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 85a1343b2e..48948fd354 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -272,7 +272,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) let print_svcomp_result (s: string): unit = - Logs.info "SV-COMP result: %s" s + Logs.result "SV-COMP result: %s" s let print_task_result (module TaskResult:TaskResult): unit = print_svcomp_result (Result.to_string TaskResult.result) From 31ad591d40dd528b98d78a6cf9df5bffcdfcff10 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 10 Jan 2024 17:51:05 +0200 Subject: [PATCH 30/39] Optimize ValueDomain.warn_type --- src/cdomain/value/cdomains/valueDomain.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 3b5914b992..ac831fdb8e 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -253,8 +253,11 @@ struct | TNamed ({ttype=t; _}, _) -> zero_init_value ~varAttr t | _ -> Top - let tag_name : t -> string = function + let show_tag : t -> string = function | Top -> "Top" | Int _ -> "Int" | Float _ -> "Float" | Address _ -> "Address" | Struct _ -> "Struct" | Union _ -> "Union" | Array _ -> "Array" | Blob _ -> "Blob" | Thread _ -> "Thread" | Mutex -> "Mutex" | MutexAttr _ -> "MutexAttr" | JmpBuf _ -> "JmpBuf" | Bot -> "Bot" + + let pretty_tag () x = Pretty.text (show_tag x) + include Printable.Std let name () = "compound" @@ -521,7 +524,7 @@ struct let warn_type op x y = - Logs.debug "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Goblint_tracing.current_loc pretty x pretty y + Logs.debug "warn_type %s: incomparable abstr. values %a and %a at %a: %a and %a" op pretty_tag x pretty_tag y CilType.Location.pretty !Goblint_tracing.current_loc pretty x pretty y let rec leq x y = match (x,y) with From 0ca32e0cd9960a529e750d5046f6475c5dbcdd71 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 10 Jan 2024 17:55:38 +0200 Subject: [PATCH 31/39] Use messages for dbg.print_tids --- src/analyses/threadId.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index 61e2d72639..70ae13661e 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -175,13 +175,9 @@ struct let non_uniques = List.filter_map (fun (a,b) -> if not (Thread.is_unique a) then Some a else None) tids in let uc = List.length uniques in let nc = List.length non_uniques in - Logs.debug "Encountered number of thread IDs (unique): %i (%i)" (uc+nc) uc; - Logs.debug "unique: "; - List.iter (fun tid -> Logs.debug " %s " (Thread.show tid)) uniques; - Logs.newline (); - Logs.debug "non-unique: "; - List.iter (fun tid -> Logs.debug " %s " (Thread.show tid)) non_uniques; - Logs.newline () + M.debug_noloc ~category:Analyzer "Encountered number of thread IDs (unique): %i (%i)" (uc+nc) uc; + M.msg_group Debug ~category:Analyzer "Unique TIDs" (List.map (fun tid -> (Thread.pretty () tid, None)) uniques); + M.msg_group Debug ~category:Analyzer "Non-unique TIDs" (List.map (fun tid -> (Thread.pretty () tid, None)) non_uniques) let finalize () = if GobConfig.get_bool "dbg.print_tids" then print_tid_info (); From 6f89b91be213d7f2a27a3cfc2e26640cedf8b075 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 11:14:18 +0200 Subject: [PATCH 32/39] Update cram test with SV-COMP specification --- tests/regression/29-svcomp/32-no-ov.t | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/29-svcomp/32-no-ov.t b/tests/regression/29-svcomp/32-no-ov.t index 1dc22ed89e..c58099b5e4 100644 --- a/tests/regression/29-svcomp/32-no-ov.t +++ b/tests/regression/29-svcomp/32-no-ov.t @@ -1,5 +1,5 @@ $ goblint --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )" 32-no-ov.c - SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) ) + [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) ) [Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (32-no-ov.c:5:6-5:159) [Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (32-no-ov.c:5:6-5:159) [Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (32-no-ov.c:5:6-5:159) From 355c52120ddd8dae7bf825eaaa7d324e25afd807 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 12:02:39 +0200 Subject: [PATCH 33/39] Update log levels in debugging docs --- docs/developer-guide/debugging.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/developer-guide/debugging.md b/docs/developer-guide/debugging.md index bc6e1e8c0a..680e15fe3d 100644 --- a/docs/developer-guide/debugging.md +++ b/docs/developer-guide/debugging.md @@ -3,9 +3,11 @@ ## Logging Instead of debug printing directly to `stdout`, all logging should be done using the `Logs` module. This allows for consistent pretty terminal output, as well as avoiding interference with server mode. -There are four logging levels: error, warning, info and debug. +There are five logging levels: result, error, warning, info and debug. Log output is controlled by the `dbg.level` option, which defaults to "info". +Logs are written to `stderr`, except for result level, which go to `stdout` by default. + Goblint extensively uses [CIL's `Pretty`](https://people.eecs.berkeley.edu/~necula/cil/api/Pretty.html) module for output due to many non-primitive values. * Logging CIL values (e.g. an expression `exp`) using the corresponding pretty-printer `d_exp` from `Cil` module: From c9834e87f74533da12e8b3dc594df71003ad02b4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 12:12:29 +0200 Subject: [PATCH 34/39] Add warning about dbg.print_wpoints --- src/maingoblint.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 2af5091382..6fc6ed8b71 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -168,7 +168,9 @@ let check_arguments () = set_string "sem.int.signed_overflow" "assume_none"; warn "termination analysis implicitly activates threadflag analysis and set sem.int.signed_overflow to assume_none"; ); - if not (get_bool "ana.sv-comp.enabled") && get_bool "witness.graphml.enabled" then fail "witness.graphml.enabled: cannot generate GraphML witness without SV-COMP mode (ana.sv-comp.enabled)" + if not (get_bool "ana.sv-comp.enabled") && get_bool "witness.graphml.enabled" then fail "witness.graphml.enabled: cannot generate GraphML witness without SV-COMP mode (ana.sv-comp.enabled)"; + if get_bool "dbg.print_wpoints" && not (Logs.Level.should_log Debug) then + warn "dbg.print_wpoints requires dbg.level debug" (** Initialize some globals in other modules. *) let handle_flags () = From 32db3a3c9bc6b3a02360821b969916ecb52229ff Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 12:12:53 +0200 Subject: [PATCH 35/39] Add result log level to options --- src/config/options.schema.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index a22809f7bf..df4b1365db 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1813,7 +1813,7 @@ "title": "dbg.level", "description": "Logging level.", "type": "string", - "enum": ["debug", "info", "warning", "error"], + "enum": ["debug", "info", "warning", "error", "result"], "default": "info" }, "timing": { From 9135222e802c29e3f04a53726358552fe40ca165 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 12:39:05 +0200 Subject: [PATCH 36/39] Remove print_endline for GobView Normal logging works just fine. --- src/incremental/serialize.ml | 4 +--- src/solver/generic.ml | 4 +--- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/incremental/serialize.ml b/src/incremental/serialize.ml index 2b1b04bc3f..e988f643e7 100644 --- a/src/incremental/serialize.ml +++ b/src/incremental/serialize.ml @@ -27,9 +27,7 @@ let marshal obj fileName = close_out chan let unmarshal fileName = - if Logs.Level.should_log Debug then - (* Do NOT replace with Printf because of GobView: https://github.com/goblint/gobview/issues/10 *) - print_endline ("Unmarshalling " ^ Fpath.to_string fileName ^ "... If type of content changed, this will result in a segmentation fault!"); + Logs.debug "Unmarshalling %s... If type of content changed, this will result in a segmentation fault!" (Fpath.to_string fileName); Marshal.input (open_in_bin (Fpath.to_string fileName)) let results_exist () = diff --git a/src/solver/generic.ml b/src/solver/generic.ml index 604fb5bd43..8a38bc4771 100644 --- a/src/solver/generic.ml +++ b/src/solver/generic.ml @@ -12,9 +12,7 @@ module LoadRunSolver: GenericEqSolver = let solver_file = "solver.marshalled" in let load_run = Fpath.v (get_string "load_run") in let solver = Fpath.(load_run / solver_file) in - if Logs.Level.should_log Debug then - (* Do NOT replace with Printf because of GobView: https://github.com/goblint/gobview/issues/10 *) - print_endline ("Loading the solver result of a saved run from " ^ (Fpath.to_string solver)); + Logs.debug "Loading the solver result of a saved run from %s" (Fpath.to_string solver); let vh: S.d VH.t = Serialize.unmarshal solver in if get_bool "ana.opt.hashcons" then ( let vh' = VH.create (VH.length vh) in From 05d9cce733566db7ff158caf558ea9f3dbe55e33 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 12:47:14 +0200 Subject: [PATCH 37/39] Do not use stdout for logs if server.mode is stdio --- src/util/server.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/util/server.ml b/src/util/server.ml index 829ee92ee8..31e1036652 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -172,8 +172,11 @@ let make ?(input=stdin) ?(output=stdout) file : t = } let bind () = - let mode = GobConfig.get_string "server.mode" in - if mode = "stdio" then None, None else ( + match GobConfig.get_string "server.mode" with + | "stdio" -> + Logs.Result.use_stdout := false; + (None, None) + | "unix" -> let path = GobConfig.get_string "server.unix-socket" in if Sys.file_exists path then Sys.remove path; @@ -183,7 +186,8 @@ let bind () = let conn, _ = Unix.accept socket in Unix.close socket; Sys.remove path; - Some (Unix.input_of_descr conn), Some (Unix.output_of_descr conn)) + (Some (Unix.input_of_descr conn), Some (Unix.output_of_descr conn)) + | _ -> assert false let start file = let input, output = bind () in From b8b98f302e965515cf1204c4c88db28c795cd0fe Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 7 Feb 2024 10:06:59 +0200 Subject: [PATCH 38/39] Add warning about dbg.print_tids --- src/maingoblint.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 6fc6ed8b71..40a997edee 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -170,7 +170,9 @@ let check_arguments () = ); if not (get_bool "ana.sv-comp.enabled") && get_bool "witness.graphml.enabled" then fail "witness.graphml.enabled: cannot generate GraphML witness without SV-COMP mode (ana.sv-comp.enabled)"; if get_bool "dbg.print_wpoints" && not (Logs.Level.should_log Debug) then - warn "dbg.print_wpoints requires dbg.level debug" + warn "dbg.print_wpoints requires dbg.level debug"; + if get_bool "dbg.print_tids" && not (Logs.Level.should_log Debug) then + warn "dbg.print_tids requires dbg.level debug" (** Initialize some globals in other modules. *) let handle_flags () = From 520c742793059990b49e10f975fadb445e9d5768 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 7 Feb 2024 10:10:03 +0200 Subject: [PATCH 39/39] Replace WTF error in Goblint_tracing --- src/util/tracing/goblint_tracing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/tracing/goblint_tracing.ml b/src/util/tracing/goblint_tracing.ml index 5cbaf62ef7..7881306217 100644 --- a/src/util/tracing/goblint_tracing.ml +++ b/src/util/tracing/goblint_tracing.ml @@ -28,7 +28,7 @@ let activate (sys:string) (subsys: string list): unit = activated := Strs.union !activated subs; Hashtbl.add active_dep sys subs let deactivate (sys:string): unit = - activated := Strs.diff !activated (try Hashtbl.find active_dep sys with Not_found -> Goblint_logs.Logs.error "WTF? %s" sys; Strs.empty) + activated := Strs.diff !activated (try Hashtbl.find active_dep sys with Not_found -> Goblint_logs.Logs.error "Missing tracing active_dep for %s" sys; Strs.empty) let indent_level = ref 0 let traceIndent () = indent_level := !indent_level + 2