generalize search graph to enable fuzzing #127627

lcnr · 2024-07-11T21:20:26Z

I do not believe it to be feasible to correctly implement the search graph without fuzzing. This PR enables this by requiring a fuzzer to only implement three new traits:

Cx: implemented by all I: Interner
ProofTreeBuilder: implemented by struct ProofTreeBuilder<D> for all D: SolverDelegate
Delegate: implemented for a new struct SearchGraphDelegate<D> for all D: SolverDelegate

It also moves the evaluation cache implementation into rustc_type_ir, requiring Interner to provide methods to create and access arbitrary WithDepNode<T> and to provide mutable access to a given GlobalCache. It otherwise does not change the API surface for users of the shared library.

This change should not impact behavior in any way.

r? @compiler-errors

compiler/rustc_next_trait_solver/src/solve/search_graph.rs

compiler-errors

r=me after nits and comments

compiler/rustc_next_trait_solver/src/solve/inspect/build.rs

compiler/rustc_type_ir/src/search_graph/global_cache.rs

compiler/rustc_type_ir/src/search_graph/mod.rs

lcnr · 2024-07-12T10:04:34Z

@bors r=compiler-errors rollup

bors · 2024-07-12T10:04:36Z

📌 Commit 208d709 has been approved by compiler-errors

It is now in the queue for this repository.

compiler-errors · 2024-07-12T10:19:16Z

compiler/rustc_next_trait_solver/src/solve/search_graph.rs

 use crate::delegate::SolverDelegate;
-use crate::solve::inspect::{self, ProofTreeBuilder};
-use crate::solve::{
-    CacheData, CanonicalInput, Certainty, QueryResult, SolverMode, FIXPOINT_STEP_LIMIT,
-};
-
-#[derive(Copy, Clone, PartialEq, Eq, Debug)]
-pub struct SolverLimit(usize);
-
-rustc_index::newtype_index! {
-    #[orderable]
-    #[gate_rustc_only]
-    pub struct StackDepth {}
-}
-
-bitflags::bitflags! {
-    /// Whether and how this goal has been used as the root of a
-    /// cycle. We track the kind of cycle as we're otherwise forced
-    /// to always rerun at least once.
-    #[derive(Debug, Clone, Copy, PartialEq, Eq)]
-    struct HasBeenUsed: u8 {
-        const INDUCTIVE_CYCLE = 1 << 0;
-        const COINDUCTIVE_CYCLE = 1 << 1;
-    }
-}
-
-#[derive(derivative::Derivative)]
-#[derivative(Debug(bound = ""))]
-struct StackEntry<I: Interner> {
-    input: CanonicalInput<I>,
-
-    available_depth: SolverLimit,
-
-    /// The maximum depth reached by this stack entry, only up-to date
-    /// for the top of the stack and lazily updated for the rest.
-    reached_depth: StackDepth,
-
-    /// Whether this entry is a non-root cycle participant.
-    ///
-    /// We must not move the result of non-root cycle participants to the
-    /// global cache. We store the highest stack depth of a head of a cycle
-    /// this goal is involved in. This necessary to soundly cache its
-    /// provisional result.
-    non_root_cycle_participant: Option<StackDepth>,
-
-    encountered_overflow: bool,
-
-    has_been_used: HasBeenUsed,
-
-    /// We put only the root goal of a coinductive cycle into the global cache.
-    ///
-    /// If we were to use that result when later trying to prove another cycle
-    /// participant, we can end up with unstable query results.
-    ///
-    /// See tests/ui/next-solver/coinduction/incompleteness-unstable-result.rs for
-    /// an example of where this is needed.
-    ///
-    /// There can  be multiple roots on the same stack, so we need to track
-    /// cycle participants per root:
-    /// ```plain
-    /// A :- B
-    /// B :- A, C
-    /// C :- D
-    /// D :- C
-    /// ```
-    nested_goals: HashSet<CanonicalInput<I>>,
-    /// Starts out as `None` and gets set when rerunning this
-    /// goal in case we encounter a cycle.
-    provisional_result: Option<QueryResult<I>>,
-}
-
-/// The provisional result for a goal which is not on the stack.
-#[derive(Debug)]
-struct DetachedEntry<I: Interner> {
-    /// The head of the smallest non-trivial cycle involving this entry.
-    ///
-    /// Given the following rules, when proving `A` the head for
-    /// the provisional entry of `C` would be `B`.
-    /// ```plain
-    /// A :- B
-    /// B :- C
-    /// C :- A + B + C
-    /// ```
-    head: StackDepth,
-    result: QueryResult<I>,
-}
+use rustc_type_ir::inherent::Predicate;
+use rustc_type_ir::search_graph::{self, CycleKind, UsageKind};
+use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult};
+use rustc_type_ir::Interner;
+use std::marker::PhantomData;


