Module search_graph

Module search_graph 

Source
Expand description

The search graph is responsible for caching and cycle detection in the trait solver. Making sure that caching doesnโ€™t result in soundness bugs or unstable query results is very challenging and makes this one of the most-involved self-contained components of the compiler.

We added fuzzing support to test its correctness. The fuzzers used to verify the current implementation can be found in https://github.com/lcnr/search_graph_fuzz.

This is just a quick overview of the general design, please check out the relevant rustc-dev-guide chapter for more details. Caching is split between a global cache and the per-cycle provisional_cache. The global cache has to be completely unobservable, while the per-cycle cache may impact behavior as long as the resulting behavior is still correct.

Modulesยง

global_cache ๐Ÿ”’
stack ๐Ÿ”’

Structsยง

AvailableDepth ๐Ÿ”’
CandidateHeadUsages
CycleHead ๐Ÿ”’
CycleHeads ๐Ÿ”’
All cycle heads a given goal depends on, ordered by their stack depth.
EvaluationResult ๐Ÿ”’
The final result of evaluating a goal.
GlobalCache
HeadUsages ๐Ÿ”’
The kinds of cycles a cycle head was involved in.
NestedGoals ๐Ÿ”’
The nested goals of each stack entry and the path from the stack entry to that nested goal.
PathsToNested
Tracks how nested goals have been accessed. This is necessary to disable global cache entries if computing them would otherwise result in a cycle or access a provisional cache entry.
ProvisionalCacheEntry ๐Ÿ”’
A provisional result of an already computed goals which depends on other goals still on the stack.
SearchGraph

Enumsยง

PathKind
In the initial iteration of a cycle, we do not yet have a provisional result. In the case we return an initial provisional result depending on the kind of cycle.
UpdateParentGoalCtxt ๐Ÿ”’
While SearchGraph::update_parent_goal can be mostly shared between ordinary nested goals/global cache hits and provisional cache hits, using the provisional cache should not add any nested goals.

Traitsยง

Cx
The search graph does not simply use Interner directly to enable its fuzzing without having to stub the rest of the interner. We donโ€™t make this a super trait of Interner as users of the shared type library shouldnโ€™t have to care about Input and Result as they are implementation details of the search graph.
Delegate