Update features/verify-std branch #3508
Merged
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
In some cases, Kani would report a spurious counter example for cases where a match arm contained more than one pattern. This was fixed by changing how we handle storage lifecycle in model-checking#2995. This PR is only adding the related test to the regression. Resolves model-checking#3432 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…ing#3350) This PR adds support of copying memory initialization state without checks in-between. Every time a copy is performed, the tracked byte is non-deterministically switched. Resolves model-checking#3347 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…3453) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `ab9723a` to `80b93a7`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/80b93a7f1d187fef005c8c896ab99278b6865dbe"><code>80b93a7</code></a> chore: release 1.44.1 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2299">#2299</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/5e354d1e5c70cc5e94af80c19113710695a019e1"><code>5e354d1</code></a> build(deps): update toml requirement from 0.7 to 0.8 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2288">#2288</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/7175cd2165a188c6e0a0da44ff5e7b9a7e72bd52"><code>7175cd2</code></a> build(deps): update s2n-tls requirement from 0.2 to 0.3 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2298">#2298</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/ab9723a772f03a9793c9863e73c9a48fab3c5235...80b93a7f1d187fef005c8c896ab99278b6865dbe">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>
…ing#3452) Initially, points-to analysis tried to determine the body of an intrinsic (if it was available) to avoid enumerating them all. However, it turned out this logic was faulty, and the analysis attempted to query the body for intrinsics that didn't have it and ICEd. I added a couple of missing intrinsics, which had a side benefit of removing some duplicate assertion failures. Resolves model-checking#3447 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>
This extend model-checking#3120 with loop scanner that counts the number of loops in each function and the number of functions that contain loops. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…using backward iteration (model-checking#3438) This PR is a follow-up to model-checking#3374. Its main purpose is to properly handle a corner-case when multiple instrumentation instructions are added to the same instruction and not all of them are skipped during subsequent instrumentation. For example, if instrumentation is added after a terminator, a new basic block will be created, containing the added instrumentation. However, we currently only mark the first statement (or the terminator, if there are none) of the new basic block as skipped for subsequent instrumentation. That means that if instrumentation in this case contains some instrumentation targets itself, it will never terminate. Coincidentally, this is not currently the case, but could lead to subtle bugs if we decide to change instrumentation. In fact, this bug was only surfaced when I experimented with checking all memory accesses, which introduced significantly more checks. Ultimately, this shows that the current way to avoiding instrumentation is limited and needs to be changed. The PR introduces the following changes: - Group instrumentation into separate basic blocks instead of adding instructions one-by-one. - Use backward iteration to avoid having to reason about which instructions need to be skipped. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
We reverted the hierarchical logs a while ago (model-checking#2581) due to an outdated dependency that has since been fixed. I think this makes the logs much more readable, by indenting the logs given the scope. More than one scope makes the lines way too long, which I think it's harder to read. This is how the logs look without this change: ``` 2024-08-17T02:42:21.874979Z DEBUG CodegenFunction{name="kani::assert"}: kani_compiler::codegen_cprover_gotoc::utils::debug: handling kani::assert 2024-08-17T02:42:21.875008Z DEBUG CodegenFunction{name="kani::assert"}: kani_compiler::codegen_cprover_gotoc::utils::debug: variables: 2024-08-17T02:42:21.875026Z DEBUG CodegenFunction{name="kani::assert"}: kani_compiler::codegen_cprover_gotoc::utils::debug: let _0: Ty { id: 4, kind: RigidTy(Tuple([])) } ``` This is how it looks after this change: ``` ┐kani_compiler::codegen_cprover_gotoc::codegen::function::CodegenFunction name="kani::assert" ├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug handling kani::assert ├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug variables: ├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _0: Ty { id: 4, kind: RigidTy(Tuple([])) } ├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _1: Ty { id: 6, kind: RigidTy(Bool) } ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…tr` (model-checking#3448) We were missing a match arm for the case where a raw pointer to a string slice was created from a thin pointer and the string size. Resolves model-checking#3312 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>
…3460) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `80b93a7` to `8f7c04b`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/8f7c04be292f6419b38e37bd7ff67f15833735d7"><code>8f7c04b</code></a> ci: remove static page rebuild on push to main (<a href="https://redirect.github.com/aws/s2n-quic/issues/2304">#2304</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/a753efb9678562a0b75e41f27ef0de75783f5591"><code>a753efb</code></a> docs(s2n-quic): update CI docs (<a href="https://redirect.github.com/aws/s2n-quic/issues/2297">#2297</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/314813839672d3c2ad3c6033ce5b5c7062e0fe6a"><code>3148138</code></a> build(deps): update bindgen requirement from 0.69 to 0.70 in /tools/xdp (<a href="https://redirect.github.com/aws/s2n-quic/issues/2301">#2301</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/f70b834976aeeccdd07dd9f954288d683d250b89"><code>f70b834</code></a> build(deps): bump actions/checkout from 3 to 4 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2303">#2303</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/15fde00c8192eed85f051205c18eed75c7870823"><code>15fde00</code></a> ci: PR/Issue Dashboard (<a href="https://redirect.github.com/aws/s2n-quic/issues/2296">#2296</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/80b93a7f1d187fef005c8c896ab99278b6865dbe...8f7c04be292f6419b38e37bd7ff67f15833735d7">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>
The current `cargo deny` configuration in `deny.toml` uses several keys that have been deprecated. This PR removes the deprecated keys, and updates the deny action to use v2 (as well as renames it from `audit.yml` to `deny.yml`). The only semantic difference is that `cargo deny` will now reject crates that are maintained or have a notice on them, whereas previously, our configuration set both to "warn". As mentioned in the docs though, one can add an "ignore" if needed to bypass those advisories: https://embarkstudios.github.io/cargo-deny/checks/advisories/cfg.html#the-version-field-optional By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…king#3444) This PR introduces very basic support for memory initialization checks for unions. As of now, the following is supported: - Unions can be created - Union fields can be assigned to - Union fields can be read from - Unions can be assigned directly to another union For more information about planned functionality, see model-checking#3300 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…-checking#3464) With diffblue/cbmc#8413, CBMC will no longer create property checks for assigns clauses that are trivially true. We had CBMC-Nightly failing since August 17th given the CBMC change. This will bring CBMC-Nightly back to a passing state. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Looking at the RFC template file, I thought that the recommendation to leave the software design section empty referred to everything below the comment, rather than just that section. This PR updates the comment. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Upgrades the Kani coverage feature with the source-based code coverage implementation used in the Rust compiler. Rendered version available [here](https://github.com/adpaco-aws/rmc/blob/rfc-region-cov/rfc/src/rfcs/0011-source-coverage.md). Related to model-checking#2640 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…ng#3119) This PR replaces the line-based coverage instrumentation we introduced in model-checking#2609 with the standard source-based code coverage instrumentation performed by the Rust compiler. As a result, we now insert code coverage checks in the `StatementKind::Coverage(..)` statements produced by the Rust compiler during compilation. These checks include coverage-relevant information[^note-internal] such as the coverage counter/expression they represent [^note-instrument]. Both the coverage metadata (`kanimap`) and coverage results (`kaniraw`) are saved into files after the verification stage. Unfortunately, we currently have a chicken-egg problem with this PR and model-checking#3121, where we introduce a tool named `kani-cov` to postprocess coverage results. As explained in model-checking#3143, `kani-cov` is expected to be an alias for the `cov` subcommand and provide most of the postprocessing features for coverage-related purposes. But, the tool will likely be introduced after this change. Therefore, we propose to temporarily print a list of the regions in each function with their associated coverage status (i.e., `COVERED` or `UNCOVERED`). ### Source-based code coverage: An example The main advantage of source-based coverage results is their precision with respect to the source code. The [Source-based Code Coverage](https://clang.llvm.org/docs/SourceBasedCodeCoverage.html) documentation explains more details about the LLVM coverage workflow and its different options. For example, let's take this Rust code: ```rust 1 fn _other_function() { 2 println!("Hello, world!"); 3 } 4 5 fn test_cov(val: u32) -> bool { 6 if val < 3 || val == 42 { 7 true 8 } else { 9 false 10 } 11 } 12 13 #[cfg_attr(kani, kani::proof)] 14 fn main() { 15 let test1 = test_cov(1); 16 let test2 = test_cov(2); 17 assert!(test1); 18 assert!(test2); 19 } ``` Compiling and running the program with `rustc` and the `-C instrument-coverage` flag, and using the LLVM tools can get us the following coverage result:  In contrast, the `cargo kani --coverage -Zsource-coverage` command currently generates: ``` src/main.rs (main) * 14:1 - 19:2 COVERED src/main.rs (test_cov) * 5:1 - 6:15 COVERED * 6:19 - 6:28 UNCOVERED * 7:9 - 7:13 COVERED * 9:9 - 9:14 UNCOVERED * 11:1 - 11:2 COVERED ``` which is a verification-based coverage result almost equivalent to the runtime coverage results. ### Benchmarking We have evaluated the performance impact of the instrumentation using the `kani-perf.sh` suite (14 benchmarks). For each test, we compare the average time to run standard verification against the average time to run verification with the source-based code coverage feature enabled[^note-line-evaluation]. The evaluation has been performed on an EC2 `m5a.4xlarge` instance running Ubuntu 22.04. The experimental data has been obtained by running the `kani-perf.sh` script 10 times for each version (`only verification` and `verification + coverage`), computing the average and standard deviation. We've split this data into `small` (tests taking 60s or less) and `large` (tests taking more than 60s) and drawn the two graphs below. #### Performance comparison - `small` benchmarks  #### Performance comparison - `large` benchmarks  #### Comments on performance Looking at the small tests, the performance impact seems negligible in such cases. The difference is more noticeable in the large tests, where the time to run verification and coverage can take 2x or even more. It wouldn't be surprising that, as programs become larger, the complexity of the coverage checking grows exponentially as well. However, since most verification jobs don't take longer than 30min (1800s), it's OK to say that coverage checking represents a 100-200% slowdown in the worst case w.r.t. standard verification. It's also worth noting a few other things: * The standard deviation remains similar in most cases, meaning that the coverage feature doesn't have an impact on their stability. * We haven't tried any SAT solvers other than the ones used by default for each benchmark. It's possible that other solvers perform better/worse with the coverage feature enabled. ### Call-outs * The soundness issue documented in model-checking#3441. * The issue with saving coverage mappings for non-reachable functions documented in model-checking#3445. * I've modified the test cases in `tests/coverage/` to test this feature. Since this technique is simpler, we don't need that many test cases. However, it's possible I've left some test cases which don't contribute much. Please let me know if you want to add/remove a test case. [^note-internal]: The coverage mappings can't be accessed through the StableMIR interface so we retrieve them through the internal API. [^note-instrument]: The instrumentation replaces certain counters with expressions based on other counters when possible to avoid a part of the runtime overhead. More details can be found [here](https://github.com/rust-lang/rustc-dev-guide/blob/master/src/llvm-coverage-instrumentation.md#mir-pass-instrumentcoverage). Unfortunately, we can't avoid instrumenting expressions at the moment. [^note-line-evaluation]: We have not compared performance against the line-based code coverage feature because it doesn't seem worth it. The line-based coverage feature is guaranteed to include more coverage checks than the source-based one for any function. In addition, source-based results are more precise than line-based ones. So this change represents both a quantitative and qualitative improvement. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Upgrades toolchain to 08/28 Culprit upstream changes: 1. rust-lang/rust#128812 2. rust-lang/rust#128703 3. rust-lang/rust#127679 4. rust-lang/rust-clippy#12993 5. rust-lang/cargo#14370 6. rust-lang/rust#128806 Resolves model-checking#3429 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…ecking#3419) This PR is a follow-up to model-checking#3374. It introduces the following changes: - Instrument more writes to avoid the case when points-to analysis overapproximates too much. - Add extra tests featuring safe abstractions from standard library. 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 8/29. Culprit upstream changes: rust-lang/rust#129686 Resolves model-checking#3466 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-08-29 to nightly-2024-08-30 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
…l-checking#3457) This is the first part needed for us to add support to stubbing trait implementations (model-checking#1997) and primitive types (model-checking#2646). After this change, we need to change stubs to accept a `FnResolution` instead of `FnDef`. We also need to find out how to retrieve methods of primitive types. 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> Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
…cking#3470) This PR partially integrates uninitialized memory checks into the `verify_std` pipeline, which makes it possible to enable them for the Rust Standard Library verification. Changes: - Move `mem_init.rs` library code into `kani_core`. - Add a conditional compilation flag to disable uninitialized memory checks whenever some functionality is not yet supported. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Updates toolchain to 9/1. This couldn't run automatically because of model-checking#3476. 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>
…3481) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `8f7c04b` to `1ff3a9c`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/1ff3a9c8adee30346537698c7b2a12279facd2d3"><code>1ff3a9c</code></a> chore: import 8/29 version (<a href="https://redirect.github.com/aws/s2n-quic/issues/2311">#2311</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/b6ca57b00f39b3eb816cfaed3029606393dbcc44"><code>b6ca57b</code></a> test(s2n-quic-core): revert to bigger length for Kani test (<a href="https://redirect.github.com/aws/s2n-quic/issues/2312">#2312</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/24089b41a31e6711a47255df392e0ba3dbc60d66"><code>24089b4</code></a> chore: release 1.45.0 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2310">#2310</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/a74e9cb52e647d4644d78ce3d8bc2407160a4a80"><code>a74e9cb</code></a> fix(s2n-quic-transport): don't let cwnd drop below initial cwnd when MTU decr...</li> <li><a href="https://github.com/aws/s2n-quic/commit/9af5d196e82811d0b520f5110c39a36bb1d02f88"><code>9af5d19</code></a> docs(s2n-quic): fix link to compliance report in CI doc</li> <li><a href="https://github.com/aws/s2n-quic/commit/acd3fe49d9a682f7cff1cfff9df8866e661d196d"><code>acd3fe4</code></a> build(deps): update ring requirement from 0.16 to 0.17 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2287">#2287</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/2869c1941e4859b295bec793db9754c9a6e791cd"><code>2869c19</code></a> build(deps): update lru requirement from 0.10 to 0.12 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2286">#2286</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/b3a10a1467ce46d84448ba94721d00e705174344"><code>b3a10a1</code></a> fix(s2n-quic): ConfirmComplete with handshake de-duplication (<a href="https://redirect.github.com/aws/s2n-quic/issues/2307">#2307</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/b4ba62d0b90dbd965a13ccbf421ff5298340ddf1"><code>b4ba62d</code></a> fix(s2n-quic-transport): wait until handshake is confirmed to start MTU probi...</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/8f7c04be292f6419b38e37bd7ff67f15833735d7...1ff3a9c8adee30346537698c7b2a12279facd2d3">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 Rust toolchain from nightly-2024-09-01 to nightly-2024-09-02 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
Update Rust toolchain from nightly-2024-09-02 to nightly-2024-09-03 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
RFC for the `kani list` subcommand. I saw the comment [in the template](https://github.com/model-checking/kani/blob/main/rfc/src/template.md#software-design) to leave the Software Design section empty, but I was looking at the raw MD file and made the mistake of thinking it referred to all sections below the comment. In other words, I thought when it said "We recommend you to leave this empty for the first version of your RFC" it meant that everything below the comment should be empty (so Rationale, Open Questions, and Future Work) and not Software Design. I realized my mistake when I was making this PR, but I figured I may as well leave it since I already wrote it. I [opened a PR](model-checking#3462) to update the comment. Resolves [model-checking#2573](model-checking#2573), [model-checking#1612](#model-checking#1612). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
model-checking#2239 and model-checking#3022 are resolved in Kani v0.5.4. Add tests for them. Resolves model-checking#2239 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Add the following to the book: - **Reference section on contracts**. The point of this section is not to be an exhaustive explanation--we have good documentation on contracts already, and we don't want to maintain it in two places. The goal of the section is to give readers an intuition for the main idea and then direct them to more detailed resources. - **Add a reference to the blog**--it's a good resource to learn about Kani and it would be nice to have an easier way to find it. Inspired by [this post](https://users.rust-lang.org/t/can-somebody-explain-how-kani-verifier-works/113918). - **Move the crates documentation earlier.** This partly addresses [model-checking#3029](model-checking#3029) by at least making our crates documentation more visible in the book. (I don't have this PR as resolving that issue, since we would need to actually publish the docs on `crates.io` to do that.) 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 introduces support for memory initialization checks for unions passed across the function boundary. Whenever a union is passed as an argument, we need to make sure that its initialization state is preserved. Unlike pointers, unions do not have a stable memory address which could identify them in shadow memory. Hence, we need to pass extra information across function boundary since unions are passed “by value”. We introduce a global variable to store the previous address of unions passed as function arguments, which allows us to effectively tie the initialization state of unions passed between functions. This struct is written to by the caller and read from by the callee. For more information about planned functionality, see model-checking#3300 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
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 <tautschn@amazon.com> Co-authored-by: Michael Tautschnig <mt@debian.org>
Fixes the macro expansion for contracts to properly place history expressions. ## Problem Before this PR, instantiations of "remembers variables" (i.e., the variables that save the value before the function executes) were always put *above* any statements from previous macro expansions. For example, for this code (from model-checking#3359): ```rust #[kani::requires(val < i32::MAX)] #[kani::ensures(|result| *result == old(val + 1))] pub fn next(mut val: i32) -> i32 { val + 1 } ``` Kani would first expand the `requires` attribute and insert `kani::assume(val < i32::MAX)`. The expansion of `ensures` would then put the remembers variables first, generating this: ``` let remember_kani_internal_1e725538cd5566b8 = val + 1; kani::assume(val < i32::MAX); ``` which causes an integer overflow because we don't restrict the value of `val` before adding 1. Instead, we want: ``` kani::assume(val < i32::MAX); let remember_kani_internal_1e725538cd5566b8 = val + 1; ``` ## Solution The solution is to insert the remembers variables immediately after preconditions--that way, they respect the preconditions but are still declared before the function under contract executes. When we're expanding an `ensures` clause, we iterate through each of the already-generated statements, find the position where the preconditions end, then insert the remembers variables there. For instance: ``` kani::assume(x < 100); kani::assume(y < 10); kani::assume(x + y < 105); <-- remembers variables go here --> let _wrapper_arg = ... ``` --- Resolves model-checking#3359 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
These are the auto-generated release notes: ## What's Changed * Update CBMC build instructions for Amazon Linux 2 by @tautschnig in model-checking#3431 * Handle intrinsics systematically by @artemagvanian in model-checking#3422 * Bump tests/perf/s2n-quic from `445f73b` to `ab9723a` by @dependabot in model-checking#3434 * Automatic cargo update to 2024-08-12 by @github-actions in model-checking#3433 * Actually apply CBMC patch by @tautschnig in model-checking#3436 * Update features/verify-rust-std branch by @feliperodri in model-checking#3435 * Add test related to issue 3432 by @celinval in model-checking#3439 * Implement memory initialization state copy functionality by @artemagvanian in model-checking#3350 * Bump tests/perf/s2n-quic from `ab9723a` to `80b93a7` by @dependabot in model-checking#3453 * Make points-to analysis handle all intrinsics explicitly by @artemagvanian in model-checking#3452 * Automatic cargo update to 2024-08-19 by @github-actions in model-checking#3450 * Add loop scanner to tool-scanner by @qinheping in model-checking#3443 * Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in model-checking#3438 * Re-enabled hierarchical logs in the compiler by @celinval in model-checking#3449 * Fix ICE due to mishandling of Aggregate rvalue for raw pointers to `str` by @celinval in model-checking#3448 * Automatic cargo update to 2024-08-26 by @github-actions in model-checking#3459 * Bump tests/perf/s2n-quic from `80b93a7` to `8f7c04b` by @dependabot in model-checking#3460 * Update deny action by @zhassan-aws in model-checking#3461 * Basic support for memory initialization checks for unions by @artemagvanian in model-checking#3444 * Adjust test patterns so as not to check for trivial properties by @tautschnig in model-checking#3464 * Clarify comment in RFC Template by @carolynzech in model-checking#3462 * RFC: Source-based code coverage by @adpaco-aws in model-checking#3143 * Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in model-checking#3119 * Upgrade toolchain to 08/28 by @jaisnan in model-checking#3454 * Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in model-checking#3419 * Upgrade Toolchain to 8/29 by @carolynzech in model-checking#3468 * Automatic toolchain upgrade to nightly-2024-08-30 by @github-actions in model-checking#3469 * Extend name resolution to support qualified paths (Partial Fix) by @celinval in model-checking#3457 * Partially integrate uninit memory checks into `verify_std` by @artemagvanian in model-checking#3470 * Update Toolchain to 9/1 by @carolynzech in model-checking#3478 * Automatic cargo update to 2024-09-02 by @github-actions in model-checking#3480 * Bump tests/perf/s2n-quic from `8f7c04b` to `1ff3a9c` by @dependabot in model-checking#3481 * Automatic toolchain upgrade to nightly-2024-09-02 by @github-actions in model-checking#3479 * Automatic toolchain upgrade to nightly-2024-09-03 by @github-actions in model-checking#3482 * RFC for List Subcommand by @carolynzech in model-checking#3463 * Add tests for fixed issues. by @carolynzech in model-checking#3484 **Full Changelog**: model-checking/kani@kani-0.54.0...kani-0.55.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
RFC for loop contracts in Kani. Rendered version available [here](https://github.com/qinheping/kani/blob/rfc-loop-contracts/rfc/src/rfcs/0012-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: Celina G. Val <celinval@amazon.com>
) The following security advisory has been issued today regarding the `proc-macro-error` crate which is causing our CI to fail: https://rustsec.org/advisories/RUSTSEC-2024-0370 Replacing the crate with `proc-macro-error2` which is a fork of that crate. 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-09-03 to nightly-2024-09-04 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>
Update Rust toolchain from nightly-2024-09-04 to nightly-2024-09-05 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
Update the `cmake` configuration step used for building CBMC to include cadical. Resolves model-checking#3497 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Addresses @jaisnan's feedback on list RFC--change `human` output to `pretty` and fix Kani version typo. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…cking#3496) Previously, Kani was not able to resolve methods that belong to primitive types, which would not allow users to specify primitive types as stub target, neither for contracts. Thus, extend the name resolution to be able to convert a type expression into a `Ty` for primitive types, and add a new method to search for function implementation for primitive types. I also moved the type resolution logic to its own module to make it a bit cleaner. Resolves model-checking#2646 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-09-05 to nightly-2024-09-06 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
As suggested in GnomedDev/proc-macro-error-2#1 (comment), turning on the `nightly` feature for `proc-macro-error2` to restore the previous error message for `derive(Arbitrary)`. Resolves model-checking#3495 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#128776: The `TreatParams` enum variants were renamed. Resolves model-checking#3503 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>
Update Rust toolchain from nightly-2024-09-07 to nightly-2024-09-08 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
carolynzech
merged commit cda1b30
into
model-checking:features/verify-rust-std
89 of 92 checks passed
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 PR isn't meant to be merged. Just checking if CI passes, then I will force push these changes.
Tests passed locally:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.