From b6e4972b303b21fdbbd92af522409de4e10a628f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 11 Jun 2024 19:28:07 +0200 Subject: [PATCH 1/5] Pointers-out-of-scope test no longer is "fixme" (#3252) We handle these adequately as of 0cc4b2463828. Resolves: #77 --- .../dead-invalid-access-via-raw/{expected => main.expected} | 0 tests/expected/dead-invalid-access-via-raw/value.expected | 2 ++ .../dead-invalid-access-via-raw/value.rs} | 1 - 3 files changed, 2 insertions(+), 1 deletion(-) rename tests/expected/dead-invalid-access-via-raw/{expected => main.expected} (100%) create mode 100644 tests/expected/dead-invalid-access-via-raw/value.expected rename tests/{kani/Pointers_OutOfScopeFail/fixme_main.rs => expected/dead-invalid-access-via-raw/value.rs} (96%) diff --git a/tests/expected/dead-invalid-access-via-raw/expected b/tests/expected/dead-invalid-access-via-raw/main.expected similarity index 100% rename from tests/expected/dead-invalid-access-via-raw/expected rename to tests/expected/dead-invalid-access-via-raw/main.expected diff --git a/tests/expected/dead-invalid-access-via-raw/value.expected b/tests/expected/dead-invalid-access-via-raw/value.expected new file mode 100644 index 000000000000..858d44d54ea4 --- /dev/null +++ b/tests/expected/dead-invalid-access-via-raw/value.expected @@ -0,0 +1,2 @@ +Failed Checks: assertion failed: *p_subscoped == 7 +Failed Checks: dereference failure: dead object diff --git a/tests/kani/Pointers_OutOfScopeFail/fixme_main.rs b/tests/expected/dead-invalid-access-via-raw/value.rs similarity index 96% rename from tests/kani/Pointers_OutOfScopeFail/fixme_main.rs rename to tests/expected/dead-invalid-access-via-raw/value.rs index 5bbcb93930bb..6160325174b7 100644 --- a/tests/kani/Pointers_OutOfScopeFail/fixme_main.rs +++ b/tests/expected/dead-invalid-access-via-raw/value.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-verify-fail #[kani::proof] fn main() { From ca110f7b2c1d7cf219595863ef355713b306dc28 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 11 Jun 2024 12:12:04 -0700 Subject: [PATCH 2/5] Fix a few issues with std verification (#3255) - Contracts cannot duplicate some attributes. I think we need a better solution than just duplicate all attributes, but for now just filter the ones we know are problematic. - Do not make contract generated functions `const` when annotating constant functions. - I also moved the compilation of no_core up since it is much faster. ## Call-out Need to add a test. Resolves #3251 Resolves #3254 --- kani-driver/src/call_cargo.rs | 15 +- library/kani_core/src/lib.rs | 83 ++++- library/kani_core/src/mem.rs | 313 ++++++++++++++++++ .../src/sysroot/contracts/bootstrap.rs | 2 + .../src/sysroot/contracts/check.rs | 2 + .../kani_macros/src/sysroot/contracts/mod.rs | 10 +- .../src/sysroot/contracts/replace.rs | 2 + .../src/sysroot/contracts/shared.rs | 27 ++ .../function-contract/const_fn.expected | 2 + tests/expected/function-contract/const_fn.rs | 16 + .../verify_std_cmd/verify_std.sh | 3 + tools/build-kani/src/sysroot.rs | 4 +- 12 files changed, 466 insertions(+), 13 deletions(-) create mode 100644 library/kani_core/src/mem.rs create mode 100644 tests/expected/function-contract/const_fn.expected create mode 100644 tests/expected/function-contract/const_fn.rs diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index ade9785b8fdd..4e8e83b562af 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -84,8 +84,19 @@ impl KaniSession { .env("CARGO_TERM_PROGRESS_WHEN", "never") .env("__CARGO_TESTS_ONLY_SRC_ROOT", std_path.as_os_str()); - let build_artifacts = self.run_build(cmd)?; - Ok(build_artifacts.into_iter().filter_map(map_kani_artifact).collect()) + Ok(self + .run_build(cmd)? + .into_iter() + .filter_map(|artifact| { + if artifact.target.crate_types.contains(&CRATE_TYPE_LIB.to_string()) + || artifact.target.crate_types.contains(&CRATE_TYPE_RLIB.to_string()) + { + map_kani_artifact(artifact) + } else { + None + } + }) + .collect()) } /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir` diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index c31e964eeb0a..05ccb91eacb6 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -19,6 +19,7 @@ #![no_core] mod arbitrary; +mod mem; pub use kani_macros::*; @@ -34,15 +35,21 @@ macro_rules! kani_lib { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] pub mod kani { - pub use kani_core::{ensures, proof, proof_for_contract, requires, should_panic}; - kani_core::kani_intrinsics!(); + pub use kani_core::{ + ensures, modifies, proof, proof_for_contract, requires, should_panic, + }; + kani_core::kani_intrinsics!(core); kani_core::generate_arbitrary!(core); + + pub mod mem { + kani_core::kani_mem!(core); + } } }; (kani) => { pub use kani_core::*; - kani_core::kani_intrinsics!(); + kani_core::kani_intrinsics!(std); kani_core::generate_arbitrary!(std); }; } @@ -54,7 +61,7 @@ macro_rules! kani_lib { /// TODO: Use this inside kani library so that we dont have to maintain two copies of the same intrinsics. #[macro_export] macro_rules! kani_intrinsics { - () => { + ($core:tt) => { /// 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. @@ -262,6 +269,74 @@ macro_rules! kani_intrinsics { } pub mod internal { + + /// Helper trait for code generation for `modifies` contracts. + /// + /// We allow the user to provide us with a pointer-like object that we convert as needed. + #[doc(hidden)] + pub trait Pointer<'a> { + /// Type of the pointed-to data + type Inner; + + /// Used for checking assigns contracts where we pass immutable references to the function. + /// + /// We're using a reference to self here, because the user can use just a plain function + /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it. + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; + + /// used for havocking on replecement of a `modifies` clause. + unsafe fn assignable(self) -> &'a mut Self::Inner; + } + + impl<'a, 'b, T> Pointer<'a> for &'b T { + type Inner = T; + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + $core::mem::transmute(*self) + } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn assignable(self) -> &'a mut Self::Inner { + $core::mem::transmute(self as *const T) + } + } + + impl<'a, 'b, T> Pointer<'a> for &'b mut T { + type Inner = T; + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + $core::mem::transmute::<_, &&'a T>(self) + } + + unsafe fn assignable(self) -> &'a mut Self::Inner { + $core::mem::transmute(self) + } + } + + impl<'a, T> Pointer<'a> for *const T { + type Inner = T; + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + &**self as &'a T + } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn assignable(self) -> &'a mut Self::Inner { + $core::mem::transmute(self) + } + } + + impl<'a, T> Pointer<'a> for *mut T { + type Inner = T; + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + &**self as &'a T + } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn assignable(self) -> &'a mut Self::Inner { + $core::mem::transmute(self) + } + } + /// A way to break the ownerhip rules. Only used by contracts where we can /// guarantee it is done safely. #[inline(never)] diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs new file mode 100644 index 000000000000..8dd4a27cb03a --- /dev/null +++ b/library/kani_core/src/mem.rs @@ -0,0 +1,313 @@ +// 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. + +#[macro_export] +macro_rules! kani_mem { + ($core:tt) => { + use super::kani_intrinsic; + use private::Internal; + use $core::mem::{align_of, size_of}; + use $core::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. + // TODO: Add this back! We might need to rename the attribute. + //#[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. + // TODO: Add this back! We might need to rename the attribute. + //#[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(); + metadata.is_ptr_aligned(thin_ptr, Internal) + && is_inbounds(&metadata, thin_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. + // TODO: Add this back! We might need to rename the attribute. + //#[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(); + is_inbounds(&metadata, thin_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 + 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() + } + + /// Get the object ID of the given pointer. + #[rustc_diagnostic_item = "KaniPointerObject"] + #[inline(never)] + pub fn pointer_object(_ptr: *const T) -> usize { + kani_intrinsic() + } + + /// Get the object offset of the given pointer. + #[rustc_diagnostic_item = "KaniPointerOffset"] + #[inline(never)] + pub fn pointer_offset(_ptr: *const T) -> usize { + kani_intrinsic() + } + }; +} diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 6a48bab08070..dee0bca42c54 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -74,6 +74,8 @@ impl<'a> ContractConditionsHandler<'a> { let mut wrapper_sig = sig.clone(); wrapper_sig.ident = recursion_wrapper_name; + // We use non-constant functions, thus, the wrapper cannot be constant. + wrapper_sig.constness = None; let args = pats_to_idents(&mut wrapper_sig.inputs).collect::>(); let also_args = args.iter(); diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 473535e8d8fd..bd4c09b07796 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -120,6 +120,8 @@ impl<'a> ContractConditionsHandler<'a> { } let body = self.make_check_body(); let mut sig = self.annotated_fn.sig.clone(); + // We use non-constant functions, thus, the wrapper cannot be constant. + sig.constness = None; if let Some(ident) = override_function_dent { sig.ident = ident; } diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index de3b5da123ed..7a25cc390100 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -36,12 +36,12 @@ //! expanded. When we expand the first (outermost) `requires` or `ensures` //! attribute on such a function we re-emit the function unchanged but we also //! generate fresh "check" and "replace" functions that enforce the condition -//! carried by the attribute currently being expanded. We copy all additional -//! attributes from the original function to both the "check" and the "replace". -//! This allows us to deal both with renaming and also support non-contract -//! attributes. +//! carried by the attribute currently being expanded. //! -//! In addition to copying attributes we also add new marker attributes to +//! We don't copy all attributes from the original function since they may have +//! unintended consequences for the stubs, such as `inline` or `rustc_diagnostic_item`. +//! +//! We also add new marker attributes to //! advance the state machine. The "check" function gets a //! `kanitool::is_contract_generated(check)` attributes and analogous for //! replace. The re-emitted original meanwhile is decorated with diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 546568dc8a1d..1a84e40523c2 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -116,6 +116,8 @@ impl<'a> ContractConditionsHandler<'a> { self.output.extend(quote!(#[kanitool::is_contract_generated(replace)])); } let mut sig = self.annotated_fn.sig.clone(); + // We use non-constant functions, thus, the wrapper cannot be constant. + sig.constness = None; let body = self.make_replace_body(); if let Some(ident) = override_function_ident { sig.ident = ident; diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 3bef8b68f688..ed6b5467b260 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -53,7 +53,34 @@ impl<'a> ContractConditionsHandler<'a> { #[allow(dead_code, unused_variables, unused_mut)] )); } + + #[cfg(not(feature = "no_core"))] self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream)); + + // When verifying core and standard library, we need to add an unstable attribute to + // the functions generated by Kani. + // We also need to filter `rustc_diagnostic_item` attribute. + // We should consider a better strategy than just duplicating all attributes. + #[cfg(feature = "no_core")] + { + self.output.extend(quote!( + #[unstable(feature="kani", issue="none")] + )); + self.output.extend( + self.annotated_fn + .attrs + .iter() + .filter(|attr| { + if let Some(ident) = attr.path().get_ident() { + let name = ident.to_string(); + !name.starts_with("rustc") && !(name == "stable") + } else { + true + } + }) + .flat_map(Attribute::to_token_stream), + ); + } } } diff --git a/tests/expected/function-contract/const_fn.expected b/tests/expected/function-contract/const_fn.expected new file mode 100644 index 000000000000..10cf9fe451f0 --- /dev/null +++ b/tests/expected/function-contract/const_fn.expected @@ -0,0 +1,2 @@ +Checking harness check... +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/const_fn.rs b/tests/expected/function-contract/const_fn.rs new file mode 100644 index 000000000000..44b937cedce4 --- /dev/null +++ b/tests/expected/function-contract/const_fn.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zmem-predicates + +//! Check that Kani contract can be applied to a constant function. +//! + +#[kani::requires(kani::mem::can_dereference(arg))] +const unsafe fn dummy(arg: *const T) -> T { + std::ptr::read(arg) +} + +#[kani::proof_for_contract(dummy)] +fn check() { + unsafe { dummy(&kani::any::()) }; +} 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 9897a036dd22..0cc2bab48429 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -40,7 +40,10 @@ pub mod verify { fake_function(true); } + /// Add a `rustc_diagnostic_item` to ensure this works. + /// See for more details. #[kani::requires(x == true)] + #[rustc_diagnostic_item = "fake_function"] fn fake_function(x: bool) -> bool { x } diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index 4f2265515762..ca42fea3f441 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -75,9 +75,9 @@ fn build_target() -> &'static str { /// - The `lib-playback/` folder contains the sysroot used for playback. pub fn build_lib(bin_folder: &Path) -> Result<()> { let compiler_path = bin_folder.join("kani-compiler"); + build_no_core_lib(&compiler_path)?; build_verification_lib(&compiler_path)?; - build_playback_lib(&compiler_path)?; - build_no_core_lib(&compiler_path) + build_playback_lib(&compiler_path) } /// Build the `lib/` folder for the new sysroot used during verification. From 34b35d8bfb10b4520ac0d738e29d62544aecc2de Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 11 Jun 2024 22:28:14 -0700 Subject: [PATCH 3/5] Fix contract of constant fn with effect feature (#3259) We now check if the host effect index is present. If so, remove it before performing stub operation. Resolves #3258 --- kani-compiler/src/kani_middle/stubbing/mod.rs | 41 ++++++++++++++++--- .../src/kani_middle/transform/stubs.rs | 8 +++- .../const_fn_with_effect.expected | 2 + .../function-contract/const_fn_with_effect.rs | 18 ++++++++ .../verify_std_cmd/verify_std.expected | 5 ++- .../verify_std_cmd/verify_std.sh | 13 ++++++ 6 files changed, 78 insertions(+), 9 deletions(-) create mode 100644 tests/expected/function-contract/const_fn_with_effect.expected create mode 100644 tests/expected/function-contract/const_fn_with_effect.rs diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 1abcc0ec4f80..f21a02b7681e 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -17,7 +17,7 @@ use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, MirVisitor}; use stable_mir::mir::Constant; -use stable_mir::ty::FnDef; +use stable_mir::ty::{FnDef, RigidTy, TyKind}; use stable_mir::{CrateDef, CrateItem}; use self::annotations::update_stub_mapping; @@ -37,6 +37,24 @@ pub fn harness_stub_map( stub_pairs } +/// Retrieve the index of the host parameter if old definition has one, but not the new definition. +/// +/// This is to allow constant functions to be stubbed by non-constant functions when the +/// `effect` feature is on. +/// +/// Note that the opposite is not supported today, but users should be able to change their stubs. +/// +/// Note that this has no effect at runtime. +pub fn contract_host_param(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Option { + let old_generics = tcx.generics_of(rustc_internal::internal(tcx, old_def.def_id())); + let new_generics = tcx.generics_of(rustc_internal::internal(tcx, new_def.def_id())); + if old_generics.host_effect_index.is_some() && new_generics.host_effect_index.is_none() { + old_generics.host_effect_index + } else { + None + } +} + /// Checks whether the stub is compatible with the original function/method: do /// the arities and types (of the parameters and return values) match up? This /// does **NOT** check whether the type variables are constrained to implement @@ -61,15 +79,26 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul // Check whether the numbers of generic parameters match. let old_def_id = rustc_internal::internal(tcx, old_def.def_id()); let new_def_id = rustc_internal::internal(tcx, new_def.def_id()); - let old_num_generics = tcx.generics_of(old_def_id).count(); - let stub_num_generics = tcx.generics_of(new_def_id).count(); - if old_num_generics != stub_num_generics { + let old_ty = rustc_internal::stable(tcx.type_of(old_def_id)).value; + let new_ty = rustc_internal::stable(tcx.type_of(new_def_id)).value; + let TyKind::RigidTy(RigidTy::FnDef(_, mut old_args)) = old_ty.kind() else { + unreachable!("Expected function, but found {old_ty}") + }; + let TyKind::RigidTy(RigidTy::FnDef(_, new_args)) = new_ty.kind() else { + unreachable!("Expected function, but found {new_ty}") + }; + if let Some(idx) = contract_host_param(tcx, old_def, new_def) { + old_args.0.remove(idx); + } + + // TODO: We should check for the parameter type too or replacement will fail. + if old_args.0.len() != new_args.0.len() { let msg = format!( "mismatch in the number of generic parameters: original function/method `{}` takes {} generic parameters(s), stub `{}` takes {}", old_def.name(), - old_num_generics, + old_args.0.len(), new_def.name(), - stub_num_generics + new_args.0.len(), ); return Err(msg); } diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 7c4319319b8e..53db34dc902f 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -3,7 +3,7 @@ //! This module contains code related to the MIR-to-MIR pass that performs the //! stubbing of functions and methods. use crate::kani_middle::codegen_units::Stubs; -use crate::kani_middle::stubbing::validate_stub_const; +use crate::kani_middle::stubbing::{contract_host_param, validate_stub_const}; use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; @@ -46,8 +46,12 @@ impl TransformPass for FnStubPass { fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { trace!(function=?instance.name(), "transform"); let ty = instance.ty(); - if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = ty.kind() { + if let TyKind::RigidTy(RigidTy::FnDef(fn_def, mut args)) = ty.kind() { if let Some(replace) = self.stubs.get(&fn_def) { + if let Some(idx) = contract_host_param(tcx, fn_def, *replace) { + debug!(?idx, "FnStubPass::transform remove_host_param"); + args.0.remove(idx); + } let new_instance = Instance::resolve(*replace, &args).unwrap(); debug!(from=?instance.name(), to=?new_instance.name(), "FnStubPass::transform"); if let Some(body) = FnStubValidator::validate(tcx, (fn_def, *replace), new_instance) diff --git a/tests/expected/function-contract/const_fn_with_effect.expected b/tests/expected/function-contract/const_fn_with_effect.expected new file mode 100644 index 000000000000..10cf9fe451f0 --- /dev/null +++ b/tests/expected/function-contract/const_fn_with_effect.expected @@ -0,0 +1,2 @@ +Checking harness check... +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/const_fn_with_effect.rs b/tests/expected/function-contract/const_fn_with_effect.rs new file mode 100644 index 000000000000..d57c1f42fe16 --- /dev/null +++ b/tests/expected/function-contract/const_fn_with_effect.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zmem-predicates + +//! Check that Kani contract can be applied to a constant function. +//! + +#![feature(effects)] + +#[kani::requires(kani::mem::can_dereference(arg))] +const unsafe fn dummy(arg: *const T) -> T { + std::ptr::read(arg) +} + +#[kani::proof_for_contract(dummy)] +fn check() { + unsafe { dummy(&kani::any::()) }; +} diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected index 449148c5d904..aa30da375dd3 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -6,7 +6,10 @@ VERIFICATION:- SUCCESSFUL Checking harness verify::harness... VERIFICATION:- SUCCESSFUL +Checking harness verify::check_dummy_read... +VERIFICATION:- SUCCESSFUL + Checking harness num::verify::check_non_zero... VERIFICATION:- SUCCESSFUL -Complete - 3 successfully verified harnesses, 0 failures, 3 total. +Complete - 4 successfully verified harnesses, 0 failures, 4 total. 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 0cc2bab48429..3253ad29756e 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -47,6 +47,19 @@ pub mod verify { fn fake_function(x: bool) -> bool { x } + + #[kani::proof_for_contract(dummy_read)] + fn check_dummy_read() { + let val: char = kani::any(); + assert_eq!(unsafe { dummy_read(&val) }, val); + } + + /// Ensure we can verify constant functions. + #[kani::requires(kani::mem::can_dereference(ptr))] + #[rustc_diagnostic_item = "dummy_read"] + const unsafe fn dummy_read(ptr: *const T) -> T { + *ptr + } } ' From db54783933b8f90e892a54a39a1a815007faca8d Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 12 Jun 2024 03:48:28 -0700 Subject: [PATCH 4/5] Fix a few more issues with the std library (#3261) - Enable Kani to use fallback fn body for intrinsics, so they can be verified. - Until is implemented, we have to check has_body and must_be_overridden - Export all kani_macro definitions. Rename `unstable` to avoid conflict with the Rust standard library one. - Dump stable mir body since transformations are made at that level. - I just did this as I was debugging things. Co-authored-by: Michael Tautschnig --- .../codegen_cprover_gotoc/codegen/operand.rs | 2 +- .../codegen/statement.rs | 22 ++++++++---- .../compiler_interface.rs | 2 +- kani-compiler/src/kani_middle/attributes.rs | 4 +-- kani-compiler/src/kani_middle/mod.rs | 30 ++++++++-------- kani-compiler/src/kani_middle/reachability.rs | 13 ++++++- library/kani/src/lib.rs | 2 ++ library/kani_core/src/arbitrary.rs | 2 ++ library/kani_core/src/lib.rs | 5 ++- library/kani_macros/src/lib.rs | 2 +- .../src/sysroot/contracts/shared.rs | 4 ++- tests/cargo-ui/unstable-attr/defs/src/lib.rs | 4 +-- tests/cargo-ui/unstable-attr/invalid/expected | 34 +++++++++---------- .../cargo-ui/unstable-attr/invalid/src/lib.rs | 8 ++--- 14 files changed, 80 insertions(+), 54 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index a7a3c43edbff..3b71cfec91c2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -614,7 +614,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Ensure that the given instance is in the symbol table, returning the symbol. fn codegen_func_symbol(&mut self, instance: Instance) -> &Symbol { - let sym = if instance.is_foreign_item() { + let sym = if instance.is_foreign_item() && !instance.has_body() { // Get the symbol that represents a foreign instance. self.codegen_foreign_fn(instance) } else { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 0c43f566e5ac..1e81cccd0c07 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -518,13 +518,21 @@ impl<'tcx> GotocCtx<'tcx> { if let Some(instance) = instance_opt && matches!(instance.kind, InstanceKind::Intrinsic) { - return self.codegen_funcall_of_intrinsic( - instance, - &args, - &destination, - target.map(|bb| bb), - span, - ); + let TyKind::RigidTy(RigidTy::FnDef(def, _)) = instance.ty().kind() else { + unreachable!("Expected function type for intrinsic: {instance:?}") + }; + // The compiler is currently transitioning how to handle intrinsic fallback body. + // Until https://github.com/rust-lang/project-stable-mir/issues/79 is implemented + // we have to check `must_be_overridden` and `has_body`. + if def.as_intrinsic().unwrap().must_be_overridden() || !instance.has_body() { + return self.codegen_funcall_of_intrinsic( + instance, + &args, + &destination, + target.map(|bb| bb), + span, + ); + } } let loc = self.codegen_span_stable(span); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index ca66e1c0e165..6e2d5cb46e96 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -93,7 +93,7 @@ impl GotocCodegenBackend { || collect_reachable_items(tcx, &mut transformer, starting_items), "codegen reachability analysis", ); - dump_mir_items(tcx, &items, &symtab_goto.with_extension("kani.mir")); + dump_mir_items(tcx, &mut transformer, &items, &symtab_goto.with_extension("kani.mir")); // Follow rustc naming convention (cx is abbrev for context). // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index a9c777d84506..c74f0c744093 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -782,10 +782,10 @@ impl<'a> UnstableAttrParseError<'a> { tcx.dcx() .struct_span_err( self.attr.span, - format!("failed to parse `#[kani::unstable]`: {}", self.reason), + format!("failed to parse `#[kani::unstable_feature]`: {}", self.reason), ) .with_note(format!( - "expected format: #[kani::unstable({}, {}, {})]", + "expected format: #[kani::unstable_feature({}, {}, {})]", r#"feature="""#, r#"issue="""#, r#"reason="""# )) .emit() diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 257d337cd576..ce9a80fe1f80 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -6,9 +6,9 @@ use std::collections::HashSet; use std::path::Path; +use crate::kani_middle::transform::BodyTransformation; use crate::kani_queries::QueryDb; use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE}; -use rustc_middle::mir::write_mir_pretty; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, @@ -21,9 +21,9 @@ use rustc_span::source_map::respan; use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; -use stable_mir::mir::mono::{InstanceKind, MonoItem}; +use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, TyKind}; -use stable_mir::{CrateDef, DefId}; +use stable_mir::CrateDef; use std::fs::File; use std::io::BufWriter; use std::io::Write; @@ -93,17 +93,19 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) } /// Print MIR for the reachable items if the `--emit mir` option was provided to rustc. -pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { +pub fn dump_mir_items( + tcx: TyCtxt, + transformer: &mut BodyTransformation, + items: &[MonoItem], + output: &Path, +) { /// Convert MonoItem into a DefId. /// Skip stuff that we cannot generate the MIR items. - fn visible_item(item: &MonoItem) -> Option<(MonoItem, DefId)> { + fn get_instance(item: &MonoItem) -> Option { match item { // Exclude FnShims and others that cannot be dumped. - MonoItem::Fn(instance) if matches!(instance.kind, InstanceKind::Item) => { - Some((item.clone(), instance.def.def_id())) - } - MonoItem::Fn(..) => None, - MonoItem::Static(def) => Some((item.clone(), def.def_id())), + MonoItem::Fn(instance) => Some(*instance), + MonoItem::Static(def) => Some((*def).into()), MonoItem::GlobalAsm(_) => None, } } @@ -114,10 +116,10 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { let mut writer = BufWriter::new(out_file); // For each def_id, dump their MIR - for (item, def_id) in items.iter().filter_map(visible_item) { - writeln!(writer, "// Item: {item:?}").unwrap(); - write_mir_pretty(tcx, Some(rustc_internal::internal(tcx, def_id)), &mut writer) - .unwrap(); + for instance in items.iter().filter_map(get_instance) { + writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap(); + let body = transformer.body(tcx, instance); + let _ = body.dump(&mut writer, &instance.name()); } } } diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 9c6c7e0ec350..4ebff6868bf5 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -262,11 +262,22 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { /// Collect an instance depending on how it is used (invoked directly or via fn_ptr). fn collect_instance(&mut self, instance: Instance, is_direct_call: bool) { let should_collect = match instance.kind { - InstanceKind::Virtual { .. } | InstanceKind::Intrinsic => { + InstanceKind::Virtual { .. } => { // Instance definition has no body. assert!(is_direct_call, "Expected direct call {instance:?}"); false } + InstanceKind::Intrinsic => { + // Intrinsics may have a fallback body. + assert!(is_direct_call, "Expected direct call {instance:?}"); + let TyKind::RigidTy(RigidTy::FnDef(def, _)) = instance.ty().kind() else { + unreachable!("Expected function type for intrinsic: {instance:?}") + }; + // The compiler is currently transitioning how to handle intrinsic fallback body. + // Until https://github.com/rust-lang/project-stable-mir/issues/79 is implemented + // we have to check `must_be_overridden` and `has_body`. + !def.as_intrinsic().unwrap().must_be_overridden() && instance.has_body() + } InstanceKind::Shim | InstanceKind::Item => true, }; if should_collect && should_codegen_locally(&instance) { diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index e81ddbe7904b..acf1e08e0441 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -323,4 +323,6 @@ pub use core::assert as __kani__workaround_core_assert; // Kani proc macros must be in a separate crate pub use kani_macros::*; +pub(crate) use kani_macros::unstable_feature as unstable; + pub mod contracts; diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index e7ac4dc81508..d202df4ead1d 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -72,6 +72,8 @@ macro_rules! generate_arbitrary { } // Generate trivial arbitrary values + trivial_arbitrary!(()); + trivial_arbitrary!(u8); trivial_arbitrary!(u16); trivial_arbitrary!(u32); diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 05ccb91eacb6..de808ffaf918 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -35,9 +35,8 @@ macro_rules! kani_lib { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] pub mod kani { - pub use kani_core::{ - ensures, modifies, proof, proof_for_contract, requires, should_panic, - }; + // We need to list them all today because there is conflict with unstable. + pub use kani_core::*; kani_core::kani_intrinsics!(core); kani_core::generate_arbitrary!(core); diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 44a0ca78ea41..0a000910174a 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -96,7 +96,7 @@ pub fn solver(attr: TokenStream, item: TokenStream) -> TokenStream { /// See https://model-checking.github.io/kani/rfc/rfcs/0006-unstable-api.html for more details. #[doc(hidden)] #[proc_macro_attribute] -pub fn unstable(attr: TokenStream, item: TokenStream) -> TokenStream { +pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::unstable(attr, item) } diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index ed6b5467b260..bf204e6bca32 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -73,7 +73,9 @@ impl<'a> ContractConditionsHandler<'a> { .filter(|attr| { if let Some(ident) = attr.path().get_ident() { let name = ident.to_string(); - !name.starts_with("rustc") && !(name == "stable") + !name.starts_with("rustc") + && !(name == "stable") + && !(name == "unstable") } else { true } diff --git a/tests/cargo-ui/unstable-attr/defs/src/lib.rs b/tests/cargo-ui/unstable-attr/defs/src/lib.rs index 9515cf1d48a8..91b5a4d539bf 100644 --- a/tests/cargo-ui/unstable-attr/defs/src/lib.rs +++ b/tests/cargo-ui/unstable-attr/defs/src/lib.rs @@ -1,13 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -#[kani::unstable(feature = "always_fails", reason = "do not enable", issue = "")] +#[kani::unstable_feature(feature = "always_fails", reason = "do not enable", issue = "")] pub fn always_fails() { assert!(false, "don't call me"); } /// We use "gen-c" since it has to be an existing feature. -#[kani::unstable(feature = "gen-c", reason = "internal fake api", issue = "")] +#[kani::unstable_feature(feature = "gen-c", reason = "internal fake api", issue = "")] pub fn no_op() { kani::cover!(true); } diff --git a/tests/cargo-ui/unstable-attr/invalid/expected b/tests/cargo-ui/unstable-attr/invalid/expected index 49db2367b832..fd6ee1c694c2 100644 --- a/tests/cargo-ui/unstable-attr/invalid/expected +++ b/tests/cargo-ui/unstable-attr/invalid/expected @@ -1,32 +1,32 @@ -error: failed to parse `#[kani::unstable]`: missing `feature` field\ +error: failed to parse `#[kani::unstable_feature]`: missing `feature` field\ lib.rs |\ -9 | #[kani::unstable(reason = "just checking", issue = "")]\ - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ +9 | #[kani::unstable_feature(reason = "just checking", issue = "")]\ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ |\ - = note: expected format: #[kani::unstable(feature="", issue="", reason="")]\ - = note: this error originates in the attribute macro `kani::unstable` (in Nightly builds, run with -Z macro-backtrace for more info) + = note: expected format: #[kani::unstable_feature(feature="", issue="", reason="")]\ + = note: this error originates in the attribute macro `kani::unstable_feature` (in Nightly builds, run with -Z macro-backtrace for more info) -error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature("invalid_args")`\ +error: failed to parse `#[kani::unstable_feature]`: expected "key = value" pair, but found `feature("invalid_args")`\ lib.rs\ |\ -| #[kani::unstable(feature("invalid_args"))]\ -| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ +| #[kani::unstable_feature(feature("invalid_args"))]\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ |\ - = note: expected format: #[kani::unstable(feature="", issue="", reason="")] + = note: expected format: #[kani::unstable_feature(feature="", issue="", reason="")] -error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature`\ +error: failed to parse `#[kani::unstable_feature]`: expected "key = value" pair, but found `feature`\ lib.rs\ |\ -| #[kani::unstable(feature, issue)]\ -| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ +| #[kani::unstable_feature(feature, issue)]\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ |\ - = note: expected format: #[kani::unstable(feature="", issue="", reason="")] + = note: expected format: #[kani::unstable_feature(feature="", issue="", reason="")] -error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `1010`\ +error: failed to parse `#[kani::unstable_feature]`: expected "key = value" pair, but found `1010`\ lib.rs\ |\ -| #[kani::unstable(1010)]\ -| ^^^^^^^^^^^^^^^^^^^^^^^\ +| #[kani::unstable_feature(1010)]\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ |\ - = note: expected format: #[kani::unstable(feature="", issue="", reason="")] + = note: expected format: #[kani::unstable_feature(feature="", issue="", reason="")] diff --git a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs index 5fbfc768c883..f0d92f0882d7 100644 --- a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs +++ b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs @@ -6,18 +6,18 @@ //! we don't guarantee the order that these will be evaluated. //! TODO: We should break down this test to ensure all of these fail. -#[kani::unstable(reason = "just checking", issue = "")] +#[kani::unstable_feature(reason = "just checking", issue = "")] pub fn missing_feature() { todo!() } -#[kani::unstable(feature("invalid_args"))] +#[kani::unstable_feature(feature("invalid_args"))] pub fn invalid_fn_style() {} -#[kani::unstable(feature, issue)] +#[kani::unstable_feature(feature, issue)] pub fn invalid_list() {} -#[kani::unstable(1010)] +#[kani::unstable_feature(1010)] pub fn invalid_argument() {} #[kani::proof] From d588c011c88b82bb1a3bee2d4a17a0be89d7ce19 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 14:27:21 +0200 Subject: [PATCH 5/5] Fix typed_swap for ZSTs (#3256) typed_swap needs to be a no-op on ZSTs as pointers to those have an arbitrary value in Kani. Resolves: #3182 --- .../codegen/intrinsic.rs | 61 +++++++++++-------- tests/kani/Intrinsics/typed_swap.rs | 7 +++ tests/std-checks/core/src/mem.rs | 2 - 3 files changed, 43 insertions(+), 27 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 4e965b4105ef..942c39203083 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1880,12 +1880,11 @@ impl<'tcx> GotocCtx<'tcx> { "`dst` must be properly aligned", loc, ); - let deref = dst.dereference(); - if deref.typ().sizeof(&self.symbol_table) == 0 { + if self.is_zst_stable(pointee_type_stable(dst_typ).unwrap()) { // do not attempt to dereference (and assign) a ZST align_check } else { - let expr = deref.assign(src, loc); + let expr = dst.dereference().assign(src, loc); Stmt::block(vec![align_check, expr], loc) } } @@ -1991,30 +1990,42 @@ impl<'tcx> GotocCtx<'tcx> { let x = fargs.remove(0); let y = fargs.remove(0); - // if(same_object(x, y)) { - // assert(x + 1 <= y || y + 1 <= x); - // assume(x + 1 <= y || y + 1 <= x); - // } - let one = Expr::int_constant(1, Type::c_int()); - let non_overlapping = - x.clone().plus(one.clone()).le(y.clone()).or(y.clone().plus(one.clone()).le(x.clone())); - let non_overlapping_check = self.codegen_assert_assume( - non_overlapping, - PropertyClass::SafetyCheck, - "memory regions pointed to by `x` and `y` must not overlap", - loc, - ); - let non_overlapping_stmt = - Stmt::if_then_else(x.clone().same_object(y.clone()), non_overlapping_check, None, loc); + if self.is_zst_stable(pointee_type_stable(farg_types[0]).unwrap()) { + // do not attempt to dereference (and assign) a ZST + Stmt::skip(loc) + } else { + // if(same_object(x, y)) { + // assert(x + 1 <= y || y + 1 <= x); + // assume(x + 1 <= y || y + 1 <= x); + // } + let one = Expr::int_constant(1, Type::c_int()); + let non_overlapping = x + .clone() + .plus(one.clone()) + .le(y.clone()) + .or(y.clone().plus(one.clone()).le(x.clone())); + let non_overlapping_check = self.codegen_assert_assume( + non_overlapping, + PropertyClass::SafetyCheck, + "memory regions pointed to by `x` and `y` must not overlap", + loc, + ); + let non_overlapping_stmt = Stmt::if_then_else( + x.clone().same_object(y.clone()), + non_overlapping_check, + None, + loc, + ); - // T t = *y; *y = *x; *x = t; - let deref_y = y.clone().dereference(); - let (temp_var, assign_to_t) = - self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc); - let assign_to_y = y.dereference().assign(x.clone().dereference(), loc); - let assign_to_x = x.dereference().assign(temp_var, loc); + // T t = *y; *y = *x; *x = t; + let deref_y = y.clone().dereference(); + let (temp_var, assign_to_t) = + self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc); + let assign_to_y = y.dereference().assign(x.clone().dereference(), loc); + let assign_to_x = x.dereference().assign(temp_var, loc); - Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc) + Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc) + } } } diff --git a/tests/kani/Intrinsics/typed_swap.rs b/tests/kani/Intrinsics/typed_swap.rs index 4279bb713ece..996784b5181d 100644 --- a/tests/kani/Intrinsics/typed_swap.rs +++ b/tests/kani/Intrinsics/typed_swap.rs @@ -19,3 +19,10 @@ fn test_typed_swap_u32() { assert!(b == a_before); assert!(a == b_before); } + +#[kani::proof] +pub fn check_swap_unit() { + let mut x: () = kani::any(); + let mut y: () = kani::any(); + std::mem::swap(&mut x, &mut y) +} diff --git a/tests/std-checks/core/src/mem.rs b/tests/std-checks/core/src/mem.rs index 5ca439a18e1c..4f41d176a73a 100644 --- a/tests/std-checks/core/src/mem.rs +++ b/tests/std-checks/core/src/mem.rs @@ -45,8 +45,6 @@ mod verify { /// FIX-ME: Modifies clause fail with pointer to ZST. /// - /// FIX-ME: `typed_swap` intrisic fails for ZST. - /// #[kani::proof_for_contract(contracts::swap)] pub fn check_swap_unit() { let mut x: () = kani::any();