flux-rs / flux

Refinement Types for Rust
MIT License
663 stars 21 forks source link

Panic when dropping and replacing value through a mutable reference #431

Closed nilehmann closed 4 days ago

nilehmann commented 1 year ago

The following code panic when trying to update centers[i]

#[flux::sig(fn(&RVec<f32>[@n], usize) -> RVec<f32>[n])]
fn normal(x: &RVec<f32>, w: usize) -> RVec<f32> {
    let mut i = 0;
    let mut res = RVec::new();
    while i < x.len() {
        res.push(x[i] / (w as f32));
        i += 1;
    }
    res
}

#[flux::sig(fn (n: usize, centers: &mut RVec<RVec<f32>[n]>[@k], new_centers: RVec<(usize, (RVec<f32>, usize))>))]
fn update_centers(
    n: usize,
    centers: &mut RVec<RVec<f32>>,
    new_centers: RVec<(usize, (RVec<f32>, usize))>,
) {
    for (i, (x, size)) in new_centers {
        centers[i] = normal(&x, size)
    }
}

This is the panic

error: internal compiler error: flux-refineck/src/type_env.rs:169:17: cannot move out of `*_21`, which is behind a `&mut` reference
  --> /home/nlehmann/phd/flux-rs/flux/attic/playground.rs:24:9
   |
24 |         centers[i] = normal(&x, size)
   |         ^^^^^^^^^^
-Ztrack-diagnostics: created at /rustc/700938c0781c9f135244bb1ec846fe1a5e03ae7d/compiler/rustc_errors/src/lib.rs:995:33
nilehmann commented 1 year ago

Here's a minimal repro

fn test(vec: &mut RVec<RVec<i32>>) {
    vec[0] = RVec::new();
}
nilehmann commented 1 year ago

Here's the issue. Because RVec<T> is Drop, the line vec[0] = RVec::new() is "swapping" the old value with RVec::new() and dropping the old value. This used to happen as a single mir operation called DropAndReplace but now it desugars to more than one statement. Something like

1: _2 = vec.index_mut(0)
2: drop(*_2)
3: (*_2) = RVec::new()

Here _2 should have type &mut RVec<i32> but in between lines 2 and 3 , the reference momentarily points to uninitialized memory, so we are are "breaking" the invariant (i.e., it is a value of type RVec<i32>) after 2 and then reestablishing it in 3. This would be fundamentally addressed with folding/unfolding of mutable references, but in this particular case I think we could just ignore drop(*_2)