Reborrowing a shared reference is unsupported, results in a generic "generating fold-unfold Viper statements failed"

[suhr]

Prusti reports this error at push_all function:

[Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Pred(Local(_old$l22$0: Ref(__TYPARAM__$T$__), Position { line: 0, column: 0, id: 0 }), read)))

Source code: https://gist.github.com/suhr/64870f086ec99899c1db4a52b195a1cb

[fpoli]

Thank you for the report! I think the reason of the error is that push_all uses an iterator (for i in 0..slice_len(slice)), which is currently unsupported. Prusti should have reported that. To verify your function you can try rewriting the for loop to a let mut i = 0; while i < slice_len(slice) { ... ; i += 1; }.

On a side note, arrays like [T] are also unsupported, but if you just pass the instance around without accessing the elements then Prusti should be fine with it. @dario23, the linked program might be a good use case for your project on supporting arrays and slices.

[suhr]

I see, thanks. But the way, what I am aiming for is to prove leftpad.

[suhr]

It finds out that a while loop version also errors with a similar error.

[suhr]

The actual source of the error is the .clone() call.

[fpoli]

The actual source of the error is the .clone() call.

Thanks for identifying the reason. That's strange, we need to debug this.

[fpoli]

I investigated a bit more. The issue is caused by index_slice, whose result reborrows an argument of type shared reference. Reborrowing a shared reference is still unsupported.

A slightly simpler program to reproduce the issue:

use prusti_contracts::*;

#[pure]
#[trusted]
fn slice_len(slice: &[u32]) -> usize {
    unimplemented!()
}

#[trusted]
fn push(vec: &mut Vec<u32>, value: u32) {
    unimplemented!()
}

#[trusted]
fn index_slice(slice: &[u32], ix: usize) -> &u32 {
    unimplemented!()
}

fn push_all(vec: &mut Vec<u32>, slice: &[u32]) {
    let mut i = 0;
    while i < slice_len(slice) {
        push(vec, index_slice(slice, i).clone());
        i += 1;
    }
}

fn main() {}

[fpoli]

The first example now reports the correct error

error: [Prusti: unsupported feature] iterators are not fully supported yet
  --> program.rs:39:14
   |
39 |     for i in 0..slice_len(slice) {
   |              ^^^^^^^^^^^^^^^^^^^

However, the second program that I posted still doesn't work.