-
Notifications
You must be signed in to change notification settings - Fork 84
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Call
check_proof_attribute
for contract harnesses (#3522)
Kani enforces that `[kani::proof]` attribute is not applied to generic functions. We do not currently enforce this restriction on contract harnesses. When the compiler [searches for harnesses to verify](https://github.com/model-checking/kani/blob/dba8f3926a61025f5078de787ebd8d21278333ca/kani-compiler/src/kani_middle/codegen_units.rs#L63), it only looks at monomorphized functions. Thus, currently a user can write this code: ```rust #[kani::requires(true)] fn foo() {} #[kani::proof_for_contract(foo)] fn check_foo<T>() { foo() } ``` and get "No proof harnesses (functions with #[kani::proof]) were found to verify." In the case where a user is running many harnesses, they may not notice that Kani skipped the harness. For example, we currently have [this harness](https://github.com/model-checking/verify-rust-std/blob/149f6dd5409fac01a983d7b98c51d51666c74e45/library/core/src/ptr/unique.rs#L288) in the standard library, which doesn't actually run. (PR to fix is [here](model-checking/verify-rust-std#86)). After this PR merges, the code snippet above would instead error with: ```rust error: the '#[kani::proof_for_contract]' attribute cannot be applied to generic functions --> src/lib.rs:4:1 | 4 | #[kani::proof_for_contract(foo)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info) error: aborting due to 1 previous error ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
- Loading branch information
1 parent
d2051b7
commit dd26362
Showing
5 changed files
with
65 additions
and
8 deletions.
There are no files selected for viewing
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
error: only one '#[kani::proof_for_contract]' attribute is allowed per harness\ | ||
invalid.rs:\ | ||
|\ | ||
| #[kani::proof_for_contract(foo)]\ | ||
| ^^^^^^^^^^^^^^ | ||
|
||
error: functions used as harnesses cannot have any arguments\ | ||
invalid.rs:\ | ||
|\ | ||
| #[kani::proof_for_contract(foo)] | ||
| ^^^^^^^^^^^^^^ | ||
|
||
error: the '#[kani::proof_for_contract]' attribute cannot be applied to generic functions\ | ||
invalid.rs:\ | ||
|\ | ||
| #[kani::proof_for_contract(foo)]\ | ||
| ^^^^^^^^^^^^^^ |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
// kani-flags: -Zfunction-contracts | ||
|
||
// This test is to check Kani's error handling of invalid usages of the `proof_for_contract` harness. | ||
// We also ensure that all errors and warnings are printed in one compilation. | ||
|
||
#[kani::requires(true)] | ||
fn foo() {} | ||
|
||
#[kani::proof_for_contract(foo)] | ||
#[kani::proof_for_contract(foo)] | ||
fn multiple_proof_annotations() { | ||
foo(); | ||
} | ||
|
||
#[kani::proof_for_contract(foo)] | ||
fn proof_with_arg(arg: bool) { | ||
foo(); | ||
} | ||
|
||
#[kani::proof_for_contract(foo)] | ||
fn generic_harness<T: Default>() { | ||
foo(); | ||
} |
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1 @@ | ||
error: the `proof` attribute cannot be applied to generic functions | ||
error: the '#[kani::proof]' attribute cannot be applied to generic functions |