#[kanitool::is_contract_generated] attribute is not detected

[carolynzech]

During contract instrumentation, we annotate the closures we add during instrumentation with #[kanitool::is_contract_generated]. However, calling tcx.get_attrs_unchecked on such a closure does not return this tool attribute. This means that if we have something like:

#[kani::requires(true)] // the contents of the contract don't matter for this example
fn add(x: u8) -> u8 {
    x + 1
}

and we filter like this:

// This will include closures
let crate_fns = stable_mir::all_local_items()
        .into_iter()
        .filter(|item| matches!(item.kind(), ItemKind::Fn));

if KaniAttributes::for_def_id(tcx, fn_item.def_id()).is_kani_instrumentation() {
      return Some(AutoHarnessSkipReason::KaniImpl);
  }
  
let instance = match Instance::try_from(fn_item) {
    Ok(inst) => inst,
    Err(_) => {
        return Some(AutoHarnessSkipReason::GenericFn); 
    }
};

where KaniAttributes::is_kani_instrumentation is defined as:

pub fn is_kani_instrumentation(&self) -> bool {
    self.fn_marker().is_some() || self.map.contains_key(&KaniAttributeKind::IsContractGenerated)
}

we would expect that all contract instrumentation closures are registered as such, and thus we report the reason for skipping as AutoHarnessSkipReason::KaniImpl. Instead, we get:

+--------------------------------------------+---------------------+
| Skipped Function                           | Reason for Skipping |
+==================================================================+
| add::{closure#0}                           | Generic Function    |
|--------------------------------------------+---------------------|
| add::{closure#0}::{closure#0}              | Generic Function    |
|--------------------------------------------+---------------------|
| add::{closure#0}::{closure#1}              | Generic Function    |
|--------------------------------------------+---------------------|
| add::{closure#0}::{closure#1}::{closure#0} | Generic Function    |
|--------------------------------------------+---------------------|
| add::{closure#1}                           | Generic Function    |
|--------------------------------------------+---------------------|
| add::{closure#2}                           | Generic Function    |
|--------------------------------------------+---------------------|
| add::{closure#2}::{closure#0}              | Generic Function    |
|--------------------------------------------+---------------------|
| add::{closure#3}                           | Generic Function    |
|--------------------------------------------+---------------------|
| add::{closure#3}::{closure#0}              | Generic Function    |
+--------------------------------------------+---------------------+

i.e., the closures have no attributes, but we fail to generate an Instance from them, so they get erroneously reported to the user as generic functions.

[carolynzech]

This is_contract_generated attribute got added way back in #2655, when contract instrumentation was still fns and not closures. So I suspect we just moved the attribute over without checking that it still shows up; none of our current logic relies on it anymore.
I did some digging upstream and wasn't able to determine why tcx.get_attrs_unchecked wouldn't return this attribute on closures. I'm not comfortable calling it a rustc "bug" until I do some more investigation; it could be that I'm calling it wrong, or that this is in fact a deliberate decision upstream that we just need to figure out.

[carolynzech]

For now, we'll just skip generating automatic harnesses for all closures, since top-level closures are pretty rare anyway. But it would be better to be able to differentiate between Kani's instrumented closures and closures from the user so that we can generate harnesses for the latter.