Merge branch 'master' into arm64

.git-blame-ignore-revs

@@ -22,3 +22,9 @@ dd220cf089efd7dfb022e6dbc9a00749a5f72cb2
 
 # Reorder so correct query function is used
 78eb0601b5f680d8789366b725cfc6df48137a31
+
+# Fix recent indentation problems in messages, JSON, Z3
+ec8611a3a72ae0d95ec82ffee16c5c4785111aa1
+
+# Set up end-of-line normalization.
+78fd79e7f4d15c4412221b155971fac2e0616b90

.github/workflows/indentation.yml

@@ -13,6 +13,8 @@ jobs:
 
     runs-on: ${{ matrix.os }}
 
+    if: ${{ github.event.before != '0000000000000000000000000000000000000000' }}
+
     steps:
       - name: Checkout code
         uses: actions/checkout@v2

.github/workflows/locked.yml

@@ -0,0 +1,50 @@
+name: locked
+
+on:
+  push:
+  pull_request:
+
+jobs:
+  regression:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-latest
+          - macos-latest
+        ocaml-compiler:
+          - 4.12.0 # matches opam lock file
+          # don't add any other because they won't be used
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v2
+
+      - 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
+
+      - name: Build
+        run: ./make.sh nat
+
+      - 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
+
+      - name: Build domaintest
+        run: ./make.sh domaintest
+
+      - name: Test domains
+        run: ./goblint.domaintest

.github/workflows/semgrep.yml

@@ -0,0 +1,26 @@
+name: semgrep
+
+on:
+  push:
+  pull_request:
+
+jobs:
+  semgrep:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v2
+
+      - name: Run semgrep
+        uses: returntocorp/semgrep-action@v1
+        with:
+          config: >-
+            .semgrep/
+          generateSarif: "1"
+
+      - name: Upload SARIF file to GitHub Advanced Security Dashboard
+        uses: github/codeql-action/upload-sarif@v1
+        with:
+          sarif_file: semgrep.sarif
+        if: always()

.github/workflows/unlocked.yml

@@ -0,0 +1,69 @@
+name: unlocked
+
+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:
+  regression:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-latest
+          - macos-latest
+        ocaml-compiler:
+          # - 4.13.x # TODO: re-enable when Batteries gets support: https://github.com/ocaml-batteries-team/batteries-included/issues/1045
+          - 4.12.x
+          - 4.09.x
+        apron:
+          - false
+          - true
+
+    # 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
+    name: regression (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}${{ matrix.apron && ', apron' || '' }})
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v2
+
+      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Install dependencies
+        run: opam install . --deps-only
+
+      - name: Install Apron dependencies
+        if: ${{ matrix.apron }}
+        run: |
+          opam depext apron
+          opam install apron
+
+      - name: Build
+        run: ./make.sh nat
+
+      - 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!)
+        if: ${{ matrix.apron }}
+        run: ruby scripts/update_suite.rb group apron -s
+
+      - name: Build domaintest
+        run: ./make.sh domaintest
+
+      - name: Test domains
+        run: ./goblint.domaintest # could be made long
+
+      - name: Test marshal regression
+        run: ruby scripts/update_suite.rb -m

.gitignore

@@ -53,6 +53,7 @@ goblint.bc.js
 
 # Files generated by merge tools after conflicts
 *.orig
+*.rej
 
 sv-comp/goblint.zip
 
