Skip to content

Commit 6193c5c

Browse files
committed
translate Verifys into TypeTests and check them
1 parent cd564d2 commit 6193c5c

File tree

5 files changed

+389
-24
lines changed

5 files changed

+389
-24
lines changed

src/librustc_mir/borrow_check/nll/region_infer/dfs.rs

Lines changed: 34 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -11,11 +11,12 @@
1111
//! Module defining the `dfs` method on `RegionInferenceContext`, along with
1212
//! its associated helper traits.
1313
14+
use borrow_check::nll::universal_regions::UniversalRegions;
15+
use borrow_check::nll::region_infer::RegionInferenceContext;
16+
use borrow_check::nll::region_infer::values::{RegionElementIndex, RegionValues, RegionValueElements};
1417
use rustc::mir::{Location, Mir};
1518
use rustc::ty::RegionVid;
1619
use rustc_data_structures::fx::FxHashSet;
17-
use super::RegionInferenceContext;
18-
use super::values::{RegionElementIndex, RegionValues, RegionValueElements};
1920

2021
impl<'tcx> RegionInferenceContext<'tcx> {
2122
/// Function used to satisfy or test a `R1: R2 @ P`
@@ -165,17 +166,16 @@ impl<'v> DfsOp for CopyFromSourceToTarget<'v> {
165166
/// condition. Similarly, if we reach the end of the graph and find
166167
/// that R1 contains some universal region that R2 does not contain,
167168
/// we abort the walk early.
168-
#[allow(dead_code)] // TODO
169-
pub(super) struct TestTarget<'v> {
170-
source_region: RegionVid,
171-
target_region: RegionVid,
172-
elements: &'v RegionValueElements,
173-
inferred_values: &'v RegionValues,
174-
constraint_point: Location,
169+
pub(super) struct TestTargetOutlivesSource<'v, 'tcx: 'v> {
170+
pub source_region: RegionVid,
171+
pub target_region: RegionVid,
172+
pub elements: &'v RegionValueElements,
173+
pub universal_regions: &'v UniversalRegions<'tcx>,
174+
pub inferred_values: &'v RegionValues,
175+
pub constraint_point: Location,
175176
}
176177

177-
#[allow(dead_code)] // TODO
178-
impl<'v> DfsOp for TestTarget<'v> {
178+
impl<'v, 'tcx> DfsOp for TestTargetOutlivesSource<'v, 'tcx> {
179179
/// The element that was not found within R2.
180180
type Early = RegionElementIndex;
181181

@@ -204,12 +204,32 @@ impl<'v> DfsOp for TestTarget<'v> {
204204
fn add_universal_regions_outlived_by_source_to_target(
205205
&mut self,
206206
) -> Result<bool, RegionElementIndex> {
207-
for ur in self.inferred_values
207+
// For all `ur_in_source` in `source_region`.
208+
for ur_in_source in self.inferred_values
208209
.universal_regions_outlived_by(self.source_region)
209210
{
210-
if !self.inferred_values.contains(self.target_region, ur) {
211-
return Err(self.elements.index(ur));
211+
// Check that `target_region` outlives `ur_in_source`.
212+
213+
// If `ur_in_source` is a member of `target_region`, OK.
214+
//
215+
// (This is implied by the loop below, actually, just an
216+
// irresistible micro-opt. Mm. Premature optimization. So
217+
// tasty.)
218+
if self.inferred_values.contains(self.target_region, ur_in_source) {
219+
continue;
212220
}
221+
222+
// If there is some other element X such that `target_region: X` and
223+
// `X: ur_in_source`, OK.
224+
if self.inferred_values
225+
.universal_regions_outlived_by(self.target_region)
226+
.any(|ur_in_target| self.universal_regions.outlives(ur_in_target, ur_in_source))
227+
{
228+
continue;
229+
}
230+
231+
// Otherwise, not known to be true.
232+
return Err(self.elements.index(ur_in_source));
213233
}
214234

215235
Ok(false)

src/librustc_mir/borrow_check/nll/region_infer/mod.rs

Lines changed: 217 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ use rustc::infer::InferCtxt;
1414
use rustc::infer::NLLRegionVariableOrigin;
1515
use rustc::infer::RegionVariableOrigin;
1616
use rustc::infer::SubregionOrigin;
17-
use rustc::infer::region_constraints::VarOrigins;
17+
use rustc::infer::region_constraints::{GenericKind, VarOrigins};
1818
use rustc::mir::{ClosureOutlivesRequirement, ClosureRegionRequirements, Location, Mir};
1919
use rustc::ty::{self, RegionVid};
2020
use rustc_data_structures::indexed_vec::IndexVec;
@@ -24,7 +24,7 @@ use syntax_pos::Span;
2424

2525
mod annotation;
2626
mod dfs;
27-
use self::dfs::CopyFromSourceToTarget;
27+
use self::dfs::{CopyFromSourceToTarget, TestTargetOutlivesSource};
2828
mod dump_mir;
2929
mod graphviz;
3030
mod values;
@@ -53,6 +53,9 @@ pub struct RegionInferenceContext<'tcx> {
5353
/// The constraints we have accumulated and used during solving.
5454
constraints: Vec<Constraint>,
5555

56+
/// Type constraints that we check after solving.
57+
type_tests: Vec<TypeTest<'tcx>>,
58+
5659
/// Information about the universally quantified regions in scope
5760
/// on this function and their (known) relations to one another.
5861
universal_regions: UniversalRegions<'tcx>,
@@ -95,6 +98,90 @@ pub struct Constraint {
9598
span: Span,
9699
}
97100

101+
/// A "type test" corresponds to an outlives constraint between a type
102+
/// and a lifetime, like `T: 'x` or `<T as Foo>::Bar: 'x`. They are
103+
/// translated from the `Verify` region constraints in the ordinary
104+
/// inference context.
105+
///
106+
/// These sorts of constraints are handled differently than ordinary
107+
/// constraints, at least at present. During type checking, the
108+
/// `InferCtxt::process_registered_region_obligations` method will
109+
/// attempt to convert a type test like `T: 'x` into an ordinary
110+
/// outlives constraint when possible (for example, `&'a T: 'b` will
111+
/// be converted into `'a: 'b` and registered as a `Constraint`).
112+
///
113+
/// In some cases, however, there are outlives relationships that are
114+
/// not converted into a region constraint, but rather into one of
115+
/// these "type tests". The distinction is that a type test does not
116+
/// influence the inference result, but instead just examines the
117+
/// values that we ultimately inferred for each region variable and
118+
/// checks that they meet certain extra criteria. If not, an error
119+
/// can be issued.
120+
///
121+
/// One reason for this is that these type tests always boil down to a
122+
/// check like `'a: 'x` where `'a` is a universally quantified region
123+
/// -- and therefore not one whose value is really meant to be
124+
/// *inferred*, precisely. Another reason is that these type tests can
125+
/// involve *disjunction* -- that is, they can be satisfied in more
126+
/// than one way.
127+
///
128+
/// For more information about this translation, see
129+
/// `InferCtxt::process_registered_region_obligations` and
130+
/// `InferCtxt::type_must_outlive` in `rustc::infer::outlives`.
131+
#[derive(Clone, Debug)]
132+
pub struct TypeTest<'tcx> {
133+
/// The type `T` that must outlive the region.
134+
pub generic_kind: GenericKind<'tcx>,
135+
136+
/// The region `'x` that the type must outlive.
137+
pub lower_bound: RegionVid,
138+
139+
/// The point where the outlives relation must hold.
140+
pub point: Location,
141+
142+
/// Where did this constraint arise?
143+
pub span: Span,
144+
145+
/// A test which, if met by the region `'x`, proves that this type
146+
/// constraint is satisfied.
147+
pub test: RegionTest,
148+
}
149+
150+
/// A "test" that can be applied to some "subject region" `'x`. These are used to
151+
/// describe type constraints. Tests do not presently affect the
152+
/// region values that get inferred for each variable; they only
153+
/// examine the results *after* inference. This means they can
154+
/// conveniently include disjuction ("a or b must be true").
155+
#[derive(Clone, Debug)]
156+
pub enum RegionTest {
157+
/// The subject region `'x` must by outlived by *some* region in
158+
/// the given set of regions.
159+
///
160+
/// This test comes from e.g. a where clause like `T: 'a + 'b`,
161+
/// which implies that we know that `T: 'a` and that `T:
162+
/// 'b`. Therefore, if we are trying to prove that `T: 'x`, we can
163+
/// do so by showing that `'a: 'x` *or* `'b: 'x`.
164+
IsOutlivedByAnyRegionIn(Vec<RegionVid>),
165+
166+
/// The subject region `'x` must by outlived by *all* regions in
167+
/// the given set of regions.
168+
///
169+
/// This test comes from e.g. a projection type like `T = <u32 as
170+
/// Trait<'a, 'b>>::Foo`, which must outlive `'a` or `'b`, and
171+
/// maybe both. Therefore we can prove that `T: 'x` if we know
172+
/// that `'a: 'x` *and* `'b: 'x`.
173+
IsOutlivedByAllRegionsIn(Vec<RegionVid>),
174+
175+
/// Any of the given tests are true.
176+
///
177+
/// This arises from projections, for which there are multiple
178+
/// ways to prove an outlives relationship.
179+
Any(Vec<RegionTest>),
180+
181+
/// All of the given tests are true.
182+
All(Vec<RegionTest>),
183+
}
184+
98185
impl<'tcx> RegionInferenceContext<'tcx> {
99186
/// Creates a new region inference context with a total of
100187
/// `num_region_variables` valid inference variables; the first N
@@ -122,6 +209,7 @@ impl<'tcx> RegionInferenceContext<'tcx> {
122209
liveness_constraints: RegionValues::new(elements, num_region_variables),
123210
inferred_values: None,
124211
constraints: Vec::new(),
212+
type_tests: Vec::new(),
125213
universal_regions,
126214
};
127215

@@ -243,7 +331,14 @@ impl<'tcx> RegionInferenceContext<'tcx> {
243331
});
244332
}
245333

246-
/// Perform region inference.
334+
/// Add a "type test" that must be satisfied.
335+
pub(super) fn add_type_test(&mut self, type_test: TypeTest<'tcx>) {
336+
self.type_tests.push(type_test);
337+
}
338+
339+
/// Perform region inference and report errors if we see any
340+
/// unsatisfiable constraints. If this is a closure, returns the
341+
/// region requirements to propagate to our creator, if any.
247342
pub(super) fn solve(
248343
&mut self,
249344
infcx: &InferCtxt<'_, '_, 'tcx>,
@@ -254,6 +349,8 @@ impl<'tcx> RegionInferenceContext<'tcx> {
254349

255350
self.propagate_constraints(mir);
256351

352+
self.check_type_tests(infcx, mir);
353+
257354
let outlives_requirements = self.check_universal_regions(infcx, mir_def_id);
258355

259356
if outlives_requirements.is_empty() {
@@ -315,6 +412,123 @@ impl<'tcx> RegionInferenceContext<'tcx> {
315412
self.inferred_values = Some(inferred_values);
316413
}
317414

415+
/// Once regions have been propagated, this method is used to see
416+
/// whether any of the constraints were too strong. In particular,
417+
/// we want to check for a case where a universally quantified
418+
/// region exceeded its bounds. Consider:
419+
///
420+
/// fn foo<'a, 'b>(x: &'a u32) -> &'b u32 { x }
421+
///
422+
/// In this case, returning `x` requires `&'a u32 <: &'b u32`
423+
/// and hence we establish (transitively) a constraint that
424+
/// `'a: 'b`. The `propagate_constraints` code above will
425+
/// therefore add `end('a)` into the region for `'b` -- but we
426+
/// have no evidence that `'b` outlives `'a`, so we want to report
427+
/// an error.
428+
fn check_type_tests(
429+
&self,
430+
infcx: &InferCtxt<'_, '_, 'tcx>,
431+
mir: &Mir<'tcx>,
432+
) {
433+
for type_test in &self.type_tests {
434+
debug!("check_type_test: {:?}", type_test);
435+
436+
if !self.eval_region_test(
437+
mir,
438+
type_test.point,
439+
type_test.lower_bound,
440+
&type_test.test,
441+
) {
442+
// Oh the humanity. Obviously we will do better than this error eventually.
443+
infcx.tcx.sess.span_err(
444+
type_test.span,
445+
&format!("failed type test: {:?}", type_test),
446+
);
447+
}
448+
}
449+
}
450+
451+
/// Test if `test` is true when applied to `lower_bound` at
452+
/// `point`, and returns true or false.
453+
fn eval_region_test(
454+
&self,
455+
mir: &Mir<'tcx>,
456+
point: Location,
457+
lower_bound: RegionVid,
458+
test: &RegionTest,
459+
) -> bool {
460+
debug!(
461+
"eval_region_test(point={:?}, lower_bound={:?}, test={:?})",
462+
point,
463+
lower_bound,
464+
test
465+
);
466+
467+
match test {
468+
RegionTest::IsOutlivedByAllRegionsIn(regions) => regions
469+
.iter()
470+
.all(|&r| self.eval_outlives(mir, r, lower_bound, point)),
471+
472+
RegionTest::IsOutlivedByAnyRegionIn(regions) => regions
473+
.iter()
474+
.any(|&r| self.eval_outlives(mir, r, lower_bound, point)),
475+
476+
RegionTest::Any(tests) => tests
477+
.iter()
478+
.any(|test| self.eval_region_test(mir, point, lower_bound, test)),
479+
480+
RegionTest::All(tests) => tests
481+
.iter()
482+
.all(|test| self.eval_region_test(mir, point, lower_bound, test)),
483+
}
484+
}
485+
486+
// Evaluate whether `sup_region: sub_region @ point`.
487+
fn eval_outlives(
488+
&self,
489+
mir: &Mir<'tcx>,
490+
sup_region: RegionVid,
491+
sub_region: RegionVid,
492+
point: Location,
493+
) -> bool {
494+
debug!(
495+
"eval_outlives({:?}: {:?} @ {:?})",
496+
sup_region,
497+
sub_region,
498+
point
499+
);
500+
501+
// Roughly speaking, do a DFS of all region elements reachable
502+
// from `point` contained in `sub_region`. If any of those are
503+
// *not* present in `sup_region`, the DFS will abort early and
504+
// yield an `Err` result.
505+
match self.dfs(
506+
mir,
507+
TestTargetOutlivesSource {
508+
source_region: sub_region,
509+
target_region: sup_region,
510+
constraint_point: point,
511+
elements: &self.elements,
512+
universal_regions: &self.universal_regions,
513+
inferred_values: self.inferred_values.as_ref().unwrap(),
514+
},
515+
) {
516+
Ok(_) => {
517+
debug!("eval_outlives: true");
518+
true
519+
}
520+
521+
Err(elem) => {
522+
debug!(
523+
"eval_outlives: false because `{:?}` is not present in `{:?}`",
524+
self.elements.to_element(elem),
525+
sup_region
526+
);
527+
false
528+
}
529+
}
530+
}
531+
318532
/// Once regions have been propagated, this method is used to see
319533
/// whether any of the constraints were too strong. In particular,
320534
/// we want to check for a case where a universally quantified

0 commit comments

Comments
 (0)