Add images too

Author: amandasystems

src/img/region-graphviz.png

@@ -25,24 +25,23 @@ for the alternative lectures.
 ## Defining a Dataflow Analysis
 
 The interface for dataflow analyses is split into three traits. The first is
-[`AnalysisDomain`], which must be implemented by *all* analyses. In addition to
+[`AnalysisDomain`], which must be implemented by _all_ analyses. In addition to
 the type of the dataflow state, this trait defines the initial value of that
 state at entry to each block, as well as the direction of the analysis, either
 forward or backward. The domain of your dataflow analysis must be a [lattice][]
 (strictly speaking a join-semilattice) with a well-behaved `join` operator. See
 documentation for the [`lattice`] module, as well as the [`JoinSemiLattice`]
 trait, for more information.
 
-You must then provide *either* a direct implementation of the [`Analysis`] trait
-*or* an implementation of the proxy trait [`GenKillAnalysis`]. The latter is for
+You must then provide _either_ a direct implementation of the [`Analysis`] trait
+_or_ an implementation of the proxy trait [`GenKillAnalysis`]. The latter is for
 so-called ["gen-kill" problems], which have a simple class of transfer function
 that can be applied very efficiently. Analyses whose domain is not a `BitSet`
 of some index type, or whose transfer functions cannot be expressed through
 "gen" and "kill" operations, must implement `Analysis` directly, and will run
 slower as a result. All implementers of `GenKillAnalysis` also implement
 `Analysis` automatically via a default `impl`.
 
-
 ```text
  AnalysisDomain
        ^
@@ -77,7 +76,7 @@ and `kill` operations for mutation.
 
 ### "Before" Effects
 
-Observant readers of the documentation may notice that there are actually *two*
+Observant readers of the documentation may notice that there are actually _two_
 possible effects for each statement and terminator, the "before" effect and the
 unprefixed (or "primary") effect. The "before" effects are applied immediately
 before the unprefixed effect **regardless of the direction of the analysis**.
@@ -99,17 +98,18 @@ In order to reach equilibrium, your analysis must obey some laws. One of the
 laws it must obey is that the bottom value[^bottom-purpose] joined with some
 other value equals the second value. Or, as an equation:
 
-> *bottom* join *x* = *x*
+> _bottom_ join _x_ = _x_
 
 Another law is that your analysis must have a "top value" such that
 
-> *top* join *x* = *top*
+> _top_ join _x_ = _top_
 
 Having a top value ensures that your semilattice has a finite height, and the
 law state above ensures that once the dataflow state reaches top, it will no
 longer change (the fixpoint will be top).
 
-[^bottom-purpose]: The bottom value's primary purpose is as the initial dataflow
+[^bottom-purpose]:
+    The bottom value's primary purpose is as the initial dataflow
     state. Each basic block's entry state is initialized to bottom before the
     analysis starts.
 
@@ -151,7 +151,7 @@ Calling `iterate_to_fixpoint` on your `Engine` will return a `Results`, which
 contains the dataflow state at fixpoint upon entry of each block. Once you have
 a `Results`, you can inspect the dataflow state at fixpoint at any point in
 the CFG. If you only need the state at a few locations (e.g., each `Drop`
-terminator) use a [`ResultsCursor`]. If you need the state at *every* location,
+terminator) use a [`ResultsCursor`]. If you need the state at _every_ location,
 a [`ResultsVisitor`] will be more efficient.
 
 ```text
@@ -172,7 +172,6 @@ a [`ResultsVisitor`] will be more efficient.
 
 For example, the following code uses a [`ResultsVisitor`]...
 
-
 ```rust,ignore
 // Assuming `MyVisitor` implements `ResultsVisitor<FlowState = MyAnalysis::Domain>`...
 let mut my_visitor = MyVisitor::new();
@@ -212,25 +211,30 @@ either "all" or the name of the MIR body you are interested in.
 These `.dot` files will be saved in your `mir_dump` directory and will have the
 [`NAME`] of the analysis (e.g. `maybe_inits`) as part of their filename. Each
 visualization will display the full dataflow state at entry and exit of each
-block, as well as any changes that occur in each statement and terminator.  See
+block, as well as any changes that occur in each statement and terminator. See
 the example below:
 
 ![A graphviz diagram for a dataflow analysis](../img/dataflow-graphviz-example.png)
 
 ### Region Constraint Graphs and Their Strongly Connected Components
 
+![A graph showing a small number of regions with their outlives relations](../img/region-graphviz.png)
+
 With `-Z dump-mir-graphviz=yes`, you will also get Graphviz files for the outlives constraints
 of the MIR bodies you asked for, as well as the strongly connected components (SCCs) on them.
-They are available as 
+They are available as
 `mir_dump/rs-file-name.function-name.-------.nll.0.regioncx.all.dot` and
 `mir_dump/rs-file-name.function-name.-------.nll.0.regioncx.scc.dot` respectively. For both
 graphs, named region variables will be shown with their external name (such as `'static`)
 shown in parenthesis. For region inference variables in universes other than the root universe,
-they will be shown as `/U13` (for universe 13). In the region graph, edges are labelled with 
-the MIR locations where the relationship holds.
+they will be shown as `/U13` (for universe 13). In the region graph, edges are labelled with
+the MIR locations where the relationship holds, or `All` if it's everywhere.
+
+![A graph showing a small number of strongly connected components on the region-outlives-graph above](../img/scc-graphviz.png)
 
-**Note:** there are implicit edges from `'static` to every region, but those are not rendered
-in the region graph to avoid clutter. They *do* however show up in the SCC graph.
+**Note:** There are implicit edges from `'static` to every region, but those are not rendered
+in the region graph to avoid clutter. They _do_ however show up in the SCC graph. This is why there are outgoing edges from SCC(5) in the SCC graph above
+that do not seem to have corresponding edges in the region outlives graph above.
 
 ["gen-kill" problems]: https://en.wikipedia.org/wiki/Data-flow_analysis#Bit_vector_problems
 [*Static Program Analysis*]: https://cs.au.dk/~amoeller/spa/