Update features/verify-rust-std branch to 11-06 #3690
Closed
Conversation
This file contains 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
Update Rust toolchain from nightly-2024-10-22 to nightly-2024-10-23 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
This is a clean-up PR: I noticed that the `run_piped` function has an `Option` layer that is unnecessary: - If the process launching fails, it returns an error. - If it succeeds, it returns `Ok(Some(process))` Thus, the `Option` layer is always `Some`. The main change is updating the function signature from: ```rust pub fn run_piped(verbosity: &impl Verbosity, mut cmd: Command) -> Result<Option<Child>> ``` to: ```rust pub fn run_piped(verbosity: &impl Verbosity, mut cmd: Command) -> Result<Child> ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This is a follow-up on #3514. As @celinval suggested ([here](#3514 (comment))), renaming all user-facing options from "Aeneas" to Lean. Inside the Kani compiler which is only concerned with producing LLBC (and doesn't know about Lean/Aeneas), I'm renaming the relevant feature from `aeneas` to `llbc`, and the backend is now called the LLBC backend as opposed to the Aeneas backend. Towards #3585 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…ait objects (#3636) Add a match arm for the `AggregateKind::RawPtr(TyKind::RigidTy(RigidTy::Dynamic(..)))` case. Pointers to trait objects [are fat](https://github.com/rust-lang/rust/blob/master/library/core/src/ptr/metadata.rs#L20-#L27), so generate a fat pointer for the rvalue. Resolves #3631 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-2024-10-23 to nightly-2024-10-24 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
I'm adding a few fix-me tests that I bumped into while working on #3363. Most of them will be fixed by #3363, except the one related to #3370. The original PR is already quite large, so I decided to just push all of these as fixme tests for now. This is now ready for review! 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: Felipe R. Monteiro <felisous@amazon.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Carolyn Zech <cmzech@amazon.com>
DFCC should be called only once. This PR combined the two DCFF calls into one. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This PR adds another step to the `cargo bundle` command so that `kani-cov` is built in release mode and then included in the bundle. This will allow users to call `kani-cov` once Kani has been setup. I have manually tested it works by running: ``` cargo bundle tar -xzf kani-0.56.0-x86_64-unknown-linux-gnu.tar.gz ls kani-0.56.0/bin/ ``` This showed `kani-cov` along with other binaries like `cbmc` and `kissat`. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
In loop contracts transformation, we want to visit non-loop blocks before visiting loop blocks. So we pop `loop_queue` only when `queue` is empty. We should use `or_else` instead of `or` which always pop the front of `loop_queue`. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Culprit PR: rust-lang/rust#131985 The automatic PR failed because the culprit PR removed the `host_param_index` field that we used in the `contract_host_param` function. We needed the `contract_host_param` function in the first place because previously, Rust would add a `<const HOST: bool>` parameter to a function's `GenericArgs` to handle trait constness (c.f. #3258). The culprit PR [removed that argument](https://github.com/rust-lang/rust/pull/131985/files#diff-0a61b538a3cec072c76fecae4635af6a12ec3256860029ac70549c2aa53ab394L1527), so our logic to find and remove this parameter during stubbing is no longer necessary. Resolves #3645 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-2024-10-25 to nightly-2024-10-26 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
Update Rust toolchain from nightly-2024-10-26 to nightly-2024-10-27 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `cd0314b` to `ed9db08`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/ed9db08c4a6fc1fa439d91871ef07ec770293b7b"><code>ed9db08</code></a> test(s2n-quic): failure is not fatal for dedupe (<a href="https://redirect.github.com/aws/s2n-quic/issues/2355">#2355</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/cd0314b87de035fdd80573625ba643f6d5d75722...ed9db08c4a6fc1fa439d91871ef07ec770293b7b">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> Co-authored-by: Zyad Hassan <zyadh@amazon.com>
Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Update Rust toolchain from nightly-2024-10-27 to nightly-2024-10-28 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
This is a mitigation for #3611 till we determine the reason for the high memory consumption. Since this test frequently fails due to running out of memory when running locally, reducing the number of object bits. Without this change, memory usage is ~9 GB: ``` SUMMARY: ** 0 of 182 failed (1 unreachable) VERIFICATION:- SUCCESSFUL Verification Time: 30.51689s Complete - 1 successfully verified harnesses, 0 failures, 1 total. Command being timed: "kani refcell.rs -Zfunction-contracts" User time (seconds): 25.17 System time (seconds): 8.07 Percent of CPU this job got: 100% Elapsed (wall clock) time (h:mm:ss or m:ss): 0:33.20 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 9196056 Average resident set size (kbytes): 0 Major (requiring I/O) page faults: 0 Minor (reclaiming a frame) page faults: 3464218 Voluntary context switches: 1834 Involuntary context switches: 128 Swaps: 0 File system inputs: 0 File system outputs: 5400 Socket messages sent: 0 Socket messages received: 0 Signals delivered: 0 Page size (bytes): 4096 Exit status: 0 ``` and with this change, it's about ~600MB: ``` VERIFICATION:- SUCCESSFUL Verification Time: 2.0234118s Complete - 1 successfully verified harnesses, 0 failures, 1 total. Command being timed: "kani refcell.rs -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 12" User time (seconds): 3.82 System time (seconds): 0.92 Percent of CPU this job got: 100% Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.72 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 613636 Average resident set size (kbytes): 0 Major (requiring I/O) page faults: 60 Minor (reclaiming a frame) page faults: 289631 Voluntary context switches: 1882 Involuntary context switches: 16 Swaps: 0 File system inputs: 11832 File system outputs: 5400 Socket messages sent: 0 Socket messages received: 0 Signals delivered: 0 Page size (bytes): 4096 Exit status: 0 ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Move `any_slice_from_array` to `kani_core` so that we can call them in verify-rust-std (an example harness in model-checking/verify-rust-std#122). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Culprit PR identified by @tautschnig: rust-lang/rust#132252 Resolves #3657 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This PR adds a new option, `--cbmc-timeout` which can be used for setting a timeout for the CBMC run. The timeout applies on a per-harness basis in the Kani run. The implementation uses [tokio ](https://tokio.rs/) to perform non-blocking reads from the CBMC process's `stdout` so that the timeout can be checked asynchronously. **Call-outs:** There are other names I considered for the option: - `--harness-timeout`: This makes it clearer that the timeout applies to each individual harness (and not to the overall Kani run). It doesn't indicate that the timeout only applies to the CBMC portion of the flow though. - `--engine-timeout`: This makes it a bit more general across multiple engine/backends. The notion of an engine is not really part of the Kani jargon currently though, so might not be clear to users. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Changes required due to rust-lang/rust#132157 (Remove detail from label/note that is already available in other note). Resolves: #3659 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Culprit upstream change: rust-lang/rust#132338 Resolves #3664 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Changes required due to rust-lang/rust#132246 (Rename `rustc_abi::Abi` to `BackendRepr`). Resolves: #3669 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-2024-11-01 to nightly-2024-11-02 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
Update Rust toolchain from nightly-2024-11-02 to nightly-2024-11-03 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
) Directly question the layout if it is uninhabited. This makes Kani more resilient to changes in the upstream rustc toolchain, as the convenience function which exposes this is precisely to allow compilers to not fixate as much on the innermost details of rustc's codegen process. Found while reviewing #3671
Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com>
Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `192de7d` to `65d55a4`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/65d55a48ae4916c2a0c4ab9a90631668ba8ea23f"><code>65d55a4</code></a> test(s2n-quic-dc): add tests for map events (<a href="https://redirect.github.com/aws/s2n-quic/issues/2363">#2363</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/fcdb9142a898764816d52f5a09b6e9eb26a0dff8"><code>fcdb914</code></a> feat(s2n-quic-dc): add map events (<a href="https://redirect.github.com/aws/s2n-quic/issues/2362">#2362</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/fad92d2b6d54673ff65cc9c2bd82e21399d4663f"><code>fad92d2</code></a> fix(s2n-quic-core): always wake application on available datagram capacity (#...</li> <li><a href="https://github.com/aws/s2n-quic/commit/afc56cd96b7693179bce0e2bc110f184db1f109c"><code>afc56cd</code></a> refactor(s2n-quic-dc): put map impl behind trait (<a href="https://redirect.github.com/aws/s2n-quic/issues/2361">#2361</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/e2ac09e6d4483a509e15357eb4a5df5990b040f0"><code>e2ac09e</code></a> feat(s2n-quic-dc): export event module (<a href="https://redirect.github.com/aws/s2n-quic/issues/2360">#2360</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/01cbb44d6d9cb36723b44f4cb16afc9f494b9be2"><code>01cbb44</code></a> fix(s2n-quic-dc): wait to insert in peer map until handshake completes (<a href="https://redirect.github.com/aws/s2n-quic/issues/2358">#2358</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/6c7057f68d76724266a952868574874a62225a6e"><code>6c7057f</code></a> feat(s2n-quic-platform): emit socket events (<a href="https://redirect.github.com/aws/s2n-quic/issues/2356">#2356</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/192de7d2efb5a0eceab79f68870b162a1ecb1986...65d55a48ae4916c2a0c4ab9a90631668ba8ea23f">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>
Update dependencies following Audit workflow failure triggerd by `hasbrown` 0.15.0 being yanked because of a bad `borsh` implementation. 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>
Resolves #3356 1. Changes allow for directory with individual output of files named by the full harness name. --output-into-files command line argument will allow for placing all output of individual harnesses into files named by the full harness pretty_name. The output directory is either --target-dir or a hard coded default: "kani_output" directory. (These can be changed if there is a better interface). Still prints output to std::out exactly as previous. 2. Previously, all output was placed into std::out. This will allow for some control over output. It will also enable easier parsing of harness output. 3. Only solved #3356 but could be expanded to include more features. 4. Ran manually to check the flags and output behaved as expected. Indeed: --output-into-files enabled will place output into individual files, disabled will not --output-terse will create terse output to command line, regular output to individual files if --output-into-files is enabled. --target-dir will place output into target-dir directory when --output-into-files is enabled, and will not place file output when disabled. Let me know if you need specific explanations of code segments, a clean list of all the testing configurations, or any feature enhancement for greater configuration options. 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: Alexander Aghili <Alexsky2@LEAHs-MacBook-Pro.local> Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Co-authored-by: Celina G. Val <celinval@amazon.com>
This PR advances the Charon submodule commit from 2024-09-02 to 2024-11-04. The main changes are due to: - AeneasVerif/charon#346: This changed some terminators into statements. - AeneasVerif/charon#407: The removal of some dependence on rustc code in the Charon library. Towards: #3585 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This PR adds support for the [`float_to_int_unchecked`](https://doc.rust-lang.org/std/intrinsics/fn.float_to_int_unchecked.html) intrinsic for `f32` and `f64`. Towards #3629 Keeping it as draft till I add more tests. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
For that, change the function to cast the given pointer to a thin pointer of type `*const ()`, and use that instead. Resolves #3665 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Upgrade CBMC to its latest release. Co-authored-by: qinheping <16714939+qinheping@users.noreply.github.com> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
qinheping
changed the title
qinheping
changed the title
|
I don't think we need this one too. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This is not intended for a merge. We want to ensure that all CI checks pass and review the full list of commits before updating this branch.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.