diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 6e94b10a60d8..9b74ff0d793c 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -1,4 +1,4 @@ -# The Kani Rust Verifier +# Kani Rust Verifier - [Getting started](./getting-started.md) - [Installation](./install-guide.md) diff --git a/docs/src/bookrunner.md b/docs/src/bookrunner.md index 4e5aad062c20..c9e647dd6552 100644 --- a/docs/src/bookrunner.md +++ b/docs/src/bookrunner.md @@ -20,7 +20,7 @@ Because of that, we run up to three different types of jobs when generating the 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](https://github.com/awslabs/aws-build-accumulator) does not +> **NOTE**: [Litani](https://github.com/awslabs/aws-build-accumulator) does not > support hierarchical views at the moment. For this reason, we are publishing a > [text version of the book runner report](./bookrunner/bookrunner.txt) which > displays the same results in a hierarchical way while we work on [improvements @@ -34,7 +34,7 @@ Before running the above mentioned jobs, we pre-process the examples to: 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 is considered a failed example that cannot be handled by Kani. +If an example shows one red bar, it's considered a failed example that cannot be handled by Kani. The [book runner report](./bookrunner/index.html) and [its text version](./bookrunner/bookrunner.txt) are automatically updated whenever a PR gets merged into Kani. @@ -49,8 +49,8 @@ To kick off the book runner process use: cargo run -p bookrunner ``` -The main function of the bookrunner is `generate_run()` in -[`src/tools/bookrunner/src/books.rs`](https://github.com/model-checking/kani/blob/main/tools/bookrunner/src/books.rs), +The main function of the bookrunner is `generate_run()` (code available +[here](https://github.com/model-checking/kani/blob/main/tools/bookrunner/src/books.rs)) which follows these steps: 1. Sets up all the books, including data about their summaries. 2. Then, for each book: diff --git a/docs/src/dev-documentation.md b/docs/src/dev-documentation.md index 611645e8e4a1..d480c4340d19 100644 --- a/docs/src/dev-documentation.md +++ b/docs/src/dev-documentation.md @@ -14,7 +14,7 @@ developers (including external contributors): 3. [Development setup recommendations for working with `rustc`](./rustc-hacks.md). 4. [Guide for testing in Kani](./testing.md). -> **NOTE:** The developer documentation is intended for Kani developers and not +> **NOTE**: The developer documentation is intended for Kani developers and not users. At present, the project is under heavy development and some items discussed in this documentation may stop working without notice (e.g., commands or configurations). Therefore, we recommend users to not rely on them. diff --git a/docs/src/install-guide.md b/docs/src/install-guide.md index ebbd2843a13b..c93e3104e098 100644 --- a/docs/src/install-guide.md +++ b/docs/src/install-guide.md @@ -4,8 +4,8 @@ Kani must currently be built from source. In general, the following dependencies are required. -> **Note:** These dependencies may be installed by running the CI scripts shown -> below and there is no need to install them separately, for their respective +> **NOTE**: These dependencies may be installed by running the CI scripts shown +> below and there's no need to install them separately, for their respective > OS. 1. Cargo installed via [rustup](https://rustup.rs/) @@ -62,7 +62,7 @@ Then, optionally, run the regression tests: ./scripts/kani-regression.sh ``` -This script has a lot of noisy output, but on a successful run you will see: +This script has a lot of noisy output, but on a successful run you'll see: ``` All Kani regression tests completed successfully. diff --git a/docs/src/kani-tutorial.md b/docs/src/kani-tutorial.md index 74ff646e2c8b..5c075c608fee 100644 --- a/docs/src/kani-tutorial.md +++ b/docs/src/kani-tutorial.md @@ -1,6 +1,6 @@ # Tutorial -> Note: This tutorial expects you to have followed the Kani [installation instructions](./install-guide.md) first. +> **NOTE**: This tutorial expects you to have followed the Kani [installation instructions](./install-guide.md) first. This tutorial will step you through a progression from simple to moderately complex tasks with Kani. It's meant to ensure you can get started, and see at least some simple examples of how typical proofs are structured. diff --git a/docs/src/regression-testing.md b/docs/src/regression-testing.md index b4154e02f251..07c99358668e 100644 --- a/docs/src/regression-testing.md +++ b/docs/src/regression-testing.md @@ -16,7 +16,7 @@ The `kani-regression.sh` script executes different testing commands, which we cl See below for a description of each one. Note that regression testing is run whenever a Pull Request is opened, updated or merged -into the main branch. Therefore, it is a good idea to run regression testing locally before +into the main branch. Therefore, it's a good idea to run regression testing locally before submitting a Pull Request for Kani. ## Kani testing suites @@ -33,7 +33,7 @@ Command-line options can be passed to the test by adding a special comment to the file. See [testing options](#testing-options) for more details. In particular, the Kani testing suites are composed of: - * `kani`: The main testing suite for Kani. The test is a single Rust file that is + * `kani`: The main testing suite for Kani. The test is a single Rust file that's run through Kani. In general, the test passes if verification with Kani is successful, otherwise it fails. * `firecracker`: Works like `kani` but contains tests inspired by @@ -57,7 +57,7 @@ In particular, the Kani testing suites are composed of: Similar to the `expected` suite, we look for `*.expected` files for each harness in the package. -We have extended +We've extended [`compiletest`](https://rustc-dev-guide.rust-lang.org/tests/intro.html) (the Rust compiler testing framework) to work with these suites. That way, we take advantage of all `compiletest` features (e.g., parallel execution). @@ -77,7 +77,7 @@ If a test fails, the error message will include the stage where it failed: error: test failed: expected check success, got failure ``` -When working on a test that is expected to fail, there are two options to +When working on a test that's expected to fail, there are two options to indicate an expected failure. The first one is to add a comment ```rust,noplaypen @@ -92,7 +92,7 @@ that you expect not to hold during verification. The testing framework expects one `EXPECTED FAIL` message in the verification output for each use of the predicate. -> **NOTE:** `kani::expect_fail` is only useful to indicate failure in the +> **NOTE**: `kani::expect_fail` is only useful to indicate failure in the > `verify` stage, errors in other stages will be considered testing failures. ### Testing options diff --git a/docs/src/rust-feature-support.md b/docs/src/rust-feature-support.md index e45298fe13ec..892e84afdb61 100644 --- a/docs/src/rust-feature-support.md +++ b/docs/src/rust-feature-support.md @@ -148,9 +148,9 @@ features](#code-generation-for-unsupported-features). This results in verification failures if a call to one of these missing functions is reachable. -We have done some experiments to embed the standard library into the generated +We've done some experiments to embed the standard library into the generated code, but this causes verification times to increase significantly. As of now, -we have not been able to find a simple solution for [this +we've not been able to find a simple solution for [this issue](https://github.com/model-checking/kani/issues/581), but we have some ideas for future work in this direction. At present, Kani [overrides](./overrides.md) a few common functions (e.g., print macros) as @@ -177,7 +177,7 @@ In particular, there are some outstanding issues to note here: We are particularly interested in bug reports concerning these features, so please [file a bug report](https://github.com/model-checking/kani/issues/new?assignees=&labels=bug&template=bug_report.md) -if you are aware of one. +if you're aware of one. ### Panic strategies diff --git a/docs/src/rustc-hacks.md b/docs/src/rustc-hacks.md index 960d94c6b999..79ff206e0e70 100644 --- a/docs/src/rustc-hacks.md +++ b/docs/src/rustc-hacks.md @@ -36,7 +36,7 @@ rustup toolchain install nightly --component rustc-dev ### CLion / IntelliJ This is not a great solution, but it works for now (see for more details). -Edit the `Cargo.toml` of the package that you are working on and add artificial dependencies on the `rustc` packages that you would like to explore. +Edit the `Cargo.toml` of the package that you're working on and add artificial dependencies on the `rustc` packages that you would like to explore. ```toml # This configuration doesn't exist so it shouldn't affect your build. @@ -59,7 +59,7 @@ There are a few reasons why you may want to use your own copy of `rustc`. E.g.: We will assume that you already have a Kani setup and that the variable `KANI_WORKSPACE` contains the path to your Kani workspace. -**It is highly recommended that you start from the commit that corresponds to the current `rustc` version from your workspace.** +**It's highly recommended that you start from the commit that corresponds to the current `rustc` version from your workspace.** To get that information, run the following command: ```bash cd ${KANI_WORKSPACE} # Go to your Kani workspace. @@ -102,4 +102,4 @@ cargo build In order to enable logs, you can just define the `RUSTC_LOG` variable, as documented here: . -Note that depending on the level of logs you would like to enable, you will need to build your own version of `rustc` as described above. +Note that depending on the level of logs you would like to enable, you'll need to build your own version of `rustc` as described above. diff --git a/docs/src/testing.md b/docs/src/testing.md index 3896e0bc0ce1..a69495922a90 100644 --- a/docs/src/testing.md +++ b/docs/src/testing.md @@ -14,5 +14,5 @@ two very good reasons to do it: particularly valuable for project management purposes. We recommend reading our section on [Regression Testing](./regression-testing.md) -if you are interested in Kani development. At present, we obtain metrics based +if you're interested in Kani development. At present, we obtain metrics based on the [book runner](./bookrunner.md). \ No newline at end of file diff --git a/docs/src/tool-comparison.md b/docs/src/tool-comparison.md index d11e50c9968c..cfbf86e16383 100644 --- a/docs/src/tool-comparison.md +++ b/docs/src/tool-comparison.md @@ -13,7 +13,7 @@ Tests in this style do actually state properties: *For all inputs (of some const Property testing is often quite effective, but the engine can't fully prove the property: It can only sample randomly a few of those values to test (though property testing libraries frequently give interesting "edge cases" a higher probability, making them more effective at bug-finding). -**Model checking** is similar to these techniques in how you use them, but it is non-random and exhaustive (though often only up to some bound on input or problem size). +**Model checking** is similar to these techniques in how you use them, but it's non-random and exhaustive (though often only up to some bound on input or problem size). Thus, properties checked with a model checker are effectively proofs. Instead of naively trying all possible _concrete_ inputs (which could be infeasible and blow up exponentially), model checkers like Kani will cleverly encode program traces as _symbolic_ "[SAT](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem)/[SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)" problems, and hand them off to SAT/SMT solvers. Again, SAT/SMT solving is an [NP-complete](https://en.wikipedia.org/wiki/NP-completeness) problem, but most practical programs can be model- checked within milliseconds to seconds (with notable exceptions: you can easily try to reverse a cryptographic hash with a model checker, but good luck getting it to terminate!) diff --git a/docs/src/tutorial-first-steps.md b/docs/src/tutorial-first-steps.md index e3c5a736509f..b0eee6f46a3e 100644 --- a/docs/src/tutorial-first-steps.md +++ b/docs/src/tutorial-first-steps.md @@ -4,7 +4,7 @@ Kani is unlike the testing tools you may already be familiar with. Much of testing is concerned with thinking of new corner cases that need to be covered. With Kani, all the corner cases are covered from the start, and the new concern is narrowing down the scope to something manageable for the checker. -Consider this first program (which can be found under [`docs/src/tutorial/kani-first-steps`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/kani-first-steps/)): +Consider this first program (which can be found under [`kani-first-steps`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/kani-first-steps/)): ```rust,noplaypen {{#include tutorial/kani-first-steps/src/lib.rs:code}} @@ -99,7 +99,7 @@ warning: dereferencing a null pointer = note: `#[warn(deref_nullptr)]` on by default ``` -Still, it is just a warning, and we can run the code without test failures just as before. +Still, it's just a warning, and we can run the code without test failures just as before. But Kani still catches the issue: ``` @@ -149,7 +149,7 @@ Let's encode this fact about our function by asserting some reasonable bound on {{#include tutorial/kani-first-steps/src/final_form.rs:code}} ``` -Now we have stated our previously implicit expectation: this function should never be called with inputs that are too big. +Now we've stated our previously implicit expectation: this function should never be called with inputs that are too big. But if we attempt to verify this, we get a problem: ``` diff --git a/docs/src/tutorial-kinds-of-failure.md b/docs/src/tutorial-kinds-of-failure.md index d218960ce844..67a51fdbd96f 100644 --- a/docs/src/tutorial-kinds-of-failure.md +++ b/docs/src/tutorial-kinds-of-failure.md @@ -8,7 +8,7 @@ In this section, we're going to expand on these additional checks, to give you a ## Bounds checking and pointers Rust is safe by default, and so includes dynamic (run-time) bounds checking where needed. -Consider this Rust code (from [`src/bounds_check.rs`](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs)): +Consider this Rust code (available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs)): ```rust,noplaypen {{#include tutorial/kinds-of-failure/src/bounds_check.rs:code}} @@ -148,7 +148,7 @@ Kani will spot this not as a bound error, but as a mathematical error: on an emp 1. Exercise: Try to run Kani on the above, to see what this kind of failure looks like. Rust also performs runtime safety checks for integer overflows, much like it does for bounds checks. -Consider this code (from [`src/overflow.rs`](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow.rs)): +Consider this code (available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow.rs)): ```rust,noplaypen {{#include tutorial/kinds-of-failure/src/overflow.rs:code}} @@ -175,7 +175,7 @@ For instance, instead of `a + b` write `a.wrapping_add(b)`. ### Exercise: Classic overflow failure One of the classic subtle bugs that persisted in many implementations for a very long time is finding the midpoint in quick sort. -This often naively looks like this (from [`src/overflow_quicksort.rs`](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow_quicksort.rs)): +This often naively looks like this (code available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow_quicksort.rs)): ```rust,noplaypen {{#include tutorial/kinds-of-failure/src/overflow_quicksort.rs:code}} diff --git a/docs/src/tutorial-loop-unwinding.md b/docs/src/tutorial-loop-unwinding.md index 8c601a857fa7..bd8920476b38 100644 --- a/docs/src/tutorial-loop-unwinding.md +++ b/docs/src/tutorial-loop-unwinding.md @@ -1,6 +1,6 @@ # Loops, unwinding, and bounds -Consider code like this (from [`src/lib.rs`](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/loops-unwinding/src/lib.rs)): +Consider code like this (available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/loops-unwinding/src/lib.rs)): ```rust,noplaypen {{#include tutorial/loops-unwinding/src/lib.rs:code}} @@ -16,7 +16,7 @@ We can try to find this bug with a proof harness like this: When we run Kani on this, we run into an unfortunate result: non-termination. This non-termination is caused by CBMC trying to unwind the loop an unlimited number of times. -> **NOTE:** Presently, [due to a bug](https://github.com/model-checking/kani/issues/493), this is especially bad: we don't see any output at all. +> **NOTE**: Presently, [due to a bug](https://github.com/model-checking/kani/issues/493), this is especially bad: we don't see any output at all. > Kani is supposed to emit some log lines that might give some clue that an infinite loop is occurring. > If Kani doesn't terminate, it's almost always the problem that this section covers. diff --git a/docs/src/tutorial-nondeterministic-variables.md b/docs/src/tutorial-nondeterministic-variables.md index 1c9fcd9a54f0..5ea27d5c42aa 100644 --- a/docs/src/tutorial-nondeterministic-variables.md +++ b/docs/src/tutorial-nondeterministic-variables.md @@ -13,14 +13,14 @@ In this tutorial, we will show how to: ## Safe nondeterministic variables -Let's say you are developing an inventory management tool, and you would like to verify that your API to manage items is correct. +Let's say you're developing an inventory management tool, and you would like to verify that your API to manage items is correct. Here is a simple implementation of this API: ```rust,noplaypen {{#include tutorial/arbitrary-variables/src/inventory.rs:inventory_lib}} ``` -Now we would like to verify that, no matter which combination of `id` and `quantity`, a call to `Inventory::update()` followed by a call to `Inventory::get()` using the same `id` returns some value that is equal to the one we inserted: +Now we would like to verify that, no matter which combination of `id` and `quantity`, a call to `Inventory::update()` followed by a call to `Inventory::get()` using the same `id` returns some value that's equal to the one we inserted: ```rust,noplaypen {{#include tutorial/arbitrary-variables/src/inventory.rs:safe_update}} @@ -32,7 +32,7 @@ In this harness, we use `kani::any()` to generate the new `id` and `quantity`. If we run this example, Kani verification will succeed, including the assertion that shows that the underlying `u32` variable used to represent `NonZeroU32` cannot be zero, per its type invariant: You can try it out by running the example under -[arbitrary-variables directory](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/): +[`arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/): ``` cargo kani --harness safe_update @@ -57,7 +57,7 @@ The verification will now fail showing that the `inventory.get(&id).unwrap()` me This is an interesting issue that emerges from how `rustc` optimizes the memory layout of `Option`. The compiler is able to represent `Option` using `32` bits by using the value `0` to represent `None`. -You can try it out by running the example under [arbitrary-variables directory](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/): +You can try it out by running the example under [`arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/): ``` cargo kani --harness unsafe_update @@ -88,7 +88,7 @@ Now you can use `kani::any()` to create valid nondeterministic variables of the ``` You can try it out by running the example under -[`docs/src/tutorial/arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/): +[`arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/): ``` cargo kani --harness check_rating