Replace direct stdout printing with logging

.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

src/analyses/apron/relationAnalysis.apron.ml

@@ -727,7 +727,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 ()

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 !Tracing.current_loc (is_unprotected ask x) VD.pretty v);
+     Logs.debug "READ GLOBAL %a (%a, %B) = %a" d_varinfo x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v;
      r *)
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
     let cpa' = CPA.add x v st.cpa in
@@ -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" d_varinfo 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" d_varinfo x VD.pretty v CPA.pretty cpa';
      cpa' *)
 
   let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
@@ -1674,7 +1674,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

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.info
       "Copy spin/pthread_base.pml to same folder and then do: spin -a \
        pthread.pml && cc -o pan pan.c && ./pan -a"
 end

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

src/analyses/raceAnalysis.ml

@@ -105,7 +105,7 @@ struct
       let g: V.t = Obj.obj g in
       begin match g with
         | `Left g' -> (* accesses *)
-          (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
+          (* Logs.debug "WarnGlobal %a" CilType.Varinfo.pretty g; *)
           let trie = G.access (ctx.global g) in
           (** Distribute access to contained fields. *)
           let rec distribute_inner offset (accs, children) ancestor_accs =

src/analyses/termination.ml

@@ -140,7 +140,7 @@ class loopInstrVisitor (fd : fundec) = object(self)
          | _ -> ());
         s
       | Loop (b, loc, eloc, Some continue, Some break) ->
-        print_endline @@ "WARN: Could not determine loop variable for loop at " ^ CilType.Location.show loc;
+        Logs.warn "WARN: Could not determine loop variable for loop at %a" CilType.Location.pretty loc;
         s
       | _ when Hashtbl.mem loopBreaks s.sid -> (* after a loop, we check that t is bounded/positive (no overflow happened) *)
         let loc = Hashtbl.find loopBreaks s.sid in

src/analyses/threadId.ml

@@ -156,12 +156,13 @@ struct
     let non_uniques = List.filter_map (fun (a,b) -> if not (Thread.is_unique a) then Some a else None) tids in
     let uc = List.length uniques in
     let nc = List.length non_uniques in
-    Printf.printf "Encountered number of thread IDs (unique): %i (%i)\n" (uc+nc) uc;
-    Printf.printf "unique: ";
-    List.iter (fun tid -> Printf.printf " %s " (Thread.show tid)) uniques;
-    Printf.printf "\nnon-unique: ";
-    List.iter (fun tid -> Printf.printf " %s " (Thread.show tid)) non_uniques;
-    Printf.printf "\n"
+    Logs.debug "Encountered number of thread IDs (unique): %i (%i)" (uc+nc) uc;
+    Logs.debug "unique: ";
+    List.iter (fun tid -> Logs.debug " %s " (Thread.show tid)) uniques;
+    Logs.newline ();
+    Logs.debug "non-unique: ";
+    List.iter (fun tid -> Logs.debug " %s " (Thread.show tid)) non_uniques;
+    Logs.newline ()
 
   let finalize () =
     if GobConfig.get_bool "dbg.print_tids" then print_tid_info ();

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;
          setCongruenceRecursive (Cilfacade.find_varinfo_fundec vinfo) (depth -1) neigbourFunction
       )
       (FunctionSet.filter (*for extern and builtin functions there is no function definition in CIL*)
@@ -125,10 +125,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
@@ -144,7 +144,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"])];
       )
     )
@@ -192,7 +192,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;
   )
 
@@ -214,7 +214,7 @@ let focusOnSpecification () =
   match Svcomp.Specification.of_option () 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;
@@ -363,9 +363,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;
@@ -396,14 +396,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
   {
@@ -420,10 +420,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";
   }
 
 
@@ -443,13 +443,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
 
@@ -459,11 +459,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;

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

src/cdomains/valueDomain.ml

@@ -502,7 +502,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 !Tracing.current_loc pretty x pretty y
+      Logs.debug "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Tracing.current_loc pretty x pretty y
 
   let rec leq x y =
     match (x,y) with

src/domains/mapDomain.ml

@@ -196,7 +196,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 *)
 

src/domains/printable.ml

@@ -146,12 +146,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
     )

src/framework/analyses.ml

@@ -252,7 +252,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 "<run>";
         BatPrintf.fprintf f "<parameters>%s</parameters>" GobSys.command_line;
         BatPrintf.fprintf f "<statistics>";
@@ -292,7 +292,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);
@@ -307,7 +307,7 @@ struct
         write_file f (get_string "outfile")
     | "sarif" ->
       let open BatPrintf in
-      printf "Writing Sarif to file: %s\n%!" (get_string "outfile");
+      Logs.info "Writing Sarif to file: %s" (get_string "outfile");
       Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list));
     | "json-messages" ->
       let json = `Assoc [

src/framework/cfgTools.ml

@@ -475,7 +475,7 @@ let createCFG (file: file) =
     );
   if Messages.tracing then Messages.trace "cfg" "CFG building finished.\n\n";
   if get_bool "dbg.verbose" then
-    ignore (Pretty.eprintf "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB));
+    Logs.debug "cfgF (%a), cfgB (%a)" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB);
   cfgF, cfgB, skippedByEdge
 
 let createCFG = Timing.wrap "createCFG" createCFG