Merge branch 'master' into compilation-database

Author: sim642

.devcontainer/Dockerfile

@@ -11,3 +11,8 @@ RUN rm ~/.gitconfig
 
 # otherwise perl (not ruby!) complains during regression testing
 ENV LC_ALL=C.UTF-8
+
+# update local opam repository because base image may be outdated
+RUN cd /home/opam/opam-repository \
+    && git pull origin master \
+    && opam update

.github/workflows/docker.yml

@@ -1,14 +1,23 @@
 name: docker
 
 on:
-  # not on push or 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
 
+  push:
+    # not on push branch
+    tags:
+      - '**'
+
+  workflow_dispatch:
+    inputs:
+      tag:
+        description: Docker tag
+        required: true
+        default: latest
+
 env:
   REGISTRY: ghcr.io
   IMAGE_NAME: ${{ github.repository }}
@@ -28,6 +37,9 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v2
 
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v1 # needed for GitHub Actions Cache in build-push-action
+
       - name: Log in to the Container registry
         uses: docker/login-action@v1
         with:
@@ -41,18 +53,23 @@ jobs:
         with:
           images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
           tags: |
-            type=raw,value=latest
+            type=schedule
+            type=ref,event=tag
+            type=raw,enable=${{ github.event_name == 'workflow_dispatch' }},value=${{ github.event.inputs.tag }}
 
       - name: Build Docker image
+        id: build
         uses: docker/build-push-action@v2
         with:
           context: .
           load: true # load into docker instead of immediately pushing
           tags: ${{ steps.meta.outputs.tags }}
           labels: ${{ steps.meta.outputs.labels }}
+          cache-from: type=gha
+          cache-to: type=gha,mode=max # max mode caches all layers for multi-stage image
 
       - name: Check Docker image
-        run: docker run --rm -v $(pwd):/data ${{ steps.meta.outputs.tags }} /data/tests/regression/04-mutex/01-simple_rc.c # TODO: breaks if multiple tags?
+        run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags
 
       - name: Push Docker image
         uses: docker/build-push-action@v2

.github/workflows/semgrep.yml

@@ -11,6 +11,8 @@ jobs:
   semgrep:
     runs-on: ubuntu-latest
 
+    continue-on-error: true # TODO: remove when semgrep fixed: https://github.com/returntocorp/semgrep-action/issues/429
+
     steps:
       - name: Checkout code
         uses: actions/checkout@v2
@@ -21,6 +23,8 @@ jobs:
           config: >-
             .semgrep/
           generateSarif: "1"
+        env:
+          SEMGREP_AGENT_DEBUG: 1 # https://github.com/returntocorp/semgrep-action/issues/429
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
         uses: github/codeql-action/upload-sarif@v1

Dockerfile

@@ -9,6 +9,10 @@ WORKDIR /home/opam/analyzer/
 # TODO: use opam depext
 RUN sudo apt-get update \
     && sudo apt-get install -y libgmp-dev libmpfr-dev
+# update local opam repository because base image may be outdated
+RUN cd /home/opam/opam-repository \
+    && git pull origin master \
+    && opam update
 RUN make setup
 # copy the rest
 COPY --chown=opam . /home/opam/analyzer

README.md

