From edded56800e355867c439137e3de83b39b9252ad Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 3 Sep 2024 21:46:12 -0400 Subject: [PATCH 1/2] Update Kani Book (#3474) Add the following to the book: - **Reference section on contracts**. The point of this section is not to be an exhaustive explanation--we have good documentation on contracts already, and we don't want to maintain it in two places. The goal of the section is to give readers an intuition for the main idea and then direct them to more detailed resources. - **Add a reference to the blog**--it's a good resource to learn about Kani and it would be nice to have an easier way to find it. Inspired by [this post](https://users.rust-lang.org/t/can-somebody-explain-how-kani-verifier-works/113918). - **Move the crates documentation earlier.** This partly addresses [#3029](https://github.com/model-checking/kani/issues/3029) by at least making our crates documentation more visible in the book. (I don't have this PR as resolving that issue, since we would need to actually publish the docs on `crates.io` to do that.) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- docs/src/SUMMARY.md | 5 +- docs/src/getting-started.md | 1 + docs/src/reference/experimental/contracts.md | 66 ++++++++++++++++++++ docs/src/reference/experimental/coverage.md | 2 +- 4 files changed, 71 insertions(+), 3 deletions(-) create mode 100644 docs/src/reference/experimental/contracts.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 784ec075d183..d534cf1f7f22 100644 --- a/docs/src/SUMMARY.md +++ b/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) diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md index 5de7ae431850..1acfd039ce97 100644 --- a/docs/src/getting-started.md +++ b/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. diff --git a/docs/src/reference/experimental/contracts.md b/docs/src/reference/experimental/contracts.md new file mode 100644 index 000000000000..fd4e8169bc34 --- /dev/null +++ b/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). diff --git a/docs/src/reference/experimental/coverage.md b/docs/src/reference/experimental/coverage.md index fb73d5f7c05b..5e536b3992b6 100644 --- a/docs/src/reference/experimental/coverage.md +++ b/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: From 93a29af23c569c51ddc56d1a2d22bec1d21e01c2 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Tue, 3 Sep 2024 23:00:36 -0400 Subject: [PATCH 2/2] Cross-function union instrumentation (#3465) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR introduces support for memory initialization checks for unions passed across the function boundary. Whenever a union is passed as an argument, we need to make sure that its initialization state is preserved. Unlike pointers, unions do not have a stable memory address which could identify them in shadow memory. Hence, we need to pass extra information across function boundary since unions are passed “by value”. We introduce a global variable to store the previous address of unions passed as function arguments, which allows us to effectively tie the initialization state of unions passed between functions. This struct is written to by the caller and read from by the callee. For more information about planned functionality, see https://github.com/model-checking/kani/issues/3300 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../kani_middle/transform/check_uninit/mod.rs | 68 ++++++++- .../check_uninit/ptr_uninit/uninit_visitor.rs | 132 +++++++++++++----- .../check_uninit/relevant_instruction.rs | 99 ++++++------- .../transform/check_uninit/ty_layout.rs | 59 ++++++-- .../kani_middle/transform/kani_intrinsics.rs | 8 +- library/kani_core/src/mem_init.rs | 81 ++++++++++- tests/expected/uninit/fixme_unions.rs | 58 +++++++- tests/expected/uninit/unions.expected | 22 ++- tests/expected/uninit/unions.rs | 109 +++++++++++++++ 9 files changed, 516 insertions(+), 120 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 0130c00d1a71..726dc1965770 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/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, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 207005dafb27..bd4356017b6b 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/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 { 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 + }) + } + } } } _ => {} diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs index 6120f2d3d4c4..9ad23071df4a 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs @@ -16,65 +16,38 @@ use strum_macros::AsRefStr; pub enum MemoryInitOp { /// Check memory initialization of data bytes in a memory region starting from the pointer /// `operand` and of length `sizeof(operand)` bytes. - Check { - operand: Operand, - }, + Check { operand: Operand }, /// Set memory initialization state of data bytes in a memory region starting from the pointer /// `operand` and of length `sizeof(operand)` bytes. - Set { - operand: Operand, - value: bool, - position: InsertPosition, - }, + Set { operand: Operand, value: bool, position: InsertPosition }, /// Check memory initialization of data bytes in a memory region starting from the pointer /// `operand` and of length `count * sizeof(operand)` bytes. - CheckSliceChunk { - operand: Operand, - count: Operand, - }, + CheckSliceChunk { operand: Operand, count: Operand }, /// Set memory initialization state of data bytes in a memory region starting from the pointer /// `operand` and of length `count * sizeof(operand)` bytes. - SetSliceChunk { - operand: Operand, - count: Operand, - value: bool, - position: InsertPosition, - }, + SetSliceChunk { operand: Operand, count: Operand, value: bool, position: InsertPosition }, /// Set memory initialization of data bytes in a memory region starting from the reference to /// `operand` and of length `sizeof(operand)` bytes. - CheckRef { - operand: Operand, - }, + CheckRef { operand: Operand }, /// Set memory initialization of data bytes in a memory region starting from the reference to /// `operand` and of length `sizeof(operand)` bytes. - SetRef { - operand: Operand, - value: bool, - position: InsertPosition, - }, + SetRef { operand: Operand, value: bool, position: InsertPosition }, /// Unsupported memory initialization operation. - Unsupported { - reason: String, - }, + Unsupported { reason: String }, /// Operation that trivially accesses uninitialized memory, results in injecting `assert!(false)`. - TriviallyUnsafe { - reason: String, - }, - /// Operation that copies memory initialization state over to another operand. - Copy { - from: Operand, - to: Operand, - count: Operand, - }, - - AssignUnion { - lvalue: Place, - rvalue: Operand, - }, - CreateUnion { - operand: Operand, - field: FieldIdx, - }, + TriviallyUnsafe { reason: String }, + /// Copy memory initialization state over to another operand. + Copy { from: Operand, to: Operand, count: Operand }, + /// Copy memory initialization state over from one union variable to another. + AssignUnion { lvalue: Place, rvalue: Operand }, + /// Create a union from scratch with a given field index and store it in the provided operand. + CreateUnion { operand: Operand, field: FieldIdx }, + /// Load argument containing a union from the argument buffer together if the argument number + /// provided matches. + LoadArgument { operand: Operand, argument_no: usize }, + /// Store argument containing a union into the argument buffer together with the argument number + /// provided. + StoreArgument { operand: Operand, argument_no: usize }, } impl MemoryInitOp { @@ -94,7 +67,9 @@ impl MemoryInitOp { | MemoryInitOp::SetSliceChunk { operand, .. } => operand.clone(), MemoryInitOp::CheckRef { operand, .. } | MemoryInitOp::SetRef { operand, .. } - | MemoryInitOp::CreateUnion { operand, .. } => { + | MemoryInitOp::CreateUnion { operand, .. } + | MemoryInitOp::LoadArgument { operand, .. } + | MemoryInitOp::StoreArgument { operand, .. } => { mk_ref(operand, body, statements, source) } MemoryInitOp::Copy { .. } @@ -141,7 +116,9 @@ impl MemoryInitOp { | MemoryInitOp::SetSliceChunk { operand, .. } => operand.ty(body.locals()).unwrap(), MemoryInitOp::SetRef { operand, .. } | MemoryInitOp::CheckRef { operand, .. } - | MemoryInitOp::CreateUnion { operand, .. } => { + | MemoryInitOp::CreateUnion { operand, .. } + | MemoryInitOp::LoadArgument { operand, .. } + | MemoryInitOp::StoreArgument { operand, .. } => { let place = match operand { Operand::Copy(place) | Operand::Move(place) => place, Operand::Constant(_) => unreachable!(), @@ -188,7 +165,9 @@ impl MemoryInitOp { | MemoryInitOp::CreateUnion { .. } | MemoryInitOp::AssignUnion { .. } | MemoryInitOp::Unsupported { .. } - | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(), + | MemoryInitOp::TriviallyUnsafe { .. } + | MemoryInitOp::StoreArgument { .. } + | MemoryInitOp::LoadArgument { .. } => unreachable!(), } } @@ -204,7 +183,9 @@ impl MemoryInitOp { | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } | MemoryInitOp::Copy { .. } - | MemoryInitOp::AssignUnion { .. } => unreachable!(), + | MemoryInitOp::AssignUnion { .. } + | MemoryInitOp::StoreArgument { .. } + | MemoryInitOp::LoadArgument { .. } => unreachable!(), } } @@ -220,7 +201,9 @@ impl MemoryInitOp { | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } | MemoryInitOp::Copy { .. } - | MemoryInitOp::AssignUnion { .. } => None, + | MemoryInitOp::AssignUnion { .. } + | MemoryInitOp::StoreArgument { .. } + | MemoryInitOp::LoadArgument { .. } => None, } } @@ -233,12 +216,22 @@ impl MemoryInitOp { | MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::CheckRef { .. } | MemoryInitOp::Unsupported { .. } - | MemoryInitOp::TriviallyUnsafe { .. } => InsertPosition::Before, + | MemoryInitOp::TriviallyUnsafe { .. } + | MemoryInitOp::StoreArgument { .. } + | MemoryInitOp::LoadArgument { .. } => InsertPosition::Before, MemoryInitOp::Copy { .. } | MemoryInitOp::AssignUnion { .. } | MemoryInitOp::CreateUnion { .. } => InsertPosition::After, } } + + pub fn expect_argument_no(&self) -> usize { + match self { + MemoryInitOp::LoadArgument { argument_no, .. } + | MemoryInitOp::StoreArgument { argument_no, .. } => *argument_no, + _ => unreachable!(), + } + } } /// Represents an instruction in the source code together with all memory initialization checks/sets diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index dac130f11545..8a9e3ac094d5 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -3,11 +3,12 @@ // //! Utility functions that help calculate type layout. +use std::fmt::Display; + use stable_mir::{ abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape}, target::{MachineInfo, MachineSize}, ty::{AdtKind, IndexedVal, RigidTy, Ty, TyKind, UintTy, VariantIdx}, - CrateDef, }; /// Represents a chunk of data bytes in a data structure. @@ -68,8 +69,41 @@ pub struct PointeeInfo { layout: PointeeLayout, } +/// Different layout computation errors that could arise from the currently unsupported constructs. +pub enum LayoutComputationError { + UnknownUnsizedLayout(Ty), + EnumWithNicheEncoding(Ty), + EnumWithMultiplePaddingVariants(Ty), + UnsupportedType(Ty), + UnionAsField(Ty), +} + +impl Display for LayoutComputationError { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + LayoutComputationError::UnknownUnsizedLayout(ty) => { + write!(f, "Cannot determine layout for an unsized type {ty}") + } + LayoutComputationError::EnumWithNicheEncoding(ty) => { + write!(f, "Cannot determine layout for an Enum with niche encoding of type {ty}") + } + LayoutComputationError::EnumWithMultiplePaddingVariants(ty) => write!( + f, + "Cannot determine layout for an Enum of type {ty}, as it has multiple variants that have different padding." + ), + LayoutComputationError::UnsupportedType(ty) => { + write!(f, "Cannot determine layout for an unsupported type {ty}.") + } + LayoutComputationError::UnionAsField(ty) => write!( + f, + "Cannot determine layout for a type that contains union of type {ty} as a field." + ), + } + } +} + impl PointeeInfo { - pub fn from_ty(ty: Ty) -> Result { + pub fn from_ty(ty: Ty) -> Result { match ty.kind() { TyKind::RigidTy(rigid_ty) => match rigid_ty { RigidTy::Adt(adt_def, args) if adt_def.kind() == AdtKind::Union => { @@ -120,7 +154,7 @@ impl PointeeInfo { }; Ok(PointeeInfo { pointee_ty: ty, layout }) } else { - Err(format!("Cannot determine type layout for type `{ty}`")) + Err(LayoutComputationError::UnknownUnsizedLayout(ty)) } } }, @@ -144,7 +178,7 @@ fn data_bytes_for_ty( machine_info: &MachineInfo, ty: Ty, current_offset: usize, -) -> Result, String> { +) -> Result, LayoutComputationError> { let layout = ty.layout().unwrap().shape(); match layout.fields { @@ -201,9 +235,7 @@ fn data_bytes_for_ty( VariantsShape::Multiple { tag_encoding: TagEncoding::Niche { .. }, .. - } => { - Err(format!("Unsupported Enum `{}` check", def.trimmed_name()))? - } + } => Err(LayoutComputationError::EnumWithNicheEncoding(ty)), VariantsShape::Multiple { variants, tag, .. } => { // Retrieve data bytes for the tag. let tag_size = match tag { @@ -273,10 +305,11 @@ fn data_bytes_for_ty( } else { // Struct has multiple padding variants, Kani cannot // differentiate between them. - Err(format!( - "Unsupported Enum `{}` check", - def.trimmed_name() - )) + Err( + LayoutComputationError::EnumWithMultiplePaddingVariants( + ty, + ), + ) } } } @@ -362,10 +395,10 @@ fn data_bytes_for_ty( | RigidTy::Coroutine(_, _, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) - | RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")), + | RigidTy::Dynamic(_, _, _) => Err(LayoutComputationError::UnsupportedType(ty)), } } - FieldsShape::Union(_) => Err(format!("Unions as fields of unions are unsupported {ty:?}")), + FieldsShape::Union(_) => Err(LayoutComputationError::UnionAsField(ty)), FieldsShape::Array { .. } => Ok(vec![]), } } diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 9210c43fb163..5a026db525a7 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -195,9 +195,9 @@ impl IntrinsicGeneratorPass { let arg_ty = new_body.locals()[1].ty; // Sanity check: since CBMC memory object primitives only accept pointers, need to // ensure the correct type. - let TyKind::RigidTy(RigidTy::RawPtr(target_ty, _)) = arg_ty.kind() else { unreachable!() }; + let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = arg_ty.kind() else { unreachable!() }; // Calculate pointee layout for byte-by-byte memory initialization checks. - let pointee_info = PointeeInfo::from_ty(target_ty); + let pointee_info = PointeeInfo::from_ty(pointee_ty); match pointee_info { Ok(pointee_info) => { match pointee_info.layout() { @@ -338,7 +338,7 @@ impl IntrinsicGeneratorPass { } }; } - Err(msg) => { + Err(reason) => { // We failed to retrieve the type layout. let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { const_: MirConst::from_bool(false), @@ -348,7 +348,7 @@ impl IntrinsicGeneratorPass { let result = new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let reason = format!( - "Kani currently doesn't support checking memory initialization of `{target_ty}`. {msg}" + "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}. {reason}", ); new_body.insert_check( tcx, diff --git a/library/kani_core/src/mem_init.rs b/library/kani_core/src/mem_init.rs index cec23c14263b..6475c62e31ae 100644 --- a/library/kani_core/src/mem_init.rs +++ b/library/kani_core/src/mem_init.rs @@ -22,6 +22,13 @@ #[allow(clippy::crate_in_macro_def)] macro_rules! kani_mem_init { ($core:path) => { + /// Global object for tracking memory initialization state. + #[rustc_diagnostic_item = "KaniMemoryInitializationState"] + static mut MEM_INIT_STATE: MemoryInitializationState = MemoryInitializationState::new(); + + /// Global object for tracking union initialization state across function boundaries. + static mut ARGUMENT_BUFFER: Option = None; + /// Bytewise mask, representing which bytes of a type are data and which are padding. /// For example, for a type like this: /// ``` @@ -97,6 +104,7 @@ macro_rules! kani_mem_init { /// Copy memory initialization state by non-deterministically switching the tracked object and /// adjusting the tracked offset. + #[kanitool::disable_checks(pointer)] pub fn copy( &mut self, from_ptr: *const u8, @@ -119,6 +127,24 @@ macro_rules! kani_mem_init { self.tracked_offset += to_offset - from_offset; // Note that this preserves the value. } + } else { + self.bless::(to_ptr, 1); + } + } + + /// Set currently tracked memory initialization state to `true` if `ptr` points to the + /// currently tracked object and the tracked offset lies within `LAYOUT_SIZE * num_elts` + /// bytes of `ptr`. + #[kanitool::disable_checks(pointer)] + pub fn bless(&mut self, ptr: *const u8, num_elts: usize) { + let obj = super::mem::pointer_object(ptr); + let offset = super::mem::pointer_offset(ptr); + + if self.tracked_object_id == obj + && self.tracked_offset >= offset + && self.tracked_offset < offset + num_elts * LAYOUT_SIZE + { + self.value = true; } } @@ -172,10 +198,6 @@ macro_rules! kani_mem_init { } } - /// Global object for tracking memory initialization state. - #[rustc_diagnostic_item = "KaniMemoryInitializationState"] - static mut MEM_INIT_STATE: MemoryInitializationState = MemoryInitializationState::new(); - /// Set tracked object and tracked offset to a non-deterministic value. #[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniInitializeMemoryInitializationState"] @@ -343,5 +365,56 @@ macro_rules! kani_mem_init { fn copy_init_state_single(from: *const T, to: *const T) { copy_init_state::(from, to, 1); } + + /// Information about currently tracked argument, used for passing union initialization + /// state across function boundaries. This struct is written to by the caller and read from + /// by the callee. + #[derive(Clone, Copy)] + struct ArgumentBuffer { + selected_argument: usize, + saved_address: *const (), + layout_size: usize, + } + + /// Non-deterministically store information about currently tracked argument in the argument + /// buffer. + #[kanitool::disable_checks(pointer)] + #[rustc_diagnostic_item = "KaniStoreArgument"] + fn store_argument(from: *const T, selected_argument: usize) { + let (from_ptr, _) = from.to_raw_parts(); + let should_store: bool = super::any(); + if should_store { + unsafe { + ARGUMENT_BUFFER = Some(ArgumentBuffer { + selected_argument, + saved_address: from_ptr, + layout_size: LAYOUT_SIZE, + }) + } + } + } + + /// Load information from the argument buffer (if the argument position matches) via copying + /// the memory initialization information from an address in the caller to an address in the + /// callee. Otherwise, mark that the argument as initialized, as it will be checked by + /// another non-deterministic branch. Reset the argument buffer after loading from it. + #[kanitool::disable_checks(pointer)] + #[rustc_diagnostic_item = "KaniLoadArgument"] + fn load_argument(to: *const T, selected_argument: usize) { + let (to_ptr, _) = to.to_raw_parts(); + if let Some(buffer) = unsafe { ARGUMENT_BUFFER } { + if buffer.selected_argument == selected_argument { + assert!(buffer.layout_size == LAYOUT_SIZE); + copy_init_state_single::(buffer.saved_address, to_ptr); + unsafe { + ARGUMENT_BUFFER = None; + } + return; + } + } + unsafe { + MEM_INIT_STATE.bless::(to_ptr as *const u8, 1); + } + } }; } diff --git a/tests/expected/uninit/fixme_unions.rs b/tests/expected/uninit/fixme_unions.rs index ec86e5e7e07f..b0e7d600187d 100644 --- a/tests/expected/uninit/fixme_unions.rs +++ b/tests/expected/uninit/fixme_unions.rs @@ -14,14 +14,13 @@ union U { b: u32, } -/// Reading padding data via simple union access if union is passed to another function. +/// Reading non-padding data but a union is behind a pointer. #[kani::proof] -unsafe fn cross_function_union_should_fail() { - unsafe fn helper(u: U) { - let padding = u.b; // Read 4 bytes from `u`. - } +unsafe fn pointer_union_should_pass() { let u = U { a: 0 }; // `u` is initialized for 2 bytes. - helper(u); + let u_ptr = addr_of!(u); + let u1 = *u_ptr; + let padding = u1.a; // Read 2 bytes from `u`. } /// Reading padding data but a union is behind a pointer. @@ -48,14 +47,59 @@ unsafe fn union_as_subfields_should_pass() { let padding = u1.a; // Read 2 bytes from `u`. } +/// Tests initialized access if unions are top-level subfields. +#[kani::proof] +unsafe fn union_as_subfields_should_fail() { + let u = U { a: 0 }; // `u` is initialized for 2 bytes. + let s = S { u }; + let s1 = s; + let u1 = s1.u; // `u1` is initialized for 2 bytes. + let padding = u1.b; // Read 4 bytes from `u`. +} + union Outer { u: U, a: u32, } -/// Tests unions composing with other unions. +/// Tests unions composing with other unions and reading non-padding data. #[kani::proof] unsafe fn uber_union_should_pass() { let u = Outer { u: U { b: 0 } }; // `u` is initialized for 4 bytes. let non_padding = u.a; // Read 4 bytes from `u`. } + +/// Tests unions composing with other unions and reading padding data. +#[kani::proof] +unsafe fn uber_union_should_fail() { + let u = Outer { u: U { a: 0 } }; // `u` is initialized for 2 bytes. + let padding = u.a; // Read 4 bytes from `u`. +} + +/// Attempting to read initialized data via transmuting a union. +#[kani::proof] +unsafe fn transmute_union_should_pass() { + let u = U { b: 0 }; // `u` is initialized for 4 bytes. + let non_padding: u32 = std::mem::transmute(u); // Transmute `u` into a value of 4 bytes. +} + +/// Attempting to read uninitialized data via transmuting a union. +#[kani::proof] +unsafe fn transmute_union_should_fail() { + let u = U { a: 0 }; // `u` is initialized for 2 bytes. + let padding: u32 = std::mem::transmute(u); // Transmute `u` into a value of 4 bytes. +} + +/// Attempting to transmute into union and read initialized data. +#[kani::proof] +unsafe fn transmute_into_union_should_pass() { + let u: U = std::mem::transmute(0u32); // `u` is initialized for 4 bytes. + let non_padding = u.b; // Read 4 bytes from `u`. +} + +/// Attempting to transmute into union and read uninitialized data. +#[kani::proof] +unsafe fn transmute_into_union_should_fail() { + let u: U = std::mem::transmute_copy(&0u16); // `u` is initialized for 2 bytes. + let padding = u.b; // Read 4 bytes from `u`. +} diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected index 05fdac3a8765..ca7f777c4065 100644 --- a/tests/expected/uninit/unions.expected +++ b/tests/expected/uninit/unions.expected @@ -10,8 +10,28 @@ basic_union_should_fail.assertion.1\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" +cross_function_union_should_fail::helper.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" + +cross_function_multi_union_should_fail::helper.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" + +multi_cross_function_union_should_fail::sub_helper.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" + +basic_multifield_union_should_fail.assertion.7\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" + Summary: +Verification failed for - cross_function_multi_union_should_fail +Verification failed for - multi_cross_function_union_should_fail +Verification failed for - cross_function_union_should_fail Verification failed for - union_update_should_fail Verification failed for - union_complex_subfields_should_fail +Verification failed for - basic_multifield_union_should_fail Verification failed for - basic_union_should_fail -Complete - 3 successfully verified harnesses, 3 failures, 6 total. +Complete - 7 successfully verified harnesses, 7 failures, 14 total. diff --git a/tests/expected/uninit/unions.rs b/tests/expected/uninit/unions.rs index c623f9fcea94..979120fb566c 100644 --- a/tests/expected/uninit/unions.rs +++ b/tests/expected/uninit/unions.rs @@ -30,6 +30,42 @@ unsafe fn basic_union_should_fail() { let padding = u1.b; } +#[repr(C)] +#[derive(Clone, Copy)] +union MultiU { + d: u128, + a: u16, + c: u64, + b: u32, +} + +/// Simple and correct multifield union access. +#[kani::proof] +unsafe fn basic_multifield_union_should_pass() { + let u = MultiU { c: 0 }; + let mut u1 = u; + let non_padding_a = u1.a; + assert!(non_padding_a == 0); + let non_padding_b = u1.b; + assert!(non_padding_b == 0); + let non_padding_c = u1.c; + assert!(non_padding_c == 0); +} + +/// Reading padding data via simple multifield union access. +#[kani::proof] +unsafe fn basic_multifield_union_should_fail() { + let u = MultiU { c: 0 }; + let mut u1 = u; + let non_padding_a = u1.a; + assert!(non_padding_a == 0); + let non_padding_b = u1.b; + assert!(non_padding_b == 0); + let non_padding_c = u1.c; + assert!(non_padding_c == 0); + let padding = u1.d; // Accessing uninitialized data. +} + #[repr(C)] union U1 { a: (u32, u8), @@ -66,3 +102,76 @@ unsafe fn union_update_should_fail() { u.a = 0; let padding = u.b; } + +/// Reading padding data via simple union access if union is passed to another function. +#[kani::proof] +unsafe fn cross_function_union_should_fail() { + unsafe fn helper(u: U) { + let padding = u.b; // Read 4 bytes from `u`. + } + let u = U { a: 0 }; // `u` is initialized for 2 bytes. + helper(u); +} + +/// Reading non-padding data via simple union access if union is passed to another function. +#[kani::proof] +unsafe fn cross_function_union_should_pass() { + unsafe fn helper(u: U) { + let non_padding = u.a; // Read 2 bytes from `u`. + } + let u = U { a: 0 }; // `u` is initialized for 2 bytes. + helper(u); +} + +/// Reading padding data via simple union access if union is passed to another function multiple +/// times. +#[kani::proof] +unsafe fn multi_cross_function_union_should_fail() { + unsafe fn helper(u: U) { + sub_helper(u); + } + unsafe fn sub_helper(u: U) { + let padding = u.b; // Read 4 bytes from `u`. + } + let u = U { a: 0 }; // `u` is initialized for 2 bytes. + helper(u); +} + +/// Reading non-padding data via simple union access if union is passed to another function multiple +/// times. +#[kani::proof] +unsafe fn multi_cross_function_union_should_pass() { + unsafe fn helper(u: U) { + sub_helper(u); + } + unsafe fn sub_helper(u: U) { + let non_padding = u.a; // Read 2 bytes from `u`. + } + let u = U { a: 0 }; // `u` is initialized for 2 bytes. + helper(u); +} + +/// Reading padding data via simple union access if multiple unions are passed to another function. +#[kani::proof] +unsafe fn cross_function_multi_union_should_fail() { + unsafe fn helper(u1: U, u2: U) { + let padding = u1.b; // Read 4 bytes from `u1`. + let non_padding = u2.b; // Read 4 bytes from `u2`. + } + let u1 = U { a: 0 }; // `u1` is initialized for 2 bytes. + let u2 = U { b: 0 }; // `u2` is initialized for 4 bytes. + helper(u1, u2); +} + +/// Reading non-padding data via simple union access if multiple unions are passed to another +/// function. +#[kani::proof] +unsafe fn cross_function_multi_union_should_pass() { + unsafe fn helper(u1: U, u2: U) { + let padding = u1.b; // Read 4 bytes from `u1`. + let non_padding = u2.b; // Read 4 bytes from `u2`. + } + let u1 = U { b: 0 }; // `u1` is initialized for 4 bytes. + let u2 = U { b: 0 }; // `u2` is initialized for 4 bytes. + helper(u1, u2); +}