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.

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() {

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)]\
+| ^^^^^^^^^^^^^^

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<T: Default>() {
+ foo();
+}

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]\

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