Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 21f7a72

Browse files
committedAug 12, 2024
implement a performant and fuzzed solver cache
1 parent f860873 commit 21f7a72

File tree

4 files changed

+573
-318
lines changed

4 files changed

+573
-318
lines changed
 

‎compiler/rustc_next_trait_solver/src/solve/search_graph.rs

+28-18
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ use std::convert::Infallible;
22
use std::marker::PhantomData;
33

44
use rustc_type_ir::inherent::*;
5-
use rustc_type_ir::search_graph::{self, CycleKind, UsageKind};
5+
use rustc_type_ir::search_graph::{self, CycleKind};
66
use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult};
77
use rustc_type_ir::Interner;
88

99
use super::inspect::ProofTreeBuilder;
10-
use super::FIXPOINT_STEP_LIMIT;
10+
use super::{has_no_inference_or_external_constraints, FIXPOINT_STEP_LIMIT};
1111
use crate::delegate::SolverDelegate;
1212

1313
/// This type is never constructed. We only use it to implement `search_graph::Delegate`
@@ -23,10 +23,11 @@ where
2323
{
2424
type Cx = D::Interner;
2525

26+
const ENABLE_PROVISIONAL_CACHE: bool = true;
2627
type ValidationScope = Infallible;
2728
fn enter_validation_scope(
2829
_cx: Self::Cx,
29-
_input: <Self::Cx as search_graph::Cx>::Input,
30+
_input: CanonicalInput<I>,
3031
) -> Option<Self::ValidationScope> {
3132
None
3233
}
@@ -38,6 +39,7 @@ where
3839
inspect.is_noop()
3940
}
4041

42+
const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize = 4;
4143
fn recursion_limit(cx: I) -> usize {
4244
cx.recursion_limit()
4345
}
@@ -53,24 +55,16 @@ where
5355
}
5456
}
5557

56-
fn reached_fixpoint(
57-
cx: I,
58-
kind: UsageKind,
58+
fn is_initial_provisional_result(
59+
cx: Self::Cx,
60+
kind: CycleKind,
5961
input: CanonicalInput<I>,
60-
provisional_result: Option<QueryResult<I>>,
6162
result: QueryResult<I>,
6263
) -> bool {
63-
if let Some(r) = provisional_result {
64-
r == result
65-
} else {
66-
match kind {
67-
UsageKind::Single(CycleKind::Coinductive) => {
68-
response_no_constraints(cx, input, Certainty::Yes) == result
69-
}
70-
UsageKind::Single(CycleKind::Inductive) => {
71-
response_no_constraints(cx, input, Certainty::overflow(false)) == result
72-
}
73-
UsageKind::Mixed => false,
64+
match kind {
65+
CycleKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes) == result,
66+
CycleKind::Inductive => {
67+
response_no_constraints(cx, input, Certainty::overflow(false)) == result
7468
}
7569
}
7670
}
@@ -88,6 +82,22 @@ where
8882
response_no_constraints(cx, input, Certainty::overflow(false))
8983
}
9084

85+
fn is_ambiguous_result(result: QueryResult<I>) -> bool {
86+
result.is_ok_and(|response| {
87+
has_no_inference_or_external_constraints(response)
88+
&& matches!(response.value.certainty, Certainty::Maybe(_))
89+
})
90+
}
91+
92+
fn propagate_ambiguity(
93+
cx: I,
94+
for_input: CanonicalInput<I>,
95+
from_result: QueryResult<I>,
96+
) -> QueryResult<I> {
97+
let certainty = from_result.unwrap().value.certainty;
98+
response_no_constraints(cx, for_input, certainty)
99+
}
100+
91101
fn step_is_coinductive(cx: I, input: CanonicalInput<I>) -> bool {
92102
input.value.goal.predicate.is_coinductive(cx)
93103
}
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,17 @@
11
use derive_where::derive_where;
2-
use rustc_index::IndexVec;
32

4-
use super::{AvailableDepth, Cx, StackDepth, StackEntry};
5-
use crate::data_structures::{HashMap, HashSet};
3+
use super::{AvailableDepth, Cx, NestedGoals};
4+
use crate::data_structures::HashMap;
65

76
struct Success<X: Cx> {
8-
result: X::Tracked<X::Result>,
97
additional_depth: usize,
8+
nested_goals: NestedGoals<X>,
9+
result: X::Tracked<X::Result>,
10+
}
11+
12+
struct WithOverflow<X: Cx> {
13+
nested_goals: NestedGoals<X>,
14+
result: X::Tracked<X::Result>,
1015
}
1116

1217
/// The cache entry for a given input.
@@ -17,23 +22,15 @@ struct Success<X: Cx> {
1722
#[derive_where(Default; X: Cx)]
1823
struct CacheEntry<X: Cx> {
1924
success: Option<Success<X>>,
20-
/// We have to be careful when caching roots of cycles.
21-
///
22-
/// See the doc comment of `StackEntry::cycle_participants` for more
23-
/// details.
24-
nested_goals: HashSet<X::Input>,
25-
with_overflow: HashMap<usize, X::Tracked<X::Result>>,
25+
with_overflow: HashMap<usize, WithOverflow<X>>,
2626
}
2727

2828
#[derive_where(Debug; X: Cx)]
2929
pub(super) struct CacheData<'a, X: Cx> {
3030
pub(super) result: X::Result,
3131
pub(super) additional_depth: usize,
3232
pub(super) encountered_overflow: bool,
33-
// FIXME: This is currently unused, but impacts the design
34-
// by requiring a closure for `Cx::with_global_cache`.
35-
#[allow(dead_code)]
36-
pub(super) nested_goals: &'a HashSet<X::Input>,
33+
pub(super) nested_goals: &'a NestedGoals<X>,
3734
}
3835
#[derive_where(Default; X: Cx)]
3936
pub struct GlobalCache<X: Cx> {
@@ -52,15 +49,17 @@ impl<X: Cx> GlobalCache<X> {
5249

5350
additional_depth: usize,
5451
encountered_overflow: bool,
55-
nested_goals: &HashSet<X::Input>,
52+
nested_goals: NestedGoals<X>,
5653
) {
5754
let result = cx.mk_tracked(result, dep_node);
5855
let entry = self.map.entry(input).or_default();
59-
entry.nested_goals.extend(nested_goals);
6056
if encountered_overflow {
61-
entry.with_overflow.insert(additional_depth, result);
57+
let with_overflow = WithOverflow { nested_goals, result };
58+
let prev = entry.with_overflow.insert(additional_depth, with_overflow);
59+
assert!(prev.is_none());
6260
} else {
63-
entry.success = Some(Success { result, additional_depth });
61+
let prev = entry.success.replace(Success { additional_depth, nested_goals, result });
62+
assert!(prev.is_none());
6463
}
6564
}
6665

@@ -72,30 +71,37 @@ impl<X: Cx> GlobalCache<X> {
7271
&'a self,
7372
cx: X,
7473
input: X::Input,
75-
stack: &IndexVec<StackDepth, StackEntry<X>>,
7674
available_depth: AvailableDepth,
75+
mut candidate_is_applicable: impl FnMut(&NestedGoals<X>) -> bool,
7776
) -> Option<CacheData<'a, X>> {
7877
let entry = self.map.get(&input)?;
79-
if stack.iter().any(|e| entry.nested_goals.contains(&e.input)) {
80-
return None;
78+
if let Some(Success { additional_depth, ref nested_goals, ref result }) = entry.success {
79+
if available_depth.cache_entry_is_applicable(additional_depth)
80+
&& candidate_is_applicable(nested_goals)
81+
{
82+
return Some(CacheData {
83+
result: cx.get_tracked(&result),
84+
additional_depth,
85+
encountered_overflow: false,
86+
nested_goals,
87+
});
88+
}
8189
}
8290

83-
if let Some(ref success) = entry.success {
84-
if available_depth.cache_entry_is_applicable(success.additional_depth) {
91+
let additional_depth = available_depth.0;
92+
if let Some(WithOverflow { nested_goals, result }) =
93+
entry.with_overflow.get(&additional_depth)
94+
{
95+
if candidate_is_applicable(nested_goals) {
8596
return Some(CacheData {
86-
result: cx.get_tracked(&success.result),
87-
additional_depth: success.additional_depth,
88-
encountered_overflow: false,
89-
nested_goals: &entry.nested_goals,
97+
result: cx.get_tracked(result),
98+
additional_depth,
99+
encountered_overflow: true,
100+
nested_goals,
90101
});
91102
}
92103
}
93104

94-
entry.with_overflow.get(&available_depth.0).map(|e| CacheData {
95-
result: cx.get_tracked(e),
96-
additional_depth: available_depth.0,
97-
encountered_overflow: true,
98-
nested_goals: &entry.nested_goals,
99-
})
105+
None
100106
}
101107
}
There was a problem loading the remainder of the diff.

0 commit comments

Comments
 (0)
Failed to load comments.