Polonius

https://rust-lang.github.io/polonius/
Admin
Polonius is a core library that models the borrow check, implementing the analysis described in its...
Tokens:10,070
Snippets:117
Trust Score:9.7
Update:3 months ago
Show doc for...
Tokens:
Raw
### Polonius Analysis Output Example

Source: https://rust-lang.github.io/polonius/getting_started.html

Example output from running a Polonius analysis, showing the directory processed, the time taken, and a separator line.

```text
Finished release [optimized] target(s) in 0.05 secs
     Running `target/release/borrow-check 'inputs/clap-rs/app-parser-{{impl}}-add_defaults/'`
--------------------------------------------------
Directory: inputs/clap-rs/app-parser-{{impl}}-add_defaults/
Time: 3.856s
```

--------------------------------

### Placeholder Origins Example

Source: https://rust-lang.github.io/polonius/rules/relations.html

Demonstrates how placeholder origins are generated for generic lifetime parameters in function signatures.

```Rust
#![allow(unused)]
fn main() {
fn my_function<'a, 'b>(x: &'a u32, y: &'b u32) {
    ...
}
}
```

--------------------------------

### Example of Placeholder Subset Declaration

Source: https://rust-lang.github.io/polonius/print.html

Illustrates user-supplied and implied subset relationships between placeholder origins in a Rust function signature.

```rust
#![allow(unused)]
fn main() {
fn foo<'a, 'b: 'a, 'c>(x: &'c &'a u32) {
    ...
}
}
```

--------------------------------

### Example of known_placeholder_subset relation

Source: https://rust-lang.github.io/polonius/rules/relations.html

Demonstrates a function signature with explicit and implied subset bounds that would result in `known_placeholder_subset` entries. Polonius infers transitive subsets.

```rust
#![allow(unused)]
fn main() {
fn foo<'a, 'b: 'a, 'c>(x: &'c &'a u32) {
    ...
}
}

```

--------------------------------

### Subset Base Example

Source: https://rust-lang.github.io/polonius/rules/relations.html

Shows the 'subset_base' relation, representing the 'outlives' or 'flows into' relationship between lifetimes.

```Rust
#![allow(unused)]
fn main() {
let a: u32 = 1;
let b: &u32 = &a;
//            ^ let's call this 'a
//     ^ and let's call this 'b
}
```

--------------------------------

### Loan Killed At Example

Source: https://rust-lang.github.io/polonius/rules/relations.html

Illustrates the 'loan_killed_at' relation where a loan is invalidated by an assignment to the borrowed path.

```Rust
#![allow(unused)]
fn main() {
let mut a = 1;
let mut b = 2;
let mut q = &mut a;
let r = &mut *q; // loan L0 of `*q`
// `q` can't be used here, one has to go through `r`
q = &mut b; // killed(L0)
// `q` and `r` can be used here
}
```

--------------------------------

### Loan Issuance Fact Example

Source: https://rust-lang.github.io/polonius/rules/relations.html

Demonstrates the `loan_issued_at` relation, which records that a loan was issued at a specific point in the code, creating a reference with a given origin. This fact links the loan to the origin of the borrow expression.

```rust
#![allow(unused)]
fn main() {
let mut a = 0;
let r = &mut a; // this creates the loan L0
//      ^ let's call this 'a
}
```

--------------------------------

### CFG Edge Representation in Polonius

Source: https://rust-lang.github.io/polonius/rules/relations.html

Illustrates how control flow graph edges are represented as input facts in Polonius. Each MIR statement location generates 'Start' and 'Mid' points, linked by cfg_edge facts.

```rust
#![allow(unused)]
fn main() {
bb0: {
  ...          // bb0[0]
  ...          // bb0[1]
  goto -> bb3; // bb0[2]
}

...

bb3: {
  ... // bb3[0]
}

}
```

```rust
cfg_edge = vec![
  // statement at location bb0[0]:
  (bb0-0-start, bb0-0-mid),
  (bb0-0-mid, bb0-1-start),
  
  // statement at location bb0[1]:
  (bb0-1-start, bb0-1-mid),
  (bb0-1-mid, bb0-2-start),
  
  // terminator at location bb0[2]:
  (bb0-2-start, bb0-2-mid),
  (bb0-2-mid, bb3-0-start),
];
```

