GitXplorerGitXplorer
r

polonius

public
1382 stars
73 forks
41 issues

Commits

List of commits on branch master.
Unverified
adbeac35bfe5b1d8a9dd538f6e6b4889ed817f99

polonius-proof in book

llengyijun committed 3 years ago
Verified
cf585fd76c9e65552fd9a8f320c3c2d8f822a75e

Merge pull request #180 from mlindner/master

llqd committed 3 years ago
Unverified
9d3011989e923b89df8a5bf3d0bdd2915627b00e

fix typo in README quote

mmlindner committed 3 years ago
Verified
0cbbb7c6b2f9dd713266b77c0c13903ac16e1679

Merge pull request #173 from domenicquirl/parser

llqd committed 3 years ago
Unverified
a7301ff6ef47b03c6d34b2f3a6d56a6bfcad1b45

fix old rust-lang nursery reference

llqd committed 3 years ago
Unverified
c3e7a8413e1d170e935806a7a3acb8d938474ea8

fix typo in readme

llqd committed 3 years ago

README

The README file for this repository.

This is a core library that models the borrow check. It implements the analysis described in this blogpost and in this talk. Details are in the Polonius book.

Why the name "Polonius"?

The name comes from the famous quote "Neither a borrower nor a lender be", which comes from the character Polonius in Shakespeare's Hamlet.

Want to run the code?

One of the goals with this repo is to experiment and compare different implementations of the same algorithm. You can run the analysis by using cargo run and you can choose the analysis with -a. So for example to run against an example extract from clap, you might do:

> cargo +nightly run --release -- -a DatafrogOpt inputs/clap-rs/app-parser-{{impl}}-add_defaults/
    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

You could also try -a Naive to get the naive rules (more readable, slower) -- these are the exact rules described in the blogpost. You can also use -a LocationInsensitive to use a location insensitive analysis (faster, but may yield spurious errors).

By default, cargo run just prints timing. If you also want to see the results, try --show-tuples (which will show errors) and maybe -v (to show more intermediate computations). You can supply --help to get more docs.

How to generate your own inputs

To run the borrow checker on an input, you first need to generate the input facts. For that, you will need to run rustc with the -Znll-facts option:

> rustc -Znll-facts inputs/issue-47680/issue-47680.rs

Or, for generating the input facts of a crate using the #![feature(nll)] flag:

> cargo rustc -- -Znll-facts

This will generate a nll-facts directory with one subdirectory per function:

> ls -F nll-facts
{{impl}}-maybe_next/  main/

You can then run on these directories.