Upgrade stable branch to Rust 1.89.0 #4280
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 <felisous@amazon.com>
…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 <delmasrd@amazon.com> Co-authored-by: Celina G. Val <celinval@amazon.com> Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
…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 "fix(s2n-quic-dc): derive crypto before opening TCP stream (<a href="https://redirect.github.com/aws/s2n-quic/issues/2451">#2451</a>)" (#...</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] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com>
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 <88045115+zhassan-aws@users.noreply.github.com>
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 <88045115+zhassan-aws@users.noreply.github.com>
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 <1144736+tautschnig@users.noreply.github.com>
…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] <support@github.com> 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 <88045115+zhassan-aws@users.noreply.github.com>
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 <1144736+tautschnig@users.noreply.github.com>
…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] <support@github.com> 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 <cmzech@amazon.com>
…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 <mt@debian.org>
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 <zyadh@amazon.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
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 <71352687+carolynzech@users.noreply.github.com>
Upstream PRs requiring changes: rust-lang/rust#135994 rust-lang/rust#136466 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 <1144736+tautschnig@users.noreply.github.com>
Bumps [ncipollo/release-action](https://github.com/ncipollo/release-action) from 1.15.0 to 1.16.0. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/ncipollo/release-action/releases">ncipollo/release-action's releases</a>.</em></p> <blockquote> <h2>v1.16.0</h2> <h2>What's Changed</h2> <ul> <li>Bump <code>@octokit/request-error</code> from 5.0.1 to 5.1.1 by <a href="https://github.com/dependabot"><code>@dependabot</code></a> in <a href="https://redirect.github.com/ncipollo/release-action/pull/498">ncipollo/release-action#498</a></li> <li>Update checkout action version in example by <a href="https://github.com/Cycloctane"><code>@Cycloctane</code></a> in <a href="https://redirect.github.com/ncipollo/release-action/pull/496">ncipollo/release-action#496</a></li> <li>Bump undici from 5.28.4 to 5.28.5 by <a href="https://github.com/dependabot"><code>@dependabot</code></a> in <a href="https://redirect.github.com/ncipollo/release-action/pull/499">ncipollo/release-action#499</a></li> <li>Bump glob from 11.0.0 to 11.0.1 by <a href="https://github.com/dependabot"><code>@dependabot</code></a> in <a href="https://redirect.github.com/ncipollo/release-action/pull/495">ncipollo/release-action#495</a></li> <li>Bump <code>@types/node</code> from 22.10.3 to 22.13.4 by <a href="https://github.com/dependabot"><code>@dependabot</code></a> in <a href="https://redirect.github.com/ncipollo/release-action/pull/500">ncipollo/release-action#500</a></li> <li>Regenerate release notes on release updates by <a href="https://github.com/rantoniuk"><code>@rantoniuk</code></a> in <a href="https://redirect.github.com/ncipollo/release-action/pull/497">ncipollo/release-action#497</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/rantoniuk"><code>@rantoniuk</code></a> made their first contribution in <a href="https://redirect.github.com/ncipollo/release-action/pull/497">ncipollo/release-action#497</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/ncipollo/release-action/compare/v1...v1.16.0">https://github.com/ncipollo/release-action/compare/v1...v1.16.0</a></p> </blockquote> </details> <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/ncipollo/release-action/commit/440c8c1cb0ed28b9f43e4d1d670870f059653174"><code>440c8c1</code></a> preparing release 1.16.0</li> <li><a href="https://github.com/ncipollo/release-action/commit/e805702217830bf10c24c2f76e2aa5a7217d96ef"><code>e805702</code></a> preparing release 1.17.0</li> <li><a href="https://github.com/ncipollo/release-action/commit/bd572a1942a7b6abcc0f0d08d49abff2ffcfb877"><code>bd572a1</code></a> preparing release 1.17.0</li> <li><a href="https://github.com/ncipollo/release-action/commit/706b28e44cafbb6d40a2dd212782f79aa976fc9e"><code>706b28e</code></a> Update tag scheme in sheepit</li> <li><a href="https://github.com/ncipollo/release-action/commit/411ac011dfc7b5246b787e1283307b266750887e"><code>411ac01</code></a> preparing release 1.16.0</li> <li><a href="https://github.com/ncipollo/release-action/commit/a8c5a7f25281c4c6db1f89e47b936a12049e4fd5"><code>a8c5a7f</code></a> Fixes <a href="https://redirect.github.com/ncipollo/release-action/issues/474">#474</a> Regenerate release notes on release updates (<a href="https://redirect.github.com/ncipollo/release-action/issues/497">#497</a>)</li> <li><a href="https://github.com/ncipollo/release-action/commit/62f16c02e783fdc3fe43af16e2ad203ffba8bbef"><code>62f16c0</code></a> Add sheepit config</li> <li><a href="https://github.com/ncipollo/release-action/commit/00e83e3d358649a5f48877272bbcd086d2c0b7dd"><code>00e83e3</code></a> Attempt <a href="https://redirect.github.com/ncipollo/release-action/issues/1">#1</a> at fixing workflow file</li> <li><a href="https://github.com/ncipollo/release-action/commit/906fc7711314593609ffa59457f383d9230b33b1"><code>906fc77</code></a> Add initial releases workflow</li> <li><a href="https://github.com/ncipollo/release-action/commit/17b559883ec5bed1296fa4faf0225a8615a1c6cd"><code>17b5598</code></a> Add biome and initial format rules</li> <li>Additional commits viewable in <a href="https://github.com/ncipollo/release-action/compare/v1.15.0...v1.16.0">compare view</a></li> </ul> </details> <br /> [](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores) 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] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
…4148) Motivated by the finding that the [`write_goto_binary_file`](https://github.com/model-checking/kani/blob/1b25a1853fab3262380e9baefdfeb929edd53fd1/cprover_bindings/src/irep/goto_binary_serde.rs#L97-L103) function is responsible for around half of our compiler's codegen time, this PR does a collection of low-hanging fruit optimizations for the way we export goto files in the `cprover_bindings` crate. This includes: - Switching `IrepNumbering` caches to use the faster [`FxHashMap`](https://nnethercote.github.io/2021/12/08/a-brutally-effective-hash-function-in-rust.html) (as used in the rust compiler) - Using `.entry().or_insert()` to initialize the irep cache - This avoids having to hash separately for a `.get()` and `.insert()` (as the compiler seemed to have not optimized them together) - Making `IrepId` strings copy-on-write - This avoids unnecessary string allocations by allowing us to construct `InternedString`s directly from borrowed string literals when possible Initial testing (on [`perf/format`](https://github.com/model-checking/kani/blob/main/tests/perf/format/src/lib.rs) & [`perf/vec/vec`](https://github.com/model-checking/kani/blob/main/tests/perf/vec/vec/src/main.rs)) suggests that these changes make our compiler ~13% faster, but I'm also working on comparing performance on the whole std project for the future. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Adds the ability for `cargo kani` to optionally output the info needed for generating flamegraphs of the compiler & driver's performance. When enabled with the `FLAMEGRAPH` environment variable, it will generate an output file for the driver and one for each crate in the workspace as they are compiled. These output files can then be rendered as flamegraphs to see where Kani is spending most of its execution time. See [this draft docs page](https://github.com/AlexanderPortland/kani/blob/flamegraph/docs/src/profiling.md) for more detailed instructions on how it would be used. This should help us pinpoint which pieces of the compilation process are most to blame for our compilation times and focus future efforts to improve them. Resolves model-checking#4075 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 <carolynzech@gmail.com> Co-authored-by: Carolyn Zech <cmzech@amazon.com>
This PR fixes the bug: Static union values can panic Kani. The reason behind the bug is Kani's translation of Union type is not consistent with its layout defined by Rust. Specifically, the size of the Union is not just the max of its fields but that maximum should be round up to a multiple of its alignment. See: https://web.mit.edu/rust-lang_v1.25/arch/amd64_ubuntu1404/share/doc/rust/html/reference/type-layout.html#:~:text=The%20layout%20of%20a%20type,also%20part%20of%20type%20layout In this PR, I add another variant for DataComponent: DataComponent::UnionField, with a padded_type of a Union (a struct which contains a padding and the real field type) to fix the translated layout and support reasoning about transmute function for union type. Resolves model-checking#4097 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Culprit PRs: - June 4: rust-lang/rust#141741 - June 5: rust-lang/rust#142015 - June 6: rust-lang/rust#138677, rust-lang/rust#142005 - June 7: rust-lang/rust#142012 - June 9: rust-lang/rust#141700 - June 10: rust-lang/rust#142179, rust-lang/rust#141803 Resolves model-checking#4140 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 <1144736+tautschnig@users.noreply.github.com>
Updates as suggested by `cargo outdated --workspace`. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Relevant upstream PR: - rust-lang/rust#142410 (intrinsics: rename min_align_of to align_of) Resolves: model-checking#4155 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…4160) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `3129ad5` to `c6e694e`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/c6e694e99cc4e81d1863b8b3bb5a23311f24e40f"><code>c6e694e</code></a> build(deps): update prost requirement from 0.13 to 0.14 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2667">#2667</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/c54d5f33b3805efe52a92c96be5771c8f01b415a"><code>c54d5f3</code></a> fix(ci): skip max_total_test for cargotiming job (<a href="https://redirect.github.com/aws/s2n-quic/issues/2665">#2665</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/4161e8efac1bcf938f5ccc492db2ef490acea7d1"><code>4161e8e</code></a> Revert "ci(GithubAction): only run aws credential on upstream s2n-quic (<a href="https://redirect.github.com/aws/s2n-quic/issues/2656">#2656</a>...</li> <li><a href="https://github.com/aws/s2n-quic/commit/bf17f77bc8ca5e51c74f959a38e93c9284979c3d"><code>bf17f77</code></a> build(deps): update bindgen requirement from 0.71 to 0.72 in /tools/xdp (<a href="https://redirect.github.com/aws/s2n-quic/issues/2660">#2660</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/8081777532f3e82d419ab889ddd5e5f8ee5ddc4d"><code>8081777</code></a> fix(dc/wireshark): Provide Rust edition to bindgen (<a href="https://redirect.github.com/aws/s2n-quic/issues/2663">#2663</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/a1c0626f5cacc2e7d1caa87c7b5097ab5c90e657"><code>a1c0626</code></a> ci(GithubAction): only run aws credential on upstream s2n-quic (<a href="https://redirect.github.com/aws/s2n-quic/issues/2656">#2656</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/3129ad5ac618bb7b9b4fcddb67129af0f274c99e...c6e694e99cc4e81d1863b8b3bb5a23311f24e40f">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] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
…4164) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `c6e694e` to `b1b5bf8`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/b1b5bf8bee2e3998cf5a7bf9a90bb3b96b57cd37"><code>b1b5bf8</code></a> build(deps): revert update of prost requirement from 0.13 to 0.14 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2671">#2671</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/f84b71ad5526650b7293c523b191e47db3de93e0"><code>f84b71a</code></a> feat(s2n-quic-dc): Increase background handshake jitter (<a href="https://redirect.github.com/aws/s2n-quic/issues/2670">#2670</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/c6e694e99cc4e81d1863b8b3bb5a23311f24e40f...b1b5bf8bee2e3998cf5a7bf9a90bb3b96b57cd37">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] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Relevant upstream PR: - rust-lang/rust#141769 (Move metadata object generation for dylibs to the linker code) Resolves: model-checking#4162 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 <88045115+zhassan-aws@users.noreply.github.com>
Dependency upgrade resulting from `cargo update`. --------- Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
Modifies the `RustcIntrinsicsPass` to stub out panic functions during
body transformation at the MIR level. This avoids having to bring in
(and do transformation passes on) the large amounts of code they use for
string formatting. Our panic hook has been modified to then detect these
stubs during codegen and still generate the same Goto code for them.
The results of this change on the MIR bloat of `panic!()` and its
callers is shown below:
| test | lines of MIR (before) | lines of MIR (w/ panic stubbing) |
| - | - | - |
| `Option<usize>::unwrap()` | 292 | 217 |
| `Option<usize>::expect()` | 8664 | 225 |
| `Result<usize, usize>::unwrap()` | 20461 | 20374 |
| `Result<usize, usize>::expect()` | 20463 | 20376 |
| `panic!("hello!")` | 8498 | 41 |
| `panic!("hello {x}!")` (x being a `&'static str`) | 8502 | 45 |
The lack of significant improvement on the two `Result` functions is
elaborated on in model-checking#4168 and will take additional consideration to fix.
Resolves model-checking#2835
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
…4175) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `b1b5bf8` to `32ba87d`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/32ba87d2eb08459ad5ad6e3cf7207cba72c47a49"><code>32ba87d</code></a> ci: remove skipping tests for cargotiming (<a href="https://redirect.github.com/aws/s2n-quic/issues/2680">#2680</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/748245795b8bb28faf58adeca703226c4a6791ec"><code>7482457</code></a> Emit event for deduplicated connection opens (<a href="https://redirect.github.com/aws/s2n-quic/issues/2677">#2677</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/43178b13b43349bcc489dbeb6ceb750aa679bf26"><code>43178b1</code></a> Define dcQUIC stream connect events (<a href="https://redirect.github.com/aws/s2n-quic/issues/2675">#2675</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/a5da5db467621280c9e88eae14f0d708660c05b2"><code>a5da5db</code></a> build(deps): update prost requirement from 0.13 to 0.14 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2674">#2674</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/95fa51db26b84cf5a1ea114c54887b54fb7ed3b2"><code>95fa51d</code></a> build(deps): bump docker/setup-buildx-action from 3.11.0 to 3.11.1 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2673">#2673</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/a1343aea4b211f8f434c5b54f101c412499a4e59"><code>a1343ae</code></a> build(deps): bump docker/setup-buildx-action from 3.10.0 to 3.11.0 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2672">#2672</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/b1b5bf8bee2e3998cf5a7bf9a90bb3b96b57cd37...32ba87d2eb08459ad5ad6e3cf7207cba72c47a49">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] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Handle enums with zero or one variants when deriving `BoundedArbitrary`. Resolves model-checking#4170 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
We have an existing `benchcomp` script to measure Kani's performance in CI, but it is prone to noise and only focuses on the end-to-end performance of compilation and verification together, leaving a need for more granular measurements. This script focuses solely on changes in the runtime of the Kani compiler and runs with warm ups, repeats and outlier detection (based on the rust compiler's method in [`rustc-perf`](https://github.com/rust-lang/rustc-perf)) in an attempt to limit noise. The new `compile-timer-short` CI job uses this script on a subset of the `perf` tests (currently excluding `s2n-quic`, `kani-lib/arbitrary` & `misc/display-trait`) to produce a `benchcomp`-like table comparing the compiler performance per-crate before and after a given commit. This also modifies our auto-labeller to ensure end-to-end benchmarks (like `benchcomp`) and the new compiler-specific ones are only run when the parts of Kani that they profile have changed. We manually tested the CI job on my personal fork (see [this regressing run](https://github.com/AlexanderPortland/kani/actions/runs/15788016660?pr=6) from a test PR that intentionally slows down the compiler). Resolves model-checking#2442 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Relevant upstream PR: rust-lang/rust#137944 (Sized Hierarchy: Part I). This PR implements a part of [RFC 3729](rust-lang/rfcs#3729), which prescribes a hierarchy of `Sized` traits. Notably, this disallows instantiation of `size_of_val` and `align_of_val` with extern types. Consequently, the code in tests `unsized_foreign.rs` as well as parts of `foreign_type.rs` no longer compile (when previously some of the tests would panic). These test were therefore removed. Resolves: model-checking#4165 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Adds a simple cache of the `~/.cargo/registry` directory and Kani's `target` directory to reduce compilation times of our dependencies in CI. This also caches the `~/.rustup` directory to avoid having to re-download toolchains and re-compile the standard library every CI run. Caches are shared between workflows that compile Kani in the same way (e.g. between the `benchcomp-tests` & `perf` jobs since they both compile in release mode). Based on testing on my local fork, this change seems to make a minor, but not insignificant impact on runtimes. Although lost in the noise on longer jobs, `llbc-regression` & `benchcomp-tests` got noticeably faster, as did the compiler benchmarking workflows which have to compile Kani for each commit they are comparing. **Test runs:** General Kani CI workflow: [before](https://github.com/AlexanderPortland/kani/actions/runs/15886762745) | [after](https://github.com/AlexanderPortland/kani/actions/runs/15887740017) Compiler bench workflow: [before](https://github.com/AlexanderPortland/kani/actions/runs/15888031249) | [after](https://github.com/AlexanderPortland/kani/actions/runs/15889545021) Resolves model-checking#4153 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…#4167) While generating automatic harnesses, derive `Arbitrary` implementations for structs and enums that don't have implementations. ## Implementation Overview 1. In `automatic_harness_partition`, we mark a function as eligible for autoharness if its arguments either: a. implement `Arbitrary`, or b. are structs/enums whose fields implement `Arbitrary`. 2. `AutomaticHarnessPass` runs as before, but now may generate harnesses that call `kani::any()` for structs/enums that do not actually implement `Arbitrary`. See the definition of `kani::any()`: https://github.com/model-checking/kani/blob/b64e59de669cd77b625cc8c0b9a94f29117a0ff7/library/kani_core/src/lib.rs#L274-L276 The initial `kani::any()` call resolves fine, but the compiler would ICE if it tried to resolve `T::any()`. 3. To avoid the ICE, we add a new `AutomaticArbitraryPass` that runs after the `AutomaticHarnessPass`. This pass detects the calls to nonexistent `T::any()`s and replaces them with inlined `T::any()` implementations. These implementations are based on what Kani's derive macros for structs and enums produce. ## Example Given the automatic harness `foo_harness` produced by `AutomaticHarnessPass`: ```rust struct Foo(u32) fn function_with_foo(foo: Foo) { ... } // pretend this is an autoharness, just written in source code for the example #[kani::proof] fn foo_harness() { let foo = kani::any(); function_with_foo(foo); } ``` `AutomaticArbitraryPass` will rewrite `kani::any()`: ```rust pub fn any() -> Foo { Foo::any() } ``` as: ```rust pub fn any() -> Foo { Self(kani::any()) } ``` i.e., replace the call to `Foo::any()` with what the derive macro would have produced for the body of `Foo::any()` (had the programmer used the derive macro instead). ## Limitations The fields need to have `Arbitrary` implementations; there is no support for recursive derivation. See the tests for examples; this should be resolvable through further engineering effort. 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.
Relevant upstream PRs: - rust-lang/rust#141061 (Change __rust_no_alloc_shim_is_unstable to be a function) - rust-lang/rust#142650 (Refactor Translator) Resolves: model-checking#4176 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Install `wget` as part of the dependencies as it's needed for downloading kissat (`scripts/setup/install_kissat.sh`). Without that, users may run into an error: ``` + wget -O rel-4.0.1.tar.gz https://github.com/arminbiere/kissat/archive/refs/tags/rel-4.0.1.tar.gz /Users/foo/git/kani/scripts/setup/macos-14/../install_kissat.sh: line 33: wget: command not found ``` 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 <1144736+tautschnig@users.noreply.github.com> Co-authored-by: Carolyn Zech <cmzech@amazon.com>
This PR adds support for loop assigns in loop contracts. Resolves model-checking#3871 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
github-actions
bot
added
Z-EndToEndBenchCI
carolynzech
approved these changes
Aug 11, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
15 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Advance the stable branch to b705ac5 and use the 1.89.0 channel.
This PR was created through:
git merge b705ac564a0905549a5fb45610f876e1d7133678 -X theirsrust-toolchain.tomlto1.89.0The rationale for picking b705ac5 is as follows:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.