Merge branch 'main' into toolchain-2024-09-04

docs/src/SUMMARY.md

@@ -7,6 +7,8 @@
  - [Using Kani](./usage.md)
  - [Verification results](./verification-results.md)
 
+- [Crates Documentation](./crates/index.md)
+
 - [Tutorial](./kani-tutorial.md)
  - [First steps](./tutorial-first-steps.md)
  - [Failures that Kani can spot](./tutorial-kinds-of-failure.md)
@@ -18,6 +20,7 @@
  - [Experimental features](./reference/experimental/experimental-features.md)
  - [Coverage](./reference/experimental/coverage.md)
  - [Stubbing](./reference/experimental/stubbing.md)
+ - [Contracts](./reference/experimental/contracts.md)
  - [Concrete Playback](./reference/experimental/concrete-playback.md)
 - [Application](./application.md)
  - [Comparison with other tools](./tool-comparison.md)
@@ -45,8 +48,6 @@
  - [Unstable features](./rust-feature-support/unstable.md)
  - [Overrides](./overrides.md)
 
-- [Crates Documentation](./crates/index.md)
-
 ---
 
 - [FAQ](./faq.md)

docs/src/getting-started.md

@@ -15,6 +15,7 @@ Proof harnesses are similar to test harnesses, especially property-based test ha
 Kani is currently under active development.
 Releases are published [here](https://github.com/model-checking/kani/releases).
 Major changes to Kani are documented in the [RFC Book](https://model-checking.github.io/kani/rfc).
+We also publish updates on Kani use cases and features on our [blog](https://model-checking.github.io/kani-verifier-blog/).
 
 There is support for a fair amount of Rust language features, but not all (e.g., concurrency).
 Please see [Limitations](./limitations.md) for a detailed list of supported features.

docs/src/reference/experimental/contracts.md

@@ -0,0 +1,66 @@
+# Contracts
+
+Consider the following example:
+
+```rust
+fn gcd(mut max: u8, mut min: u8) -> u8 {
+ if min > max {
+ std::mem::swap(&mut max, &mut min);
+ }
+
+ let rest = max % min;
+ if rest == 0 { min } else { gcd(min, rest) }
+}
+```
+Let's assume we want to verify some code that calls `gcd`.
+In the [worst case](https://en.wikipedia.org/wiki/Euclidean_algorithm#Worst-case), the number of steps (recursions) in `gcd` approaches 1.5 times the number of bits needed to represent the input numbers. 
+So, for two large 64-bit numbers, a single call to `gcd` can take almost 96 iterations.
+It would be very expensive for Kani to unroll each of these iterations and then perform symbolic execution.
+
+Instead, we can write *contracts* with guarantees about `gcd`'s behavior.
+Once Kani verifies that `gcd`'s contracts are correct, it can replace each invocation of `gcd` with its contracts, which reduces verification time for `gcd`'s callers.
+For example, perhaps we want to ensure that the returned `result` does indeed divide both `max` and `min`.
+In that case, we could write contracts like these:
+
+```rust
+#[kani::requires(min != 0 && max != 0)]
+#[kani::ensures(|result| *result != 0 && max % *result == 0 && min % *result == 0)]
+#[kani::recursion]
+fn gcd(mut max: u8, mut min: u8) -> u8 { ... }
+```
+
+Since `gcd` performs `max % min` (and perhaps swaps those values), passing zero as an argument could cause a division by zero.
+The `requires` contract tells Kani to restrict the range of nondeterministic inputs to nonzero ones so that we don't run into this error.
+The `ensures` contract is what actually checks that the result is a correct divisor for the inputs.
+(The `recursion` attribute is required when using contracts on recursive functions).
+
+Then, we would write a harness to *verify* those contracts, like so:
+
+```rust
+#[kani::proof_for_contract(gcd)]
+fn check_gcd() {
+ let max: u8 = kani::any();
+ let min: u8 = kani::any();
+ gcd(max, min);
+}
+```
+
+and verify it by running `kani -Z function-contracts`.
+
+Once Kani verifies the contracts, we can use Kani's [stubbing feature](stubbing.md) to replace all invocations to `gcd` with its contracts, for instance:
+
+```rust
+// Assume foo() invokes gcd().
+// By using stub_verified, we tell Kani to replace 
+// invocations of gcd() with its verified contracts.
+#[kani::proof]
+#[kani::stub_verified(gcd)]
+fn check_foo() {
+ let x: u8 = kani::any();
+ foo(x);
+}
+```
+By leveraging the stubbing feature, we can replace the (expensive) `gcd` call with a *verified abstraction* of its behavior, greatly reducing verification time for `foo`.
+
+There is far more to learn about contracts.
+We highly recommend reading our [blog post about contracts](https://model-checking.github.io/kani-verifier-blog/2024/01/29/function-contracts.html) (from which this `gcd` example is taken). We also recommend looking at the `contracts` module in our [documentation](../../crates/index.md).

docs/src/reference/experimental/coverage.md

@@ -1,4 +1,4 @@
-## Coverage
+# Coverage
 
 Recall our `estimate_size` example from [First steps](../../tutorial-first-steps.md),
 where we wrote a proof harness constraining the range of inputs to integers less than 4096:

kani-compiler/src/kani_middle/transform/check_uninit/mod.rs

@@ -45,6 +45,9 @@ const KANI_IS_STR_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniIsStrPtrInitialized";
 const KANI_SET_STR_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniSetStrPtrInitialized";
 const KANI_COPY_INIT_STATE_DIAGNOSTIC: &str = "KaniCopyInitState";
 const KANI_COPY_INIT_STATE_SINGLE_DIAGNOSTIC: &str = "KaniCopyInitStateSingle";
+const KANI_LOAD_ARGUMENT_DIAGNOSTIC: &str = "KaniLoadArgument";
+const KANI_STORE_ARGUMENT_DIAGNOSTIC: &str = "KaniStoreArgument";
+const KANI_RESET_ARGUMENT_BUFFER_DIAGNOSTIC: &str = "KaniResetArgumentBuffer";
 
 // Function bodies of those functions will not be instrumented as not to cause infinite recursion.
 const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = &[
@@ -58,6 +61,9 @@ const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = &[
  KANI_SET_STR_PTR_INITIALIZED_DIAGNOSTIC,
  KANI_COPY_INIT_STATE_DIAGNOSTIC,
  KANI_COPY_INIT_STATE_SINGLE_DIAGNOSTIC,
+ KANI_LOAD_ARGUMENT_DIAGNOSTIC,
+ KANI_STORE_ARGUMENT_DIAGNOSTIC,
+ KANI_RESET_ARGUMENT_BUFFER_DIAGNOSTIC,
 ];
 
 /// Instruments the code with checks for uninitialized memory, agnostic to the source of targets.
@@ -159,9 +165,9 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
  // Calculate pointee layout for byte-by-byte memory initialization checks.
  match PointeeInfo::from_ty(pointee_ty) {
  Ok(type_info) => type_info,
- Err(_) => {
+ Err(reason) => {
  let reason = format!(
- "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}.",
+ "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}. {reason}",
  );
  self.inject_assert_false(self.tcx, body, source, operation.position(), &reason);
  return;
@@ -185,6 +191,9 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
  MemoryInitOp::AssignUnion { .. } => {
  self.build_assign_union(body, source, operation, pointee_info)
  }
+ MemoryInitOp::StoreArgument { .. } | MemoryInitOp::LoadArgument { .. } => {
+ self.build_argument_operation(body, source, operation, pointee_info)
+ }
  MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => {
  unreachable!()
  }
@@ -532,6 +541,61 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
  );
  }
 
+ /// Instrument the code to pass information about arguments containing unions. Whenever a
+ /// function is called and some of the arguments contain unions, we store the information. And
+ /// when we enter the callee, we load the information.
+ fn build_argument_operation(
+ &mut self,
+ body: &mut MutableBody,
+ source: &mut SourceInstruction,
+ operation: MemoryInitOp,
+ pointee_info: PointeeInfo,
+ ) {
+ let ret_place = Place {
+ local: body.new_local(Ty::new_tuple(&[]), source.span(body.blocks()), Mutability::Not),
+ projection: vec![],
+ };
+ let mut statements = vec![];
+ let layout_size = pointee_info.layout().maybe_size().unwrap();
+ let diagnostic = match operation {
+ MemoryInitOp::LoadArgument { .. } => KANI_LOAD_ARGUMENT_DIAGNOSTIC,
+ MemoryInitOp::StoreArgument { .. } => KANI_STORE_ARGUMENT_DIAGNOSTIC,
+ _ => unreachable!(),
+ };
+ let argument_operation_instance = resolve_mem_init_fn(
+ get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache),
+ layout_size,
+ *pointee_info.ty(),
+ );
+ let operand = operation.mk_operand(body, &mut statements, source);
+ let argument_no = operation.expect_argument_no();
+ let terminator = Terminator {
+ kind: TerminatorKind::Call {
+ func: Operand::Copy(Place::from(body.new_local(
+ argument_operation_instance.ty(),
+ source.span(body.blocks()),
+ Mutability::Not,
+ ))),
+ args: vec![
+ operand,
+ Operand::Constant(ConstOperand {
+ span: source.span(body.blocks()),
+ user_ty: None,
+ const_: MirConst::try_from_uint(argument_no as u128, UintTy::Usize)
+ .unwrap(),
+ }),
+ ],
+ destination: ret_place.clone(),
+ target: Some(0), // this will be overriden in add_bb
+ unwind: UnwindAction::Terminate,
+ },
+ span: source.span(body.blocks()),
+ };
+
+ // Construct the basic block and insert it into the body.
+ body.insert_bb(BasicBlock { statements, terminator }, source, operation.position());
+ }
+
  /// Copy memory initialization state from one union variable to another.
  fn build_assign_union(
  &mut self,

kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs

@@ -9,8 +9,8 @@ use crate::{
  body::{InsertPosition, MutableBody, SourceInstruction},
  check_uninit::{
  relevant_instruction::{InitRelevantInstruction, MemoryInitOp},
- ty_layout::tys_layout_compatible_to_size,
- TargetFinder,
+ ty_layout::{tys_layout_compatible_to_size, LayoutComputationError},
+ PointeeInfo, TargetFinder,
  },
  },
 };
@@ -38,11 +38,38 @@ impl TargetFinder for CheckUninitVisitor {
  fn find_all(mut self, body: &MutableBody) -> Vec<InitRelevantInstruction> {
  self.locals = body.locals().to_vec();
  for (bb_idx, bb) in body.blocks().iter().enumerate() {
- self.current_target = InitRelevantInstruction {
- source: SourceInstruction::Statement { idx: 0, bb: bb_idx },
- before_instruction: vec![],
- after_instruction: vec![],
+ // Set the first target to start iterating from.
+ self.current_target = if !bb.statements.is_empty() {
+ InitRelevantInstruction {
+ source: SourceInstruction::Statement { idx: 0, bb: bb_idx },
+ before_instruction: vec![],
+ after_instruction: vec![],
+ }
+ } else {
+ InitRelevantInstruction {
+ source: SourceInstruction::Terminator { bb: bb_idx },
+ before_instruction: vec![],
+ after_instruction: vec![],
+ }
  };
+ if bb_idx == 0 {
+ let union_args: Vec<_> = body
+ .locals()
+ .iter()
+ .enumerate()
+ .skip(1)
+ .take(body.arg_count())
+ .filter(|(_, local)| local.ty.kind().is_union())
+ .collect();
+ if !union_args.is_empty() {
+ for (idx, _) in union_args {
+ self.push_target(MemoryInitOp::LoadArgument {
+ operand: Operand::Copy(Place { local: idx, projection: vec![] }),
+ argument_no: idx,
+ })
+ }
+ }
+ }
  self.visit_basic_block(bb);
  }
  self.targets
@@ -84,6 +111,22 @@ impl MirVisitor for CheckUninitVisitor {
  StatementKind::Assign(place, rvalue) => {
  // First check rvalue.
  self.visit_rvalue(rvalue, location);
+
+ // Preemptively check if we do not support computing the layout of a type because of
+ // inner union fields. This allows to inject `assert!(false)` early.
+ if let Err(reason @ LayoutComputationError::UnionAsField(_)) =
+ PointeeInfo::from_ty(place.ty(&self.locals).unwrap())
+ {
+ self.push_target(MemoryInitOp::Unsupported {
+ reason: format!(
+ "Checking memory initialization of type {} is not supported. {}",
+ place.ty(&self.locals).unwrap(),
+ reason
+ ),
+ });
+ return;
+ }
+
  // Check whether we are assigning into a dereference (*ptr = _).
  if let Some(place_without_deref) = try_remove_topmost_deref(place) {
  // First, check that we are not dereferencing extra pointers along the way
@@ -127,9 +170,10 @@ impl MirVisitor for CheckUninitVisitor {
  // if a union as a subfield is detected, `assert!(false)` will be injected from
  // the type layout code.
  let is_inside_union = {
- let mut contains_union = false;
  let mut place_to_add_projections =
  Place { local: place.local, projection: vec![] };
+ let mut contains_union =
+ place_to_add_projections.ty(&self.locals).unwrap().kind().is_union();
  for projection_elem in place.projection.iter() {
  if place_to_add_projections.ty(&self.locals).unwrap().kind().is_union() {
  contains_union = true;
@@ -143,35 +187,37 @@ impl MirVisitor for CheckUninitVisitor {
  // Need to copy some information about union initialization, since lvalue is
  // either a union or a field inside a union.
  if is_inside_union {
- if let Rvalue::Use(operand) = rvalue {
- // This is a union-to-union assignment, so we need to copy the
- // initialization state.
- if place.ty(&self.locals).unwrap().kind().is_union() {
- self.push_target(MemoryInitOp::AssignUnion {
- lvalue: place.clone(),
- rvalue: operand.clone(),
- });
- } else {
- // This is assignment to a field of a union.
- self.push_target(MemoryInitOp::SetRef {
- operand: Operand::Copy(place.clone()),
- value: true,
- position: InsertPosition::After,
- });
+ match rvalue {
+ Rvalue::Use(operand) => {
+ // This is a union-to-union assignment, so we need to copy the
+ // initialization state.
+ if place.ty(&self.locals).unwrap().kind().is_union() {
+ self.push_target(MemoryInitOp::AssignUnion {
+ lvalue: place.clone(),
+ rvalue: operand.clone(),
+ });
+ } else {
+ // This is assignment to a field of a union.
+ self.push_target(MemoryInitOp::SetRef {
+ operand: Operand::Copy(place.clone()),
+ value: true,
+ position: InsertPosition::After,
+ });
+ }
  }
- }
- }
-
- // Create a union from scratch as an aggregate. We handle it here because we
- // need to know which field is getting assigned.
- if let Rvalue::Aggregate(AggregateKind::Adt(adt_def, _, _, _, union_field), _) =
- rvalue
- {
- if adt_def.kind() == AdtKind::Union {
- self.push_target(MemoryInitOp::CreateUnion {
-  operand: Operand::Copy(place.clone()),
-  field: union_field.unwrap(), // Safe to unwrap because we know this is a union.
- });
+  Rvalue::Aggregate(AggregateKind::Adt(adt_def, _, _, _, union_field), _) => {
+  // Create a union from scratch as an aggregate. We handle it here because we
+ // need to know which field is getting assigned.
+  if adt_def.kind() == AdtKind::Union {
+  self.push_target(MemoryInitOp::CreateUnion {
+  operand: Operand::Copy(place.clone()),
+  field: union_field.unwrap(), // Safe to unwrap because we know this is a union.
+  });
+  }
+ }
+ // TODO: add support for Rvalue::Cast, etc.
+ _ => self
+  .push_target(MemoryInitOp::Unsupported { reason: "Performing a union assignment with a non-supported construct as an Rvalue".to_string() }),
  }
  }
  }
@@ -218,7 +264,7 @@ impl MirVisitor for CheckUninitVisitor {
  before_instruction: vec![],
  };
  } else {
- unreachable!()
+ // The only instruction in this basic block is the terminator, which was already set.
  }
  // Leave it as an exhaustive match to be notified when a new kind is added.
  match &term.kind {
@@ -340,6 +386,20 @@ impl MirVisitor for CheckUninitVisitor {
  }
  _ => {}
  }
+ } else {
+ let union_args: Vec<_> = args
+ .iter()
+ .enumerate()
+ .filter(|(_, arg)| arg.ty(&self.locals).unwrap().kind().is_union())
+ .collect();
+ if !union_args.is_empty() {
+ for (idx, operand) in union_args {
+ self.push_target(MemoryInitOp::StoreArgument {
+ operand: operand.clone(),
+ argument_no: idx + 1, // since arguments are 1-indexed
+ })
+ }
+ }
  }
  }
  _ => {}