Merge branch 'main' into sqrt-intrinsics

.github/dependabot.yml

@@ -9,3 +9,10 @@ updates:
     directory: "/"
     schedule:
       interval: "weekly"
+
+  - package-ecosystem: "gitsubmodule"
+    directory: "/"
+    allow:
+      - dependency-name: "tests/perf/s2n-quic"
+    schedule:
+      interval: "weekly"

.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/kani.yml

@@ -17,7 +17,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 +27,6 @@ jobs:
         with:
           os: ${{ matrix.os }}
 
-      - name: Build Kani
-        run: cargo build-dev
-
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
@@ -88,47 +85,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