Skip to content

Commit 7139063

Browse files
celinvaladpaco-aws
celinval
and
adpaco-aws
authored
Upgrade rust toolchain to nightly-2023-06-20 (rust-lang#2551)
Change Kani's compiler and tests to adapt to changes done to the toolchain. The biggest changes were: Implement overflow checks as part of rvalue.rs instead of intrinsics due to lowering of intrinsics to BinOp. Add a unsupported check for handling C string literals. Co-authored-by: Adrian Palacios <[email protected]>
1 parent 8b89160 commit 7139063

File tree

24 files changed

+325
-114
lines changed

24 files changed

+325
-114
lines changed

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

Lines changed: 5 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,7 @@ use super::typ::{self, pointee_type};
55
use super::PropertyClass;
66
use crate::codegen_cprover_gotoc::GotocCtx;
77
use cbmc::goto_program::{
8-
arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr,
9-
Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
8+
ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
109
};
1110
use rustc_middle::mir::{BasicBlock, Operand, Place};
1211
use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement};
@@ -183,43 +182,6 @@ impl<'tcx> GotocCtx<'tcx> {
183182
}};
184183
}
185184

186-
// Intrinsics which encode a simple arithmetic operation with overflow check
187-
macro_rules! codegen_op_with_overflow_check {
188-
($f:ident) => {{
189-
let a = fargs.remove(0);
190-
let b = fargs.remove(0);
191-
let op_type = a.typ().clone();
192-
let res = a.$f(b);
193-
// add to symbol table
194-
let struct_tag = self.codegen_arithmetic_overflow_result_type(op_type.clone());
195-
assert_eq!(*res.typ(), struct_tag);
196-
197-
// store the result in a temporary variable
198-
let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc);
199-
let check = self.codegen_assert(
200-
var.clone()
201-
.member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table)
202-
.cast_to(Type::c_bool())
203-
.not(),
204-
PropertyClass::ArithmeticOverflow,
205-
format!("attempt to compute {} which would overflow", intrinsic).as_str(),
206-
loc,
207-
);
208-
self.codegen_expr_to_place(
209-
p,
210-
Expr::statement_expression(
211-
vec![
212-
decl,
213-
check,
214-
var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table)
215-
.as_stmt(loc),
216-
],
217-
op_type,
218-
),
219-
)
220-
}};
221-
}
222-
223185
// Intrinsics which encode a division operation with overflow check
224186
macro_rules! codegen_op_with_div_overflow_check {
225187
($f:ident) => {{
@@ -617,19 +579,12 @@ impl<'tcx> GotocCtx<'tcx> {
617579
"unaligned_volatile_load" => {
618580
unstable_codegen!(self.codegen_expr_to_place(p, fargs.remove(0).dereference()))
619581
}
620-
"unchecked_add" => codegen_op_with_overflow_check!(add_overflow_result),
582+
"unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr"
583+
| "unchecked_sub" => {
584+
unreachable!("Expected intrinsic `{intrinsic}` to be lowered before codegen")
585+
}
621586
"unchecked_div" => codegen_op_with_div_overflow_check!(div),
622-
"unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow_result),
623587
"unchecked_rem" => codegen_op_with_div_overflow_check!(rem),
624-
"unchecked_shl" => codegen_intrinsic_binop!(shl),
625-
"unchecked_shr" => {
626-
if fargs[0].typ().is_signed(self.symbol_table.machine_model()) {
627-
codegen_intrinsic_binop!(ashr)
628-
} else {
629-
codegen_intrinsic_binop!(lshr)
630-
}
631-
}
632-
"unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow_result),
633588
"unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)),
634589
"unreachable" => unreachable!(
635590
"Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
@@ -1808,19 +1763,4 @@ impl<'tcx> GotocCtx<'tcx> {
18081763
);
18091764
(size_of_count_elems.result, assert_stmt)
18101765
}
1811-
1812-
/// Codegens the struct type that CBMC produces for its arithmetic with overflow operators:
1813-
/// ```
1814-
/// struct overflow_result_<operand_type> {
1815-
/// operand_type result; // the result of the operation
1816-
/// bool overflowed; // whether the operation overflowed
1817-
/// }
1818-
/// ```
1819-
/// and adds the type to the symbol table
1820-
fn codegen_arithmetic_overflow_result_type(&mut self, operand_type: Type) -> Type {
1821-
let res_type = arithmetic_overflow_result_type(operand_type);
1822-
self.ensure_struct(res_type.tag().unwrap(), res_type.tag().unwrap(), |_, _| {
1823-
res_type.components().unwrap().clone()
1824-
})
1825-
}
18261766
}

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -227,6 +227,19 @@ impl<'tcx> GotocCtx<'tcx> {
227227
);
228228
}
229229
}
230+
ty::Adt(def, _) if Some(def.did()) == self.tcx.lang_items().c_str() => {
231+
// TODO: Handle CString
232+
// <https://github.com/model-checking/kani/issues/2549>
233+
let loc = self.codegen_span_option(span.cloned());
234+
let typ = self.codegen_ty(lit_ty);
235+
let operation_name = "C string literal";
236+
return self.codegen_unimplemented_expr(
237+
&operation_name,
238+
typ,
239+
loc,
240+
"https://github.com/model-checking/kani/issues/2549",
241+
);
242+
}
230243
_ => {}
231244
}
232245
}

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

