Merge branch 'main' into no-assume

model-checking · Sep 2, 2023 · be11b58 · be11b58
2 parents aec5fb5 + edd5751
commit be11b58
Show file tree

Hide file tree

Showing 499 changed files with 13,202 additions and 3,823 deletions.
diff --git a/.github/actions/setup/action.yml b/.github/actions/setup/action.yml
@@ -12,6 +12,15 @@ inputs:
 runs:
   using: composite
   steps:
+      - name: Remove unnecessary software to free up disk space
+        if: contains(fromJSON('["ubuntu-20.04","ubuntu-22.04"]'), inputs.os)
+        shell: bash
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+          df -h
+
       - name: Install dependencies
         run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
         shell: bash

diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml
@@ -0,0 +1,89 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Kani Performance Benchmarks
+on:
+  push:
+    tags:
+      - kani-*
+    branches:
+      - 'main'
+  pull_request:
+    types:
+      - labeled
+
+jobs:
+  perf-benchcomp:
+    if: ${{ github.event_name == 'push' 
+      || (github.event_name == 'pull_request' 
+         && github.event.action == 'labeled'
+         && github.event.label.name == 'Z-BenchCI')
+      }}
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Save push event HEAD and HEAD~ to environment variables
+        if: ${{ github.event_name == 'push' }}
+        run: |
+          echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV"
+          echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV"
+
+      - name: Save pull request HEAD and base to environment variables
+        if: ${{ github.event_name == 'pull_request' }}
+        run: |
+          echo "OLD_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
+          echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
+
+      - name: Check out Kani (old variant)
+        uses: actions/checkout@v3
+        with:
+          path: ./old
+          ref: ${{ env.OLD_REF }}
+          fetch-depth: 2
+
+      - name: Check out Kani (new variant)
+        uses: actions/checkout@v3
+        with:
+          path: ./new
+          ref: ${{ env.NEW_REF }}
+          fetch-depth: 1
+
+      - name: Set up Kani Dependencies (old variant)
+        uses: ./old/.github/actions/setup
+        with:
+          os: ubuntu-20.04
+          kani_dir: old
+
+      - name: Set up Kani Dependencies (new variant)
+        uses: ./new/.github/actions/setup
+        with:
+          os: ubuntu-20.04
+          kani_dir: new
+
+      - name: Build Kani (new variant)
+        run: pushd new && cargo build-dev
+
+      - name: Build Kani (old variant)
+        run: pushd old && cargo build-dev
+
+      - name: Copy benchmarks from new to old
+        run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/
+
+      - name: Run benchcomp
+        run: |
+          new/tools/benchcomp/bin/benchcomp \
+            --config new/tools/benchcomp/configs/perf-regression.yaml \
+            run
+          new/tools/benchcomp/bin/benchcomp \
+            --config new/tools/benchcomp/configs/perf-regression.yaml \
+            collate
+
+      - name: Perf Regression Results Table
+        run: |
+          new/tools/benchcomp/bin/benchcomp \
+            --config new/tools/benchcomp/configs/perf-regression.yaml \
+            visualize --only dump_markdown_results_table >> "$GITHUB_STEP_SUMMARY"
+
+      - name: Run other visualizations
+        run: |
+          new/tools/benchcomp/bin/benchcomp \
+            --config new/tools/benchcomp/configs/perf-regression.yaml \
+            visualize --except dump_markdown_results_table
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
@@ -45,12 +45,14 @@ jobs:
           os: ubuntu-20.04
 
       - name: Build Kani
-        run: cargo build-dev
+        run: cargo build-dev -- --features write_json_symtab
+
+      - name: Run tests
+        run: |
+          cargo run -p compiletest --quiet -- --suite kani --mode kani --quiet --no-fail-fast
+          cargo run -p compiletest --quiet -- --suite expected --mode expected --quiet --no-fail-fast
+          cargo run -p compiletest --quiet -- --suite cargo-kani --mode cargo-kani --quiet --no-fail-fast
 
-      - name: Execute Kani regression
-        env:
-          KANI_ENABLE_WRITE_JSON_SYMTAB: 1
-        run: ./scripts/kani-regression.sh
 
   benchcomp-tests:
     runs-on: ubuntu-20.04
@@ -91,6 +93,8 @@ jobs:
 
       - name: Execute Kani performance tests
         run: ./scripts/kani-perf.sh
