From e95a7bb886683c9443e42c78bf31ea11eff9d7f6 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 25 Sep 2023 13:38:13 -0400 Subject: [PATCH 01/13] Fix issue 2589 (#2787) Co-authored-by: Felipe R. Monteiro --- kani-compiler/src/kani_middle/reachability.rs | 58 ++++++++++++++++++- tests/expected/issue-2589/issue_2589.expected | 1 + tests/expected/issue-2589/issue_2589.rs | 21 +++++++ 3 files changed, 78 insertions(+), 2 deletions(-) create mode 100644 tests/expected/issue-2589/issue_2589.expected create mode 100644 tests/expected/issue-2589/issue_2589.rs diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 5ac0344c9fbd..66cebf9c8f6f 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -13,6 +13,7 @@ //! - For every static, collect initializer and drop functions. //! //! We have kept this module agnostic of any Kani code in case we can contribute this back to rustc. +use rustc_span::ErrorGuaranteed; use tracing::{debug, debug_span, trace, warn}; use rustc_data_structures::fingerprint::Fingerprint; @@ -26,6 +27,7 @@ use rustc_middle::mir::mono::MonoItem; use rustc_middle::mir::visit::Visitor as MirVisitor; use rustc_middle::mir::{ Body, CastKind, Constant, ConstantKind, Location, Rvalue, Terminator, TerminatorKind, + UnevaluatedConst, }; use rustc_middle::span_bug; use rustc_middle::ty::adjustment::PointerCoercion; @@ -458,7 +460,23 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { // The `monomorphize` call should have evaluated that constant already. Ok(const_val) => const_val, Err(ErrorHandled::TooGeneric(span)) => { - span_bug!(span, "Unexpected polymorphic constant: {:?}", literal) + if graceful_const_resolution_err( + self.tcx, + &un_eval, + span, + self.instance.def_id(), + ) + .is_some() + { + return; + } else { + span_bug!( + span, + "Unexpected polymorphic constant: {:?} {:?}", + literal, + constant.literal + ) + } } Err(error) => { warn!(?error, "Error already reported"); @@ -494,6 +512,12 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { // implement the same traits as those in the // original function/method. A trait mismatch shows // up here, when we try to resolve a trait method + + // FIXME: This assumes the type resolving the + // trait is the first argument, but that isn't + // necessarily true. It could be any argument or + // even the return type, for instance for a + // trait like `FromIterator`. let generic_ty = outer_args[0].ty(self.body, tcx).peel_refs(); let receiver_ty = tcx.subst_and_normalize_erasing_regions( substs, @@ -508,7 +532,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { "`{receiver_ty}` doesn't implement \ `{trait_}`. The function `{caller}` \ cannot be stubbed by `{}` due to \ - generic bounds not being met.", + generic bounds not being met. Callee: {callee}", tcx.def_path_str(stub) ), ); @@ -555,6 +579,36 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { } } +/// Try to construct a nice error message when const evaluation fails. +/// +/// This function handles the `Trt::CNST` case where there is one trait (`Trt`) +/// which defined a constant `CNST` that we failed to resolve. As such we expect +/// that the trait can be resolved from the constant and that only one generic +/// parameter, the instantiation of `Trt`, is present. +/// +/// If these expectations are not met we return `None`. We do not know in what +/// situation that would be the case and if they are even possible. +fn graceful_const_resolution_err<'tcx>( + tcx: TyCtxt<'tcx>, + mono_const: &UnevaluatedConst<'tcx>, + span: rustc_span::Span, + parent_fn: DefId, +) -> Option { + let implementor = match mono_const.args.as_slice() { + [one] => one.as_type(), + _ => None, + }?; + let trait_ = tcx.trait_of_item(mono_const.def)?; + let msg = format!( + "Type `{implementor}` does not implement trait `{}`. \ + This is likely because `{}` is used as a stub but its \ + generic bounds are not being met.", + tcx.def_path_str(trait_), + tcx.def_path_str(parent_fn) + ); + Some(tcx.sess.span_err(span, msg)) +} + /// Convert a `MonoItem` into a stable `Fingerprint` which can be used as a stable hash across /// compilation sessions. This allow us to provide a stable deterministic order to codegen. fn to_fingerprint(tcx: TyCtxt, item: &MonoItem) -> Fingerprint { diff --git a/tests/expected/issue-2589/issue_2589.expected b/tests/expected/issue-2589/issue_2589.expected new file mode 100644 index 000000000000..0352a8933b6d --- /dev/null +++ b/tests/expected/issue-2589/issue_2589.expected @@ -0,0 +1 @@ +error: Type `std::string::String` does not implement trait `Dummy`. This is likely because `original` is used as a stub but its generic bounds are not being met. diff --git a/tests/expected/issue-2589/issue_2589.rs b/tests/expected/issue-2589/issue_2589.rs new file mode 100644 index 000000000000..a9442091c1e3 --- /dev/null +++ b/tests/expected/issue-2589/issue_2589.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing + +fn original() {} + +trait Dummy { + const TRUE: bool = true; +} + +fn stub() { + // Do nothing. + assert!(T::TRUE); +} + +#[kani::proof] +#[kani::stub(original, stub)] +fn check_mismatch() { + original::(); +} From 6b1a09d56e88471d17cc6d3b97bb5d3a5eb156cc Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 25 Sep 2023 15:05:00 -0700 Subject: [PATCH 02/13] Auto label PRs that may require extra checks (#2785) Add a new workflow that automatically adds the label "Z-BenchCI" to PRs that touch compiler, toolchain, dependencies and driver files that invoke our dependencies. I also removed the label from the toolchain update job since this workflow will add the label once the PR is created. --- .github/labeler.yml | 16 +++++++++++++ .github/workflows/labeler.yml | 30 +++++++++++++++++++++++++ .github/workflows/toolchain-upgrade.yml | 1 - 3 files changed, 46 insertions(+), 1 deletion(-) create mode 100644 .github/labeler.yml create mode 100644 .github/workflows/labeler.yml diff --git a/.github/labeler.yml b/.github/labeler.yml new file mode 100644 index 000000000000..ec81f0aa15cc --- /dev/null +++ b/.github/labeler.yml @@ -0,0 +1,16 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# Configuration for auto-labeling PRs +# +# Note that we enable dot, so "**" matches all files in a folder + +Z-BenchCI: + - kani-compiler/** + - rust-toolchain.toml + - kani-dependencies + - kani-driver/src/call-* + - Cargo.lock + - cprover_bindings/** + - library/** + diff --git a/.github/workflows/labeler.yml b/.github/workflows/labeler.yml new file mode 100644 index 000000000000..70f7bf61e36b --- /dev/null +++ b/.github/workflows/labeler.yml @@ -0,0 +1,30 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# Auto label PRs based on the files that were changed +# +# This PR runs on `pull_request_target` because it needs extra write permission. +# +# Thus, we keep this workflow minimal, and the only action used here is from a +# verified publisher. +# +# See for more details. + +name: Auto Label +on: pull_request_target + +jobs: + auto-label: + permissions: + contents: read + pull-requests: write + runs-on: ubuntu-latest + steps: + - name: Checkout Kani + uses: actions/checkout@v3 + + - name: Label PR + uses: actions/labeler@v4 + with: + dot: true + diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml index 2c199161f9e0..8d54ebe189ff 100644 --- a/.github/workflows/toolchain-upgrade.yml +++ b/.github/workflows/toolchain-upgrade.yml @@ -74,7 +74,6 @@ jobs: branch: toolchain-${{ env.next_toolchain_date }} delete-branch: true title: 'Automatic toolchain upgrade to nightly-${{ env.next_toolchain_date }}' - labels: Z-BenchCI body: > Update Rust toolchain from nightly-${{ env.current_toolchain_date }} to nightly-${{ env.next_toolchain_date }} without any other source changes. From 8480dc611f35942955747b5ca076dbe6967bee35 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Mon, 25 Sep 2023 23:02:15 -0700 Subject: [PATCH 03/13] Deprecate any_slice (#2789) Deprecate kani::slice::any_slice in Kani 0.38.0 (and the related AnySlice struct), and remove it in a later version. Motivation: The Kani library's `slice::any_slice` API is doing more harm than benefit: it is meant to provide a convenient way for users to generate non-deterministic slices, but its current implementation aims to avoid any unsoundness by making sure that for the non-deterministic slice returned by the API, accessing memory beyond the slice length is flagged as an out-of-bounds access (see #1009 for details). However, in practical scenarios, using it ends up causing memory to blowup for CBMC. Given that users may not care about this type of unsoundness, which is only possible through using a pointer dereference inside an unsafe block (see discussion in #2634). Thus, we should leave it to the user to decide the suitable method for generating slices that fits their verification needs. For example, they can use Kani's alternative API, `any_slice_of_array` that extracts a slice of a non-deterministic start and end from a given array. --- library/kani/src/slice.rs | 14 ++++++++++++ tests/expected/nondet-slice-i32-oob/main.rs | 7 +++--- tests/expected/nondet-slice-len/expected | 19 +++++++++++----- tests/expected/nondet-slice-len/main.rs | 15 +++++++------ tests/expected/nondet-slice-u8-oob/main.rs | 7 +++--- tests/kani/NondetSlices/test2.rs | 5 +++-- tests/kani/NondetSlices/test3.rs | 5 +++-- tests/kani/NondetSlices/test4.rs | 19 ---------------- tests/kani/Slice/slice-drop.rs | 25 --------------------- tests/ui/any-slice-deprecated/expected | 2 ++ tests/ui/any-slice-deprecated/test.rs | 10 +++++++++ 11 files changed, 62 insertions(+), 66 deletions(-) delete mode 100644 tests/kani/NondetSlices/test4.rs delete mode 100644 tests/kani/Slice/slice-drop.rs create mode 100644 tests/ui/any-slice-deprecated/expected create mode 100644 tests/ui/any-slice-deprecated/test.rs diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs index f06118a4b2f5..27a4a6a5d8fd 100644 --- a/library/kani/src/slice.rs +++ b/library/kani/src/slice.rs @@ -47,12 +47,17 @@ fn any_range() -> (usize, usize) { /// let slice: kani::slice::AnySlice = kani::slice::any_slice(); /// foo(&slice); // where foo is a function that takes a slice and verifies a property about it /// ``` +#[deprecated( + since = "0.38.0", + note = "Use `any_slice_of_array` or `any_slice_of_array_mut` instead" +)] pub struct AnySlice { layout: Layout, ptr: *mut T, slice_len: usize, } +#[allow(deprecated)] impl AnySlice { fn new() -> Self where @@ -103,6 +108,7 @@ impl AnySlice { } } +#[allow(deprecated)] impl Drop for AnySlice { fn drop(&mut self) { if self.slice_len > 0 { @@ -114,6 +120,7 @@ impl Drop for AnySlice { } } +#[allow(deprecated)] impl Deref for AnySlice { type Target = [T]; @@ -122,15 +129,22 @@ impl Deref for AnySlice { } } +#[allow(deprecated)] impl DerefMut for AnySlice { fn deref_mut(&mut self) -> &mut Self::Target { self.get_slice_mut() } } +#[deprecated( + since = "0.38.0", + note = "Use `any_slice_of_array` or `any_slice_of_array_mut` instead" +)] +#[allow(deprecated)] pub fn any_slice() -> AnySlice where T: Arbitrary, { + #[allow(deprecated)] AnySlice::::new() } diff --git a/tests/expected/nondet-slice-i32-oob/main.rs b/tests/expected/nondet-slice-i32-oob/main.rs index 399304469960..9537bbc5de43 100644 --- a/tests/expected/nondet-slice-i32-oob/main.rs +++ b/tests/expected/nondet-slice-i32-oob/main.rs @@ -2,11 +2,12 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // This test checks that Kani reports out-of-bound accesses on a non-det slice -// created using kani::slice::any_slice +// created using `kani::slice::any_slice_of_array` #[kani::proof] fn check_out_of_bounds() { - let bytes = kani::slice::any_slice::(); - let val = unsafe { *bytes.get_slice().as_ptr().offset(1) }; + let arr: [i32; 8] = kani::any(); + let bytes = kani::slice::any_slice_of_array(&arr); + let val = unsafe { *bytes.as_ptr().offset(1) }; assert_eq!(val - val, 0); } diff --git a/tests/expected/nondet-slice-len/expected b/tests/expected/nondet-slice-len/expected index 3a9f223e446c..629888bd74d6 100644 --- a/tests/expected/nondet-slice-len/expected +++ b/tests/expected/nondet-slice-len/expected @@ -1,5 +1,14 @@ -Failed Checks: assertion failed: s.len() != 0 -Failed Checks: assertion failed: s.len() != 1 -Failed Checks: assertion failed: s.len() != 2 -Failed Checks: assertion failed: s.len() != 3 -Failed Checks: assertion failed: s.len() != 4 +Status: SATISFIED\ +Description: "cover condition: s.len() == 0" + +Status: SATISFIED\ +Description: "cover condition: s.len() == 1" + +Status: SATISFIED\ +Description: "cover condition: s.len() == 2" + +Status: SATISFIED\ +Description: "cover condition: s.len() == 3" + +Status: SATISFIED\ +Description: "cover condition: s.len() == 4" diff --git a/tests/expected/nondet-slice-len/main.rs b/tests/expected/nondet-slice-len/main.rs index 842a181b54be..cf4cb55fc89f 100644 --- a/tests/expected/nondet-slice-len/main.rs +++ b/tests/expected/nondet-slice-len/main.rs @@ -1,15 +1,16 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test checks that non-det slices created using kani::slice::any_slice can +// This test checks that non-det slices created using `kani::slice::any_slice_of_array` // assume any length up the specified maximum #[kani::proof] fn check_possible_slice_lengths() { - let s = kani::slice::any_slice::(); - assert!(s.len() != 0); - assert!(s.len() != 1); - assert!(s.len() != 2); - assert!(s.len() != 3); - assert!(s.len() != 4); + let arr: [i32; 4] = kani::any(); + let s = kani::slice::any_slice_of_array(&arr); + kani::cover!(s.len() == 0); + kani::cover!(s.len() == 1); + kani::cover!(s.len() == 2); + kani::cover!(s.len() == 3); + kani::cover!(s.len() == 4); } diff --git a/tests/expected/nondet-slice-u8-oob/main.rs b/tests/expected/nondet-slice-u8-oob/main.rs index 26df22279c05..fcebe171f7bd 100644 --- a/tests/expected/nondet-slice-u8-oob/main.rs +++ b/tests/expected/nondet-slice-u8-oob/main.rs @@ -2,12 +2,13 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // This test checks that Kani reports out-of-bound accesses on a non-det slice -// created using kani::slice::any_slice +// created using `kani::slice::any_slice_of_array` #[kani::proof] fn check_out_of_bounds() { - let mut bytes = kani::slice::any_slice::(); - let val = unsafe { *bytes.get_slice().as_ptr().add(4) }; + let arr: [u8; 5] = kani::any(); + let mut bytes = kani::slice::any_slice_of_array(&arr); + let val = unsafe { *bytes.as_ptr().add(4) }; kani::assume(val != 0); assert_ne!(val, 0); } diff --git a/tests/kani/NondetSlices/test2.rs b/tests/kani/NondetSlices/test2.rs index 2f0fc72f0a1f..26a1738f9da8 100644 --- a/tests/kani/NondetSlices/test2.rs +++ b/tests/kani/NondetSlices/test2.rs @@ -9,7 +9,8 @@ fn check(s: &[u8]) { #[kani::proof] fn main() { - // returns a slice of length between 0 and 5 with non-det content - let slice: kani::slice::AnySlice = kani::slice::any_slice(); + let arr: [u8; 5] = kani::any(); + // returns a slice of length between 0 and 5 + let slice = kani::slice::any_slice_of_array(&arr); check(&slice); } diff --git a/tests/kani/NondetSlices/test3.rs b/tests/kani/NondetSlices/test3.rs index 9a334c249284..a876b8ec045d 100644 --- a/tests/kani/NondetSlices/test3.rs +++ b/tests/kani/NondetSlices/test3.rs @@ -1,13 +1,14 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test uses kani::slice::any_slice of i32 +// This test uses `kani::slice::any_slice_of_array` with `i32` // kani-flags: --default-unwind 6 #[kani::proof] fn check_any_slice_i32() { - let s = kani::slice::any_slice::(); + let a: [i32; 5] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); s.iter().for_each(|x| kani::assume(*x < 10 && *x > -20)); let sum = s.iter().fold(0, |acc, x| acc + x); assert!(sum <= 45); // 9 * 5 diff --git a/tests/kani/NondetSlices/test4.rs b/tests/kani/NondetSlices/test4.rs deleted file mode 100644 index 1a61233d1e2b..000000000000 --- a/tests/kani/NondetSlices/test4.rs +++ /dev/null @@ -1,19 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// This test checks that values returned by `kani::slice::any_slice` satisfy the -// type invariant - -// kani-flags: --default-unwind 4 - -extern crate kani; -use kani::slice::{any_slice, AnySlice}; - -#[kani::proof] -fn check_any_slice_valid() { - let s: AnySlice = any_slice(); - for c in s.get_slice() { - kani::assume(*c != char::MAX); - assert!(*c < char::MAX); - } -} diff --git a/tests/kani/Slice/slice-drop.rs b/tests/kani/Slice/slice-drop.rs deleted file mode 100644 index 41d596c3be46..000000000000 --- a/tests/kani/Slice/slice-drop.rs +++ /dev/null @@ -1,25 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Assigning to a memory location via pointer dereferencing causes Drop::drop to be called for the location to which the pointer points. -// Here, kani::Arbitrary implementation for MyStruct deterministically sets MyStruct.0 to 1. -// We check whether AnySlice will properly initialize memory making the assertion in drop() to pass. - -struct MyStruct(i32); - -impl Drop for MyStruct { - fn drop(&mut self) { - assert!(self.0 == 1); - } -} - -impl kani::Arbitrary for MyStruct { - fn any() -> Self { - MyStruct(1) - } -} - -#[kani::proof] -fn my_proof() { - let my_slice = kani::slice::any_slice::(); -} diff --git a/tests/ui/any-slice-deprecated/expected b/tests/ui/any-slice-deprecated/expected new file mode 100644 index 000000000000..db7d5dc3e970 --- /dev/null +++ b/tests/ui/any-slice-deprecated/expected @@ -0,0 +1,2 @@ +warning: use of deprecated function `kani::slice::any_slice`: Use `any_slice_of_array` or `any_slice_of_array_mut` instead +warning: use of deprecated struct `kani::slice::AnySlice`: Use `any_slice_of_array` or `any_slice_of_array_mut` instead diff --git a/tests/ui/any-slice-deprecated/test.rs b/tests/ui/any-slice-deprecated/test.rs new file mode 100644 index 000000000000..0561986ece73 --- /dev/null +++ b/tests/ui/any-slice-deprecated/test.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! A test that checks that Kani emits the deprecated message for `any_slice` +//! and `AnySlice` + +#[kani::proof] +fn check_any_slice_deprecated() { + let _s: kani::slice::AnySlice = kani::slice::any_slice(); +} From dba16744ee1d9299b379d9f876c28a8d07376933 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 27 Sep 2023 14:05:30 -0400 Subject: [PATCH 04/13] Simple Stubbing with Contracts (#2746) ### Description of changes: Expands the contract features introduced in #2655 by completing the checking with stubbing/replacement capabilities. ### Resolved issues: Resolves #2621 ### Related RFC: [0009 Function Contracts](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val Co-authored-by: Felipe R. Monteiro --- kani-compiler/src/kani_middle/attributes.rs | 185 ++++- library/kani/src/contracts.rs | 173 ++++ library/kani/src/lib.rs | 4 +- library/kani_macros/src/lib.rs | 60 +- library/kani_macros/src/sysroot/contracts.rs | 767 +++++++++++++----- .../gcd_replacement_fail.expected | 17 + .../function-contract/gcd_replacement_fail.rs | 67 ++ .../gcd_replacement_pass.expected | 17 + .../function-contract/gcd_replacement_pass.rs | 67 ++ .../missing_contract_for_check.expected | 9 + .../missing_contract_for_check.rs | 10 + .../missing_contract_for_replace.expected | 9 + .../missing_contract_for_replace.rs | 11 + .../allowed_mut_return_ref.rs | 17 +- .../prohibit-pointers/return_pointer.rs | 12 +- .../simple_replace_fail.expected | 3 + .../function-contract/simple_replace_fail.rs | 15 + .../simple_replace_pass.expected | 9 + .../function-contract/simple_replace_pass.rs | 15 + .../type_annotation_needed.expected | 1 + .../type_annotation_needed.rs | 14 + 21 files changed, 1225 insertions(+), 257 deletions(-) create mode 100644 library/kani/src/contracts.rs create mode 100644 tests/expected/function-contract/gcd_replacement_fail.expected create mode 100644 tests/expected/function-contract/gcd_replacement_fail.rs create mode 100644 tests/expected/function-contract/gcd_replacement_pass.expected create mode 100644 tests/expected/function-contract/gcd_replacement_pass.rs create mode 100644 tests/expected/function-contract/missing_contract_for_check.expected create mode 100644 tests/expected/function-contract/missing_contract_for_check.rs create mode 100644 tests/expected/function-contract/missing_contract_for_replace.expected create mode 100644 tests/expected/function-contract/missing_contract_for_replace.rs create mode 100644 tests/expected/function-contract/simple_replace_fail.expected create mode 100644 tests/expected/function-contract/simple_replace_fail.rs create mode 100644 tests/expected/function-contract/simple_replace_pass.expected create mode 100644 tests/expected/function-contract/simple_replace_pass.rs create mode 100644 tests/expected/function-contract/type_annotation_needed.expected create mode 100644 tests/expected/function-contract/type_annotation_needed.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d1ef8fdf33e3..2c9c6d7ee54c 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -19,7 +19,7 @@ use strum_macros::{AsRefStr, EnumString}; use tracing::{debug, trace}; -use super::resolve::{self, resolve_fn}; +use super::resolve::{self, resolve_fn, ResolveError}; #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] #[strum(serialize_all = "snake_case")] @@ -31,6 +31,9 @@ enum KaniAttributeKind { /// Attribute used to mark unstable APIs. Unstable, Unwind, + /// A sound [`Self::Stub`] that replaces a function by a stub generated from + /// its contract. + StubVerified, /// A harness, similar to [`Self::Proof`], but for checking a function /// contract, e.g. the contract check is substituted for the target function /// before the the verification runs. @@ -38,6 +41,10 @@ enum KaniAttributeKind { /// Attribute on a function with a contract that identifies the code /// implementing the check for this contract. CheckedWith, + /// Internal attribute of the contracts implementation that identifies the + /// name of the function which was generated as the sound stub from the + /// contract of this function. + ReplacedWith, /// Attribute on a function that was auto-generated from expanding a /// function contract. IsContractGenerated, @@ -52,8 +59,10 @@ impl KaniAttributeKind { | KaniAttributeKind::Solver | KaniAttributeKind::Stub | KaniAttributeKind::ProofForContract + | KaniAttributeKind::StubVerified | KaniAttributeKind::Unwind => true, KaniAttributeKind::Unstable + | KaniAttributeKind::ReplacedWith | KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => false, } @@ -134,6 +143,30 @@ impl<'tcx> KaniAttributes<'tcx> { } } + /// Parse, extract and resolve the target of `stub_verified(TARGET)`. The + /// returned `Symbol` and `DefId` are respectively the name and id of + /// `TARGET`. The `Span` is that of the contents of the attribute and used + /// for error reporting. + fn interpret_stub_verified_attribute( + &self, + ) -> Vec> { + self.map + .get(&KaniAttributeKind::StubVerified) + .map_or([].as_slice(), Vec::as_slice) + .iter() + .map(|attr| { + let name = expect_key_string_value(self.tcx.sess, attr)?; + let ok = self.resolve_sibling(name.as_str()).map_err(|e| { + self.tcx.sess.span_err( + attr.span, + format!("Failed to resolve replacement function {}: {e}", name.as_str()), + ) + })?; + Ok((name, ok, attr.span)) + }) + .collect() + } + /// Parse and extract the `proof_for_contract(TARGET)` attribute. The /// returned symbol and DefId are respectively the name and id of `TARGET`, /// the span in the span for the attribute (contents). @@ -142,30 +175,50 @@ impl<'tcx> KaniAttributes<'tcx> { ) -> Option> { self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| { let name = expect_key_string_value(self.tcx.sess, target)?; - let resolved = resolve_fn( - self.tcx, - self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), - name.as_str(), - ); - resolved.map(|ok| (name, ok, target.span)).map_err(|resolve_err| { - self.tcx.sess.span_err( - target.span, - format!( - "Failed to resolve replacement function {} because {resolve_err}", - name.as_str() - ), - ) - }) + self.resolve_sibling(name.as_str()).map(|ok| (name, ok, target.span)).map_err( + |resolve_err| { + self.tcx.sess.span_err( + target.span, + format!( + "Failed to resolve checking function {} because {resolve_err}", + name.as_str() + ), + ) + }, + ) }) } - /// Extract the name of the sibling function this contract is checked with - /// (if any). + /// Extract the name of the sibling function this function's contract is + /// checked with (if any). + /// + /// `None` indicates this function does not use a contract, `Some(Err(_))` + /// indicates a contract does exist but an error occurred during resolution. pub fn checked_with(&self) -> Option> { self.expect_maybe_one(KaniAttributeKind::CheckedWith) .map(|target| expect_key_string_value(self.tcx.sess, target)) } + /// Extract the name of the sibling function this function's contract is + /// stubbed as (if any). + /// + /// `None` indicates this function does not use a contract, `Some(Err(_))` + /// indicates a contract does exist but an error occurred during resolution. + pub fn replaced_with(&self) -> Option> { + self.expect_maybe_one(KaniAttributeKind::ReplacedWith) + .map(|target| expect_key_string_value(self.tcx.sess, target)) + } + + /// Resolve a function that is known to reside in the same module as the one + /// these attributes belong to (`self.item`). + fn resolve_sibling(&self, path_str: &str) -> Result> { + resolve_fn( + self.tcx, + self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), + path_str, + ) + } + /// Check that all attributes assigned to an item is valid. /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate /// the session and emit all errors found. @@ -223,7 +276,10 @@ impl<'tcx> KaniAttributes<'tcx> { } expect_single(self.tcx, kind, &attrs); } - KaniAttributeKind::CheckedWith => { + KaniAttributeKind::StubVerified => { + expect_single(self.tcx, kind, &attrs); + } + KaniAttributeKind::CheckedWith | KaniAttributeKind::ReplacedWith => { self.expect_maybe_one(kind) .map(|attr| expect_key_string_value(&self.tcx.sess, attr)); } @@ -325,38 +381,87 @@ impl<'tcx> KaniAttributes<'tcx> { harness.unwind_value = parse_unwind(self.tcx, attributes[0]) } KaniAttributeKind::Proof => harness.proof = true, - KaniAttributeKind::ProofForContract => { - harness.proof = true; - let Some(Ok((name, id, span))) = self.interpret_the_for_contract_attribute() - else { - self.tcx.sess.span_err( - self.tcx.def_span(self.item), - format!("Invalid `{}` attribute format", kind.as_ref()), - ); - return harness; - }; - let Some(Ok(replacement_name)) = - KaniAttributes::for_item(self.tcx, id).checked_with() - else { - self.tcx - .sess - .span_err(span, "Target function for this check has no contract"); - return harness; - }; - harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); - } + KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness), + KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness), KaniAttributeKind::Unstable => { // Internal attribute which shouldn't exist here. unreachable!() } - KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => { - todo!("Contract attributes are not supported on proofs") + KaniAttributeKind::CheckedWith + | KaniAttributeKind::IsContractGenerated + | KaniAttributeKind::ReplacedWith => { + self.tcx.sess.span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); } }; harness }) } + fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) { + let sess = self.tcx.sess; + let (name, id, span) = match self.interpret_the_for_contract_attribute() { + None => unreachable!( + "impossible, was asked to handle `proof_for_contract` but didn't find such an attribute." + ), + Some(Err(_)) => return, // This error was already emitted + Some(Ok(values)) => values, + }; + let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, id).checked_with() + else { + sess.struct_span_err( + span, + format!( + "Failed to check contract: Function `{}` has no contract.", + self.item_name(), + ), + ) + .span_note(self.tcx.def_span(id), "Try adding a contract to this function.") + .emit(); + return; + }; + harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); + } + + fn handle_stub_verified(&self, harness: &mut HarnessAttributes) { + let sess = self.tcx.sess; + for contract in self.interpret_stub_verified_attribute() { + let Ok((name, def_id, span)) = contract else { + // This error has already been emitted so we can ignore it now. + // Later the session will fail anyway so we can just + // optimistically forge on and try to find more errors. + continue; + }; + let replacement_name = match KaniAttributes::for_item(self.tcx, def_id).replaced_with() + { + None => { + sess.struct_span_err( + span, + format!( + "Failed to generate verified stub: Function `{}` has no contract.", + self.item_name(), + ), + ) + .span_note( + self.tcx.def_span(def_id), + format!( + "Try adding a contract to this function or use the unsound `{}` attribute instead.", + KaniAttributeKind::Stub.as_ref(), + ) + ) + .emit(); + continue; + } + Some(Ok(replacement_name)) => replacement_name, + Some(Err(_)) => continue, + }; + harness.stubs.push(self.stub_for_relative_item(name, replacement_name)) + } + } + + fn item_name(&self) -> Symbol { + self.tcx.item_name(self.item) + } + /// Check that if this item is tagged with a proof_attribute, it is a valid harness. fn check_proof_attribute(&self, proof_attribute: &Attribute) { let span = proof_attribute.span; diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs new file mode 100644 index 000000000000..8a99f4892b0a --- /dev/null +++ b/library/kani/src/contracts.rs @@ -0,0 +1,173 @@ +// 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 +//! +//! There are currently two specification attributes available for describing +//! function behavior: [`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`. +//! +//! 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. +pub use super::{ensures, proof_for_contract, requires, stub_verified}; diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 6125c589a957..1da6a4655018 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -294,5 +294,7 @@ macro_rules! cover { }; } -/// Kani proc macros must be in a separate crate +// Kani proc macros must be in a separate crate pub use kani_macros::*; + +pub mod contracts; diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 3b4ea87636f3..89482a6266ca 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -97,9 +97,10 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } -/// Add a precondition to this function. +/// Add a precondition to this function. /// -/// This is part of the function contract API, together with [`ensures`]. +/// This is part of the function contract API, for more general information see +/// the [module-level documentation](../kani/contracts/index.html). /// /// The contents of the attribute is a condition over the input values to the /// annotated function. All Rust syntax is supported, even calling other @@ -107,11 +108,9 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// 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. -/// -/// This attribute is part of the unstable contracts API and requires -/// `-Zfunction-contracts` flag to be used. +/// [`ensures`][macro@ensures]) to have at least one designated +/// [`proof_for_contract`][macro@proof_for_contract] harness for checking the +/// contract. #[proc_macro_attribute] pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::requires(attr, item) @@ -119,7 +118,8 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { /// Add a postcondition to this function. /// -/// This is part of the function contract API, together with [`requires`]. +/// This is part of the function contract API, for more general information see +/// the [module-level documentation](../kani/contracts/index.html). /// /// 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 @@ -128,11 +128,9 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { /// 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. -/// -/// This attribute is part of the unstable contracts API and requires -/// `-Zfunction-contracts` flag to be used. +/// [`requires`][macro@requires]) to have at least one designated +/// [`proof_for_contract`][macro@proof_for_contract] harness for checking the +/// contract. #[proc_macro_attribute] pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::ensures(attr, item) @@ -144,24 +142,31 @@ pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { /// `super::some_mod::foo` or `crate::SomeStruct::foo`) to the function, the /// contract of which should be checked. /// -/// The harness is expected to set up the arguments that `foo` should be called -/// with and initialzied 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 of those types have special invariants you can use `kani::assume` to -/// enforce them, but other than condition on inputs and checks of outputs -/// should be in the contract, not the harness for maximum soundness. -/// -/// This attribute is part of the unstable contracts API and requires -/// `-Zfunction-contracts` flag to be used. +/// This is part of the function contract API, for more general information see +/// the [module-level documentation](../kani/contracts/index.html). #[proc_macro_attribute] pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::proof_for_contract(attr, item) } +/// `stub_verified(TARGET)` is a harness attribute (to be used on +/// [`proof`][macro@proof] or [`proof_for_contract`][macro@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](../contracts/index.html#specification-attributes-overview). +/// +/// 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/contracts/index.html). +#[proc_macro_attribute] +pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::stub_verified(attr, item) +} + /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] @@ -170,7 +175,7 @@ mod sysroot { mod contracts; - pub use contracts::{ensures, proof_for_contract, requires}; + pub use contracts::{ensures, proof_for_contract, requires, stub_verified}; use super::*; @@ -344,4 +349,5 @@ mod regular { no_op!(requires); no_op!(ensures); no_op!(proof_for_contract); + no_op!(stub_verified); } diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 856f25b7d597..242d3e4deba0 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -1,15 +1,182 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use std::collections::{HashMap, HashSet}; - -use proc_macro::TokenStream; - -use { - quote::{quote, ToTokens}, - syn::{parse_macro_input, spanned::Spanned, visit::Visit, Expr, ItemFn}, -}; +//! Implementation of the function contracts code generation. +//! +//! The most exciting part is the handling of `requires` and `ensures`, the main +//! entry point to which is [`requires_ensures_main`]. Most of the code +//! generation for that is implemented on [`ContractConditionsHandler`] with +//! [`ContractFunctionState`] steering the code generation. The function state +//! implements a state machine in order to be able to handle multiple attributes +//! on the same function correctly. +//! +//! ## How the handling for `requires` and `ensures` works. +//! +//! Our aim is to generate a "check" function that can be used to verify the +//! validity of the contract and a "replace" function that can be used as a +//! stub, generated from the contract that can be used instead of the original +//! function. +//! +//! Let me first introduce the constraints which we are operating under to +//! explain why we need the somewhat involved state machine to achieve this. +//! +//! Proc-macros are expanded one-at-a-time, outside-in and they can also be +//! renamed. Meaning the user can do `use kani::requires as precondition` and +//! then use `precondition` everywhere. We want to support this functionality +//! instead of throwing a hard error but this means we cannot detect if a given +//! function has further contract attributes placed on it during any given +//! expansion. As a result every expansion needs to leave the code in a valid +//! state that could be used for all contract functionality but it must alow +//! further contract attributes to compose with what was already generated. In +//! addition we also want to make sure to support non-contract attributes on +//! functions with contracts. +//! +//! To this end we use a state machine. The initial state is an "untouched" +//! function with possibly multiple contract attributes, none of which have been +//! expanded. When we expand the first (outermost) `requires` or `ensures` +//! attribute on such a function we re-emit the function unchanged but we also +//! generate fresh "check" and "replace" functions that enforce the condition +//! carried by the attribute currently being expanded. We copy all additional +//! attributes from the original function to both the "check" and the "replace". +//! This allows us to deal both with renaming and also support non-contract +//! attributes. +//! +//! In addition to copying attributes we also add new marker attributes to +//! advance the state machine. The "check" function gets a +//! `kanitool::is_contract_generated(check)` attributes and analogous for +//! replace. The re-emitted original meanwhile is decorated with +//! `kanitool::checked_with(name_of_generated_check_function)` and an analogous +//! `kanittool::replaced_with` attribute also. The next contract attribute that +//! is expanded will detect the presence of these markers in the attributes of +//! the item and be able to determine their position in the state machine this +//! way. If the state is either a "check" or "replace" then the body of the +//! function is augmented with the additional conditions carried by the macro. +//! If the state is the "original" function, no changes are performed. +//! +//! We place marker attributes at the bottom of the attribute stack (innermost), +//! otherwise they would not be visible to the future macro expansions. +//! +//! Below you can see a graphical rendering where boxes are states and each +//! arrow represents the expansion of a `requires` or `ensures` macro. +//! +//! ```plain +//! v +//! +-----------+ +//! | Untouched | +//! | Function | +//! +-----+-----+ +//! | +//! Emit | Generate + Copy Attributes +//! +-----------------+------------------+ +//! | | | +//! | | | +//! v v v +//! +----------+ +-------+ +---------+ +//! | Original |<-+ | Check |<-+ | Replace |<-+ +//! +--+-------+ | +---+---+ | +----+----+ | +//! | | Ignore | | Augment | | Augment +//! +----------+ +------+ +-------+ +//! +//! | | | | +//! +--------------+ +------------------------------+ +//! Presence of Presence of +//! "checked_with" "is_contract_generated" +//! +//! State is detected via +//! ``` +//! +//! All named arguments of the annotated function are unsafely shallow-copied +//! with the `kani::untracked_deref` function to circumvent the borrow checker +//! for postconditions. The case where this is relevant is if you want to return +//! a mutable borrow from the function which means any immutable borrow in the +//! postcondition would be illegal. We must ensure that those copies are not +//! dropped (causing a double-free) so after the postconditions we call +//! `mem::forget` on each copy. +//! +//! ## Check function +//! +//! Generates a `check__` function that assumes preconditions +//! and asserts postconditions. The check function is also marked as generated +//! with the `#[kanitool::is_contract_generated(check)]` attribute. +//! +//! Decorates the original function with `#[kanitool::checked_by = +//! "check__"]`. +//! +//! The check function is a copy of the original function with preconditions +//! added before the body and postconditions after as well as injected before +//! every `return` (see [`PostconditionInjector`]). Attributes on the original +//! function are also copied to the check function. +//! +//! ## Replace Function +//! +//! As the mirror to that also generates a `replace__` +//! function that asserts preconditions and assumes postconditions. The replace +//! function is also marked as generated with the +//! `#[kanitool::is_contract_generated(replace)]` attribute. +//! +//! Decorates the original function with `#[kanitool::replaced_by = +//! "replace__"]`. +//! +//! The replace function has the same signature as the original function but its +//! body is replaced by `kani::any()`, which generates a non-deterministic +//! value. +//! +//! # Complete example +//! +//! ``` +//! #[kani::requires(divisor != 0)] +//! #[kani::ensures(result <= dividend)] +//! fn div(dividend: u32, divisor: u32) -> u32 { +//! dividend / divisor +//! } +//! ``` +//! +//! Turns into +//! +//! ``` +//! #[kanitool::checked_with = "div_check_965916"] +//! #[kanitool::replaced_with = "div_replace_965916"] +//! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } +//! +//! #[allow(dead_code)] +//! #[allow(unused_variables)] +//! #[kanitool::is_contract_generated(check)] +//! fn div_check_965916(dividend: u32, divisor: u32) -> u32 { +//! let dividend_renamed = kani::untracked_deref(÷nd); +//! let divisor_renamed = kani::untracked_deref(&divisor); +//! let result = { kani::assume(divisor != 0); { dividend / divisor } }; +//! kani::assert(result <= dividend_renamed, "result <= dividend"); +//! std::mem::forget(dividend_renamed); +//! std::mem::forget(divisor_renamed); +//! result +//! } +//! +//! #[allow(dead_code)] +//! #[allow(unused_variables)] +//! #[kanitool::is_contract_generated(replace)] +//! fn div_replace_965916(dividend: u32, divisor: u32) -> u32 { +//! kani::assert(divisor != 0, "divisor != 0"); +//! let dividend_renamed = kani::untracked_deref(÷nd); +//! let divisor_renamed = kani::untracked_deref(&divisor); +//! let result = kani::any(); +//! kani::assume(result <= dividend_renamed, "result <= dividend"); +//! std::mem::forget(dividend_renamed); +//! std::mem::forget(divisor_renamed); +//! result +//! } +//! ``` + +use proc_macro::{Diagnostic, TokenStream}; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; +use quote::{quote, ToTokens}; +use std::{ + borrow::Cow, + collections::{HashMap, HashSet}, +}; +use syn::{ + parse_macro_input, spanned::Spanned, visit::Visit, visit_mut::VisitMut, Attribute, Expr, + ItemFn, PredicateType, ReturnType, Signature, TraitBound, TypeParamBound, WhereClause, +}; /// Create a unique hash for a token stream (basically a [`std::hash::Hash`] /// impl for `proc_macro2::TokenStream`). @@ -29,8 +196,6 @@ fn hash_of_token_stream(hasher: &mut H, stream: proc_macro } } -use syn::visit_mut::VisitMut; - /// Hash this `TokenStream` and return an integer that is at most digits /// long when hex formatted. fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { @@ -50,11 +215,11 @@ fn identifier_for_generated_function(related_function: &ItemFn, purpose: &str, h } pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { - requires_ensures_alt(attr, item, true) + requires_ensures_main(attr, item, true) } pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { - requires_ensures_alt(attr, item, false) + requires_ensures_main(attr, item, false) } /// Collect all named identifiers used in the argument patterns of a function. @@ -92,7 +257,7 @@ impl<'a> VisitMut for Renamer<'a> { /// This restores shadowing. Without this we would rename all ident /// occurrences, but not rebinding location. This is because our - /// [`visit_expr_path_mut`] is scope-unaware. + /// [`Self::visit_expr_path_mut`] is scope-unaware. fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) { if let Some(new) = self.0.get(&i.ident) { i.ident = new.clone(); @@ -120,7 +285,7 @@ where && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) } -/// Classifies the state a function is in the contract handling pipeline. +/// Classifies the state a function is in in the contract handling pipeline. #[derive(Clone, Copy, PartialEq, Eq)] enum ContractFunctionState { /// This is the original code, re-emitted from a contract attribute. @@ -131,34 +296,62 @@ enum ContractFunctionState { /// This is a check function that was generated from a previous evaluation /// of a contract attribute. Check, + /// This is a replace function that was generated from a previous evaluation + /// of a contract attribute. + Replace, } -impl ContractFunctionState { +impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState { + type Error = Option; + /// Find out if this attribute could be describing a "contract handling" /// state and if so return it. - fn from_attribute(attribute: &syn::Attribute) -> Option { + fn try_from(attribute: &'a syn::Attribute) -> Result { if let syn::Meta::List(lst) = &attribute.meta { if matches_path(&lst.path, &["kanitool", "is_contract_generated"]) { - match syn::parse2::(lst.tokens.clone()) { - Err(e) => { - lst.span().unwrap().error(format!("{e}")).emit(); + let ident = syn::parse2::(lst.tokens.clone()) + .map_err(|e| Some(lst.span().unwrap().error(format!("{e}"))))?; + let ident_str = ident.to_string(); + return match ident_str.as_str() { + "check" => Ok(Self::Check), + "replace" => Ok(Self::Replace), + _ => { + Err(Some(lst.span().unwrap().error("Expected `check` or `replace` ident"))) } - Ok(ident) => { - if ident.to_string() == "check" { - return Some(Self::Check); - } else { - lst.span().unwrap().error("Expected `check` ident").emit(); - } - } - } + }; } } if let syn::Meta::NameValue(nv) = &attribute.meta { if matches_path(&nv.path, &["kanitool", "checked_with"]) { - return Some(ContractFunctionState::Original); + return Ok(ContractFunctionState::Original); } } - None + Err(None) + } +} + +impl ContractFunctionState { + // If we didn't find any other contract handling related attributes we + // assume this function has not been touched by a contract before. + fn from_attributes(attributes: &[syn::Attribute]) -> Self { + attributes + .iter() + .find_map(|attr| { + let state = ContractFunctionState::try_from(attr); + if let Err(Some(diag)) = state { + diag.emit(); + None + } else { + state.ok() + } + }) + .unwrap_or(ContractFunctionState::Untouched) + } + + /// Do we need to emit the `is_contract_generated` tag attribute on the + /// generated function(s)? + fn emit_tag_attr(self) -> bool { + matches!(self, ContractFunctionState::Untouched) } } @@ -183,7 +376,7 @@ impl ContractFunctionState { struct PostconditionInjector(TokenStream2); impl VisitMut for PostconditionInjector { - /// We leave this emtpy to stop the recursion here. We don't want to look + /// We leave this empty to stop the recursion here. We don't want to look /// inside the closure, because the return statements contained within are /// for a different function. fn visit_expr_closure_mut(&mut self, _: &mut syn::ExprClosure) {} @@ -218,7 +411,7 @@ impl VisitMut for PostconditionInjector { /// - Creates new names for them; /// - Replaces all occurrences of those idents in `attrs` with the new names and; /// - Returns the mapping of old names to new names. -fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { +fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { let mut arg_ident_collector = ArgumentIdentCollector::new(); arg_ident_collector.visit_signature(&sig); @@ -237,179 +430,382 @@ fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap< arg_idents } -/// The main meat of handling requires/ensures contracts. -/// -/// Generates a `check__` function that assumes preconditions -/// and asserts postconditions. The check function is also marked as generated -/// with the `#[kanitool::is_contract_generated(check)]` attribute. -/// -/// Decorates the original function with `#[kanitool::checked_by = -/// "check__"] -/// -/// The check function is a copy of the original function with preconditions -/// added before the body and postconditions after as well as injected before -/// every `return` (see [`PostconditionInjector`]). Attributes on the original -/// function are also copied to the check function. Each clause (requires or -/// ensures) after the first clause will be ignored on the original function -/// (detected by finding the `kanitool::checked_with` attribute). On the check -/// function (detected by finding the `kanitool::is_contract_generated` -/// attribute) it expands into a new layer of pre- or postconditions. This state -/// machine is also explained in more detail in comments in the body of this -/// macro. -/// -/// In the check function all named arguments of the function are unsafely -/// shallow-copied with the `kani::untracked_deref` function to circumvent the -/// borrow checker for postconditions. We must ensure that those copies are not -/// dropped so after the postconditions we call `mem::forget` on each copy. -/// -/// # Complete example +/// The information needed to generate the bodies of check and replacement +/// functions that integrate the conditions from this contract attribute. +struct ContractConditionsHandler<'a> { + function_state: ContractFunctionState, + /// Information specific to the type of contract attribute we're expanding. + condition_type: ContractConditionsType, + /// The contents of the attribute. + attr: Expr, + /// Body of the function this attribute was found on. + annotated_fn: &'a ItemFn, + /// An unparsed, unmodified copy of `attr`, used in the error messages. + attr_copy: TokenStream2, + /// The stream to which we should write the generated code. + output: &'a mut TokenStream2, +} + +/// Information needed for generating check and replace handlers for different +/// contract attributes. +enum ContractConditionsType { + Requires, + Ensures { + /// Translation map from original argument names to names of the copies + /// we will be emitting. + argument_names: HashMap, + }, +} + +impl ContractConditionsType { + /// Constructs a [`Self::Ensures`] from the signature of the decorated + /// function and the contents of the decorating attribute. + /// + /// Renames the [`Ident`]s used in `attr` and stores the translation map in + /// `argument_names`. + fn new_ensures(sig: &Signature, attr: &mut Expr) -> Self { + let argument_names = rename_argument_occurrences(sig, attr); + ContractConditionsType::Ensures { argument_names } + } +} + +impl<'a> ContractConditionsHandler<'a> { + /// Initialize the handler. Constructs the required + /// [`ContractConditionsType`] depending on `is_requires`. + fn new( + function_state: ContractFunctionState, + is_requires: bool, + mut attr: Expr, + annotated_fn: &'a ItemFn, + attr_copy: TokenStream2, + output: &'a mut TokenStream2, + ) -> Self { + let condition_type = if is_requires { + ContractConditionsType::Requires + } else { + ContractConditionsType::new_ensures(&annotated_fn.sig, &mut attr) + }; + + Self { function_state, condition_type, attr, annotated_fn, attr_copy, output } + } + + /// Create the body of a check function. + /// + /// Wraps the conditions from this attribute around `self.body`. + fn make_check_body(&self) -> TokenStream2 { + let Self { attr, attr_copy, .. } = self; + let ItemFn { sig, block, .. } = self.annotated_fn; + let return_type = return_type_to_type(&sig.output); + + match &self.condition_type { + ContractConditionsType::Requires => quote!( + kani::assume(#attr); + #block + ), + ContractConditionsType::Ensures { argument_names } => { + let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); + + // The code that enforces the postconditions and cleans up the shallow + // argument copies (with `mem::forget`). + let exec_postconditions = quote!( + kani::assert(#attr, stringify!(#attr_copy)); + #copy_clean + ); + + // We make a copy here because we'll modify it. Technically not + // necessary but could lead to weird results if + // `make_replace_body` were called after this if we modified in + // place. + let mut call = block.clone(); + let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); + inject_conditions.visit_block_mut(&mut call); + + quote!( + #arg_copies + let result : #return_type = #call; + #exec_postconditions + result + ) + } + } + } + + /// Create the body of a stub for this contract. + /// + /// Wraps the conditions from this attribute around a prior call. If + /// `use_nondet_result` is `true` we will use `kani::any()` to create a + /// result, otherwise whatever the `body` of our annotated function was. + /// + /// `use_nondet_result` will only be true if this is the first time we are + /// generating a replace function. + fn make_replace_body(&self, use_nondet_result: bool) -> TokenStream2 { + let Self { attr, attr_copy, .. } = self; + let ItemFn { sig, block, .. } = self.annotated_fn; + let call_to_prior = + if use_nondet_result { quote!(kani::any()) } else { block.to_token_stream() }; + let return_type = return_type_to_type(&sig.output); + + match &self.condition_type { + ContractConditionsType::Requires => quote!( + kani::assert(#attr, stringify!(#attr_copy)); + #call_to_prior + ), + ContractConditionsType::Ensures { argument_names } => { + let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); + quote!( + #arg_copies + let result: #return_type = #call_to_prior; + kani::assume(#attr); + #copy_clean + result + ) + } + } + } + + /// Emit the check function into the output stream. + /// + /// See [`Self::make_check_body`] for the most interesting parts of this + /// function. + fn emit_check_function(&mut self, check_function_ident: Ident) { + self.emit_common_header(); + + if self.function_state.emit_tag_attr() { + // If it's the first time we also emit this marker. Again, order is + // important so this happens as the last emitted attribute. + self.output.extend(quote!(#[kanitool::is_contract_generated(check)])); + } + let body = self.make_check_body(); + let mut sig = self.annotated_fn.sig.clone(); + sig.ident = check_function_ident; + self.output.extend(quote!( + #sig { + #body + } + )) + } + + /// Emit the replace funtion into the output stream. + /// + /// See [`Self::make_replace_body`] for the most interesting parts of this + /// function. + fn emit_replace_function(&mut self, replace_function_ident: Ident, is_first_emit: bool) { + self.emit_common_header(); + + if self.function_state.emit_tag_attr() { + // If it's the first time we also emit this marker. Again, order is + // important so this happens as the last emitted attribute. + self.output.extend(quote!(#[kanitool::is_contract_generated(replace)])); + } + let mut sig = self.annotated_fn.sig.clone(); + if is_first_emit { + attach_require_kani_any(&mut sig); + } + let body = self.make_replace_body(is_first_emit); + sig.ident = replace_function_ident; + + // Finally emit the check function itself. + self.output.extend(quote!( + #sig { + #body + } + )); + } + + /// Emit attributes common to check or replace function into the output + /// stream. + fn emit_common_header(&mut self) { + if self.function_state.emit_tag_attr() { + self.output.extend(quote!( + #[allow(dead_code, unused_variables)] + )); + } + self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream)); + } +} + +/// If an explicit return type was provided it is returned, otherwise `()`. +fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { + match return_type { + syn::ReturnType::Default => Cow::Owned(syn::Type::Tuple(syn::TypeTuple { + paren_token: syn::token::Paren::default(), + elems: Default::default(), + })), + syn::ReturnType::Type(_, typ) => Cow::Borrowed(typ.as_ref()), + } +} + +/// Looks complicated but does something very simple: attach a bound for +/// `kani::Arbitrary` on the return type to the provided signature. Pushes it +/// onto a preexisting where condition, initializing a new `where` condition if +/// it doesn't already exist. /// -/// ```rs -/// #[kani::requires(divisor != 0)] -/// #[kani::ensures(result <= dividend)] -/// fn div(dividend: u32, divisor: u32) -> u32 { -/// dividend / divisor -/// } -/// ``` +/// Very simple example: `fn foo() -> usize { .. }` would be rewritten `fn foo() +/// -> usize where usize: kani::Arbitrary { .. }`. /// -/// Turns into +/// This is called when we first emit a replace function. Later we can rely on +/// this bound already being present. +fn attach_require_kani_any(sig: &mut Signature) { + if matches!(sig.output, ReturnType::Default) { + // It's the default return type, e.g. `()` so we can skip adding the + // constraint. + return; + } + let return_ty = return_type_to_type(&sig.output); + let where_clause = sig.generics.where_clause.get_or_insert_with(|| WhereClause { + where_token: syn::Token![where](Span::call_site()), + predicates: Default::default(), + }); + + where_clause.predicates.push(syn::WherePredicate::Type(PredicateType { + lifetimes: None, + bounded_ty: return_ty.into_owned(), + colon_token: syn::Token![:](Span::call_site()), + bounds: [TypeParamBound::Trait(TraitBound { + paren_token: None, + modifier: syn::TraitBoundModifier::None, + lifetimes: None, + path: syn::Path { + leading_colon: None, + segments: [ + syn::PathSegment { + ident: Ident::new("kani", Span::call_site()), + arguments: syn::PathArguments::None, + }, + syn::PathSegment { + ident: Ident::new("Arbitrary", Span::call_site()), + arguments: syn::PathArguments::None, + }, + ] + .into_iter() + .collect(), + }, + })] + .into_iter() + .collect(), + })) +} + +/// We make shallow copies of the argument for the postconditions in both +/// `requires` and `ensures` clauses and later clean them up. /// -/// ```rs -/// #[kanitool::checked_with = "div_check_965916"] -/// fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } +/// This function creates the code necessary to both make the copies (first +/// tuple elem) and to clean them (second tuple elem). +fn make_unsafe_argument_copies( + renaming_map: &HashMap, +) -> (TokenStream2, TokenStream2) { + let arg_names = renaming_map.values(); + let also_arg_names = renaming_map.values(); + let arg_values = renaming_map.keys(); + ( + quote!(#(let #arg_names = kani::untracked_deref(&#arg_values);)*), + quote!(#(std::mem::forget(#also_arg_names);)*), + ) +} + +/// The main meat of handling requires/ensures contracts. /// -/// #[allow(dead_code)] -/// #[allow(unused_variables)] -/// #[kanitool::is_contract_generated(check)] -/// fn div_check_965916(dividend: u32, divisor: u32) -> u32 { -/// let dividend_renamed = kani::untracked_deref(÷nd); -/// let divisor_renamed = kani::untracked_deref(&divisor); -/// let result = { kani::assume(divisor != 0); { dividend / divisor } }; -/// kani::assert(result <= dividend_renamed, "result <= dividend"); -/// std::mem::forget(dividend_renamed); -/// std::mem::forget(divisor_renamed); -/// result -/// } -/// ``` -fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { - let attr_copy = proc_macro2::TokenStream::from(attr.clone()); - let mut attr = parse_macro_input!(attr as Expr); +/// See the [module level documentation][self] for a description of how the code +/// generation works. +fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { + let attr_copy = TokenStream2::from(attr.clone()); + let attr = parse_macro_input!(attr as Expr); let mut output = proc_macro2::TokenStream::new(); + let item_stream_clone = item.clone(); + let item_fn = parse_macro_input!(item as ItemFn); - let a_short_hash = short_hash_of_token_stream(&item); - let item_fn = &mut parse_macro_input!(item as ItemFn); - - // If we didn't find any other contract handling related attributes we - // assume this function has not been touched by a contract before. - let function_state = item_fn - .attrs - .iter() - .find_map(ContractFunctionState::from_attribute) - .unwrap_or(ContractFunctionState::Untouched); + let function_state = ContractFunctionState::from_attributes(&item_fn.attrs); if matches!(function_state, ContractFunctionState::Original) { // If we're the original function that means we're *not* the first time // that a contract attribute is handled on this function. This means // there must exist a generated check function somewhere onto which the // attributes have been copied and where they will be expanded into more - // checks. So we just return outselves unchanged. + // checks. So we just return ourselves unchanged. + // + // Since this is the only function state case that doesn't need a + // handler to be constructed, we do this match early, separately. return item_fn.into_token_stream().into(); } - let attrs = std::mem::replace(&mut item_fn.attrs, vec![]); - - if matches!(function_state, ContractFunctionState::Untouched) { - // We are the first time a contract is handled on this function, so - // we're responsible for: - // 1. Generating a name for the check function; - // 2. Emitting the original, unchanged item and register the check - // function on it via attribute; - // 3. Renaming our item to the new name; - // 4. And (minor point) adding #[allow(dead_code)] and - // #[allow(unused_variables)] to the check function attributes. - - let check_fn_name = identifier_for_generated_function(item_fn, "check", a_short_hash); - - // Constructing string literals explicitly here, because `stringify!` - // doesn't work. Let's say we have an identifier `check_fn` and we were - // to do `quote!(stringify!(check_fn))` to try to have it expand to - // `"check_fn"` in the generated code. Then when the next macro parses - // this it will *not* see the literal `"check_fn"` as you may expect but - // instead the *expression* `stringify!(check_fn)`. - let check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); - - // The order of `attrs` and `kanitool::{checked_with, - // is_contract_generated}` is important here, because macros are - // expanded outside in. This way other contract annotations in `attrs` - // sees those attribuites and can use them to determine - // `function_state`. - // - // We're emitting the original here but the same applies later when we - // emit the check function. - output.extend(quote!( - #(#attrs)* - #[kanitool::checked_with = #check_fn_name_str] - #item_fn - - #[allow(dead_code)] - #[allow(unused_variables)] - )); - item_fn.sig.ident = check_fn_name; - } + let mut handler = ContractConditionsHandler::new( + function_state, + is_requires, + attr, + &item_fn, + attr_copy, + &mut output, + ); + + match function_state { + ContractFunctionState::Check => { + // The easy cases first: If we are on a check or replace function + // emit them again but with additional conditions layered on. + // + // Since we are already on the check function, it will have an + // appropriate, unique generated name which we are just going to + // pass on. + handler.emit_check_function(item_fn.sig.ident.clone()); + } + ContractFunctionState::Replace => { + // Analogous to above + handler.emit_replace_function(item_fn.sig.ident.clone(), false); + } + ContractFunctionState::Original => { + unreachable!("Impossible: This is handled via short circuiting earlier.") + } + ContractFunctionState::Untouched => { + // The complex case. We are the first time a contract is handled on this function, so + // we're responsible for + // + // 1. Generating a name for the check function + // 2. Emitting the original, unchanged item and register the check + // function on it via attribute + // 3. Renaming our item to the new name + // 4. And (minor point) adding #[allow(dead_code)] and + // #[allow(unused_variables)] to the check function attributes + + // We'll be using this to postfix the generated names for the "check" + // and "replace" functions. + let item_hash = short_hash_of_token_stream(&item_stream_clone); + + let check_fn_name = identifier_for_generated_function(&item_fn, "check", item_hash); + let replace_fn_name = identifier_for_generated_function(&item_fn, "replace", item_hash); + + // Constructing string literals explicitly here, because `stringify!` + // doesn't work. Let's say we have an identifier `check_fn` and we were + // to do `quote!(stringify!(check_fn))` to try to have it expand to + // `"check_fn"` in the generated code. Then when the next macro parses + // this it will *not* see the literal `"check_fn"` as you may expect but + // instead the *expression* `stringify!(check_fn)`. + let replace_fn_name_str = + syn::LitStr::new(&replace_fn_name.to_string(), Span::call_site()); + let check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); + + // The order of `attrs` and `kanitool::{checked_with, + // is_contract_generated}` is important here, because macros are + // expanded outside in. This way other contract annotations in `attrs` + // sees those attributes and can use them to determine + // `function_state`. + // + // The same care is taken when we emit check and replace functions. + // emit the check function. + let ItemFn { attrs, vis, sig, block } = &item_fn; + handler.output.extend(quote!( + #(#attrs)* + #[kanitool::checked_with = #check_fn_name_str] + #[kanitool::replaced_with = #replace_fn_name_str] + #vis #sig { + #block + } + )); - let call_to_prior = &mut item_fn.block; - - let check_body = if is_requires { - quote!( - kani::assume(#attr); - #call_to_prior - ) - } else { - let arg_idents = rename_argument_occurences(&item_fn.sig, &mut attr); - - let arg_copy_names = arg_idents.values(); - let also_arg_copy_names = arg_copy_names.clone(); - let arg_idents = arg_idents.keys(); - - // The code that enforces the postconditions and cleans up the shallow - // argument copies (with `mem::forget`). - let exec_postconditions = quote!( - kani::assert(#attr, stringify!(#attr_copy)); - #(std::mem::forget(#also_arg_copy_names);)* - ); - - let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); - inject_conditions.visit_block_mut(&mut *call_to_prior); - - quote!( - #(let #arg_copy_names = kani::untracked_deref(&#arg_idents);)* - let result = #call_to_prior; - #exec_postconditions - result - ) - }; - - let sig = &item_fn.sig; - - // Prepare emitting the check function by emitting the rest of the - // attributes. - output.extend(quote!( - #(#attrs)* - )); - - if matches!(function_state, ContractFunctionState::Untouched) { - // If it's the first time we also emit this marker. Again, order is - // important so this happens as the last emitted attribute. - output.extend(quote!(#[kanitool::is_contract_generated(check)])); + handler.emit_check_function(check_fn_name); + handler.emit_replace_function(replace_fn_name, true); + } } - // Finally emit the check function itself. - output.extend(quote!( - #sig { - #check_body - } - )); output.into() } @@ -436,4 +832,5 @@ macro_rules! passthrough { } } +passthrough!(stub_verified, false); passthrough!(proof_for_contract, true); diff --git a/tests/expected/function-contract/gcd_replacement_fail.expected b/tests/expected/function-contract/gcd_replacement_fail.expected new file mode 100644 index 000000000000..a993325bd5e5 --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_fail.expected @@ -0,0 +1,17 @@ +Frac::check_equals.assertion\ +- Status: FAILURE\ +- Description: "attempt to calculate the remainder with a divisor of zero" + +Frac::check_equals.assertion\ +- Status: FAILURE\ +- Description: "assertion failed: self.den % f2.den == 0" + +Frac::check_equals.assertion\ +- Status: FAILURE\ +- Description: "assertion failed: gcd1 == gcd2" + +Failed Checks: attempt to calculate the remainder with a divisor of zero +Failed Checks: assertion failed: self.den % f2.den == 0 +Failed Checks: assertion failed: gcd1 == gcd2 + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_replacement_fail.rs b/tests/expected/function-contract/gcd_replacement_fail.rs new file mode 100644 index 000000000000..8bd59c5c14fe --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_fail.rs @@ -0,0 +1,67 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + min = res; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof] +#[kani::stub_verified(gcd)] +fn main() { + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_replacement_pass.expected b/tests/expected/function-contract/gcd_replacement_pass.expected new file mode 100644 index 000000000000..48d3565ef9f1 --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_pass.expected @@ -0,0 +1,17 @@ +gcd.assertion\ +- Status: SUCCESS\ +- Description: "x != 0 && y != 0" + +Frac::check_equals.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: self.num % f2.num == 0" + +Frac::check_equals.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: self.den % f2.den == 0" + +Frac::check_equals.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: gcd1 == gcd2" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_replacement_pass.rs b/tests/expected/function-contract/gcd_replacement_pass.rs new file mode 100644 index 000000000000..9827dd3a1512 --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_pass.rs @@ -0,0 +1,67 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + min = res; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof] +#[kani::stub_verified(gcd)] +fn main() { + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/missing_contract_for_check.expected b/tests/expected/function-contract/missing_contract_for_check.expected new file mode 100644 index 000000000000..6836fb06f0a6 --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_check.expected @@ -0,0 +1,9 @@ +error: Failed to check contract: Function `harness` has no contract. + | +7 | #[kani::proof_for_contract(no_contract)] + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | +note: Try adding a contract to this function. + | +5 | fn no_contract() {} + | ^^^^^^^^^^^^^^^^ diff --git a/tests/expected/function-contract/missing_contract_for_check.rs b/tests/expected/function-contract/missing_contract_for_check.rs new file mode 100644 index 000000000000..1fccd1ed7448 --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_check.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +fn no_contract() {} + +#[kani::proof_for_contract(no_contract)] +fn harness() { + no_contract(); +} diff --git a/tests/expected/function-contract/missing_contract_for_replace.expected b/tests/expected/function-contract/missing_contract_for_replace.expected new file mode 100644 index 000000000000..29f3fa955307 --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_replace.expected @@ -0,0 +1,9 @@ +error: Failed to generate verified stub: Function `harness` has no contract. + | +8 | #[kani::stub_verified(no_contract)] + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | +note: Try adding a contract to this function or use the unsound `stub` attribute instead. + | +5 | fn no_contract() {} + | ^^^^^^^^^^^^^^^^ diff --git a/tests/expected/function-contract/missing_contract_for_replace.rs b/tests/expected/function-contract/missing_contract_for_replace.rs new file mode 100644 index 000000000000..25abe89bb80e --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_replace.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +fn no_contract() {} + +#[kani::proof] +#[kani::stub_verified(no_contract)] +fn harness() { + no_contract(); +} diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs index 07da23e907a3..e5151396898d 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs @@ -1,14 +1,25 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts - #![allow(unreachable_code, unused_variables)] +extern crate kani; + static mut B: bool = false; +/// This only exists so I can fake a [`kani::Arbitrary`] instance for `&mut +/// bool`. +struct ArbitraryPointer

(P); + +impl<'a> kani::Arbitrary for ArbitraryPointer<&'a mut bool> { + fn any() -> Self { + ArbitraryPointer(unsafe { &mut B as &'a mut bool }) + } +} + #[kani::ensures(true)] -fn allowed_mut_return_ref<'a>() -> &'a mut bool { - unsafe { &mut B as &'a mut bool } +fn allowed_mut_return_ref<'a>() -> ArbitraryPointer<&'a mut bool> { + ArbitraryPointer(unsafe { &mut B as &'a mut bool }) } #[kani::proof_for_contract(allowed_mut_return_ref)] diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs index 44e57ed9bc9d..fc279667ad13 100644 --- a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs +++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs @@ -4,8 +4,18 @@ #![allow(unreachable_code, unused_variables)] +/// This only exists so I can fake a [`kani::Arbitrary`] instance for `*const +/// usize`. +struct ArbitraryPointer

(P); + +impl kani::Arbitrary for ArbitraryPointer<*const usize> { + fn any() -> Self { + unreachable!() + } +} + #[kani::ensures(true)] -fn return_pointer() -> *const usize { +fn return_pointer() -> ArbitraryPointer<*const usize> { unreachable!() } diff --git a/tests/expected/function-contract/simple_replace_fail.expected b/tests/expected/function-contract/simple_replace_fail.expected new file mode 100644 index 000000000000..b6806befc22c --- /dev/null +++ b/tests/expected/function-contract/simple_replace_fail.expected @@ -0,0 +1,3 @@ +main.assertion\ +- Status: FAILURE\ +- Description: ""contract doesn't guarantee equality"" diff --git a/tests/expected/function-contract/simple_replace_fail.rs b/tests/expected/function-contract/simple_replace_fail.rs new file mode 100644 index 000000000000..33a531a3aef7 --- /dev/null +++ b/tests/expected/function-contract/simple_replace_fail.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(divisor != 0)] +#[kani::ensures(result <= dividend)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof] +#[kani::stub_verified(div)] +fn main() { + assert!(div(9, 4) == 2, "contract doesn't guarantee equality"); +} diff --git a/tests/expected/function-contract/simple_replace_pass.expected b/tests/expected/function-contract/simple_replace_pass.expected new file mode 100644 index 000000000000..e1fc78ca462f --- /dev/null +++ b/tests/expected/function-contract/simple_replace_pass.expected @@ -0,0 +1,9 @@ +div.assertion\ +- Status: SUCCESS\ +- Description: "divisor != 0" + +main.assertion\ +- Status: SUCCESS\ +- Description: ""contract guarantees smallness"" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_replace_pass.rs b/tests/expected/function-contract/simple_replace_pass.rs new file mode 100644 index 000000000000..0dcc6cd59fe3 --- /dev/null +++ b/tests/expected/function-contract/simple_replace_pass.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(divisor != 0)] +#[kani::ensures(result <= dividend)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof] +#[kani::stub_verified(div)] +fn main() { + assert!(div(9, 1) != 10, "contract guarantees smallness"); +} diff --git a/tests/expected/function-contract/type_annotation_needed.expected b/tests/expected/function-contract/type_annotation_needed.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/type_annotation_needed.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/type_annotation_needed.rs b/tests/expected/function-contract/type_annotation_needed.rs new file mode 100644 index 000000000000..09b20443d47b --- /dev/null +++ b/tests/expected/function-contract/type_annotation_needed.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result.is_some())] +fn or_default(opt: Option) -> Option { + opt.or(Some(T::default())) +} + +#[kani::proof_for_contract(or_default)] +fn harness() { + let input: Option = kani::any(); + or_default(input); +} From a20437a54fdc28203dc4154255848dad3d93ed47 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 29 Sep 2023 13:13:34 -0400 Subject: [PATCH 05/13] Avoid mismatch when generating structs that represent scalar data but also include ZSTs (#2794) This change considers another case for the code generation of scalar data. In particular, when the expected type is an ADT, we previously considered two cases: either there is no field or there is one. But in cases where the ADT includes a ZST, the ADT will contain multiple fields: one associated to the scalar data, and other fields associated to the ZSTs. In those cases, we ended up crashing as in #2680: ```rust error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9: assertion failed: `(left == right)` left: `2`, right: `1`: Error in struct_expr; mismatch in number of fields and values. StructTag("tag-_161424092592971241517604180463813633314") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]. thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9: assertion failed: `(left == right)` left: `2`, right: `1`: Error in struct_expr; mismatch in number of fields and values. StructTag("tag-_161424092592971241517604180463813633314") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }] ``` With the changes in this PR, that's no longer the case. Resolves #2364 Resolves #2680 --- .../codegen_cprover_gotoc/codegen/operand.rs | 56 ++++++++++--------- .../codegen-scalar-with-phantom/Cargo.toml | 11 ++++ .../check_phantom_data.expected | 4 ++ .../codegen-scalar-with-phantom/src/lib.rs | 21 +++++++ .../codegen-scalar-with-zsts/Cargo.toml | 11 ++++ .../check_zst.expected | 4 ++ .../codegen-scalar-with-zsts/src/lib.rs | 17 ++++++ 7 files changed, 98 insertions(+), 26 deletions(-) create mode 100644 tests/cargo-kani/codegen-scalar-with-phantom/Cargo.toml create mode 100644 tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected create mode 100644 tests/cargo-kani/codegen-scalar-with-phantom/src/lib.rs create mode 100644 tests/cargo-kani/codegen-scalar-with-zsts/Cargo.toml create mode 100644 tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected create mode 100644 tests/cargo-kani/codegen-scalar-with-zsts/src/lib.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 687761e134a7..45ce90880fd6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -303,38 +303,39 @@ impl<'tcx> GotocCtx<'tcx> { } } (Scalar::Int(_), ty::Adt(adt, subst)) => { - if adt.is_struct() || adt.is_union() { - // in this case, we must have a one variant ADT. there are two cases - let variant = &adt.variants().raw[0]; - // if there is no field, then it's just a ZST - if variant.fields.is_empty() { - if adt.is_struct() { - let overall_t = self.codegen_ty(ty); - Expr::struct_expr_from_values(overall_t, vec![], &self.symbol_table) - } else { - unimplemented!() - } - } else { - // otherwise, there is just one field, which is stored as the scalar data - let field = &variant.fields[0usize.into()]; - let fty = field.ty(self.tcx, subst); - - let overall_t = self.codegen_ty(ty); - if adt.is_struct() { - self.codegen_single_variant_single_field(s, span, overall_t, fty) - } else { - unimplemented!() - } - } - } else { - // if it's an enum + if adt.is_struct() { + // In this case, we must have a one variant ADT. + let variant = adt.non_enum_variant(); + let overall_type = self.codegen_ty(ty); + // There must be at least one field associated with the scalar data. + // Any additional fields correspond to ZSTs. + let field_types: Vec> = + variant.fields.iter().map(|f| f.ty(self.tcx, subst)).collect(); + // Check that there is a single non-ZST field. + let non_zst_types: Vec<_> = + field_types.iter().filter(|t| !self.is_zst(**t)).collect(); + assert!( + non_zst_types.len() == 1, + "error: expected exactly one field whose type is not a ZST" + ); + let field_values: Vec = field_types + .iter() + .map(|t| { + if self.is_zst(*t) { + Expr::init_unit(self.codegen_ty(*t), &self.symbol_table) + } else { + self.codegen_scalar(s, *t, span) + } + }) + .collect(); + Expr::struct_expr_from_values(overall_type, field_values, &self.symbol_table) + } else if adt.is_enum() { let layout = self.layout_of(ty); let overall_t = self.codegen_ty(ty); match &layout.variants { Variants::Single { index } => { // here we must have one variant let variant = &adt.variants()[*index]; - match variant.fields.len() { 0 => Expr::struct_expr_from_values( overall_t, @@ -398,6 +399,9 @@ impl<'tcx> GotocCtx<'tcx> { } }, } + } else { + // if it's a union + unimplemented!() } } (Scalar::Int(int), ty::Tuple(_)) => { diff --git a/tests/cargo-kani/codegen-scalar-with-phantom/Cargo.toml b/tests/cargo-kani/codegen-scalar-with-phantom/Cargo.toml new file mode 100644 index 000000000000..541ac718603f --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-phantom/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "codegen-scalar-with-phantom" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected b/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected new file mode 100644 index 000000000000..97d4b6c54c09 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected @@ -0,0 +1,4 @@ +Status: SUCCESS\ +Description: "assertion failed: C.x == 0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/codegen-scalar-with-phantom/src/lib.rs b/tests/cargo-kani/codegen-scalar-with-phantom/src/lib.rs new file mode 100644 index 000000000000..9b17a8207e28 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-phantom/src/lib.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that we can codegen structs with scalar and phantom data. +//! +//! Note: Phantom data is represented with ZSTs, which are already covered by +//! the test `codegen-scalar-with-zsts`, but we include this one as well for +//! completeness. + +use std::marker::PhantomData; + +pub struct Foo { + x: u8, + _t: PhantomData, +} + +#[kani::proof] +fn check_phantom_data() { + const C: Foo = Foo { x: 0, _t: PhantomData }; + assert_eq!(C.x, 0); +} diff --git a/tests/cargo-kani/codegen-scalar-with-zsts/Cargo.toml b/tests/cargo-kani/codegen-scalar-with-zsts/Cargo.toml new file mode 100644 index 000000000000..86bf3dff0ecb --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-zsts/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "codegen-scalar-with-zsts" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected b/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected new file mode 100644 index 000000000000..97d4b6c54c09 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected @@ -0,0 +1,4 @@ +Status: SUCCESS\ +Description: "assertion failed: C.x == 0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/codegen-scalar-with-zsts/src/lib.rs b/tests/cargo-kani/codegen-scalar-with-zsts/src/lib.rs new file mode 100644 index 000000000000..e50e64f18580 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-zsts/src/lib.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that we can codegen structs with scalar and ZSTs. + +struct Empty {} + +pub struct Foo { + x: u8, + _t: Empty, +} + +#[kani::proof] +fn check_zst() { + const C: Foo = Foo { x: 0, _t: Empty {} }; + assert_eq!(C.x, 0); +} From ed671fc3c4125e36a9da2299475a0ad34987c6de Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 29 Sep 2023 11:23:39 -0700 Subject: [PATCH 06/13] Update PR template (#2791) Change the template to be more concise to address the team's concern that the template was too verbose. The new template is also cleaner since we are now using the PR description as the base for the commit message. --------- Co-authored-by: Michael Tautschnig Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- .github/PULL_REQUEST_TEMPLATE.md | 38 ++++++-------------------------- 1 file changed, 7 insertions(+), 31 deletions(-) diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 7635b0adccf5..84fd2d144fff 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -1,35 +1,11 @@ - -### Description of changes: - -Describe Kani's current behavior and how your code changes that behavior. If there are no issues this PR is resolving, explain why this change is necessary. - -### Resolved issues: +> Please ensure your PR description includes the following: +> 1. A description of how your changes improve Kani. +> 2. Some context on the problem you are solving. +> 3. A list of issues that are resolved by this PR. +> 4. If you had to perform any manual test, please describe them. +> +> **Make sure you remove this list from the final PR description.** Resolves #ISSUE-NUMBER -### Related RFC: - - -Optional #ISSUE-NUMBER. - -### Call-outs: - - - -### Testing: - -* How is this change tested? - -* Is this a refactor change? - -### Checklist -- [ ] Each commit message has a non-empty body, explaining why the change was made -- [ ] Methods or procedures are documented -- [ ] Regression or unit tests are included, or existing tests cover the modified code -- [ ] My PR is restricted to a single feature or bugfix - By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. From 964f986a90ba4b603971db3d86a4731118cfd64c Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Fri, 29 Sep 2023 14:32:15 -0700 Subject: [PATCH 07/13] Bump CBMC version (#2796) Upgrade CBMC version to latest (5.93.0). Resolves #2650 --- kani-dependencies | 2 +- scripts/kani-regression.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-dependencies b/kani-dependencies index 771bfd3cd881..3b90d0439d70 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,4 +1,4 @@ -CBMC_VERSION="5.92.0" +CBMC_VERSION="5.93.0" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_VERSION="3.8" KISSAT_VERSION="3.1.1" diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 0633f1f9e88b..23546bf68ccd 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -19,7 +19,7 @@ KANI_DIR=$SCRIPT_DIR/.. export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true" # Required dependencies -check-cbmc-version.py --major 5 --minor 92 +check-cbmc-version.py --major 5 --minor 93 check-cbmc-viewer-version.py --major 3 --minor 8 check_kissat_version.sh From ed2df13bb471280a9b74de918c4321b33f310406 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 2 Oct 2023 21:43:52 +0200 Subject: [PATCH 08/13] Update dependencies (#2797) Updated via `cargo update`. No further (manual) updates were suggested by `cargo outdated --workspace`. --- Cargo.lock | 132 +++++++++++++++++++++-------------------------------- 1 file changed, 52 insertions(+), 80 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 736dd6c3cfb0..d361244a5005 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -25,18 +25,18 @@ dependencies = [ [[package]] name = "aho-corasick" -version = "1.1.0" +version = "1.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f2135563fb5c609d2b2b87c1e8ce7bc41b0b45430fa9661f457981503dd5bf0" +checksum = "ea5d730647d4fadd988536d06fecce94b7b4f2a7efdae548f1cf4b63205518ab" dependencies = [ "memchr", ] [[package]] name = "anstream" -version = "0.5.0" +version = "0.6.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b1f58811cfac344940f1a400b6e6231ce35171f614f26439e80f8c1465c5cc0c" +checksum = "2ab91ebe16eb252986481c5b62f6098f3b698a45e34b5b98200cf20dd2484a44" dependencies = [ "anstyle", "anstyle-parse", @@ -48,15 +48,15 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.3" +version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b84bf0a05bbb2a83e5eb6fa36bb6e87baa08193c35ff52bbf6b38d8af2890e46" +checksum = "7079075b41f533b8c61d2a4d073c4676e1f8b249ff94a393b0595db304e0dd87" [[package]] name = "anstyle-parse" -version = "0.2.1" +version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "938874ff5980b03a87c5524b3ae5b59cf99b1d6bc836848df7bc5ada9643c333" +checksum = "317b9a89c1868f5ea6ff1d9539a69f45dffc21ce321ac1fd1160dfa48c8e2140" dependencies = [ "utf8parse", ] @@ -72,9 +72,9 @@ dependencies = [ [[package]] name = "anstyle-wincon" -version = "2.1.0" +version = "3.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "58f54d10c6dfa51283a066ceab3ec1ab78d13fae00aa49243a45e4571fb79dfd" +checksum = "f0699d10d2f4d628a98ee7b57b289abbc98ff3bad977cb3152709d4bf2330628" dependencies = [ "anstyle", "windows-sys 0.48.0", @@ -176,9 +176,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.4.4" +version = "4.4.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b1d7b8d5ec32af0fadc644bf1fd509a688c2103b185644bb1e29d164e0703136" +checksum = "d04704f56c2cde07f43e8e2c154b43f216dc5c92fc98ada720177362f953b956" dependencies = [ "clap_builder", "clap_derive", @@ -186,9 +186,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.4.4" +version = "4.4.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5179bb514e4d7c2051749d8fcefa2ed6d06a9f4e6d69faf3805f5d80b8cf8d56" +checksum = "0e231faeaca65ebd1ea3c737966bf858971cd38c3849107aa3ea7de90a804e45" dependencies = [ "anstream", "anstyle", @@ -277,16 +277,6 @@ dependencies = [ "tracing", ] -[[package]] -name = "crossbeam-channel" -version = "0.5.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a33c2bf77f2df06183c3aa30d1e96c0695a313d4f9c453cc3762a6db39f99200" -dependencies = [ - "cfg-if", - "crossbeam-utils", -] - [[package]] name = "crossbeam-deque" version = "0.8.3" @@ -365,9 +355,9 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.3" +version = "0.3.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "136526188508e25c6fef639d7927dfb3e0e3084488bf202267829cf7fc23dbdd" +checksum = "add4f07d43996f76ef320709726a556a9d4f965d9410d8d0271132d2f8293480" dependencies = [ "errno-dragonfly", "libc", @@ -421,9 +411,9 @@ dependencies = [ [[package]] name = "hashbrown" -version = "0.14.0" +version = "0.14.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2c6201b9ff9fd90a5a3bac2e56a830d0caa509576f0e503818ee82c181b3437a" +checksum = "7dfda62a12f55daeae5015f81b0baea145391cb4520f86c248fc615d72640d12" [[package]] name = "heck" @@ -431,12 +421,6 @@ version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" -[[package]] -name = "hermit-abi" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d77f7ec81a6d05a3abb01ab6eb7590f6083d08449fe5a1c8b1e620283546ccb7" - [[package]] name = "home" version = "0.5.5" @@ -448,12 +432,12 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.0.0" +version = "2.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d5477fe2230a79769d8dc68e0eabf5437907c0457a5614a9e8dddb67f65eb65d" +checksum = "8adf3ddd720272c6ea8bf59463c04e0f93d0bbf7c5439b691bca2987e0270897" dependencies = [ "equivalent", - "hashbrown 0.14.0", + "hashbrown 0.14.1", ] [[package]] @@ -580,9 +564,9 @@ dependencies = [ [[package]] name = "linux-raw-sys" -version = "0.4.7" +version = "0.4.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a9bad9f94746442c783ca431b22403b519cd7fbeed0533fdd6328b2f2212128" +checksum = "3852614a3bd9ca9804678ba6be5e3b8ce76dfc902cae004e3e0c44051b6e88db" [[package]] name = "lock_api" @@ -611,9 +595,9 @@ dependencies = [ [[package]] name = "memchr" -version = "2.6.3" +version = "2.6.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8f232d6ef707e1956a43342693d2a31e72989554d58299d7a88738cc95b0d35c" +checksum = "f665ee40bc4a3c5590afb1e9677db74a508659dfd71e126420da8274909a0167" [[package]] name = "memoffset" @@ -728,16 +712,6 @@ dependencies = [ "autocfg", ] -[[package]] -name = "num_cpus" -version = "1.16.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43" -dependencies = [ - "hermit-abi", - "libc", -] - [[package]] name = "once_cell" version = "1.18.0" @@ -886,9 +860,9 @@ dependencies = [ [[package]] name = "rayon" -version = "1.7.0" +version = "1.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1d2df5196e37bcc87abebc0053e20787d73847bb33134a69841207dd0a47f03b" +checksum = "9c27db03db7734835b3f53954b534c91069375ce6ccaa2e065441e07d9b6cdb1" dependencies = [ "either", "rayon-core", @@ -896,14 +870,12 @@ dependencies = [ [[package]] name = "rayon-core" -version = "1.11.0" +version = "1.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4b8f95bd6966f5c87776639160a66bd8ab9895d9d4ab01ddba9fc60661aebe8d" +checksum = "5ce3fb6ad83f861aac485e76e1985cd109d9a3713802152be56c3b1f0e0658ed" dependencies = [ - "crossbeam-channel", "crossbeam-deque", "crossbeam-utils", - "num_cpus", ] [[package]] @@ -917,13 +889,13 @@ dependencies = [ [[package]] name = "regex" -version = "1.9.5" +version = "1.9.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "697061221ea1b4a94a624f67d0ae2bfe4e22b8a17b6a192afb11046542cc8c47" +checksum = "ebee201405406dbf528b8b672104ae6d6d63e6d118cb10e4d51abbc7b58044ff" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.3.8", + "regex-automata 0.3.9", "regex-syntax 0.7.5", ] @@ -938,9 +910,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.3.8" +version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c2f401f4955220693b56f8ec66ee9c78abffd8d1c4f23dc41a23839eb88f0795" +checksum = "59b23e92ee4318893fa3fe3e6fb365258efbfe6ac6ab30f090cdcbb7aa37efa9" dependencies = [ "aho-corasick", "memchr", @@ -974,9 +946,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.13" +version = "0.38.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7db8590df6dfcd144d22afd1b83b36c21a18d7cbc1dc4bb5295a8712e9eb662" +checksum = "d2f9da0cbd88f9f09e7814e388301c8414c51c62aa6ce1e4b5c551d49d96e531" dependencies = [ "bitflags 2.4.0", "errno", @@ -1014,9 +986,9 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "semver" -version = "1.0.18" +version = "1.0.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0293b4b29daaf487284529cc2f5675b8e57c61f70167ba415a463651fd6a918" +checksum = "ad977052201c6de01a8ef2aa3378c4bd23217a056337d1d6da40468d267a4fb0" dependencies = [ "serde", ] @@ -1085,9 +1057,9 @@ dependencies = [ [[package]] name = "sharded-slab" -version = "0.1.4" +version = "0.1.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "900fba806f70c630b0a382d0d825e17a0f19fcd059a2ade1ff237bcddf446b31" +checksum = "c1b21f559e07218024e7e9f90f96f601825397de0e25420135f7f952453fed0b" dependencies = [ "lazy_static", ] @@ -1130,9 +1102,9 @@ dependencies = [ [[package]] name = "smallvec" -version = "1.11.0" +version = "1.11.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62bb4feee49fdd9f707ef802e22365a35de4b7b299de4763d44bfea899442ff9" +checksum = "942b4a808e05215192e39f4ab80813e599068285906cc91aa64f923db842bd5a" [[package]] name = "std" @@ -1220,18 +1192,18 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.48" +version = "1.0.49" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9d6d7a740b8a666a7e828dd00da9c0dc290dff53154ea77ac109281de90589b7" +checksum = "1177e8c6d7ede7afde3585fd2513e611227efd6481bd78d2e82ba1ce16557ed4" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.48" +version = "1.0.49" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49922ecae66cc8a249b77e68d1d0623c1b2c514f0060c27cdc68bd62a1219d35" +checksum = "10712f02019e9288794769fba95cd6847df9874d49d871d062172f9dd41bc4cc" dependencies = [ "proc-macro2", "quote", @@ -1250,9 +1222,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.8.0" +version = "0.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c226a7bba6d859b63c92c4b4fe69c5b6b72d0cb897dbc8e6012298e6154cb56e" +checksum = "1bc1433177506450fe920e46a4f9812d0c211f5dd556da10e731a0a3dfa151f0" dependencies = [ "serde", "serde_spanned", @@ -1271,9 +1243,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.20.0" +version = "0.20.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ff63e60a958cefbb518ae1fd6566af80d9d4be430a33f3723dfc47d1d411d95" +checksum = "ca676d9ba1a322c1b64eb8045a5ec5c0cfb0c9d08e15e9ff622589ad5221c8fe" dependencies = [ "indexmap", "serde", @@ -1458,9 +1430,9 @@ checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" [[package]] name = "winapi-util" -version = "0.1.5" +version = "0.1.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178" +checksum = "f29e6f9198ba0d26b4c9f07dbe6f9ed633e1f3d5b8b414090084349e46a52596" dependencies = [ "winapi", ] From 62f136c9c2c99334f9830e8ef61404c50c7ca7b5 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Tue, 3 Oct 2023 12:15:20 -0400 Subject: [PATCH 09/13] Prevent kani crash during setup for first time (#2799) > Please ensure your PR description includes the following: > 1. A description of how your changes improve Kani. > 2. Some context on the problem you are solving. > 3. A list of issues that are resolved by this PR. > 4. If you had to perform any manual test, please describe them. > > **Make sure you remove this list from the final PR description.** By using the `tar` file as a lock mechanism, we can detect incomplete setups i.e when both `kani's` working directory and the tar file present before setup, we can simply use the local bundle to start setup again. Resolves #1545 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- src/lib.rs | 11 ++++++++++- src/setup.rs | 21 ++++++++++++++++++++- 2 files changed, 30 insertions(+), 2 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 4639354d8d02..9a1ac90f5dda 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -16,11 +16,11 @@ mod cmd; mod os_hacks; mod setup; -use std::env; use std::ffi::OsString; use std::os::unix::prelude::CommandExt; use std::path::{Path, PathBuf}; use std::process::Command; +use std::{env, fs}; use anyhow::{bail, Context, Result}; @@ -33,6 +33,15 @@ pub fn proxy(bin: &str) -> Result<()> { fail_if_in_dev_environment()?; if !setup::appears_setup() { setup::setup(None)?; + } else { + // This handles cases where the setup was left incomplete due to an interrupt + // For example - https://github.com/model-checking/kani/issues/1545 + if let Some(path_to_bundle) = setup::appears_incomplete() { + setup::setup(Some(path_to_bundle.clone().into_os_string()))?; + // Suppress warning with unused assignment + // and remove the bundle if it still exists + let _ = fs::remove_file(path_to_bundle); + } } exec(bin) } diff --git a/src/setup.rs b/src/setup.rs index b7fc48fcf83d..2d2c643bbdd5 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -53,6 +53,22 @@ pub fn appears_setup() -> bool { kani_dir().expect("couldn't find kani directory").exists() } +// Ensure that the tar file does not exist, essentially using its presence +// to detect setup completion as if it were a lock file. +pub fn appears_incomplete() -> Option { + let kani_dir = kani_dir().expect("couldn't find kani directory"); + let kani_dir_parent = kani_dir.parent().unwrap(); + + for entry in std::fs::read_dir(&kani_dir_parent).ok()?.flatten() { + if let Some(file_name) = entry.file_name().to_str() { + if file_name.ends_with(".tar.gz") { + return Some(kani_dir_parent.join(file_name)); + } + } + } + None +} + /// Sets up Kani by unpacking/installing to `~/.kani/kani-VERSION` pub fn setup(use_local_bundle: Option) -> Result<()> { let kani_dir = kani_dir()?; @@ -92,7 +108,10 @@ fn setup_kani_bundle(kani_dir: &Path, use_local_bundle: Option) -> Res .arg("-zxf") .arg(&path) .current_dir(&kani_dir) - .run()?; + .run() + .context( + "Failed to extract tar file, try removing Kani setup located in .kani in your home directory and restarting", + )?; } else { let filename = download_filename(); println!("[2/5] Downloading Kani release bundle: {}", &filename); From fb08f3e11384a36585de3db13c8bcd9b6c0060d1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 4 Oct 2023 22:17:09 +0200 Subject: [PATCH 10/13] Create concrete playback temp files in source directory (#2804) Concrete playback seeks to generate unit tests in the original source file. An intermediate temporary file is used to reduce the risk of corrupting original source files. Once the temporary file has been completely written to, it is to be atomically moved to replace the source file. This can only be done on the same file system. We now create the temporary file in the same source directory as the original source file to ensure we are on the same file system. The implementation uses NamedTempFile from the tempfile crate, which renders our own tempfile implementation redundant. Tested on Ubuntu 20.04 with /tmp on a different partition (where our regression tests would previously fail). Resolves: #2705 --- Cargo.lock | 20 +++++ kani-driver/Cargo.toml | 1 + .../src/concrete_playback/test_generator.rs | 25 +++--- kani-driver/src/util.rs | 78 ------------------- 4 files changed, 35 insertions(+), 89 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index d361244a5005..59770bbda6d2 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -374,6 +374,12 @@ dependencies = [ "libc", ] +[[package]] +name = "fastrand" +version = "2.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "25cbce373ec4653f1a01a31e8a5e5ec0c622dc27ff9c4e6606eefef5cbbed4a5" + [[package]] name = "getopts" version = "0.2.21" @@ -504,6 +510,7 @@ dependencies = [ "serde_json", "strum 0.25.0", "strum_macros 0.25.2", + "tempfile", "toml", "tracing", "tracing-subscriber", @@ -1190,6 +1197,19 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "tempfile" +version = "3.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cb94d2f3cc536af71caac6b6fcebf65860b347e7ce0cc9ebe8f70d3e521054ef" +dependencies = [ + "cfg-if", + "fastrand", + "redox_syscall", + "rustix", + "windows-sys 0.48.0", +] + [[package]] name = "thiserror" version = "1.0.49" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index c541803bb10d..2f01fa9e83dd 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -29,6 +29,7 @@ rayon = "1.5.3" comfy-table = "7.0.1" strum = {version = "0.25.0"} strum_macros = {version = "0.25.2"} +tempfile = "3" tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} rand = "0.8" diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 049b294c9848..492369fb32eb 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -7,7 +7,6 @@ use crate::args::ConcretePlaybackMode; use crate::call_cbmc::VerificationResult; use crate::session::KaniSession; -use crate::util::tempfile::TempFile; use anyhow::{Context, Result}; use concrete_vals_extractor::{extract_harness_values, ConcreteVal}; use kani_metadata::HarnessMetadata; @@ -18,6 +17,7 @@ use std::hash::{Hash, Hasher}; use std::io::{BufRead, BufReader, Write}; use std::path::Path; use std::process::Command; +use tempfile::NamedTempFile; impl KaniSession { /// The main driver for generating concrete playback unit tests and adding them to source code. @@ -158,25 +158,28 @@ impl KaniSession { // Create temp file if !unit_tests.is_empty() { - let mut temp_file = TempFile::try_new("concrete_playback.tmp")?; + let source_basedir = Path::new(source_path).parent().unwrap_or(Path::new(".")); + let mut temp_file = NamedTempFile::with_prefix_in("concrete_playback", source_basedir)?; let mut curr_line_num = 0; // Use a buffered reader/writer to generate the unit test line by line for line in source_reader.lines().flatten() { curr_line_num += 1; - if let Some(temp_writer) = temp_file.writer.as_mut() { - writeln!(temp_writer, "{line}")?; - if curr_line_num == proof_harness_end_line { - for unit_test in unit_tests.iter() { - for unit_test_line in unit_test.code.iter() { - curr_line_num += 1; - writeln!(temp_writer, "{unit_test_line}")?; - } + writeln!(temp_file, "{line}")?; + if curr_line_num == proof_harness_end_line { + for unit_test in unit_tests.iter() { + for unit_test_line in unit_test.code.iter() { + curr_line_num += 1; + writeln!(temp_file, "{unit_test_line}")?; } } } } - temp_file.rename(source_path).expect("Could not rename file"); + + // Renames are usually automic, so we won't corrupt the user's source file during a + // crash; but first flush all updates to disk, which persist wouldn't take care of. + temp_file.as_file().sync_all()?; + temp_file.persist(source_path).expect("Could not rename file"); } Ok(!unit_tests.is_empty()) diff --git a/kani-driver/src/util.rs b/kani-driver/src/util.rs index a9800785f869..1e0957dc7726 100644 --- a/kani-driver/src/util.rs +++ b/kani-driver/src/util.rs @@ -14,84 +14,6 @@ use std::ffi::OsString; use std::path::{Path, PathBuf}; use std::process::Command; -pub mod tempfile { - use std::{ - env, - fs::{self, rename, File}, - io::{BufWriter, Error, Write}, - path::PathBuf, - }; - - use crate::util; - use ::rand; - use anyhow::Context; - use rand::Rng; - - /// Handle a writable temporary file which will be deleted when the object is dropped. - /// To save the contents of the file, users can invoke `rename` which will move the file to - /// its new location and no further deletion will be performed. - pub struct TempFile { - pub file: File, - pub temp_path: PathBuf, - pub writer: Option>, - renamed: bool, - } - - impl TempFile { - /// Create a temp file - pub fn try_new(suffix_name: &str) -> Result { - let mut temp_path = env::temp_dir(); - - // Generate a unique name for the temporary directory - let hash: u32 = rand::thread_rng().gen(); - let file_name: &str = &format!("kani_tmp_{hash}_{suffix_name}"); - - temp_path.push(file_name); - let temp_file = File::create(&temp_path)?; - let writer = BufWriter::new(temp_file.try_clone()?); - - Ok(Self { file: temp_file, temp_path, writer: Some(writer), renamed: false }) - } - - /// Rename the temporary file to the new path, replacing the original file if the path points to a file that already exists. - pub fn rename(mut self, source_path: &str) -> Result<(), String> { - // flush here - self.writer.as_mut().unwrap().flush().unwrap(); - self.writer = None; - // Renames are usually automic, so we won't corrupt the user's source file during a crash. - rename(&self.temp_path, source_path) - .with_context(|| format!("Error renaming file {}", self.temp_path.display())) - .unwrap(); - self.renamed = true; - Ok(()) - } - } - - /// Ensure that the bufwriter is flushed and temp variables are dropped - /// everytime the tempfile is out of scope - /// note: the fields for the struct are dropped automatically by destructor - impl Drop for TempFile { - fn drop(&mut self) { - // if writer is not flushed, flush it - if self.writer.as_ref().is_some() { - // couldn't use ? as drop does not handle returns - if let Err(e) = self.writer.as_mut().unwrap().flush() { - util::warning( - format!("failed to flush {}: {e}", self.temp_path.display()).as_str(), - ); - } - self.writer = None; - } - - if !self.renamed { - if let Err(_e) = fs::remove_file(&self.temp_path.clone()) { - util::warning(&format!("Error removing file {}", self.temp_path.display())); - } - } - } - } -} - /// Replace an extension with another one, in a new PathBuf. (See tests for examples) pub fn alter_extension(path: &Path, ext: &str) -> PathBuf { path.with_extension(ext) From fece7ee258f1e3961d8b4e9845ecdc2607710be2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 4 Oct 2023 23:37:24 +0200 Subject: [PATCH 11/13] Address clippy warnings (#2807) Versions of clippy that come with newer toolchains report a large number of needless_borrows_for_generic_args. We can address these now so that we don't have to make these changes as part of a toolchain update. --- cprover_bindings/src/goto_program/builtin.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/operand.rs | 8 ++++---- .../src/codegen_cprover_gotoc/codegen/place.rs | 12 +++++++----- .../src/codegen_cprover_gotoc/codegen/typ.rs | 6 +++--- .../src/codegen_cprover_gotoc/compiler_interface.rs | 2 +- kani-compiler/src/kani_compiler.rs | 2 +- kani-compiler/src/kani_middle/reachability.rs | 2 +- kani-driver/src/args/mod.rs | 6 +++--- kani-driver/src/args/playback_args.rs | 2 +- kani-driver/src/assess/metadata.rs | 2 +- kani-driver/src/assess/scan.rs | 2 +- kani-driver/src/concrete_playback/playback.rs | 2 +- kani-driver/src/project.rs | 2 +- kani-driver/src/session.rs | 2 +- kani_metadata/src/artifact.rs | 4 ++-- src/os_hacks.rs | 10 +++++----- src/setup.rs | 8 ++++---- tools/bookrunner/src/books.rs | 6 +++--- tools/bookrunner/src/util.rs | 2 +- tools/build-kani/src/main.rs | 4 ++-- tools/build-kani/src/sysroot.rs | 2 +- tools/compiletest/src/json.rs | 2 +- tools/compiletest/src/main.rs | 4 ++-- tools/compiletest/src/runtest.rs | 12 ++++++------ 24 files changed, 54 insertions(+), 52 deletions(-) diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index 95c38d7e0f8a..438bc2eea1e9 100644 --- a/cprover_bindings/src/goto_program/builtin.rs +++ b/cprover_bindings/src/goto_program/builtin.rs @@ -329,7 +329,7 @@ impl BuiltinFn { /// Converters: build symbols and expressions from Builtins impl BuiltinFn { pub fn as_symbol(&self) -> Symbol { - Symbol::builtin_function(&self.to_string(), self.param_types(), self.return_type()) + Symbol::builtin_function(self.to_string(), self.param_types(), self.return_type()) } pub fn as_expr(&self) -> Expr { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 45ce90880fd6..300817af0c98 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -561,7 +561,7 @@ impl<'tcx> GotocCtx<'tcx> { } let mem_place = - self.symbol_table.lookup(&self.alloc_map.get(&alloc).unwrap()).unwrap().to_expr(); + self.symbol_table.lookup(self.alloc_map.get(&alloc).unwrap()).unwrap().to_expr(); mem_place.address_of() } @@ -579,16 +579,16 @@ impl<'tcx> GotocCtx<'tcx> { // initializers. For example, for a boolean static variable, the variable will have type // CBool and the initializer will be a single byte (a one-character array) representing the // bit pattern for the boolean value. - let alloc_typ_ref = self.ensure_struct(&struct_name, &struct_name, |ctx, _| { + let alloc_typ_ref = self.ensure_struct(struct_name, struct_name, |ctx, _| { ctx.codegen_allocation_data(alloc) .iter() .enumerate() .map(|(i, d)| match d { AllocData::Bytes(bytes) => DatatypeComponent::field( - &i.to_string(), + i.to_string(), Type::unsigned_int(8).array_of(bytes.len()), ), - AllocData::Expr(e) => DatatypeComponent::field(&i.to_string(), e.typ().clone()), + AllocData::Expr(e) => DatatypeComponent::field(i.to_string(), e.typ().clone()), }) .collect() }); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 4506680158ca..31fa878c854a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -268,8 +268,10 @@ impl<'tcx> GotocCtx<'tcx> { | ty::Param(_) | ty::Infer(_) | ty::Error(_) => unreachable!("type {parent_ty:?} does not have a field"), - ty::Tuple(_) => Ok(parent_expr - .member(&Self::tuple_fld_name(field.index()), &self.symbol_table)), + ty::Tuple(_) => { + Ok(parent_expr + .member(Self::tuple_fld_name(field.index()), &self.symbol_table)) + } ty::Adt(def, _) if def.repr().simd() => Ok(self.codegen_simd_field( parent_expr, *field, @@ -278,10 +280,10 @@ impl<'tcx> GotocCtx<'tcx> { // if we fall here, then we are handling either a struct or a union ty::Adt(def, _) => { let field = &def.variants().raw[0].fields[*field]; - Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table)) + Ok(parent_expr.member(field.name.to_string(), &self.symbol_table)) } ty::Closure(..) => { - Ok(parent_expr.member(&field.index().to_string(), &self.symbol_table)) + Ok(parent_expr.member(field.index().to_string(), &self.symbol_table)) } ty::Generator(..) => { let field_name = self.generator_field_name(field.as_usize()); @@ -299,7 +301,7 @@ impl<'tcx> GotocCtx<'tcx> { // if we fall here, then we are handling an enum TypeOrVariant::Variant(parent_var) => { let field = &parent_var.fields[*field]; - Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table)) + Ok(parent_expr.member(field.name.to_string(), &self.symbol_table)) } TypeOrVariant::GeneratorVariant(_var_idx) => { let field_name = self.generator_field_name(field.index()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index b1384d68013f..cdbe84d5111a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -864,7 +864,7 @@ impl<'tcx> GotocCtx<'tcx> { // We need to pad to the next offset let padding_size = next_offset - current_offset; let name = format!("$pad{idx}"); - Some(DatatypeComponent::padding(&name, padding_size.bits())) + Some(DatatypeComponent::padding(name, padding_size.bits())) } else { None } @@ -1378,7 +1378,7 @@ impl<'tcx> GotocCtx<'tcx> { .iter() .map(|f| { DatatypeComponent::field( - &f.name.to_string(), + f.name.to_string(), ctx.codegen_ty(f.ty(ctx.tcx, subst)), ) }) @@ -1641,7 +1641,7 @@ impl<'tcx> GotocCtx<'tcx> { None } else { Some(DatatypeComponent::field( - &case.name.to_string(), + case.name.to_string(), self.codegen_enum_case_struct( name, pretty_name, diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index b3262c23c9c8..68fb2b88cb52 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -271,7 +271,7 @@ impl CodegenBackend for GotocCodegenBackend { if let MonoItem::Fn(instance) = test_fn { instance } else { continue }; let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename); let test_model_path = &metadata.goto_file.as_ref().unwrap(); - std::fs::copy(&model_path, &test_model_path).expect(&format!( + std::fs::copy(&model_path, test_model_path).expect(&format!( "Failed to copy {} to {}", model_path.display(), test_model_path.display() diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 38a90686abc1..56cd02ce542d 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -352,7 +352,7 @@ impl KaniCompiler { /// Write the metadata to a file fn store_metadata(&self, metadata: &KaniMetadata, filename: &Path) { debug!(?filename, "write_metadata"); - let out_file = File::create(&filename).unwrap(); + let out_file = File::create(filename).unwrap(); let writer = BufWriter::new(out_file); if self.queries.lock().unwrap().args().output_pretty_json { serde_json::to_writer_pretty(writer, &metadata).unwrap(); diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 66cebf9c8f6f..37b26a136447 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -725,7 +725,7 @@ mod debug { debug!(?target, "dump_dot"); let outputs = tcx.output_filenames(()); let path = outputs.output_path(OutputType::Metadata).with_extension("dot"); - let out_file = File::create(&path)?; + let out_file = File::create(path)?; let mut writer = BufWriter::new(out_file); writeln!(writer, "digraph ReachabilityGraph {{")?; if target.is_empty() { diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 043aae45f43b..6651f72db7c2 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -427,7 +427,7 @@ fn check_no_cargo_opt(is_set: bool, name: &str) -> Result<(), Error> { if is_set { Err(Error::raw( ErrorKind::UnknownArgument, - &format!("argument `{}` cannot be used with standalone Kani.", name), + format!("argument `{}` cannot be used with standalone Kani.", name), )) } else { Ok(()) @@ -453,7 +453,7 @@ impl ValidateArgs for StandaloneArgs { if !input.is_file() { return Err(Error::raw( ErrorKind::InvalidValue, - &format!( + format!( "Invalid argument: Input invalid. `{}` is not a regular file.", input.display() ), @@ -583,7 +583,7 @@ impl ValidateArgs for VerificationArgs { if out_dir.exists() && !out_dir.is_dir() { return Err(Error::raw( ErrorKind::InvalidValue, - &format!( + format!( "Invalid argument: `--target-dir` argument `{}` is not a directory", out_dir.display() ), diff --git a/kani-driver/src/args/playback_args.rs b/kani-driver/src/args/playback_args.rs index c47b81515953..bdad446a1158 100644 --- a/kani-driver/src/args/playback_args.rs +++ b/kani-driver/src/args/playback_args.rs @@ -74,7 +74,7 @@ impl ValidateArgs for KaniPlaybackArgs { if !self.input.is_file() { return Err(Error::raw( ErrorKind::InvalidValue, - &format!( + format!( "Invalid argument: Input invalid. `{}` is not a regular file.", self.input.display() ), diff --git a/kani-driver/src/assess/metadata.rs b/kani-driver/src/assess/metadata.rs index 122261ce66bb..d555f1e4d309 100644 --- a/kani-driver/src/assess/metadata.rs +++ b/kani-driver/src/assess/metadata.rs @@ -88,7 +88,7 @@ pub struct SessionError { /// If given the argument to so do, write the assess metadata to the target file. pub(crate) fn write_metadata(args: &AssessArgs, metadata: AssessMetadata) -> Result<()> { if let Some(path) = &args.emit_metadata { - let out_file = File::create(&path)?; + let out_file = File::create(path)?; let writer = BufWriter::new(out_file); // use pretty for now to keep things readable and debuggable, but this should change eventually serde_json::to_writer_pretty(writer, &metadata)?; diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs index 17a3a56e2171..5e4dc81d7e2a 100644 --- a/kani-driver/src/assess/scan.rs +++ b/kani-driver/src/assess/scan.rs @@ -179,7 +179,7 @@ fn invoke_assess( // Additionally, this should be `--manifest-path` but `cargo kani` doesn't support that yet. cmd.arg("-p").arg(package); cmd.arg("--enable-unstable"); // This has to be after `-p` due to an argument parsing bug in kani-driver - cmd.args(&["assess", "--emit-metadata"]) + cmd.args(["assess", "--emit-metadata"]) .arg(outfile) .current_dir(dir) .stdout(log.try_clone()?) diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index bb060cea58bd..96ed30da904d 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -84,7 +84,7 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result rustc_args.push("--error-format=json".into()); } - let mut cmd = Command::new(&install.kani_compiler()?); + let mut cmd = Command::new(install.kani_compiler()?); cmd.args(rustc_args); session::run_terminal(&args.playback.common_opts, cmd)?; diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index c776a106ae47..df85ca151077 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -364,6 +364,6 @@ fn metadata_with_function( // Note: `out_dir` is already on canonical form, so no need to invoke `try_new()`. fn standalone_artifact(out_dir: &Path, crate_name: &String, typ: ArtifactType) -> Artifact { let mut path = out_dir.join(crate_name); - let _ = path.set_extension(&typ); + let _ = path.set_extension(typ); Artifact { path, typ } } diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 043730caf74a..5b9b90854789 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -216,7 +216,7 @@ pub fn run_redirect( stdout.display() ); } - let output_file = std::fs::File::create(&stdout)?; + let output_file = std::fs::File::create(stdout)?; cmd.stdout(output_file); let program = cmd.get_program().to_string_lossy().to_string(); diff --git a/kani_metadata/src/artifact.rs b/kani_metadata/src/artifact.rs index 54ff7a025e19..078cad14f679 100644 --- a/kani_metadata/src/artifact.rs +++ b/kani_metadata/src/artifact.rs @@ -56,7 +56,7 @@ pub fn convert_type(path: &Path, from: ArtifactType, to: ArtifactType) -> PathBu match from { // Artifact types that has only one extension. ArtifactType::Goto => { - result.set_extension(&to); + result.set_extension(to); } // Artifact types that has two extensions. ArtifactType::Metadata @@ -66,7 +66,7 @@ pub fn convert_type(path: &Path, from: ArtifactType, to: ArtifactType) -> PathBu | ArtifactType::VTableRestriction | ArtifactType::PrettyNameMap => { result.set_extension(""); - result.set_extension(&to); + result.set_extension(to); } } result diff --git a/src/os_hacks.rs b/src/os_hacks.rs index e4a7fb9a6a4c..cf39c39be82d 100644 --- a/src/os_hacks.rs +++ b/src/os_hacks.rs @@ -61,8 +61,8 @@ pub fn setup_python_deps_on_ubuntu_18_04(pyroot: &Path, pkg_versions: &[&str]) - // Step 1: use `--system --prefix pyroot`. This disables the broken behavior, and creates `bin` but... Command::new("python3") - .args(&["-m", "pip", "install", "--system", "--prefix"]) - .arg(&pyroot) + .args(["-m", "pip", "install", "--system", "--prefix"]) + .arg(pyroot) .args(pkg_versions) .run()?; @@ -128,7 +128,7 @@ fn setup_nixos_patchelf(kani_dir: &Path) -> Result<()> { // Find the correct path to link C++ stdlib: // `rpath=$(nix-instantiate --eval -E "(import {}).stdenv.cc.cc.lib.outPath")/lib` let rpath_output = Command::new("nix-instantiate") - .args(&["--eval", "-E", "(import {}).stdenv.cc.cc.lib.outPath"]) + .args(["--eval", "-E", "(import {}).stdenv.cc.cc.lib.outPath"]) .output()?; if !rpath_output.status.success() { bail!("Failed to find C++ standard library with `nix-instantiate`"); @@ -139,10 +139,10 @@ fn setup_nixos_patchelf(kani_dir: &Path) -> Result<()> { let rpath = format!("{rpath_prefix}/lib"); let patch_interp = |file: &Path| -> Result<()> { - Command::new("patchelf").args(&["--set-interpreter", interp]).arg(file).run() + Command::new("patchelf").args(["--set-interpreter", interp]).arg(file).run() }; let patch_rpath = |file: &Path| -> Result<()> { - Command::new("patchelf").args(&["--set-rpath", &rpath]).arg(file).run() + Command::new("patchelf").args(["--set-rpath", &rpath]).arg(file).run() }; let bin = kani_dir.join("bin"); diff --git a/src/setup.rs b/src/setup.rs index 2d2c643bbdd5..1e9287542c93 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -107,7 +107,7 @@ fn setup_kani_bundle(kani_dir: &Path, use_local_bundle: Option) -> Res .arg("--strip-components=1") .arg("-zxf") .arg(&path) - .current_dir(&kani_dir) + .current_dir(kani_dir) .run() .context( "Failed to extract tar file, try removing Kani setup located in .kani in your home directory and restarting", @@ -118,7 +118,7 @@ fn setup_kani_bundle(kani_dir: &Path, use_local_bundle: Option) -> Res fail_if_unsupported_target()?; let bundle = base_dir.join(filename); Command::new("curl") - .args(&["-sSLf", "-o"]) + .args(["-sSLf", "-o"]) .arg(&bundle) .arg(download_url()) .run() @@ -143,7 +143,7 @@ fn setup_rust_toolchain(kani_dir: &Path) -> Result { // Currently this means we require the bundle to have been unpacked first! let toolchain_version = get_rust_toolchain_version(kani_dir)?; println!("[3/5] Installing rust toolchain version: {}", &toolchain_version); - Command::new("rustup").args(&["toolchain", "install", &toolchain_version]).run()?; + Command::new("rustup").args(["toolchain", "install", &toolchain_version]).run()?; let toolchain = home::rustup_home()?.join("toolchains").join(&toolchain_version); @@ -165,7 +165,7 @@ fn setup_python_deps(kani_dir: &Path, os: &os_info::Info) -> Result<()> { } Command::new("python3") - .args(&["-m", "pip", "install", "--target"]) + .args(["-m", "pip", "install", "--target"]) .arg(&pyroot) .args(pkg_versions) .run()?; diff --git a/tools/bookrunner/src/books.rs b/tools/bookrunner/src/books.rs index 713e6d2b15f7..0e8b8fb8857d 100644 --- a/tools/bookrunner/src/books.rs +++ b/tools/bookrunner/src/books.rs @@ -88,7 +88,7 @@ impl Book { let summary_dir = summary_path.parent().unwrap().to_path_buf(); let summary = fs::read_to_string(summary_path.clone()).unwrap(); assert!( - summary.starts_with(&summary_start.as_str()), + summary.starts_with(summary_start.as_str()), "Error: The start of {} summary file changed.", self.name ); @@ -409,7 +409,7 @@ fn extract( config_paths: &mut HashSet, default_edition: Edition, ) { - let code = fs::read_to_string(&par_from).unwrap(); + let code = fs::read_to_string(par_from).unwrap(); let mut examples = Examples(Vec::new()); find_testable_code(&code, &mut examples, ErrorCodes::No, false, None); for mut example in examples.0 { @@ -514,7 +514,7 @@ fn generate_text_bookrunner(bookrunner: bookrunner::Tree, path: &Path) { bookrunner.data.num_fail, bookrunner ); - fs::write(&path, bookrunner_str).expect("Error: Unable to write bookrunner results"); + fs::write(path, bookrunner_str).expect("Error: Unable to write bookrunner results"); } /// Runs examples using Litani build. diff --git a/tools/bookrunner/src/util.rs b/tools/bookrunner/src/util.rs index 260c3253df69..542ad70dbc96 100644 --- a/tools/bookrunner/src/util.rs +++ b/tools/bookrunner/src/util.rs @@ -206,7 +206,7 @@ pub fn add_verification_job(litani: &mut Litani, test_props: &TestProps) { // Add `--function main` so we can run these without having to amend them to add `#[kani::proof]`. // Some of test_props.kani_args will contains `--cbmc-args` so we should always put that last. kani.arg(&test_props.path) - .args(&["--enable-unstable", "--function", "main"]) + .args(["--enable-unstable", "--function", "main"]) .args(&test_props.kani_args); if !test_props.rustc_args.is_empty() { kani.env("RUSTFLAGS", test_props.rustc_args.join(" ")); diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index e781f3ceb942..b94e951fe178 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -83,7 +83,7 @@ fn bundle_kani(dir: &Path) -> Result<()> { // 2. Kani scripts let scripts = dir.join("scripts"); - std::fs::create_dir(&scripts)?; + std::fs::create_dir(scripts)?; // 3. Kani libraries let library = dir.join("library"); @@ -148,7 +148,7 @@ fn bundle_kissat(dir: &Path) -> Result<()> { /// This should include all files as `dir/` in the tarball. /// e.g. `kani-1.0/bin/kani-compiler` not just `bin/kani-compiler`. fn create_release_bundle(dir: &Path, bundle: &str) -> Result<()> { - Command::new("tar").args(&["zcf", bundle]).arg(dir).run() + Command::new("tar").args(["zcf", bundle]).arg(dir).run() } /// Helper trait to fallibly run commands diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index 525104888656..3a6239106826 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -151,7 +151,7 @@ fn build_kani_lib( /// Copy all the artifacts to their correct place to generate a valid sysroot. fn copy_artifacts(artifacts: &[Artifact], sysroot_lib: &Path, target: &str) -> Result<()> { // Create sysroot folder hierarchy. - sysroot_lib.exists().then(|| fs::remove_dir_all(&sysroot_lib)); + sysroot_lib.exists().then(|| fs::remove_dir_all(sysroot_lib)); let std_path = path_buf!(&sysroot_lib, "rustlib", target, "lib"); fs::create_dir_all(&std_path).expect(&format!("Failed to create {std_path:?}")); diff --git a/tools/compiletest/src/json.rs b/tools/compiletest/src/json.rs index ec1de29aa640..c46c3b3225e8 100644 --- a/tools/compiletest/src/json.rs +++ b/tools/compiletest/src/json.rs @@ -63,7 +63,7 @@ pub fn extract_rendered(output: &str) -> String { String::new(), |mut output, item| { use std::fmt::Write; - let _ = write!(output, "Future breakage diagnostic:\n"); + let _ = writeln!(output, "Future breakage diagnostic:"); let s = item .diagnostic .rendered diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index cdef1446763a..5418ad47f7fa 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -467,7 +467,7 @@ fn collect_rs_tests_from_dir( // tests themselves, they race for the privilege of // creating the directories and sometimes fail randomly. let build_dir = output_relative_path(config, relative_dir_path); - fs::create_dir_all(&build_dir).unwrap(); + fs::create_dir_all(build_dir).unwrap(); // Add each `.rs` file as a test, and recurse further on any // subdirectories we find, except for `aux` directories. @@ -571,7 +571,7 @@ fn make_test_name(config: &Config, testpaths: &TestPaths) -> test::TestName { // ui/foo/bar/baz.rs let path = PathBuf::from(config.src_base.file_name().unwrap()) .join(&testpaths.relative_dir) - .join(&testpaths.file.file_name().unwrap()); + .join(testpaths.file.file_name().unwrap()); test::DynTestName(format!("[{}] {}", config.mode, path.display())) } diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 2da10826b3c2..ee89c252dc4f 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -57,7 +57,7 @@ pub fn run(config: Config, testpaths: &TestPaths) { let props = TestProps::from_file(&testpaths.file, &config); let cx = TestCx { config: &config, props: &props, testpaths }; - create_dir_all(&cx.output_base_dir()).unwrap(); + create_dir_all(cx.output_base_dir()).unwrap(); cx.run(); cx.create_stamp(); } @@ -97,7 +97,7 @@ impl<'test> TestCx<'test> { env::split_paths(&env::var_os(dylib_env_var()).unwrap_or_default()).collect::>(); // Add the new dylib search path var - let newpath = env::join_paths(&path).unwrap(); + let newpath = env::join_paths(path).unwrap(); command.env(dylib_env_var(), newpath); let mut child = disable_error_reporting(|| command.spawn()) @@ -136,7 +136,7 @@ impl<'test> TestCx<'test> { fn dump_output_file(&self, out: &str, extension: &str) { let outfile = self.make_out_name(extension); - fs::write(&outfile, out).unwrap(); + fs::write(outfile, out).unwrap(); } /// Creates a filename for output with the given extension. @@ -273,7 +273,7 @@ impl<'test> TestCx<'test> { .arg("kani") .arg("--target-dir") .arg(self.output_base_dir().join("target")) - .current_dir(&parent_dir) + .current_dir(parent_dir) .args(&self.config.extra_args); if test { cargo.arg("--tests"); @@ -321,7 +321,7 @@ impl<'test> TestCx<'test> { kani.env("RUSTFLAGS", self.props.compile_flags.join(" ")); } kani.arg(&self.testpaths.file).args(&self.props.kani_flags); - kani.arg("--coverage").args(&["-Z", "line-coverage"]); + kani.arg("--coverage").args(["-Z", "line-coverage"]); if !self.props.cbmc_flags.is_empty() { kani.arg("--cbmc-args").args(&self.props.cbmc_flags); @@ -506,7 +506,7 @@ impl<'test> TestCx<'test> { fn create_stamp(&self) { let stamp = crate::stamp(self.config, self.testpaths); - fs::write(&stamp, "we only support one configuration").unwrap(); + fs::write(stamp, "we only support one configuration").unwrap(); } } From 7bf5a6d54ed438e9dccbda10539394443b182563 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 5 Oct 2023 08:05:45 +0200 Subject: [PATCH 12/13] Update Rust toolchain to 2023-09-23 (#2806) Source changes required by the following upstream commits: * rust-lang/rust@5a0a1ff0cd move ConstValue into mir * rust-lang/rust@ea22adbabd adjust constValue::Slice to work for arbitrary slice types * rust-lang/rust@c94410c145 rename mir::Constant -> mir::ConstOperand, mir::ConstKind -> mir::Const Fixes: #2784 --- .../codegen_cprover_gotoc/codegen/operand.rs | 32 ++++++++----------- kani-compiler/src/kani_middle/intrinsics.rs | 4 +-- kani-compiler/src/kani_middle/reachability.rs | 24 +++++++------- .../src/kani_middle/stubbing/transform.rs | 5 ++- rust-toolchain.toml | 2 +- 5 files changed, 30 insertions(+), 37 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 300817af0c98..2e76cb00276c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -6,10 +6,8 @@ use crate::unwrap_or_return_codegen_unimplemented; use cbmc::btree_string_map; use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Symbol, Type}; use rustc_ast::ast::Mutability; -use rustc_middle::mir::interpret::{ - read_target_uint, AllocId, Allocation, ConstValue, GlobalAlloc, Scalar, -}; -use rustc_middle::mir::{Constant, ConstantKind, Operand, UnevaluatedConst}; +use rustc_middle::mir::interpret::{read_target_uint, AllocId, Allocation, GlobalAlloc, Scalar}; +use rustc_middle::mir::{Const as mirConst, ConstOperand, ConstValue, Operand, UnevaluatedConst}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uint, UintTy}; use rustc_span::def_id::DefId; @@ -56,13 +54,13 @@ impl<'tcx> GotocCtx<'tcx> { /// 1. `Ty` means e.g. that it's a const generic parameter. (See `codegen_const`) /// 2. `Val` means it's a constant value of various kinds. (See `codegen_const_value`) /// 3. `Unevaluated` means we need to run the interpreter, to get a `ConstValue`. (See `codegen_const_unevaluated`) - fn codegen_constant(&mut self, c: &Constant<'tcx>) -> Expr { + fn codegen_constant(&mut self, c: &ConstOperand<'tcx>) -> Expr { trace!(constant=?c, "codegen_constant"); let span = Some(&c.span); - match self.monomorphize(c.literal) { - ConstantKind::Ty(ct) => self.codegen_const(ct, span), - ConstantKind::Val(val, ty) => self.codegen_const_value(val, ty, span), - ConstantKind::Unevaluated(unevaluated, ty) => { + match self.monomorphize(c.const_) { + mirConst::Ty(ct) => self.codegen_const(ct, span), + mirConst::Val(val, ty) => self.codegen_const_value(val, ty, span), + mirConst::Unevaluated(unevaluated, ty) => { self.codegen_const_unevaluated(unevaluated, ty, span) } } @@ -125,8 +123,8 @@ impl<'tcx> GotocCtx<'tcx> { 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 } => { - self.codegen_slice_value(v, lit_ty, span, data.inner(), start, end) + ConstValue::Slice { data, meta } => { + self.codegen_slice_value(v, lit_ty, span, data.inner(), meta.try_into().unwrap()) } ConstValue::Indirect { alloc_id, offset } => { let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory(); @@ -155,15 +153,12 @@ impl<'tcx> GotocCtx<'tcx> { lit_ty: Ty<'tcx>, span: Option<&Span>, data: &'tcx Allocation, - start: usize, - end: usize, + size: usize, ) -> Expr { if let ty::Ref(_, ref_ty, _) = lit_ty.kind() { match ref_ty.kind() { ty::Str => { // a string literal - // These seem to always start at 0 - assert_eq!(start, 0); // Create a static variable that holds its value let mem_var = self.codegen_const_allocation(data, None); @@ -179,7 +174,7 @@ impl<'tcx> GotocCtx<'tcx> { }; // Extract the actual string literal - let slice = data.inspect_with_uninit_and_ptr_outside_interpreter(start..end); + let slice = data.inspect_with_uninit_and_ptr_outside_interpreter(0..size); let s = ::std::str::from_utf8(slice).expect("non utf8 str from miri"); // Store the identifier to the string literal in the goto context @@ -187,7 +182,7 @@ impl<'tcx> GotocCtx<'tcx> { // Codegen as a fat pointer let data_expr = mem_var.cast_to(Type::unsigned_int(8).to_pointer()); - let len_expr = Expr::int_constant(end - start, Type::size_t()); + let len_expr = Expr::int_constant(size, Type::size_t()); return slice_fat_ptr( self.codegen_ty(lit_ty), data_expr, @@ -198,8 +193,7 @@ impl<'tcx> GotocCtx<'tcx> { ty::Slice(slice_ty) => { if let Uint(UintTy::U8) = slice_ty.kind() { let mem_var = self.codegen_const_allocation(data, None); - let slice = - data.inspect_with_uninit_and_ptr_outside_interpreter(start..end); + let slice = data.inspect_with_uninit_and_ptr_outside_interpreter(0..size); let len = slice.len(); let data_expr = mem_var.cast_to(Type::unsigned_int(8).to_pointer()); let len_expr = Expr::int_constant(len, Type::size_t()); diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index fd296b28d757..c4785ac98b81 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -3,7 +3,7 @@ //! This module contains a MIR pass that replaces some intrinsics by rust intrinsics models as //! well as validation logic that can only be added during monomorphization. use rustc_index::IndexVec; -use rustc_middle::mir::{interpret::ConstValue, Body, ConstantKind, Operand, TerminatorKind}; +use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, TerminatorKind}; use rustc_middle::mir::{Local, LocalDecl}; use rustc_middle::ty::{self, Ty, TyCtxt}; use rustc_middle::ty::{Const, GenericArgsRef}; @@ -69,7 +69,7 @@ impl<'tcx> ModelIntrinsics<'tcx> { new_gen_args.push(len.into()); let Operand::Constant(fn_def) = func else { unreachable!() }; - fn_def.literal = ConstantKind::from_value( + fn_def.const_ = mirConst::from_value( ConstValue::ZeroSized, tcx.type_of(stub_id).instantiate(tcx, &new_gen_args), ); diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 37b26a136447..c27b5e9ae0d9 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -22,11 +22,11 @@ use rustc_data_structures::stable_hasher::{HashStable, StableHasher}; use rustc_hir::def::DefKind; use rustc_hir::def_id::DefId; use rustc_hir::ItemId; -use rustc_middle::mir::interpret::{AllocId, ConstValue, ErrorHandled, GlobalAlloc, Scalar}; +use rustc_middle::mir::interpret::{AllocId, ErrorHandled, GlobalAlloc, Scalar}; use rustc_middle::mir::mono::MonoItem; use rustc_middle::mir::visit::Visitor as MirVisitor; use rustc_middle::mir::{ - Body, CastKind, Constant, ConstantKind, Location, Rvalue, Terminator, TerminatorKind, + Body, CastKind, Const, ConstOperand, ConstValue, Location, Rvalue, Terminator, TerminatorKind, UnevaluatedConst, }; use rustc_middle::span_bug; @@ -322,7 +322,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { ConstValue::Scalar(Scalar::Ptr(ptr, _size)) => { self.collected.extend(collect_alloc_items(self.tcx, ptr.provenance).iter()); } - ConstValue::Slice { data: alloc, start: _, end: _ } => { + ConstValue::Slice { data: alloc, .. } => { for id in alloc.inner().provenance().provenances() { self.collected.extend(collect_alloc_items(self.tcx, id).iter()) } @@ -435,12 +435,12 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { } /// Collect constants that are represented as static variables. - fn visit_constant(&mut self, constant: &Constant<'tcx>, location: Location) { - let literal = self.monomorphize(constant.literal); - debug!(?constant, ?location, ?literal, "visit_constant"); - let val = match literal { - ConstantKind::Val(const_val, _) => const_val, - ConstantKind::Ty(ct) => match ct.kind() { + fn visit_constant(&mut self, constant: &ConstOperand<'tcx>, location: Location) { + let const_ = self.monomorphize(constant.const_); + debug!(?constant, ?location, ?const_, "visit_constant"); + let val = match const_ { + Const::Val(const_val, _) => const_val, + Const::Ty(ct) => match ct.kind() { ConstKind::Value(v) => self.tcx.valtree_to_const_val((ct.ty(), v)), ConstKind::Unevaluated(_) => unreachable!(), // Nothing to do @@ -454,7 +454,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { unreachable!("Unexpected constant type {:?} ({:?})", ct, ct.kind()) } }, - ConstantKind::Unevaluated(un_eval, _) => { + Const::Unevaluated(un_eval, _) => { // Thread local fall into this category. match self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, None) { // The `monomorphize` call should have evaluated that constant already. @@ -473,8 +473,8 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { span_bug!( span, "Unexpected polymorphic constant: {:?} {:?}", - literal, - constant.literal + const_, + constant.const_ ) } } diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs index 3774d0afc148..a455a8d5e7ca 100644 --- a/kani-compiler/src/kani_middle/stubbing/transform.rs +++ b/kani-compiler/src/kani_middle/stubbing/transform.rs @@ -14,8 +14,7 @@ use rustc_data_structures::fingerprint::Fingerprint; use rustc_hir::{def_id::DefId, definitions::DefPathHash}; use rustc_index::IndexVec; use rustc_middle::mir::{ - interpret::ConstValue, visit::MutVisitor, Body, ConstantKind, Local, LocalDecl, Location, - Operand, + visit::MutVisitor, Body, Const, ConstValue, Local, LocalDecl, Location, Operand, }; use rustc_middle::ty::{self, TyCtxt}; @@ -79,7 +78,7 @@ impl<'tcx> MutVisitor<'tcx> for ForeignFunctionTransformer<'tcx> { let Operand::Constant(function_definition) = operand else { return; }; - function_definition.literal = ConstantKind::from_value( + function_definition.const_ = Const::from_value( ConstValue::ZeroSized, self.tcx.type_of(stub).instantiate(self.tcx, arguments), ); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index b89dd2f6a55e..53fedae29b02 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-09-19" +channel = "nightly-2023-09-23" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 6d9575e049fca615c7f4b20edebbeee05331c5e5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 5 Oct 2023 12:25:57 +0200 Subject: [PATCH 13/13] Bump Kani version to 0.38.0 (#2798) Next Kani release. Also includes fixes to changelog formatting. --- CHANGELOG.md | 34 ++++++++++++++++++++++++++-------- Cargo.lock | 18 +++++++++--------- Cargo.toml | 2 +- cprover_bindings/Cargo.toml | 2 +- kani-compiler/Cargo.toml | 2 +- kani-driver/Cargo.toml | 2 +- kani_metadata/Cargo.toml | 2 +- library/kani/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 11 files changed, 44 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b987e5a8f76..760748037be5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,24 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. +## [0.38.0] + +### Major Changes + +* Deprecate `any_slice` by @zhassan-aws in https://github.com/model-checking/kani/pull/2789 + +### What's Changed + +* Provide better error message for invalid stubs by @JustusAdam in https://github.com/model-checking/kani/pull/2787 +* Simple Stubbing with Contracts by @JustusAdam in https://github.com/model-checking/kani/pull/2746 +* Avoid mismatch when generating structs that represent scalar data but also include ZSTs by @adpaco-aws in https://github.com/model-checking/kani/pull/2794 +* Prevent kani crash during setup for first time by @jaisnan in https://github.com/model-checking/kani/pull/2799 +* Create concrete playback temp files in source directory by @tautschnig in https://github.com/model-checking/kani/pull/2804 +* Bump CBMC version by @zhassan-aws in https://github.com/model-checking/kani/pull/2796 +* Update Rust toolchain to 2023-09-23 by @tautschnig in https://github.com/model-checking/kani/pull/2806 + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.37.0...kani-0.38.0 + ## [0.37.0] ### Major Changes @@ -11,7 +29,7 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from * Delete obsolete stubs for `Vec` and related options by @zhassan-aws in https://github.com/model-checking/kani/pull/2770 * Add support for the ARM64 Linux platform by @adpaco-aws in https://github.com/model-checking/kani/pull/2757 -## What's Changed +### What's Changed * Function Contracts: Support for defining and checking `requires` and `ensures` clauses by @JustusAdam in https://github.com/model-checking/kani/pull/2655 * Force `any_vec` capacity to match length by @celinval in https://github.com/model-checking/kani/pull/2765 @@ -24,7 +42,7 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from ## [0.36.0] -## What's Changed +### What's Changed * Enable `-Z stubbing` and error out instead of ignoring stub by @celinval in https://github.com/model-checking/kani/pull/2678 * Enable concrete playback for failure of UB checks by @zhassan-aws in https://github.com/model-checking/kani/pull/2727 @@ -35,7 +53,7 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from ## [0.35.0] -## What's Changed +### What's Changed * Add support to `simd_bitmask` by @celinval in https://github.com/model-checking/kani/pull/2677 * Add integer overflow checking for `simd_div` and `simd_rem` by @reisnera in https://github.com/model-checking/kani/pull/2645 @@ -52,7 +70,7 @@ By default, Kani will now run CBMC with CaDiCaL, since this solver has outperfor User's should still be able to select Minisat (or a different solver) either by using `#[solver]` harness attribute, or by passing `--solver=` command line option. -## What's Changed +### What's Changed * Allow specifying the scheduling strategy in #[kani_proof] for async functions by @fzaiser in https://github.com/model-checking/kani/pull/1661 * Support for stubbing out foreign functions by @feliperodri in https://github.com/model-checking/kani/pull/2658 @@ -67,7 +85,7 @@ or by passing `--solver=` command line option. ## [0.33.0] -## What's Changed +### What's Changed * Add support for sysconf by @feliperodri in https://github.com/model-checking/kani/pull/2557 * Print Kani version by @adpaco-aws in https://github.com/model-checking/kani/pull/2619 * Upgrade Rust toolchain to nightly-2023-07-01 by @qinheping in https://github.com/model-checking/kani/pull/2616 @@ -77,7 +95,7 @@ or by passing `--solver=` command line option. ## [0.32.0] -## What's Changed +### What's Changed * Add kani::spawn and an executor to the Kani library by @fzaiser in https://github.com/model-checking/kani/pull/1659 * Add "kani" configuration key to enable conditional compilation in build scripts by @celinval in https://github.com/model-checking/kani/pull/2297 @@ -91,7 +109,7 @@ or by passing `--solver=` command line option. ## [0.31.0] -## What's Changed +### What's Changed * Add `--exact` flag by @jaisnan in https://github.com/model-checking/kani/pull/2527 * Build the verification libraries using Kani compiler by @celinval in https://github.com/model-checking/kani/pull/2534 * Verify all Kani attributes in all crate items upfront by @celinval in https://github.com/model-checking/kani/pull/2536 @@ -102,7 +120,7 @@ or by passing `--solver=` command line option. ## [0.30.0] -## What's Changed +### What's Changed * Remove --harness requirement from stubbing by @celinval in https://github.com/model-checking/kani/pull/2495 * Add target selection for cargo kani by @celinval in https://github.com/model-checking/kani/pull/2507 * Generate Multiple playback harnesses when multiple crashes exist in a single harness. by @YoshikiTakashima in https://github.com/model-checking/kani/pull/2496 diff --git a/Cargo.lock b/Cargo.lock index 59770bbda6d2..5aad3f1d4614 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -119,7 +119,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.37.0" +version = "0.38.0" dependencies = [ "anyhow", "cargo_metadata", @@ -264,7 +264,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.37.0" +version = "0.38.0" dependencies = [ "lazy_static", "linear-map", @@ -463,14 +463,14 @@ checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" [[package]] name = "kani" -version = "0.37.0" +version = "0.38.0" dependencies = [ "kani_macros", ] [[package]] name = "kani-compiler" -version = "0.37.0" +version = "0.38.0" dependencies = [ "clap", "cprover_bindings", @@ -491,7 +491,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.37.0" +version = "0.38.0" dependencies = [ "anyhow", "cargo_metadata", @@ -519,7 +519,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.37.0" +version = "0.38.0" dependencies = [ "anyhow", "home", @@ -528,7 +528,7 @@ dependencies = [ [[package]] name = "kani_macros" -version = "0.37.0" +version = "0.38.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -538,7 +538,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.37.0" +version = "0.38.0" dependencies = [ "clap", "cprover_bindings", @@ -1115,7 +1115,7 @@ checksum = "942b4a808e05215192e39f4ab80813e599068285906cc91aa64f923db842bd5a" [[package]] name = "std" -version = "0.37.0" +version = "0.38.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index d99a2ffde289..e2a61bdd95b3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.37.0" +version = "0.38.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index e8c523ad4bd3..2a1d5e50c0ac 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index c888afac5f01..f0758cd28ecf 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 2f01fa9e83dd..3238e9bc599c 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.37.0" +version = "0.38.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 0deb1b994821..c9fb64016b7c 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 97e30ba6294e..358e1a3c20d8 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 42c30f20c29a..535dd19a2a03 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 2a5ed385c8dc..157ef0acc613 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 014f2949af0f..bfd81c1be85e 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.37.0" +version = "0.38.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"