--------------------------------

### Using Naive or Location-Insensitive Analysis

Source: https://rust-lang.github.io/polonius/print.html

Demonstrates how to select different analysis strategies like 'Naive' for readability or 'LocationInsensitive' for speed.

```bash
cargo +nightly run --release -- -a Naive
```

```bash
cargo +nightly run --release -- -a LocationInsensitive
```

--------------------------------

### Naive Datalog Rules for Subset Computation

Source: https://rust-lang.github.io/polonius/rules/loans.html

These Datalog rules compute the complete graph of subsets between origins. They establish initial subsets from `subset_base`, compute the transitive closure at a given point, and propagate these subsets along the CFG based on origin liveness.

```datalog
.decl subset(Origin1:origin, Origin2:origin, Point:point)

// R1: the initial subsets are the non-transitive `subset_base` static input
subset(Origin1, Origin2, Point) :-
  subset_base(Origin1, Origin2, Point).

// R2: compute the subset transitive closure, at a given point
subset(Origin1, Origin3, Point) :-
  subset(Origin1, Origin2, Point),
  subset(Origin2, Origin3, Point).

// R3: propagate subsets along the CFG, according to liveness
subset(Origin1, Origin2, TargetPoint) :-
  subset(Origin1, Origin2, SourcePoint),
  cfg_edge(SourcePoint, TargetPoint),
  (origin_live_on_entry(Origin1, TargetPoint); placeholder(Origin1, _)),
  (origin_live_on_entry(Origin2, TargetPoint); placeholder(Origin2, _)).

```

--------------------------------

### Run UI Tests with Polonius Comparison Mode

Source: https://rust-lang.github.io/polonius/testing.html

This command invokes the Rust test suite with Polonius' output compared against the current NLL (New Lexical Analysis) implementation. It is used for running UI tests.

```bash
./x.py test -i --stage 1 --compare-mode polonius src/test/ui
```

--------------------------------

### List Generated NLL Facts Directories

Source: https://rust-lang.github.io/polonius/print.html

After generating facts, a `nll-facts` directory is created containing subdirectories for each function.

```bash
ls -F nll-facts
{{impl}}-maybe_next/
main/
```

--------------------------------

### Run UI Tests with Polonius Compare Mode

Source: https://rust-lang.github.io/polonius/print.html

Invoke the Rust test suite in a mode that compares Polonius' output to the current NLL output. This command runs the UI tests with the specified compare mode.

```bash
$ ./x.py test -i --stage 1 --compare-mode polonius src/test/ui
```

--------------------------------

### Loan Liveness and Error Detection Rules

Source: https://rust-lang.github.io/polonius/rules/loans.html

Computes whether a loan is live at a given point and identifies illegal access errors, which occur when a live loan is invalidated.

```datalog
.decl loan_live_at(Loan:loan, Point:point)

// R7: compute whether a loan is live at a given point, i.e. whether it is
// contained in a live origin at this point
loan_live_at(Loan, Point) :-
  origin_contains_loan_on_entry(Origin, Loan, Point),
  (origin_live_on_entry(Origin, Point); placeholder(Origin, _)).

.decl errors(Loan:loan, Point:point)

// R8: compute illegal access errors, i.e. an invalidation of a live loan
errors(Loan, Point) :-
  loan_invalidated_at(Loan, Point),
  loan_live_at(Loan, Point).
```

--------------------------------

### Compute Loan Containment and Propagate Along CFG

Source: https://rust-lang.github.io/polonius/print.html

These rules determine which loans are contained within which origins at specific CFG points. Rule R4 initializes loans from `loan_issued_at`. Rule R5 propagates loans based on subset relations. Rule R6 propagates loans along the CFG, considering liveness and kill points.

