Merge branch 'master' into thread-unsafe-funs

.git-blame-ignore-revs

@@ -28,3 +28,6 @@ ec8611a3a72ae0d95ec82ffee16c5c4785111aa1
 
 # Set up end-of-line normalization.
 78fd79e7f4d15c4412221b155971fac2e0616b90
+
+# fix indentation in baseInvariant
+f3ffd5e45c034574020f56519ccdb021da2a1479

.github/workflows/coverage.yml

@@ -0,0 +1,92 @@
+name: coverage
+
+on:
+  pull_request:
+
+  workflow_dispatch:
+
+  schedule:
+    # nightly
+    - cron: '31 1 * * *' # 01:31 UTC, 02:31/03:31 Munich, 03:31/04:31 Tartu
+    # GitHub Actions load is high at minute 0, so avoid that
+
+jobs:
+  coverage:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-latest
+        ocaml-compiler:
+          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          # don't add any other because they won't be used
+
+    runs-on: ${{ matrix.os }}
+
+    env:
+      OCAMLRUNPARAM: b
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v3
+
+      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
+        env:
+          # otherwise setup-ocaml pins non-locked dependencies
+          # https://github.com/ocaml/setup-ocaml/issues/166
+          OPAMLOCKED: locked
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Install dependencies
+        run: opam install . --deps-only --locked --with-test
+
+      - name: Install coverage dependencies
+        run: opam install bisect_ppx
+
+      - name: Build
+        run: ./make.sh coverage
+
+      - name: Test regression
+        run: ./make.sh headers testci
+
+      - name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: |
+          ruby scripts/update_suite.rb group apron -s
+          ruby scripts/update_suite.rb group apron2 -s
+
+      - name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group octagon -s
+
+      - name: Test apron affeq regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group affeq -s
+
+      - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group apron-mukherjee -s
+
+      - name: Test regression cram
+        run: opam exec -- dune runtest tests/regression
+
+      - name: Test incremental cram
+        run: opam exec -- dune runtest tests/incremental
+
+      - name: Test unit
+        run: opam exec -- dune runtest unittest
+
+      - name: Test incremental regression
+        run: ruby scripts/update_suite.rb -i
+
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
+      - run: opam exec -- bisect-ppx-report send-to Coveralls --coverage-path=.
+        env:
+          COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
+          PULL_REQUEST_NUMBER: ${{ github.event.number }}
+
+      - uses: actions/upload-artifact@v3
+        if: always()
+        with:
+          name: suite_result
+          path: tests/suite_result/

.github/workflows/docs.yml

@@ -52,7 +52,7 @@ jobs:
         run: opam exec -- dune build @doc
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
+        uses: actions/upload-pages-artifact@v2
         with:
           path: _build/default/_doc/_html/
 

.github/workflows/locked.yml

@@ -174,5 +174,4 @@ jobs:
 
       - name: Test Gobview
         run: |
-          ./goblint --enable gobview tests/regression/00-sanity/01-assert.c
           python3 scripts/test-gobview.py

.gitignore

@@ -94,3 +94,10 @@ transformed.c
 
 # docs
 site/
