-# Appendix B: Background topics
+# Background topics
This section covers a numbers of common compiler terms that arise in
this guide. We try to give the general definition while providing some
## What is a control-flow graph?
-A control-flow graph is a common term from compilers. If you've ever
+A control-flow graph (CFG) is a common term from compilers. If you've ever
used a flow-chart, then the concept of a control-flow graph will be
pretty familiar to you. It's a representation of your program that
-exposes the underlying control flow in a very clear way.
+clearly exposes the underlying control flow.
A control-flow graph is structured as a set of **basic blocks**
connected by edges. The key idea of a basic block is that it is a set
d = 1;
```
-This would compile into four basic blocks:
+This would compile into four basic blocks in MIR. In textual form, it looks like
+this:
```mir
BB0: {
a = 1;
- if some_variable { goto BB1 } else { goto BB2 }
+ if some_variable {
+ goto BB1;
+ } else {
+ goto BB2;
+ }
}
BB1: {
BB3: {
d = 1;
- ...;
+ ...
}
```
+In graphical form, it looks like this:
+
+```
+ BB0
+ +--------------------+
+ | a = 1; |
+ +--------------------+
+ / \
+ if some_variable else
+ / \
+ BB1 / \ BB2
+ +-----------+ +-----------+
+ | b = 1; | | c = 1; |
+ +-----------+ +-----------+
+ \ /
+ \ /
+ \ BB3 /
+ +----------+
+ | d = 1; |
+ | ... |
+ +----------+
+```
+
When using a control-flow graph, a loop simply appears as a cycle in
the graph, and the `break` keyword translates into a path out of that
cycle.
[*Static Program Analysis*](https://cs.au.dk/~amoeller/spa/) by Anders Møller
and Michael I. Schwartzbach is an incredible resource!
-*to be written*
+_Dataflow analysis_ is a type of static analysis that is common in many
+compilers. It describes a general technique, rather than a particular analysis.
+
+The basic idea is that we can walk over a [control-flow graph (CFG)](#cfg) and
+keep track of what some value could be. At the end of the walk, we might have
+shown that some claim is true or not necessarily true (e.g. "this variable must
+be initialized"). `rustc` tends to do dataflow analyses over the MIR, since MIR
+is already a CFG.
+
+For example, suppose we want to check that `x` is initialized before it is used
+in this snippet:
+
+```rust,ignore
+fn foo() {
+ let mut x;
+
+ if some_cond {
+ x = 1;
+ }
+
+ dbg!(x);
+}
+```
+
+A CFG for this code might look like this:
+
+```txt
+ +------+
+ | Init | (A)
+ +------+
+ | \
+ | if some_cond
+ else \ +-------+
+ | \| x = 1 | (B)
+ | +-------+
+ | /
+ +---------+
+ | dbg!(x) | (C)
+ +---------+
+```
+
+We can do the dataflow analysis as follows: we will start off with a flag `init`
+which indicates if we know `x` is initialized. As we walk the CFG, we will
+update the flag. At the end, we can check its value.
+
+So first, in block (A), the variable `x` is declared but not initialized, so
+`init = false`. In block (B), we initialize the value, so we know that `x` is
+initialized. So at the end of (B), `init = true`.
+
+Block (C) is where things get interesting. Notice that there are two incoming
+edges, one from (A) and one from (B), corresponding to whether `some_cond` is true or not.
+But we cannot know that! It could be the case the `some_cond` is always true,
+so that `x` is actually always initialized. It could also be the case that
+`some_cond` depends on something random (e.g. the time), so `x` may not be
+initialized. In general, we cannot know statically (due to [Rice's
+Theorem][rice]). So what should the value of `init` be in block (C)?
+
+[rice]: https://en.wikipedia.org/wiki/Rice%27s_theorem
+
+Generally, in dataflow analyses, if a block has multiple parents (like (C) in
+our example), its dataflow value will be some function of all its parents (and
+of course, what happens in (C)). Which function we use depends on the analysis
+we are doing.
+
+In this case, we want to be able to prove definitively that `x` must be
+initialized before use. This forces us to be conservative and assume that
+`some_cond` might be false sometimes. So our "merging function" is "and". That
+is, `init = true` in (C) if `init = true` in (A) _and_ in (B) (or if `x` is
+initialized in (C)). But this is not the case; in particular, `init = false` in
+(A), and `x` is not initialized in (C). Thus, `init = false` in (C); we can
+report an error that "`x` may not be initialized before use".
+
+There is definitely a lot more that can be said about dataflow analyses. There is an
+extensive body of research literature on the topic, including a lot of theory.
+We only discussed a forwards analysis, but backwards dataflow analysis is also
+useful. For example, rather than starting from block (A) and moving forwards,
+we might have started with the usage of `x` and moved backwards to try to find
+its initialization.
<a name="quantified"></a>
## What is "universally quantified"? What about "existentially quantified"?
-*to be written*
+In math, a predicate may be _universally quantified_ or _existentially
+quantified_:
+
+- _Universal_ quantification:
+ - the predicate holds if it is true for all possible inputs.
+ - Traditional notation: ∀x: P(x). Read as "for all x, P(x) holds".
+- _Existential_ quantification:
+ - the predicate holds if there is any input where it is true, i.e., there
+ only has to be a single input.
+ - Traditional notation: ∃x: P(x). Read as "there exists x such that P(x) holds".
+
+In Rust, they come up in type checking and trait solving. For example,
+
+```rust,ignore
+fn foo<T>()
+```
+This function claims that the function is well-typed for all types `T`: `∀ T: well_typed(foo)`.
+
+Another example:
+
+```rust,ignore
+fn foo<'a>(_: &'a usize)
+```
+This function claims that for any lifetime `'a` (determined by the
+caller), it is well-typed: `∀ 'a: well_typed(foo)`.
+
+Another example:
+
+```rust,ignore
+fn foo<F>()
+where for<'a> F: Fn(&'a u8)
+```
+This function claims that it is well-typed for all types `F` such that for all
+lifetimes `'a`, `F: Fn(&'a u8)`: `∀ F: ∀ 'a: (F: Fn(&'a u8)) => well_typed(foo)`.
+
+One more example:
+
+```rust,ignore
+fn foo(_: dyn Debug)
+```
+This function claims that there exists some type `T` that implements `Debug`
+such that the function is well-typed: `∃ T: (T: Debug) and well_typed(foo)`.
<a name="variance"></a>
-## What is co- and contra-variance?
+## What is a de Bruijn Index?
+
+[De Bruijn indices][wikideb] are a way of representing, using only integers,
+which variables are bound in which binders. They were originally invented for
+use in lambda calculus evaluation (see [this Wikipedia article][wikideb] for
+more). In `rustc`, we use de Bruijn indices to [represent generic types][sub].
+
+[wikideb]: https://en.wikipedia.org/wiki/De_Bruijn_index
+[sub]: ../generics.md
+
+Here is a basic example of how de Bruijn indices might be used for closures (we
+don't actually do this in `rustc` though!):
+
+```rust,ignore
+|x| {
+ f(x) // de Bruijn index of `x` is 1 because `x` is bound 1 level up
+
+ |y| {
+ g(x, y) // index of `x` is 2 because it is bound 2 levels up
+ // index of `y` is 1 because it is bound 1 level up
+ }
+}
+```
+
+## What are co- and contra-variance?
Check out the subtyping chapter from the
[Rust Nomicon](https://doc.rust-lang.org/nomicon/subtyping.html).
Let's describe the concepts of free vs bound in terms of program
variables, since that's the thing we're most familiar with.
-- Consider this expression, which creates a closure: `|a,
- b| a + b`. Here, the `a` and `b` in `a + b` refer to the arguments
- that the closure will be given when it is called. We say that the
- `a` and `b` there are **bound** to the closure, and that the closure
- signature `|a, b|` is a **binder** for the names `a` and `b`
- (because any references to `a` or `b` within refer to the variables
- that it introduces).
-- Consider this expression: `a + b`. In this expression, `a` and `b`
- refer to local variables that are defined *outside* of the
- expression. We say that those variables **appear free** in the
- expression (i.e., they are **free**, not **bound** (tied up)).
+- Consider this expression, which creates a closure: `|a, b| a + b`.
+ Here, the `a` and `b` in `a + b` refer to the arguments that the closure will
+ be given when it is called. We say that the `a` and `b` there are **bound** to
+ the closure, and that the closure signature `|a, b|` is a **binder** for the
+ names `a` and `b` (because any references to `a` or `b` within refer to the
+ variables that it introduces).
+- Consider this expression: `a + b`. In this expression, `a` and `b` refer to
+ local variables that are defined *outside* of the expression. We say that
+ those variables **appear free** in the expression (i.e., they are **free**,
+ not **bound** (tied up)).
So there you have it: a variable "appears free" in some
expression/statement/whatever if it refers to something defined
> recommendations, and to `tinaun` for posting a link to a [twitter thread from
> Graydon Hoare](https://twitter.com/graydon_pub/status/1039615569132118016)
> which had some more recommendations!
->
+>
> Other sources: https://gcc.gnu.org/wiki/ListOfCompilerBooks
>
> If you have other suggestions, please feel free to open an issue or PR.
- [Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/tapl/)
- [Programming Language Pragmatics](https://www.cs.rochester.edu/~scott/pragmatics/)
- [Practical Foundations for Programming Languages](https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf)
-- [Compilers: Principles, Techniques, and Tools, 2nd Edition](https://www.amazon.com/dp/9332518661/ref=cm_sw_r_other_apa_1tUSBb5VHAVA1)
+- [Compilers: Principles, Techniques, and Tools, 2nd Edition](https://www.pearson.com/us/higher-education/program/Aho-Compilers-Principles-Techniques-and-Tools-2nd-Edition/PGM167067.html)
- [Garbage Collection: Algorithms for Automatic Dynamic Memory Management](https://www.cs.kent.ac.uk/people/staff/rej/gcbook/)
-- [Linkers and Loaders](https://linker.iecc.com/)
+- [Linkers and Loaders](https://www.amazon.com/Linkers-Kaufmann-Software-Engineering-Programming/dp/1558604960) (There are also free versions of this, but the version we had linked seems to be offline at the moment.)
- [Advanced Compiler Design and Implementation](https://www.goodreads.com/book/show/887908.Advanced_Compiler_Design_and_Implementation)
- [Building an Optimizing Compiler](https://www.goodreads.com/book/show/2063103.Building_an_Optimizing_Compiler)
- [Crafting Interpreters](http://www.craftinginterpreters.com/)
## Misc Papers and Blog Posts
- [Programming in Martin-Löf's Type Theory](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.118.6683&rep=rep1&type=pdf)
-- [Polymorphism, Subtyping, and Type Inference in MLsub](https://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf)
+- [Polymorphism, Subtyping, and Type Inference in MLsub](https://dl.acm.org/doi/10.1145/3093333.3009882)
projects / rustc.git / blobdiff