@@ -64,3 +65,9 @@ runtime/*
 
 # perf
 perf.data*
+
+# incremental analysis
+incremental_data/
+
+# test-incremental.sh
+*.log

.mailmap

@@ -0,0 +1,27 @@
+# git shortlog -nse
+
+Martin Schwarz <[email protected]>
+Martin Schwarz <[email protected]> <schwarz@dellseidl5.(none)>
+Alexander Herz <[email protected]> <[email protected]>
+Vootele Rõtov <[email protected]>
+
+Stefan Marcik <[email protected]>
+Stefan Marcik <[email protected]> <stefan@stefan-vmware-work.(none)>
+Stefan Marcik <[email protected]> <stefan@hiwi-vm.(none)>
+Stefan Marcik <[email protected]> <stefan@Stefan-Work-VM.(none)>
+Stefan Marcik <[email protected]> <stefan@stefan-work-vm64.(none)>
+Stefan Marcik <[email protected]> <stefan@stefan-ubuntu.(none)>
+
+<[email protected]> <[email protected]>
+<[email protected]> <kalmera@dellseidl1.(none)>
+Ralf Vogler <[email protected]>
+<[email protected]> <[email protected]>
+<[email protected]> <[email protected]>
+
+Ivana Zuzic <[email protected]> <[email protected]>
+Kerem Çakırer <[email protected]> <[email protected]>
+
+Elias Brandstetter <[email protected]> <[email protected]>
+wherekonshade <[email protected]> <[email protected]>
+Martin Wehking <[email protected]>
+Edin Citaku <[email protected]>

.semgrep/cil.yml

@@ -0,0 +1,14 @@
+rules:
+  - id: cilfacade
+    pattern-either:
+      - pattern: Cil.typeOf
+      - pattern: Cil.typeOfLval
+      - pattern: Cil.typeOfInit
+      - pattern: Cil.typeOffset
+      - pattern: Cil.get_stmtLoc
+    paths:
+      exclude:
+        - cilfacade.ml
+    message: use Cilfacade instead
+    languages: [ocaml]
+    severity: WARNING

.semgrep/hashtbl.yml

@@ -0,0 +1,15 @@
+rules:
+  - id: hashtbl-iter-modify
+    patterns:
+      - pattern-either:
+        - pattern: $HM.clear $H
+        - pattern: $HM.reset $H
+        - pattern: $HM.add $H $K $V
+        - pattern: $HM.remove $H $K
+        - pattern: $HM.replace $H $K $V
+      - pattern-either:
+        - pattern-inside: $HM.iter ... $H
+        - pattern-inside: $HM.fold ... $H
+    message: modifying Hashtbl during iteration is undefined behavior
+    languages: [ocaml]
+    severity: ERROR

.semgrep/tracing.yml

@@ -0,0 +1,14 @@
+rules:
+  - id: trace-not-in-tracing
+    patterns:
+      - pattern-either:
+        - pattern: Messages.trace
+        - pattern: Messages.tracel
+        - pattern: Messages.tracei
+        - pattern: Messages.tracec
+        - pattern: Messages.traceu
+        - pattern: Messages.traceli
+      - pattern-not-inside: if Messages.tracing then ...
+    message: trace functions should only be called if tracing is enabled at compile time
+    languages: [ocaml]
+    severity: WARNING

README.md

@@ -1,43 +1,41 @@
-# goblint
-![Build status](https://github.com/goblint/analyzer/workflows/build%20and%20run%20tests/badge.svg)
-[![Docker Build Status](https://img.shields.io/docker/cloud/build/voglerr/goblint)](https://hub.docker.com/r/voglerr/goblint)
+# Goblint
+[![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)
 [![Documentation Status](https://readthedocs.org/projects/goblint/badge/?version=latest)](https://goblint.readthedocs.io/en/latest/?badge=latest)
+[![Docker Build Status](https://img.shields.io/docker/cloud/build/voglerr/goblint)](https://hub.docker.com/r/voglerr/goblint)
 
 Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/en/latest/) or [GitHub](./docs/).
 
-## Setup
-### Linux / MacOS
-**For an up-to-date-version, clone this repository, use `make setup` to install OCaml and all dependencies, and `make` to build.**
-
-Alternatively: Install [opam](http://opam.ocaml.org/doc/Install.html), and then do `opam install goblint`. Warning: The OPAM package is updated infrequently.
+## Installing
+Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository.
 
-Run goblint: `./goblint tests/regression/04-mutex/01-simple_rc.c`.
+_The [goblint package on opam](https://opam.ocaml.org/packages/goblint/) is very outdated and should currently not be used._
 
-If something goes wrong, take a look at [travis-ci.sh](scripts/travis-ci.sh) for an example Ubuntu/macOS setup.
+### Linux
+1. Install [opam](https://opam.ocaml.org/doc/Install.html).
+2. Make sure the following are installed: `git patch m4 autoconf libgmp-dev libmpfr-dev`.
+3. Run `make setup` to install OCaml and dependencies via opam.
+4. Run `make` to build Goblint itself.
 
-### macOS
-Goblint relies on GNU `cpp` to preprocess source files - the default clang `cpp` on macOS will not work.
-You can install it with `brew install gcc` (first do `xcode-select --install` if you don't want to build from source). You can check src/config.ml to see what command is used to call `cpp`.
+### MacOS
+1. Install GCC with `brew install gcc` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work.
+2. Continue using Linux instructions.
 
 ### Windows
-For Windows, we recommend using [WSL](https://docs.microsoft.com/de-de/windows/wsl/install-win10).
-
-### Docker / Virtual machine
-You can run Goblint in a [Docker container](https://hub.docker.com/r/voglerr/goblint/) using: `docker run -it voglerr/goblint ./goblint --help`.
-
-A virtual machine containing Goblint can be set up using [Vagrant](http://www.vagrantup.com/): `vagrant up && vagrant ssh`.
+1. Install [WSL](https://docs.microsoft.com/en-us/windows/wsl/install-win10).
+2. Continue using Linux instructions in WSL.
 
-### Web frontend
-The analysis results are printed to stdout by default.
-Adding `--html` saves the results as XML, which is then transformed to be viewable in a web browser.
-Use `make jar` to build the needed Java program.
+### Other
+* **Docker.** Clone and run `make docker`.
+* **Vagrant.** Clone and run `vagrant up && vagrant ssh`.
+* **[Docker Hub](https://hub.docker.com/r/voglerr/goblint)** (outdated). Run `docker run -it voglerr/goblint bash`.
+* **[opam](https://opam.ocaml.org/packages/goblint/)** (very outdated). Run `opam install goblint`.
 
-    ./goblint --html path/to/file.c
 
-Open `result/index.xml` in a browser of your choice.
-Depending on the browser security settings, it might be necessary to serve the result directory from a webserver to access it.
-This can be done by e.g. running `python3 -m http.server` in the `result` directory. The results should then be accessible at `http://localhost:8000`
+## Running
+To confirm that the installation worked, you can try running Goblint as follows:
+```
+./goblint tests/regression/04-mutex/01-simple_rc.c
+```
 
-<!-- ### Web frontend -->
-<!-- Use `make npm` to setup the web frontend and start serving on <http://localhost:3000>. -->
-<!-- See its [README](https://github.com/vogler/goblint-webapp) for details. -->
+For further information, see [documentation](https://goblint.readthedocs.io/en/latest/user-guide/running/).