From 65c93460b3a179101afe5a3632823ab8dc7a3f66 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 30 Aug 2019 07:56:20 -0400 Subject: [PATCH] add a book --- book/.gitignore | 1 + book/book.toml | 5 +++++ book/src/SUMMARY.md | 9 +++++++++ book/src/current_status.md | 26 ++++++++++++++++++++++++++ book/src/generate_inputs.md | 24 ++++++++++++++++++++++++ book/src/getting_started.md | 27 +++++++++++++++++++++++++++ book/src/rules.md | 4 ++++ book/src/rules/initialization.md | 1 + book/src/see_also.md | 10 ++++++++++ book/src/what_is_polonius.md | 14 ++++++++++++++ 10 files changed, 121 insertions(+) create mode 100644 book/.gitignore create mode 100644 book/book.toml create mode 100644 book/src/SUMMARY.md create mode 100644 book/src/current_status.md create mode 100644 book/src/generate_inputs.md create mode 100644 book/src/getting_started.md create mode 100644 book/src/rules.md create mode 100644 book/src/rules/initialization.md create mode 100644 book/src/see_also.md create mode 100644 book/src/what_is_polonius.md diff --git a/book/.gitignore b/book/.gitignore new file mode 100644 index 00000000000..7585238efed --- /dev/null +++ b/book/.gitignore @@ -0,0 +1 @@ +book diff --git a/book/book.toml b/book/book.toml new file mode 100644 index 00000000000..c8b69d01b62 --- /dev/null +++ b/book/book.toml @@ -0,0 +1,5 @@ +[book] +authors = ["Polonius authors"] +multilingual = false +src = "src" +title = "Polonius" diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md new file mode 100644 index 00000000000..a16f7ceca52 --- /dev/null +++ b/book/src/SUMMARY.md @@ -0,0 +1,9 @@ +# Summary + +- [What is Polonius?](./what_is_polonius.md) +- [Current status and roadmap](./current_status.md) +- [Getting started](./getting_started.md) +- [Generating inputs from rustc](./generate_inputs.md) +- [Rules](./rules.md) + - [Initialization](./rules/initialization.md) +- [See also](./see_also.md) diff --git a/book/src/current_status.md b/book/src/current_status.md new file mode 100644 index 00000000000..72d8e80f82e --- /dev/null +++ b/book/src/current_status.md @@ -0,0 +1,26 @@ +# Current status + +Polonius has been provisionally integrated into rustc. You can run a nightly +rustc with the `-Zpolonius` flag to try it out. However, it is not really +ready for widespread use. + +Our current roadmap is as follows: + +- **Complete the analysis:** Polonius represents only a portion of the full + borrow checker analysis. We would like to move as much as possible from the + handwritten Rust code in rustc into the datalog-based approach of polonius. +- **Optimize:** Naively implementing the polonius rules can be quite + slow, so it's important that we optimize the rules and produce a + more optimized version. This will also likely require some special + case optimizations to help with specific cases, such as large static + constants. + +After those two steps are done, and presuming all goes well, we expect +to replace the existing rustc borrow checker with the polonius +crate. The crate will continue to exist. + +## Want to help? + +Check out the [polonius working group][wg] of the compiler team. + +[wg]; https://rust-lang.github.io/compiler-team/working-groups/polonius/ diff --git a/book/src/generate_inputs.md b/book/src/generate_inputs.md new file mode 100644 index 00000000000..a0d3192ea95 --- /dev/null +++ b/book/src/generate_inputs.md @@ -0,0 +1,24 @@ +# 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: + +```bash +> ls -F nll-facts +{{impl}}-maybe_next/ main/ +``` + +You can then run on these directories. diff --git a/book/src/getting_started.md b/book/src/getting_started.md new file mode 100644 index 00000000000..1a3520c94d9 --- /dev/null +++ b/book/src/getting_started.md @@ -0,0 +1,27 @@ +# 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: + +```bash +> 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][post]. 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. + +[post]: http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/ diff --git a/book/src/rules.md b/book/src/rules.md new file mode 100644 index 00000000000..3ee65e6b0d3 --- /dev/null +++ b/book/src/rules.md @@ -0,0 +1,4 @@ +# Rules + +These chapters document and explain the Polonius rules, primarily in +datalog form. diff --git a/book/src/rules/initialization.md b/book/src/rules/initialization.md new file mode 100644 index 00000000000..7597c975219 --- /dev/null +++ b/book/src/rules/initialization.md @@ -0,0 +1 @@ +# Initialization diff --git a/book/src/see_also.md b/book/src/see_also.md new file mode 100644 index 00000000000..4e15c844c5e --- /dev/null +++ b/book/src/see_also.md @@ -0,0 +1,10 @@ +# See also + +There have been a number of blog posts related to Polonius as it evolves: + +- http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/ +- ... TODO add the rest ... + +The academic work "Oxide" is partially inspired by Polonius: + +- [Oxide](https://aaronweiss.us/pubs/draft19-oxide.pdf) diff --git a/book/src/what_is_polonius.md b/book/src/what_is_polonius.md new file mode 100644 index 00000000000..9343d32be63 --- /dev/null +++ b/book/src/what_is_polonius.md @@ -0,0 +1,14 @@ +# What is polonius? + +This is a core library that models the borrow check. It implements the analysis +[described in this blogpost][post]. + +[post]: http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/ + +## Why the name "Polonius"? + +The name comes from the famous quote ["Neither borrower nor lender +be"][nblnb], which comes from the character Polonius in Shakespeare's +*Hamlet*. + +[nblnb]: https://literarydevices.net/neither-a-borrower-nor-a-lender-be/