Skip to content

Commit

Permalink
Auto merge of #45825 - nikomatsakis:nll-factor-region-inference, r=ar…
Browse files Browse the repository at this point in the history
…ielb1

integrate MIR type-checker with NLL inference

This branch refactors NLL type inference so that it uses the MIR type-checker to gather constraints. Along the way, it also refactors how region constraints are gathered in the normal inference context mildly. The new setup is like this:

- What used to be `region_inference` is split into two parts:
    - `region_constraints`, which just collects up sets of constraints
    - `lexical_region_resolve`, which does the iterative, lexical region resolution
- When `resolve_regions_and_report_errors` is invoked, the inference engine converts the constraints into final values.
- In the MIR type checker, however, we do not invoke this method, but instead periodically take the region constraints and package them up for the NLL solver to use later.
    - This allows us to track when and where those constraints were incurred.
    - We also remove the central fulfillment context from the MIR type checker, instead instantiating new fulfillment contexts at each point. This allows us to capture the set of obligations that occurred at a particular point, and also to ensure that if the same obligation arises at two points, we will enforce the region constraints at both locations.
- The MIR type checker is also enhanced to instantiate late-bound-regions with fresh variables and handle a few other corner cases that arose.
- I also extracted some of the 'outlives' logic from the regionck, which will be needed later (see future work) to handle the type-outlives relationships.

One concern I have with this branch: since the MIR type checker is used even without the `-Znll` switch, I'm not sure if it will impact performance. One simple fix here would be to only enable the MIR type-checker if debug-assertions are enabled, since it just serves to validate the MIR. Longer term I hope to address this by improving the interface to the trait solver to be more query-based (ongoing work).

There is plenty of future work left. Here are two things that leap to mind:

- **Type-region outlives.** Currently, the NLL solver will ICE if it is required to handle a constraint like `T: 'a`. Fixing this will require a small amount of refactoring to extract the implied bounds code. I plan to follow a file-up bug on this (hopefully with mentoring instructions).
- **Testing.** It's a good idea to enumerate some of the tricky scenarios that need testing, but I think it'd be nice to try and parallelize some of the actual test writing (and resulting bug fixing):
    - Same obligation occurring at two points.
    - Well-formedness and trait obligations of various kinds (which are not all processed by the current MIR type-checker).
    - More tests for how subtyping and region inferencing interact.
    - More suggestions welcome!

r? @arielb1
  • Loading branch information
bors committed Nov 16, 2017
2 parents 58d8761 + 8c109f5 commit d0f8e29
Show file tree
Hide file tree
Showing 69 changed files with 4,835 additions and 3,616 deletions.
438 changes: 213 additions & 225 deletions src/librustc/infer/README.md

Large diffs are not rendered by default.

3 changes: 2 additions & 1 deletion src/librustc/infer/equate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,8 @@ impl<'combine, 'infcx, 'gcx, 'tcx> TypeRelation<'infcx, 'gcx, 'tcx>
a,
b);
let origin = Subtype(self.fields.trace.clone());
self.fields.infcx.region_vars.make_eqregion(origin, a, b);
self.fields.infcx.borrow_region_constraints()
.make_eqregion(origin, a, b);
Ok(a)
}

Expand Down
4 changes: 2 additions & 2 deletions src/librustc/infer/error_reporting/different_lifetimes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@
use hir;
use infer::InferCtxt;
use ty::{self, Region};
use infer::region_inference::RegionResolutionError::*;
use infer::region_inference::RegionResolutionError;
use infer::lexical_region_resolve::RegionResolutionError::*;
use infer::lexical_region_resolve::RegionResolutionError;
use hir::map as hir_map;
use middle::resolve_lifetime as rl;
use hir::intravisit::{self, Visitor, NestedVisitorMap};
Expand Down
76 changes: 37 additions & 39 deletions src/librustc/infer/error_reporting/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -57,8 +57,8 @@

use infer;
use super::{InferCtxt, TypeTrace, SubregionOrigin, RegionVariableOrigin, ValuePairs};
use super::region_inference::{RegionResolutionError, ConcreteFailure, SubSupConflict,
GenericBoundFailure, GenericKind};
use super::region_constraints::GenericKind;
use super::lexical_region_resolve::RegionResolutionError;

