History

Aaron Hill 6728f21d85 Generate documentation for auto-trait impls A new section is added to both both struct and trait doc pages. On struct/enum pages, a new 'Auto Trait Implementations' section displays any synthetic implementations for auto traits. Currently, this is only done for Send and Sync. On trait pages, a new 'Auto Implementors' section displays all types which automatically implement the trait. Effectively, this is a list of all public types in the standard library. Synthesized impls for a particular auto trait ('synthetic impls') take into account generic bounds. For example, a type 'struct Foo<T>(T)' will have 'impl<T> Send for Foo<T> where T: Send' generated for it. Manual implementations of auto traits are also taken into account. If we have the following types: 'struct Foo<T>(T)' 'struct Wrapper<T>(Foo<T>)' 'unsafe impl<T> Send for Wrapper<T>' // pretend that Wrapper<T> makes this sound somehow Then Wrapper will have the following impl generated: 'impl<T> Send for Wrapper<T>' reflecting the fact that 'T: Send' need not hold for 'Wrapper<T>: Send' to hold Lifetimes, HRTBS, and projections (e.g. '<T as Iterator>::Item') are taken into account by synthetic impls However, if a type can never implement a particular auto trait (e.g. 'struct MyStruct<T>(*const T)'), then a negative impl will be generated (in this case, 'impl<T> !Send for MyStruct<T>') All of this means that a user should be able to copy-paste a synthetic impl into their code, without any observable changes in behavior (assuming the rest of the program remains unchanged).		2018-02-18 16:29:24 -05:00
..
mod.rs	Generate documentation for auto-trait impls	2018-02-18 16:29:24 -05:00
README.md	fix more typos found by codespell.	2018-02-17 17:38:49 +01:00
taint.rs

README.md

Region constraint collection

Terminology

Note that we use the terms region and lifetime interchangeably.

Introduction

As described in the inference README, and 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 should 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".

Skolemization

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