From 6d58a693df17368f320ff6c9670f33e0d8ab2cfd Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 15 Oct 2024 18:25:09 -0700 Subject: [PATCH] Implement proper function pointer handling Add a test that I was working on that triggered this issue. --- .../src/kani_middle/transform/check_values.rs | 95 +++++++++---------- .../can_dereference.expected | 3 + .../valid-value-checks/can_dereference.rs | 24 +++++ 3 files changed, 71 insertions(+), 51 deletions(-) create mode 100644 tests/expected/valid-value-checks/can_dereference.expected create mode 100644 tests/expected/valid-value-checks/can_dereference.rs diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index d0fd553ef5cf..16a15278d5a9 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -24,7 +24,7 @@ use rustc_middle::ty::{Const, TyCtxt}; use rustc_smir::rustc_internal; use stable_mir::CrateDef; use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange}; -use stable_mir::mir::mono::{Instance, InstanceKind}; +use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef}; use stable_mir::mir::{ AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, ConstOperand, FieldIdx, Local, LocalDecl, @@ -384,51 +384,47 @@ impl<'a, 'b> MirVisitor for CheckValueVisitor<'a, 'b> { TerminatorKind::Call { func, args, .. } => { // Note: For transmute, both Src and Dst must be valid type. // In this case, we need to save the Dst, and invoke super_terminator. - self.super_terminator(term, location); - let instance = expect_instance(self.locals, func); - if instance.kind == InstanceKind::Intrinsic { - match instance.intrinsic_name().unwrap().as_str() { - "write_bytes" => { - // The write bytes intrinsic may trigger UB in safe code. - // pub unsafe fn write_bytes(dst: *mut T, val: u8, count: usize) - // - // This is an over-approximation since writing an invalid value is - // not UB, only reading it will be. - assert_eq!( - args.len(), - 3, - "Unexpected number of arguments for `write_bytes`" - ); - let TyKind::RigidTy(RigidTy::RawPtr(target_ty, Mutability::Mut)) = - args[0].ty(self.locals).unwrap().kind() - else { - unreachable!() - }; - let validity = ty_validity_per_offset(&self.machine, target_ty, 0); - match validity { - Ok(ranges) if ranges.is_empty() => {} - Ok(ranges) => { - let sz = rustc_internal::stable(Const::from_target_usize( - self.tcx, - target_ty.layout().unwrap().shape().size.bytes() as u64, - )); - self.push_target(SourceOp::BytesValidity { - target_ty, - rvalue: Rvalue::Repeat(args[1].clone(), sz), - ranges, - }) - } - _ => self.push_target(SourceOp::UnsupportedCheck { - check: "write_bytes".to_string(), - ty: target_ty, - }), + match intrinsic_name(self.locals, func).as_deref() { + Some("write_bytes") => { + // The write bytes intrinsic may trigger UB in safe code. + // pub unsafe fn write_bytes(dst: *mut T, val: u8, count: usize) + // + // This is an over-approximation since writing an invalid value is + // not UB, only reading it will be. + assert_eq!( + args.len(), + 3, + "Unexpected number of arguments for `write_bytes`" + ); + let TyKind::RigidTy(RigidTy::RawPtr(target_ty, Mutability::Mut)) = + args[0].ty(self.locals).unwrap().kind() + else { + unreachable!() + }; + let validity = ty_validity_per_offset(&self.machine, target_ty, 0); + match validity { + Ok(ranges) if ranges.is_empty() => {} + Ok(ranges) => { + let sz = rustc_internal::stable(Const::from_target_usize( + self.tcx, + target_ty.layout().unwrap().shape().size.bytes() as u64, + )); + self.push_target(SourceOp::BytesValidity { + target_ty, + rvalue: Rvalue::Repeat(args[1].clone(), sz), + ranges, + }) } + _ => self.push_target(SourceOp::UnsupportedCheck { + check: "write_bytes".to_string(), + ty: target_ty, + }), } - "transmute" | "transmute_copy" => { - unreachable!("Should've been lowered") - } - _ => {} } + Some("transmute") | Some("transmute_copy") => { + unreachable!("Should've been lowered") + } + _ => {} } } TerminatorKind::Goto { .. } @@ -741,16 +737,13 @@ fn assignment_check_points( invalid_ranges } -/// Retrieve instance for the given function operand. +/// Retrieve the name of the intrinsic if this operand is an intrinsic. /// -/// This will panic if the operand is not a function or if it cannot be resolved. -fn expect_instance(locals: &[LocalDecl], func: &Operand) -> Instance { +/// Intrinsics can only be invoked directly, so we can safely ignore other operand types. +fn intrinsic_name(locals: &[LocalDecl], func: &Operand) -> Option { let ty = func.ty(locals).unwrap(); - match ty.kind() { - TyKind::RigidTy(RigidTy::FnDef(def, args)) => Instance::resolve(def, &args).unwrap(), - TyKind::RigidTy(RigidTy::FnPtr(sig)) => todo!("Add support to FnPtr: {sig:?}"), - _ => unreachable!("Found: {func:?}"), - } + let TyKind::RigidTy(RigidTy::FnDef(def, args)) = ty.kind() else { return None }; + Instance::resolve(def, &args).unwrap().intrinsic_name() } /// Instrument MIR to check the value pointed by `rvalue_ptr` satisfies requirement `req`. diff --git a/tests/expected/valid-value-checks/can_dereference.expected b/tests/expected/valid-value-checks/can_dereference.expected new file mode 100644 index 000000000000..157cea584e5d --- /dev/null +++ b/tests/expected/valid-value-checks/can_dereference.expected @@ -0,0 +1,3 @@ +2 of 2 cover properties satisfied + +Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/expected/valid-value-checks/can_dereference.rs b/tests/expected/valid-value-checks/can_dereference.rs new file mode 100644 index 000000000000..b3e5521dac89 --- /dev/null +++ b/tests/expected/valid-value-checks/can_dereference.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z valid-value-checks -Z mem-predicates +//! Check that Kani can identify invalid value when using `can_dereference` API. + +#[kani::proof] +fn check_can_dereference_char() { + let val: [u32; 2] = kani::any(); + kani::cover!(kani::mem::can_dereference(&val as *const _ as *const [char; 2])); + kani::cover!(!kani::mem::can_dereference(&val as *const _ as *const [char; 2])); +} + +#[kani::proof] +fn check_can_dereference_always_valid() { + let val: [char; 2] = [kani::any(), kani::any()]; + assert!(kani::mem::can_dereference(&val as *const _ as *const [u32; 2])); +} + +#[kani::proof] +fn check_can_dereference_always_invalid() { + let val: [u8; 2] = kani::any(); + kani::assume(val[0] > 1 || val[1] > 1); + assert!(!kani::mem::can_dereference(&val as *const _ as *const [bool; 2])); +}