Merge branch 'main' into fix-136

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

@@ -1883,12 +1883,11 @@ impl<'tcx> GotocCtx<'tcx> {
  "`dst` must be properly aligned",
  loc,
  );
- let deref = dst.dereference();
- if deref.typ().sizeof(&self.symbol_table) == 0 {
+ if self.is_zst_stable(pointee_type_stable(dst_typ).unwrap()) {
  // do not attempt to dereference (and assign) a ZST
  align_check
  } else {
- let expr = deref.assign(src, loc);
+ let expr = dst.dereference().assign(src, loc);
  Stmt::block(vec![align_check, expr], loc)
  }
  }
@@ -1994,30 +1993,42 @@ impl<'tcx> GotocCtx<'tcx> {
  let x = fargs.remove(0);
  let y = fargs.remove(0);
 
- // if(same_object(x, y)) {
- // assert(x + 1 <= y || y + 1 <= x);
- // assume(x + 1 <= y || y + 1 <= x);
- // }
- let one = Expr::int_constant(1, Type::c_int());
- let non_overlapping =
- x.clone().plus(one.clone()).le(y.clone()).or(y.clone().plus(one.clone()).le(x.clone()));
- let non_overlapping_check = self.codegen_assert_assume(
- non_overlapping,
- PropertyClass::SafetyCheck,
- "memory regions pointed to by `x` and `y` must not overlap",
- loc,
- );
- let non_overlapping_stmt =
- Stmt::if_then_else(x.clone().same_object(y.clone()), non_overlapping_check, None, loc);
+ if self.is_zst_stable(pointee_type_stable(farg_types[0]).unwrap()) {
+ // do not attempt to dereference (and assign) a ZST
+ Stmt::skip(loc)
+ } else {
+ // if(same_object(x, y)) {
+ // assert(x + 1 <= y || y + 1 <= x);
+ // assume(x + 1 <= y || y + 1 <= x);
+ // }
+ let one = Expr::int_constant(1, Type::c_int());
+ let non_overlapping = x
+ .clone()
+ .plus(one.clone())
+ .le(y.clone())
+ .or(y.clone().plus(one.clone()).le(x.clone()));
+ let non_overlapping_check = self.codegen_assert_assume(
+ non_overlapping,
+ PropertyClass::SafetyCheck,
+ "memory regions pointed to by `x` and `y` must not overlap",
+ loc,
+ );
+ let non_overlapping_stmt = Stmt::if_then_else(
+ x.clone().same_object(y.clone()),
+ non_overlapping_check,
+ None,
+ loc,
+ );
 
- // T t = *y; *y = *x; *x = t;
- let deref_y = y.clone().dereference();
- let (temp_var, assign_to_t) =
- self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc);
- let assign_to_y = y.dereference().assign(x.clone().dereference(), loc);
- let assign_to_x = x.dereference().assign(temp_var, loc);
+  // T t = *y; *y = *x; *x = t;
+  let deref_y = y.clone().dereference();
+  let (temp_var, assign_to_t) =
+  self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc);
+  let assign_to_y = y.dereference().assign(x.clone().dereference(), loc);
+  let assign_to_x = x.dereference().assign(temp_var, loc);
 
- Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc)
+ Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc)
+ }
  }
 }
 

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

