Replace direct `stdout` printing with logging #1117

sim642 · 2023-07-25T16:50:56Z

Apparently this is something I started but never opened a PR for. The problem is that there's lots of direct printing to stdout throughout Goblint, which makes output uncontrollable and unpredictable. For example, server mode cannot use stdout because some random printing might get mixed in and break the whole JSON stream.

The idea is to add a Logs library, which is a bit like Messages. It has various logging levels that can be toggled globally (unlike direct printing). The difference is that Messages is for things related to analysis results and shown in IDE, while logging is about Goblint itself, e.g. those TD3 incremental changes lines.
Messages are unordered and incrementally preserved, while Logs just come out in the order they happen and aren't preserved like that.

TODO

Fix conflicts with master. (latest: 2024-02-13)
Replace all new direct printing on master with Logs. (latest: 2024-02-13)
Add log level option.
Maingoblint.check_arguments.
Remove dbg.verbose.
What to do with GobView printing hacks?
Document Logs in developer guide.
Adapt to Logs module in Goblint gobview#40.

src/analyses/extractPthread.ml

src/maingoblint.ml

src/spec/specUtil.ml

src/util/backtrace/goblint_backtrace.ml

src/util/options.ml

src/maingoblint.ml

This is needed to preserve compatibility with version checks, e.g. in BenchExec.

src/maingoblint.ml

src/analyses/extractPthread.ml


    let rec process_def res =
-      print_endline @@ Resource.show res ;
+      print_endline @@ Resource.show res ; (* nosemgrep: print-not-logging *)


src/config/options.ml


 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 *)


src/config/options.ml


 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 *)


src/maingoblint.ml

 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 *)


src/util/backtrace/goblint_backtrace.ml

  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 *)


Normal logging works just fine.

sim642 · 2024-01-11T10:50:08Z

There's now a "result" log level that by default goes to stdout for the handful of places that were pointed out. In server mode, it is also directed to stderr to allow clean JSON-RPC communication.

michael-schwarz

Looks good! I have a few remaining questions in some places 😄

src/analyses/extractPthread.ml

src/analyses/threadId.ml

src/framework/constraints.ml

src/framework/control.ml

src/witness/witness.ml

src/util/tracing/goblint_tracing.ml

michael-schwarz · 2024-02-07T06:54:40Z

It seems like there's only two open comments left. I'd suggest to merge as soon as these are addressed to avoid it going out-of-sync and requiring a lot of work again. Wdyt?

sim642 · 2024-02-07T08:47:37Z

Indeed, but I cannot check if GobView still works because of

Add alert for unsupported queries gobview#25 (comment)
Remove unused Libmaincil module cil#165, Adapt to removed Libmaincil module #1350, Adapt to removed Libmaincil module gobview#39

sim642 · 2024-02-13T13:47:35Z

On top of GobView fixes, I confirmed that it still works.

sim642 added 14 commits March 14, 2023 13:52

Add Logs prototype

b1e3770

Add semgrep rule for printing

f7d2d5b

Start using Logs

80125a7

Add newline after logging

aff84b1

Use more Logs

72bf02f

Add Logs.newline

aa1e112

Use Logs everywhere

1aa91c1

Remove %! from Logs formats

22d8963

Remove newlines from log messages

2d8678f

Implement Logs.newline

3dcf492

Extract GobPretty.igprintf from Tracing

9c4d1b8

Add logging levels

67441e0

Use Logs where semgrep missed

5cd82af

Add colors to Logs

61646c5

sim642 added the cleanup Refactoring, clean-up label Jul 25, 2023

sim642 self-assigned this Jul 25, 2023

github-advanced-security bot found potential problems Jul 25, 2023

View reviewed changes

sim642 mentioned this pull request Jul 25, 2023

Semgrep doesn't respect ignores if --sarif argument is used semgrep/semgrep#7121

Closed

3 tasks

Merge branch 'master' into logs

a229a40

github-advanced-security bot found potential problems Jul 26, 2023

View reviewed changes

src/maingoblint.ml Fixed Show fixed Hide fixed

sim642 added 8 commits July 26, 2023 13:45

Use Logs.info in longjmp autotune

0697234

Remove unused Printf opens

23a14b0

Fix d_varinfo mismerge

d2377cd

Add dbg.level option

b836978

Remove Maingoblint.eprint_color

16344cc

Add log message level printing

e673d9d

Fix log output in cram tests

ec1eeb5

Revert --version to normal stdout printing

ea809cf

This is needed to preserve compatibility with version checks, e.g. in BenchExec.

github-advanced-security bot found potential problems Aug 1, 2023

View reviewed changes

Use Logs.debug instead of dbg.verbose conditional in most places

d3283ea

sim642 added this to the v2.4.0 milestone Nov 28, 2023

sim642 added 2 commits January 10, 2024 16:24

Merge branch 'master' into logs

eb8b14d

Replace merged direct printing with Logs

a354ce3

github-advanced-security bot found potential problems Jan 10, 2024

View reviewed changes

sim642 added 10 commits January 10, 2024 17:44

Add Result log level to stdout

bbc360f

Use Logs.result

68d1d1a

Optimize ValueDomain.warn_type

31ad591

Use messages for dbg.print_tids

0ca32e0

Update cram test with SV-COMP specification

6f89b91

Update log levels in debugging docs

355c521

Add warning about dbg.print_wpoints

c9834e8

Add result log level to options

32db3a3

Remove print_endline for GobView

9135222

Normal logging works just fine.

Do not use stdout for logs if server.mode is stdio

05d9cce

sim642 requested a review from michael-schwarz January 23, 2024 08:42

michael-schwarz reviewed Jan 24, 2024

View reviewed changes

sim642 added 2 commits February 7, 2024 10:06

Add warning about dbg.print_tids

b8b98f3

Replace WTF error in Goblint_tracing

520c742

sim642 mentioned this pull request Feb 7, 2024

Adapt to Logs module in Goblint goblint/gobview#40

Merged

Merge branch 'master' into logs

f3b1945

Merge branch 'master' into logs

b61a064

sim642 merged commit 60c1030 into master Feb 13, 2024

sim642 deleted the logs branch February 13, 2024 13:51

sim642 mentioned this pull request Aug 2, 2024

[new release] goblint (2.4.0) ocaml/opam-repository#26327

Merged

Replace direct stdout printing with logging #1117

Replace direct stdout printing with logging #1117

Uh oh!

Conversation

sim642 commented Jul 25, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

TODO

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Check warning

Check warning

Check warning

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Check warning

Check warning

sim642 commented Jan 11, 2024

Uh oh!

michael-schwarz left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

michael-schwarz commented Feb 7, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sim642 commented Feb 7, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sim642 commented Feb 13, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Replace direct `stdout` printing with logging #1117

Replace direct `stdout` printing with logging #1117

sim642 commented Jul 25, 2023 •

edited

Loading

michael-schwarz commented Feb 7, 2024 •

edited

Loading

sim642 commented Feb 7, 2024 •

edited

Loading