diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 838ff8855840..6a176aaf20a6 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -562,7 +562,14 @@ impl Expr { // For variadic functions, all named arguments must match the type of their formal param. // Extra arguments (e.g the ... args) can have any type. fn typecheck_named_args(parameters: &[Parameter], arguments: &[Expr]) -> bool { - parameters.iter().zip(arguments.iter()).all(|(p, a)| a.typ() == p.typ()) + parameters.iter().zip(arguments.iter()).all(|(p, a)| { + if a.typ() == p.typ() { + true + } else { + tracing::error!(param=?p.typ(), arg=?a.typ(), "Argument doesn't check"); + false + } + }) } if function.typ().is_code() { diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index f76437405757..6827f93f75e3 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -3,9 +3,7 @@ - [Getting started](./getting-started.md) - [Installation](./install-guide.md) - [Building from source](./build-from-source.md) - - [Usage](./usage.md) - - [On a single file](./kani-single-file.md) - - [On a package](./cargo-kani.md) + - [Using Kani](./usage.md) - [Verification results](./verification-results.md) - [Tutorial](./kani-tutorial.md) diff --git a/docs/src/build-from-source.md b/docs/src/build-from-source.md index 6f0b48d201e2..baf986895b48 100644 --- a/docs/src/build-from-source.md +++ b/docs/src/build-from-source.md @@ -29,15 +29,15 @@ cd kani git submodule update --init ./scripts/setup/ubuntu/install_deps.sh ./scripts/setup/ubuntu/install_cbmc.sh -./scripts/setup/install_viewer.sh 3.5 -./scripts/setup/install_rustup.sh +./scripts/setup/install_viewer.sh # If you haven't already: +./scripts/setup/install_rustup.sh source $HOME/.cargo/env ``` ### Install dependencies on macOS -Support is available for macOS 10.15. You need to have [Homebrew](https://brew.sh/) installed already. +Support is available for macOS 10.15+. You need to have [Homebrew](https://brew.sh/) installed already. ``` # git clone git@github.com:model-checking/kani.git @@ -46,9 +46,9 @@ cd kani git submodule update --init ./scripts/setup/macos-10.15/install_deps.sh ./scripts/setup/macos-10.15/install_cbmc.sh -./scripts/setup/install_viewer.sh 3.5 -./scripts/setup/install_rustup.sh +./scripts/setup/install_viewer.sh # If you haven't already: +./scripts/setup/install_rustup.sh source $HOME/.cargo/env ``` @@ -74,7 +74,7 @@ All Kani regression tests completed successfully. ## Adding Kani to your path -To use Kani from anywhere, add the Kani scripts to your path: +To use a locally-built Kani from anywhere, add the Kani scripts to your path: ```bash export PATH=$(pwd)/scripts:$PATH diff --git a/docs/src/cargo-kani.md b/docs/src/cargo-kani.md index ecc53ec0fd75..3fed4948489a 100644 --- a/docs/src/cargo-kani.md +++ b/docs/src/cargo-kani.md @@ -1,32 +1,3 @@ # Usage on a package -Kani is also integrated with `cargo` and can be invoked from a crate directory as follows: - -```bash -cargo kani []* -``` - -`cargo kani` supports all `kani` arguments. - -`cargo kani` is the recommended approach for using Kani on a project, due to its -ability to handle external dependencies and the option add configurations via the `Cargo.toml` file. - -If your proof harness is placed under `tests/`, you will need to run -`cargo kani` with the `--tests` for Kani to be able to find your -harness. - -## Configuration - -Users can add a default configuration to the `Cargo.toml` file for running harnesses in a package. -Kani will extract any arguments from these sections: - * `[kani]` - * `[workspace.metadata.kani]` - * `[package.metadata.kani]` - -For example, say you want to set a loop unwinding bound of `5` for all the harnesses in a package. -You can achieve this by adding the following lines to the package's `Cargo.toml`: - -```toml -[package.metadata.kani] -flags = { default-unwind = "5" } -``` +[See here](./usage.md#usage-on-a-package) diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md index 0cd9962799b9..35bbf483209d 100644 --- a/docs/src/getting-started.md +++ b/docs/src/getting-started.md @@ -2,17 +2,20 @@ Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs. Kani is particularly useful for verifying unsafe code in Rust, where many of the Rust’s usual guarantees are no longer checked 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., panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows). +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. -Kani uses proof harnesses to analyze programs. Proof harnesses are similar to test harnesses, especially property-based test harnesses. +Kani uses proof harnesses to analyze programs. +Proof harnesses are similar to test harnesses, especially property-based test harnesses. ## Project Status -Kani is currently under active development. Releases are published [here](https://github.com/model-checking/kani/releases). +Kani is currently under active development. +Releases are published [here](https://github.com/model-checking/kani/releases). There is support for a fair amount of Rust language features, but not all (e.g., concurrency). Please see [Limitations - Rust feature support](./rust-feature-support.md) for a detailed list of supported features. -Kani usually synchronizes with the nightly release of Rust every two weeks, and so is generally up-to-date with the latest Rust language 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](https://github.com/model-checking/kani/issues/new/choose). diff --git a/docs/src/kani-single-file.md b/docs/src/kani-single-file.md index 8683e22a8f15..2f6ac118a02a 100644 --- a/docs/src/kani-single-file.md +++ b/docs/src/kani-single-file.md @@ -1,40 +1,3 @@ # Usage on a single file -For small examples or initial learning, it's very common to run Kani on just one source file. - -The command line format for invoking Kani directly is the following: - -``` -kani filename.rs []* -``` - -For example, - -``` -kani example.rs -``` - -runs Kani on all the proof harnesses from file `example.rs`. -A proof harness is simply a function with the `#[kani::proof]` annotation. - -## Common arguments - -The most common `kani` arguments are the following: - - * `--harness `: By default, Kani checks all proof harnesses it finds. You - can switch to checking a single harness using this flag. - - * `--default-unwind `: Set a global upper [loop - unwinding](./tutorial-loop-unwinding.md) bound on all loops. This can force - termination when CBMC tries to unwind loops indefinitely. - - * `--output-format `: By default (`regular`), Kani - post-processes CBMC's output to produce more comprehensible results. In - contrast, `terse` outputs only a summary of these results, and `old` forces - Kani to emit the original output from CBMC. - - * `--visualize`: Generates an HTML report in the local directory accessible - through `report/html/index.html`. This report shows coverage information and - provides traces (i.e., counterexamples) for each failure found by Kani. - -Run `kani --help` to see a complete list of arguments. +[See here](./usage.md#usage-on-a-single-crate) diff --git a/docs/src/tool-comparison.md b/docs/src/tool-comparison.md index cfbf86e16383..495244a9ad1b 100644 --- a/docs/src/tool-comparison.md +++ b/docs/src/tool-comparison.md @@ -16,7 +16,7 @@ Property testing is often quite effective, but the engine can't fully prove the **Model checking** is similar to these techniques in how you use them, but it's non-random and exhaustive (though often only up to some bound on input or problem size). Thus, properties checked with a model checker are effectively proofs. Instead of naively trying all possible _concrete_ inputs (which could be infeasible and blow up exponentially), model checkers like Kani will cleverly encode program traces as _symbolic_ "[SAT](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem)/[SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)" problems, and hand them off to SAT/SMT solvers. -Again, SAT/SMT solving is an [NP-complete](https://en.wikipedia.org/wiki/NP-completeness) problem, but most practical programs can be model- checked within milliseconds to seconds (with notable exceptions: you can easily try to reverse a cryptographic hash with a model checker, but good luck getting it to terminate!) +SAT/SMT solving is an [NP-complete](https://en.wikipedia.org/wiki/NP-completeness) problem, but many practical programs can be model-checked within milliseconds to seconds (with notable exceptions: you can easily try to reverse a cryptographic hash with a model checker, but good luck getting it to terminate!) Model checking allows you to prove non-trivial properties about programs, and check those proofs in roughly the same amount of time as a traditional test suite would take to run. The downside is many types of properties can quickly become "too large" to practically model-check, and so writing "proof harnesses" (very similar to property tests and fuzzer harnesses) requires some skill to understand why the solver is not terminating and fix the structure of the problem you're giving it so that it does. diff --git a/docs/src/tutorial-real-code.md b/docs/src/tutorial-real-code.md index 9ccfb52d396e..c4bad5a2d82e 100644 --- a/docs/src/tutorial-real-code.md +++ b/docs/src/tutorial-real-code.md @@ -40,12 +40,12 @@ Sometimes the best place to start won't be your code, but the code that you depe If it's used by more projects that just yours, it will be valuable to more people, too! 3. Find well-tested code. -Code structure changes to make code more unit-testable will make it more provable, too. +When you make changes to improve the unit-testability of code, that also makes it more amenable to proof, too. Here are some things to avoid, when starting out: 1. Lots of loops, or at least nested loops. -As we saw in the last section, right now we often need to put upper bounds on these to make more limited claims. +As we saw in the [tutorial](./tutorial-loop-unwinding.md), right now we often need to put upper bounds on loops to make more limited claims. 2. Inductive data structures. These are data structures with unbounded size (e.g., linked lists or trees.) @@ -73,12 +73,21 @@ A first proof will likely start in the following form: Running Kani on this simple starting point will help figure out: -1. What unexpected constraints might be needed on your inputs to avoid "expected" failures. -2. Whether you're over-constrained. Check the coverage report using `--visualize`. Ideally you'd see 100% coverage, and if not, it's usually because now you've over-constrained the inputs. +1. What unexpected constraints might be needed on your inputs (using `kani::assume`) to avoid "expected" failures. +2. Whether you're over-constrained. Check the coverage report using `--visualize`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs). 3. Whether Kani will support all the Rust features involved. 4. Whether you've started with a tractable problem. -(If the problem is initially intractable, try `--default-unwind 1` and see if you can follow the techniques in the previous section to put a bound on the problem.) +(Remember to try setting `#[kani::unwind(1)]` to force early termination and work up from there.) -Once you've got something working, the next step is to prove more interesting properties than what Kani covers by default. +Once you've got something working, the next step is to prove more interesting properties than just what Kani covers by default. You accomplish this by adding new assertions (not just in your harness, but also to the code being run). Even if a proof harness has no post-conditions being asserted directly, the assertions encountered along the way can be meaningful proof results by themselves. + + +## Examples of the use of Kani + +On the [Kani blog](https://model-checking.github.io/kani-verifier-blog/), we've documented worked examples of applying Kani: + +1. [The `Rectangle` example of the Rust Book](https://model-checking.github.io/kani-verifier-blog/2022/05/04/announcing-the-kani-rust-verifier-project.html) +2. [A Rust standard library CVE](https://model-checking.github.io/kani-verifier-blog/2022/06/01/using-the-kani-rust-verifier-on-a-rust-standard-library-cve.html) +3. [Verifying a part of Firecracker](https://model-checking.github.io/kani-verifier-blog/2022/07/13/using-the-kani-rust-verifier-on-a-firecracker-example.html) diff --git a/docs/src/undefined-behaviour.md b/docs/src/undefined-behaviour.md index 1b43299a5c47..8d883b1e4152 100644 --- a/docs/src/undefined-behaviour.md +++ b/docs/src/undefined-behaviour.md @@ -35,7 +35,7 @@ A non-exhaustive list of these, based on the non-exhaustive list from the [Rust * Calling a function with the wrong call ABI or unwinding from a function with the wrong unwind ABI. * Kani relies on `rustc` to check for this case. * Producing an invalid value, even in private fields and locals. - * Kani provides a [mechanism](./tutorial-nondeterministic-variables.md#safe-nondeterministic-variables-for-custom-types) `is_valid()` which users can use to check validity of objects, but it does not currently apply to all types. + * Kani [won't create invalid values](./tutorial-nondeterministic-variables.md) with `kani::any()` but it also won't complain if you `transmute` an invalid value to a Rust type (for example, a `0` to `NonZeroU32`). * Incorrect use of inline assembly. * Kani does not support inline assembly. * Using uninitialized memory. @@ -46,5 +46,3 @@ Kani makes a best-effort attempt to detect some cases of UB: * Kani can detect invalid dereferences, but may not detect them in [place expression context](https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions). * Invoking undefined behavior via compiler intrinsics. * See [current support for compiler intrinsics](./rust-feature-support/intrinsics.md). -* Producing an invalid value, even in private fields and locals. - * Kani provides a [mechanism](./tutorial-nondeterministic-variables.md#safe-nondeterministic-variables-for-custom-types) `is_valid()` which users can use to check validity of objects, but it does not currently apply to all types. diff --git a/docs/src/usage.md b/docs/src/usage.md index a53a648ff152..8db4d1273a7b 100644 --- a/docs/src/usage.md +++ b/docs/src/usage.md @@ -1,12 +1,94 @@ -# Usage +# Using Kani At present, Kani can used in two ways: - * [On a single file](./kani-single-file.md) with the `kani` command. - * [On a package](./cargo-kani.md) with the `cargo-kani` command. -Running [Kani on a single file](./kani-single-file.md) is quite useful for small -examples or projects that don't use `cargo`. + * [On a single crate](#usage-on-a-single-crate) with the `kani` command. + * [On a Cargo package](#usage-on-a-package) with the `cargo kani` command. -However, if you plan to integrate Kani in your projects, the recommended -approach is to use [Kani on a package](./cargo-kani.md) because of its ability -to handle external dependencies. +If you plan to integrate Kani in your projects, the recommended approach is to use `cargo kani`. +If you're already using cargo, this will handle dependencies automatically, and it can be configured (if needed) in `Cargo.toml`. +But `kani` is useful for small examples/tests. + +## Usage on a package + +Kani is integrated with `cargo` and can be invoked from a package as follows: + +```bash +cargo kani [OPTIONS] +``` + +This works like `cargo test` except that it will analyze all proof harnesses instead of running all test harnesses. + +## Common command line flags + +Common to both `kani` and `cargo kani` are many command-line flags: + + * `--visualize`: Generates an HTML report showing coverage information and providing traces (i.e., counterexamples) for each failure found by Kani. + + * `--tests`: Build in "[test mode](https://doc.rust-lang.org/rustc/tests/index.html)", i.e. with `cfg(test)` set and `dev-dependencies` available (when using `cargo kani`). + + * `--harness `: By default, Kani checks all proof harnesses it finds. + You can switch to checking a single harness using this flag. + + * `--default-unwind `: Set a default global upper [loop unwinding](./tutorial-loop-unwinding.md) bound for proof harnesses. + This can force termination when CBMC tries to unwind loops indefinitely. + +Run `cargo kani --help` to see a complete list of arguments. + +## Usage on a single crate + +For small examples or initial learning, it's very common to run Kani on just one source file. +The command line format for invoking Kani directly is the following: + +``` +kani filename.rs [OPTIONS] +``` + +This will build `filename.rs` and run all proof harnesses found within. + +## Configuration in `Cargo.toml` + +Users can add a default configuration to the `Cargo.toml` file for running harnesses in a package. +Kani will extract any arguments from these sections: + + * `[workspace.metadata.kani.flags]` + * `[package.metadata.kani.flags]` + +For example, if you want to set a default loop unwinding bound (when it's not otherwise specified), you can achieve this by adding the following lines to the package's `Cargo.toml`: + +```toml +[package.metadata.kani.flags] +default-unwind = 1 +``` + +The options here are the same as on the command line (`cargo kani --help`), and flags (that is, command line arguments that don't take a value) are enabled by setting them to `true`. + +## The build process + +When Kani builds your code, it does two important things: + +1. It sets `cfg(kani)`. +2. It injects the `kani` crate. + +A proof harness (which you can [learn more about in the tutorial](./kani-tutorial.md)), is a function annotated with `#[kani::proof]` much like a test is annotated with `#[test]`. +But you may experience a similar problem using Kani as you would with `dev-dependencies`: if you try writing `#[kani::proof]` directly in your code, `cargo build` will fail because it doesn't know what the `kani` crate is. + +This is why we recommend the same conventions as are used when writing tests in Rust: wrap your proof harnesses in `cfg(kani)` conditional compilation: + +```rust +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::proof] + pub fn check_something() { + // .... + } +} +``` + +This will ensure that a normal build of your code will be completely unaffected by anything Kani-related. + +This conditional compilation with `cfg(kani)` (as seen above) is still required for Kani proofs placed under `tests/`. +When this code is built by `cargo test`, the `kani` crate is not available, and so it would otherwise cause build failures. +(Whereas the use of `dev-dependencies` under `tests/` does not need to be gated with `cfg(test)` since that code is already only built when testing.) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 3f97e688944c..c86c4a50b030 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -1,9 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This file contains the code that acts as a wrapper to create the new assert and related statements +//! This module is the central location for handling assertions and assumptions in Kani. + +use crate::codegen_cprover_gotoc::utils; use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::{Expr, Location, Stmt}; +use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt}; +use rustc_span::Span; use std::convert::AsRef; use strum_macros::{AsRefStr, EnumString}; @@ -39,6 +42,7 @@ impl PropertyClass { } impl<'tcx> GotocCtx<'tcx> { + /// Generates a CBMC assertion. Note: Does _NOT_ assume. pub fn codegen_assert( &self, cond: Expr, @@ -51,6 +55,7 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::assert(cond, property_name, message, loc) } + /// Generates a CBMC assertion, followed by an assumption of the same condition. pub fn codegen_assert_assume( &self, cond: Expr, @@ -66,6 +71,7 @@ impl<'tcx> GotocCtx<'tcx> { ) } + /// A shorthand for generating a CBMC assert-false. TODO: This should probably be eliminated! pub fn codegen_assert_false( &self, property_class: PropertyClass, @@ -76,4 +82,49 @@ impl<'tcx> GotocCtx<'tcx> { let property_name = property_class.as_str(); Stmt::assert_false(property_name, message, loc) } + + /// Kani hooks function calls to `panic` and calls this intead. + pub fn codegen_panic(&self, span: Option, fargs: Vec) -> Stmt { + // CBMC requires that the argument to the assertion must be a string constant. + // If there is one in the MIR, use it; otherwise, explain that we can't. + assert!(!fargs.is_empty(), "Panic requires a string message"); + let msg = utils::extract_const_message(&fargs[0]).unwrap_or(String::from( + "This is a placeholder message; Kani doesn't support message formatted at runtime", + )); + + self.codegen_fatal_error(PropertyClass::Assertion, &msg, span) + } + + /// Generate code for fatal error which should trigger an assertion failure and abort the + /// execution. + pub fn codegen_fatal_error( + &self, + property_class: PropertyClass, + msg: &str, + span: Option, + ) -> Stmt { + let loc = self.codegen_caller_span(&span); + Stmt::block( + vec![ + self.codegen_assert_false(property_class, msg, loc), + BuiltinFn::Abort.call(vec![], loc).as_stmt(loc), + ], + loc, + ) + } + + /// Generate code to cover the given condition at the current location + pub fn codegen_cover(&self, cond: Expr, msg: &str, span: Option) -> Stmt { + let loc = self.codegen_caller_span(&span); + // Should use Stmt::cover, but currently this doesn't work with CBMC + // unless it is run with '--cover cover' (see + // https://github.com/diffblue/cbmc/issues/6613). So for now use + // assert(!cond). + self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc) + } + + /// Generate code to cover the current location + pub fn codegen_cover_loc(&self, msg: &str, span: Option) -> Stmt { + self.codegen_cover(Expr::bool_true(), msg, span) + } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index f6bdd2725df4..9298c8851eea 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs @@ -1,12 +1,16 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This file contains functions related to codegenning MIR blocks into gotoc - use crate::codegen_cprover_gotoc::GotocCtx; use rustc_middle::mir::{BasicBlock, BasicBlockData}; impl<'tcx> GotocCtx<'tcx> { + /// Generates Goto-C for a basic block. + /// + /// A MIR basic block consists of 0 or more statements followed by a terminator. + /// + /// This function does not return a value, but mutates state with + /// `self.current_fn_mut().push_onto_block(...)` pub fn codegen_block(&mut self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) { self.current_fn_mut().set_current_bb(bb); let label: String = self.current_fn().find_label(&bb); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index c3bc7974dd74..f12a88c9ed3e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -10,7 +10,6 @@ use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{self, Ty}; use rustc_middle::ty::{Instance, InstanceDef}; use rustc_span::Span; -use rustc_target::abi::InitKind; use tracing::{debug, warn}; macro_rules! emit_concurrency_warning { @@ -767,9 +766,7 @@ impl<'tcx> GotocCtx<'tcx> { // Then we check if the type allows "raw" initialization for the cases // where memory is zero-initialized or entirely uninitialized - if intrinsic == "assert_zero_valid" - && !layout.might_permit_raw_init(self, InitKind::Zero, false) - { + if intrinsic == "assert_zero_valid" && !self.tcx.permits_zero_init(layout) { return self.codegen_fatal_error( PropertyClass::SafetyCheck, &format!("attempted to zero-initialize type `{}`, which is invalid", ty), @@ -777,9 +774,7 @@ impl<'tcx> GotocCtx<'tcx> { ); } - if intrinsic == "assert_uninit_valid" - && !layout.might_permit_raw_init(self, InitKind::Uninit, false) - { + if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(layout) { return self.codegen_fatal_error( PropertyClass::SafetyCheck, &format!("attempted to leave type `{}` uninitialized, which is invalid", ty), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 869a83b2f2ed..b01573bb4d03 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -14,7 +14,7 @@ use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uin use rustc_span::def_id::DefId; use rustc_span::Span; use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants}; -use tracing::debug; +use tracing::{debug, trace}; enum AllocData<'a> { Bytes(&'a [u8]), @@ -23,9 +23,10 @@ enum AllocData<'a> { impl<'tcx> GotocCtx<'tcx> { pub fn codegen_operand(&mut self, o: &Operand<'tcx>) -> Expr { + trace!(operand=?o, "codegen_operand"); match o { Operand::Copy(d) | Operand::Move(d) => - // TODO: move shouldn't be the same as copy + // TODO: move is an opportunity to poison/nondet the original memory. { let projection = unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(d)); @@ -44,6 +45,7 @@ impl<'tcx> GotocCtx<'tcx> { } fn codegen_constant(&mut self, c: &Constant<'tcx>) -> Expr { + trace!(constant=?c, "codegen_constant"); let const_ = match self.monomorphize(c.literal) { ConstantKind::Ty(ct) => ct, ConstantKind::Val(val, ty) => return self.codegen_const_value(val, ty, Some(&c.span)), @@ -145,6 +147,7 @@ impl<'tcx> GotocCtx<'tcx> { lit_ty: Ty<'tcx>, span: Option<&Span>, ) -> Expr { + trace!(val=?v, ?lit_ty, "codegen_const_value"); match v { ConstValue::Scalar(s) => self.codegen_scalar(s, lit_ty, span), ConstValue::Slice { data, start, end } => { @@ -160,11 +163,15 @@ impl<'tcx> GotocCtx<'tcx> { .cast_to(self.codegen_ty(lit_ty).to_pointer()) .dereference() } + ConstValue::ZeroSized => match lit_ty.kind() { + ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span), + _ => unimplemented!(), + }, } } fn codegen_scalar(&mut self, s: Scalar, ty: Ty<'tcx>, span: Option<&Span>) -> Expr { - debug! {"codegen_scalar\n{:?}\n{:?}\n{:?}\n{:?}",s, ty, span, &ty.kind()}; + debug!(scalar=?s, ?ty, kind=?ty.kind(), ?span, "codegen_scalar"); match (s, &ty.kind()) { (Scalar::Int(_), ty::Int(it)) => match it { IntTy::I8 => Expr::int_constant(s.to_i8().unwrap(), Type::signed_int(8)), @@ -199,9 +206,9 @@ impl<'tcx> GotocCtx<'tcx> { FloatTy::F64 => Expr::double_constant_from_bitpattern(s.to_u64().unwrap()), } } - (Scalar::Int(int), ty::FnDef(d, substs)) => { - assert_eq!(int.size(), Size::ZERO); - self.codegen_fndef(*d, substs, span) + (Scalar::Int(..), ty::FnDef(..)) => { + // This was removed here: https://github.com/rust-lang/rust/pull/98957. + unreachable!("ZST is no longer represented as a scalar") } (Scalar::Int(_), ty::RawPtr(tm)) => { Expr::pointer_constant(s.to_u64().unwrap(), self.codegen_ty(tm.ty).to_pointer()) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 4548e06520a6..f5d2cbfe2cdd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -547,6 +547,13 @@ impl<'tcx> GotocCtx<'tcx> { self, ) } + ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new( + before.goto_expr.cast_to(self.codegen_ty(ty)), + TypeOrVariant::Type(ty), + before.fat_ptr_goto_expr, + before.fat_ptr_mir_typ, + self, + ), } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 8e7d1db1c64a..858e06a494d2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -419,6 +419,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_rvalue(&mut self, rv: &Rvalue<'tcx>, loc: Location) -> Expr { let res_ty = self.rvalue_ty(rv); + debug!(?rv, "codegen_rvalue"); match rv { Rvalue::Use(p) => self.codegen_operand(p), Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, res_ty), @@ -493,6 +494,11 @@ impl<'tcx> GotocCtx<'tcx> { "https://github.com/model-checking/kani/issues/541", ) } + // A CopyForDeref is equivalent to a read from a place at the codegen level. + // https://github.com/rust-lang/rust/blob/1673f1450eeaf4a5452e086db0fe2ae274a0144f/compiler/rustc_middle/src/mir/syntax.rs#L1055 + Rvalue::CopyForDeref(place) => { + unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(place)).goto_expr + } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 8db1b24507e3..06640a76f4b0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -4,10 +4,9 @@ use super::typ::TypeExt; use super::typ::FN_RETURN_VOID_VAR_NAME; use super::PropertyClass; use crate::codegen_cprover_gotoc::codegen::typ::pointee_type; -use crate::codegen_cprover_gotoc::utils; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; -use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; +use cbmc::goto_program::{Expr, Location, Stmt, Type}; use cbmc::utils::BUG_REPORT_URL; use kani_queries::UserInput; use rustc_hir::def_id::DefId; @@ -24,19 +23,166 @@ use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; use tracing::{debug, info_span, trace, warn}; impl<'tcx> GotocCtx<'tcx> { - fn codegen_ret_unit(&mut self) -> Stmt { - let is_file_local = false; - let ty = self.codegen_ty_unit(); - let var = self.ensure_global_var( - FN_RETURN_VOID_VAR_NAME, - is_file_local, - ty, - Location::none(), - |_, _| None, - ); - Stmt::ret(Some(var), Location::none()) + /// Generate Goto-C for MIR [Statement]s. + /// This does not cover all possible "statements" because MIR distinguishes between ordinary + /// statements and [Terminator]s, which can exclusively appear at the end of a basic block. + /// + /// See [GotocCtx::codegen_terminator] for those. + pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt { + let _trace_span = info_span!("CodegenStatement", statement = ?stmt).entered(); + debug!(?stmt, kind=?stmt.kind, "handling_statement"); + let location = self.codegen_span(&stmt.source_info.span); + match &stmt.kind { + StatementKind::Assign(box (l, r)) => { + let lty = self.place_ty(l); + let rty = self.rvalue_ty(r); + let llayout = self.layout_of(lty); + // we ignore assignment for all zero size types + if llayout.is_zst() { + Stmt::skip(Location::none()) + } else if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() { + // implicit address of a function pointer, e.g. + // let fp: fn() -> i32 = foo; + // where the reference is implicit. + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) + .goto_expr + .assign(self.codegen_rvalue(r, location).address_of(), location) + } else if rty.is_bool() { + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) + .goto_expr + .assign(self.codegen_rvalue(r, location).cast_to(Type::c_bool()), location) + } else { + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) + .goto_expr + .assign(self.codegen_rvalue(r, location), location) + } + } + StatementKind::Deinit(place) => { + // From rustc doc: "This writes `uninit` bytes to the entire place." + // Thus, we assign nondet() value to the entire place. + let dst_mir_ty = self.place_ty(place); + let dst_type = self.codegen_ty(dst_mir_ty); + let layout = self.layout_of(dst_mir_ty); + if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 { + // We ignore assignment for all zero size types + // Ignore generators too for now: + // https://github.com/model-checking/kani/issues/416 + Stmt::skip(location) + } else { + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)) + .goto_expr + .assign(dst_type.nondet(), location) + } + } + StatementKind::SetDiscriminant { place, variant_index } => { + // this requires place points to an enum type. + let pt = self.place_ty(place); + let (def, _) = match pt.kind() { + ty::Adt(def, substs) => (def, substs), + ty::Generator(..) => { + return self + .codegen_unimplemented( + "ty::Generator", + Type::code(vec![], Type::empty()), + location, + "https://github.com/model-checking/kani/issues/416", + ) + .as_stmt(location); + } + _ => unreachable!(), + }; + let layout = self.layout_of(pt); + match &layout.variants { + Variants::Single { .. } => Stmt::skip(location), + Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { + TagEncoding::Direct => { + let discr = def.discriminant_for_variant(self.tcx, *variant_index); + let discr_t = self.codegen_enum_discr_typ(pt); + // The constant created below may not fit into the type. + // https://github.com/model-checking/kani/issues/996 + // + // It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)` + // or `discr.ty`. It looks like something is wrong with `discriminat_for_variant` + // because when it tries to codegen `std::cmp::Ordering` (which should produce + // discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types: + // + // debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty); + // DISCRIMINANT - val:255 ty:i8 + // DISCRIMINANT - val:0 ty:i8 + // DISCRIMINANT - val:1 ty:i8 + let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t)); + unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place(place) + ) + .goto_expr + .member("case", &self.symbol_table) + .assign(discr, location) + } + TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { + if dataful_variant != variant_index { + let offset = match &layout.fields { + FieldsShape::Arbitrary { offsets, .. } => { + offsets[0].bytes_usize() + } + _ => unreachable!("niche encoding must have arbitrary fields"), + }; + let discr_ty = self.codegen_enum_discr_typ(pt); + let discr_ty = self.codegen_ty(discr_ty); + let niche_value = + variant_index.as_u32() - niche_variants.start().as_u32(); + let niche_value = (niche_value as u128).wrapping_add(*niche_start); + let value = + if niche_value == 0 && tag.primitive() == Primitive::Pointer { + discr_ty.null() + } else { + Expr::int_constant(niche_value, discr_ty.clone()) + }; + let place = unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place(place) + ) + .goto_expr; + self.codegen_get_niche(place, offset, discr_ty) + .assign(value, location) + } else { + Stmt::skip(location) + } + } + }, + } + } + StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me + StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me + StatementKind::CopyNonOverlapping(box mir::CopyNonOverlapping { + ref src, + ref dst, + ref count, + }) => { + // Pack the operands and their types, then call `codegen_copy` + let fargs = vec![ + self.codegen_operand(src), + self.codegen_operand(dst), + self.codegen_operand(count), + ]; + let farg_types = + &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)]; + self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location) + } + StatementKind::FakeRead(_) + | StatementKind::Retag(_, _) + | StatementKind::AscribeUserType(_, _) + | StatementKind::Nop + | StatementKind::Coverage { .. } => Stmt::skip(location), + } + .with_location(self.codegen_span(&stmt.source_info.span)) } + /// Generate Goto-c for MIR [Terminator] statements. + /// Many kinds of seemingly ordinary statements in Rust are "terminators" (i.e. the sort of statement that _ends_ a basic block) + /// because of the need for unwinding/drop. For instance, function calls. + /// + /// See also [`GotocCtx::codegen_statement`] for ordinary [Statement]s. pub fn codegen_terminator(&mut self, term: &Terminator<'tcx>) -> Stmt { let loc = self.codegen_span(&term.source_info.span); let _trace_span = info_span!("CodegenTerminator", statement = ?term.kind).entered(); @@ -83,9 +229,6 @@ impl<'tcx> GotocCtx<'tcx> { loc, ), TerminatorKind::Drop { place, target, unwind: _ } => self.codegen_drop(place, target), - TerminatorKind::DropAndReplace { .. } => { - unreachable!("this instruction is unreachable") - } TerminatorKind::Call { func, args, destination, target, .. } => { self.codegen_funcall(func, args, destination, target, term.source_info.span) } @@ -130,10 +273,14 @@ impl<'tcx> GotocCtx<'tcx> { loc, ) } - TerminatorKind::Yield { .. } - | TerminatorKind::GeneratorDrop + TerminatorKind::DropAndReplace { .. } | TerminatorKind::FalseEdge { .. } - | TerminatorKind::FalseUnwind { .. } => unreachable!("we should not hit these cases"), + | TerminatorKind::FalseUnwind { .. } => { + unreachable!("drop elaboration removes these TerminatorKind") + } + TerminatorKind::Yield { .. } | TerminatorKind::GeneratorDrop => { + unreachable!("we should not hit these cases") // why? + } TerminatorKind::InlineAsm { .. } => self .codegen_unimplemented( "InlineAsm", @@ -145,25 +292,43 @@ impl<'tcx> GotocCtx<'tcx> { } } - // TODO: this function doesn't handle unwinding which begins if the destructor panics - // https://github.com/model-checking/kani/issues/221 - fn codegen_drop(&mut self, location: &Place<'tcx>, target: &BasicBlock) -> Stmt { - let loc_ty = self.place_ty(location); - debug!(?loc_ty, "codegen_drop"); - let drop_instance = Instance::resolve_drop_in_place(self.tcx, loc_ty); + /// A special case handler to codegen `return ();` + fn codegen_ret_unit(&mut self) -> Stmt { + let is_file_local = false; + let ty = self.codegen_ty_unit(); + let var = self.ensure_global_var( + FN_RETURN_VOID_VAR_NAME, + is_file_local, + ty, + Location::none(), + |_, _| None, + ); + Stmt::ret(Some(var), Location::none()) + } + + /// Generates Goto-C for MIR [TerminatorKind::Drop] calls. We only handle code _after_ Rust's "drop elaboration" + /// transformation, so these have a simpler semantics. + /// + /// The generated code should invoke the appropriate `drop` function on `place`, then goto `target`. + fn codegen_drop(&mut self, place: &Place<'tcx>, target: &BasicBlock) -> Stmt { + // TODO: this function doesn't handle unwinding which begins if the destructor panics + // https://github.com/model-checking/kani/issues/221 + let place_ty = self.place_ty(place); + debug!(?place_ty, "codegen_drop"); + let drop_instance = Instance::resolve_drop_in_place(self.tcx, place_ty); // Once upon a time we did a `hook_applies` check here, but we no longer seem to hook drops let drop_implementation = match drop_instance.def { InstanceDef::DropGlue(_, None) => { // We can skip empty DropGlue functions Stmt::skip(Location::none()) } - _ => { - match loc_ty.kind() { + InstanceDef::DropGlue(_def_id, Some(_)) => { + match place_ty.kind() { ty::Dynamic(..) => { // Virtual drop via a vtable lookup let trait_fat_ptr = unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place(location) + self.codegen_place(place) ) .fat_ptr_goto_expr .unwrap(); @@ -177,7 +342,7 @@ impl<'tcx> GotocCtx<'tcx> { let fn_ptr = vtable.member("drop", &self.symbol_table); // Pull the self argument off of the fat pointer's data pointer - if let Some(typ) = pointee_type(self.local_ty(location.local)) { + if let Some(typ) = pointee_type(self.local_ty(place.local)) { if !(typ.is_trait() || typ.is_box()) { warn!(self_type=?typ, "Unsupported drop of unsized"); return self @@ -213,7 +378,7 @@ impl<'tcx> GotocCtx<'tcx> { let func = self.codegen_func_expr(drop_instance, None); let place = unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place(location) + self.codegen_place(place) ); let arg = if let Some(fat_ptr) = place.fat_ptr_goto_expr { // Drop takes the fat pointer if it exists @@ -245,15 +410,18 @@ impl<'tcx> GotocCtx<'tcx> { } } } + _ => unreachable!( + "TerminatorKind::Drop but not InstanceDef::DropGlue should be impossible" + ), }; let goto_target = Stmt::goto(self.current_fn().find_label(target), Location::none()); let block = vec![drop_implementation, goto_target]; Stmt::block(block, Location::none()) } - /// + /// Generates Goto-C for MIR [TerminatorKind::SwitchInt]. /// Operand evaluates to an integer; - /// jump depending on its value to one of the targets, and otherwise fallback to otherwise. + /// jump depending on its value to one of the targets, and otherwise fallback to `targets.otherwise()`. /// The otherwise value is stores as the last value of targets. fn codegen_switch_int( &mut self, @@ -302,6 +470,9 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// As part of **calling** a function (closure actually), we may need to un-tuple arguments. + /// + /// See [GotocCtx::ty_needs_closure_untupled] fn codegen_untuple_closure_args( &mut self, instance: Instance<'tcx>, @@ -343,6 +514,8 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Because function calls terminate basic blocks, to "end" a function call, we + /// must jump to the next basic block. fn codegen_end_call(&self, target: Option<&BasicBlock>, loc: Location) -> Stmt { if let Some(next_bb) = target { Stmt::goto(self.current_fn().find_label(next_bb), loc) @@ -356,7 +529,10 @@ impl<'tcx> GotocCtx<'tcx> { } } - pub fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec { + /// Generate Goto-C for each argument to a function call. + /// + /// N.B. public only because instrinsics use this directly, too. + pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec { args.iter() .map(|o| { if self.operand_ty(o).is_bool() { @@ -368,6 +544,18 @@ impl<'tcx> GotocCtx<'tcx> { .collect() } + /// Generates Goto-C for a MIR [TerminatorKind::Call] statement. + /// + /// This calls either: + /// + /// 1. A statically-known function definition. + /// 2. A statically-known trait function, which gets a pointer out of a vtable. + /// 2. A direct function pointer. + /// + /// Kani also performs a few alterations: + /// + /// 1. Do nothing for "empty drop glue" + /// 2. If a Kani hook applies, do that instead. fn codegen_funcall( &mut self, func: &Operand<'tcx>, @@ -458,8 +646,8 @@ impl<'tcx> GotocCtx<'tcx> { } /// Extract a reference to self for virtual method calls. - /// See [codegen_dynamic_function_sig](GotocCtx::codegen_dynamic_function_sig) for more - /// details. + /// + /// See [GotocCtx::codegen_dynamic_function_sig] for more details. fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty<'tcx>) -> Expr { // Generate an expression that indexes the pointer. let expr = self @@ -556,10 +744,11 @@ impl<'tcx> GotocCtx<'tcx> { ret_stmts } - /// A place is similar to the C idea of a LHS. For example, the returned value of a function call is stored to a place. - /// If the place is unit (i.e. the statement value is not stored anywhere), then we can just turn it directly to a statement. - /// Otherwise, we assign the value of the expression to the place. - pub fn codegen_expr_to_place(&mut self, p: &Place<'tcx>, e: Expr) -> Stmt { + /// Generates Goto-C to assign a value to a [Place]. + /// A MIR [Place] is an L-value (i.e. the LHS of an assignment). + /// + /// In Kani, we slightly optimize the special case for Unit and don't assign anything. + pub(crate) fn codegen_expr_to_place(&mut self, p: &Place<'tcx>, e: Expr) -> Stmt { if self.place_ty(p).is_unit() { e.as_stmt(Location::none()) } else { @@ -568,183 +757,4 @@ impl<'tcx> GotocCtx<'tcx> { .assign(e, Location::none()) } } - - pub fn codegen_panic(&self, span: Option, fargs: Vec) -> Stmt { - // CBMC requires that the argument to the assertion must be a string constant. - // If there is one in the MIR, use it; otherwise, explain that we can't. - assert!(!fargs.is_empty(), "Panic requires a string message"); - let msg = utils::extract_const_message(&fargs[0]).unwrap_or(String::from( - "This is a placeholder message; Kani doesn't support message formatted at runtime", - )); - - self.codegen_fatal_error(PropertyClass::Assertion, &msg, span) - } - - // Generate code for fatal error which should trigger an assertion failure and abort the - // execution. - pub fn codegen_fatal_error( - &self, - property_class: PropertyClass, - msg: &str, - span: Option, - ) -> Stmt { - let loc = self.codegen_caller_span(&span); - Stmt::block( - vec![ - self.codegen_assert_false(property_class, msg, loc), - BuiltinFn::Abort.call(vec![], loc).as_stmt(loc), - ], - loc, - ) - } - - /// Generate code to cover the given condition at the current location - pub fn codegen_cover(&self, cond: Expr, msg: &str, span: Option) -> Stmt { - let loc = self.codegen_caller_span(&span); - // Should use Stmt::cover, but currently this doesn't work with CBMC - // unless it is run with '--cover cover' (see - // https://github.com/diffblue/cbmc/issues/6613). So for now use - // assert(!cond). - self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc) - } - - /// Generate code to cover the current location - pub fn codegen_cover_loc(&self, msg: &str, span: Option) -> Stmt { - self.codegen_cover(Expr::bool_true(), msg, span) - } - - pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt { - let _trace_span = info_span!("CodegenStatement", statement = ?stmt).entered(); - debug!("handling statement {:?}", stmt); - let location = self.codegen_span(&stmt.source_info.span); - match &stmt.kind { - StatementKind::Assign(box (l, r)) => { - let lty = self.place_ty(l); - let rty = self.rvalue_ty(r); - let llayout = self.layout_of(lty); - // we ignore assignment for all zero size types - if llayout.is_zst() { - Stmt::skip(Location::none()) - } else if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() { - // implicit address of a function pointer, e.g. - // let fp: fn() -> i32 = foo; - // where the reference is implicit. - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location).address_of(), location) - } else if rty.is_bool() { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location).cast_to(Type::c_bool()), location) - } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location), location) - } - } - StatementKind::Deinit(place) => { - // From rustc doc: "This writes `uninit` bytes to the entire place." - // Thus, we assign nondet() value to the entire place. - let dst_mir_ty = self.place_ty(place); - let dst_type = self.codegen_ty(dst_mir_ty); - let layout = self.layout_of(dst_mir_ty); - if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 { - // We ignore assignment for all zero size types - Stmt::skip(location) - } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)) - .goto_expr - .assign(dst_type.nondet(), location) - } - } - StatementKind::SetDiscriminant { place, variant_index } => { - // this requires place points to an enum type. - let pt = self.place_ty(place); - let layout = self.layout_of(pt); - match &layout.variants { - Variants::Single { .. } => Stmt::skip(location), - Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { - TagEncoding::Direct => { - let discr = - pt.discriminant_for_variant(self.tcx, *variant_index).unwrap(); - let discr_t = self.codegen_enum_discr_typ(pt); - // The constant created below may not fit into the type. - // https://github.com/model-checking/kani/issues/996 - // - // It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)` - // or `discr.ty`. It looks like something is wrong with `discriminat_for_variant` - // because when it tries to codegen `std::cmp::Ordering` (which should produce - // discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types: - // - // debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty); - // DISCRIMINANT - val:255 ty:i8 - // DISCRIMINANT - val:0 ty:i8 - // DISCRIMINANT - val:1 ty:i8 - let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t)); - let place_goto_expr = unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place(place) - ) - .goto_expr; - self.codegen_discriminant_field(place_goto_expr, pt) - .assign(discr, location) - } - TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { - if dataful_variant != variant_index { - let offset = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => { - offsets[0].bytes_usize() - } - _ => unreachable!("niche encoding must have arbitrary fields"), - }; - let discr_ty = self.codegen_enum_discr_typ(pt); - let discr_ty = self.codegen_ty(discr_ty); - let niche_value = - variant_index.as_u32() - niche_variants.start().as_u32(); - let niche_value = (niche_value as u128).wrapping_add(*niche_start); - let value = - if niche_value == 0 && tag.primitive() == Primitive::Pointer { - discr_ty.null() - } else { - Expr::int_constant(niche_value, discr_ty.clone()) - }; - let place = unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place(place) - ) - .goto_expr; - self.codegen_get_niche(place, offset, discr_ty) - .assign(value, location) - } else { - Stmt::skip(location) - } - } - }, - } - } - StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me - StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me - StatementKind::CopyNonOverlapping(box mir::CopyNonOverlapping { - ref src, - ref dst, - ref count, - }) => { - // Pack the operands and their types, then call `codegen_copy` - let fargs = vec![ - self.codegen_operand(src), - self.codegen_operand(dst), - self.codegen_operand(count), - ]; - let farg_types = - &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)]; - self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location) - } - StatementKind::FakeRead(_) - | StatementKind::Retag(_, _) - | StatementKind::AscribeUserType(_, _) - | StatementKind::Nop - | StatementKind::Coverage { .. } => Stmt::skip(location), - } - .with_location(self.codegen_span(&stmt.source_info.span)) - } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs index a1e414119e1c..dfea9d31858d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -11,13 +11,16 @@ use rustc_middle::ty::{subst::InternalSubsts, Instance}; use tracing::debug; impl<'tcx> GotocCtx<'tcx> { + /// Ensures a static variable is initialized. pub fn codegen_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) { debug!("codegen_static"); let alloc = self.tcx.eval_static_initializer(def_id).unwrap(); let symbol_name = item.symbol_name(self.tcx).to_string(); + // This is an `Expr` constructing function, but it mutates the symbol table to ensure initialization. self.codegen_allocation(alloc.inner(), |_| symbol_name.clone(), Some(symbol_name.clone())); } + /// Mutates the Goto-C symbol table to add a forward-declaration of the static variable. pub fn declare_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) { // Unique mangled monomorphized name. let symbol_name = item.symbol_name(self.tcx).to_string(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 4d6794c88756..af9622afcf06 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -814,6 +814,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// A closure in Rust MIR takes two arguments: + /// /// 0. a struct representing the environment /// 1. a tuple containing the parameters /// @@ -823,16 +824,22 @@ impl<'tcx> GotocCtx<'tcx> { /// Checking whether the type's kind is a closure is insufficient, because /// a virtual method call through a vtable can have the trait's non-closure /// type. For example: + /// + /// ``` /// let p: &dyn Fn(i32) = &|x| assert!(x == 1); /// p(1); + /// ``` /// - /// Here, the call p(1) desugars to an MIR trait call Fn::call(&p, (1,)), + /// Here, the call `p(1)` desugars to an MIR trait call `Fn::call(&p, (1,))`, /// where the second argument is a tuple. The instance type kind for - /// Fn::call is not a closure, because dynamically, the pointer may be to + /// `Fn::call` is not a closure, because dynamically, the pointer may be to /// a function definition instead. We still need to untuple in this case, /// so we follow the example elsewhere in Rust to use the ABI call type. - /// See `make_call_args` in kani/compiler/rustc_mir/src/transform/inline.rs + /// + /// See `make_call_args` in `rustc_mir_transform/src/inline.rs` pub fn ty_needs_closure_untupled(&self, ty: Ty<'tcx>) -> bool { + // Note that [Abi::RustCall] is not [Abi::Rust]. + // Documentation is sparse, but it does seem to correspond to the need for untupling. match ty.kind() { ty::FnDef(..) | ty::FnPtr(..) => ty.fn_sig(self.tcx).abi() == Abi::RustCall, _ => unreachable!("Can't treat type as a function: {:?}", ty), diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index db3fbda9c69e..1918174a8c63 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -151,7 +151,7 @@ impl CodegenBackend for GotocCodegenBackend { let metadata = KaniMetadata { proof_harnesses: c.proof_harnesses }; // No output should be generated if user selected no_codegen. - if !tcx.sess.opts.debugging_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { + if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { let outputs = tcx.output_filenames(()); let base_filename = outputs.output_path(OutputType::Object); let pretty = self.queries.get_output_pretty_json(); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 468e8286bdab..a1e7f9af086c 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2022-07-05" +channel = "nightly-2022-07-19" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/cargo-kani/vecdeque-cve/src/harness.rs b/tests/cargo-kani/vecdeque-cve/src/harness.rs index b4cb038f0f04..5a53c2c517d6 100644 --- a/tests/cargo-kani/vecdeque-cve/src/harness.rs +++ b/tests/cargo-kani/vecdeque-cve/src/harness.rs @@ -22,7 +22,7 @@ mod fixed; mod raw_vec; use abstract_vecdeque::*; -const MAX_CAPACITY: usize = usize::MAX >> 1; +const MAX_CAPACITY: usize = usize::MAX >> 2; /// This module uses a version of VecDeque that includes the CVE fix. mod fixed_proofs { diff --git a/tests/kani/DerefCopy/check_deref_copy.rs b/tests/kani/DerefCopy/check_deref_copy.rs new file mode 100644 index 000000000000..49444c37f34e --- /dev/null +++ b/tests/kani/DerefCopy/check_deref_copy.rs @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +/// Adapted from: +/// +#[kani::proof] +fn check_deref_copy() { + let mut a = (42, 43); + let mut b = (99, &mut a); + let x = &mut (*b.1).0; + let y = &mut (*b.1).1; + assert_eq!(*x, 42); + assert_eq!(*y, 43); +} diff --git a/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs b/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs new file mode 100644 index 000000000000..4fadabd92da2 --- /dev/null +++ b/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +//! Tests that check handling of opaque casts. Tests were adapted from the rustc repository. + +#![feature(type_alias_impl_trait)] + +#[derive(Copy, Clone)] +struct Foo((u32, u32)); + +/// Adapted from: +/// +#[kani::proof] +fn check_unconstrained_upvar() { + type T = impl Copy; + let foo: T = Foo((1u32, 2u32)); + let x = move || { + let Foo((a, b)) = foo; + assert_eq!(a, 1u32); + assert_eq!(b, 2u32); + }; +} + +/// Adapted from: +/// +#[kani::proof] +fn check_unconstrained_struct() { + type U = impl Copy; + let foo: U = Foo((1u32, 2u32)); + let Foo((a, b)) = foo; + assert_eq!(a, 1u32); + assert_eq!(b, 2u32); +} + +/// Adapted from: +/// +#[kani::proof] +fn check_unpack_option_tuple() { + type T = impl Copy; + let foo: T = Some((1u32, 2u32)); + match foo { + None => (), + Some((a, b)) => { + assert_eq!(a, 1u32); + assert_eq!(b, 2u32) + } + } +} diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index f186f5251933..a87440021250 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -177,7 +177,7 @@ pub fn parse_config(args: Vec) -> Config { let mut root_folder = top_level().expect( format!("Cannot find root directory. Please provide --{} option.", nm).as_str(), ); - default.into_iter().for_each(|f| root_folder.push(f)); + default.iter().for_each(|f| root_folder.push(f)); root_folder } } @@ -272,8 +272,7 @@ pub fn run_tests(config: Config) { let opts = test_opts(&config); - let mut configs = Vec::new(); - configs.push(config.clone()); + let configs = vec![config.clone()]; let mut tests = Vec::new(); for c in &configs { diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 35e817d32a58..85eb1fb973d9 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -176,10 +176,8 @@ impl<'test> TestCx<'test> { if proc_res.status.success() { self.fatal_proc_rec("test failed: expected check failure, got success", &proc_res); } - } else { - if !proc_res.status.success() { - self.fatal_proc_rec("test failed: expected check success, got failure", &proc_res); - } + } else if !proc_res.status.success() { + self.fatal_proc_rec("test failed: expected check success, got failure", &proc_res); } } @@ -202,13 +200,8 @@ impl<'test> TestCx<'test> { &proc_res, ); } - } else { - if !proc_res.status.success() { - self.fatal_proc_rec( - "test failed: expected codegen success, got failure", - &proc_res, - ); - } + } else if !proc_res.status.success() { + self.fatal_proc_rec("test failed: expected codegen success, got failure", &proc_res); } } @@ -247,13 +240,11 @@ impl<'test> TestCx<'test> { &proc_res, ); } - } else { - if !proc_res.status.success() { - self.fatal_proc_rec( - "test failed: expected verification success, got failure", - &proc_res, - ); - } + } else if !proc_res.status.success() { + self.fatal_proc_rec( + "test failed: expected verification success, got failure", + &proc_res, + ); } } } @@ -278,12 +269,10 @@ impl<'test> TestCx<'test> { /// If the test file contains expected failures in some locations, ensure /// that verification does not succeed in those locations. fn verify_expect_fail(str: &str) -> Vec { - let re = Regex::new(r"line [0-9]+ EXPECTED FAIL: SUCCESS").unwrap(); + let re = Regex::new(r"line ([0-9]+) EXPECTED FAIL: SUCCESS").unwrap(); let mut lines = vec![]; - for m in re.find_iter(str) { - let splits = m.as_str().split_ascii_whitespace(); - let num_str = splits.skip(1).next().unwrap(); - let num = num_str.parse().unwrap(); + for m in re.captures_iter(str) { + let num = m.get(1).unwrap().as_str().parse().unwrap(); lines.push(num); } lines @@ -365,15 +354,16 @@ impl<'test> TestCx<'test> { fn verify_output(&self, proc_res: &ProcRes, expected: &str) { // Include the output from stderr here for cases where there are exceptions let output = proc_res.stdout.to_string() + &proc_res.stderr; - if let Some(lines) = - TestCx::contains_lines(&output.split('\n').collect(), expected.split('\n').collect()) - { + if let Some(lines) = TestCx::contains_lines( + &output.split('\n').collect::>(), + expected.split('\n').collect(), + ) { self.fatal_proc_rec( &format!( "test failed: expected output to contain the line(s):\n{}", lines.join("\n") ), - &proc_res, + proc_res, ); } } @@ -381,19 +371,19 @@ impl<'test> TestCx<'test> { /// Looks for each line or set of lines in `str`. Returns `None` if all /// lines are in `str`. Otherwise, it returns the first line not found in /// `str`. - fn contains_lines<'a>(str: &Vec<&str>, lines: Vec<&'a str>) -> Option> { + fn contains_lines<'a>(str: &[&str], lines: Vec<&'a str>) -> Option> { let mut consecutive_lines: Vec<&str> = Vec::new(); for line in lines { // A line that ends in "\" indicates that the next line in the // expected file should appear on the consecutive line in the // output. This is a temporary mechanism until we have more robust // json-based checking of verification results - if let Some(prefix) = line.strip_suffix("\\") { + if let Some(prefix) = line.strip_suffix('\\') { // accumulate the lines consecutive_lines.push(prefix); } else { consecutive_lines.push(line); - if !TestCx::contains(&str, &consecutive_lines) { + if !TestCx::contains(str, &consecutive_lines) { return Some(consecutive_lines); } consecutive_lines.clear(); @@ -404,7 +394,7 @@ impl<'test> TestCx<'test> { /// Check if there is a set of consecutive lines in `str` where each line /// contains a line from `lines` - fn contains(str: &Vec<&str>, lines: &Vec<&str>) -> bool { + fn contains(str: &[&str], lines: &[&str]) -> bool { let mut i = str.iter(); while let Some(output_line) = i.next() { if output_line.contains(&lines[0]) { @@ -413,9 +403,9 @@ impl<'test> TestCx<'test> { let mut matches = true; // Clone the iterator so that we keep i unchanged let mut j = i.clone(); - for i in 1..lines.len() { + for line in lines.iter().skip(1) { if let Some(output_line) = j.next() { - if output_line.contains(lines[i]) { + if output_line.contains(line) { continue; } } @@ -431,7 +421,7 @@ impl<'test> TestCx<'test> { } fn create_stamp(&self) { - let stamp = crate::stamp(&self.config, self.testpaths, self.revision); + let stamp = crate::stamp(self.config, self.testpaths, self.revision); fs::write(&stamp, "we only support one configuration").unwrap(); } }