diff --git a/src/refine/env.rs b/src/refine/env.rs index ba494acb..f54ca15c 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -1050,7 +1050,6 @@ where #[derive(Debug, Clone)] enum Path { - PlaceTy(Box), Local(Local), Deref(Box), TupleProj(Box, usize), @@ -1079,23 +1078,12 @@ impl<'tcx> From> for Path { } } -impl Path { - fn deref(self) -> Self { - Path::Deref(Box::new(self)) - } - - fn tuple_proj(self, idx: usize) -> Self { - Path::TupleProj(Box::new(self), idx) - } -} - impl Env where T: EnumDefProvider, { fn path_type(&self, path: &Path) -> PlaceType { match path { - Path::PlaceTy(pty) => *pty.clone(), Path::Local(local) => self.local_type(*local), Path::Deref(path) => self.path_type(path).deref(), Path::TupleProj(path, idx) => self.path_type(path).tuple_proj(*idx), @@ -1111,38 +1099,54 @@ where } fn dropping_assumption(&mut self, path: &Path) -> Assumption { - let ty = self.path_type(path); - if ty.ty.is_mut() { - let mut builder = PlaceTypeBuilder::default(); - let (_, term) = builder.subsume(ty); - builder.push_formula(term.clone().mut_final().equal_to(term.mut_current())); - builder.build_assumption() - } else if ty.ty.is_own() { - self.dropping_assumption(&path.clone().deref()) - } else if let Some(tty) = ty.ty.as_tuple() { - (0..tty.elems.len()) - .map(|i| self.dropping_assumption(&path.clone().tuple_proj(i))) - .collect() - } else if let Some(ety) = ty.ty.as_enum() { + let PlaceType { + ty, + mut existentials, + term, + mut formula, + } = self.path_type(path); + formula.push_conj(self.dropping_formula_for_term(&mut existentials, &ty, term)); + Assumption::new(existentials, formula) + } + + fn dropping_formula_for_term( + &self, + existentials: &mut IndexVec, + ty: &rty::Type, + term: chc::Term, + ) -> chc::Body { + if ty.is_mut() { + term.clone().mut_final().equal_to(term.mut_current()).into() + } else if ty.is_own() { + let inner = &ty.as_pointer().unwrap().elem.ty; + self.dropping_formula_for_term(existentials, inner, term.box_current()) + } else if let Some(tty) = ty.as_tuple() { + let mut body = chc::Body::default(); + for (i, elem) in tty.elems.iter().enumerate() { + body.push_conj(self.dropping_formula_for_term( + existentials, + &elem.ty, + term.clone().tuple_proj(i), + )); + } + body + } else if let Some(ety) = ty.as_enum() { + let mut body = chc::Body::default(); + let enum_def = self.enum_defs.enum_def(&ety.symbol); let matcher_pred = chc::MatcherPred::new(ety.symbol.clone(), ety.arg_sorts()); - let PlaceType { - ty: _, - mut existentials, - term, - mut formula, - } = ty; - let mut pred_args = vec![]; for field_ty in enum_def.field_tys() { let mut field_rty = rty::RefinedType::unrefined(field_ty.clone().vacuous()); field_rty.instantiate_ty_params(ety.args.clone()); + let field_type = field_rty.ty; - let ev = existentials.push(field_rty.ty.to_sort()); - pred_args.push(chc::Term::var(ev.into())); + let ev = existentials.push(field_type.to_sort()); + let field_term = chc::Term::var(ev.into()); + pred_args.push(field_term.clone()); - if let Some(p) = field_rty.ty.as_pointer() { + if let Some(p) = field_type.as_pointer() { if matches!(&p.elem.ty, rty::Type::Enum(e) if e.symbol == ety.symbol) { // TODO: we need recursively defined drop_pred for the recursive ADTs! tracing::warn!("skipping recursive variant"); @@ -1150,42 +1154,18 @@ where } } - let field_pty = { - let rty::RefinedType { - ty: field_ty, - refinement, - } = field_rty; - let rty::Refinement { body, existentials } = refinement; - PlaceType { - ty: field_ty, - existentials, - term: chc::Term::var(ev.into()), - formula: body.map_var(|v| match v { - rty::RefinedTypeVar::Value => PlaceTypeVar::Existential(ev), - rty::RefinedTypeVar::Free(v) => PlaceTypeVar::Var(v), - // TODO: (but otherwise we can't distinguish field existentials from them...) - rty::RefinedTypeVar::Existential(_) => { - panic!("cannot handle existentials in field_rty") - } - }), - } - }; - - let Assumption { - existentials: assumption_existentials, - body: assumption_body, - } = self.dropping_assumption(&Path::PlaceTy(Box::new(field_pty))); - // dropping assumption should not generate any existential - assert!(assumption_existentials.is_empty()); - formula.push_conj(assumption_body); + body.push_conj(self.dropping_formula_for_term( + existentials, + &field_type, + field_term, + )); } pred_args.push(term); - formula.push_conj(chc::Atom::new(matcher_pred.into(), pred_args)); - - Assumption::new(existentials, formula) + body.push_conj(chc::Atom::new(matcher_pred.into(), pred_args)); + body } else { - Assumption::default() + chc::Body::default() } } diff --git a/tests/ui/fail/enum_tuple_mut_drop.rs b/tests/ui/fail/enum_tuple_mut_drop.rs new file mode 100644 index 00000000..aee45705 --- /dev/null +++ b/tests/ui/fail/enum_tuple_mut_drop.rs @@ -0,0 +1,21 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +#[allow(dead_code)] +enum Pair<'a> { + Two((&'a mut i32, &'a mut i32)), + None, +} + +#[thrust::callable] +fn check(a: &mut i32, b: &mut i32) { + *a = 10; + *b = 20; + { + let _p = Pair::Two((a, b)); + } + // wrong: `*a` is 10, not 11 + assert!(*a == 11); +} + +fn main() {} diff --git a/tests/ui/pass/enum_tuple_mut_drop.rs b/tests/ui/pass/enum_tuple_mut_drop.rs new file mode 100644 index 00000000..8972d70e --- /dev/null +++ b/tests/ui/pass/enum_tuple_mut_drop.rs @@ -0,0 +1,23 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +#[allow(dead_code)] +enum Pair<'a> { + Two((&'a mut i32, &'a mut i32)), + None, +} + +#[thrust::callable] +fn check(a: &mut i32, b: &mut i32) { + *a = 10; + *b = 20; + { + // Construct and drop the enum without mutating through the packed references. + let _p = Pair::Two((a, b)); + } + // Dropping resolves both prophecies to identity, so the values are unchanged. + assert!(*a == 10); + assert!(*b == 20); +} + +fn main() {}