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/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() { 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.