flux-rs / flux

Refinement Types for Rust
MIT License
632 stars 17 forks source link

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

Closed ranjitjhala closed 8 months ago

ranjitjhala commented 8 months ago

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 https://github.com/flux-rs/flux/pull/575#discussion_r1430773298_

ranjitjhala commented 8 months ago

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);
     }
}