Skip to content

Conversation

@zhassan-aws
Copy link
Contributor

@zhassan-aws zhassan-aws commented Apr 3, 2025

Advance the stable branch to fe0d9d2 and use the 1.86.0 channel.

Additional Details:

  • The 1.86.0 release was branched from main on 2025-02-14 (see https://releases.rs/docs/1.86.0/)
  • The latest commit on main with a close toolchain is fe0d9d2 which upgraded the toolchain to 2025-02-12. The next commit upgrades the toolchain to 2025-02-21, which doesn't compile without reverting some of the changes done in that commit.
  • Based on the previous point, I picked fe0d9d2, and made an additional change to make it compatible with the 1.86.0 release:
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 860619668c9..0c2a81c3082 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -667,7 +667,7 @@ fn codegen_rvalue_aggregate(
                 assert!(operands.len() == 2);
                 let typ = self.codegen_ty_stable(res_ty);
                 let layout = self.layout_of_stable(res_ty);
-                assert!(layout.ty.is_unsafe_ptr());
+                assert!(layout.ty.is_raw_ptr());
                 let data = self.codegen_operand_stable(&operands[0]);
                 match pointee_ty.kind() {
                     TyKind::RigidTy(RigidTy::Slice(inner_ty)) => {

(the same change was made in the next commit that upgraded the toolchain to 2025-02-21)

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

feliperodri and others added 29 commits January 28, 2025 21:42
Resolves model-checking#3854.

This upgrade requires changes to remove `RunCompiler` due to the
following changes:

- rust-lang/rust@a77776cc1d Remove RunCompiler


By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Signed-off-by: Felipe R. Monteiro <[email protected]>
…hecking#3808)

Resolves model-checking#3804.

Enables multiple `stub_verified(TARGET)` annotations on a harness, but
still detect and report duplicate targets.

Adds positive and negative tests.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Remi Delmas <[email protected]>
Co-authored-by: Celina G. Val <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>
…ng#3851)

Resolves model-checking#3815 


[Documentations](https://github.com/model-checking/kani/blob/main/library/kani_core/src/mem.rs#L3)
of `kani_core` modules doesn't show up correctly on
https://model-checking.github.io/kani/crates/doc/kani/mem/index.html.
This PR move the comments to the right place so that they will show up
correctly.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
In cases where a function pointer is created, but its value is never
used, Kani crashes due to missing function declaration.

For now, collect any instance that has its address taken even if its
never used.

Fixes model-checking#3799

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Instead of crashing, add a safety check that ensures the transmute is
not reachable.

Resolves model-checking#3839 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
CBMC's `symtab2gb` binary is no longer used since Kani now generates a
goto binary directly. Removing it from the Kani bundle.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
The old hack doesn't work anymore.

I pulled this from model-checking#3546 per PR comment

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
…3872)

Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`4500593` to `82dd0b5`.
<details>
<summary>Commits</summary>
<ul>
<li><a
href="https://github.com/aws/s2n-quic/commit/82dd0b595e7e9e58531ff26b908fd0f6bbc36e45"><code>82dd0b5</code></a>
fix: process packets from different sources before handshake confirmed
(<a
href="https://redirect.github.com/aws/s2n-quic/issues/2463">#2463</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/8bfc8a8d3cbfbf4932176593962b4a24e60abafe"><code>8bfc8a8</code></a>
build(deps): bump aws-actions/configure-aws-credentials (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2461">#2461</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/eace16636f4828ec2f1468309489cbde1c50fd87"><code>eace166</code></a>
fix: ignore local address when considering path migration (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2458">#2458</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/75c64e43c9cfd2b569d2b696f9c5f07cabf65945"><code>75c64e4</code></a>
Revert &quot;fix(s2n-quic-dc): derive crypto before opening TCP stream
(<a
href="https://redirect.github.com/aws/s2n-quic/issues/2451">#2451</a>)&quot;
(#...</li>
<li>See full diff in <a
href="https://github.com/aws/s2n-quic/compare/450059379ac24f9ba73c8ac940b1c6820af401ce...82dd0b595e7e9e58531ff26b908fd0f6bbc36e45">compare
view</a></li>
</ul>
</details>
<br />


Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.

[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)

---

<details>
<summary>Dependabot commands and options</summary>
<br />

You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)


</details>

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Dependency upgrade resulting from `cargo update`.

Co-authored-by: tautschnig <[email protected]>
This PR adds reference of loop contracts:
Rendered version:
https://github.com/qinheping/kani/blob/docs/loop-contracts/docs/src/reference/experimental/loop-contracts.md

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <[email protected]>
Resolves model-checking#3620

Removing default flag float overflow check, which reports overflow for
arithmetic operations over floating-point numbers that result in +/-Inf.
This doesn't panic in Rust and it shouldn't be consider a verification
failure by default.

Users can enable them using --cbmc-args as and when required.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Github generated release notes:

## What's Changed
* Automatic toolchain upgrade to nightly-2025-01-08 by @github-actions
in model-checking#3821
* Automatic cargo update to 2025-01-13 by @github-actions in
model-checking#3824
* Automatic toolchain upgrade to nightly-2025-01-09 by @github-actions
in model-checking#3825
* Bump ncipollo/release-action from 1.14.0 to 1.15.0 by @dependabot in
model-checking#3826
* Bump tests/perf/s2n-quic from `ac52a48` to `adc7ba9` by @dependabot in
model-checking#3827
* Automatic toolchain upgrade to nightly-2025-01-10 by @github-actions
in model-checking#3828
* Automatic toolchain upgrade to nightly-2025-01-11 by @github-actions
in model-checking#3830
* Verify contracts/stubs for generic types with multiple inherent
implementations by @carolynzech in
model-checking#3829
* Update Charon submodule by @thanhnguyen-aws in
model-checking#3823
* Automatic toolchain upgrade to nightly-2025-01-12 by @github-actions
in model-checking#3831
* Automatic toolchain upgrade to nightly-2025-01-13 by @github-actions
in model-checking#3833
* Upgrade toolchain to 2025-01-15 by @tautschnig in
model-checking#3835
* Automatic toolchain upgrade to nightly-2025-01-16 by @github-actions
in model-checking#3836
* Add a regression test for `no_std` feature by @carolynzech in
model-checking#3837
* Use fully-qualified name for size_of by @zhassan-aws in
model-checking#3838
* Automatic cargo update to 2025-01-20 by @github-actions in
model-checking#3842
* Bump tests/perf/s2n-quic from `adc7ba9` to `f0649f9` by @dependabot in
model-checking#3844
* Upgrade toolchain to nightly-2025-01-22 by @tautschnig in
model-checking#3843
* Remove `DefKind::Ctor` from filtering crate items by @carolynzech in
model-checking#3845
* Enable valid_ptr post_condition harnesses by @tautschnig in
model-checking#3847
* Update build command in docs to use release mode by @zhassan-aws in
model-checking#3846
* Automatic toolchain upgrade to nightly-2025-01-23 by @github-actions
in model-checking#3848
* Automatic toolchain upgrade to nightly-2025-01-24 by @github-actions
in model-checking#3850
* Remove the openssl-devel package from dependencies by @zhassan-aws in
model-checking#3852
* Fix validity checks for `char` by @celinval in
model-checking#3853
* Bump tests/perf/s2n-quic from `f0649f9` to `4500593` by @dependabot in
model-checking#3857
* Automatic cargo update to 2025-01-27 by @github-actions in
model-checking#3856
* Deprecate `--enable-unstable` and `--restrict-vtable` by @celinval in
model-checking#3859
* Stub linker to avoid missing symbols errors by @celinval in
model-checking#3858
* Toolchain upgrade to nightly-2025-01-28 by @feliperodri in
model-checking#3855
* Allow multiple annotations, but check for duplicate targets. by
@remi-delmas-3000 in model-checking#3808
* Move documentation of kani_core modules to right places by @qinheping
in model-checking#3851
* Fix missing function declaration issue by @celinval in
model-checking#3862
* Fix transmute codegen when sizes are different by @celinval in
model-checking#3861
* Remove symtab2gb from bundle by @zhassan-aws in
model-checking#3865
* Update the rustc hack for CLion / RustRover by @celinval in
model-checking#3868
* Bump tests/perf/s2n-quic from `4500593` to `82dd0b5` by @dependabot in
model-checking#3872
* Automatic cargo update to 2025-02-03 by @github-actions in
model-checking#3869
* Add reference for loop contracts by @qinheping in
model-checking#3849
* remove flag float-overflow-check by @rajath-mk in
model-checking#3873

## New Contributors
* @rajath-mk made their first contribution in
model-checking#3873

**Full Changelog**:
model-checking/kani@kani-0.58.0...kani-0.59.0



By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <[email protected]>
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Dependency upgrade resulting from `cargo update`.

Co-authored-by: tautschnig <[email protected]>
…3882)

Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`82dd0b5` to `a5d8422`.
<details>
<summary>Commits</summary>
<ul>
<li><a
href="https://github.com/aws/s2n-quic/commit/a5d84229dae984a40ece44add3f418b00342fa01"><code>a5d8422</code></a>
feat(s2n-quic-dc): Replace requested_handshakes map with immediate
request (#...</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/21464fc0d76a439279c54ebd826f2af95ebee33f"><code>21464fc</code></a>
build(deps): update lru requirement from 0.12 to 0.13 (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2467">#2467</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/b871ad0eafc48540499ee20299012ec3f52816e0"><code>b871ad0</code></a>
chore: release 1.53.0 (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2465">#2465</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/e8df067b214a8ecb43f00f149b4d2c971fabe4f3"><code>e8df067</code></a>
fix(s2n-quic-dc): Replace shared map with larger bitset (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2464">#2464</a>)</li>
<li>See full diff in <a
href="https://github.com/aws/s2n-quic/compare/82dd0b595e7e9e58531ff26b908fd0f6bbc36e45...a5d84229dae984a40ece44add3f418b00342fa01">compare
view</a></li>
</ul>
</details>
<br />


Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.

[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)

---

<details>
<summary>Dependabot commands and options</summary>
<br />

You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)


</details>

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
… is observed - Use case : CI speed up (model-checking#3879)

Resolves model-checking#3458 

Added the option `--fail-fast`, which would stop the verification
process whenever any of the harnesses fails, and returns the failed
harness as an error.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <[email protected]>
This PR introduces an initial implementation for the `autoharness`
subcommand and a book chapter describing the feature. I recommend
reading the book chapter before reviewing the code (or proceeding
further in this PR description).

## Callouts
`--harness` is to manual harnesses what `--include-function` and
`--exclude-function` are to autoharness; both allow the user to filter
which harnesses/functions get verified. Their implementation is
different, however--`--harness` is a driver-only flag, i.e., we still
compile every harness, but then only call CBMC on the ones specified in
`--harness`. `--include-function` and `--exclude-function` get passed to
the compiler. I made this design choice to try to be more aggressive
about improving compiler performance--if a user only asks to verify one
function and we go try to codegen a thousand, the compiler will take
much longer than it needs to. I thought this more aggressive
optimization was warranted given that crates are likely to have far many
more functions eligible for autoverification than manual Kani harnesses.

(See also the limitations in the book chapter).

## Testing
Besides the new tests in this PR, I also ran against
[s2n-quic](https://github.com/aws/s2n-quic) to confirm that the
subcommand works on larger crates.

Towards model-checking#3832

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Upgrade toolchain to 2/10.

I **highly recommend** reviewing this PR commit-by-commit. The
description in each commit message links to the upstream PRs that
prompted those particular changes.

## Callouts
- 2/1 had a lot of formatting changes. I split the commits for that day
into formatting changes and functionality changes accordingly.
- 2/5 introduced a regression in our delayed UB instrumentation, so I
made a new fixme test. See model-checking#3881 for details.


## Culprit PRs:
rust-lang/rust#134424 
rust-lang/rust#130514
rust-lang/rust#135748
rust-lang/rust#136590
rust-lang/rust#135318
rust-lang/rust#135265

rust-lang/rust@bcb8565
rust-lang/rust#136471
rust-lang/rust#136645

Resolves model-checking#3863

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Add documentation of loop contracts to `SUMMARY.md` so that it will show
up in the book.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
…hecking#3888)

### Problem
When CBMC generates a JSON trace for a nondeterministic array, it will
output a key-value pair `elements: [array]`, where `array` contains
concrete values for each element in the array. If the array is length 64
or shorter, it will _also_ output the elements of the array as separate
values in the trace (so each element is in the trace twice). Prior to
this PR, concrete playback relied on the latter output format to find
elements of an array. However, when the array was length 65 or greater,
those elements wouldn't be values in their own right, so we wouldn't
find any values for the array and just output an empty array.

### Solution
This PR changes our representation of concrete values to handle arrays
explicitly; i.e., to look for the `elements` array and populate the
concrete values of the array from that instead.

### Callouts
For those wondering why the `playback_already_existed` test changed,
it's because we're hashing `ConcreteItem` instead of `ConcreteValue`, so
the hash changes.

Resolves model-checking#3787

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Dependency upgrade resulting from `cargo update`.

Co-authored-by: tautschnig <[email protected]>
…3894)

Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`a5d8422` to `00e3371`.
<details>
<summary>Commits</summary>
<ul>
<li><a
href="https://github.com/aws/s2n-quic/commit/00e33714d74b0646bc18ab65c90a45504a185828"><code>00e3371</code></a>
build(deps): update rand requirement in /tools/xdp (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2474">#2474</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/d7b2c8778f9a4ad8c3295c066c8f204ed5f51d2b"><code>d7b2c87</code></a>
build(deps): bump docker/setup-buildx-action from 3.8.0 to 3.9.0 (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2470">#2470</a>)</li>
<li>See full diff in <a
href="https://github.com/aws/s2n-quic/compare/a5d84229dae984a40ece44add3f418b00342fa01...00e33714d74b0646bc18ab65c90a45504a185828">compare
view</a></li>
</ul>
</details>
<br />


Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.

[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)

---

<details>
<summary>Dependabot commands and options</summary>
<br />

You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)


</details>

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Anything listed as undefined behavior (UB) at
https://doc.rust-lang.org/reference/behavior-considered-undefined.html
must also be considered UB by Kani and should not pass under
`should_fail`. In preparation of this PR, all occurrences of
`PropertyClass` in the code base were audited and, where necessary,
adjusted.

Also, all uses of `kani::assert` were audited to confirm or adjust them.
This resulted in first-time use of the `UnsupportedCheck` hook, which
implied fixes to its implementation.

Resolves: model-checking#3571

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Carolyn Zech <[email protected]>
…nge (model-checking#3892)

Resolves model-checking#3891

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Michael Tautschnig <[email protected]>
Update Rust to nightly-2025-02-11

Upstream PR:
rust-lang/rust@ee7dc06#diff-51b3860a8aed92b0e981635d4118d369c49850f5b7acf780d31f5ddd5d5d0bc2

Resolves model-checking#3884

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
model-checking#3755 introduced additional safety checks for the `offset` intrinsic,
including a check for whether `count` overflows `isize`. However, such
overflow is allowed for ZSTs. This PR changes the model to check for
ZSTs before computing the offset to avoid triggering an overflow failure
for ZSTs.

I also moved an existing test called `offset-overflow` into another
test, since model-checking#3755 changed the failure for that test to be about an out
of bounds allocation, not an isize overflow.

Resolves model-checking#3896

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Update Rust toolchain from nightly-2025-02-11 to nightly-2025-02-12
without any other source changes.

Co-authored-by: carolynzech <[email protected]>
@zhassan-aws zhassan-aws requested a review from a team as a code owner April 3, 2025 17:59
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Apr 3, 2025
@zhassan-aws
Copy link
Contributor Author

Only review the last commit in this PR. The others are merged as is from main.

Copy link
Contributor

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It may be cleaner to do this via rebase rather than have a merge commit, but I'll leave that up to you.

Also, for posterity, would you mind updating the PR description with something like:
"Kani went from the 2/12 toolchain to 2/21, while 1.86.0 branched off of the 2/14 toolchain. So, this PR operates off of the 2/12 version of Kani, with a small change in 860140a to make it compatible with the 2/14 stable version."
Just so that future contributors know the steps we take to go about updating the stable branch.

@zhassan-aws
Copy link
Contributor Author

After this PR, the diff w.r.t to the corresponding commit in main is reduced than for 1.85.1 (and is expected to be reduced further in the future):

diff --git a/.cargo/config.toml b/.cargo/config.toml
index 9bb4e080834..f0df939ef50 100644
--- a/.cargo/config.toml
+++ b/.cargo/config.toml
@@ -20,6 +20,8 @@ KANI_SYSROOT ={value = "target/kani", relative = true}
 KANI_BUILD_LIBS ={value = "target/build-libs", relative = true}
 # Build Kani library without `build-std`.
 KANI_LEGACY_LIBS ={value = "target/legacy-libs", relative = true}
+# This is only required for stable but is a no-op for nightly channels
+RUSTC_BOOTSTRAP = "1"
 
 [target.'cfg(all())']
 rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 860619668c9..0c2a81c3082 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -667,7 +667,7 @@ fn codegen_rvalue_aggregate(
                 assert!(operands.len() == 2);
                 let typ = self.codegen_ty_stable(res_ty);
                 let layout = self.layout_of_stable(res_ty);
-                assert!(layout.ty.is_unsafe_ptr());
+                assert!(layout.ty.is_raw_ptr());
                 let data = self.codegen_operand_stable(&operands[0]);
                 match pointee_ty.kind() {
                     TyKind::RigidTy(RigidTy::Slice(inner_ty)) => {
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index c8a56d3ef06..106ad662b3a 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -16,6 +16,8 @@
 #![feature(f128)]
 #![feature(f16)]
 #![feature(non_exhaustive_omitted_patterns_lint)]
+#![feature(cfg_version)]
+#![cfg_attr(not(version("1.86")), feature(float_next_up_down))]
 #![feature(try_blocks)]
 extern crate rustc_abi;
 extern crate rustc_ast;
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 4c39b03183b..9097713a001 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -206,6 +206,8 @@ pub fn cargo_build(&mut self, keep_going: bool) -> Result<CargoOutputs> {
                     // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
                     // https://doc.rust-lang.org/cargo/reference/environment-variables.html
                     .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
+                    // This is only required for stable but is a no-op for nightly channels
+                    .env("RUSTC_BOOTSTRAP", "1")
                     .env("CARGO_TERM_PROGRESS_WHEN", "never");
 
                 match self.run_build_target(cmd, verification_target.target()) {
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 9a09ce6163f..f21f8334578 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -84,6 +84,8 @@ pub fn compile_single_rust_file(
         let mut cmd = Command::new(&self.kani_compiler);
         let kani_compiler_args = to_rustc_arg(kani_args);
         cmd.arg(kani_compiler_args).args(rustc_args);
+        // This is only required for stable but is a no-op for nightly channels
+        cmd.env("RUSTC_BOOTSTRAP", "1");
 
         if self.args.common_args.quiet {
             self.run_suppress(cmd)?;
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 2286133bf40..4e330c13244 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-02-12"
+channel = "1.86.0"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/rustfmt.toml b/rustfmt.toml
index 44cbfe4a3dc..f8ff0d0fd10 100644
--- a/rustfmt.toml
+++ b/rustfmt.toml
@@ -6,13 +6,3 @@ edition = "2021"
 style_edition = "2024"
 use_small_heuristics = "Max"
 merge_derives = false
-
-ignore = [
-    "**/build/",
-    "**/target/",
-
-    # Do not format submodules
-    # For some reason, this is not working without the directory wildcard.
-    "**/firecracker",
-    "**/tests/perf/s2n-quic/",
-]
diff --git a/scripts/kani-fmt.sh b/scripts/kani-fmt.sh
index 5eca1582cc4..6a136f244ff 100755
--- a/scripts/kani-fmt.sh
+++ b/scripts/kani-fmt.sh
@@ -19,19 +19,25 @@ error=0
 cargo fmt "$@" || error=1
 
 # Check test source files.
-# Note that this will respect the ignore section of rustfmt.toml. If you need to
-# skip any file / directory, add it there.
 TESTS=("tests" "docs/src/tutorial")
+# Add ignore patterns for code we don't want to format.
+IGNORE=("*/perf/s2n-quic/*")
+
+# Arguments for the find command for excluding the IGNORE paths
+IGNORE_ARGS=()
+for ignore in "${IGNORE[@]}"; do
+    IGNORE_ARGS+=(-not -path "$ignore")
+done
 
 for suite in "${TESTS[@]}"; do
     # Find uses breakline to split between files. This ensures that we can
     # handle files with space in their path.
     set -f; IFS=$'\n'
-    files=($(find "${suite}" -name "*.rs"))
+    files=($(find "${suite}" -name "*.rs" ${IGNORE_ARGS[@]}))
     set +f; unset IFS
     # Note: We set the configuration file here because some submodules have
     # their own configuration file.
-    rustfmt --unstable-features "$@" --config-path rustfmt.toml "${files[@]}" || error=1
+    rustfmt --config-path rustfmt.toml "${files[@]}" || error=1
 done
 
 exit $error
diff --git a/tests/cargo-ui/verbose-cmds/expected b/tests/cargo-ui/verbose-cmds/expected
index f883ef972cb..b47b60d51ff 100644
--- a/tests/cargo-ui/verbose-cmds/expected
+++ b/tests/cargo-ui/verbose-cmds/expected
@@ -1,5 +1,5 @@
 CARGO_ENCODED_RUSTFLAGS=
-cargo +nightly
+cargo +
 Running: `goto-cc
 Running: `goto-instrument
 Checking harness dummy_harness...
diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected
index 38f31a63d5c..0c43cd901cc 100644
--- a/tests/expected/function-contract/valid_ptr.expected
+++ b/tests/expected/function-contract/valid_ptr.expected
@@ -4,9 +4,7 @@ Failed Checks: |result| kani::mem::can_dereference(result.0)
 VERIFICATION:- FAILED
 
 Checking harness pre_condition::harness_invalid_ptr...
-Failed Checks: assertion failed: unsafe { read_ptr(ptr) } == -20
 Failed Checks: Kani does not support reasoning about pointer to unallocated memory
-Failed Checks: dereference failure: pointer outside object bounds
 VERIFICATION:- FAILED
 
 Checking harness pre_condition::harness_stack_ptr...

@zhassan-aws
Copy link
Contributor Author

zhassan-aws commented Apr 3, 2025

It may be cleaner to do this via rebase rather than have a merge commit, but I'll leave that up to you.

I've been deliberating this, and it seemed to me that doing a rebase would make us lose the commits for the previous releases since history will be rewritten. Using a merge commit, we would be able to maintain commits for previous stable releases (and perhaps we should even tag them). What do you think?

Also, for posterity, would you mind updating the PR description with something like

Will do. Done

@carolynzech
Copy link
Contributor

I've been deliberating this, and it seemed to me that doing a rebase would make us lose the commits for the previous releases since history will be rewritten. Using a merge commit, we would be able to maintain commits for previous stable releases (and perhaps we should even tag them). What do you think?

Yeah, you're right, let's keep it as is.

@zhassan-aws
Copy link
Contributor Author

The release bundle local toolchain test is failing because it's trying to download the bundle's nightly toolchain. We will probably need to create a separate workflow for testing the stable release bundle.

Merging this PR since the release bundle is not a required check anyway.

@zhassan-aws zhassan-aws merged commit 158f1af into model-checking:stable Apr 4, 2025
23 of 28 checks passed
@zhassan-aws zhassan-aws deleted the 1.86.0 branch April 4, 2025 18:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

9 participants