Merge branch 'main' into shift-checks

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

@@ -29,7 +29,7 @@ use tracing::debug;
 /// Classifies the type of CBMC `assert`, as different assertions can have different semantics (e.g. cover)
 ///
 /// Each property class should justify its existence with a note about the special handling it recieves.
-#[derive(Debug, Clone, EnumString, AsRefStr)]
+#[derive(Debug, Clone, EnumString, AsRefStr, PartialEq)]
 #[strum(serialize_all = "snake_case")]
 pub enum PropertyClass {
  /// Overflow panics that can be generated by Intrisics.
@@ -45,6 +45,19 @@ pub enum PropertyClass {
  ///
  /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
  Cover,
+ /// The class of checks used for code coverage instrumentation. Only needed
+ /// when working on coverage-related features.
+ ///
+ /// Do not mistake with `Cover`, they are different:
+ /// - `CodeCoverage` checks have a fixed condition (`false`) and description.
+ /// - `CodeCoverage` checks are filtered out from verification results and
+ /// postprocessed to build coverage reports.
+ /// - `Cover` checks can be added by users (using the `kani::cover` macro),
+ /// while `CodeCoverage` checks are not exposed to users (i.e., they are
+ /// automatically added if running with the coverage option).
+ ///
+ /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
+ CodeCoverage,
  /// Ordinary (Rust) assertions and panics.
  ///
  /// SPECIAL BEHAVIOR: These assertion failures should be observable during normal execution of Rust code.
@@ -134,6 +147,21 @@ impl<'tcx> GotocCtx<'tcx> {
  self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc)
  }
 
+ /// Generate a cover statement for code coverage reports.
+ pub fn codegen_coverage(&self, span: Span) -> Stmt {
+ let loc = self.codegen_caller_span(&Some(span));
+ // Should use Stmt::cover, but currently this doesn't work with CBMC
+ // unless it is run with '--cover cover' (see
+ // https://github.com/diffblue/cbmc/issues/6613). So for now use
+ // `assert(false)`.
+ self.codegen_assert(
+ Expr::bool_false(),
+ PropertyClass::CodeCoverage,
+ "code coverage for location",
+ loc,
+ )
+ }
+
  // The above represent the basic operations we can perform w.r.t. assert/assume/cover
  // Below are various helper functions for constructing the above more easily.
 

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

@@ -16,25 +16,55 @@ impl<'tcx> GotocCtx<'tcx> {
  debug!(?bb, "Codegen basicblock");
  self.current_fn_mut().set_current_bb(bb);
  let label: String = self.current_fn().find_label(&bb);
+ let check_coverage = self.queries.check_coverage;
  // the first statement should be labelled. if there is no statements, then the
  // terminator should be labelled.
  match bbd.statements.len() {
  0 => {
  let term = bbd.terminator();
  let tcode = self.codegen_terminator(term);
- self.current_fn_mut().push_onto_block(tcode.with_label(label));
+ // When checking coverage, the `coverage` check should be
+ // labelled instead.
+ if check_coverage {
+ let span = term.source_info.span;
+ let cover = self.codegen_coverage(span);
+ self.current_fn_mut().push_onto_block(cover.with_label(label));
+ self.current_fn_mut().push_onto_block(tcode);
+ } else {
+ self.current_fn_mut().push_onto_block(tcode.with_label(label));
+ }
  }
  _ => {
  let stmt = &bbd.statements[0];
  let scode = self.codegen_statement(stmt);
- self.current_fn_mut().push_onto_block(scode.with_label(label));
+ // When checking coverage, the `coverage` check should be
+ // labelled instead.
+ if check_coverage {
+ let span = stmt.source_info.span;
+ let cover = self.codegen_coverage(span);
+ self.current_fn_mut().push_onto_block(cover.with_label(label));
+ self.current_fn_mut().push_onto_block(scode);
+ } else {
+ self.current_fn_mut().push_onto_block(scode.with_label(label));
+ }
 
  for s in &bbd.statements[1..] {
+ if check_coverage {
+ let span = s.source_info.span;
+ let cover = self.codegen_coverage(span);
+ self.current_fn_mut().push_onto_block(cover);
+ }
  let stmt = self.codegen_statement(s);
  self.current_fn_mut().push_onto_block(stmt);
  }
- let term = self.codegen_terminator(bbd.terminator());
- self.current_fn_mut().push_onto_block(term);
+ let term = bbd.terminator();
+ if check_coverage {
+ let span = term.source_info.span;
+ let cover = self.codegen_coverage(span);
+ self.current_fn_mut().push_onto_block(cover);
+ }
+ let tcode = self.codegen_terminator(term);
+ self.current_fn_mut().push_onto_block(tcode);
  }
  }
  self.current_fn_mut().reset_current_bb();

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

@@ -188,7 +188,7 @@ impl<'tcx> GotocCtx<'tcx> {
  let a = fargs.remove(0);
  let b = fargs.remove(0);
  let div_does_not_overflow = self.div_does_not_overflow(a.clone(), b.clone());
- let div_overflow_check = self.codegen_assert(
+ let div_overflow_check = self.codegen_assert_assume(
  div_does_not_overflow,
  PropertyClass::ArithmeticOverflow,
  format!("attempt to compute {} which would overflow", intrinsic).as_str(),

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

@@ -626,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)