Migrate intrinsics module to use StableMIR (#2939)

This one was fairly straight forward. It still uses a few internal APIs
for user friendly errors, for type layout, SIMD information and
intrinsic validity.

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

@@ -150,7 +150,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
  /// Generate a cover statement for code coverage reports.
  pub fn codegen_coverage(&self, span: Span) -> Stmt {
- let loc = self.codegen_caller_span(&Some(span));
+ let loc = self.codegen_caller_span(&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
@@ -214,9 +214,9 @@ impl<'tcx> GotocCtx<'tcx> {
  &self,
  property_class: PropertyClass,
  msg: &str,
- span: Option<Span>,
+ span: SpanStable,
  ) -> Stmt {
- let loc = self.codegen_caller_span(&span);
+ let loc = self.codegen_caller_span_stable(span);
  self.codegen_assert_assume_false(property_class, msg, loc)
  }
 
@@ -228,9 +228,7 @@ impl<'tcx> GotocCtx<'tcx> {
  let msg = self.extract_const_message(&fargs[0]).unwrap_or(String::from(
  "This is a placeholder message; Kani doesn't support message formatted at runtime",
  ));
-
- let loc = self.codegen_caller_span_stable(span);
- self.codegen_assert_assume_false(PropertyClass::Assertion, &msg, loc)
+ self.codegen_fatal_error(PropertyClass::Assertion, &msg, span)
  }
 
  /// Kani does not currently support all MIR constructs.

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

@@ -393,7 +393,7 @@ impl<'tcx> GotocCtx<'tcx> {
  // Check that computing `offset` in bytes would not overflow
  let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(
  ce2.clone().cast_to(Type::ssize_t()),
- rustc_internal::internal(ty),
+ ty,
  Type::ssize_t(),
  "offset",
  loc,

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

@@ -33,20 +33,16 @@ impl<'tcx> GotocCtx<'tcx> {
  }
 
  pub fn codegen_caller_span_stable(&self, sp: SpanStable) -> Location {
- self.codegen_caller_span(&Some(rustc_internal::internal(sp)))
+ self.codegen_caller_span(&rustc_internal::internal(sp))
  }
 
  /// Get the location of the caller. This will attempt to reach the macro caller.
  /// This function uses rustc_span methods designed to returns span for the macro which
  /// originally caused the expansion to happen.
  /// Note: The API stops backtracing at include! boundary.
- pub fn codegen_caller_span(&self, sp: &Option<Span>) -> Location {
- if let Some(span) = sp {
- let topmost = span.ctxt().outer_expn().expansion_cause().unwrap_or(*span);
- self.codegen_span(&topmost)
- } else {
- Location::none()
- }
+ pub fn codegen_caller_span(&self, span: &Span) -> Location {
+ let topmost = span.ctxt().outer_expn().expansion_cause().unwrap_or(*span);
+ self.codegen_span(&topmost)
  }
 
  pub fn codegen_span_option(&self, sp: Option<Span>) -> Location {

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

@@ -3,6 +3,7 @@
 use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
 use super::PropertyClass;
+use crate::codegen_cprover_gotoc::codegen::ty_stable::StableConverter;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
@@ -18,7 +19,7 @@ use rustc_smir::rustc_internal;
 use rustc_span::Span;
 use rustc_target::abi::VariantIdx;
 use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
-use stable_mir::mir::Place as PlaceStable;
+use stable_mir::mir::{Operand as OperandStable, Place as PlaceStable};
 use tracing::{debug, debug_span, trace};
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -68,15 +69,13 @@ impl<'tcx> GotocCtx<'tcx> {
  StatementKind::Intrinsic(box NonDivergingIntrinsic::CopyNonOverlapping(
  mir::CopyNonOverlapping { ref src, ref dst, ref count },
  )) => {
+ let operands =
+ [src, dst, count].map(|op| StableConverter::convert_operand(self, op.clone()));
  // Pack the operands and their types, then call `codegen_copy`
- let fargs = vec![
- self.codegen_operand(src),
- self.codegen_operand(dst),
- self.codegen_operand(count),
- ];
- let farg_types =
- &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)];
- self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location)
+ let fargs =
+ operands.iter().map(|op| self.codegen_operand_stable(op)).collect::<Vec<_>>();
+ let farg_types = operands.map(|op| self.operand_ty_stable(&op));
+ self.codegen_copy("copy_nonoverlapping", true, fargs, &farg_types, None, location)
  }
  StatementKind::Intrinsic(box NonDivergingIntrinsic::Assume(ref op)) => {
  let cond = self.codegen_operand(op).cast_to(Type::bool());
@@ -474,20 +473,20 @@ impl<'tcx> GotocCtx<'tcx> {
  /// This is used because we ignore ZST arguments, except for intrinsics.
  pub(crate) fn codegen_funcall_args(
  &mut self,
- args: &[Operand<'tcx>],
+ args: &[OperandStable],
  skip_zst: bool,
  ) -> Vec<Expr> {
  let fargs = args
  .iter()
- .filter_map(|o| {
- let op_ty = self.operand_ty(o);
- if op_ty.is_bool() {
- Some(self.codegen_operand(o).cast_to(Type::c_bool()))
- } else if !self.is_zst(op_ty) || !skip_zst {
- Some(self.codegen_operand(o))
+ .filter_map(|op| {
+ let op_ty = self.operand_ty_stable(op);
+ if op_ty.kind().is_bool() {
+ Some(self.codegen_operand_stable(op).cast_to(Type::c_bool()))
+ } else if !self.is_zst_stable(op_ty) || !skip_zst {
+ Some(self.codegen_operand_stable(op))
  } else {
  // We ignore ZST types.
- debug!(arg=?o, "codegen_funcall_args ignore");
+ debug!(arg=?op, "codegen_funcall_args ignore");
  None
  }
  })
@@ -517,13 +516,26 @@ impl<'tcx> GotocCtx<'tcx> {
  span: Span,
  ) -> Stmt {
  debug!(?func, ?args, ?destination, ?span, "codegen_funcall");
- if self.is_intrinsic(func) {
- return self.codegen_funcall_of_intrinsic(func, args, destination, target, span);
+ let func_stable = StableConverter::convert_operand(self, func.clone());
+ let args_stable = args
+ .iter()
+ .map(|arg| StableConverter::convert_operand(self, arg.clone()))
+ .collect::<Vec<_>>();
+ let destination_stable = StableConverter::convert_place(self, *destination);
+
+ if self.is_intrinsic(&func_stable) {
+ return self.codegen_funcall_of_intrinsic(
+ &func_stable,
+ &args_stable,
+ &destination_stable,
+ target.map(|bb| bb.index()),
+ rustc_internal::stable(span),
+ );
  }
 
  let loc = self.codegen_span(&span);
  let funct = self.operand_ty(func);
- let mut fargs = self.codegen_funcall_args(args, true);
+ let mut fargs = self.codegen_funcall_args(&args_stable, true);
  match &funct.kind() {
  ty::FnDef(defid, subst) => {
  let instance =
@@ -700,13 +712,13 @@ impl<'tcx> GotocCtx<'tcx> {
  /// A MIR [Place] is an L-value (i.e. the LHS of an assignment).
  ///
  /// In Kani, we slightly optimize the special case for Unit and don't assign anything.
- pub(crate) fn codegen_expr_to_place_stable(&mut self, p: &PlaceStable, e: Expr) -> Stmt {
- if e.typ().is_unit() {
- e.as_stmt(Location::none())
+ pub(crate) fn codegen_expr_to_place_stable(&mut self, place: &PlaceStable, expr: Expr) -> Stmt {
+ if self.place_ty_stable(place).kind().is_unit() {
+ expr.as_stmt(Location::none())
  } else {
- unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(p))
+ unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(place))
  .goto_expr
- .assign(e, Location::none())
+ .assign(expr, Location::none())
  }
  }
 

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

@@ -33,11 +33,11 @@ impl<'tcx> GotocCtx<'tcx> {
  self.codegen_ty_ref(rustc_internal::internal(ty))
  }
 
- pub fn local_ty_stable(&mut self, local: Local) -> Ty {
+ pub fn local_ty_stable(&self, local: Local) -> Ty {
  self.current_fn().body().local_decl(local).unwrap().ty
  }
 
- pub fn operand_ty_stable(&mut self, operand: &Operand) -> Ty {
+ pub fn operand_ty_stable(&self, operand: &Operand) -> Ty {
  operand.ty(self.current_fn().body().locals()).unwrap()
  }
 
@@ -89,6 +89,11 @@ impl<'tcx> GotocCtx<'tcx> {
  pub fn rvalue_ty_stable(&self, rvalue: &Rvalue) -> Ty {
  rvalue.ty(self.current_fn().body().locals()).unwrap()
  }
+
+ pub fn simd_size_and_type(&self, ty: Ty) -> (u64, Ty) {
+ let (sz, ty) = rustc_internal::internal(ty).simd_size_and_type(self.tcx);
+ (sz, rustc_internal::stable(ty))
+ }
 }
 /// If given type is a Ref / Raw ref, return the pointee type.
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
@@ -99,6 +104,14 @@ pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
  }
 }
 
+/// Convert a type into a user readable type representation.
+///
+/// This should be replaced by StableMIR `pretty_ty()` after
+/// <https://github.com/rust-lang/rust/pull/118364> is merged.
+pub fn pretty_ty(ty: Ty) -> String {
+ rustc_internal::internal(ty).to_string()
+}
+
 /// Convert internal rustc's structs into StableMIR ones.
 ///
 /// The body of a StableMIR instance already comes monomorphized, which is different from rustc's

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

@@ -1898,12 +1898,6 @@ fn common_vtable_fields(drop_in_place: Type) -> Vec<DatatypeComponent> {
  fields
 }
 
-/// The mir type is a mir pointer type (Ref or RawPtr).
-/// This will return false for all smart pointers. See is_std_pointer for a more complete check.
-pub fn is_pointer(mir_type: Ty) -> bool {
- return pointee_type(mir_type).is_some();
-}
-
 /// If given type is a Ref / Raw ref, return the pointee type.
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
  match mir_type.kind() {

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

@@ -1,12 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::super::codegen::TypeExt;
-use crate::codegen_cprover_gotoc::codegen::typ::{is_pointer, pointee_type};
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, ExprValue, Location, SymbolTable, Type};
 use cbmc::{btree_string_map, InternedString};
-use rustc_middle::ty::layout::LayoutOf;
-use rustc_middle::ty::Ty;
+use rustc_middle::ty::TyCtxt;
+use rustc_smir::rustc_internal;
+use stable_mir::ty::Span;
 use tracing::debug;
 
 // Should move into rvalue
@@ -20,21 +20,6 @@ pub fn dynamic_fat_ptr(typ: Type, data: Expr, vtable: Expr, symbol_table: &Symbo
 }
 
 impl<'tcx> GotocCtx<'tcx> {
- /// Generates an expression `(ptr as usize) % align_of(T) == 0`
- /// to determine if a pointer `ptr` with pointee type `T` is aligned.
- pub fn is_ptr_aligned(&mut self, typ: Ty<'tcx>, ptr: Expr) -> Expr {
- // Ensure `typ` is a pointer, then extract the pointee type
- assert!(is_pointer(typ));
- let pointee_type = pointee_type(typ).unwrap();
- // Obtain the alignment for the pointee type `T`
- let layout = self.layout_of(pointee_type);
- let align = Expr::int_constant(layout.align.abi.bytes(), Type::size_t());
- // Cast the pointer to `usize` and return the alignment expression
- let cast_ptr = ptr.cast_to(Type::size_t());
- let zero = Type::size_t().zero();
- cast_ptr.rem(align).eq(zero)
- }
-
  pub fn unsupported_msg(item: &str, url: Option<&str>) -> String {
  let mut s = format!("{item} is not currently supported by Kani");
  if let Some(url) = url {
@@ -207,3 +192,7 @@ impl<'tcx> GotocCtx<'tcx> {
  assert!(component.typ().is_pointer() || component.typ().is_rust_fat_ptr(&self.symbol_table))
  }
 }
+
+pub fn span_err(tcx: TyCtxt, span: Span, msg: String) {
+ tcx.sess.span_err(rustc_internal::internal(span), msg);
+}