Skip to content

Commit

Permalink
Add out of bounds check for offset intrinsics (#3755)
Browse files Browse the repository at this point in the history
Note that the `offset` intrinsics is lowered to `Rvalue::Offset`. Thus,
we have to replace the entire statement.

This PR does not address `ptr_offset_from` and
`ptr_offset_from_unsigned`. I'll push those changes to a separate PR.

Resolves #1233 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Carolyn Zech <[email protected]>
  • Loading branch information
celinval and carolynzech authored Dec 11, 2024
1 parent db1c5fe commit 2334f2c
Show file tree
Hide file tree
Showing 37 changed files with 529 additions and 118 deletions.
11 changes: 6 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ pub enum PropertyClass {
/// Overflow panics that can be generated by Intrisics.
/// NOTE: Not all uses of this are found by rust-analyzer because of the use of macros. Try grep instead.
///
/// SPECIAL BEHAVIOR: None TODO: Why should this exist?
/// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `SafetyCheck`.
ArithmeticOverflow,
/// The Rust `assume` instrinsic is `assert`'d by Kani, and gets this property class.
///
Expand Down Expand Up @@ -67,13 +67,13 @@ pub enum PropertyClass {
/// That is, they do not depend on special instrumentation that Kani performs that wouldn't
/// otherwise be observable.
Assertion,
/// Another instrinsic check.
/// Another intrinsic check.
///
/// SPECIAL BEHAVIOR: None TODO: Why should this exist?
/// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `SafetyCheck`.
ExactDiv,
/// Another instrinsic check.
/// Another intrinsic check.
///
/// SPECIAL BEHAVIOR: None TODO: Why should this exist?
/// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `SafetyCheck`.
FiniteCheck,
/// Checks added by Kani compiler to determine whether a property (e.g.
/// `PropertyClass::Assertion` or `PropertyClass:Cover`) is reachable
Expand All @@ -82,6 +82,7 @@ pub enum PropertyClass {
/// E.g., things that trigger UB or unstable behavior.
///
/// SPECIAL BEHAVIOR: Assertions that may not exist when running code normally (i.e. not under Kani)
/// This is not caught by `#[should_panic]`.
SafetyCheck,
/// Checks to ensure that Kani's code generation is correct.
///
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1015,7 +1015,7 @@ impl GotocCtx<'_> {
///
/// This function handles code generation for the `arith_offset` intrinsic.
/// <https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html>
/// According to the documenation, the operation is always safe.
/// According to the documentation, the operation is always safe.
fn codegen_arith_offset(&mut self, mut fargs: Vec<Expr>, p: &Place, loc: Location) -> Stmt {
let src_ptr = fargs.remove(0);
let offset = fargs.remove(0);
Expand Down
43 changes: 8 additions & 35 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -356,7 +356,7 @@ impl GotocCtx<'_> {

fn codegen_rvalue_binary_op(
&mut self,
ty: Ty,
_ty: Ty,
op: &BinOp,
e1: &Operand,
e2: &Operand,
Expand Down Expand Up @@ -405,42 +405,15 @@ impl GotocCtx<'_> {
}
// https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
BinOp::Offset => {
// We don't need to check for UB since we handled user calls of offset already
// via rustc_intrinsic transformation pass.
//
// This operation may still be used by other Kani instrumentation which should
// ensure safety.
// We should consider adding sanity checks if `debug_assertions` are enabled.
let ce1 = self.codegen_operand_stable(e1);
let ce2 = self.codegen_operand_stable(e2);

// Check that computing `offset` in bytes would not overflow
let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(
ce2.clone().cast_to(Type::ssize_t()),
pointee_type_stable(ty).unwrap(),
Type::ssize_t(),
"offset",
loc,
);

// Check that the computation would not overflow an `isize` which is UB:
// https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
// These checks may allow a wrapping-around behavior in CBMC:
// https://github.com/model-checking/kani/issues/1150
// Note(std): We don't check that the starting or resulting pointer stay
// within bounds of the object they point to. Doing so causes spurious
// failures due to the usage of these intrinsics in the standard library.
// See <https://github.com/model-checking/kani/issues/1233> for more details.
// Note that this is one of the safety conditions for `offset`:
// <https://doc.rust-lang.org/std/primitive.pointer.html#safety-2>

let overflow_res = ce1.clone().cast_to(Type::ssize_t()).add_overflow(offset_bytes);
let overflow_check = self.codegen_assert_assume(
overflow_res.overflowed.not(),
PropertyClass::ArithmeticOverflow,
"attempt to compute offset which would overflow",
loc,
);
let res = ce1.clone().plus(ce2);
Expr::statement_expression(
vec![bytes_overflow_check, overflow_check, res.as_stmt(loc)],
ce1.typ().clone(),
loc,
)
ce1.clone().plus(ce2)
}
}
}
Expand Down
49 changes: 41 additions & 8 deletions kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -134,15 +134,46 @@ impl GotocHook for Assert {

let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span);

// Since `cond` might have side effects, assign it to a temporary
// variable so that it's evaluated once, then assert and assume it
// TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps
let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc);
Stmt::block(
vec![
reach_stmt,
decl,
gcx.codegen_assert_assume(tmp, PropertyClass::Assertion, &msg, caller_loc),
gcx.codegen_assert_assume(cond, PropertyClass::Assertion, &msg, caller_loc),
Stmt::goto(bb_label(target), caller_loc),
],
caller_loc,
)
}
}

