Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Allow modifies clause for verification only #3098

Merged
merged 12 commits into from
Apr 2, 2024
Merged

Allow modifies clause for verification only #3098

merged 12 commits into from
Apr 2, 2024

Conversation

feliperodri
Copy link
Contributor

@feliperodri feliperodri commented Mar 20, 2024 •
edited
Loading

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.

@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Mar 20, 2024
@feliperodri feliperodri force-pushed the only-verify-contracts branch 2 times, most recently from 98eb910 to 62bdf68 Compare March 21, 2024 20:00
@feliperodri feliperodri marked this pull request as ready for review March 21, 2024 20:01
@feliperodri feliperodri requested a review from a team as a code owner March 21, 2024 20:01
celinval
celinval reviewed Mar 21, 2024
View reviewed changes
Copy link
Contributor

@celinval celinval left a 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 remove this logic too?

kani-compiler/src/kani_middle/reachability.rs Outdated Show resolved Hide resolved
library/kani/src/lib.rs Outdated Show resolved Hide resolved
@feliperodri
Copy link
Contributor Author

We must update the RFC.

@feliperodri
Allow modifies clause for verification only
609619a 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Add recursion attribute
2c0a909 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri feliperodri force-pushed the only-verify-contracts branch from 468c9ab to 2c0a909 Compare March 28, 2024 23:35
@feliperodri
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>
@feliperodri
Replace attribute for any_modifies
8c4eb46 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri feliperodri self-assigned this Mar 28, 2024
@feliperodri
Remove unused functions and imports
e8186e7 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri feliperodri requested a review from celinval March 29, 2024 16:39
@feliperodri
Update regression tests after removing check_is_contract_safe
cd99121 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
celinval
celinval approved these changes Apr 1, 2024
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 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
@feliperodri
Include documentation for recursion attribute
463cee9 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Add missing newline
39f68ba 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Clarify condition for any_modifies transformation
3d37518 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Use diagnose info instead of name in reachability
9c43563 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Kani fails without proper annotation for recursive functions
6635a93 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Merge branch 'main' into only-verify-contracts
b9615bf
@feliperodri feliperodri enabled auto-merge (squash) April 2, 2024 18:13
@feliperodri feliperodri merged commit 946ea80 into model-checking:main Apr 2, 2024
23 checks passed
@feliperodri feliperodri deleted the only-verify-contracts branch April 2, 2024 18:28
@tautschnig tautschnig mentioned this pull request Apr 5, 2024
Merged
tautschnig added a commit that referenced this pull request Apr 5, 2024
@tautschnig
Bump Kani version to 0.49.0 (#3126)
ac46d98 
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
@feliperodri feliperodri mentioned this pull request May 1, 2024
Merged
adpaco-aws pushed a commit that referenced this pull request May 3, 2024
@feliperodri
Remove kani::Arbitrary from the modifies contract instrumentation (#3169
c0e4e1b 
)

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>
zpzigi754 pushed a commit to zpzigi754/kani that referenced this pull request May 8, 2024
@tautschnig @zpzigi754
Bump Kani version to 0.49.0 (model-checking#3126)
4936191 
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
zpzigi754 pushed a commit to zpzigi754/kani that referenced this pull request May 8, 2024
@feliperodri @zpzigi754
Remove kani::Arbitrary from the modifies contract instrumentation (mo…
c128918 
…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>
qinheping pushed a commit to qinheping/kani that referenced this pull request May 9, 2024
@feliperodri @qinheping
Remove kani::Arbitrary from the modifies contract instrumentation (mo…
df2c1fb 
…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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@celinval celinval celinval approved these changes

Assignees

@feliperodri feliperodri

Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Users should be able to create contracts suitable for verification but not stubbing
2 participants
@feliperodri @celinval