diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index d5cefba..4d01eff 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -13,7 +13,7 @@ use crate::analyze; use crate::chc; use crate::pretty::PrettyDisplayExt as _; use crate::refine::{ - self, Assumption, BasicBlockType, Env, PlaceType, PlaceTypeVar, TempVarIdx, + self, Assumption, BasicBlockType, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, TemplateTypeGenerator, UnrefinedTypeGenerator, Var, }; use crate::rty::{ @@ -138,12 +138,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { Rvalue::Use(operand) => self.operand_type(operand), Rvalue::UnaryOp(op, operand) => { let operand_ty = self.operand_type(operand); - match (&operand_ty.ty, op) { + + let mut builder = PlaceTypeBuilder::default(); + let (operand_ty, operand_term) = builder.subsume(operand_ty); + match (&operand_ty, op) { (rty::Type::Bool, mir::UnOp::Not) => { - operand_ty.replace(|_, term| (rty::Type::Bool, term.not())) + builder.build(rty::Type::Bool, operand_term.not()) } (rty::Type::Int, mir::UnOp::Neg) => { - operand_ty.replace(|_, term| (rty::Type::Int, term.neg())) + builder.build(rty::Type::Int, operand_term.neg()) } _ => unimplemented!("ty={}, op={:?}", operand_ty.display(), op), } @@ -152,51 +155,47 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let (lhs, rhs) = *operands; let lhs_ty = self.operand_type(lhs); let rhs_ty = self.operand_type(rhs); - match (&lhs_ty.ty, op) { - (rty::Type::Int, mir::BinOp::Add) => lhs_ty - .merge(rhs_ty, |(lhs_ty, lhs_term), (_, rhs_term)| { - (lhs_ty, lhs_term.add(rhs_term)) - }), - (rty::Type::Int, mir::BinOp::Sub) => lhs_ty - .merge(rhs_ty, |(lhs_ty, lhs_term), (_, rhs_term)| { - (lhs_ty, lhs_term.sub(rhs_term)) - }), - (rty::Type::Int, mir::BinOp::Mul) => lhs_ty - .merge(rhs_ty, |(lhs_ty, lhs_term), (_, rhs_term)| { - (lhs_ty, lhs_term.mul(rhs_term)) - }), - (rty::Type::Int | rty::Type::Bool, mir::BinOp::Ge) => lhs_ty - .merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| { - (rty::Type::Bool, lhs_term.ge(rhs_term)) - }), - (rty::Type::Int | rty::Type::Bool, mir::BinOp::Gt) => lhs_ty - .merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| { - (rty::Type::Bool, lhs_term.gt(rhs_term)) - }), - (rty::Type::Int | rty::Type::Bool, mir::BinOp::Le) => lhs_ty - .merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| { - (rty::Type::Bool, lhs_term.le(rhs_term)) - }), - (rty::Type::Int | rty::Type::Bool, mir::BinOp::Lt) => lhs_ty - .merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| { - (rty::Type::Bool, lhs_term.lt(rhs_term)) - }), - (rty::Type::Int | rty::Type::Bool, mir::BinOp::Eq) => lhs_ty - .merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| { - (rty::Type::Bool, lhs_term.eq(rhs_term)) - }), - (rty::Type::Int | rty::Type::Bool, mir::BinOp::Ne) => lhs_ty - .merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| { - (rty::Type::Bool, lhs_term.ne(rhs_term)) - }), + + let mut builder = PlaceTypeBuilder::default(); + let (lhs_ty, lhs_term) = builder.subsume(lhs_ty); + let (_rhs_ty, rhs_term) = builder.subsume(rhs_ty); + match (&lhs_ty, op) { + (rty::Type::Int, mir::BinOp::Add) => { + builder.build(lhs_ty, rhs_term.add(lhs_term)) + } + (rty::Type::Int, mir::BinOp::Sub) => { + builder.build(lhs_ty, lhs_term.sub(rhs_term)) + } + (rty::Type::Int, mir::BinOp::Mul) => { + builder.build(lhs_ty, lhs_term.mul(rhs_term)) + } + (rty::Type::Int | rty::Type::Bool, mir::BinOp::Ge) => { + builder.build(rty::Type::Bool, lhs_term.ge(rhs_term)) + } + (rty::Type::Int | rty::Type::Bool, mir::BinOp::Gt) => { + builder.build(rty::Type::Bool, lhs_term.gt(rhs_term)) + } + (rty::Type::Int | rty::Type::Bool, mir::BinOp::Le) => { + builder.build(rty::Type::Bool, lhs_term.le(rhs_term)) + } + (rty::Type::Int | rty::Type::Bool, mir::BinOp::Lt) => { + builder.build(rty::Type::Bool, lhs_term.lt(rhs_term)) + } + (rty::Type::Int | rty::Type::Bool, mir::BinOp::Eq) => { + builder.build(rty::Type::Bool, lhs_term.eq(rhs_term)) + } + (rty::Type::Int | rty::Type::Bool, mir::BinOp::Ne) => { + builder.build(rty::Type::Bool, lhs_term.ne(rhs_term)) + } _ => unimplemented!("ty={}, op={:?}", lhs_ty.display(), op), } } Rvalue::Ref(_, mir::BorrowKind::Shared, place) => { let ty = self.env.place_type(self.elaborate_place(&place)); - ty.replace(|ty, term| { - (rty::PointerType::immut_to(ty).into(), chc::Term::box_(term)) - }) + + let mut builder = PlaceTypeBuilder::default(); + let (ty, term) = builder.subsume(ty); + builder.build(rty::PointerType::immut_to(ty).into(), chc::Term::box_(term)) } Rvalue::Aggregate(kind, fields) => { // elaboration: all fields are boxed @@ -240,12 +239,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let sort_args: Vec<_> = params.iter().map(|rty| rty.ty.to_sort()).collect(); let ty = rty::EnumType::new(ty_sym.clone(), params).into(); - PlaceType::aggregate( - field_tys, - |_| ty, - |fields_term| { - chc::Term::datatype_ctor(ty_sym, sort_args, v_sym, fields_term) - }, + + let mut builder = PlaceTypeBuilder::default(); + let mut field_terms = Vec::new(); + for field_ty in field_tys { + let (_, field_term) = builder.subsume(field_ty); + field_terms.push(field_term); + } + builder.build( + ty, + chc::Term::datatype_ctor(ty_sym, sort_args, v_sym, field_terms), ) } _ => PlaceType::tuple(field_tys), @@ -276,7 +279,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .expect("discriminant of non-enum") .symbol .clone(); - ty.replace(|_ty, term| (rty::Type::Int, chc::Term::datatype_discr(sym, term))) + + let mut builder = PlaceTypeBuilder::default(); + let (_, term) = builder.subsume(ty); + builder.build(rty::Type::Int, chc::Term::datatype_discr(sym, term)) } _ => unimplemented!( "rvalue={:?} ({:?})", @@ -383,20 +389,23 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { _ => unimplemented!(), }; - self.with_assumption( - discr_ty - .clone() - .into_assumption(|term| term.equal_to(target_term.clone())), - |ecx| { - callback(ecx, bb); - ecx.type_goto(bb, expected_ret); - }, - ); - negations.push( - discr_ty - .clone() - .into_assumption(|term| term.not_equal_to(target_term)), - ); + let pos_assumption = { + let mut builder = PlaceTypeBuilder::default(); + let (_, discr_term) = builder.subsume(discr_ty.clone()); + builder.push_formula(discr_term.equal_to(target_term.clone())); + builder.build_assumption() + }; + self.with_assumption(pos_assumption, |ecx| { + callback(ecx, bb); + ecx.type_goto(bb, expected_ret); + }); + let neg_assumption = { + let mut builder = PlaceTypeBuilder::default(); + let (_, discr_term) = builder.subsume(discr_ty.clone()); + builder.push_formula(discr_term.not_equal_to(target_term.clone())); + builder.build_assumption() + }; + negations.push(neg_assumption); } self.with_assumptions(negations, |ecx| { callback(ecx, targets.otherwise()); @@ -508,11 +517,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let local_ty = self.env.local_type(local); let rvalue_ty = self.rvalue_type(rvalue); if !rvalue_ty.ty.to_sort().is_singleton() { - self.env.assume( - local_ty.merge_into_assumption(rvalue_ty, |local_term, rvalue_term| { - local_term.mut_final().equal_to(rvalue_term) - }), - ); + let mut builder = PlaceTypeBuilder::default(); + let (_, local_term) = builder.subsume(local_ty); + let (_, rvalue_term) = builder.subsume(rvalue_ty); + builder.push_formula(local_term.mut_final().equal_to(rvalue_term)); + let assumption = builder.build_assumption(); + self.env.assume(assumption); } } diff --git a/src/refine.rs b/src/refine.rs index 9c058cf..60f29f4 100644 --- a/src/refine.rs +++ b/src/refine.rs @@ -5,7 +5,7 @@ mod basic_block; pub use basic_block::BasicBlockType; mod env; -pub use env::{Assumption, Env, PlaceType, PlaceTypeVar, TempVarIdx, Var}; +pub use env::{Assumption, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, Var}; use crate::chc::DatatypeSymbol; use rustc_middle::ty as mir_ty; diff --git a/src/refine/env.rs b/src/refine/env.rs index 26e1ad3..e647765 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -222,6 +222,75 @@ impl PlaceTypeVar { } } +/// A builder for `PlaceType` and `Assumption`. +/// +/// We often combine multiple [`PlaceType`]s and [`rty::RefinedType`]s into a single one in order to +/// construct another [`PlaceType`], while retaining formulas from each. [`PlaceTypeBuilder`] helps +/// this by properly managing existential variable indices. +#[derive(Debug, Clone, Default)] +pub struct PlaceTypeBuilder { + existentials: IndexVec, + formula: chc::Body, +} + +impl PlaceTypeBuilder { + pub fn subsume(&mut self, pty: PlaceType) -> (rty::Type, chc::Term) { + let PlaceType { + ty, + existentials, + term, + formula, + } = pty; + self.formula + .push_conj(formula.map_var(|v| v.shift_existential(self.existentials.len()))); + let term = term.map_var(|v| v.shift_existential(self.existentials.len())); + self.existentials.extend(existentials); + (ty, term) + } + + pub fn subsume_rty( + &mut self, + rty: rty::RefinedType, + ) -> (rty::Type, rty::ExistentialVarIdx) { + let rty::RefinedType { ty, refinement } = rty; + let rty::Refinement { existentials, body } = refinement; + let value_var_ex = self.existentials.push(ty.to_sort()); + self.formula.push_conj(body.map_var(|v| match v { + rty::RefinedTypeVar::Value => PlaceTypeVar::Existential(value_var_ex), + rty::RefinedTypeVar::Existential(ev) => { + PlaceTypeVar::Existential(ev + self.existentials.len()) + } + rty::RefinedTypeVar::Free(v) => PlaceTypeVar::Var(v), + })); + self.existentials.extend(existentials); + (ty, value_var_ex) + } + + pub fn push_formula(&mut self, formula: impl Into>) { + self.formula.push_conj(formula); + } + + pub fn push_existential(&mut self, sort: chc::Sort) -> rty::ExistentialVarIdx { + self.existentials.push(sort) + } + + pub fn build(self, ty: rty::Type, term: chc::Term) -> PlaceType { + PlaceType { + ty, + existentials: self.existentials, + term, + formula: self.formula, + } + } + + pub fn build_assumption(self) -> Assumption { + Assumption { + existentials: self.existentials, + body: self.formula, + } + } +} + #[derive(Debug, Clone)] pub struct PlaceType { pub ty: rty::Type, @@ -302,82 +371,26 @@ impl PlaceType { } } - pub fn into_assumption(self, term_to_atom: F) -> Assumption - where - F: FnOnce(chc::Term) -> chc::Atom, - { - let PlaceType { - ty: _, - existentials, - term, - mut formula, - } = self; - formula.push_conj(term_to_atom(term)); - Assumption::new(existentials, formula) - } - pub fn deref(self) -> PlaceType { - let PlaceType { - ty: inner_ty, - mut existentials, - term: inner_term, - mut formula, - } = self; + let mut builder = PlaceTypeBuilder::default(); + let (inner_ty, inner_term) = builder.subsume(self); let inner_ty = inner_ty.into_pointer().unwrap(); - let rty::RefinedType { ty, refinement } = *inner_ty.elem; - let rty::Refinement { - existentials: inner_existentials, - body: inner_formula, - } = refinement; - let value_var_ex = existentials.push(ty.to_sort()); + let (ty, value_var_ex) = builder.subsume_rty(*inner_ty.elem); + let term = chc::Term::var(value_var_ex.into()); - formula.push_conj(term.clone().equal_to(inner_ty.kind.deref_term(inner_term))); - formula.push_conj(inner_formula.map_var(|v| match v { - rty::RefinedTypeVar::Value => PlaceTypeVar::Existential(value_var_ex), - rty::RefinedTypeVar::Existential(ev) => { - PlaceTypeVar::Existential(ev + existentials.len()) - } - rty::RefinedTypeVar::Free(v) => PlaceTypeVar::Var(v), - })); - existentials.extend(inner_existentials); - PlaceType { - ty, - existentials, - term, - formula, - } + builder.push_formula(term.clone().equal_to(inner_ty.kind.deref_term(inner_term))); + builder.build(ty, term) } pub fn tuple_proj(self, idx: usize) -> PlaceType { - let PlaceType { - ty: inner_ty, - mut existentials, - term: inner_term, - mut formula, - } = self; + let mut builder = PlaceTypeBuilder::default(); + let (inner_ty, inner_term) = builder.subsume(self); let inner_ty = inner_ty.into_tuple().unwrap(); - let rty::RefinedType { ty, refinement } = inner_ty.elems[idx].clone(); - let rty::Refinement { - existentials: inner_existentials, - body: inner_formula, - } = refinement; - let value_var_ex = existentials.push(ty.to_sort()); + let (ty, value_var_ex) = builder.subsume_rty(inner_ty.elems[idx].clone()); + let term = chc::Term::var(value_var_ex.into()); - formula.push_conj(term.clone().equal_to(inner_term.tuple_proj(idx))); - formula.push_conj(inner_formula.map_var(|v| match v { - rty::RefinedTypeVar::Value => PlaceTypeVar::Existential(value_var_ex), - rty::RefinedTypeVar::Existential(ev) => { - PlaceTypeVar::Existential(ev + existentials.len()) - } - rty::RefinedTypeVar::Free(v) => PlaceTypeVar::Var(v), - })); - existentials.extend(inner_existentials); - PlaceType { - ty, - existentials, - term, - formula, - } + builder.push_formula(term.clone().equal_to(inner_term.tuple_proj(idx))); + builder.build(ty, term) } pub fn downcast( @@ -386,12 +399,8 @@ impl PlaceType { field_idx: FieldIdx, enum_defs: &HashMap, ) -> PlaceType { - let PlaceType { - ty: inner_ty, - mut existentials, - term: inner_term, - mut formula, - } = self; + let mut builder = PlaceTypeBuilder::default(); + let (inner_ty, inner_term) = builder.subsume(self); let inner_ty = inner_ty.into_enum().unwrap(); let def = &enum_defs[&inner_ty.symbol]; let variant = &def.variants[variant_idx]; @@ -401,23 +410,13 @@ impl PlaceType { for field_ty in variant.field_tys.clone() { let mut rty = rty::RefinedType::unrefined(field_ty.vacuous()); rty.instantiate_ty_params(inner_ty.args.clone()); - let rty::RefinedType { ty, refinement } = rty.boxed(); + let (ty, field_ex_var) = builder.subsume_rty(rty.boxed()); - let field_ex_var = existentials.push(ty.to_sort()); field_terms.push(chc::Term::var(field_ex_var.into())); field_tys.push(ty); - - formula.push_conj(refinement.body.map_var(|v| match v { - rty::RefinedTypeVar::Value => PlaceTypeVar::Existential(field_ex_var), - rty::RefinedTypeVar::Existential(ev) => { - PlaceTypeVar::Existential(ev + existentials.len()) - } - rty::RefinedTypeVar::Free(v) => PlaceTypeVar::Var(v), - })); - existentials.extend(refinement.existentials); } - formula.push_conj( + builder.push_formula( chc::Term::datatype_ctor( def.name.clone(), inner_ty.arg_sorts(), @@ -429,113 +428,15 @@ impl PlaceType { let ty = field_tys[field_idx.index()].clone(); let term = field_terms[field_idx.index()].clone(); - PlaceType { - ty, - existentials, - term, - formula, - } + builder.build(ty, term) } pub fn boxed(self) -> PlaceType { - let PlaceType { - ty: inner_ty, - existentials, - term: inner_term, - formula, - } = self; + let mut builder = PlaceTypeBuilder::default(); + let (inner_ty, inner_term) = builder.subsume(self); let term = chc::Term::box_(inner_term); let ty = rty::PointerType::own(inner_ty).into(); - PlaceType { - ty, - existentials, - term, - formula, - } - } - - pub fn replace(self, f: F) -> PlaceType - where - F: FnOnce( - rty::Type, - chc::Term, - ) -> (rty::Type, chc::Term), - { - let PlaceType { - ty, - existentials, - term, - formula, - } = self; - let (ty, term) = f(ty, term); - PlaceType { - ty, - existentials, - term, - formula, - } - } - - pub fn merge_into_assumption(self, other: PlaceType, f: F) -> Assumption - where - F: FnOnce(chc::Term, chc::Term) -> chc::Atom, - { - let PlaceType { - ty: _ty1, - mut existentials, - term: term1, - mut formula, - } = self; - let PlaceType { - ty: _ty2, - existentials: evs2, - term: term2, - formula: formula2, - } = other; - let atom = f( - term1, - term2.map_var(|v| v.shift_existential(existentials.len())), - ); - formula.push_conj(formula2.map_var(|v| v.shift_existential(existentials.len()))); - formula.push_conj(atom); - existentials.extend(evs2); - Assumption::new(existentials, formula) - } - - pub fn merge(self, other: PlaceType, f: F) -> PlaceType - where - F: FnOnce( - (rty::Type, chc::Term), - (rty::Type, chc::Term), - ) -> (rty::Type, chc::Term), - { - let PlaceType { - ty: ty1, - mut existentials, - term: term1, - mut formula, - } = self; - let PlaceType { - ty: ty2, - existentials: evs2, - term: term2, - formula: formula2, - } = other; - let (ty, term) = f( - (ty1, term1), - ( - ty2, - term2.map_var(|v| v.shift_existential(existentials.len())), - ), - ); - formula.push_conj(formula2.map_var(|v| v.shift_existential(existentials.len()))); - existentials.extend(evs2); - PlaceType { - ty, - existentials, - term, - formula, - } + builder.build(ty, term) } pub fn mut_with_proph_term(self, proph: chc::Term) -> PlaceType { @@ -544,58 +445,29 @@ impl PlaceType { } pub fn mut_with(self, proph: PlaceType) -> PlaceType { - self.merge(proph, |(ty1, term1), (_, term2)| - // TODO: check ty1 = ty2 - (rty::PointerType::mut_to(ty1).into(), chc::Term::mut_(term1, term2))) - } - - pub fn aggregate(ptys: I, make_ty: F, make_term: G) -> PlaceType - where - I: IntoIterator, - F: FnOnce(Vec>) -> rty::Type, - G: FnOnce(Vec>) -> chc::Term, - { - #[derive(Default)] - struct State { - tys: Vec>, - terms: Vec>, - existentials: IndexVec, - formula: chc::Body, - } - let State { - tys, - terms, - existentials, - formula, - } = ptys - .into_iter() - .fold(Default::default(), |mut st: State, ty| { - let PlaceType { - ty, - existentials, - term, - formula, - } = ty; - st.tys.push(ty); - st.terms - .push(term.map_var(|v| v.shift_existential(st.existentials.len()))); - st.formula - .push_conj(formula.map_var(|v| v.shift_existential(st.existentials.len()))); - st.existentials.extend(existentials); - st - }); - let ty = make_ty(tys); - let term = make_term(terms); - PlaceType { - ty, - existentials, - term, - formula, + let mut builder = PlaceTypeBuilder::default(); + let (ty1, term1) = builder.subsume(self); + let (_ty2, term2) = builder.subsume(proph); + // TODO: check ty1 = ty2 + let ty = rty::PointerType::mut_to(ty1).into(); + let term = chc::Term::mut_(term1, term2); + builder.build(ty, term) + } + + pub fn tuple(ptys: Vec) -> PlaceType { + let mut builder = PlaceTypeBuilder::default(); + let mut tys = Vec::new(); + let mut terms = Vec::new(); + + for ty in ptys { + let (ty, term) = builder.subsume(ty); + tys.push(ty); + terms.push(term); } - } - pub fn tuple(tys: Vec) -> PlaceType { - PlaceType::aggregate(tys, |tys| rty::TupleType::new(tys).into(), chc::Term::tuple) + let ty = rty::TupleType::new(tys); + let term = chc::Term::tuple(terms); + builder.build(ty.into(), term) } pub fn enum_( @@ -604,50 +476,27 @@ impl PlaceType { discr: TempVarIdx, field_tys: Vec, ) -> PlaceType { - #[derive(Default)] - struct State { - existentials: IndexVec, - terms: Vec>, - formula: chc::Body, + let mut builder = PlaceTypeBuilder::default(); + let mut terms = Vec::new(); + + for ty in field_tys { + let (_, term) = builder.subsume(ty); + terms.push(term); } - let State { - mut existentials, - terms, - mut formula, - } = field_tys - .into_iter() - .fold(Default::default(), |mut st: State, ty| { - let PlaceType { - ty: _, - existentials, - term, - formula, - } = ty; - st.terms - .push(term.map_var(|v| v.shift_existential(st.existentials.len()))); - st.formula - .push_conj(formula.map_var(|v| v.shift_existential(st.existentials.len()))); - st.existentials.extend(existentials); - st - }); + let ty: rty::Type<_> = enum_ty.clone().into(); - let value_var_ev = existentials.push(ty.to_sort()); + let value_var_ev = builder.push_existential(ty.to_sort()); let term = chc::Term::var(value_var_ev.into()); let mut pred_args = terms; pred_args.push(chc::Term::var(value_var_ev.into())); - formula.push_conj(chc::Atom::new(matcher_pred, pred_args)); - formula.push_conj( + builder.push_formula(chc::Atom::new(matcher_pred, pred_args)); + builder.push_formula( chc::Term::var(discr.into()).equal_to(chc::Term::datatype_discr( enum_ty.symbol.clone(), chc::Term::var(value_var_ev.into()), )), ); - PlaceType { - ty, - existentials, - term, - formula, - } + builder.build(ty, term) } } @@ -1252,10 +1101,10 @@ impl Env { fn dropping_assumption(&mut self, path: &Path) -> Assumption { let ty = self.path_type(path); if ty.ty.is_mut() { - ty.into_assumption(|term| { - let term = term.map_var(Into::into); - term.clone().mut_final().equal_to(term.mut_current()) - }) + 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() {