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