Indexing into `Vec` is poorly supported

[jmc-figueira]

The following verification

#[ensures(self.counters[id] == old(self).counters[id] + 1)]
fn increment(&mut self, id: usize) {
    self.counters[id] += 1;
}

results in the following internal error

error: internal compiler error: compiler/rustc_metadata/src/rmeta/decoder.rs:1185:17: get_optimized_mir: missing MIR for `DefId(2:2355 ~ core[5aef]::ops::index::Index::index)`

thread 'rustc' panicked at 'Box<Any>', compiler/rustc_errors/src/lib.rs:958:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

note: Prusti or the compiler unexpectedly panicked. This is a bug.

note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: Prusti version: {commit 6e9dbad5 2021-01-06 15:15:04 UTC, built on 2021-01-08 15:01:51 UTC}

error: aborting due to previous error; 4 warnings emitted

It appears to be an issue related to Vec indexing (counters is of type Vec<i64>). Is there any known workaround for this?

[fpoli]

Thanks for the report. Crashing is surely a bug.

Instead of old(self).counters[id] you should use old(self.counters[id]), because you want to evaluate self.counters[id] in the old state, and not just self. However, this does not prevent the crash.

A workaround is to wrap the vector in a structure with methods marked as #[trusted], like here. A second workaround is to use the new #[extern_spec] feature, to attach specifications to library methods like here, but the feature is still a bit experimental and does not always work as mentioned here.

[JonasAlaif]

Both the pure and non-pure versions of the following are not yet supported:

(#[pure])
fn foo(vec: &Vec<i32>) {
    let i = vec[0];
}

The following does not throw an error since it is an std::ops::IndexMut::index_mut rather than an std::ops::Index::index, but is also not implemented:

fn foo(vec: &mut Vec<i32>) {
    vec[0] = 0;
}

Even the len of a Vec does't work like that of a slice (error):

#[requires(vec.len() > 0)]

We should implement these ASAP, as soon as the extern_spec work is done.