69 lines
2.6 KiB
Markdown
69 lines
2.6 KiB
Markdown
# Kani
|
|
This document describes how to **locally** install and use Kani, along
|
|
with its experimental PropProof feature. Because of instability in
|
|
Kani internals, the GitHub action is the recommended option if you are
|
|
running in CI.
|
|
|
|
Kani is a software verification tool that complements testing by
|
|
proving the absence of certain classes of bugs like unwrap exceptions,
|
|
overflows, and assertion failures. See the [Kani
|
|
book](https://model-checking.github.io/kani/) for a full list of
|
|
capabilities and limitations.
|
|
|
|
## Installing Kani and PropProof
|
|
- The install instructions for Kani can be [found
|
|
here](https://model-checking.github.io/kani/install-guide.html). Once
|
|
Kani is installed, you can run with `cargo kani` for projects or
|
|
`kani` for individual Rust files.
|
|
- **[UNSTABLE]** To use PropProof, first download the source code
|
|
from the Kani repository.
|
|
```bash
|
|
git clone https://github.com/model-checking/kani.git --branch features/proptest propproof
|
|
cd propproof; git submodule update --init
|
|
```
|
|
|
|
Then, use `.cargo/config.toml` enable it in the local directory you
|
|
want to run Kani in. This will override the `proptest` import in
|
|
your repo.
|
|
|
|
```bash
|
|
cd $YOUR_REPO_LOCAL_PATH
|
|
mkdir '.cargo'
|
|
echo "paths =[\"$PATH_TO_PROPPROOF\"]" > .cargo/config.toml
|
|
```
|
|
|
|
**Please Note**:
|
|
- `features/proptest` branch under Kani is likely not the final
|
|
location for this code. If these instructions stop working, please
|
|
consult the Kani documentation and file an issue on [the Kani
|
|
repo](https://github.com/model-checking/kani.git).
|
|
- The cargo config file will force cargo to always use PropProof. To
|
|
use `proptest`, delete the file.
|
|
|
|
## Running Kani
|
|
After installing Kani and PropProof, `cargo kani --tests` should
|
|
automatically run `proptest!` harnesses inside your crate. Use
|
|
`--harness` to run a specific harness, and `-p` for a specific
|
|
sub-crate.
|
|
|
|
If Kani returns with an error, you can use the concrete playback
|
|
feature using `--enable-unstable --concrete-playback print` and paste
|
|
in the code to your repository. Running this harness with `cargo test`
|
|
will replay the input found by Kani that produced this crash. Please
|
|
note that this feature is unstable and using `--concrete-playback
|
|
inplace` to automatically inject a replay harness is not supported
|
|
when using PropProof.
|
|
|
|
## Debugging CI Failure
|
|
```yaml
|
|
- name: Verify with Kani
|
|
uses: model-checking/kani-github-action@v0.xx
|
|
with:
|
|
enable-propproof: true
|
|
args: |
|
|
$KANI_ARGUMENTS
|
|
```
|
|
|
|
The above GitHub CI workflow is equivalent to `cargo kani
|
|
$KANI_ARGUMENTS` with PropProof installed. To replicate issues
|
|
locally, run `cargo kani` with the same arguments.
|