Skip to content

Commit ed7e698

Browse files
celinvalcelinval
committed
Implement bounds check on offset
Still need to adjust tests
1 parent ceb87da commit ed7e698

File tree

18 files changed

+423
-97
lines changed

18 files changed

+423
-97
lines changed

‎kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ pub enum PropertyClass {
3838
/// Overflow panics that can be generated by Intrisics.
3939
/// NOTE: Not all uses of this are found by rust-analyzer because of the use of macros. Try grep instead.
4040
///
41-
/// SPECIAL BEHAVIOR: None TODO: Why should this exist?
41+
/// SPECIAL BEHAVIOR: Same as SafetyCheck.
4242
ArithmeticOverflow,
4343
/// The Rust `assume` instrinsic is `assert`'d by Kani, and gets this property class.
4444
///
@@ -67,13 +67,13 @@ pub enum PropertyClass {
6767
/// That is, they do not depend on special instrumentation that Kani performs that wouldn't
6868
/// otherwise be observable.
6969
Assertion,
70-
/// Another instrinsic check.
70+
/// Another intrinsic check.
7171
///
72-
/// SPECIAL BEHAVIOR: None TODO: Why should this exist?
72+
/// SPECIAL BEHAVIOR: Same as SafetyCheck
7373
ExactDiv,
74-
/// Another instrinsic check.
74+
/// Another intrinsic check.
7575
///
76-
/// SPECIAL BEHAVIOR: None TODO: Why should this exist?
76+
/// SPECIAL BEHAVIOR: Same as SafetyCheck
7777
FiniteCheck,
7878
/// Checks added by Kani compiler to determine whether a property (e.g.
7979
/// `PropertyClass::Assertion` or `PropertyClass:Cover`) is reachable
@@ -82,6 +82,7 @@ pub enum PropertyClass {
8282
/// E.g., things that trigger UB or unstable behavior.
8383
///
8484
/// SPECIAL BEHAVIOR: Assertions that may not exist when running code normally (i.e. not under Kani)
85+
/// This is not caught by `#[should_panic]`.
8586
SafetyCheck,
8687
/// Checks to ensure that Kani's code generation is correct.
8788
///

‎kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1015,7 +1015,7 @@ impl GotocCtx<'_> {
10151015
///
10161016
/// This function handles code generation for the `arith_offset` intrinsic.
10171017
/// <https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html>
1018-
/// According to the documenation, the operation is always safe.
1018+
/// According to the documentation, the operation is always safe.
10191019
fn codegen_arith_offset(&mut self, mut fargs: Vec<Expr>, p: &Place, loc: Location) -> Stmt {
10201020
let src_ptr = fargs.remove(0);
10211021
let offset = fargs.remove(0);

‎kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs‎

Lines changed: 8 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -356,7 +356,7 @@ impl GotocCtx<'_> {
356356

357357
fn codegen_rvalue_binary_op(
358358
&mut self,
359-
ty: Ty,
359+
_ty: Ty,
360360
op: &BinOp,
361361
e1: &Operand,
362362
e2: &Operand,
@@ -405,42 +405,15 @@ impl GotocCtx<'_> {
405405
}
406406
// https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
407407
BinOp::Offset => {
408+
// We don't need to check for UB since we handled user calls of offset already
409+
// via rustc_intrinsic transformation pass.
410+
//
411+
// This operation may still be used by other Kani instrumentation which should
412+
// ensure safety.
413+
// We should consider adding sanity checks if `debug_assertions` are enabled.
408414
let ce1 = self.codegen_operand_stable(e1);
409415
let ce2 = self.codegen_operand_stable(e2);
410-
411-
// Check that computing `offset` in bytes would not overflow
412-
let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(
413-
ce2.clone().cast_to(Type::ssize_t()),
414-
pointee_type_stable(ty).unwrap(),
415-
Type::ssize_t(),
416-
"offset",
417-
loc,
418-
);
419-
420-
// Check that the computation would not overflow an `isize` which is UB:
421-
// https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
422-
// These checks may allow a wrapping-around behavior in CBMC:
423-
// https://github.com/model-checking/kani/issues/1150
424-
// Note(std): We don't check that the starting or resulting pointer stay
425-
// within bounds of the object they point to. Doing so causes spurious
426-
// failures due to the usage of these intrinsics in the standard library.
427-
// See <https://github.com/model-checking/kani/issues/1233> for more details.
428-
// Note that this is one of the safety conditions for `offset`:
429-
// <https://doc.rust-lang.org/std/primitive.pointer.html#safety-2>
430-
431-
let overflow_res = ce1.clone().cast_to(Type::ssize_t()).add_overflow(offset_bytes);
432-
let overflow_check = self.codegen_assert_assume(
433-
overflow_res.overflowed.not(),
434-
PropertyClass::ArithmeticOverflow,
435-
"attempt to compute offset which would overflow",
436-
loc,
437-
);
438-
let res = ce1.clone().plus(ce2);
439-
Expr::statement_expression(
440-
vec![bytes_overflow_check, overflow_check, res.as_stmt(loc)],
441-
ce1.typ().clone(),
442-
loc,
443-
)
416+
ce1.clone().plus(ce2)
444417
}
445418
}
446419
}

‎kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs‎

Lines changed: 51 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -134,22 +134,36 @@ impl GotocHook for Assert {
134134

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

137-
// Since `cond` might have side effects, assign it to a temporary
138-
// variable so that it's evaluated once, then assert and assume it
139-
// TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps
140-
let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc);
141137
Stmt::block(
142138
vec![
143139
reach_stmt,
144-
decl,
145-
gcx.codegen_assert_assume(tmp, PropertyClass::Assertion, &msg, caller_loc),
140+
gcx.codegen_assert_assume(cond, PropertyClass::Assertion, &msg, caller_loc),
146141
Stmt::goto(bb_label(target), caller_loc),
147142
],
148143
caller_loc,
149144
)
150145
}
151146
}
152147

