diff --git a/.semgrep/logs.yml b/.semgrep/logs.yml new file mode 100644 index 0000000000..dad32adadf --- /dev/null +++ b/.semgrep/logs.yml @@ -0,0 +1,38 @@ +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_string + paths: + exclude: + - logs.ml + - bench/ + 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/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/docs/developer-guide/debugging.md b/docs/developer-guide/debugging.md index d218e1a8b8..680e15fe3d 100644 --- a/docs/developer-guide/debugging.md +++ b/docs/developer-guide/debugging.md @@ -1,39 +1,46 @@ # 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 five logging levels: result, 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: +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: ```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 91fba82b51..f988545202 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/gobview b/gobview index f873913017..649451b76d 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit f873913017d3846ca686df4079d8d171b1d3a201 +Subproject commit 649451b76de7294b736ff863d1c1479bf5be2270 diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index ea570b338a..c7b62e8d16 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -761,7 +761,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!"; Timing.wrap "relation.prec-dump" store_data (Fpath.v file) end; Priv.finalize () diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 479ffc2d93..043168ba57 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 - ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Goblint_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 !Goblint_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 - ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" CilType.Varinfo.pretty 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 - ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" CilType.Varinfo.pretty 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 = @@ -1657,7 +1657,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 CilType.Varinfo.pretty x VD.pretty v) + Logs.debug "%a %a = %a" CilType.Location.pretty l CilType.Varinfo.pretty 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/extractPthread.ml b/src/analyses/extractPthread.ml index 8412a65683..6cc347d511 100644 --- a/src/analyses/extractPthread.ml +++ b/src/analyses/extractPthread.ml @@ -576,7 +576,7 @@ module Codegen = struct let dir = GobSys.mkdir_or_exists_absolute (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" @@ -612,7 +612,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.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/analyses/mCP.ml b/src/analyses/mCP.ml index 50f6d5409b..a3943651c0 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -58,7 +58,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 Stdlib.Exit end in diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 7dae319d6f..2f6611d467 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -269,7 +269,7 @@ struct let g: V.t = Obj.obj g in begin match g with | `Left g' -> (* accesses *) - (* ignore (Pretty.printf "WarnGlobal %a\n" Access.MemoRoot.pretty g'); *) + (* Logs.debug "WarnGlobal %a" Access.MemoRoot.pretty g'; *) let trie = G.access (ctx.global g) in (** Distribute access to contained fields. *) let rec distribute_inner offset (accs, children) ~prefix ~type_suffix_prefix = diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index 86e7f770a8..70ae13661e 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -175,12 +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 - 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" + 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 (); diff --git a/src/autoTune.ml b/src/autoTune.ml index 3cda36a302..637a61c2f1 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -85,7 +85,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 *) @@ -98,7 +98,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; match Cilfacade.find_varinfo_fundec vinfo with | fd -> setCongruenceRecursive fd (depth -1) neigbourFunction | exception Not_found -> () (* Happens for __goblint_bounded *) @@ -127,10 +127,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 @@ -146,7 +146,7 @@ let disableIntervalContextsInRecursiveFunctions () = (ResettableLazy.force functionCallMaps).calling |> 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 and interval_set contexts"); + Logs.info "function %s is recursive, disable interval and interval_set contexts" f.vname; f.vattr <- addAttributes (f.vattr) [Attr ("goblint_context",[AStr "base.no-interval"; AStr "base.no-interval_set"; AStr "relation.no-context"])]; ) ) @@ -194,7 +194,7 @@ let reduceThreadAnalyses () = in let hasThreadCreate = hasFunction isThreadCreate in if not @@ hasThreadCreate then ( - print_endline @@ "no thread creation -> disabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; + Logs.info "no thread creation -> disabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses); disableAnalyses notNeccessaryThreadAnalyses; ) @@ -208,7 +208,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; ) @@ -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; @@ -258,7 +258,7 @@ let focusOnSpecification (spec: Svcomp.Specification.t) = match spec with | UnreachCall s -> () | NoDataRace -> (*enable all thread analyses*) - print_endline @@ "Specification: NoDataRace -> enabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; + Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses); enableAnalyses notNeccessaryThreadAnalyses; | NoOverflow -> (*We focus on integer analysis*) set_bool "ana.int.def_exc" true; @@ -411,9 +411,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; @@ -445,14 +445,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 { @@ -469,10 +469,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"; } let activateTmpSpecialAnalysis () = @@ -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; ) @@ -503,13 +503,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 @@ -527,11 +527,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..8f87256854 100644 --- a/src/autoTune0.ml +++ b/src/autoTune0.ml @@ -17,17 +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); - 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/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index bb3592ebb6..de23a46620 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -251,8 +251,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" @@ -519,8 +522,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: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 diff --git a/src/cdomain/value/dune b/src/cdomain/value/dune index c89d5be04d..7e5f727699 100644 --- a/src/cdomain/value/dune +++ b/src/cdomain/value/dune @@ -7,13 +7,14 @@ (libraries batteries.unthreaded goblint_std + goblint_logs goblint_common goblint_config goblint_library goblint_domain goblint_incremental goblint-cil) - (flags :standard -open Goblint_std) + (flags :standard -open Goblint_std -open Goblint_logs) (preprocess (pps ppx_deriving.std diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index 0b1769e99c..b0e5d725a7 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -134,12 +134,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" 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" pretty x pretty y; assert (not (Base.equal x.BatHashcons.obj y.BatHashcons.obj)); false ) diff --git a/src/common/dune b/src/common/dune index 8576970900..0cded0bdf9 100644 --- a/src/common/dune +++ b/src/common/dune @@ -8,6 +8,7 @@ batteries.unthreaded zarith goblint_std + goblint_logs goblint_config goblint_tracing goblint-cil @@ -15,7 +16,7 @@ yojson goblint_timing qcheck-core.runner) - (flags :standard -open Goblint_std) + (flags :standard -open Goblint_std -open Goblint_logs) (foreign_stubs (language c) (names stubs)) (ocamlopt_flags :standard -no-float-const-prop) (preprocess diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index 093099dee1..77460f9f41 100644 --- a/src/common/framework/cfgTools.ml +++ b/src/common/framework/cfgTools.ml @@ -469,8 +469,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 (NH.stats cfgF) GobHashtbl.pretty_statistics (NH.stats cfgB)); + Logs.debug "cfgF (%a), cfgB (%a)" GobHashtbl.pretty_statistics (NH.stats cfgF) GobHashtbl.pretty_statistics (NH.stats cfgB); cfgF, cfgB, skippedByEdge let createCFG = Timing.wrap "createCFG" createCFG diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 602f1a5adc..9d2f8b2d3a 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -96,7 +96,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); + Logs.debug "Adding constructors to: %s" fd.svar.vname; let loc = match fd.sbody.bstmts with | s :: _ -> get_stmtLoc s | [] -> locUnknown @@ -136,7 +136,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); + Logs.debug "Constructors: %a" (Pretty.d_list ", " d_fundec) constructors; visitCilFileSameGlobals (new addConstructors constructors) ast; ast @@ -161,9 +161,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" 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" mn; set_string "exitfun[+]" mn; add_exit def acc | GFun ({svar={vstorage=NoStorage; vattr; _}; _} as def, _) when get_bool "nonstatic" && not (Cil.hasAttribute "goblint_stub" vattr) -> 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/common/util/gobFormat.ml b/src/common/util/gobFormat.ml index 11beec524c..3cda0a4758 100644 --- a/src/common/util/gobFormat.ml +++ b/src/common/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/common/util/messageUtil.ml b/src/common/util/messageUtil.ml index 17651fb05f..c0fcaab505 100644 --- a/src/common/util/messageUtil.ml +++ b/src/common/util/messageUtil.ml @@ -2,23 +2,20 @@ 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 *) diff --git a/src/common/util/messages.ml b/src/common/util/messages.ml index d7afec43c5..fe090379a1 100644 --- a/src/common/util/messages.ml +++ b/src/common/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 diff --git a/src/config/dune b/src/config/dune index ce5cb11559..c278dafb3c 100644 --- a/src/config/dune +++ b/src/config/dune @@ -7,6 +7,7 @@ (libraries batteries.unthreaded goblint_std + goblint_logs goblint_tracing fpath yojson @@ -14,7 +15,7 @@ cpu goblint.sites qcheck-core.runner) - (flags :standard -open Goblint_std) + (flags :standard -open Goblint_std -open Goblint_logs) (preprocess (pps ppx_blob)) diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml index 16b5511717..11f050b354 100644 --- a/src/config/gobConfig.ml +++ b/src/config/gobConfig.ml @@ -179,7 +179,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'" s; failwith "parsing" (** Here we store the actual configuration. *) @@ -302,10 +302,10 @@ struct if Goblint_tracing.tracing then Goblint_tracing.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" 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?" st print; failwith "get_path_string" let get_json : string -> Yojson.Safe.t = get_path_string Fun.id @@ -378,7 +378,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'." st s; raise e let merge json = diff --git a/src/config/jsonSchema.ml b/src/config/jsonSchema.ml index 701c948f3a..59b9733ca2 100644 --- a/src/config/jsonSchema.ml +++ b/src/config/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" 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" Json_schema.pp (create element); failwith "element_require_all" in { element with kind = kind' } diff --git a/src/config/options.ml b/src/config/options.ml index 125da3330b..861b87c290 100644 --- a/src/config/options.ml +++ b/src/config/options.ml @@ -29,7 +29,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" Json_schema.pp (create element); failwith "element_paths" let schema_paths (schema: schema): string list = @@ -71,7 +71,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" Json_schema.pp (create element); failwith "element_completions" let schema_completions (schema: schema): (string * string list) list = @@ -112,7 +112,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/config/options.schema.json b/src/config/options.schema.json index 0c83e342e0..df4b1365db 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1809,11 +1809,12 @@ "description": "Debugging options", "type": "object", "properties": { - "verbose": { - "title": "dbg.verbose", - "description": "Prints some status information.", - "type": "boolean", - "default": false + "level": { + "title": "dbg.level", + "description": "Logging level.", + "type": "string", + "enum": ["debug", "info", "warning", "error", "result"], + "default": "info" }, "timing": { "title": "dbg.timing", diff --git a/src/domain/mapDomain.ml b/src/domain/mapDomain.ml index 740da9969e..5f3c324317 100644 --- a/src/domain/mapDomain.ml +++ b/src/domain/mapDomain.ml @@ -199,7 +199,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 *) diff --git a/src/dune b/src/dune index d7c6d28026..7e44010648 100644 --- a/src/dune +++ b/src/dune @@ -7,7 +7,7 @@ (name goblint_lib) (public_name goblint.lib) (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare) - (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing + (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs ; Conditionally compile based on whether apron optional dependency is installed or not. ; Alternative dependencies seem like the only way to optionally depend on optional dependencies. ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies. @@ -60,7 +60,7 @@ (-> violationZ3.no-z3.ml) ) ) - (flags :standard -open Goblint_std) + (flags :standard -open Goblint_std -open Goblint_logs) (ocamlopt_flags :standard -no-float-const-prop) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson ppx_blob)) diff --git a/src/framework/analysisResult.ml b/src/framework/analysisResult.ml index e53ed37192..41c2bbd2c7 100644 --- a/src/framework/analysisResult.ml +++ b/src/framework/analysisResult.ml @@ -112,7 +112,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" fn; BatPrintf.fprintf f ""; BatPrintf.fprintf f "%s" GobSys.command_line; BatPrintf.fprintf f ""; @@ -152,7 +152,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" fn; fprintf f "{\n \"parameters\": \"%s\",\n " GobSys.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); @@ -166,8 +166,7 @@ struct let f = BatIO.output_channel out in write_file f (get_string "outfile") | "sarif" -> - let open BatPrintf in - printf "Writing Sarif to file: %s\n%!" (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/framework/constraints.ml b/src/framework/constraints.ml index 31dc668937..030b86446c 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -899,25 +899,25 @@ struct | Some {changes; _} -> changes | None -> empty_change_info () in - List.(Printf.printf "change_info = { unchanged = %d; changed = %d (with unchangedHeader = %d); added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (BatList.count_matching (fun c -> c.unchangedHeader) c.changed) (length c.added) (length c.removed)); + List.(Logs.info "change_info = { unchanged = %d; changed = %d (with unchangedHeader = %d); added = %d; removed = %d }" (length c.unchanged) (length c.changed) (BatList.count_matching (fun c -> c.unchangedHeader) 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 @@ -1713,22 +1713,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" 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" 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" 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; - 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" !eq !le !gr !uk let compare_locals h1 h2 = let eq, le, gr, uk = ref 0, ref 0, ref 0, ref 0 in @@ -1741,16 +1741,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" 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" 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" 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 @@ -1760,8 +1760,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" !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 @@ -1778,16 +1778,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" 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" 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" 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 @@ -1801,7 +1801,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" !eq !le !gr !uk !no2 !no1 let compare (name1,name2) (l1,g1) (l2,g2) = let one_ctx (n,_) v h = @@ -1813,11 +1813,12 @@ 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.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; - print_newline (); + Logs.newline (); end module CompareHashtbl (Var: VarType) (Dom: Lattice.S) (VH: Hashtbl.S with type key = Var.t) = @@ -1845,11 +1846,12 @@ 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.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 - ignore (Pretty.printf "EqConstrSys comparison summary: %t\n" (fun () -> msg)); - print_newline (); + Logs.info "EqConstrSys comparison summary: %t" (fun () -> msg); + Logs.newline (); end module CompareGlobal (GVar: VarType) (G: Lattice.S) (GH: Hashtbl.S with type key = GVar.t) = @@ -1857,11 +1859,12 @@ 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.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 - ignore (Pretty.printf "Globals comparison summary: %t\n" (fun () -> msg)); - print_newline (); + Logs.info "Globals comparison summary: %t" (fun () -> msg); + Logs.newline (); end module CompareNode (C: Printable.S) (D: Lattice.S) (LH: Hashtbl.S with type key = VarF (C).t) = @@ -1886,11 +1889,12 @@ struct nh let compare (name1, name2) vh1 vh2 = - Printf.printf "\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 - ignore (Pretty.printf "Nodes comparison summary: %t\n" (fun () -> msg)); - print_newline (); + Logs.info "Nodes comparison summary: %t" (fun () -> msg); + Logs.newline (); end diff --git a/src/framework/control.ml b/src/framework/control.ml index 391c766feb..4349b881d0 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -307,7 +307,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."); + 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 = @@ -374,21 +374,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" (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" (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."); + Logs.debug "Initializing %d globals." (CfgTools.numGlobals file); Timing.wrap "global_inits" do_global_inits file in @@ -482,7 +482,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 @@ -528,8 +528,7 @@ struct Some solver_data | 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.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 @@ -543,9 +542,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 ( - 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.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 @@ -556,9 +553,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 ( - 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.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; @@ -732,7 +727,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)) @@ -787,7 +782,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_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 @@ -819,7 +814,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 print_endline "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 25e809f9e9..24afae1597 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 () = @@ -34,10 +33,8 @@ let main () = handle_extraspecials (); GoblintDir.init (); - if get_bool "dbg.verbose" then ( - print_endline (GobUnix.localtime ()); - print_endline GobSys.command_line; - ); + Logs.debug "%s" (GobUnix.localtime ()); + Logs.debug "%s" GobSys.command_line; (* When analyzing a termination specification, activate the termination analysis before pre-processing. *) if get_bool "ana.autotune.enabled" && AutoTune.specificationTerminationIsActivated () then AutoTune.focusOnTermination (); let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in @@ -76,12 +73,12 @@ let main () = | Sys.Break -> (* raised on Ctrl-C if `Sys.catch_break true` *) do_stats (); Printexc.print_backtrace stderr; - eprintf "%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.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" (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/goblint_lib.ml b/src/goblint_lib.ml index 4b2eecb632..2fa83d0a7b 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -294,6 +294,7 @@ module CilMaps = CilMaps Various input/output interfaces and formats. *) module Messages = Messages +module Logs = Logs (** {2 Front-end} diff --git a/src/incremental/dune b/src/incremental/dune index 15c1d2a7af..9ac01dff97 100644 --- a/src/incremental/dune +++ b/src/incremental/dune @@ -8,11 +8,12 @@ batteries.unthreaded zarith goblint_std + goblint_logs goblint_config goblint_common goblint-cil fpath) - (flags :standard -open Goblint_std) + (flags :standard -open Goblint_std -open Goblint_logs) (preprocess (pps ppx_deriving.std diff --git a/src/incremental/makefileUtil.ml b/src/incremental/makefileUtil.ml index 843981ee38..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 print_endline ("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 print_endline ("deleting " ^ comb); + Logs.debug "deleting %s" comb; Sys.remove comb; done with Failure e -> () @@ -67,7 +67,7 @@ let run_cilly (path: Fpath.t) ~all_cppflags = let cflags = if all_cppflags = [] then "" else " CFLAGS+=" ^ Filename.quote (BatString.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) ^ ".") @@ -78,14 +78,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/incremental/serialize.ml b/src/incremental/serialize.ml index bddf3aa383..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 GobConfig.get_bool "dbg.verbose" 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/index.mld b/src/index.mld index 0f6b1c3e69..f0d63a0fc7 100644 --- a/src/index.mld +++ b/src/index.mld @@ -67,6 +67,9 @@ The following libraries provide utilities which are completely independent of Go {2 Library goblint.tracing} {!modules:Goblint_tracing} +{2 Library goblint.logs} +{!modules:Goblint_logs} + {1 Vendored} The following libraries are vendored in Goblint. diff --git a/src/maingoblint.ml b/src/maingoblint.ml index f1d2793d2e..40a997edee 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; - printf "Cil version: %s\n" Cil.cilVersion; - printf "Dune profile: %s\n" Goblint_build_info.dune_profile; - printf "OCaml version: %s\n" Sys.ocaml_version; - printf "OCaml flambda: %s\n" Goblint_build_info.ocaml_flambda; - if get_bool "dbg.verbose" then ( - printf "Library versions:\n"; + 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 ( + Logs.result "Library versions:"; List.iter (fun (name, version) -> let version = Option.default "[unknown]" version in - printf " %s: %s\n" name version + Logs.result " %s: %s" name version ) Goblint_build_info.statically_linked_libraries ); exit 0 @@ -54,7 +54,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 Goblint_tracing.addsystem sys - else (prerr_endline "Goblint has been compiled without tracing, recompile in trace profile (./scripts/trace_on.sh)"; raise Stdlib.Exit) + else (Logs.error "Goblint has been compiled without tracing, recompile in trace profile (./scripts/trace_on.sh)"; raise Stdlib.Exit) in let configure_html () = if (get_string "outfile" = "") then @@ -98,12 +98,12 @@ 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), "" ; "--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), "" @@ -124,14 +124,15 @@ 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 Stdlib.Exit -let eprint_color m = eprintf "%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 - 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."); @@ -167,11 +168,15 @@ 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"; + 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 () = - if get_bool "dbg.verbose" then ( + if Logs.Level.should_log Debug then ( Printexc.record_backtrace true; Errormsg.debugFlag := true; Errormsg.verboseFlag := true @@ -190,6 +195,7 @@ let handle_flags () = set_string "outfile" "" let handle_options () = + Logs.Level.current := Logs.Level.of_string (get_string "dbg.level"); check_arguments (); 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. *) if AutoTune.isActivated "memsafetySpecification" && get_string "ana.specification" <> "" then @@ -213,8 +219,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 Stdlib.Exit ) @@ -248,7 +254,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 print_endline command; + Logs.debug "%s" command; (nname, Some {ProcessPool.command; cwd = None}) ) else @@ -294,15 +300,13 @@ 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 ( - print_endline "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)) - ) 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 - 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 -> @@ -373,7 +377,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."; + Logs.debug "Preprocessing files."; let rec preprocess_arg_file ?preprocess = function | filename when not (Sys.file_exists (Fpath.to_string filename)) -> @@ -436,7 +440,7 @@ let special_path_regexp = Str.regexp "<.+>" (** Parse preprocessed files *) let parse_preprocessed preprocessed = (* get the AST *) - if get_bool "dbg.verbose" then print_endline "Parsing files."; + Logs.debug "Parsing files."; let goblint_cwd = GobFpath.cwd () in let get_ast_and_record_deps (preprocessed_file, task_opt) = @@ -512,10 +516,10 @@ let preprocess_parse_merge () = let do_stats () = if get_bool "dbg.timing.enabled" then ( - print_newline (); + Logs.newline (); Goblint_solver.SolverStats.print (); - print_newline (); - print_string "Timings:\n"; + Logs.newline (); + Logs.info "Timings:"; Timing.Default.print (Stdlib.Format.formatter_of_out_channel @@ Messages.get_out "timing" Legacy.stderr); flush_all () ) @@ -539,20 +543,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 print_endline "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 ignore (Pretty.printf "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a\n" - L.pretty stf L.pretty exf L.pretty otf); + 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 - print_endline @@ "Activated analyses: " ^ aa; - print_endline @@ "Activated transformations: " ^ 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?) *) @@ -565,7 +567,7 @@ let do_analyze change_info merged_AST = (* trigger Generic.SolverStats...print_stats *) GobSys.(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 @@ -587,11 +589,11 @@ let do_html_output () = in 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" command | exception 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\"." (Unix.error_message e) f a ) else - Format.eprintf "Warning: jar file %a not found.\n" Fpath.pp jar + Logs.Format.error "Warning: jar file %a not found." Fpath.pp jar ) let do_gobview cilfile = @@ -636,7 +638,7 @@ let do_gobview cilfile = ) dist_files ) else - eprintf "Warning: Cannot locate GobView.\n" + Logs.error "Warning: Cannot locate GobView." ) let handle_extraspecials () = @@ -647,7 +649,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; @@ -691,4 +693,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 (GobSys.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 (GobSys.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/messagesCompare.ml b/src/messagesCompare.ml index b4f43f8b10..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 ( - Printf.printf "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; ); - print_newline (); + Logs.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):" (MS.cardinal right_only_messages); MS.iter (Messages.print) right_only_messages; ) | _ -> diff --git a/src/solver/dune b/src/solver/dune index bd6d7a4d0a..577c75c9de 100644 --- a/src/solver/dune +++ b/src/solver/dune @@ -6,13 +6,14 @@ (libraries batteries.unthreaded goblint_std + goblint_logs goblint_common goblint_config goblint_domain goblint_constraint goblint_incremental goblint-cil) - (flags :standard -open Goblint_std) + (flags :standard -open Goblint_std -open Goblint_logs) (preprocess (pps ppx_deriving.std diff --git a/src/solver/generic.ml b/src/solver/generic.ml index 1a866546a1..63c1973b94 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 get_bool "dbg.verbose" 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 @@ -73,7 +71,7 @@ struct let eval_rhs_event x = if full_trace then trace "sol" "(Re-)evaluating %a\n" Var.pretty_trace x; incr SolverStats.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,14 +91,14 @@ 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 - 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:" !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 k let stats_csv = let save_run_str = GobConfig.get_string "save_run" in @@ -113,22 +111,22 @@ struct (* print generic and specific stats *) let print_stats _ = - print_newline (); + Logs.newline (); (* print_endline "# Generic solver stats"; *) - Printf.printf "runtime: %s\n" (GobSys.string_of_time ()); - Printf.printf "vars: %d, evals: %d\n" !SolverStats.vars !SolverStats.evals; - Option.may (fun v -> ignore @@ Pretty.printf "max updates: %d for var %a\n" !max_c Var.pretty_trace v) !max_var; - print_newline (); + Logs.info "runtime: %s" (GobSys.string_of_time ()); + Logs.info "vars: %d, evals: %d" !SolverStats.vars !SolverStats.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 (); - 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 = GobGc.print_quick_stat Legacy.stdout in - print_newline (); - Option.may (write_csv [GobSys.string_of_time (); string_of_int !SolverStats.vars; string_of_int !SolverStats.evals; string_of_int !ncontexts; string_of_int gc.Gc.top_heap_words]) stats_csv; + let gc = GobGc.print_quick_stat Legacy.stderr in + Logs.newline (); + Option.may (write_csv [GobSys.string_of_time (); string_of_int !SolverStats.vars; string_of_int !SolverStats.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/solver/postSolver.ml b/src/solver/postSolver.ml index 7f4f9c2b1f..c8b0e1dfd6 100644 --- a/src/solver/postSolver.ml +++ b/src/solver/postSolver.ml @@ -64,8 +64,7 @@ module Prune: F = include Unit (S) (VH) let finalize ~vh ~reachable = - if get_bool "dbg.verbose" then - print_endline "Pruning result"; + Logs.debug "Pruning result"; VH.filteri_inplace (fun x _ -> VH.mem reachable x @@ -84,13 +83,12 @@ module Verify: F = let complain_constraint x ~lhs ~rhs = AnalysisState.verified := Some false; M.msg_final Error ~category:Unsound "Fixpoint not reached"; - 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 = AnalysisState.verified := Some false; - M.msg_final Error ~category:Unsound "Fixpoint not reached"; - 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 @@ -134,8 +132,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 - Format.printf "Saving the solver result to %a\n" 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 @@ -178,8 +175,7 @@ struct module VH = PS.VH let post xs vs vh = - if get_bool "dbg.verbose" then - print_endline "Postsolving\n"; + Logs.debug "Postsolving"; let module StartS = struct diff --git a/src/solver/sLR.ml b/src/solver/sLR.ml index 8213fe8166..4d9b7fdbb9 100644 --- a/src/solver/sLR.ml +++ b/src/solver/sLR.ml @@ -153,9 +153,10 @@ 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; - print_newline (); + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; + Logs.newline (); ); HM.clear key ; @@ -329,13 +330,13 @@ module Make0 = let _ = P.rem_item stable x in if k < sk then 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 +356,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 +369,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 +388,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 = @@ -447,9 +448,10 @@ 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; - print_newline (); + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; + Logs.newline (); ); X.to_list () diff --git a/src/solver/sLRphased.ml b/src/solver/sLRphased.ml index 17571f0138..628b709685 100644 --- a/src/solver/sLRphased.ml +++ b/src/solver/sLRphased.ml @@ -136,10 +136,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; @@ -189,9 +189,10 @@ 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; - print_newline (); + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; + Logs.newline (); ); HM.clear key ; diff --git a/src/solver/sLRterm.ml b/src/solver/sLRterm.ml index 8ec34c7dc2..ab5e985392 100644 --- a/src/solver/sLRterm.ml +++ b/src/solver/sLRterm.ml @@ -50,11 +50,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" (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 vid in let init ?(side=false) x = @@ -208,9 +208,10 @@ 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; - print_newline (); + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; + Logs.newline (); ); HM.clear key ; diff --git a/src/solver/solverStats.ml b/src/solver/solverStats.ml index f8429f0868..a517f3f764 100644 --- a/src/solver/solverStats.ml +++ b/src/solver/solverStats.ml @@ -5,7 +5,7 @@ let evals = ref 0 let narrow_reuses = ref 0 let print () = - ignore (GoblintCil.Pretty.printf "vars = %d evals = %d narrow_reuses = %d\n" !vars !evals !narrow_reuses) + Logs.info "vars = %d evals = %d narrow_reuses = %d" !vars !evals !narrow_reuses let reset () = vars := 0; diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 54b7520cd6..ae899b7337 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -83,21 +83,21 @@ module Base = } let print_data data = - Printf.printf "|rho|=%d\n" (HM.length data.rho); - Printf.printf "|stable|=%d\n" (HM.length data.stable); - Printf.printf "|infl|=%d\n" (HM.length data.infl); - Printf.printf "|wpoint|=%d\n" (HM.length data.wpoint); - Printf.printf "|sides|=%d\n" (HM.length data.sides); - Printf.printf "|side_dep|=%d\n" (HM.length data.side_dep); - Printf.printf "|side_infl|=%d\n" (HM.length data.side_infl); - Printf.printf "|var_messages|=%d\n" (HM.length data.var_messages); - Printf.printf "|rho_write|=%d\n" (HM.length data.rho_write); - Printf.printf "|dep|=%d\n" (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 ( - Printf.printf "%s:\n" str; + if Logs.Level.should_log Debug then ( + Logs.debug "%s:" str; print_data data ) @@ -106,7 +106,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" S.Var.pretty_trace x; assert false ) ) data.rho @@ -204,7 +204,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 ); @@ -255,7 +255,7 @@ module Base = let () = print_solver_stats := fun () -> print_data data; - Printf.printf "|called|=%d\n" (HM.length called); + Logs.info "|called|=%d" (HM.length called); print_context_stats rho in @@ -406,7 +406,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" S.Var.pretty_trace y S.Dom.pretty d; ); assert (Hooks.system y = None); init y; @@ -521,7 +521,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" 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 *) @@ -634,14 +634,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? *) @@ -652,10 +652,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" S.Var.pretty_trace k; destabilize k ) ) sys_change.delete @@ -687,7 +687,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." S.Var.pretty_trace v else if HM.mem stable v then destabilize_leaf v ) sys_change.restart; @@ -706,7 +706,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" S.Var.pretty_trace v; restart_and_destabilize v (* restart side effect from start *) | _ -> (* don't restart unchanged start global *) @@ -723,7 +723,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" S.Var.pretty_trace v; restart_and_destabilize v | _ -> () @@ -743,7 +743,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" S.Var.pretty_trace y; HM.replace rho y (S.Dom.bot ()); ) w ) rho_write @@ -757,21 +757,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" 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; @@ -786,11 +786,11 @@ 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 !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; - print_newline (); + 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; + Logs.newline (); flush_all (); ); List.iter (fun x -> solve x Widen) unstable_vs; @@ -809,12 +809,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" 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" 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 ( @@ -823,9 +823,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" 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 ( @@ -836,8 +836,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 - print_endline ("Restoring missing values."); + Logs.debug "Restoring missing values."; let restore () = let get x = let d = get ~check:true x in @@ -847,7 +846,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" !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); ); @@ -856,9 +855,10 @@ module Base = print_data_verbose 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; - print_newline (); + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; + Logs.newline (); ); (* Prune other data structures than rho with reachable. @@ -993,7 +993,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 *) @@ -1003,7 +1003,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 @@ -1100,7 +1100,7 @@ module DepVals: GenericEqIncrSolver = module HM = HM let print_data () = - Printf.printf "|dep_vals|=%d\n" (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/solver/topDown_space_cache_term.ml b/src/solver/topDown_space_cache_term.ml index f6c256517c..689ebf56fb 100644 --- a/src/solver/topDown_space_cache_term.ml +++ b/src/solver/topDown_space_cache_term.ml @@ -141,7 +141,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" S.Var.pretty_trace x; S.Dom.top () ) else HM.find rho x @@ -149,7 +149,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" S.Var.pretty_trace y S.Dom.pretty d S.Dom.pretty d' in let eq x = match S.system x with @@ -160,7 +160,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 @@ -171,8 +171,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 - print_endline ("Restoring missing values."); + Logs.debug "Restoring missing values."; let restore () = let get x = let d = get x in @@ -181,7 +180,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" !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/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml index 2c7e61efd0..0cf59f0c78 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" @@ -88,7 +85,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)"; + Logs.debug "| (Unparseable)"; Some false (* Successfully parsed expression *) | Some expression -> @@ -96,7 +93,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)"; + Logs.debug "| (Unreachable)"; Some false (* Valid location *) | Some value_before -> @@ -120,17 +117,11 @@ struct (* Prefer successor evaluation *) match successor_evaluation with | None -> - if is_debug () then - begin - print_endline ("| /*" ^ (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 - print_endline ("| " ^ (statement |> string_of_statement) ^ "/*" ^ (value_after |> string_of_evaluation_result) ^ "*/"); - print_endline ("| " ^ (~! !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 = @@ -159,8 +150,7 @@ struct | Error message -> 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) = @@ -202,16 +192,18 @@ struct match res with | Some value -> if value then - print_endline (loc |> string_of_location) - else if is_debug () then - print_endline ((loc |> string_of_location) ^ " x") + Logs.info "%s" (loc |> string_of_location) + else + Logs.debug "%s x" (loc |> string_of_location) | None -> - if query.mode = `May || is_debug () then - print_endline ((loc |> string_of_location) ^ " ?") + 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 - | Error e -> prerr_endline e + | Error e -> Logs.error "%s" e let name = transformation_identifier diff --git a/src/transform/transform.ml b/src/transform/transform.ml index 337f3dfddb..b13766c4ab 100644 --- a/src/transform/transform.ml +++ b/src/transform/transform.ml @@ -50,16 +50,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 (Z.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/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/compilationDatabase.ml b/src/util/compilationDatabase.ml index 2443b8d3ab..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 - 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" 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 - 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" 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/logs/ansiColors.ml b/src/util/logs/ansiColors.ml new file mode 100644 index 0000000000..0f3819d7b5 --- /dev/null +++ b/src/util/logs/ansiColors.ml @@ -0,0 +1,12 @@ +(** ANSI escape colors. *) + +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/logs/dune b/src/util/logs/dune new file mode 100644 index 0000000000..d630d38547 --- /dev/null +++ b/src/util/logs/dune @@ -0,0 +1,16 @@ +(include_subdirs no) + +(library + (name goblint_logs) + (public_name goblint.logs) + (libraries + batteries.unthreaded + goblint_std + goblint-cil) + (flags :standard -open Goblint_std) + (preprocess + (pps + ppx_deriving.std + ppx_deriving_hash + ppx_deriving_yojson)) + (instrumentation (backend bisect_ppx))) diff --git a/src/util/logs/logs.ml b/src/util/logs/logs.ml new file mode 100644 index 0000000000..496a4182fe --- /dev/null +++ b/src/util/logs/logs.ml @@ -0,0 +1,175 @@ +(** Logging, which isn't for presenting analysis results. *) + +module Level = +struct + type t = + | Debug + | 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 *) + + let compare x y = Stdlib.compare (to_enum x) (to_enum y) + + let of_string = function + | "debug" -> Debug + | "info" -> Info + | "warning" -> Warning + | "error" -> Error + | "result" -> Result + | _ -> invalid_arg "Logs.Level.of_string" + + let current = ref Debug + + 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 *) + | Result -> "reset" +end + +module Result = +struct + let use_stdout = ref true (* TODO: disable in server mode *) +end + + +module type Kind = +sig + type b + type c + val log: Level.t -> ('a, b, c, unit) format4 -> 'a +end + +module PrettyKind = +struct + open GoblintCil + + type b = unit + type c = Pretty.doc + let log level fmt = + 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 + GobPretty.igprintf () fmt +end + +module FormatKind = +struct + type b = Format.formatter + type c = unit + let log level fmt = + if Level.should_log level then ( + 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 + Format.ifprintf Format.err_formatter fmt +end + +module BatteriesKind = +struct + type b = unit BatIO.output + type c = unit + let log level fmt = + 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 + BatPrintf.ifprintf BatIO.stderr fmt +end + + +module MakeKind (Kind: Kind) = +struct + open Kind + + let log = 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 () +end + +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 *) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 26f306a267..519477557b 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -154,7 +154,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 @@ -274,25 +274,25 @@ let fixedLoopSize loopStatement func = else constBefore var loopStatement func >>= fun start -> assignmentDifference loopStatement var >>= fun diff -> - print_endline "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 "comparison: "; + Pretty.fprint stderr (dn_exp () comparison) ~width:max_int; + 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 @@ -353,7 +353,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*) @@ -450,7 +450,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) -> diff --git a/src/util/precCompare.ml b/src/util/precCompare.ml index 45b3e32ed8..a04e395e83 100644 --- a/src/util/precCompare.ml +++ b/src/util/precCompare.ml @@ -81,7 +81,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" 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 @@ -129,6 +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) -> 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.result "%t" (fun () -> msg)); + Logs.newline (); + Logs.result "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 1da3aa25ce..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 - Printf.printf "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/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 diff --git a/src/util/tracing/dune b/src/util/tracing/dune index 7e37139567..452d226eec 100644 --- a/src/util/tracing/dune +++ b/src/util/tracing/dune @@ -5,5 +5,6 @@ (public_name goblint.tracing) (libraries goblint_std + goblint_logs goblint-cil goblint_build_info)) diff --git a/src/util/tracing/goblint_tracing.ml b/src/util/tracing/goblint_tracing.ml index 0e5580b036..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 -> print_endline ("WTF? " ^ 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 diff --git a/src/witness/violation.ml b/src/witness/violation.ml index d48005a988..2c43217a68 100644 --- a/src/witness/violation.ml +++ b/src/witness/violation.ml @@ -70,9 +70,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 @@ -81,7 +81,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 @@ -125,7 +125,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 @@ -146,12 +146,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 29f337a668..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 = - Printf.printf "SV-COMP result: %s\n" s + Logs.result "SV-COMP result: %s" s let print_task_result (module TaskResult:TaskResult): unit = print_svcomp_result (Result.to_string TaskResult.result) @@ -284,7 +284,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" (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 a93684bdb3..d004320ad3 100644 --- a/src/witness/z3/violationZ3.z3.ml +++ b/src/witness/z3/violationZ3.z3.ml @@ -154,16 +154,16 @@ struct end and do_assert revpath' i env' expr = - Printf.printf "%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 - Printf.printf "%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 -> - Printf.printf "%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 -> @@ -183,7 +183,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 *) 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/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) 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; 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]