diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 71af1ac04b..3ad4565136 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/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:?}"); } } diff --git a/crates/flux-refineck/src/type_env/place_ty.rs b/crates/flux-refineck/src/type_env/place_ty.rs index d67c5591ef..d01bda23a8 100644 --- a/crates/flux-refineck/src/type_env/place_ty.rs +++ b/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( diff --git a/tests/tests/neg/surface/issue-431.rs b/tests/tests/neg/surface/issue-431.rs new file mode 100644 index 0000000000..0f576aee45 --- /dev/null +++ b/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>) { + vec[0] = RVec::new(); +} + +#[flux::sig(fn(&RVec[@n], usize) -> RVec[n])] +fn normal(x: &RVec, w: usize) -> RVec { + 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[n]>[@k], new_centers: RVec<(usize{v: v < k}, (RVec, usize))>))] +pub fn update_centers_bad( + _n: usize, + centers: &mut RVec>, + new_centers: RVec<(usize, (RVec, usize))>, +) { + for (i, (x, size)) in new_centers { + centers[i] = normal(&x, size) //~ ERROR refinement type + } +} diff --git a/tests/tests/pos/surface/issue-431.rs b/tests/tests/pos/surface/issue-431.rs new file mode 100644 index 0000000000..022dca6051 --- /dev/null +++ b/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>) { + vec[0] = RVec::new(); +} + +#[flux::sig(fn(&RVec[@n], usize) -> RVec[n])] +fn normal(x: &RVec, w: usize) -> RVec { + 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[n]>[@k], new_centers: RVec<(usize{v: v < k}, (RVec[n], usize))>))] +pub fn update_centers( + _n: usize, + centers: &mut RVec>, + new_centers: RVec<(usize, (RVec, usize))>, +) { + for (i, (x, size)) in new_centers { + centers[i] = normal(&x, size) + } +}