diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs index 378fa14138..ac086c5d08 100644 --- a/crates/flux-infer/src/infer.rs +++ b/crates/flux-infer/src/infer.rs @@ -239,21 +239,18 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> { t } - // [NOTE:INFCX-SCOPE] (see https://github.com/flux-rs/flux/pull/900#discussion_r1853052650) - // The InferCtxt is a cursor into a tree. Some functions like define_var, assume_pred and - // by extension unpack advance the cursor. For example, defining a variable pushes a node - // as a child of the current node and then moves the cursor into that new node. - // Other functions, like subtyping or check_pred (typically the ones defined in InferCtxtAt) - // do not advance the cursor (from the caller's perspective). For example, if you call - // subtyping a subtree is pushed under the current node, and the cursor is returned - // to where it was. That's the purpose of infcx.branch: to "clone" the cursor such - // that the original one doesn't get modified. - // `infcx.pop_scope()` and `infcx.replace_evars(...)` are supposed to be called when - // the `infcx`` is on the same node where the push_scope was called, because - // `replace_evars`` only replaces evars below that node. - // If `pop_scope` is called at a node further down (e.g. after calling unpack), - // the evars above that cursor will not be replaced. - + /// The `InferCtxt` is a cursor into a tree. Some functions like `define_var`, `assume_pred` and + /// by extension `unpack` advance the cursor. For example, defining a variable pushes a node + /// as a child of the current node and then moves the cursor into that new node. Other functions, + /// like `subtyping` or `check_pred` (typically the ones defined in `InferCtxtAt`) do not advance + /// the cursor (from the caller's perspective). For example, if you call subtyping a subtree is + /// pushed under the current node, and the cursor is returned to where it was. That's the purpose + /// of infcx.branch: to "clone" the cursor such that the original one doesn't get modified. + /// `infcx.pop_scope()` and `infcx.replace_evars(...)` are supposed to be called when the `infcx` + /// is on the same node where the `push_scope` was called, because `replace_evars` only replaces + /// evars below that node. If `pop_scope` is called at a node further down (e.g. after calling + /// `unpack`), the evars above that cursor will not be replaced. + /// (see ) pub fn push_scope(&mut self) { let scope = self.scope(); self.inner.borrow_mut().evars.enter_context(scope); @@ -459,6 +456,7 @@ pub trait LocEnv { ) -> InferResult; fn unfold_strg_ref(&mut self, infcx: &mut InferCtxt, path: &Path, ty: &Ty) -> InferResult; + fn get(&self, path: &Path) -> Ty; } @@ -472,19 +470,6 @@ struct Sub { obligations: Vec>, } -/// [NOTE:unfold_strg_ref] We use this function to unfold a strong reference prior to a subtyping check. -/// Normally, when checking a function body, a `StrgRef` is automatically unfolded -/// i.e. `x:&strg T` is turned into turned into a `x:Ptr(l); l: T` where `l` is some -/// fresh location. However, we need the below to do a similar unfolding in `check_fn_subtyping` -/// where we just have the super-type signature that needs to be unfolded. -/// We also add the binding to the environment so that we can: -/// (1) UPDATE the location after the call, and -/// (2) CHECK the relevant `ensures` clauses of the super-sig. -/// Nico: More importantly, we are assuming functions always give back the "ownership" -/// of the location so even though we should technically "consume" the ownership and -/// remove the location from the environment, the type is always going to be overwritten. -/// (there's a check for this btw, if you write an &strg we require an ensures for that -/// location for the signature to be well-formed) impl Sub { fn new(reason: ConstrReason, span: Span) -> Self { Self { reason, span, obligations: vec![] } @@ -503,6 +488,7 @@ impl Sub { ) -> InferResult { let infcx = &mut infcx.branch(); // infcx.push_trace(TypeTrace::tys(a, b)); + match (a.kind(), b.kind()) { (_, TyKind::Exists(ctor_b)) => { infcx.enter_exists(ctor_b, |infcx, ty_b| self.fun_args(infcx, env, a, &ty_b)) @@ -512,12 +498,26 @@ impl Sub { self.fun_args(infcx, env, a, ty_b) } (TyKind::Ptr(PtrKind::Mut(_), path1), TyKind::StrgRef(_, path2, ty2)) => { + // We should technically remove `path1` from `env`, but we are assuming that functions + // always give back ownership of the location so `path1` is going to be overwritten + // after the call anyways. let ty1 = env.get(path1); infcx.unify_exprs(&path1.to_expr(), &path2.to_expr()); self.tys(infcx, &ty1, ty2) } (TyKind::StrgRef(_, path1, ty1), TyKind::StrgRef(_, path2, ty2)) => { - env.unfold_strg_ref(infcx, path1, ty1)?; // see [NOTE:unfold_strg_ref] + // We has to unfold strong references prior to a subtyping check. Normally, when + // checking a function body, a `StrgRef` is automatically unfolded i.e. `x:&strg T` + // is turned into a `x:ptr(l); l: T` where `l` is some fresh location. However, we + // need the below to do a similar unfolding in `check_fn_subtyping` where we just + // have the super-type signature that needs to be unfolded. We also add the binding + // to the environment so that we can: + // (1) UPDATE the location after the call, and + // (2) CHECK the relevant `ensures` clauses of the super-sig. + // Same as the `Ptr` case above we should remove the location from the environment + // after unfolding to consume it, but we are assuming functions always give back + // ownership. + env.unfold_strg_ref(infcx, path1, ty1)?; let ty1 = env.get(path1); infcx.unify_exprs(&path1.to_expr(), &path2.to_expr()); self.tys(infcx, &ty1, ty2) diff --git a/crates/flux-middle/src/rty/region_matching.rs b/crates/flux-middle/src/rty/region_matching.rs index 28d963fd57..223de20d63 100644 --- a/crates/flux-middle/src/rty/region_matching.rs +++ b/crates/flux-middle/src/rty/region_matching.rs @@ -22,8 +22,9 @@ pub fn rty_match_regions(a: &rty::Ty, b: &rty::Ty) -> rty::Ty { subst.apply(&a) } -/// Replace all regions with a [`ReVar`] assigning each a unique [`RegionVid`]. This is used -/// to have a unique identifier for each position such that we can infer a region substitution. +/// Replace all non-bound regions with a [`rty::ReVar`] assigning each a unique [`rty::RegionVid`]. +/// This is used to have a unique identifier for each position such that we can infer a region +/// substitution. fn replace_regions_with_unique_vars(ty: &rty::Ty) -> rty::Ty { struct Replacer { next_rvid: u32, diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index dd2176ee82..4f10394e92 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -285,7 +285,7 @@ fn check_fn_subtyping( infcx.check_pred(requires, reason); } - // 4. Plug in the EVAR solution / replace evars -- see [NOTE:INFCX-SCOPE] + // 4. Plug in the EVAR solution / replace evars -- see [`InferCtxt::push_scope`] let evars_sol = infcx.pop_scope().with_span(span)?; infcx.replace_evars(&evars_sol); let output = sub_sig @@ -384,13 +384,13 @@ fn find_trait_item( Ok(None) } -/// [NOTE:Unfold-Local-Pointers] temporarily (at a call-site) convert an &mut to an &strg -/// to allow for the call to be checked. This is done by unfolding the &mut into a local pointer -/// at the call-site and then folding the pointer back into the &mut upon return. -/// See [NOTE:Fold-Local-Pointers] +/// Temporarily (around a function call) convert an `&mut` to an `&strg` to allow for the call to be +/// checked. This is done by unfolding the `&mut` into a local pointer at the call-site and then +/// folding the pointer back into the `&mut` upon return. +/// See also [`fold_local_ptrs`]. /// /// ```text -/// unpack(T) = T' +/// unpack(T) = T' /// ---------------------------------------[local-unfold] /// Γ ; &mut T => Γ, l:[<: T] T' ; ptr(l) /// ``` @@ -421,12 +421,11 @@ fn unfold_local_ptrs( Ok(tys) } -/// [NOTE:Fold-Local-Pointers] Fold local pointers implements roughly a rule like this (for all the -/// local pointers) that converts the local pointers created via [NOTE:Unfold-Local-Pointers] back -/// into &mut. +/// Fold local pointers implements roughly a rule like the following (for all local pointers) +/// that converts the local pointers created via [`unfold_local_ptrs`] back into `&mut`. /// /// ```text -/// T1 <: T2 +/// T1 <: T2 /// --------------------- [local-fold] /// Γ, l:[<: T2] T1 => Γ /// ``` @@ -956,8 +955,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { Ok(Guard::Pred(pred)) } - /// Checks conditional branching as in a `match` statement. [`SwitchTargets`] (https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/struct.SwitchTargets.html) contains a list of branches - the exact bit value which is being compared and the block to jump to. Using the conditionals, each branch can be checked using the new control flow information. - /// See https://github.com/flux-rs/flux/pull/840#discussion_r1786543174 + /// Checks conditional branching as in a `match` statement. [`SwitchTargets`](https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/struct.SwitchTargets.html) contains a list of branches - the exact bit value which is being compared and the block to jump to. Using the conditionals, each branch can be checked using the new control flow information. + /// See fn check_if(discr_ty: &Ty, targets: &SwitchTargets) -> Vec<(BasicBlock, Guard)> { let mk = |bits| { match discr_ty.kind() { diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 337735c66f..9642762290 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -334,7 +334,7 @@ impl<'a> TypeEnv<'a> { Ok(loc) } - /// ``` + /// ```text /// ----------------------------------- /// Γ ; &strg <ℓ: t> => Γ,ℓ: t ; ptr(ℓ) /// ```