```Datalog
.decl origin_contains_loan_on_entry(Origin:origin, Loan:loan, Point:point)

// R4: the issuing origins are the ones initially containing loans
origin_contains_loan_on_entry(Origin, Loan, Point) :-
  loan_issued_at(Origin, Loan, Point).

// R5: propagate loans within origins, at a given point, according to subsets
origin_contains_loan_on_entry(Origin2, Loan, Point) :-
  origin_contains_loan_on_entry(Origin1, Loan, Point),
  subset(Origin1, Origin2, Point).

// R6: propagate loans along the CFG, according to liveness
origin_contains_loan_on_entry(Origin, Loan, TargetPoint) :-
  origin_contains_loan_on_entry(Origin, Loan, SourcePoint),
  !loan_killed_at(Loan, SourcePoint),
  cfg_edge(SourcePoint, TargetPoint),
  (origin_live_on_entry(Origin, TargetPoint); placeholder(Origin, _)).

```

--------------------------------

### Run Polonius Analysis with Cargo

Source: https://rust-lang.github.io/polonius/getting_started.html

Execute a specific Polonius analysis (e.g., DatafrogOpt) on a given input directory using Cargo. This command allows for release builds and specifies the analysis type.

```bash
cargo +nightly run --release -- -a DatafrogOpt inputs/clap-rs/app-parser-{{impl}}-add_defaults/
```

--------------------------------

### Naive Variant: Potential Errors

Source: https://rust-lang.github.io/polonius/rules/loans.html

Computes potential illegal access errors by detecting invalidations of live loans.

```soufflé
.decl potential_errors(Loan:loan, Point:point)

// R5b: Compute potential illegal access errors, i.e. invalidations
// of live loans.
potential_errors(Loan, Point) :-
  loan_invalidated_at(Loan, Point),
  loan_live_at(Loan, Point).
```

--------------------------------

### LocationInsensitive Variant: Loan Liveness and Potential Errors Rules

Source: https://rust-lang.github.io/polonius/print.html

Approximates loan liveness based on origin liveness and computes potential illegal access errors by checking invalidated live loans.

```rust
.decl loan_live_at(Loan:loan, Point:point)

// R5a: Approximate loan liveness. If an origin is live at a given
// point, and it contains a loan *anywhere* in the CFG, that loan is
// considered live at that point.
loan_live_at(Loan, Point) :-
  origin_contains_loan(Origin, Loan),
  (origin_live_on_entry(Origin, Point); placeholder_origin(Origin)).

.decl potential_errors(Loan:loan, Point:point)

// R5b: Compute potential illegal access errors, i.e. invalidations
// of live loans.
potential_errors(Loan, Point) :-
  loan_invalidated_at(Loan, Point),
  loan_live_at(Loan, Point).
```

--------------------------------

### Input Relations for Loan Analysis

Source: https://rust-lang.github.io/polonius/rules/loans.html

Defines the input relations for Polonius's loan analysis. These relations specify how loans are issued, killed, invalidated, and how subset relationships between origins are established and known.

```datalog
// Indicates that the `loan` was "issued" at the given `point`, creating a
// reference with the `origin`. Effectively, `origin` may refer to data from
// `loan` starting at `point` (this is usually the point *after* a borrow rvalue).
.decl loan_issued_at(Origin:origin, Loan:loan, Point:point)
.input loan_issued_at

// When some prefix of the path borrowed at `loan` is assigned at `point`.
// Indicates that the path borrowed by the `loan` has changed in some way that the
// loan no longer needs to be tracked. (In particular, mutations to the path that
// was borrowed no longer invalidate the loan)
.decl loan_killed_at(Loan:loan, Point:point)
.input loan_killed_at

// Indicates that the `loan` is invalidated by some action
// taking place at `point`; if any origin that references this loan is live,
// this is an error.
.decl loan_invalidated_at(Loan:loan, Point:point)
.input loan_invalidated_at

// When we require `origin1@point: origin2@point`.
// Indicates that `origin1 <= origin2` -- i.e., the set of loans in `origin1`
// are a subset of those in `origin2`.
.decl subset_base(Origin1:origin, Origin2:origin, Point:point)
.input subset_base

// Describes a placeholder `origin`, with its associated placeholder `loan`.
.decl placeholder(Origin:origin, Loan:loan)
.input placeholder

// These reflect the `'a: 'b` relations that are either declared by the user on
// function declarations or which are inferred via implied bounds.
// For example: `fn foo<'a, 'b: 'a, 'c>(x: &'c &'a u32)` would have two entries:
// - one for the user-supplied subset `'b: 'a`
// - and one for the `'a: 'c` implied bound from the `x` parameter,
// (note that the transitive relation `'b: 'c` is not necessarily included
// explicitly, but rather inferred by polonius).
.decl known_placeholder_subset(Origin1:origin, Origin2:origin)
.input known_placeholder_subset

```