+
+# coverage
+
+# bisect_ppx
+*.coverage
+# bisect-ppx-report
+_coverage/*

README.md

@@ -1,11 +1,13 @@
 # Goblint
+[![GitHub release status](https://img.shields.io/github/v/release/goblint/analyzer)](https://github.com/goblint/analyzer/releases)
+[![opam package status](https://badgen.net/opam/v/goblint)](https://opam.ocaml.org/packages/goblint)
+[![Zenodo DOI](https://zenodo.org/badge/2066905.svg)](https://zenodo.org/badge/latestdoi/2066905)
+
 [![locked workflow status](https://github.com/goblint/analyzer/actions/workflows/locked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/locked.yml)
 [![unlocked workflow status](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml)
+[![Coverage Status](https://coveralls.io/repos/github/goblint/analyzer/badge.svg?branch=master)](https://coveralls.io/github/goblint/analyzer?branch=master)
 [![docker workflow status](https://github.com/goblint/analyzer/actions/workflows/docker.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/docker.yml)
 [![Documentation Status](https://readthedocs.org/projects/goblint/badge/?version=latest)](https://goblint.readthedocs.io/en/latest/?badge=latest)
-[![GitHub release status](https://img.shields.io/github/v/release/goblint/analyzer)](https://github.com/goblint/analyzer/releases)
-[![opam package status](https://badgen.net/opam/v/goblint)](https://opam.ocaml.org/packages/goblint)
-[![Zenodo DOI](https://zenodo.org/badge/2066905.svg)](https://zenodo.org/badge/latestdoi/2066905)
 
 Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/en/latest/) or [GitHub](./docs/).
 

docs/developer-guide/testing.md

@@ -11,7 +11,8 @@ Regression tests can be run with various granularity:
 * Run all tests with: `./scripts/update_suite.rb`.
 * Run a group of tests with: `./scripts/update_suite.rb group sanity`.
 
-    Unfortunately this also runs skipped tests...
+    Unfortunately this also runs skipped tests.
+    This is a bug that is used as a feature in the tests with Apron, as not all CI jobs have the Apron library installed.
 
 * Run a single test with: `./scripts/update_suite.rb assert`.
 * Run a single test with full output: `./regtest.sh 00 01`.
@@ -24,8 +25,42 @@ gobopt='--set ana.base.privatization write+lock' ./scripts/update_suite.rb
 ```
 
 ### Writing
-* Add parameters to a regression test in the first line: `// PARAM: --set warn.debug true`
-* Annotate lines inside the regression test with comments: `arr[9] = 10; // WARN`
+Regression tests use single-line comments (with `//`) as annotations.
+
+#### First line
+A comment on the first line can contain the following:
+
+| Annotation | Comment |
+| ---------- | ------- |
+| `PARAM: ` <br> (NB! space) | The following command line parameters are added to Goblint for this test. |
+| `SKIP` | The test is skipped (except when run with `./scripts/update_suite.rb group`). |
+| `NOMARSHAL` | Marshaling and unmarshaling of results is not tested on this program. |
+
+#### End of line
+Comments at the end of other lines indicate the behavior on that line:
+
+| Annotation | Expected Goblint result | Concrete semantics | Checks |
+| ---------- | ----- | ------------- | --- |
+| `SUCCESS` <br> or nothing | Assertion succeeds | Assertion always succeeds | Precision |
+| `FAIL` | Assertion fails | Assertion always fails | Precision |
+| `UNKNOWN!` | Assertion is unknown | Assertion may both <br> succeed or fail | Soundness |
+| `UNKNOWN` | Assertion is unknown | — | Intended imprecision |
+| `TODO` <br> or `SKIP` | Assertion is unknown <br> or succeeds | Assertion always succeeds | Precision improvement |
+| `NORACE` | No race warning | No data race | Precision |
+| `RACE!` | Race warning | Data race is possible | Soundness |
+| `RACE` | Race warning | — | Intended imprecision |
+| `NODEADLOCK` | No deadlock warning | No deadlock | Precision |
+| `DEADLOCK` | Deadlock warning | Deadlock is possible | Soundness |
+| `NOWARN` | No warning | — | Precision |
+| `WARN` | Some warning | — | Soundness |
+
+#### Other
+Other useful constructs are the following:
+
+| Code with annotation | Comment |
+| -------------------- | ------- |
+| `__goblint_check(1); // reachable` | Checks that the line is reachable according <br> to Goblint results (soundness). |
+| `__goblint_check(0); // NOWARN (unreachable)` | Checks that the line is unreachable (precision). |
 
 ## Cram Tests
 [Cram-style tests](https://dune.readthedocs.io/en/stable/tests.html#cram-tests) are also used to verify that existing functionality hasn't been broken.
@@ -119,3 +154,17 @@ To test a domain, you need to do the following:
 
 1. Implement `arbitrary` (reasonably).
 2. Add the domain to `Maindomaintest`.
+
+## Coverage
+
+The [bisect_ppx](https://github.com/aantron/bisect_ppx) tool is used to produce code coverage reports for Goblint.
+The code coverage reports are available on [Coveralls](https://coveralls.io/github/goblint/analyzer).
+
+To run `bisect_ppx` locally:
+
+1. Install bisect_ppx with `opam install bisect_ppx`.
+2. Run `make coverage` to build Goblint with bisect_ppx instrumentation.
+3. Run tests (this will now generate `.coverage` files in various directories).
+4. Generate coverage report with `bisect-ppx-report html --coverage-path=.`.
+5. After that the generated `.coverage` files can be removed with `find . -type f -name '*.coverage' -delete`.
+6. The HTML report can be found in the `_coverage` folder.

docs/user-guide/inspecting.md

@@ -19,6 +19,7 @@ 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. Run Goblint with these flags: `--enable gobview --set save_run DIR` (`DIR` is the name of the result directory that Goblint will create and populate, if not specified it is `run`)
-3. `cd` into `DIR` and run `python3 -m http.server`
-4. Visit <http://localhost:8000>
+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>

make.sh

@@ -23,6 +23,11 @@ rule() {
       dune build $TARGET.exe &&
       rm -f goblint &&
       cp _build/default/$TARGET.exe goblint
+    ;; coverage)
+      eval $(opam config env)
+      dune build --instrument-with bisect_ppx $TARGET.exe &&
+      rm -f goblint &&
+      cp _build/default/$TARGET.exe goblint
     ;; release)
       eval $(opam config env)
       dune build --profile=release $TARGET.exe &&

scripts/bash-completion.sh

@@ -40,7 +40,9 @@ _update_suite ()
     case $COMP_CWORD in
         1)
             COMPREPLY=($(ls -1 tests/regression/*/*.c | sed -n -r 's|.*/([0-9][0-9])-(.*)\.c|\2|p' | grep "^${COMP_WORDS[1]}"))