+        env:
+          RUST_TEST_THREADS: 1
 
   bookrunner:
     runs-on: ubuntu-20.04
@@ -125,14 +129,17 @@ jobs:
       - name: Detect unexpected book runner failures
         run: ./scripts/ci/detect_bookrunner_failures.sh build/output/latest/html/bookrunner.txt
 
+      - name: Install book dependencies
+        run: ./scripts/setup/ubuntu/install_doc_deps.sh
+
       # On one OS only, build the documentation, too.
       - name: Build Documentation
         run: ./scripts/build-docs.sh
 
       # When we're pushed to main branch, only then actually publish the docs.
       - name: Publish Documentation
         if: ${{ github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }}
-        uses: JamesIves/github-pages-deploy-action@v4.3.3
+        uses: JamesIves/github-pages-deploy-action@v4
         with:
           branch: gh-pages
           folder: docs/book/
@@ -184,7 +191,15 @@ jobs:
     runs-on: ubuntu-20.04
     container:
       image: ubuntu:18.04
+      volumes:
+        - /usr/local:/mnt/host-local
     steps:
+      - name: Remove unnecessary software to free up disk space
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          rm -r /mnt/host-local/lib/android /mnt/host-local/.ghcup
+          df -h
       # This is required before checkout because the container does not
       # have Git installed, so cannot run checkout action. The checkout
       # action requires Git >=2.18, so use the Git maintainers' PPA.
@@ -249,61 +264,3 @@ jobs:
           if-no-files-found: error
           # Aggressively short retention: we don't really need these
           retention-days: 3
-
-  perf-benchcomp:
-    runs-on: ubuntu-20.04
-    steps:
-      - name: Save push event HEAD and HEAD~ to environment variables
-        if: ${{ github.event_name == 'push' }}
-        run: |
-          echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV"
-          # We want to compare with $NEW_REF~. But we can't know what
-          # that ref actually is until we clone the repository, so for
-          # now make it equal to $NEW_REF
-          echo "OLD_REF=${{ github.event.after }}" | tee -a "$GITHUB_ENV"
-
-      - name: Save pull request HEAD and target to environment variables
-        if: ${{ github.event_name == 'pull_request' }}
-        run: |
-          echo "OLD_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
-          echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
-
-      - name: Check out Kani (old variant)
-        uses: actions/checkout@v3
-        with:
-          path: ./old
-          ref: ${{ env.OLD_REF }}
-          fetch-depth: 2
-
-      - name: Check out HEAD~ of push event as 'old' variant
-        if: ${{ github.event_name == 'push' }}
-        run: pushd old && git checkout "${NEW_REF}^"
-
-      - name: Check out Kani (new variant)
-        uses: actions/checkout@v3
-        with:
-          path: ./new
-          ref: ${{ env.NEW_REF }}
-
-      - name: Set up Kani Dependencies (old variant)
-        uses: ./old/.github/actions/setup
-        with:
-          os: ubuntu-20.04
-          kani_dir: old
-
-      - name: Set up Kani Dependencies (new variant)
-        uses: ./new/.github/actions/setup
-        with:
-          os: ubuntu-20.04
-          kani_dir: new
-
-      - name: Build Kani (new variant)
-        run: pushd new && cargo build-dev
-
-      - name: Build Kani (old variant)
-        run: pushd old && cargo build-dev
-
-      - name: Run benchcomp
-        run: |
-          new/tools/benchcomp/bin/benchcomp \
-            --config new/tools/benchcomp/configs/perf-regression.yaml
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -84,9 +84,17 @@ jobs:
     runs-on: ubuntu-20.04
     container:
       image: ubuntu:18.04
+      volumes:
+        - /usr/local:/mnt/host-local
     permissions:
       contents: write
     steps:
+      - name: Remove unnecessary software to free up disk space
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          rm -r /mnt/host-local/lib/android /mnt/host-local/.ghcup
+          df -h
       # This is required before checkout because the container does not
       # have Git installed, so cannot run checkout action. The checkout
       # action requires Git >=2.18, so use the Git maintainers' PPA.

diff --git a/.gitignore b/.gitignore
@@ -81,5 +81,6 @@ tests/rustdoc-gui/src/**.lock
 tests/kani-dependency-test/diamond-dependency/build
 tests/kani-multicrate/type-mismatch/mismatch/target
 /docs/book
+/docs/gen_src
 /docs/mdbook*
 /kani-*.tar.gz