Merge branch 'master' into issue-1192

Author: karoliineh

.git-blame-ignore-revs

@@ -31,3 +31,6 @@ ec8611a3a72ae0d95ec82ffee16c5c4785111aa1
 
 # fix indentation in baseInvariant
 f3ffd5e45c034574020f56519ccdb021da2a1479
+
+# Fix indentation in various non-legacy code
+c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9

.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

conf/incremental.json

@@ -24,7 +24,7 @@
     "earlyglobs": true
   },
   "dbg": {
-    "verbose": true,
+    "level": "debug",
     "trace": {
       "context": true
     },

conf/minimal_incremental.json

@@ -23,7 +23,7 @@
     "earlyglobs": true
   },
   "dbg": {
-    "verbose": true,
+    "level": "debug",
     "trace": {
       "context": true
     },

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;
 ```

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
 

goblint.opam

@@ -77,7 +77,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

goblint.opam.locked

@@ -131,6 +131,10 @@ post-messages: [
 ]
 # TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
 pin-depends: [
+  [
+    "goblint-cil.2.0.3"
+    "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51"
+  ]
   [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"

goblint.opam.template

@@ -3,7 +3,7 @@
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

gobview

@@ -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 ()

src/analyses/apron/relationAnalysis.apron.ml

@@ -1020,7 +1020,7 @@ struct
     match ofs with
     | NoOffset -> `NoOffset
     | Field (fld, ofs) -> `Field (fld, convert_offset ~ctx st ofs)
-    | Index (exp, ofs) when CilType.Exp.equal exp Offset.Index.Exp.any -> (* special offset added by convertToQueryLval *)
+    | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
       `Index (IdxDom.top (), convert_offset ~ctx st ofs)
     | Index (exp, ofs) ->
       match eval_rv ~ctx st exp with
@@ -2347,7 +2347,7 @@ struct
                | CArrays.IsNotSubstr -> Address (AD.null_ptr)
                | CArrays.IsSubstrAtIndex0 -> Address (eval_lv ~ctx st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset))
                | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv ~ctx st
-                                                              (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr)))
+                                                              (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Lazy.force Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr)))
         | None -> st
       end
     | Strcmp { s1; s2; n }, _ ->

src/analyses/base.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

src/analyses/basePriv.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

src/analyses/extractPthread.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/mCP.ml

@@ -171,7 +171,7 @@ struct
       match ofs with
       | NoOffset -> `NoOffset
       | Field (fld, ofs) -> `Field (fld, convert_offset ofs)
-      | Index (exp, ofs) when CilType.Exp.equal exp Offset.Index.Exp.any -> (* special offset added by convertToQueryLval *)
+      | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
         `Index (ID.top (), convert_offset ofs)
       | Index (exp, ofs) ->
         let i = match ctx.ask (Queries.EvalInt exp) with

src/analyses/memOutOfBounds.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 =

src/analyses/raceAnalysis.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 ();