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..72dbd8025918 --- /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 18.04, 20.04 and 22.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:
+cargo build-dev
+
+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:
+pub trait Arbitrarywhere
+ Self: Sized,{
+ // Required method
+ fn any() -> Self;
+
+ // Provided method
+ fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
+ where [(); { _ }]: { ... }
+}
This trait should be used to generate symbolic variables that represent any valid value of +its type.
+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
+#[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 condition over the input values to the
+annotated function and its return value, accessible as a variable called
+result
. 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]
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.
#[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.
+#[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 condition over the input values to the
+annotated function and its return value, accessible as a variable called
+result
. 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: u32, divisor: u32) -> u32 {
+ 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 <= 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 arguments the postcondition
+also has access to the value returned from the function in a variable called
+result
.
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:
#[kani::requires(divisor != 0)]
+#[kani::ensures(result <= dividend)]
+fn my_div(dividend: u32, divisor: u32) -> u32 {
+ 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 = vec![...];
+ 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
.
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
.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::<std::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 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 arbitrary::Arbitrary;
pub use futures::block_on;
pub use futures::block_on_with_spawn;
pub use futures::spawn;
pub use futures::yield_now;
pub use futures::RoundRobin;
kani::Arbitrary
. Tuples of size up to 12 are supported in this
+file.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.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.#[derive(Arbitrary)]
macro.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..c92e39249f1a --- /dev/null +++ b/crates/doc/kani/macro.cover.html @@ -0,0 +1,28 @@ +macro_rules! cover { + () => { ... }; + ($cond:expr $(,)?) => { ... }; + ($cond:expr, $msg:literal) => { ... }; +}
A macro to check if a condition is satisfiable at a specific location in the +code.
+let mut set: BTreeSet<i32> = BTreeSet::new();
+set.insert(kani::any());
+set.insert(kani::any());
+// check if the set can end up with a single element (if both elements
+// inserted were the same)
+kani::cover!(set.len() == 1);
The macro can also be called without any arguments to check if a location is +reachable.
+match e {
+ MyEnum::A => { /* .. */ }
+ MyEnum::B => {
+ // make sure the `MyEnum::B` variant is possible
+ kani::cover!();
+ // ..
+ }
+}
A custom message can also be passed to the macro.
+kani::cover!(x > y, "x can be greater than y")
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..807a26bffaf5 --- /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.
pub fn assert_valid_ptr<T>(ptr: *const T) -> bool
Assert that the pointer is valid for access according to crate::mem conditions 1, 2 and 3.
+Note that an unaligned pointer is still considered valid.
+TODO: Kani should automatically add those checks when a de-reference happens. +https://github.com/model-checking/kani/issues/2975
+This function will either panic or return true
. This is to make it easier to use it in
+contracts.
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.
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.T
. You can …\nThis creates a symbolic valid value of type T
. The value …\nThis module introduces the Arbitrary trait as well as …\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 …\nA macro to check if a condition is satisfiable at a …\nAdd a postcondition to this function.\nThis module contains functions to work with futures (and …\nimplies!(premise => conclusion)
means that if the premise
…\nThis module contains functions useful for checking unsafe …\nDeclaration of an explicit write-set for the annotated …\nMarks a Kani proof harness\nDesignates this function as a harness to check a function …\nSpecifies that a function contains recursion for contract …\nAdd a precondition to this function.\nSpecifies that a proof harness is expected to panic.**\nSelect the SAT solver to use with CBMC for this harness\nSpecify a function/method stub pair to use for proof …\nstub_verified(TARGET)
is a harness attribute (to be used on\nSupport for arbitrary tuples where each element implements …\nSet Loop unwind limit for proof harnesses The attribute …\nThis trait should be used to generate symbolic variables …\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\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 …\nAssert that the pointer is valid for access according to …\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..1677495c7783
--- /dev/null
+++ b/crates/doc/settings.html
@@ -0,0 +1 @@
+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 +
// 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 std::{
+ marker::{PhantomData, PhantomPinned},
+ num::*,
+};
+
+/// This trait should be used to generate symbolic variables that represent any valid value of
+/// its type.
+pub trait Arbitrary
+where
+ Self: Sized,
+{
+ fn any() -> Self;
+ fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
+ // the requirement defined in the where clause must appear on the `impl`'s method `any_array`
+ // but also on the corresponding trait's method
+ where
+ [(); std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:,
+ {
+ [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
+ }
+}
+
+/// The given type can be represented by an unconstrained symbolic value of size_of::<T>.
+macro_rules! trivial_arbitrary {
+ ( $type: ty ) => {
+ impl Arbitrary for $type {
+ #[inline(always)]
+ fn any() -> Self {
+ // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic.
+ unsafe { crate::any_raw_internal::<Self, { std::mem::size_of::<Self>() }>() }
+ }
+ fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
+ where
+ // `generic_const_exprs` requires all potential errors to be reflected in the signature/header.
+ // We must repeat the expression in the header, to make sure that if the body can fail the header will also fail.
+ [(); { std::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:,
+ {
+ unsafe {
+ crate::any_raw_internal::<
+ [Self; MAX_ARRAY_LENGTH],
+ { std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() },
+ >()
+ }
+ }
+ }
+ };
+}
+
+trivial_arbitrary!(u8);
+trivial_arbitrary!(u16);
+trivial_arbitrary!(u32);
+trivial_arbitrary!(u64);
+trivial_arbitrary!(u128);
+trivial_arbitrary!(usize);
+
+trivial_arbitrary!(i8);
+trivial_arbitrary!(i16);
+trivial_arbitrary!(i32);
+trivial_arbitrary!(i64);
+trivial_arbitrary!(i128);
+trivial_arbitrary!(isize);
+
+// We do not constraint floating points values per type spec. Users must add assumptions to their
+// verification code if they want to eliminate NaN, infinite, or subnormal.
+trivial_arbitrary!(f32);
+trivial_arbitrary!(f64);
+
+trivial_arbitrary!(());
+
+impl Arbitrary for bool {
+ #[inline(always)]
+ fn any() -> Self {
+ let byte = u8::any();
+ crate::assume(byte < 2);
+ byte == 1
+ }
+}
+
+/// 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>
+impl Arbitrary for char {
+ #[inline(always)]
+ fn any() -> Self {
+ // Generate an arbitrary u32 and constrain it to make it a valid representation of char.
+ let val = u32::any();
+ crate::assume(val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val));
+ unsafe { char::from_u32_unchecked(val) }
+ }
+}
+
+macro_rules! nonzero_arbitrary {
+ ( $type: ty, $base: ty ) => {
+ impl Arbitrary for $type {
+ #[inline(always)]
+ fn any() -> Self {
+ let val = <$base>::any();
+ crate::assume(val != 0);
+ unsafe { <$type>::new_unchecked(val) }
+ }
+ }
+ };
+}
+
+nonzero_arbitrary!(NonZeroU8, u8);
+nonzero_arbitrary!(NonZeroU16, u16);
+nonzero_arbitrary!(NonZeroU32, u32);
+nonzero_arbitrary!(NonZeroU64, u64);
+nonzero_arbitrary!(NonZeroU128, u128);
+nonzero_arbitrary!(NonZeroUsize, usize);
+
+nonzero_arbitrary!(NonZeroI8, i8);
+nonzero_arbitrary!(NonZeroI16, i16);
+nonzero_arbitrary!(NonZeroI32, i32);
+nonzero_arbitrary!(NonZeroI64, i64);
+nonzero_arbitrary!(NonZeroI128, i128);
+nonzero_arbitrary!(NonZeroIsize, isize);
+
+impl<T, const N: usize> Arbitrary for [T; N]
+where
+ T: Arbitrary,
+ [(); std::mem::size_of::<[T; N]>()]:,
+{
+ fn any() -> Self {
+ T::any_array()
+ }
+}
+
+impl<T> Arbitrary for Option<T>
+where
+ T: Arbitrary,
+{
+ fn any() -> Self {
+ if bool::any() { Some(T::any()) } else { None }
+ }
+}
+
+impl<T, E> Arbitrary for Result<T, E>
+where
+ T: Arbitrary,
+ E: Arbitrary,
+{
+ fn any() -> Self {
+ if bool::any() { Ok(T::any()) } else { Err(E::any()) }
+ }
+}
+
+impl<T: ?Sized> Arbitrary for std::marker::PhantomData<T> {
+ fn any() -> Self {
+ PhantomData
+ }
+}
+
+impl Arbitrary for std::marker::PhantomPinned {
+ fn any() -> Self {
+ PhantomPinned
+ }
+}
+
+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 +
// 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: u32, divisor: u32) -> u32 {
+//! 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`.
+//!
+//! ```ignore
+//! #[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`][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:
+//!
+//! ```
+//! #[ensures(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`][macro@requires]. In addition to the arguments the postcondition
+//! also has access to the value returned from the function in a variable called
+//! `result`.
+//!
+//! 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:
+//!
+//! ```
+//! #[kani::requires(divisor != 0)]
+//! #[kani::ensures(result <= dividend)]
+//! fn my_div(dividend: u32, divisor: u32) -> u32 {
+//! 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.
+//!
+//! ```
+//! #[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.
+//!
+//! ```
+//! #[kani::proof]
+//! #[kani::stub_verified(my_div)]
+//! fn use_div() {
+//! let v = vec![...];
+//! 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`.
+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 +
// 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,
+}
+
+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")]
+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")]
+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 +
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// Helper trait for code generation for `modifies` contracts.
+///
+/// We allow the user to provide us with a pointer-like object that we convert as needed.
+#[doc(hidden)]
+pub trait Pointer<'a> {
+ /// Type of the pointed-to data
+ type Inner;
+
+ /// Used for checking assigns contracts where we pass immutable references to the function.
+ ///
+ /// We're using a reference to self here, because the user can use just a plain function
+ /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it.
+ unsafe fn decouple_lifetime(&self) -> &'a Self::Inner;
+
+ /// used for havocking on replecement of a `modifies` clause.
+ unsafe fn assignable(self) -> &'a mut Self::Inner;
+}
+
+impl<'a, 'b, T> Pointer<'a> for &'b T {
+ type Inner = T;
+ unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
+ std::mem::transmute(*self)
+ }
+
+ #[allow(clippy::transmute_ptr_to_ref)]
+ unsafe fn assignable(self) -> &'a mut Self::Inner {
+ std::mem::transmute(self as *const T)
+ }
+}
+
+impl<'a, 'b, T> Pointer<'a> for &'b mut T {
+ type Inner = T;
+
+ #[allow(clippy::transmute_ptr_to_ref)]
+ unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
+ std::mem::transmute::<_, &&'a T>(self)
+ }
+
+ unsafe fn assignable(self) -> &'a mut Self::Inner {
+ std::mem::transmute(self)
+ }
+}
+
+impl<'a, T> Pointer<'a> for *const T {
+ type Inner = T;
+ unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
+ &**self as &'a T
+ }
+
+ #[allow(clippy::transmute_ptr_to_ref)]
+ unsafe fn assignable(self) -> &'a mut Self::Inner {
+ std::mem::transmute(self)
+ }
+}
+
+impl<'a, T> Pointer<'a> for *mut T {
+ type Inner = T;
+ unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
+ &**self as &'a T
+ }
+
+ #[allow(clippy::transmute_ptr_to_ref)]
+ unsafe fn assignable(self) -> &'a mut Self::Inner {
+ std::mem::transmute(self)
+ }
+}
+
+/// A way to break the ownerhip rules. Only used by contracts where we can
+/// guarantee it is done safely.
+#[inline(never)]
+#[doc(hidden)]
+#[rustc_diagnostic_item = "KaniUntrackedDeref"]
+pub fn untracked_deref<T>(_: &T) -> T {
+ todo!()
+}
+
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 +279 +280 +281 +282 +283 +284 +285 +286 +287 +288 +289 +290 +291 +292 +293 +294 +295 +296 +297 +298 +299 +300 +301 +302 +303 +304 +305 +306 +307 +308 +309 +310 +311 +312 +313 +314 +315 +316 +317 +318 +319 +320 +321 +322 +323 +
// 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)]
+// This is required for the optimized version of `any_array()`
+#![feature(generic_const_exprs)]
+#![allow(incomplete_features)]
+// Used to model simd.
+#![feature(repr_simd)]
+// 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(ptr_metadata)]
+
+pub mod arbitrary;
+#[cfg(feature = "concrete_playback")]
+mod concrete_playback;
+pub mod futures;
+pub mod mem;
+pub mod slice;
+pub mod tuple;
+pub mod vec;
+
+#[doc(hidden)]
+pub mod internal;
+
+mod models;
+
+pub use arbitrary::Arbitrary;
+#[cfg(feature = "concrete_playback")]
+pub use concrete_playback::concrete_playback_run;
+
+#[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::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin};
+
+/// 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.
+///
+/// # Example:
+///
+/// The code snippet below should never panic.
+///
+/// ```rust
+/// let i : i32 = kani::any();
+/// kani::assume(i > 10);
+/// if i < 0 {
+/// panic!("This will never panic");
+/// }
+/// ```
+///
+/// The following code may panic though:
+///
+/// ```rust
+/// let i : i32 = kani::any();
+/// assert!(i < 0, "This may panic and verification should fail.");
+/// kani::assume(i > 10);
+/// ```
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniAssume"]
+#[cfg(not(feature = "concrete_playback"))]
+pub fn assume(cond: bool) {
+ let _ = cond;
+}
+
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniAssume"]
+#[cfg(feature = "concrete_playback")]
+pub fn assume(cond: bool) {
+ assert!(cond, "`kani::assume` should always hold");
+}
+
+/// `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)
+ };
+}
+
+/// Creates an assertion of the specified condition and message.
+///
+/// # Example:
+///
+/// ```rust
+/// let x: bool = kani::any();
+/// let y = !x;
+/// kani::assert(x || y, "ORing a boolean variable with its negation must be true")
+/// ```
+#[cfg(not(feature = "concrete_playback"))]
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniAssert"]
+pub const fn assert(cond: bool, msg: &'static str) {
+ let _ = cond;
+ let _ = msg;
+}
+
+#[cfg(feature = "concrete_playback")]
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniAssert"]
+pub const fn assert(cond: bool, msg: &'static str) {
+ assert!(cond, "{}", msg);
+}
+
+/// Creates a cover property with the specified condition and message.
+///
+/// # Example:
+///
+/// ```rust
+/// 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:
+/// - SATISFIED: if Kani found an execution that satisfies the condition
+/// - UNSATISFIABLE: if Kani proved that the condition cannot be satisfied
+/// - UNREACHABLE: if Kani proved that the cover property itself is unreachable (i.e. it is vacuously UNSATISFIABLE)
+///
+/// This function is called by the [`cover!`] macro. The macro is more
+/// convenient to use.
+///
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniCover"]
+pub const fn cover(_cond: bool, _msg: &'static str) {}
+
+/// 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.
+///
+/// # Example:
+///
+/// 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.
+///
+/// ```rust
+/// let inputA = kani::any::<std::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`.
+#[rustc_diagnostic_item = "KaniAny"]
+#[inline(always)]
+pub fn any<T: Arbitrary>() -> T {
+ T::any()
+}
+
+/// This function is only used for function contract instrumentation.
+/// It behaves exaclty like `kani::any<T>()`, except it will check for the trait bounds
+/// at compilation time. It allows us to avoid type checking errors while using function
+/// contracts only for verification.
+#[rustc_diagnostic_item = "KaniAnyModifies"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn any_modifies<T>() -> T {
+ // This function should not be reacheable.
+ // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
+ // otherwise, this might not be properly instantiate. We mark this as unreachable to make
+ // sure Kani doesn't report any false positives.
+ unreachable!()
+}
+
+/// 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.
+///
+/// # Example:
+///
+/// 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.
+///
+/// ```rust
+/// 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`.
+#[inline(always)]
+pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
+ let result = T::any();
+ assume(f(&result));
+ result
+}
+
+/// This function creates a symbolic value of type `T`. This may result in an invalid value.
+///
+/// # Safety
+///
+/// This function is unsafe and it may represent invalid `T` values which can lead to many
+/// undesirable undefined behaviors. Because of that, this function can only be used
+/// internally when we can guarantee that the type T has no restriction regarding its bit level
+/// representation.
+///
+/// This function is also used to find concrete values in the CBMC output trace
+/// and return those concrete values in concrete playback mode.
+///
+/// Note that SIZE_T must be equal the size of type T in bytes.
+#[inline(never)]
+#[cfg(not(feature = "concrete_playback"))]
+pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
+ any_raw_inner::<T>()
+}
+
+#[inline(never)]
+#[cfg(feature = "concrete_playback")]
+pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
+ concrete_playback::any_raw_internal::<T, SIZE_T>()
+}
+
+/// This low-level function returns nondet bytes of size T.
+#[rustc_diagnostic_item = "KaniAnyRaw"]
+#[inline(never)]
+#[allow(dead_code)]
+fn any_raw_inner<T>() -> T {
+ kani_intrinsic()
+}
+
+/// Function used to generate panic with a static message as this is the only one currently
+/// supported by Kani display.
+///
+/// During verification this will get replaced by `assert(false)`. For concrete executions, we just
+/// invoke the regular `std::panic!()` function. This function is used by our standard library
+/// overrides, but not the other way around.
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniPanic"]
+#[doc(hidden)]
+pub const fn panic(message: &'static str) -> ! {
+ panic!("{}", message)
+}
+
+/// An empty body that can be used to define Kani intrinsic functions.
+///
+/// A Kani intrinsic is a function that is interpreted by Kani compiler.
+/// While we could use `unreachable!()` or `panic!()` as the body of a kani intrinsic
+/// function, both cause Kani to produce a warning since we don't support caller location.
+/// (see https://github.com/model-checking/kani/issues/2010).
+///
+/// This function is dead, since its caller is always handled via a hook anyway,
+/// so we just need to put a body that rustc does not complain about.
+/// An infinite loop works out nicely.
+fn kani_intrinsic<T>() -> T {
+ #[allow(clippy::empty_loop)]
+ loop {}
+}
+/// A macro to check if a condition is satisfiable at a specific location in the
+/// code.
+///
+/// # Example 1:
+///
+/// ```rust
+/// let mut set: BTreeSet<i32> = BTreeSet::new();
+/// set.insert(kani::any());
+/// set.insert(kani::any());
+/// // check if the set can end up with a single element (if both elements
+/// // inserted were the same)
+/// kani::cover!(set.len() == 1);
+/// ```
+/// The macro can also be called without any arguments to check if a location is
+/// reachable.
+///
+/// # Example 2:
+///
+/// ```rust
+/// match e {
+/// MyEnum::A => { /* .. */ }
+/// MyEnum::B => {
+/// // make sure the `MyEnum::B` variant is possible
+/// kani::cover!();
+/// // ..
+/// }
+/// }
+/// ```
+///
+/// A custom message can also be passed to the macro.
+///
+/// # Example 3:
+///
+/// ```rust
+/// kani::cover!(x > y, "x can be greater than y")
+/// ```
+#[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);
+ };
+}
+
+// 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;
+
+// Kani proc macros must be in a separate crate
+pub use kani_macros::*;
+
+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 +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 +
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! 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)
+//!
+//! 1. A null pointer is never valid, not even for accesses of size zero.
+//! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer
+//! be dereferenceable: the memory range of the given size starting at the pointer must all be
+//! within the bounds of a single allocated object. Note that in Rust, every (stack-allocated)
+//! variable is considered a separate allocated object.
+//! Even for operations of size zero, the pointer must not be pointing to deallocated memory,
+//! i.e., deallocation makes pointers invalid even for zero-sized operations.
+//! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized
+//! accesses, even if some memory happens to exist at that address and gets deallocated.
+//! This corresponds to writing your own allocator: allocating zero-sized objects is not very
+//! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is
+//! `NonNull::dangling`.
+//! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic
+//! operations used to synchronize between threads.
+//! This means it is undefined behavior to perform two concurrent accesses to the same location
+//! from different threads unless both accesses only read from memory.
+//! Notice that this explicitly includes `read_volatile` and `write_volatile`:
+//! Volatile accesses cannot be used for inter-thread synchronization.
+//! 5. The result of casting a reference to a pointer is valid for as long as the underlying
+//! object is live and no reference (just raw pointers) is used to access the same memory.
+//! That is, reference and pointer accesses cannot be interleaved.
+//!
+//! 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.
+
+use crate::kani_intrinsic;
+use crate::mem::private::Internal;
+use std::mem::{align_of, size_of};
+use std::ptr::{DynMetadata, NonNull, Pointee};
+
+/// Assert that the pointer is valid for access according to [crate::mem] conditions 1, 2 and 3.
+///
+/// Note that an unaligned pointer is still considered valid.
+///
+/// TODO: Kani should automatically add those checks when a de-reference happens.
+/// <https://github.com/model-checking/kani/issues/2975>
+///
+/// This function will either panic or return `true`. This is to make it easier to use it in
+/// contracts.
+#[crate::unstable(
+ feature = "mem-predicates",
+ issue = 2690,
+ reason = "experimental memory predicate API"
+)]
+pub fn assert_valid_ptr<T>(ptr: *const T) -> bool
+where
+ T: ?Sized,
+ <T as Pointee>::Metadata: PtrProperties<T>,
+{
+ crate::assert(!ptr.is_null(), "Expected valid pointer, but found `null`");
+
+ let (thin_ptr, metadata) = ptr.to_raw_parts();
+ let sz = metadata.pointee_size(Internal);
+ if sz == 0 {
+ true // ZST pointers are always valid
+ } else {
+ // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be
+ // stubbed.
+ crate::assert(
+ is_read_ok(thin_ptr, sz),
+ "Expected valid pointer, but found dangling pointer",
+ );
+ true
+ }
+}
+
+mod private {
+ /// Define like this to restrict usage of PtrProperties functions outside Kani.
+ #[derive(Copy, Clone)]
+ pub struct Internal;
+}
+
+/// Trait that allow us to extract information from pointers without de-referencing them.
+#[doc(hidden)]
+pub trait PtrProperties<T: ?Sized> {
+ fn pointee_size(&self, _: Internal) -> usize;
+
+ fn min_alignment(&self, _: Internal) -> usize;
+
+ fn dangling(&self, _: Internal) -> *const ();
+}
+
+/// Get the information for sized types (they don't have metadata).
+impl<T> PtrProperties<T> for () {
+ fn pointee_size(&self, _: Internal) -> usize {
+ size_of::<T>()
+ }
+
+ fn min_alignment(&self, _: Internal) -> usize {
+ align_of::<T>()
+ }
+
+ fn dangling(&self, _: Internal) -> *const () {
+ NonNull::<T>::dangling().as_ptr() as *const _
+ }
+}
+
+/// Get the information from the str metadata.
+impl PtrProperties<str> for usize {
+ #[inline(always)]
+ fn pointee_size(&self, _: Internal) -> usize {
+ *self
+ }
+
+ /// String slices are a UTF-8 representation of characters that have the same layout as slices
+ /// of type [u8].
+ /// <https://doc.rust-lang.org/reference/type-layout.html#str-layout>
+ fn min_alignment(&self, _: Internal) -> usize {
+ align_of::<u8>()
+ }
+
+ fn dangling(&self, _: Internal) -> *const () {
+ NonNull::<u8>::dangling().as_ptr() as _
+ }
+}
+
+/// Get the information from the slice metadata.
+impl<T> PtrProperties<[T]> for usize {
+ fn pointee_size(&self, _: Internal) -> usize {
+ *self * size_of::<T>()
+ }
+
+ fn min_alignment(&self, _: Internal) -> usize {
+ align_of::<T>()
+ }
+
+ fn dangling(&self, _: Internal) -> *const () {
+ NonNull::<T>::dangling().as_ptr() as _
+ }
+}
+
+/// Get the information from the vtable.
+impl<T> PtrProperties<T> for DynMetadata<T>
+where
+ T: ?Sized,
+{
+ fn pointee_size(&self, _: Internal) -> usize {
+ self.size_of()
+ }
+
+ fn min_alignment(&self, _: Internal) -> usize {
+ self.align_of()
+ }
+
+ fn dangling(&self, _: Internal) -> *const () {
+ NonNull::<&T>::dangling().as_ptr() as _
+ }
+}
+
+/// Check if the pointer `_ptr` contains an allocated address of size equal or greater than `_size`.
+///
+/// This function should only be called to ensure a pointer is valid. The opposite isn't true.
+/// I.e.: This function always returns `true` if the pointer is valid.
+/// Otherwise, it returns non-det boolean.
+#[rustc_diagnostic_item = "KaniIsReadOk"]
+#[inline(never)]
+fn is_read_ok(_ptr: *const (), _size: usize) -> bool {
+ kani_intrinsic()
+}
+
+#[cfg(test)]
+mod tests {
+ use super::{assert_valid_ptr, PtrProperties};
+ use crate::mem::private::Internal;
+ use std::fmt::Debug;
+ use std::intrinsics::size_of;
+ use std::mem::{align_of, align_of_val, size_of_val};
+ use std::ptr;
+ use std::ptr::{NonNull, Pointee};
+
+ fn size_of_t<T>(ptr: *const T) -> usize
+ where
+ T: ?Sized,
+ <T as Pointee>::Metadata: PtrProperties<T>,
+ {
+ let (_, metadata) = ptr.to_raw_parts();
+ metadata.pointee_size(Internal)
+ }
+
+ fn align_of_t<T>(ptr: *const T) -> usize
+ where
+ T: ?Sized,
+ <T as Pointee>::Metadata: PtrProperties<T>,
+ {
+ let (_, metadata) = ptr.to_raw_parts();
+ metadata.min_alignment(Internal)
+ }
+
+ #[test]
+ fn test_size_of() {
+ assert_eq!(size_of_t("hi"), size_of_val("hi"));
+ assert_eq!(size_of_t(&0u8), size_of_val(&0u8));
+ assert_eq!(size_of_t(&0u8 as *const dyn std::fmt::Display), size_of_val(&0u8));
+ assert_eq!(size_of_t(&[0u8, 1u8] as &[u8]), size_of_val(&[0u8, 1u8]));
+ assert_eq!(size_of_t(&[] as &[u8]), size_of_val::<[u8; 0]>(&[]));
+ assert_eq!(
+ size_of_t(NonNull::<u32>::dangling().as_ptr() as *const dyn std::fmt::Display),
+ size_of::<u32>()
+ );
+ }
+
+ #[test]
+ fn test_alignment() {
+ assert_eq!(align_of_t("hi"), align_of_val("hi"));
+ assert_eq!(align_of_t(&0u8), align_of_val(&0u8));
+ assert_eq!(align_of_t(&0u32 as *const dyn std::fmt::Display), align_of_val(&0u32));
+ assert_eq!(align_of_t(&[0isize, 1isize] as &[isize]), align_of_val(&[0isize, 1isize]));
+ assert_eq!(align_of_t(&[] as &[u8]), align_of_val::<[u8; 0]>(&[]));
+ assert_eq!(
+ align_of_t(NonNull::<u32>::dangling().as_ptr() as *const dyn std::fmt::Display),
+ align_of::<u32>()
+ );
+ }
+
+ #[test]
+ pub fn test_empty_slice() {
+ let slice_ptr = Vec::<char>::new().as_slice() as *const [char];
+ assert_valid_ptr(slice_ptr);
+ }
+
+ #[test]
+ pub fn test_empty_str() {
+ let slice_ptr = String::new().as_str() as *const str;
+ assert_valid_ptr(slice_ptr);
+ }
+
+ #[test]
+ fn test_dangling_zst() {
+ test_dangling_of_t::<()>();
+ test_dangling_of_t::<[(); 10]>();
+ }
+
+ fn test_dangling_of_t<T>() {
+ let dangling: *const T = NonNull::<T>::dangling().as_ptr();
+ assert_valid_ptr(dangling);
+
+ let vec_ptr = Vec::<T>::new().as_ptr();
+ assert_valid_ptr(vec_ptr);
+ }
+
+ #[test]
+ #[should_panic(expected = "Expected valid pointer, but found `null`")]
+ fn test_null_fat_ptr() {
+ assert_valid_ptr(ptr::null::<char>() as *const dyn Debug);
+ }
+
+ #[test]
+ #[should_panic(expected = "Expected valid pointer, but found `null`")]
+ fn test_null_char() {
+ assert_valid_ptr(ptr::null::<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 +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 +
// 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 + 7) / 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.clone())) },
+ 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.clone())) };
+ 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 +
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+use crate::{any, assume};
+
+/// 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.
+///
+/// # Example:
+///
+/// ```rust
+/// 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<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T] {
+ let (from, to) = any_range::<LENGTH>();
+ &arr[from..to]
+}
+
+/// A mutable version of the previous function
+pub fn any_slice_of_array_mut<T, const LENGTH: usize>(arr: &mut [T; LENGTH]) -> &mut [T] {
+ let (from, to) = any_range::<LENGTH>();
+ &mut arr[from..to]
+}
+
+fn any_range<const LENGTH: usize>() -> (usize, usize) {
+ let from: usize = any();
+ let to: usize = any();
+ assume(to <= LENGTH);
+ assume(from <= to);
+ (from, to)
+}
+
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 +
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Support for arbitrary tuples where each element implements
+//! `kani::Arbitrary`. Tuples of size up to 12 are supported in this
+//! file.
+
+use crate::Arbitrary;
+
+/// This macro implements `kani::Arbitrary` on a tuple whose elements
+/// already implement `kani::Arbitrary` by running `kani::any()` on
+/// each index of the tuple.
+macro_rules! tuple {
+ ($($typ:ident),*) => {
+ impl<$($typ : Arbitrary),*> Arbitrary for ($($typ,)*) {
+ #[inline(always)]
+ fn any() -> Self {
+ ($(crate::any::<$typ>(),)*)
+ }
+ }
+ }
+}
+
+tuple!(A);
+tuple!(A, B);
+tuple!(A, B, C);
+tuple!(A, B, C, D);
+tuple!(A, B, C, D, E);
+tuple!(A, B, C, D, E, F);
+tuple!(A, B, C, D, E, F, G);
+tuple!(A, B, C, D, E, F, G, H);
+tuple!(A, B, C, D, E, F, G, H, I);
+tuple!(A, B, C, D, E, F, G, H, I, J);
+tuple!(A, B, C, D, E, F, G, H, I, J, K);
+tuple!(A, B, C, D, E, F, G, H, I, J, K, L);
+
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 +
// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+use crate::{any, any_where, Arbitrary};
+
+/// 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,
+ [(); std::mem::size_of::<[T; MAX_LENGTH]>()]:,
+{
+ 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,
+ [(); std::mem::size_of::<[T; EXACT_LENGTH]>()]:,
+{
+ 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:
+When the result of a certain check comes back as a FAILURE
,
+Kani offers different options to help debug:
--concrete-playback
. This experimental feature generates a Rust unit test case that plays back a failing
+proof harness using a concrete counterexample.--visualize
. This feature generates an HTML text-based trace that
+enumerates the execution steps leading to the check failure.When concrete playback is enabled, Kani will generate unit tests for assertions that failed during verification, +as well as cover statements that are reachable.
+These tests can then be executed using Kani's playback subcommand.
+In order to enable this feature, run Kani with the -Z concrete-playback --concrete-playback=[print|inplace]
flag.
+After getting a verification failure, Kani will generate a Rust unit test case that plays back a failing
+proof harness with a concrete counterexample.
+The concrete playback modes mean the following:
print
: Kani will just print the unit test to stdout.
+You will then need to copy this unit test into the same module as your proof harness.
+This is also helpful if you just want to quickly find out which values were assigned by kani::any()
calls.inplace
: Kani will automatically copy the unit test into your source code.
+Before running this mode, you might find it helpful to have your existing code committed to git
.
+That way, you can easily remove the unit test with git revert
.
+Note that Kani will not copy the unit test into your source code if it detects
+that the exact same test already exists.After the unit test is in your source code, you can run it with the playback
subcommand.
+To debug it, there are a couple of options:
To manually compile and run the test, you can use Kani's playback
subcommand:
cargo kani playback -Z concrete-playback -- ${unit_test_func_name}
+
+The output from this command is similar to cargo test
.
+The output will have a line in the beginning like
+Running unittests {files} ({binary})
.
You can further debug the binary with tools like rust-gdb
or lldb
.
Running kani -Z concrete-playback --concrete-playback=print
on the following source file:
#[kani::proof]
+fn proof_harness() {
+ let a: u8 = kani::any();
+ let b: u16 = kani::any();
+ assert!(a / 2 * 2 == a &&
+ b / 2 * 2 == b);
+}
+
+yields a concrete playback Rust unit test similar to the one below:
+#[test]
+fn kani_concrete_playback_proof_harness_16220658101615121791() {
+ let concrete_vals: Vec<Vec<u8>> = vec![
+ // 133
+ vec![133],
+ // 35207
+ vec![135, 137],
+ ];
+ kani::concrete_playback_run(concrete_vals, proof_harness);
+}
+
+Here, 133
and 35207
are the concrete values that, when substituted for a
and b
,
+cause an assertion failure.
+vec![135, 137]
is the byte array representation of 35207
.
This feature is experimental and is therefore subject to change. +If you have ideas for improving the user experience of this feature, +please add them to this GitHub issue. +We are tracking the existing feature requests in +this GitHub milestone.
+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.
+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.
+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.
+ +