From a5f34440c0f65de3cfb306a026acd1da955c78a9 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Fri, 13 Sep 2024 19:14:07 -0700 Subject: [PATCH 1/8] add instruction to run specific proofs in library using kani --- doc/src/tools/kani.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 985d507c4be33..22334f8e1c328 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -55,12 +55,12 @@ To aid the Rust Standard Library verification effort, Kani provides a sub-comman Modify your local copy of the Rust Standard Library by writing proofs for the functions/methods that you want to verify. -For example, insert this short blob into your copy of the library. This blob imports the building-block APIs such as +For example, insert this short blob into a rust file named `example.rs` inside your copy of the library folder. This blob imports the building-block APIs such as `assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `proof_for_contract` and `fake_function`. ``` rust #[cfg(kani)] -kani_core::kani_lib!(core); +use crate::kani; #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] @@ -88,14 +88,14 @@ pub mod verify { Run the following command in your local terminal: -`kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing`. +`kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing -Z mem-predicates`. 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. - `"path/to/library"`: This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script. - `--target-dir "path/to/target"`: This optional argument sets the target directory where Kani will store its output and intermediate files. -Apart from these, you can use your regular `kani-args` such as `-Z function-contracts` and `-Z stubbing` depending on your verification needs. +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 kani error that says `Use of unstable feature`, add the corresponding feature with `-Z` to the command. 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) ### Step 3 @@ -112,6 +112,9 @@ Verification Time: 0.017101772s Complete - 2 successfully verified harnesses, 0 failures, 2 total. ``` +### Step 4 +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 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 fullname 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 fullname of a harness, check the kani output and find the line starting with `Checking harness [harness fullname]`. + ## More details You can find more information about how to install and how you can customize your use of Kani in the From 50bbe1048fba928c9cc83352ed5f5a3d2e510846 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Fri, 13 Sep 2024 19:32:45 -0700 Subject: [PATCH 2/8] revert to kani_core --- doc/src/tools/kani.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 22334f8e1c328..473803e9c0582 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -60,7 +60,7 @@ For example, insert this short blob into a rust file named `example.rs` inside y ``` rust #[cfg(kani)] -use crate::kani; +kani_core::kani_lib!(core); #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] From 8b6a357e8434845f72d939d33fbe1170222f592a Mon Sep 17 00:00:00 2001 From: Qinyuan Wu <53478459+QinyuanWu@users.noreply.github.com> Date: Mon, 16 Sep 2024 09:17:27 -0700 Subject: [PATCH 3/8] Update doc/src/tools/kani.md Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> --- doc/src/tools/kani.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 473803e9c0582..72a438fb9482b 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -86,7 +86,7 @@ pub mod verify { ### Step 2 -Run the following command in your local terminal: +Run the following command in your local terminal (replace /path/ with your local paths): `kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing -Z mem-predicates`. From 27e78f6b87a3b26155b2c93ef9e69d9ee3a67ee6 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Mon, 16 Sep 2024 09:25:05 -0700 Subject: [PATCH 4/8] remove -Z stubbing --- doc/src/tools/kani.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 72a438fb9482b..879b266cdd953 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -86,9 +86,9 @@ pub mod verify { ### Step 2 -Run the following command in your local terminal (replace /path/ with your local paths): +Run the following command in your local terminal (replace /path/to/ with your local paths): -`kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing -Z mem-predicates`. +`kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z mem-predicates`. 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. From aab0d704e4d0a15f098957eb2aa563a9bbac069d Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 27 Sep 2024 13:16:25 -0400 Subject: [PATCH 5/8] Update doc/src/tools/kani.md --- doc/src/tools/kani.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 83e7c1a2a413f..129203ad9dcfc 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -98,7 +98,7 @@ The command `kani verify-std` is a sub-command of the `kani`. This specific sub- - `"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` -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 kani error that says `Use of unstable feature`, add the corresponding feature with `-Z` to the command. +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) ### Step 3 - Check verification result From 5a72f27b49da647b575b3fae548b1807821042fa Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 27 Sep 2024 13:16:33 -0400 Subject: [PATCH 6/8] Update doc/src/tools/kani.md --- doc/src/tools/kani.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 129203ad9dcfc..a7175208fbb0c 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -146,7 +146,7 @@ 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 individual proof, use `--harness [harness_function_name]`. +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 fullname of the harness. For example, to run the proof harness named `check_new` in `library/core/src/ptr/unique.rs`, use From 10724fa4a4358d152f26fb32f3bbc913577dc47e Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 27 Sep 2024 13:16:41 -0400 Subject: [PATCH 7/8] Update doc/src/tools/kani.md --- doc/src/tools/kani.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index a7175208fbb0c..da9ac6b1490b5 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -148,7 +148,7 @@ 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 fullname of the harness. +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 fullname of a harness, check the kani output and find the line starting with `Checking harness [harness fullname]`. From b1356164aa482aaf71fec7f7e20316071e783540 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 27 Sep 2024 13:16:47 -0400 Subject: [PATCH 8/8] Update doc/src/tools/kani.md --- doc/src/tools/kani.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index da9ac6b1490b5..9cfd198e9bc8e 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -151,7 +151,7 @@ Note that Kani will batch run all proofs in the library folder if you do not sup 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 fullname of a harness, check the kani output and find the line starting with `Checking harness [harness fullname]`. +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