From dd26362479ca9f57445f66187ea33d6a70ced534 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Sep 2024 15:08:13 -0400 Subject: [PATCH 1/2] 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() { 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](https://github.com/model-checking/verify-rust-std/pull/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. --- kani-compiler/src/kani_middle/attributes.rs | 27 +++++++++++++++----- tests/ui/invalid-contract-harness/expected | 17 ++++++++++++ tests/ui/invalid-contract-harness/invalid.rs | 25 ++++++++++++++++++ tests/ui/invalid-harnesses/expected | 2 +- tests/ui/mir-linker/generic-harness/expected | 2 +- 5 files changed, 65 insertions(+), 8 deletions(-) create mode 100644 tests/ui/invalid-contract-harness/expected create mode 100644 tests/ui/invalid-contract-harness/invalid.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 9a3ff7c1d6a6..86e97f633dfb 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -358,7 +358,7 @@ impl<'tcx> KaniAttributes<'tcx> { ); } expect_single(self.tcx, kind, &attrs); - attrs.iter().for_each(|attr| self.check_proof_attribute(attr)) + attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr)) } KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| { let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(self.tcx)); @@ -370,6 +370,7 @@ impl<'tcx> KaniAttributes<'tcx> { ); } expect_single(self.tcx, kind, &attrs); + attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr)) } KaniAttributeKind::StubVerified => { expect_single(self.tcx, kind, &attrs); @@ -583,15 +584,29 @@ impl<'tcx> KaniAttributes<'tcx> { } /// Check that if this item is tagged with a proof_attribute, it is a valid harness. - fn check_proof_attribute(&self, proof_attribute: &Attribute) { + fn check_proof_attribute(&self, kind: KaniAttributeKind, proof_attribute: &Attribute) { let span = proof_attribute.span; let tcx = self.tcx; - expect_no_args(tcx, KaniAttributeKind::Proof, proof_attribute); + if let KaniAttributeKind::Proof = kind { + expect_no_args(tcx, kind, proof_attribute); + } + if tcx.def_kind(self.item) != DefKind::Fn { - tcx.dcx().span_err(span, "the `proof` attribute can only be applied to functions"); + tcx.dcx().span_err( + span, + format!( + "the '#[kani::{}]' attribute can only be applied to functions", + kind.as_ref() + ), + ); } else if tcx.generics_of(self.item).requires_monomorphization(tcx) { - tcx.dcx() - .span_err(span, "the `proof` attribute cannot be applied to generic functions"); + tcx.dcx().span_err( + span, + format!( + "the '#[kani::{}]' attribute cannot be applied to generic functions", + kind.as_ref() + ), + ); } else { let instance = Instance::mono(tcx, self.item); if !super::fn_abi(tcx, instance).args.is_empty() { diff --git a/tests/ui/invalid-contract-harness/expected b/tests/ui/invalid-contract-harness/expected new file mode 100644 index 000000000000..1e07c4ca4b16 --- /dev/null +++ b/tests/ui/invalid-contract-harness/expected @@ -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)]\ +| ^^^^^^^^^^^^^^ diff --git a/tests/ui/invalid-contract-harness/invalid.rs b/tests/ui/invalid-contract-harness/invalid.rs new file mode 100644 index 000000000000..e30382e3c602 --- /dev/null +++ b/tests/ui/invalid-contract-harness/invalid.rs @@ -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() { + foo(); +} diff --git a/tests/ui/invalid-harnesses/expected b/tests/ui/invalid-harnesses/expected index 7def51a0d85a..265af44a1685 100644 --- a/tests/ui/invalid-harnesses/expected +++ b/tests/ui/invalid-harnesses/expected @@ -10,7 +10,7 @@ invalid.rs:\ | #[kani::proof] | ^^^^^^^^^^^^^^ -error: the `proof` attribute cannot be applied to generic functions\ +error: the '#[kani::proof]' attribute cannot be applied to generic functions\ invalid.rs:\ |\ | #[kani::proof]\ diff --git a/tests/ui/mir-linker/generic-harness/expected b/tests/ui/mir-linker/generic-harness/expected index 0798bb9e99a3..176ca1a5b7db 100644 --- a/tests/ui/mir-linker/generic-harness/expected +++ b/tests/ui/mir-linker/generic-harness/expected @@ -1 +1 @@ -error: the `proof` attribute cannot be applied to generic functions +error: the '#[kani::proof]' attribute cannot be applied to generic functions From 27cee8b71d8e82d86e04d315534d1677d2744716 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Sep 2024 16:11:23 -0400 Subject: [PATCH 2/2] Add tests for issue 3009 (#3526) Kani v0.55 no longer has the overly broad span issue reported in #3009. I suspect that our shift (#3363) from functions to closures for contracts allows rustc to produce better error messages. Add tests to prevent regression in the future. Resolves #3009 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../function-contracts/non_bool_contracts.expected | 11 +++++++++++ tests/ui/function-contracts/non_bool_contracts.rs | 13 +++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 tests/ui/function-contracts/non_bool_contracts.expected create mode 100644 tests/ui/function-contracts/non_bool_contracts.rs diff --git a/tests/ui/function-contracts/non_bool_contracts.expected b/tests/ui/function-contracts/non_bool_contracts.expected new file mode 100644 index 000000000000..a6d7704330db --- /dev/null +++ b/tests/ui/function-contracts/non_bool_contracts.expected @@ -0,0 +1,11 @@ +| +| #[kani::requires(a + b)] +| -----------------^^^^^-- +| | | +| | expected `bool`, found `u64` +| arguments to this function are incorrect +| + +| +| #[kani::ensures(|result| a % *result && b % *result == 0 && *result != 0)] +| ^^^^^^^^^^^ expected `bool`, found `u64` \ No newline at end of file diff --git a/tests/ui/function-contracts/non_bool_contracts.rs b/tests/ui/function-contracts/non_bool_contracts.rs new file mode 100644 index 000000000000..e192e625cac3 --- /dev/null +++ b/tests/ui/function-contracts/non_bool_contracts.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// This tests that Kani reports the "ideal" error message when contracts are non-boolean expressions +// By "ideal," we mean that the error spans are as narrow as possible +// (c.f. https://github.com/model-checking/kani/issues/3009) + +#[kani::requires(a + b)] +#[kani::ensures(|result| a % *result && b % *result == 0 && *result != 0)] +fn gcd(a: u64, b: u64) -> u64 { + 0 +}