use std::fmt;
use hir;
Expand Down Expand Up @@ -177,13 +177,7 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {

ty::ReEarlyBound(_) |
ty::ReFree(_) => {
let scope = match *region {
ty::ReEarlyBound(ref br) => {
self.parent_def_id(br.def_id).unwrap()
}
ty::ReFree(ref fr) => fr.scope,
_ => bug!()
};
let scope = region.free_region_binding_scope(self);
let prefix = match *region {
ty::ReEarlyBound(ref br) => {
format!("the lifetime {} as defined on", br.name)
Expand Down Expand Up @@ -293,33 +287,37 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
debug!("report_region_errors: error = {:?}", error);

if !self.try_report_named_anon_conflict(&error) &&
!self.try_report_anon_anon_conflict(&error) {

match error.clone() {
// These errors could indicate all manner of different
// problems with many different solutions. Rather
// than generate a "one size fits all" error, what we
// attempt to do is go through a number of specific
// scenarios and try to find the best way to present
// the error. If all of these fails, we fall back to a rather
// general bit of code that displays the error information
ConcreteFailure(origin, sub, sup) => {
self.report_concrete_failure(region_scope_tree, origin, sub, sup).emit();
}

GenericBoundFailure(kind, param_ty, sub) => {
self.report_generic_bound_failure(region_scope_tree, kind, param_ty, sub);
}

SubSupConflict(var_origin, sub_origin, sub_r, sup_origin, sup_r) => {
!self.try_report_anon_anon_conflict(&error)
{
match error.clone() {
// These errors could indicate all manner of different
// problems with many different solutions. Rather
// than generate a "one size fits all" error, what we
// attempt to do is go through a number of specific
// scenarios and try to find the best way to present
// the error. If all of these fails, we fall back to a rather
// general bit of code that displays the error information
RegionResolutionError::ConcreteFailure(origin, sub, sup) => {
self.report_concrete_failure(region_scope_tree, origin, sub, sup).emit();
}

RegionResolutionError::GenericBoundFailure(kind, param_ty, sub) => {
self.report_generic_bound_failure(region_scope_tree, kind, param_ty, sub);
}

RegionResolutionError::SubSupConflict(var_origin,
sub_origin,
sub_r,
sup_origin,
sup_r) => {
self.report_sub_sup_conflict(region_scope_tree,
var_origin,
sub_origin,
sub_r,
sup_origin,
sup_r);
}
}
}
}
}
}
}
Expand Down Expand Up @@ -351,9 +349,9 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
// the only thing in the list.

let is_bound_failure = |e: &RegionResolutionError<'tcx>| match *e {
ConcreteFailure(..) => false,
SubSupConflict(..) => false,
GenericBoundFailure(..) => true,
RegionResolutionError::GenericBoundFailure(..) => true,
RegionResolutionError::ConcreteFailure(..) |
RegionResolutionError::SubSupConflict(..) => false,
};


Expand All @@ -365,9 +363,9 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {

// sort the errors by span, for better error message stability.
errors.sort_by_key(|u| match *u {
ConcreteFailure(ref sro, _, _) => sro.span(),
GenericBoundFailure(ref sro, _, _) => sro.span(),
SubSupConflict(ref rvo, _, _, _, _) => rvo.span(),
RegionResolutionError::ConcreteFailure(ref sro, _, _) => sro.span(),
RegionResolutionError::GenericBoundFailure(ref sro, _, _) => sro.span(),
RegionResolutionError::SubSupConflict(ref rvo, _, _, _, _) => rvo.span(),
});
errors
}
Expand Down Expand Up @@ -880,14 +878,13 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
};

if let SubregionOrigin::CompareImplMethodObligation {
span, item_name, impl_item_def_id, trait_item_def_id, lint_id
span, item_name, impl_item_def_id, trait_item_def_id,
} = origin {
self.report_extra_impl_obligation(span,
item_name,
impl_item_def_id,
trait_item_def_id,
&format!("`{}: {}`", bound_kind, sub),
lint_id)
&format!("`{}: {}`", bound_kind, sub))
.emit();
return;
}
Expand Down Expand Up @@ -1026,6 +1023,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
let var_name = self.tcx.hir.name(var_node_id);
format!(" for capture of `{}` by closure", var_name)
}
infer::NLL(..) => bug!("NLL variable found in lexical phase"),
};

