The purpose of the book runner is to get data about feature coverage in Kani. To this end, we use Rust code snippet examples from the following general Rust documentation books:
- The Rust Reference
- The Rustonomicon
- The Rust Unstable Book
- Rust By Example
However, not all examples from these books are suited for verification. For instance, some of them are only included to show what is valid Rust code (or what is not).
Because of that, we run up to three different types of jobs when generating the report:
checkjobs: This check uses the Rust front-end to detect if the example is valid Rust code.
codegenjobs: This check uses the Kani back-end to determine if we can generate GotoC code.
verificationjobs: This check uses CBMC to obtain a verification result.
Note that these are incremental: A
verification job depends on a previous
codegen job depends on a
NOTE: Litani does not support hierarchical views at the moment. For this reason, we are publishing a text version of the book runner report which displays the same results in a hierarchical way while we work on improvements for the visualization and navigation of book runner results.
Before running the above mentioned jobs, we pre-process the examples to:
- Set the expected output according to flags present in the code snippet.
- Add any required compiler/Kani flags (e.g., unwinding).
Finally, we run all jobs, collect their outputs and compare them against the expected outputs. The results are summarized as follows: If the obtained and expected outputs differ, the color of the stage bar will be red. Otherwise, it will be blue. If an example shows one red bar, it's considered a failed example that cannot be handled by Kani.
This section describes how the book runner operates at a high level.
To kick off the book runner process use:
cargo run -p bookrunner
The main function of the bookrunner is
generate_run() (code available
which follows these steps:
- Sets up all the books, including data about their summaries.
- Then, for each book:
- Calls the
parse_hierarchy()method to parse its summary files.
- Calls the
extract_examples()method to extract all examples from the book. Note that
rustdocfunctions to ensure the extracted examples are runnable.
- Checks if there is a corresponding
src/tools/bookrunner/configs/. If there is, prepends the contents of these files (testing options) to the example.
- The resulting examples are written to the
In general, the path to a given example is
<line>is the line number where the example appears in the markdown file where it's written. The
.propsfiles mentioned above follow the same naming scheme in order to match them and detect conflicts.
- Runs all examples using
Litani with the
- Parses the Litani log file with
- Generates the text version of the bookrunner
NOTE: Any changes done to the examples in
src/test/bookrunner/books/may be overwritten if the bookrunner is executed.