Allow modifies clause for verification only by feliperodri · Pull Request #3098 · model-checking/kani

feliperodri · 2024-03-20T16:57:56Z

Allow contracts to be used for verification, even if it is not suitable for stubbing. For that, we remove the requirement that modifies and return types of a function annotated with contracts must implement kani::Arbitrary, since that is only needed for recursion and stubbing with contract.

This is done via a new intrinsic any_modifies to Kani that should only be used by contract instrumentation. The T: Arbitrary requirement is only checked when users try to use the contract as stub or to check recursive functions.

For now, we also require users to annotate their contracts with kani::recursion if they want to use inductive reasoning to verify a recursive function.

Resolves #2997.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

celinval

Don't we need to remove this logic too?

kani-compiler/src/kani_middle/reachability.rs

library/kani/src/lib.rs

tests/expected/function-contract/modifies/mistake_condition_return.expected

feliperodri · 2024-03-21T21:20:43Z

We must update the RFC.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Contracts now are able to reason about the heap, thus, this safety check is no longer necessary. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

celinval

Just some minor comments. I'm still not a bit fan of the kani::recursion attribute, but I think we can improve this later on and it would be nice to unblock contracts for verification only.

kani-compiler/src/kani_middle/attributes.rs

kani-compiler/src/kani_middle/reachability.rs

kani-compiler/src/kani_middle/provide.rs

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

@zhassan-aws

Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.48.0"/version = "0.49.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Upgrade Rust toolchain to 2024-03-14 by @zhassan-aws in #3081 * Disable removal of storage markers by @zhassan-aws in #3083 * Automatic cargo update to 2024-03-18 by @github-actions in #3086 * Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` by @dependabot in #3087 * Upgrade toolchain to nightly-2024-03-15 by @celinval in #3084 * Add optional scatterplot to benchcomp output by @tautschnig in #3077 * Benchcomp scatterplots: quote axis labels by @tautschnig in #3097 * Expand ${var} in benchcomp variant `env` by @karkhaz in #3090 * Add test for #3099 by @zhassan-aws in #3100 * Automatic cargo update to 2024-03-25 by @github-actions in #3103 * Bump tests/perf/s2n-quic from `1a7faa8` to `0a60ec1` by @dependabot in #3104 * Implement validity checks by @celinval in #3085 * Add `benchcomp filter` command by @karkhaz in #3105 * Add CI test for --use-local-toolchain by @jaisnan in #3074 * Upgrade Rust toolchain to `nightly-2024-03-21` by @adpaco-aws in #3102 * Use `intrinsic_name` to get the intrinsic name by @adpaco-aws in #3114 * Bump tests/perf/s2n-quic from `0a60ec1` to `2d5e891` by @dependabot in #3118 * Allow modifies clause for verification only by @feliperodri in #3098 * Automatic cargo update to 2024-04-01 by @github-actions in #3117 * Automatic cargo update to 2024-04-04 by @github-actions in #3122 * Remove bookrunner by @tautschnig in #3123 * Upgrade Rust toolchain to nightly-2024-03-29 by @feliperodri in #3116 * Remove unnecessary build step for some workflows by @zhassan-aws in #3124 * Ensure storage markers are kept in std code by @zhassan-aws in #3080 **Full Changelog**: kani-0.48.0...kani-0.49.0

) This is an additional fix for #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>

