Merge branch 'master' into linear-two-var-equality

.git-blame-ignore-revs

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

.github/workflows/coverage.yml

@@ -38,6 +38,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test

.github/workflows/docs.yml

@@ -2,8 +2,7 @@ name: docs
 
 on:
   push:
-    branches:
-      - master
+  pull_request:
 
   workflow_dispatch:
 
@@ -55,7 +54,7 @@ jobs:
         run: opam exec -- dune build @doc
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v2
+        uses: actions/upload-pages-artifact@v3
         with:
           path: _build/default/_doc/_html/
 
@@ -65,7 +64,8 @@ jobs:
       url: ${{ steps.deployment.outputs.page_url }}
     runs-on: ubuntu-latest
     needs: api-build
+    if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v3
+        uses: actions/deploy-pages@v4

.github/workflows/locked.yml

@@ -40,6 +40,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
@@ -117,6 +122,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install spin
         run: sudo apt-get -y install spin
@@ -173,7 +183,7 @@ jobs:
         run: ./make.sh nat
 
       - name: Build Gobview
-        run: opam exec -- dune build gobview
+        run: ./make.sh view
 
       - name: Install selenium
         run: pip3 install selenium webdriver-manager

.github/workflows/unlocked.yml

@@ -34,9 +34,6 @@ jobs:
           - os: ubuntu-latest
             ocaml-compiler: 4.14.x
             z3: true
-          - os: ubuntu-latest
-            ocaml-compiler: 5.0.0
-            apron: false
 
     # customize name to use readable string for apron instead of just a boolean
     # workaround for missing ternary operator: https://github.com/actions/runner/issues/409
@@ -52,6 +49,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
@@ -60,7 +62,7 @@ jobs:
         if: ${{ matrix.apron }}
         run: |
           opam depext apron
-          opam install apron
+          opam install apron mlgmpidl.1.2.15
 
       - name: Install Z3 dependencies
         if: ${{ matrix.z3 }}
@@ -146,14 +148,19 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
 
       - name: Install Apron dependencies
         run: |
           opam depext apron
-          opam install apron
+          opam install apron mlgmpidl.1.2.15
 
       - name: Build
         if: ${{ false }}
@@ -262,14 +269,19 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install Goblint with test
         run: opam install goblint --with-test
 
       - name: Install Apron dependencies
         run: |
           opam depext apron
-          opam install apron
+          opam install apron mlgmpidl.1.2.15
 
       - name: Symlink installed goblint to repository # because tests want to use locally built one
         run: ln -s $(opam exec -- which goblint) goblint

.gitignore

@@ -10,6 +10,7 @@ goblint
 goblint.byte
 goblint.json
 goblint.domaintest
+goblint_http.exe
 src/config*.ml
 tests/bench.txt
 .DS_Store

.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
 

docs/user-guide/annotating.md

@@ -66,3 +66,4 @@ Include `goblint.h` when using these.
 * `__goblint_assume_join(id)` is like `pthread_join(id, NULL)`, but considers the given thread IDs must-joined even if Goblint cannot, e.g. due to non-uniqueness.
   Notably, this annotation can be used after a threads joining loop to make the assumption that the loop correctly joined all those threads.
   _Misuse of this annotation can cause unsoundness._
+* `__goblint_globalize(ptr)` forces all data potentially pointed to by `ptr` to be treated as global by simulating it escaping the thread.

docs/user-guide/inspecting.md

@@ -18,11 +18,10 @@ For the initial setup:
 
 To build GobView (also for development):
 
-1. Run `dune build gobview` in the analyzer directory to build the web UI
-2. The executable for the http-server can then be found in the directory `./_build/default/gobview/goblint-http-server`. It takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\
-`./_build/default/gobview/goblint-http-server/goblint_http.exe -with-goblint ../analyzer/goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"`
-
-4. Visit <http://localhost:8080>
+1. Run `make view` in the analyzer directory to build the web UI
+2. The executable `goblint_http.exe` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\
+`./goblint_http.exe tests/regression/00-sanity/01-assert.c`
+3. Visit <http://localhost:8080>
 
 ## Witnesses
 

dune-project

@@ -59,6 +59,7 @@
   )
   (conflicts
     (result (< 1.5)) ; transitive dependency, overrides standard Result module and doesn't have map_error, bind
+    (ez-conf-lib (= 1)) ; https://github.com/nberth/ez-conf-lib/issues/3
   )
   (sites
     (share lib)

goblint.opam

@@ -54,6 +54,7 @@ depends: [
 depopts: ["apron" "z3"]
 conflicts: [
   "result" {< "1.5"}
+  "ez-conf-lib" {= "1"}
 ]
 build: [
   ["dune" "subst"] {dev}
@@ -77,10 +78,13 @@ 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#833378d9102578bab7b62174cb029d385db417a5" ]
   # 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" ]
 ]
+depexts: [
+  ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

goblint.opam.locked

@@ -125,14 +125,20 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 conflicts: [
   "result" {< "1.5"}
+  "ez-conf-lib" {= "1"}
 ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
 # 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#833378d9102578bab7b62174cb029d385db417a5"
+  ]
   [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
   ]
 ]
+depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

goblint.opam.template

@@ -3,10 +3,13 @@
 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#833378d9102578bab7b62174cb029d385db417a5" ]
   # 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" ]
 ]
+depexts: [
+  ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

lib/goblint/runtime/include/goblint.h

@@ -3,6 +3,7 @@ void __goblint_assume(int exp);
 void __goblint_assert(int exp);
 
 void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to avoid pthread.h interfering with Linux kernel headers
+void __goblint_globalize(void *ptr);
 
 void __goblint_split_begin(int exp);
 void __goblint_split_end(int exp);