@@ -622,7 +622,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
  /// Ensure that the given instance is in the symbol table, returning the symbol.
  fn codegen_func_symbol(&mut self, instance: Instance) -> &Symbol {
- let sym = if instance.is_foreign_item() {
+ let sym = if instance.is_foreign_item() && !instance.has_body() {
  // Get the symbol that represents a foreign instance.
  self.codegen_foreign_fn(instance)
  } else {

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

@@ -521,13 +521,21 @@ impl<'tcx> GotocCtx<'tcx> {
  if let Some(instance) = instance_opt
  && matches!(instance.kind, InstanceKind::Intrinsic)
  {
- return self.codegen_funcall_of_intrinsic(
- instance,
- &args,
- &destination,
- target.map(|bb| bb),
- span,
- );
+ let TyKind::RigidTy(RigidTy::FnDef(def, _)) = instance.ty().kind() else {
+ unreachable!("Expected function type for intrinsic: {instance:?}")
+ };
+ // The compiler is currently transitioning how to handle intrinsic fallback body.
+ // Until https://github.com/rust-lang/project-stable-mir/issues/79 is implemented
+ // we have to check `must_be_overridden` and `has_body`.
+ if def.as_intrinsic().unwrap().must_be_overridden() || !instance.has_body() {
+ return self.codegen_funcall_of_intrinsic(
+ instance,
+ &args,
+ &destination,
+ target.map(|bb| bb),
+ span,
+ );
+ }
  }
 
  let loc = self.codegen_span_stable(span);

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -93,7 +93,7 @@ impl GotocCodegenBackend {
  || collect_reachable_items(tcx, &mut transformer, starting_items),
  "codegen reachability analysis",
  );
- dump_mir_items(tcx, &items, &symtab_goto.with_extension("kani.mir"));
+ dump_mir_items(tcx, &mut transformer, &items, &symtab_goto.with_extension("kani.mir"));
 
  // Follow rustc naming convention (cx is abbrev for context).
  // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions

kani-compiler/src/kani_middle/attributes.rs

@@ -782,10 +782,10 @@ impl<'a> UnstableAttrParseError<'a> {
  tcx.dcx()
  .struct_span_err(
  self.attr.span,
- format!("failed to parse `#[kani::unstable]`: {}", self.reason),
+ format!("failed to parse `#[kani::unstable_feature]`: {}", self.reason),
  )
  .with_note(format!(
- "expected format: #[kani::unstable({}, {}, {})]",
+ "expected format: #[kani::unstable_feature({}, {}, {})]",
  r#"feature="<IDENTIFIER>""#, r#"issue="<ISSUE>""#, r#"reason="<DESCRIPTION>""#
  ))
  .emit()

kani-compiler/src/kani_middle/mod.rs

@@ -6,9 +6,9 @@
 use std::collections::HashSet;
 use std::path::Path;
 
+use crate::kani_middle::transform::BodyTransformation;
 use crate::kani_queries::QueryDb;
 use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE};
-use rustc_middle::mir::write_mir_pretty;
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
  FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError,
@@ -21,9 +21,9 @@ use rustc_span::source_map::respan;
 use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
-use stable_mir::mir::mono::{InstanceKind, MonoItem};
+use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, TyKind};
-use stable_mir::{CrateDef, DefId};
+use stable_mir::CrateDef;
 use std::fs::File;
 use std::io::BufWriter;
 use std::io::Write;
@@ -93,17 +93,19 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
 }
 
 /// Print MIR for the reachable items if the `--emit mir` option was provided to rustc.
-pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
+pub fn dump_mir_items(
+ tcx: TyCtxt,
+ transformer: &mut BodyTransformation,
+ items: &[MonoItem],
+ output: &Path,
+) {
  /// Convert MonoItem into a DefId.
  /// Skip stuff that we cannot generate the MIR items.
- fn visible_item(item: &MonoItem) -> Option<(MonoItem, DefId)> {
+ fn get_instance(item: &MonoItem) -> Option<Instance> {
  match item {
  // Exclude FnShims and others that cannot be dumped.
- MonoItem::Fn(instance) if matches!(instance.kind, InstanceKind::Item) => {
- Some((item.clone(), instance.def.def_id()))
- }
- MonoItem::Fn(..) => None,
- MonoItem::Static(def) => Some((item.clone(), def.def_id())),
+ MonoItem::Fn(instance) => Some(*instance),
+ MonoItem::Static(def) => Some((*def).into()),
  MonoItem::GlobalAsm(_) => None,
  }
  }
@@ -114,10 +116,10 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
  let mut writer = BufWriter::new(out_file);
 
  // For each def_id, dump their MIR
- for (item, def_id) in items.iter().filter_map(visible_item) {
- writeln!(writer, "// Item: {item:?}").unwrap();
- write_mir_pretty(tcx, Some(rustc_internal::internal(tcx, def_id)), &mut writer)
-  .unwrap();
+ for instance in items.iter().filter_map(get_instance) {
+ writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap();
+ let body = transformer.body(tcx, instance);
+ let _ = body.dump(&mut writer, &instance.name());
  }
  }
 }

kani-compiler/src/kani_middle/reachability.rs

@@ -262,11 +262,22 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
  /// Collect an instance depending on how it is used (invoked directly or via fn_ptr).
  fn collect_instance(&mut self, instance: Instance, is_direct_call: bool) {
  let should_collect = match instance.kind {
- InstanceKind::Virtual { .. } | InstanceKind::Intrinsic => {
+ InstanceKind::Virtual { .. } => {
  // Instance definition has no body.
  assert!(is_direct_call, "Expected direct call {instance:?}");
  false
  }
+ InstanceKind::Intrinsic => {
+ // Intrinsics may have a fallback body.
+ assert!(is_direct_call, "Expected direct call {instance:?}");
+ let TyKind::RigidTy(RigidTy::FnDef(def, _)) = instance.ty().kind() else {
+ unreachable!("Expected function type for intrinsic: {instance:?}")
+ };
+ // The compiler is currently transitioning how to handle intrinsic fallback body.
+ // Until https://github.com/rust-lang/project-stable-mir/issues/79 is implemented
+ // we have to check `must_be_overridden` and `has_body`.
+ !def.as_intrinsic().unwrap().must_be_overridden() && instance.has_body()
+ }
  InstanceKind::Shim | InstanceKind::Item => true,
  };
  if should_collect && should_codegen_locally(&instance) {

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -17,7 +17,7 @@ use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, MirVisitor};
 use stable_mir::mir::Constant;
-use stable_mir::ty::FnDef;
+use stable_mir::ty::{FnDef, RigidTy, TyKind};
 use stable_mir::{CrateDef, CrateItem};
 
 use self::annotations::update_stub_mapping;
@@ -37,6 +37,24 @@ pub fn harness_stub_map(
  stub_pairs
 }
 
+/// Retrieve the index of the host parameter if old definition has one, but not the new definition.
+///
+/// This is to allow constant functions to be stubbed by non-constant functions when the
+/// `effect` feature is on.
+///
+/// Note that the opposite is not supported today, but users should be able to change their stubs.
+///
+/// Note that this has no effect at runtime.
+pub fn contract_host_param(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Option<usize> {
+ let old_generics = tcx.generics_of(rustc_internal::internal(tcx, old_def.def_id()));
+ let new_generics = tcx.generics_of(rustc_internal::internal(tcx, new_def.def_id()));
+ if old_generics.host_effect_index.is_some() && new_generics.host_effect_index.is_none() {
+ old_generics.host_effect_index
+ } else {
+ None
+ }
+}
+
 /// Checks whether the stub is compatible with the original function/method: do
 /// the arities and types (of the parameters and return values) match up? This
 /// does **NOT** check whether the type variables are constrained to implement
@@ -61,15 +79,26 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul
  // Check whether the numbers of generic parameters match.
  let old_def_id = rustc_internal::internal(tcx, old_def.def_id());
  let new_def_id = rustc_internal::internal(tcx, new_def.def_id());
- let old_num_generics = tcx.generics_of(old_def_id).count();
- let stub_num_generics = tcx.generics_of(new_def_id).count();
- if old_num_generics != stub_num_generics {
+ let old_ty = rustc_internal::stable(tcx.type_of(old_def_id)).value;
+ let new_ty = rustc_internal::stable(tcx.type_of(new_def_id)).value;
+ let TyKind::RigidTy(RigidTy::FnDef(_, mut old_args)) = old_ty.kind() else {
+ unreachable!("Expected function, but found {old_ty}")
+ };
+ let TyKind::RigidTy(RigidTy::FnDef(_, new_args)) = new_ty.kind() else {
+ unreachable!("Expected function, but found {new_ty}")
+ };
+ if let Some(idx) = contract_host_param(tcx, old_def, new_def) {
+ old_args.0.remove(idx);
+ }
+
+ // TODO: We should check for the parameter type too or replacement will fail.
+ if old_args.0.len() != new_args.0.len() {
  let msg = format!(
  "mismatch in the number of generic parameters: original function/method `{}` takes {} generic parameters(s), stub `{}` takes {}",
  old_def.name(),
- old_num_generics,
+ old_args.0.len(),
  new_def.name(),
- stub_num_generics
+ new_args.0.len(),
  );
  return Err(msg);
  }

kani-compiler/src/kani_middle/transform/stubs.rs

@@ -3,7 +3,7 @@
 //! This module contains code related to the MIR-to-MIR pass that performs the
 //! stubbing of functions and methods.
 use crate::kani_middle::codegen_units::Stubs;
-use crate::kani_middle::stubbing::validate_stub_const;
+use crate::kani_middle::stubbing::{contract_host_param, validate_stub_const};
 use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
@@ -46,8 +46,12 @@ impl TransformPass for FnStubPass {
  fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
  trace!(function=?instance.name(), "transform");
  let ty = instance.ty();
- if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = ty.kind() {
+ if let TyKind::RigidTy(RigidTy::FnDef(fn_def, mut args)) = ty.kind() {
  if let Some(replace) = self.stubs.get(&fn_def) {
+ if let Some(idx) = contract_host_param(tcx, fn_def, *replace) {
+ debug!(?idx, "FnStubPass::transform remove_host_param");
+ args.0.remove(idx);
+ }
  let new_instance = Instance::resolve(*replace, &args).unwrap();
  debug!(from=?instance.name(), to=?new_instance.name(), "FnStubPass::transform");
  if let Some(body) = FnStubValidator::validate(tcx, (fn_def, *replace), new_instance)

kani-driver/src/call_cargo.rs

@@ -84,8 +84,19 @@ impl KaniSession {
  .env("CARGO_TERM_PROGRESS_WHEN", "never")
  .env("__CARGO_TESTS_ONLY_SRC_ROOT", std_path.as_os_str());
 
- let build_artifacts = self.run_build(cmd)?;
- Ok(build_artifacts.into_iter().filter_map(map_kani_artifact).collect())
+ Ok(self
+ .run_build(cmd)?
+ .into_iter()
+ .filter_map(|artifact| {
+ if artifact.target.crate_types.contains(&CRATE_TYPE_LIB.to_string())
+ || artifact.target.crate_types.contains(&CRATE_TYPE_RLIB.to_string())
+ {
+ map_kani_artifact(artifact)
+ } else {
+ None
+ }
+ })
+ .collect())
  }
 
  /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir`

library/kani/src/lib.rs

@@ -323,4 +323,6 @@ pub use core::assert as __kani__workaround_core_assert;
 // Kani proc macros must be in a separate crate
 pub use kani_macros::*;
 
+pub(crate) use kani_macros::unstable_feature as unstable;
+
 pub mod contracts;

library/kani_core/src/arbitrary.rs

@@ -72,6 +72,8 @@ macro_rules! generate_arbitrary {
  }
 
  // Generate trivial arbitrary values
+ trivial_arbitrary!(());
+
  trivial_arbitrary!(u8);
  trivial_arbitrary!(u16);
  trivial_arbitrary!(u32);