-            COMPREPLY+=("group")
+            if [[ "group" =~ ^${COMP_WORDS[1]} ]]; then
+                COMPREPLY+=("group")
+            fi
             ;;
         2)
             if [[ ${COMP_WORDS[1]} == "group" ]] ; then

scripts/hooks/pre-commit

@@ -71,7 +71,7 @@ for f in $(git diff --cached --name-only | grep -E ".*\.mli?$"); do
       lines="$a-$b"
     fi
     echo "ocp-indent file: $f, lines: $lines"
-    [[ $lines -eq "0" ]] || diff $f <(ocp-indent --lines=$lines $f) || fail="true"
+    [[ $lines -eq "0" ]] || diff $f <(ocp-indent --lines=$lines $f | sed 's/^[[:space:]]\+$//') || fail="true"
   done
 done
 if [ "$fail" == "true" ]; then

scripts/test-gobview.py

@@ -7,32 +7,30 @@
 from selenium.webdriver.common.by import By
 from selenium.webdriver.chrome.options import Options
 from threading import Thread
-import http.server
-import socketserver
+import subprocess
 
-PORT = 9000
+PORT = 8080 # has to match port defined in goblint_http.ml
 DIRECTORY = "run"
 IP = "localhost"
 url = 'http://' + IP + ':' + str(PORT) + '/'
 
 # cleanup
-def cleanup(browser, httpd, thread):
+def cleanup(browser, thread):
   print("cleanup")
   browser.close()
-  httpd.shutdown()
-  httpd.server_close()
+  p.kill()
   thread.join()
 
 # serve GobView in different thread so it does not block the testing
-class Handler(http.server.SimpleHTTPRequestHandler):
-    def __init__(self, *args, **kwargs):
-        super().__init__(*args, directory=DIRECTORY, **kwargs)
-class Server(socketserver.TCPServer):
-    allow_reuse_address = True # avoids that during a consecutive run the server cannot connect due to an 'Adress already in use' os error
+def serve():
+  global p
+  goblint_http_path = '_build/default/gobview/goblint-http-server/goblint_http.exe'
+  p = subprocess.Popen(['./' + goblint_http_path,
+                  '-with-goblint', '../analyzer/goblint',
+                  '-goblint', '--set', 'files[+]', '"../analyzer/tests/regression/00-sanity/01-assert.c"'])
 