--------------------------------

### Compute Loan Liveness and Illegal Access Errors

Source: https://rust-lang.github.io/polonius/print.html

These rules compute whether a loan is live at a given point and detect illegal access errors. Rule R7 determines loan liveness based on origin liveness. Rule R8 identifies illegal access errors as invalidations of live loans.

```Datalog
.decl loan_live_at(Loan:loan, Point:point)

// R7: compute whether a loan is live at a given point, i.e. whether it is
// contained in a live origin at this point
loan_live_at(Loan, Point) :-
  origin_contains_loan_on_entry(Origin, Loan, Point),
  (origin_live_on_entry(Origin, Point); placeholder(Origin, _)).

.decl errors(Loan:loan, Point:point)

// R8: compute illegal access errors, i.e. an invalidation of a live loan
errors(Loan, Point) :-
  loan_invalidated_at(Loan, Point),
  loan_live_at(Loan, Point).

```

--------------------------------

### Displaying Polonius Analysis Results

Source: https://rust-lang.github.io/polonius/print.html

Command to show detailed results of the Polonius analysis, including errors and intermediate computations.

```bash
cargo run --show-tuples -v
```

--------------------------------

### Datalog Relations for Loan Analysis

Source: https://rust-lang.github.io/polonius/print.html

Defines the input relations used in Polonius for tracking loans and subset relationships between origins.

```datalog
.decl loan_issued_at(Origin:origin, Loan:loan, Point:point)
.input loan_issued_at

// When some prefix of the path borrowed at `loan` is assigned at `point`.
// Indicates that the path borrowed by the `loan` has changed in some way that the
// loan no longer needs to be tracked. (In particular, mutations to the path that
// was borrowed no longer invalidate the loan)
.decl loan_killed_at(Loan:loan, Point:point)
.input loan_killed_at

// Indicates that the `loan` is invalidated by some action
// taking place at `point`; if any origin that references this loan is live,
// this is an error.
.decl loan_invalidated_at(Loan:loan, Point:point)
.input loan_invalidated_at

// When we require `origin1@point: origin2@point`.
// Indicates that `origin1 <= origin2` -- i.e., the set of loans in `origin1`
// are a subset of those in `origin2`.
.decl subset_base(Origin1:origin, Origin2:origin, Point:point)
.input subset_base

// Describes a placeholder `origin`, with its associated placeholder `loan`.
.decl placeholder(Origin:origin, Loan:loan)
.input placeholder

// These reflect the `'a: 'b` relations that are either declared by the user on
// function declarations or which are inferred via implied bounds.
// For example: `fn foo<'a, 'b: 'a, 'c>(x: &'c &'a u32)` would have two entries:
// - one for the user-supplied subset `'b: 'a`
// - and one for the `'a: 'c` implied bound from the `x` parameter,
// (note that the transitive relation `'b: 'c` is not necessarily included
// explicitly, but rather inferred by polonius).
.decl known_placeholder_subset(Origin1:origin, Origin2:origin)
.input known_placeholder_subset
```

--------------------------------

### Generate NLL Facts for a Single File

Source: https://rust-lang.github.io/polonius/generate_inputs.html

Use this command to generate NLL facts for a specific Rust source file. This requires running rustc directly with the appropriate flag.

```bash
rustc -Znll-facts inputs/issue-47680/issue-47680.rs
```

--------------------------------

### List Generated NLL Fact Directories

Source: https://rust-lang.github.io/polonius/generate_inputs.html

