Error when annotating an associated function with a contract

[zhassan-aws]

I tried this code:

extern crate kani;

#[derive(PartialEq, Eq)]
enum Foo {
    A,
    B,
}

impl Foo {
    #[kani::ensures(result == Foo::A)]
    pub fn new() -> Foo {
        Foo::A
    }
}

#[kani::proof_for_contract(Foo::new)]
fn check() {
    let _ = Foo::new();
}

using the following command line invocation:

kani enum_ensures.rs -Zfunction-contracts

with Kani version: f10e61c

I expected to see this happen: Verification succeeds

Instead, this happened:

$ kani enum_ensures.rs -Zfunction-contracts
Kani Rust Verifier 0.51.0 (standalone)
error[E0425]: cannot find function `new_wrapper_faac06` in this scope
  --> enum_ensures.rs:10:5
   |
10 |     #[kani::ensures(result == Foo::A)]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not found in this scope
   |
   = note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)
help: consider using the associated function on `Self`
   |
10 |     Self::#[kani::ensures(result == Foo::A)]
   |     ++++++

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0425`.
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 1

[zhassan-aws]

Found a workaround: the error goes away if I use Self as the return type instead of Foo:

$ diff enum_ensures.rs enum_ensures_self.rs 
11c11
<     pub fn new() -> Foo {
---
>     pub fn new() -> Self {

Verification fails though:

$ kani enum_ensures_self.rs -Zfunction-contracts
...
SUMMARY:
 ** 1 of 1336 failed
Failed Checks: result == Foo::A
 File: "enum_ensures_self.rs", line 10, in Foo::new_check_478ff5

VERIFICATION:- FAILED
Verification Time: 1.9594536s

[zhassan-aws]

The issue in the previous comment seems to be independent of associated functions, so I filed a separate issue for it (#3228).

[celinval]

I was talking to @JustusAdam about this. I think the way contract works today won't work with trait implementations, neither associated functions that do not refer to the Self type. See this comment for an explanation on how associated functions are handled today.

One way to overcome these two limitations would be to change the contract functions to be generated as nested functions. This would allow us to attach contracts to associated functions and trait implementations.

However, doing so will remove access to generic parameters defined as part of the impl block, including Self. I.e., the following would not work:

impl<T: Default> Foo<T> {
    pub fn new() -> Foo<T> {
        fn bar() -> T { //<---- T cannot be used in this context.
           // ...
        }
        Foo(bar())
    }
}

See E0401 for more details.

Another possibility would be to convert the functions into closures instead. This will also require changes to how contracts are handled in the compiler.

Let's say we have the following function:

#[kani::requires(can_dereference(ptr))]
unsafe fn read<T>(ptr: *const T) -> T {
    *ptr
}

Ignoring the recursive case for now, this could become something roughly like:

#[kanitool::contract]
unsafe fn read<T>(ptr: *const T) -> T {
    let original_fn = |ptr: *const T| -> T { /* original_body */ };
    let check_fn = |ptr| {
        assert!(can_dereference(ptr));
        original_fn(ptr)
    };
    let replace_fn = |ptr: *const T| -> T {
        assert!(can_dereference(ptr));
        kani::any_modifies()
    };
    kani::contract_pick(original_fn, check_fn, replace_fn);
}

Now the transformation pass would need to pick the correct closure body to do the replacement.

[JustusAdam]

Yes right now the support for associated functions is limited because the macro only has access to the function body itself. It looks at that and basically tries to guess whether it may be an associated function, in this case by looking for an occurrence of self or Self.

I think I agree that closures are the best way to go because they can do generics and avoid this associated function. business. Although we should be careful with actually closing over the arguments, because that can get annoying with lifetimes.
The other problem with closures is that multiple clauses are harder to handle. At the moment such clauses are incrementally expanded on the check and replace functions themselves. On closures there's no stable way to attach attributes to the closure so the incremental expanding may not work.