Upgrade rust toolchain to nightly-2023-06-20

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

@@ -5,8 +5,7 @@ use super::typ::{self, pointee_type};
 use super::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{
- arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr,
- Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
+ ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
 };
 use rustc_middle::mir::{BasicBlock, Operand, Place};
 use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement};
@@ -183,43 +182,6 @@ impl<'tcx> GotocCtx<'tcx> {
  }};
  }
 
- // Intrinsics which encode a simple arithmetic operation with overflow check
- macro_rules! codegen_op_with_overflow_check {
- ($f:ident) => {{
- let a = fargs.remove(0);
- let b = fargs.remove(0);
- let op_type = a.typ().clone();
- let res = a.$f(b);
- // add to symbol table
- let struct_tag = self.codegen_arithmetic_overflow_result_type(op_type.clone());
- assert_eq!(*res.typ(), struct_tag);
-
- // store the result in a temporary variable
- let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc);
- let check = self.codegen_assert(
- var.clone()
- .member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table)
- .cast_to(Type::c_bool())
- .not(),
- PropertyClass::ArithmeticOverflow,
- format!("attempt to compute {} which would overflow", intrinsic).as_str(),
- loc,
- );
- self.codegen_expr_to_place(
- p,
- Expr::statement_expression(
- vec![
- decl,
- check,
- var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table)
- .as_stmt(loc),
- ],
- op_type,
- ),
- )
- }};
- }
-
  // Intrinsics which encode a division operation with overflow check
  macro_rules! codegen_op_with_div_overflow_check {
  ($f:ident) => {{
@@ -617,19 +579,12 @@ impl<'tcx> GotocCtx<'tcx> {
  "unaligned_volatile_load" => {
  unstable_codegen!(self.codegen_expr_to_place(p, fargs.remove(0).dereference()))
  }
- "unchecked_add" => codegen_op_with_overflow_check!(add_overflow_result),
+ "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr"
+ | "unchecked_sub" => {
+ unreachable!("Expected intrinsic `{intrinsic}` to be lowered before codegen")
+ }
  "unchecked_div" => codegen_op_with_div_overflow_check!(div),
- "unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow_result),
  "unchecked_rem" => codegen_op_with_div_overflow_check!(rem),
- "unchecked_shl" => codegen_intrinsic_binop!(shl),
- "unchecked_shr" => {
- if fargs[0].typ().is_signed(self.symbol_table.machine_model()) {
- codegen_intrinsic_binop!(ashr)
- } else {
- codegen_intrinsic_binop!(lshr)
- }
- }
- "unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow_result),
  "unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)),
  "unreachable" => unreachable!(
  "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
@@ -1808,19 +1763,4 @@ impl<'tcx> GotocCtx<'tcx> {
  );
  (size_of_count_elems.result, assert_stmt)
  }
-
- /// Codegens the struct type that CBMC produces for its arithmetic with overflow operators:
- /// ```
- /// struct overflow_result_<operand_type> {
- /// operand_type result; // the result of the operation
- /// bool overflowed; // whether the operation overflowed
- /// }
- /// ```
- /// and adds the type to the symbol table
- fn codegen_arithmetic_overflow_result_type(&mut self, operand_type: Type) -> Type {
- let res_type = arithmetic_overflow_result_type(operand_type);
- self.ensure_struct(res_type.tag().unwrap(), res_type.tag().unwrap(), |_, _| {
- res_type.components().unwrap().clone()
- })
- }
 }

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

@@ -227,6 +227,19 @@ impl<'tcx> GotocCtx<'tcx> {
  );
  }
  }
+ ty::Adt(def, _) if Some(def.did()) == self.tcx.lang_items().c_str() => {
+ // TODO: Handle CString
+ // <https://github.com/model-checking/kani/issues/2549>
+ let loc = self.codegen_span_option(span.cloned());
+ let typ = self.codegen_ty(lit_ty);
+ let operation_name = "C string literal";
+ return self.codegen_unimplemented_expr(
+ &operation_name,
+ typ,
+ loc,
+ "https://github.com/model-checking/kani/issues/2549",
+ );
+ }
  _ => {}
  }
  }

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

@@ -163,6 +163,52 @@ impl<'tcx> GotocCtx<'tcx> {
  }
  }
 
+ /// Generate code for a binary operation with an overflow check.
+ fn codegen_binop_with_overflow_check(
+ &mut self,
+ op: &BinOp,
+ left_op: &Operand<'tcx>,
+ right_op: &Operand<'tcx>,
+ loc: Location,
+ ) -> Expr {
+ debug!(?op, "codegen_binop_with_overflow_check");
+ let left = self.codegen_operand(left_op);
+ let right = self.codegen_operand(right_op);
+ let ret_type = left.typ().clone();
+ let (bin_op, op_name) = match op {
+ BinOp::AddUnchecked => (BinaryOperator::OverflowResultPlus, "unchecked_add"),
+ BinOp::SubUnchecked => (BinaryOperator::OverflowResultMinus, "unchecked_sub"),
+ BinOp::MulUnchecked => (BinaryOperator::OverflowResultMult, "unchecked_mul"),
+ _ => unreachable!("Expected Add/Sub/Mul but got {op:?}"),
+ };
+ // Create CBMC result type and add to the symbol table.
+ let res_type = arithmetic_overflow_result_type(left.typ().clone());
+ let tag = res_type.tag().unwrap();
+ let struct_tag =
+ self.ensure_struct(tag, tag, |_, _| res_type.components().unwrap().clone());
+ let res = left.overflow_op(bin_op, right);
+ // store the result in a temporary variable
+ let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc);
+ // cast into result type
+ let check = self.codegen_assert(
+ var.clone()
+ .member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table)
+ .cast_to(Type::c_bool())
+ .not(),
+ PropertyClass::ArithmeticOverflow,
+ format!("attempt to compute `{op_name}` which would overflow").as_str(),
+ loc,
+ );
+ Expr::statement_expression(
+ vec![
+ decl,
+ check,
+ var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table).as_stmt(loc),
+ ],
+ ret_type,
+ )
+ }
+
  /// Generate code for a binary operation with an overflow and returns a tuple (res, overflow).
  pub fn codegen_binop_with_overflow(
  &mut self,
@@ -297,7 +343,28 @@ impl<'tcx> GotocCtx<'tcx> {
  BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Shl | BinOp::Shr => {
  self.codegen_scalar_binop(op, e1, e2)
  }
- BinOp::Div | BinOp::Rem | BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => {
+ // We currently rely on CBMC's UB checks for shift which isn't always accurate.
+ // We should implement the checks ourselves.
+ // See https://github.com/model-checking/kani/issues/2374
+ BinOp::ShlUnchecked => self.codegen_scalar_binop(&BinOp::Shl, e1, e2),
+ BinOp::ShrUnchecked => self.codegen_scalar_binop(&BinOp::Shr, e1, e2),
+ BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => {
+ self.codegen_binop_with_overflow_check(op, e1, e2, loc)
+ }
+ BinOp::Div | BinOp::Rem => {
+ let result = self.codegen_unchecked_scalar_binop(op, e1, e2);
+ if self.operand_ty(e1).is_integral() {
+ let is_rem = matches!(op, BinOp::Rem);
+ let check = self.check_div_overflow(e1, e2, is_rem, loc);
+ Expr::statement_expression(
+ vec![check, result.clone().as_stmt(loc)],
+ result.typ().clone(),
+ )
+ } else {
+ result
+ }
+ }
+ BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => {
  self.codegen_unchecked_scalar_binop(op, e1, e2)
  }
  BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
@@ -341,6 +408,53 @@ impl<'tcx> GotocCtx<'tcx> {
  }
  }
 
+ /// Check that a division does not overflow.
+ /// For integer types, division by zero is UB, as is MIN / -1 for signed.
+ /// Note that the compiler already inserts these checks for regular division.
+ /// However, since <https://github.com/rust-lang/rust/pull/112168>, unchecked divisions are
+ /// lowered to `BinOp::Div`. Prefer adding duplicated checks for now.
+ fn check_div_overflow(
+ &mut self,
+ dividend: &Operand<'tcx>,
+ divisor: &Operand<'tcx>,
+ is_remainder: bool,
+ loc: Location,
+ ) -> Stmt {
+ let divisor_expr = self.codegen_operand(divisor);
+ let msg = if is_remainder {
+ "attempt to calculate the remainder with a divisor of zero"
+ } else {
+ "attempt to divide by zero"
+ };
+ let div_by_zero_check = self.codegen_assert_assume(
+ divisor_expr.clone().is_zero().not(),
+ PropertyClass::ArithmeticOverflow,
+ msg,
+ loc,
+ );
+ if self.operand_ty(dividend).is_signed() {
+ let dividend_expr = self.codegen_operand(dividend);
+ let overflow_msg = if is_remainder {
+ "attempt to calculate the remainder with overflow"
+ } else {
+ "attempt to divide with overflow"
+ };
+ let overflow_expr = dividend_expr
+ .clone()
+ .eq(dividend_expr.typ().min_int_expr(self.symbol_table.machine_model()))
+ .and(divisor_expr.clone().eq(Expr::int_constant(-1, divisor_expr.typ().clone())));
+ let overflow_check = self.codegen_assert_assume(
+ overflow_expr.not(),
+ PropertyClass::ArithmeticOverflow,
+ overflow_msg,
+ loc,
+ );
+ Stmt::block(vec![overflow_check, div_by_zero_check], loc)
+ } else {
+ div_by_zero_check
+ }
+ }
+
  /// Create an initializer for a generator struct.
  fn codegen_rvalue_generator(
  &mut self,

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

@@ -149,7 +149,7 @@ impl<'tcx> GotocCtx<'tcx> {
  "unreachable code",
  loc,
  ),
- TerminatorKind::Drop { place, target, unwind: _ } => {
+ TerminatorKind::Drop { place, target, unwind: _, replace: _ } => {
  self.codegen_drop(place, target, loc)
  }
  TerminatorKind::Call { func, args, destination, target, .. } => {
@@ -161,12 +161,12 @@ impl<'tcx> GotocCtx<'tcx> {
  if *expected { r } else { Expr::not(r) }
  };
 
- let msg = if let AssertKind::BoundsCheck { .. } = msg {
+ let msg = if let AssertKind::BoundsCheck { .. } = &**msg {
  // For bounds check the following panic message is generated at runtime:
  // "index out of bounds: the length is {len} but the index is {index}",
  // but CBMC only accepts static messages so we don't add values to the message.
  "index out of bounds: the length is less than or equal to the given index"
- } else if let AssertKind::MisalignedPointerDereference { .. } = msg {
+ } else if let AssertKind::MisalignedPointerDereference { .. } = &**msg {
  // Misaligned pointer dereference check messages is also a runtime messages.
  // Generate a generic one here.
  "misaligned pointer dereference: address must be a multiple of its type's alignment"

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

@@ -303,7 +303,7 @@ impl<'tcx> GotocCtx<'tcx> {
  var: ty::BoundVar::from_usize(bound_vars.len() - 1),
  kind: ty::BoundRegionKind::BrEnv,
  };
- let env_region = self.tcx.mk_re_late_bound(ty::INNERMOST, br);
+ let env_region = ty::Region::new_late_bound(self.tcx, ty::INNERMOST, br);
  let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap();
 
  let sig = sig.skip_binder();
@@ -345,7 +345,7 @@ impl<'tcx> GotocCtx<'tcx> {
  kind: ty::BoundRegionKind::BrEnv,
  };
  let env_region = ty::ReLateBound(ty::INNERMOST, br);
- let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region_from_kind(env_region), ty);
+ let env_ty = self.tcx.mk_mut_ref(ty::Region::new_from_kind(self.tcx, env_region), ty);
 
  let pin_did = self.tcx.require_lang_item(LangItem::Pin, None);
  let pin_adt_ref = self.tcx.adt_def(pin_did);
@@ -429,7 +429,7 @@ impl<'tcx> GotocCtx<'tcx> {
  current_fn.instance().subst_mir_and_normalize_erasing_regions(
  self.tcx,
  ty::ParamEnv::reveal_all(),
- value,
+ ty::EarlyBinder::bind(value),
  )
  } else {
  // TODO: confirm with rust team there is no way to monomorphize
@@ -665,8 +665,8 @@ impl<'tcx> GotocCtx<'tcx> {
  }
  _ => {
  // This hash is documented to be the same no matter the crate context
- let id_u64 = self.tcx.type_id_hash(t).as_u64();
- format!("_{id_u64}").intern()
+ let id = self.tcx.type_id_hash(t).as_u128();
+ format!("_{id}").intern()
  }
  }
  }