struct UnsupportedCheck;
impl GotocHook for UnsupportedCheck {
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
unreachable!("{UNEXPECTED_CALL}")
}

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 msg = fargs.pop().unwrap();
let cond = fargs.pop().unwrap().cast_to(Type::bool());
let msg = gcx.extract_const_message(&msg).unwrap();
let target = target.unwrap();
let caller_loc = gcx.codegen_caller_span_stable(span);
Stmt::block(
vec![
gcx.codegen_assert_assume(
cond,
PropertyClass::UnsupportedConstruct,
&msg,
caller_loc,
),
Stmt::goto(bb_label(target), caller_loc),
],
caller_loc,
Expand All @@ -166,8 +197,8 @@ impl GotocHook for SafetyCheck {
span: Span,
) -> Stmt {
assert_eq!(fargs.len(), 2);
let cond = fargs.remove(0).cast_to(Type::bool());
let msg = fargs.remove(0);
let msg = fargs.pop().unwrap();
let cond = fargs.pop().unwrap().cast_to(Type::bool());
let msg = gcx.extract_const_message(&msg).unwrap();
let target = target.unwrap();
let caller_loc = gcx.codegen_caller_span_stable(span);
Expand All @@ -181,6 +212,7 @@ impl GotocHook for SafetyCheck {
}
}

// TODO: Remove this and replace occurrences with `SanityCheck`.
struct Check;
impl GotocHook for Check {
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
Expand Down Expand Up @@ -709,6 +741,7 @@ pub fn fn_hooks() -> GotocHooks {
(KaniHook::IsAllocated, Rc::new(IsAllocated)),
(KaniHook::PointerObject, Rc::new(PointerObject)),
(KaniHook::PointerOffset, Rc::new(PointerOffset)),
(KaniHook::UnsupportedCheck, Rc::new(UnsupportedCheck)),
(KaniHook::UntrackedDeref, Rc::new(UntrackedDeref)),
(KaniHook::InitContracts, Rc::new(InitContracts)),
(KaniHook::FloatToIntInRange, Rc::new(FloatToIntInRange)),
Expand Down
4 changes: 4 additions & 0 deletions kani-compiler/src/kani_middle/kani_functions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,8 @@ pub enum KaniModel {
IsSliceChunkPtrInitialized,
#[strum(serialize = "IsSlicePtrInitializedModel")]
IsSlicePtrInitialized,
#[strum(serialize = "OffsetModel")]
Offset,
#[strum(serialize = "RunContractModel")]
RunContract,
#[strum(serialize = "RunLoopContractModel")]
Expand Down Expand Up @@ -140,6 +142,8 @@ pub enum KaniHook {
PointerOffset,
#[strum(serialize = "SafetyCheckHook")]
SafetyCheck,
#[strum(serialize = "UnsupportedCheckHook")]
UnsupportedCheck,
#[strum(serialize = "UntrackedDerefHook")]
UntrackedDeref,
}
Expand Down
5 changes: 5 additions & 0 deletions kani-compiler/src/kani_middle/transform/body.rs
Original file line number Diff line number Diff line change
Expand Up @@ -434,6 +434,11 @@ impl MutableBody {
) {
self.blocks.get_mut(source_instruction.bb()).unwrap().terminator = new_term;
}

/// Remove the given statement.
pub fn remove_stmt(&mut self, bb: BasicBlockIdx, stmt: usize) {
self.blocks[bb].statements.remove(stmt);
}
}

// TODO: Remove this enum, since we now only support kani's assert.
Expand Down
117 changes: 107 additions & 10 deletions kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,21 @@
use crate::intrinsics::Intrinsic;
use crate::kani_middle::kani_functions::{KaniFunction, KaniModel};
use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody};
use crate::kani_middle::transform::body::{
InsertPosition, MutMirVisitor, MutableBody, SourceInstruction,
};
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::mir::mono::Instance;
use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind};
use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
use stable_mir::mir::{
BasicBlockIdx, BinOp, Body, ConstOperand, LocalDecl, Operand, Rvalue, StatementKind,
Terminator, TerminatorKind,
};
use stable_mir::ty::{
FnDef, GenericArgKind, GenericArgs, IntTy, MirConst, RigidTy, Span, Ty, TyKind, UintTy,
};
use std::collections::HashMap;
use tracing::debug;

Expand Down Expand Up @@ -42,12 +50,14 @@ impl TransformPass for RustcIntrinsicsPass {

/// 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(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
debug!(function=?instance.name(), "transform");
let mut new_body = MutableBody::from(body);
let mut visitor = ReplaceIntrinsicVisitor::new(&self.models, new_body.locals().to_vec());
let mut visitor =
ReplaceIntrinsicCallVisitor::new(&self.models, new_body.locals().to_vec());
visitor.visit_body(&mut new_body);
(visitor.changed, new_body.into())
let changed = self.replace_lowered_intrinsics(tcx, &mut new_body);
(visitor.changed || changed, new_body.into())
}
}

