Merge remote-tracking branch 'origin/main' into issue-2113-toolchain

Conflicts:
    - kani-compiler/src/kani_middle/stubbing/annotations.rs
    - kani-compiler/src/session.rs (logger initialization issue)

Author: celinval

.cargo/config.toml

@@ -4,7 +4,7 @@
 # Command aliases
 [alias]
 # Build kani with development configuration.
-build-dev = "run -p build-kani -- build-dev"
+build-dev = "run --target-dir target/tools -p build-kani -- build-dev"
 # Build kani release bundle.
 bundle = "run -p build-kani -- bundle"
 

.github/actions/setup/action.yml

@@ -5,22 +5,22 @@ inputs:
   os:
     description: In which Operating System is this running
     required: true
-  install_cbmc:
-    description: Whether to install CBMC
+  kani_dir:
+    description: Path to Kani's root directory
     required: false
-    default: 'true'
+    default: '.'
 runs:
   using: composite
   steps:
       - name: Install dependencies
-        run: ./scripts/setup/${{ inputs.os }}/install_deps.sh
+        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
         shell: bash
 
       - name: Install Rust toolchain
-        run: ./scripts/setup/install_rustup.sh
+        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/install_rustup.sh
         shell: bash
 
       - name: Update submodules
         run: |
-          git submodule update --init --depth 1
+          cd ${{ inputs.kani_dir }} && git submodule update --init --depth 1
         shell: bash

.github/workflows/cbmc-latest.yml

@@ -21,67 +21,71 @@ jobs:
       matrix:
         os: [macos-11, ubuntu-18.04, ubuntu-20.04, ubuntu-22.04]
     steps:
-      - name: Checkout CBMC under "cbmc"
+      - name: Checkout Kani under "kani"
         uses: actions/checkout@v3
         with:
-          repository: diffblue/cbmc
-          path: cbmc
-
-      - name: Build CBMC
-        run: |
-          cd cbmc
-          cmake -S . -Bbuild -DWITH_JBMC=OFF
-          cmake --build build -- -j 4
-          sudo cmake --build build --target install
-          # Cleanup cbmc directory
-          cd ..
-          rm -rf cbmc
-
-      - name: Checkout Kani
-        uses: actions/checkout@v3
+          path: kani
 
       - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
+        uses: ./kani/.github/actions/setup
         with:
           os: ${{ matrix.os }}
-          install_cbmc: 'false'
+          kani_dir: 'kani'
 
       - name: Build Kani
+        working-directory: ./kani
         run: cargo build-dev
 
-      - name: Execute Kani regressions
-        run: ./scripts/kani-regression.sh
-
-  perf:
-    runs-on: ubuntu-20.04
-    steps:
       - name: Checkout CBMC under "cbmc"
         uses: actions/checkout@v3
         with:
           repository: diffblue/cbmc
           path: cbmc
 
       - name: Build CBMC
+        working-directory: ./cbmc
         run: |
-          cd cbmc
-          cmake -S . -Bbuild -DWITH_JBMC=OFF
-          cmake --build build -- -j 4
-          sudo cmake --build build --target install
-          # Cleanup cbmc directory
-          cd ..
-          rm -rf cbmc
+          make -C src minisat2-download cadical-download
+          make -C src -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
+          # Prepend the bin directory to $PATH
+          echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
 
-      - name: Checkout Kani
+      - name: Execute Kani regressions
+        working-directory: ./kani
+        run: ./scripts/kani-regression.sh
+
+  perf:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Kani under "kani"
         uses: actions/checkout@v3
+        with:
+          path: kani
 
       - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
+        uses: ./kani/.github/actions/setup
         with:
           os: ubuntu-20.04
-          install_cbmc: 'false'
+          kani_dir: 'kani'
 
       - name: Build Kani using release mode
+        working-directory: ./kani
         run: cargo build-dev -- --release
 
+      - name: Checkout CBMC under "cbmc"
+        uses: actions/checkout@v3
+        with:
+          repository: diffblue/cbmc
+          path: cbmc
+
+      - name: Build CBMC
+        working-directory: ./cbmc
+        run: |
+          cmake -S . -Bbuild -DWITH_JBMC=OFF
+          cmake --build build -- -j 4
+          # Prepend the bin directory to $PATH
+          echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
+
       - name: Execute Kani performance tests
+        working-directory: ./kani
         run: ./scripts/kani-perf.sh

.github/workflows/kani.yml

@@ -33,6 +33,25 @@ jobs:
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
+  write-json-symtab-regression:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v3
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: ubuntu-20.04
+
+      - name: Build Kani
+        run: cargo build-dev
+
+      - name: Execute Kani regression
+        env:
+          KANI_ENABLE_WRITE_JSON_SYMTAB: 1
+        run: ./scripts/kani-regression.sh
+
   experimental-features-regression:
     runs-on: ubuntu-20.04
     env:

CHANGELOG.md

@@ -0,0 +1,26 @@
+# Changelog
+
+This file contains notable changes (e.g. breaking changes, major changes, etc.) in Kani releases.
+
+This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
+
+## [0.23.0]
+
+### Breaking Changes
+
+- Remove the second parameter in the `kani::any_where` function by @zhassan-aws in #2257  
+We removed the second parameter in the `kani::any_where` function (`_msg: &'static str`) to make the function more ergonomic to use.
+We suggest moving the explanation for why the assumption is introduced into a comment.
+For example, the following code:
+```rust
+    let len: usize = kani::any_where(|x| *x < 5, "Restrict the length to a value less than 5");
+```
+should be replaced by:
+```rust
+    // Restrict the length to a value less than 5
+    let len: usize = kani::any_where(|x| *x < 5);
+```
+
+### Major Changes
+
+- Enable the build cache to avoid recompiling crates that haven't changed, and introduce `--force-build` option to compile all crates from scratch by @celinval in #2232.