Merge branch 'main' into issue-3206-tests

.github/workflows/cargo-update.yml

@@ -37,7 +37,7 @@ jobs:
             git diff
           fi
       - name: Create Pull Request
-        uses: peter-evans/create-pull-request@v6
+        uses: peter-evans/create-pull-request@v7
         with:
           commit-message: Upgrade cargo dependencies to ${{ env.today }}
           branch: cargo-update-${{ env.today }}

.github/workflows/cbmc-latest.yml

@@ -87,7 +87,7 @@ jobs:
       - name: Build CBMC
         working-directory: ./cbmc
         run: |
-          cmake -S . -Bbuild -DWITH_JBMC=OFF
+          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

.github/workflows/cbmc-update.yml

@@ -51,6 +51,8 @@ jobs:
             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
+            # install the newer CBMC version
+            ./scripts/setup/ubuntu/install_cbmc.sh
             if ! ./scripts/kani-regression.sh ; then
               echo "next_step=create_issue" >> $GITHUB_ENV
             else
@@ -63,7 +65,7 @@ jobs:
 
       - name: Create Pull Request
         if: ${{ env.next_step == 'create_pr' }}
-        uses: peter-evans/create-pull-request@v6
+        uses: peter-evans/create-pull-request@v7
         with:
           commit-message: Upgrade CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }}
           branch: cbmc-${{ env.CBMC_LATEST }}

.github/workflows/audit.yml → .github/workflows/deny.yml

@@ -4,9 +4,10 @@
 # 1. Checks licenses for allowed license.
 # 2. Checks Rust-Sec registry for security advisories.
 
-name: Cargo Audit
+name: Cargo Deny
 on:
   pull_request:
+  merge_group:
   push:
     # Run on changes to branches but not tags.
     branches:
@@ -17,7 +18,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - uses: EmbarkStudios/cargo-deny-action@v1
+        with:
+          submodules: recursive
+      - uses: EmbarkStudios/cargo-deny-action@v2
         with:
           arguments: --all-features --workspace
           command-arguments: -s

.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.
@@ -46,7 +47,7 @@ jobs:
 
       - name: 'Run Clippy'
         run: |
-          cargo clippy --all -- -D warnings
+          cargo clippy --workspace -- -D warnings
 
       - name: 'Print Clippy Statistics'
         run: |

.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.
@@ -97,6 +98,8 @@ jobs:
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4
+        with:
+          submodules: recursive
 
       - 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'

.github/workflows/toolchain-upgrade.yml

@@ -36,8 +36,9 @@ jobs:
         run: git clean -f
 
       - name: Create Pull Request
+        id: create_pr
         if: ${{ env.next_step == 'create_pr' }}
-        uses: peter-evans/create-pull-request@v6
+        uses: peter-evans/create-pull-request@v7
         with:
           commit-message: Upgrade Rust toolchain to nightly-${{ env.next_toolchain_date }}
           branch: toolchain-${{ env.next_toolchain_date }}
@@ -47,14 +48,25 @@ jobs:
             Update Rust toolchain from nightly-${{ env.current_toolchain_date }} to
             nightly-${{ env.next_toolchain_date }} without any other source changes.
 
-            This is an automatically generated pull request. If any of the CI checks fail,
-            manual intervention is required. In such a case, review the changes at
-            https://github.com/rust-lang/rust from
-            https://github.com/rust-lang/rust/commit/${{ env.current_toolchain_hash }} up to
-            https://github.com/rust-lang/rust/commit/${{ env.next_toolchain_hash }}. The log
-            for this commit range is:
+      - name: Add debugging hints
+        if: ${{ steps.create_pr.outputs.pull-request-number }}
+        uses: actions/github-script@v7
+        with:
+          script: |
+            github.rest.issues.createComment({
+              issue_number: ${{ steps.create_pr.outputs.pull-request-number }},
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              body: `This is an automatically generated pull request. If any of the CI checks fail,
+                manual intervention is required. In such a case, review the changes at
+                https://github.com/rust-lang/rust from
+                https://github.com/rust-lang/rust/commit/${{ env.current_toolchain_hash }} up to
+                https://github.com/rust-lang/rust/commit/${{ env.next_toolchain_hash }}. The log
+                for this commit range is:
+
+                ` + process.env.git_log
+            })
 
-            ${{ env.git_log }}
       - name: Create Issue
         if: ${{ env.next_step == 'create_issue' }}
         uses: dacbd/create-issue-action@main

.github/workflows/verify-std-check.yml

@@ -59,7 +59,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z ptr-to-ref-cast-checks
+            -Z mem-predicates
 
       # If the head failed, check if it's a new failure.
       - name: Checkout base
@@ -77,7 +77,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z ptr-to-ref-cast-checks
+            -Z mem-predicates
 
       - name: Compare PR results
         if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome

.gitignore

