From 520cb3e01dd4a2c53dfcb1cc8c3a8ee5d6c6e29f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 5 Aug 2024 21:01:12 +0200 Subject: [PATCH 01/10] Update toolchain to 2024-08-05 (#3416) * Remove `gen_function_local_variable` and `initializer_fn_name`, the last uses of both of which were removed in #3305. * Mark `arg_count`, which was introduced in #3363, as `allow(dead_code)` as it will soon be used. * Mark `insert_bb`, which was introduced in #3382, as `allow(dead_code)` as it will soon be used. The toolchain upgrade to 2024-08-04 includes several bugfixes to dead-code analysis in rustc, explaining why we the recent PRs as listed above weren't flagged before for introducing dead code. Resolves: #3411 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../src/codegen_cprover_gotoc/context/goto_ctx.rs | 11 ----------- .../src/codegen_cprover_gotoc/utils/names.rs | 4 ---- kani-compiler/src/kani_middle/transform/body.rs | 2 ++ rust-toolchain.toml | 2 +- 4 files changed, 3 insertions(+), 16 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index e360cd491edd..3f17f4b87233 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -139,17 +139,6 @@ impl<'tcx> GotocCtx<'tcx> { sym } - // Generate a Symbol Expression representing a function variable from the MIR - pub fn gen_function_local_variable( - &mut self, - c: u64, - fname: &str, - t: Type, - loc: Location, - ) -> Symbol { - self.gen_stack_variable(c, fname, "var", t, loc) - } - /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable /// It is an error to reuse an existing `c`, `fname` `prefix` tuple. fn gen_stack_variable( diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index c290f2bf6428..01f5ca4b3dce 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -45,10 +45,6 @@ impl<'tcx> GotocCtx<'tcx> { (name, base_name) } - pub fn initializer_fn_name(var_name: &str) -> String { - format!("{var_name}_init") - } - /// The name for a tuple field pub fn tuple_fld_name(n: usize) -> String { format!("{n}") diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 3d110c4e9656..fa4e5eb1ad97 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -54,6 +54,7 @@ impl MutableBody { &self.locals } + #[allow(dead_code)] pub fn arg_count(&self) -> usize { self.arg_count } @@ -330,6 +331,7 @@ impl MutableBody { /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the /// terminator of the newly inserted basic block. + #[allow(dead_code)] pub fn insert_bb( &mut self, mut bb: BasicBlock, diff --git a/rust-toolchain.toml b/rust-toolchain.toml index ab901a10d7e4..4b2a2819e4ce 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-08-03" +channel = "nightly-2024-08-05" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 6eb7dddb0a15615ad341af2b7289def5bb4a4a43 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 6 Aug 2024 11:11:39 +0200 Subject: [PATCH 02/10] Automatic toolchain upgrade to nightly-2024-08-06 (#3420) Update Rust toolchain from nightly-2024-08-05 to nightly-2024-08-06 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com> --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 4b2a2819e4ce..23a3f2bc99eb 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-08-05" +channel = "nightly-2024-08-06" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 2a0e9bdbb65459b05f499f687285cb764e654354 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Tue, 6 Aug 2024 11:59:15 -0400 Subject: [PATCH 03/10] Unify kani library and kani core logic (#3333) 1. Unifies `Kani library` and `kani_core` for `Arbitrary`, `mem` and `intrinsics` along with the `internal` module. 2. Adjusts some regression expected files to reflect the new underlying source of Arbitrary Related to #https://github.com/model-checking/kani/issues/3257 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- Cargo.lock | 1 + library/kani/Cargo.toml | 2 + library/kani/src/arbitrary.rs | 146 +----- library/kani/src/internal.rs | 160 ------- library/kani/src/lib.rs | 310 +------------ library/kani/src/mem.rs | 433 ------------------ library/kani_core/Cargo.toml | 2 +- library/kani_core/src/lib.rs | 5 + library/kani_core/src/mem.rs | 76 ++- library/kani_macros/Cargo.toml | 2 +- .../modifies/check_invalid_modifies.expected | 7 +- .../function-contract/valid_ptr.expected | 1 - .../verify_std_cmd/verify_std.sh | 2 +- .../non_arbitrary_param/expected | 6 +- 14 files changed, 71 insertions(+), 1082 deletions(-) delete mode 100644 library/kani/src/internal.rs delete mode 100644 library/kani/src/mem.rs diff --git a/Cargo.lock b/Cargo.lock index dcd7b057b3d8..7d7580e3b742 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -434,6 +434,7 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" name = "kani" version = "0.53.0" dependencies = [ + "kani_core", "kani_macros", ] diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 91fee3dabf30..1fba7875672a 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -10,6 +10,8 @@ publish = false [dependencies] kani_macros = { path = "../kani_macros" } +kani_core = { path = "../kani_core" } [features] concrete_playback = [] +no_core=["kani_macros/no_core"] diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 83b113d64927..f16f06165d29 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -4,151 +4,7 @@ //! This module introduces the `Arbitrary` trait as well as implementation for //! primitive types and other std containers. -use std::{ - marker::{PhantomData, PhantomPinned}, - num::*, -}; - -/// This trait should be used to generate symbolic variables that represent any valid value of -/// its type. -pub trait Arbitrary -where - Self: Sized, -{ - fn any() -> Self; - fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - [(); MAX_ARRAY_LENGTH].map(|_| Self::any()) - } -} - -/// The given type can be represented by an unconstrained symbolic value of size_of::. -macro_rules! trivial_arbitrary { - ( $type: ty ) => { - impl Arbitrary for $type { - #[inline(always)] - fn any() -> Self { - // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic. - unsafe { crate::any_raw_internal::() } - } - fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - unsafe { crate::any_raw_array::() } - } - } - }; -} - -trivial_arbitrary!(u8); -trivial_arbitrary!(u16); -trivial_arbitrary!(u32); -trivial_arbitrary!(u64); -trivial_arbitrary!(u128); -trivial_arbitrary!(usize); - -trivial_arbitrary!(i8); -trivial_arbitrary!(i16); -trivial_arbitrary!(i32); -trivial_arbitrary!(i64); -trivial_arbitrary!(i128); -trivial_arbitrary!(isize); - -// We do not constrain floating points values per type spec. Users must add assumptions to their -// verification code if they want to eliminate NaN, infinite, or subnormal. -trivial_arbitrary!(f32); -trivial_arbitrary!(f64); - -// Similarly, we do not constraint values for non-standard floating types. -trivial_arbitrary!(f16); -trivial_arbitrary!(f128); - -trivial_arbitrary!(()); - -impl Arbitrary for bool { - #[inline(always)] - fn any() -> Self { - let byte = u8::any(); - crate::assume(byte < 2); - byte == 1 - } -} - -/// Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] -/// Ref: -impl Arbitrary for char { - #[inline(always)] - fn any() -> Self { - // Generate an arbitrary u32 and constrain it to make it a valid representation of char. - let val = u32::any(); - crate::assume(val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val)); - unsafe { char::from_u32_unchecked(val) } - } -} - -macro_rules! nonzero_arbitrary { - ( $type: ty, $base: ty ) => { - impl Arbitrary for $type { - #[inline(always)] - fn any() -> Self { - let val = <$base>::any(); - crate::assume(val != 0); - unsafe { <$type>::new_unchecked(val) } - } - } - }; -} - -nonzero_arbitrary!(NonZeroU8, u8); -nonzero_arbitrary!(NonZeroU16, u16); -nonzero_arbitrary!(NonZeroU32, u32); -nonzero_arbitrary!(NonZeroU64, u64); -nonzero_arbitrary!(NonZeroU128, u128); -nonzero_arbitrary!(NonZeroUsize, usize); - -nonzero_arbitrary!(NonZeroI8, i8); -nonzero_arbitrary!(NonZeroI16, i16); -nonzero_arbitrary!(NonZeroI32, i32); -nonzero_arbitrary!(NonZeroI64, i64); -nonzero_arbitrary!(NonZeroI128, i128); -nonzero_arbitrary!(NonZeroIsize, isize); - -impl Arbitrary for [T; N] -where - T: Arbitrary, -{ - fn any() -> Self { - T::any_array() - } -} - -impl Arbitrary for Option -where - T: Arbitrary, -{ - fn any() -> Self { - if bool::any() { Some(T::any()) } else { None } - } -} - -impl Arbitrary for Result -where - T: Arbitrary, - E: Arbitrary, -{ - fn any() -> Self { - if bool::any() { Ok(T::any()) } else { Err(E::any()) } - } -} - -impl Arbitrary for std::marker::PhantomData { - fn any() -> Self { - PhantomData - } -} - -impl Arbitrary for std::marker::PhantomPinned { - fn any() -> Self { - PhantomPinned - } -} +use crate::Arbitrary; impl Arbitrary for std::boxed::Box where diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs deleted file mode 100644 index 68b15316b4c1..000000000000 --- a/library/kani/src/internal.rs +++ /dev/null @@ -1,160 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use crate::arbitrary::Arbitrary; -use std::ptr; - -/// Helper trait for code generation for `modifies` contracts. -/// -/// We allow the user to provide us with a pointer-like object that we convert as needed. -#[doc(hidden)] -pub trait Pointer { - /// Type of the pointed-to data - type Inner: ?Sized; - - /// used for havocking on replecement of a `modifies` clause. - unsafe fn assignable(self) -> *mut Self::Inner; -} - -impl Pointer for &T { - type Inner = T; - unsafe fn assignable(self) -> *mut Self::Inner { - self as *const T as *mut T - } -} - -impl Pointer for &mut T { - type Inner = T; - - unsafe fn assignable(self) -> *mut Self::Inner { - self as *mut T - } -} - -impl Pointer for *const T { - type Inner = T; - - unsafe fn assignable(self) -> *mut Self::Inner { - self as *mut T - } -} - -impl Pointer for *mut T { - type Inner = T; - unsafe fn assignable(self) -> *mut Self::Inner { - self - } -} - -/// A way to break the ownerhip rules. Only used by contracts where we can -/// guarantee it is done safely. -/// TODO: Remove this! This is not safe. Users should be able to use `ptr::read` and `old` if -/// they really need to. See . -#[inline(never)] -#[doc(hidden)] -#[rustc_diagnostic_item = "KaniUntrackedDeref"] -pub fn untracked_deref(_: &T) -> T { - todo!() -} - -/// CBMC contracts currently has a limitation where `free` has to be in scope. -/// However, if there is no dynamic allocation in the harness, slicing removes `free` from the -/// scope. -/// -/// Thus, this function will basically translate into: -/// ```c -/// // This is a no-op. -/// free(NULL); -/// ``` -#[inline(never)] -#[doc(hidden)] -#[rustc_diagnostic_item = "KaniInitContracts"] -pub fn init_contracts() {} - -/// This should only be used within contracts. The intent is to -/// perform type inference on a closure's argument -/// TODO: This should be generated inside the function that has contract. This is used for -/// remembers. -#[doc(hidden)] -pub fn apply_closure bool>(f: U, x: &T) -> bool { - f(x) -} - -/// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. -/// Only for use within function contracts and will not be replaced if the recursive or function stub -/// replace contracts are not used. -#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] -#[rustc_diagnostic_item = "KaniWriteAny"] -#[inline(never)] -#[doc(hidden)] -pub unsafe fn write_any(_pointer: *mut T) { - // This function should not be reacheable. - // Users must include `#[kani::recursion]` in any function contracts for recursive functions; - // otherwise, this might not be properly instantiate. We mark this as unreachable to make - // sure Kani doesn't report any false positives. - unreachable!() -} - -/// Fill in a slice with kani::any. -/// Intended as a post compilation replacement for write_any -#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] -#[rustc_diagnostic_item = "KaniWriteAnySlice"] -#[inline(always)] -pub unsafe fn write_any_slice(slice: *mut [T]) { - (*slice).fill_with(T::any) -} - -/// Fill in a pointer with kani::any. -/// Intended as a post compilation replacement for write_any -#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] -#[rustc_diagnostic_item = "KaniWriteAnySlim"] -#[inline(always)] -pub unsafe fn write_any_slim(pointer: *mut T) { - ptr::write(pointer, T::any()) -} - -/// Fill in a str with kani::any. -/// Intended as a post compilation replacement for write_any. -/// Not yet implemented -#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] -#[rustc_diagnostic_item = "KaniWriteAnyStr"] -#[inline(always)] -pub unsafe fn write_any_str(_s: *mut str) { - //TODO: strings introduce new UB - //(*s).as_bytes_mut().fill_with(u8::any) - //TODO: String validation - unimplemented!("Kani does not support creating arbitrary `str`") -} - -/// Function that calls a closure used to implement contracts. -/// -/// In contracts, we cannot invoke the generated closures directly, instead, we call register -/// contract. This function is a no-op. However, in the reality, we do want to call the closure, -/// so we swap the register body by this function body. -#[doc(hidden)] -#[allow(dead_code)] -#[rustc_diagnostic_item = "KaniRunContract"] -#[crate::unstable( - feature = "function-contracts", - issue = "none", - reason = "internal function required to run contract closure" -)] -fn run_contract_fn T>(func: F) -> T { - func() -} - -/// This is used by contracts to select which version of the contract to use during codegen. -#[doc(hidden)] -pub type Mode = u8; - -/// Keep the original body. -pub const ORIGINAL: Mode = 0; - -/// Run the check with recursion support. -pub const RECURSION_CHECK: Mode = 1; - -/// Run the simple check with no recursion support. -pub const SIMPLE_CHECK: Mode = 2; - -/// Stub the body with its contract. -pub const REPLACE: Mode = 3; diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 046c6e7a0667..59a89622a52d 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -28,19 +28,13 @@ pub mod arbitrary; mod concrete_playback; pub mod futures; pub mod invariant; -pub mod mem; pub mod shadow; pub mod slice; -pub mod tuple; pub mod vec; -#[doc(hidden)] -pub mod internal; - mod mem_init; mod models; -pub use arbitrary::Arbitrary; #[cfg(feature = "concrete_playback")] pub use concrete_playback::concrete_playback_run; pub use invariant::Invariant; @@ -53,287 +47,19 @@ pub fn concrete_playback_run(_: Vec>, _: F) { pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin}; -/// Creates an assumption that will be valid after this statement run. Note that the assumption -/// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the -/// program will exit successfully. -/// -/// # Example: -/// -/// The code snippet below should never panic. -/// -/// ```rust -/// let i : i32 = kani::any(); -/// kani::assume(i > 10); -/// if i < 0 { -/// panic!("This will never panic"); -/// } -/// ``` -/// -/// The following code may panic though: -/// -/// ```rust -/// let i : i32 = kani::any(); -/// assert!(i < 0, "This may panic and verification should fail."); -/// kani::assume(i > 10); -/// ``` -#[inline(never)] -#[rustc_diagnostic_item = "KaniAssume"] -#[cfg(not(feature = "concrete_playback"))] -pub fn assume(cond: bool) { - let _ = cond; -} - -#[inline(never)] -#[rustc_diagnostic_item = "KaniAssume"] -#[cfg(feature = "concrete_playback")] -pub fn assume(cond: bool) { - assert!(cond, "`kani::assume` should always hold"); -} - -/// `implies!(premise => conclusion)` means that if the `premise` is true, so -/// must be the `conclusion`. -/// -/// This simply expands to `!premise || conclusion` and is intended to make checks more readable, -/// as the concept of an implication is more natural to think about than its expansion. -#[macro_export] -macro_rules! implies { - ($premise:expr => $conclusion:expr) => { - !($premise) || ($conclusion) - }; -} - -/// Creates an assertion of the specified condition and message. -/// -/// # Example: -/// -/// ```rust -/// let x: bool = kani::any(); -/// let y = !x; -/// kani::assert(x || y, "ORing a boolean variable with its negation must be true") -/// ``` -#[cfg(not(feature = "concrete_playback"))] -#[inline(never)] -#[rustc_diagnostic_item = "KaniAssert"] -pub const fn assert(cond: bool, msg: &'static str) { - let _ = cond; - let _ = msg; -} - -#[cfg(feature = "concrete_playback")] -#[inline(never)] -#[rustc_diagnostic_item = "KaniAssert"] -pub const fn assert(cond: bool, msg: &'static str) { - assert!(cond, "{}", msg); -} - -/// Creates an assertion of the specified condition, but does not assume it afterwards. -/// -/// # Example: -/// -/// ```rust -/// let x: bool = kani::any(); -/// let y = !x; -/// kani::check(x || y, "ORing a boolean variable with its negation must be true") -/// ``` -#[cfg(not(feature = "concrete_playback"))] -#[inline(never)] -#[rustc_diagnostic_item = "KaniCheck"] -pub const fn check(cond: bool, msg: &'static str) { - let _ = cond; - let _ = msg; -} - -#[cfg(feature = "concrete_playback")] -#[inline(never)] -#[rustc_diagnostic_item = "KaniCheck"] -pub const fn check(cond: bool, msg: &'static str) { - assert!(cond, "{}", msg); -} - -/// Creates a cover property with the specified condition and message. -/// -/// # Example: -/// -/// ```rust -/// kani::cover(slice.len() == 0, "The slice may have a length of 0"); -/// ``` -/// -/// A cover property checks if there is at least one execution that satisfies -/// the specified condition at the location in which the function is called. -/// -/// Cover properties are reported as: -/// - SATISFIED: if Kani found an execution that satisfies the condition -/// - UNSATISFIABLE: if Kani proved that the condition cannot be satisfied -/// - UNREACHABLE: if Kani proved that the cover property itself is unreachable (i.e. it is vacuously UNSATISFIABLE) -/// -/// This function is called by the [`cover!`] macro. The macro is more -/// convenient to use. -/// -#[inline(never)] -#[rustc_diagnostic_item = "KaniCover"] -pub const fn cover(_cond: bool, _msg: &'static str) {} +// Kani proc macros must be in a separate crate +pub use kani_macros::*; -/// This creates an symbolic *valid* value of type `T`. You can assign the return value of this -/// function to a variable that you want to make symbolic. -/// -/// # Example: -/// -/// In the snippet below, we are verifying the behavior of the function `fn_under_verification` -/// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero. -/// -/// ```rust -/// let inputA = kani::any::(); -/// fn_under_verification(inputA); -/// ``` -/// -/// Note: This is a safe construct and can only be used with types that implement the `Arbitrary` -/// trait. The Arbitrary trait is used to build a symbolic value that represents all possible -/// valid values for type `T`. -#[rustc_diagnostic_item = "KaniAny"] -#[inline(always)] -pub fn any() -> T { - T::any() -} +// Declare common Kani API such as assume, assert +kani_core::kani_lib!(kani); -/// This function is only used for function contract instrumentation. -/// It behaves exaclty like `kani::any()`, except it will check for the trait bounds -/// at compilation time. It allows us to avoid type checking errors while using function -/// contracts only for verification. -#[rustc_diagnostic_item = "KaniAnyModifies"] -#[inline(never)] +// Used to bind `core::assert` to a different name to avoid possible name conflicts if a +// crate uses `extern crate std as core`. See +// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187 #[doc(hidden)] -pub fn any_modifies() -> T { - // This function should not be reacheable. - // Users must include `#[kani::recursion]` in any function contracts for recursive functions; - // otherwise, this might not be properly instantiate. We mark this as unreachable to make - // sure Kani doesn't report any false positives. - unreachable!() -} - -/// This creates a symbolic *valid* value of type `T`. -/// The value is constrained to be a value accepted by the predicate passed to the filter. -/// You can assign the return value of this function to a variable that you want to make symbolic. -/// -/// # Example: -/// -/// In the snippet below, we are verifying the behavior of the function `fn_under_verification` -/// under all possible `u8` input values between 0 and 12. -/// -/// ```rust -/// let inputA: u8 = kani::any_where(|x| *x < 12); -/// fn_under_verification(inputA); -/// ``` -/// -/// Note: This is a safe construct and can only be used with types that implement the `Arbitrary` -/// trait. The Arbitrary trait is used to build a symbolic value that represents all possible -/// valid values for type `T`. -#[inline(always)] -pub fn any_where bool>(f: F) -> T { - let result = T::any(); - assume(f(&result)); - result -} - -/// This function creates a symbolic value of type `T`. This may result in an invalid value. -/// -/// # Safety -/// -/// This function is unsafe and it may represent invalid `T` values which can lead to many -/// undesirable undefined behaviors. Because of that, this function can only be used -/// internally when we can guarantee that the type T has no restriction regarding its bit level -/// representation. -/// -/// This function is also used to find concrete values in the CBMC output trace -/// and return those concrete values in concrete playback mode. -/// -/// Note that SIZE_T must be equal the size of type T in bytes. -#[inline(never)] -#[cfg(not(feature = "concrete_playback"))] -unsafe fn any_raw_internal() -> T { - any_raw::() -} - -/// This is the same as [any_raw_internal] for verification flow, but not for concrete playback. -#[inline(never)] #[cfg(not(feature = "concrete_playback"))] -unsafe fn any_raw_array() -> [T; N] { - any_raw::<[T; N]>() -} - -#[cfg(feature = "concrete_playback")] -use concrete_playback::{any_raw_array, any_raw_internal}; - -/// This low-level function returns nondet bytes of size T. -#[rustc_diagnostic_item = "KaniAnyRaw"] -#[inline(never)] -#[allow(dead_code)] -fn any_raw() -> T { - kani_intrinsic() -} - -/// Function used to generate panic with a static message as this is the only one currently -/// supported by Kani display. -/// -/// During verification this will get replaced by `assert(false)`. For concrete executions, we just -/// invoke the regular `std::panic!()` function. This function is used by our standard library -/// overrides, but not the other way around. -#[inline(never)] -#[rustc_diagnostic_item = "KaniPanic"] -#[doc(hidden)] -pub const fn panic(message: &'static str) -> ! { - panic!("{}", message) -} +pub use core::assert as __kani__workaround_core_assert; -/// An empty body that can be used to define Kani intrinsic functions. -/// -/// A Kani intrinsic is a function that is interpreted by Kani compiler. -/// While we could use `unreachable!()` or `panic!()` as the body of a kani intrinsic -/// function, both cause Kani to produce a warning since we don't support caller location. -/// (see https://github.com/model-checking/kani/issues/2010). -/// -/// This function is dead, since its caller is always handled via a hook anyway, -/// so we just need to put a body that rustc does not complain about. -/// An infinite loop works out nicely. -fn kani_intrinsic() -> T { - #[allow(clippy::empty_loop)] - loop {} -} -/// A macro to check if a condition is satisfiable at a specific location in the -/// code. -/// -/// # Example 1: -/// -/// ```rust -/// let mut set: BTreeSet = BTreeSet::new(); -/// set.insert(kani::any()); -/// set.insert(kani::any()); -/// // check if the set can end up with a single element (if both elements -/// // inserted were the same) -/// kani::cover!(set.len() == 1); -/// ``` -/// The macro can also be called without any arguments to check if a location is -/// reachable. -/// -/// # Example 2: -/// -/// ```rust -/// match e { -/// MyEnum::A => { /* .. */ } -/// MyEnum::B => { -/// // make sure the `MyEnum::B` variant is possible -/// kani::cover!(); -/// // .. -/// } -/// } -/// ``` -/// -/// A custom message can also be passed to the macro. -/// -/// # Example 3: -/// -/// ```rust -/// kani::cover!(x > y, "x can be greater than y") -/// ``` #[macro_export] macro_rules! cover { () => { @@ -347,15 +73,17 @@ macro_rules! cover { }; } -// Used to bind `core::assert` to a different name to avoid possible name conflicts if a -// crate uses `extern crate std as core`. See -// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187 -#[doc(hidden)] -#[cfg(not(feature = "concrete_playback"))] -pub use core::assert as __kani__workaround_core_assert; - -// Kani proc macros must be in a separate crate -pub use kani_macros::*; +/// `implies!(premise => conclusion)` means that if the `premise` is true, so +/// must be the `conclusion`. +/// +/// This simply expands to `!premise || conclusion` and is intended to make checks more readable, +/// as the concept of an implication is more natural to think about than its expansion. +#[macro_export] +macro_rules! implies { + ($premise:expr => $conclusion:expr) => { + !($premise) || ($conclusion) + }; +} pub(crate) use kani_macros::unstable_feature as unstable; diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs deleted file mode 100644 index f718c09ec38d..000000000000 --- a/library/kani/src/mem.rs +++ /dev/null @@ -1,433 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains functions useful for checking unsafe memory access. -//! -//! Given the following validity rules provided in the Rust documentation: -//! (accessed Feb 6th, 2024) -//! -//! 1. A null pointer is never valid, not even for accesses of size zero. -//! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer -//! be dereferenceable: the memory range of the given size starting at the pointer must all be -//! within the bounds of a single allocated object. Note that in Rust, every (stack-allocated) -//! variable is considered a separate allocated object. -//! ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory, -//! i.e., deallocation makes pointers invalid even for zero-sized operations.~~ -//! ZST access is not OK for any pointer. -//! See: -//! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized -//! accesses, even if some memory happens to exist at that address and gets deallocated. -//! This corresponds to writing your own allocator: allocating zero-sized objects is not very -//! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is -//! `NonNull::dangling`. -//! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic -//! operations used to synchronize between threads. -//! This means it is undefined behavior to perform two concurrent accesses to the same location -//! from different threads unless both accesses only read from memory. -//! Notice that this explicitly includes `read_volatile` and `write_volatile`: -//! Volatile accesses cannot be used for inter-thread synchronization. -//! 5. The result of casting a reference to a pointer is valid for as long as the underlying -//! object is live and no reference (just raw pointers) is used to access the same memory. -//! That is, reference and pointer accesses cannot be interleaved. -//! -//! Kani is able to verify #1 and #2 today. -//! -//! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if -//! the address matches `NonNull::<()>::dangling()`. -//! The way Kani tracks provenance is not enough to check if the address was the result of a cast -//! from a non-zero integer literal. - -use crate::kani_intrinsic; -use crate::mem::private::Internal; -use std::mem::{align_of, size_of}; -use std::ptr::{DynMetadata, NonNull, Pointee}; - -/// Check if the pointer is valid for write access according to [crate::mem] conditions 1, 2 -/// and 3. -/// -/// Note this function also checks for pointer alignment. Use [self::can_write_unaligned] -/// if you don't want to fail for unaligned pointers. -/// -/// This function does not check if the value stored is valid for the given type. Use -/// [self::can_dereference] for that. -/// -/// This function will panic today if the pointer is not null, and it points to an unallocated or -/// deallocated memory location. This is an existing Kani limitation. -/// See for more details. -#[crate::unstable( - feature = "mem-predicates", - issue = 2690, - reason = "experimental memory predicate API" -)] -pub fn can_write(ptr: *mut T) -> bool -where - T: ?Sized, - ::Metadata: PtrProperties, -{ - // The interface takes a mutable pointer to improve readability of the signature. - // However, using constant pointer avoid unnecessary instrumentation, and it is as powerful. - // Hence, cast to `*const T`. - let ptr: *const T = ptr; - let (thin_ptr, metadata) = ptr.to_raw_parts(); - metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) -} - -/// Check if the pointer is valid for unaligned write access according to [crate::mem] conditions -/// 1, 2 and 3. -/// -/// Note this function succeeds for unaligned pointers. See [self::can_write] if you also -/// want to check pointer alignment. -/// -/// This function will panic today if the pointer is not null, and it points to an unallocated or -/// deallocated memory location. This is an existing Kani limitation. -/// See for more details. -#[crate::unstable( - feature = "mem-predicates", - issue = 2690, - reason = "experimental memory predicate API" -)] -pub fn can_write_unaligned(ptr: *const T) -> bool -where - T: ?Sized, - ::Metadata: PtrProperties, -{ - let (thin_ptr, metadata) = ptr.to_raw_parts(); - is_inbounds(&metadata, thin_ptr) -} - -/// Checks that pointer `ptr` point to a valid value of type `T`. -/// -/// For that, the pointer has to be a valid pointer according to [crate::mem] conditions 1, 2 -/// and 3, -/// and the value stored must respect the validity invariants for type `T`. -/// -/// TODO: Kani should automatically add those checks when a de-reference happens. -/// -/// -/// This function will panic today if the pointer is not null, and it points to an unallocated or -/// deallocated memory location. This is an existing Kani limitation. -/// See for more details. -#[crate::unstable( - feature = "mem-predicates", - issue = 2690, - reason = "experimental memory predicate API" -)] -#[allow(clippy::not_unsafe_ptr_arg_deref)] -pub fn can_dereference(ptr: *const T) -> bool -where - T: ?Sized, - ::Metadata: PtrProperties, -{ - let (thin_ptr, metadata) = ptr.to_raw_parts(); - // Need to assert `is_initialized` because non-determinism is used under the hood, so it does - // not make sense to use it inside assumption context. - metadata.is_ptr_aligned(thin_ptr, Internal) - && is_inbounds(&metadata, thin_ptr) - && assert_is_initialized(ptr) - && unsafe { has_valid_value(ptr) } -} - -/// Checks that pointer `ptr` point to a valid value of type `T`. -/// -/// For that, the pointer has to be a valid pointer according to [crate::mem] conditions 1, 2 -/// and 3, -/// and the value stored must respect the validity invariants for type `T`. -/// -/// Note this function succeeds for unaligned pointers. See [self::can_dereference] if you also -/// want to check pointer alignment. -/// -/// This function will panic today if the pointer is not null, and it points to an unallocated or -/// deallocated memory location. This is an existing Kani limitation. -/// See for more details. -#[crate::unstable( - feature = "mem-predicates", - issue = 2690, - reason = "experimental memory predicate API" -)] -#[allow(clippy::not_unsafe_ptr_arg_deref)] -pub fn can_read_unaligned(ptr: *const T) -> bool -where - T: ?Sized, - ::Metadata: PtrProperties, -{ - let (thin_ptr, metadata) = ptr.to_raw_parts(); - // Need to assert `is_initialized` because non-determinism is used under the hood, so it does - // not make sense to use it inside assumption context. - is_inbounds(&metadata, thin_ptr) - && assert_is_initialized(ptr) - && unsafe { has_valid_value(ptr) } -} - -/// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. -/// -/// This will panic if `data_ptr` points to an invalid `non_null` -fn is_inbounds(metadata: &M, data_ptr: *const ()) -> bool -where - M: PtrProperties, - T: ?Sized, -{ - let sz = metadata.pointee_size(Internal); - if sz == 0 { - true // ZST pointers are always valid including nullptr. - } else if data_ptr.is_null() { - false - } else { - // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be - // stubbed. - // We first assert that the data_ptr - crate::assert( - unsafe { is_allocated(data_ptr, 0) }, - "Kani does not support reasoning about pointer to unallocated memory", - ); - unsafe { is_allocated(data_ptr, sz) } - } -} - -mod private { - /// Define like this to restrict usage of PtrProperties functions outside Kani. - #[derive(Copy, Clone)] - pub struct Internal; -} - -/// Trait that allow us to extract information from pointers without de-referencing them. -#[doc(hidden)] -pub trait PtrProperties { - fn pointee_size(&self, _: Internal) -> usize; - - /// A pointer is aligned if its address is a multiple of its minimum alignment. - fn is_ptr_aligned(&self, ptr: *const (), internal: Internal) -> bool { - let min = self.min_alignment(internal); - ptr as usize % min == 0 - } - - fn min_alignment(&self, _: Internal) -> usize; - - fn dangling(&self, _: Internal) -> *const (); -} - -/// Get the information for sized types (they don't have metadata). -impl PtrProperties for () { - fn pointee_size(&self, _: Internal) -> usize { - size_of::() - } - - fn min_alignment(&self, _: Internal) -> usize { - align_of::() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::::dangling().as_ptr() as *const _ - } -} - -/// Get the information from the str metadata. -impl PtrProperties for usize { - #[inline(always)] - fn pointee_size(&self, _: Internal) -> usize { - *self - } - - /// String slices are a UTF-8 representation of characters that have the same layout as slices - /// of type [u8]. - /// - fn min_alignment(&self, _: Internal) -> usize { - align_of::() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::::dangling().as_ptr() as _ - } -} - -/// Get the information from the slice metadata. -impl PtrProperties<[T]> for usize { - fn pointee_size(&self, _: Internal) -> usize { - *self * size_of::() - } - - fn min_alignment(&self, _: Internal) -> usize { - align_of::() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::::dangling().as_ptr() as _ - } -} - -/// Get the information from the vtable. -impl PtrProperties for DynMetadata -where - T: ?Sized, -{ - fn pointee_size(&self, _: Internal) -> usize { - self.size_of() - } - - fn min_alignment(&self, _: Internal) -> usize { - self.align_of() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::<&T>::dangling().as_ptr() as _ - } -} - -/// Check if the pointer `_ptr` contains an allocated address of size equal or greater than `_size`. -/// -/// # Safety -/// -/// This function should only be called to ensure a pointer is always valid, i.e., in an assertion -/// context. -/// -/// I.e.: This function always returns `true` if the pointer is valid. -/// Otherwise, it returns non-det boolean. -#[rustc_diagnostic_item = "KaniIsAllocated"] -#[inline(never)] -unsafe fn is_allocated(_ptr: *const (), _size: usize) -> bool { - kani_intrinsic() -} - -/// Check if the value stored in the given location satisfies type `T` validity requirements. -/// -/// # Safety -/// -/// - Users have to ensure that the pointer is aligned the pointed memory is allocated. -#[rustc_diagnostic_item = "KaniValidValue"] -#[inline(never)] -unsafe fn has_valid_value(_ptr: *const T) -> bool { - kani_intrinsic() -} - -/// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. -#[rustc_diagnostic_item = "KaniIsInitialized"] -#[inline(never)] -pub(crate) fn is_initialized(_ptr: *const T) -> bool { - kani_intrinsic() -} - -/// A helper to assert `is_initialized` to use it as a part of other predicates. -fn assert_is_initialized(ptr: *const T) -> bool { - crate::check(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer"); - true -} - -/// Get the object ID of the given pointer. -#[doc(hidden)] -#[crate::unstable( - feature = "ghost-state", - issue = 3184, - reason = "experimental ghost state/shadow memory API" -)] -#[rustc_diagnostic_item = "KaniPointerObject"] -#[inline(never)] -pub fn pointer_object(_ptr: *const T) -> usize { - kani_intrinsic() -} - -/// Get the object offset of the given pointer. -#[doc(hidden)] -#[crate::unstable( - feature = "ghost-state", - issue = 3184, - reason = "experimental ghost state/shadow memory API" -)] -#[rustc_diagnostic_item = "KaniPointerOffset"] -#[inline(never)] -pub fn pointer_offset(_ptr: *const T) -> usize { - kani_intrinsic() -} - -#[cfg(test)] -mod tests { - use super::{can_dereference, can_write, PtrProperties}; - use crate::mem::private::Internal; - use std::fmt::Debug; - use std::intrinsics::size_of; - use std::mem::{align_of, align_of_val, size_of_val}; - use std::ptr; - use std::ptr::{NonNull, Pointee}; - - fn size_of_t(ptr: *const T) -> usize - where - T: ?Sized, - ::Metadata: PtrProperties, - { - let (_, metadata) = ptr.to_raw_parts(); - metadata.pointee_size(Internal) - } - - fn align_of_t(ptr: *const T) -> usize - where - T: ?Sized, - ::Metadata: PtrProperties, - { - let (_, metadata) = ptr.to_raw_parts(); - metadata.min_alignment(Internal) - } - - #[test] - fn test_size_of() { - assert_eq!(size_of_t("hi"), size_of_val("hi")); - assert_eq!(size_of_t(&0u8), size_of_val(&0u8)); - assert_eq!(size_of_t(&0u8 as *const dyn std::fmt::Display), size_of_val(&0u8)); - assert_eq!(size_of_t(&[0u8, 1u8] as &[u8]), size_of_val(&[0u8, 1u8])); - assert_eq!(size_of_t(&[] as &[u8]), size_of_val::<[u8; 0]>(&[])); - assert_eq!( - size_of_t(NonNull::::dangling().as_ptr() as *const dyn std::fmt::Display), - size_of::() - ); - } - - #[test] - fn test_alignment() { - assert_eq!(align_of_t("hi"), align_of_val("hi")); - assert_eq!(align_of_t(&0u8), align_of_val(&0u8)); - assert_eq!(align_of_t(&0u32 as *const dyn std::fmt::Display), align_of_val(&0u32)); - assert_eq!(align_of_t(&[0isize, 1isize] as &[isize]), align_of_val(&[0isize, 1isize])); - assert_eq!(align_of_t(&[] as &[u8]), align_of_val::<[u8; 0]>(&[])); - assert_eq!( - align_of_t(NonNull::::dangling().as_ptr() as *const dyn std::fmt::Display), - align_of::() - ); - } - - #[test] - pub fn test_empty_slice() { - let slice_ptr = Vec::::new().as_mut_slice() as *mut [char]; - assert!(can_write(slice_ptr)); - } - - #[test] - pub fn test_empty_str() { - let slice_ptr = String::new().as_mut_str() as *mut str; - assert!(can_write(slice_ptr)); - } - - #[test] - fn test_dangling_zst() { - test_dangling_of_zst::<()>(); - test_dangling_of_zst::<[(); 10]>(); - } - - fn test_dangling_of_zst() { - let dangling: *mut T = NonNull::::dangling().as_ptr(); - assert!(can_write(dangling)); - - let vec_ptr = Vec::::new().as_mut_ptr(); - assert!(can_write(vec_ptr)); - } - - #[test] - fn test_null_fat_ptr() { - assert!(!can_dereference(ptr::null::() as *const dyn Debug)); - } - - #[test] - fn test_null_char() { - assert!(!can_dereference(ptr::null::())); - } - - #[test] - fn test_null_mut() { - assert!(!can_write(ptr::null_mut::())); - } -} diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index ec12209f0e08..5388dcfb9427 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -10,7 +10,7 @@ publish = false description = "Define core constructs to use with Kani" [dependencies] -kani_macros = { path = "../kani_macros", features = ["no_core"] } +kani_macros = { path = "../kani_macros"} [features] no_core=["kani_macros/no_core"] diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index b7263816800a..6cbe98d30df2 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -52,6 +52,10 @@ macro_rules! kani_lib { pub use kani_core::*; kani_core::kani_intrinsics!(std); kani_core::generate_arbitrary!(std); + + pub mod mem { + kani_core::kani_mem!(std); + } }; } @@ -298,6 +302,7 @@ macro_rules! kani_intrinsics { loop {} } + #[doc(hidden)] pub mod internal { use crate::kani::Arbitrary; use core::ptr; diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 0b029ad53089..34cff4b17ad7 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -36,6 +36,7 @@ //! The way Kani tracks provenance is not enough to check if the address was the result of a cast //! from a non-zero integer literal. +#[allow(clippy::crate_in_macro_def)] #[macro_export] macro_rules! kani_mem { ($core:tt) => { @@ -56,12 +57,11 @@ macro_rules! kani_mem { /// This function will panic today if the pointer is not null, and it points to an unallocated or /// deallocated memory location. This is an existing Kani limitation. /// See for more details. - // TODO: Add this back! We might need to rename the attribute. - //#[crate::unstable( - // feature = "mem-predicates", - // issue = 2690, - // reason = "experimental memory predicate API" - //)] + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] pub fn can_write(ptr: *mut T) -> bool where T: ?Sized, @@ -84,12 +84,11 @@ macro_rules! kani_mem { /// This function will panic today if the pointer is not null, and it points to an unallocated or /// deallocated memory location. This is an existing Kani limitation. /// See for more details. - // TODO: Add this back! We might need to rename the attribute. - //#[crate::unstable( - // feature = "mem-predicates", - // issue = 2690, - // reason = "experimental memory predicate API" - //)] + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] pub fn can_write_unaligned(ptr: *const T) -> bool where T: ?Sized, @@ -111,11 +110,11 @@ macro_rules! kani_mem { /// This function will panic today if the pointer is not null, and it points to an unallocated or /// deallocated memory location. This is an existing Kani limitation. /// See for more details. - //#[crate::unstable( - // feature = "mem-predicates", - // issue = 2690, - // reason = "experimental memory predicate API" - //)] + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] #[allow(clippy::not_unsafe_ptr_arg_deref)] pub fn can_dereference(ptr: *const T) -> bool where @@ -143,12 +142,11 @@ macro_rules! kani_mem { /// This function will panic today if the pointer is not null, and it points to an unallocated or /// deallocated memory location. This is an existing Kani limitation. /// See for more details. - // TODO: Add this back! We might need to rename the attribute. - //#[crate::unstable( - // feature = "mem-predicates", - // issue = 2690, - // reason = "experimental memory predicate API" - //)] + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] #[allow(clippy::not_unsafe_ptr_arg_deref)] pub fn can_read_unaligned(ptr: *const T) -> bool where @@ -180,7 +178,7 @@ macro_rules! kani_mem { // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be // stubbed. // We first assert that the data_ptr - assert!( + super::assert( unsafe { is_allocated(data_ptr, 0) }, "Kani does not support reasoning about pointer to unallocated memory", ); @@ -320,30 +318,28 @@ macro_rules! kani_mem { } /// Get the object ID of the given pointer. - // TODO: Add this back later, as there is no unstable attribute here. - // #[doc(hidden)] - // #[crate::unstable( - // feature = "ghost-state", - // issue = 3184, - // reason = "experimental ghost state/shadow memory API" - // )] + #[doc(hidden)] + #[crate::kani::unstable_feature( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" + )] #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] - pub(crate) fn pointer_object(_ptr: *const T) -> usize { + pub fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } /// Get the object offset of the given pointer. - // TODO: Add this back later, as there is no unstable attribute here. - // #[doc(hidden)] - // #[crate::unstable( - // feature = "ghost-state", - // issue = 3184, - // reason = "experimental ghost state/shadow memory API" - // )] + #[doc(hidden)] + #[crate::kani::unstable_feature( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" + )] #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] - pub(crate) fn pointer_offset(_ptr: *const T) -> usize { + pub fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } }; diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 5917c322729e..42eb37a56584 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -22,4 +22,4 @@ syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-tra rustc_private = true [features] -no_core = [] \ No newline at end of file +no_core = [] diff --git a/tests/expected/function-contract/modifies/check_invalid_modifies.expected b/tests/expected/function-contract/modifies/check_invalid_modifies.expected index 660430705aa2..c0ce839c3aae 100644 --- a/tests/expected/function-contract/modifies/check_invalid_modifies.expected +++ b/tests/expected/function-contract/modifies/check_invalid_modifies.expected @@ -1,7 +1,2 @@ -error: `&str` doesn't implement `kani::Arbitrary`\ - -->\ -| -| T::any() -| ^^^^^^^^ -| +error: `&str` doesn't implement `kani::Arbitrary`. = help: All objects in the modifies clause must implement the Arbitrary. The return type must also implement the Arbitrary trait if you are checking recursion or using verified stub. diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index 1b62781adaaf..4014a0723029 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -1,5 +1,4 @@ Checking harness pre_condition::harness_invalid_ptr... -Failed Checks: Kani does not support reasoning about pointer to unallocated memory VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) Checking harness pre_condition::harness_stack_ptr... diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index 3a24bf15241e..6a95c667b71b 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -51,7 +51,7 @@ cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs echo "[TEST] Run kani verify-std" export RUST_BACKTRACE=1 -kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing +kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing -Z mem-predicates # Cleanup rm -r ${TMP_DIR} diff --git a/tests/ui/derive-arbitrary/non_arbitrary_param/expected b/tests/ui/derive-arbitrary/non_arbitrary_param/expected index 55f12678cf9a..68e3710d6dcb 100644 --- a/tests/ui/derive-arbitrary/non_arbitrary_param/expected +++ b/tests/ui/derive-arbitrary/non_arbitrary_param/expected @@ -1,4 +1,4 @@ error[E0277]: the trait bound `Void: kani::Arbitrary` is not satisfied - |\ -14 | let _wrapper: Wrapper = kani::any();\ - | ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`, which is required by `Wrapper: kani::Arbitrary`\ +|\ +| let _wrapper: Wrapper = kani::any();\ +| ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`, which is required by `Wrapper: kani::Arbitrary`\ From c515d662fff970ae4e5f50dfffa01ab77375bf34 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Aug 2024 18:05:08 +0200 Subject: [PATCH 04/10] Toolchain update: avoid Javascript interpreting git log (#3421) git log entries may themselves use backticks, which prematurely ended the string (and then caused Javascript syntax errors). Avoid this problem by using the environment variable rather than having Javascript see the string contents (of that environment variable). 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: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- .github/workflows/toolchain-upgrade.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml index b11f4e6b591a..76c3a5484414 100644 --- a/.github/workflows/toolchain-upgrade.yml +++ b/.github/workflows/toolchain-upgrade.yml @@ -64,7 +64,7 @@ jobs: https://github.com/rust-lang/rust/commit/${{ env.next_toolchain_hash }}. The log for this commit range is: - ${{ env.git_log }}` + ` + process.env.git_log }) - name: Create Issue From fdce213672724675d1f76f05ede100172ae3ff9f Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Wed, 7 Aug 2024 13:09:48 -0400 Subject: [PATCH 05/10] Automatic toolchain upgrade to nightly-2024-08-07 (#3423) Update Rust toolchain from nightly-2024-08-06 to nightly-2024-08-07 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com> --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 23a3f2bc99eb..e3b6229d73c6 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-08-06" +channel = "nightly-2024-08-07" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 3fb3a73d6d563e92eb447b32ec963ea77853ec00 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 7 Aug 2024 13:34:46 -0700 Subject: [PATCH 06/10] Stabilize pointer-to-reference cast validity checks (#3426) This PR stabilizes pointer-to-reference cast validity checks, so that they are run by default. Resolves #3425 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/workflows/verify-std-check.yml | 4 ++-- kani-compiler/src/args.rs | 3 --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 21 +++++++------------ kani-driver/src/call_single_file.rs | 4 ---- kani_metadata/src/unstable.rs | 2 -- tests/expected/dangling-ptr-println/main.rs | 1 - .../ptr_to_ref_cast/ptr_to_ref_cast.rs | 1 - tests/std-checks/core/Cargo.toml | 2 +- 8 files changed, 11 insertions(+), 27 deletions(-) diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml index 1bad09cd3c6d..6935b2bb4073 100644 --- a/.github/workflows/verify-std-check.yml +++ b/.github/workflows/verify-std-check.yml @@ -59,7 +59,7 @@ jobs: continue-on-error: true run: | kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ - -Z mem-predicates -Z ptr-to-ref-cast-checks + -Z mem-predicates # If the head failed, check if it's a new failure. - name: Checkout base @@ -77,7 +77,7 @@ jobs: continue-on-error: true run: | kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ - -Z mem-predicates -Z ptr-to-ref-cast-checks + -Z mem-predicates - name: Compare PR results if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 3efc5c0f4f61..3fa74b0e5aba 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -82,9 +82,6 @@ pub enum ExtraChecks { /// Check that produced values are valid except for uninitialized values. /// See https://github.com/model-checking/kani/issues/920. Validity, - /// Check pointer validity when casting pointers to references. - /// See https://github.com/model-checking/kani/issues/2975. - PtrToRefCast, /// Check for using uninitialized memory. Uninit, } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 4883c608f482..a30eeb7639ce 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::args::ExtraChecks; use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace; use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::codegen::PropertyClass; @@ -730,18 +729,14 @@ impl<'tcx> GotocCtx<'tcx> { Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc), Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => { let place_ref = self.codegen_place_ref_stable(&p, loc); - if self.queries.args().ub_check.contains(&ExtraChecks::PtrToRefCast) { - let place_ref_type = place_ref.typ().clone(); - match self.codegen_raw_ptr_deref_validity_check(&p, &loc) { - Some(ptr_validity_check_expr) => Expr::statement_expression( - vec![ptr_validity_check_expr, place_ref.as_stmt(loc)], - place_ref_type, - loc, - ), - None => place_ref, - } - } else { - place_ref + let place_ref_type = place_ref.typ().clone(); + match self.codegen_raw_ptr_deref_validity_check(&p, &loc) { + Some(ptr_validity_check_expr) => Expr::statement_expression( + vec![ptr_validity_check_expr, place_ref.as_stmt(loc)], + place_ref_type, + loc, + ), + None => place_ref, } } Rvalue::Len(p) => self.codegen_rvalue_len(p, loc), diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index bbeb5bfa417d..4b30fe877507 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -135,10 +135,6 @@ impl KaniSession { flags.push("--ub-check=validity".into()) } - if self.args.common_args.unstable_features.contains(UnstableFeature::PtrToRefCastChecks) { - flags.push("--ub-check=ptr_to_ref_cast".into()) - } - if self.args.common_args.unstable_features.contains(UnstableFeature::UninitChecks) { // Automatically enable shadow memory, since the version of uninitialized memory checks // without non-determinism depends on it. diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 68e4fba28819..120ab0a9e55c 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -89,8 +89,6 @@ pub enum UnstableFeature { ValidValueChecks, /// Ghost state and shadow memory APIs. GhostState, - /// Automatically check that pointers are valid when casting them to references. - PtrToRefCastChecks, /// Automatically check that uninitialized memory is not used. UninitChecks, /// Enable an unstable option or subcommand. diff --git a/tests/expected/dangling-ptr-println/main.rs b/tests/expected/dangling-ptr-println/main.rs index a83afa6f8313..04328c92cb52 100644 --- a/tests/expected/dangling-ptr-println/main.rs +++ b/tests/expected/dangling-ptr-println/main.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ptr-to-ref-cast-checks //! These tests check that Kani correctly detects dangling pointer dereference inside println macro. //! Related issue: . diff --git a/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs b/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs index 3b713a34d967..e04ac9cd3169 100644 --- a/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs +++ b/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ptr-to-ref-cast-checks //! This test case checks that raw pointer validity is checked before converting it to a reference, e.g., &(*ptr). diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml index f6e1645c3a39..9cacaa1368e3 100644 --- a/tests/std-checks/core/Cargo.toml +++ b/tests/std-checks/core/Cargo.toml @@ -7,7 +7,7 @@ edition = "2021" description = "This crate contains contracts and harnesses for core library" [package.metadata.kani] -unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true } +unstable = { function-contracts = true, mem-predicates = true } [package.metadata.kani.flags] output-format = "terse" From 2a3538dc4a63bd52677738da017ec019caf5d71b Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Wed, 7 Aug 2024 18:35:35 -0400 Subject: [PATCH 07/10] Update depencencies (#3428) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Signed-off-by: Felipe R. Monteiro --- Cargo.lock | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 7d7580e3b742..52250d2468c8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -991,9 +991,9 @@ dependencies = [ [[package]] name = "serde_test" -version = "1.0.176" +version = "1.0.177" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a2f49ace1498612d14f7e0b8245519584db8299541dfe31a06374a828d620ab" +checksum = "7f901ee573cab6b3060453d2d5f0bae4e6d628c23c0a962ff9b5f1d7c8d4f1ed" dependencies = [ "serde", ] @@ -1098,15 +1098,15 @@ dependencies = [ [[package]] name = "tempfile" -version = "3.11.0" +version = "3.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8fcd239983515c23a32fb82099f97d0b11b8c72f654ed659363a95c3dad7a53" +checksum = "04cbcdd0c794ebb0d4cf35e88edd2f7d2c4c3e9a5a6dab322839b321c6a87a64" dependencies = [ "cfg-if", "fastrand", "once_cell", "rustix", - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] From 7a6f1a445066c7c6720cd0583cf1cf56f6646955 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 8 Aug 2024 21:07:32 -0400 Subject: [PATCH 08/10] Bump Kani version to 0.54.0 (#3430) ## 0.54.0 ### Major Changes * We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts. * We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros. * We enabled support for concrete playback for harness that contains stubs or function contracts. * We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs. ### Breaking Changes * The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default. ## What's Changed * Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in https://github.com/model-checking/kani/pull/3332 * Fix visibility of some Kani intrinsics by @artemagvanian in https://github.com/model-checking/kani/pull/3323 * Function Contracts: Modify Slices by @pi314mm in https://github.com/model-checking/kani/pull/3295 * Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3344 * Add support for global transformations by @artemagvanian in https://github.com/model-checking/kani/pull/3348 * Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in https://github.com/model-checking/kani/pull/3283 * Fix contract handling of promoted constants and constant static by @celinval in https://github.com/model-checking/kani/pull/3305 * Bump CBMC Viewer to 3.9 by @tautschnig in https://github.com/model-checking/kani/pull/3373 * Update to CBMC version 6.1.1 by @tautschnig in https://github.com/model-checking/kani/pull/2995 * Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in https://github.com/model-checking/kani/pull/3270 * Enable concrete playback for contract and stubs by @celinval in https://github.com/model-checking/kani/pull/3389 * Add code scanner tool by @celinval in https://github.com/model-checking/kani/pull/3120 * Enable contracts in associated functions by @celinval in https://github.com/model-checking/kani/pull/3363 * Enable log2*, log10* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3001 * Enable powif* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/2999 * Enable fma* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3002 * Enable sqrt* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3000 * Remove assigns clause for ZST pointers by @carolynzech in https://github.com/model-checking/kani/pull/3417 * Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in https://github.com/model-checking/kani/pull/3374 * Unify kani library and kani core logic by @jaisnan in https://github.com/model-checking/kani/pull/3333 * Stabilize pointer-to-reference cast validity checks by @artemagvanian in https://github.com/model-checking/kani/pull/3426 * Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri ## New Contributors * @carolynzech made their first contribution in https://github.com/model-checking/kani/pull/3387 **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Signed-off-by: Felipe R. Monteiro --- CHANGELOG.md | 40 ++++++++++++++++++++++++++++++++++ Cargo.lock | 20 ++++++++--------- 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_core/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 12 files changed, 60 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 47ae290853a3..d36def1a45f1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,46 @@ 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.54.0] + +### Major Changes +* We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts. +* We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros. +* We enabled support for concrete playback for harness that contains stubs or function contracts. +* We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs. + +### Breaking Changes +* The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default. + +## What's Changed +* Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in https://github.com/model-checking/kani/pull/3332 +* Fix visibility of some Kani intrinsics by @artemagvanian in https://github.com/model-checking/kani/pull/3323 +* Function Contracts: Modify Slices by @pi314mm in https://github.com/model-checking/kani/pull/3295 +* Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3344 +* Add support for global transformations by @artemagvanian in https://github.com/model-checking/kani/pull/3348 +* Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in https://github.com/model-checking/kani/pull/3283 +* Fix contract handling of promoted constants and constant static by @celinval in https://github.com/model-checking/kani/pull/3305 +* Bump CBMC Viewer to 3.9 by @tautschnig in https://github.com/model-checking/kani/pull/3373 +* Update to CBMC version 6.1.1 by @tautschnig in https://github.com/model-checking/kani/pull/2995 +* Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in https://github.com/model-checking/kani/pull/3270 +* Enable concrete playback for contract and stubs by @celinval in https://github.com/model-checking/kani/pull/3389 +* Add code scanner tool by @celinval in https://github.com/model-checking/kani/pull/3120 +* Enable contracts in associated functions by @celinval in https://github.com/model-checking/kani/pull/3363 +* Enable log2*, log10* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3001 +* Enable powif* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/2999 +* Enable fma* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3002 +* Enable sqrt* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3000 +* Remove assigns clause for ZST pointers by @carolynzech in https://github.com/model-checking/kani/pull/3417 +* Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in https://github.com/model-checking/kani/pull/3374 +* Unify kani library and kani core logic by @jaisnan in https://github.com/model-checking/kani/pull/3333 +* Stabilize pointer-to-reference cast validity checks by @artemagvanian in https://github.com/model-checking/kani/pull/3426 +* Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri + +## New Contributors +* @carolynzech made their first contribution in https://github.com/model-checking/kani/pull/3387 + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0 + ## [0.53.0] ### Major Changes diff --git a/Cargo.lock b/Cargo.lock index 52250d2468c8..12c28c49c1bf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -92,7 +92,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" [[package]] name = "build-kani" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "cargo_metadata", @@ -234,7 +234,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.53.0" +version = "0.54.0" dependencies = [ "lazy_static", "linear-map", @@ -432,7 +432,7 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "kani" -version = "0.53.0" +version = "0.54.0" dependencies = [ "kani_core", "kani_macros", @@ -440,7 +440,7 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.53.0" +version = "0.54.0" dependencies = [ "clap", "cprover_bindings", @@ -461,7 +461,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "cargo_metadata", @@ -489,7 +489,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "home", @@ -498,14 +498,14 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.53.0" +version = "0.54.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.53.0" +version = "0.54.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -515,7 +515,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.53.0" +version = "0.54.0" dependencies = [ "clap", "cprover_bindings", @@ -1034,7 +1034,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" [[package]] name = "std" -version = "0.53.0" +version = "0.54.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index 68b5bcc20ff3..f2301983fcb4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.53.0" +version = "0.54.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 aced9e5b9b65..c53ffb207fcf 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.53.0" +version = "0.54.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 23389c156302..24ed00f54338 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.53.0" +version = "0.54.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index d58d686d7d43..c57ec8e8e2f2 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.53.0" +version = "0.54.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 816752a58e03..de91900d6d9c 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.53.0" +version = "0.54.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 1fba7875672a..7d7ced8ee0b7 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.53.0" +version = "0.54.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index 5388dcfb9427..8928992c3f16 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.53.0" +version = "0.54.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 42eb37a56584..475e2978df91 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.53.0" +version = "0.54.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index ae70767f6781..9f0d09b0d7bb 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.53.0" +version = "0.54.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 7c8e6eef122a..cd2985e4ad68 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.53.0" +version = "0.54.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" From bec5fd1a2298f7f455c559ddfc938fd7a24e9b4d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 9 Aug 2024 16:37:57 +0200 Subject: [PATCH 09/10] Update CBMC build instructions for Amazon Linux 2 (#3431) The default compiler on Amazon Linux 2 is GCC 7, which is not sufficiently recent for building CBMC v6+. Install and use GCC 10, adjust warnings to cope with the flex version provided by Amazon Linux 2, and handle the non-default std::filesystem support. Furthermore, apply a workaround until https://github.com/diffblue/cbmc/issues/8357 has been fixed on the CBMC side. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- scripts/setup/al2/install_cbmc.sh | 79 +++++++++++++++++++++++++++++-- scripts/setup/al2/install_deps.sh | 1 + 2 files changed, 77 insertions(+), 3 deletions(-) diff --git a/scripts/setup/al2/install_cbmc.sh b/scripts/setup/al2/install_cbmc.sh index 34abcc52db93..de4b5215e083 100755 --- a/scripts/setup/al2/install_cbmc.sh +++ b/scripts/setup/al2/install_cbmc.sh @@ -21,10 +21,83 @@ git clone \ pushd "${WORK_DIR}" -mkdir build -git submodule update --init +# apply workaround for https://github.com/diffblue/cbmc/issues/8357 until it is +# properly fixed in CBMC +cat > varargs.patch << "EOF" +--- a/src/ansi-c/library/stdio.c ++++ b/src/ansi-c/library/stdio.c +@@ -1135,7 +1135,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg) -cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" + (void)*format; + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) < +- __CPROVER_OBJECT_SIZE(arg)) ++ __CPROVER_OBJECT_SIZE(*(void **)&arg)) + { + void *a = va_arg(arg, void *); + __CPROVER_havoc_object(a); +@@ -1233,7 +1233,7 @@ int __stdio_common_vfscanf( + + (void)*format; + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) < +- __CPROVER_OBJECT_SIZE(args)) ++ __CPROVER_OBJECT_SIZE(*(void **)&args)) + { + void *a = va_arg(args, void *); + __CPROVER_havoc_object(a); +@@ -1312,7 +1312,7 @@ __CPROVER_HIDE:; + (void)*s; + (void)*format; + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) < +- __CPROVER_OBJECT_SIZE(arg)) ++ __CPROVER_OBJECT_SIZE(*(void **)&arg)) + { + void *a = va_arg(arg, void *); + __CPROVER_havoc_object(a); +@@ -1388,7 +1388,7 @@ int __stdio_common_vsscanf( + (void)*s; + (void)*format; + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) < +- __CPROVER_OBJECT_SIZE(args)) ++ __CPROVER_OBJECT_SIZE(*(void **)&args)) + { + void *a = va_arg(args, void *); + __CPROVER_havoc_object(a); +@@ -1774,12 +1774,12 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap) + (void)*fmt; + + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) < +- __CPROVER_OBJECT_SIZE(ap)) ++ __CPROVER_OBJECT_SIZE(*(void **)&ap)) + + { + (void)va_arg(ap, int); + __CPROVER_precondition( +- __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap), ++ __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap), + "vsnprintf object overlap"); + } + +@@ -1822,12 +1822,12 @@ int __builtin___vsnprintf_chk( + (void)*fmt; + + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) < +- __CPROVER_OBJECT_SIZE(ap)) ++ __CPROVER_OBJECT_SIZE(*(void **)&ap)) + + { + (void)va_arg(ap, int); + __CPROVER_precondition( +- __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap), ++ __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap), + "vsnprintf object overlap"); + } + +EOF + +cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \ + -DCMAKE_C_COMPILER=gcc10-cc -DCMAKE_CXX_COMPILER=gcc10-c++ \ + -DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \ + -DCMAKE_CXX_FLAGS=-Wno-error=register cmake3 --build build -- -j$(nproc) sudo make -C build install diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh index 0010aa58bab4..ce901ab8afa5 100755 --- a/scripts/setup/al2/install_deps.sh +++ b/scripts/setup/al2/install_deps.sh @@ -11,6 +11,7 @@ set -eu DEPS=( cmake cmake3 + gcc10-c++ git openssl-devel python3-pip From 6553afa4dc854478da1570517f522776ae0601e2 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 9 Aug 2024 11:47:40 -0700 Subject: [PATCH 10/10] Handle intrinsics systematically (#3422) Since compiler intrinsics are handled both in codegen and instrumentation, it would make sense to have a single source of truth with regard to which intrinsics we support and update it systematically. This PR introduces an `Intrinsic` enum, which allows to parse intrinsic name into one of the predefined variants we support or a catch-all `Unsupported` variant. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../codegen/intrinsic.rs | 414 ++++----- kani-compiler/src/intrinsics.rs | 798 ++++++++++++++++++ .../points_to/points_to_analysis.rs | 411 +++++---- .../delayed_ub/initial_target_visitor.rs | 37 +- .../check_uninit/ptr_uninit/uninit_visitor.rs | 378 ++++----- kani-compiler/src/main.rs | 1 + 6 files changed, 1393 insertions(+), 646 deletions(-) create mode 100644 kani-compiler/src/intrinsics.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index c4d5396f1fe8..421d79e943c4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -5,6 +5,7 @@ use super::typ; use super::{bb_label, PropertyClass}; use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::{utils, GotocCtx}; +use crate::intrinsics::Intrinsic; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{ ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type, @@ -114,7 +115,7 @@ impl<'tcx> GotocCtx<'tcx> { span: Span, ) -> Stmt { let intrinsic_name = instance.intrinsic_name().unwrap(); - let intrinsic = intrinsic_name.as_str(); + let intrinsic_str = intrinsic_name.as_str(); let loc = self.codegen_span_stable(span); debug!(?instance, "codegen_intrinsic"); debug!(?fargs, "codegen_intrinsic"); @@ -163,7 +164,7 @@ impl<'tcx> GotocCtx<'tcx> { let div_overflow_check = self.codegen_assert_assume( div_does_not_overflow, PropertyClass::ArithmeticOverflow, - format!("attempt to compute {} which would overflow", intrinsic).as_str(), + format!("attempt to compute {} which would overflow", intrinsic_str).as_str(), loc, ); let res = a.$f(b); @@ -257,7 +258,7 @@ impl<'tcx> GotocCtx<'tcx> { macro_rules! codegen_atomic_binop { ($op: ident) => {{ let loc = self.codegen_span_stable(span); - self.store_concurrent_construct(intrinsic, loc); + self.store_concurrent_construct(intrinsic_str, loc); let var1_ref = fargs.remove(0); let var1 = var1_ref.dereference(); let (tmp, decl_stmt) = @@ -280,7 +281,7 @@ impl<'tcx> GotocCtx<'tcx> { macro_rules! unstable_codegen { ($($tt:tt)*) => {{ let expr = self.codegen_unimplemented_expr( - &format!("'{}' intrinsic", intrinsic), + &format!("'{}' intrinsic", intrinsic_str), cbmc_ret_ty, loc, "https://github.com/model-checking/kani/issues/new/choose", @@ -289,342 +290,273 @@ impl<'tcx> GotocCtx<'tcx> { }}; } - if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") { - assert!(fargs.len() == 3, "`simd_shuffle` had unexpected arguments {fargs:?}"); - let n: u64 = self.simd_shuffle_length(stripped, farg_types, span); - return self.codegen_intrinsic_simd_shuffle(fargs, place, farg_types, ret_ty, n, span); - } + let intrinsic = Intrinsic::from_instance(&instance); match intrinsic { - "add_with_overflow" => { + Intrinsic::AddWithOverflow => { self.codegen_op_with_overflow(BinaryOperator::OverflowResultPlus, fargs, place, loc) } - "arith_offset" => self.codegen_offset(intrinsic, instance, fargs, place, loc), - "assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span), - "assert_mem_uninitialized_valid" => { - self.codegen_assert_intrinsic(instance, intrinsic, span) + Intrinsic::ArithOffset => { + self.codegen_offset(intrinsic_str, instance, fargs, place, loc) + } + Intrinsic::AssertInhabited => { + self.codegen_assert_intrinsic(instance, intrinsic_str, span) + } + Intrinsic::AssertMemUninitializedValid => { + self.codegen_assert_intrinsic(instance, intrinsic_str, span) + } + Intrinsic::AssertZeroValid => { + self.codegen_assert_intrinsic(instance, intrinsic_str, span) } - "assert_zero_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span), // https://doc.rust-lang.org/core/intrinsics/fn.assume.html // Informs the optimizer that a condition is always true. // If the condition is false, the behavior is undefined. - "assume" => self.codegen_assert_assume( + Intrinsic::Assume => self.codegen_assert_assume( fargs.remove(0).cast_to(Type::bool()), PropertyClass::Assume, "assumption failed", loc, ), - "atomic_and_seqcst" => codegen_atomic_binop!(bitand), - "atomic_and_acquire" => codegen_atomic_binop!(bitand), - "atomic_and_acqrel" => codegen_atomic_binop!(bitand), - "atomic_and_release" => codegen_atomic_binop!(bitand), - "atomic_and_relaxed" => codegen_atomic_binop!(bitand), - name if name.starts_with("atomic_cxchg") => { - self.codegen_atomic_cxchg(intrinsic, fargs, place, loc) + Intrinsic::AtomicAnd(_) => codegen_atomic_binop!(bitand), + Intrinsic::AtomicCxchg(_) | Intrinsic::AtomicCxchgWeak(_) => { + self.codegen_atomic_cxchg(intrinsic_str, fargs, place, loc) } - "atomic_fence_seqcst" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_fence_acquire" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_fence_acqrel" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_fence_release" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_load_seqcst" => self.codegen_atomic_load(intrinsic, fargs, place, loc), - "atomic_load_acquire" => self.codegen_atomic_load(intrinsic, fargs, place, loc), - "atomic_load_relaxed" => self.codegen_atomic_load(intrinsic, fargs, place, loc), - "atomic_load_unordered" => self.codegen_atomic_load(intrinsic, fargs, place, loc), - "atomic_max_seqcst" => codegen_atomic_binop!(max), - "atomic_max_acquire" => codegen_atomic_binop!(max), - "atomic_max_acqrel" => codegen_atomic_binop!(max), - "atomic_max_release" => codegen_atomic_binop!(max), - "atomic_max_relaxed" => codegen_atomic_binop!(max), - "atomic_min_seqcst" => codegen_atomic_binop!(min), - "atomic_min_acquire" => codegen_atomic_binop!(min), - "atomic_min_acqrel" => codegen_atomic_binop!(min), - "atomic_min_release" => codegen_atomic_binop!(min), - "atomic_min_relaxed" => codegen_atomic_binop!(min), - "atomic_nand_seqcst" => codegen_atomic_binop!(bitnand), - "atomic_nand_acquire" => codegen_atomic_binop!(bitnand), - "atomic_nand_acqrel" => codegen_atomic_binop!(bitnand), - "atomic_nand_release" => codegen_atomic_binop!(bitnand), - "atomic_nand_relaxed" => codegen_atomic_binop!(bitnand), - "atomic_or_seqcst" => codegen_atomic_binop!(bitor), - "atomic_or_acquire" => codegen_atomic_binop!(bitor), - "atomic_or_acqrel" => codegen_atomic_binop!(bitor), - "atomic_or_release" => codegen_atomic_binop!(bitor), - "atomic_or_relaxed" => codegen_atomic_binop!(bitor), - "atomic_singlethreadfence_seqcst" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_singlethreadfence_acquire" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_singlethreadfence_acqrel" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_singlethreadfence_release" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_store_seqcst" => self.codegen_atomic_store(intrinsic, fargs, place, loc), - "atomic_store_release" => self.codegen_atomic_store(intrinsic, fargs, place, loc), - "atomic_store_relaxed" => self.codegen_atomic_store(intrinsic, fargs, place, loc), - "atomic_store_unordered" => self.codegen_atomic_store(intrinsic, fargs, place, loc), - "atomic_umax_seqcst" => codegen_atomic_binop!(max), - "atomic_umax_acquire" => codegen_atomic_binop!(max), - "atomic_umax_acqrel" => codegen_atomic_binop!(max), - "atomic_umax_release" => codegen_atomic_binop!(max), - "atomic_umax_relaxed" => codegen_atomic_binop!(max), - "atomic_umin_seqcst" => codegen_atomic_binop!(min), - "atomic_umin_acquire" => codegen_atomic_binop!(min), - "atomic_umin_acqrel" => codegen_atomic_binop!(min), - "atomic_umin_release" => codegen_atomic_binop!(min), - "atomic_umin_relaxed" => codegen_atomic_binop!(min), - "atomic_xadd_seqcst" => codegen_atomic_binop!(plus), - "atomic_xadd_acquire" => codegen_atomic_binop!(plus), - "atomic_xadd_acqrel" => codegen_atomic_binop!(plus), - "atomic_xadd_release" => codegen_atomic_binop!(plus), - "atomic_xadd_relaxed" => codegen_atomic_binop!(plus), - "atomic_xchg_seqcst" => self.codegen_atomic_store(intrinsic, fargs, place, loc), - "atomic_xchg_acquire" => self.codegen_atomic_store(intrinsic, fargs, place, loc), - "atomic_xchg_acqrel" => self.codegen_atomic_store(intrinsic, fargs, place, loc), - "atomic_xchg_release" => self.codegen_atomic_store(intrinsic, fargs, place, loc), - "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, place, loc), - "atomic_xor_seqcst" => codegen_atomic_binop!(bitxor), - "atomic_xor_acquire" => codegen_atomic_binop!(bitxor), - "atomic_xor_acqrel" => codegen_atomic_binop!(bitxor), - "atomic_xor_release" => codegen_atomic_binop!(bitxor), - "atomic_xor_relaxed" => codegen_atomic_binop!(bitxor), - "atomic_xsub_seqcst" => codegen_atomic_binop!(sub), - "atomic_xsub_acquire" => codegen_atomic_binop!(sub), - "atomic_xsub_acqrel" => codegen_atomic_binop!(sub), - "atomic_xsub_release" => codegen_atomic_binop!(sub), - "atomic_xsub_relaxed" => codegen_atomic_binop!(sub), - "bitreverse" => { + + Intrinsic::AtomicFence(_) => self.codegen_atomic_noop(intrinsic_str, loc), + Intrinsic::AtomicLoad(_) => self.codegen_atomic_load(intrinsic_str, fargs, place, loc), + Intrinsic::AtomicMax(_) => codegen_atomic_binop!(max), + Intrinsic::AtomicMin(_) => codegen_atomic_binop!(min), + Intrinsic::AtomicNand(_) => codegen_atomic_binop!(bitnand), + Intrinsic::AtomicOr(_) => codegen_atomic_binop!(bitor), + Intrinsic::AtomicSingleThreadFence(_) => self.codegen_atomic_noop(intrinsic_str, loc), + Intrinsic::AtomicStore(_) => { + self.codegen_atomic_store(intrinsic_str, fargs, place, loc) + } + Intrinsic::AtomicUmax(_) => codegen_atomic_binop!(max), + Intrinsic::AtomicUmin(_) => codegen_atomic_binop!(min), + Intrinsic::AtomicXadd(_) => codegen_atomic_binop!(plus), + Intrinsic::AtomicXchg(_) => self.codegen_atomic_store(intrinsic_str, fargs, place, loc), + Intrinsic::AtomicXor(_) => codegen_atomic_binop!(bitxor), + Intrinsic::AtomicXsub(_) => codegen_atomic_binop!(sub), + Intrinsic::Bitreverse => { self.codegen_expr_to_place_stable(place, fargs.remove(0).bitreverse(), loc) } // black_box is an identity function that hints to the compiler // to be maximally pessimistic to limit optimizations - "black_box" => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc), - "breakpoint" => Stmt::skip(loc), - "bswap" => self.codegen_expr_to_place_stable(place, fargs.remove(0).bswap(), loc), - "caller_location" => self.codegen_unimplemented_stmt( - intrinsic, - loc, - "https://github.com/model-checking/kani/issues/374", - ), - "catch_unwind" => self.codegen_unimplemented_stmt( - intrinsic, - loc, - "https://github.com/model-checking/kani/issues/267", - ), - "ceilf32" => codegen_simple_intrinsic!(Ceilf), - "ceilf64" => codegen_simple_intrinsic!(Ceil), - "compare_bytes" => self.codegen_compare_bytes(fargs, place, loc), - "copy" => self.codegen_copy(intrinsic, false, fargs, farg_types, Some(place), loc), - "copy_nonoverlapping" => unreachable!( - "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`" - ), - "copysignf32" => codegen_simple_intrinsic!(Copysignf), - "copysignf64" => codegen_simple_intrinsic!(Copysign), - "cosf32" => codegen_simple_intrinsic!(Cosf), - "cosf64" => codegen_simple_intrinsic!(Cos), - "ctlz" => codegen_count_intrinsic!(ctlz, true), - "ctlz_nonzero" => codegen_count_intrinsic!(ctlz, false), - "ctpop" => self.codegen_ctpop(place, span, fargs.remove(0), farg_types[0]), - "cttz" => codegen_count_intrinsic!(cttz, true), - "cttz_nonzero" => codegen_count_intrinsic!(cttz, false), - "discriminant_value" => { + Intrinsic::BlackBox => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc), + Intrinsic::Breakpoint => Stmt::skip(loc), + Intrinsic::Bswap => { + self.codegen_expr_to_place_stable(place, fargs.remove(0).bswap(), loc) + } + Intrinsic::CeilF32 => codegen_simple_intrinsic!(Ceilf), + Intrinsic::CeilF64 => codegen_simple_intrinsic!(Ceil), + Intrinsic::CompareBytes => self.codegen_compare_bytes(fargs, place, loc), + Intrinsic::Copy => { + self.codegen_copy(intrinsic_str, false, fargs, farg_types, Some(place), loc) + } + Intrinsic::CopySignF32 => codegen_simple_intrinsic!(Copysignf), + Intrinsic::CopySignF64 => codegen_simple_intrinsic!(Copysign), + Intrinsic::CosF32 => codegen_simple_intrinsic!(Cosf), + Intrinsic::CosF64 => codegen_simple_intrinsic!(Cos), + Intrinsic::Ctlz => codegen_count_intrinsic!(ctlz, true), + Intrinsic::CtlzNonZero => codegen_count_intrinsic!(ctlz, false), + Intrinsic::Ctpop => self.codegen_ctpop(place, span, fargs.remove(0), farg_types[0]), + Intrinsic::Cttz => codegen_count_intrinsic!(cttz, true), + Intrinsic::CttzNonZero => codegen_count_intrinsic!(cttz, false), + Intrinsic::DiscriminantValue => { let sig = instance.ty().kind().fn_sig().unwrap().skip_binder(); let ty = pointee_type_stable(sig.inputs()[0]).unwrap(); let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty); self.codegen_expr_to_place_stable(place, e, loc) } - "exact_div" => self.codegen_exact_div(fargs, place, loc), - "exp2f32" => codegen_simple_intrinsic!(Exp2f), - "exp2f64" => codegen_simple_intrinsic!(Exp2), - "expf32" => codegen_simple_intrinsic!(Expf), - "expf64" => codegen_simple_intrinsic!(Exp), - "fabsf32" => codegen_simple_intrinsic!(Fabsf), - "fabsf64" => codegen_simple_intrinsic!(Fabs), - "fadd_fast" => { + Intrinsic::ExactDiv => self.codegen_exact_div(fargs, place, loc), + Intrinsic::Exp2F32 => codegen_simple_intrinsic!(Exp2f), + Intrinsic::Exp2F64 => codegen_simple_intrinsic!(Exp2), + Intrinsic::ExpF32 => codegen_simple_intrinsic!(Expf), + Intrinsic::ExpF64 => codegen_simple_intrinsic!(Exp), + Intrinsic::FabsF32 => codegen_simple_intrinsic!(Fabsf), + Intrinsic::FabsF64 => codegen_simple_intrinsic!(Fabs), + Intrinsic::FaddFast => { let fargs_clone = fargs.clone(); let binop_stmt = codegen_intrinsic_binop!(plus); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) + self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span) } - "fdiv_fast" => { + Intrinsic::FdivFast => { let fargs_clone = fargs.clone(); let binop_stmt = codegen_intrinsic_binop!(div); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) + self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span) } - "floorf32" => codegen_simple_intrinsic!(Floorf), - "floorf64" => codegen_simple_intrinsic!(Floor), - "fmaf32" => codegen_simple_intrinsic!(Fmaf), - "fmaf64" => codegen_simple_intrinsic!(Fma), - "fmul_fast" => { + Intrinsic::FloorF32 => codegen_simple_intrinsic!(Floorf), + Intrinsic::FloorF64 => codegen_simple_intrinsic!(Floor), + Intrinsic::FmafF32 => codegen_simple_intrinsic!(Fmaf), + Intrinsic::FmafF64 => codegen_simple_intrinsic!(Fma), + Intrinsic::FmulFast => { let fargs_clone = fargs.clone(); let binop_stmt = codegen_intrinsic_binop!(mul); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) + self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span) } - "forget" => Stmt::skip(loc), - "fsub_fast" => { + Intrinsic::Forget => Stmt::skip(loc), + Intrinsic::FsubFast => { let fargs_clone = fargs.clone(); let binop_stmt = codegen_intrinsic_binop!(sub); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) + self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span) } - "is_val_statically_known" => { + Intrinsic::IsValStaticallyKnown => { // Returning false is sound according do this intrinsic's documentation: // https://doc.rust-lang.org/nightly/std/intrinsics/fn.is_val_statically_known.html self.codegen_expr_to_place_stable(place, Expr::c_false(), loc) } - "likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc), - "log10f32" => codegen_simple_intrinsic!(Log10f), - "log10f64" => codegen_simple_intrinsic!(Log10), - "log2f32" => codegen_simple_intrinsic!(Log2f), - "log2f64" => codegen_simple_intrinsic!(Log2), - "logf32" => codegen_simple_intrinsic!(Logf), - "logf64" => codegen_simple_intrinsic!(Log), - "maxnumf32" => codegen_simple_intrinsic!(Fmaxf), - "maxnumf64" => codegen_simple_intrinsic!(Fmax), - "min_align_of" => codegen_intrinsic_const!(), - "min_align_of_val" => codegen_size_align!(align), - "minnumf32" => codegen_simple_intrinsic!(Fminf), - "minnumf64" => codegen_simple_intrinsic!(Fmin), - "mul_with_overflow" => { + Intrinsic::Likely => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc), + Intrinsic::Log10F32 => codegen_simple_intrinsic!(Log10f), + Intrinsic::Log10F64 => codegen_simple_intrinsic!(Log10), + Intrinsic::Log2F32 => codegen_simple_intrinsic!(Log2f), + Intrinsic::Log2F64 => codegen_simple_intrinsic!(Log2), + Intrinsic::LogF32 => codegen_simple_intrinsic!(Logf), + Intrinsic::LogF64 => codegen_simple_intrinsic!(Log), + Intrinsic::MaxNumF32 => codegen_simple_intrinsic!(Fmaxf), + Intrinsic::MaxNumF64 => codegen_simple_intrinsic!(Fmax), + Intrinsic::MinAlignOf => codegen_intrinsic_const!(), + Intrinsic::MinAlignOfVal => codegen_size_align!(align), + Intrinsic::MinNumF32 => codegen_simple_intrinsic!(Fminf), + Intrinsic::MinNumF64 => codegen_simple_intrinsic!(Fmin), + Intrinsic::MulWithOverflow => { self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc) } - "nearbyintf32" => codegen_simple_intrinsic!(Nearbyintf), - "nearbyintf64" => codegen_simple_intrinsic!(Nearbyint), - "needs_drop" => codegen_intrinsic_const!(), - // As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset` - "offset" => unreachable!( - "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`" - ), - "powf32" => codegen_simple_intrinsic!(Powf), - "powf64" => codegen_simple_intrinsic!(Pow), - "powif32" => codegen_simple_intrinsic!(Powif), - "powif64" => codegen_simple_intrinsic!(Powi), - "pref_align_of" => codegen_intrinsic_const!(), - "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), - "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc), - "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, place, loc), - "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), - "retag_box_to_raw" => self.codegen_retag_box_to_raw(fargs, place, loc), - "rintf32" => codegen_simple_intrinsic!(Rintf), - "rintf64" => codegen_simple_intrinsic!(Rint), - "rotate_left" => codegen_intrinsic_binop!(rol), - "rotate_right" => codegen_intrinsic_binop!(ror), - "roundf32" => codegen_simple_intrinsic!(Roundf), - "roundf64" => codegen_simple_intrinsic!(Round), - "saturating_add" => codegen_intrinsic_binop_with_mm!(saturating_add), - "saturating_sub" => codegen_intrinsic_binop_with_mm!(saturating_sub), - "sinf32" => codegen_simple_intrinsic!(Sinf), - "sinf64" => codegen_simple_intrinsic!(Sin), - "simd_add" => self.codegen_simd_op_with_overflow( + Intrinsic::NearbyIntF32 => codegen_simple_intrinsic!(Nearbyintf), + Intrinsic::NearbyIntF64 => codegen_simple_intrinsic!(Nearbyint), + Intrinsic::NeedsDrop => codegen_intrinsic_const!(), + Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf), + Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow), + Intrinsic::PowIF32 => codegen_simple_intrinsic!(Powif), + Intrinsic::PowIF64 => codegen_simple_intrinsic!(Powi), + Intrinsic::PrefAlignOf => codegen_intrinsic_const!(), + Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), + Intrinsic::PtrOffsetFrom => self.codegen_ptr_offset_from(fargs, place, loc), + Intrinsic::PtrOffsetFromUnsigned => { + self.codegen_ptr_offset_from_unsigned(fargs, place, loc) + } + Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), + Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc), + Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf), + Intrinsic::RintF64 => codegen_simple_intrinsic!(Rint), + Intrinsic::RotateLeft => codegen_intrinsic_binop!(rol), + Intrinsic::RotateRight => codegen_intrinsic_binop!(ror), + Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf), + Intrinsic::RoundF64 => codegen_simple_intrinsic!(Round), + Intrinsic::SaturatingAdd => codegen_intrinsic_binop_with_mm!(saturating_add), + Intrinsic::SaturatingSub => codegen_intrinsic_binop_with_mm!(saturating_sub), + Intrinsic::SinF32 => codegen_simple_intrinsic!(Sinf), + Intrinsic::SinF64 => codegen_simple_intrinsic!(Sin), + Intrinsic::SimdAdd => self.codegen_simd_op_with_overflow( Expr::plus, Expr::add_overflow_p, fargs, - intrinsic, + intrinsic_str, place, loc, ), - "simd_and" => codegen_intrinsic_binop!(bitand), + Intrinsic::SimdAnd => codegen_intrinsic_binop!(bitand), // TODO: `simd_rem` doesn't check for overflow cases for floating point operands. // - "simd_div" | "simd_rem" => { - self.codegen_simd_div_with_overflow(fargs, intrinsic, place, loc) + Intrinsic::SimdDiv | Intrinsic::SimdRem => { + self.codegen_simd_div_with_overflow(fargs, intrinsic_str, place, loc) } - "simd_eq" => { + Intrinsic::SimdEq => { self.codegen_simd_cmp(Expr::vector_eq, fargs, place, span, farg_types, ret_ty) } - "simd_extract" => { + Intrinsic::SimdExtract => { self.codegen_intrinsic_simd_extract(fargs, place, farg_types, ret_ty, span) } - "simd_ge" => { + Intrinsic::SimdGe => { self.codegen_simd_cmp(Expr::vector_ge, fargs, place, span, farg_types, ret_ty) } - "simd_gt" => { + Intrinsic::SimdGt => { self.codegen_simd_cmp(Expr::vector_gt, fargs, place, span, farg_types, ret_ty) } - "simd_insert" => { + Intrinsic::SimdInsert => { self.codegen_intrinsic_simd_insert(fargs, place, cbmc_ret_ty, farg_types, span, loc) } - "simd_le" => { + Intrinsic::SimdLe => { self.codegen_simd_cmp(Expr::vector_le, fargs, place, span, farg_types, ret_ty) } - "simd_lt" => { + Intrinsic::SimdLt => { self.codegen_simd_cmp(Expr::vector_lt, fargs, place, span, farg_types, ret_ty) } - "simd_mul" => self.codegen_simd_op_with_overflow( + Intrinsic::SimdMul => self.codegen_simd_op_with_overflow( Expr::mul, Expr::mul_overflow_p, fargs, - intrinsic, + intrinsic_str, place, loc, ), - "simd_ne" => { + Intrinsic::SimdNe => { self.codegen_simd_cmp(Expr::vector_neq, fargs, place, span, farg_types, ret_ty) } - "simd_or" => codegen_intrinsic_binop!(bitor), - "simd_shl" | "simd_shr" => { - self.codegen_simd_shift_with_distance_check(fargs, intrinsic, place, loc) + Intrinsic::SimdOr => codegen_intrinsic_binop!(bitor), + Intrinsic::SimdShl | Intrinsic::SimdShr => { + self.codegen_simd_shift_with_distance_check(fargs, intrinsic_str, place, loc) + } + Intrinsic::SimdShuffle(stripped) => { + let n: u64 = self.simd_shuffle_length(stripped.as_str(), farg_types, span); + self.codegen_intrinsic_simd_shuffle(fargs, place, farg_types, ret_ty, n, span) } - // "simd_shuffle#" => handled in an `if` preceding this match - "simd_sub" => self.codegen_simd_op_with_overflow( + Intrinsic::SimdSub => self.codegen_simd_op_with_overflow( Expr::sub, Expr::sub_overflow_p, fargs, - intrinsic, + intrinsic_str, place, loc, ), - "simd_xor" => codegen_intrinsic_binop!(bitxor), - "size_of" => unreachable!(), - "size_of_val" => codegen_size_align!(size), - "sqrtf32" => codegen_simple_intrinsic!(Sqrtf), - "sqrtf64" => codegen_simple_intrinsic!(Sqrt), - "sub_with_overflow" => self.codegen_op_with_overflow( + Intrinsic::SimdXor => codegen_intrinsic_binop!(bitxor), + Intrinsic::SizeOfVal => codegen_size_align!(size), + Intrinsic::SqrtF32 => codegen_simple_intrinsic!(Sqrtf), + Intrinsic::SqrtF64 => codegen_simple_intrinsic!(Sqrt), + Intrinsic::SubWithOverflow => self.codegen_op_with_overflow( BinaryOperator::OverflowResultMinus, fargs, place, loc, ), - "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, place, loc), - "truncf32" => codegen_simple_intrinsic!(Truncf), - "truncf64" => codegen_simple_intrinsic!(Trunc), - "type_id" => codegen_intrinsic_const!(), - "type_name" => codegen_intrinsic_const!(), - "typed_swap" => self.codegen_swap(fargs, farg_types, loc), - "unaligned_volatile_load" => { + Intrinsic::Transmute => self.codegen_intrinsic_transmute(fargs, ret_ty, place, loc), + Intrinsic::TruncF32 => codegen_simple_intrinsic!(Truncf), + Intrinsic::TruncF64 => codegen_simple_intrinsic!(Trunc), + Intrinsic::TypeId => codegen_intrinsic_const!(), + Intrinsic::TypeName => codegen_intrinsic_const!(), + Intrinsic::TypedSwap => self.codegen_swap(fargs, farg_types, loc), + Intrinsic::UnalignedVolatileLoad => { unstable_codegen!(self.codegen_expr_to_place_stable( place, fargs.remove(0).dereference(), loc )) } - "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr" - | "unchecked_sub" => { - unreachable!("Expected intrinsic `{intrinsic}` to be lowered before codegen") - } - "unchecked_div" => codegen_op_with_div_overflow_check!(div), - "unchecked_rem" => codegen_op_with_div_overflow_check!(rem), - "unlikely" => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc), - "unreachable" => unreachable!( - "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`" - ), - "volatile_copy_memory" => unstable_codegen!(codegen_intrinsic_copy!(Memmove)), - "volatile_copy_nonoverlapping_memory" => { + Intrinsic::UncheckedDiv => codegen_op_with_div_overflow_check!(div), + Intrinsic::UncheckedRem => codegen_op_with_div_overflow_check!(rem), + Intrinsic::Unlikely => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc), + Intrinsic::VolatileCopyMemory => unstable_codegen!(codegen_intrinsic_copy!(Memmove)), + Intrinsic::VolatileCopyNonOverlappingMemory => { unstable_codegen!(codegen_intrinsic_copy!(Memcpy)) } - "volatile_load" => self.codegen_volatile_load(fargs, farg_types, place, loc), - "volatile_store" => { + Intrinsic::VolatileLoad => self.codegen_volatile_load(fargs, farg_types, place, loc), + Intrinsic::VolatileStore => { assert!(self.place_ty_stable(place).kind().is_unit()); self.codegen_volatile_store(fargs, farg_types, loc) } - "vtable_size" => self.vtable_info(VTableInfo::Size, fargs, place, loc), - "vtable_align" => self.vtable_info(VTableInfo::Align, fargs, place, loc), - "wrapping_add" => codegen_wrapping_op!(plus), - "wrapping_mul" => codegen_wrapping_op!(mul), - "wrapping_sub" => codegen_wrapping_op!(sub), - "write_bytes" => { + Intrinsic::VtableSize => self.vtable_info(VTableInfo::Size, fargs, place, loc), + Intrinsic::VtableAlign => self.vtable_info(VTableInfo::Align, fargs, place, loc), + Intrinsic::WrappingAdd => codegen_wrapping_op!(plus), + Intrinsic::WrappingMul => codegen_wrapping_op!(mul), + Intrinsic::WrappingSub => codegen_wrapping_op!(sub), + Intrinsic::WriteBytes => { assert!(self.place_ty_stable(place).kind().is_unit()); self.codegen_write_bytes(fargs, farg_types, loc) } // Unimplemented - _ => self.codegen_unimplemented_stmt( - intrinsic, - loc, - "https://github.com/model-checking/kani/issues/new/choose", - ), + Intrinsic::Unimplemented { name, issue_link } => { + self.codegen_unimplemented_stmt(&name, loc, &issue_link) + } } } diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs new file mode 100644 index 000000000000..9485d8525410 --- /dev/null +++ b/kani-compiler/src/intrinsics.rs @@ -0,0 +1,798 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Single source of truth about which intrinsics we support. + +use stable_mir::{ + mir::{mono::Instance, Mutability}, + ty::{FloatTy, IntTy, RigidTy, TyKind, UintTy}, +}; + +// Enumeration of all intrinsics we support right now, with the last option being a catch-all. This +// way, adding an intrinsic would highlight all places where they are used. +#[allow(unused)] +#[derive(Clone, Debug)] +pub enum Intrinsic { + AddWithOverflow, + ArithOffset, + AssertInhabited, + AssertMemUninitializedValid, + AssertZeroValid, + Assume, + AtomicAnd(String), + AtomicCxchg(String), + AtomicCxchgWeak(String), + AtomicFence(String), + AtomicLoad(String), + AtomicMax(String), + AtomicMin(String), + AtomicNand(String), + AtomicOr(String), + AtomicSingleThreadFence(String), + AtomicStore(String), + AtomicUmax(String), + AtomicUmin(String), + AtomicXadd(String), + AtomicXchg(String), + AtomicXor(String), + AtomicXsub(String), + Bitreverse, + BlackBox, + Breakpoint, + Bswap, + CeilF32, + CeilF64, + CompareBytes, + Copy, + CopySignF32, + CopySignF64, + CosF32, + CosF64, + Ctlz, + CtlzNonZero, + Ctpop, + Cttz, + CttzNonZero, + DiscriminantValue, + ExactDiv, + Exp2F32, + Exp2F64, + ExpF32, + ExpF64, + FabsF32, + FabsF64, + FaddFast, + FdivFast, + FloorF32, + FloorF64, + FmafF32, + FmafF64, + FmulFast, + Forget, + FsubFast, + IsValStaticallyKnown, + Likely, + Log10F32, + Log10F64, + Log2F32, + Log2F64, + LogF32, + LogF64, + MaxNumF32, + MaxNumF64, + MinAlignOf, + MinAlignOfVal, + MinNumF32, + MinNumF64, + MulWithOverflow, + NearbyIntF32, + NearbyIntF64, + NeedsDrop, + PowF32, + PowF64, + PowIF32, + PowIF64, + PrefAlignOf, + PtrGuaranteedCmp, + PtrOffsetFrom, + PtrOffsetFromUnsigned, + RawEq, + RetagBoxToRaw, + RintF32, + RintF64, + RotateLeft, + RotateRight, + RoundF32, + RoundF64, + SaturatingAdd, + SaturatingSub, + SinF32, + SinF64, + SimdAdd, + SimdAnd, + SimdDiv, + SimdRem, + SimdEq, + SimdExtract, + SimdGe, + SimdGt, + SimdInsert, + SimdLe, + SimdLt, + SimdMul, + SimdNe, + SimdOr, + SimdShl, + SimdShr, + SimdShuffle(String), + SimdSub, + SimdXor, + SizeOfVal, + SqrtF32, + SqrtF64, + SubWithOverflow, + Transmute, + TruncF32, + TruncF64, + TypeId, + TypeName, + TypedSwap, + UnalignedVolatileLoad, + UncheckedDiv, + UncheckedRem, + Unlikely, + VolatileCopyMemory, + VolatileCopyNonOverlappingMemory, + VolatileLoad, + VolatileStore, + VtableSize, + VtableAlign, + WrappingAdd, + WrappingMul, + WrappingSub, + WriteBytes, + Unimplemented { name: String, issue_link: String }, +} + +/// Assert that top-level types of a function signature match the given patterns. +macro_rules! assert_sig_matches { + ($sig:expr, $($input_type:pat),* => $output_type:pat) => { + let inputs = $sig.inputs(); + let output = $sig.output(); + #[allow(unused_mut)] + let mut index = 0; + $( + #[allow(unused_assignments)] + { + assert!(matches!(inputs[index].kind(), TyKind::RigidTy($input_type))); + index += 1; + } + )* + assert!(inputs.len() == index); + assert!(matches!(output.kind(), TyKind::RigidTy($output_type))); + } +} + +impl Intrinsic { + /// Create an intrinsic enum from a given intrinsic instance, shallowly validating the argument types. + pub fn from_instance(intrinsic_instance: &Instance) -> Self { + let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap(); + let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder(); + match intrinsic_str.as_str() { + "add_with_overflow" => { + assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_)); + Self::AddWithOverflow + } + "arith_offset" => { + assert_sig_matches!(sig, + RigidTy::RawPtr(_, Mutability::Not), + RigidTy::Int(IntTy::Isize) + => RigidTy::RawPtr(_, Mutability::Not)); + Self::ArithOffset + } + "assert_inhabited" => { + assert_sig_matches!(sig, => RigidTy::Tuple(_)); + Self::AssertInhabited + } + "assert_mem_uninitialized_valid" => { + assert_sig_matches!(sig, => RigidTy::Tuple(_)); + Self::AssertMemUninitializedValid + } + "assert_zero_valid" => { + assert_sig_matches!(sig, => RigidTy::Tuple(_)); + Self::AssertZeroValid + } + "assume" => { + assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Tuple(_)); + Self::Assume + } + "bitreverse" => { + assert_sig_matches!(sig, _ => _); + Self::Bitreverse + } + "black_box" => { + assert_sig_matches!(sig, _ => _); + Self::BlackBox + } + "breakpoint" => { + assert_sig_matches!(sig, => RigidTy::Tuple(_)); + Self::Breakpoint + } + "bswap" => { + assert_sig_matches!(sig, _ => _); + Self::Bswap + } + "caller_location" => { + assert_sig_matches!(sig, => RigidTy::Ref(_, _, Mutability::Not)); + Self::Unimplemented { + name: intrinsic_str, + issue_link: "https://github.com/model-checking/kani/issues/374".into(), + } + } + "catch_unwind" => { + assert_sig_matches!(sig, RigidTy::FnPtr(_), RigidTy::RawPtr(_, Mutability::Mut), RigidTy::FnPtr(_) => RigidTy::Int(IntTy::I32)); + Self::Unimplemented { + name: intrinsic_str, + issue_link: "https://github.com/model-checking/kani/issues/267".into(), + } + } + "compare_bytes" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not), RigidTy::Uint(UintTy::Usize) => RigidTy::Int(IntTy::I32)); + Self::CompareBytes + } + "copy" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Mut), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_)); + Self::Copy + } + "copy_nonoverlapping" => unreachable!( + "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`" + ), + "ctlz" => { + assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32)); + Self::Ctlz + } + "ctlz_nonzero" => { + assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32)); + Self::CtlzNonZero + } + "ctpop" => { + assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32)); + Self::Ctpop + } + "cttz" => { + assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32)); + Self::Cttz + } + "cttz_nonzero" => { + assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32)); + Self::CttzNonZero + } + "discriminant_value" => { + assert_sig_matches!(sig, RigidTy::Ref(_, _, Mutability::Not) => _); + Self::DiscriminantValue + } + "exact_div" => { + assert_sig_matches!(sig, _, _ => _); + Self::ExactDiv + } + "fadd_fast" => { + assert_sig_matches!(sig, _, _ => _); + Self::FaddFast + } + "fdiv_fast" => { + assert_sig_matches!(sig, _, _ => _); + Self::FdivFast + } + "fmul_fast" => { + assert_sig_matches!(sig, _, _ => _); + Self::FmulFast + } + "forget" => { + assert_sig_matches!(sig, _ => RigidTy::Tuple(_)); + Self::Forget + } + "fsub_fast" => { + assert_sig_matches!(sig, _, _ => _); + Self::FsubFast + } + "is_val_statically_known" => { + assert_sig_matches!(sig, _ => RigidTy::Bool); + Self::IsValStaticallyKnown + } + "likely" => { + assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Bool); + Self::Likely + } + "min_align_of" => { + assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize)); + Self::MinAlignOf + } + "min_align_of_val" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize)); + Self::MinAlignOfVal + } + "mul_with_overflow" => { + assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_)); + Self::MulWithOverflow + } + "needs_drop" => { + assert_sig_matches!(sig, => RigidTy::Bool); + Self::NeedsDrop + } + // As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset` + "offset" => unreachable!( + "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`" + ), + "pref_align_of" => { + assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize)); + Self::PrefAlignOf + } + "ptr_guaranteed_cmp" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::U8)); + Self::PtrGuaranteedCmp + } + "ptr_offset_from" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Int(IntTy::Isize)); + Self::PtrOffsetFrom + } + "ptr_offset_from_unsigned" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize)); + Self::PtrOffsetFromUnsigned + } + "raw_eq" => { + assert_sig_matches!(sig, RigidTy::Ref(_, _, Mutability::Not), RigidTy::Ref(_, _, Mutability::Not) => RigidTy::Bool); + Self::RawEq + } + "rotate_left" => { + assert_sig_matches!(sig, _, RigidTy::Uint(UintTy::U32) => _); + Self::RotateLeft + } + "rotate_right" => { + assert_sig_matches!(sig, _, RigidTy::Uint(UintTy::U32) => _); + Self::RotateRight + } + "saturating_add" => { + assert_sig_matches!(sig, _, _ => _); + Self::SaturatingAdd + } + "saturating_sub" => { + assert_sig_matches!(sig, _, _ => _); + Self::SaturatingSub + } + "size_of" => unreachable!(), + "size_of_val" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize)); + Self::SizeOfVal + } + "sub_with_overflow" => { + assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_)); + Self::SubWithOverflow + } + "transmute" => { + assert_sig_matches!(sig, _ => _); + Self::Transmute + } + "type_id" => { + assert_sig_matches!(sig, => RigidTy::Uint(UintTy::U128)); + Self::TypeId + } + "type_name" => { + assert_sig_matches!(sig, => RigidTy::Ref(_, _, Mutability::Not)); + Self::TypeName + } + "typed_swap" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Mut) => RigidTy::Tuple(_)); + Self::TypedSwap + } + "unaligned_volatile_load" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _); + Self::UnalignedVolatileLoad + } + "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr" + | "unchecked_sub" => { + unreachable!("Expected intrinsic `{intrinsic_str}` to be lowered before codegen") + } + "unchecked_div" => { + assert_sig_matches!(sig, _, _ => _); + Self::UncheckedDiv + } + "unchecked_rem" => { + assert_sig_matches!(sig, _, _ => _); + Self::UncheckedRem + } + "unlikely" => { + assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Bool); + Self::Unlikely + } + "unreachable" => unreachable!( + "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`" + ), + "volatile_copy_memory" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Not), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_)); + Self::VolatileCopyMemory + } + "volatile_copy_nonoverlapping_memory" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Not), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_)); + Self::VolatileCopyNonOverlappingMemory + } + "volatile_load" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _); + Self::VolatileLoad + } + "volatile_store" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_)); + Self::VolatileStore + } + "vtable_size" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize)); + Self::VtableSize + } + "vtable_align" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize)); + Self::VtableAlign + } + "wrapping_add" => { + assert_sig_matches!(sig, _, _ => _); + Self::WrappingAdd + } + "wrapping_mul" => { + assert_sig_matches!(sig, _, _ => _); + Self::WrappingMul + } + "wrapping_sub" => { + assert_sig_matches!(sig, _, _ => _); + Self::WrappingSub + } + "write_bytes" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::Uint(UintTy::U8), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_)); + Self::WriteBytes + } + _ => try_match_atomic(intrinsic_instance) + .or_else(|| try_match_simd(intrinsic_instance)) + .or_else(|| try_match_f32(intrinsic_instance)) + .or_else(|| try_match_f64(intrinsic_instance)) + .unwrap_or(Self::Unimplemented { + name: intrinsic_str, + issue_link: "https://github.com/model-checking/kani/issues/new/choose".into(), + }), + } + } +} + +/// Match atomic intrinsics by instance, returning an instance of the intrinsics enum if the match +/// is successful. +fn try_match_atomic(intrinsic_instance: &Instance) -> Option { + let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap(); + let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder(); + if let Some(suffix) = intrinsic_str.strip_prefix("atomic_and_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicAnd(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchgweak_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicCxchgWeak(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchg_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicCxchg(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence_") { + assert_sig_matches!(sig, => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicFence(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_load_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _); + Some(Intrinsic::AtomicLoad(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_max_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicMax(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_min_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicMin(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_nand_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicNand(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_or_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicOr(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_singlethreadfence_") { + assert_sig_matches!(sig, => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicSingleThreadFence(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_store_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicStore(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umax_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicUmax(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umin_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicUmin(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xadd_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicXadd(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xchg_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicXchg(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xor_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicXor(suffix.into())) + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xsub_") { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicXsub(suffix.into())) + } else { + None + } +} + +/// Match SIMD intrinsics by instance, returning an instance of the intrinsics enum if the match +/// is successful. +fn try_match_simd(intrinsic_instance: &Instance) -> Option { + let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap(); + let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder(); + match intrinsic_str.as_str() { + "simd_add" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdAdd) + } + "simd_and" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdAnd) + } + "simd_div" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdDiv) + } + "simd_rem" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdRem) + } + "simd_eq" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdEq) + } + "simd_extract" => { + assert_sig_matches!(sig, _, RigidTy::Uint(UintTy::U32) => _); + Some(Intrinsic::SimdExtract) + } + "simd_ge" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdGe) + } + "simd_gt" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdGt) + } + "simd_insert" => { + assert_sig_matches!(sig, _, RigidTy::Uint(UintTy::U32), _ => _); + Some(Intrinsic::SimdInsert) + } + "simd_le" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdLe) + } + "simd_lt" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdLt) + } + "simd_mul" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdMul) + } + "simd_ne" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdNe) + } + "simd_or" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdOr) + } + "simd_shl" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdShl) + } + "simd_shr" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdShr) + } + "simd_sub" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdSub) + } + "simd_xor" => { + assert_sig_matches!(sig, _, _ => _); + Some(Intrinsic::SimdXor) + } + name => { + if let Some(suffix) = name.strip_prefix("simd_shuffle") { + assert_sig_matches!(sig, _, _, _ => _); + Some(Intrinsic::SimdShuffle(suffix.into())) + } else { + None + } + } + } +} + +/// Match f32 arithmetic intrinsics by instance, returning an instance of the intrinsics enum if the match +/// is successful. +fn try_match_f32(intrinsic_instance: &Instance) -> Option { + let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap(); + let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder(); + match intrinsic_str.as_str() { + "ceilf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::CeilF32) + } + "copysignf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::CopySignF32) + } + "cosf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::CosF32) + } + "exp2f32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::Exp2F32) + } + "expf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::ExpF32) + } + "fabsf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::FabsF32) + } + "floorf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::FloorF32) + } + "fmaf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::FmafF32) + } + "log10f32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::Log10F32) + } + "log2f32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::Log2F32) + } + "logf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::LogF32) + } + "maxnumf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::MaxNumF32) + } + "minnumf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::MinNumF32) + } + "nearbyintf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::NearbyIntF32) + } + "powf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::PowF32) + } + "powif32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::PowIF32) + } + "rintf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::RintF32) + } + "roundf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::RoundF32) + } + "sinf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::SinF32) + } + "sqrtf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::SqrtF32) + } + "truncf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::TruncF32) + } + _ => None, + } +} + +/// Match f64 arithmetic intrinsics by instance, returning an instance of the intrinsics enum if the match +/// is successful. +fn try_match_f64(intrinsic_instance: &Instance) -> Option { + let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap(); + let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder(); + match intrinsic_str.as_str() { + "ceilf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::CeilF64) + } + "copysignf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::CopySignF64) + } + "cosf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::CosF64) + } + "exp2f64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::Exp2F64) + } + "expf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::ExpF64) + } + "fabsf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::FabsF64) + } + "floorf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::FloorF64) + } + "fmaf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::FmafF64) + } + "log10f64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::Log10F64) + } + "log2f64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::Log2F64) + } + "logf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::LogF64) + } + "maxnumf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::MaxNumF64) + } + "minnumf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::MinNumF64) + } + "nearbyintf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::NearbyIntF64) + } + "powf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::PowF64) + } + "powif64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::PowIF64) + } + "rintf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::RintF64) + } + "roundf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::RoundF64) + } + "sinf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::SinF64) + } + "sqrtf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::SqrtF64) + } + "truncf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::TruncF64) + } + _ => None, + } +} diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 640318ccb584..15593549b690 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -24,12 +24,14 @@ //! Currently, the analysis is not field-sensitive: e.g., if a field of a place aliases to some //! other place, we treat it as if the place itself aliases to another place. -use crate::kani_middle::{ - points_to::{MemLoc, PointsToGraph}, - reachability::CallGraph, - transform::RustcInternalMir, +use crate::{ + intrinsics::Intrinsic, + kani_middle::{ + points_to::{MemLoc, PointsToGraph}, + reachability::CallGraph, + transform::RustcInternalMir, + }, }; -use rustc_ast::Mutability; use rustc_middle::{ mir::{ BasicBlock, BinOp, Body, CallReturnPlaces, Location, NonDivergingIntrinsic, Operand, Place, @@ -202,161 +204,117 @@ impl<'a, 'tcx> Analysis<'tcx> for PointsToAnalysis<'a, 'tcx> { match instance.def { // Intrinsics could introduce aliasing edges we care about, so need to handle them. InstanceKind::Intrinsic(def_id) => { - match self.tcx.intrinsic(def_id).unwrap().name.to_string().as_str() { - name if name.starts_with("atomic") => { - match name { - // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments. - // This is equivalent to `destination = *dst; *dst = src`. - name if name.starts_with("atomic_cxchg") => { - assert_eq!( - args.len(), - 3, - "Unexpected number of arguments for `{name}`" - ); - assert!(matches!( - args[0].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Mut) - )); - let src_set = - self.successors_for_operand(state, args[2].node.clone()); - let dst_set = - self.successors_for_deref(state, args[0].node.clone()); - let destination_set = - state.resolve_place(*destination, self.instance); - state.extend(&destination_set, &state.successors(&dst_set)); - state.extend(&dst_set, &src_set); - } - // All `atomic_load` intrinsics take `src` as an argument. - // This is equivalent to `destination = *src`. - name if name.starts_with("atomic_load") => { - assert_eq!( - args.len(), - 1, - "Unexpected number of arguments for `{name}`" - ); - assert!(matches!( - args[0].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Not) - )); - let src_set = - self.successors_for_deref(state, args[0].node.clone()); - let destination_set = - state.resolve_place(*destination, self.instance); - state.extend(&destination_set, &state.successors(&src_set)); - } - // All `atomic_store` intrinsics take `dst, val` as arguments. - // This is equivalent to `*dst = val`. - name if name.starts_with("atomic_store") => { - assert_eq!( - args.len(), - 2, - "Unexpected number of arguments for `{name}`" - ); - assert!(matches!( - args[0].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Mut) - )); - let dst_set = - self.successors_for_deref(state, args[0].node.clone()); - let val_set = - self.successors_for_operand(state, args[1].node.clone()); - state.extend(&dst_set, &val_set); - } - // All other `atomic` intrinsics take `dst, src` as arguments. - // This is equivalent to `destination = *dst; *dst = src`. - _ => { - assert_eq!( - args.len(), - 2, - "Unexpected number of arguments for `{name}`" - ); - assert!(matches!( - args[0].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Mut) - )); - let src_set = - self.successors_for_operand(state, args[1].node.clone()); - let dst_set = - self.successors_for_deref(state, args[0].node.clone()); - let destination_set = - state.resolve_place(*destination, self.instance); - state.extend(&destination_set, &state.successors(&dst_set)); - state.extend(&dst_set, &src_set); - } - }; - } - // Similar to `copy_nonoverlapping`, argument order is `src`, `dst`, `count`. - "copy" => { - assert_eq!(args.len(), 3, "Unexpected number of arguments for `copy`"); - assert!(matches!( - args[0].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Not) - )); - assert!(matches!( - args[1].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Mut) - )); - self.apply_copy_effect( - state, - args[0].node.clone(), - args[1].node.clone(), - ); - } - // Similar to `copy_nonoverlapping`, argument order is `dst`, `src`, `count`. - "volatile_copy_memory" | "volatile_copy_nonoverlapping_memory" => { - assert_eq!(args.len(), 3, "Unexpected number of arguments for `copy`"); - assert!(matches!( - args[0].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Mut) - )); - assert!(matches!( - args[1].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Not) - )); - self.apply_copy_effect( - state, - args[1].node.clone(), - args[0].node.clone(), - ); - } - // Semantically equivalent to dest = *a - "volatile_load" | "unaligned_volatile_load" => { - assert_eq!( - args.len(), - 1, - "Unexpected number of arguments for `volatile_load`" - ); - assert!(matches!( - args[0].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Not) - )); - // Destination of the return value. - let lvalue_set = state.resolve_place(*destination, self.instance); - let rvalue_set = self.successors_for_deref(state, args[0].node.clone()); - state.extend(&lvalue_set, &state.successors(&rvalue_set)); - } - // Semantically equivalent *a = b. - "volatile_store" | "unaligned_volatile_store" => { - assert_eq!( - args.len(), - 2, - "Unexpected number of arguments for `volatile_store`" - ); - assert!(matches!( - args[0].node.ty(self.body, self.tcx).kind(), - TyKind::RawPtr(_, Mutability::Mut) - )); - let lvalue_set = self.successors_for_deref(state, args[0].node.clone()); - let rvalue_set = - self.successors_for_operand(state, args[1].node.clone()); - state.extend(&lvalue_set, &rvalue_set); - } - _ => { - // TODO: this probably does not handle all relevant intrinsics, so more - // need to be added. For more information, see: - // https://github.com/model-checking/kani/issues/3300 - if self.tcx.is_mir_available(def_id) { - self.apply_regular_call_effect(state, instance, args, destination); + // Check if the intrinsic has a body we can analyze. + if self.tcx.is_mir_available(def_id) { + self.apply_regular_call_effect(state, instance, args, destination); + } else { + // Check all of the other intrinsics. + match Intrinsic::from_instance(&rustc_internal::stable(instance)) { + intrinsic if is_identity_aliasing_intrinsic(intrinsic.clone()) => { + // Treat the intrinsic as an aggregate, taking a union of all of the + // arguments' aliases. + let destination_set = + state.resolve_place(*destination, self.instance); + let operands_set = args + .into_iter() + .flat_map(|operand| { + self.successors_for_operand(state, operand.node.clone()) + }) + .collect(); + state.extend(&destination_set, &operands_set); + } + // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments. + // This is equivalent to `destination = *dst; *dst = src`. + Intrinsic::AtomicCxchg(_) | Intrinsic::AtomicCxchgWeak(_) => { + let src_set = + self.successors_for_operand(state, args[2].node.clone()); + let dst_set = + self.successors_for_deref(state, args[0].node.clone()); + let destination_set = + state.resolve_place(*destination, self.instance); + state.extend(&destination_set, &state.successors(&dst_set)); + state.extend(&dst_set, &src_set); + } + // All `atomic_load` intrinsics take `src` as an argument. + // This is equivalent to `destination = *src`. + Intrinsic::AtomicLoad(_) => { + let src_set = + self.successors_for_deref(state, args[0].node.clone()); + let destination_set = + state.resolve_place(*destination, self.instance); + state.extend(&destination_set, &state.successors(&src_set)); + } + // All `atomic_store` intrinsics take `dst, val` as arguments. + // This is equivalent to `*dst = val`. + Intrinsic::AtomicStore(_) => { + let dst_set = + self.successors_for_deref(state, args[0].node.clone()); + let val_set = + self.successors_for_operand(state, args[1].node.clone()); + state.extend(&dst_set, &val_set); + } + // All other `atomic` intrinsics take `dst, src` as arguments. + // This is equivalent to `destination = *dst; *dst = src`. + Intrinsic::AtomicAnd(_) + | Intrinsic::AtomicMax(_) + | Intrinsic::AtomicMin(_) + | Intrinsic::AtomicNand(_) + | Intrinsic::AtomicOr(_) + | Intrinsic::AtomicUmax(_) + | Intrinsic::AtomicUmin(_) + | Intrinsic::AtomicXadd(_) + | Intrinsic::AtomicXchg(_) + | Intrinsic::AtomicXor(_) + | Intrinsic::AtomicXsub(_) => { + let src_set = + self.successors_for_operand(state, args[1].node.clone()); + let dst_set = + self.successors_for_deref(state, args[0].node.clone()); + let destination_set = + state.resolve_place(*destination, self.instance); + state.extend(&destination_set, &state.successors(&dst_set)); + state.extend(&dst_set, &src_set); + } + // Similar to `copy_nonoverlapping`, argument order is `src`, `dst`, `count`. + Intrinsic::Copy => { + self.apply_copy_effect( + state, + args[0].node.clone(), + args[1].node.clone(), + ); + } + // Similar to `copy_nonoverlapping`, argument order is `dst`, `src`, `count`. + Intrinsic::VolatileCopyMemory + | Intrinsic::VolatileCopyNonOverlappingMemory => { + self.apply_copy_effect( + state, + args[1].node.clone(), + args[0].node.clone(), + ); + } + // Semantically equivalent to dest = *a + Intrinsic::VolatileLoad | Intrinsic::UnalignedVolatileLoad => { + // Destination of the return value. + let lvalue_set = state.resolve_place(*destination, self.instance); + let rvalue_set = + self.successors_for_deref(state, args[0].node.clone()); + state.extend(&lvalue_set, &state.successors(&rvalue_set)); + } + // Semantically equivalent *a = b. + Intrinsic::VolatileStore => { + let lvalue_set = + self.successors_for_deref(state, args[0].node.clone()); + let rvalue_set = + self.successors_for_operand(state, args[1].node.clone()); + state.extend(&lvalue_set, &rvalue_set); + } + Intrinsic::Unimplemented { .. } => { + // This will be taken care of at the codegen level. + } + intrinsic => { + unimplemented!( + "Kani does not support reasoning about aliasing in presence of intrinsic `{intrinsic:?}`. For more information about the state of uninitialized memory checks implementation, see: https://github.com/model-checking/kani/issues/3300." + ); } } } @@ -652,3 +610,136 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { } } } + +/// Determines if the intrinsic does not influence aliasing beyond being treated as an identity +/// function (i.e. propagate aliasing without changes). +fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { + match intrinsic { + Intrinsic::AddWithOverflow + | Intrinsic::ArithOffset + | Intrinsic::AssertInhabited + | Intrinsic::AssertMemUninitializedValid + | Intrinsic::AssertZeroValid + | Intrinsic::Assume + | Intrinsic::Bitreverse + | Intrinsic::BlackBox + | Intrinsic::Breakpoint + | Intrinsic::Bswap + | Intrinsic::CeilF32 + | Intrinsic::CeilF64 + | Intrinsic::CompareBytes + | Intrinsic::CopySignF32 + | Intrinsic::CopySignF64 + | Intrinsic::CosF32 + | Intrinsic::CosF64 + | Intrinsic::Ctlz + | Intrinsic::CtlzNonZero + | Intrinsic::Ctpop + | Intrinsic::Cttz + | Intrinsic::CttzNonZero + | Intrinsic::DiscriminantValue + | Intrinsic::ExactDiv + | Intrinsic::Exp2F32 + | Intrinsic::Exp2F64 + | Intrinsic::ExpF32 + | Intrinsic::ExpF64 + | Intrinsic::FabsF32 + | Intrinsic::FabsF64 + | Intrinsic::FaddFast + | Intrinsic::FdivFast + | Intrinsic::FloorF32 + | Intrinsic::FloorF64 + | Intrinsic::FmafF32 + | Intrinsic::FmafF64 + | Intrinsic::FmulFast + | Intrinsic::Forget + | Intrinsic::FsubFast + | Intrinsic::IsValStaticallyKnown + | Intrinsic::Likely + | Intrinsic::Log10F32 + | Intrinsic::Log10F64 + | Intrinsic::Log2F32 + | Intrinsic::Log2F64 + | Intrinsic::LogF32 + | Intrinsic::LogF64 + | Intrinsic::MaxNumF32 + | Intrinsic::MaxNumF64 + | Intrinsic::MinAlignOf + | Intrinsic::MinAlignOfVal + | Intrinsic::MinNumF32 + | Intrinsic::MinNumF64 + | Intrinsic::MulWithOverflow + | Intrinsic::NearbyIntF32 + | Intrinsic::NearbyIntF64 + | Intrinsic::NeedsDrop + | Intrinsic::PowF32 + | Intrinsic::PowF64 + | Intrinsic::PowIF32 + | Intrinsic::PowIF64 + | Intrinsic::PrefAlignOf + | Intrinsic::PtrGuaranteedCmp + | Intrinsic::PtrOffsetFrom + | Intrinsic::PtrOffsetFromUnsigned + | Intrinsic::RawEq + | Intrinsic::RintF32 + | Intrinsic::RintF64 + | Intrinsic::RotateLeft + | Intrinsic::RotateRight + | Intrinsic::RoundF32 + | Intrinsic::RoundF64 + | Intrinsic::SaturatingAdd + | Intrinsic::SaturatingSub + | Intrinsic::SinF32 + | Intrinsic::SinF64 + | Intrinsic::SizeOfVal + | Intrinsic::SqrtF32 + | Intrinsic::SqrtF64 + | Intrinsic::SubWithOverflow + | Intrinsic::TruncF32 + | Intrinsic::TruncF64 + | Intrinsic::TypeId + | Intrinsic::TypeName + | Intrinsic::UncheckedDiv + | Intrinsic::UncheckedRem + | Intrinsic::Unlikely + | Intrinsic::VtableSize + | Intrinsic::VtableAlign + | Intrinsic::WrappingAdd + | Intrinsic::WrappingMul + | Intrinsic::WrappingSub + | Intrinsic::WriteBytes => { + /* Intrinsics that do not interact with aliasing beyond propagating it. */ + true + } + Intrinsic::SimdAdd + | Intrinsic::SimdAnd + | Intrinsic::SimdDiv + | Intrinsic::SimdRem + | Intrinsic::SimdEq + | Intrinsic::SimdExtract + | Intrinsic::SimdGe + | Intrinsic::SimdGt + | Intrinsic::SimdInsert + | Intrinsic::SimdLe + | Intrinsic::SimdLt + | Intrinsic::SimdMul + | Intrinsic::SimdNe + | Intrinsic::SimdOr + | Intrinsic::SimdShl + | Intrinsic::SimdShr + | Intrinsic::SimdShuffle(_) + | Intrinsic::SimdSub + | Intrinsic::SimdXor => { + /* SIMD operations */ + true + } + Intrinsic::AtomicFence(_) | Intrinsic::AtomicSingleThreadFence(_) => { + /* Atomic fences */ + true + } + _ => { + /* Everything else */ + false + } + } +} diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs index 11ac412703ae..35d0e7041704 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs @@ -4,14 +4,17 @@ //! This module contains the visitor responsible for collecting initial analysis targets for delayed //! UB instrumentation. -use crate::kani_middle::transform::check_uninit::ty_layout::tys_layout_equal_to_size; +use crate::{ + intrinsics::Intrinsic, + kani_middle::transform::check_uninit::ty_layout::tys_layout_equal_to_size, +}; use stable_mir::{ mir::{ alloc::GlobalAlloc, mono::{Instance, InstanceKind, StaticDef}, visit::Location, - Body, CastKind, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, - Rvalue, Statement, StatementKind, Terminator, TerminatorKind, + Body, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, Rvalue, + Statement, StatementKind, Terminator, TerminatorKind, }, ty::{ConstantKind, RigidTy, TyKind}, }; @@ -101,34 +104,12 @@ impl MirVisitor for InitialTargetVisitor { if let TerminatorKind::Call { func, args, .. } = &term.kind { let instance = try_resolve_instance(self.body.locals(), func).unwrap(); if instance.kind == InstanceKind::Intrinsic { - match instance.intrinsic_name().unwrap().as_str() { - "copy" => { - assert_eq!(args.len(), 3, "Unexpected number of arguments for `copy`"); - assert!(matches!( - args[0].ty(self.body.locals()).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) - )); - assert!(matches!( - args[1].ty(self.body.locals()).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) - )); + match Intrinsic::from_instance(&instance) { + Intrinsic::Copy => { // Here, `dst` is the second argument. self.push_operand(&args[1]); } - "volatile_copy_memory" | "volatile_copy_nonoverlapping_memory" => { - assert_eq!( - args.len(), - 3, - "Unexpected number of arguments for `volatile_copy`" - ); - assert!(matches!( - args[0].ty(self.body.locals()).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) - )); - assert!(matches!( - args[1].ty(self.body.locals()).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) - )); + Intrinsic::VolatileCopyMemory | Intrinsic::VolatileCopyNonOverlappingMemory => { // Here, `dst` is the first argument. self.push_operand(&args[0]); } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 837e14abc886..f682f93a261e 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -3,12 +3,15 @@ // //! Visitor that collects all instructions relevant to uninitialized memory access. -use crate::kani_middle::transform::{ - body::{InsertPosition, MutableBody, SourceInstruction}, - check_uninit::{ - relevant_instruction::{InitRelevantInstruction, MemoryInitOp}, - ty_layout::tys_layout_compatible_to_size, - TargetFinder, +use crate::{ + intrinsics::Intrinsic, + kani_middle::transform::{ + body::{InsertPosition, MutableBody, SourceInstruction}, + check_uninit::{ + relevant_instruction::{InitRelevantInstruction, MemoryInitOp}, + ty_layout::tys_layout_compatible_to_size, + TargetFinder, + }, }, }; use stable_mir::{ @@ -16,8 +19,8 @@ use stable_mir::{ alloc::GlobalAlloc, mono::{Instance, InstanceKind}, visit::{Location, PlaceContext}, - BasicBlockIdx, CastKind, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand, - Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, + BasicBlockIdx, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, + PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }, ty::{ConstantKind, RigidTy, TyKind}, @@ -182,46 +185,30 @@ impl MirVisitor for CheckUninitVisitor { }; match instance.kind { InstanceKind::Intrinsic => { - match instance.intrinsic_name().unwrap().as_str() { - intrinsic_name if can_skip_intrinsic(intrinsic_name) => { + match Intrinsic::from_instance(&instance) { + intrinsic_name if can_skip_intrinsic(intrinsic_name.clone()) => { /* Intrinsics that can be safely skipped */ } - name if name.starts_with("atomic") => { - let num_args = match name { - // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments. - name if name.starts_with("atomic_cxchg") => 3, - // All `atomic_load` intrinsics take `src` as an argument. - name if name.starts_with("atomic_load") => 1, - // All other `atomic` intrinsics take `dst, src` as arguments. - _ => 2, - }; - assert_eq!( - args.len(), - num_args, - "Unexpected number of arguments for `{name}`" - ); - assert!(matches!( - args[0].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(..)) - )); + Intrinsic::AtomicAnd(_) + | Intrinsic::AtomicCxchg(_) + | Intrinsic::AtomicCxchgWeak(_) + | Intrinsic::AtomicLoad(_) + | Intrinsic::AtomicMax(_) + | Intrinsic::AtomicMin(_) + | Intrinsic::AtomicNand(_) + | Intrinsic::AtomicOr(_) + | Intrinsic::AtomicStore(_) + | Intrinsic::AtomicUmax(_) + | Intrinsic::AtomicUmin(_) + | Intrinsic::AtomicXadd(_) + | Intrinsic::AtomicXchg(_) + | Intrinsic::AtomicXor(_) + | Intrinsic::AtomicXsub(_) => { self.push_target(MemoryInitOp::Check { operand: args[0].clone(), }); } - "compare_bytes" => { - assert_eq!( - args.len(), - 3, - "Unexpected number of arguments for `compare_bytes`" - ); - assert!(matches!( - args[0].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) - )); - assert!(matches!( - args[1].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) - )); + Intrinsic::CompareBytes => { self.push_target(MemoryInitOp::CheckSliceChunk { operand: args[0].clone(), count: args[2].clone(), @@ -231,22 +218,7 @@ impl MirVisitor for CheckUninitVisitor { count: args[2].clone(), }); } - "copy" - | "volatile_copy_memory" - | "volatile_copy_nonoverlapping_memory" => { - assert_eq!( - args.len(), - 3, - "Unexpected number of arguments for `copy`" - ); - assert!(matches!( - args[0].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) - )); - assert!(matches!( - args[1].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) - )); + Intrinsic::Copy => { self.push_target(MemoryInitOp::CheckSliceChunk { operand: args[0].clone(), count: args[2].clone(), @@ -258,20 +230,20 @@ impl MirVisitor for CheckUninitVisitor { position: InsertPosition::After, }); } - "typed_swap" => { - assert_eq!( - args.len(), - 2, - "Unexpected number of arguments for `typed_swap`" - ); - assert!(matches!( - args[0].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) - )); - assert!(matches!( - args[1].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) - )); + Intrinsic::VolatileCopyMemory + | Intrinsic::VolatileCopyNonOverlappingMemory => { + self.push_target(MemoryInitOp::CheckSliceChunk { + operand: args[1].clone(), + count: args[2].clone(), + }); + self.push_target(MemoryInitOp::SetSliceChunk { + operand: args[0].clone(), + count: args[2].clone(), + value: true, + position: InsertPosition::After, + }); + } + Intrinsic::TypedSwap => { self.push_target(MemoryInitOp::Check { operand: args[0].clone(), }); @@ -279,46 +251,19 @@ impl MirVisitor for CheckUninitVisitor { operand: args[1].clone(), }); } - "volatile_load" | "unaligned_volatile_load" => { - assert_eq!( - args.len(), - 1, - "Unexpected number of arguments for `volatile_load`" - ); - assert!(matches!( - args[0].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) - )); + Intrinsic::VolatileLoad | Intrinsic::UnalignedVolatileLoad => { self.push_target(MemoryInitOp::Check { operand: args[0].clone(), }); } - "volatile_store" => { - assert_eq!( - args.len(), - 2, - "Unexpected number of arguments for `volatile_store`" - ); - assert!(matches!( - args[0].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) - )); + Intrinsic::VolatileStore => { self.push_target(MemoryInitOp::Set { operand: args[0].clone(), value: true, position: InsertPosition::After, }); } - "write_bytes" => { - assert_eq!( - args.len(), - 3, - "Unexpected number of arguments for `write_bytes`" - ); - assert!(matches!( - args[0].ty(&self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) - )); + Intrinsic::WriteBytes => { self.push_target(MemoryInitOp::SetSliceChunk { operand: args[0].clone(), count: args[2].clone(), @@ -328,7 +273,7 @@ impl MirVisitor for CheckUninitVisitor { } intrinsic => { self.push_target(MemoryInitOp::Unsupported { - reason: format!("Kani does not support reasoning about memory initialization of intrinsic `{intrinsic}`."), + reason: format!("Kani does not support reasoning about memory initialization of intrinsic `{intrinsic:?}`."), }); } } @@ -519,132 +464,131 @@ impl MirVisitor for CheckUninitVisitor { /// Determines if the intrinsic has no memory initialization related function and hence can be /// safely skipped. -fn can_skip_intrinsic(intrinsic_name: &str) -> bool { - match intrinsic_name { - "add_with_overflow" - | "arith_offset" - | "assert_inhabited" - | "assert_mem_uninitialized_valid" - | "assert_zero_valid" - | "assume" - | "bitreverse" - | "black_box" - | "breakpoint" - | "bswap" - | "caller_location" - | "ceilf32" - | "ceilf64" - | "copysignf32" - | "copysignf64" - | "cosf32" - | "cosf64" - | "ctlz" - | "ctlz_nonzero" - | "ctpop" - | "cttz" - | "cttz_nonzero" - | "discriminant_value" - | "exact_div" - | "exp2f32" - | "exp2f64" - | "expf32" - | "expf64" - | "fabsf32" - | "fabsf64" - | "fadd_fast" - | "fdiv_fast" - | "floorf32" - | "floorf64" - | "fmaf32" - | "fmaf64" - | "fmul_fast" - | "forget" - | "fsub_fast" - | "is_val_statically_known" - | "likely" - | "log10f32" - | "log10f64" - | "log2f32" - | "log2f64" - | "logf32" - | "logf64" - | "maxnumf32" - | "maxnumf64" - | "min_align_of" - | "min_align_of_val" - | "minnumf32" - | "minnumf64" - | "mul_with_overflow" - | "nearbyintf32" - | "nearbyintf64" - | "needs_drop" - | "powf32" - | "powf64" - | "powif32" - | "powif64" - | "pref_align_of" - | "raw_eq" - | "rintf32" - | "rintf64" - | "rotate_left" - | "rotate_right" - | "roundf32" - | "roundf64" - | "saturating_add" - | "saturating_sub" - | "sinf32" - | "sinf64" - | "sqrtf32" - | "sqrtf64" - | "sub_with_overflow" - | "truncf32" - | "truncf64" - | "type_id" - | "type_name" - | "unchecked_div" - | "unchecked_rem" - | "unlikely" - | "vtable_size" - | "vtable_align" - | "wrapping_add" - | "wrapping_mul" - | "wrapping_sub" => { +fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool { + match intrinsic { + Intrinsic::AddWithOverflow + | Intrinsic::ArithOffset + | Intrinsic::AssertInhabited + | Intrinsic::AssertMemUninitializedValid + | Intrinsic::AssertZeroValid + | Intrinsic::Assume + | Intrinsic::Bitreverse + | Intrinsic::BlackBox + | Intrinsic::Breakpoint + | Intrinsic::Bswap + | Intrinsic::CeilF32 + | Intrinsic::CeilF64 + | Intrinsic::CopySignF32 + | Intrinsic::CopySignF64 + | Intrinsic::CosF32 + | Intrinsic::CosF64 + | Intrinsic::Ctlz + | Intrinsic::CtlzNonZero + | Intrinsic::Ctpop + | Intrinsic::Cttz + | Intrinsic::CttzNonZero + | Intrinsic::DiscriminantValue + | Intrinsic::ExactDiv + | Intrinsic::Exp2F32 + | Intrinsic::Exp2F64 + | Intrinsic::ExpF32 + | Intrinsic::ExpF64 + | Intrinsic::FabsF32 + | Intrinsic::FabsF64 + | Intrinsic::FaddFast + | Intrinsic::FdivFast + | Intrinsic::FloorF32 + | Intrinsic::FloorF64 + | Intrinsic::FmafF32 + | Intrinsic::FmafF64 + | Intrinsic::FmulFast + | Intrinsic::Forget + | Intrinsic::FsubFast + | Intrinsic::IsValStaticallyKnown + | Intrinsic::Likely + | Intrinsic::Log10F32 + | Intrinsic::Log10F64 + | Intrinsic::Log2F32 + | Intrinsic::Log2F64 + | Intrinsic::LogF32 + | Intrinsic::LogF64 + | Intrinsic::MaxNumF32 + | Intrinsic::MaxNumF64 + | Intrinsic::MinAlignOf + | Intrinsic::MinAlignOfVal + | Intrinsic::MinNumF32 + | Intrinsic::MinNumF64 + | Intrinsic::MulWithOverflow + | Intrinsic::NearbyIntF32 + | Intrinsic::NearbyIntF64 + | Intrinsic::NeedsDrop + | Intrinsic::PowF32 + | Intrinsic::PowF64 + | Intrinsic::PowIF32 + | Intrinsic::PowIF64 + | Intrinsic::PrefAlignOf + | Intrinsic::RawEq + | Intrinsic::RintF32 + | Intrinsic::RintF64 + | Intrinsic::RotateLeft + | Intrinsic::RotateRight + | Intrinsic::RoundF32 + | Intrinsic::RoundF64 + | Intrinsic::SaturatingAdd + | Intrinsic::SaturatingSub + | Intrinsic::SinF32 + | Intrinsic::SinF64 + | Intrinsic::SqrtF32 + | Intrinsic::SqrtF64 + | Intrinsic::SubWithOverflow + | Intrinsic::TruncF32 + | Intrinsic::TruncF64 + | Intrinsic::TypeId + | Intrinsic::TypeName + | Intrinsic::UncheckedDiv + | Intrinsic::UncheckedRem + | Intrinsic::Unlikely + | Intrinsic::VtableSize + | Intrinsic::VtableAlign + | Intrinsic::WrappingAdd + | Intrinsic::WrappingMul + | Intrinsic::WrappingSub => { /* Intrinsics that do not interact with memory initialization. */ true } - "ptr_guaranteed_cmp" | "ptr_offset_from" | "ptr_offset_from_unsigned" | "size_of_val" => { + Intrinsic::PtrGuaranteedCmp + | Intrinsic::PtrOffsetFrom + | Intrinsic::PtrOffsetFromUnsigned + | Intrinsic::SizeOfVal => { /* AFAICS from the documentation, none of those require the pointer arguments to be actually initialized. */ true } - name if name.starts_with("simd") => { + Intrinsic::SimdAdd + | Intrinsic::SimdAnd + | Intrinsic::SimdDiv + | Intrinsic::SimdRem + | Intrinsic::SimdEq + | Intrinsic::SimdExtract + | Intrinsic::SimdGe + | Intrinsic::SimdGt + | Intrinsic::SimdInsert + | Intrinsic::SimdLe + | Intrinsic::SimdLt + | Intrinsic::SimdMul + | Intrinsic::SimdNe + | Intrinsic::SimdOr + | Intrinsic::SimdShl + | Intrinsic::SimdShr + | Intrinsic::SimdShuffle(_) + | Intrinsic::SimdSub + | Intrinsic::SimdXor => { /* SIMD operations */ true } - name if name.starts_with("atomic_fence") - || name.starts_with("atomic_singlethreadfence") => - { + Intrinsic::AtomicFence(_) | Intrinsic::AtomicSingleThreadFence(_) => { /* Atomic fences */ true } - "copy_nonoverlapping" => unreachable!( - "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`" - ), - "offset" => unreachable!( - "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`" - ), - "unreachable" => unreachable!( - "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`" - ), - "transmute" | "transmute_copy" | "unchecked_add" | "unchecked_mul" | "unchecked_shl" - | "size_of" | "unchecked_shr" | "unchecked_sub" => { - unreachable!("Expected intrinsic to be lowered before codegen") - } - "catch_unwind" => { - unimplemented!("") - } - "retag_box_to_raw" => { - unreachable!("This was removed in the latest Rust version.") - } _ => { /* Everything else */ false diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 7f1fb144a09b..e47483fb4fa5 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -39,6 +39,7 @@ extern crate tempfile; mod args; #[cfg(feature = "cprover")] mod codegen_cprover_gotoc; +mod intrinsics; mod kani_compiler; mod kani_middle; mod kani_queries;