148+
struct UnsupportedCheck;
149+
impl GotocHook for UnsupportedCheck {
150+
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
151+
unreachable!("{UNEXPECTED_CALL}")
152+
}
153+
154+
fn handle(
155+
&self,
156+
gcx: &mut GotocCtx,
157+
_instance: Instance,
158+
fargs: Vec<Expr>,
159+
_assign_to: &Place,
160+
target: Option<BasicBlockIdx>,
161+
span: Span,
162+
) -> Stmt {
163+
check_hook(PropertyClass::UnsupportedConstruct, gcx, fargs, target, span)
164+
}
165+
}
166+
153167
struct SafetyCheck;
154168
impl GotocHook for SafetyCheck {
155169
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
@@ -160,24 +174,12 @@ impl GotocHook for SafetyCheck {
160174
&self,
161175
gcx: &mut GotocCtx,
162176
_instance: Instance,
163-
mut fargs: Vec<Expr>,
177+
fargs: Vec<Expr>,
164178
_assign_to: &Place,
165179
target: Option<BasicBlockIdx>,
166180
span: Span,
167181
) -> Stmt {
168-
assert_eq!(fargs.len(), 2);
169-
let cond = fargs.remove(0).cast_to(Type::bool());
170-
let msg = fargs.remove(0);
171-
let msg = gcx.extract_const_message(&msg).unwrap();
172-
let target = target.unwrap();
173-
let caller_loc = gcx.codegen_caller_span_stable(span);
174-
Stmt::block(
175-
vec![
176-
gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc),
177-
Stmt::goto(bb_label(target), caller_loc),
178-
],
179-
caller_loc,
180-
)
182+
check_hook(PropertyClass::SafetyCheck, gcx, fargs, target, span)
181183
}
182184
}
183185

@@ -205,10 +207,15 @@ impl GotocHook for Check {
205207

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

210+
// Since `cond` might have side effects, assign it to a temporary
211+
// variable so that it's evaluated once, then assert and assume it
212+
// TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps
213+
let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc);
208214
Stmt::block(
209215
vec![
210216
reach_stmt,
211-
gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc),
217+
decl,
218+
gcx.codegen_assert(tmp, PropertyClass::Assertion, &msg, caller_loc),
212219
Stmt::goto(bb_label(target), caller_loc),
213220
],
214221
caller_loc,
@@ -709,6 +716,7 @@ pub fn fn_hooks() -> GotocHooks {
709716
(KaniHook::IsAllocated, Rc::new(IsAllocated)),
710717
(KaniHook::PointerObject, Rc::new(PointerObject)),
711718
(KaniHook::PointerOffset, Rc::new(PointerOffset)),
719+
(KaniHook::UnsupportedCheck, Rc::new(UnsupportedCheck)),
712720
(KaniHook::UntrackedDeref, Rc::new(UntrackedDeref)),
713721
(KaniHook::InitContracts, Rc::new(InitContracts)),
714722
(KaniHook::FloatToIntInRange, Rc::new(FloatToIntInRange)),
@@ -747,3 +755,25 @@ impl GotocHooks {
747755
}
748756
}
749757
}
758+
759+
fn check_hook(
760+
prop_class: PropertyClass,
761+
gcx: &mut GotocCtx,
762+
mut fargs: Vec<Expr>,
763+
target: Option<BasicBlockIdx>,
764+
span: Span,
765+
) -> Stmt {
766+
assert_eq!(fargs.len(), 2);
767+
let msg = fargs.pop().unwrap();
768+
let cond = fargs.pop().unwrap().cast_to(Type::bool());
769+
let msg = gcx.extract_const_message(&msg).unwrap();
770+
let target = target.unwrap();
771+
let caller_loc = gcx.codegen_caller_span_stable(span);
772+
Stmt::block(
773+
vec![
774+
gcx.codegen_assert_assume(cond, prop_class, &msg, caller_loc),
775+
Stmt::goto(bb_label(target), caller_loc),
776+
],
777+
caller_loc,
778+
)
779+
}

‎kani-compiler/src/kani_middle/kani_functions.rs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,8 @@ pub enum KaniModel {
8181
IsSliceChunkPtrInitialized,
8282
#[strum(serialize = "IsSlicePtrInitializedModel")]
8383
IsSlicePtrInitialized,
84+
#[strum(serialize = "OffsetModel")]
85+
Offset,
8486
#[strum(serialize = "RunContractModel")]
8587
RunContract,
8688
#[strum(serialize = "RunLoopContractModel")]
@@ -140,6 +142,8 @@ pub enum KaniHook {
140142
PointerOffset,
141143
#[strum(serialize = "SafetyCheckHook")]
142144
SafetyCheck,
145+
#[strum(serialize = "UnsupportedCheckHook")]
146+
UnsupportedCheck,
143147
#[strum(serialize = "UntrackedDerefHook")]
144148
UntrackedDeref,
145149
}

‎kani-compiler/src/kani_middle/transform/body.rs‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -434,6 +434,11 @@ impl MutableBody {
434434
) {
435435
self.blocks.get_mut(source_instruction.bb()).unwrap().terminator = new_term;
436436
}
437+
438+
/// Remove the given statement.
439+
pub fn remove_stmt(&mut self, bb: BasicBlockIdx, stmt: usize) {
440+
self.blocks[bb].statements.remove(stmt);
441+
}
437442
}
438443

439444
// TODO: Remove this enum, since we now only support kani's assert.

0 commit comments

Comments
 (0)