Update book

Author: ecstatic-morse

book/src/SUMMARY.md

@@ -7,8 +7,11 @@
 - [Rules](./rules.md)
   - [Atoms](./rules/atoms.md)
   - [Relations](./rules/relations.md)
+  - [Control Flow Graph](./rules/cfg.md)
+  - [Move Paths](./rules/paths.md)
   - [Initialization analysis](./rules/initialization.md)
   - [Liveness analysis](./rules/liveness.md)
-  - [Loan analysis](./rules/loans.md)
+  - [Loan analysis](./rules/naive.md)
+  - [Optimized Variant](./rules/opt.md)
 - [Testing Polonius](./testing.md)
 - [See also](./see_also.md)

book/src/rules/atoms.md

@@ -1,12 +1,5 @@
 # Atoms
 
-Polonius defines the following **atoms**. To Polonius, these are
-opaque identifiers that identify particular things within the input
-program (literally they are newtype'd integers). Their meaning and
-relationships come entirely from the input relations.
-
-## Example
-
 We'll use this snippet of Rust code to illustrate the various kinds of
 atoms that can exist.
 
@@ -17,13 +10,15 @@ let z = x.0;
 drop(y);
 ```
 
-## Variables
+#### `Var`
 
 A **variable** represents a user variable defined by the Rust source
 code. In our snippet, `x`, `y`, and `z` are variables. Other kinds of
 variables include parameters.
 
-## Path
+	.type Var <: unsigned
+
+#### `Path`
 
 A **path** indicates a path through memory to a memory location --
 these roughly correspond to **places** in MIR, although we only
@@ -49,7 +44,9 @@ atom P1 for the path `x` and another atom P2 for the path `x.0`.
 These atoms are related to one another through the `path_parent`
 relation.
 
-## Node
+	.type Path <: unsigned
+
+#### `Node`
 
 Nodes are, well, *nodes* in the control-flow graph. They are related
 to one another by the `cfg_edge` relation.
@@ -60,17 +57,30 @@ begun executing -- the other is called the "mid node" -- which
 represents the point where S "takes effect". Each start node has
 exactly one successor, the mid node.
 
-## Loans
+	.type Node <: unsigned
+
+#### `Block`
+
+	.type Block <: unsigned
+
+#### `Location`
+
+	.type Location = [ block: Block, stmt: unsigned, mid: symbol ]
+
+#### `Loan`
 
 A **loan** represents some borrow that occurs in the source.  Each
 loan has an associated path that was borrowed along with a mutability.
 So, in our example, there would be a single loan, for the `&x.1`
 expression.
 
-## Origins
+	.type Loan <: unsigned
+
+#### `Origin`
 
 An **origin** is what it typically called in Rust a **lifetime**. In
 Polonius, an **origin** refers to the set of loans from which a
 reference may have been created.
 
+	.type Origin <: unsigned
 

book/src/rules/cfg.md

@@ -0,0 +1,47 @@
+# Control-flow graph
+
+## Nodes
+
+#### `cfg_edge`
+
+Indicates that an edge exists between `source` and `target`
+
+	.decl cfg_edge(sourceNode: Node, targetNode: Node)
+	.input cfg_edge
+
+#### `cfg_node`
+
+Enumerates all nodes (note that this approach implies that a single node
+graph is essentially not a thing).
+
+	.decl cfg_node(p: Node)
+
+	cfg_node(p) :- cfg_edge(p, _).
+	cfg_node(p) :- cfg_edge(_, p).
+
+## Basic Blocks
+
+#### `bb_edge`
+
+	.decl bb_edge(src: Block, targ: Block)
+	.input bb_edge
+
+#### `node_is_loc`
+
+	.decl node_is_loc(node: Node, loc: Location)
+	.input node_is_loc
+
+#### `precedes_in_block`
+
+	.decl precedes_in_block(loc1: Location, loc2: Location) inline
+
+	precedes_in_block([bb, stmt1, mid1], [bb, stmt2, mid2]) :-
+	    stmt2 > stmt1; (stmt1 = stmt2, mid2 = "Mid", mid1 = "Start").
+
+#### `succeeds_in_block`
+
+	.decl succeeds_in_block(loc1: Location, loc2: Location) inline
+
+	succeeds_in_block([bb, stmt1, mid1], [bb, stmt2, mid2]) :-
+	    stmt2 > stmt1; (stmt1 = stmt2, mid1 = "Mid", mid2 = "Start").
+

book/src/rules/init.md

@@ -0,0 +1,82 @@
+# Initialization
+
+## Relations
+
+#### `path_maybe_initialized_on_exit`
+
+Here we compute the set of paths that *may* contain a value on exit from
+each given node in the CFG. This is used later as part of the liveness
+analysis. In particular, if a value has been moved, then its drop is a
+no-op.
+
+This is not used to compute move errors -- it would be too "optimistic",
+since it only computes if a value *may* be initialized. See the next section
+on computing *uninitialization*.
+
+	.decl path_maybe_initialized_on_exit(path: Path, node: Node) brie
+
+	path_maybe_initialized_on_exit(path, node) :-
+	    path_assigned_at(path, node).
+
+	path_maybe_initialized_on_exit(path, targetNode) :-
+	    path_maybe_initialized_on_exit(path, sourceNode),
+	    cfg_edge(sourceNode, targetNode),
+	    !path_moved_at(path, targetNode).
+
+#### `var_maybe_partly_initialized_on_exit`
+
+We also compute which **variables** may be initialized (or at least partly
+initialized). Drops for variables that are not even partly initialized are
+known to be a no-op.
+
+	.decl var_maybe_partly_initialized_on_exit(var: Var, node: Node)
+
+	var_maybe_partly_initialized_on_exit(var, node) :-
+	    path_maybe_initialized_on_exit(path, node),
+	    path_begins_with_var(path, var).
+
+#### `path_maybe_uninitialized_on_exit`
+
+Here we compute the set of paths that are maybe *uninitialized* on exit from
+a node. Naturally, it would be illegal to access a path that is maybe
+uninitialized.
+
+We compute "maybe uninitialized" because it is easier than computing "must
+be initialized" (though they are equivalent), since the latter requires
+intersection, which is not available in "core datalog". It may make sense --
+as an optimization -- to try and convert to intersection, although it is
+debatable which will result in more tuples overall.
+
+	.decl path_maybe_uninitialized_on_exit(path: Path, node: Node) brie
+
+	path_maybe_uninitialized_on_exit(path, node) :-
+	    path_moved_at(path, node).
+
+	path_maybe_uninitialized_on_exit(path, targetNode) :-
+	    path_maybe_uninitialized_on_exit(path, sourceNode),
+	    cfg_edge(sourceNode, targetNode),
+	    !path_assigned_at(path, targetNode).
+
+#### `path_maybe_accessed_later`
+
+	.decl path_maybe_accessed_later(path: Path, node: Node) brie
+
+	path_maybe_accessed_later(path, node) :-
+	    path_accessed_at(path, node).
+
+	path_maybe_accessed_later(path, src) :-
+	    path_maybe_accessed_later(path, dst),
+	    cfg_edge(src, dst).
+
+## Errors
+
+#### `move_errors`
+
+	.decl move_errors(path: Path, node: Node)
+	.output move_errors
+
+	move_errors(path, targetNode) :-
+	    path_maybe_uninitialized_on_exit(path, sourceNode),
+	    cfg_edge(sourceNode, targetNode),
+	    path_accessed_at(path, targetNode).
+

book/src/rules/liveness.md

@@ -1,3 +1,119 @@
 # Liveness analysis
 
-**These rules are not yet described.**
+The role of the liveness computation is to figure out, for each cfg node,
+which variables may be accessed at some point in the future. We also
+distinguish between variables that may be accessed in general and those that
+may only be dropped. This is because a "full access" may potentially
+dereference any reference found in the variable, whereas a drop is more
+limited in its effects.
+
+One interesting wrinkle around drops is that we also need to consider the
+initialization state of each variable. This is because `Drop` statements can
+be added for variables which are never initialized, or whose values have
+been moved. Such statements are considered no-ops in MIR.
+
+## Inputs
+
+#### `var_used_at`
+
+Variable is used at the given CFG node
+
+	.decl var_used_at(variable: Var, node: Node)
+	.input var_used_at
+
+#### `var_defined_at`
+
+Variable is defined (overwritten) at the given CFG node
+
+	.decl var_defined_at(variable: Var, node: Node)
+	.input var_defined_at
+
+#### `var_dropped_at`
+
+Variable is dropped at this cfg node
+
+	.decl var_dropped_at(variable: Var, node: Node)
+	.input var_dropped_at
+
+#### `use_of_var_derefs_origin`
+
+References with the given origin may be
+dereferenced when the variable is used.
+
+In rustc, we generate this whenever the
+type of the variable includes the given
+origin.
+
+	.decl use_of_var_derefs_origin(variable: Var, origin: Origin)
+	.input use_of_var_derefs_origin
+
+References with the given origin may be
+dereferenced when the variable is dropped
+
+#### `drop_of_var_derefs_origin`
+
+In rustc, we generate this by examining the type
+and taking into account various
+unstable attributes. It is always a subset
+of `use_of_var_derefs_origin`.
+
+	.decl drop_of_var_derefs_origin(variable: Var, origin: Origin)
+	.input drop_of_var_derefs_origin
+
+## Relations
+
+#### `var_live_on_entry`
+
+Variables that are live on entry.
+
+	.decl var_live_on_entry(var: Var, node: Node)
+
+	var_live_on_entry(var, node) :-
+	    var_used_at(var, node).
+
+	var_live_on_entry(var, sourceNode) :-
+	    var_live_on_entry(var, targetNode),
+	    cfg_edge(sourceNode, targetNode),
+	    !var_defined_at(var, sourceNode).
+
+#### `var_drop_live_on_entry`
+
+Variables that are "drop live" on entry.
+
+The initial rule is that, when a variable is dropped, that makes it
+drop-live -- unless we know that the variable is fully uninitialized, in
+which case the drop is a no-op.
+
+**Optimization:** In rustc, we compute drop-live only up to the point where
+something becomes "use-live". We could do the same here by adding some `!`
+checks against `var_live_on_entry`, though it would require stratification
+in the datalog (not a problem).
+
+	.decl var_drop_live_on_entry(var: Var, node: Node)
+
+	var_drop_live_on_entry(var, targetNode) :-
+	    var_dropped_at(var, targetNode),
+	    cfg_edge(sourceNode, targetNode),
+	    var_maybe_partly_initialized_on_exit(var, sourceNode).
+
+	var_drop_live_on_entry(var, sourceNode) :-
+	    var_drop_live_on_entry(var, targetNode),
+	    cfg_edge(sourceNode, targetNode),
+	    !var_defined_at(var, sourceNode),
+	    var_maybe_partly_initialized_on_exit(var, sourceNode).
+
+#### `origin_live_on_entry`
+
+An origin is live at the node N if some reference with that origin may be
+dereferenced in the future.
+
+	.decl origin_live_on_entry(origin: Origin, node: Node)
+
+	origin_live_on_entry(origin, node) :-
+	    var_live_on_entry(var, node),
+	    use_of_var_derefs_origin(var, origin).
+
+	origin_live_on_entry(origin, node) :-
+	    var_drop_live_on_entry(var, node),
+	    drop_of_var_derefs_origin(var, origin).
+