Add method to assert a pointer is safe to access

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());

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,

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<Expr>,
+ assign_to: &Place,
+ target: Option<BasicBlockIdx>,
+ 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),

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 {

library/kani/src/lib.rs

@@ -14,13 +14,17 @@
 #![feature(repr_simd)]
 // Features used for tests only.
 #![cfg_attr(test, feature(core_intrinsics, portable_simd))]
-// Required for rustc_diagnostic_item
+// 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<F: Fn()>(_: Vec<Vec<u8>>, _: 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)
  };
 }
 

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:
+//! <https://doc.rust-lang.org/std/ptr/index.html> (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<T>(ptr: *const T) -> bool
+where
+ T: ?Sized,
+ <T as Pointee>::Metadata: PtrProperties<T>,
+{
+ 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<T>(ptr: *const T) -> bool
+where
+ T: ?Sized,
+ <T as Pointee>::Metadata: PtrProperties<T>,
+{
+ 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<T: ?Sized> {
+ 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<T> PtrProperties<T> for () {
+ fn pointee_size(&self, _: Internal) -> usize {
+ size_of::<T>()
+ }
+
+ fn min_alignment(&self, _: Internal) -> usize {
+ align_of::<T>()
+ }
+
+ fn can_read(&self, thin_ptr: *const (), _: Internal) -> bool {
+ let sz = size_of::<T>();
+ if NonNull::<T>::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<str> 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].
+ /// <https://doc.rust-lang.org/reference/type-layout.html#str-layout>
+ fn min_alignment(&self, _: Internal) -> usize {
+ align_of::<u8>()
+ }
+}
+
+impl<T> PtrProperties<[T]> for usize {
+ fn pointee_size(&self, _: Internal) -> usize {
+ *self
+ }
+
+ fn min_alignment(&self, _: Internal) -> usize {
+ align_of::<T>()
+ }
+}
+
+impl<T> PtrProperties<T> for DynMetadata<T>
+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<T>(ptr: *const T) -> usize
+ where
+ T: ?Sized,
+ <T as Pointee>::Metadata: PtrProperties<T>,
+ {
+ let (_, metadata) = ptr.to_raw_parts();
+ metadata.pointee_size(Internal)
+ }
+
+ fn align_of_t<T>(ptr: *const T) -> usize
+ where
+ T: ?Sized,
+ <T as Pointee>::Metadata: PtrProperties<T>,
+ {
+ 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::<u32>::dangling().as_ptr() as *const dyn std::fmt::Display),
+ size_of::<u32>()
+ );
+ }
+
+ #[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::<u32>::dangling().as_ptr() as *const dyn std::fmt::Display),
+ align_of::<u32>()
+ );
+ }
+}