From 185c6e652affa867d64d08771cd18f79fe69abb5 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 6 Feb 2024 19:00:58 -0800 Subject: [PATCH 1/4] Add method to assert a pointer is safe to access --- cprover_bindings/src/goto_program/expr.rs | 12 + cprover_bindings/src/irep/to_irep.rs | 5 + .../codegen_cprover_gotoc/overrides/hooks.rs | 36 +++ kani_metadata/src/unstable.rs | 2 + library/kani/src/lib.rs | 23 +- library/kani/src/mem.rs | 224 ++++++++++++++++++ tests/kani/MemPredicates/fat_ptr_validity.rs | 46 ++++ 7 files changed, 336 insertions(+), 12 deletions(-) create mode 100644 library/kani/src/mem.rs create mode 100644 tests/kani/MemPredicates/fat_ptr_validity.rs diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 09adbdb20df3..28f8afb4fae7 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -126,6 +126,10 @@ pub enum ExprValue { Nondet, /// `NULL` PointerConstant(u64), + ReadOk { + ptr: Expr, + size: Expr, + }, // `op++` etc SelfOp { op: SelfOperator, @@ -717,6 +721,14 @@ impl Expr { expr!(Nondet, typ) } + /// `read_ok(ptr, size)` + pub fn read_ok(ptr: Expr, size: Expr) -> Self { + assert_eq!(*ptr.typ(), Type::void_pointer()); + assert_eq!(*size.typ(), Type::size_t()); + + expr!(ReadOk { ptr, size }, Type::bool()) + } + /// `e.g. NULL` pub fn pointer_constant(c: u64, typ: Type) -> Self { assert!(typ.is_pointer()); diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 16b8b69c8fe7..bb282d7574f4 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -293,6 +293,11 @@ impl ToIrep for ExprValue { Irep::just_bitpattern_id(*i, mm.pointer_width, false) )], }, + ExprValue::ReadOk { ptr, size } => Irep { + id: IrepId::ROk, + sub: vec![ptr.to_irep(mm), size.to_irep(mm)], + named_sub: linear_map![], + }, ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]), ExprValue::StatementExpression { statements: ops } => side_effect_irep( IrepId::StatementExpression, diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 0141c2886539..eeb101c12547 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -217,6 +217,41 @@ impl GotocHook for Panic { } } +/// Encodes __CBMC_r_ok +struct IsReadOk; +impl GotocHook for IsReadOk { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + matches_function(tcx, instance, "KaniIsReadOk") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let size = fargs.pop().unwrap(); + let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer()); + let target = target.unwrap(); + let loc = gcx.codegen_caller_span_stable(span); + let ret_place = + unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to)); + let ret_type = ret_place.goto_expr.typ().clone(); + + Stmt::block( + vec![ + ret_place.goto_expr.assign(Expr::read_ok(ptr, size).cast_to(ret_type), loc), + Stmt::goto(bb_label(target), Location::none()), + ], + Location::none(), + ) + } +} + struct RustAlloc; // Removing this hook causes regression failures. // https://github.com/model-checking/kani/issues/1170 @@ -373,6 +408,7 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(Assert), Rc::new(Cover), Rc::new(Nondet), + Rc::new(IsReadOk), Rc::new(RustAlloc), Rc::new(MemCmp), Rc::new(UntrackedDeref), diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 060508666735..3820f3f2238e 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -82,6 +82,8 @@ pub enum UnstableFeature { LineCoverage, /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) FunctionContracts, + /// Memory predicate APIs. + MemPredicates, } impl UnstableFeature { diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 087e23c7d47e..e8482641c901 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -13,14 +13,18 @@ // Used to model simd. #![feature(repr_simd)] // Features used for tests only. -#![cfg_attr(test, feature(core_intrinsics, portable_simd))] -// Required for rustc_diagnostic_item +#![cfg_attr(test, feature(portable_simd))] +// Required for `rustc_diagnostic_item` and `core_intrinsics` #![allow(internal_features)] +// Required for implementing memory predicates. +#![feature(core_intrinsics)] +#![feature(ptr_metadata)] pub mod arbitrary; #[cfg(feature = "concrete_playback")] mod concrete_playback; pub mod futures; +pub mod mem; pub mod slice; pub mod tuple; pub mod vec; @@ -33,6 +37,7 @@ mod models; pub use arbitrary::Arbitrary; #[cfg(feature = "concrete_playback")] pub use concrete_playback::concrete_playback_run; + #[cfg(not(feature = "concrete_playback"))] /// NOP `concrete_playback` for type checking during verification mode. pub fn concrete_playback_run(_: Vec>, _: F) { @@ -80,18 +85,12 @@ pub fn assume(cond: bool) { /// `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 be used -/// in function contracts to make them more readable, as the concept of an -/// implication is more natural to think about than its expansion. -/// -/// For further convenience multiple comma separated premises are allowed, and -/// are joined with `||` in the expansion. E.g. `implies!(a, b => c)` expands to -/// `!a || !b || c` and says that `c` is true if both `a` and `b` are true (see -/// also [Horn Clauses](https://en.wikipedia.org/wiki/Horn_clause)). +/// 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) + ($premise:expr => $conclusion:expr) => { + !($premise) || ($conclusion) }; } diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs new file mode 100644 index 000000000000..bee8d18d2fb1 --- /dev/null +++ b/library/kani/src/mem.rs @@ -0,0 +1,224 @@ +// 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. +//! 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::mem::private::Internal; +use std::mem::{align_of, size_of}; +use std::ptr::{DynMetadata, NonNull, Pointee}; + +/// Assert that the pointer is valid for access according to [crate::mem] conditions 1, 2 and 3. +/// +/// TODO: Kani will automatically add those checks when a de-reference happens. +/// https://github.com/model-checking/kani/issues/2975 +/// +/// TODO: Add tests for nullptr, dangling, slice, trait, ZST, and sized objects. +/// +/// This function will either panic or return `true`. This is to make it easier to use it in +/// contracts. +#[crate::unstable( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" +)] +pub fn assert_valid_ptr(ptr: *const T) -> bool +where + T: ?Sized, + ::Metadata: PtrProperties, +{ + crate::assert(!ptr.is_null(), "Expected valid pointer, but found `null`"); + + let (thin_ptr, metadata) = ptr.to_raw_parts(); + metadata.can_read(thin_ptr, Internal) +} + +#[crate::unstable( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" +)] +pub fn is_ptr_aligned(ptr: *const T) -> bool +where + T: ?Sized, + ::Metadata: PtrProperties, +{ + let (thin_ptr, metadata) = ptr.to_raw_parts(); + thin_ptr as usize % metadata.min_alignment(Internal) == 0 +} + +mod private { + /// Define like this to restrict usage of PtrProperties functions outside Kani. + 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; + + fn min_alignment(&self, _: Internal) -> usize; + + fn can_read(&self, thin_ptr: *const (), _: Internal) -> bool { + crate::assert( + is_read_ok(thin_ptr, self.pointee_size(Internal)), + "Expected valid pointer, but found dangling pointer", + ); + true + } +} + +impl PtrProperties for () { + fn pointee_size(&self, _: Internal) -> usize { + size_of::() + } + + fn min_alignment(&self, _: Internal) -> usize { + align_of::() + } + + fn can_read(&self, thin_ptr: *const (), _: Internal) -> bool { + let sz = size_of::(); + if NonNull::::dangling().as_ptr() as *const _ as *const () == thin_ptr { + crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access") + } else { + crate::assert( + is_read_ok(thin_ptr, sz), + "Expected valid pointer, but found dangling pointer", + ); + } + true + } +} + +impl PtrProperties for usize { + 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::() + } +} + +impl PtrProperties<[T]> for usize { + fn pointee_size(&self, _: Internal) -> usize { + *self + } + + fn min_alignment(&self, _: Internal) -> usize { + align_of::() + } +} + +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() + } +} + +/// Check if the pointer `_ptr` contains an allocated address of size equal or greater than `_size`. +/// +/// This function should only be called to ensure a pointer is valid. The opposite isn't true. +/// I.e.: This function always returns `true` if the pointer is valid. +/// Otherwise, it returns non-det boolean. +#[rustc_diagnostic_item = "KaniIsReadOk"] +#[inline(never)] +fn is_read_ok(_ptr: *const (), _size: usize) -> bool { + // This will be replaced by Kani codegen. + #[allow(clippy::empty_loop)] + loop {} +} + +#[cfg(test)] +mod tests { + use super::PtrProperties; + use crate::mem::private::Internal; + use std::intrinsics::size_of; + use std::mem::{align_of, align_of_val, size_of_val}; + 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(&0u8 as *const dyn std::fmt::Display), align_of_val(&0u8)); + assert_eq!(align_of_t(&[0u8, 1u8] as &[u8]), align_of_val(&[0u8, 1u8])); + 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::() + ); + } +} diff --git a/tests/kani/MemPredicates/fat_ptr_validity.rs b/tests/kani/MemPredicates/fat_ptr_validity.rs new file mode 100644 index 000000000000..2d70197e8d8e --- /dev/null +++ b/tests/kani/MemPredicates/fat_ptr_validity.rs @@ -0,0 +1,46 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z mem-predicates +//! Check that Kani's memory predicates work for fat pointers. + +extern crate kani; + +use kani::mem::assert_valid_ptr; +use std::fmt::Debug; + +mod valid_access { + use super::*; + #[kani::proof] + pub fn check_valid_dyn_ptr() { + let boxed: Box> = Box::new(10u8); + let raw_ptr = Box::into_raw(boxed); + assert_valid_ptr(raw_ptr); + let boxed = unsafe { Box::from_raw(raw_ptr) }; + assert_ne!(*boxed, 0); + } + + #[kani::proof] + pub fn check_valid_slice_ptr() { + let array = ['a', 'b', 'c']; + let slice = &array as *const [char]; + assert_valid_ptr(slice); + assert_eq!(unsafe { &*slice }[0], 'a'); + assert_eq!(unsafe { &*slice }[2], 'c'); + } +} + +mod invalid_access { + use super::*; + #[kani::proof] + #[kani::should_panic] + pub fn check_invalid_dyn_ptr() { + let raw_ptr: *const dyn PartialEq = unsafe { new_dead_ptr::() }; + assert_valid_ptr(raw_ptr); + assert_eq!(*unsafe { &*raw_ptr }, 0u8); + } + + unsafe fn new_dead_ptr() -> *const T { + let var = T::default(); + &var as *const _ + } +} From 83dfcc61064662d0629c90ee52757a20ab61f46c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 7 Mar 2024 15:40:20 -0800 Subject: [PATCH 2/4] Add more tests and adjust a few issues with ZST --- library/kani/src/lib.rs | 25 ++-- library/kani/src/mem.rs | 132 +++++++++++++----- scripts/kani-regression.sh | 3 +- tests/kani/MemPredicates/fat_ptr_validity.rs | 35 ++++- tests/kani/MemPredicates/thin_ptr_validity.rs | 60 ++++++++ 5 files changed, 202 insertions(+), 53 deletions(-) create mode 100644 tests/kani/MemPredicates/thin_ptr_validity.rs diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index e8482641c901..e3d27c4b1bfb 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -13,11 +13,10 @@ // Used to model simd. #![feature(repr_simd)] // Features used for tests only. -#![cfg_attr(test, feature(portable_simd))] +#![cfg_attr(test, feature(core_intrinsics, portable_simd))] // Required for `rustc_diagnostic_item` and `core_intrinsics` #![allow(internal_features)] // Required for implementing memory predicates. -#![feature(core_intrinsics)] #![feature(ptr_metadata)] pub mod arbitrary; @@ -216,13 +215,7 @@ pub(crate) unsafe fn any_raw_internal() -> T { #[inline(never)] #[allow(dead_code)] fn any_raw_inner() -> T { - // while we could use `unreachable!()` or `panic!()` as the body of this - // function, both cause Kani to produce a warning on any program that uses - // kani::any() (see https://github.com/model-checking/kani/issues/2010). - // This function is 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. - #[allow(clippy::empty_loop)] - loop {} + kani_intrinsic() } /// Function used to generate panic with a static message as this is the only one currently @@ -238,6 +231,20 @@ pub const fn panic(message: &'static str) -> ! { panic!("{}", message) } +/// 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. /// diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index bee8d18d2fb1..065332017580 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -34,17 +34,18 @@ //! 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}; /// Assert that the pointer is valid for access according to [crate::mem] conditions 1, 2 and 3. /// +/// Note that a unaligned pointer is still considered valid. +/// /// TODO: Kani will automatically add those checks when a de-reference happens. /// https://github.com/model-checking/kani/issues/2975 /// -/// TODO: Add tests for nullptr, dangling, slice, trait, ZST, and sized objects. -/// /// This function will either panic or return `true`. This is to make it easier to use it in /// contracts. #[crate::unstable( @@ -60,25 +61,30 @@ where crate::assert(!ptr.is_null(), "Expected valid pointer, but found `null`"); let (thin_ptr, metadata) = ptr.to_raw_parts(); - metadata.can_read(thin_ptr, Internal) + can_read(&metadata, thin_ptr) } -#[crate::unstable( - feature = "mem-predicates", - issue = 2690, - reason = "experimental memory predicate API" -)] -pub fn is_ptr_aligned(ptr: *const T) -> bool +fn can_read(metadata: &M, data_ptr: *const ()) -> bool where + M: PtrProperties, T: ?Sized, - ::Metadata: PtrProperties, { - let (thin_ptr, metadata) = ptr.to_raw_parts(); - thin_ptr as usize % metadata.min_alignment(Internal) == 0 + let marker = Internal; + let sz = metadata.pointee_size(marker); + if metadata.dangling(marker) as *const _ == data_ptr { + crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access") + } else { + crate::assert( + is_read_ok(data_ptr, sz), + "Expected valid pointer, but found dangling pointer", + ); + } + true } mod private { /// Define like this to restrict usage of PtrProperties functions outside Kani. + #[derive(Copy, Clone)] pub struct Internal; } @@ -89,15 +95,10 @@ pub trait PtrProperties { fn min_alignment(&self, _: Internal) -> usize; - fn can_read(&self, thin_ptr: *const (), _: Internal) -> bool { - crate::assert( - is_read_ok(thin_ptr, self.pointee_size(Internal)), - "Expected valid pointer, but found dangling pointer", - ); - true - } + 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::() @@ -107,21 +108,14 @@ impl PtrProperties for () { align_of::() } - fn can_read(&self, thin_ptr: *const (), _: Internal) -> bool { - let sz = size_of::(); - if NonNull::::dangling().as_ptr() as *const _ as *const () == thin_ptr { - crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access") - } else { - crate::assert( - is_read_ok(thin_ptr, sz), - "Expected valid pointer, but found dangling pointer", - ); - } - true + 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 } @@ -132,18 +126,28 @@ impl PtrProperties for usize { 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 + *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, @@ -155,6 +159,10 @@ where 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`. @@ -165,17 +173,17 @@ where #[rustc_diagnostic_item = "KaniIsReadOk"] #[inline(never)] fn is_read_ok(_ptr: *const (), _size: usize) -> bool { - // This will be replaced by Kani codegen. - #[allow(clippy::empty_loop)] - loop {} + kani_intrinsic() } #[cfg(test)] mod tests { - use super::PtrProperties; + use super::{assert_valid_ptr, 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 @@ -213,12 +221,62 @@ mod tests { 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(&0u8 as *const dyn std::fmt::Display), align_of_val(&0u8)); - assert_eq!(align_of_t(&[0u8, 1u8] as &[u8]), align_of_val(&[0u8, 1u8])); + 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_slice() as *const [char]; + assert_valid_ptr(slice_ptr); + } + + #[test] + pub fn test_empty_str() { + let slice_ptr = String::new().as_str() as *const str; + assert_valid_ptr(slice_ptr); + } + + #[test] + fn test_dangling_zst() { + test_dangling_of_t::<()>(); + test_dangling_of_t::<[(); 10]>(); + } + + fn test_dangling_of_t() { + let dangling: *const T = NonNull::::dangling().as_ptr(); + assert_valid_ptr(dangling); + + let vec_ptr = Vec::::new().as_ptr(); + assert_valid_ptr(vec_ptr); + } + + #[test] + #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")] + fn test_dangling_char() { + test_dangling_of_t::(); + } + + #[test] + #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")] + fn test_dangling_slice() { + test_dangling_of_t::<&str>(); + } + + #[test] + #[should_panic(expected = "Expected valid pointer, but found `null`")] + fn test_null_fat_ptr() { + assert_valid_ptr(ptr::null::() as *const dyn Debug); + } + + #[test] + #[should_panic(expected = "Expected valid pointer, but found `null`")] + fn test_null_char() { + assert_valid_ptr(ptr::null::()); + } } diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 20782abe5cbc..3b029c475d5f 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -41,7 +41,8 @@ cargo test -p cprover_bindings cargo test -p kani-compiler cargo test -p kani-driver cargo test -p kani_metadata -cargo test -p kani --lib # skip doc tests. +# skip doc tests and enable assertions to fail +cargo test -p kani --lib --features concrete_playback # Test the actual macros, skipping doc tests and enabling extra traits for "syn" # so we can debug print AST RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib diff --git a/tests/kani/MemPredicates/fat_ptr_validity.rs b/tests/kani/MemPredicates/fat_ptr_validity.rs index 2d70197e8d8e..51d784f06566 100644 --- a/tests/kani/MemPredicates/fat_ptr_validity.rs +++ b/tests/kani/MemPredicates/fat_ptr_validity.rs @@ -6,7 +6,6 @@ extern crate kani; use kani::mem::assert_valid_ptr; -use std::fmt::Debug; mod valid_access { use super::*; @@ -27,6 +26,15 @@ mod valid_access { assert_eq!(unsafe { &*slice }[0], 'a'); assert_eq!(unsafe { &*slice }[2], 'c'); } + + #[kani::proof] + pub fn check_valid_zst() { + let slice_ptr = Vec::::new().as_slice() as *const [char]; + assert_valid_ptr(slice_ptr); + + let str_ptr = String::new().as_str() as *const str; + assert_valid_ptr(str_ptr); + } } mod invalid_access { @@ -34,13 +42,28 @@ mod invalid_access { #[kani::proof] #[kani::should_panic] pub fn check_invalid_dyn_ptr() { - let raw_ptr: *const dyn PartialEq = unsafe { new_dead_ptr::() }; + let raw_ptr: *const dyn PartialEq = unsafe { new_dead_ptr::(0) }; assert_valid_ptr(raw_ptr); - assert_eq!(*unsafe { &*raw_ptr }, 0u8); } - unsafe fn new_dead_ptr() -> *const T { - let var = T::default(); - &var as *const _ + #[kani::proof] + #[kani::should_panic] + pub fn check_invalid_slice_ptr() { + let raw_ptr: *const [char] = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) }; + assert_valid_ptr(raw_ptr); + } + + #[kani::proof] + #[kani::should_panic] + pub fn check_invalid_slice_len() { + let array = [10usize; 10]; + let invalid: *const [usize; 11] = &array as *const [usize; 10] as *const [usize; 11]; + let ptr: *const [usize] = invalid as *const _; + assert_valid_ptr(ptr); + } + + unsafe fn new_dead_ptr(val: T) -> *const T { + let local = val; + &local as *const _ } } diff --git a/tests/kani/MemPredicates/thin_ptr_validity.rs b/tests/kani/MemPredicates/thin_ptr_validity.rs new file mode 100644 index 000000000000..638b7e1d1fc8 --- /dev/null +++ b/tests/kani/MemPredicates/thin_ptr_validity.rs @@ -0,0 +1,60 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z mem-predicates +//! Check that Kani's memory predicates work for thin pointers. + +extern crate kani; + +use kani::mem::assert_valid_ptr; +use std::ptr::NonNull; + +mod valid_access { + use super::*; + #[kani::proof] + pub fn check_dangling_zst() { + let dangling = NonNull::<()>::dangling().as_ptr(); + assert_valid_ptr(dangling); + + let vec_ptr = Vec::<()>::new().as_ptr(); + assert_valid_ptr(vec_ptr); + + let dangling = NonNull::<[char; 0]>::dangling().as_ptr(); + assert_valid_ptr(dangling); + } + + #[kani::proof] + pub fn check_valid_array() { + let array = ['a', 'b', 'c']; + assert_valid_ptr(&array); + } +} + +mod invalid_access { + use super::*; + #[kani::proof] + #[kani::should_panic] + pub fn check_invalid_ptr() { + let raw_ptr = unsafe { new_dead_ptr::(0) }; + assert_valid_ptr(raw_ptr); + } + + #[kani::proof] + #[kani::should_panic] + pub fn check_invalid_array() { + let raw_ptr = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) }; + assert_valid_ptr(raw_ptr); + } + + #[kani::proof] + #[kani::should_panic] + pub fn check_invalid_zst() { + let raw_ptr: *const [char; 0] = + unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) } as *const _; + assert_valid_ptr(raw_ptr); + } + + unsafe fn new_dead_ptr(val: T) -> *const T { + let local = val; + &local as *const _ + } +} From ad72920100140d7edabffa0f9941be67a375c017 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 8 Mar 2024 11:34:53 -0800 Subject: [PATCH 3/4] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- .../src/codegen_cprover_gotoc/overrides/hooks.rs | 2 +- library/kani/src/mem.rs | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index eeb101c12547..2fcbaa36fb44 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -217,7 +217,7 @@ impl GotocHook for Panic { } } -/// Encodes __CBMC_r_ok +/// Encodes __CPROVER_r_ok struct IsReadOk; impl GotocHook for IsReadOk { fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 065332017580..203eae2229c4 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -16,12 +16,12 @@ //! 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. +//! `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: +//! 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. @@ -41,9 +41,9 @@ use std::ptr::{DynMetadata, NonNull, Pointee}; /// Assert that the pointer is valid for access according to [crate::mem] conditions 1, 2 and 3. /// -/// Note that a unaligned pointer is still considered valid. +/// Note that an unaligned pointer is still considered valid. /// -/// TODO: Kani will automatically add those checks when a de-reference happens. +/// TODO: Kani should automatically add those checks when a de-reference happens. /// https://github.com/model-checking/kani/issues/2975 /// /// This function will either panic or return `true`. This is to make it easier to use it in From ce022e216aed69d1b71c9a017784a1ed14c510ee Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 8 Mar 2024 12:37:26 -0800 Subject: [PATCH 4/4] Add a expected test using the new method in a contract --- .../function-contract/valid_ptr.expected | 11 ++++ tests/expected/function-contract/valid_ptr.rs | 61 +++++++++++++++++++ 2 files changed, 72 insertions(+) create mode 100644 tests/expected/function-contract/valid_ptr.expected create mode 100644 tests/expected/function-contract/valid_ptr.rs diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected new file mode 100644 index 000000000000..a9dc8dd5992d --- /dev/null +++ b/tests/expected/function-contract/valid_ptr.expected @@ -0,0 +1,11 @@ +Checking harness pre_condition::harness_invalid_ptr... +Failed Checks: Dangling pointer is only valid for zero-sized access + +Checking harness pre_condition::harness_stack_ptr... +VERIFICATION:- SUCCESSFUL + +Checking harness pre_condition::harness_head_ptr... +VERIFICATION:- SUCCESSFUL + +Verification failed for - pre_condition::harness_invalid_ptr +Complete - 2 successfully verified harnesses, 1 failures, 3 total diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs new file mode 100644 index 000000000000..da212c7fa63e --- /dev/null +++ b/tests/expected/function-contract/valid_ptr.rs @@ -0,0 +1,61 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zmem-predicates + +//! Test that it is sound to use `assert_valid_ptr` inside a contract pre-condition. +//! We cannot validate post-condition yet. This can be done once we fix: +//! +#![feature(pointer_is_aligned)] + +mod pre_condition { + /// This contract should succeed only if the input is a valid pointer. + #[kani::requires(kani::mem::assert_valid_ptr(ptr) && ptr.is_aligned())] + unsafe fn read_ptr(ptr: *const i32) -> i32 { + *ptr + } + + #[kani::proof_for_contract(read_ptr)] + fn harness_head_ptr() { + let boxed = Box::new(10); + let raw_ptr = Box::into_raw(boxed); + assert_eq!(unsafe { read_ptr(raw_ptr) }, 10); + let _ = unsafe { Box::from_raw(raw_ptr) }; + } + + #[kani::proof_for_contract(read_ptr)] + fn harness_stack_ptr() { + let val = -20; + assert_eq!(unsafe { read_ptr(&val) }, -20); + } + + #[kani::proof_for_contract(read_ptr)] + fn harness_invalid_ptr() { + let ptr = std::ptr::NonNull::::dangling().as_ptr(); + assert_eq!(unsafe { read_ptr(ptr) }, -20); + } +} + +/// TODO: Enable once we fix: +#[cfg(not_supported)] +mod post_condition { + + /// This contract should fail since we are creating a dangling pointer. + #[kani::ensures(kani::mem::assert_valid_ptr(result.0))] + unsafe fn new_invalid_ptr() -> PtrWrapper { + let var = 'c'; + PtrWrapper(&var as *const _) + } + + #[kani::proof_for_contract(new_invalid_ptr)] + fn harness() { + let _ = unsafe { new_invalid_ptr() }; + } + + struct PtrWrapper(*const T); + + impl kani::Arbitrary for PtrWrapper { + fn any() -> Self { + unreachable!("Do not invoke stubbing") + } + } +}