Upgrade stable branch to Rust 1.88.0 #4184
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 <[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 "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] <[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]>
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 <[email protected]>
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="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/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="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/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="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/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="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/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="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/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="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/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="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/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] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Update Rust toolchain from nightly-2025-05-16 to nightly-2025-05-17 without any other source changes. Co-authored-by: celinval <[email protected]>
Background: 1. Kani currently cannot be installed using `cargo install kani-verifier` on Ubuntu 20.04 because of the older glibc version, and thus needs to be built from source. 2. The `scripts/setup/ubuntu-20.04` directory is a symlink to `scripts/setup/ubuntu` which is incorrect because the installation scripts in the `ubuntu` directory assume the existence of a deb package for CBMC which is not the case for Ubuntu 20.04. To make it easier for users to build from source on Ubuntu 20.04, this PR adds the necessary setup scripts under a new `scripts/setup/ubuntu-20.04` directory. 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-05-17 to nightly-2025-05-18 without any other source changes. Co-authored-by: celinval <[email protected]>
Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <[email protected]>
Update Rust toolchain from nightly-2025-05-18 to nightly-2025-05-19 without any other source changes. Co-authored-by: celinval <[email protected]>
Update Rust toolchain from nightly-2025-05-19 to nightly-2025-05-20 without any other source changes. Co-authored-by: celinval <[email protected]>
…4089) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `5f323b7` to `22434aa`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/22434aa541781e42924bcf9856cd435250150344"><code>22434aa</code></a> chore: schedule daily qns job (<a href="https://redirect.github.com/aws/s2n-quic/issues/2636">#2636</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/a5921e570d3542beb362edb516ec05f8356e9a08"><code>a5921e5</code></a> fix(s2n-quic-h3): support h3-0.0.8 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2629">#2629</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/a961b1f5f8b3f244664b840fa00dd1c3219c750b"><code>a961b1f</code></a> build(deps): bump aws-actions/configure-aws-credentials (<a href="https://redirect.github.com/aws/s2n-quic/issues/2627">#2627</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/e89ebaa29fd9079c008f1728ae3b7e2bb3645f57"><code>e89ebaa</code></a> build(deps): update elf requirement from 0.7 to 0.8 in /tools/xdp (<a href="https://redirect.github.com/aws/s2n-quic/issues/2637">#2637</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/da13f32cf5071702aec48bff2cf4960e20fddee3"><code>da13f32</code></a> ci: Pin to older docker version (<a href="https://redirect.github.com/aws/s2n-quic/issues/2639">#2639</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/5f323b77155766d3878755e5de48972df4b47344...22434aa541781e42924bcf9856cd435250150344">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>
… quantifier's closure. (model-checking#4088) Previously, if we run Kani on the following harness: ```Rust #[kani::proof] fn test() { let quan = kani::forall!(|j in (0, 100)| j < 100); assert!(quan); } ``` it will panic: ``` thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs:827:43: index out of bounds: the len is 2 but the index is 2 ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
tautschnig
reviewed
Jun 27, 2025
tautschnig
reviewed
Jun 27, 2025
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.
Member
|
I'm actually quite confused by each of the CI failures seen here. The "Auto Label" problem we can easily work around by no longer marking it "Required." |
Contributor
|
I think what's happening is that it's trying to run the workflow from the branch we're merging into, so the stable branch, where the changes from 9d87281 don't exist. So I think you'd need to cherry pick that commit into See https://github.com/orgs/community/discussions/25746. |
Contributor
|
I think taking a step back: I may just recommend that you push directly to stable in this instance, instead of having to cherry pick over there just to get this PR merged; seems messy. Seems ok to do in this one-off instance, since we can see from the CI run here that regressions pass. |
Contributor
Author
|
That makes sense. Thanks for looking into this, @carolynzech. If I can get an approval, I'll merge the PR, and we can follow-up on any failures afterwards. |
Contributor
Author
|
Or maybe, I misunderstood what you meant by push directly to stable. Can you clarify? |
carolynzech
approved these changes
Jun 27, 2025
Contributor
carolynzech
left a comment
carolynzech
left a comment
There was a problem hiding this comment.
Approving with the understanding that these failures will be fixed once the workflow label changes are in the stable branch
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
12 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 0b68df0 and use the 1.88.0 channel.
This PR was created through:
git merge 0b68df0b8ed585b4bae9d6c07db64875137f1ae7 -X theirsrust-toolchain.tomlto1.88.0The rationale for picking 0b68df0 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.