From 0d665356390eaa3d468608b0511fa5564ae93272 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 24 Oct 2024 13:31:32 -0400 Subject: [PATCH 1/3] Add kani script instructions to book --- doc/src/general-rules.md | 4 +++- doc/src/tools/kani.md | 39 +++++++++++++++++++++------------------ 2 files changed, 24 insertions(+), 19 deletions(-) diff --git a/doc/src/general-rules.md b/doc/src/general-rules.md index 4f419decbdf6b..79c940230dea0 100644 --- a/doc/src/general-rules.md +++ b/doc/src/general-rules.md @@ -5,7 +5,9 @@ **Verification Target:** [Our repository](https://github.com/model-checking/verify-rust-std) is a fork of the original Rust repository, and we kept a copy of the Rust standard library inside the `library/` folder that shall be used as the verification target for all our challenges. We will periodically update the `library/` folder to track newer versions of the [official Rust standard library](https://github.com/rust-lang/rust/). -NOTE: This work is not officially affiliated, or endorsed by the Rust project or Rust Foundation. + +**NOTE:** This work is not officially affiliated, or endorsed by the Rust project or Rust Foundation. + **Challenges:** Each individual verification effort will have a tracking issue where contributors can add comments and ask clarification questions. You can find the list of [open challenges here](https://github.com/model-checking/verify-rust-std/labels/Challenge). diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 9cfd198e9bc8e..9c1a74cb39b5d 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -59,7 +59,7 @@ Create a local copy of the [model-checking fork](https://github.com/model-checki `assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `modifies`, `requires` and `ensures`) directly. -For example, insert this module into an existing file in the core library, like `library/core/src/hint.rs` or `library/core/src/error.rs` in your copy of the library. This is just for the purpose of getting started, so you can insert in any existing file in the core library if you have other preferences. +For example, insert this module into an existing file in the core library, like `library/core/src/hint.rs` or `library/core/src/error.rs` in your copy of the library. This is just for the purpose of getting started, so you can insert in any other existing file in the core library as well. ``` rust #[cfg(kani)] @@ -84,22 +84,22 @@ pub mod verify { } ``` -### Step 2 - Run the Kani verify-std subcommand +### Step 2 - Run the Kani script on the std library -To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started. -Run the following command in your local terminal (Replace "/path/to/library" and "/path/to/target" with your local paths) from the verify repository root: +To aid the Rust Standard Library verification effort, Kani provides a script out of the box to help you get started. +Run the following command in your local terminal from the verify repository root: ``` -kani verify-std -Z unstable-options "/path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z mem-predicates +./scripts/run-kani.sh --path . ``` -The command `kani verify-std` is a sub-command of the `kani`. This specific sub-command is used to verify the Rust Standard Library with the following arguments. +To pass kani arguments such as `--harness`, you can run the script with `--kani-args` and continue passing in all the necessary arguments: -- `"path/to/library"`: This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script. For example, `./library` or `/home/ubuntu/verify-rust-std/library` -- `--target-dir "path/to/target"`: This optional argument sets the target directory where Kani will store its output and intermediate files. For example, `/tmp` or `/tmp/verify-std` +``` +./scripts/run-kani.sh --path . --kani-args --harness alloc::layout::verify::check_array_i32 --output-format=terse +``` -Apart from these, you can use your regular `kani-args` such as `-Z function-contracts`, `-Z stubbing` and `-Z mem-predicates` depending on your verification needs. If you run into a Kani error that says `Use of unstable feature`, add the corresponding feature with `-Z` to the command line. -For more details on Kani's features, refer to [the features section in the Kani Book](https://model-checking.github.io/kani/reference/attributes.html) +The script `run-kani` installs the right version of Kani for you, builds it and then finally runs the verify-std sub-command of the `kani` with some default flags. ### Step 3 - Check verification result @@ -122,7 +122,7 @@ You can specify a specific harness to be verified using the `--harness` flag. For example, in your local copy of the verify repo, run the following command. ``` -kani verify-std --harness harness_introduction -Z unstable-options "./library" --target-dir "/tmp" -Z function-contracts -Z mem-predicates +./scripts/run-kani.sh --kani-args --harness harness_introduction ``` This gives you the verification result for just `harness_introduction` from the aforementioned blob. @@ -144,13 +144,16 @@ Verification Time: 0.01885804s Complete - 1 successfully verified harnesses, 0 failures, 1 total. ``` -Now you can write proof harnesses to verify specific functions in the library. -The current convention is to keep proofs in the same module file of the verification target. -To run Kani for an individual proof, use `--harness [harness_function_name]`. -Note that Kani will batch run all proofs in the library folder if you do not supply the `--harness` flag. -If Kani returns the error `no harnesses matched the harness filter`, you can give the full name of the harness. -For example, to run the proof harness named `check_new` in `library/core/src/ptr/unique.rs`, use -`--harness ptr::unique::verify::check_new`. To run all proofs in `unique.rs`, use `--harness ptr::unique::verify`. +Now you can write proof harnesses to verify specific functions in the library. +The current convention is to keep proofs in the same module file of the verification target. + +To run Kani for an individual proof, use `--harness [harness_function_name]`. +Note that Kani will batch run all proofs in the library folder if you do not supply the `--harness` flag. + +If Kani returns the error `no harnesses matched the harness filter`, you can give the full name of the harness. +For example, to run the proof harness named `check_new` in `library/core/src/ptr/unique.rs`, use +`--harness ptr::unique::verify::check_new`. To run all proofs in `unique.rs`, use `--harness ptr::unique::verify`. + To find the full name of a harness, check the Kani output and find the line starting with `Checking harness [harness full name]`. ## More details From 5903fa6d4686fb06fbc35cbf7c8b97af1bf1ce99 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Tue, 29 Oct 2024 13:26:00 -0400 Subject: [PATCH 2/3] Apply suggestions from code review Co-authored-by: Carolyn Zech --- doc/src/tools/kani.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 9c1a74cb39b5d..62150d6f98588 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -59,7 +59,8 @@ Create a local copy of the [model-checking fork](https://github.com/model-checki `assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `modifies`, `requires` and `ensures`) directly. -For example, insert this module into an existing file in the core library, like `library/core/src/hint.rs` or `library/core/src/error.rs` in your copy of the library. This is just for the purpose of getting started, so you can insert in any other existing file in the core library as well. +For example, insert this module into an existing file in the core library, like `library/core/src/hint.rs` or `library/core/src/error.rs` in your copy of the library. +This is just for the purpose of getting started, so you can insert it in a different (existing) file in the core library instead. ``` rust #[cfg(kani)] From 03a79e6b8fcda6f05af2c574b25ad3ba05c43789 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Tue, 29 Oct 2024 14:26:01 -0400 Subject: [PATCH 3/3] Address PR comment --- doc/src/tools/kani.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 9c1a74cb39b5d..ef16dc69c06a3 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -101,6 +101,8 @@ To pass kani arguments such as `--harness`, you can run the script with `--kani- The script `run-kani` installs the right version of Kani for you, builds it and then finally runs the verify-std sub-command of the `kani` with some default flags. +**NOTE:** This script may crash due to linking issues. If the script fails with an error message related to linking, link the new CBMC version, delete the `./kani_build` directory and re-run. + ### Step 3 - Check verification result After running the command, you can expect an output that looks like this: