Merge branch 'main' into simd-div-overflow

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

@@ -535,16 +535,8 @@ impl<'tcx> GotocCtx<'tcx> {
  self.codegen_simd_cmp(Expr::vector_neq, fargs, p, span, farg_types, ret_ty)
  }
  "simd_or" => codegen_intrinsic_binop!(bitor),
- // TODO: `simd_shl` and `simd_shr` don't check overflow cases.
- // <https://github.com/model-checking/kani/issues/1963>
- "simd_shl" => codegen_intrinsic_binop!(shl),
- "simd_shr" => {
- if fargs[0].typ().base_type().unwrap().is_signed(self.symbol_table.machine_model())
- {
- codegen_intrinsic_binop!(ashr)
- } else {
- codegen_intrinsic_binop!(lshr)
- }
+ "simd_shl" | "simd_shr" => {
+ self.codegen_simd_shift_with_distance_check(fargs, intrinsic, p, loc)
  }
  // "simd_shuffle#" => handled in an `if` preceding this match
  "simd_sub" => self.codegen_simd_op_with_overflow(
@@ -1588,6 +1580,75 @@ impl<'tcx> GotocCtx<'tcx> {
  Stmt::block(vec![check_stmt, expr_place], loc)
  }
 
+ /// Intrinsics which encode a SIMD bitshift.
+ /// Also checks for valid shift distance. Shifts on an integer of type T are UB if shift
+ /// distance < 0 or >= T::BITS.
+ fn codegen_simd_shift_with_distance_check(
+ &mut self,
+ mut fargs: Vec<Expr>,
+ intrinsic: &str,
+ p: &Place<'tcx>,
+ loc: Location,
+ ) -> Stmt {
+ let values = fargs.remove(0);
+ let distances = fargs.remove(0);
+
+ let values_len = values.typ().len().unwrap();
+ let distances_len = distances.typ().len().unwrap();
+ assert_eq!(values_len, distances_len, "expected same length vectors");
+
+ let value_type = values.typ().base_type().unwrap();
+ let distance_type = distances.typ().base_type().unwrap();
+ let value_width = value_type.sizeof_in_bits(&self.symbol_table);
+ let value_width_expr = Expr::int_constant(value_width, distance_type.clone());
+ let distance_is_signed = distance_type.is_signed(self.symbol_table.machine_model());
+
+ let mut excessive_check = Expr::bool_false();
+ let mut negative_check = Expr::bool_false();
+ for i in 0..distances_len {
+ let index = Expr::int_constant(i, Type::ssize_t());
+ let distance = distances.clone().index_array(index);
+ let excessive_distance_cond = distance.clone().ge(value_width_expr.clone());
+ excessive_check = excessive_check.or(excessive_distance_cond);
+ if distance_is_signed {
+ let negative_distance_cond = distance.is_negative();
+ negative_check = negative_check.or(negative_distance_cond);
+ }
+ }
+ let excessive_check_stmt = self.codegen_assert_assume(
+ excessive_check.not(),
+ PropertyClass::ArithmeticOverflow,
+ format!("attempt {intrinsic} with excessive shift distance").as_str(),
+ loc,
+ );
+
+ let op_fun = match intrinsic {
+ "simd_shl" => Expr::shl,
+ "simd_shr" => {
+ if distance_is_signed {
+ Expr::ashr
+ } else {
+ Expr::lshr
+ }
+ }
+ _ => unreachable!("expected a simd shift intrinsic"),
+ };
+ let res = op_fun(values, distances);
+ let expr_place = self.codegen_expr_to_place(p, res);
+
+ if distance_is_signed {
+ let negative_check_stmt = self.codegen_assert_assume(
+ negative_check.not(),
+ PropertyClass::ArithmeticOverflow,
+ format!("attempt {intrinsic} with negative shift distance").as_str(),
+ loc,
+ );
+ Stmt::block(vec![excessive_check_stmt, negative_check_stmt, expr_place], loc)
+ } else {
+ Stmt::block(vec![excessive_check_stmt, expr_place], loc)
+ }
+ }
+
  /// `simd_shuffle` constructs a new vector from the elements of two input
  /// vectors, choosing values according to an input array of indexes.
  ///

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

@@ -23,7 +23,7 @@ use tracing::{debug, trace, warn};
 
 /// A projection in Kani can either be to a type (the normal case),
 /// or a variant in the case of a downcast.
-#[derive(Debug)]
+#[derive(Copy, Clone, Debug)]
 pub enum TypeOrVariant<'tcx> {
  Type(Ty<'tcx>),
  Variant(&'tcx VariantDef),
@@ -235,15 +235,21 @@ impl<'tcx> TypeOrVariant<'tcx> {
 }
 
 impl<'tcx> GotocCtx<'tcx> {
+ /// Codegen field access for types that allow direct field projection.
+ ///
+ /// I.e.: Algebraic data types, closures, and generators.
+ ///
+ /// Other composite types such as array only support index projection.
  fn codegen_field(
  &mut self,
- res: Expr,
- t: TypeOrVariant<'tcx>,
- f: &FieldIdx,
+ parent_expr: Expr,
+ parent_ty_or_var: TypeOrVariant<'tcx>,
+ field: &FieldIdx,
+ field_ty_or_var: TypeOrVariant<'tcx>,
  ) -> Result<Expr, UnimplementedData> {
- match t {
- TypeOrVariant::Type(t) => {
- match t.kind() {
+ match parent_ty_or_var {
+ TypeOrVariant::Type(parent_ty) => {
+ match parent_ty.kind() {
  ty::Alias(..)
  | ty::Bool
  | ty::Char
@@ -254,56 +260,98 @@ impl<'tcx> GotocCtx<'tcx> {
  | ty::Never
  | ty::FnDef(..)
  | ty::GeneratorWitness(..)
+ | ty::GeneratorWitnessMIR(..)
  | ty::Foreign(..)
  | ty::Dynamic(..)
  | ty::Bound(..)
  | ty::Placeholder(..)
  | ty::Param(_)
  | ty::Infer(_)
- | ty::Error(_) => unreachable!("type {:?} does not have a field", t),
- ty::Tuple(_) => {
- Ok(res.member(&Self::tuple_fld_name(f.index()), &self.symbol_table))
- }
- ty::Adt(def, _) if def.repr().simd() => {
- // this is a SIMD vector - the index represents one
- // of the elements, so we want to index as an array
- // Example:
- // pub struct i64x2(i64, i64);
- // fn main() {
- // let v = i64x2(1, 2);
- // assert!(v.0 == 1); // refers to the first i64
- // assert!(v.1 == 2);
- // }
- let size_index = Expr::int_constant(f.index(), Type::size_t());
- Ok(res.index_array(size_index))
- }
+ | ty::Error(_) => unreachable!("type {parent_ty:?} does not have a field"),
+ ty::Tuple(_) => Ok(parent_expr
+ .member(&Self::tuple_fld_name(field.index()), &self.symbol_table)),
+ ty::Adt(def, _) if def.repr().simd() => Ok(self.codegen_simd_field(
+ parent_expr,
+ *field,
+ field_ty_or_var.expect_type(),
+ )),
  // if we fall here, then we are handling either a struct or a union
  ty::Adt(def, _) => {
- let field = &def.variants().raw[0].fields[*f];
- Ok(res.member(&field.name.to_string(), &self.symbol_table))
+ let field = &def.variants().raw[0].fields[*field];
+ Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table))
+ }
+ ty::Closure(..) => {
+ Ok(parent_expr.member(&field.index().to_string(), &self.symbol_table))
  }
- ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)),
  ty::Generator(..) => {
- let field_name = self.generator_field_name(f.as_usize());
- Ok(res
+ let field_name = self.generator_field_name(field.as_usize());
+ Ok(parent_expr
  .member("direct_fields", &self.symbol_table)
  .member(field_name, &self.symbol_table))
  }
- _ => unimplemented!(),
+ ty::Str | ty::Array(_, _) | ty::Slice(_) | ty::RawPtr(_) | ty::Ref(_, _, _) => {
+ unreachable!(
+ "element of {parent_ty:?} is not accessed via field projection"
+ )
+ }
  }
  }
  // if we fall here, then we are handling an enum
- TypeOrVariant::Variant(v) => {
- let field = &v.fields[*f];
- Ok(res.member(&field.name.to_string(), &self.symbol_table))
+ TypeOrVariant::Variant(parent_var) => {
+ let field = &parent_var.fields[*field];
+ Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table))
  }
  TypeOrVariant::GeneratorVariant(_var_idx) => {
- let field_name = self.generator_field_name(f.index());
- Ok(res.member(field_name, &self.symbol_table))
+ let field_name = self.generator_field_name(field.index());
+ Ok(parent_expr.member(field_name, &self.symbol_table))
  }
  }
  }
 
+ /// This is a SIMD vector, which has 2 possible internal representations:
+ /// 1- Multi-field representation (original and currently deprecated)
+ /// In this case, a field is one lane (i.e.: one element)
+ /// Example:
+ /// ```ignore
+ /// pub struct i64x2(i64, i64);
+ /// fn main() {
+ /// let v = i64x2(1, 2);
+ /// assert!(v.0 == 1); // refers to the first i64
+ /// assert!(v.1 == 2);
+ /// }
+ /// ```
+ /// 2- Array-based representation
+ /// In this case, the projection refers to the entire array.
+ /// ```ignore
+ /// pub struct i64x2([i64; 2]);
+ /// fn main() {
+ /// let v = i64x2([1, 2]);
+ /// assert!(v.0 == [1, 2]); // refers to the entire array
+ /// }
+ /// ```
+ /// * Note that projection inside SIMD structs may eventually become illegal.
+ /// See <https://github.com/rust-lang/stdarch/pull/1422#discussion_r1176415609> thread.
+ ///
+ /// Since the goto representation for both is the same, we use the expected type to decide
+ /// what to return.
+ fn codegen_simd_field(
+ &mut self,
+ parent_expr: Expr,
+ field: FieldIdx,
+ field_ty: Ty<'tcx>,
+ ) -> Expr {
+ if matches!(field_ty.kind(), ty::Array { .. }) {
+ // Array based
+ assert_eq!(field.index(), 0);
+ let field_typ = self.codegen_ty(field_ty);
+ parent_expr.reinterpret_cast(field_typ)
+ } else {
+ // Return the given field.
+ let index_expr = Expr::int_constant(field.index(), Type::size_t());
+ parent_expr.index_array(index_expr)
+ }
+ }
+
  /// If a local is a function definition, ignore the local variable name and
  /// generate a function call based on the def id.
  ///
@@ -424,7 +472,8 @@ impl<'tcx> GotocCtx<'tcx> {
  }
  ProjectionElem::Field(f, t) => {
  let typ = TypeOrVariant::Type(t);
- let expr = self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f)?;
+ let expr =
+ self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f, typ)?;
  ProjectedPlace::try_new(
  expr,
  typ,

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

@@ -116,6 +116,14 @@ impl<'tcx> GotocCtx<'tcx> {
  BinOp::BitXor => ce1.bitxor(ce2),
  BinOp::Div => ce1.div(ce2),
  BinOp::Rem => ce1.rem(ce2),
+ BinOp::ShlUnchecked => ce1.shl(ce2),
+ BinOp::ShrUnchecked => {
+ if self.operand_ty(e1).is_signed() {
+ ce1.ashr(ce2)
+ } else {
+ ce1.lshr(ce2)
+ }
+ }
  _ => unreachable!("Unexpected {:?}", op),
  }
  }
@@ -343,11 +351,14 @@ impl<'tcx> GotocCtx<'tcx> {
  BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Shl | BinOp::Shr => {
  self.codegen_scalar_binop(op, e1, e2)
  }
- // 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::ShlUnchecked | BinOp::ShrUnchecked => {
+ let result = self.codegen_unchecked_scalar_binop(op, e1, e2);
+ let check = self.check_unchecked_shift_distance(e1, e2, loc);
+ Expr::statement_expression(
+ vec![check, result.clone().as_stmt(loc)],
+ result.typ().clone(),
+ )
+ }
  BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => {
  self.codegen_binop_with_overflow_check(op, e1, e2, loc)
  }
@@ -455,6 +466,39 @@ impl<'tcx> GotocCtx<'tcx> {
  }
  }
 
+ /// Check for valid unchecked shift distance.
+ /// Shifts on an integer of type T are UB if shift distance < 0 or >= T::BITS.
+ fn check_unchecked_shift_distance(
+ &mut self,
+ value: &Operand<'tcx>,
+ distance: &Operand<'tcx>,
+ loc: Location,
+ ) -> Stmt {
+ let value_expr = self.codegen_operand(value);
+ let distance_expr = self.codegen_operand(distance);
+ let value_width = value_expr.typ().sizeof_in_bits(&self.symbol_table);
+ let value_width_expr = Expr::int_constant(value_width, distance_expr.typ().clone());
+
+ let excessive_distance_check = self.codegen_assert_assume(
+ distance_expr.clone().lt(value_width_expr),
+ PropertyClass::ArithmeticOverflow,
+ "attempt to shift by excessive shift distance",
+ loc,
+ );
+
+ if distance_expr.typ().is_signed(self.symbol_table.machine_model()) {
+ let negative_distance_check = self.codegen_assert_assume(
+ distance_expr.is_non_negative(),
+ PropertyClass::ArithmeticOverflow,
+ "attempt to shift by negative distance",
+ loc,
+ );
+ Stmt::block(vec![negative_distance_check, excessive_distance_check], loc)
+ } else {
+ excessive_distance_check
+ }
+ }
+
  /// Create an initializer for a generator struct.
  fn codegen_rvalue_generator(
  &mut self,
@@ -582,24 +626,28 @@ impl<'tcx> GotocCtx<'tcx> {
  AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => {
  let typ = self.codegen_ty(res_ty);
  let layout = self.layout_of(res_ty);
- let vector_element_type = typ.base_type().unwrap().clone();
- Expr::vector_expr(
- typ,
- layout
- .fields
- .index_by_increasing_offset()
- .map(|idx| {
- let cgo = self.codegen_operand(&operands[idx.into()]);
- // The input operand might actually be a one-element array, as seen
- // when running assess on firecracker.
- if *cgo.typ() == vector_element_type {
- cgo
- } else {
- cgo.transmute_to(vector_element_type.clone(), &self.symbol_table)
- }
- })
- .collect(),
- )
+ trace!(shape=?layout.fields, "codegen_rvalue_aggregate");
+ assert!(operands.len() > 0, "SIMD vector cannot be empty");
+ if operands.len() == 1 {
+ let data = self.codegen_operand(&operands[0u32.into()]);
+ if data.typ().is_array() {
+ // Array-based SIMD representation.
+ data.transmute_to(typ, &self.symbol_table)
+ } else {
+ // Multi field-based representation with one field.
+ Expr::vector_expr(typ, vec![data])
+ }
+ } else {
+ // Multi field SIMD representation.
+ Expr::vector_expr(
+ typ,
+ layout
+ .fields
+ .index_by_increasing_offset()
+ .map(|idx| self.codegen_operand(&operands[idx.into()]))
+ .collect(),
+ )
+ }
  }
  AggregateKind::Adt(_, variant_index, ..) if res_ty.is_enum() => {
  self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc)

kani-driver/src/call_cbmc.rs

@@ -167,7 +167,6 @@ impl KaniSession {
  args.push("--div-by-zero-check".into());
  args.push("--float-overflow-check".into());
  args.push("--nan-check".into());
- args.push("--undefined-shift-check".into());
  // With PR #647 we use Rust's `-C overflow-checks=on` instead of:
  // --unsigned-overflow-check
  // --signed-overflow-check