Book runner
The book runner is a testing tool based on Litani.
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:
check
jobs: This check uses the Rust front-end to detect if the example is valid Rust code.codegen
jobs: This check uses the Kani back-end to determine if we can generate GotoC code.verification
jobs: This check uses CBMC to obtain a verification result.
Note that these are incremental: A verification
job depends on a previous codegen
job.
Similary, a codegen
job depends on a check
job.
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.
The book runner report and its text version are automatically updated whenever a PR gets merged into Kani.
The book running procedure
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
here)
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 thatextract_examples()
usesrustdoc
functions to ensure the extracted examples are runnable. - Checks if there is a corresponding
.props
file insrc/tools/bookrunner/configs/
. If there is, prepends the contents of these files (testing options) to the example. - The resulting examples are written to the
src/test/bookrunner/books/
folder.
In general, the path to a given example is
src/test/bookrunner/books/<book>/<chapter>/<section>/<subsection>/<line>.rs
where<line>
is the line number where the example appears in the markdown file where it's written. The.props
files mentioned above follow the same naming scheme in order to match them and detect conflicts.
- Runs all examples using
Litani with the
litani_run_tests()
function. - Parses the Litani log file with
parse_litani_output(...)
. - Generates the text version of the bookrunner
with
generate_text_bookrunner(...)
.
NOTE: Any changes done to the examples in
src/test/bookrunner/books/
may be overwritten if the bookrunner is executed.