Skip to content

Commit

Permalink
Merge branch 'main' into atomic-challenge
Browse files Browse the repository at this point in the history
  • Loading branch information
carolynzech authored Oct 30, 2024
2 parents 7ecabf1 + abe2354 commit cc84fc7
Show file tree
Hide file tree
Showing 29 changed files with 1,372 additions and 104 deletions.
45 changes: 37 additions & 8 deletions .github/workflows/kani.yml
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
# This workflow is responsible for verifying the standard library with Kani.

name: Kani

on:
workflow_dispatch:
pull_request:
Expand All @@ -9,30 +8,60 @@ on:
paths:
- 'library/**'
- '.github/workflows/kani.yml'
- 'scripts/check_kani.sh'
- 'scripts/run-kani.sh'

defaults:
run:
shell: bash

jobs:
build:
check-kani-on-std:
name: Verify std library
runs-on: ${{ matrix.os }}
strategy:
matrix:
# Kani does not support windows.
os: [ubuntu-latest, macos-latest]
include:
- os: ubuntu-latest
base: ubuntu
- os: macos-latest
base: macos
steps:
- name: Checkout Library
# Step 1: Check out the repository
- name: Checkout Repository
uses: actions/checkout@v4
with:
path: head
submodules: true

- name: Run Kani Script
run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head
# Step 2: Run Kani on the std library (default configuration)
- name: Run Kani Verification
run: head/scripts/run-kani.sh --path ${{github.workspace}}/head

test-kani-script:
name: Test Kani script
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macos-latest]
include:
- os: ubuntu-latest
base: ubuntu
- os: macos-latest
base: macos
steps:
# Step 1: Check out the repository
- name: Checkout Repository
uses: actions/checkout@v4
with:
path: head
submodules: true

# Step 2: Test Kani verification script with specific arguments
- name: Test Kani script (Custom Args)
run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse

# Step 3: Test Kani verification script in the repository directory
- name: Test Kani script (In Repo Directory)
working-directory: ${{github.workspace}}/head
run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
2 changes: 2 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,9 @@ Session.vim
## Build
/book/
/build/
/kani_build/
/target
library/target
*.rlib
*.rmeta
*.mir
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -47,4 +47,4 @@ See [the Rust repository](https://github.com/rust-lang/rust) for details.

## Introducing a New Tool

Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool.
Please use the [template available in this repository](./doc/src/tool_template.md) to introduce a new verification tool.
4 changes: 2 additions & 2 deletions doc/src/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@
[Introduction](intro.md)

- [General Rules](./general-rules.md)
- [Challenge Template](./template.md)
- [Tool application](./todo.md)
- [Challenge Template](./challenge_template.md)
- [Tool Application Template](./tool_template.md)

- [Verification Tools](./tools.md)
- [Kani](./tools/kani.md)
Expand Down
File renamed without changes.
6 changes: 3 additions & 3 deletions doc/src/general-rules.md
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ A proposed solution to a verification problem will only **be reviewed** if all t
* The contribution must be automated and should be checked and pass as part of the PR checks.
* All tools used by the solution must be in [the list of accepted tools](tools.md#approved-tools),
and previously integrated in the repository.
If that is not the case, please submit a separate [tool application first](todo.md).
If that is not the case, please submit a separate [tool application first](./general-rules.md#tool-applications).
* There is no restriction on the number of contributors for a solution.
Make sure you have the rights to submit your solution and that all contributors are properly mentioned.
* The solution cannot impact the runtime logic of the standard library unless the change is proposed and incorporated
Expand All @@ -56,7 +56,7 @@ The type of obstacles users face may depend on which part of the standard librar
Everyone is welcome to submit new challenge proposals for review by our committee.
Follow the following steps to create a new proposal:

1. Create a tracking issue using the Issue template [Challenge Proposal](template.md) for your challenge.
1. Create a tracking issue using the [challenge template](./challenge_template.md) for your challenge.
2. In your fork of this repository do the following:
1. Copy the template file (`book/src/challenge_template.md`) to `book/src/challenges/<ID_NUMBER>-<challenge-name>.md`.
2. Fill in the details according to the template instructions.
Expand All @@ -69,7 +69,7 @@ Follow the following steps to create a new proposal:

Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools):

* Any new tool that participants want to enable will require an application using the Issue template [Tool application](todo.md).
* Any new tool that participants want to enable will require an application using the [tool application template](./tool_template.md).
* The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS
* A new tool application should clearly specify the differences to existing techniques and provide sufficient background
of why this is needed.
Expand Down
3 changes: 0 additions & 3 deletions doc/src/todo.md

This file was deleted.

File renamed without changes.
77 changes: 59 additions & 18 deletions doc/src/tools/kani.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Kani is designed to prove safety properties in your code as well as
the absence of some forms of undefined behavior. It uses model checking under the hood to ensure that
Rust programs adhere to user specified properties.

You can find more information about how to install in [this section of the Kani book](https://model-checking.github.io/kani/install-guide.html).
You can find more information about how to install in [the installation section of the Kani book](https://model-checking.github.io/kani/install-guide.html).

## Usage

Expand All @@ -27,7 +27,8 @@ fn harness() {
let a = kani::any::<i32>();
let b = kani::any::<i32>();
let result = abs_diff(a, b);
kani::assert(result >= 0, "Result should always be more than 0");}
kani::assert(result >= 0, "Result should always be more than 0");
}
```

Running the command `cargo kani` in your cargo crate will give the result
Expand All @@ -46,29 +47,28 @@ Verification failed for - harness
Complete - 0 successfully verified harnesses, 1 failures, 1 total.
```

For a more detailed tutorial, you can refer to the [tutorial section of the Kani book](https://model-checking.github.io/kani/kani-tutorial.html).

## Using Kani to verify the Rust Standard Library

To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started.
Here is a short tutorial of how to use Kani to verify proofs for the standard library.

### Step 1
### Step 1 - Add some proofs to your copy of the model-checking std

Modify your local copy of the Rust Standard Library by writing proofs for the functions/methods that you want to verify.
Create a local copy of the [model-checking fork](https://github.com/model-checking/verify-rust-std) of the Rust Standard Library. The fork comes with Kani configured, so all you'll need to do is to call Kani's 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 `modifies`, `requires` and `ensures`) directly.

For example, insert this short blob into your copy of the library. 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);
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.

``` rust
#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
pub mod verify {
use crate::kani;

#[kani::proof]
pub fn harness() {
pub fn harness_introduction() {
kani::assert(true, "yay");
}

Expand All @@ -84,21 +84,24 @@ pub mod verify {
}
```

### Step 2
### Step 2 - Run the Kani verify-std subcommand

Run the following command in your local terminal:
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:

`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 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.
- `"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` 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 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
### Step 3 - Check verification result

After running the command, you can expect an output that looks like this:

Expand All @@ -112,6 +115,44 @@ Verification Time: 0.017101772s
Complete - 2 successfully verified harnesses, 0 failures, 2 total.
```

### Running on a specific harness

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
```

This gives you the verification result for just `harness_introduction` from the aforementioned blob.

```
RESULTS:
Check 1: verify::harness_introduction.assertion.1
- Status: SUCCESS
- Description: "yay"
- Location: library/core/src/lib.rs:479:9 in function verify::harness_introduction
SUMMARY:
** 0 of 1 failed
VERIFICATION:- SUCCESSFUL
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`.
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

You can find more information about how to install and how you can customize your use of Kani in the
Expand Down
1 change: 1 addition & 0 deletions library/alloc/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ edition = "2021"
[dependencies]
core = { path = "../core" }
compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] }
safety = { path = "../contracts/safety" }

[dev-dependencies]
rand = { version = "0.8.5", default-features = false, features = ["alloc"] }
Expand Down
1 change: 1 addition & 0 deletions library/alloc/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@
//
// Library features:
// tidy-alphabetical-start
#![cfg_attr(kani, feature(kani))]
#![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))]
#![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))]
#![feature(alloc_layout_extra)]
Expand Down
24 changes: 20 additions & 4 deletions library/contracts/safety/src/kani.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use proc_macro::{TokenStream};
use quote::{quote, format_ident};
use syn::{ItemFn, parse_macro_input};
use proc_macro::TokenStream;
use quote::{format_ident, quote};
use syn::{parse_macro_input, ItemFn, Stmt};

pub(crate) fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
rewrite_attr(attr, item, "requires")
Expand All @@ -10,12 +10,28 @@ pub(crate) fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
rewrite_attr(attr, item, "ensures")
}

pub(crate) fn loop_invariant(attr: TokenStream, stmt: TokenStream) -> TokenStream {
rewrite_stmt_attr(attr, stmt, "loop_invariant")
}

fn rewrite_stmt_attr(attr: TokenStream, stmt_stream: TokenStream, name: &str) -> TokenStream {
let args = proc_macro2::TokenStream::from(attr);
let stmt = parse_macro_input!(stmt_stream as Stmt);
let attribute = format_ident!("{}", name);
quote!(
#[kani_core::#attribute(#args)]
#stmt
)
.into()
}

fn rewrite_attr(attr: TokenStream, item: TokenStream, name: &str) -> TokenStream {
let args = proc_macro2::TokenStream::from(attr);
let fn_item = parse_macro_input!(item as ItemFn);
let attribute = format_ident!("{}", name);
quote!(
#[kani_core::#attribute(#args)]
#fn_item
).into()
)
.into()
}
Loading

0 comments on commit cc84fc7

Please sign in to comment.