Merge branch 'main' into kanicov-tool

.github/workflows/audit.yml

@@ -7,6 +7,7 @@
 name: Cargo Audit
 on:
   pull_request:
+  merge_group:
   push:
     # Run on changes to branches but not tags.
     branches:

.github/workflows/bench.yml

@@ -55,12 +55,6 @@ jobs:
           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/
 

.github/workflows/cbmc-latest.yml

@@ -32,24 +32,30 @@ jobs:
           os: ${{ matrix.os }}
           kani_dir: 'kani'
 
-      - name: Build Kani
-        working-directory: ./kani
-        run: cargo build-dev
-
       - name: Checkout CBMC under "cbmc"
         uses: actions/checkout@v4
         with:
           repository: diffblue/cbmc
           path: cbmc
 
-      - name: Build CBMC
+      - name: Build CBMC (Linux)
+        if: ${{ startsWith(matrix.os, 'ubuntu') }}
         working-directory: ./cbmc
         run: |
           cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
           cmake --build build -- -j 4
           # Prepend the bin directory to $PATH
           echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
 
+      - name: Build CBMC (macOS)
+        if: ${{ startsWith(matrix.os, 'macos') }}
+        working-directory: ./cbmc
+        run: |
+          cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" -DCMAKE_CXX_COMPILER=$(which clang++)
+          cmake --build build -- -j 4
+          # Prepend the bin directory to $PATH
+          echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
+
       - name: Execute Kani regressions
         working-directory: ./kani
         run: ./scripts/kani-regression.sh

.github/workflows/cbmc-update.yml

@@ -30,7 +30,7 @@ jobs:
         env:
           GH_TOKEN: ${{ github.token }}
         run: |
-          grep ^CBMC_VERSION kani-dependencies >> $GITHUB_ENV
+          grep ^CBMC_VERSION kani-dependencies | sed 's/"//g' >> $GITHUB_ENV
           CBMC_LATEST=$(gh -R diffblue/cbmc release list | grep Latest | awk '{print $1}' | cut -f2 -d-)
           echo "CBMC_LATEST=$CBMC_LATEST" >> $GITHUB_ENV
           # check whether the version has changed at all
@@ -47,8 +47,8 @@ jobs:
           elif ! git ls-remote --exit-code origin cbmc-$CBMC_LATEST ; then
             CBMC_LATEST_MAJOR=$(echo $CBMC_LATEST | cut -f1 -d.)
             CBMC_LATEST_MINOR=$(echo $CBMC_LATEST | cut -f2 -d.)
-            sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_MAJOR\"/" kani-dependencies
-            sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_MINOR\"/" kani-dependencies
+            sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_LATEST_MAJOR\"/" kani-dependencies
+            sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_LATEST_MINOR\"/" kani-dependencies
             sed -i "s/^CBMC_VERSION=.*/CBMC_VERSION=\"$CBMC_LATEST\"/" kani-dependencies
             git diff
             if ! ./scripts/kani-regression.sh ; then
@@ -79,7 +79,7 @@ jobs:
           token: ${{ github.token }}
           title: 'CBMC upgrade to ${{ env.CBMC_LATEST }} failed'
           body: >
-            Updating CBMC from ${{ evn.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed.
+            Updating CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed.
 
             The failed automated run
             [can be found here.](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }})

.github/workflows/extra_jobs.yml

@@ -18,7 +18,9 @@
 # See <https://github.com/actions/labeler/issues/121> for more details.
 
 name: Kani Extra
-on: pull_request_target
+on:
+  pull_request_target:
+  merge_group:
 
 jobs:
   # Keep this job minimal since it requires extra permission
@@ -45,5 +47,5 @@ jobs:
     name: Verification Benchmarks
     needs: auto-label
     permissions: {}
-    if: contains(needs.auto-label.outputs.all-labels, 'Z-BenchCI')
+    if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-BenchCI') && github.event_name != 'merge_group' }}
     uses: ./.github/workflows/bench.yml

.github/workflows/format-check.yml

@@ -3,6 +3,7 @@
 name: Kani Format Check
 on:
   pull_request:
+  merge_group:
   push:
     # Not just any push, as that includes tags.
     # We don't want to re-trigger this workflow when tagging an existing commit.

.github/workflows/kani.yml

@@ -3,6 +3,7 @@
 name: Kani CI
 on:
   pull_request:
+  merge_group:
   push:
     # Not just any push, as that includes tags.
     # We don't want to re-trigger this workflow when tagging an existing commit.
@@ -17,7 +18,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04, macos-14]
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4
@@ -27,9 +28,6 @@ jobs:
         with:
           os: ${{ matrix.os }}
 
-      - name: Build Kani
-        run: cargo build-dev
-
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
@@ -88,47 +86,19 @@ jobs:
         with:
           os: ubuntu-20.04
 
-      - name: Build Kani using release mode
-        run: cargo build-dev -- --release
-
       - name: Execute Kani performance tests
         run: ./scripts/kani-perf.sh
         env:
           RUST_TEST_THREADS: 1
 
-  bookrunner:
+  documentation:
     runs-on: ubuntu-20.04
     permissions:
       contents: write
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4
 
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-20.04
-
-      - name: Build Kani
-        run: cargo build-dev
-
-      - name: Install book runner dependencies
-        run: ./scripts/setup/install_bookrunner_deps.sh
-
-      - name: Generate book runner report
-        run: cargo run -p bookrunner
-        env:
-          DOC_RUST_LANG_ORG_CHANNEL: nightly
-
-      - name: Print book runner text results
-        run: cat build/output/latest/html/bookrunner.txt
-
-      - name: Print book runner failures grouped by stage
-        run: python3 scripts/ci/bookrunner_failures_by_stage.py build/output/latest/html/index.html
-
-      - 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
 

.github/workflows/release.yml

@@ -8,6 +8,7 @@
 name: Release Bundle
 on:
   pull_request:
+  merge_group:
   push:
     branches:
       - 'main'
@@ -16,6 +17,7 @@ on:
 
 env:
   RUST_BACKTRACE: 1
+  ACTIONS_ALLOW_USE_UNSECURE_NODE_VERSION: true
 
 jobs:
   build_bundle_macos:
@@ -44,6 +46,32 @@ jobs:
           os: macos-13
           arch: x86_64-apple-darwin
 
+  build_bundle_macos_aarch64:
+    name: BuildBundle-MacOs-ARM
+    runs-on: macos-14
+    permissions:
+      contents: write
+    outputs:
+      version: ${{ steps.bundle.outputs.version }}
+      bundle: ${{ steps.bundle.outputs.bundle }}
+      package: ${{ steps.bundle.outputs.package }}
+      crate_version: ${{ steps.bundle.outputs.crate_version }}
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: macos-14
+
+      - name: Build bundle
+        id: bundle
+        uses: ./.github/actions/build-bundle
+        with:
+          os: macos-14
+          arch: aarch64-apple-darwin
+
   build_bundle_linux:
     name: BuildBundle-Linux
     runs-on: ubuntu-20.04
@@ -77,12 +105,16 @@ jobs:
           apt-get install -y software-properties-common apt-utils
           add-apt-repository ppa:git-core/ppa
           add-apt-repository ppa:deadsnakes/ppa
+          add-apt-repository ppa:ubuntu-toolchain-r/test
           apt-get update
           apt-get install -y \
-            build-essential bash-completion curl lsb-release sudo g++ gcc flex \
+            build-essential bash-completion curl lsb-release sudo g++-9 gcc-9 flex \
             bison make patch git python3.7 python3.7-dev python3.7-distutils
+          update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-9 110 \
+            --slave /usr/bin/g++ g++ /usr/bin/g++-9
+          ln -sf cpp-9 /usr/bin/cpp
           update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1
-          curl -s https://bootstrap.pypa.io/get-pip.py -o get-pip.py
+          curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py
           python3 get-pip.py --force-reinstall
           rm get-pip.py
 
@@ -136,7 +168,7 @@ jobs:
       - name: Get toolchain version used to setup kani
         run: |
           tar zxvf ${{ matrix.prev_job.bundle }}
-          DATE=$(cat ./kani-latest/rust-toolchain-version | cut -d'-' -f2,3,4)
+          DATE=$(cat ./kani-${{ matrix.prev_job.version }}/rust-toolchain-version | cut -d'-' -f2,3,4)
           echo "Nightly date: $DATE"
           echo "DATE=$DATE" >> $GITHUB_ENV
 
@@ -180,7 +212,7 @@ jobs:
 
       - name: Run cargo-kani tests after moving
         run: |
-          for dir in function multiple-harnesses verbose; do
+          for dir in supported-lib-types/rlib multiple-harnesses verbose; do
             >&2 echo "Running test $dir"
             pushd ${{ github.workspace }}/../post-setup-tests/cargo-ui/$dir
             cargo kani
@@ -296,7 +328,7 @@ jobs:
     if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }}
     name: Release
     runs-on: ubuntu-20.04
-    needs: [build_bundle_macos, build_bundle_linux, test_bundle, test_alt_platform]
+    needs: [build_bundle_macos, build_bundle_macos_aarch64, build_bundle_linux, test_bundle, test_alt_platform]
     permissions:
       contents: write
     outputs:
@@ -328,6 +360,11 @@ jobs:
         with:
           name: ${{ needs.build_bundle_macos.outputs.bundle }}
 
+      - name: Download MacOS ARM bundle
+        uses: actions/download-artifact@v3
+        with:
+          name: ${{ needs.build_bundle_macos_aarch64.outputs.bundle }}
+
       - name: Download Linux bundle
         uses: actions/download-artifact@v3
         with:
@@ -341,7 +378,7 @@ jobs:
         with:
           name: kani-${{ env.TAG_VERSION }}
           tag: kani-${{ env.TAG_VERSION }}
-          artifacts: "${{ needs.build_bundle_linux.outputs.bundle }},${{ needs.build_bundle_macos.outputs.bundle }}"
+          artifacts: "${{ needs.build_bundle_linux.outputs.bundle }},${{ needs.build_bundle_macos.outputs.bundle }},${{ needs.build_bundle_macos_aarch64.outputs.bundle }}"
           body: |
             Kani Rust verifier release bundle version ${{ env.TAG_VERSION }}.
           draft: true
@@ -384,7 +421,7 @@ jobs:
           OWNER: '${{ github.repository_owner }}'
 
       - name: Build and push
-        uses: docker/build-push-action@v5
+        uses: docker/build-push-action@v6
         with:
           context: .
           file: scripts/ci/Dockerfile.bundle-release-20-04