Expand All @@ -63,21 +73,78 @@ impl RustcIntrinsicsPass {
debug!(?models, "RustcIntrinsicsPass::new");
RustcIntrinsicsPass { models }
}

/// This function checks if we need to replace intrinsics that have been lowered.
fn replace_lowered_intrinsics(&self, tcx: TyCtxt, body: &mut MutableBody) -> bool {
// Do a reverse iteration on the instructions since we will replace Rvalues by a function
// call, which will split the basic block.
let mut changed = false;
let orig_bbs = body.blocks().len();
for bb in (0..orig_bbs).rev() {
let num_stmts = body.blocks()[bb].statements.len();
for stmt in (0..num_stmts).rev() {
changed |= self.replace_offset(tcx, body, bb, stmt);
}
}
changed
}

/// Replace a lowered offset intrinsic.
fn replace_offset(
&self,
tcx: TyCtxt,
body: &mut MutableBody,
bb: BasicBlockIdx,
stmt: usize,
) -> bool {
let statement = &body.blocks()[bb].statements[stmt];
let StatementKind::Assign(place, rvalue) = &statement.kind else {
return false;
};
let Rvalue::BinaryOp(BinOp::Offset, op1, op2) = rvalue else { return false };
let mut source = SourceInstruction::Statement { idx: stmt, bb };

// Double check input parameters of `offset` operation.
let offset_ty = op2.ty(body.locals()).unwrap();
let pointer_ty = op1.ty(body.locals()).unwrap();
validate_offset(tcx, offset_ty, statement.span);
validate_raw_ptr(tcx, pointer_ty, statement.span);
tcx.dcx().abort_if_errors();

let pointee_ty = pointer_ty.kind().builtin_deref(true).unwrap().ty;
// The model takes the following parameters (PointeeType, PointerType, OffsetType).
let model = self.models[&KaniModel::Offset];
let params = vec![
GenericArgKind::Type(pointee_ty),
GenericArgKind::Type(pointer_ty),
GenericArgKind::Type(offset_ty),
];
let instance = Instance::resolve(model, &GenericArgs(params)).unwrap();
body.insert_call(
&instance,
&mut source,
InsertPosition::After,
vec![op1.clone(), op2.clone()],
place.clone(),
);
body.remove_stmt(bb, stmt);
true
}
}

