diff --git a/crates/flux-common/src/dbg.rs b/crates/flux-common/src/dbg.rs index 1876b8c875..08de577f1e 100644 --- a/crates/flux-common/src/dbg.rs +++ b/crates/flux-common/src/dbg.rs @@ -72,7 +72,7 @@ pub use crate::_basic_block_start as basic_block_start; macro_rules! _statement{ ($pos:literal, $stmt:expr, $infcx:expr, $env:expr, $span:expr, $checker:expr) => {{ if config::dump_checker_trace() { - let rcx = $infcx.rcx(); + let rcx = $infcx.cursor(); let ck = $checker; let genv = ck.genv; let local_names = &ck.body.local_names; diff --git a/crates/flux-infer/src/evars.rs b/crates/flux-infer/src/evars.rs index e56d3d9692..13fcb3f4d3 100644 --- a/crates/flux-infer/src/evars.rs +++ b/crates/flux-infer/src/evars.rs @@ -6,7 +6,7 @@ use flux_middle::{ rty::{fold::TypeFoldable, EVid, Expr}, }; -use crate::refine_tree::{RefineCtxt, Snapshot}; +use crate::refine_tree::Marker; #[derive(Default, Debug)] pub(crate) struct EVarStore { @@ -16,12 +16,12 @@ pub(crate) struct EVarStore { pub(crate) enum EVarState { Solved(Expr), - Unsolved(Snapshot), + Unsolved(Marker), } impl EVarStore { - pub(crate) fn fresh(&mut self, rcx: &RefineCtxt) -> EVid { - let evid = self.evars.push(EVarState::Unsolved(rcx.snapshot())); + pub(crate) fn fresh(&mut self, marker: Marker) -> EVid { + let evid = self.evars.push(EVarState::Unsolved(marker)); if let Some(scope) = self.scopes.last_mut() { scope.push(evid); } diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs index 7dd9249fb9..e54cc232ee 100644 --- a/crates/flux-infer/src/infer.rs +++ b/crates/flux-infer/src/infer.rs @@ -27,7 +27,7 @@ use rustc_span::Span; use crate::{ evars::{EVarState, EVarStore}, fixpoint_encoding::{FixQueryCache, FixpointCtxt, KVarEncoding, KVarGen}, - refine_tree::{AssumeInvariants, RefineCtxt, RefineTree, Scope, Snapshot, Unpacker}, + refine_tree::{AssumeInvariants, Cursor, Marker, RefineTree, Scope, Unpacker}, }; pub type InferResult = std::result::Result; @@ -149,7 +149,7 @@ impl<'genv, 'tcx> InferCtxtRoot<'genv, 'tcx> { genv: self.genv, region_infcx, def_id, - rcx: self.refine_tree.refine_ctxt_at_root(), + cursor: self.refine_tree.cursor_at_root(), inner: &self.inner, check_overflow: self.opts.check_overflow, } @@ -209,9 +209,9 @@ pub struct InferCtxt<'infcx, 'genv, 'tcx> { pub genv: GlobalEnv<'genv, 'tcx>, pub region_infcx: &'infcx rustc_infer::infer::InferCtxt<'tcx>, pub def_id: DefId, - rcx: RefineCtxt<'infcx>, - inner: &'infcx RefCell, pub check_overflow: bool, + cursor: Cursor<'infcx>, + inner: &'infcx RefCell, } struct InferCtxtInner { @@ -278,12 +278,12 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> { /// Generate a fresh kvar in the current scope. See [`KVarGen::fresh`]. pub fn fresh_kvar(&self, binders: &[BoundVariableKinds], encoding: KVarEncoding) -> Expr { let inner = &mut *self.inner.borrow_mut(); - inner.kvars.fresh(binders, self.rcx.vars(), encoding) + inner.kvars.fresh(binders, self.cursor.vars(), encoding) } fn fresh_evar(&self) -> Expr { let evars = &mut self.inner.borrow_mut().evars; - Expr::evar(evars.fresh(&self.rcx)) + Expr::evar(evars.fresh(self.cursor.marker())) } pub fn unify_exprs(&self, a: &Expr, b: &Expr) { @@ -292,8 +292,8 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> { } let evars = &mut self.inner.borrow_mut().evars; if let ExprKind::Var(Var::EVar(evid)) = b.kind() - && let EVarState::Unsolved(snapshot) = evars.get(*evid) - && !snapshot.has_free_vars(a) + && let EVarState::Unsolved(marker) = evars.get(*evid) + && !marker.has_free_vars(a) { evars.solve(*evid, a.clone()); } @@ -351,59 +351,60 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> { self.genv.tcx() } - pub fn rcx(&self) -> &RefineCtxt<'infcx> { - &self.rcx + pub fn cursor(&self) -> &Cursor<'infcx> { + &self.cursor } } -/// Methods that modify or advance the [`RefineTree`] cursor +/// Methods that interact with the underlying [`Cursor`] impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> { pub fn change_item<'a>( &'a mut self, def_id: LocalDefId, region_infcx: &'a rustc_infer::infer::InferCtxt<'tcx>, ) -> InferCtxt<'a, 'genv, 'tcx> { - InferCtxt { def_id: def_id.to_def_id(), rcx: self.rcx.branch(), region_infcx, ..*self } + InferCtxt { + def_id: def_id.to_def_id(), + cursor: self.cursor.branch(), + region_infcx, + ..*self + } } - pub fn change_root( - &mut self, - snapshot: &Snapshot, - clear_children: bool, - ) -> InferCtxt<'_, 'genv, 'tcx> { - InferCtxt { rcx: self.rcx.change_root(snapshot, clear_children).unwrap(), ..*self } + pub fn move_to(&mut self, marker: &Marker, clear_children: bool) -> InferCtxt<'_, 'genv, 'tcx> { + InferCtxt { cursor: self.cursor.move_to(marker, clear_children).unwrap(), ..*self } } pub fn branch(&mut self) -> InferCtxt<'_, 'genv, 'tcx> { - InferCtxt { rcx: self.rcx.branch(), ..*self } + InferCtxt { cursor: self.cursor.branch(), ..*self } } pub fn define_vars(&mut self, sort: &Sort) -> Expr { - self.rcx.define_vars(sort) + self.cursor.define_vars(sort) } pub fn define_var(&mut self, sort: &Sort) -> Name { - self.rcx.define_var(sort) + self.cursor.define_var(sort) } pub fn check_pred(&mut self, pred: impl Into, tag: Tag) { - self.rcx.check_pred(pred, tag); + self.cursor.check_pred(pred, tag); } pub fn assume_pred(&mut self, pred: impl Into) { - self.rcx.assume_pred(pred); + self.cursor.assume_pred(pred); } pub fn unpack(&mut self, ty: &Ty) -> Ty { self.hoister(false).hoist(ty) } - pub fn snapshot(&self) -> Snapshot { - self.rcx.snapshot() + pub fn marker(&self) -> Marker { + self.cursor.marker() } pub fn hoister(&mut self, assume_invariants: bool) -> Hoister> { - self.rcx.hoister(if assume_invariants { + self.cursor.hoister(if assume_invariants { AssumeInvariants::yes(self.check_overflow) } else { AssumeInvariants::No @@ -411,17 +412,17 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> { } pub fn assume_invariants(&mut self, ty: &Ty) { - self.rcx.assume_invariants(ty, self.check_overflow); + self.cursor.assume_invariants(ty, self.check_overflow); } fn check_impl(&mut self, pred1: impl Into, pred2: impl Into, tag: Tag) { - self.rcx.check_impl(pred1, pred2, tag); + self.cursor.check_impl(pred1, pred2, tag); } } impl std::fmt::Debug for InferCtxt<'_, '_, '_> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - std::fmt::Debug::fmt(&self.rcx, f) + std::fmt::Debug::fmt(&self.cursor, f) } } diff --git a/crates/flux-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs index 7d79005021..4de91ff047 100644 --- a/crates/flux-infer/src/refine_tree.rs +++ b/crates/flux-infer/src/refine_tree.rs @@ -30,10 +30,10 @@ use crate::{ /// whose satisfiability implies the safety of a function. /// /// We try to hide the representation of the tree as much as possible and only a couple of operations -/// can be used to manipulate the structure of the tree explicitly. Instead, the tree is mostly constructed -/// implicitly via a restricted api provided by [`RefineCtxt`]. Some methods operate on *nodes* of -/// the tree which we try to keep abstract, but it is important to remember that there's an underlying -/// tree. +/// can be used to manipulate the structure of the tree explicitly. Instead, the tree is mostly +/// constructed implicitly via a restricted api provided by [`Cursor`]. Some methods operate on *nodes* +/// of the tree which we try to keep abstract, but it is important to remember that there's an +/// underlying tree. /// /// The current implementation uses [`Rc`] and [`RefCell`] to represent the tree, but we ensure /// statically that the [`RefineTree`] is the single owner of the data and require a mutable reference @@ -46,41 +46,182 @@ pub struct RefineTree { root: NodePtr, } -/// A *refine*ment *c*on*t*e*xt* tracks all the refinement parameters and predicates -/// available in a particular path during type-checking. For example, consider the following -/// program: -/// -/// ```ignore -/// #[flux::sig(fn(i32[@a0], i32{v : v > a0})) -> i32] -/// fn add(x: i32, y: i32) -> i32 { -/// x + y -/// } -/// ``` -/// -/// At the beginning of the function, the refinement context will be `{a0: int, a1: int, a1 > a0}`, -/// where `a1` is a freshly generated name for the existential variable in the refinement of `y`. -/// -/// More specifically, a [`RefineCtxt`] represents a path from the root to some internal node in a -/// [refinement tree]. +impl RefineTree { + pub(crate) fn new(params: Vec<(Var, Sort)>) -> RefineTree { + let root = + Node { kind: NodeKind::Root(params), nbindings: 0, parent: None, children: vec![] }; + let root = NodePtr(Rc::new(RefCell::new(root))); + RefineTree { root } + } + + pub(crate) fn simplify(&mut self, defns: &SpecFuncDefns) { + self.root.borrow_mut().simplify(defns); + } + + pub(crate) fn into_fixpoint( + self, + cx: &mut FixpointCtxt, + ) -> QueryResult { + Ok(self + .root + .borrow() + .to_fixpoint(cx)? + .unwrap_or(fixpoint::Constraint::TRUE)) + } + + pub(crate) fn cursor_at_root(&mut self) -> Cursor { + Cursor { ptr: NodePtr(Rc::clone(&self.root)), tree: self } + } + + pub(crate) fn replace_evars(&mut self, evars: &EVarStore) -> Result<(), EVid> { + self.root.borrow_mut().replace_evars(evars) + } +} + +/// A cursor into the [refinement tree]. More specifically, a [`Cursor`] represents a path from the +/// root to some internal node in a [refinement tree]. /// /// [refinement tree]: RefineTree -pub struct RefineCtxt<'a> { +pub struct Cursor<'a> { tree: &'a mut RefineTree, ptr: NodePtr, } -/// A snapshot of a [`RefineCtxt`] at a particular point during type-checking. Alternatively, a -/// snapshot corresponds to a reference to a node in a [refinement tree]. Snapshots may become invalid -/// if the underlying node is [`cleared`]. +impl<'a> Cursor<'a> { + /// Moves the cursor to the specified [marker]. If `clear_children` is `true`, all children of + /// the node are removed after moving the cursor, invalidating any markers pointing to a node + /// within those children. + /// + /// [marker]: Marker + pub(crate) fn move_to(&mut self, marker: &Marker, clear_children: bool) -> Option { + let ptr = marker.ptr.upgrade()?; + if clear_children { + ptr.borrow_mut().children.clear(); + } + Some(Cursor { ptr, tree: self.tree }) + } + + /// Returns a marker to the current node + #[must_use] + pub(crate) fn marker(&self) -> Marker { + Marker { ptr: NodePtr::downgrade(&self.ptr) } + } + + #[must_use] + pub(crate) fn branch(&mut self) -> Cursor { + Cursor { tree: self.tree, ptr: NodePtr::clone(&self.ptr) } + } + + pub(crate) fn vars(&self) -> impl Iterator { + // TODO(nilehmann) we could incrementally cache the scope + self.ptr.scope().into_iter() + } + + #[expect(dead_code, reason = "used for debugging")] + pub(crate) fn push_trace(&mut self, trace: TypeTrace) { + self.ptr = self.ptr.push_node(NodeKind::Trace(trace)); + } + + /// Defines a fresh refinement variable with the given `sort` and advance the cursor to the new + /// node. It returns the freshly generated name for the variable. + pub(crate) fn define_var(&mut self, sort: &Sort) -> Name { + let fresh = Name::from_usize(self.ptr.next_name_idx()); + self.ptr = self.ptr.push_node(NodeKind::ForAll(fresh, sort.clone())); + fresh + } + + /// Given a [`sort`] that may contain aggregate sorts ([tuple] or [adt]), it destructs the sort + /// recursively, generating multiple fresh variables and returning an "eta-expanded" expression + /// of fresh variables. This is in contrast to generating a single fresh variable of aggregate + /// sort. + /// + /// For example, given the sort `(int, (bool, int))` it returns `(a0, (a1, a2))` for fresh variables + /// `a0: int`, `a1: bool`, and `a2: int`. + /// + /// [`sort`]: Sort + /// [tuple]: Sort::Tuple + /// [adt]: flux_middle::rty::SortCtor::Adt + pub(crate) fn define_vars(&mut self, sort: &Sort) -> Expr { + Expr::fold_sort(sort, |sort| Expr::fvar(self.define_var(sort))) + } + + /// Pushes an [assumption] and moves the cursor into the new node. + /// + /// [assumption]: NodeKind::Assumption + pub(crate) fn assume_pred(&mut self, pred: impl Into) { + let pred = pred.into(); + if !pred.is_trivially_true() { + self.ptr = self.ptr.push_node(NodeKind::Assumption(pred)); + } + } + + /// Pushes a predicate that must be true assuming variables and predicates in the current branch + /// of the tree (i.e., it pushes a [`NodeKind::Head`]). This methods does not advance the cursor. + pub(crate) fn check_pred(&mut self, pred: impl Into, tag: Tag) { + let pred = pred.into(); + if !pred.is_trivially_true() { + self.ptr.push_node(NodeKind::Head(pred, tag)); + } + } + + /// Convenience method to push an assumption followed by a predicate that needs to be checked. + /// This method does not advance the cursor. + pub(crate) fn check_impl(&mut self, pred1: impl Into, pred2: impl Into, tag: Tag) { + self.ptr + .push_node(NodeKind::Assumption(pred1.into())) + .push_node(NodeKind::Head(pred2.into(), tag)); + } + + pub(crate) fn hoister( + &mut self, + assume_invariants: AssumeInvariants, + ) -> Hoister> { + Hoister::with_delegate(Unpacker { cursor: self, assume_invariants }).transparent() + } + + pub(crate) fn assume_invariants(&mut self, ty: &Ty, overflow_checking: bool) { + struct Visitor<'a, 'b> { + cursor: &'a mut Cursor<'b>, + overflow_checking: bool, + } + impl TypeVisitor for Visitor<'_, '_> { + fn visit_bty(&mut self, bty: &BaseTy) -> ControlFlow { + match bty { + BaseTy::Adt(adt_def, substs) if adt_def.is_box() => substs.visit_with(self), + BaseTy::Ref(_, ty, _) => ty.visit_with(self), + BaseTy::Tuple(tys) => tys.visit_with(self), + _ => ControlFlow::Continue(()), + } + } + + fn visit_ty(&mut self, ty: &Ty) -> ControlFlow { + if let TyKind::Indexed(bty, idx) = ty.kind() + && !idx.has_escaping_bvars() + { + for invariant in bty.invariants(self.overflow_checking) { + let invariant = invariant.apply(idx); + self.cursor.assume_pred(&invariant); + } + } + ty.super_visit_with(self) + } + } + ty.visit_with(&mut Visitor { cursor: self, overflow_checking }); + } +} + +/// A marker is a pointer to a node in the [refinement tree] that can be used to query information +/// about that node or to move the cursor. A marker may become invalid if the underlying node is +/// [cleared]. /// -/// [`cleared`]: RefineCtxt::clear_children +/// [cleared]: Cursor::move_to /// [refinement tree]: RefineTree -pub struct Snapshot { +pub struct Marker { ptr: WeakNodePtr, } -impl Snapshot { - /// Returns the [`scope`] at the snapshot if it is still valid or [`None`] otherwise. +impl Marker { + /// Returns the [`scope`] at the marker if it is still valid or [`None`] otherwise. /// /// [`scope`]: Scope pub fn scope(&self) -> Option { @@ -91,7 +232,7 @@ impl Snapshot { let ptr = self .ptr .upgrade() - .unwrap_or_else(|| tracked_span_bug!("`has_free_vars` called on invalid `Snapshot`")); + .unwrap_or_else(|| tracked_span_bug!("`has_free_vars` called on invalid `Marker`")); let nbindings = ptr.next_name_idx(); @@ -102,8 +243,8 @@ impl Snapshot { /// A list of refinement variables and their sorts. #[derive(PartialEq, Eq)] pub struct Scope { - bindings: IndexVec, params: Vec<(Var, Sort)>, + bindings: IndexVec, } impl Scope { @@ -208,158 +349,12 @@ impl WeakNodePtr { enum NodeKind { /// List of const and refinement generics Root(Vec<(Var, Sort)>), - /// Used for debugging. See [`TypeTrace`] - Trace(TypeTrace), ForAll(Name, Sort), Assumption(Expr), Head(Expr, Tag), True, -} - -impl RefineTree { - pub(crate) fn new(params: Vec<(Var, Sort)>) -> RefineTree { - let root = - Node { kind: NodeKind::Root(params), nbindings: 0, parent: None, children: vec![] }; - let root = NodePtr(Rc::new(RefCell::new(root))); - RefineTree { root } - } - - pub(crate) fn simplify(&mut self, defns: &SpecFuncDefns) { - self.root.borrow_mut().simplify(defns); - } - - pub(crate) fn into_fixpoint( - self, - cx: &mut FixpointCtxt, - ) -> QueryResult { - Ok(self - .root - .borrow() - .to_fixpoint(cx)? - .unwrap_or(fixpoint::Constraint::TRUE)) - } - - pub(crate) fn refine_ctxt_at_root(&mut self) -> RefineCtxt { - RefineCtxt { ptr: NodePtr(Rc::clone(&self.root)), tree: self } - } - - pub(crate) fn replace_evars(&mut self, evars: &EVarStore) -> Result<(), EVid> { - self.root.borrow_mut().replace_evars(evars) - } -} - -impl<'rcx> RefineCtxt<'rcx> { - pub(crate) fn change_root( - &mut self, - snapshot: &Snapshot, - clear_children: bool, - ) -> Option { - let ptr = snapshot.ptr.upgrade()?; - if clear_children { - ptr.borrow_mut().children.clear(); - } - Some(RefineCtxt { ptr, tree: self.tree }) - } - - pub(crate) fn snapshot(&self) -> Snapshot { - Snapshot { ptr: NodePtr::downgrade(&self.ptr) } - } - - #[must_use] - pub(crate) fn branch(&mut self) -> RefineCtxt { - RefineCtxt { tree: self.tree, ptr: NodePtr::clone(&self.ptr) } - } - - pub(crate) fn vars(&self) -> impl Iterator { - // TODO(nilehmann) we could incrementally cache the scope by only iterating over the nodes - // we haven't yet visited - self.ptr.scope().into_iter() - } - - #[expect(dead_code, reason = "used for debugging")] - pub(crate) fn push_trace(&mut self, trace: TypeTrace) { - self.ptr = self.ptr.push_node(NodeKind::Trace(trace)); - } - - /// Defines a fresh refinement variable with the given `sort`. It returns the freshly generated - /// name for the variable. - pub(crate) fn define_var(&mut self, sort: &Sort) -> Name { - let fresh = Name::from_usize(self.ptr.next_name_idx()); - self.ptr = self.ptr.push_node(NodeKind::ForAll(fresh, sort.clone())); - fresh - } - - /// Given a [`sort`] that may contain aggregate sorts ([tuple] or [adt]), it destructs the sort - /// recursively, generating multiple fresh variables and returning an "eta-expanded" expression - /// of fresh variables. This is in contrast to generating a single fresh variable of aggregate - /// sort. - /// - /// For example, given the sort `(int, (bool, int))` it returns `(a0, (a1, a2))` for fresh variables - /// `a0: int`, `a1: bool`, and `a2: int`. - /// - /// [`sort`]: Sort - /// [tuple]: Sort::Tuple - /// [adt]: flux_middle::rty::SortCtor::Adt - pub(crate) fn define_vars(&mut self, sort: &Sort) -> Expr { - Expr::fold_sort(sort, |sort| Expr::fvar(self.define_var(sort))) - } - - pub(crate) fn assume_pred(&mut self, pred: impl Into) { - let pred = pred.into(); - if !pred.is_trivially_true() { - self.ptr = self.ptr.push_node(NodeKind::Assumption(pred)); - } - } - - pub(crate) fn check_pred(&mut self, pred: impl Into, tag: Tag) { - let pred = pred.into(); - if !pred.is_trivially_true() { - self.ptr.push_node(NodeKind::Head(pred, tag)); - } - } - - pub(crate) fn check_impl(&mut self, pred1: impl Into, pred2: impl Into, tag: Tag) { - self.ptr - .push_node(NodeKind::Assumption(pred1.into())) - .push_node(NodeKind::Head(pred2.into(), tag)); - } - - pub(crate) fn hoister( - &mut self, - assume_invariants: AssumeInvariants, - ) -> Hoister> { - Hoister::with_delegate(Unpacker { rcx: self, assume_invariants }).transparent() - } - - pub(crate) fn assume_invariants(&mut self, ty: &Ty, overflow_checking: bool) { - struct Visitor<'a, 'rcx> { - rcx: &'a mut RefineCtxt<'rcx>, - overflow_checking: bool, - } - impl TypeVisitor for Visitor<'_, '_> { - fn visit_bty(&mut self, bty: &BaseTy) -> ControlFlow { - match bty { - BaseTy::Adt(adt_def, substs) if adt_def.is_box() => substs.visit_with(self), - BaseTy::Ref(_, ty, _) => ty.visit_with(self), - BaseTy::Tuple(tys) => tys.visit_with(self), - _ => ControlFlow::Continue(()), - } - } - - fn visit_ty(&mut self, ty: &Ty) -> ControlFlow { - if let TyKind::Indexed(bty, idx) = ty.kind() - && !idx.has_escaping_bvars() - { - for invariant in bty.invariants(self.overflow_checking) { - let invariant = invariant.apply(idx); - self.rcx.assume_pred(&invariant); - } - } - ty.super_visit_with(self) - } - } - ty.visit_with(&mut Visitor { rcx: self, overflow_checking }); - } + /// Used for debugging. See [`TypeTrace`] + Trace(TypeTrace), } pub(crate) enum AssumeInvariants { @@ -373,22 +368,22 @@ impl AssumeInvariants { } } -pub struct Unpacker<'a, 'rcx> { - rcx: &'a mut RefineCtxt<'rcx>, +pub struct Unpacker<'a, 'b> { + cursor: &'a mut Cursor<'b>, assume_invariants: AssumeInvariants, } impl HoisterDelegate for Unpacker<'_, '_> { fn hoist_exists(&mut self, ty_ctor: &TyCtor) -> Ty { - let ty = ty_ctor.replace_bound_refts_with(|sort, _, _| self.rcx.define_vars(sort)); + let ty = ty_ctor.replace_bound_refts_with(|sort, _, _| self.cursor.define_vars(sort)); if let AssumeInvariants::Yes { check_overflow } = self.assume_invariants { - self.rcx.assume_invariants(&ty, check_overflow); + self.cursor.assume_invariants(&ty, check_overflow); } ty } fn hoist_constr(&mut self, pred: Expr) { - self.rcx.assume_pred(pred); + self.cursor.assume_pred(pred); } } @@ -709,7 +704,7 @@ mod pretty { } } - impl Pretty for RefineCtxt<'_> { + impl Pretty for Cursor<'_> { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { let mut elements = vec![]; for node in ParentsIter::new(NodePtr::clone(&self.ptr)) { @@ -759,7 +754,7 @@ mod pretty { impl_debug_with_default_cx!( RefineTree => "refine_tree", - RefineCtxt<'_> => "refine_ctxt", + Cursor<'_> => "cursor", Scope, ); } @@ -778,8 +773,8 @@ struct RcxBind { } impl RefineCtxtTrace { - pub fn new(genv: GlobalEnv, rcx: &RefineCtxt) -> Self { - let parents = ParentsIter::new(NodePtr::clone(&rcx.ptr)).collect_vec(); + pub fn new(genv: GlobalEnv, cursor: &Cursor) -> Self { + let parents = ParentsIter::new(NodePtr::clone(&cursor.ptr)).collect_vec(); let mut bindings = vec![]; let mut exprs = vec![]; let cx = &PrettyCx::default(genv); diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index c33c12ac0f..188a773e86 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -6,7 +6,7 @@ use flux_infer::{ infer::{ ConstrReason, GlobalEnvExt as _, InferCtxt, InferCtxtRoot, InferResult, SubtypeReason, }, - refine_tree::{RefineCtxtTrace, Snapshot}, + refine_tree::{Marker, RefineCtxtTrace}, }; use flux_middle::{ global_env::GlobalEnv, @@ -68,9 +68,9 @@ pub(crate) struct Checker<'ck, 'genv, 'tcx, M> { /// The type used for the `resume` argument if we are checking a generator. resume_ty: Option, output: Binder, - /// A snapshot of the refinement context at the end of the basic block after applying the effects - /// of the terminator. - snapshots: IndexVec>, + /// A marker to the node in the refinement tree at the end of the basic block after applying + /// the effects of the terminator. + markers: IndexVec>, visited: BitSet, queue: WorkQueue<'ck>, default_refiner: Refiner<'genv, 'tcx>, @@ -441,7 +441,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { resume_ty, visited: BitSet::new_empty(body.basic_blocks.len()), output: fn_sig.output().clone(), - snapshots: IndexVec::from_fn_n(|_| None, body.basic_blocks.len()), + markers: IndexVec::from_fn_n(|_| None, body.basic_blocks.len()), queue: WorkQueue::empty(body.basic_blocks.len(), &body.dominator_order_rank), default_refiner: Refiner::default_for_item(genv, def_id.to_def_id()).with_span(span)?, }; @@ -456,8 +456,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { M::clear(&mut ck, bb); } - let snapshot = ck.snapshot_at_dominator(bb); - let mut infcx = infcx.change_root(snapshot, visited); + let marker = ck.marker_at_dominator(bb); + let mut infcx = infcx.move_to(marker, visited); let mut env = M::enter_basic_block(&mut ck, &mut infcx, bb); env.unpack(&mut infcx); ck.check_basic_block(infcx, env, bb)?; @@ -514,7 +514,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { self.check_terminator(&mut infcx, &mut env, terminator, last_stmt_span)?; dbg::terminator!("end", terminator, infcx, env); - self.snapshots[bb] = Some(infcx.snapshot()); + self.markers[bb] = Some(infcx.marker()); let term_span = last_stmt_span.unwrap_or(span); self.check_successors(infcx, env, bb, term_span, successors) })?; @@ -1510,8 +1510,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { } #[track_caller] - fn snapshot_at_dominator(&self, bb: BasicBlock) -> &Snapshot { - snapshot_at_dominator(self.body, &self.snapshots, bb) + fn marker_at_dominator(&self, bb: BasicBlock) -> &Marker { + marker_at_dominator(self.body, &self.markers, bb) } fn dominators(&self) -> &'ck Dominators { @@ -1723,7 +1723,7 @@ impl Mode for ShapeMode { let modified = match bb_envs.entry(ck.def_id).or_default().entry(target) { Entry::Occupied(mut entry) => entry.get_mut().join(env), Entry::Vacant(entry) => { - let scope = snapshot_at_dominator(ck.body, &ck.snapshots, target) + let scope = marker_at_dominator(ck.body, &ck.markers, target) .scope() .unwrap_or_else(|| tracked_span_bug!()); entry.insert(env.into_infer(scope)); @@ -1771,7 +1771,7 @@ impl Mode for RefineMode { ) -> Result { let bb_env = &ck.inherited.mode.bb_envs[&ck.def_id][&target]; debug_assert_eq!( - &ck.snapshot_at_dominator(target) + &ck.marker_at_dominator(target) .scope() .unwrap_or_else(|| tracked_span_bug!()), bb_env.scope() @@ -1852,16 +1852,16 @@ impl ShapeResult { } } -fn snapshot_at_dominator<'a>( +fn marker_at_dominator<'a>( body: &Body, - snapshots: &'a IndexVec>, + markers: &'a IndexVec>, bb: BasicBlock, -) -> &'a Snapshot { +) -> &'a Marker { let dominator = body .dominators() .immediate_dominator(bb) .unwrap_or_else(|| tracked_span_bug!()); - snapshots[dominator] + markers[dominator] .as_ref() .unwrap_or_else(|| tracked_span_bug!()) }