Document not found (404)
+This URL is invalid, sorry. Please use the navigation bar or search to continue.
+ +diff --git a/.nojekyll b/.nojekyll new file mode 100644 index 000000000000..f17311098f54 --- /dev/null +++ b/.nojekyll @@ -0,0 +1 @@ +This file makes sure that Github Pages doesn't process mdBook's output. diff --git a/404.html b/404.html new file mode 100644 index 000000000000..b233fd9fa8bd --- /dev/null +++ b/404.html @@ -0,0 +1,170 @@ + + +
+ + +This URL is invalid, sorry. Please use the navigation bar or search to continue.
+ +You may be interested in applying Kani if you're in this situation:
+++If you haven't already, we also recommend techniques like property testing and fuzzing (e.g. with
+bolero
). +These yield good results, are very cheap to apply, and are often easy to adopt and debug.
In this section, we explain how Kani compares with other tools +and suggest where to start applying Kani in real code.
+ +benchcomp
command linebenchcomp
is a single command that runs benchmarks, parses their results, combines these results, and emits visualizations.
+benchcomp
also provides subcommands to run these steps individually.
+Most users will want to invoke benchcomp
in one of two ways:
benchcomp
without any subcommands, which runs the entire performance comparison process as depicted belowbenchcomp visualize
, which runs the visualization step on the results of a previous benchmark run without actually re-running the benchmarks.
+This is useful when tweaking the parameters of a visualization, for example changing the threshold of what is considered to be a regression.The subcommands run
and collate
are also available.
+The diagram below depicts benchcomp
's order of operation.
Running benchcomp
invokes run
, collate
, and visualize
behind the scenes.
+If you have previously run benchcomp
, then running benchcomp visualize
will emit the visualizations in the config file using the previous result.yaml
.
In the diagram above, two different suites (1 and 2) are both run using two variants---combinations of command, working directory, and environment variables.
+Benchmark suite 2 requires a totally different command line to suite 1---for example, suite_1
might contain Kani harnesses invoked through cargo kani
, while suite_2
might contain CBMC harnesses invoked through run_cbmc_proofs.py
.
+Users would therefore define different variants (c
and d
) for invoking suite_2
, and also specify a different parser to parse the results.
+No matter how different the benchmark suites are, the collate
stage combines their results so that they can later be compared.
Users must specify the actual suites to run, the parsers used to collect their results, and the visualizations to emit in a file called benchcomp.yaml
or a file passed to the -c/--config
flag.
+The next section describes the schema for this configuration file.
+A run similar to the diagram above might be achieved using the following configuration file:
# Compare a range of Kani and CBMC benchmarks when
+# using Cadical versus the default SAT solver
+
+variants:
+ variant_a:
+ config:
+ directory: kani_benchmarks
+ command_line: scripts/kani-perf.sh
+ env: {}
+
+ variant_b:
+ config:
+ directory: kani_benchmarks
+ command_line: scripts/kani-perf.sh
+ # This variant uses a hypothetical environment variable that
+ # forces Kani to use the cadical SAT solver
+ env:
+ KANI_SOLVER: cadical
+
+ variant_c:
+ config:
+ directory: cbmc_benchmarks
+ command_line: run_cbmc_proofs.py
+ env: {}
+
+ variant_d:
+ config:
+ directory: cbmc_benchmarks
+ command_line: run_cbmc_proofs.py
+ env:
+ EXTERNAL_SAT_SOLVER: cadical
+
+run:
+ suites:
+ suite_1:
+ parser:
+ module: kani_perf
+ variants: [variant_a, variant_b]
+
+ suite_2:
+ parser:
+ module: cbmc_litani_parser
+ variants: [variant_c, variant_d]
+
+visualize:
+ - type: dump_graph
+ out_file: graph.svg
+
+ - type: dump_markdown_results_table
+ out_file: summary.md
+ extra_columns: []
+
+ - type: error_on_regression
+ variant_pairs:
+ - [variant_a, variant_b]
+ - [variant_c, variant_d]
+
+
+ benchcomp
configuration filebenchcomp
's operation is controlled through a YAML file---benchcomp.yaml
by default or a file passed to the -c/--config
option.
+This page lists the different visualizations that are available.
A variant is a single invocation of a benchmark suite. Benchcomp runs several
+variants, so that their performance can be compared later. A variant consists of
+a command-line argument, working directory, and environment. Benchcomp invokes
+the command using the operating system environment, updated with the keys and
+values in env
. If any values in env
contain strings of the form ${var}
,
+Benchcomp expands them to the value of the environment variable $var
.
variants:
+ variant_1:
+ config:
+ command_line: echo "Hello, world"
+ directory: /tmp
+ env:
+ PATH: /my/local/directory:${PATH}
+
+After benchcomp has finished parsing the results, it writes the results to results.yaml
by default.
+Before visualizing the results (see below), benchcomp can filter the results by piping them into an external program.
To filter results before visualizing them, add filters
to the configuration file.
filters:
+ - command_line: ./scripts/remove-redundant-results.py
+ - command_line: cat
+
+The value of filters
is a list of dicts.
+Currently the only legal key for each of the dicts is command_line
.
+Benchcomp invokes each command_line
in order, passing the results as a JSON file on stdin, and interprets the stdout as a YAML-formatted modified set of results.
+Filter scripts can emit either YAML (which might be more readable while developing the script), or JSON (which benchcomp will parse as a subset of YAML).
The following visualizations are available; these can be added to the visualize
list of benchcomp.yaml
.
Detailed documentation for these visualizations follows.
+Scatterplot configuration options
+Print Markdown-formatted tables displaying benchmark results
+For each metric, this visualization prints out a table of benchmarks, +showing the value of the metric for each variant, combined with an optional +scatterplot.
+The 'out_file' key is mandatory; specify '-' to print to stdout.
+'extra_colums' can be an empty dict. The sample configuration below assumes +that each benchmark result has a 'success' and 'runtime' metric for both +variants, 'variant_1' and 'variant_2'. It adds a 'ratio' column to the table +for the 'runtime' metric, and a 'change' column to the table for the +'success' metric. The 'text' lambda is called once for each benchmark. The +'text' lambda accepts a single argument---a dict---that maps variant +names to the value of that variant for a particular metric. The lambda +returns a string that is rendered in the benchmark's row in the new column. +This allows you to emit arbitrary text or markdown formatting in response to +particular combinations of values for different variants, such as +regressions or performance improvements.
+'scatterplot' takes the values 'off' (default), 'linear' (linearly scaled +axes), or 'log' (logarithmically scaled axes).
+Sample configuration:
+visualize:
+- type: dump_markdown_results_table
+ out_file: "-"
+ scatterplot: linear
+ extra_columns:
+ runtime:
+ - column_name: ratio
+ text: >
+ lambda b: str(b["variant_2"]/b["variant_1"])
+ if b["variant_2"] < (1.5 * b["variant_1"])
+ else "**" + str(b["variant_2"]/b["variant_1"]) + "**"
+ success:
+ - column_name: change
+ text: >
+ lambda b: "" if b["variant_2"] == b["variant_1"]
+ else "newly passing" if b["variant_2"]
+ else "regressed"
+
+Example output:
+## runtime
+
+| Benchmark | variant_1 | variant_2 | ratio |
+| --- | --- | --- | --- |
+| bench_1 | 5 | 10 | **2.0** |
+| bench_2 | 10 | 5 | 0.5 |
+
+## success
+
+| Benchmark | variant_1 | variant_2 | change |
+| --- | --- | --- | --- |
+| bench_1 | True | True | |
+| bench_2 | True | False | regressed |
+| bench_3 | False | True | newly passing |
+
+Print the YAML-formatted results to a file.
+The 'out_file' key is mandatory; specify '-' to print to stdout.
+Sample configuration:
+visualize:
+- type: dump_yaml
+ out_file: '-'
+
+Terminate benchcomp with a return code of 1 if any benchmark regressed.
+This visualization checks whether any benchmark regressed from one variant +to another. Sample configuration:
+visualize:
+- type: error_on_regression
+ variant_pairs:
+ - [variant_1, variant_2]
+ - [variant_1, variant_3]
+ checks:
+ - metric: runtime
+ test: "lambda old, new: new / old > 1.1"
+ - metric: passed
+ test: "lambda old, new: False if not old else not new"
+
+This says to check whether any benchmark regressed when run under variant_2 +compared to variant_1. A benchmark is considered to have regressed if the +value of the 'runtime' metric under variant_2 is 10% higher than the value +under variant_1. Furthermore, the benchmark is also considered to have +regressed if it was previously passing, but is now failing. These same +checks are performed on all benchmarks run under variant_3 compared to +variant_1. If any of those lambda functions returns True, then benchcomp +will terminate with a return code of 1.
+Run an executable command, passing the performance metrics as JSON on stdin.
+This allows you to write your own visualization, which reads a result file +on stdin and does something with it, e.g. writing out a graph or other +output file.
+Sample configuration:
+visualize:
+- type: run_command
+ command: ./my_visualization.py
+
+
+ Benchcomp ships with built-in parsers that retrieve the results of a benchmark suite after the run has completed. +You can also create your own parser, either to run locally or to check into the Kani codebase.
+You specify which parser should run for each benchmark suite in benchcomp.yaml
.
+For example, if you're running the kani performance suite, you would use the built-in kani_perf
parser to parse the results:
suites:
+ my_benchmark_suite:
+ variants: [variant_1, variant_2]
+ parser:
+ module: kani_perf
+
+A parser is a program that benchcomp runs inside the root directory of a benchmark suite, after the suite run has completed.
+The parser should retrieve the results of the run (by parsing output files etc.) and print the results out as a YAML document.
+You can use your executable parser by specifying the command
key rather than the module
key in your benchconf.yaml
file:
suites:
+ my_benchmark_suite:
+ variants: [variant_1, variant_2]
+ parser:
+ command: ./my-cool-parser.sh
+
+The kani_perf
parser mentioned above, in tools/benchcomp/benchcomp/parsers/kani_perf.py
, is a good starting point for writing a custom parser, as it also works as a standalone executable.
+Here is an example output from an executable parser:
metrics:
+ runtime: {}
+ success: {}
+ errors: {}
+benchmarks:
+ bench_1:
+ metrics:
+ runtime: 32
+ success: true
+ errors: []
+ bench_2:
+ metrics:
+ runtime: 0
+ success: false
+ errors: ["compilation failed"]
+
+The above format is different from the final result.yaml
file that benchcomp writes, because the above file represents the output of running a single benchmark suite using a single variant.
+Your parser will run once for each variant, and benchcomp combines the dictionaries into the final result.yaml
file.
To turn your executable parser into one that benchcomp can invoke as a module, ensure that it has a main(working_directory)
method that returns a dict (the same dict that it would print out as a YAML file to stdout).
+Save the file in tools/benchcomp/benchcomp/parsers
using python module naming conventions (filename should be an identifier and end in .py
).
++If you were able to install Kani normally, you do not need to build Kani from source. +You probably want to proceed to the Kani tutorial.
+
In general, the following dependencies are required to build Kani from source.
+++ +NOTE: These dependencies may be installed by running the scripts shown +below and don't need to be manually installed.
+
Kani has been tested in Ubuntu and macOS platforms.
+Support is available for Ubuntu 20.04, 22.04, and 24.04. +The simplest way to install dependencies (especially if you're using a fresh VM) +is following our CI scripts:
+# git clone git@github.com:model-checking/kani.git
+git clone https://github.com/model-checking/kani.git
+cd kani
+git submodule update --init
+./scripts/setup/ubuntu/install_deps.sh
+# If you haven't already (or from https://rustup.rs/):
+./scripts/setup/install_rustup.sh
+source $HOME/.cargo/env
+
+Support is available for macOS 11. You need to have Homebrew installed already.
+# git clone git@github.com:model-checking/kani.git
+git clone https://github.com/model-checking/kani.git
+cd kani
+git submodule update --init
+./scripts/setup/macos/install_deps.sh
+# If you haven't already (or from https://rustup.rs/):
+./scripts/setup/install_rustup.sh
+source $HOME/.cargo/env
+
+Build the Kani package using:
+cargo build-dev -- --release
+
+to compile with optimizations turned on or using:
+cargo build-dev
+
+to compile in debug/development mode.
+Then, optionally, run the regression tests:
+./scripts/kani-regression.sh
+
+This script has a lot of noisy output, but on a successful run you'll see at the end of the execution:
+All Kani regression tests completed successfully.
+
+To use a locally-built Kani from anywhere, add the Kani scripts to your path:
+export PATH=$(pwd)/scripts:$PATH
+
+If you're learning Kani for the first time, you may be interested in our tutorial.
+ +This section describes how to access more advanced CBMC options from Kani.
+Kani is able to handle common CBMC arguments as if they were its own (e.g.,
+--default-unwind <n>
), but sometimes it may be necessary to use CBMC arguments which
+are not handled by Kani.
To pass additional arguments for CBMC, you pass --cbmc-args
to Kani. Note that
+this "switches modes" from Kani arguments to CBMC arguments: Any arguments that
+appear after --cbmc-args
are considered to be CBMC arguments, so all Kani
+arguments must be placed before it.
Thus, the command line format to invoke cargo kani
with CBMC arguments is:
cargo kani [<kani-args>]* --cbmc-args [<cbmc-args>]*
+
+++NOTE: In cases where CBMC is not expected to emit a verification output, +you have to use Kani's argument
+--output-format old
to turn off the +post-processing of output from CBMC.
Setting --default-unwind <n>
affects every loop in a harness.
+Once you know a particular loop is causing trouble, sometimes it can be helpful to provide a specific bound for it.
In the general case, specifying just the highest bound globally for all loops +shouldn't cause any problems, except that the solver may take more time because +all loops will be unwound to the specified bound.
+In situations where you need to optimize for the solver, individual bounds for
+each loop can be provided on the command line. To do so, we first need to know
+the labels assigned to each loop with the CBMC argument --show-loops
:
# kani src/lib.rs --output-format old --cbmc-args --show-loops
+[...]
+Loop _RNvCs6JP7pnlEvdt_3lib17initialize_prefix.0:
+ file ./src/lib.rs line 11 column 5 function initialize_prefix
+
+Loop _RNvMs8_NtNtCswN0xKFrR8r_4core3ops5rangeINtB5_14RangeInclusivejE8is_emptyCs6JP7pnlEvdt_3lib.0:
+ file $RUST/library/core/src/ops/range.rs line 540 column 9 function std::ops::RangeInclusive::<Idx>::is_empty
+
+Loop gen-repeat<[u8; 10]::16806744624734428132>.0:
+
+This command shows us the labels of the loops involved. Note that, as mentioned
+in CBMC arguments, we need to use --output-format old
to
+avoid post-processing the output from CBMC.
++NOTE: At the moment, these labels are constructed using the mangled name +of the function and an index. Mangled names are likely to change across +different versions, so this method is highly unstable.
+
Then, we can use the CBMC argument --unwindset label_1:bound_1,label_2:bound_2,...
to specify an individual bound for each
+loop as follows:
kani src/lib.rs --cbmc-args --unwindset _RNvCs6JP7pnlEvdt_3lib17initialize_prefix.0:12
+
+
+ Development work in the Kani project depends on multiple tools. Regardless of +your familiarity with the project, the commands below may be useful for +development purposes.
+# Error "'rustc' panicked at 'failed to lookup `SourceFile` in new context'"
+# or similar error? Cleaning artifacts might help.
+# Otherwise, comment the line below.
+cargo clean
+cargo build-dev
+
+# Full regression suite
+./scripts/kani-regression.sh
+
+# Delete regression test caches (Linux)
+rm -r build/x86_64-unknown-linux-gnu/tests/
+
+# Delete regression test caches (macOS)
+rm -r build/x86_64-apple-darwin/tests/
+
+# Test suite run (we can only run one at a time)
+# cargo run -p compiletest -- --suite ${suite} --mode ${mode}
+cargo run -p compiletest -- --suite kani --mode kani
+
+# Build documentation
+cd docs
+./build-docs.sh
+
+These can help understand what Kani is generating or encountering on an example or test file:
+# Enable `debug!` macro logging output when running Kani:
+kani --debug file.rs
+
+# Use KANI_LOG for a finer grain control of the source and verbosity of logs.
+# E.g.: The command below will print all logs from the kani_middle module.
+KANI_LOG="kani_compiler::kani_middle=trace" kani file.rs
+
+# Keep CBMC Symbol Table and Goto-C output (.json and .goto)
+kani --keep-temps file.rs
+
+# Generate "C code" from CBMC IR (.c)
+kani --gen-c file.rs
+
+# Generate a ${INPUT}.kani.mir file with a human friendly MIR dump
+# for all items that are compiled to the respective goto-program.
+RUSTFLAGS="--emit mir" kani ${INPUT}.rs
+
+The KANI_REACH_DEBUG
environment variable can be used to debug Kani's reachability analysis.
+If defined, Kani will generate a DOT graph ${INPUT}.dot
with the graph traversed during reachability analysis.
+If defined and not empty, the graph will be filtered to end at functions that contains the substring
+from KANI_REACH_DEBUG
.
Note that this will only work on debug builds.
+# Generate a DOT graph ${INPUT}.dot with the graph traversed during reachability analysis
+KANI_REACH_DEBUG= kani ${INPUT}.rs
+
+# Generate a DOT graph ${INPUT}.dot with the sub-graph traversed during the reachability analysis
+# that connect to the given target.
+KANI_REACH_DEBUG="${TARGET_ITEM}" kani ${INPUT}.rs
+
+# See CBMC IR from a C file:
+goto-cc file.c -o file.out
+goto-instrument --print-internal-representation file.out
+# or (for json symbol table)
+cbmc --show-symbol-table --json-ui file.out
+# or (an alternative concise format)
+cbmc --show-goto-functions file.out
+
+# Recover C from goto-c binary
+goto-instrument --dump-c file.out > file.gen.c
+
+The Kani project follows the squash and merge option for pull request merges. +As a result:
+But the main commit message body is editable at merge time, so you don't have to worry about "typo fix" messages because these can be removed before merging.
+# Set up your git fork
+git remote add fork git@github.com:${USER}/kani.git
+
+# Reset everything. Don't have any uncommitted changes!
+git clean -xffd
+git submodule foreach --recursive git clean -xffd
+git submodule update --init
+
+# Need to update local branch (e.g. for an open pull request?)
+git fetch origin
+git merge origin/main
+# Or rebase, but that requires a force push,
+# and because we squash and merge, an extra merge commit in a PR doesn't hurt.
+
+# Checkout a pull request locally without the github cli
+git fetch origin pull/$ID/head:pr/$ID
+git switch pr/$ID
+
+# Push to someone else's pull request
+git origin add $USER $GIR_URL_FOR_THAT_USER
+git push $USER $LOCAL_BRANCH:$THEIR_PR_BRANCH_NAME
+
+# Search only git-tracked files
+git grep codegen_panic
+
+# Accidentally commit to main?
+# "Move" commit to a branch:
+git checkout -b my_branch
+# Fix main:
+git branch --force main origin/main
+
+
+ We automate most of our formatting preferences. Our CI will run format checkers for PRs and pushes. +These checks are required for merging any PR.
+For Rust, we use rustfmt
+which is configured via the rustfmt.toml file.
+We are also in the process of enabling clippy
.
+Because of that, we still have a couple of lints disabled (see .cargo/config for the updated list).
We also have a bit of C and Python code in our repository.
+For C we use clang-format
and for Python scripts we use autopep8
.
+See .clang-format
+and pyproject.toml
+for their configuration.
We recognize that in some cases, the formatting and lints automation may not be applicable to a specific code.
+In those cases, we usually prefer explicitly allowing exceptions by locally disabling the check.
+E.g., use #[allow]
annotation instead of disabling a link on a crate or project level.
All source code files begin with a copyright and license notice. If this is a new file, please add the following notice:
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+When modifying a file from another project, please keep their headers as is and append the following notice after them:
+// ... existing licensing headers ...
+
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+Note: The comment escape characters will depend on the type of file you are working with. E.g.: For rust start the
+header with //
, but for python start with #
.
We also have automated checks for the copyright notice. +There are a few file types where this rule doesn't apply. +You can see that list in the copyright-exclude file.
+We are developing Kani to provide assurance that critical Rust components are verifiably free of certain classes of +security and correctness issues. +Thus, it is critical that we provide a verification tool that is sound. +For the class of errors that Kani can verify, we should not produce a "No Error" result if there was in fact an +error in the code being verified, i.e., it has no +"False Negatives".
+Because of that, we bias on the side of correctness. +Any incorrect modeling +that may trigger an unsound analysis that cannot be fixed in the short term should be mitigated. +Here are a few ways how we do that.
+Make sure to add user-friendly errors for constructs that we can't handle. +For example, Kani cannot handle the panic unwind strategy, and it will fail compilation if the crate uses this +configuration.
+In general, it's preferred that error messages follow these guidelines used for rustc
development.
+If the errors are being emitted from kani-compiler
, you should use the compiler error message utilities (e.g., the Session::span_err
method). However, if the
+errors are being emitted from kani-driver
, you should use the functions provided in the util
module in kani-driver
.
Even though this doesn't provide users the best experience, you are encouraged to add checks in the compiler for any
+assumptions you make during development.
+Those checks can be on the form of assert!()
or unreachable!()
+statement.
+Please provide a meaningful message to help user understand why something failed, and try to explain, at least with
+a comment, why this is the case.
We don't formally use any specific formal representation of function contract, +but whenever possible we do instrument the code with assertions that may represent the function pre- and +post-conditions to ensure we are modeling the user code correctly.
+In cases where Kani fails to model a certain instruction or local construct that doesn't have a global effect,
+we encode this failure as a verification error.
+I.e., we generate an assertion failure instead of the construct we are modeling using
+codegen_unimplemented()
,
+which blocks the execution whenever this construct is reached.
This will allow users to verify their crate successfully as long as
+that construct is not reachable in any harness. If a harness has at least one possible execution path that reaches
+such construct, Kani will fail the verification, and it will mark all checks, other than failed checks, with
+UNDETERMINED
status.
It is OK to add "TODO" comments as long as they don't compromise user experience or the tool correctness. +When doing so, please create an issue that captures the task. +Add details about the task at hand including any impact to the user. +Finally, add the link to the issue that captures the "TODO" task as part of your comment.
+E.g.:
+// TODO: This function assumes type cannot be ZST. Check if that's always the case.
+// https://github.com/model-checking/kani/issues/XXXX
+assert!(!typ.is_zst(), "Unexpected ZST type");
+
+We aim at writing code that is performant but also readable and easy to maintain. +Avoid compromising the code quality if the performance gain is not significant.
+Here are few tips that can help the readability of your code:
+This module introduces the Arbitrary
trait as well as implementation for
+primitive types and other std containers.
Redirecting to ../../kani/enum.AllocationStatus.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/arbitrary_ptr/fn.pointer_generator.html b/crates/doc/kani/arbitrary_ptr/fn.pointer_generator.html new file mode 100644 index 000000000000..ab6a6cf0c987 --- /dev/null +++ b/crates/doc/kani/arbitrary_ptr/fn.pointer_generator.html @@ -0,0 +1,11 @@ + + + + +Redirecting to ../../kani/fn.pointer_generator.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/arbitrary_ptr/struct.ArbitraryPointer.html b/crates/doc/kani/arbitrary_ptr/struct.ArbitraryPointer.html new file mode 100644 index 000000000000..656534c5c522 --- /dev/null +++ b/crates/doc/kani/arbitrary_ptr/struct.ArbitraryPointer.html @@ -0,0 +1,11 @@ + + + + +Redirecting to ../../kani/struct.ArbitraryPointer.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/arbitrary_ptr/struct.PointerGenerator.html b/crates/doc/kani/arbitrary_ptr/struct.PointerGenerator.html new file mode 100644 index 000000000000..edddd32c905f --- /dev/null +++ b/crates/doc/kani/arbitrary_ptr/struct.PointerGenerator.html @@ -0,0 +1,11 @@ + + + + +Redirecting to ../../kani/struct.PointerGenerator.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/attr.ensures.html b/crates/doc/kani/attr.ensures.html new file mode 100644 index 000000000000..8ae1bb99f607 --- /dev/null +++ b/crates/doc/kani/attr.ensures.html @@ -0,0 +1,13 @@ +#[ensures]
Add a postcondition to this function.
+This is part of the function contract API, for more general information see +the module-level documentation.
+The contents of the attribute is a closure that captures the input values to +the annotated function and the input to the function is the return value of +the function passed by reference. All Rust syntax is supported, even calling +other functions, but the computations must be side effect free, e.g. it +cannot perform I/O or use mutable memory.
+Kani requires each function that uses a contract (this attribute or
+requires
) to have at least one designated
+proof_for_contract
harness for checking the
+contract.
#[loop_invariant]
Add a loop invariant to this loop.
+The contents of the attribute is a condition that should be satisfied at the +beginning of every iteration of the loop. +All Rust syntax is supported, even calling other functions, but +the computations must be side effect free, e.g. it cannot perform I/O or use +mutable memory.
+#[modifies]
Declaration of an explicit write-set for the annotated function.
+This is part of the function contract API, for more general information see +the module-level documentation.
+The contents of the attribute is a series of comma-separated expressions referencing the
+arguments of the function. Each expression is expected to return a pointer type, i.e. *const T
,
+*mut T
, &T
or &mut T
. The pointed-to type must implement
+Arbitrary
.
All Rust syntax is supported, even calling other functions, but the computations must be side +effect free, e.g. it cannot perform I/O or use mutable memory.
+Kani requires each function that uses a contract to have at least one designated
+proof_for_contract
harness for checking the
+contract.
#[proof]
Marks a Kani proof harness
+For async harnesses, this will call block_on
to drive the future to completion (see its documentation for more information).
If you want to spawn tasks in an async harness, you have to pass a schedule to the #[kani::proof]
attribute,
+e.g. #[kani::proof(schedule = kani::RoundRobin::default())]
.
This will wrap the async function in a call to block_on_with_spawn
(see its documentation for more information).
#[proof_for_contract]
Designates this function as a harness to check a function contract.
+The argument to this macro is the relative path (e.g. foo
or
+super::some_mod::foo
or crate::SomeStruct::foo
) to the function, the
+contract of which should be checked.
This is part of the function contract API, for more general information see +the module-level documentation.
+#[recursion]
Specifies that a function contains recursion for contract instrumentation.**
+This attribute is only used for function-contract instrumentation. Kani uses
+this annotation to identify recursive functions and properly instantiate
+kani::any_modifies
to check such functions using induction.
#[requires]
Add a precondition to this function.
+This is part of the function contract API, for more general information see +the module-level documentation.
+The contents of the attribute is a condition over the input values to the +annotated function. All Rust syntax is supported, even calling other +functions, but the computations must be side effect free, e.g. it cannot +perform I/O or use mutable memory.
+Kani requires each function that uses a contract (this attribute or
+ensures
) to have at least one designated
+proof_for_contract
harness for checking the
+contract.
#[should_panic]
Specifies that a proof harness is expected to panic.**
+This attribute allows users to exercise negative verification.
+It’s analogous to how
+#[should_panic]
+allows users to exercise negative testing
+for Rust unit tests.
The #[kani::should_panic]
attribute verifies that there are one or more failed checks related to panics.
+At the moment, it’s not possible to pin it down to specific panics.
#[solver]
Select the SAT solver to use with CBMC for this harness
+The attribute #[kani::solver(arg)]
can only be used alongside #[kani::proof]
.
arg - name of solver, e.g. kissat
+#[stub]
Specify a function/method stub pair to use for proof harness
+The attribute #[kani::stub(original, replacement)]
can only be used alongside #[kani::proof]
.
original
- The function or method to replace, specified as a path.replacement
- The function or method to use as a replacement, specified as a path.#[stub_verified]
stub_verified(TARGET)
is a harness attribute (to be used on
+proof
or proof_for_contract
+function) that replaces all occurrences of TARGET
reachable from this
+harness with a stub generated from the contract on TARGET
.
The target of stub_verified
must have a contract. More information about
+how to specify a contract for your function can be found
+here.
You may use multiple stub_verified
attributes on a single harness.
This is part of the function contract API, for more general information see +the module-level documentation.
+#[unwind]
Set Loop unwind limit for proof harnesses
+The attribute #[kani::unwind(arg)]
can only be called alongside #[kani::proof]
.
+arg - Takes in a integer value (u32) that represents the unwind value for the harness.
#[ensures]
Add a postcondition to this function.
+This is part of the function contract API, for more general information see +the module-level documentation.
+The contents of the attribute is a closure that captures the input values to +the annotated function and the input to the function is the return value of +the function passed by reference. All Rust syntax is supported, even calling +other functions, but the computations must be side effect free, e.g. it +cannot perform I/O or use mutable memory.
+Kani requires each function that uses a contract (this attribute or
+requires
) to have at least one designated
+proof_for_contract
harness for checking the
+contract.
#[modifies]
Declaration of an explicit write-set for the annotated function.
+This is part of the function contract API, for more general information see +the module-level documentation.
+The contents of the attribute is a series of comma-separated expressions referencing the
+arguments of the function. Each expression is expected to return a pointer type, i.e. *const T
,
+*mut T
, &T
or &mut T
. The pointed-to type must implement
+Arbitrary
.
All Rust syntax is supported, even calling other functions, but the computations must be side +effect free, e.g. it cannot perform I/O or use mutable memory.
+Kani requires each function that uses a contract to have at least one designated
+proof_for_contract
harness for checking the
+contract.
#[proof_for_contract]
Designates this function as a harness to check a function contract.
+The argument to this macro is the relative path (e.g. foo
or
+super::some_mod::foo
or crate::SomeStruct::foo
) to the function, the
+contract of which should be checked.
This is part of the function contract API, for more general information see +the module-level documentation.
+#[requires]
Add a precondition to this function.
+This is part of the function contract API, for more general information see +the module-level documentation.
+The contents of the attribute is a condition over the input values to the +annotated function. All Rust syntax is supported, even calling other +functions, but the computations must be side effect free, e.g. it cannot +perform I/O or use mutable memory.
+Kani requires each function that uses a contract (this attribute or
+ensures
) to have at least one designated
+proof_for_contract
harness for checking the
+contract.
#[stub_verified]
stub_verified(TARGET)
is a harness attribute (to be used on
+proof
or proof_for_contract
+function) that replaces all occurrences of TARGET
reachable from this
+harness with a stub generated from the contract on TARGET
.
The target of stub_verified
must have a contract. More information about
+how to specify a contract for your function can be found
+here.
You may use multiple stub_verified
attributes on a single harness.
This is part of the function contract API, for more general information see +the module-level documentation.
+Kani implementation of function contracts.
+Function contracts are still under development. Using the APIs therefore
+requires the unstable -Zfunction-contracts
flag to be passed. You can join
+the discussion on contract design by reading our
+RFC
+and commenting on the tracking
+issue.
The function contract API is expressed as proc-macro attributes, and there +are two parts to it.
+requires
and ensures
.proof_for_contract
and
+stub_verified
.Let us explore using a workflow involving contracts on the example of a
+simple division function my_div
:
fn my_div(dividend: usize, divisor: usize) -> usize {
+ dividend / divisor
+}
With the contract specification attributes we can specify the behavior of
+this function declaratively. The requires
attribute
+allows us to declare constraints on what constitutes valid inputs to our
+function. In this case we would want to disallow a divisor that is 0
.
#[requires(divisor != 0)]
This is called a precondition, because it is enforced before (pre-) the
+function call. As you can see attribute has access to the functions
+arguments. The condition itself is just regular Rust code. You can use any
+Rust code, including calling functions and methods. However you may not
+perform I/O (like println!
) or mutate memory (like Vec::push
).
The ensures
attribute on the other hand lets us describe
+the output value in terms of the inputs. You may be as (im)precise as you
+like in the ensures
clause, depending on your needs. One
+approximation of the result of division for instance could be this:
#[ensures(|result : &usize| *result <= dividend)]
This is called a postcondition and it also has access to the arguments and
+is expressed in regular Rust code. The same restrictions apply as did for
+requires
. In addition to the postcondition is expressed
+as a closure where the value returned from the function is passed to this
+closure by reference.
You may combine as many requires
and
+ensures
attributes on a single function as you please.
+They all get enforced (as if their conditions were &&
ed together) and the
+order does not matter. In our example putting them together looks like this:
use kani::{requires, ensures};
+
+#[requires(divisor != 0)]
+#[ensures(|result : &usize| *result <= dividend)]
+fn my_div(dividend: usize, divisor: usize) -> usize {
+ dividend / divisor
+}
Once we are finished specifying our contract we can ask Kani to check it’s
+validity. For this we need to provide a proof harness that exercises the
+function. The harness is created like any other, e.g. as a test-like
+function with inputs and using kani::any
to create arbitrary values.
+However we do not need to add any assertions or assumptions about the
+inputs, Kani will use the pre- and postconditions we have specified for that
+and we use the proof_for_contract
attribute
+instead of proof
and provide it with the path to the
+function we want to check.
#[kani::proof_for_contract(my_div)]
+fn my_div_harness() {
+ my_div(kani::any(), kani::any());
+}
The harness is checked like any other by running cargo kani
and can be
+specifically selected with --harness my_div_harness
.
Once we have verified that our contract holds, we can use perhaps it’s +coolest feature: verified stubbing. This allows us to use the conditions of +the contract instead of it’s implementation. This can be very powerful for +expensive implementations (involving loops for instance).
+Verified stubbing is available to any harness via the
+stub_verified
harness attribute. We must provide
+the attribute with the path to the function to stub, but unlike with
+stub
we do not need to provide a function to replace with,
+the contract will be used automatically.
#[kani::proof]
+#[kani::stub_verified(my_div)]
+fn use_div() {
+ let v = kani::vec::any_vec::<char, 5>();
+ let some_idx = my_div(v.len() - 1, 3);
+ v[some_idx];
+}
In this example the contract is sufficient to prove that the element access +in the last line cannot be out-of-bounds.
+The basic two specification attributes available for describing
+function behavior are requires
for preconditions and
+ensures
for postconditions. Both admit arbitrary Rust
+expressions as their bodies which may also reference the function arguments
+but must not mutate memory or perform I/O. The postcondition may
+additionally reference the return value of the function as the variable
+result
.
In addition Kani provides the modifies
attribute. This
+works a bit different in that it does not contain conditions but a comma
+separated sequence of expressions that evaluate to pointers. This attribute
+constrains to which memory locations the function is allowed to write. Each
+expression can contain arbitrary Rust syntax, though it may not perform side
+effects and it is also currently unsound if the expression can panic. For more
+information see the write sets section.
During verified stubbing the return value of a function with a contract is
+replaced by a call to kani::any
. As such the return value must implement
+the kani::Arbitrary
trait.
In Kani, function contracts are optional. As such a function with at least
+one specification attribute is considered to “have a contract” and any
+absent specification type defaults to its most general interpretation
+(true
). All functions with not a single specification attribute are
+considered “not to have a contract” and are ineligible for use as the target
+of a proof_for_contract
of
+stub_verified
attribute.
Contract are used both to verify function behavior and to leverage the +verification result as a sound abstraction.
+Verifying function behavior currently requires the designation of at least
+one checking harness with the
+proof_for_contract
attribute. A harness may
+only have one proof_for_contract
attribute and it may not also have a
+proof
attribute.
The checking harness is expected to set up the arguments that foo
should
+be called with and initialized any static mut
globals that are reachable.
+All of these should be initialized to as general value as possible, usually
+achieved using kani::any
. The harness must call e.g. foo
at least once
+and if foo
has type parameters, only one instantiation of those parameters
+is admissible. Violating either results in a compile error.
If any inputs have special invariants you can use kani::assume
to
+enforce them but this may introduce unsoundness. In general all restrictions
+on input parameters should be part of the requires
+clause of the function contract.
Once the contract has been verified it may be used as a verified stub. For
+this the stub_verified
attribute is used.
+stub_verified
is a harness attribute, like
+unwind
, meaning it is used on functions that are
+annotated with proof
. It may also be used on a
+proof_for_contract
proof.
Unlike proof_for_contract
multiple stub_verified
attributes are allowed
+on the same proof harness though they must target different functions.
Function contracts by default use inductive verification to efficiently +verify recursive functions. In inductive verification a recursive function +is executed once and every recursive call instead uses the contract +replacement. In this way many recursive calls can be checked with a +single verification pass.
+The downside of inductive verification is that the return value of a
+contracted function must implement kani::Arbitrary
. Due to restrictions to
+code generation in proc macros, the contract macros cannot determine reliably
+in all cases whether a given function with a contract is recursive. As a
+result it conservatively sets up inductive verification for every function
+and requires the kani::Arbitrary
constraint for contract checks.
If you feel strongly about this issue you can join the discussion on issue +#2823 to enable +opt-out of inductive verification.
+The modifies
attribute is used to describe which
+locations in memory a function may assign to. The attribute contains a comma
+separated series of expressions that reference the function arguments.
+Syntactically any expression is permissible, though it may not perform side
+effects (I/O, mutation) or panic. As an example consider this super simple
+function:
#[kani::modifies(ptr, my_box.as_ref())]
+fn a_function(ptr: &mut u32, my_box: &mut Box<u32>) {
+ *ptr = 80;
+ *my_box.as_mut() = 90;
+}
Because the function performs an observable side-effect (setting both the
+value behind the pointer and the value pointed-to by the box) we need to
+provide a modifies
attribute. Otherwise Kani will reject a contract on
+this function.
An expression used in a modifies
clause must return a pointer to the
+location that you would like to allow to be modified. This can be any basic
+Rust pointer type (&T
, &mut T
, *const T
or *mut T
). In addition T
+must implement Arbitrary
. This is used to assign
+kani::any()
to the location when the function is used in a stub_verified
.
Additionally, an ensures clause is allowed to refer to the state of the function arguments before function execution and perform simple computations on them
+via an old
monad. Any instance of old(computation)
will evaluate the
+computation before the function is called. It is required that this computation
+is effect free and closed with respect to the function arguments.
For example, the following code passes kani tests:
+ +#[kani::modifies(a)]
+#[kani::ensures(|result| old(*a).wrapping_add(1) == *a)]
+#[kani::ensures(|result : &u32| old(*a).wrapping_add(1) == *result)]
+fn add1(a : &mut u32) -> u32 {
+ *a=a.wrapping_add(1);
+ *a
+}
Here, the value stored in a
is precomputed and remembered after the function
+is called, even though the contents of a
changed during the function execution.
stub_verified(TARGET)
is a harness attribute (to be used on
+proof
or proof_for_contract
+function) that replaces all occurrences of TARGET
reachable from this
+harness with a stub generated from the contract on TARGET
.#[derive(Arbitrary)]
+{
+ // Attributes available to this derive:
+ #[safety_constraint]
+}
+
Allow users to auto generate Arbitrary
implementations by using
+#[derive(Arbitrary)]
macro.
#[safety_constraint(...)]
attributeWhen using #[derive(Arbitrary)]
on a struct, the
+#[safety_constraint(<cond>)]
attribute can be added to either the struct
+or its fields (but not both) to indicate a type safety invariant condition
+<cond>
. Since kani::any()
is always expected to produce type-safe
+values, adding #[safety_constraint(...)]
to the struct or any of its
+fields will further constrain the objects generated with kani::any()
.
For example, the check_positive
harness in this code is expected to
+pass:
#[derive(kani::Arbitrary)]
+struct AlwaysPositive {
+ #[safety_constraint(*inner >= 0)]
+ inner: i32,
+}
+
+#[kani::proof]
+fn check_positive() {
+ let val: AlwaysPositive = kani::any();
+ assert!(val.inner >= 0);
+}
But using the #[safety_constraint(...)]
attribute can lead to vacuous
+results when the values are over-constrained. For example, in this code
+the check_positive
harness will pass too:
#[derive(kani::Arbitrary)]
+struct AlwaysPositive {
+ #[safety_constraint(*inner >= 0 && *inner < i32::MIN)]
+ inner: i32,
+}
+
+#[kani::proof]
+fn check_positive() {
+ let val: AlwaysPositive = kani::any();
+ assert!(val.inner >= 0);
+}
Unfortunately, we made a mistake when specifying the condition because
+*inner >= 0 && *inner < i32::MIN
is equivalent to false
. This results
+in the relevant assertion being unreachable:
Check 1: check_positive.assertion.1
+ - Status: UNREACHABLE
+ - Description: "assertion failed: val.inner >= 0"
+ - Location: src/main.rs:22:5 in function check_positive
As usual, we recommend users to defend against these behaviors by using
+kani::cover!(...)
checks and watching out for unreachable assertions in
+their project’s code.
#[safety_constraint(...)]
to the struct as opposed to its fieldsAs mentioned earlier, the #[safety_constraint(...)]
attribute can be added
+to either the struct or its fields, but not to both. Adding the
+#[safety_constraint(...)]
attribute to both the struct and its fields will
+result in an error.
In practice, only one type of specification is need. If the condition for
+the type safety invariant involves a relation between two or more struct
+fields, the struct-level attribute should be used. Otherwise, using the
+#[safety_constraint(...)]
on field(s) is recommended since it helps with readability.
For example, if we were defining a custom vector MyVector
and wanted to
+specify that the inner vector’s length is always less than or equal to its
+capacity, we should do it as follows:
#[derive(Arbitrary)]
+#[safety_constraint(vector.len() <= *capacity)]
+struct MyVector<T> {
+ vector: Vec<T>,
+ capacity: usize,
+}
However, if we were defining a struct whose fields are not related in any
+way, we would prefer using the #[safety_constraint(...)]
attribute on its
+fields:
#[derive(Arbitrary)]
+struct PositivePoint {
+ #[safety_constraint(*x >= 0)]
+ x: i32,
+ #[safety_constraint(*y >= 0)]
+ y: i32,
+}
#[derive(Invariant)]
+{
+ // Attributes available to this derive:
+ #[safety_constraint]
+}
+
Allow users to auto generate Invariant
implementations by using
+#[derive(Invariant)]
macro.
#[safety_constraint(...)]
attributeWhen using #[derive(Invariant)]
on a struct, the
+#[safety_constraint(<cond>)]
attribute can be added to either the struct
+or its fields (but not both) to indicate a type safety invariant condition
+<cond>
. This will ensure that the type-safety condition gets additionally
+checked when using the is_safe()
method automatically generated by the
+#[derive(Invariant)]
macro.
For example, the check_positive
harness in this code is expected to
+fail:
#[derive(kani::Invariant)]
+struct AlwaysPositive {
+ #[safety_constraint(*inner >= 0)]
+ inner: i32,
+}
+
+#[kani::proof]
+fn check_positive() {
+ let val = AlwaysPositive { inner: -1 };
+ assert!(val.is_safe());
+}
This is not too surprising since the type safety invariant that we indicated
+is not being taken into account when we create the AlwaysPositive
object.
As mentioned, the is_safe()
methods generated by the
+#[derive(Invariant)]
macro check the corresponding is_safe()
method for
+each field in addition to any type safety invariants specified through the
+#[safety_constraint(...)]
attribute.
For example, for the AlwaysPositive
struct from above, we will generate
+the following implementation:
impl kani::Invariant for AlwaysPositive {
+ fn is_safe(&self) -> bool {
+ let obj = self;
+ let inner = &obj.inner;
+ true && *inner >= 0 && inner.is_safe()
+ }
+}
Note: the assignments to obj
and inner
are made so that we can treat the
+fields as if they were references.
#[safety_constraint(...)]
to the struct as opposed to its fieldsAs mentioned earlier, the #[safety_constraint(...)]
attribute can be added
+to either the struct or its fields, but not to both. Adding the
+#[safety_constraint(...)]
attribute to both the struct and its fields will
+result in an error.
In practice, only one type of specification is need. If the condition for
+the type safety invariant involves a relation between two or more struct
+fields, the struct-level attribute should be used. Otherwise, using the
+#[safety_constraint(...)]
is recommended since it helps with readability.
For example, if we were defining a custom vector MyVector
and wanted to
+specify that the inner vector’s length is always less than or equal to its
+capacity, we should do it as follows:
#[derive(Invariant)]
+#[safety_constraint(vector.len() <= *capacity)]
+struct MyVector<T> {
+ vector: Vec<T>,
+ capacity: usize,
+}
However, if we were defining a struct whose fields are not related in any
+way, we would prefer using the #[safety_constraint(...)]
attribute on its
+fields:
#[derive(Invariant)]
+struct PositivePoint {
+ #[safety_constraint(*x >= 0)]
+ x: i32,
+ #[safety_constraint(*y >= 0)]
+ y: i32,
+}
pub enum AllocationStatus {
+ Dangling,
+ DeadObject,
+ Null,
+ InBounds,
+ OutOfBounds,
+}
Enumeration with the cases currently covered by the pointer generator.
+Dangling pointers
+Pointer to dead object
+Null pointers
+In bounds pointer (it may be unaligned)
+The pointer cannot be read / written to for the given type since one or more bytes +would be out of bounds of the current allocation.
+source
. Read morepub fn float_to_int_in_range<Float, Int>(value: Float) -> boolwhere
+ Float: FloatToInt<Int>,
Returns whether the given float value
satisfies the range
+condition of the to_int_unchecked
methods, namely that the value
+after truncation is in range of the target Int
let f: f32 = 145.7;
+let fits_in_i8 = kani::float::float_to_int_in_range::<f32, i8>(f);
+// doesn't fit in `i8` because the value after truncation (`145.0`) is larger than `i8::MAX`
+assert!(!fits_in_i8);
+
+let f: f64 = 1e6;
+let fits_in_u32 = kani::float::float_to_int_in_range::<f64, u32>(f);
+// fits in `u32` because the value after truncation (`1e6`) is smaller than `u32::MAX`
+assert!(fits_in_u32);
This module contains functions useful for float-related checks
+value
satisfies the range
+condition of the to_int_unchecked
methods, namely that the value
+after truncation is in range of the target Int
pub fn any<T: Arbitrary>() -> T
This creates an symbolic valid value of type T
. You can assign the return value of this
+function to a variable that you want to make symbolic.
In the snippet below, we are verifying the behavior of the function fn_under_verification
+under all possible NonZeroU8
input values, i.e., all possible u8
values except zero.
let inputA = kani::any::<core::num::NonZeroU8>();
+fn_under_verification(inputA);
Note: This is a safe construct and can only be used with types that implement the Arbitrary
+trait. The Arbitrary trait is used to build a symbolic value that represents all possible
+valid values for type T
.
pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T
This creates a symbolic valid value of type T
.
+The value is constrained to be a value accepted by the predicate passed to the filter.
+You can assign the return value of this function to a variable that you want to make symbolic.
In the snippet below, we are verifying the behavior of the function fn_under_verification
+under all possible u8
input values between 0 and 12.
let inputA: u8 = kani::any_where(|x| *x < 12);
+fn_under_verification(inputA);
Note: This is a safe construct and can only be used with types that implement the Arbitrary
+trait. The Arbitrary trait is used to build a symbolic value that represents all possible
+valid values for type T
.
pub fn assume(cond: bool)
Creates an assumption that will be valid after this statement run. Note that the assumption +will only be applied for paths that follow the assumption. If the assumption doesn’t hold, the +program will exit successfully.
+The code snippet below should never panic.
+ +let i : i32 = kani::any();
+kani::assume(i > 10);
+if i < 0 {
+ panic!("This will never panic");
+}
The following code may panic though:
+ +let i : i32 = kani::any();
+assert!(i < 0, "This may panic and verification should fail.");
+kani::assume(i > 10);
pub const fn cover(_cond: bool, _msg: &'static str)
Creates a cover property with the specified condition and message.
+kani::cover(slice.len() == 0, "The slice may have a length of 0");
A cover property checks if there is at least one execution that satisfies +the specified condition at the location in which the function is called.
+Cover properties are reported as:
+This function is called by the cover!
macro. The macro is more
+convenient to use.
pub fn pointer_generator<T, const NUM_ELTS: usize>() -> PointerGenerator<{ _ }>
Create a pointer generator that fits at least N
elements of type T
.
pub enum SchedulingAssumption {
+ CanAssumeRunning,
+ CannotAssumeRunning,
+}
Indicates to the scheduler whether it can kani::assume
that the returned task is running.
This is useful if the task was picked nondeterministically using kani::any()
.
+For more information, see SchedulingStrategy
.
pub fn block_on<T>(fut: impl Future<Output = T>) -> T
A very simple executor: it polls the future in a busy loop until completion
+This is intended as a drop-in replacement for futures::block_on
, which Kani cannot handle.
+Whereas a clever executor like block_on
in futures
or tokio
would interact with the OS scheduler
+to be woken up when a resource becomes available, this is not supported by Kani.
+As a consequence, this function completely ignores the waker infrastructure and just polls the given future in a busy loop.
Note that spawn
is not supported with this function. Use block_on_with_spawn
if you need it.
pub fn block_on_with_spawn<F: Future<Output = ()> + Sync + 'static>(
+ fut: F,
+ scheduling_plan: impl SchedulingStrategy,
+)
Polls the given future and the tasks it may spawn until all of them complete
+Contrary to block_on
, this allows spawn
ing other futures
pub fn spawn<F: Future<Output = ()> + Sync + 'static>(fut: F) -> JoinHandle ⓘ
Spawns a task on the current global executor (which is set by block_on_with_spawn
)
This function can only be called inside a future passed to block_on_with_spawn
.
This module contains functions to work with futures (and async/.await) in Kani.
+kani::assume
that the returned task is running.block_on_with_spawn
)pub struct JoinHandle { /* private fields */ }
Result of spawning a task.
+If you .await
a JoinHandle, this will wait for the spawned task to complete.
pub struct RoundRobin { /* private fields */ }
Keeps cycling through the tasks in a deterministic order
+pub trait SchedulingStrategy {
+ // Required method
+ fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption);
+}
Trait that determines the possible sequence of tasks scheduling for a harness.
+If your harness spawns several tasks, Kani’s scheduler has to decide in what order to poll them. +This order may depend on the needs of your verification goal. +For example, you sometimes may wish to verify all possible schedulings, i.e. a nondeterministic scheduling strategy.
+Nondeterministic scheduling strategies can be very slow to verify because they require Kani to check a large number of permutations of tasks.
+So if you want to verify a harness that uses spawn
, but don’t care about concurrency issues, you can simply use a deterministic scheduling strategy,
+such as RoundRobin
, which polls each task in turn.
Finally, you have the option of providing your own scheduling strategy by implementing this trait. +This can be useful, for example, if you want to verify that things work correctly for a very specific task ordering.
+Picks the next task to be scheduled whenever the scheduler needs to pick a task to run next, and whether it can be assumed that the picked task is still running
+Tasks are numbered 0..num_tasks
.
+For example, if pick_task(4) returns (2, CanAssumeRunning) than it picked the task with index 2 and allows Kani to assume
that this task is still running.
+This is useful if the task is chosen nondeterministicall (kani::any()
) and allows the verifier to discard useless execution branches (such as polling a completed task again).
As a rule of thumb:
+if the scheduling strategy picks the next task nondeterministically (using kani::any()
), return CanAssumeRunning, otherwise CannotAssumeRunning.
+When returning CanAssumeRunning
, the scheduler will then assume that the picked task is still running, which cuts off “useless” paths where a completed task is polled again.
+It is even necessary to make things terminate if nondeterminism is involved:
+if we pick the task nondeterministically, and don’t have the restriction to still running tasks, we could poll the same task over and over again.
However, for most deterministic scheduling strategies, e.g. the round robin scheduling strategy, assuming that the picked task is still running is generally not possible
+because if that task has ended, we are saying assume(false) and the verification effectively stops (which is undesirable, of course).
+In such cases, return CannotAssumeRunning
instead.
pub use invariant::Invariant;
pub use futures::RoundRobin;
pub use futures::block_on;
pub use futures::block_on_with_spawn;
pub use futures::spawn;
pub use futures::yield_now;
Arbitrary
trait as well as implementation for
+primitive types and other std containers.Invariant
trait as well as its implementation
+for primitive types.kani::Arbitrary
on a tuple whose elements
+already implement kani::Arbitrary
by running kani::any()
on
+each index of the tuple.implies!(premise => conclusion)
means that if the premise
is true, so
+must be the conclusion
.T
. You can assign the return value of this
+function to a variable that you want to make symbolic.T
.
+The value is constrained to be a value accepted by the predicate passed to the filter.
+You can assign the return value of this function to a variable that you want to make symbolic.concrete_playback
for type checking during verification mode.N
elements of type T
.stub_verified(TARGET)
is a harness attribute (to be used on
+proof
or proof_for_contract
+function) that replaces all occurrences of TARGET
reachable from this
+harness with a stub generated from the contract on TARGET
.#[kani::unwind(arg)]
can only be called alongside #[kani::proof]
.
+arg - Takes in a integer value (u32) that represents the unwind value for the harness.This module introduces the Invariant
trait as well as its implementation
+for primitive types.
pub trait Invariantwhere
+ Self: Sized,{
+ // Required method
+ fn is_safe(&self) -> bool;
+}
This trait should be used to specify and check type safety invariants for a +type. For type invariants, we refer to the definitions in the Rust’s Unsafe +Code Guidelines Reference: +https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#validity-and-safety-invariant
+In summary, the reference distinguishes two kinds of type invariants:
+Therefore, validity invariants must be upheld at all times, while safety +invariants only need to be upheld at the boundaries to safe code.
+Safety invariants are particularly interesting for user-defined types, and
+the Invariant
trait allows you to check them with Kani.
It can also be used in tests. It’s a programmatic way to specify (in Rust) +properties over your data types. Since it’s written in Rust, it can be used +for static and dynamic checking.
+For example, let’s say you’re creating a type that represents a date:
+ +#[derive(kani::Arbitrary)]
+pub struct MyDate {
+ day: u8,
+ month: u8,
+ year: i64,
+}
You can specify its safety invariant as:
+ +
+impl kani::Invariant for MyDate {
+ fn is_safe(&self) -> bool {
+ self.month > 0
+ && self.month <= 12
+ && self.day > 0
+ && self.day <= days_in_month(self.year, self.month)
+ }
+}
And use it to check that your APIs are safe:
+ +#[kani::proof]
+fn check_increase_date() {
+ let mut date: MyDate = kani::any();
+ // Increase date by one day
+ increase_date(&mut date, 1);
+ assert!(date.is_safe());
+}
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Redirecting to macro.arbitrary_tuple.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.arbitrary_tuple.html b/crates/doc/kani/macro.arbitrary_tuple.html new file mode 100644 index 000000000000..03fc08793c29 --- /dev/null +++ b/crates/doc/kani/macro.arbitrary_tuple.html @@ -0,0 +1,6 @@ +macro_rules! arbitrary_tuple {
+ ($($type:ident),*) => { ... };
+}
This macro implements kani::Arbitrary
on a tuple whose elements
+already implement kani::Arbitrary
by running kani::any()
on
+each index of the tuple.
Redirecting to macro.cover.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.cover.html b/crates/doc/kani/macro.cover.html new file mode 100644 index 000000000000..b5214bb326d4 --- /dev/null +++ b/crates/doc/kani/macro.cover.html @@ -0,0 +1,5 @@ +macro_rules! cover {
+ () => { ... };
+ ($cond:expr $(,)?) => { ... };
+ ($cond:expr, $msg:literal) => { ... };
+}
Redirecting to macro.generate_arbitrary.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.generate_arbitrary.html b/crates/doc/kani/macro.generate_arbitrary.html new file mode 100644 index 000000000000..d92cf9b355af --- /dev/null +++ b/crates/doc/kani/macro.generate_arbitrary.html @@ -0,0 +1,3 @@ +macro_rules! generate_arbitrary {
+ ($core:path) => { ... };
+}
Redirecting to macro.generate_float.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.generate_float.html b/crates/doc/kani/macro.generate_float.html new file mode 100644 index 000000000000..af361d5dc643 --- /dev/null +++ b/crates/doc/kani/macro.generate_float.html @@ -0,0 +1,3 @@ +macro_rules! generate_float {
+ ($core:path) => { ... };
+}
Redirecting to macro.generate_models.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.generate_models.html b/crates/doc/kani/macro.generate_models.html new file mode 100644 index 000000000000..8014a317946c --- /dev/null +++ b/crates/doc/kani/macro.generate_models.html @@ -0,0 +1,3 @@ +macro_rules! generate_models {
+ () => { ... };
+}
Redirecting to macro.implies.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.implies.html b/crates/doc/kani/macro.implies.html new file mode 100644 index 000000000000..aef26f57a275 --- /dev/null +++ b/crates/doc/kani/macro.implies.html @@ -0,0 +1,7 @@ +macro_rules! implies {
+ ($premise:expr => $conclusion:expr) => { ... };
+}
implies!(premise => conclusion)
means that if the premise
is true, so
+must be the conclusion
.
This simply expands to !premise || conclusion
and is intended to make checks more readable,
+as the concept of an implication is more natural to think about than its expansion.
Redirecting to macro.kani_intrinsics.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.kani_intrinsics.html b/crates/doc/kani/macro.kani_intrinsics.html new file mode 100644 index 000000000000..1596a0bd9a94 --- /dev/null +++ b/crates/doc/kani/macro.kani_intrinsics.html @@ -0,0 +1,7 @@ +macro_rules! kani_intrinsics {
+ ($core:tt) => { ... };
+}
Kani intrinsics contains the public APIs used by users to verify their harnesses. +This macro is a part of kani_core as that allows us to verify even libraries that are no_core +such as core in rust’s std library itself.
+TODO: Use this inside kani library so that we dont have to maintain two copies of the same intrinsics.
+Redirecting to macro.kani_lib.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.kani_lib.html b/crates/doc/kani/macro.kani_lib.html new file mode 100644 index 000000000000..3503db606486 --- /dev/null +++ b/crates/doc/kani/macro.kani_lib.html @@ -0,0 +1,11 @@ +macro_rules! kani_lib {
+ (core) => { ... };
+ (kani) => { ... };
+}
Users should only need to invoke this.
+Options are:
+kani
: Add definitions needed for Kani library.core
: Define a kani
module inside core
crate.std
: TODO: Define a kani
module inside std
crate. Users must define kani inside core.Redirecting to macro.kani_mem.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.kani_mem.html b/crates/doc/kani/macro.kani_mem.html new file mode 100644 index 000000000000..b53027256a63 --- /dev/null +++ b/crates/doc/kani/macro.kani_mem.html @@ -0,0 +1,3 @@ +macro_rules! kani_mem {
+ ($core:tt) => { ... };
+}
Redirecting to macro.kani_mem_init.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.kani_mem_init.html b/crates/doc/kani/macro.kani_mem_init.html new file mode 100644 index 000000000000..dca5c196ba13 --- /dev/null +++ b/crates/doc/kani/macro.kani_mem_init.html @@ -0,0 +1,3 @@ +macro_rules! kani_mem_init {
+ ($core:path) => { ... };
+}
Redirecting to macro.ptr_generator.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.ptr_generator.html b/crates/doc/kani/macro.ptr_generator.html new file mode 100644 index 000000000000..44b79927a9e2 --- /dev/null +++ b/crates/doc/kani/macro.ptr_generator.html @@ -0,0 +1,3 @@ +macro_rules! ptr_generator {
+ () => { ... };
+}
Redirecting to macro.ptr_generator_fn.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.ptr_generator_fn.html b/crates/doc/kani/macro.ptr_generator_fn.html new file mode 100644 index 000000000000..783616112076 --- /dev/null +++ b/crates/doc/kani/macro.ptr_generator_fn.html @@ -0,0 +1,3 @@ +macro_rules! ptr_generator_fn {
+ () => { ... };
+}
Redirecting to macro.slice_generator.html...
+ + + \ No newline at end of file diff --git a/crates/doc/kani/macro.slice_generator.html b/crates/doc/kani/macro.slice_generator.html new file mode 100644 index 000000000000..5503043d9ac6 --- /dev/null +++ b/crates/doc/kani/macro.slice_generator.html @@ -0,0 +1,3 @@ +macro_rules! slice_generator {
+ () => { ... };
+}
pub fn can_dereference<T: ?Sized>(ptr: *const T) -> bool
Checks that pointer ptr
point to a valid value of type T
.
For that, the pointer has to be a valid pointer according to crate::mem conditions 1, 2
+and 3,
+and the value stored must respect the validity invariants for type T
.
TODO: Kani should automatically add those checks when a de-reference happens. +https://github.com/model-checking/kani/issues/2975
+This function will panic today if the pointer is not null, and it points to an unallocated or +deallocated memory location. This is an existing Kani limitation. +See https://github.com/model-checking/kani/issues/2690 for more details.
+pub fn can_read_unaligned<T: ?Sized>(ptr: *const T) -> bool
Checks that pointer ptr
point to a valid value of type T
.
For that, the pointer has to be a valid pointer according to crate::mem conditions 1, 2
+and 3,
+and the value stored must respect the validity invariants for type T
.
Note this function succeeds for unaligned pointers. See self::can_dereference if you also +want to check pointer alignment.
+This function will panic today if the pointer is not null, and it points to an unallocated or +deallocated memory location. This is an existing Kani limitation. +See https://github.com/model-checking/kani/issues/2690 for more details.
+pub fn can_write<T: ?Sized>(ptr: *mut T) -> bool
Check if the pointer is valid for write access according to crate::mem conditions 1, 2 +and 3.
+Note this function also checks for pointer alignment. Use self::can_write_unaligned +if you don’t want to fail for unaligned pointers.
+This function does not check if the value stored is valid for the given type. Use +self::can_dereference for that.
+This function will panic today if the pointer is not null, and it points to an unallocated or +deallocated memory location. This is an existing Kani limitation. +See https://github.com/model-checking/kani/issues/2690 for more details.
+pub fn can_write_unaligned<T: ?Sized>(ptr: *const T) -> bool
Check if the pointer is valid for unaligned write access according to crate::mem conditions +1, 2 and 3.
+Note this function succeeds for unaligned pointers. See self::can_write if you also +want to check pointer alignment.
+This function will panic today if the pointer is not null, and it points to an unallocated or +deallocated memory location. This is an existing Kani limitation. +See https://github.com/model-checking/kani/issues/2690 for more details.
+This module contains functions useful for checking unsafe memory access.
+Given the following validity rules provided in the Rust documentation: +https://doc.rust-lang.org/std/ptr/index.html (accessed Feb 6th, 2024)
+NonNull::dangling
.read_volatile
and write_volatile
:
+Volatile accesses cannot be used for inter-thread synchronization.Kani is able to verify #1 and #2 today.
+For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if
+the address matches NonNull::<()>::dangling()
.
+The way Kani tracks provenance is not enough to check if the address was the result of a cast
+from a non-zero integer literal.
ptr
point to a valid value of type T
.ptr
point to a valid value of type T
.This module contains an API for shadow memory. +Shadow memory is a mechanism by which we can store metadata on memory +locations, e.g. whether a memory location is initialized.
+The main data structure provided by this module is the ShadowMem
struct,
+which allows us to store metadata on a given memory location.
use kani::shadow::ShadowMem;
+use std::alloc::{alloc, Layout};
+
+let mut sm = ShadowMem::new(false);
+
+unsafe {
+ let ptr = alloc(Layout::new::<u8>());
+ // assert the memory location is not initialized
+ assert!(!sm.get(ptr));
+ // write to the memory location
+ *ptr = 42;
+ // update the shadow memory to indicate that this location is now initialized
+ sm.set(ptr, true);
+}
T
.
+Each element of the outer array represents an object, and each element of
+the inner array represents a byte in the object.pub struct ShadowMem<T: Copy> { /* private fields */ }
A shadow memory data structure that contains a two-dimensional array of a
+generic type T
.
+Each element of the outer array represents an object, and each element of
+the inner array represents a byte in the object.
pub fn any_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T]
Given an array arr
of length LENGTH
, this function returns a valid
+slice of arr
with non-deterministic start and end points. This is useful
+in situations where one wants to verify that all possible slices of a given
+array satisfy some property.
let arr = [1, 2, 3];
+let slice = kani::slice::any_slice_of_array(&arr);
+foo(slice); // where foo is a function that takes a slice and verifies a property about it
pub fn any_slice_of_array_mut<T, const LENGTH: usize>(
+ arr: &mut [T; LENGTH],
+) -> &mut [T]
A mutable version of the previous function
+arr
of length LENGTH
, this function returns a valid
+slice of arr
with non-deterministic start and end points. This is useful
+in situations where one wants to verify that all possible slices of a given
+array satisfy some property.pub struct ArbitraryPointer<'a, T> {
+ pub ptr: *mut T,
+ pub status: AllocationStatus,
+ pub is_initialized: bool,
+ /* private fields */
+}
Holds information about a pointer that is generated non-deterministically.
+ptr: *mut T
The pointer that was generated.
+status: AllocationStatus
The expected allocation status.
+is_initialized: bool
Whether the pointer was generated with an initialized value or not.
+pub struct PointerGenerator<const BYTES: usize> { /* private fields */ }
Pointer generator that can be used to generate arbitrary pointers.
+This generator allows users to build pointers with different safety properties. +This is different than creating a pointer that can have any address, since it will never +point to a previously allocated object. +See this section +for more details.
+The generator contains an internal buffer of a constant generic size, BYTES
, that it
+uses to generate InBounds
and OutOfBounds
pointers.
+In those cases, the generated pointers will have the same provenance as the generator,
+and the same lifetime.
+The address of an InBounds
pointer will represent all possible addresses in the range
+of the generator’s buffer address.
For other allocation statuses, the generator will create a pointer that satisfies the +given condition. +The pointer address will not represent all possible addresses that satisfies the +given allocation status.
+For example:
+ + let mut generator = PointerGenerator::<10>::new();
+ let arbitrary = generator.any_alloc_status::<char>();
+ kani::assume(arbitrary.status == AllocationStatus::InBounds);
+ // Pointer may be unaligned, but it should be in-bounds, so it is safe to write to
+ unsafe { arbitrary.ptr.write_unaligned(kani::any()) }
The generator is parameterized by the number of bytes of its internal buffer. +See pointer_generator function if you would like to create a generator that fits +a minimum number of objects of a given type. Example:
+ + // These generators have the same capacity of 6 bytes.
+ let generator1 = PointerGenerator::<6>::new();
+ let generator2 = pointer_generator::<i16, 3>();
The internal buffer is used to generate pointers, and its size determines the maximum +number of pointers it can generate without overlapping. +Larger values will impact the maximum distance between generated pointers.
+We recommend that you pick a size that is at least big enough to
+cover the cases where all pointers produced are non-overlapping.
+The buffer size in bytes must be big enough to fit distinct objects for each call
+of generate pointer.
+For example, generating two *mut u8
and one *mut u32
requires a buffer
+of at least 6 bytes.
This guarantees that your harness covers cases where all generated pointers +point to allocated positions that do not overlap. For example:
+ + let mut generator = PointerGenerator::<6>::new();
+ let ptr1: *mut u8 = generator.any_in_bounds().ptr;
+ let ptr2: *mut u8 = generator.any_in_bounds().ptr;
+ let ptr3: *mut u32 = generator.any_in_bounds().ptr;
+ // This cover is satisfied.
+ cover!((ptr1 as usize) >= (ptr2 as usize) + size_of::<u8>()
+ && (ptr2 as usize) >= (ptr3 as usize) + size_of::<u32>());
+ // As well as having overlapping pointers.
+ cover!((ptr1 as usize) == (ptr3 as usize));
The first cover will be satisfied, since there exists at least one path where +the generator produces inbounds pointers that do not overlap. Such as this scenario:
++--------+--------+--------+--------+--------+--------+
+| Byte 0 | Byte 1 | Byte 2 | Byte 3 | Byte 4 | Byte 5 |
++--------+--------+--------+--------+--------+--------+
+<--------------- ptr3 --------------><--ptr2-><--ptr1->
I.e., the generator buffer is large enough to fit all 3 objects without overlapping.
+In contrast, if we had used a size of 1 element, all calls to any_in_bounds()
would
+return elements that overlap, and the first cover would no longer be satisfied.
Note that the generator requires a minimum number of 1 byte, otherwise the
+InBounds
case would never be covered.
+Compilation will fail if you try to create a generator of size 0
.
Additionally, the verification will fail if you try to generate a pointer for a type +with size greater than the buffer size.
+Use larger buffer size if you want to cover scenarios where the distance +between the generated pointers matters.
+The only caveats of using very large numbers are:
+isize::MAX
).The pointer returned in the InBounds
and OutOfBounds
case will have the same
+provenance as the generator.
Use the same generator if you want to handle cases where 2 or more pointers may overlap. E.g.:
+ + let mut generator = pointer_generator::<char, 5>();
+ let ptr1 = generator.any_in_bounds::<char>().ptr;
+ let ptr2 = generator.any_in_bounds::<char>().ptr;
+ // This cover is satisfied.
+ cover!(ptr1 == ptr2)
If you want to cover cases where two or more pointers may not have the same +provenance, you will need to instantiate multiple generators. +You can also apply non-determinism to cover cases where the pointers may or may not +have the same provenance. E.g.:
+ + let mut generator1 = pointer_generator::<char, 5>();
+ let mut generator2 = pointer_generator::<char, 5>();
+ let ptr1: *const char = generator1.any_in_bounds().ptr;
+ let ptr2: *const char = if kani::any() {
+ // Pointers will have same provenance and may overlap.
+ generator1.any_in_bounds().ptr
+ } else {
+ // Pointers will have different provenance and will not overlap.
+ generator2.any_in_bounds().ptr
+ };
+ // Invoke the function under verification
+ unsafe { my_target(ptr1, ptr2) };
Creating a pointer using the generator is different than generating a pointer +with any address.
+I.e.:
+ + // This pointer represents any address, and it may point to anything in memory,
+ // allocated or not.
+ let ptr1 = kani::any::<usize>() as *const u8;
+
+ // This pointer address will either point to unallocated memory, to a dead object
+ // or to allocated memory within the generator address space.
+ let mut generator = PointerGenerator::<5>::new();
+ let ptr2: *const u8 = generator.any_alloc_status().ptr;
Kani cannot reason about a pointer allocation status (except for asserting its validity). +Thus, the generator was introduced to help writing harnesses that need to impose +constraints to the arbitrary pointer allocation status. +It also allow us to restrict the pointer provenance, excluding for example the address of +variables that are not available in the current context. +As a limitation, it will not cover the entire address space that a pointer can take.
+If your harness does not need to reason about pointer allocation, for example, verifying +pointer wrapping arithmetic, using a pointer with any address will allow you to cover +all possible scenarios.
+Creates a raw pointer with non-deterministic properties.
+The pointer returned is either dangling or has the same provenance of the generator.
+Creates a in-bounds raw pointer with non-deterministic properties.
+The pointer points to an allocated location with the same provenance of the generator. +The pointer may be unaligned, and the pointee may be uninitialized.
+ + let mut generator = PointerGenerator::<6>::new();
+ let ptr1: *mut u8 = generator.any_in_bounds().ptr;
+ let ptr2: *mut u8 = generator.any_in_bounds().ptr;
+ // SAFETY: Both pointers have the same provenance.
+ let distance = unsafe { ptr1.offset_from(ptr2) };
+ assert!(distance > -5 && distance < 5)
pub trait Arbitrarywhere
+ Self: Sized,{
+ // Required method
+ fn any() -> Self;
+
+ // Provided method
+ fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] { ... }
+}
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] +Ref: https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html
+Arbitrary
implementations by …\nHolds information about a pointer that is generated …\nDangling pointers\nPointer to dead object\nIn bounds pointer (it may be unaligned)\nAllow users to auto generate Invariant
implementations by …\nNull pointers\nThe pointer cannot be read / written to for the given type …\nPointer generator that can be used to generate arbitrary …\nThis creates an symbolic valid value of type T
. You can …\nCreates a raw pointer with non-deterministic properties.\nCreates a in-bounds raw pointer with non-deterministic …\nThis creates a symbolic valid value of type T
. The value …\nThis module introduces the Arbitrary
trait as well as …\nThis macro implements kani::Arbitrary
on a tuple whose …\nCreates an assertion of the specified condition and …\nCreates an assumption that will be valid after this …\nNOP concrete_playback
for type checking during …\nKani implementation of function contracts.\nCreates a cover property with the specified condition and …\nAdd a postcondition to this function.\nThis module contains functions useful for float-related …\nReturns the argument unchanged.\nReturns the argument unchanged.\nReturns the argument unchanged.\nThis module contains functions to work with futures (and …\nimplies!(premise => conclusion)
means that if the premise
…\nCalls U::from(self)
.\nCalls U::from(self)
.\nCalls U::from(self)
.\nThis module introduces the Invariant
trait as well as its …\nWhether the pointer was generated with an initialized …\nKani intrinsics contains the public APIs used by users to …\nUsers should only need to invoke this.\nAdd a loop invariant to this loop.\nThis module contains functions useful for checking unsafe …\nDeclaration of an explicit write-set for the annotated …\nCreate a new PointerGenerator.\nCreate a pointer generator that fits at least N
elements …\nMarks a Kani proof harness\nDesignates this function as a harness to check a function …\nThe pointer that was generated.\nSpecifies that a function contains recursion for contract …\nAdd a precondition to this function.\nThis module contains an API for shadow memory. Shadow …\nSpecifies that a proof harness is expected to panic.**\nSelect the SAT solver to use with CBMC for this harness\nThe expected allocation status.\nSpecify a function/method stub pair to use for proof …\nstub_verified(TARGET)
is a harness attribute (to be used on\nSet Loop unwind limit for proof harnesses The attribute …\nAdd a postcondition to this function.\nDeclaration of an explicit write-set for the annotated …\nDesignates this function as a harness to check a function …\nAdd a precondition to this function.\nstub_verified(TARGET)
is a harness attribute (to be used on\nReturns whether the given float value
satisfies the range …\nResult of spawning a task.\nKeeps cycling through the tasks in a deterministic order\nIndicates to the scheduler whether it can kani::assume
…\nTrait that determines the possible sequence of tasks …\nA very simple executor: it polls the future in a busy loop …\nPolls the given future and the tasks it may spawn until …\nReturns the argument unchanged.\nReturns the argument unchanged.\nReturns the argument unchanged.\nCalls U::from(self)
.\nCalls U::from(self)
.\nCalls U::from(self)
.\nPicks the next task to be scheduled whenever the scheduler …\nSpawns a task on the current global executor (which is set …\nSuspends execution of the current future, to allow the …\nThis trait should be used to specify and check type safety …\nChecks that pointer ptr
point to a valid value of type T
.\nChecks that pointer ptr
point to a valid value of type T
.\nCheck if the pointer is valid for write access according …\nCheck if the pointer is valid for unaligned write access …\nCompute the size of the val pointed to if safe.\nCompute the size of the val pointed to if it is safe to do …\nCheck if two pointers points to the same allocated object, …\nA shadow memory data structure that contains a …\nReturns the argument unchanged.\nGet the shadow memory value of the given pointer\nCalls U::from(self)
.\nCreate a new shadow memory instance initialized with the …\nSet the shadow memory value of the given pointer\nGiven an array arr
of length LENGTH
, this function returns …\nA mutable version of the previous function\nGenerates an arbitrary vector whose length is at most …\nGenerates an arbitrary vector that is exactly EXACT_LENGTH …")
\ No newline at end of file
diff --git a/crates/doc/settings.html b/crates/doc/settings.html
new file mode 100644
index 000000000000..ada0eb811a30
--- /dev/null
+++ b/crates/doc/settings.html
@@ -0,0 +1 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module introduces the `Arbitrary` trait as well as implementation for
+//! primitive types and other std containers.
+
+use crate::Arbitrary;
+
+impl<T> Arbitrary for std::boxed::Box<T>
+where
+ T: Arbitrary,
+{
+ fn any() -> Self {
+ Box::new(T::any())
+ }
+}
+
+impl Arbitrary for std::time::Duration {
+ fn any() -> Self {
+ const NANOS_PER_SEC: u32 = 1_000_000_000;
+ let nanos = u32::any();
+ crate::assume(nanos < NANOS_PER_SEC);
+ std::time::Duration::new(u64::any(), nanos)
+ }
+}
+
+1 +2 +3 +4 +5 +6 +7 +8 +9 +10 +11 +12 +13 +14 +15 +16 +17 +18 +19 +20 +21 +22 +23 +24 +25 +26 +27 +28 +29 +30 +31 +32 +33 +34 +35 +36 +37 +38 +39 +40 +41 +42 +43 +44 +45 +46 +47 +48 +49 +50 +51 +52 +53 +54 +55 +56 +57 +58 +59 +60 +61 +62 +63 +64 +65 +66 +67 +68 +69 +70 +71 +72 +73 +74 +75 +76 +77 +78 +79 +80 +81 +82 +83 +84 +85 +86 +87 +88 +89 +90 +91 +92 +93 +94 +95 +96 +97 +98 +99 +100 +101 +102 +103 +104 +105 +106 +107 +108 +109 +110 +111 +112 +113 +114 +115 +116 +117 +118 +119 +120 +121 +122 +123 +124 +125 +126 +127 +128 +129 +130 +131 +132 +133 +134 +135 +136 +137 +138 +139 +140 +141 +142 +143 +144 +145 +146 +147 +148 +149 +150 +151 +152 +153 +154 +155 +156 +157 +158 +159 +160 +161 +162 +163 +164 +165 +166 +167 +168 +169 +170 +171 +172 +173 +174 +175 +176 +177 +178 +179 +180 +181 +182 +183 +184 +185 +186 +187 +188 +189 +190 +191 +192 +193 +194 +195 +196 +197 +198 +199 +200 +201 +202 +203 +204 +205 +206 +207 +208 +209 +210 +211 +212 +213 +214 +215 +216 +217 +218 +219 +220 +221 +222 +223 +224 +225 +226 +227 +228 +229 +230 +231 +232 +233 +234 +235 +236 +237 +238 +239 +240 +241 +242 +243 +244 +245 +246 +247 +248 +249 +250 +251 +252 +253 +254 +255 +256 +257 +258 +259 +260 +261 +262 +263 +264 +265 +266 +267 +268 +269 +270 +271 +272 +273 +274 +275 +276 +277 +278
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Kani implementation of function contracts.
+//!
+//! Function contracts are still under development. Using the APIs therefore
+//! requires the unstable `-Zfunction-contracts` flag to be passed. You can join
+//! the discussion on contract design by reading our
+//! [RFC](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html)
+//! and [commenting on the tracking
+//! issue](https://github.com/model-checking/kani/issues/2652).
+//!
+//! The function contract API is expressed as proc-macro attributes, and there
+//! are two parts to it.
+//!
+//! 1. [Contract specification attributes](#specification-attributes-overview):
+//! [`requires`][macro@requires] and [`ensures`][macro@ensures].
+//! 2. [Contract use attributes](#contract-use-attributes-overview):
+//! [`proof_for_contract`][macro@proof_for_contract] and
+//! [`stub_verified`][macro@stub_verified].
+//!
+//! ## Step-by-step Guide
+//!
+//! Let us explore using a workflow involving contracts on the example of a
+//! simple division function `my_div`:
+//!
+//! ```
+//! fn my_div(dividend: usize, divisor: usize) -> usize {
+//! dividend / divisor
+//! }
+//! ```
+//!
+//! With the contract specification attributes we can specify the behavior of
+//! this function declaratively. The [`requires`][macro@requires] attribute
+//! allows us to declare constraints on what constitutes valid inputs to our
+//! function. In this case we would want to disallow a divisor that is `0`.
+//!
+//! ```
+//! # use kani::requires;
+//! #[requires(divisor != 0)]
+//! # fn my_div(dividend: usize, divisor: usize) -> usize {
+//! # dividend / divisor
+//! # }
+//! ```
+//!
+//! This is called a precondition, because it is enforced before (pre-) the
+//! function call. As you can see attribute has access to the functions
+//! arguments. The condition itself is just regular Rust code. You can use any
+//! Rust code, including calling functions and methods. However you may not
+//! perform I/O (like [`println!`]) or mutate memory (like [`Vec::push`]).
+//!
+//! The [`ensures`][macro@ensures] attribute on the other hand lets us describe
+//! the output value in terms of the inputs. You may be as (im)precise as you
+//! like in the [`ensures`][macro@ensures] clause, depending on your needs. One
+//! approximation of the result of division for instance could be this:
+//!
+//! ```
+//! # use kani::ensures;
+//! #[ensures(|result : &usize| *result <= dividend)]
+//! # fn my_div(dividend: usize, divisor: usize) -> usize {
+//! # dividend / divisor
+//! # }
+//! ```
+//!
+//! This is called a postcondition and it also has access to the arguments and
+//! is expressed in regular Rust code. The same restrictions apply as did for
+//! [`requires`][macro@requires]. In addition to the postcondition is expressed
+//! as a closure where the value returned from the function is passed to this
+//! closure by reference.
+//!
+//! You may combine as many [`requires`][macro@requires] and
+//! [`ensures`][macro@ensures] attributes on a single function as you please.
+//! They all get enforced (as if their conditions were `&&`ed together) and the
+//! order does not matter. In our example putting them together looks like this:
+//!
+//! ```
+//! use kani::{requires, ensures};
+//!
+//! #[requires(divisor != 0)]
+//! #[ensures(|result : &usize| *result <= dividend)]
+//! fn my_div(dividend: usize, divisor: usize) -> usize {
+//! dividend / divisor
+//! }
+//! ```
+//!
+//! Once we are finished specifying our contract we can ask Kani to check it's
+//! validity. For this we need to provide a proof harness that exercises the
+//! function. The harness is created like any other, e.g. as a test-like
+//! function with inputs and using `kani::any` to create arbitrary values.
+//! However we do not need to add any assertions or assumptions about the
+//! inputs, Kani will use the pre- and postconditions we have specified for that
+//! and we use the [`proof_for_contract`][macro@proof_for_contract] attribute
+//! instead of [`proof`](crate::proof) and provide it with the path to the
+//! function we want to check.
+//!
+//! ```
+//! # use kani::{requires, ensures};
+//! #
+//! # #[requires(divisor != 0)]
+//! # #[ensures(|result : &usize| *result <= dividend)]
+//! # fn my_div(dividend: usize, divisor: usize) -> usize {
+//! # dividend / divisor
+//! # }
+//! #
+//! #[kani::proof_for_contract(my_div)]
+//! fn my_div_harness() {
+//! my_div(kani::any(), kani::any());
+//! }
+//! ```
+//!
+//! The harness is checked like any other by running `cargo kani` and can be
+//! specifically selected with `--harness my_div_harness`.
+//!
+//! Once we have verified that our contract holds, we can use perhaps it's
+//! coolest feature: verified stubbing. This allows us to use the conditions of
+//! the contract *instead* of it's implementation. This can be very powerful for
+//! expensive implementations (involving loops for instance).
+//!
+//! Verified stubbing is available to any harness via the
+//! [`stub_verified`][macro@stub_verified] harness attribute. We must provide
+//! the attribute with the path to the function to stub, but unlike with
+//! [`stub`](crate::stub) we do not need to provide a function to replace with,
+//! the contract will be used automatically.
+//!
+//! ```
+//! # use kani::{requires, ensures};
+//! #
+//! # #[requires(divisor != 0)]
+//! # #[ensures(|result : &usize| *result <= dividend)]
+//! # fn my_div(dividend: usize, divisor: usize) -> usize {
+//! # dividend / divisor
+//! # }
+//! #
+//! #[kani::proof]
+//! #[kani::stub_verified(my_div)]
+//! fn use_div() {
+//! let v = kani::vec::any_vec::<char, 5>();
+//! let some_idx = my_div(v.len() - 1, 3);
+//! v[some_idx];
+//! }
+//! ```
+//!
+//! In this example the contract is sufficient to prove that the element access
+//! in the last line cannot be out-of-bounds.
+//!
+//! ## Specification Attributes Overview
+//!
+//! The basic two specification attributes available for describing
+//! function behavior are [`requires`][macro@requires] for preconditions and
+//! [`ensures`][macro@ensures] for postconditions. Both admit arbitrary Rust
+//! expressions as their bodies which may also reference the function arguments
+//! but must not mutate memory or perform I/O. The postcondition may
+//! additionally reference the return value of the function as the variable
+//! `result`.
+//!
+//! In addition Kani provides the [`modifies`](macro@modifies) attribute. This
+//! works a bit different in that it does not contain conditions but a comma
+//! separated sequence of expressions that evaluate to pointers. This attribute
+//! constrains to which memory locations the function is allowed to write. Each
+//! expression can contain arbitrary Rust syntax, though it may not perform side
+//! effects and it is also currently unsound if the expression can panic. For more
+//! information see the [write sets](#write-sets) section.
+//!
+//! During verified stubbing the return value of a function with a contract is
+//! replaced by a call to `kani::any`. As such the return value must implement
+//! the `kani::Arbitrary` trait.
+//!
+//! In Kani, function contracts are optional. As such a function with at least
+//! one specification attribute is considered to "have a contract" and any
+//! absent specification type defaults to its most general interpretation
+//! (`true`). All functions with not a single specification attribute are
+//! considered "not to have a contract" and are ineligible for use as the target
+//! of a [`proof_for_contract`][macro@proof_for_contract] of
+//! [`stub_verified`][macro@stub_verified] attribute.
+//!
+//! ## Contract Use Attributes Overview
+//!
+//! Contract are used both to verify function behavior and to leverage the
+//! verification result as a sound abstraction.
+//!
+//! Verifying function behavior currently requires the designation of at least
+//! one checking harness with the
+//! [`proof_for_contract`](macro@proof_for_contract) attribute. A harness may
+//! only have one `proof_for_contract` attribute and it may not also have a
+//! `proof` attribute.
+//!
+//! The checking harness is expected to set up the arguments that `foo` should
+//! be called with and initialized any `static mut` globals that are reachable.
+//! All of these should be initialized to as general value as possible, usually
+//! achieved using `kani::any`. The harness must call e.g. `foo` at least once
+//! and if `foo` has type parameters, only one instantiation of those parameters
+//! is admissible. Violating either results in a compile error.
+//!
+//! If any inputs have special invariants you *can* use `kani::assume` to
+//! enforce them but this may introduce unsoundness. In general all restrictions
+//! on input parameters should be part of the [`requires`](macro@requires)
+//! clause of the function contract.
+//!
+//! Once the contract has been verified it may be used as a verified stub. For
+//! this the [`stub_verified`](macro@stub_verified) attribute is used.
+//! `stub_verified` is a harness attribute, like
+//! [`unwind`](macro@crate::unwind), meaning it is used on functions that are
+//! annotated with [`proof`](macro@crate::proof). It may also be used on a
+//! `proof_for_contract` proof.
+//!
+//! Unlike `proof_for_contract` multiple `stub_verified` attributes are allowed
+//! on the same proof harness though they must target different functions.
+//!
+//! ## Inductive Verification
+//!
+//! Function contracts by default use inductive verification to efficiently
+//! verify recursive functions. In inductive verification a recursive function
+//! is executed once and every recursive call instead uses the contract
+//! replacement. In this way many recursive calls can be checked with a
+//! single verification pass.
+//!
+//! The downside of inductive verification is that the return value of a
+//! contracted function must implement `kani::Arbitrary`. Due to restrictions to
+//! code generation in proc macros, the contract macros cannot determine reliably
+//! in all cases whether a given function with a contract is recursive. As a
+//! result it conservatively sets up inductive verification for every function
+//! and requires the `kani::Arbitrary` constraint for contract checks.
+//!
+//! If you feel strongly about this issue you can join the discussion on issue
+//! [#2823](https://github.com/model-checking/kani/issues/2823) to enable
+//! opt-out of inductive verification.
+//!
+//! ## Write Sets
+//!
+//! The [`modifies`](macro@modifies) attribute is used to describe which
+//! locations in memory a function may assign to. The attribute contains a comma
+//! separated series of expressions that reference the function arguments.
+//! Syntactically any expression is permissible, though it may not perform side
+//! effects (I/O, mutation) or panic. As an example consider this super simple
+//! function:
+//!
+//! ```
+//! #[kani::modifies(ptr, my_box.as_ref())]
+//! fn a_function(ptr: &mut u32, my_box: &mut Box<u32>) {
+//! *ptr = 80;
+//! *my_box.as_mut() = 90;
+//! }
+//! ```
+//!
+//! Because the function performs an observable side-effect (setting both the
+//! value behind the pointer and the value pointed-to by the box) we need to
+//! provide a `modifies` attribute. Otherwise Kani will reject a contract on
+//! this function.
+//!
+//! An expression used in a `modifies` clause must return a pointer to the
+//! location that you would like to allow to be modified. This can be any basic
+//! Rust pointer type (`&T`, `&mut T`, `*const T` or `*mut T`). In addition `T`
+//! must implement [`Arbitrary`](super::Arbitrary). This is used to assign
+//! `kani::any()` to the location when the function is used in a `stub_verified`.
+//!
+//! ## History Expressions
+//!
+//! Additionally, an ensures clause is allowed to refer to the state of the function arguments before function execution and perform simple computations on them
+//! via an `old` monad. Any instance of `old(computation)` will evaluate the
+//! computation before the function is called. It is required that this computation
+//! is effect free and closed with respect to the function arguments.
+//!
+//! For example, the following code passes kani tests:
+//!
+//! ```
+//! #[kani::modifies(a)]
+//! #[kani::ensures(|result| old(*a).wrapping_add(1) == *a)]
+//! #[kani::ensures(|result : &u32| old(*a).wrapping_add(1) == *result)]
+//! fn add1(a : &mut u32) -> u32 {
+//! *a=a.wrapping_add(1);
+//! *a
+//! }
+//! ```
+//!
+//! Here, the value stored in `a` is precomputed and remembered after the function
+//! is called, even though the contents of `a` changed during the function execution.
+//!
+pub use super::{ensures, modifies, proof_for_contract, requires, stub_verified};
+
+1 +2 +3 +4 +5 +6 +7 +8 +9 +10 +11 +12 +13 +14 +15 +16 +17 +18 +19 +20 +21 +22 +23 +24 +25 +26 +27 +28 +29 +30 +31 +32 +33 +34 +35 +36 +37 +38 +39 +40 +41 +42 +43 +44 +45 +46 +47 +48 +49 +50 +51 +52 +53 +54 +55 +56 +57 +58 +59 +60 +61 +62 +63 +64 +65 +66 +67 +68 +69 +70 +71 +72 +73 +74 +75 +76 +77 +78 +79 +80 +81 +82 +83 +84 +85 +86 +87 +88 +89 +90 +91 +92 +93 +94 +95 +96 +97 +98 +99 +100 +101 +102 +103 +104 +105 +106 +107 +108 +109 +110 +111 +112 +113 +114 +115 +116 +117 +118 +119 +120 +121 +122 +123 +124 +125 +126 +127 +128 +129 +130 +131 +132 +133 +134 +135 +136 +137 +138 +139 +140 +141 +142 +143 +144 +145 +146 +147 +148 +149 +150 +151 +152 +153 +154 +155 +156 +157 +158 +159 +160 +161 +162 +163 +164 +165 +166 +167 +168 +169 +170 +171 +172 +173 +174 +175 +176 +177 +178 +179 +180 +181 +182 +183 +184 +185 +186 +187 +188 +189 +190 +191 +192 +193 +194 +195 +196 +197 +198 +199 +200 +201 +202 +203 +204 +205 +206 +207 +208 +209 +210 +211 +212 +213 +214 +215 +216 +217 +218 +219 +220 +221 +222 +223 +224 +225 +226 +227 +228 +229 +230 +231 +232 +233 +234 +235 +236 +237
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module contains functions to work with futures (and async/.await) in Kani.
+
+use std::{
+ future::Future,
+ pin::Pin,
+ task::{Context, RawWaker, RawWakerVTable, Waker},
+};
+
+/// A very simple executor: it polls the future in a busy loop until completion
+///
+/// This is intended as a drop-in replacement for `futures::block_on`, which Kani cannot handle.
+/// Whereas a clever executor like `block_on` in `futures` or `tokio` would interact with the OS scheduler
+/// to be woken up when a resource becomes available, this is not supported by Kani.
+/// As a consequence, this function completely ignores the waker infrastructure and just polls the given future in a busy loop.
+///
+/// Note that [`spawn`] is not supported with this function. Use [`block_on_with_spawn`] if you need it.
+#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
+pub fn block_on<T>(mut fut: impl Future<Output = T>) -> T {
+ let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
+ let cx = &mut Context::from_waker(&waker);
+ // SAFETY: we shadow the original binding, so it cannot be accessed again for the rest of the scope.
+ // This is the same as what the pin_mut! macro in the futures crate does.
+ let mut fut = unsafe { Pin::new_unchecked(&mut fut) };
+ loop {
+ match fut.as_mut().poll(cx) {
+ std::task::Poll::Ready(res) => return res,
+ std::task::Poll::Pending => continue,
+ }
+ }
+}
+
+/// A dummy waker, which is needed to call [`Future::poll`]
+const NOOP_RAW_WAKER: RawWaker = {
+ #[inline]
+ unsafe fn clone_waker(_: *const ()) -> RawWaker {
+ NOOP_RAW_WAKER
+ }
+
+ #[inline]
+ unsafe fn noop(_: *const ()) {}
+
+ RawWaker::new(std::ptr::null(), &RawWakerVTable::new(clone_waker, noop, noop, noop))
+};
+
+/// The global executor used by [`spawn`] and [`block_on_with_spawn`] to run tasks.
+static mut GLOBAL_EXECUTOR: Option<Scheduler> = None;
+
+type BoxFuture = Pin<Box<dyn Future<Output = ()> + Sync + 'static>>;
+
+/// Indicates to the scheduler whether it can `kani::assume` that the returned task is running.
+///
+/// This is useful if the task was picked nondeterministically using `kani::any()`.
+/// For more information, see [`SchedulingStrategy`].
+pub enum SchedulingAssumption {
+ CanAssumeRunning,
+ CannotAssumeRunning,
+}
+
+/// Trait that determines the possible sequence of tasks scheduling for a harness.
+///
+/// If your harness spawns several tasks, Kani's scheduler has to decide in what order to poll them.
+/// This order may depend on the needs of your verification goal.
+/// For example, you sometimes may wish to verify all possible schedulings, i.e. a nondeterministic scheduling strategy.
+///
+/// Nondeterministic scheduling strategies can be very slow to verify because they require Kani to check a large number of permutations of tasks.
+/// So if you want to verify a harness that uses `spawn`, but don't care about concurrency issues, you can simply use a deterministic scheduling strategy,
+/// such as [`RoundRobin`], which polls each task in turn.
+///
+/// Finally, you have the option of providing your own scheduling strategy by implementing this trait.
+/// This can be useful, for example, if you want to verify that things work correctly for a very specific task ordering.
+pub trait SchedulingStrategy {
+ /// Picks the next task to be scheduled whenever the scheduler needs to pick a task to run next, and whether it can be assumed that the picked task is still running
+ ///
+ /// Tasks are numbered `0..num_tasks`.
+ /// For example, if pick_task(4) returns (2, CanAssumeRunning) than it picked the task with index 2 and allows Kani to `assume` that this task is still running.
+ /// This is useful if the task is chosen nondeterministicall (`kani::any()`) and allows the verifier to discard useless execution branches (such as polling a completed task again).
+ ///
+ /// As a rule of thumb:
+ /// if the scheduling strategy picks the next task nondeterministically (using `kani::any()`), return CanAssumeRunning, otherwise CannotAssumeRunning.
+ /// When returning `CanAssumeRunning`, the scheduler will then assume that the picked task is still running, which cuts off "useless" paths where a completed task is polled again.
+ /// It is even necessary to make things terminate if nondeterminism is involved:
+ /// if we pick the task nondeterministically, and don't have the restriction to still running tasks, we could poll the same task over and over again.
+ ///
+ /// However, for most deterministic scheduling strategies, e.g. the round robin scheduling strategy, assuming that the picked task is still running is generally not possible
+ /// because if that task has ended, we are saying assume(false) and the verification effectively stops (which is undesirable, of course).
+ /// In such cases, return `CannotAssumeRunning` instead.
+ fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption);
+}
+
+/// Keeps cycling through the tasks in a deterministic order
+#[derive(Default)]
+pub struct RoundRobin {
+ index: usize,
+}
+
+impl SchedulingStrategy for RoundRobin {
+ #[inline]
+ fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption) {
+ self.index = (self.index + 1) % num_tasks;
+ (self.index, SchedulingAssumption::CannotAssumeRunning)
+ }
+}
+
+pub(crate) struct Scheduler {
+ tasks: Vec<Option<BoxFuture>>,
+ num_running: usize,
+}
+
+impl Scheduler {
+ /// Creates a scheduler with an empty task list
+ #[inline]
+ pub(crate) const fn new() -> Scheduler {
+ Scheduler { tasks: Vec::new(), num_running: 0 }
+ }
+
+ /// Adds a future to the scheduler's task list, returning a JoinHandle
+ pub(crate) fn spawn<F: Future<Output = ()> + Sync + 'static>(&mut self, fut: F) -> JoinHandle {
+ let index = self.tasks.len();
+ self.tasks.push(Some(Box::pin(fut)));
+ self.num_running += 1;
+ JoinHandle { index }
+ }
+
+ /// Runs the scheduler with the given scheduling plan until all tasks have completed
+ fn run(&mut self, mut scheduling_plan: impl SchedulingStrategy) {
+ let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
+ let cx = &mut Context::from_waker(&waker);
+ while self.num_running > 0 {
+ let (index, assumption) = scheduling_plan.pick_task(self.tasks.len());
+ let task = &mut self.tasks[index];
+ if let Some(fut) = task.as_mut() {
+ match fut.as_mut().poll(cx) {
+ std::task::Poll::Ready(()) => {
+ self.num_running -= 1;
+ let _prev = task.take();
+ }
+ std::task::Poll::Pending => (),
+ }
+ } else if let SchedulingAssumption::CanAssumeRunning = assumption {
+ crate::assume(false); // useful so that we can assume that a nondeterministically picked task is still running
+ }
+ }
+ }
+
+ /// Polls the given future and the tasks it may spawn until all of them complete
+ fn block_on<F: Future<Output = ()> + Sync + 'static>(
+ &mut self,
+ fut: F,
+ scheduling_plan: impl SchedulingStrategy,
+ ) {
+ self.spawn(fut);
+ self.run(scheduling_plan);
+ }
+}
+
+/// Result of spawning a task.
+///
+/// If you `.await` a JoinHandle, this will wait for the spawned task to complete.
+pub struct JoinHandle {
+ index: usize,
+}
+
+#[allow(static_mut_refs)]
+impl Future for JoinHandle {
+ type Output = ();
+
+ fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll<Self::Output> {
+ if unsafe { GLOBAL_EXECUTOR.as_mut().unwrap().tasks[self.index].is_some() } {
+ std::task::Poll::Pending
+ } else {
+ cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers.
+ std::task::Poll::Ready(())
+ }
+ }
+}
+
+/// Spawns a task on the current global executor (which is set by [`block_on_with_spawn`])
+///
+/// This function can only be called inside a future passed to [`block_on_with_spawn`].
+#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
+#[allow(static_mut_refs)]
+pub fn spawn<F: Future<Output = ()> + Sync + 'static>(fut: F) -> JoinHandle {
+ unsafe {
+ if let Some(executor) = GLOBAL_EXECUTOR.as_mut() {
+ executor.spawn(fut)
+ } else {
+ // An explicit panic instead of `.expect(...)` has better location information in Kani's output
+ panic!("`spawn` should only be called within `block_on_with_spawn`")
+ }
+ }
+}
+
+/// Polls the given future and the tasks it may spawn until all of them complete
+///
+/// Contrary to [`block_on`], this allows `spawn`ing other futures
+#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
+#[allow(static_mut_refs)]
+pub fn block_on_with_spawn<F: Future<Output = ()> + Sync + 'static>(
+ fut: F,
+ scheduling_plan: impl SchedulingStrategy,
+) {
+ unsafe {
+ assert!(GLOBAL_EXECUTOR.is_none(), "`block_on_with_spawn` should not be nested");
+ GLOBAL_EXECUTOR = Some(Scheduler::new());
+ GLOBAL_EXECUTOR.as_mut().unwrap().block_on(fut, scheduling_plan);
+ GLOBAL_EXECUTOR = None;
+ }
+}
+
+/// Suspends execution of the current future, to allow the scheduler to poll another future
+///
+/// Specifically, it returns a future that isn't ready until the second time it is polled.
+#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
+pub fn yield_now() -> impl Future<Output = ()> {
+ struct YieldNow {
+ yielded: bool,
+ }
+
+ impl Future for YieldNow {
+ type Output = ();
+
+ fn poll(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll<Self::Output> {
+ if self.yielded {
+ cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers.
+ std::task::Poll::Ready(())
+ } else {
+ self.yielded = true;
+ std::task::Poll::Pending
+ }
+ }
+ }
+
+ YieldNow { yielded: false }
+}
+
+1 +2 +3 +4 +5 +6 +7 +8 +9 +10 +11 +12 +13 +14 +15 +16 +17 +18 +19 +20 +21 +22 +23 +24 +25 +26 +27 +28 +29 +30 +31 +32 +33 +34 +35 +36 +37 +38 +39 +40 +41 +42 +43 +44 +45 +46 +47 +48 +49 +50 +51 +52 +53 +54 +55 +56 +57 +58 +59 +60 +61 +62 +63 +64 +65 +66 +67 +68 +69 +70 +71 +72 +73 +74 +75 +76 +77 +78 +79 +80 +81 +82 +83 +84 +85 +86 +87 +88 +89 +90 +91 +92 +93 +94 +95 +96 +97 +98 +99 +100 +101 +102 +103 +104 +105 +106 +107 +108 +109 +110 +111 +112 +113 +114 +115 +116 +117 +118 +119 +120 +121 +122 +123 +124 +125 +126 +127 +128 +129 +130 +131 +132 +133
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module introduces the `Invariant` trait as well as its implementation
+//! for primitive types.
+
+/// This trait should be used to specify and check type safety invariants for a
+/// type. For type invariants, we refer to the definitions in the Rust's Unsafe
+/// Code Guidelines Reference:
+/// <https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#validity-and-safety-invariant>
+///
+/// In summary, the reference distinguishes two kinds of type invariants:
+/// - *Validity invariant*: An invariant that all data must uphold any time
+/// it's accessed or copied in a typed manner. This invariant is exploited by
+/// the compiler to perform optimizations.
+/// - *Safety invariant*: An invariant that safe code may assume all data to
+/// uphold. This invariant can be temporarily violated by unsafe code, but
+/// must always be upheld when interfacing with unknown safe code.
+///
+/// Therefore, validity invariants must be upheld at all times, while safety
+/// invariants only need to be upheld at the boundaries to safe code.
+///
+/// Safety invariants are particularly interesting for user-defined types, and
+/// the `Invariant` trait allows you to check them with Kani.
+///
+/// It can also be used in tests. It's a programmatic way to specify (in Rust)
+/// properties over your data types. Since it's written in Rust, it can be used
+/// for static and dynamic checking.
+///
+/// For example, let's say you're creating a type that represents a date:
+///
+/// ```rust
+/// #[derive(kani::Arbitrary)]
+/// pub struct MyDate {
+/// day: u8,
+/// month: u8,
+/// year: i64,
+/// }
+/// ```
+/// You can specify its safety invariant as:
+/// ```rust
+/// # #[derive(kani::Arbitrary)]
+/// # pub struct MyDate {
+/// # day: u8,
+/// # month: u8,
+/// # year: i64,
+/// # }
+/// # fn days_in_month(_: i64, _: u8) -> u8 { 31 }
+///
+/// impl kani::Invariant for MyDate {
+/// fn is_safe(&self) -> bool {
+/// self.month > 0
+/// && self.month <= 12
+/// && self.day > 0
+/// && self.day <= days_in_month(self.year, self.month)
+/// }
+/// }
+/// ```
+/// And use it to check that your APIs are safe:
+/// ```no_run
+/// # use kani::Invariant;
+/// #
+/// # #[derive(kani::Arbitrary)]
+/// # pub struct MyDate {
+/// # day: u8,
+/// # month: u8,
+/// # year: i64,
+/// # }
+/// #
+/// # fn days_in_month(_: i64, _: u8) -> u8 { todo!() }
+/// # fn increase_date(_: &mut MyDate, _: u8) { todo!() }
+/// #
+/// # impl Invariant for MyDate {
+/// # fn is_safe(&self) -> bool {
+/// # self.month > 0
+/// # && self.month <= 12
+/// # && self.day > 0
+/// # && self.day <= days_in_month(self.year, self.month)
+/// # }
+/// # }
+/// #
+/// #[kani::proof]
+/// fn check_increase_date() {
+/// let mut date: MyDate = kani::any();
+/// // Increase date by one day
+/// increase_date(&mut date, 1);
+/// assert!(date.is_safe());
+/// }
+/// ```
+pub trait Invariant
+where
+ Self: Sized,
+{
+ fn is_safe(&self) -> bool;
+}
+
+/// Any value is considered safe for the type
+macro_rules! trivial_invariant {
+ ( $type: ty ) => {
+ impl Invariant for $type {
+ #[inline(always)]
+ fn is_safe(&self) -> bool {
+ true
+ }
+ }
+ };
+}
+
+trivial_invariant!(u8);
+trivial_invariant!(u16);
+trivial_invariant!(u32);
+trivial_invariant!(u64);
+trivial_invariant!(u128);
+trivial_invariant!(usize);
+
+trivial_invariant!(i8);
+trivial_invariant!(i16);
+trivial_invariant!(i32);
+trivial_invariant!(i64);
+trivial_invariant!(i128);
+trivial_invariant!(isize);
+
+// We do not constrain the safety invariant for floating points types.
+// Users can create a new type wrapping the floating point type and define an
+// invariant that checks for NaN, infinite, or subnormal values.
+trivial_invariant!(f32);
+trivial_invariant!(f64);
+trivial_invariant!(f16);
+trivial_invariant!(f128);
+
+trivial_invariant!(());
+trivial_invariant!(bool);
+trivial_invariant!(char);
+
+1 +2 +3 +4 +5 +6 +7 +8 +9 +10 +11 +12 +13 +14 +15 +16 +17 +18 +19 +20 +21 +22 +23 +24 +25 +26 +27 +28 +29 +30 +31 +32 +33 +34 +35 +36 +37 +38 +39 +40 +41 +42 +43 +44 +45 +46 +47 +48 +49 +50 +51 +52 +53 +54 +55 +56 +57 +58 +59 +60 +61 +62 +63 +64 +65 +66 +67 +68 +69 +70 +71 +72 +73 +74 +75 +76 +77 +78 +79 +80 +81 +82 +83 +84 +85 +86 +87 +88 +89 +90
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Required so we can use kani_macros attributes.
+#![feature(register_tool)]
+#![register_tool(kanitool)]
+// Used for rustc_diagnostic_item.
+// Note: We could use a kanitool attribute instead.
+#![feature(rustc_attrs)]
+// Used to model simd.
+#![feature(repr_simd)]
+#![feature(generic_const_exprs)]
+#![allow(incomplete_features)]
+// Features used for tests only.
+#![cfg_attr(test, feature(core_intrinsics, portable_simd))]
+// Required for `rustc_diagnostic_item` and `core_intrinsics`
+#![allow(internal_features)]
+// Required for implementing memory predicates.
+#![feature(layout_for_ptr)]
+#![feature(ptr_metadata)]
+#![feature(f16)]
+#![feature(f128)]
+#![feature(convert_float_to_int)]
+
+// Allow us to use `kani::` to access crate features.
+extern crate self as kani;
+
+pub mod arbitrary;
+#[cfg(feature = "concrete_playback")]
+mod concrete_playback;
+pub mod futures;
+pub mod invariant;
+pub mod shadow;
+pub mod vec;
+
+mod models;
+
+#[cfg(feature = "concrete_playback")]
+pub use concrete_playback::concrete_playback_run;
+pub use invariant::Invariant;
+
+#[cfg(not(feature = "concrete_playback"))]
+/// NOP `concrete_playback` for type checking during verification mode.
+pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
+ unreachable!("Concrete playback does not work during verification")
+}
+
+pub use futures::{RoundRobin, block_on, block_on_with_spawn, spawn, yield_now};
+
+// Kani proc macros must be in a separate crate
+pub use kani_macros::*;
+
+// Declare common Kani API such as assume, assert
+kani_core::kani_lib!(kani);
+
+// Used to bind `core::assert` to a different name to avoid possible name conflicts if a
+// crate uses `extern crate std as core`. See
+// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187
+#[doc(hidden)]
+#[cfg(not(feature = "concrete_playback"))]
+pub use core::assert as __kani__workaround_core_assert;
+
+#[macro_export]
+macro_rules! cover {
+ () => {
+ kani::cover(true, "cover location");
+ };
+ ($cond:expr $(,)?) => {
+ kani::cover($cond, concat!("cover condition: ", stringify!($cond)));
+ };
+ ($cond:expr, $msg:literal) => {
+ kani::cover($cond, $msg);
+ };
+}
+
+/// `implies!(premise => conclusion)` means that if the `premise` is true, so
+/// must be the `conclusion`.
+///
+/// This simply expands to `!premise || conclusion` and is intended to make checks more readable,
+/// as the concept of an implication is more natural to think about than its expansion.
+#[macro_export]
+macro_rules! implies {
+ ($premise:expr => $conclusion:expr) => {
+ !($premise) || ($conclusion)
+ };
+}
+
+pub(crate) use kani_macros::unstable_feature as unstable;
+
+pub mod contracts;
+
+1 +2 +3 +4 +5 +6 +7 +8 +9 +10 +11 +12 +13 +14 +15 +16 +17 +18 +19 +20 +21 +22 +23 +24 +25 +26 +27 +28 +29 +30 +31 +32 +33 +34 +35 +36 +37 +38 +39 +40 +41 +42 +43 +44 +45 +46 +47 +48 +49 +50 +51 +52 +53 +54 +55 +56 +57 +58 +59 +60 +61 +62 +63 +64 +65 +66 +67 +68 +69 +70 +71 +72 +73 +74 +75 +76 +77 +78 +79 +80 +81 +82 +83 +84 +85 +86 +87 +88 +89 +90 +91 +92 +93 +94 +95 +96 +97 +98 +99 +100 +101 +102 +103 +104 +105 +106 +107 +108 +109 +110 +111 +112 +113 +114 +115 +116 +117 +118 +119 +120 +121 +122 +123 +124 +125 +126 +127 +128 +129 +130 +131 +132 +133 +134 +135 +136 +137 +138 +139 +140 +141 +142 +143 +144 +145 +146 +147 +148 +149 +150 +151 +152 +153 +154 +155 +156 +157 +158 +159 +160 +161 +162 +163 +164 +165 +166 +167 +168 +169 +170 +171 +172 +173 +174 +175 +176 +177 +178 +179 +180 +181 +182 +183 +184 +185 +186 +187 +188 +189 +190 +191 +192 +193 +194 +195 +196 +197 +198 +199 +200 +201 +202 +203 +204 +205 +206 +207 +208 +209 +210 +211 +212 +213 +214 +215 +216 +217 +218 +219 +220 +221 +222 +223 +224 +225 +226
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Contains definitions that Kani compiler may use to model functions that are not suitable for
+//! verification or functions without a body, such as intrinsics.
+//!
+//! Note that these are models that Kani uses by default; thus, we keep them separate from stubs.
+
+// Definitions in this module are not meant to be visible to the end user, only the compiler.
+#[allow(dead_code)]
+mod intrinsics {
+ use std::fmt::Debug;
+ use std::mem::size_of;
+
+ /// Similar definition to portable SIMD.
+ /// We cannot reuse theirs since TRUE and FALSE defs are private.
+ /// We leave this private today, since this is not necessarily a final solution, so we don't
+ /// want users relying on this.
+ /// Our definitions are also a bit more permissive to comply with the platform intrinsics.
+ pub(super) trait MaskElement: PartialEq + Debug {
+ const TRUE: Self;
+ const FALSE: Self;
+ }
+
+ macro_rules! impl_element {
+ { $ty:ty } => {
+ impl MaskElement for $ty {
+ const TRUE: Self = -1;
+ const FALSE: Self = 0;
+ }
+ }
+ }
+
+ macro_rules! impl_unsigned_element {
+ { $ty:ty } => {
+ impl MaskElement for $ty {
+ // Note that in the declaration of the intrinsic it is documented that the lane
+ // values should be -1 or 0:
+ // <https://github.com/rust-lang/rust/blob/338cfd3/library/portable-simd/crates/core_simd/src/intrinsics.rs#L134-L144>
+ //
+ // However, MIRI and the Rust compiler seems to accept unsigned values and they
+ // use their binary representation. Thus, that's what we use for now.
+ /// All bits are 1 which represents TRUE.
+ const TRUE: Self = <$ty>::MAX;
+ /// All bits are 0 which represents FALSE.
+ const FALSE: Self = 0;
+ }
+ }
+ }
+
+ impl_element! { i8 }
+ impl_element! { i16 }
+ impl_element! { i32 }
+ impl_element! { i64 }
+ impl_element! { i128 }
+ impl_element! { isize }
+
+ impl_unsigned_element! { u8 }
+ impl_unsigned_element! { u16 }
+ impl_unsigned_element! { u32 }
+ impl_unsigned_element! { u64 }
+ impl_unsigned_element! { u128 }
+ impl_unsigned_element! { usize }
+
+ /// Calculate the minimum number of lanes to represent a mask
+ /// Logic similar to `bitmask_len` from `portable_simd`.
+ /// <https://github.com/rust-lang/portable-simd/blob/490b5cf/crates/core_simd/src/masks/to_bitmask.rs#L75-L79>
+ pub(super) const fn mask_len(len: usize) -> usize {
+ len.div_ceil(8)
+ }
+
+ #[cfg(target_endian = "little")]
+ unsafe fn simd_bitmask_impl<T, const LANES: usize>(input: &[T; LANES]) -> [u8; mask_len(LANES)]
+ where
+ T: MaskElement,
+ {
+ let mut mask_array = [0; mask_len(LANES)];
+ for lane in (0..input.len()).rev() {
+ let byte = lane / 8;
+ let mask = &mut mask_array[byte];
+ let shift_mask = *mask << 1;
+ *mask = if input[lane] == T::TRUE {
+ shift_mask | 0x1
+ } else {
+ assert_eq!(input[lane], T::FALSE, "Masks values should either be 0 or -1");
+ shift_mask
+ };
+ }
+ mask_array
+ }
+
+ /// Stub for simd_bitmask.
+ ///
+ /// It will reduce a simd vector (TxN), into an integer of size S (in bits), where S >= N.
+ /// Each bit of the output will represent a lane from the input. A lane value of all 0's will be
+ /// translated to 1b0, while all 1's will be translated to 1b1.
+ ///
+ /// In order to be able to do this pragmatically, we take additional parameters that are filled
+ /// by the compiler.
+ #[rustc_diagnostic_item = "KaniModelSimdBitmask"]
+ pub(super) unsafe fn simd_bitmask<T, U, E, const LANES: usize>(input: T) -> U
+ where
+ [u8; mask_len(LANES)]: Sized,
+ E: MaskElement,
+ {
+ // These checks are compiler sanity checks to ensure we are not doing anything invalid.
+ assert_eq!(
+ size_of::<U>(),
+ size_of::<[u8; mask_len(LANES)]>(),
+ "Expected size of return type and mask lanes to match",
+ );
+ assert_eq!(
+ size_of::<T>(),
+ size_of::<Simd::<E, LANES>>(),
+ "Expected size of input and lanes to match",
+ );
+
+ let data = &*(&input as *const T as *const [E; LANES]);
+ let mask = simd_bitmask_impl(data);
+ (&mask as *const [u8; mask_len(LANES)] as *const U).read()
+ }
+
+ /// Structure used for sanity check our parameters.
+ #[repr(simd)]
+ struct Simd<T, const LANES: usize>([T; LANES]);
+}
+
+#[cfg(test)]
+mod test {
+ use super::intrinsics as kani_intrinsic;
+ use std::intrinsics::simd::*;
+ use std::{fmt::Debug, simd::*};
+
+ /// Test that the `simd_bitmask` model is equivalent to the intrinsic for all true and all false
+ /// masks with lanes represented using i16.
+ #[test]
+ fn test_bitmask_i16() {
+ check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(false));
+ check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(true));
+ }
+
+ /// Tests that the model correctly fails if an invalid value is given.
+ #[test]
+ #[should_panic(expected = "Masks values should either be 0 or -1")]
+ fn test_invalid_bitmask() {
+ let invalid_mask = unsafe { mask32x16::from_int_unchecked(i32x16::splat(10)) };
+ assert_eq!(
+ unsafe { kani_intrinsic::simd_bitmask::<_, u16, i32, 16>(invalid_mask) },
+ u16::MAX
+ );
+ }
+
+ /// Tests that the model correctly fails if the size parameter of the mask doesn't match the
+ /// expected number of bytes in the representation.
+ #[test]
+ #[should_panic(expected = "Expected size of return type and mask lanes to match")]
+ fn test_invalid_generics() {
+ let mask = mask32x16::splat(false);
+ assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u16, i32, 2>(mask) }, u16::MAX);
+ }
+
+ /// Test that the `simd_bitmask` model is equivalent to the intrinsic for a few random values.
+ /// These values shouldn't be symmetric and ensure that we also handle endianness correctly.
+ #[test]
+ fn test_bitmask_i32() {
+ check_portable_bitmask::<_, i32, 8, u8>(mask32x8::from([
+ true, true, false, true, false, false, false, true,
+ ]));
+
+ check_portable_bitmask::<_, i32, 4, u8>(mask32x4::from([true, false, false, true]));
+ }
+
+ #[repr(simd)]
+ #[derive(Clone, Debug)]
+ struct CustomMask<T, const LANES: usize>([T; LANES]);
+
+ /// Check that the bitmask model can handle odd size SIMD arrays.
+ /// Since the portable_simd restricts the number of lanes, we have to use our own custom SIMD.
+ #[test]
+ fn test_bitmask_odd_lanes() {
+ check_bitmask::<_, [u8; 3], i128, 23>(CustomMask([0i128; 23]));
+ check_bitmask::<_, [u8; 9], i128, 70>(CustomMask([-1i128; 70]));
+ }
+
+ /// Compare the value returned by our model and the portable simd representation.
+ fn check_portable_bitmask<T, E, const LANES: usize, M>(mask: Mask<T, LANES>)
+ where
+ T: std::simd::MaskElement,
+ LaneCount<LANES>: SupportedLaneCount,
+ E: kani_intrinsic::MaskElement,
+ [u8; kani_intrinsic::mask_len(LANES)]: Sized,
+ u64: From<M>,
+ {
+ assert_eq!(
+ unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask)) },
+ mask.to_bitmask()
+ );
+ }
+
+ /// Compare the value returned by our model and the simd_bitmask intrinsic.
+ fn check_bitmask<T, U, E, const LANES: usize>(mask: T)
+ where
+ T: Clone,
+ U: PartialEq + Debug,
+ E: kani_intrinsic::MaskElement,
+ [u8; kani_intrinsic::mask_len(LANES)]: Sized,
+ {
+ assert_eq!(
+ unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask.clone()) },
+ unsafe { simd_bitmask::<T, U>(mask) }
+ );
+ }
+
+ /// Similar to portable simd_harness.
+ #[test]
+ fn check_mask_harness() {
+ // From array doesn't work either. Manually build [false, true, false, true]
+ let mut mask = mask32x4::splat(false);
+ mask.set(1, true);
+ mask.set(3, true);
+ let bitmask = mask.to_bitmask();
+ assert_eq!(bitmask, 0b1010);
+
+ let kani_mask = unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask)) };
+ assert_eq!(kani_mask, bitmask);
+ }
+}
+
+1 +2 +3 +4 +5 +6 +7 +8 +9 +10 +11 +12 +13 +14 +15 +16 +17 +18 +19 +20 +21 +22 +23 +24 +25 +26 +27 +28 +29 +30 +31 +32 +33 +34 +35 +36 +37 +38 +39 +40 +41 +42 +43 +44 +45 +46 +47 +48 +49 +50 +51 +52 +53 +54 +55 +56 +57 +58 +59 +60 +61 +62 +63 +64 +65 +66 +67 +68 +69 +70 +71 +72 +73 +74 +75 +76 +77 +78 +79 +80 +81 +82 +83
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module contains an API for shadow memory.
+//! Shadow memory is a mechanism by which we can store metadata on memory
+//! locations, e.g. whether a memory location is initialized.
+//!
+//! The main data structure provided by this module is the `ShadowMem` struct,
+//! which allows us to store metadata on a given memory location.
+//!
+//! # Example
+//!
+//! ```no_run
+//! use kani::shadow::ShadowMem;
+//! use std::alloc::{alloc, Layout};
+//!
+//! let mut sm = ShadowMem::new(false);
+//!
+//! unsafe {
+//! let ptr = alloc(Layout::new::<u8>());
+//! // assert the memory location is not initialized
+//! assert!(!sm.get(ptr));
+//! // write to the memory location
+//! *ptr = 42;
+//! // update the shadow memory to indicate that this location is now initialized
+//! sm.set(ptr, true);
+//! }
+//! ```
+
+const MAX_NUM_OBJECTS: usize = 1024;
+const MAX_OBJECT_SIZE: usize = 64;
+
+const MAX_NUM_OBJECTS_ASSERT_MSG: &str = "The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024)";
+const MAX_OBJECT_SIZE_ASSERT_MSG: &str =
+ "The object size exceeds the maximum size supported by Kani's shadow memory model (64)";
+
+/// A shadow memory data structure that contains a two-dimensional array of a
+/// generic type `T`.
+/// Each element of the outer array represents an object, and each element of
+/// the inner array represents a byte in the object.
+pub struct ShadowMem<T: Copy> {
+ mem: [[T; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS],
+}
+
+impl<T: Copy> ShadowMem<T> {
+ /// Create a new shadow memory instance initialized with the given value
+ #[crate::unstable(
+ feature = "ghost-state",
+ issue = 3184,
+ reason = "experimental ghost state/shadow memory API"
+ )]
+ pub const fn new(val: T) -> Self {
+ Self { mem: [[val; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] }
+ }
+
+ /// Get the shadow memory value of the given pointer
+ #[crate::unstable(
+ feature = "ghost-state",
+ issue = 3184,
+ reason = "experimental ghost state/shadow memory API"
+ )]
+ pub fn get<U>(&self, ptr: *const U) -> T {
+ let obj = crate::mem::pointer_object(ptr);
+ let offset = crate::mem::pointer_offset(ptr);
+ crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG);
+ crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG);
+ self.mem[obj][offset]
+ }
+
+ /// Set the shadow memory value of the given pointer
+ #[crate::unstable(
+ feature = "ghost-state",
+ issue = 3184,
+ reason = "experimental ghost state/shadow memory API"
+ )]
+ pub fn set<U>(&mut self, ptr: *const U, val: T) {
+ let obj = crate::mem::pointer_object(ptr);
+ let offset = crate::mem::pointer_offset(ptr);
+ crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG);
+ crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG);
+ self.mem[obj][offset] = val;
+ }
+}
+
+1 +2 +3 +4 +5 +6 +7 +8 +9 +10 +11 +12 +13 +14 +15 +16 +17 +18 +19 +20 +21 +22 +23 +24 +25 +26 +27 +28 +29 +30 +31
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+use crate::{Arbitrary, any, any_where};
+
+/// Generates an arbitrary vector whose length is at most MAX_LENGTH.
+pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
+where
+ T: Arbitrary,
+{
+ let real_length: usize = any_where(|sz| *sz <= MAX_LENGTH);
+ match real_length {
+ 0 => vec![],
+ exact if exact == MAX_LENGTH => exact_vec::<T, MAX_LENGTH>(),
+ _ => {
+ let mut any_vec = exact_vec::<T, MAX_LENGTH>();
+ any_vec.truncate(real_length);
+ any_vec.shrink_to_fit();
+ assert!(any_vec.capacity() == any_vec.len());
+ any_vec
+ }
+ }
+}
+
+/// Generates an arbitrary vector that is exactly EXACT_LENGTH long.
+pub fn exact_vec<T, const EXACT_LENGTH: usize>() -> Vec<T>
+where
+ T: Arbitrary,
+{
+ let boxed_array: Box<[T; EXACT_LENGTH]> = Box::new(any());
+ <[T]>::into_vec(boxed_array)
+}
+
fn:
) to \
+ restrict the search to a given item kind.","Accepted kinds are: fn
, mod
, struct
, \
+ enum
, trait
, type
, macro
, \
+ and const
.","Search functions by type signature (e.g., vec -> usize
or \
+ -> vec
or String, enum:Cow -> bool
)","You can look for items with an exact name by putting double quotes around \
+ your request: \"string\"
",`Look for functions that accept or return \
+ slices and \
+ arrays by writing square \
+ brackets (e.g., -> [u8]
or [] -> Option
)`,"Look for items inside another one by searching for a path: vec::Vec
",].map(x=>""+x+"
").join("");const div_infos=document.createElement("div");addClass(div_infos,"infos");div_infos.innerHTML="${value.replaceAll(" ", " ")}
`}else{error[index]=value}});output+=`Kani currently ships with a kani
crate that provide APIs to allow users to
+write and configure their harnesses.
+These APIs are tightly coupled with each Kani version, so they are not
+published yet at https://crates.io.
You can find their latest documentation here:
+cargo kani assess
Assess is an experimental new feature to gather data about Rust crates, to aid the start of proof writing.
+In the short-term, assess collects and dumps tables of data that may help Kani developers understand what's needed to begin writing proofs for another project. +For instance, assess may help answer questions like:
+In the long-term, assess will become a user-facing feature, and help Kani users get started writing proofs. +We expect that users will have the same questions as above, but in the long term, hopefully the answers to those trend towards an uninteresting "yes." +So the new questions might be:
+These long-term goals are only "hinted at" with the present experimental version of assess. +Currently, we only get as far as finding out which tests successfully verify (concretely) with Kani. +This might indicate tests that could be generalized and converted into proofs, but we currently don't do anything to group, rank, or otherwise heuristically prioritize what might be most "interesting." +(For instance, we'd like to eventually compute coverage information and use that to help rank the results.) +As a consequence, the output of the tool is very hard to interpret, and likely not (yet!) helpful to new or potential Kani users.
+To assess a package, run:
+cargo kani --enable-unstable assess
+
+As a temporary hack (arguments shouldn't work like this), to assess a single cargo workspace, run:
+cargo kani --enable-unstable --workspace assess
+
+To scan a collection of workspaces or packages that are not part of a shared workspace, run:
+cargo kani --enable-unstable assess scan
+
+The only difference between 'scan' and 'regular' assess is how the packages built are located.
+All versions of assess produce the same output and metrics.
+Assess will normally build just like cargo kani
or cargo build
, whereas scan
will find all cargo packages beneath the current directory, even in unrelated workspaces.
+Thus, 'scan' may be helpful in the case where the user has a choice of packages and is looking for the easiest to get started with (in addition to the Kani developer use-case, of aggregating statistics across many packages).
(Tip: Assess may need to run for awhile, so try using screen
, tmux
or nohup
to avoid terminating the process if, for example, an ssh connection breaks.
+Some tests can also consume huge amounts of ram when run through Kani, so you may wish to use ulimit -v 6000000
to prevent any processes from using more than 6GB.
+You can also limit the number of concurrent tests that will be run by providing e.g. -j 4
, currently as a prepended argument, like --enable-unstable
or --workspace
in the examples above.)
Assess builds all the packages requested in "test mode" (i.e. --tests
), and runs all the same tests that cargo test
would, except through Kani.
+This gives end-to-end assurance we're able to actually build and run code from these packages, skipping nothing of what the verification process would need, except that the harnesses don't have any nondeterminism (kani::any()
) and consequently don't "prove" much.
+The interesting signal comes from what tests cannot be analyzed by Kani due to unsupported features, performance problems, crash bugs, or other issues that get in the way.
Currently, assess forces termination by using unwind(1)
on all tests, so many tests will fail with unwinding assertions.
Assess produces a few tables of output (both visually in the terminal, and in a more detailed json format) so far:
+======================================================
+ Unsupported feature | Crates | Instances
+ | impacted | of use
+-------------------------------+----------+-----------
+ caller_location | 71 | 239
+ simd_bitmask | 39 | 160
+...
+
+The unsupported features table aggregates information about features that Kani does not yet support.
+These correspond to uses of codegen_unimplemented
in the kani-compiler
, and appear as warnings during compilation.
Unimplemented features are not necessarily actually hit by (dynamically) reachable code, so an immediate future improvement on this table would be to count the features actually hit by failing test cases, instead of just those features reported as existing in code by the compiler. +In other words, the current unsupported features table is not what we want to see, in order to perfectly prioritize implementing these features, because we may be counting features that no proof would ever hit. +A perfect signal here isn't possible: there may be code that looks statically reachable, but is never dynamically reachable, and we can't tell. +But we can use test coverage as an approximation: well-tested code will hopefully cover most of the dynamically reachable code. +The operating hypothesis of assess is that code covered by tests is code that could be covered by proof, and so measuring unsupported features by those actually hit by a test should provide a better "signal" about priorities. +Implicitly deprioritizing unsupported features because they aren't covered by tests may not be a bug, but a feature: we may simply not want to prove anything about that code, if it hasn't been tested first, and so adding support for that feature may not be important.
+A few notes on terminology:
+1
in this column, regardless of the number of dependencies.================================================
+ Reason for failure | Number of tests
+------------------------------+-----------------
+ unwind | 61
+ none (success) | 6
+ assertion + overflow | 2
+...
+
+The test failure reasons table indicates why, when assess ran a test through Kani, it failed to verify. +Notably:
+unwind(1)
, we expect unwind
to rank highly.assertion
means an ordinary assert!()
was hit (or something else with this property class).+
, such as assertion + overflow
.should_fail
tests, so assertion
may actually be "success": the test should hit an assertion and did.=============================================================================
+ Candidate for proof harness | Location
+-------------------------------------------------------+---------------------
+ float::tests::f64_edge_cases | src/float.rs:226
+ float::tests::f32_edge_cases | src/float.rs:184
+ integer::tests::test_integers | src/integer.rs:171
+
+This table is the most rudimentary so far, but is the core of what long-term assess will help accomplish. +Currently, this table just presents (with paths displayed in a clickable manner) the tests that successfully "verify" with Kani. +These might be good candidates for turning into proof harnesses. +This list is presently unordered; the next step for improving it would be to find even a rudimentary way of ranking these test cases (e.g. perhaps by code coverage).
+kani-compiler
emits *.kani-metadata.json
for each target it builds.
+This format can be found in the kani_metadata
crate, shared by kani-compiler
and kani-driver
.
+This is the starting point for assess.
Assess obtains this metadata by essentially running a cargo kani
:
--all-features
turned onunwind
always set to 1
--tests
Assess starts by getting all the information from these metadata files. +This is enough by itself to construct a rudimentary "unsupported features" table. +But assess also uses it to discover all the test cases, and (instead of running proof harnesses) it then runs all these test harnesses under Kani.
+Assess produces a second metadata format, called (unsurprisingly) "assess metadata".
+(Found in kani-driver
under src/assess/metadata.rs
.)
+This format records the results of what assess does.
This metadata can be written to a json file by providing --emit-metadata <file>
to assess
.
+Likewise, scan
can be told to write out this data with the same option.
Assess metadata is an aggregatable format.
+It does not apply to just one package, as assess can work on a workspace of packages.
+Likewise, scan
uses and produces the exact same format, across multiple workspaces.
So far all assess metadata comes in the form of "tables" which are built with TableBuilder<T: TableRow>
.
+This is documented further in src/assess/table_builder.rs
.
There is a script in the Kani repo for this purpose.
+This will clone the top-100 crates to /tmp/top-100-experiment
and run assess scan on them:
./scripts/exps/assess-scan-on-repos.sh
+
+If you'd like to preseve the results, you can direct scan to use a different directory with an environment variable:
+ASSESS_SCAN="~/top-100-experiment" ./scripts/exps/assess-scan-on-repos.sh
+
+To re-run the experiment, it suffices to be in the experiment directory:
+cd ~/top-100-experiment && ~/kani/scripts/exps/assess-scan-on-repos.sh
+
+
+ Kani is an open source project open to external contributions.
+The easiest way to contribute is to report any +issue you encounter +while using the tool. If you want to contribute to its development, +we recommend looking into these issues.
+In this chapter, we provide documentation that might be helpful for Kani +developers (including external contributors):
+cbmc
.rustc
.++ +NOTE: The developer documentation is intended for Kani developers and not +users. At present, the project is under heavy development and some items +discussed in this documentation may stop working without notice (e.g., commands +or configurations). Therefore, we recommend users to not rely on them.
+
This section collects frequently asked questions about Kani. +Please consider opening an issue if you have a question that would like to see here.
+kani::assume(false)
. Why?kani::assume(false)
(or kani::assume(cond)
where cond
is a condition that results in false
in the context of the program), won't cause errors in Kani.
+Instead, such an assumption has the effect of blocking all the symbolic execution paths from the assumption.
+Therefore, all checks after the assumption should appear as UNREACHABLE
.
+That's the expected behavior for kani::assume(false)
in Kani.
If you didn't expect certain checks in a harness to be UNREACHABLE
, we recommend using the kani::cover
macro to determine what conditions are possible in case you've over-constrained the harness.
kani::Arbitrary
trait for a type that's not from my crate, and got the error
+only traits defined in the current crate can be implemented for types defined outside of the crate
.
+What does this mean? What can I do?This error is due to a violation of Rust's orphan rules for trait implementations, which are explained here. +In that case, you'll need to write a function that builds an object from non-deterministic variables. +Inside this function you would simply return an arbitrary value by generating arbitrary values for its components.
+For example, let's assume the type you're working with is this enum:
+#[derive(Copy, Clone)]
+pub enum Rating {
+ One,
+ Two,
+ Three,
+}
+
+Then, you can match on a non-deterministic integer (supplied by kani::any
) to return non-deterministic Rating
variants:
pub fn any_rating() -> Rating {
+ match kani::any() {
+ 0 => Rating::One,
+ 1 => Rating::Two,
+ _ => Rating::Three,
+ }
+ }
+
+More details about this option, which also useful in other cases, can be found here.
+If the type comes from std
(Rust's standard library), you can open a request for adding Arbitrary
implementations to the Kani library.
+Otherwise, there are more involved options to consider:
Arbitrary
there.Arbitrary
implementation to the external crate that defines the type.Kani is an open-source verification tool that uses model checking to analyze Rust programs. +Kani is particularly useful for verifying unsafe code blocks in Rust, where the "unsafe superpowers" are unchecked by the compiler. +Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows). +Kani can also prove custom properties provided in the form of user-specified assertions. +As Kani uses model checking, Kani will either prove the property, disprove the +property (with a counterexample), or may run out of resources.
+Kani uses proof harnesses to analyze programs. +Proof harnesses are similar to test harnesses, especially property-based test harnesses.
+Kani is currently under active development. +Releases are published here. +Major changes to Kani are documented in the RFC Book. +We also publish updates on Kani use cases and features on our blog.
+There is support for a fair amount of Rust language features, but not all (e.g., concurrency). +Please see Limitations for a detailed list of supported features.
+Kani releases every two weeks. +As part of every release, Kani will synchronize with a recent nightly release of Rust, and so is generally up-to-date with the latest Rust language features.
+If you encounter issues when using Kani, we encourage you to report them to us.
+ +Kani is an open-source verification tool that uses model checking to analyze Rust programs. +Kani is particularly useful for verifying unsafe code blocks in Rust, where the "unsafe superpowers" are unchecked by the compiler. +Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows). +Kani can also prove custom properties provided in the form of user-specified assertions. +As Kani uses model checking, Kani will either prove the property, disprove the +property (with a counterexample), or may run out of resources.
+Kani uses proof harnesses to analyze programs. +Proof harnesses are similar to test harnesses, especially property-based test harnesses.
+Kani is currently under active development. +Releases are published here. +Major changes to Kani are documented in the RFC Book. +We also publish updates on Kani use cases and features on our blog.
+There is support for a fair amount of Rust language features, but not all (e.g., concurrency). +Please see Limitations for a detailed list of supported features.
+Kani releases every two weeks. +As part of every release, Kani will synchronize with a recent nightly release of Rust, and so is generally up-to-date with the latest Rust language features.
+If you encounter issues when using Kani, we encourage you to report them to us.
+ +