-httpd = Server((IP, PORT), Handler)
 print("serving at port", PORT)
-thread = Thread(target=httpd.serve_forever, args=())
+thread = Thread(target=serve, args=())
 thread.start()
 
 # installation of browser
@@ -42,6 +40,7 @@ class Server(socketserver.TCPServer):
 browser = webdriver.Chrome(service=Service(ChromeDriverManager().install()),options=options)
 print("finished webdriver installation \n")
 browser.maximize_window()
+browser.implicitly_wait(10);
 
 try:
     # retrieve and wait until page is fully loaded and rendered
@@ -62,8 +61,8 @@ class Server(socketserver.TCPServer):
     panel = browser.find_element(By.CLASS_NAME, "panel")
     print("found DOM elements main, sidebar-left, sidebar-right, content and panel")
 
-    cleanup(browser, httpd, thread)
+    cleanup(browser, thread)
 
 except Exception as e:
-    cleanup(browser, httpd, thread)
+    cleanup(browser, thread)
     raise e

scripts/update_suite.rb

@@ -139,18 +139,16 @@ def report
   end
 
   def collect_warnings
-    warnings[-1] = "term"
     lines = IO.readlines(warnfile, :encoding => "UTF-8")
     lines.each do |l|
-      if l =~ /Function 'main' does not return/ then warnings[-1] = "noterm" end
       if l =~ /vars = (\d*).*evals = (\d+)/ then
         @vars = $1
         @evals = $2
       end
       next unless l =~ /(.*)\(.*?\:(\d+)(?:\:\d+)?(?:-(?:\d+)(?:\:\d+)?)?\)/
       obj,i = $1,$2.to_i
 
-      ranking = ["other", "warn", "race", "norace", "deadlock", "nodeadlock", "success", "fail", "unknown", "term", "noterm"]
+      ranking = ["other", "warn", "race", "norace", "deadlock", "nodeadlock", "success", "fail", "unknown"]
       thiswarn =  case obj
                     when /\(conf\. \d+\)/            then "race"
                     when /Deadlock/                  then "deadlock"
@@ -195,7 +193,7 @@ def compare_warnings
         end
       }
       case type
-      when "deadlock", "race", "fail", "noterm", "unknown", "term", "warn"
+      when "deadlock", "race", "fail", "unknown", "warn"
         check.call warnings[idx] == type
       when "nowarn"
         check.call warnings[idx].nil?
@@ -308,12 +306,6 @@ def parse_tests (lines)
         end
       end
     end
-    case lines[0]
-    when /NON?TERM/
-      tests[-1] = "noterm"
-    when /TERM/
-      tests[-1] = "term"
-    end
     Tests.new(self, tests, tests_line, todo)
   end
 

src/analyses/accessAnalysis.ml

@@ -42,13 +42,15 @@ struct
       + [deref=true], [reach=false] - Access [exp] by dereferencing once (may-point-to), used for lval writes and shallow special accesses.
       + [deref=true], [reach=true] - Access [exp] by dereferencing transitively (reachable), used for deep special accesses. *)
   let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp =
-    if M.tracing then M.traceli "access" "access_one_top %a %b %a:\n" AccessKind.pretty kind reach d_exp exp;
+    if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)\n" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
     if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) then (
-      if deref then
+      if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *)
         do_access ctx kind reach exp;
-      Access.distribute_access_exp (do_access ctx Read false) exp
+      if M.tracing then M.tracei "access" "distribute_access_exp\n";
+      Access.distribute_access_exp (do_access ctx Read false) exp;
+      if M.tracing then M.traceu "access" "distribute_access_exp\n";
     );
-    if M.tracing then M.traceu "access" "access_one_top %a %b %a\n" AccessKind.pretty kind reach d_exp exp
+    if M.tracing then M.traceu "access" "access_one_top\n"
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()