After generating NLL facts, a `nll-facts` directory is created. This command lists the subdirectories within it, each corresponding to a function.

```bash
ls -F nll-facts
{{impl}}-maybe_next/  main/
```

--------------------------------

### Origin Contains Loan Rules

Source: https://rust-lang.github.io/polonius/rules/loans.html

Defines how loans are contained within origins at different points in the CFG. Includes initial issuance, propagation within origins via subsets, and propagation along the CFG considering liveness and kill points.

```datalog
.decl origin_contains_loan_on_entry(Origin:origin, Loan:loan, Point:point)

// R4: the issuing origins are the ones initially containing loans
origin_contains_loan_on_entry(Origin, Loan, Point) :-
  loan_issued_at(Origin, Loan, Point).

// R5: propagate loans within origins, at a given point, according to subsets
origin_contains_loan_on_entry(Origin2, Loan, Point) :-
  origin_contains_loan_on_entry(Origin1, Loan, Point),
  subset(Origin1, Origin2, Point).

// R6: propagate loans along the CFG, according to liveness
origin_contains_loan_on_entry(Origin, Loan, TargetPoint) :-
  origin_contains_loan_on_entry(Origin, Loan, SourcePoint),
  !loan_killed_at(Loan, SourcePoint),
  cfg_edge(SourcePoint, TargetPoint),
  (origin_live_on_entry(Origin, TargetPoint); placeholder(Origin, _)).
```

--------------------------------

### Illustrative Rust Code Snippet

Source: https://rust-lang.github.io/polonius/rules/atoms.html

This Rust code snippet demonstrates the creation and usage of variables, references, and their subsequent dropping, which are relevant to understanding Polonius atoms.

```rust
#![allow(unused)]
fn main() {
let x = (vec![22], vec![44]);
let y = &x.1;
let z = x.0;
drop(y);
}
```

--------------------------------

### Naive Variant: Loan Liveness Approximation

Source: https://rust-lang.github.io/polonius/rules/loans.html

Approximates loan liveness at a point if the origin containing the loan is live at that point.

```soufflé
.decl loan_live_at(Loan:loan, Point:point)

// R5a: Approximate loan liveness. If an origin is live at a given
// point, and it contains a loan *anywhere* in the CFG, that loan is
// considered live at that point.
loan_live_at(Loan, Point) :-
  origin_contains_loan(Origin, Loan),
  (origin_live_on_entry(Origin, Point); placeholder_origin(Origin)).
```

--------------------------------

### Generate NLL Facts for a Cargo Crate

Source: https://rust-lang.github.io/polonius/generate_inputs.html

To generate NLL facts for a crate managed by Cargo, use the `cargo rustc` command with the `-Znll-facts` flag. Ensure the `nll` feature is enabled in your crate.

```bash
cargo rustc -- -Znll-facts
```

--------------------------------

### Naive Variant: Origin Contains Loan

Source: https://rust-lang.github.io/polonius/rules/loans.html

Tracks loans contained within origins, including initial issuance, placeholder loans, and propagation through subsets.

```soufflé
.decl origin_contains_loan(Origin:origin, Loan:loan)

// R2: the issuing origins are the ones initially containing loans.
origin_contains_loan(Origin, Loan) :-
  loan_issued_at(Origin, Loan, _).

// R3: the placeholder origins also contain their placeholder loan.
origin_contains_loan(Origin, Loan) :-
  placeholder_loan(Origin, Loan).

// R4: propagate the loans from the origins to their subsets.
origin_contains_loan(Origin2, Loan) :-
  origin_contains_loan(Origin1, Loan),
  subset(Origin1, Origin2).
```

--------------------------------

### Naive Variant: Subset Relation

Source: https://rust-lang.github.io/polonius/rules/loans.html

Defines the transitive subsets of origins based on static input, stripping location information.

```soufflé
.decl subset(Origin1:origin, Origin2:origin)

// R1: the subsets are the non-transitive `subset_base` static input,
// with their location stripped.
subset(Origin1, Origin2) :-
  subset_base(Origin1, Origin2, _).
```

--------------------------------