Lines changed: 115 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -163,6 +163,52 @@ impl<'tcx> GotocCtx<'tcx> {
163163
}
164164
}
165165

166+
/// Generate code for a binary operation with an overflow check.
167+
fn codegen_binop_with_overflow_check(
168+
&mut self,
169+
op: &BinOp,
170+
left_op: &Operand<'tcx>,
171+
right_op: &Operand<'tcx>,
172+
loc: Location,
173+
) -> Expr {
174+
debug!(?op, "codegen_binop_with_overflow_check");
175+
let left = self.codegen_operand(left_op);
176+
let right = self.codegen_operand(right_op);
177+
let ret_type = left.typ().clone();
178+
let (bin_op, op_name) = match op {
179+
BinOp::AddUnchecked => (BinaryOperator::OverflowResultPlus, "unchecked_add"),
180+
BinOp::SubUnchecked => (BinaryOperator::OverflowResultMinus, "unchecked_sub"),
181+
BinOp::MulUnchecked => (BinaryOperator::OverflowResultMult, "unchecked_mul"),
182+
_ => unreachable!("Expected Add/Sub/Mul but got {op:?}"),
183+
};
184+
// Create CBMC result type and add to the symbol table.
185+
let res_type = arithmetic_overflow_result_type(left.typ().clone());
186+
let tag = res_type.tag().unwrap();
187+
let struct_tag =
188+
self.ensure_struct(tag, tag, |_, _| res_type.components().unwrap().clone());
189+
let res = left.overflow_op(bin_op, right);
190+
// store the result in a temporary variable
191+
let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc);
192+
// cast into result type
193+
let check = self.codegen_assert(
194+
var.clone()
195+
.member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table)
196+
.cast_to(Type::c_bool())
197+
.not(),
198+
PropertyClass::ArithmeticOverflow,
199+
format!("attempt to compute `{op_name}` which would overflow").as_str(),
200+
loc,
201+
);
202+
Expr::statement_expression(
203+
vec![
204+
decl,
205+
check,
206+
var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table).as_stmt(loc),
207+
],
208+
ret_type,
209+
)
210+
}
211+
166212
/// Generate code for a binary operation with an overflow and returns a tuple (res, overflow).
167213
pub fn codegen_binop_with_overflow(
168214
&mut self,
@@ -297,7 +343,28 @@ impl<'tcx> GotocCtx<'tcx> {
297343
BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Shl | BinOp::Shr => {
298344
self.codegen_scalar_binop(op, e1, e2)
299345
}
300-
BinOp::Div | BinOp::Rem | BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => {
346+
// We currently rely on CBMC's UB checks for shift which isn't always accurate.
347+
// We should implement the checks ourselves.
348+
// See https://github.com/model-checking/kani/issues/2374
349+
BinOp::ShlUnchecked => self.codegen_scalar_binop(&BinOp::Shl, e1, e2),
350+
BinOp::ShrUnchecked => self.codegen_scalar_binop(&BinOp::Shr, e1, e2),
351+
BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => {
352+
self.codegen_binop_with_overflow_check(op, e1, e2, loc)
353+
}
354+
BinOp::Div | BinOp::Rem => {
355+
let result = self.codegen_unchecked_scalar_binop(op, e1, e2);
356+
if self.operand_ty(e1).is_integral() {
357+
let is_rem = matches!(op, BinOp::Rem);
358+
let check = self.check_div_overflow(e1, e2, is_rem, loc);
359+
Expr::statement_expression(
360+
vec![check, result.clone().as_stmt(loc)],
361+
result.typ().clone(),
362+
)
363+
} else {
364+
result
365+
}
366+
}
367+
BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => {
301368
self.codegen_unchecked_scalar_binop(op, e1, e2)
302369
}
303370
BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
@@ -341,6 +408,53 @@ impl<'tcx> GotocCtx<'tcx> {
341408
}
342409
}
343410

411+
/// Check that a division does not overflow.
412+
/// For integer types, division by zero is UB, as is MIN / -1 for signed.
413+
/// Note that the compiler already inserts these checks for regular division.
414+
/// However, since <https://github.com/rust-lang/rust/pull/112168>, unchecked divisions are
415+
/// lowered to `BinOp::Div`. Prefer adding duplicated checks for now.
416+
fn check_div_overflow(
417+
&mut self,
418+
dividend: &Operand<'tcx>,
419+
divisor: &Operand<'tcx>,
420+
is_remainder: bool,
421+
loc: Location,
422+
) -> Stmt {
423+
let divisor_expr = self.codegen_operand(divisor);
424+
let msg = if is_remainder {
425+
"attempt to calculate the remainder with a divisor of zero"
426+
} else {
427+
"attempt to divide by zero"
428+
};
429+
let div_by_zero_check = self.codegen_assert_assume(
430+
divisor_expr.clone().is_zero().not(),
431+
PropertyClass::ArithmeticOverflow,
432+
msg,
433+
loc,
434+
);
435+
if self.operand_ty(dividend).is_signed() {
436+
let dividend_expr = self.codegen_operand(dividend);
437+
let overflow_msg = if is_remainder {
438+
"attempt to calculate the remainder with overflow"
439+
} else {
440+
"attempt to divide with overflow"
441+
};
442+
let overflow_expr = dividend_expr
443+
.clone()
444+
.eq(dividend_expr.typ().min_int_expr(self.symbol_table.machine_model()))
445+
.and(divisor_expr.clone().eq(Expr::int_constant(-1, divisor_expr.typ().clone())));
446+
let overflow_check = self.codegen_assert_assume(
447+
overflow_expr.not(),
448+
PropertyClass::ArithmeticOverflow,
449+
overflow_msg,
450+
loc,
451+
);
452+
Stmt::block(vec![overflow_check, div_by_zero_check], loc)
453+
} else {
454+
div_by_zero_check
455+
}
456+
}
457+
344458
/// Create an initializer for a generator struct.
345459
fn codegen_rvalue_generator(
346460
&mut self,

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ impl<'tcx> GotocCtx<'tcx> {
149149
"unreachable code",
150150
loc,
151151
),
152-
TerminatorKind::Drop { place, target, unwind: _ } => {
152+
TerminatorKind::Drop { place, target, unwind: _, replace: _ } => {
153153
self.codegen_drop(place, target, loc)
154154
}
155155
TerminatorKind::Call { func, args, destination, target, .. } => {
@@ -161,12 +161,12 @@ impl<'tcx> GotocCtx<'tcx> {
161161
if *expected { r } else { Expr::not(r) }
162162
};
163163

164-
let msg = if let AssertKind::BoundsCheck { .. } = msg {
164+
let msg = if let AssertKind::BoundsCheck { .. } = &**msg {
165165
// For bounds check the following panic message is generated at runtime:
166166
// "index out of bounds: the length is {len} but the index is {index}",
167167
// but CBMC only accepts static messages so we don't add values to the message.
168168
"index out of bounds: the length is less than or equal to the given index"
169-
} else if let AssertKind::MisalignedPointerDereference { .. } = msg {
169+
} else if let AssertKind::MisalignedPointerDereference { .. } = &**msg {
170170
// Misaligned pointer dereference check messages is also a runtime messages.
171171
// Generate a generic one here.
172172
"misaligned pointer dereference: address must be a multiple of its type's alignment"

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -303,7 +303,7 @@ impl<'tcx> GotocCtx<'tcx> {
303303
var: ty::BoundVar::from_usize(bound_vars.len() - 1),
304304
kind: ty::BoundRegionKind::BrEnv,
305305
};
306-
let env_region = self.tcx.mk_re_late_bound(ty::INNERMOST, br);
306+
let env_region = ty::Region::new_late_bound(self.tcx, ty::INNERMOST, br);
307307
let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap();
308308

309309
let sig = sig.skip_binder();
@@ -345,7 +345,7 @@ impl<'tcx> GotocCtx<'tcx> {
345345
kind: ty::BoundRegionKind::BrEnv,
346346
};
347347
let env_region = ty::ReLateBound(ty::INNERMOST, br);
348-
let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region_from_kind(env_region), ty);
348+
let env_ty = self.tcx.mk_mut_ref(ty::Region::new_from_kind(self.tcx, env_region), ty);
349349

350350
let pin_did = self.tcx.require_lang_item(LangItem::Pin, None);
351351
let pin_adt_ref = self.tcx.adt_def(pin_did);
@@ -429,7 +429,7 @@ impl<'tcx> GotocCtx<'tcx> {
429429
current_fn.instance().subst_mir_and_normalize_erasing_regions(
430430
self.tcx,
431431
ty::ParamEnv::reveal_all(),
432-
value,
432+
ty::EarlyBinder::bind(value),
433433
)
434434
} else {
435435
// TODO: confirm with rust team there is no way to monomorphize
@@ -665,8 +665,8 @@ impl<'tcx> GotocCtx<'tcx> {
665665
}
666666
_ => {
667667
// This hash is documented to be the same no matter the crate context
668-
let id_u64 = self.tcx.type_id_hash(t).as_u64();
669-
format!("_{id_u64}").intern()
668+
let id = self.tcx.type_id_hash(t).as_u128();
669+
format!("_{id}").intern()
670670
}
671671
}
672672
}

0 commit comments

Comments
 (0)