Struct rustc_type_ir::search_graph::SearchGraph

source ·
pub struct SearchGraph<D: Delegate<Cx = X>, X: Cx = X> {
    mode: SolverMode,
    stack: IndexVec<StackDepth, StackEntry<X>>,
    provisional_cache: HashMap<X::Input, Vec<ProvisionalCacheEntry<X>>>,
    _marker: PhantomData<D>,
}

Fields§

§mode: SolverMode§stack: IndexVec<StackDepth, StackEntry<X>>

The stack of goals currently being computed.

An element is deeper in the stack if its index is lower.

§provisional_cache: HashMap<X::Input, Vec<ProvisionalCacheEntry<X>>>

The provisional cache contains entries for already computed goals which still depend on goals higher-up in the stack. We don’t move them to the global cache and track them locally instead. A provisional cache entry is only valid until the result of one of its cycle heads changes.

§_marker: PhantomData<D>

Implementations§

source§

impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D>

source

pub fn new(mode: SolverMode) -> SearchGraph<D>

source

pub fn solver_mode(&self) -> SolverMode

source

fn update_parent_goal( cx: X, stack: &mut IndexVec<StackDepth, StackEntry<X>>, reached_depth: StackDepth, heads: &CycleHeads, encountered_overflow: bool, nested_goals: &NestedGoals<X>, )

Lazily update the stack entry for the parent goal. This behavior is shared between actually evaluating goals and using existing global cache entries to make sure they have the same impact on the remaining evaluation.

source

pub fn is_empty(&self) -> bool

source

pub fn debug_current_depth(&self) -> usize

The number of goals currently in the search graph. This should only be used for debugging purposes.

source

fn step_kind(cx: X, input: X::Input) -> PathKind

source

fn stack_path_kind( cx: X, stack: &IndexVec<StackDepth, StackEntry<X>>, head: StackDepth, ) -> PathKind

Whether the path from head to the current stack entry is inductive or coinductive.

source

pub fn with_new_goal( &mut self, cx: X, input: X::Input, inspect: &mut D::ProofTreeBuilder, evaluate_goal: impl FnMut(&mut Self, &mut D::ProofTreeBuilder) -> X::Result, ) -> X::Result

Probably the most involved method of the whole solver.

Given some goal which is proven via the prove_goal closure, this handles caching, overflow, and coinductive cycles.

source

fn handle_overflow( &mut self, cx: X, input: X::Input, inspect: &mut D::ProofTreeBuilder, ) -> X::Result

source

fn clear_dependent_provisional_results(&mut self)

When reevaluating a goal with a changed provisional result, all provisional cache entry which depend on this goal get invalidated.

source

fn rebase_provisional_cache_entries( &mut self, cx: X, stack_entry: &StackEntry<X>, mutate_result: impl FnMut(X::Input, X::Result) -> X::Result, )

A necessary optimization to handle complex solver cycles. A provisional cache entry relies on a set of cycle heads and the path towards these heads. When popping a cycle head from the stack after we’ve finished computing it, we can’t be sure that the provisional cache entry is still applicable. We need to keep the cache entries to prevent hangs.

What we therefore do is check whether the cycle kind of all cycles the goal of a provisional cache entry is involved in would stay the same when computing the goal without its cycle head on the stack. For more details, see the relevant rustc-dev-guide chapter.

This can be thought of rotating the sub-tree of this provisional result and changing its entry point while making sure that all paths through this sub-tree stay the same.

In case the popped cycle head failed to reach a fixpoint anything which depends on its provisional result is invalid. Actually discarding provisional cache entries in this case would cause hangs, so we instead change the result of dependant provisional cache entries to also be ambiguous. This causes some undesirable ambiguity for nested goals whose result doesn’t actually depend on this cycle head, but that’s acceptable to me.

source

fn lookup_provisional_cache( &mut self, cx: X, input: X::Input, ) -> Option<X::Result>

source

fn candidate_is_applicable( cx: X, stack: &IndexVec<StackDepth, StackEntry<X>>, provisional_cache: &HashMap<X::Input, Vec<ProvisionalCacheEntry<X>>>, nested_goals: &NestedGoals<X>, ) -> bool

Even if there is a global cache entry for a given goal, we need to make sure evaluating this entry would not have ended up depending on either a goal already on the stack or a provisional cache entry.

source

fn lookup_global_cache_untracked( &self, cx: X, input: X::Input, available_depth: AvailableDepth, ) -> Option<X::Result>

Used when fuzzing the global cache. Accesses the global cache without updating the state of the search graph.

source

fn lookup_global_cache( &mut self, cx: X, input: X::Input, available_depth: AvailableDepth, ) -> Option<X::Result>

