flux-rs/flux

Bug when using `.iter()` over a reference

Closed this issue · 1 comments

The following code crashes with an assertion failure:

pub fn baz(v: &Vec<i32>) {
    for x in v {}
}

See below for notes.
Ok did some digging, this is indeed a bug somewhere else.

When calling Iter::next we "downgrade" a pointer to a reference (this line) changing the lifetime to something that makes the assertion fail.

So, we start with

r: ptr(x), x: Iter<'?11, i32>

Then, just before the call, we have

r: &mut Iter<?20, i32>, x: †Iter<'?20, i32>

i.e., the pointer r is now a mutable reference, and the type of x has been strongly updated (and blocked). The issue is that lifetimes should never be strongly updated. The call to block_with should update everything but lifetimes. That's what we do in assignments https://github.com/flux-rs/flux/blob/main/crates/flux-refineck/src/type_env.rs#L172.

The fix is a bit tricky because we are updating through a path not a place, so we can't do the same as we do in assign.

Originally posted by @nilehmann in #575 (comment)

Ideally we'd want stuff like this to work

#[flux::sig(fn (bool[true]))]
fn assert(_b: bool) {}

pub fn test() {
    let mut s: Vec<i32> = vec![];
    s.push(666);
    for v in &s {
        assert(*v >= 0);
    }
}

and

pub fn test() {
    let mut s: RSet<i32> = RSet::new();
    s.insert(10);
    s.insert(20);
    s.insert(30);


     for v in s.iter() {
         assert(*v >= 10);
     }
}