struct ReplaceIntrinsicVisitor<'a> {
struct ReplaceIntrinsicCallVisitor<'a> {
models: &'a HashMap<KaniModel, FnDef>,
locals: Vec<LocalDecl>,
changed: bool,
}

impl<'a> ReplaceIntrinsicVisitor<'a> {
impl<'a> ReplaceIntrinsicCallVisitor<'a> {
fn new(models: &'a HashMap<KaniModel, FnDef>, locals: Vec<LocalDecl>) -> Self {
ReplaceIntrinsicVisitor { models, locals, changed: false }
ReplaceIntrinsicCallVisitor { models, locals, changed: false }
}
}

impl MutMirVisitor for ReplaceIntrinsicVisitor<'_> {
impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> {
/// Replace the terminator for some rustc's intrinsics.
///
/// In some cases, we replace a function call to a rustc intrinsic by a call to the
Expand Down Expand Up @@ -117,3 +184,33 @@ impl MutMirVisitor for ReplaceIntrinsicVisitor<'_> {
self.super_terminator(term);
}
}

/// Validate whether the offset type is valid, i.e., `isize` or `usize`.
///
/// This will emit an error if the type is wrong but not abort.
/// Invoke `tcx.dcx().abort_if_errors()` to abort execution.
fn validate_offset(tcx: TyCtxt, offset_ty: Ty, span: Span) {
if !matches!(
offset_ty.kind(),
TyKind::RigidTy(RigidTy::Int(IntTy::Isize)) | TyKind::RigidTy(RigidTy::Uint(UintTy::Usize))
) {
tcx.dcx().span_err(
rustc_internal::internal(tcx, span),
format!("Expected `isize` or `usize` for offset type. Found `{offset_ty}` instead"),
);
}
}

/// Validate that we have a raw pointer otherwise emit an error.
///
/// This will emit an error if the type is wrong but not abort.
/// Invoke `tcx.dcx().abort_if_errors()` to abort execution.
fn validate_raw_ptr(tcx: TyCtxt, ptr_ty: Ty, span: Span) {
let pointer_ty_kind = ptr_ty.kind();
if !pointer_ty_kind.is_raw_ptr() {
tcx.dcx().span_err(
rustc_internal::internal(tcx, span),
format!("Expected raw pointer for pointer type. Found `{ptr_ty}` instead"),
);
}
}
14 changes: 14 additions & 0 deletions library/kani_core/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -308,6 +308,20 @@ macro_rules! kani_intrinsics {
assert!(cond, "Safety check failed: {msg}");
}

/// This should indicate that Kani does not support a certain operation.
#[doc(hidden)]
#[allow(dead_code)]
#[kanitool::fn_marker = "UnsupportedCheckHook"]
#[inline(never)]
#[allow(clippy::diverging_sub_expression)]
pub(crate) fn unsupported(msg: &'static str) -> ! {
#[cfg(not(feature = "concrete_playback"))]
return kani_intrinsic();

#[cfg(feature = "concrete_playback")]
unimplemented!("Unsupported Kani operation: {msg}")
}

/// An empty body that can be used to define Kani intrinsic functions.
///
/// A Kani intrinsic is a function that is interpreted by Kani compiler.
Expand Down
Loading

0 comments on commit 2334f2c

Please sign in to comment.