@zhassan-aws

Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.48.0"/version = "0.49.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Upgrade Rust toolchain to 2024-03-14 by @zhassan-aws in model-checking#3081 * Disable removal of storage markers by @zhassan-aws in model-checking#3083 * Automatic cargo update to 2024-03-18 by @github-actions in model-checking#3086 * Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` by @dependabot in model-checking#3087 * Upgrade toolchain to nightly-2024-03-15 by @celinval in model-checking#3084 * Add optional scatterplot to benchcomp output by @tautschnig in model-checking#3077 * Benchcomp scatterplots: quote axis labels by @tautschnig in model-checking#3097 * Expand ${var} in benchcomp variant `env` by @karkhaz in model-checking#3090 * Add test for model-checking#3099 by @zhassan-aws in model-checking#3100 * Automatic cargo update to 2024-03-25 by @github-actions in model-checking#3103 * Bump tests/perf/s2n-quic from `1a7faa8` to `0a60ec1` by @dependabot in model-checking#3104 * Implement validity checks by @celinval in model-checking#3085 * Add `benchcomp filter` command by @karkhaz in model-checking#3105 * Add CI test for --use-local-toolchain by @jaisnan in model-checking#3074 * Upgrade Rust toolchain to `nightly-2024-03-21` by @adpaco-aws in model-checking#3102 * Use `intrinsic_name` to get the intrinsic name by @adpaco-aws in model-checking#3114 * Bump tests/perf/s2n-quic from `0a60ec1` to `2d5e891` by @dependabot in model-checking#3118 * Allow modifies clause for verification only by @feliperodri in model-checking#3098 * Automatic cargo update to 2024-04-01 by @github-actions in model-checking#3117 * Automatic cargo update to 2024-04-04 by @github-actions in model-checking#3122 * Remove bookrunner by @tautschnig in model-checking#3123 * Upgrade Rust toolchain to nightly-2024-03-29 by @feliperodri in model-checking#3116 * Remove unnecessary build step for some workflows by @zhassan-aws in model-checking#3124 * Ensure storage markers are kept in std code by @zhassan-aws in model-checking#3080 **Full Changelog**: model-checking/kani@kani-0.48.0...kani-0.49.0

…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>

github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Mar 20, 2024

feliperodri force-pushed the only-verify-contracts branch 2 times, most recently from 98eb910 to 62bdf68 Compare March 21, 2024 20:00

feliperodri marked this pull request as ready for review March 21, 2024 20:01

feliperodri requested a review from a team as a code owner March 21, 2024 20:01

celinval reviewed Mar 21, 2024

View reviewed changes

kani-compiler/src/kani_middle/reachability.rs Outdated Show resolved Hide resolved

library/kani/src/lib.rs Outdated Show resolved Hide resolved

celinval reviewed Mar 21, 2024

View reviewed changes

tests/expected/function-contract/modifies/mistake_condition_return.expected Outdated Show resolved Hide resolved

feliperodri added 2 commits March 28, 2024 19:06

Allow modifies clause for verification only

609619a

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Add recursion attribute

2c0a909

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri force-pushed the only-verify-contracts branch from 468c9ab to 2c0a909 Compare March 28, 2024 23:35

feliperodri added 2 commits March 28, 2024 19:38

Remove check_is_contract_safe function

0c9a0fa

Contracts now are able to reason about the heap, thus, this safety check is no longer necessary. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Replace attribute for any_modifies

8c4eb46

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri self-assigned this Mar 28, 2024

Remove unused functions and imports

e8186e7

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri requested a review from celinval March 29, 2024 16:39

Update regression tests after removing check_is_contract_safe

cd99121

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

celinval approved these changes Apr 1, 2024

View reviewed changes

kani-compiler/src/kani_middle/attributes.rs Show resolved Hide resolved

kani-compiler/src/kani_middle/reachability.rs Outdated Show resolved Hide resolved

kani-compiler/src/kani_middle/provide.rs Outdated Show resolved Hide resolved

feliperodri and others added 6 commits April 2, 2024 13:49

Include documentation for recursion attribute

463cee9

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Add missing newline

39f68ba

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Clarify condition for any_modifies transformation

3d37518

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Use diagnose info instead of name in reachability

9c43563

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Kani fails without proper annotation for recursive functions

6635a93

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Merge branch 'main' into only-verify-contracts

b9615bf

feliperodri enabled auto-merge (squash) April 2, 2024 18:13

feliperodri merged commit 946ea80 into model-checking:main Apr 2, 2024

feliperodri deleted the only-verify-contracts branch April 2, 2024 18:28

tautschnig mentioned this pull request Apr 5, 2024

Bump Kani version to 0.49.0 #3126

Merged

feliperodri mentioned this pull request May 1, 2024

Remove kani::Arbitrary from the modifies contract instrumentation #3169

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Allow modifies clause for verification only#3098

Allow modifies clause for verification only#3098
feliperodri merged 12 commits intomodel-checking:mainfrom
feliperodri:only-verify-contracts

feliperodri commented Mar 20, 2024 •

edited

Loading

Uh oh!

celinval left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri commented Mar 21, 2024

Uh oh!

celinval left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

feliperodri commented Mar 20, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri commented Mar 21, 2024

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

feliperodri commented Mar 20, 2024 •

edited

Loading