Merge branch 'master' into region-escape

goblint · Nov 17, 2023 · d26f8fb · d26f8fb
2 parents f020dde + 03e17b6
commit d26f8fb
Show file tree

Hide file tree

Showing 989 changed files with 38,108 additions and 8,266 deletions.
diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
@@ -28,3 +28,6 @@ ec8611a3a72ae0d95ec82ffee16c5c4785111aa1
 
 # Set up end-of-line normalization.
 78fd79e7f4d15c4412221b155971fac2e0616b90
+
+# fix indentation in baseInvariant
+f3ffd5e45c034574020f56519ccdb021da2a1479
diff --git a/.github/workflows/coverage.yml b/.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@v4
+
+      - 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/
diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
@@ -35,21 +35,21 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2 # 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@v2
+        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@v4
+        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@v4
+        uses: docker/build-push-action@v5
         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@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           push: true

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -0,0 +1,71 @@
+name: docs
+
+on:
+  push:
+    branches:
+      - master
+
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: true
+
+jobs:
+  api-build:
+    strategy:
+      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 }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - 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@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Setup Pages
+        id: pages
+        uses: actions/configure-pages@v3
+
+      - 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@v2
+        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
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v2
diff --git a/.github/workflows/indentation.yml b/.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
         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@v4
         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@v2
         with:
-          ocaml-version: ${{ matrix.ocaml-compiler }}
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Install ocp-indent
         run: opam install -y ocp-indent

diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
@@ -25,9 +25,12 @@ jobs:
 
     runs-on: ${{ matrix.os }}
 
+    env:
+      OCAMLRUNPARAM: b
+
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -64,6 +67,9 @@ jobs:
       - 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
 
@@ -73,6 +79,12 @@ jobs:
       - name: Test incremental regression with cfg comparison
         run: ruby scripts/update_suite.rb -c
 
+      - uses: actions/upload-artifact@v3
+        if: always()
+        with:
+          name: suite_result
+          path: tests/suite_result/
+
   extraction:
     if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
 
@@ -89,7 +101,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -129,7 +141,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -141,7 +153,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 
@@ -156,3 +168,10 @@ jobs:
 
       - name: Build Gobview
         run: opam exec -- dune build gobview
+
+      - name: Install selenium
+        run: pip3 install selenium webdriver-manager
+
+      - name: Test Gobview
+        run: |
+          python3 scripts/test-gobview.py
diff --git a/.github/workflows/metadata.yml b/.github/workflows/metadata.yml
@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Validate CITATION.cff
         uses: docker://citationcff/cffconvert:latest
@@ -36,10 +36,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 

diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
@@ -15,21 +15,21 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 
       - name: Install ajv-cli
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/util/options.schema.json
+        run: ajv migrate -s src/common/util/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/util/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/util/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"