Try to fetch a previously computed result from the global cache, making sure to only do so if it would match the result of reevaluating this goal.

source

fn check_cycle_on_stack(&mut self, cx: X, input: X::Input) -> Option<X::Result>

source

fn reached_fixpoint( &mut self, cx: X, stack_entry: &StackEntry<X>, usage_kind: UsageKind, result: X::Result, ) -> bool

Whether we’ve reached a fixpoint when evaluating a cycle head.

source

fn evaluate_goal_in_task( &mut self, cx: X, input: X::Input, inspect: &mut D::ProofTreeBuilder, evaluate_goal: impl FnMut(&mut Self, &mut D::ProofTreeBuilder) -> X::Result, ) -> (StackEntry<X>, X::Result)

When we encounter a coinductive cycle, we have to fetch the result of that cycle while we are still computing it. Because of this we continuously recompute the cycle until the result of the previous iteration is equal to the final result, at which point we are done.

source

fn insert_global_cache( &mut self, cx: X, input: X::Input, final_entry: StackEntry<X>, result: X::Result, dep_node: X::DepNodeIndex, )

When encountering a cycle, both inductive and coinductive, we only move the root into the global cache. We also store all other cycle participants involved.

We must not use the global cache entry of a root goal if a cycle participant is on the stack. This is necessary to prevent unstable results. See the comment of StackEntry::nested_goals for more details.

Auto Trait Implementations§

§

impl<D, X> Freeze for SearchGraph<D, X>

§

impl<D, X> RefUnwindSafe for SearchGraph<D, X>
where D: RefUnwindSafe, <X as Cx>::Input: RefUnwindSafe, <X as Cx>::Result: RefUnwindSafe,

§

impl<D, X> Send for SearchGraph<D, X>
where D: Send, <X as Cx>::Input: Send, <X as Cx>::Result: Send,

§

impl<D, X> Sync for SearchGraph<D, X>
where D: Sync, <X as Cx>::Input: Sync, <X as Cx>::Result: Sync,

§

impl<D, X> Unpin for SearchGraph<D, X>
where D: Unpin, <X as Cx>::Input: Unpin, <X as Cx>::Result: Unpin,

§

impl<D, X> UnwindSafe for SearchGraph<D, X>
where <X as Cx>::Input: UnwindSafe, D: UnwindSafe, <X as Cx>::Result: UnwindSafe,

Blanket Implementations§

source§

impl<T> Aligned for T

source§

const ALIGN: Alignment = _

Alignment of Self.
source§

impl<T> Any for T
where T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for T
where T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T, R> CollectAndApply<T, R> for T

source§

fn collect_and_apply<I, F>(iter: I, f: F) -> R
where I: Iterator<Item = T>, F: FnOnce(&[T]) -> R,

Equivalent to f(&iter.collect::<Vec<_>>()).

source§

type Output = R

source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T> Instrument for T

source§

fn instrument(self, span: Span) -> Instrumented<Self>

Instruments this type with the provided Span, returning an Instrumented wrapper. Read more
source§

fn in_current_span(self) -> Instrumented<Self>

Instruments this type with the current Span, returning an Instrumented wrapper. Read more
source§

impl<T, U> Into<U> for T
where U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T> IntoEither for T

source§

fn into_either(self, into_left: bool) -> Either<Self, Self>

Converts self into a Left variant of Either<Self, Self> if into_left is true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more
source§

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
where F: FnOnce(&Self) -> bool,

Converts self into a Left variant of Either<Self, Self> if into_left(&self) returns true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more
source§

impl<T> Same for T

source§

type Output = T

Should always be Self
source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

source§

type Error = Infallible

The type returned in the event of a conversion error.
source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
source§

impl<I, T, U> Upcast<I, U> for T
where U: UpcastFrom<I, T>,

source§

fn upcast(self, interner: I) -> U

source§

impl<I, T> UpcastFrom<I, T> for T

source§

fn upcast_from(from: T, _tcx: I) -> T

source§

impl<T> WithSubscriber for T

source§

fn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self>
where S: Into<Dispatch>,

Attaches the provided Subscriber to this type, returning a WithDispatch wrapper. Read more
source§

fn with_current_subscriber(self) -> WithDispatch<Self>

Attaches the current default Subscriber to this type, returning a WithDispatch wrapper. Read more
source§

impl<'a, T> Captures<'a> for T
where T: ?Sized,

Layout§

Note: Most layout information is completely unstable and may even differ between compilations. The only exception is types with certain repr(...) attributes. Please see the Rust Reference's “Type Layout” chapter for details on type layout guarantees.

Size: 64 bytes