### LocationInsensitive Variant: Subset and Origin Contains Loan Rules

Source: https://rust-lang.github.io/polonius/print.html

Defines the base subset relation and rules for determining which loans are contained within an origin, approximating loan propagation.

```rust
.decl subset(Origin1:origin, Origin2:origin)

// R1: the subsets are the non-transitive `subset_base` static input,
// with their location stripped.
subset(Origin1, Origin2) :-
  subset_base(Origin1, Origin2, _).

.decl origin_contains_loan(Origin:origin, Loan:loan)

// R2: the issuing origins are the ones initially containing loans.
origin_contains_loan(Origin, Loan) :-
  loan_issued_at(Origin, Loan, _).

// R3: the placeholder origins also contain their placeholder loan.
origin_contains_loan(Origin, Loan) :-
  placeholder_loan(Origin, Loan).

// R4: propagate the loans from the origins to their subsets.
origin_contains_loan(Origin2, Loan) :-
  origin_contains_loan(Origin1, Loan),
  subset(Origin1, Origin2).
```

--------------------------------

### Potential Subset Errors Calculation

Source: https://rust-lang.github.io/polonius/rules/loans.html

Detects potential illegal subset relation errors by identifying unexpected flow of placeholder loans into placeholder origins.

```soufflé
.decl potential_subset_errors(Origin1:origin, Origin2:origin)

// R6: compute potential illegal subset relations errors, i.e. the
// placeholder loans which ultimately flowed into another placeholder
// origin unexpectedly.
potential_subset_errors(Origin1, Origin2) :-
  placeholder(Origin1, Loan1),
  placeholder(Origin2, _),
  origin_contains_loan(Origin2, Loan1),
  !placeholder_known_to_contain(Origin2, Loan1).
```

--------------------------------

### Path Grammar Definition

Source: https://rust-lang.github.io/polonius/rules/atoms.html

Defines the grammar for paths in Polonius, which represent memory locations and are composed of variables, field accesses, indexing, and dereferencing.

```plaintext
Path = Variable
     | Path "." Field // field access
     | Path "[" "]"   // index
     | "*" Path
```

--------------------------------

### Placeholder Subset Error Rule

Source: https://rust-lang.github.io/polonius/rules/loans.html

Detects illegal subset relations between two placeholder origins that are not explicitly declared. This rule is used in variants like 'Naive' and 'Opt'.

```datalog
.decl subset_errors(Origin1:origin, Origin2:origin, Point:point)

// R9: compute illegal subset relations errors, i.e. the undeclared subsets
// between two placeholder origins.
subset_errors(Origin1, Origin2, Point) :-
  subset(Origin1, Origin2, Point),
  placeholder_origin(Origin1),
  placeholder_origin(Origin2),
  !known_placeholder_subset(Origin1, Origin2).
```

--------------------------------

### Compute Subset Errors for Placeholder Origins

Source: https://rust-lang.github.io/polonius/print.html

This rule computes errors related to undeclared subset relations between two placeholder origins. It flags a subset as an error if it exists between two placeholder origins and is not explicitly known.

```Datalog
.decl subset_errors(Origin1:origin, Origin2:origin, Point:point)

// R9: compute illegal subset relations errors, i.e. the undeclared subsets
// between two placeholder origins.
subset_errors(Origin1, Origin2, Point) :-
  subset(Origin1, Origin2, Point),
  placeholder_origin(Origin1),
  placeholder_origin(Origin2),
  !known_placeholder_subset(Origin1, Origin2).

```

--------------------------------

### Placeholder Known to Contain Loan

Source: https://rust-lang.github.io/polonius/rules/loans.html

Tracks placeholder loans known to be contained by a placeholder origin, including transitive relationships.

```soufflé
.decl placeholder_known_to_contain(Origin:origin, Loan:loan)

placeholder_known_to_contain(Origin, Loan) :-
  placeholder(Origin, Loan).

placeholder_known_to_contain(Origin2, Loan1) :-
  placeholder_known_to_contain(Origin1, Loan1),
  known_placeholder_subset(Origin1, Origin2).
```
Tokens:
Raw