From 6cf4ea46924f17c148cc590fe99b40c6a5282a52 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 3 Sep 2024 13:12:22 -0400 Subject: [PATCH 01/21] Add tests for fixed issues. (#3484) #2239 and #3022 are resolved in Kani v0.5.4. Add tests for them. Resolves #2239 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- tests/expected/issue-2239/issue_2239.expected | 5 ++++ tests/expected/issue-2239/issue_2239.rs | 15 ++++++++++++ tests/expected/issue-3022/issue_3022.expected | 5 ++++ tests/expected/issue-3022/issue_3022.rs | 24 +++++++++++++++++++ 4 files changed, 49 insertions(+) create mode 100644 tests/expected/issue-2239/issue_2239.expected create mode 100644 tests/expected/issue-2239/issue_2239.rs create mode 100644 tests/expected/issue-3022/issue_3022.expected create mode 100644 tests/expected/issue-3022/issue_3022.rs diff --git a/tests/expected/issue-2239/issue_2239.expected b/tests/expected/issue-2239/issue_2239.expected new file mode 100644 index 000000000000..8bdab0df1862 --- /dev/null +++ b/tests/expected/issue-2239/issue_2239.expected @@ -0,0 +1,5 @@ +test_trivial_bounds.unreachable.1\ +- Status: FAILURE\ +- Description: "unreachable code" + +VERIFICATION:- FAILED \ No newline at end of file diff --git a/tests/expected/issue-2239/issue_2239.rs b/tests/expected/issue-2239/issue_2239.rs new file mode 100644 index 000000000000..36c41dec604d --- /dev/null +++ b/tests/expected/issue-2239/issue_2239.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#![feature(trivial_bounds)] +#![allow(unused, trivial_bounds)] + +#[kani::proof] +fn test_trivial_bounds() +where + i32: Iterator, +{ + for _ in 2i32 {} +} + +fn main() {} diff --git a/tests/expected/issue-3022/issue_3022.expected b/tests/expected/issue-3022/issue_3022.expected new file mode 100644 index 000000000000..9600182a5209 --- /dev/null +++ b/tests/expected/issue-3022/issue_3022.expected @@ -0,0 +1,5 @@ +main.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: inner == func2.inner" + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/issue-3022/issue_3022.rs b/tests/expected/issue-3022/issue_3022.rs new file mode 100644 index 000000000000..6ef6f944395f --- /dev/null +++ b/tests/expected/issue-3022/issue_3022.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +type BuiltIn = for<'a> fn(&str); + +struct Function { + inner: BuiltIn, +} + +impl Function { + fn new(subr: BuiltIn) -> Self { + Self { inner: subr } + } +} + +fn dummy(_: &str) {} + +#[kani::proof] +fn main() { + let func1 = Function::new(dummy); + let func2 = Function::new(dummy); + let inner: fn(&'static _) -> _ = func1.inner; + assert!(inner == func2.inner); +} From edded56800e355867c439137e3de83b39b9252ad Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 3 Sep 2024 21:46:12 -0400 Subject: [PATCH 02/21] 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 03/21] 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); +} From 4a9a70c1a2119c47004adcb1e9f4bd9ebcbe8eec Mon Sep 17 00:00:00 2001 From: rahulku Date: Wed, 4 Sep 2024 05:18:07 -0700 Subject: [PATCH 04/21] vstte paper (#3473) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig Co-authored-by: Michael Tautschnig --- papers/vstte2024/README.md | 1 + papers/vstte2024/paper.bib | 135 ++++++++++++++++++++++++++ papers/vstte2024/paper.tex | 172 ++++++++++++++++++++++++++++++++++ scripts/ci/copyright_check.py | 12 +-- 4 files changed, 314 insertions(+), 6 deletions(-) create mode 100644 papers/vstte2024/README.md create mode 100644 papers/vstte2024/paper.bib create mode 100644 papers/vstte2024/paper.tex diff --git a/papers/vstte2024/README.md b/papers/vstte2024/README.md new file mode 100644 index 000000000000..568b501138b5 --- /dev/null +++ b/papers/vstte2024/README.md @@ -0,0 +1 @@ +This contains the contents for a short paper at VSTTE2024. In order to build this, please download the LLNCS style file available at https://resource-cms.springernature.com/springer-cms/rest/v1/content/19238648/data/v8, unpack the resulting llncs.zip, and use standard LaTeX tools to build the paper. \ No newline at end of file diff --git a/papers/vstte2024/paper.bib b/papers/vstte2024/paper.bib new file mode 100644 index 000000000000..dafdbc98cbb2 --- /dev/null +++ b/papers/vstte2024/paper.bib @@ -0,0 +1,135 @@ +% Copyright Kani Contributors +% SPDX-License-Identifier: Apache-2.0 OR MIT + +\begin{paper}{8} +@inproceedings{verus-sys, + author = {Lattuada, Andrea and Hance, Travis and Bosamiya, Jay and Brun, Matthias and Cho, Chanhee and LeBlanc, Hayley and Srinivasan, Pranav and Achermann, Reto and Chajed, Tej and Hawblitzel, Chris and Howell, Jon and Lorch, Jay and Padon, Oded and Parno, Bryan}, + booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)}, + code = {https://github.com/verus-lang/verus}, + month = {November}, + title = {Verus: A Practical Foundation for Systems Verification}, + year = {2024} +} + +@inproceedings{denis2022creusot, + title={Creusot: a foundry for the deductive verification of {R}ust programs}, + author={Denis, Xavier and Jourdan, Jacques-Henri and March{'e}, Claude}, + booktitle={International Conference on Formal Engineering Methods}, + pages={90--105}, + year={2022}, + organization={Springer} +} + +@inproceedings{astrauskas2022prusti, + title={The {P}rusti project: Formal verification for {R}ust}, + author={Astrauskas, Vytautas and B{\'\i}l{\`y}, Aurel and Fiala, Jon{\'a}{\v{s}} and Grannan, Zachary and Matheja, Christoph and M{\"u}ller, Peter and Poli, Federico and Summers, Alexander J}, + booktitle={NASA Formal Methods Symposium}, + pages={88--108}, + year={2022}, + organization={Springer} +} + +@inproceedings{vanhattum2022verifying, + title={Verifying dynamic trait objects in {R}ust}, + author={VanHattum, Alexa and Schwartz-Narbonne, Daniel and Chong, Nathan and Sampson, Adrian}, + booktitle={Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice}, + pages={321--330}, + year={2022} +} + +@manual{superPower, + title = {Unsafe Rust}, + url = {https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html}, + author = {Rust Documentation} +} + +@inproceedings{li2021mirchecker, + title={MirChecker: detecting bugs in {R}ust programs via static analysis}, + author={Li, Zhuohua and Wang, Jincheng and Sun, Mingshen and Lui, John CS}, + booktitle={Proceedings of the 2021 ACM SIGSAC conference on computer and communications security}, + pages={2183--2196}, + year={2021} +} + +@manual{stringChallenge, + title = {Memory Safety of String}, + year = {2024}, + author = {Zyad Hassan}, + url = {https://model-checking.github.io/verify-rust-std/challenges/0010-string.html} +} + +@manual{anderson20medium, + title = {The Rust Compilation Model Calamity}, + year = {2020}, + url = {https://pingcap.medium.com/the-rust-compilation-model-calamity-1a8ce781cf6cb}, + author = {Brian Anderson} +} + +@article{matsakis2014rust, + title={The rust language}, + author={Matsakis, Nicholas D and Klock, Felix S}, + journal={ACM SIGAda Ada Letters}, + volume={34}, + number={3}, + pages={103--104}, + year={2014}, + publisher={ACM New York, NY, USA} +} + +@manual{challenge, + title = {Memory Safety of String}, + url = {https://github.com/model-checking/verify-rust-std/issues/61}, + author = {Zyad Hassan}, + year = {2024} +} + +@manual{solution, + title = {char and ascii{\_}char contracts}, + url = {https://github.com/model-checking/verify-rust-std/pull/48}, + year = {2024}, + author = {Carolyn Zech} +} + +@manual{rustAndroid, + title = {The Impact of Rust on Security Development}, + year = {2024}, + url = {https://www.riscure.com/the-impact-of-rust-on-security-development}, + author = {Christiaan Biesterbosch and Valeria Vatolina} +} +@manual{liam2022android, + title = {How Google is using Rust to reduce memory safety vulnerabilities in Android}, + year = {2020}, + url = {https://www.zdnet.com/article/google-after-using-rust-we-slashed-android-memory-safety-vulnerabilities/}, + author = {Liam Tung} +} + +@article{jung2017rustbelt, + title={RustBelt: Securing the foundations of the Rust programming language}, + author={Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek}, + journal={Proceedings of the ACM on Programming Languages}, + volume={2}, + number={POPL}, + pages={1--34}, + year={2017}, + publisher={ACM New York, NY, USA} +} + +@article{ayoun2024hybrid, + title={A hybrid approach to semi-automated Rust verification}, + author={Ayoun, Sacha-{\'E}lie and Denis, Xavier and Maksimovi{\'c}, Petar and Gardner, Philippa}, + journal={arXiv preprint arXiv:2403.15122}, + year={2024} +} + +@article{ho2022aeneas, + title={Aeneas: Rust verification by functional translation}, + author={Ho, Son and Protzenko, Jonathan}, + journal={Proceedings of the ACM on Programming Languages}, + volume={6}, + number={ICFP}, + pages={711--741}, + year={2022}, + publisher={ACM New York, NY, USA} +} + +\end{thebibliography} \ No newline at end of file diff --git a/papers/vstte2024/paper.tex b/papers/vstte2024/paper.tex new file mode 100644 index 000000000000..a523bbf1de5b --- /dev/null +++ b/papers/vstte2024/paper.tex @@ -0,0 +1,172 @@ +% Copyright Kani Contributors +% SPDX-License-Identifier: Apache-2.0 OR MIT + +\documentclass[runningheads]{llncs} +% +\usepackage[T1]{fontenc} +\usepackage{graphicx} +\usepackage{amsmath,amsfonts} +\usepackage{hyperref} +\usepackage{listings} +\usepackage{xcolor} +\usepackage{color} +\usepackage{listings} +\definecolor{GrayCodeBlock}{RGB}{241,241,241} +\definecolor{BlackText}{RGB}{110,107,94} +\definecolor{RedTypename}{RGB}{182,86,17} +\definecolor{GreenString}{RGB}{96,172,57} +\definecolor{PurpleKeyword}{RGB}{184,84,212} +\definecolor{GrayComment}{RGB}{170,170,170} +\definecolor{GoldDocumentation}{RGB}{180,165,45} +\lstdefinelanguage{rust} +{ + columns=fullflexible, + keepspaces=true, + frame=single, + framesep=0pt, + framerule=0pt, + framexleftmargin=4pt, + framexrightmargin=4pt, + framextopmargin=5pt, + framexbottommargin=3pt, + xleftmargin=4pt, + xrightmargin=4pt, + backgroundcolor=\color{GrayCodeBlock}, + basicstyle=\ttfamily\color{BlackText}, + keywords={ + true,false, + unsafe,async,await,move, + use,pub,crate,super,self,mod, + struct,enum,fn,const,static,let,mut,ref,type,impl,dyn,trait,where,as, + break,continue,if,else,while,for,loop,match,return,yield,in + }, + keywordstyle=\color{PurpleKeyword}, + ndkeywords={ + bool,u8,u16,u32,u64,u128,i8,i16,i32,i64,i128,char,str, + Self,Option,Some,None,Result,Ok,Err,String,Box,Vec,Rc,Arc,Cell,RefCell,HashMap,BTreeMap, + macro_rules + }, + ndkeywordstyle=\color{RedTypename}, + comment=[l][\color{GrayComment}\slshape]{//}, + morecomment=[s][\color{GrayComment}\slshape]{/*}{*/}, + morecomment=[l][\color{GoldDocumentation}\slshape]{///}, + morecomment=[s][\color{GoldDocumentation}\slshape]{/*!}{*/}, + morecomment=[l][\color{GoldDocumentation}\slshape]{//!}, + morecomment=[s][\color{RedTypename}]{\#![}{]}, + morecomment=[s][\color{RedTypename}]{\#[}{]}, + stringstyle=\color{GreenString}, + string=[b]" +} + +\begin{document} +% +\title{Verifying the Rust Standard Library} +%\titlerunning{Verifying the Rust} + +\author{ +Rahul Kumar \and +Celina Val \and +Felipe Monteiro \and +Michael Tautschnig \and +Zyad Hassan \and +Qinheping Hu \and +Adrian Palacios \and +Remi Delmas \and +Jaisurya Nanduri \and +Felix Klock \and +Justus Adam \and +Carolyn Zech \and +Artem Agvanian +} +% +\authorrunning{R. Kumar et al.} + +\institute{Amazon Web Services, USA\\ \url{https://aws.amazon.com/} +} + +\maketitle + +\begin{abstract} +The Rust programming language is growing fast and seeing increased adoption due to performance and speed-of-development benefits. It provides strong compile-time guarantees along with blazing performance and an active community of support. The Rust language has experienced steady growth in the last few years with a total developer size of close to 3M developers. Several large projects such as Servo, TiKV, and the Rust compiler itself are in the millions of lines of code. Although Rust provides strong safety guarantees for \texttt{safe} code, the story with \texttt{unsafe} code is incomplete. In this short paper, we motivate the case for verifying the Rust standard library and how we are approaching this endeavor. We describe our effort to verify the Rust standard library via a crowd-sourced verification effort, wherein verifying the Rust standard library is specified as a set of challenges open to all. + +\keywords{Rust \and standard library \and verification \and formal methods \and safe +\and unsafe \and memory safety \and correctness \and challenge} +\end{abstract} + +\section{Rust} + +Rust~\cite{matsakis2014rust} is a modern programming language designed to enable developers to efficiently create high performance reliable systems. Rust delivers high performance because it does not use a garbage collector. Combined with a powerful type system that enforces ownership of memory wherein memory can be shared or mutable, but never both. This helps avoid data-races and memory errors, thereby reducing the trade-off between high-level safety guarantees and low-level controls -- a highly desired property of programming languages. Unlike C/C++, the Rust language aims to minimize undefined behavior statically by employing a strong type system and an \textit{extensible} ownership model for memory. + +The extensible model of ownership relies on the simple (yet difficult) principle of enforcing that an object can be accessed by multiple aliases/references only for read purposes. To write to an object, there can only be one reference to it at any given time. Such a principle in practice eliminates significant amounts of memory-related errors~\cite{rustAndroid}. In spite of the great benefits in practice, this principle tends to be restrictive for a certain subset of implementations that are too low-level or require very specific types of synchronization. As a result, the Rust language introduced the \texttt{unsafe} keyword. When used, the compiler may not be able to prove the memory safety rules that are enforced on \texttt{safe} code blocks. Alias tracking is not performed for raw pointers which can only be used in \texttt{unsafe} code blocks, which enables developers to perform actions that would be rejected by the compiler in \texttt{safe} code blocks. This is also referred to as \textit{superpowers}~\cite{superPower} of \texttt{unsafe} code blocks. Examples of these superpowers include dereferencing a raw pointer, calling an unsafe function or method, and accessing fields of unions etc. A clear side-effect of this choice is that most if not all memory related errors in the code are due to the \texttt{unsafe} code blocks introduced by the developer. + +Rust developers use \textit{encapsulation} as a common design pattern to mask unsafe code blocks. The safe abstractions allow \texttt{unsafe} code blocks to be limited in number and not leak into all parts of the codebase. The Rust standard library itself has widespread use of \texttt{unsafe} code blocks, with almost 5.5K \texttt{unsafe} functions and 4.8K \texttt{unsafe} code blocks. In the last 3 years, 40 soundness issues have been filed in the Rust standard library along with 17 reported CVEs, even with the extensive testing and usage of the library. The onus of proving the safety and correctness of these \texttt{unsafe} code blocks is on the developers. Some such efforts have been made, but there is still a lot of ground to cover~\cite{jung2017rustbelt}. + +Verifying the Rust standard library is important and rewarding along multiple dimensions such as improving Rust, creating better verification tools, and enabling a safer ecosystem. Given the size and scope of this exercise, we believe doing this in isolation would be expensive and counter-productive. Ergo, we believe that motivating the community and creating a unified crowd-sourced effort is the desirable method, which we hope to catalyze via our proposed effort. + + +\section{Rust Verification Landscape} + +A common misconception Rust developers have is that they are producing \texttt{safe} memory-safe code by simply using Rust as their development language. To counter this, there have been significant efforts to create tools and techniques that enable verification of Rust code. Here we list (alphabetically) some tools: + +\begin{itemize} + + \item \textbf{Creusot}~\cite{denis2022creusot} is a Rust verifier that also employs deductive-style verification for \texttt{safe} Rust code. Creusot also introduces \textbf{Pearlite} - a specification language for specifying function and loop contracts. + + \item \textbf{Gillian-Rust}~\cite{ayoun2024hybrid} is a separation logic based hybrid verification tool for Rust programs with support for \texttt{unsafe} code. Gillian-Rust is also linked to Creusot, but does in certain cases require manual intervention. + + \item \textbf{Kani}~\cite{vanhattum2022verifying} uses bounded model checking to verify generic memory safety properties and user specified assertions. Kani supports both \texttt{unsafe} and \texttt{safe} code, but cannot guarantee unbounded verification in all cases. + + \item \textbf{Prusti}~\cite{astrauskas2022prusti} employs deductive verification to prove functional correctness of \texttt{safe} Rust code. Specifically, it targets certain type of \textit{panics} and allows users to specify properties of interest. + + \item \textbf{Verus}~\cite{verus-sys} is an SMT-based tool used to verify Rust code and can support \texttt{unsafe} in certain situations such as the use of raw pointers and unsafe cells. + + \item There are several other tools which are in the related space, but we do not list them here explicitly. +\end{itemize} + +\section{Verifying the Rust Standard Library} + +We are proposing the creation of a crowd-sourced verification effort, wherein verifying the Rust standard library is specified as a set of challenges. Each challenge describes the goal and the success criteria. Currently, we are focusing on doing verification for memory-safety. The challenges are open to anyone. This effort aims to be \textit{tool agnostic} to facilitate the introduction of verification solutions into the Rust mainline and making verification an integral part of the Rust ecosystem. Towards this, we have been working with the Rust language team to introduce function and loop contracts into the Rust mainline and have created a fork of the Rust standard library repository \url{https://github.com/model-checking/verify-rust-std/} wherein all solutions to challenges and verification artifacts are stored. Challenges can come in various flavors: 1/ specifying contracts for a part of the Rust standard library, 2/ specify and verify a part of the Rust standard library, and 3/ introduce new tools/techniques to verify parts of the Rust standard library. The repository provides templates for introducing new challenges, new tools, and instructions on how to submit solutions to challenges. To date, we have over 20 students, academics, and researchers engaging. + +As part of this effort, we are also creating challenges. For example, we have created a challenge to verify the String library in the standard library~\cite{stringChallenge}. In this challenge, the goal is to verify the memory safety of \texttt{std::string::String} and prove the absence of undefined behavior (UB). Even though the majority of \texttt{String} methods are safe, many of them are safe abstractions over unsafe code. For instance, the insert method is implemented as follows : +\begin{lstlisting}[language=rust, caption=Unsafe usage in String, frame=single, numbers=left] + pub fn insert(&mut self, idx: usize, ch: char) { + assert!(self.is_char_boundary(idx)); + let mut bits = [0; 4]; + let bits = ch.encode_utf8(&mut bits).as_bytes(); + + unsafe { + self.insert_bytes(idx, bits); + } + } +\end{lstlisting} + +The goal also specifies the \textit{success criteria} that must be met for the solution to be reviewed and merged into the CI pipeline. +\begin{lstlisting}[caption=Success criteria for the String challenge.,frame=single] +Verify the memory safety of all public functions that are +safe abstractions over unsafe code: + unbounded: from_utf16le, from_utf16le_lossy, + from_utf16be, from_utf16be_lossy, + remove_matches, insert_str, + split_off, replace_range, retain + others: pop, remove, insert, drain, leak, + into_boxed_str +Ones marked as unbounded must be verified for any +string/slice length. +\end{lstlisting} + +Example of a solution for a challenge can be found in~\cite{solution}. This particular solution introduces new contracts for \texttt{char} and \texttt{ascii\_char}. The contracts are also verified using Kani. + +\noindent \textbf{Our call to action} to you is to come and be a part of this effort and contribute by solving challenges, introducing new challenges, introducing new tools, or helping review and refine the current processes! + +\begin{credits} +\subsubsection{\ackname} We would like to thank all the academic partners that have helped us shape challenges, started contributing to challenges, and provide invaluable advice throughout the process of jump starting this initiative. We also would like to thank Niko Matsakis, Byron Cook, and Kurt Kufeld for their support and leadership. +\end{credits} + +% +% Bibliography +% +\bibliographystyle{splncs04} +\bibliography{paper} + + +\end{document} diff --git a/scripts/ci/copyright_check.py b/scripts/ci/copyright_check.py index 3b07fb56da58..64fd92d06712 100755 --- a/scripts/ci/copyright_check.py +++ b/scripts/ci/copyright_check.py @@ -8,15 +8,15 @@ from itertools import chain -COMMENT_OR_EMPTY_PATTERN = '^(//.*$|#.*$|\\s*$)' +COMMENT_OR_EMPTY_PATTERN = '^(//.*$|#.*$|%.*$|\\s*$)' -STANDARD_HEADER_PATTERN_1 = '(//|#) Copyright Kani Contributors' -STANDARD_HEADER_PATTERN_2 = '(//|#) SPDX-License-Identifier: Apache-2.0 OR MIT' +STANDARD_HEADER_PATTERN_1 = '(//|#|%) Copyright Kani Contributors' +STANDARD_HEADER_PATTERN_2 = '(//|#|%) SPDX-License-Identifier: Apache-2.0 OR MIT' -MODIFIED_HEADER_PATTERN_1 = '(//|#) SPDX-License-Identifier: Apache-2.0 OR MIT' +MODIFIED_HEADER_PATTERN_1 = '(//|#|%) SPDX-License-Identifier: Apache-2.0 OR MIT' MODIFIED_HEADER_PATTERN_2 = COMMENT_OR_EMPTY_PATTERN -MODIFIED_HEADER_PATTERN_3 = '(//|#) Modifications Copyright Kani Contributors' -MODIFIED_HEADER_PATTERN_4 = '(//|#) See GitHub history for details.' +MODIFIED_HEADER_PATTERN_3 = '(//|#|%) Modifications Copyright Kani Contributors' +MODIFIED_HEADER_PATTERN_4 = '(//|#|%) See GitHub history for details.' class CheckResult(Enum): FAIL = 1 From 33e3c361d8b0ba404e51e7a119edabad41b1e86b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 4 Sep 2024 14:44:42 -0400 Subject: [PATCH 05/21] Fix contract expansion for `old` (#3491) Fixes the macro expansion for contracts to properly place history expressions. ## Problem Before this PR, instantiations of "remembers variables" (i.e., the variables that save the value before the function executes) were always put *above* any statements from previous macro expansions. For example, for this code (from #3359): ```rust #[kani::requires(val < i32::MAX)] #[kani::ensures(|result| *result == old(val + 1))] pub fn next(mut val: i32) -> i32 { val + 1 } ``` Kani would first expand the `requires` attribute and insert `kani::assume(val < i32::MAX)`. The expansion of `ensures` would then put the remembers variables first, generating this: ``` let remember_kani_internal_1e725538cd5566b8 = val + 1; kani::assume(val < i32::MAX); ``` which causes an integer overflow because we don't restrict the value of `val` before adding 1. Instead, we want: ``` kani::assume(val < i32::MAX); let remember_kani_internal_1e725538cd5566b8 = val + 1; ``` ## Solution The solution is to insert the remembers variables immediately after preconditions--that way, they respect the preconditions but are still declared before the function under contract executes. When we're expanding an `ensures` clause, we iterate through each of the already-generated statements, find the position where the preconditions end, then insert the remembers variables there. For instance: ``` kani::assume(x < 100); kani::assume(y < 10); kani::assume(x + y < 105); <-- remembers variables go here --> let _wrapper_arg = ... ``` --- Resolves #3359 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../src/sysroot/contracts/check.rs | 11 ++-- .../src/sysroot/contracts/helpers.rs | 53 ++++++++++++++++++- .../kani_macros/src/sysroot/contracts/mod.rs | 7 +++ .../src/sysroot/contracts/replace.rs | 8 ++- .../ensures_before_requires.expected | 5 ++ .../ensures_before_requires.rs | 18 +++++++ .../respects-preconditions/modifies.expected | 5 ++ .../respects-preconditions/modifies.rs | 29 ++++++++++ .../requires_before_ensures.expected | 5 ++ .../requires_before_ensures.rs | 17 ++++++ 10 files changed, 152 insertions(+), 6 deletions(-) create mode 100644 tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.expected create mode 100644 tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.rs create mode 100644 tests/expected/function-contract/history/respects-preconditions/modifies.expected create mode 100644 tests/expected/function-contract/history/respects-preconditions/modifies.rs create mode 100644 tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.expected create mode 100644 tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.rs diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 69f280ad9335..314a5e74bc98 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -9,8 +9,8 @@ use std::mem; use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt}; use super::{ - helpers::*, shared::build_ensures, ContractConditionsData, ContractConditionsHandler, - INTERNAL_RESULT_IDENT, + helpers::*, shared::build_ensures, ClosureType, ContractConditionsData, + ContractConditionsHandler, INTERNAL_RESULT_IDENT, }; const WRAPPER_ARG: &str = "_wrapper_arg"; @@ -38,9 +38,14 @@ impl<'a> ContractConditionsHandler<'a> { ); let return_expr = body_stmts.pop(); + + let (assumes, rest_of_body) = + split_for_remembers(&body_stmts[..], ClosureType::Check); + quote!({ + #(#assumes)* #remembers - #(#body_stmts)* + #(#rest_of_body)* #exec_postconditions #return_expr }) diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index 410c2d971c44..8db6218e2693 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -4,10 +4,14 @@ //! Functions that operate third party data structures with no logic that is //! specific to Kani and contracts. +use crate::attr_impl::contracts::ClosureType; use proc_macro2::{Ident, Span}; use std::borrow::Cow; use syn::spanned::Spanned; -use syn::{parse_quote, Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt}; +use syn::{ + parse_quote, Attribute, Expr, ExprBlock, ExprCall, ExprPath, Local, LocalInit, PatIdent, Path, + Stmt, +}; /// If an explicit return type was provided it is returned, otherwise `()`. pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { @@ -169,6 +173,53 @@ pub fn chunks_by<'a, T, C: Default + Extend>( }) } +/// Splits `stmts` into (preconditions, rest). +/// For example, ClosureType::Check assumes preconditions, so given this sequence of statements: +/// ```ignore +/// kani::assume(.. precondition_1); +/// kani::assume(.. precondition_2); +/// let _wrapper_arg = (ptr as * const _,); +/// ... +/// ``` +/// This function would return the two kani::assume statements in the former slice +/// and the remaining statements in the latter. +/// The flow for ClosureType::Replace is the same, except preconditions are asserted rather than assumed. +/// +/// The caller can use the returned tuple to insert remembers statements after `preconditions` and before `rest`. +/// Inserting the remembers statements after `preconditions` ensures that they are bound by the preconditions. +/// To understand why this is important, take the following example: +/// ```ignore +/// #[kani::requires(x < u32::MAX)] +/// #[kani::ensures(|result| old(x + 1) == *result)] +/// fn add_one(x: u32) -> u32 {...} +/// ``` +/// If the `old(x + 1)` statement didn't respect the precondition's upper bound on `x`, Kani would encounter an integer overflow. +/// +/// Inserting the remembers statements before `rest` ensures that they are declared before the original function executes, +/// so that they will store historical, pre-computation values as intended. +pub fn split_for_remembers(stmts: &[Stmt], closure_type: ClosureType) -> (&[Stmt], &[Stmt]) { + let mut pos = 0; + + let check_str = match closure_type { + ClosureType::Check => "assume", + ClosureType::Replace => "assert", + }; + + for stmt in stmts { + if let Stmt::Expr(Expr::Call(ExprCall { func, .. }), _) = stmt { + if let Expr::Path(ExprPath { path: Path { segments, .. }, .. }) = func.as_ref() { + let first_two_idents = + segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::>(); + + if first_two_idents == vec!["kani", check_str] { + pos += 1; + } + } + } + } + stmts.split_at(pos) +} + macro_rules! assert_spanned_err { ($condition:expr, $span_source:expr, $msg:expr, $($args:expr),+) => { if !$condition { diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index db5f30131405..281960bf041b 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -514,6 +514,13 @@ enum ContractConditionsData { }, } +/// Which function are we currently generating? +#[derive(Copy, Clone, Eq, PartialEq)] +enum ClosureType { + Check, + Replace, +} + impl<'a> ContractConditionsHandler<'a> { /// Handle the contract state and return the generated code fn dispatch_on(mut self, state: ContractFunctionState) -> TokenStream2 { diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 02ac4a772348..71913e630622 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -11,7 +11,7 @@ use syn::Stmt; use super::{ helpers::*, shared::{build_ensures, try_as_result_assign}, - ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, + ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, }; impl<'a> ContractConditionsHandler<'a> { @@ -84,9 +84,13 @@ impl<'a> ContractConditionsHandler<'a> { ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + + let (asserts, rest_of_before) = split_for_remembers(before, ClosureType::Replace); + quote!({ + #(#asserts)* #remembers - #(#before)* + #(#rest_of_before)* #(#after)* kani::assume(#ensures_clause); #result diff --git a/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.expected b/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.expected new file mode 100644 index 000000000000..a9e6a1a6a601 --- /dev/null +++ b/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.expected @@ -0,0 +1,5 @@ +next\ + - Status: SUCCESS\ + - Description: "attempt to add with overflow" + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.rs b/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.rs new file mode 100644 index 000000000000..380da8898e71 --- /dev/null +++ b/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Demonstrate that when the ensures contract is before the requires contract, +// the history expression respects the upper bound on x, so x + 1 doesn't overflow +// This example is taken from https://github.com/model-checking/kani/issues/3359 + +#[kani::ensures(|result| *result == old(val + 1))] +#[kani::requires(val < i32::MAX)] +pub fn next(val: i32) -> i32 { + val + 1 +} + +#[kani::proof_for_contract(next)] +pub fn check_next() { + let _ = next(kani::any()); +} diff --git a/tests/expected/function-contract/history/respects-preconditions/modifies.expected b/tests/expected/function-contract/history/respects-preconditions/modifies.expected new file mode 100644 index 000000000000..40dd76d9ce4d --- /dev/null +++ b/tests/expected/function-contract/history/respects-preconditions/modifies.expected @@ -0,0 +1,5 @@ +modify\ + - Status: SUCCESS\ + - Description: "attempt to add with overflow" + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/history/respects-preconditions/modifies.rs b/tests/expected/function-contract/history/respects-preconditions/modifies.rs new file mode 100644 index 000000000000..b20b8396e3d6 --- /dev/null +++ b/tests/expected/function-contract/history/respects-preconditions/modifies.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Demonstrate the the history expression respects preconditions +// with multiple interleaved preconditions, modifies contracts, and history expressions + +#[derive(kani::Arbitrary)] +struct Point { + x: X, + y: Y, +} + +#[kani::requires(ptr.x < 100)] +#[kani::ensures(|result| old(ptr.x + 1) == ptr.x)] +#[kani::modifies(&mut ptr.x)] +#[kani::ensures(|result| old(ptr.y - 1) == ptr.y)] +#[kani::modifies(&mut ptr.y)] +#[kani::requires(ptr.y > 0)] +fn modify(ptr: &mut Point) { + ptr.x += 1; + ptr.y -= 1; +} + +#[kani::proof_for_contract(modify)] +fn main() { + let mut p: Point = kani::any(); + modify(&mut p); +} diff --git a/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.expected b/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.expected new file mode 100644 index 000000000000..a9e6a1a6a601 --- /dev/null +++ b/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.expected @@ -0,0 +1,5 @@ +next\ + - Status: SUCCESS\ + - Description: "attempt to add with overflow" + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.rs b/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.rs new file mode 100644 index 000000000000..4f8f6871f8f9 --- /dev/null +++ b/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Demonstrate that when the requires contract is before the ensures contract, the history expression respects the upper bound on x, so x + 1 doesn't overflow +// This example is taken from https://github.com/model-checking/kani/issues/3359 + +#[kani::requires(val < i32::MAX)] +#[kani::ensures(|result| *result == old(val + 1))] +pub fn next(val: i32) -> i32 { + val + 1 +} + +#[kani::proof_for_contract(next)] +pub fn check_next() { + let _ = next(kani::any()); +} From 603f9bf6c86aa3956acd0f686ea7ac094362360e Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Wed, 4 Sep 2024 13:00:01 -0700 Subject: [PATCH 06/21] Bump Kani version to 0.55.0 (#3486) These are the auto-generated release notes: ## What's Changed * Update CBMC build instructions for Amazon Linux 2 by @tautschnig in https://github.com/model-checking/kani/pull/3431 * Handle intrinsics systematically by @artemagvanian in https://github.com/model-checking/kani/pull/3422 * Bump tests/perf/s2n-quic from `445f73b` to `ab9723a` by @dependabot in https://github.com/model-checking/kani/pull/3434 * Automatic cargo update to 2024-08-12 by @github-actions in https://github.com/model-checking/kani/pull/3433 * Actually apply CBMC patch by @tautschnig in https://github.com/model-checking/kani/pull/3436 * Update features/verify-rust-std branch by @feliperodri in https://github.com/model-checking/kani/pull/3435 * Add test related to issue 3432 by @celinval in https://github.com/model-checking/kani/pull/3439 * Implement memory initialization state copy functionality by @artemagvanian in https://github.com/model-checking/kani/pull/3350 * Bump tests/perf/s2n-quic from `ab9723a` to `80b93a7` by @dependabot in https://github.com/model-checking/kani/pull/3453 * Make points-to analysis handle all intrinsics explicitly by @artemagvanian in https://github.com/model-checking/kani/pull/3452 * Automatic cargo update to 2024-08-19 by @github-actions in https://github.com/model-checking/kani/pull/3450 * Add loop scanner to tool-scanner by @qinheping in https://github.com/model-checking/kani/pull/3443 * Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in https://github.com/model-checking/kani/pull/3438 * Re-enabled hierarchical logs in the compiler by @celinval in https://github.com/model-checking/kani/pull/3449 * Fix ICE due to mishandling of Aggregate rvalue for raw pointers to `str` by @celinval in https://github.com/model-checking/kani/pull/3448 * Automatic cargo update to 2024-08-26 by @github-actions in https://github.com/model-checking/kani/pull/3459 * Bump tests/perf/s2n-quic from `80b93a7` to `8f7c04b` by @dependabot in https://github.com/model-checking/kani/pull/3460 * Update deny action by @zhassan-aws in https://github.com/model-checking/kani/pull/3461 * Basic support for memory initialization checks for unions by @artemagvanian in https://github.com/model-checking/kani/pull/3444 * Adjust test patterns so as not to check for trivial properties by @tautschnig in https://github.com/model-checking/kani/pull/3464 * Clarify comment in RFC Template by @carolynzech in https://github.com/model-checking/kani/pull/3462 * RFC: Source-based code coverage by @adpaco-aws in https://github.com/model-checking/kani/pull/3143 * Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in https://github.com/model-checking/kani/pull/3119 * Upgrade toolchain to 08/28 by @jaisnan in https://github.com/model-checking/kani/pull/3454 * Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3419 * Upgrade Toolchain to 8/29 by @carolynzech in https://github.com/model-checking/kani/pull/3468 * Automatic toolchain upgrade to nightly-2024-08-30 by @github-actions in https://github.com/model-checking/kani/pull/3469 * Extend name resolution to support qualified paths (Partial Fix) by @celinval in https://github.com/model-checking/kani/pull/3457 * Partially integrate uninit memory checks into `verify_std` by @artemagvanian in https://github.com/model-checking/kani/pull/3470 * Update Toolchain to 9/1 by @carolynzech in https://github.com/model-checking/kani/pull/3478 * Automatic cargo update to 2024-09-02 by @github-actions in https://github.com/model-checking/kani/pull/3480 * Bump tests/perf/s2n-quic from `8f7c04b` to `1ff3a9c` by @dependabot in https://github.com/model-checking/kani/pull/3481 * Automatic toolchain upgrade to nightly-2024-09-02 by @github-actions in https://github.com/model-checking/kani/pull/3479 * Automatic toolchain upgrade to nightly-2024-09-03 by @github-actions in https://github.com/model-checking/kani/pull/3482 * RFC for List Subcommand by @carolynzech in https://github.com/model-checking/kani/pull/3463 * Add tests for fixed issues. by @carolynzech in https://github.com/model-checking/kani/pull/3484 **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.54.0...kani-0.55.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- CHANGELOG.md | 22 ++++++++++++++++++++++ Cargo.lock | 20 ++++++++++---------- Cargo.toml | 2 +- cprover_bindings/Cargo.toml | 2 +- kani-compiler/Cargo.toml | 2 +- kani-driver/Cargo.toml | 2 +- kani_metadata/Cargo.toml | 2 +- library/kani/Cargo.toml | 2 +- library/kani_core/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 12 files changed, 42 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d36def1a45f1..e35af4c8fa24 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,28 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. +## [0.55.0] + +### Major/Breaking Changes +* Coverage reporting in Kani is now source-based instead of line-based. +Consequently, the unstable `-Zline-coverage` flag has been replaced with a `-Zsource-coverage` one. +Check the [Source-Coverage RFC](https://model-checking.github.io/kani/rfc/rfcs/0011-source-coverage.html) for more details. +* Several improvements were made to the memory initialization checks. The current state is summarized in https://github.com/model-checking/kani/issues/3300. We welcome your feedback! + +### What's Changed +* Update CBMC build instructions for Amazon Linux 2 by @tautschnig in https://github.com/model-checking/kani/pull/3431 +* Implement memory initialization state copy functionality by @artemagvanian in https://github.com/model-checking/kani/pull/3350 +* Make points-to analysis handle all intrinsics explicitly by @artemagvanian in https://github.com/model-checking/kani/pull/3452 +* Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in https://github.com/model-checking/kani/pull/3438 +* Fix ICE due to mishandling of Aggregate rvalue for raw pointers to `str` by @celinval in https://github.com/model-checking/kani/pull/3448 +* Basic support for memory initialization checks for unions by @artemagvanian in https://github.com/model-checking/kani/pull/3444 +* Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in https://github.com/model-checking/kani/pull/3119 +* Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3419 +* Partially integrate uninit memory checks into `verify_std` by @artemagvanian in https://github.com/model-checking/kani/pull/3470 +* Rust toolchain upgraded to `nightly-2024-09-03` by @jaisnan @carolynzech + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.54.0...kani-0.55.0 + ## [0.54.0] ### Major Changes diff --git a/Cargo.lock b/Cargo.lock index c180c66dde90..1c371b85fba9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -93,7 +93,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" [[package]] name = "build-kani" -version = "0.54.0" +version = "0.55.0" dependencies = [ "anyhow", "cargo_metadata", @@ -235,7 +235,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.54.0" +version = "0.55.0" dependencies = [ "lazy_static", "linear-map", @@ -459,7 +459,7 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "kani" -version = "0.54.0" +version = "0.55.0" dependencies = [ "kani_core", "kani_macros", @@ -467,7 +467,7 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.54.0" +version = "0.55.0" dependencies = [ "clap", "cprover_bindings", @@ -491,7 +491,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.54.0" +version = "0.55.0" dependencies = [ "anyhow", "cargo_metadata", @@ -520,7 +520,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.54.0" +version = "0.55.0" dependencies = [ "anyhow", "home", @@ -529,14 +529,14 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.54.0" +version = "0.55.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.54.0" +version = "0.55.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -546,7 +546,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.54.0" +version = "0.55.0" dependencies = [ "clap", "cprover_bindings", @@ -1098,7 +1098,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" [[package]] name = "std" -version = "0.54.0" +version = "0.55.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index 149b8d2c93c8..ee9848b578dc 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.54.0" +version = "0.55.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index b0e3c578bbcf..008c81aef2ad 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.54.0" +version = "0.55.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index e8e564f9616a..9ca8d10f5275 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.54.0" +version = "0.55.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 27fef66ffb65..7485d2279ad6 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.54.0" +version = "0.55.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index efa28288d148..18eadc4095ed 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.54.0" +version = "0.55.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index a3692f95e3f5..fa50783516f4 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.54.0" +version = "0.55.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index 9df828e77c5a..447cd0b3f298 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.54.0" +version = "0.55.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 574960e5fc0a..a6b20a68bc39 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.54.0" +version = "0.55.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 9f0d09b0d7bb..12c923e9b655 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.54.0" +version = "0.55.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index cd2985e4ad68..41095f1d7c3c 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.54.0" +version = "0.55.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" From 701f6fb8e26acf0c31f053cc1503a4139b277e29 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 4 Sep 2024 16:54:24 -0500 Subject: [PATCH 07/21] RFC: Loop Contracts (#3167) RFC for loop contracts in Kani. Rendered version available [here](https://github.com/qinheping/kani/blob/rfc-loop-contracts/rfc/src/rfcs/0012-loop-contracts.md). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val --- rfc/src/rfcs/0012-loop-contracts.md | 255 ++++++++++++++++++++++++++++ 1 file changed, 255 insertions(+) create mode 100644 rfc/src/rfcs/0012-loop-contracts.md diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md new file mode 100644 index 000000000000..1c0bcdafd750 --- /dev/null +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -0,0 +1,255 @@ +- **Feature Name:** Loop Contracts +- **Feature Request Issue:** [#3168](https://github.com/model-checking/kani/issues/3168) +- **RFC PR:** [#3167](https://github.com/model-checking/kani/pull/3167) +- **Status:** Under Review +- **Version:** 1 +- **Proof-of-concept:** + +------------------- + +## Summary + +Loop contracts provide way to safely abstract loops of a program, typically +in order to accelerate the verification process, and remove the loop unwinding +bounds. The key idea is to over-approximate the possible set of program states, +while still being precise enough to be able to prove the desired property. + +## User Impact + +Loop contracts provide an interface for a verified, sound abstraction. +The goal for specifying loop contracts in the source code is two fold: + +* Unbounded verification: Currently, proving correctness + (i.e. assertions never fail) on programs with unbounded control flow (e.g. + loops with dynamic bounds) Kani requires unwinding loops for a large number of + times, which is not always feasible. Loop contracts provide a way to abstract + out loops, and hence remove the need for unwinding loops. +* Faster CI runs: In most cases, the provided contracts would also significantly + improve Kani's verification time since all loops would be unrolled only to + a single iteration. + + + +Loop contracts are completely optional with no user impact if unused. This +RFC proposes the addition of new attributes, and functions, that shouldn't +interfere with existing functionalities. + + +## User Experience + +A loop contract specifies the behavior of a loop as a boolean predicate +(loop invariants clauses) with certain frames conditions (loop modifies clauses) +that can be checked against the loop implementation, and used to abstract out +the loop in the verification process. + +We illustrate the usage of loop contracts with an example. +Consider the following program: +```rs +fn simple_loop() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + while x > 1{ + x = x - 1; + }; + + assert!(x == 1); +} +``` +The loop in the `simple_loop` function keep subtracting 1 from `x` until `x` is 1. +However, Kani currently needs to unroll the loop for `u64::MAX` number of times +to verify the assertion at the end of the program. + +With loop contracts, the user can specify the behavior of the loop as follows: +```rs +fn simple_loop_with_loop_contracts() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + #[kani::loop_invariant(x >= 1)] + while x > 1{ + x = x - 1; + }; + + assert!(x == 1); +} +``` +The loop invariant clause `#[kani::loop_invariant(x >= 1)]` specifies the loop +invariants that must hold at the beginning of each iteration of the loop right before +checking the loop guard. + +In this case, Kani verifies that the loop invariant `x >= 1` is inductive, i.e., +`x` is always greater than or equal to 1 at each iteration before checking `x > 1`. + + +Also, once Kani proved that the loop invariant is inductive, it can safely use the loop +invariants to abstract the loop out of the verification process. +The idea is, instead of exploring all possible branches of the loop, Kani only needs to +prove those branches reached from an arbitrary program state that satisfies the loop contracts, +after the execution of one iteration of the loop. + +So, for loops without break statements, we can assume all post-states of the loop satisfying +`inv && !loop_guard` for proving post-loops properties. +The requirement of satisfying the negation of the loop guard comes from the fact that a path +exits loops without break statements must fail the loop guard. + +For example, applying loop contracts in `simple_loop` function is equivalent to the following: +```rs +fn simple_loop_transformed() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + x = kani::any(); // Arbitrary program state that + kani::assume( !(x > 1) && x >= 1); // satisfies !`guard` && `inv` + + assert!(x == 1); +} +``` +The assumption above is actually equivalent to `x == 1`, hence the assertion at the end +of the program is proved. + +### Write Sets and Havocking + +For those memory locations that are not modified in the loop, loop invariants state +that they stay unchanged throughout the loop are inductive. In other words, Kani should +only havoc the memory locations that are modified in the loop. This is achieved by +specifying the `modifies` clause for the loop. For example, the following program: +```rs +fn simple_loop_two_vars() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + let mut y: u64 = 1; + + #[kani::loop_invariant(x >= 1)] + #[kani::loop_modifies(x)] + while x > 1{ + x = x - 1; + }; + + assert!(x == 1); + assert!(y == 1); +} +``` +write to only `x` in the loop, hence the `modifies` clause contains only `x`. +Then when use the loop contracts to abstract the loop, Kani will only havoc the memory +location `x` and keep `y` unchanged. Note that if the `modifies` clause contains also +`y`, Kani will havoc both `x` and `y`, and hence violate the assertion `y == 1`. + +Kani can employs CBMC's write set inference to infer the write set of the loop. +So users have to specify the `modifies` clauses by their self only when the inferred write +sets are not complete---there exists some target that could be written to in the loop but +is not in the inferred write set. + +### Proof of termination + +Loop contracts also provide a way to prove the termination of the loop. +Without the proof of termination, Kani could report success of some assertions that +are actually unreachable due to non-terminating loops. +For example, consider the following program: + +```rs +fn simple_loop_non_terminating() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + #[kani::loop_invariant(x >= 1)] + while true{ + x = x; + }; + + assert!(x >= 1); +} +``` +After abstracting the loop, the loop will be transformed to no-op, and the assertion +`x >= 1` will be proved. However, the loop is actually an infinite loop, and the +assertion will never be reached. + +For this reason, Kani will also require the user to provide a `decreases` clause that +specifies a decreasing expression to prove the termination of the loop. For example, in +```rs +fn simple_loop_terminating() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + #[kani::loop_invariant(x >= 1)] + #[kani::loop_decreases(x)] + while x > 1{ + x = x - 1; + }; + + assert!(x >= 1); +} +``` +, the `decreases` clause `#[kani::loop_decreases(x)]` specifies that the value of `x` +decreases at each iteration of the loop, and hence the loop will terminate. + + +## Detailed Design + + +Kani implements the functionality of loop contracts in three places. + +1. Procedural macros `loop_invariant`, `loop_modifies`, and `loop_decreases`. +2. Code generation for builtin functions expanded from the above macros. +3. GOTO-level loop contracts using CBMC's contract language generated in + `kani-compiler`. + +### Procedural macros `loop_invariant`, `loop_modifies`, and `loop_decreases`. + +We will implement the three proc-macros `loop_invariant`, `loop_modifies`, and `loop_decreases` to +embed the annotation logic as Rust code. Kani will then compile them into MIR-level code. + + +### Code Generation for Builtin Functions + +Then in the MIR, we codegen the loop contracts as GOTO-level expressions and annotate them +into the corresponding loop latches---the jumps back to the loop head. + +The artifact `goto-instrument` in CBMC will extract the loop contracts from the named-subs +of the loop latch, and then apply and prove the extracted loop contracts. + + +### GOTO-Level Havocing + +The ordinary havocing in CBMC is not aware of the type constraints of Rust type. +Hence, we will use customized havocing functions for modifies targets. In detail, +Kani will generate code for the definition of corresponding `kani::any()` functions +for each modifies target. Then Kani will create a map from the modifies target to the +the name of its `kani::any()` function, and add the map to the loop latch too. + +On the CBMC site, `goto-instrument` will extract the map and instrument the customized +havocing functions for the modifies targets. + +## Rationale and alternatives + + + +### Rust-Level Transformation vs CBMC + +Besides transforming the loops in GOTO level using `goto-instrument`, +we could also do the transformation in Rust level using procedural macros, or +in MIR level. + +There are two reasons we prefer the GOTO-level transformation. +First, `goto-instrument` is a mature tool that can correctly instrument the frame +condition checking for the transformed loop, which will save us from reinventing +the error-prone wheel. Second, the loop contracts synthesis tool we developed and +are developing are all based on GOTO level. Hence, doing the transformation in +the GOTO level will make the integration of loop contracts with the synthesis tool +easier. + +## Open questions + +- How do we integrate loop contracts with the synthesis tool? When the user-provided + loop contracts are not enough prove the harness, we expect the loop-contract synthesizer + can fix the loop contracts. +- How do we translate back modify targets that inferred by CBMC to Rust level? +- It is not clear how the CBMC loop modifies inference works for Rust code. We need to + experiment more to decide what would be the best UX of using loop modifies. +- How do we handle havocing in unsafe code where it is fine to break the safety invariant + of Rust? In that case, we may need havocing function that preserves validity invariant + but not safety invariant. +- What is the proper mechanism for users to specify the loops that they want to opt-out from applying loop contracts, and (optionally) the unwind numbers for them. Such options should be per-harness. + +## Future possibilities + +- We can employ CBMC's decreases inference to infer the decreases clauses to reduce the + user burden of specifying the decreases clauses. + + + +--- From e3a5e8ec23f40ed1cc7a700cc57630161449d728 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Thu, 5 Sep 2024 13:47:26 -0700 Subject: [PATCH 08/21] Replace `proc-macro-error` with `proc-macro-error2` (#3493) The following security advisory has been issued today regarding the `proc-macro-error` crate which is causing our CI to fail: https://rustsec.org/advisories/RUSTSEC-2024-0370 Replacing the crate with `proc-macro-error2` which is a fork of that crate. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- Cargo.lock | 46 +++++++++--------------- library/kani_macros/Cargo.toml | 2 +- library/kani_macros/src/derive.rs | 2 +- library/kani_macros/src/lib.rs | 4 +-- tests/ui/derive-arbitrary/union/expected | 5 +-- 5 files changed, 22 insertions(+), 37 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 1c371b85fba9..560ad32c310c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -176,7 +176,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.77", + "syn", ] [[package]] @@ -483,7 +483,7 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn 2.0.77", + "syn", "tracing", "tracing-subscriber", "tracing-tree", @@ -538,10 +538,10 @@ dependencies = [ name = "kani_macros" version = "0.55.0" dependencies = [ - "proc-macro-error", + "proc-macro-error2", "proc-macro2", "quote", - "syn 2.0.77", + "syn", ] [[package]] @@ -801,27 +801,25 @@ dependencies = [ ] [[package]] -name = "proc-macro-error" -version = "1.0.4" +name = "proc-macro-error-attr2" +version = "2.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5" dependencies = [ - "proc-macro-error-attr", "proc-macro2", "quote", - "syn 1.0.109", - "version_check", ] [[package]] -name = "proc-macro-error-attr" -version = "1.0.4" +name = "proc-macro-error2" +version = "2.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +checksum = "74cdd32837fa2e86ec09c8266e5aad92400ac934c6dbca83d54673b298db3e45" dependencies = [ + "proc-macro-error-attr2", "proc-macro2", "quote", - "version_check", + "syn", ] [[package]] @@ -1029,7 +1027,7 @@ checksum = "a5831b979fd7b5439637af1752d535ff49f4860c0f341d1baeb6faf0f4242170" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn", ] [[package]] @@ -1136,17 +1134,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.77", -] - -[[package]] -name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "unicode-ident", + "syn", ] [[package]] @@ -1190,7 +1178,7 @@ checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn", ] [[package]] @@ -1287,7 +1275,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn", ] [[package]] @@ -1574,5 +1562,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn", ] diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index a6b20a68bc39..a1aeb743952b 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -13,7 +13,7 @@ proc-macro = true [dependencies] proc-macro2 = "1.0" -proc-macro-error = "1.0.4" +proc-macro-error2 = "2.0.0" quote = "1.0.20" syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-traits"] } diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index cc936560e510..e89f6f089795 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -10,7 +10,7 @@ //! //! ``` use proc_macro2::{Ident, Span, TokenStream}; -use proc_macro_error::abort; +use proc_macro_error2::abort; use quote::{quote, quote_spanned}; use syn::spanned::Spanned; use syn::{ diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 63ed990a4840..8a1d2d80f864 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -12,7 +12,7 @@ mod derive; // proc_macro::quote is nightly-only, so we'll cobble things together instead use proc_macro::TokenStream; -use proc_macro_error::proc_macro_error; +use proc_macro_error2::proc_macro_error; #[cfg(kani_sysroot)] use sysroot as attr_impl; @@ -398,7 +398,7 @@ pub fn modifies(attr: TokenStream, item: TokenStream) -> TokenStream { /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] mod sysroot { - use proc_macro_error::{abort, abort_call_site}; + use proc_macro_error2::{abort, abort_call_site}; mod contracts; diff --git a/tests/ui/derive-arbitrary/union/expected b/tests/ui/derive-arbitrary/union/expected index 3acea286d7ca..e54592a47ca6 100644 --- a/tests/ui/derive-arbitrary/union/expected +++ b/tests/ui/derive-arbitrary/union/expected @@ -3,10 +3,7 @@ error: Cannot derive `Arbitrary` for `Wrapper` union |\ | #[derive(kani::Arbitrary)]\ | ^^^^^^^^^^^^^^^\ -|\ +| note: `#[derive(Arbitrary)]` cannot be used for unions such as `Wrapper` -|\ -| union Wrapper {\ -| ^^^^^^^\ = note: this error originates in the derive macro `kani::Arbitrary` From 031587ab87879f005b946870eafbe03b7686210e Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Thu, 5 Sep 2024 13:49:35 -0700 Subject: [PATCH 09/21] Automatic toolchain upgrade to nightly-2024-09-04 (#3488) Update Rust toolchain from nightly-2024-09-03 to nightly-2024-09-04 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index a9bc7f1dd533..a8c4175df12a 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-09-03" +channel = "nightly-2024-09-04" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From faa47f7614b9d426f6de1a985a55c5abe1283619 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Fri, 6 Sep 2024 06:27:55 -0700 Subject: [PATCH 10/21] Automatic toolchain upgrade to nightly-2024-09-05 (#3500) Update Rust toolchain from nightly-2024-09-04 to nightly-2024-09-05 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com> --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index a8c4175df12a..9880980d2d48 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-09-04" +channel = "nightly-2024-09-05" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 0775ca80099dac32a09216520969a444da66114d Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Fri, 6 Sep 2024 08:41:39 -0700 Subject: [PATCH 11/21] Fix cmake configuration for perf job (#3499) Update the `cmake` configuration step used for building CBMC to include cadical. Resolves #3497 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/workflows/cbmc-latest.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml index 696f08fd44b8..b71ad55ec130 100644 --- a/.github/workflows/cbmc-latest.yml +++ b/.github/workflows/cbmc-latest.yml @@ -87,7 +87,7 @@ jobs: - name: Build CBMC working-directory: ./cbmc run: | - cmake -S . -Bbuild -DWITH_JBMC=OFF + cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" cmake --build build -- -j 4 # Prepend the bin directory to $PATH echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH From 2536f64bd79c371416cf27a7ab6729b8f76b38d6 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 6 Sep 2024 14:39:35 -0400 Subject: [PATCH 12/21] List RFC revisions (#3490) Addresses @jaisnan's feedback on list RFC--change `human` output to `pretty` and fix Kani version typo. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- rfc/src/SUMMARY.md | 3 ++- rfc/src/rfcs/{0012-list.md => 0013-list.md} | 25 +++++++++++++-------- 2 files changed, 18 insertions(+), 10 deletions(-) rename rfc/src/rfcs/{0012-list.md => 0013-list.md} (86%) diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index c5a7161d0d45..2fb7d0b133cd 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -17,4 +17,5 @@ - [0009-function-contracts](rfcs/0009-function-contracts.md) - [0010-quantifiers](rfcs/0010-quantifiers.md) - [0011-source-coverage](rfcs/0011-source-coverage.md) -- [0012-list](rfcs/0012-list.md) +- [0012-loop-contracts](rfcs/0012-loop-contracts.md) +- [0013-list](rfcs/0013-list.md) diff --git a/rfc/src/rfcs/0012-list.md b/rfc/src/rfcs/0013-list.md similarity index 86% rename from rfc/src/rfcs/0012-list.md rename to rfc/src/rfcs/0013-list.md index fea4a65be7f3..bdbf4681f430 100644 --- a/rfc/src/rfcs/0012-list.md +++ b/rfc/src/rfcs/0013-list.md @@ -2,7 +2,7 @@ - **Feature Request Issue:** [#2573](https://github.com/model-checking/kani/issues/2573), [#1612](https://github.com/model-checking/kani/issues/1612) - **RFC PR:** #3463 - **Status:** Under Review -- **Version:** 0 +- **Version:** 1 ------------------- @@ -20,18 +20,18 @@ This feature will not cause any regressions for exisiting users. ## User Experience -Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand will take the option `--message-format=[human|json]`, which changes the output format. The default is `human`, which prints to the terminal. The `json` option creates and writes to a JSON file instead. +Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand will take the option `--message-format=[pretty|json]`, which changes the output format. The default is `pretty`, which prints to the terminal. The `json` option creates and writes to a JSON file instead. This subcommand will not fail. In the case that it does not find any harnesses or contracts, it will print a message informing the user of that fact. -### Human Format +### Pretty Format -The default format, `human`, will print the harnesses and contracts in a project, along with the total counts of each. +The default format, `pretty`, will print the harnesses and contracts in a project, along with the total counts of each. For example: ``` -Kani Version: 0.5.4 +Kani Rust Verifier 0.54.0 (standalone) Standard Harnesses: - example::verify::check_new @@ -66,18 +66,22 @@ Totals: A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `#[proof_for_contract]` harness. +All sections will be present in the output, regardless of the result. If a list is empty, Kani will output a `NONE` string. + ### JSON Format -As the name implies, the goal of the `human` output is to be friendly for human readers. If the user wants an output format that's more easily parsed by a script, they can use the `json` option. +If the user wants an output format that's more easily parsed by a script, they can use the `json` option. -The JSON format will contain the same information as the human format, with the addition of file paths and file version. The file version will start at zero and increment whenever we make an update to the format. This way, any users relying on this format for their scripts can realize that changes have occurred and update their logic accordingly. +The JSON format will contain the same information as the pretty format, with the addition of file paths and file version. +The file version will use semantic versioning. +This way, any users relying on this format for their scripts can detect when we've released a new major version and update their logic accordingly. For example: ```json { - kani-version: 0.5.4, - file-version: 0, + kani-version: 0.54, + file-version: 0.1, standard-harnesses: [ { file: /Users/johnsmith/example/kani_standard_proofs.rs @@ -132,6 +136,9 @@ For example: } ``` +All sections will be present in the output, regardless of the result. +If there is no result for a given field (e.g., there are no contracts), Kani will output an empty list (or zero for totals). + ## Software Design We will add a new subcommand to `kani-driver`. From 6f8ca94edf70eb1fd95716dbedef1e40e9bef701 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 6 Sep 2024 12:16:19 -0700 Subject: [PATCH 13/21] Enable stubbing and function contracts for primitive types (#3496) Previously, Kani was not able to resolve methods that belong to primitive types, which would not allow users to specify primitive types as stub target, neither for contracts. Thus, extend the name resolution to be able to convert a type expression into a `Ty` for primitive types, and add a new method to search for function implementation for primitive types. I also moved the type resolution logic to its own module to make it a bit cleaner. Resolves #2646 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- kani-compiler/src/kani_middle/resolve.rs | 267 +++++++++--------- .../kani_middle/resolve/type_resolution.rs | 202 +++++++++++++ .../fixme_stub_lowered_methods.rs | 26 ++ .../StubPrimitives/stub_bool_methods.rs | 35 +++ .../StubPrimitives/stub_char_methods.rs | 18 ++ .../StubPrimitives/stub_float_methods.rs | 32 +++ .../StubPrimitives/stub_int_methods.rs | 39 +++ .../StubPrimitives/stub_ptr_methods.rs | 38 +++ .../StubPrimitives/stub_slice_methods.rs | 37 +++ .../resolution_errors.expected | 36 +++ .../resolution_errors.rs | 23 ++ .../unsupported_resolutions.expected | 10 +- .../unsupported_resolutions.rs | 10 +- 13 files changed, 630 insertions(+), 143 deletions(-) create mode 100644 kani-compiler/src/kani_middle/resolve/type_resolution.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_bool_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_char_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_float_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_int_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_ptr_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_slice_methods.rs create mode 100644 tests/ui/function-stubbing-error/resolution_errors.expected create mode 100644 tests/ui/function-stubbing-error/resolution_errors.rs diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 88b1af86efe9..b2b00c1e4a40 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -1,10 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains code for resolving strings representing simple paths to -//! `DefId`s for functions and methods. For the definition of a simple path, see -//! . +// +//! This module contains code for resolving strings representing paths (simple and qualified) to +//! `DefId`s for functions and methods. For the definition of a path, see +//! . //! -//! TODO: Extend this logic to support resolving qualified paths. +//! TODO: Change `resolve_fn` in order to return information about trait implementations. //! //! //! Note that glob use statements can form loops. The paths can also walk through the loop. @@ -15,6 +16,7 @@ use rustc_errors::ErrorGuaranteed; use rustc_hir::def::{DefKind, Res}; use rustc_hir::def_id::{DefId, LocalDefId, LocalModDefId, CRATE_DEF_INDEX, LOCAL_CRATE}; use rustc_hir::{ItemKind, UseKind}; +use rustc_middle::ty::fast_reject::{self, TreatParams}; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind}; @@ -22,34 +24,10 @@ use stable_mir::CrateDef; use std::collections::HashSet; use std::fmt; use std::iter::Peekable; -use std::str::FromStr; -use strum_macros::{EnumString, IntoStaticStr}; -use syn::{Ident, PathSegment, Type, TypePath}; -use tracing::debug; - -#[derive(Copy, Clone, Debug, Eq, PartialEq, IntoStaticStr, EnumString)] -#[strum(serialize_all = "lowercase")] -enum PrimitiveIdent { - Bool, - Char, - F16, - F32, - F64, - F128, - I8, - I16, - I32, - I64, - I128, - Isize, - Str, - U8, - U16, - U32, - U64, - U128, - Usize, -} +use syn::{PathSegment, QSelf, TypePath}; +use tracing::{debug, debug_span}; + +mod type_resolution; macro_rules! validate_kind { ($tcx:ident, $id:ident, $expected:literal, $kind:pat) => {{ @@ -61,6 +39,7 @@ macro_rules! validate_kind { } }}; } +pub(crate) use validate_kind; #[derive(Copy, Clone, Debug, PartialEq, Eq)] pub enum FnResolution { @@ -76,20 +55,34 @@ pub fn resolve_fn_path<'tcx>( current_module: LocalDefId, path: &TypePath, ) -> Result> { - match (&path.qself, &path.path.leading_colon) { - (Some(qself), Some(_)) => { - // Qualified path that does not define a trait. - resolve_ty(tcx, current_module, &qself.ty)?; - Err(ResolveError::UnsupportedPath { kind: "qualified bare function paths" }) - } - (Some(qself), None) => { - let ty = resolve_ty(tcx, current_module, &qself.ty)?; + let _span = debug_span!("resolve_fn_path", ?path).entered(); + match &path.qself { + // Qualified path for a trait method implementation, like `::bar`. + Some(QSelf { ty: syn_ty, position, .. }) if *position > 0 => { + let ty = type_resolution::resolve_ty(tcx, current_module, &syn_ty)?; let def_id = resolve_path(tcx, current_module, &path.path)?; validate_kind!(tcx, def_id, "function / method", DefKind::Fn | DefKind::AssocFn)?; Ok(FnResolution::FnImpl { def: stable_fn_def(tcx, def_id).unwrap(), ty }) } - (None, _) => { - // Simple path + // Qualified path for a primitive type, such as `<[u8]::sort>`. + Some(QSelf { ty: syn_ty, .. }) if type_resolution::is_type_primitive(syn_ty) => { + let ty = type_resolution::resolve_ty(tcx, current_module, &syn_ty)?; + let resolved = resolve_in_primitive(tcx, ty, path.path.segments.iter())?; + if resolved.segments.is_empty() { + Ok(FnResolution::Fn(stable_fn_def(tcx, resolved.base).unwrap())) + } else { + Err(ResolveError::UnexpectedType { tcx, item: resolved.base, expected: "module" }) + } + } + // Qualified path for a non-primitive type, such as `::foo>`. + Some(QSelf { ty: syn_ty, .. }) => { + let ty = type_resolution::resolve_ty(tcx, current_module, &syn_ty)?; + let def_id = resolve_in_user_type(tcx, ty, path.path.segments.iter())?; + validate_kind!(tcx, def_id, "function / method", DefKind::Fn | DefKind::AssocFn)?; + Ok(FnResolution::Fn(stable_fn_def(tcx, def_id).unwrap())) + } + // Simple path + None => { let def_id = resolve_path(tcx, current_module, &path.path)?; validate_kind!(tcx, def_id, "function / method", DefKind::Fn | DefKind::AssocFn)?; Ok(FnResolution::Fn(stable_fn_def(tcx, def_id).unwrap())) @@ -97,14 +90,15 @@ pub fn resolve_fn_path<'tcx>( } } -/// Attempts to resolve a simple path (in the form of a string) to a function / method `DefId`. +/// Attempts to resolve a *simple path* (in the form of a string) to a function / method `DefId`. /// -/// Use `[resolve_fn_path]` if you want to handle qualified paths and simple paths +/// Use `[resolve_fn_path]` if you want to handle qualified paths and simple paths. pub fn resolve_fn<'tcx>( tcx: TyCtxt<'tcx>, current_module: LocalDefId, path_str: &str, ) -> Result> { + let _span = debug_span!("resolve_fn", ?path_str, ?current_module).entered(); let path = syn::parse_str(path_str).map_err(|err| ResolveError::InvalidPath { msg: format!("Expected a path, but found `{path_str}`. {err}"), })?; @@ -143,74 +137,6 @@ pub fn expect_resolve_fn( } } -/// Attempts to resolve a type. -pub fn resolve_ty<'tcx>( - tcx: TyCtxt<'tcx>, - current_module: LocalDefId, - typ: &syn::Type, -) -> Result> { - debug!(?typ, ?current_module, "resolve_ty"); - let unsupported = |kind: &'static str| Err(ResolveError::UnsupportedPath { kind }); - let invalid = |kind: &'static str| { - Err(ResolveError::InvalidPath { - msg: format!("Expected a type, but found {kind} `{}`", typ.to_token_stream()), - }) - }; - #[warn(non_exhaustive_omitted_patterns)] - match typ { - Type::Path(path) if path.qself.is_none() => { - let def_id = resolve_path(tcx, current_module, &path.path)?; - validate_kind!(tcx, def_id, "type", DefKind::Struct | DefKind::Union | DefKind::Enum)?; - Ok(rustc_internal::stable(tcx.type_of(def_id)).value) - } - Type::Path(_) => unsupported("qualified paths"), - Type::Array(_) - | Type::BareFn(_) - | Type::Macro(_) - | Type::Never(_) - | Type::Paren(_) - | Type::Ptr(_) - | Type::Reference(_) - | Type::Slice(_) - | Type::Tuple(_) => unsupported("path including primitive types"), - Type::Verbatim(_) => unsupported("unknown paths"), - Type::Group(_) => invalid("group paths"), - Type::ImplTrait(_) => invalid("trait impl paths"), - Type::Infer(_) => invalid("inferred paths"), - Type::TraitObject(_) => invalid("trait object paths"), - _ => { - unreachable!() - } - } -} - -/// Checks if a Path segment represents a primitive -fn is_primitive(ident: &Ident) -> bool { - let token = ident.to_string(); - let Ok(typ) = syn::parse_str(&token) else { return false }; - #[warn(non_exhaustive_omitted_patterns)] - match typ { - Type::Array(_) - | Type::Ptr(_) - | Type::Reference(_) - | Type::Slice(_) - | Type::Never(_) - | Type::Tuple(_) => true, - Type::Path(_) => PrimitiveIdent::from_str(&token).is_ok(), - Type::BareFn(_) - | Type::Group(_) - | Type::ImplTrait(_) - | Type::Infer(_) - | Type::Macro(_) - | Type::Paren(_) - | Type::TraitObject(_) - | Type::Verbatim(_) => false, - _ => { - unreachable!() - } - } -} - /// Attempts to resolve a simple path (in the form of a string) to a `DefId`. /// The current module is provided as an argument in order to resolve relative /// paths. @@ -220,15 +146,15 @@ fn resolve_path<'tcx>( path: &syn::Path, ) -> Result> { debug!(?path, "resolve_path"); - let _span = tracing::span!(tracing::Level::DEBUG, "path_resolution").entered(); - let path = resolve_prefix(tcx, current_module, path)?; path.segments.into_iter().try_fold(path.base, |base, segment| { let name = segment.ident.to_string(); let def_kind = tcx.def_kind(base); let next_item = match def_kind { DefKind::ForeignMod | DefKind::Mod => resolve_in_module(tcx, base, &name), - DefKind::Struct | DefKind::Enum | DefKind::Union => resolve_in_type(tcx, base, &name), + DefKind::Struct | DefKind::Enum | DefKind::Union => { + resolve_in_type_def(tcx, base, &name) + } DefKind::Trait => resolve_in_trait(tcx, base, &name), kind => { debug!(?base, ?kind, "resolve_path: unexpected item"); @@ -250,6 +176,8 @@ pub enum ResolveError<'tcx> { InvalidPath { msg: String }, /// Unable to find an item. MissingItem { tcx: TyCtxt<'tcx>, base: DefId, unresolved: String }, + /// Unable to find an item in a primitive type. + MissingPrimitiveItem { base: Ty, unresolved: String }, /// Error triggered when the identifier points to an item with unexpected type. UnexpectedType { tcx: TyCtxt<'tcx>, item: DefId, expected: &'static str }, /// Error triggered when the identifier is not currently supported. @@ -291,6 +219,9 @@ impl<'tcx> fmt::Display for ResolveError<'tcx> { let def_desc = description(*tcx, *base); write!(f, "unable to find `{unresolved}` inside {def_desc}") } + ResolveError::MissingPrimitiveItem { base, unresolved } => { + write!(f, "unable to find `{unresolved}` inside `{base}`") + } ResolveError::UnsupportedPath { kind } => { write!(f, "Kani currently cannot resolve {kind}") } @@ -334,6 +265,7 @@ fn resolve_prefix<'tcx>( // Resolve qualifiers `crate`, initial `::`, and `self`. The qualifier // `self` may be followed be `super` (handled below). match (path.leading_colon, segments.next()) { + // Leading `::` indicates that the path points to an item inside an external crate. (Some(_), Some(segment)) => { // Skip root and get the external crate from the name that follows `::`. let next_name = segment.ident.to_string(); @@ -348,9 +280,11 @@ fn resolve_prefix<'tcx>( }) } } + // Path with `::` alone is invalid. (Some(_), None) => { Err(ResolveError::InvalidPath { msg: "expected identifier after `::`".to_string() }) } + // Path starting with `crate::`. (None, Some(segment)) if segment.ident == CRATE => { // Find the module at the root of the crate. let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module); @@ -360,14 +294,19 @@ fn resolve_prefix<'tcx>( }; Ok(Path { base: crate_root.to_def_id(), segments: segments.cloned().collect() }) } + // Path starting with "self::" (None, Some(segment)) if segment.ident == SELF => { resolve_super(tcx, current_module, segments.peekable()) } + // Path starting with "super::" (None, Some(segment)) if segment.ident == SUPER => { resolve_super(tcx, current_module, path.segments.iter().peekable()) } - (None, Some(segment)) if is_primitive(&segment.ident) => { - Err(ResolveError::UnsupportedPath { kind: "path including primitive types" }) + // Path starting with a primitive, such as "u8::" + (None, Some(segment)) if type_resolution::is_primitive(&segment) => { + let syn_ty = syn::parse2(segment.to_token_stream()).unwrap(); + let ty = type_resolution::resolve_ty(tcx, current_module, &syn_ty)?; + resolve_in_primitive(tcx, ty, segments) } (None, Some(segment)) => { // No special key word was used. Try local first otherwise try external name. @@ -561,8 +500,41 @@ fn resolve_in_glob_use(tcx: TyCtxt, res: &Res, name: &str) -> RelativeResolution } } -/// Resolves a function in a type. -fn resolve_in_type<'tcx>( +/// Resolves a function in a user type (non-primitive). +fn resolve_in_user_type<'tcx, 'a, I>( + tcx: TyCtxt<'tcx>, + ty: Ty, + mut segments: I, +) -> Result> +where + I: Iterator, +{ + let def_id = match ty.kind() { + TyKind::RigidTy(rigid_ty) => match rigid_ty { + RigidTy::Adt(def, _) => rustc_internal::internal(tcx, def.def_id()), + RigidTy::Foreign(_) => { + return Err(ResolveError::UnsupportedPath { kind: "foreign type" }); + } + _ => { + unreachable!("Unexpected type {ty}") + } + }, + TyKind::Alias(_, _) => return Err(ResolveError::UnsupportedPath { kind: "alias" }), + TyKind::Param(_) | TyKind::Bound(_, _) => { + // Name resolution can not resolve in a parameter or bound. + unreachable!() + } + }; + let Some(name) = segments.next() else { unreachable!() }; + if segments.next().is_some() { + Err(ResolveError::UnexpectedType { tcx, item: def_id, expected: "module" }) + } else { + resolve_in_type_def(tcx, def_id, &name.ident.to_string()) + } +} + +/// Resolves a function in a type given its `def_id`. +fn resolve_in_type_def<'tcx>( tcx: TyCtxt<'tcx>, type_id: DefId, name: &str, @@ -576,11 +548,7 @@ fn resolve_in_type<'tcx>( .iter() .flat_map(|impl_id| tcx.associated_item_def_ids(impl_id)) .cloned() - .find(|item| { - let item_path = tcx.def_path_str(*item); - let last = item_path.split("::").last().unwrap(); - last == name - }) + .find(|item| is_item_name(tcx, *item, name)) .ok_or_else(missing_item_err) } @@ -594,14 +562,53 @@ fn resolve_in_trait<'tcx>( let missing_item_err = || ResolveError::MissingItem { tcx, base: trait_id, unresolved: name.to_string() }; let trait_def = tcx.trait_def(trait_id); - // Try the inherent `impl` blocks (i.e., non-trait `impl`s). + // Look for the given name in the list of associated items for the trait definition. tcx.associated_item_def_ids(trait_def.def_id) .iter() .copied() - .find(|item| { - let item_path = tcx.def_path_str(*item); - let last = item_path.split("::").last().unwrap(); - last == name - }) + .find(|item| is_item_name(tcx, *item, name)) .ok_or_else(missing_item_err) } + +/// Resolves a primitive type function. +/// +/// This function assumes that `ty` is a primitive. +fn resolve_in_primitive<'tcx, 'a, I>( + tcx: TyCtxt<'tcx>, + ty: Ty, + mut segments: I, +) -> Result> +where + I: Iterator, +{ + if let Some(next) = segments.next() { + let name = next.ident.to_string(); + debug!(?name, ?ty, "resolve_in_primitive"); + let internal_ty = rustc_internal::internal(tcx, ty); + let simple_ty = + fast_reject::simplify_type(tcx, internal_ty, TreatParams::AsCandidateKey).unwrap(); + let impls = tcx.incoherent_impls(simple_ty).unwrap(); + // Find the primitive impl. + let item = impls + .iter() + .find_map(|item_impl| { + tcx.associated_item_def_ids(item_impl) + .iter() + .copied() + .find(|item| is_item_name(tcx, *item, &name)) + }) + .ok_or_else(|| ResolveError::MissingPrimitiveItem { + base: ty, + unresolved: name.to_string(), + })?; + Ok(Path { base: item, segments: segments.cloned().collect() }) + } else { + Err(ResolveError::InvalidPath { msg: format!("Unexpected primitive type `{ty}`") }) + } +} + +fn is_item_name(tcx: TyCtxt, item: DefId, name: &str) -> bool { + let item_path = tcx.def_path_str(item); + let last = item_path.split("::").last().unwrap(); + last == name +} diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs new file mode 100644 index 000000000000..790019ab2998 --- /dev/null +++ b/kani-compiler/src/kani_middle/resolve/type_resolution.rs @@ -0,0 +1,202 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains code used for resolve type / trait names + +use crate::kani_middle::resolve::{resolve_path, validate_kind, ResolveError}; +use quote::ToTokens; +use rustc_hir::def::DefKind; +use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use rustc_span::def_id::LocalDefId; +use stable_mir::mir::Mutability; +use stable_mir::ty::{FloatTy, IntTy, Region, RegionKind, RigidTy, Ty, UintTy}; +use std::str::FromStr; +use strum_macros::{EnumString, IntoStaticStr}; +use syn::{Expr, ExprLit, Lit, Type, TypePath}; +use tracing::{debug, debug_span}; + +/// Attempts to resolve a type from a type expression. +pub fn resolve_ty<'tcx>( + tcx: TyCtxt<'tcx>, + current_module: LocalDefId, + typ: &syn::Type, +) -> Result> { + let _span = debug_span!("resolve_ty", ?typ).entered(); + debug!(?typ, ?current_module, "resolve_ty"); + let unsupported = |kind: &'static str| Err(ResolveError::UnsupportedPath { kind }); + let invalid = |kind: &'static str| { + Err(ResolveError::InvalidPath { + msg: format!("Expected a type, but found {kind} `{}`", typ.to_token_stream()), + }) + }; + #[warn(non_exhaustive_omitted_patterns)] + match typ { + Type::Path(TypePath { qself, path }) => { + assert_eq!(*qself, None, "Unexpected qualified path"); + if let Some(primitive) = + path.get_ident().and_then(|ident| PrimitiveIdent::from_str(&ident.to_string()).ok()) + { + Ok(primitive.into()) + } else { + let def_id = resolve_path(tcx, current_module, path)?; + validate_kind!( + tcx, + def_id, + "type", + DefKind::Struct | DefKind::Union | DefKind::Enum + )?; + Ok(rustc_internal::stable(tcx.type_of(def_id)).value) + } + } + Type::Array(array) => { + let elem_ty = resolve_ty(tcx, current_module, &array.elem)?; + let len = parse_len(&array.len).map_err(|msg| ResolveError::InvalidPath { msg })?; + Ty::try_new_array(elem_ty, len.try_into().unwrap()).map_err(|err| { + ResolveError::InvalidPath { msg: format!("Cannot instantiate array. {err}") } + }) + } + Type::Paren(inner) => resolve_ty(tcx, current_module, &inner.elem), + Type::Ptr(ptr) => { + let elem_ty = resolve_ty(tcx, current_module, &ptr.elem)?; + let mutability = + if ptr.mutability.is_some() { Mutability::Mut } else { Mutability::Not }; + Ok(Ty::new_ptr(elem_ty, mutability)) + } + Type::Reference(reference) => { + let elem_ty = resolve_ty(tcx, current_module, &reference.elem)?; + let mutability = + if reference.mutability.is_some() { Mutability::Mut } else { Mutability::Not }; + Ok(Ty::new_ref(Region { kind: RegionKind::ReErased }, elem_ty, mutability)) + } + Type::Slice(slice) => { + let elem_ty = resolve_ty(tcx, current_module, &slice.elem)?; + Ok(Ty::from_rigid_kind(RigidTy::Slice(elem_ty))) + } + Type::Tuple(tuple) => { + let elems = tuple + .elems + .iter() + .map(|elem| resolve_ty(tcx, current_module, &elem)) + .collect::, _>>()?; + Ok(Ty::new_tuple(&elems)) + } + Type::Never(_) => Ok(Ty::from_rigid_kind(RigidTy::Never)), + Type::BareFn(_) => unsupported("bare function"), + Type::Macro(_) => invalid("macro"), + Type::Group(_) => invalid("group paths"), + Type::ImplTrait(_) => invalid("trait impl paths"), + Type::Infer(_) => invalid("inferred paths"), + Type::TraitObject(_) => invalid("trait object paths"), + Type::Verbatim(_) => unsupported("unknown paths"), + _ => { + unreachable!() + } + } +} + +/// Enumeration of existing primitive types that are not parametric. +#[derive(Copy, Clone, Debug, Eq, PartialEq, IntoStaticStr, EnumString)] +#[strum(serialize_all = "lowercase")] +pub(super) enum PrimitiveIdent { + Bool, + Char, + F16, + F32, + F64, + F128, + I8, + I16, + I32, + I64, + I128, + Isize, + Str, + U8, + U16, + U32, + U64, + U128, + Usize, +} + +/// Convert a primitive ident into a primitive `Ty`. +impl From for Ty { + fn from(value: PrimitiveIdent) -> Self { + match value { + PrimitiveIdent::Bool => Ty::bool_ty(), + PrimitiveIdent::Char => Ty::from_rigid_kind(RigidTy::Char), + PrimitiveIdent::F16 => Ty::from_rigid_kind(RigidTy::Float(FloatTy::F16)), + PrimitiveIdent::F32 => Ty::from_rigid_kind(RigidTy::Float(FloatTy::F32)), + PrimitiveIdent::F64 => Ty::from_rigid_kind(RigidTy::Float(FloatTy::F64)), + PrimitiveIdent::F128 => Ty::from_rigid_kind(RigidTy::Float(FloatTy::F128)), + PrimitiveIdent::I8 => Ty::signed_ty(IntTy::I8), + PrimitiveIdent::I16 => Ty::signed_ty(IntTy::I16), + PrimitiveIdent::I32 => Ty::signed_ty(IntTy::I32), + PrimitiveIdent::I64 => Ty::signed_ty(IntTy::I64), + PrimitiveIdent::I128 => Ty::signed_ty(IntTy::I128), + PrimitiveIdent::Isize => Ty::signed_ty(IntTy::Isize), + PrimitiveIdent::Str => Ty::from_rigid_kind(RigidTy::Str), + PrimitiveIdent::U8 => Ty::unsigned_ty(UintTy::U8), + PrimitiveIdent::U16 => Ty::unsigned_ty(UintTy::U16), + PrimitiveIdent::U32 => Ty::unsigned_ty(UintTy::U32), + PrimitiveIdent::U64 => Ty::unsigned_ty(UintTy::U64), + PrimitiveIdent::U128 => Ty::unsigned_ty(UintTy::U128), + PrimitiveIdent::Usize => Ty::unsigned_ty(UintTy::Usize), + } + } +} + +/// Checks if a Path segment represents a primitive. +/// +/// Note that this function will return false for expressions that cannot be parsed as a type. +pub(super) fn is_primitive(path: &T) -> bool +where + T: ToTokens, +{ + let token = path.to_token_stream(); + let Ok(typ) = syn::parse2(token) else { return false }; + is_type_primitive(&typ) +} + +/// Checks if a type is a primitive including composite ones. +pub(super) fn is_type_primitive(typ: &syn::Type) -> bool { + #[warn(non_exhaustive_omitted_patterns)] + match typ { + Type::Array(_) + | Type::Ptr(_) + | Type::Reference(_) + | Type::Slice(_) + | Type::Never(_) + | Type::Tuple(_) => true, + Type::Path(TypePath { qself: Some(qself), path }) => { + path.segments.is_empty() && is_type_primitive(&qself.ty) + } + Type::Path(TypePath { qself: None, path }) => path + .get_ident() + .map_or(false, |ident| PrimitiveIdent::from_str(&ident.to_string()).is_ok()), + Type::BareFn(_) + | Type::Group(_) + | Type::ImplTrait(_) + | Type::Infer(_) + | Type::Macro(_) + | Type::Paren(_) + | Type::TraitObject(_) + | Type::Verbatim(_) => false, + _ => { + unreachable!() + } + } +} + +/// Parse the length of the array. +/// We currently only support a constant length. +fn parse_len(len: &Expr) -> Result { + if let Expr::Lit(ExprLit { lit: Lit::Int(lit), .. }) = len { + if matches!(lit.suffix(), "" | "usize") + && let Ok(val) = usize::from_str(lit.base10_digits()) + { + return Ok(val); + } + } + Err(format!("Expected a `usize` constant, but found `{}`", len.to_token_stream())) +} diff --git a/tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs b/tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs new file mode 100644 index 000000000000..130a062071ba --- /dev/null +++ b/tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing + +//! Kani supports stubbing of most primitive methods, however, some methods, such as len, may be +//! lowered to an Rvalue. + +/// Check that we can stub slices methods +pub mod slices_check { + #[derive(kani::Arbitrary)] + pub struct MyStruct(u8, i32); + + pub fn stub_len_is_10(_: &[T]) -> usize { + 10 + } + + // This fails since `<[T]>::len` is lowered to `Rvalue::Len`. + #[kani::proof] + #[kani::stub(<[MyStruct]>::len, stub_len_is_10)] + pub fn check_stub_len_is_10() { + let input: [MyStruct; 5] = kani::any(); + let slice = kani::slice::any_slice_of_array(&input); + assert_eq!(slice.len(), 10); + } +} diff --git a/tests/kani/Stubbing/StubPrimitives/stub_bool_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_bool_methods.rs new file mode 100644 index 000000000000..44f926552c74 --- /dev/null +++ b/tests/kani/Stubbing/StubPrimitives/stub_bool_methods.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we can correctly stub bool functions. + +pub fn stub_then_some_is_none(_: bool, _: T) -> Option { + None +} + +/// Check that we can stub `then_some`. +#[kani::proof] +#[kani::stub(bool::then_some, stub_then_some_is_none)] +pub fn check_stub_then_some() { + let input: bool = kani::any(); + assert_eq!(input.then_some("h"), None); +} + +pub fn stub_then_panic(_: bool, _: F) -> Option +where + F: FnOnce() -> T, +{ + panic!() +} + +/// Check that we can stub `then`. +#[kani::proof] +#[kani::should_panic] +#[kani::stub(bool::then, stub_then_panic)] +pub fn check_stub_then() { + let input: bool = kani::any(); + let output: char = kani::any(); + assert_eq!(input.then(|| output).unwrap_or(output), output); +} diff --git a/tests/kani/Stubbing/StubPrimitives/stub_char_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_char_methods.rs new file mode 100644 index 000000000000..a012208c7761 --- /dev/null +++ b/tests/kani/Stubbing/StubPrimitives/stub_char_methods.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we can correctly stub char functions. +/// Check that we can stub is_ascii from `char`. +pub fn stub_is_ascii_true(_: &char) -> bool { + true +} + +/// Check stubbing by directly calling `str::is_ascii` +#[kani::proof] +#[kani::stub(char::is_ascii, stub_is_ascii_true)] +pub fn check_stub_is_ascii() { + let input: char = kani::any(); + assert!(input.is_ascii()); +} diff --git a/tests/kani/Stubbing/StubPrimitives/stub_float_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_float_methods.rs new file mode 100644 index 000000000000..196c1be3053e --- /dev/null +++ b/tests/kani/Stubbing/StubPrimitives/stub_float_methods.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we can correctly stub float functions. +#![feature(f128)] +#![feature(f16)] + +/// Generate stub and harness for floor method on floats. +macro_rules! stub_floor { + ($ty:ty, $harness:ident, $stub:ident) => { + // Stub that always returns 0. + pub fn $stub(_: $ty) -> $ty { + 0.0 + } + + // Harness + #[kani::proof] + #[kani::stub($ty::floor, $stub)] + pub fn $harness() { + let input = kani::any(); + let floor = <$ty>::floor(input); + assert_eq!(floor, 0.0); + } + }; +} + +stub_floor!(f16, f16_floor, stub_f16_floor); +stub_floor!(f32, f32_floor, stub_f32_floor); +stub_floor!(f64, f64_floor, stub_f64_floor); +stub_floor!(f128, f128_floor, stub_f128_floor); diff --git a/tests/kani/Stubbing/StubPrimitives/stub_int_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_int_methods.rs new file mode 100644 index 000000000000..bebbc47df245 --- /dev/null +++ b/tests/kani/Stubbing/StubPrimitives/stub_int_methods.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we can correctly stub integer types functions. + +/// Generate stub and harness for count_ones method on integers. +macro_rules! stub_count_ones { + ($ty:ty, $harness:ident, $stub:ident) => { + // Stub that always returns 0. + pub fn $stub(_: $ty) -> u32 { + 0 + } + + // Harness + #[kani::proof] + #[kani::stub($ty::count_ones, $stub)] + pub fn $harness() { + let input = kani::any(); + let ones = <$ty>::count_ones(input); + assert_eq!(ones, 0); + } + }; +} + +stub_count_ones!(u8, u8_count_ones, stub_u8_count_ones); +stub_count_ones!(u16, u16_count_ones, stub_u16_count_ones); +stub_count_ones!(u32, u32_count_ones, stub_u32_count_ones); +stub_count_ones!(u64, u64_count_ones, stub_u64_count_ones); +stub_count_ones!(u128, u128_count_ones, stub_u128_count_ones); +stub_count_ones!(usize, usize_count_ones, stub_usize_count_ones); + +stub_count_ones!(i8, i8_count_ones, stub_i8_count_ones); +stub_count_ones!(i16, i16_count_ones, stub_i16_count_ones); +stub_count_ones!(i32, i32_count_ones, stub_i32_count_ones); +stub_count_ones!(i64, i64_count_ones, stub_i64_count_ones); +stub_count_ones!(i128, i128_count_ones, stub_i128_count_ones); +stub_count_ones!(isize, isize_count_ones, stub_isize_count_ones); diff --git a/tests/kani/Stubbing/StubPrimitives/stub_ptr_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_ptr_methods.rs new file mode 100644 index 000000000000..1bce08059d4d --- /dev/null +++ b/tests/kani/Stubbing/StubPrimitives/stub_ptr_methods.rs @@ -0,0 +1,38 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we can correctly stub methods from raw pointer types. + +pub fn stub_len_is_10(_: *const [T]) -> usize { + 10 +} + +pub fn stub_mut_len_is_0(_: *mut [T]) -> usize { + 0 +} + +#[kani::proof] +#[kani::stub(<*const [u8]>::len, stub_len_is_10)] +#[kani::stub(<*mut [u8]>::len, stub_mut_len_is_0)] +pub fn check_stub_len_raw_ptr() { + let mut input: [u8; 5] = kani::any(); + let mut_ptr = &mut input as *mut [u8]; + let ptr = &input as *const [u8]; + assert_eq!(mut_ptr.len(), 0); + assert_eq!(ptr.len(), 10); +} + +pub fn stub_is_always_null(_: *const T) -> bool { + true +} + +// Fix-me: Option doesn't seem to work without the fully qualified path. +#[kani::proof] +#[kani::stub(<*const std::option::Option>::is_null, stub_is_always_null)] +pub fn check_stub_is_null() { + let input: Option = kani::any(); + let ptr = &input as *const Option; + assert!(unsafe { ptr.is_null() }); +} diff --git a/tests/kani/Stubbing/StubPrimitives/stub_slice_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_slice_methods.rs new file mode 100644 index 000000000000..b7e4fafaa638 --- /dev/null +++ b/tests/kani/Stubbing/StubPrimitives/stub_slice_methods.rs @@ -0,0 +1,37 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we can correctly stub slices and string slices functions. + +/// Check that we can stub str::is_ascii +pub mod str_check { + pub fn stub_is_ascii_false(_: &str) -> bool { + false + } + + #[kani::proof] + #[kani::stub(str::is_ascii, stub_is_ascii_false)] + pub fn check_stub_is_ascii() { + let input = "is_ascii"; + assert!(!input.is_ascii()); + } +} + +/// Check that we can stub slices +pub mod slices_check { + #[derive(kani::Arbitrary, Ord, PartialOrd, Copy, Clone, PartialEq, Eq)] + pub struct MyStruct(u8, i32); + + pub fn stub_sort_noop(_: &mut [T]) {} + + #[kani::proof] + #[kani::stub(<[MyStruct]>::sort, stub_sort_noop)] + pub fn check_stub_sort_noop() { + let mut input: [MyStruct; 5] = kani::any(); + let copy = input.clone(); + input.sort(); + assert_eq!(input, copy); + } +} diff --git a/tests/ui/function-stubbing-error/resolution_errors.expected b/tests/ui/function-stubbing-error/resolution_errors.expected new file mode 100644 index 000000000000..d722f13bd691 --- /dev/null +++ b/tests/ui/function-stubbing-error/resolution_errors.expected @@ -0,0 +1,36 @@ +error: failed to resolve `<[char ; 10]>::foo`: unable to find `foo` inside `[char; 10]` +resolution_errors.rs +| +| #[kani::stub(<[char; 10]>::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `str::foo`: unable to find `foo` inside `str` +resolution_errors.rs +| +| #[kani::stub(str::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `<[u32]>::foo`: unable to find `foo` inside `[u32]` +resolution_errors.rs +| +| #[kani::stub(<[u32]>::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `<(i32 , i32)>::foo`: unable to find `foo` inside `(i32, i32)` +resolution_errors.rs +| +| #[kani::stub(<(i32, i32)>::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `u8::foo`: unable to find `foo` inside `u8` +resolution_errors.rs +| +| #[kani::stub(u8::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `::foo`: unable to find `foo` inside struct `Bar` +resolution_errors.rs +| +| #[kani::stub(::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + diff --git a/tests/ui/function-stubbing-error/resolution_errors.rs b/tests/ui/function-stubbing-error/resolution_errors.rs new file mode 100644 index 000000000000..efb87efad08e --- /dev/null +++ b/tests/ui/function-stubbing-error/resolution_errors.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we emit a nice error message for resolution failures. + +/// Dummy structure +pub struct Bar; + +/// Dummy stub +pub fn stub_foo() -> bool { + true +} + +#[kani::proof] +#[kani::stub(::foo, stub_foo)] +#[kani::stub(u8::foo, stub_foo)] +#[kani::stub(<(i32, i32)>::foo, stub_foo)] +#[kani::stub(<[u32]>::foo, stub_foo)] +#[kani::stub(str::foo, stub_foo)] +#[kani::stub(<[char; 10]>::foo, stub_foo)] +fn invalid_methods() {} diff --git a/tests/ui/function-stubbing-error/unsupported_resolutions.expected b/tests/ui/function-stubbing-error/unsupported_resolutions.expected index 1b4c00d22f4f..e723ac97813d 100644 --- a/tests/ui/function-stubbing-error/unsupported_resolutions.expected +++ b/tests/ui/function-stubbing-error/unsupported_resolutions.expected @@ -1,8 +1,4 @@ -error: failed to resolve `<[char ; 10]>::foo`: Kani currently cannot resolve path including primitive types -error: failed to resolve `<& [u32]>::foo`: Kani currently cannot resolve path including primitive types -error: failed to resolve `<& [u32] as Foo>::foo`: Kani currently cannot resolve path including primitive types -error: failed to resolve `<(i32 , i32) as Foo>::foo`: Kani currently cannot resolve path including primitive types -error: failed to resolve `u8::foo`: Kani currently cannot resolve path including primitive types +error: Kani currently does not support stubbing trait implementations. error: failed to resolve `::bar`: unable to find `bar` inside trait `Foo` -error: Kani currently does not support stubbing trait implementations -error: failed to resolve `::foo`: Kani currently cannot resolve qualified bare function paths + +error: aborting due to 4 previous errors diff --git a/tests/ui/function-stubbing-error/unsupported_resolutions.rs b/tests/ui/function-stubbing-error/unsupported_resolutions.rs index 2fc74a0fd44f..0fcf102741eb 100644 --- a/tests/ui/function-stubbing-error/unsupported_resolutions.rs +++ b/tests/ui/function-stubbing-error/unsupported_resolutions.rs @@ -19,7 +19,7 @@ impl Foo for Bar {} impl Foo for u8 {} -impl Foo for &[T] {} +impl Foo for [T] {} impl Foo for [char; 10] {} @@ -30,13 +30,11 @@ pub fn stub_foo() -> bool { true } +/// We still do not support stubbing for trait methods. +/// #[kani::proof] -#[kani::stub(::foo, stub_foo)] #[kani::stub(::foo, stub_foo)] #[kani::stub(::bar, stub_foo)] -#[kani::stub(u8::foo, stub_foo)] #[kani::stub(<(i32, i32) as Foo>::foo, stub_foo)] -#[kani::stub(<&[u32] as Foo>::foo, stub_foo)] -#[kani::stub(<&[u32]>::foo, stub_foo)] -#[kani::stub(<[char; 10]>::foo, stub_foo)] +#[kani::stub(<[u32] as Foo>::foo, stub_foo)] fn unsupported_args() {} From fde5fbbf3cb981cb4e5e18e5c167a6518ca61415 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Fri, 6 Sep 2024 23:42:12 -0700 Subject: [PATCH 14/21] Automatic toolchain upgrade to nightly-2024-09-06 (#3502) Update Rust toolchain from nightly-2024-09-05 to nightly-2024-09-06 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com> --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 9880980d2d48..c01df140e897 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-09-05" +channel = "nightly-2024-09-06" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 20eb00c750837bce7a11e1154a6532e283bd9706 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Sat, 7 Sep 2024 09:14:52 -0700 Subject: [PATCH 15/21] Fix iss3495 (#3501) As suggested in https://github.com/GnomedDev/proc-macro-error-2/issues/1#issuecomment-2333926796, turning on the `nightly` feature for `proc-macro-error2` to restore the previous error message for `derive(Arbitrary)`. Resolves #3495 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/kani_macros/Cargo.toml | 2 +- tests/ui/derive-arbitrary/union/expected | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index a1aeb743952b..6930366b84fc 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -13,7 +13,7 @@ proc-macro = true [dependencies] proc-macro2 = "1.0" -proc-macro-error2 = "2.0.0" +proc-macro-error2 = { version = "2.0.0", features = ["nightly"] } quote = "1.0.20" syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-traits"] } diff --git a/tests/ui/derive-arbitrary/union/expected b/tests/ui/derive-arbitrary/union/expected index e54592a47ca6..3acea286d7ca 100644 --- a/tests/ui/derive-arbitrary/union/expected +++ b/tests/ui/derive-arbitrary/union/expected @@ -3,7 +3,10 @@ error: Cannot derive `Arbitrary` for `Wrapper` union |\ | #[derive(kani::Arbitrary)]\ | ^^^^^^^^^^^^^^^\ -| +|\ note: `#[derive(Arbitrary)]` cannot be used for unions such as `Wrapper` +|\ +| union Wrapper {\ +| ^^^^^^^\ = note: this error originates in the derive macro `kani::Arbitrary` From 7896cff0922cb051e261e0b7cacaf879cd612d96 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Sun, 8 Sep 2024 16:00:05 -0700 Subject: [PATCH 16/21] Upgrade toolchain to 2024-09-07 (#3504) Relevant upstream PR: https://github.com/rust-lang/rust/pull/128776: The `TreatParams` enum variants were renamed. Resolves #3503 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- kani-compiler/src/kani_middle/resolve.rs | 3 ++- rust-toolchain.toml | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index b2b00c1e4a40..d2b1fcd06471 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -586,7 +586,8 @@ where debug!(?name, ?ty, "resolve_in_primitive"); let internal_ty = rustc_internal::internal(tcx, ty); let simple_ty = - fast_reject::simplify_type(tcx, internal_ty, TreatParams::AsCandidateKey).unwrap(); + fast_reject::simplify_type(tcx, internal_ty, TreatParams::InstantiateWithInfer) + .unwrap(); let impls = tcx.incoherent_impls(simple_ty).unwrap(); // Find the primitive impl. let item = impls diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c01df140e897..871f98b09046 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-09-06" +channel = "nightly-2024-09-07" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 92c25e67af50ad24ee205ec956c942821df5f1d8 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sun, 8 Sep 2024 23:53:48 -0700 Subject: [PATCH 17/21] Automatic cargo update to 2024-09-09 (#3506) Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com> --- Cargo.lock | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 560ad32c310c..2e179767122f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -75,9 +75,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.86" +version = "1.0.87" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b3d1d046238990b9cf5bcde22a3fb3584ee5cf65fb2765f454ed428c7a0063da" +checksum = "10f00e1f6e58a40e807377c75c6a7f97bf9044fab57816f2414e6f5f4499d7b8" [[package]] name = "autocfg" @@ -147,9 +147,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.5.16" +version = "4.5.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ed6719fffa43d0d87e5fd8caeab59be1554fb028cd30edc88fc4369b17971019" +checksum = "3e5a21b8495e732f1b3c364c9949b201ca7bae518c502c80256c96ad79eaf6ac" dependencies = [ "clap_builder", "clap_derive", @@ -157,9 +157,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.15" +version = "4.5.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "216aec2b177652e3846684cbfe25c9964d18ec45234f0f5da5157b207ed1aab6" +checksum = "8cf2dd12af7a047ad9d6da2b6b249759a22a7abc0f474c1dae1777afa4b21a73" dependencies = [ "anstream", "anstyle", @@ -812,9 +812,9 @@ dependencies = [ [[package]] name = "proc-macro-error2" -version = "2.0.0" +version = "2.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "74cdd32837fa2e86ec09c8266e5aad92400ac934c6dbca83d54673b298db3e45" +checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802" dependencies = [ "proc-macro-error-attr2", "proc-macro2", @@ -951,9 +951,9 @@ checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" [[package]] name = "rustix" -version = "0.38.35" +version = "0.38.36" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a85d50532239da68e9addb745ba38ff4612a242c1c7ceea689c4bc7c2f43c36f" +checksum = "3f55e80d50763938498dd5ebb18647174e0c76dc38c5505294bb224624f30f36" dependencies = [ "bitflags", "errno", @@ -1012,18 +1012,18 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.209" +version = "1.0.210" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "99fce0ffe7310761ca6bf9faf5115afbc19688edd00171d81b1bb1b116c63e09" +checksum = "c8e3592472072e6e22e0a54d5904d9febf8508f65fb8552499a1abc7d1078c3a" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.209" +version = "1.0.210" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a5831b979fd7b5439637af1752d535ff49f4860c0f341d1baeb6faf0f4242170" +checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" dependencies = [ "proc-macro2", "quote", @@ -1032,9 +1032,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.127" +version = "1.0.128" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8043c06d9f82bd7271361ed64f415fe5e12a77fdb52e573e7f06a516dea329ad" +checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8" dependencies = [ "itoa", "memchr", From cda1b30c935c327a8d4ccba0add9f30b9612863f Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sun, 8 Sep 2024 23:54:20 -0700 Subject: [PATCH 18/21] Automatic toolchain upgrade to nightly-2024-09-08 (#3505) Update Rust toolchain from nightly-2024-09-07 to nightly-2024-09-08 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com> --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 871f98b09046..a3febf5ae7db 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-09-07" +channel = "nightly-2024-09-08" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 80a4e51833a6fd8f3398adf109129f45f4431c15 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 9 Sep 2024 10:51:14 -0700 Subject: [PATCH 19/21] Bump tests/perf/s2n-quic from `1ff3a9c` to `d8be30e` (#3509) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `1ff3a9c` to `d8be30e`.
Commits

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) ---
Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- tests/perf/s2n-quic | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 1ff3a9c8adee..d8be30efa9b9 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 1ff3a9c8adee30346537698c7b2a12279facd2d3 +Subproject commit d8be30efa9b9f0d639a08cd59b51c4e52a2a7b9b From 5f6de6ee3b42ffdc91e9414beb4c119edb81acf1 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Mon, 9 Sep 2024 13:01:24 -0700 Subject: [PATCH 20/21] Reduce object-bits for test to avoid OOM (#3511) Kani often runs out of memory on `tests/expected/function-contract/history/stub.rs` when running the regressions. In particular, `quadruple_harness` consumes over 9 GB of memory. This PR reduces the object bits for this test to 8 to avoid OOM issues. This brings down memory usage to ~125 MB. Before: ```bash $ /usr/bin/time -v kani -Zfunction-contracts stub.rs --harness quadruple_harness Maximum resident set size (kbytes): 9136036 ``` After: ```bash $ /usr/bin/time -v kani -Zfunction-contracts stub.rs --harness quadruple_harness --enable-unstable --cbmc-args --object-bits 8 ... Maximum resident set size (kbytes): 125172 ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- tests/expected/function-contract/history/stub.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/expected/function-contract/history/stub.rs b/tests/expected/function-contract/history/stub.rs index 77c590134f41..ce795bea6990 100644 --- a/tests/expected/function-contract/history/stub.rs +++ b/tests/expected/function-contract/history/stub.rs @@ -1,6 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts +// This test consumes > 9 GB of memory with 16 object bits. Reducing the number +// of object bits to 8 to avoid running out of memory. +// kani-flags: -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 8 #[kani::ensures(|result| old(*ptr + *ptr) == *ptr)] #[kani::requires(*ptr < 100)] From 76ad70111300bfca9abeff178732daa7841d6317 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 10 Sep 2024 16:31:39 -0700 Subject: [PATCH 21/21] Bump peter-evans/create-pull-request from 6 to 7 (#3510) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bumps [peter-evans/create-pull-request](https://github.com/peter-evans/create-pull-request) from 6 to 7.
Release notes

Sourced from peter-evans/create-pull-request's releases.

Create Pull Request v7.0.0

:sparkles: Now supports commit signing with bot-generated tokens! See "What's new" below. :writing_hand::robot:

Behaviour changes

  • Action input git-token has been renamed branch-token, to be more clear about its purpose. The branch-token is the token that the action will use to create and update the branch.
  • The action now handles requests that have been rate-limited by GitHub. Requests hitting a primary rate limit will retry twice, for a total of three attempts. Requests hitting a secondary rate limit will not be retried.
  • The pull-request-operation output now returns none when no operation was executed.
  • Removed deprecated output environment variable PULL_REQUEST_NUMBER. Please use the pull-request-number action output instead.

What's new

  • The action can now sign commits as github-actions[bot] when using GITHUB_TOKEN, or your own bot when using GitHub App tokens. See commit signing for details.
  • Action input draft now accepts a new value always-true. This will set the pull request to draft status when the pull request is updated, as well as on creation.
  • A new action input maintainer-can-modify indicates whether maintainers can modify the pull request. The default is true, which retains the existing behaviour of the action.
  • A new output pull-request-commits-verified returns true or false, indicating whether GitHub considers the signature of the branch's commits to be verified.

What's Changed

New Contributors

Full Changelog: https://github.com/peter-evans/create-pull-request/compare/v6.1.0...v7.0.0

Create Pull Request v6.1.0

✨ Adds pull-request-branch as an action output.

What's Changed

... (truncated)

Commits
  • 8867c4a fix: handle ambiguous argument failure on diff stat (#3312)
  • 6073f54 build(deps-dev): bump @​typescript-eslint/eslint-plugin (#3291)
  • 6d01b56 build(deps-dev): bump eslint-plugin-import from 2.29.1 to 2.30.0 (#3290)
  • 25cf845 build(deps-dev): bump @​typescript-eslint/parser from 7.17.0 to 7.18.0 (#3289)
  • d87b980 build(deps-dev): bump @​types/node from 18.19.46 to 18.19.48 (#3288)
  • 119d131 build(deps): bump peter-evans/create-pull-request from 6 to 7 (#3283)
  • 73e6230 docs: update readme
  • c0348e8 ci: add v7 to workflow
  • 4320041 feat: signed commits (v7) (#3057)
  • 0c2a66f build(deps-dev): bump ts-jest from 29.2.4 to 29.2.5 (#3256)
  • Additional commits viewable in compare view

[![Dependabot compatibility score](https://dependabot-badges.githubapp.com/badges/compatibility_score?dependency-name=peter-evans/create-pull-request&package-manager=github_actions&previous-version=6&new-version=7)](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores) Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) ---
Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/cargo-update.yml | 2 +- .github/workflows/cbmc-update.yml | 2 +- .github/workflows/toolchain-upgrade.yml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/cargo-update.yml b/.github/workflows/cargo-update.yml index d8bd170d1821..402b8ce634e7 100644 --- a/.github/workflows/cargo-update.yml +++ b/.github/workflows/cargo-update.yml @@ -37,7 +37,7 @@ jobs: git diff fi - name: Create Pull Request - uses: peter-evans/create-pull-request@v6 + uses: peter-evans/create-pull-request@v7 with: commit-message: Upgrade cargo dependencies to ${{ env.today }} branch: cargo-update-${{ env.today }} diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml index 5fe8a866c0e4..7b63c0dae7de 100644 --- a/.github/workflows/cbmc-update.yml +++ b/.github/workflows/cbmc-update.yml @@ -63,7 +63,7 @@ jobs: - name: Create Pull Request if: ${{ env.next_step == 'create_pr' }} - uses: peter-evans/create-pull-request@v6 + uses: peter-evans/create-pull-request@v7 with: commit-message: Upgrade CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} branch: cbmc-${{ env.CBMC_LATEST }} diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml index 76c3a5484414..8a7f448ca84e 100644 --- a/.github/workflows/toolchain-upgrade.yml +++ b/.github/workflows/toolchain-upgrade.yml @@ -38,7 +38,7 @@ jobs: - name: Create Pull Request id: create_pr if: ${{ env.next_step == 'create_pr' }} - uses: peter-evans/create-pull-request@v6 + uses: peter-evans/create-pull-request@v7 with: commit-message: Upgrade Rust toolchain to nightly-${{ env.next_toolchain_date }} branch: toolchain-${{ env.next_toolchain_date }}