Skip to content

#[kanitool::is_contract_generated] attribute is not detected #3921

Open
@carolynzech

Description

@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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Z-ContractsIssue related to code contracts[C] InternalTracks some internal work. I.e.: Users should not be affected.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions