@@ -2,8 +2,11 @@ use rustc_hir::def_id::DefId;
2
2
use rustc_infer:: infer:: at:: ToTrace ;
3
3
use rustc_infer:: infer:: canonical:: CanonicalVarValues ;
4
4
use rustc_infer:: infer:: type_variable:: { TypeVariableOrigin , TypeVariableOriginKind } ;
5
- use rustc_infer:: infer:: { DefineOpaqueTypes , InferCtxt , InferOk , LateBoundRegionConversionTime } ;
5
+ use rustc_infer:: infer:: {
6
+ DefineOpaqueTypes , InferCtxt , InferOk , LateBoundRegionConversionTime , TyCtxtInferExt ,
7
+ } ;
6
8
use rustc_infer:: traits:: query:: NoSolution ;
9
+ use rustc_infer:: traits:: solve:: { CanonicalGoal , Certainty , MaybeCause , QueryResult } ;
7
10
use rustc_infer:: traits:: ObligationCause ;
8
11
use rustc_middle:: infer:: unify_key:: { ConstVariableOrigin , ConstVariableOriginKind } ;
9
12
use rustc_middle:: ty:: {
@@ -13,6 +16,7 @@ use rustc_middle::ty::{
13
16
use rustc_span:: DUMMY_SP ;
14
17
use std:: ops:: ControlFlow ;
15
18
19
+ use super :: search_graph:: { self , OverflowHandler } ;
16
20
use super :: { search_graph:: SearchGraph , Goal } ;
17
21
18
22
pub struct EvalCtxt < ' a , ' tcx > {
@@ -57,6 +61,270 @@ impl NestedGoals<'_> {
57
61
}
58
62
}
59
63
64
+ pub trait InferCtxtEvalExt < ' tcx > {
65
+ /// Evaluates a goal from **outside** of the trait solver.
66
+ ///
67
+ /// Using this while inside of the solver is wrong as it uses a new
68
+ /// search graph which would break cycle detection.
69
+ fn evaluate_root_goal (
70
+ & self ,
71
+ goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ,
72
+ ) -> Result < ( bool , Certainty ) , NoSolution > ;
73
+ }
74
+
75
+ impl < ' tcx > InferCtxtEvalExt < ' tcx > for InferCtxt < ' tcx > {
76
+ #[ instrument( level = "debug" , skip( self ) ) ]
77
+ fn evaluate_root_goal (
78
+ & self ,
79
+ goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ,
80
+ ) -> Result < ( bool , Certainty ) , NoSolution > {
81
+ let mut search_graph = search_graph:: SearchGraph :: new ( self . tcx ) ;
82
+
83
+ let mut ecx = EvalCtxt {
84
+ search_graph : & mut search_graph,
85
+ infcx : self ,
86
+ // Only relevant when canonicalizing the response.
87
+ max_input_universe : ty:: UniverseIndex :: ROOT ,
88
+ var_values : CanonicalVarValues :: dummy ( ) ,
89
+ nested_goals : NestedGoals :: new ( ) ,
90
+ } ;
91
+ let result = ecx. evaluate_goal ( IsNormalizesToHack :: No , goal) ;
92
+
93
+ assert ! (
94
+ ecx. nested_goals. is_empty( ) ,
95
+ "root `EvalCtxt` should not have any goals added to it"
96
+ ) ;
97
+
98
+ assert ! ( search_graph. is_empty( ) ) ;
99
+ result
100
+ }
101
+ }
102
+
103
+ impl < ' a , ' tcx > EvalCtxt < ' a , ' tcx > {
104
+ /// The entry point of the solver.
105
+ ///
106
+ /// This function deals with (coinductive) cycles, overflow, and caching
107
+ /// and then calls [`EvalCtxt::compute_goal`] which contains the actual
108
+ /// logic of the solver.
109
+ ///
110
+ /// Instead of calling this function directly, use either [EvalCtxt::evaluate_goal]
111
+ /// if you're inside of the solver or [InferCtxtEvalExt::evaluate_root_goal] if you're
112
+ /// outside of it.
113
+ #[ instrument( level = "debug" , skip( tcx, search_graph) , ret) ]
114
+ fn evaluate_canonical_goal (
115
+ tcx : TyCtxt < ' tcx > ,
116
+ search_graph : & ' a mut search_graph:: SearchGraph < ' tcx > ,
117
+ canonical_goal : CanonicalGoal < ' tcx > ,
118
+ ) -> QueryResult < ' tcx > {
119
+ // Deal with overflow, caching, and coinduction.
120
+ //
121
+ // The actual solver logic happens in `ecx.compute_goal`.
122
+ search_graph. with_new_goal ( tcx, canonical_goal, |search_graph| {
123
+ let ( ref infcx, goal, var_values) =
124
+ tcx. infer_ctxt ( ) . build_with_canonical ( DUMMY_SP , & canonical_goal) ;
125
+ let mut ecx = EvalCtxt {
126
+ infcx,
127
+ var_values,
128
+ max_input_universe : canonical_goal. max_universe ,
129
+ search_graph,
130
+ nested_goals : NestedGoals :: new ( ) ,
131
+ } ;
132
+ ecx. compute_goal ( goal)
133
+ } )
134
+ }
135
+
136
+ /// Recursively evaluates `goal`, returning whether any inference vars have
137
+ /// been constrained and the certainty of the result.
138
+ fn evaluate_goal (
139
+ & mut self ,
140
+ is_normalizes_to_hack : IsNormalizesToHack ,
141
+ goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ,
142
+ ) -> Result < ( bool , Certainty ) , NoSolution > {
143
+ let ( orig_values, canonical_goal) = self . canonicalize_goal ( goal) ;
144
+ let canonical_response =
145
+ EvalCtxt :: evaluate_canonical_goal ( self . tcx ( ) , self . search_graph , canonical_goal) ?;
146
+
147
+ let has_changed = !canonical_response. value . var_values . is_identity ( ) ;
148
+ let certainty = self . instantiate_and_apply_query_response (
149
+ goal. param_env ,
150
+ orig_values,
151
+ canonical_response,
152
+ ) ?;
153
+
154
+ // Check that rerunning this query with its inference constraints applied
155
+ // doesn't result in new inference constraints and has the same result.
156
+ //
157
+ // If we have projection goals like `<T as Trait>::Assoc == u32` we recursively
158
+ // call `exists<U> <T as Trait>::Assoc == U` to enable better caching. This goal
159
+ // could constrain `U` to `u32` which would cause this check to result in a
160
+ // solver cycle.
161
+ if cfg ! ( debug_assertions)
162
+ && has_changed
163
+ && is_normalizes_to_hack == IsNormalizesToHack :: No
164
+ && !self . search_graph . in_cycle ( )
165
+ {
166
+ debug ! ( "rerunning goal to check result is stable" ) ;
167
+ let ( _orig_values, canonical_goal) = self . canonicalize_goal ( goal) ;
168
+ let canonical_response =
169
+ EvalCtxt :: evaluate_canonical_goal ( self . tcx ( ) , self . search_graph , canonical_goal) ?;
170
+ if !canonical_response. value . var_values . is_identity ( ) {
171
+ bug ! ( "unstable result: {goal:?} {canonical_goal:?} {canonical_response:?}" ) ;
172
+ }
173
+ assert_eq ! ( certainty, canonical_response. value. certainty) ;
174
+ }
175
+
176
+ Ok ( ( has_changed, certainty) )
177
+ }
178
+
179
+ fn compute_goal ( & mut self , goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ) -> QueryResult < ' tcx > {
180
+ let Goal { param_env, predicate } = goal;
181
+ let kind = predicate. kind ( ) ;
182
+ if let Some ( kind) = kind. no_bound_vars ( ) {
183
+ match kind {
184
+ ty:: PredicateKind :: Clause ( ty:: Clause :: Trait ( predicate) ) => {
185
+ self . compute_trait_goal ( Goal { param_env, predicate } )
186
+ }
187
+ ty:: PredicateKind :: Clause ( ty:: Clause :: Projection ( predicate) ) => {
188
+ self . compute_projection_goal ( Goal { param_env, predicate } )
189
+ }
190
+ ty:: PredicateKind :: Clause ( ty:: Clause :: TypeOutlives ( predicate) ) => {
191
+ self . compute_type_outlives_goal ( Goal { param_env, predicate } )
192
+ }
193
+ ty:: PredicateKind :: Clause ( ty:: Clause :: RegionOutlives ( predicate) ) => {
194
+ self . compute_region_outlives_goal ( Goal { param_env, predicate } )
195
+ }
196
+ ty:: PredicateKind :: Clause ( ty:: Clause :: ConstArgHasType ( ct, ty) ) => {
197
+ self . compute_const_arg_has_type_goal ( Goal { param_env, predicate : ( ct, ty) } )
198
+ }
199
+ ty:: PredicateKind :: Subtype ( predicate) => {
200
+ self . compute_subtype_goal ( Goal { param_env, predicate } )
201
+ }
202
+ ty:: PredicateKind :: Coerce ( predicate) => {
203
+ self . compute_coerce_goal ( Goal { param_env, predicate } )
204
+ }
205
+ ty:: PredicateKind :: ClosureKind ( def_id, substs, kind) => self
206
+ . compute_closure_kind_goal ( Goal {
207
+ param_env,
208
+ predicate : ( def_id, substs, kind) ,
209
+ } ) ,
210
+ ty:: PredicateKind :: ObjectSafe ( trait_def_id) => {
211
+ self . compute_object_safe_goal ( trait_def_id)
212
+ }
213
+ ty:: PredicateKind :: WellFormed ( arg) => {
214
+ self . compute_well_formed_goal ( Goal { param_env, predicate : arg } )
215
+ }
216
+ ty:: PredicateKind :: Ambiguous => {
217
+ self . evaluate_added_goals_and_make_canonical_response ( Certainty :: AMBIGUOUS )
218
+ }
219
+ // FIXME: implement these predicates :)
220
+ ty:: PredicateKind :: ConstEvaluatable ( _) | ty:: PredicateKind :: ConstEquate ( _, _) => {
221
+ self . evaluate_added_goals_and_make_canonical_response ( Certainty :: Yes )
222
+ }
223
+ ty:: PredicateKind :: TypeWellFormedFromEnv ( ..) => {
224
+ bug ! ( "TypeWellFormedFromEnv is only used for Chalk" )
225
+ }
226
+ ty:: PredicateKind :: AliasEq ( lhs, rhs) => {
227
+ self . compute_alias_eq_goal ( Goal { param_env, predicate : ( lhs, rhs) } )
228
+ }
229
+ }
230
+ } else {
231
+ let kind = self . infcx . instantiate_binder_with_placeholders ( kind) ;
232
+ let goal = goal. with ( self . tcx ( ) , ty:: Binder :: dummy ( kind) ) ;
233
+ self . add_goal ( goal) ;
234
+ self . evaluate_added_goals_and_make_canonical_response ( Certainty :: Yes )
235
+ }
236
+ }
237
+
238
+ // Recursively evaluates all the goals added to this `EvalCtxt` to completion, returning
239
+ // the certainty of all the goals.
240
+ #[ instrument( level = "debug" , skip( self ) ) ]
241
+ pub ( super ) fn try_evaluate_added_goals ( & mut self ) -> Result < Certainty , NoSolution > {
242
+ let mut goals = core:: mem:: replace ( & mut self . nested_goals , NestedGoals :: new ( ) ) ;
243
+ let mut new_goals = NestedGoals :: new ( ) ;
244
+
245
+ let response = self . repeat_while_none (
246
+ |_| Ok ( Certainty :: Maybe ( MaybeCause :: Overflow ) ) ,
247
+ |this| {
248
+ let mut has_changed = Err ( Certainty :: Yes ) ;
249
+
250
+ if let Some ( goal) = goals. normalizes_to_hack_goal . take ( ) {
251
+ let ( _, certainty) = match this. evaluate_goal (
252
+ IsNormalizesToHack :: Yes ,
253
+ goal. with ( this. tcx ( ) , ty:: Binder :: dummy ( goal. predicate ) ) ,
254
+ ) {
255
+ Ok ( r) => r,
256
+ Err ( NoSolution ) => return Some ( Err ( NoSolution ) ) ,
257
+ } ;
258
+
259
+ if goal. predicate . projection_ty
260
+ != this. resolve_vars_if_possible ( goal. predicate . projection_ty )
261
+ {
262
+ has_changed = Ok ( ( ) )
263
+ }
264
+
265
+ match certainty {
266
+ Certainty :: Yes => { }
267
+ Certainty :: Maybe ( _) => {
268
+ let goal = this. resolve_vars_if_possible ( goal) ;
269
+
270
+ // The rhs of this `normalizes-to` must always be an unconstrained infer var as it is
271
+ // the hack used by `normalizes-to` to ensure that every `normalizes-to` behaves the same
272
+ // regardless of the rhs.
273
+ //
274
+ // However it is important not to unconditionally replace the rhs with a new infer var
275
+ // as otherwise we may replace the original unconstrained infer var with a new infer var
276
+ // and never propagate any constraints on the new var back to the original var.
277
+ let term = this
278
+ . term_is_fully_unconstrained ( goal)
279
+ . then_some ( goal. predicate . term )
280
+ . unwrap_or_else ( || {
281
+ this. next_term_infer_of_kind ( goal. predicate . term )
282
+ } ) ;
283
+ let projection_pred = ty:: ProjectionPredicate {
284
+ term,
285
+ projection_ty : goal. predicate . projection_ty ,
286
+ } ;
287
+ new_goals. normalizes_to_hack_goal =
288
+ Some ( goal. with ( this. tcx ( ) , projection_pred) ) ;
289
+
290
+ has_changed = has_changed. map_err ( |c| c. unify_and ( certainty) ) ;
291
+ }
292
+ }
293
+ }
294
+
295
+ for nested_goal in goals. goals . drain ( ..) {
296
+ let ( changed, certainty) =
297
+ match this. evaluate_goal ( IsNormalizesToHack :: No , nested_goal) {
298
+ Ok ( result) => result,
299
+ Err ( NoSolution ) => return Some ( Err ( NoSolution ) ) ,
300
+ } ;
301
+
302
+ if changed {
303
+ has_changed = Ok ( ( ) ) ;
304
+ }
305
+
306
+ match certainty {
307
+ Certainty :: Yes => { }
308
+ Certainty :: Maybe ( _) => {
309
+ new_goals. goals . push ( nested_goal) ;
310
+ has_changed = has_changed. map_err ( |c| c. unify_and ( certainty) ) ;
311
+ }
312
+ }
313
+ }
314
+
315
+ core:: mem:: swap ( & mut new_goals, & mut goals) ;
316
+ match has_changed {
317
+ Ok ( ( ) ) => None ,
318
+ Err ( certainty) => Some ( Ok ( certainty) ) ,
319
+ }
320
+ } ,
321
+ ) ;
322
+
323
+ self . nested_goals = goals;
324
+ response
325
+ }
326
+ }
327
+
60
328
impl < ' tcx > EvalCtxt < ' _ , ' tcx > {
61
329
pub ( super ) fn probe < T > ( & mut self , f : impl FnOnce ( & mut EvalCtxt < ' _ , ' tcx > ) -> T ) -> T {
62
330
let mut ecx = EvalCtxt {
0 commit comments