Imports are still not cleaned up :(

compiler-errors · 2024-07-12T10:20:30Z

compiler/rustc_next_trait_solver/src/solve/search_graph.rs

-    head: StackDepth,
-    result: QueryResult<I>,
-}
+use rustc_type_ir::inherent::Predicate;


We should always just glob-import inherent::* as a convention.

fully move it into `rustc_type_ir` and make it independent of `Interner`.

compiler-errors · 2024-07-12T10:34:47Z

I've fixed the imports.

Ideally we'd enforce via lint at least that inherent::* is preferred over manually importing traits from that module, since almost certainly never want to import specific trait names from there, but that seems like a lot of effort. Seems easy to mess up with rust-analyzer's auto-imports unfortunately :(

Would prefer if we try to keep these imports clean in general 🤔 I've tried very hard to clean them up in the process of uplifting and I think it does a lot to help the code maintainability.

@bors r+

bors · 2024-07-12T10:34:49Z

📌 Commit 15f770b has been approved by compiler-errors

It is now in the queue for this repository.

…r-errors generalize search graph to enable fuzzing I do not believe it to be feasible to correctly implement the search graph without fuzzing. This PR enables this by requiring a fuzzer to only implement three new traits: - `Cx`: implemented by all `I: Interner` - `ProofTreeBuilder`: implemented by `struct ProofTreeBuilder<D>` for all `D: SolverDelegate` - `Delegate`: implemented for a new `struct SearchGraphDelegate<D>` for all `D: SolverDelegate` It also moves the evaluation cache implementation into `rustc_type_ir`, requiring `Interner` to provide methods to create and access arbitrary `WithDepNode<T>` and to provide mutable access to a given `GlobalCache`. It otherwise does not change the API surface for users of the shared library. This change should not impact behavior in any way. r? `@compiler-errors`

…iaskrgr Rollup of 9 pull requests Successful merges: - rust-lang#124980 (Generalize `fn allocator` for Rc/Arc.) - rust-lang#126639 (Add AMX target-features and `x86_amx_intrinsics` feature flag) - rust-lang#126827 (Use pidfd_spawn for faster process spawning when a PidFd is requested) - rust-lang#127153 (Initial implementation of anonymous_pipe API) - rust-lang#127433 (Stabilize const_cstr_from_ptr (CStr::from_ptr, CStr::count_bytes)) - rust-lang#127552 (remove unnecessary `git` usages) - rust-lang#127613 (Update dist-riscv64-linux to binutils 2.40) - rust-lang#127627 (generalize search graph to enable fuzzing) - rust-lang#127648 (Lower timeout of CI jobs to 4 hours) r? `@ghost` `@rustbot` modify labels: rollup

…iaskrgr Rollup of 8 pull requests Successful merges: - rust-lang#124980 (Generalize `fn allocator` for Rc/Arc.) - rust-lang#126639 (Add AMX target-features and `x86_amx_intrinsics` feature flag) - rust-lang#126827 (Use pidfd_spawn for faster process spawning when a PidFd is requested) - rust-lang#127433 (Stabilize const_cstr_from_ptr (CStr::from_ptr, CStr::count_bytes)) - rust-lang#127552 (remove unnecessary `git` usages) - rust-lang#127613 (Update dist-riscv64-linux to binutils 2.40) - rust-lang#127627 (generalize search graph to enable fuzzing) - rust-lang#127648 (Lower timeout of CI jobs to 4 hours) r? `@ghost` `@rustbot` modify labels: rollup

Rollup merge of rust-lang#127627 - lcnr:rustc_search_graph, r=compiler-errors generalize search graph to enable fuzzing I do not believe it to be feasible to correctly implement the search graph without fuzzing. This PR enables this by requiring a fuzzer to only implement three new traits: - `Cx`: implemented by all `I: Interner` - `ProofTreeBuilder`: implemented by `struct ProofTreeBuilder<D>` for all `D: SolverDelegate` - `Delegate`: implemented for a new `struct SearchGraphDelegate<D>` for all `D: SolverDelegate` It also moves the evaluation cache implementation into `rustc_type_ir`, requiring `Interner` to provide methods to create and access arbitrary `WithDepNode<T>` and to provide mutable access to a given `GlobalCache`. It otherwise does not change the API surface for users of the shared library. This change should not impact behavior in any way. r? ``@compiler-errors``

solve -> solve/mod

f56b207

rustbot assigned compiler-errors Jul 11, 2024

lcnr force-pushed the rustc_search_graph branch from 174c513 to b9cf0ab Compare July 11, 2024 21:24

compiler-errors reviewed Jul 11, 2024

View reviewed changes

compiler/rustc_next_trait_solver/src/solve/search_graph.rs Outdated Show resolved Hide resolved

lcnr force-pushed the rustc_search_graph branch from b9cf0ab to cc8ce8d Compare July 11, 2024 21:49

compiler-errors reviewed Jul 12, 2024

View reviewed changes

lcnr force-pushed the rustc_search_graph branch 2 times, most recently from 809acd2 to 208d709 Compare July 12, 2024 10:04

bors added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Jul 12, 2024

compiler-errors reviewed Jul 12, 2024

View reviewed changes

enable fuzzing of SearchGraph

15f770b

fully move it into `rustc_type_ir` and make it independent of `Interner`.

compiler-errors force-pushed the rustc_search_graph branch from 208d709 to 15f770b Compare July 12, 2024 10:32

matthiaskrgr mentioned this pull request Jul 12, 2024

Rollup of 9 pull requests #127650

Closed

matthiaskrgr mentioned this pull request Jul 12, 2024

Rollup of 8 pull requests #127653

Merged

bors merged commit 526da23 into rust-lang:master Jul 12, 2024
6 checks passed

rustbot added this to the 1.81.0 milestone Jul 12, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

generalize search graph to enable fuzzing #127627

generalize search graph to enable fuzzing #127627

lcnr commented Jul 11, 2024 •

edited

Loading

compiler-errors left a comment

lcnr commented Jul 12, 2024

bors commented Jul 12, 2024

compiler-errors Jul 12, 2024 •

edited

Loading

compiler-errors Jul 12, 2024

compiler-errors commented Jul 12, 2024 •

edited

Loading

bors commented Jul 12, 2024

generalize search graph to enable fuzzing #127627

generalize search graph to enable fuzzing #127627

Conversation

lcnr commented Jul 11, 2024 • edited Loading

compiler-errors left a comment

Choose a reason for hiding this comment

lcnr commented Jul 12, 2024

bors commented Jul 12, 2024

compiler-errors Jul 12, 2024 • edited Loading

Choose a reason for hiding this comment

compiler-errors Jul 12, 2024

Choose a reason for hiding this comment

compiler-errors commented Jul 12, 2024 • edited Loading

bors commented Jul 12, 2024

lcnr commented Jul 11, 2024 •

edited

Loading

compiler-errors Jul 12, 2024 •

edited

Loading

compiler-errors commented Jul 12, 2024 •

edited

Loading