struct_span_err!(self.tcx.sess, var_origin.span(), E0495,
Expand Down
4 changes: 2 additions & 2 deletions src/librustc/infer/error_reporting/named_anon_conflict.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@
//! Error Reporting for Anonymous Region Lifetime Errors
//! where one region is named and the other is anonymous.
use infer::InferCtxt;
use infer::region_inference::RegionResolutionError::*;
use infer::region_inference::RegionResolutionError;
use infer::lexical_region_resolve::RegionResolutionError::*;
use infer::lexical_region_resolve::RegionResolutionError;
use ty;

impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
Expand Down
6 changes: 2 additions & 4 deletions src/librustc/infer/error_reporting/note.rs
Original file line number Diff line number Diff line change
Expand Up @@ -445,14 +445,12 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
infer::CompareImplMethodObligation { span,
item_name,
impl_item_def_id,
trait_item_def_id,
lint_id } => {
trait_item_def_id } => {
self.report_extra_impl_obligation(span,
item_name,
impl_item_def_id,
trait_item_def_id,
&format!("`{}: {}`", sup, sub),
lint_id)
&format!("`{}: {}`", sup, sub))
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions src/librustc/infer/fudge.rs
Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,8 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
self.type_variables.borrow_mut().types_created_since_snapshot(
&snapshot.type_snapshot);
let region_vars =
self.region_vars.vars_created_since_snapshot(
&snapshot.region_vars_snapshot);
self.borrow_region_constraints().vars_created_since_snapshot(
&snapshot.region_constraints_snapshot);

Ok((type_variables, region_vars, value))
}
Expand Down
2 changes: 1 addition & 1 deletion src/librustc/infer/glb.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ impl<'combine, 'infcx, 'gcx, 'tcx> TypeRelation<'infcx, 'gcx, 'tcx>
b);

let origin = Subtype(self.fields.trace.clone());
Ok(self.fields.infcx.region_vars.glb_regions(origin, a, b))
Ok(self.fields.infcx.borrow_region_constraints().glb_regions(self.tcx(), origin, a, b))
}

fn binders<T>(&mut self, a: &ty::Binder<T>, b: &ty::Binder<T>)
Expand Down
26 changes: 17 additions & 9 deletions src/librustc/infer/higher_ranked/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ use super::{CombinedSnapshot,
SubregionOrigin,
SkolemizationMap};
use super::combine::CombineFields;
use super::region_inference::{TaintDirections};
use super::region_constraints::{TaintDirections};

use ty::{self, TyCtxt, Binder, TypeFoldable};
use ty::error::TypeError;
Expand Down Expand Up @@ -176,9 +176,10 @@ impl<'a, 'gcx, 'tcx> CombineFields<'a, 'gcx, 'tcx> {
.filter(|&r| r != representative)
{
let origin = SubregionOrigin::Subtype(self.trace.clone());
self.infcx.region_vars.make_eqregion(origin,
*representative,
*region);
self.infcx.borrow_region_constraints()
.make_eqregion(origin,
*representative,
*region);
}
}

Expand Down Expand Up @@ -427,7 +428,7 @@ impl<'a, 'gcx, 'tcx> CombineFields<'a, 'gcx, 'tcx> {
fn fresh_bound_variable<'a, 'gcx, 'tcx>(infcx: &InferCtxt<'a, 'gcx, 'tcx>,
debruijn: ty::DebruijnIndex)
-> ty::Region<'tcx> {
infcx.region_vars.new_bound(debruijn)
infcx.borrow_region_constraints().new_bound(infcx.tcx, debruijn)
}
}
}
Expand Down Expand Up @@ -481,7 +482,11 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
r: ty::Region<'tcx>,
directions: TaintDirections)
-> FxHashSet<ty::Region<'tcx>> {
self.region_vars.tainted(&snapshot.region_vars_snapshot, r, directions)
self.borrow_region_constraints().tainted(
self.tcx,
&snapshot.region_constraints_snapshot,
r,
directions)
}