@@ -28,7 +28,7 @@ _The [goblint package on opam](https://opam.ocaml.org/packages/goblint/) is very
 
 ### Other
 * **[devcontainer](./.devcontainer/).** Select "Reopen in Container" in VS Code and continue with `make` using Linux instructions in devcontainer.
-* **[Docker (GitHub Container Registry)](https://github.com/goblint/analyzer/pkgs/container/analyzer)**. Run `docker pull ghcr.io/goblint/analyzer:latest`.
+* **[Docker (GitHub Container Registry)](https://github.com/goblint/analyzer/pkgs/container/analyzer)**. Run `docker pull ghcr.io/goblint/analyzer:latest` (or `:nightly`).
 * **Docker (repository).** Clone and run `docker build -t goblint .`.
 * **Vagrant.** Clone and run `vagrant up && vagrant ssh`.
 * **[opam](https://opam.ocaml.org/packages/goblint/)** (very outdated). Run `opam install goblint`.
@@ -47,6 +47,6 @@ To confirm that the Docker container worked, you can try running Goblint as foll
 ```
 docker run -it --rm -v $(pwd):/data goblint /data/tests/regression/04-mutex/01-simple_rc.c
 ```
-If pulled from GitHub Container Registry, use the container name `ghcr.io/goblint/analyzer:latest` instead.
+If pulled from GitHub Container Registry, use the container name `ghcr.io/goblint/analyzer:latest` (or `:nightly`) instead.
 
 For further information, see [documentation](https://goblint.readthedocs.io/en/latest/user-guide/running/).

bench/deriving/dune

@@ -1,5 +1,5 @@
 (executable
  (name benchEq)
- (optional) ; TODO: for some reason this doesn't work: `dune build` still tries to compile if benchmark missing
+ (optional) ; TODO: for some reason this doesn't work: `dune build` still tries to compile if benchmark missing (https://github.com/ocaml/dune/issues/4065)
  (libraries benchmark batteries.unthreaded)
  (preprocess (staged_pps ppx_deriving.std)))

dune-project

@@ -24,8 +24,7 @@
   (depends
     (ocaml (>= 4.09))
     dune
-    zarith_stubs_js ; only needed for js_of_ocaml
-    goblint-cil ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
+    (goblint-cil (>= 1.8.2)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.2.0))
     qcheck-core
     (ppx_distr_guards (>= 0.2))
@@ -36,7 +35,7 @@
     (odoc :with-doc)
     dune-site
     sha
-    benchmark ; TODO: make this optional somehow, (optional) on bench executable doesn't work
+    (benchmark :with-test) ; TODO: make this optional somehow, (optional) on bench executable doesn't work
     ; TODO still need the following after switch to dune?
     ocamlbuild
     ocamlfind

goblint.opam

@@ -21,8 +21,7 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "ocaml" {>= "4.09"}
   "dune" {>= "2.8"}
-  "zarith_stubs_js"
-  "goblint-cil"
+  "goblint-cil" {>= "1.8.2"}
   "batteries" {>= "3.2.0"}
   "qcheck-core"
   "ppx_distr_guards" {>= "0.2"}
@@ -33,7 +32,7 @@ depends: [
   "odoc" {with-doc}
   "dune-site"
   "sha"
-  "benchmark"
+  "benchmark" {with-test}
   "ocamlbuild"
   "ocamlfind"
 ]
@@ -56,7 +55,8 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#c16dddf74f6053a8b3fac07ca2feff18d4d56964" ]
+  # the published goblint-cil 1.8.2 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#c16dddf74f6053a8b3fac07ca2feff18d4d56964" ]
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   [ "ppx_deriving_yojson.3.6.1" "git+https://github.com/ocaml-ppx/ppx_deriving_yojson.git#e030f13a3450e9cf7d2c43fa04e709ef608486cd" ]
   [ "zarith.1.12-gob0" "git+https://github.com/goblint/Zarith.git#goblint-release-1.12" ]

goblint.opam.locked

@@ -24,7 +24,7 @@ depends: [
   "base-threads" {= "base"}
   "base-unix" {= "base"}
   "batteries" {= "3.3.0"}
-  "benchmark" {= "1.6"}
+  "benchmark" {= "1.6" & with-test}
   "biniou" {= "1.2.1"}
   "camlidl" {= "1.09"}
   "conf-gmp" {= "3"}
@@ -35,7 +35,7 @@ depends: [
   "dune-private-libs" {= "2.9.1"}
   "dune-site" {= "2.9.1"}
   "easy-format" {= "1.3.2"}
-  "goblint-cil" {= "1.8.1"}
+  "goblint-cil" {= "1.8.2"}
   "mlgmpidl" {= "1.2.13"}
   "num" {= "1.4"}
   "ocaml" {= "4.12.0"}
@@ -59,7 +59,6 @@ depends: [
   "stdlib-shims" {= "0.3.0"}
   "yojson" {= "1.7.0"}
   "zarith" {= "1.12-gob0"}
-  "zarith_stubs_js" {= "v0.14.0"}
 ]
 build: [
   ["dune" "subst"] {dev}
@@ -79,10 +78,6 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [
-    "goblint-cil.1.8.1"
-    "git+https://github.com/goblint/cil.git#c16dddf74f6053a8b3fac07ca2feff18d4d56964"
-  ]
   [
     "apron.v0.9.13"
     "git+https://github.com/antoinemine/apron.git#c852ebcc89e5cf4a5a3318e7c13c73e1756abb11"

goblint.opam.template

@@ -1,7 +1,8 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#c16dddf74f6053a8b3fac07ca2feff18d4d56964" ]
+  # the published goblint-cil 1.8.2 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#c16dddf74f6053a8b3fac07ca2feff18d4d56964" ]
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   [ "ppx_deriving_yojson.3.6.1" "git+https://github.com/ocaml-ppx/ppx_deriving_yojson.git#e030f13a3450e9cf7d2c43fa04e709ef608486cd" ]
   [ "zarith.1.12-gob0" "git+https://github.com/goblint/Zarith.git#goblint-release-1.12" ]