### 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). ``` === COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.