fn region_vars_confined_to_snapshot(&self,
Expand Down Expand Up @@ -539,7 +544,8 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
*/

let mut region_vars =
self.region_vars.vars_created_since_snapshot(&snapshot.region_vars_snapshot);
self.borrow_region_constraints().vars_created_since_snapshot(
&snapshot.region_constraints_snapshot);

let escaping_types =
self.type_variables.borrow_mut().types_escaping_snapshot(&snapshot.type_snapshot);
Expand Down Expand Up @@ -581,7 +587,8 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
where T : TypeFoldable<'tcx>
{
let (result, map) = self.tcx.replace_late_bound_regions(binder, |br| {
self.region_vars.push_skolemized(br, &snapshot.region_vars_snapshot)
self.borrow_region_constraints()
.push_skolemized(self.tcx, br, &snapshot.region_constraints_snapshot)
});

debug!("skolemize_bound_regions(binder={:?}, result={:?}, map={:?})",
Expand Down Expand Up @@ -766,7 +773,8 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
{
debug!("pop_skolemized({:?})", skol_map);
let skol_regions: FxHashSet<_> = skol_map.values().cloned().collect();
self.region_vars.pop_skolemized(&skol_regions, &snapshot.region_vars_snapshot);
self.borrow_region_constraints()
.pop_skolemized(self.tcx, &skol_regions, &snapshot.region_constraints_snapshot);
if !skol_map.is_empty() {
self.projection_cache.borrow_mut().rollback_skolemized(
&snapshot.projection_cache_snapshot);
Expand Down
Original file line number Diff line number Diff line change
@@ -1,10 +1,13 @@
Region inference
# Region inference

# Terminology
## Terminology

Note that we use the terms region and lifetime interchangeably.

# Introduction
## Introduction

See the [general inference README](../README.md) for an overview of
how lexical-region-solving fits into the bigger picture.

Region inference uses a somewhat more involved algorithm than type
inference. It is not the most efficient thing ever written though it
Expand All @@ -16,63 +19,6 @@ it's worth spending more time on a more involved analysis. Moreover,
regions are a simpler case than types: they don't have aggregate
structure, for example.

Unlike normal type inference, which is similar in spirit to H-M and thus
works progressively, the region type inference works by accumulating
constraints over the course of a function. Finally, at the end of
processing a function, we process and solve the constraints all at
once.

The constraints are always of one of three possible forms:

- `ConstrainVarSubVar(Ri, Rj)` states that region variable Ri must be
a subregion of Rj
- `ConstrainRegSubVar(R, Ri)` states that the concrete region R (which
must not be a variable) must be a subregion of the variable Ri
- `ConstrainVarSubReg(Ri, R)` states the variable Ri shoudl be less
than the concrete region R. This is kind of deprecated and ought to
be replaced with a verify (they essentially play the same role).

In addition to constraints, we also gather up a set of "verifys"
(what, you don't think Verify is a noun? Get used to it my
friend!). These represent relations that must hold but which don't
influence inference proper. These take the form of:

- `VerifyRegSubReg(Ri, Rj)` indicates that Ri <= Rj must hold,
where Rj is not an inference variable (and Ri may or may not contain
one). This doesn't influence inference because we will already have
inferred Ri to be as small as possible, so then we just test whether
that result was less than Rj or not.
- `VerifyGenericBound(R, Vb)` is a more complex expression which tests
that the region R must satisfy the bound `Vb`. The bounds themselves
may have structure like "must outlive one of the following regions"
or "must outlive ALL of the following regions. These bounds arise
from constraints like `T: 'a` -- if we know that `T: 'b` and `T: 'c`
(say, from where clauses), then we can conclude that `T: 'a` if `'b:
'a` *or* `'c: 'a`.

# Building up the constraints

Variables and constraints are created using the following methods:

- `new_region_var()` creates a new, unconstrained region variable;
- `make_subregion(Ri, Rj)` states that Ri is a subregion of Rj
- `lub_regions(Ri, Rj) -> Rk` returns a region Rk which is
the smallest region that is greater than both Ri and Rj
- `glb_regions(Ri, Rj) -> Rk` returns a region Rk which is
the greatest region that is smaller than both Ri and Rj

The actual region resolution algorithm is not entirely
obvious, though it is also not overly complex.

## Snapshotting

It is also permitted to try (and rollback) changes to the graph. This
is done by invoking `start_snapshot()`, which returns a value. Then
later you can call `rollback_to()` which undoes the work.
Alternatively, you can call `commit()` which ends all snapshots.
Snapshots can be recursive---so you can start a snapshot when another
is in progress, but only the root snapshot can "commit".

## The problem

Basically our input is a directed graph where nodes can be divided
Expand Down Expand Up @@ -109,9 +55,9 @@ step where we walk over the verify bounds and check that they are
satisfied. These bounds represent the "maximal" values that a region
variable can take on, basically.

# The Region Hierarchy
## The Region Hierarchy

## Without closures
### Without closures

Let's first consider the region hierarchy without thinking about
closures, because they add a lot of complications. The region
Expand Down Expand Up @@ -141,7 +87,7 @@ Within that, there are sublifetimes for the assignment pattern and
also the expression `x + y`. The expression itself has sublifetimes
for evaluating `x` and `y`.

## Function calls
#s## Function calls

Function calls are a bit tricky. I will describe how we handle them
*now* and then a bit about how we can improve them (Issue #6268).
Expand Down Expand Up @@ -259,7 +205,7 @@ there is a reference created whose lifetime does not enclose
the borrow expression, we must issue sufficient restrictions to ensure
that the pointee remains valid.

## Modeling closures
### Modeling closures

Integrating closures properly into the model is a bit of
work-in-progress. In an ideal world, we would model closures as
Expand Down Expand Up @@ -314,8 +260,3 @@ handling of closures, there are no known cases where this leads to a
type-checking accepting incorrect code (though it sometimes rejects
what might be considered correct code; see rust-lang/rust#22557), but
it still doesn't feel like the right approach.

### Skolemization

For a discussion on skolemization and higher-ranked subtyping, please
see the module `middle::infer::higher_ranked::doc`.
Loading

0 comments on commit d0f8e29

Please sign in to comment.