-
Notifications
You must be signed in to change notification settings - Fork 86
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Loop Contracts Annotation for While-Loop #3151
base: main
Are you sure you want to change the base?
Loop Contracts Annotation for While-Loop #3151
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think I'm missing the big picture here, since the PR itself is currently a no-op and the attribute itself has no documentation.
Release notes are the following: ### Major Changes * Fix compilation issue with proc_macro2 (v1.0.80+) and Kani v0.49.0 (model-checking#3138). ### What's Changed * Implement valid value check for `write_bytes` by @celinval in model-checking#3108 * Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval **Full Changelog**: model-checking/kani@kani-0.49.0...kani-0.50.0
…-checking#3149) The toolchain upgrade itself didn't require any modification, but it looks like the rust toolchain script includes any untracked files to the PR, which is the root cause of the model-checking#3146 CI failure. Thus, I made the following changes (each one of them in its own commit): 1. Moved the upgrade step to its own script. 2. Added a bit of debugging and doc to the script. 3. Added a new step that cleans the workspace before the PR creation. 4. Actually update the toolchain. 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-04-18 to nightly-2024-04-19 without any other source changes. This is an automatically generated pull request. If any of the CI checks fail, manual intervention is required. In such a case, review the changes at https://github.com/rust-lang/rust from rust-lang/rust@becebb3 up to rust-lang/rust@e3181b0.
I would like to propose that we stabilize the cover statement as is. Any further improvements or changes can be done separately, with or without an RFC. I am also updating the contracts RFC status since parts of it have been integrated to Kani, but it is still unstable. ### Call-out This PR requires at least 2 approvals.
Update Rust toolchain from nightly-2024-04-19 to nightly-2024-04-20 without any other source changes. This is an automatically generated pull request. If any of the CI checks fail, manual intervention is required. In such a case, review the changes at https://github.com/rust-lang/rust from rust-lang/rust@e3181b0 up to rust-lang/rust@f9b1614.
…3140) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `2d5e891` to `5f88e54`.
Dependency upgrade resulting from `cargo update`.
Update Rust toolchain from nightly-2024-04-20 to nightly-2024-04-21 without any other source changes. This is an automatically generated pull request. If any of the CI checks fail, manual intervention is required. In such a case, review the changes at https://github.com/rust-lang/rust from rust-lang/rust@f9b1614 up to rust-lang/rust@dbce3b4.
…3159) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `5f88e54` to `9730578`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/9730578c0d562d80bbbe663161b3a5408ed3116c"><code>9730578</code></a> chore: release 1.37.0 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2187">#2187</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/b862ad982859f03d7e45f5d6291f749697a04a0f"><code>b862ad9</code></a> s2n-quic-dc: initial commit (<a href="https://redirect.github.com/aws/s2n-quic/issues/2185">#2185</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/e0f224b848e725f94e7c9050ca1dfec16eb39bd8"><code>e0f224b</code></a> feat(s2n-quic-core): allow forced PTO transmissions (<a href="https://redirect.github.com/aws/s2n-quic/issues/2130">#2130</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/bfb921daed2330c21202d441594a538458a3e5f2"><code>bfb921d</code></a> feat(s2n-quic-core): Add ability to create an incremental reader initialized ...</li> <li><a href="https://github.com/aws/s2n-quic/commit/23b07e41b6ead9621972cb0687fc3610540f7f77"><code>23b07e4</code></a> feat(s2n-quic): allow disabling active connection migration support (<a href="https://redirect.github.com/aws/s2n-quic/issues/2182">#2182</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/5f88e549821518e71b550faf353a8b9970a29deb...9730578c0d562d80bbbe663161b3a5408ed3116c">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>
Fixes cargo audit CI job by updating `rustix`. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
We had a spurious update attempt logged in model-checking#3155 for the job prior to this fix would empty out the version strings. This was caused by use of undefined variables. Resolves: model-checking#3155 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: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com>
…3166) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `9730578` to `1436af7`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/1436af712b6e73edc11640dc7c3cae23e456c0a8"><code>1436af7</code></a> ci: Remove neqo from required resumption test clients (<a href="https://redirect.github.com/aws/s2n-quic/issues/2191">#2191</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/c0bcef639de0e2a6a89202e84c9933d99d431047"><code>c0bcef6</code></a> build: remove --cfg s2n_quic_unstable (<a href="https://redirect.github.com/aws/s2n-quic/issues/2190">#2190</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/fed54a59dcfdbc70e7c3c2d4b1cf3c4991ad4403"><code>fed54a5</code></a> feat(s2n-quic-platform): make message methods public (<a href="https://redirect.github.com/aws/s2n-quic/issues/2189">#2189</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/9730578c0d562d80bbbe663161b3a5408ed3116c...1436af712b6e73edc11640dc7c3cae23e456c0a8">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>
…hecking#3134) The Rust specification does not guarantee that ZST-typed symbols are backed by unique objects, and `rustc` appears to make use of this as can be demonstrated for both locals and statics. For parameters no such example has been found, but as there remains a lack of a guarantee we err on the safe side. Resolves: model-checking#3129
This PR modifies the pattern used to exclude files from the copyright check for `expected` files. This ensures we check the copyright in files under `tests/expected/` while it skips the check for `expected` and `*.expected` files. It also adds/modifies copyright headers for some files that weren't being checked until now. Resolves model-checking#3141
…del-checking#3169) This is an additional fix for model-checking#3098. With this fix, Kani should be able to check for contracts using modifies clauses that contain references to types that doesn't implement `kani::Arbitrary`. The verification will still fail if the same contract is used as a verified stub. --------- Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com>
…3174) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `1436af7` to `6dd41e0`. <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/aws/s2n-quic/commit/6dd41e09195bc22dbac93a48f8ab35f8063726dc"><code>6dd41e0</code></a> build: fix clippy warnings for 1.78 (<a href="https://redirect.github.com/aws/s2n-quic/issues/2199">#2199</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/de5c33e800ffff14c235ed0ae7d695222f84dcca"><code>de5c33e</code></a> refactor(s2n-quic-core): improve reassembler error handling (<a href="https://redirect.github.com/aws/s2n-quic/issues/2197">#2197</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/b085808f4c898f6d4d4e68b14d6a762170fb19b1"><code>b085808</code></a> chore(s2n-quic-crypto): remove custom aesgcm implementation (<a href="https://redirect.github.com/aws/s2n-quic/issues/2186">#2186</a>)</li> <li><a href="https://github.com/aws/s2n-quic/commit/7188ce4081096256267e44d63f532a40d2c7df64"><code>7188ce4</code></a> feat(dc): DcSupportedVersions transport parameter (<a href="https://redirect.github.com/aws/s2n-quic/issues/2193">#2193</a>)</li> <li>See full diff in <a href="https://github.com/aws/s2n-quic/compare/1436af712b6e73edc11640dc7c3cae23e456c0a8...6dd41e09195bc22dbac93a48f8ab35f8063726dc">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>
We should try to produce a source location wherever possible to ease debugging and coverage reporting.
Update Cargo.lock with the following package version changes: ``` anyhow 1.0.82 -> 1.0.83 getrandom 0.2.14 -> 0.2.15 num-bigint 0.4.4 -> 0.4.5 ryu 1.0.17 -> 1.0.18 syn 2.0.60 -> 2.0.61 winnow 0.6.7 -> 0.6.8 ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
For reference, here is the auto-generated changelog ## What's Changed * Upgrade toolchain to 2024-04-18 and improve toolchain workflow by @celinval in model-checking#3149 * Automatic toolchain upgrade to nightly-2024-04-19 by @github-actions in model-checking#3150 * Stabilize cover statement and update contracts RFC by @celinval in model-checking#3091 * Automatic toolchain upgrade to nightly-2024-04-20 by @github-actions in model-checking#3154 * Bump tests/perf/s2n-quic from `2d5e891` to `5f88e54` by @dependabot in model-checking#3140 * Automatic cargo update to 2024-04-22 by @github-actions in model-checking#3157 * Automatic toolchain upgrade to nightly-2024-04-21 by @github-actions in model-checking#3158 * Bump tests/perf/s2n-quic from `5f88e54` to `9730578` by @dependabot in model-checking#3159 * Fix cargo audit error by @jaisnan in model-checking#3160 * Fix cbmc-update CI job by @tautschnig in model-checking#3156 * Automatic cargo update to 2024-04-29 by @github-actions in model-checking#3165 * Bump tests/perf/s2n-quic from `9730578` to `1436af7` by @dependabot in model-checking#3166 * Do not assume that ZST-typed symbols refer to unique objects by @tautschnig in model-checking#3134 * Fix copyright check for `expected` tests by @adpaco-aws in model-checking#3170 * Remove kani::Arbitrary from the modifies contract instrumentation by @feliperodri in model-checking#3169 * Automatic cargo update to 2024-05-06 by @github-actions in model-checking#3172 * Bump tests/perf/s2n-quic from `1436af7` to `6dd41e0` by @dependabot in model-checking#3174 * Avoid unnecessary uses of Location::none() by @tautschnig in model-checking#3173 **Full Changelog**: model-checking/kani@kani-0.50.0...kani-0.51.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: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's looking good but I'm also missing the big picture when it comes to
- the general approach to loop invariants - are we planning on doing the same for
for
loops? - the code generation for invariant/latch blocks - do you describe this transformation in the RFC?
- postprocessing of reachability checks - not sure what's being done or why it's needed
kani-compiler/src/codegen_cprover_gotoc/context/loop_contracts_ctx.rs
Outdated
Show resolved
Hide resolved
kani-compiler/src/codegen_cprover_gotoc/context/loop_contracts_ctx.rs
Outdated
Show resolved
Hide resolved
kani-compiler/src/codegen_cprover_gotoc/context/loop_contracts_ctx.rs
Outdated
Show resolved
Hide resolved
@celinval @feliperodri , I refactored the implementation with closure. It is ready for review now. |
Can you please update the description of the PR with an overview of the approach you implemented? Thanks |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is awesome! Looking forward to merging this!
kani-compiler/src/codegen_cprover_gotoc/overrides/loop_contracts_hooks.rs
Outdated
Show resolved
Hide resolved
/// kani_register_loop_contract(kani_loop_invariant) | ||
/// while guard { | ||
/// loop_body; | ||
/// kani_register_loop_contract(||->bool{true}); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
wait, why do you register a dummy closure down here?
I think we want to redefine the closure so it captures the arguments again and don't violate the borrow checker. Something like:
let kani_loop_invariant_entry = || -> bool {inv};
kani_register_loop_contract(kani_loop_invariant_entry)
while guard {
loop_body;
let kani_loop_invariant_latch = || -> bool {inv};
kani_register_loop_contract(kani_loop_invariant_latch);
}
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The idea of this implementation (and also the loop contracts in CBMC) is that we want to use one single expression as the loop invariants, and let CBMC do the transformation: rewrite loop to if, duplicate the loop invariant (check and induction assumption) to the entry of the loop as base case, instrument havocing instructions after the induction assumption, and check the loop invariant at the end of the loop.
The one single loop invariant expression in my mind should be kani_loop_invariant
which is || -> bool {inv}
. As it will be called before the entry of the loop after the transformation, it should be assigned before the loop. However, without dummy call, expanding the macro in the following way will violate the borrow check.
let kani_loop_invariant = || -> bool {inv};
while guard {
loop_body;
kani_register_loop_contract(kani_loop_invariant);
}
So I choose to use a dummy call as a place holder and later replace it with the actual call during MIR transform.
/// to | ||
/// | ||
/// ```ignore | ||
/// let kani_loop_invariant = || -> bool {inv}; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
don't we need to check the invariant before the loop entry?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We annotate the loop invariants in the loop latch goto and let CBMC instrument the checks.
/// let kani_loop_invariant = || -> bool {inv}; | ||
/// while guard { | ||
/// loop_body; | ||
/// kani_register_loop_contract(kani_loop_invariant); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This could break the aliasing and ownership model.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I understand that it will violate the borrow check in Rust. But is it also a problem if we do it in MIR level?
let args: Vec<OsString> = vec![ | ||
"--apply-loop-contracts".into(), | ||
"--loop-contracts-no-unwind".into(), | ||
"--disable-loop-contracts-side-effect-check".into(), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is that?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Because loop contracts now are wrapped in a closure which will be a side-effect expression in CBMC even they may not contain side-effect. So we disable the side-effect check for now and will implement a better check instead of simply rejecting function calls and statement expressions.
diffblue/cbmc#8393
kani_metadata/src/unstable.rs
Outdated
@@ -83,6 +83,8 @@ pub enum UnstableFeature { | |||
SourceCoverage, | |||
/// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) | |||
FunctionContracts, | |||
/// Enable loop contracts [RFC 12] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please add the link.
BTW, will this enable the entire flow where a loop is checked and later replaced?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, this will enable the entire flow. The two test cases run with loop contracts enable, where the running time is only ~1 seconds comparing to timeout when running without loop contracts
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This transformation seems very CBMC specific. I wonder if we should make this more explicit here. @zhassan-aws any thoughts on how would loop invariant be handled with the Aeneas backend?
@celinval Thank you! |
This PR introduce the loop contracts annotation for while-loops using proc-macro.
The A while loop of the form
is annotated as
We then replace the function body of the register function
kani_register_loop_contract_id
by a call to its function argumentf
.There are two calls to the register function, an actual with loop invariant closure as its argument, and a dummy one with dummy argument to bypass borrow checking. We later remove the dummy call and move the actual call to the position of the dummy call during MIR transformation.
At the end, the call to the register function will be codegened as backward goto with loop contracts annotated.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.