Merge branch 'master' into convey_retreat_venice_topsecret

Author: michael-schwarz

.devcontainer/Dockerfile

@@ -1,9 +1,9 @@
 # just -opam tag because make setup will install ocaml compiler
-FROM ocaml/opam:ubuntu-21.04-opam AS dev
+FROM ocaml/opam:ubuntu-22.04-opam AS dev
 
 # TODO: use opam depext
 RUN sudo apt-get update \
-    && sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf pkg-config ruby gem curl
+    && sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf gcc-multilib pkg-config ruby gem curl
 
 # remove default Docker <docker@example.com> git credentials added by opam base image: https://github.com/avsm/ocaml-dockerfile/blob/f184554282a3836bf3f1c34d20e77d0530f8349d/src-opam/dockerfile_linux.ml#L24-L28
 # this prevents devcontainer from using outside git credentials: https://code.visualstudio.com/docs/remote/containers#_sharing-git-credentials-with-your-container

.git-blame-ignore-revs

@@ -28,3 +28,21 @@ ec8611a3a72ae0d95ec82ffee16c5c4785111aa1
 
 # Set up end-of-line normalization.
 78fd79e7f4d15c4412221b155971fac2e0616b90
+
+# fix indentation in baseInvariant
+f3ffd5e45c034574020f56519ccdb021da2a1479
+
+# Fix indentation in various non-legacy code
+c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9
+
+# Fix LibraryFunctions.invalidate_actions indentation
+5662024232f32fe74dd25c9317dee4436ecb212d
+
+# Rename ctx -> man
+0c155e68607fede6fab17704a9a7aee38df5408e
+
+# Trim trailing whitespace in BitfieldDomain
+d4e2a5f84ed3b7fbff89e34b2f7833de975e0671
+
+# Fix BaseInvariant indentation
+15e7a7ebd34e9fabdd4129e97eb86830fea8395f

.gitattributes

@@ -0,0 +1,13 @@
+# GitHub repository language overrides
+# https://github.com/github-linguist/linguist/blob/main/docs/overrides.md
+
+# currently only dune-project is classified: https://github.com/github-linguist/linguist/pull/7126
+dune linguist-language=dune
+dune.inc linguist-language=dune
+
+# avoid misclassification as Standard ML
+*.ml linguist-language=ocaml
+*.mli linguist-language=ocaml
+
+# cram tests are classified as Raku/Terra/Turing, cram isn't separate language so consider them also dune
+*.t linguist-language=dune

.github/workflows/coverage.yml

@@ -0,0 +1,73 @@
+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-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+        ocaml-compiler:
+          - ocaml-variants.4.14.2+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@v5
+
+      - 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@v3
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
+        if: ${{ matrix.os == 'ubuntu-22.04' }}
+        run: sudo apt install -y libgraph-easy-perl
+
+      - name: Install dependencies
+        run: opam install . --deps-only --locked --with-test
+
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
+      - name: Install coverage dependencies
+        run: opam install bisect_ppx
+
+      - name: Build
+        run: ./make.sh coverage
+
+      - name: Download Linux headers
+        run: ./make.sh headers
+
+      - name: Test
+        run: opam exec -- dune runtest --instrument-with bisect_ppx
+
+      - run: opam exec -- bisect-ppx-report send-to Coveralls
+        env:
+          COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
+          PULL_REQUEST_NUMBER: ${{ github.event.number }}
+
+      - uses: actions/upload-artifact@v5
+        if: always()
+        with:
+          name: suite_result
+          path: tests/suite_result/

.github/workflows/docker.yml

@@ -35,21 +35,21 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v5
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v1 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
 
       - name: Log in to the Container registry
-        uses: docker/login-action@v1
+        uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
 
       - name: Extract metadata (tags, labels) for Docker
         id: meta
-        uses: docker/metadata-action@v3
+        uses: docker/metadata-action@v5
         with:
           images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
           tags: |
@@ -59,7 +59,7 @@ jobs:
 
       - name: Build Docker image
         id: build
-        uses: docker/build-push-action@v2
+        uses: docker/build-push-action@v6
         with:
           context: .
           load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
         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
+        uses: docker/build-push-action@v6
         with:
           context: .
           push: true

.github/workflows/docs.yml

@@ -0,0 +1,70 @@
+name: docs
+
+on:
+  push:
+  pull_request:
+
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  api-build:
+    strategy:
+      matrix:
+        os:
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+        ocaml-compiler:
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # 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@v5
+
+      - name: Check for undocumented modules
+        run: python scripts/goblint-lib-modules.py
+
+      - 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@v3
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Setup Pages
+        id: pages
+        uses: actions/configure-pages@v5
+
+      - name: Install dependencies
+        run: opam install . --deps-only --locked --with-doc
+
+      - name: Build API docs
+        run: opam exec -- dune build @doc
+
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@v4
+        with:
+          path: _build/default/_doc/_html/
+
+  api-deploy:
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: api-build
+    if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
+    concurrency:
+      group: "pages"
+      cancel-in-progress: true
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4

.github/workflows/indentation.yml

@@ -1,43 +1,33 @@
 name: indentation
 
-on: [ push, pull_request]
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
 
 jobs:
   indentation:
-    strategy: # remove?
+    strategy:
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
         ocaml-compiler:
-          - 4.14.0 # setup-ocaml@v1 does not support 4.14.x for ocaml-version
+          - 4.14.x
 
     runs-on: ${{ matrix.os }}
 
-    if: ${{ github.event.before != '0000000000000000000000000000000000000000' }}
+    if: ${{ !github.event.forced && github.event.before != '0000000000000000000000000000000000000000' }}
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v5
         with:
           fetch-depth: 0
 
-      # reuse tests.yml or depend on it to not have to setup OCaml? https://docs.github.com/en/actions/reference/workflow-syntax-for-github-actions#example-using-an-action-in-the-same-repository-as-the-workflow
-
-      # rely on cache for now
-      - name: Cache opam switch # https://github.com/marketplace/actions/cache
-        uses: actions/cache@v3
-        with:
-          # A list of files, directories, and wildcard patterns to cache and restore
-          path: |
-            ~/.opam
-            _opam
-          # Key for restoring and saving the cache
-          key: opam-ocp-indent-${{ runner.os }}-${{ matrix.ocaml-compiler }}
-
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v1 # intentionally use v1 instead of v2 because it's faster with manual caching: https://github.com/goblint/analyzer/pull/308#issuecomment-887805857
+        uses: ocaml/setup-ocaml@v3
         with:
-          ocaml-version: ${{ matrix.ocaml-compiler }}
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Install ocp-indent
         run: opam install -y ocp-indent