Skip to content

Commit

Permalink
update RFC with implementation
Browse files Browse the repository at this point in the history
  • Loading branch information
@carolynzech
carolynzech committed Sep 16, 2024
1 parent b1c5a9e commit ced1dab
Showing 1 changed file with 145 additions and 45 deletions.
190 changes: 145 additions & 45 deletions rfc/src/rfcs/0013-list.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
- **Feature Request Issue:** [#2573](https://github.com/model-checking/kani/issues/2573), [#1612](https://github.com/model-checking/kani/issues/1612)
- **RFC PR:** #3463
- **Status:** Under Review
- **Version:** 1
- **Version:** 2

-------------------

Expand All @@ -20,53 +20,53 @@ This feature will not cause any regressions for exisiting users.

## User Experience

Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand will take the option `--message-format=[pretty|json]`, which changes the output format. The default is `pretty`, which prints to the terminal. The `json` option creates and writes to a JSON file instead.
Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand takes two options:
- `--message-format=[pretty|json]`: change the output format. The default is `pretty`, which prints to the terminal. The `json` option creates and writes to a JSON file instead.
- `--std`: Include if we are running on the standard library. This option is only available for `kani list` (not `cargo kani list`), which mirrors the verification workflow for the standard library.

This subcommand will not fail. In the case that it does not find any harnesses or contracts, it will print a message informing the user of that fact.
This subcommand does not fail. In the case that it does not find any harnesses or contracts, it prints a message informing the user of that fact.

### Pretty Format

The default format, `pretty`, will print the harnesses and contracts in a project, along with the total counts of each.
The default format, `pretty`, prints a "Contracts" table and a "Standard Harnesses" list.
Each row of the "Contracts" table consists of a function, the number of contracts it has, and its contract harnesses.
A function is listed if it has contracts or it is the target of contract harness(es).

For example:

```
Kani Rust Verifier 0.54.0 (standalone)
Standard Harnesses:
- example::verify::check_new
- example::verify::check_modify
Contract Harnesses:
- example::verify::check_foo_u32
- example::verify::check_foo_u64
- example::verify::check_func
- example::verify::check_bar
Contracts:
|--------------------------|-----------------------------------------------|
| Function | Contract Harnesses |
|--------------------------|-----------------------------------------------|
| example::impl::func | example::verify::check_func |
|--------------------------|-----------------------------------------------|
| example::impl::bar | example::verify::check_bar |
|--------------------------|-----------------------------------------------|
| example::impl::foo | example::verify::check_foo_u32, |
| | example::verify::check_foo_u64 |
|--------------------------|-----------------------------------------------|
| example::prep::parse | NONE |
|--------------------------|-----------------------------------------------|
Totals:
- Standard Harnesses: 2
- Contract Harnesses: 4
- Functions with Contracts: 4
- Contracts: 10
Each function in the table below either has contracts
or is the target of a contract harness (#[kani::proof_for_contract]).
|-------|-------------------------|----------------|--------------------|
| | Function | # of Contracts | Contract Harnesses |
|-------|-------------------------|----------------|--------------------|
| | example::impl::bar | 4 | check_bar |
|-------|-------------------------|----------------|--------------------|
| | example::impl::baz | 0 | check_baz |
|-------|-------------------------|----------------|--------------------|
| | example::impl::foo | 2 | check_foo_u32 |
| | | | check_foo_u64 |
|-------|-------------------------|----------------|--------------------|
| | example::impl::func | 1 | check_func |
|-------|-------------------------|----------------|--------------------|
| | example::prep::parse | 1 | NONE |
|-------|-------------------------|----------------|--------------------|
| Total | 5 | 8 | 5 |
|-------|-------------------------|----------------|--------------------|
Standard Harnesses (#[kani::proof]):
1. example::verify::check_new
2. example::verify::check_modify
```

A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `#[proof_for_contract]` harness.

All sections will be present in the output, regardless of the result. If a list is empty, Kani will output a `NONE` string.
All sections will be present in the output, regardless of the result.
If there are no harnesses for a function under contract, Kani inserts `NONE` in the "Contract Harnesses" row.
If the "Contracts" section is empty, Kani prints a message that "No contracts or contract harnesses were found."
If the "Standard Harnesses" section is empty, Kani prints a message that "No standard harnesses were found."

### JSON Format

Expand Down Expand Up @@ -96,6 +96,7 @@ For example:
file: /Users/johnsmith/example/kani_contract_proofs.rs
harnesses: [
example::verify::check_bar,
example::verify::check_baz,
example::verify::check_foo_u32,
example::verify::check_foo_u64,
example::verify::check_func
Expand All @@ -104,34 +105,44 @@ For example:
],
contracts: [
{
function: example::impl::func
function: example::impl::bar
total_contracts: 4
file: /Users/johnsmith/example/impl.rs
harnesses: [example::verify::check_func]
harnesses: [example::verify::check_bar]
},
{
function: example::impl::bar
function: example::impl::baz
total_contracts: 0
file: /Users/johnsmith/example/impl.rs
harnesses: [example::verify::check_bar]
harnesses: [example::verify::check_baz]
},
{
function: example::impl::foo
total_contracts: 2
file: /Users/johnsmith/example/impl.rs
harnesses: [
example::verify::check_foo_u32,
example::verify::check_foo_u64
]
},
{
function: example::impl::func
total_contracts: 1
file: /Users/johnsmith/example/impl.rs
harnesses: [example::verify::check_func]
},
{
function: example::prep::parse
total_contracts: 1
file: /Users/johnsmith/example/prep.rs
harnesses: []
}
],
totals: {
standard-harnesses: 2,
contract-harnesses: 4,
functions-with-contracts: 4,
contracts: 10,
contract-harnesses: 5,
functions-with-contracts: 5,
contracts: 8,
}
}
```
Expand All @@ -141,9 +152,98 @@ If there is no result for a given field (e.g., there are no contracts), Kani wil

## Software Design

We will add a new subcommand to `kani-driver`.
### Metdata Changes
We introduce a new `ContractedFunction` struct to `kani_metadata`:
```rust
pub struct ContractedFunction {
/// The fully qualified name the user gave to the function (i.e. includes the module path).
pub function: String,
/// The (currently full-) path to the file this function was declared within.
pub file: String,
/// The number of contracts applied to this function
pub total_contracts: usize,
/// The pretty names of the proof harnesses (`#[kani::proof_for_contract]`) for this function
pub harnesses: Vec<String>,
}
```
We extend `KaniMetadata` and `CodegenUnits` with new `contracted_functions: Vec<ContractedFunction>` fields.

### Compiler Changes

This subcommand is concerned with two fields of `KaniMetadata`: `proof_harnesses` and `contracted_functions`.
In `codegen_crate()`, `kani-compiler` will check if we are running the list subcommand, and, if so, it constructs a new `CodegenUnits` object.
The `CodegenUnits` constructor handles initializing the `proof_harnesses` field for us.
We add new functionality to populate the `contracted_functions` field, which we explain in two parts:

#### Part 1: Map Functions to Harnesses

First, we iterate through each local item in the crate and construct a map of functions to contract harnesses.
The keys in this map are functions that either 1) have contracts or 2) are targets of contract harnesses.
These are not necessarily identical sets; functions under contract may not have harnesses, and targets of contract harnesses may not have contracts.

Observe that we iterate through each local item in the crate (`stable_mir::CrateItem`), not each local *instance* (`stable_mir::Instance`).
This is so that we can include generic functions with contracts in the output.
`Instances` are monomorphized.
When we're verifying a contract harness, this monomorphization assumption is fine; if the harness calls the function under contract, a monomorphized version of the function must exist.
However, if we are just trying to list metadata, we cannot rely on this assumption that the function under contract gets called, and therefore cannot assume that a monomorphized version of the generic function exists.
For example, imagine running `kani list` on a file with only these contents:
```rust
#[kani::requires(true)]
fn foo<T>(x: T) -> T { x }
```
Kani should be able to find `foo` and report it has a contract,
but we cannot construct a `stable_mir::Instance` from `foo` because it requires monomorphization.

#### Part 2: Count Contracts
For each function in the map from Part 1, we count its contracts, then construct a `ContractedFunction` object for it.

Since we are counting the contracts at the MIR level, we work with the expanded version of the contract attribute macros.
We locate the body of the `kanitool::checked_with` closure, then count the number of `kani::assume()` and `kani::assert()` calls.
For example, given the following code (example taken from `kani_macros` contracts documentation):

```rust
#[kani::requires(divisor != 0)]
#[kani::ensures(|result : &u32| *result <= dividend)]
fn div(dividend: u32, divisor: u32) -> u32 {
dividend / divisor
}
```

The generated `check` closure is:

```rust
let mut __kani_check_div =
|| -> u32
{
kani::assume(divisor != 0);
let _wrapper_arg = ();
#[kanitool::is_contract_generated(wrapper)]
#[allow(dead_code, unused_variables, unused_mut)]
let mut __kani_modifies_div =
|_wrapper_arg| -> u32 { dividend / divisor };
let result_kani_internal: u32 =
__kani_modifies_div(_wrapper_arg);
kani::assert(kani::internal::apply_closure(|result: &u32|
*result <= dividend, &result_kani_internal),
"|result : &u32| *result <= dividend");
result_kani_internal
};
;
```

Observe that there is one `kani::assume()` call for the `requires` contract and one `kani::assert()`
call for the `ensures` contract, so we can obtain the total number of contracts by counting these calls.

Once these parts are complete, `CodegenUnits` contains all of the required metadata.
We use an existing method (`CodegenUnits::write_metadata`) to write this metadata to a file.

*We will update this section once the UX is finalized*.
### Driver Changes
We add a new subcommand to `kani-driver`.
This subcommand exists for both `cargo kani` and `kani` invocations.
The driver constructs a `Project` representing the input.
(For `kani` invocations, the driver either constructs a `standalone_project` or a `std_project` depending on whether the use passed the `--std` flag).
The `Project` is populated with `metadata: Vec<KaniMetadata>` from `kani-compiler`.
We iterate through this metadata to print a table with the results or output a JSON file, depending on the user-specified `format` argument.

## Rationale and alternatives

Expand All @@ -164,7 +264,7 @@ If we do not implement this feature, users will have to obtain this metadata thr

1. Do we want to include more contracts information? We could print more granular information about contracts, e.g., the text of the contracts, the number of `requires`, `ensures`, or `modifies` contracts, or the locations of the contracts.
2. More generally, we could introduce additional options that collect information about other Kani attributes (e.g., stubs). The default would be to leave them out, but this way a user could get more verbose output if they so choose.
3. Do we want to add a filtering option? For instance, `--harnesses <pattern>` and `--contracts <pattern>`, where `pattern` corresponds to a Rust-style path. For example, `kani list --harnesses "my_crate::my_module::*"` would include all harnesses with that path prefix, while `kani list --contracts "my_crate::my_module::*"` would include all functions under contract with that path prefix.
3. Do we want to add a filtering option? For instance, `--harnesses <pattern>` and `--contracts <pattern>`, where `pattern` corresponds to a Rust-style path. For example, `kani list --harnesses "my_crate::my_module::*"` would include all harnesses with that path prefix, while `kani list --contracts "my_crate::my_module::*"` would include all functions under contract with that path prefix. (If we do this work, we could use it to improve our `--harness` [pattern handling for verification](https://github.com/model-checking/kani/blob/main/kani-driver/src/metadata.rs#L187-L189)).

## Out of scope / Future Improvements

Expand Down

0 comments on commit ced1dab

Please sign in to comment.