Ignore drop on &mut references (#906)

* move place

* hack move_place -- to basically ignore the 'move' part

* remove _is_constant_index

crates/flux-refineck/src/type_env.rs

@@ -268,12 +268,10 @@ impl<'a> TypeEnv<'a> {
         if result.is_strg {
             let uninit = Ty::uninit();
             Ok(result.update(uninit))
-        } else if result.is_constant_index {
+        } else {
             // ignore the 'move' and trust rustc managed the move correctly
             // https://github.com/flux-rs/flux/issues/725#issuecomment-2295065634
             Ok(result.ty)
-        } else {
-            tracked_span_bug!("cannot move out of {place:?}");
         }
     }
 

crates/flux-refineck/src/type_env/place_ty.rs

@@ -73,7 +73,6 @@ impl LookupKey for Path {
 pub(super) struct LookupResult<'a> {
     pub ty: Ty,
     pub is_strg: bool,
-    pub is_constant_index: bool, // doesn't feel right...
     cursor: Cursor,
     bindings: &'a mut PlacesTree,
 }
@@ -177,7 +176,6 @@ impl PlacesTree {
         let mut cursor = self.cursor_for(key);
         let mut ty = self.get_loc(&cursor.loc).ty.clone();
         let mut is_strg = true;
-        let mut is_constant_index = false;
         while let Some(elem) = cursor.next() {
             ty = mode.unpack(&ty);
             match elem {
@@ -221,7 +219,6 @@ impl PlacesTree {
                 }
                 PlaceElem::Index(_) | PlaceElem::ConstantIndex { .. } => {
                     is_strg = false;
-                    is_constant_index = matches!(elem, PlaceElem::ConstantIndex { .. });
                     match ty.kind() {
                         TyKind::Indexed(BaseTy::Array(array_ty, _), _) => {
                             ty = array_ty.clone();
@@ -236,7 +233,7 @@ impl PlacesTree {
             }
         }
         cursor.reset();
-        Ok(LookupResult { ty, is_strg, is_constant_index, cursor, bindings: self })
+        Ok(LookupResult { ty, is_strg, cursor, bindings: self })
     }
 
     pub(crate) fn lookup_unfolding(

tests/tests/neg/surface/issue-431.rs

@@ -0,0 +1,30 @@
+#[path = "../../lib/rvec.rs"]
+mod rvec;
+use rvec::RVec;
+
+#[flux::sig(fn(vec: &mut RVec<_>[100]))]
+pub fn test(vec: &mut RVec<RVec<i32>>) {
+    vec[0] = RVec::new();
+}
+
+#[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{v: v < k}, (RVec<f32>, usize))>))]
+pub fn update_centers_bad(
+    _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) //~ ERROR refinement type
+    }
+}

tests/tests/pos/surface/issue-431.rs

@@ -0,0 +1,30 @@
+#[path = "../../lib/rvec.rs"]
+mod rvec;
+use rvec::RVec;
+
+#[flux::sig(fn(vec: &mut RVec<_>[100]))]
+pub fn test(vec: &mut RVec<RVec<i32>>) {
+    vec[0] = RVec::new();
+}
+
+#[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{v: v < k}, (RVec<f32>[n], usize))>))]
+pub 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)
+    }
+}