viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.56k stars 108 forks source link

Error about chaining pure functions #903

Open atgeller opened 2 years ago

atgeller commented 2 years ago

Hi, I'm getting the following error with the prusti-assistant (latest release version): [Prusti internal error] There is no procedure contract for loan bw19. This could happen if you are chaining pure functions, which is not fully supported. However, it doesn't look to me like there are any pure functions being chained in the example (at least, where the error is being reported on line 56): vec_test.zip. Any ideas on what might be causing the issue and/or how to work around it?

atgeller commented 2 years ago

I was able to minimize the example some. Here's a smaller example where chaining a dereference with a pure function causes issues (the error occurs at the line let y = *test(&x):

#[pure]
#[ensures(*result == *x)]
fn test(x: &i32) -> &i32 {
    return x;
}

#[ensures(result == 0)]
fn test1() -> i32 {
    let x = 0;
    let y = *test(&x);
    return y;
}

I think the problem with the previous example is that the let inner_vec1 = m1.index_mut(i) from line 53 is returning a &mut VecWrapper, which is being implicitly dereferenced when calling inner_vec1.len() on line 56. Is it the case that the dereference operator winds up being represented as a pure function (either through rustc desugaring or in some internal representation in Prusti)?

fpoli commented 2 years ago

Thanks for the report! One more minimized example:

use prusti_contracts::*;

pub struct T;

impl T {
    #[trusted]
    #[pure]
    fn get(&self) -> &T {
        unimplemented!();
    }
}

pub fn test(m: &T) {
    loop {
        let r = m.get(); // ERROR
    }
}

pub fn main() {}

For this program, the reason seems to be that the get() call creates a reference in a loop, which is not supported. The error message should point that out. If the reference is to a Copy type (e.g. &i32) then you can declare a get that returns a copy of the type (i32), otherwise I'm afraid at the moment you have to rewrite the loop to be a recursive function call.

fpoli commented 2 years ago

Is it the case that the dereference operator winds up being represented as a pure function (either through rustc desugaring or in some internal representation in Prusti)?

No, the dereferentiation shouldn't generate a pure function call. I do get a different error for your program (cannot generate fold-unfold Viper statements. The required permission Acc(oldpre.val_int, read) cannot be obtained). I think that's a different issue.