@@ -77,6 +77,9 @@ package-lock.json
 ## Rustdoc GUI tests
 tests/rustdoc-gui/src/**.lock
 
+## Charon/Aeneas LLBC files
+*.llbc
+
 # Before adding new lines, see the comment at the top.
 /.ninja_deps
 /.ninja_log

.gitmodules

@@ -5,3 +5,6 @@
 	path = tests/perf/s2n-quic
 	url = https://github.com/aws/s2n-quic
 	branch = main
+[submodule "charon"]
+	path = charon
+	url = https://github.com/AeneasVerif/charon

CHANGELOG.md

@@ -4,6 +4,91 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.56.0]
+
+### Major/Breaking Changes
+
+* Remove obsolete linker options (`--mir-linker` and `--legacy-linker`) by @zhassan-aws in https://github.com/model-checking/kani/pull/3559
+* List Subcommand by @carolynzech in https://github.com/model-checking/kani/pull/3523
+* Deprecate `kani::check` by @celinval in https://github.com/model-checking/kani/pull/3557
+
+### What's Changed
+
+* Enable stubbing and function contracts for primitive types by @celinval in https://github.com/model-checking/kani/pull/3496
+* Instrument validity checks for pointer to reference casts for slices and str's by @zhassan-aws in https://github.com/model-checking/kani/pull/3513
+* Fail compilation if `proof_for_contract` is added to generic function by @carolynzech in https://github.com/model-checking/kani/pull/3522
+* Fix storing coverage data in cargo projects by @adpaco-aws in https://github.com/model-checking/kani/pull/3527
+* Add experimental API to generate arbitrary pointers by @celinval in https://github.com/model-checking/kani/pull/3538
+* Running `verify-std` no longer changes Cargo files by @celinval in https://github.com/model-checking/kani/pull/3577
+* Add an LLBC backend by @zhassan-aws in https://github.com/model-checking/kani/pull/3514
+* Fix the computation of the number of bytes of a pointer offset by @zhassan-aws in https://github.com/model-checking/kani/pull/3584
+* Rust toolchain upgraded to nightly-2024-10-03 by @qinheping @tautschnig @celinval
+* CBMC upgraded to 6.3.1 by @tautschnig in https://github.com/model-checking/kani/pull/3537
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.55.0...kani-0.56.0
+
+## [0.55.0]
+
+### Major/Breaking Changes
+* Coverage reporting in Kani is now source-based instead of line-based.
+Consequently, the unstable `-Zline-coverage` flag has been replaced with a `-Zsource-coverage` one.
+Check the [Source-Coverage RFC](https://model-checking.github.io/kani/rfc/rfcs/0011-source-coverage.html) for more details.
+* Several improvements were made to the memory initialization checks. The current state is summarized in https://github.com/model-checking/kani/issues/3300. We welcome your feedback!
+
+### What's Changed
+* Update CBMC build instructions for Amazon Linux 2 by @tautschnig in https://github.com/model-checking/kani/pull/3431
+* Implement memory initialization state copy functionality by @artemagvanian in https://github.com/model-checking/kani/pull/3350
+* Make points-to analysis handle all intrinsics explicitly by @artemagvanian in https://github.com/model-checking/kani/pull/3452
+* Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in https://github.com/model-checking/kani/pull/3438
+* Fix ICE due to mishandling of Aggregate rvalue for raw pointers to `str` by @celinval in https://github.com/model-checking/kani/pull/3448
+* Basic support for memory initialization checks for unions by @artemagvanian in https://github.com/model-checking/kani/pull/3444
+* Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in https://github.com/model-checking/kani/pull/3119
+* Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3419
+* Partially integrate uninit memory checks into `verify_std` by @artemagvanian in https://github.com/model-checking/kani/pull/3470
+* Rust toolchain upgraded to `nightly-2024-09-03` by @jaisnan @carolynzech 
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.54.0...kani-0.55.0
+
+## [0.54.0]
+
+### Major Changes
+* We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts.
+* We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros.
+* We enabled support for concrete playback for harness that contains stubs or function contracts.
+* We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs.
+
+### Breaking Changes
+* The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default.
+
+## What's Changed
+* Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in https://github.com/model-checking/kani/pull/3332
+* Fix visibility of some Kani intrinsics by @artemagvanian in https://github.com/model-checking/kani/pull/3323
+* Function Contracts: Modify Slices by @pi314mm in https://github.com/model-checking/kani/pull/3295
+* Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3344
+* Add support for global transformations by @artemagvanian in https://github.com/model-checking/kani/pull/3348
+* Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in https://github.com/model-checking/kani/pull/3283
+* Fix contract handling of promoted constants and constant static by @celinval in https://github.com/model-checking/kani/pull/3305
+* Bump CBMC Viewer to 3.9 by @tautschnig in https://github.com/model-checking/kani/pull/3373
+* Update to CBMC version 6.1.1 by @tautschnig in https://github.com/model-checking/kani/pull/2995
+* Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in https://github.com/model-checking/kani/pull/3270
+* Enable concrete playback for contract and stubs by @celinval in https://github.com/model-checking/kani/pull/3389
+* Add code scanner tool by @celinval in https://github.com/model-checking/kani/pull/3120
+* Enable contracts in associated functions by @celinval in https://github.com/model-checking/kani/pull/3363
+* Enable log2*, log10* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3001
+* Enable powif* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/2999
+* Enable fma* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3002
+* Enable sqrt* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3000
+* Remove assigns clause for ZST pointers by @carolynzech in https://github.com/model-checking/kani/pull/3417
+* Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in https://github.com/model-checking/kani/pull/3374
+* Unify kani library and kani core logic by @jaisnan in https://github.com/model-checking/kani/pull/3333
+* Stabilize pointer-to-reference cast validity checks by @artemagvanian in https://github.com/model-checking/kani/pull/3426
+* Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri
+
+## New Contributors
+* @carolynzech made their first contribution in https://github.com/model-checking/kani/pull/3387
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0
+
 ## [0.53.0]
 
 ### Major Changes