diff --git a/Cargo.toml b/Cargo.toml index 7b7d5cbe60a2..24812a157ae5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -62,6 +62,7 @@ exclude = [ "tests/perf", "tests/cargo-ui", "tests/slow", + "tests/std-checks", "tests/assess-scan-test-scaffold", "tests/script-based-pre", "tests/script-based-pre/build-cache-bin/target/new_dep", diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index d5f10adeec32..9f70c16430e5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -207,11 +207,11 @@ impl GotocHook for Panic { } } -/// Encodes __CPROVER_r_ok -struct IsReadOk; -impl GotocHook for IsReadOk { +/// Encodes __CPROVER_r_ok(ptr, size) +struct IsAllocated; +impl GotocHook for IsAllocated { fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { - matches_function(tcx, instance.def, "KaniIsReadOk") + matches_function(tcx, instance.def, "KaniIsAllocated") } fn handle( @@ -398,7 +398,7 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(Assert), Rc::new(Cover), Rc::new(Nondet), - Rc::new(IsReadOk), + Rc::new(IsAllocated), Rc::new(RustAlloc), Rc::new(MemCmp), Rc::new(UntrackedDeref), diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index d14aca3a7c5b..9402835c2ff2 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -12,6 +12,7 @@ use stable_mir::mir::{ VarDebugInfo, }; use stable_mir::ty::{Const, GenericArgs, Span, Ty, UintTy}; +use std::fmt::Debug; use std::mem; /// This structure mimics a Body that can actually be modified. @@ -224,6 +225,20 @@ impl MutableBody { } } } + + /// Clear all the existing logic of this body and turn it into a simple `return`. + /// + /// This function can be used when a new implementation of the body is needed. + /// For example, Kani intrinsics usually have a dummy body, which is replaced + /// by the compiler. This function allow us to delete the dummy body before + /// creating a new one. + /// + /// Note: We do not prune the local variables today for simplicity. + pub fn clear_body(&mut self) { + self.blocks.clear(); + let terminator = Terminator { kind: TerminatorKind::Return, span: self.span }; + self.blocks.push(BasicBlock { statements: Vec::default(), terminator }) + } } #[derive(Clone, Debug)] diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 4697c139b294..2c05c07be7f2 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -19,7 +19,6 @@ use crate::kani_middle::transform::check_values::SourceOp::UnsupportedCheck; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; -use rustc_smir::rustc_internal; use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange}; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef}; @@ -31,19 +30,14 @@ use stable_mir::mir::{ use stable_mir::target::{MachineInfo, MachineSize}; use stable_mir::ty::{AdtKind, Const, IndexedVal, RigidTy, Ty, TyKind, UintTy}; use stable_mir::CrateDef; -use std::fmt::{Debug, Formatter}; +use std::fmt::Debug; use strum_macros::AsRefStr; use tracing::{debug, trace}; /// Instrument the code with checks for invalid values. +#[derive(Debug)] pub struct ValidValuePass { - check_type: CheckType, -} - -impl ValidValuePass { - pub fn new(tcx: TyCtxt) -> Self { - ValidValuePass { check_type: CheckType::new(tcx) } - } + pub check_type: CheckType, } impl TransformPass for ValidValuePass { @@ -81,13 +75,6 @@ impl TransformPass for ValidValuePass { } } -impl Debug for ValidValuePass { - /// Implement manually since MachineInfo doesn't currently derive Debug. - fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { - "ValidValuePass".fmt(f) - } -} - impl ValidValuePass { fn build_check(&self, tcx: TyCtxt, body: &mut MutableBody, instruction: UnsafeInstruction) { debug!(?instruction, "build_check"); @@ -98,31 +85,23 @@ impl ValidValuePass { let value = body.new_assignment(rvalue, &mut source); let rvalue_ptr = Rvalue::AddressOf(Mutability::Not, Place::from(value)); for range in ranges { - let result = - self.build_limits(body, &range, rvalue_ptr.clone(), &mut source); - let msg = format!( - "Undefined Behavior: Invalid value of type `{}`", - // TODO: Fix pretty_ty - rustc_internal::internal(tcx, target_ty) - ); + let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source); + let msg = + format!("Undefined Behavior: Invalid value of type `{target_ty}`",); body.add_check(tcx, &self.check_type, &mut source, result, &msg); } } SourceOp::DerefValidity { pointee_ty, rvalue, ranges } => { for range in ranges { - let result = self.build_limits(body, &range, rvalue.clone(), &mut source); - let msg = format!( - "Undefined Behavior: Invalid value of type `{}`", - // TODO: Fix pretty_ty - rustc_internal::internal(tcx, pointee_ty) - ); + let result = build_limits(body, &range, rvalue.clone(), &mut source); + let msg = + format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",); body.add_check(tcx, &self.check_type, &mut source, result, &msg); } } SourceOp::UnsupportedCheck { check, ty } => { let reason = format!( - "Kani currently doesn't support checking validity of `{check}` for `{}` type", - rustc_internal::internal(tcx, ty) + "Kani currently doesn't support checking validity of `{check}` for `{ty}`", ); self.unsupported_check(tcx, body, &mut source, &reason); } @@ -130,57 +109,6 @@ impl ValidValuePass { } } - fn build_limits( - &self, - body: &mut MutableBody, - req: &ValidValueReq, - rvalue_ptr: Rvalue, - source: &mut SourceInstruction, - ) -> Local { - let span = source.span(body.blocks()); - debug!(?req, ?rvalue_ptr, ?span, "build_limits"); - let primitive_ty = uint_ty(req.size.bytes()); - let start_const = body.new_const_operand(req.valid_range.start, primitive_ty, span); - let end_const = body.new_const_operand(req.valid_range.end, primitive_ty, span); - let orig_ptr = if req.offset != 0 { - let start_ptr = move_local(body.new_assignment(rvalue_ptr, source)); - let byte_ptr = move_local(body.new_cast_ptr( - start_ptr, - Ty::unsigned_ty(UintTy::U8), - Mutability::Not, - source, - )); - let offset_const = body.new_const_operand(req.offset as _, UintTy::Usize, span); - let offset = move_local(body.new_assignment(Rvalue::Use(offset_const), source)); - move_local(body.new_binary_op(BinOp::Offset, byte_ptr, offset, source)) - } else { - move_local(body.new_assignment(rvalue_ptr, source)) - }; - let value_ptr = - body.new_cast_ptr(orig_ptr, Ty::unsigned_ty(primitive_ty), Mutability::Not, source); - let value = - Operand::Copy(Place { local: value_ptr, projection: vec![ProjectionElem::Deref] }); - let start_result = body.new_binary_op(BinOp::Ge, value.clone(), start_const, source); - let end_result = body.new_binary_op(BinOp::Le, value, end_const, source); - if req.valid_range.wraps_around() { - // valid >= start || valid <= end - body.new_binary_op( - BinOp::BitOr, - move_local(start_result), - move_local(end_result), - source, - ) - } else { - // valid >= start && valid <= end - body.new_binary_op( - BinOp::BitAnd, - move_local(start_result), - move_local(end_result), - source, - ) - } - } - fn unsupported_check( &self, tcx: TyCtxt, @@ -216,7 +144,7 @@ fn uint_ty(bytes: usize) -> UintTy { /// Represent a requirement for the value stored in the given offset. #[derive(Clone, Debug, Eq, PartialEq, Hash)] -struct ValidValueReq { +pub struct ValidValueReq { /// Offset in bytes. offset: usize, /// Size of this requirement. @@ -384,9 +312,13 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> { } else if self.target.is_none() { // Leave it as an exhaustive match to be notified when a new kind is added. match &stmt.kind { - StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(_)) => { - // Source and destination have the same type, so no invalid value cannot be - // generated. + StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { + // Source is a *const T and it must be safe for read. + // TODO: Implement value check. + self.push_target(SourceOp::UnsupportedCheck { + check: "copy_nonoverlapping".to_string(), + ty: copy.src.ty(self.locals).unwrap(), + }); } StatementKind::Assign(place, rvalue) => { // First check rvalue. @@ -573,11 +505,27 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> { // We only care about *mut T as *mut U return; }; + if dest_pointee_ty.kind().is_unit() { + // Ignore cast to *mut () since nothing can be written to it. + // This is a common pattern + return; + } + let src_ty = op.ty(self.locals).unwrap(); debug!(?src_ty, ?dest_ty, "visit_rvalue mutcast"); let TyKind::RigidTy(RigidTy::RawPtr(src_pointee_ty, _)) = src_ty.kind() else { unreachable!() }; + + if src_pointee_ty.kind().is_unit() { + // We cannot track what was the initial type. Thus, fail. + self.push_target(SourceOp::UnsupportedCheck { + check: "mutable cast".to_string(), + ty: src_ty, + }); + return; + } + if let Ok(src_validity) = ty_validity_per_offset(&self.machine, src_pointee_ty, 0) { @@ -626,6 +574,8 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> { }) } } + // `DynStar` is not currently supported in Kani. + // TODO: https://github.com/model-checking/kani/issues/1784 CastKind::DynStar => self.push_target(UnsupportedCheck { check: "Dyn*".to_string(), ty: (rvalue.ty(self.locals).unwrap()), @@ -784,10 +734,58 @@ fn expect_instance(locals: &[LocalDecl], func: &Operand) -> Instance { } } +/// Instrument MIR to check the value pointed by `rvalue_ptr` satisfies requirement `req`. +/// +/// The MIR will do something equivalent to: +/// ```rust +/// let ptr = rvalue_ptr.byte_offset(req.offset); +/// let typed_ptr = ptr as *const Unsigned; // Some unsigned type with length req.size +/// let value = unsafe { *typed_ptr }; +/// req.valid_range.contains(value) +/// ``` +pub fn build_limits( + body: &mut MutableBody, + req: &ValidValueReq, + rvalue_ptr: Rvalue, + source: &mut SourceInstruction, +) -> Local { + let span = source.span(body.blocks()); + debug!(?req, ?rvalue_ptr, ?span, "build_limits"); + let primitive_ty = uint_ty(req.size.bytes()); + let start_const = body.new_const_operand(req.valid_range.start, primitive_ty, span); + let end_const = body.new_const_operand(req.valid_range.end, primitive_ty, span); + let orig_ptr = if req.offset != 0 { + let start_ptr = move_local(body.new_assignment(rvalue_ptr, source)); + let byte_ptr = move_local(body.new_cast_ptr( + start_ptr, + Ty::unsigned_ty(UintTy::U8), + Mutability::Not, + source, + )); + let offset_const = body.new_const_operand(req.offset as _, UintTy::Usize, span); + let offset = move_local(body.new_assignment(Rvalue::Use(offset_const), source)); + move_local(body.new_binary_op(BinOp::Offset, byte_ptr, offset, source)) + } else { + move_local(body.new_assignment(rvalue_ptr, source)) + }; + let value_ptr = + body.new_cast_ptr(orig_ptr, Ty::unsigned_ty(primitive_ty), Mutability::Not, source); + let value = Operand::Copy(Place { local: value_ptr, projection: vec![ProjectionElem::Deref] }); + let start_result = body.new_binary_op(BinOp::Ge, value.clone(), start_const, source); + let end_result = body.new_binary_op(BinOp::Le, value, end_const, source); + if req.valid_range.wraps_around() { + // valid >= start || valid <= end + body.new_binary_op(BinOp::BitOr, move_local(start_result), move_local(end_result), source) + } else { + // valid >= start && valid <= end + body.new_binary_op(BinOp::BitAnd, move_local(start_result), move_local(end_result), source) + } +} + /// Traverse the type and find all invalid values and their location in memory. /// /// Not all values are currently supported. For those not supported, we return Error. -fn ty_validity_per_offset( +pub fn ty_validity_per_offset( machine_info: &MachineInfo, ty: Ty, current_offset: usize, diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs new file mode 100644 index 000000000000..6354e3777aca --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -0,0 +1,138 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Module responsible for generating code for a few Kani intrinsics. +//! +//! These intrinsics have code that depend on information from the compiler, such as type layout +//! information; thus, they are implemented as a transformation pass where their body get generated +//! by the transformation. + +use crate::kani_middle::attributes::matches_diagnostic; +use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_offset}; +use crate::kani_middle::transform::{TransformPass, TransformationType}; +use crate::kani_queries::QueryDb; +use rustc_middle::ty::TyCtxt; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{ + BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL, +}; +use stable_mir::target::MachineInfo; +use stable_mir::ty::{Const, RigidTy, TyKind}; +use std::fmt::Debug; +use strum_macros::AsRefStr; +use tracing::trace; + +/// Generate the body for a few Kani intrinsics. +#[derive(Debug)] +pub struct IntrinsicGeneratorPass { + pub check_type: CheckType, +} + +impl TransformPass for IntrinsicGeneratorPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Instrumentation + } + + fn is_enabled(&self, _query_db: &QueryDb) -> bool + where + Self: Sized, + { + true + } + + /// Transform the function body by inserting checks one-by-one. + /// For every unsafe dereference or a transmute operation, we check all values are valid. + fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "transform"); + if matches_diagnostic(tcx, instance.def, Intrinsics::KaniValidValue.as_ref()) { + (true, self.valid_value_body(tcx, body)) + } else { + (false, body) + } + } +} + +impl IntrinsicGeneratorPass { + /// Generate the body for valid value. Which should be something like: + /// + /// ``` + /// pub fn has_valid_value(ptr: *const T) -> bool { + /// let mut ret = true; + /// let bytes = ptr as *const u8; + /// for req in requirements { + /// ret &= in_range(bytes, req); + /// } + /// ret + /// } + /// ``` + fn valid_value_body(&self, tcx: TyCtxt, body: Body) -> Body { + let mut new_body = MutableBody::from(body); + new_body.clear_body(); + + // Initialize return variable with True. + let ret_var = RETURN_LOCAL; + let mut terminator = SourceInstruction::Terminator { bb: 0 }; + let span = new_body.locals()[ret_var].span; + let assign = StatementKind::Assign( + Place::from(ret_var), + Rvalue::Use(Operand::Constant(Constant { + span, + user_ty: None, + literal: Const::from_bool(true), + })), + ); + let stmt = Statement { kind: assign, span }; + new_body.insert_stmt(stmt, &mut terminator); + let machine_info = MachineInfo::target(); + + // The first and only argument type. + let arg_ty = new_body.locals()[1].ty; + let TyKind::RigidTy(RigidTy::RawPtr(target_ty, _)) = arg_ty.kind() else { unreachable!() }; + let validity = ty_validity_per_offset(&machine_info, target_ty, 0); + match validity { + Ok(ranges) if ranges.is_empty() => { + // Nothing to check + } + Ok(ranges) => { + // Given the pointer argument, check for possible invalid ranges. + let rvalue = Rvalue::Use(Operand::Move(Place::from(1))); + for range in ranges { + let result = + build_limits(&mut new_body, &range, rvalue.clone(), &mut terminator); + let rvalue = Rvalue::BinaryOp( + BinOp::BitAnd, + Operand::Move(Place::from(ret_var)), + Operand::Move(Place::from(result)), + ); + let assign = StatementKind::Assign(Place::from(ret_var), rvalue); + let stmt = Statement { kind: assign, span }; + new_body.insert_stmt(stmt, &mut terminator); + } + } + Err(msg) => { + // We failed to retrieve all the valid ranges. + let rvalue = Rvalue::Use(Operand::Constant(Constant { + literal: Const::from_bool(false), + span, + user_ty: None, + })); + let result = new_body.new_assignment(rvalue, &mut terminator); + let reason = format!( + "Kani currently doesn't support checking validity of `{target_ty}`. {msg}" + ); + new_body.add_check(tcx, &self.check_type, &mut terminator, result, &reason); + } + } + new_body.into() + } +} + +#[derive(Debug, Copy, Clone, Eq, PartialEq, AsRefStr)] +#[strum(serialize_all = "PascalCase")] +enum Intrinsics { + KaniValidValue, +} diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index a6cd17e8c7db..d4e06a785fb3 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -16,7 +16,9 @@ //! //! For all instrumentation passes, always use exhaustive matches to ensure soundness in case a new //! case is added. +use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_values::ValidValuePass; +use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; @@ -26,6 +28,7 @@ use std::fmt::Debug; mod body; mod check_values; +mod kani_intrinsics; /// Object used to retrieve a transformed instance body. /// The transformations to be applied may be controlled by user options. @@ -50,7 +53,9 @@ impl BodyTransformation { inst_passes: vec![], cache: Default::default(), }; - transformer.add_pass(queries, ValidValuePass::new(tcx)); + let check_type = CheckType::new(tcx); + transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); + transformer.add_pass(queries, IntrinsicGeneratorPass { check_type }); transformer } diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index b857247021ec..c485ee16a562 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -10,8 +10,10 @@ //! 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. +//! ~~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 @@ -39,39 +41,137 @@ 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. +/// Check if the pointer is valid for write access according to [crate::mem] conditions 1, 2 +/// and 3. /// -/// Note that an unaligned pointer is still considered valid. +/// Note this function also checks for pointer alignment. Use [self::can_write_unaligned] +/// if you don't want to fail for unaligned pointers. +/// +/// This function does not check if the value stored is valid for the given type. Use +/// [self::can_dereference] for that. +/// +/// This function will panic today if the pointer is not null, and it points to an unallocated or +/// deallocated memory location. This is an existing Kani limitation. +/// See for more details. +#[crate::unstable( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" +)] +pub fn can_write(ptr: *mut T) -> bool +where + T: ?Sized, + ::Metadata: PtrProperties, +{ + // The interface takes a mutable pointer to improve readability of the signature. + // However, using constant pointer avoid unnecessary instrumentation, and it is as powerful. + // Hence, cast to `*const T`. + let ptr: *const T = ptr; + let (thin_ptr, metadata) = ptr.to_raw_parts(); + metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) +} + +/// Check if the pointer is valid for unaligned write access according to [crate::mem] conditions +/// 1, 2 and 3. +/// +/// Note this function succeeds for unaligned pointers. See [self::can_write] if you also +/// want to check pointer alignment. +/// +/// This function will panic today if the pointer is not null, and it points to an unallocated or +/// deallocated memory location. This is an existing Kani limitation. +/// See for more details. +#[crate::unstable( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" +)] +pub fn can_write_unaligned(ptr: *const T) -> bool +where + T: ?Sized, + ::Metadata: PtrProperties, +{ + let (thin_ptr, metadata) = ptr.to_raw_parts(); + is_inbounds(&metadata, thin_ptr) +} + +/// Checks that pointer `ptr` point to a valid value of type `T`. +/// +/// For that, the pointer has to be a valid pointer according to [crate::mem] conditions 1, 2 +/// and 3, +/// and the value stored must respect the validity invariants for type `T`. /// /// TODO: Kani should automatically add those checks when a de-reference happens. /// /// -/// This function will either panic or return `true`. This is to make it easier to use it in -/// contracts. +/// This function will panic today if the pointer is not null, and it points to an unallocated or +/// deallocated memory location. This is an existing Kani limitation. +/// See for more details. #[crate::unstable( feature = "mem-predicates", issue = 2690, reason = "experimental memory predicate API" )] -pub fn assert_valid_ptr(ptr: *const T) -> bool +#[allow(clippy::not_unsafe_ptr_arg_deref)] +pub fn can_dereference(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.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. +#[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 + true // ZST pointers are always valid including nullptr. + } else if data_ptr.is_null() { + false } else { // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be // stubbed. + // We first assert that the data_ptr crate::assert( - is_read_ok(thin_ptr, sz), - "Expected valid pointer, but found dangling pointer", + unsafe { is_allocated(data_ptr, 0) }, + "Kani does not support reasoning about pointer to unallocated memory", ); - true + unsafe { is_allocated(data_ptr, sz) } } } @@ -86,6 +186,12 @@ mod private { 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 (); @@ -160,18 +266,33 @@ where /// 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. +/// # 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 = "KaniIsReadOk"] +#[rustc_diagnostic_item = "KaniIsAllocated"] #[inline(never)] -fn is_read_ok(_ptr: *const (), _size: usize) -> bool { +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() } #[cfg(test)] mod tests { - use super::{assert_valid_ptr, PtrProperties}; + use super::{can_dereference, can_write, PtrProperties}; use crate::mem::private::Internal; use std::fmt::Debug; use std::intrinsics::size_of; @@ -225,39 +346,42 @@ mod tests { #[test] pub fn test_empty_slice() { - let slice_ptr = Vec::::new().as_slice() as *const [char]; - assert_valid_ptr(slice_ptr); + let slice_ptr = Vec::::new().as_mut_slice() as *mut [char]; + assert!(can_write(slice_ptr)); } #[test] pub fn test_empty_str() { - let slice_ptr = String::new().as_str() as *const str; - assert_valid_ptr(slice_ptr); + let slice_ptr = String::new().as_mut_str() as *mut str; + assert!(can_write(slice_ptr)); } #[test] fn test_dangling_zst() { - test_dangling_of_t::<()>(); - test_dangling_of_t::<[(); 10]>(); + test_dangling_of_zst::<()>(); + test_dangling_of_zst::<[(); 10]>(); } - fn test_dangling_of_t() { - let dangling: *const T = NonNull::::dangling().as_ptr(); - assert_valid_ptr(dangling); + fn test_dangling_of_zst() { + let dangling: *mut T = NonNull::::dangling().as_ptr(); + assert!(can_write(dangling)); - let vec_ptr = Vec::::new().as_ptr(); - assert_valid_ptr(vec_ptr); + let vec_ptr = Vec::::new().as_mut_ptr(); + assert!(can_write(vec_ptr)); } #[test] - #[should_panic(expected = "Expected valid pointer, but found `null`")] fn test_null_fat_ptr() { - assert_valid_ptr(ptr::null::() as *const dyn Debug); + assert!(!can_dereference(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::()); + assert!(!can_dereference(ptr::null::())); + } + + #[test] + fn test_null_mut() { + assert!(!can_write(ptr::null_mut::())); } } diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 3b029c475d5f..dcced313ce0b 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -50,15 +50,16 @@ RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-trai # Declare testing suite information (suite and mode) TESTS=( "script-based-pre exec" - "coverage coverage-based" "kani kani" "expected expected" "ui expected" + "std-checks cargo-kani" "firecracker kani" "prusti kani" "smack kani" "cargo-kani cargo-kani" "cargo-ui cargo-kani" + "coverage coverage-based" "kani-docs cargo-kani" "kani-fixme kani-fixme" ) diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index f45cb4e2e826..1b62781adaaf 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -1,5 +1,6 @@ Checking harness pre_condition::harness_invalid_ptr... -Failed Checks: Expected valid pointer, but found dangling pointer +Failed Checks: Kani does not support reasoning about pointer to unallocated memory +VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) Checking harness pre_condition::harness_stack_ptr... VERIFICATION:- SUCCESSFUL @@ -7,5 +8,4 @@ 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 +Complete - 3 successfully verified harnesses, 0 failures, 3 total diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs index da212c7fa63e..2047a46caf4f 100644 --- a/tests/expected/function-contract/valid_ptr.rs +++ b/tests/expected/function-contract/valid_ptr.rs @@ -2,14 +2,13 @@ // 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. +//! Test that it is sound to use memory predicates 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())] + #[kani::requires(kani::mem::can_dereference(ptr))] unsafe fn read_ptr(ptr: *const i32) -> i32 { *ptr } @@ -29,6 +28,7 @@ mod pre_condition { } #[kani::proof_for_contract(read_ptr)] + #[kani::should_panic] fn harness_invalid_ptr() { let ptr = std::ptr::NonNull::::dangling().as_ptr(); assert_eq!(unsafe { read_ptr(ptr) }, -20); @@ -40,7 +40,7 @@ mod pre_condition { mod post_condition { /// This contract should fail since we are creating a dangling pointer. - #[kani::ensures(kani::mem::assert_valid_ptr(result.0))] + #[kani::ensures(kani::mem::can_dereference(result.0))] unsafe fn new_invalid_ptr() -> PtrWrapper { let var = 'c'; PtrWrapper(&var as *const _) diff --git a/tests/kani/MemPredicates/fat_ptr_validity.rs b/tests/kani/MemPredicates/fat_ptr_validity.rs index 51d784f06566..c4f037f3a646 100644 --- a/tests/kani/MemPredicates/fat_ptr_validity.rs +++ b/tests/kani/MemPredicates/fat_ptr_validity.rs @@ -5,24 +5,22 @@ extern crate kani; -use kani::mem::assert_valid_ptr; +use kani::mem::{can_dereference, can_write}; 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); + let mut var = 10u8; + let fat_ptr: *mut dyn PartialEq = &mut var as *mut _; + assert!(can_write(fat_ptr)); } #[kani::proof] pub fn check_valid_slice_ptr() { let array = ['a', 'b', 'c']; let slice = &array as *const [char]; - assert_valid_ptr(slice); + assert!(can_dereference(slice)); assert_eq!(unsafe { &*slice }[0], 'a'); assert_eq!(unsafe { &*slice }[2], 'c'); } @@ -30,10 +28,10 @@ mod valid_access { #[kani::proof] pub fn check_valid_zst() { let slice_ptr = Vec::::new().as_slice() as *const [char]; - assert_valid_ptr(slice_ptr); + assert!(can_dereference(slice_ptr)); let str_ptr = String::new().as_str() as *const str; - assert_valid_ptr(str_ptr); + assert!(can_dereference(str_ptr)); } } @@ -43,14 +41,14 @@ mod invalid_access { #[kani::should_panic] pub fn check_invalid_dyn_ptr() { let raw_ptr: *const dyn PartialEq = unsafe { new_dead_ptr::(0) }; - assert_valid_ptr(raw_ptr); + assert!(can_dereference(raw_ptr)); } #[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); + assert!(can_dereference(raw_ptr)); } #[kani::proof] @@ -59,7 +57,7 @@ mod invalid_access { 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); + assert!(can_dereference(ptr)); } unsafe fn new_dead_ptr(val: T) -> *const T { diff --git a/tests/kani/MemPredicates/thin_ptr_validity.rs b/tests/kani/MemPredicates/thin_ptr_validity.rs index 49e9c403cda8..553c5beab9f8 100644 --- a/tests/kani/MemPredicates/thin_ptr_validity.rs +++ b/tests/kani/MemPredicates/thin_ptr_validity.rs @@ -5,7 +5,7 @@ extern crate kani; -use kani::mem::assert_valid_ptr; +use kani::mem::can_dereference; use std::ptr::NonNull; mod valid_access { @@ -13,19 +13,19 @@ mod valid_access { #[kani::proof] pub fn check_dangling_zst() { let dangling = NonNull::<()>::dangling().as_ptr(); - assert_valid_ptr(dangling); + assert!(can_dereference(dangling)); let vec_ptr = Vec::<()>::new().as_ptr(); - assert_valid_ptr(vec_ptr); + assert!(can_dereference(vec_ptr)); let dangling = NonNull::<[char; 0]>::dangling().as_ptr(); - assert_valid_ptr(dangling); + assert!(can_dereference(dangling)); } #[kani::proof] pub fn check_valid_array() { let array = ['a', 'b', 'c']; - assert_valid_ptr(&array); + assert!(can_dereference(&array)); } } @@ -35,14 +35,14 @@ mod invalid_access { #[kani::should_panic] pub fn check_invalid_ptr() { let raw_ptr = unsafe { new_dead_ptr::(0) }; - assert_valid_ptr(raw_ptr); + assert!(!can_dereference(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); + assert!(can_dereference(raw_ptr)); } #[kani::proof] @@ -50,7 +50,7 @@ mod invalid_access { let raw_ptr: *const [char; 0] = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) } as *const _; // ZST pointer are always valid - assert_valid_ptr(raw_ptr); + assert!(can_dereference(raw_ptr)); } unsafe fn new_dead_ptr(val: T) -> *const T { diff --git a/tests/kani/ValidValues/custom_niche.rs b/tests/kani/ValidValues/custom_niche.rs index 02b5b87bd092..b282fec3c645 100644 --- a/tests/kani/ValidValues/custom_niche.rs +++ b/tests/kani/ValidValues/custom_niche.rs @@ -4,8 +4,8 @@ //! Check that Kani can identify UB when using niche attribute for a custom operation. #![feature(rustc_attrs)] -use std::mem; use std::mem::size_of; +use std::{mem, ptr}; /// A possible implementation for a system of rating that defines niche. /// A Rating represents the number of stars of a given product (1..=5). @@ -78,6 +78,25 @@ pub fn check_invalid_transmute_copy() { let _rating: Rating = unsafe { mem::transmute_copy(&any) }; } +/// This code does not trigger UB, and verification should succeed. +/// +/// FIX-ME: This is not supported today, and we fail due to unsupported check. +#[kani::proof] +#[kani::should_panic] +pub fn check_copy_nonoverlap() { + let stars = kani::any_where(|s: &u8| *s == 0 || *s > 5); + let mut rating: Rating = kani::any(); + unsafe { ptr::copy_nonoverlapping(&stars as *const _ as *const Rating, &mut rating, 1) }; +} + +#[kani::proof] +#[kani::should_panic] +pub fn check_copy_nonoverlap_ub() { + let any: u8 = kani::any(); + let mut rating: Rating = kani::any(); + unsafe { ptr::copy_nonoverlapping(&any as *const _ as *const Rating, &mut rating, 1) }; +} + #[kani::proof] #[kani::should_panic] pub fn check_invalid_increment() { diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml new file mode 100644 index 000000000000..9cacaa1368e3 --- /dev/null +++ b/tests/std-checks/core/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "verify-core" +version = "0.1.0" +edition = "2021" +description = "This crate contains contracts and harnesses for core library" + +[package.metadata.kani] +unstable = { function-contracts = true, mem-predicates = true } + +[package.metadata.kani.flags] +output-format = "terse" diff --git a/tests/std-checks/core/mem.expected b/tests/std-checks/core/mem.expected new file mode 100644 index 000000000000..8a3b89a8f66a --- /dev/null +++ b/tests/std-checks/core/mem.expected @@ -0,0 +1,3 @@ +Summary: +Verification failed for - mem::verify::check_swap_unit +Complete - 3 successfully verified harnesses, 1 failures, 4 total. diff --git a/tests/std-checks/core/ptr.expected b/tests/std-checks/core/ptr.expected new file mode 100644 index 000000000000..337174141ff0 --- /dev/null +++ b/tests/std-checks/core/ptr.expected @@ -0,0 +1,3 @@ +Summary: +Verification failed for - ptr::verify::check_replace_unit +Complete - 5 successfully verified harnesses, 1 failures, 6 total. diff --git a/tests/std-checks/core/src/lib.rs b/tests/std-checks/core/src/lib.rs new file mode 100644 index 000000000000..f0e5b480a2d2 --- /dev/null +++ b/tests/std-checks/core/src/lib.rs @@ -0,0 +1,9 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Top file that includes all sub-modules mimicking core structure. + +extern crate kani; + +pub mod mem; +pub mod ptr; diff --git a/tests/std-checks/core/src/mem.rs b/tests/std-checks/core/src/mem.rs new file mode 100644 index 000000000000..5ca439a18e1c --- /dev/null +++ b/tests/std-checks/core/src/mem.rs @@ -0,0 +1,75 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Verify a few std::ptr::NonNull functions. + +/// Create wrapper functions to standard library functions that contains their contract. +pub mod contracts { + /// Swaps the values at two mutable locations, without deinitializing either one. + /// + /// TODO: Once history variable has been added, add a post-condition. + /// Also add a function to do a bitwise value comparison between arguments (ignore paddings). + /// + /// ```ignore + /// #[kani::ensures(kani::equals(kani::old(x), y))] + /// #[kani::ensures(kani::equals(kani::old(y), x))] + /// ``` + #[kani::modifies(x)] + #[kani::modifies(y)] + pub fn swap(x: &mut T, y: &mut T) { + std::mem::swap(x, y) + } +} + +#[cfg(kani)] +mod verify { + use super::*; + + /// Use this type to ensure that mem swap does not drop the value. + #[derive(kani::Arbitrary)] + struct CannotDrop { + inner: T, + } + + impl Drop for CannotDrop { + fn drop(&mut self) { + unreachable!("Cannot drop") + } + } + + #[kani::proof_for_contract(contracts::swap)] + pub fn check_swap_primitive() { + let mut x: u8 = kani::any(); + let mut y: u8 = kani::any(); + contracts::swap(&mut x, &mut y) + } + + /// 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(); + let mut y: () = kani::any(); + contracts::swap(&mut x, &mut y) + } + + #[kani::proof_for_contract(contracts::swap)] + pub fn check_swap_adt_no_drop() { + let mut x: CannotDrop = kani::any(); + let mut y: CannotDrop = kani::any(); + contracts::swap(&mut x, &mut y); + std::mem::forget(x); + std::mem::forget(y); + } + + /// Memory swap logic is optimized according to the size and alignment of a type. + #[kani::proof_for_contract(contracts::swap)] + pub fn check_swap_large_adt_no_drop() { + let mut x: CannotDrop<[u128; 5]> = kani::any(); + let mut y: CannotDrop<[u128; 5]> = kani::any(); + contracts::swap(&mut x, &mut y); + std::mem::forget(x); + std::mem::forget(y); + } +} diff --git a/tests/std-checks/core/src/ptr.rs b/tests/std-checks/core/src/ptr.rs new file mode 100644 index 000000000000..847b8fd1c138 --- /dev/null +++ b/tests/std-checks/core/src/ptr.rs @@ -0,0 +1,112 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Add contracts for functions from std::ptr. + +use std::ptr::NonNull; + +/// Create wrapper functions to standard library functions that contains their contract. +pub mod contracts { + use super::*; + use kani::{ensures, implies, mem::*, modifies, requires}; + + #[ensures(implies!(ptr.is_null() => result.is_none()))] + #[ensures(implies!(!ptr.is_null() => result.is_some()))] + pub fn new(ptr: *mut T) -> Option> { + NonNull::new(ptr) + } + + /// # Safety: + /// When calling this method, you have to ensure that all the following is true: + /// + /// - The pointer must be properly aligned. + /// - It must be “dereferenceable” in the sense defined in the module documentation. + /// - TODO: The pointer must point to an initialized instance of T. + /// - We check for value validity, but not initialization yet. + /// + /// TODO: How to ensure aliasing rules?? + /// You must enforce Rust’s aliasing rules, since the returned lifetime 'a is arbitrarily chosen and does not + /// necessarily reflect the actual lifetime of the data. In particular, while this reference exists, the memory + /// the pointer points to must not get mutated (except inside UnsafeCell). + /// Taken from: + #[requires(can_dereference(obj.as_ptr()))] + pub unsafe fn as_ref<'a, T>(obj: &NonNull) -> &'a T { + obj.as_ref() + } + + #[requires(!ptr.is_null())] + pub unsafe fn new_unchecked(ptr: *mut T) -> NonNull { + NonNull::::new_unchecked(ptr) + } + + /// Safety + /// + /// Behavior is undefined if any of the following conditions are violated: + /// - `dst` must be valid for both reads and writes. + /// - `dst` must be properly aligned. + /// - TODO: `dst` must point to a properly initialized value of type `T`. + /// - We check validity but not initialization. + /// + /// Note that even if `T` has size 0, the pointer must be non-null and properly aligned. + #[requires(can_dereference(dst))] + #[modifies(dst)] + pub unsafe fn replace(dst: *mut T, src: T) -> T { + std::ptr::replace(dst, src) + } +} + +#[cfg(kani)] +mod verify { + use super::*; + use kani::cover; + + #[kani::proof_for_contract(contracts::new)] + pub fn check_new() { + let ptr = kani::any::() as *mut (); + let res = contracts::new(ptr); + cover!(res.is_none()); + cover!(res.is_some()); + } + + #[kani::proof_for_contract(contracts::new_unchecked)] + pub fn check_new_unchecked() { + let ptr = kani::any::() as *mut (); + let _ = unsafe { contracts::new_unchecked(ptr) }; + } + + #[kani::proof_for_contract(contracts::as_ref)] + pub fn check_as_ref() { + let ptr = kani::any::>(); + let non_null = NonNull::new(Box::into_raw(ptr)).unwrap(); + let _rf = unsafe { contracts::as_ref(&non_null) }; + } + + #[kani::proof_for_contract(contracts::as_ref)] + #[kani::should_panic] + pub fn check_as_ref_dangling() { + let ptr = kani::any::() as *mut u8; + kani::assume(!ptr.is_null()); + let non_null = NonNull::new(ptr).unwrap(); + let _rf = unsafe { contracts::as_ref(&non_null) }; + } + + /// FIX-ME: Modifies clause fail with pointer to ZST. + /// + #[kani::proof_for_contract(contracts::replace)] + pub fn check_replace_unit() { + check_replace_impl::<()>(); + } + + #[kani::proof_for_contract(contracts::replace)] + pub fn check_replace_char() { + check_replace_impl::(); + } + + fn check_replace_impl() { + let mut dst = T::any(); + let orig = dst.clone(); + let src = T::any(); + let ret = unsafe { contracts::replace(&mut dst, src.clone()) }; + assert_eq!(ret, orig); + assert_eq!(dst, src); + } +}