From 068f63cc32ab638b039ef29e1fb061559efe14d6 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 12 Jul 2024 09:01:32 -0700 Subject: [PATCH] Improve performance and language support of memory initialization checks (#3313) This is a follow-up PR for #3264, a part of the larger work towards #3300. This PR introduces: - Use of demonic non-determinism (prophecy variables) to improve memory initialization checks performance; - Instead of keeping track of memory initialization of each possibly uninitialized byte pointed to by some pointer, one is chosen non-deterministically; - Tests for proper memory initialization checks injection for compiler intrinsics; - Separate functions for checking memory initialization of slice chunks. 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: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- .../codegen_cprover_gotoc/codegen/contract.rs | 2 +- .../codegen_cprover_gotoc/overrides/hooks.rs | 36 +++ .../src/kani_middle/transform/body.rs | 21 +- .../kani_middle/transform/check_uninit/mod.rs | 161 ++++++++-- .../transform/check_uninit/uninit_visitor.rs | 169 +++++----- .../kani_middle/transform/kani_intrinsics.rs | 6 +- .../src/kani_middle/transform/mod.rs | 8 +- kani-driver/src/call_single_file.rs | 5 +- library/kani/src/lib.rs | 24 ++ library/kani/src/mem.rs | 18 +- library/kani/src/mem_init.rs | 288 +++++++++++++----- library/kani_core/src/lib.rs | 24 ++ library/kani_core/src/mem.rs | 19 +- .../access-padding-uninit.rs | 2 +- .../access-padding-via-cast.rs | 2 +- .../uninit/alloc-to-slice/alloc-to-slice.rs | 4 +- tests/expected/uninit/atomic/atomic.rs | 31 ++ tests/expected/uninit/atomic/expected | 13 + tests/expected/uninit/intrinsics/expected | 70 +++++ .../expected/uninit/intrinsics/intrinsics.rs | 127 ++++++++ .../vec-read-bad-len/vec-read-bad-len.rs | 2 +- .../vec-read-semi-init/vec-read-semi-init.rs | 2 +- .../uninit/vec-read-uninit/vec-read-uninit.rs | 2 +- .../access-padding-enum-diverging-variants.rs | 2 +- .../access-padding-enum-multiple-variants.rs | 2 +- .../access-padding-enum-single-field.rs | 2 +- .../access-padding-enum-single-variant.rs | 2 +- tests/kani/Uninit/access-padding-init.rs | 15 + tests/kani/Uninit/alloc-to-slice.rs | 19 ++ tests/kani/Uninit/alloc-zeroed-to-slice.rs | 22 ++ tests/kani/Uninit/atomic.rs | 66 ++++ .../Uninit/struct-padding-and-arr-init.rs | 21 ++ tests/kani/Uninit/vec-read-init.rs | 11 + tests/perf/uninit/Cargo.toml | 14 - tests/perf/uninit/expected | 1 - tests/perf/uninit/src/lib.rs | 68 ----- tests/std-checks/core/slice.expected | 2 +- tests/std-checks/core/src/slice.rs | 20 +- 38 files changed, 1013 insertions(+), 290 deletions(-) create mode 100644 tests/expected/uninit/atomic/atomic.rs create mode 100644 tests/expected/uninit/atomic/expected create mode 100644 tests/expected/uninit/intrinsics/expected create mode 100644 tests/expected/uninit/intrinsics/intrinsics.rs create mode 100644 tests/kani/Uninit/access-padding-init.rs create mode 100644 tests/kani/Uninit/alloc-to-slice.rs create mode 100644 tests/kani/Uninit/alloc-zeroed-to-slice.rs create mode 100644 tests/kani/Uninit/atomic.rs create mode 100644 tests/kani/Uninit/struct-padding-and-arr-init.rs create mode 100644 tests/kani/Uninit/vec-read-init.rs delete mode 100644 tests/perf/uninit/Cargo.toml delete mode 100644 tests/perf/uninit/expected delete mode 100644 tests/perf/uninit/src/lib.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index d35015aa040d..c7e7d5b817bd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -122,7 +122,7 @@ impl<'tcx> GotocCtx<'tcx> { .tcx .all_diagnostic_items(()) .name_to_id - .get(&rustc_span::symbol::Symbol::intern("KaniMemInitShadowMem")) + .get(&rustc_span::symbol::Symbol::intern("KaniMemoryInitializationState")) .map(|attr_id| { self.tcx .symbol_name(rustc_middle::ty::Instance::mono(self.tcx, *attr_id)) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index fc245fc6f4c9..c0df279932f6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -143,6 +143,41 @@ impl GotocHook for Assert { } } +struct Check; +impl GotocHook for Check { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + matches_function(tcx, instance.def, "KaniCheck") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let cond = fargs.remove(0).cast_to(Type::bool()); + let msg = fargs.remove(0); + let msg = gcx.extract_const_message(&msg).unwrap(); + let target = target.unwrap(); + let caller_loc = gcx.codegen_caller_span_stable(span); + + let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span); + + Stmt::block( + vec![ + reach_stmt, + gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) + } +} + struct Nondet; impl GotocHook for Nondet { @@ -510,6 +545,7 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(Panic), Rc::new(Assume), Rc::new(Assert), + Rc::new(Check), Rc::new(Cover), Rc::new(Nondet), Rc::new(IsAllocated), diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 22895bd8d20d..d82dda80cc05 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -387,12 +387,13 @@ pub enum CheckType { } impl CheckType { - /// This will create the type of check that is available in the current crate. + /// This will create the type of check that is available in the current crate, attempting to + /// create a check that generates an assertion following by an assumption of the same assertion. /// /// If `kani` crate is available, this will return [CheckType::Assert], and the instance will /// point to `kani::assert`. Otherwise, we will collect the `core::panic_str` method and return /// [CheckType::Panic]. - pub fn new(tcx: TyCtxt) -> CheckType { + pub fn new_assert_assume(tcx: TyCtxt) -> CheckType { if let Some(instance) = find_instance(tcx, "KaniAssert") { CheckType::Assert(instance) } else if find_instance(tcx, "panic_str").is_some() { @@ -401,6 +402,22 @@ impl CheckType { CheckType::NoCore } } + + /// This will create the type of check that is available in the current crate, attempting to + /// create a check that generates an assertion, without assuming the condition afterwards. + /// + /// If `kani` crate is available, this will return [CheckType::Assert], and the instance will + /// point to `kani::assert`. Otherwise, we will collect the `core::panic_str` method and return + /// [CheckType::Panic]. + pub fn new_assert(tcx: TyCtxt) -> CheckType { + if let Some(instance) = find_instance(tcx, "KaniCheck") { + CheckType::Assert(instance) + } else if find_instance(tcx, "panic_str").is_some() { + CheckType::Panic + } else { + CheckType::NoCore + } + } } /// We store the index of an instruction to avoid borrow checker issues and unnecessary copies. 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 6665ab697287..e1b265751fd5 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -29,8 +29,17 @@ mod uninit_visitor; pub use ty_layout::{PointeeInfo, PointeeLayout}; use uninit_visitor::{CheckUninitVisitor, InitRelevantInstruction, MemoryInitOp}; -const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = - &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized"]; +// Function bodies of those functions will not be instrumented as not to cause infinite recursion. +const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = &[ + "KaniIsPtrInitialized", + "KaniSetPtrInitialized", + "KaniIsSliceChunkPtrInitialized", + "KaniSetSliceChunkPtrInitialized", + "KaniIsSlicePtrInitialized", + "KaniSetSlicePtrInitialized", + "KaniIsStrPtrInitialized", + "KaniSetStrPtrInitialized", +]; /// Instrument the code with checks for uninitialized memory. #[derive(Debug)] @@ -59,8 +68,8 @@ impl TransformPass for UninitPass { fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { trace!(function=?instance.name(), "transform"); - // Need to break infinite recursion when shadow memory checks are inserted, - // so the internal function responsible for shadow memory checks are skipped. + // Need to break infinite recursion when memory initialization checks are inserted, so the + // internal functions responsible for memory initialization are skipped. if tcx .get_diagnostic_name(rustc_internal::internal(tcx, instance.def.def_id())) .map(|diagnostic_name| { @@ -74,6 +83,11 @@ impl TransformPass for UninitPass { let mut new_body = MutableBody::from(body); let orig_len = new_body.blocks().len(); + // Inject a call to set-up memory initialization state if the function is a harness. + if is_harness(instance, tcx) { + inject_memory_init_setup(&mut new_body, tcx, &mut self.mem_init_fn_cache); + } + // Set of basic block indices for which analyzing first statement should be skipped. // // This is necessary because some checks are inserted before the source instruction, which, in @@ -159,10 +173,12 @@ impl UninitPass { }; match operation { - MemoryInitOp::Check { .. } => { + MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::Check { .. } => { self.build_get_and_check(tcx, body, source, operation, pointee_ty_info, skip_first) } - MemoryInitOp::Set { .. } | MemoryInitOp::SetRef { .. } => { + MemoryInitOp::SetSliceChunk { .. } + | MemoryInitOp::Set { .. } + | MemoryInitOp::SetRef { .. } => { self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first) } MemoryInitOp::Unsupported { .. } => { @@ -171,8 +187,8 @@ impl UninitPass { } } - /// Inject a load from shadow memory tracking memory initialization and an assertion that all - /// non-padding bytes are initialized. + /// Inject a load from memory initialization state and an assertion that all non-padding bytes + /// are initialized. fn build_get_and_check( &mut self, tcx: TyCtxt, @@ -189,18 +205,34 @@ impl UninitPass { let ptr_operand = operation.mk_operand(body, source); match pointee_info.layout() { PointeeLayout::Sized { layout } => { + let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); + // Depending on whether accessing the known number of elements in the slice, need to + // pass is as an argument. + let (diagnostic, args) = match &operation { + MemoryInitOp::Check { .. } => { + let diagnostic = "KaniIsPtrInitialized"; + let args = vec![ptr_operand.clone(), layout_operand]; + (diagnostic, args) + } + MemoryInitOp::CheckSliceChunk { .. } => { + let diagnostic = "KaniIsSliceChunkPtrInitialized"; + let args = + vec![ptr_operand.clone(), layout_operand, operation.expect_count()]; + (diagnostic, args) + } + _ => unreachable!(), + }; let is_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, "KaniIsPtrInitialized", &mut self.mem_init_fn_cache), + get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), layout.len(), *pointee_info.ty(), ); - let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); collect_skipped(&operation, body, skip_first); body.add_call( &is_ptr_initialized_instance, source, operation.position(), - vec![ptr_operand.clone(), layout_operand, operation.expect_count()], + args, ret_place.clone(), ); } @@ -252,8 +284,8 @@ impl UninitPass { ) } - /// Inject a store into shadow memory tracking memory initialization to initialize or - /// deinitialize all non-padding bytes. + /// Inject a store into memory initialization state to initialize or deinitialize all + /// non-padding bytes. fn build_set( &mut self, tcx: TyCtxt, @@ -272,27 +304,50 @@ impl UninitPass { match pointee_info.layout() { PointeeLayout::Sized { layout } => { + let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); + // Depending on whether writing to the known number of elements in the slice, need to + // pass is as an argument. + let (diagnostic, args) = match &operation { + MemoryInitOp::Set { .. } | MemoryInitOp::SetRef { .. } => { + let diagnostic = "KaniSetPtrInitialized"; + let args = vec![ + ptr_operand, + layout_operand, + Operand::Constant(ConstOperand { + span: source.span(body.blocks()), + user_ty: None, + const_: MirConst::from_bool(value), + }), + ]; + (diagnostic, args) + } + MemoryInitOp::SetSliceChunk { .. } => { + let diagnostic = "KaniSetSliceChunkPtrInitialized"; + let args = vec![ + ptr_operand, + layout_operand, + operation.expect_count(), + Operand::Constant(ConstOperand { + span: source.span(body.blocks()), + user_ty: None, + const_: MirConst::from_bool(value), + }), + ]; + (diagnostic, args) + } + _ => unreachable!(), + }; let set_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, "KaniSetPtrInitialized", &mut self.mem_init_fn_cache), + get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), layout.len(), *pointee_info.ty(), ); - let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); collect_skipped(&operation, body, skip_first); body.add_call( &set_ptr_initialized_instance, source, operation.position(), - vec![ - ptr_operand, - layout_operand, - operation.expect_count(), - Operand::Constant(ConstOperand { - span: source.span(body.blocks()), - user_ty: None, - const_: MirConst::from_bool(value), - }), - ], + args, ret_place, ); } @@ -426,3 +481,59 @@ pub fn resolve_mem_init_fn(fn_def: FnDef, layout_size: usize, associated_type: T ) .unwrap() } + +/// Checks if the instance is a harness -- an entry point of Kani analysis. +fn is_harness(instance: Instance, tcx: TyCtxt) -> bool { + let harness_identifiers = [ + vec![ + rustc_span::symbol::Symbol::intern("kanitool"), + rustc_span::symbol::Symbol::intern("proof_for_contract"), + ], + vec![ + rustc_span::symbol::Symbol::intern("kanitool"), + rustc_span::symbol::Symbol::intern("proof"), + ], + ]; + harness_identifiers.iter().any(|attr_path| { + tcx.has_attrs_with_path(rustc_internal::internal(tcx, instance.def.def_id()), attr_path) + }) +} + +/// Inject an initial call to set-up memory initialization tracking. +fn inject_memory_init_setup( + new_body: &mut MutableBody, + tcx: TyCtxt, + mem_init_fn_cache: &mut HashMap<&'static str, FnDef>, +) { + // First statement or terminator in the harness. + let mut source = if !new_body.blocks()[0].statements.is_empty() { + SourceInstruction::Statement { idx: 0, bb: 0 } + } else { + SourceInstruction::Terminator { bb: 0 } + }; + + // Dummy return place. + let ret_place = Place { + local: new_body.new_local( + Ty::new_tuple(&[]), + source.span(new_body.blocks()), + Mutability::Not, + ), + projection: vec![], + }; + + // Resolve the instance and inject a call to set-up the memory initialization state. + let memory_initialization_init = Instance::resolve( + get_mem_init_fn_def(tcx, "KaniInitializeMemoryInitializationState", mem_init_fn_cache), + &GenericArgs(vec![]), + ) + .unwrap(); + + new_body.add_call( + &memory_initialization_init, + &mut source, + InsertPosition::Before, + vec![], + ret_place, + ); +} diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs index 0614724be6bf..f68869e6681d 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs @@ -8,11 +8,11 @@ use stable_mir::mir::alloc::GlobalAlloc; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::visit::{Location, PlaceContext}; use stable_mir::mir::{ - BasicBlockIdx, CastKind, ConstOperand, LocalDecl, MirVisitor, Mutability, - NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, - StatementKind, Terminator, TerminatorKind, + BasicBlockIdx, CastKind, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand, + Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, + TerminatorKind, }; -use stable_mir::ty::{ConstantKind, MirConst, RigidTy, Span, Ty, TyKind, UintTy}; +use stable_mir::ty::{ConstantKind, RigidTy, Ty, TyKind}; use strum_macros::AsRefStr; use super::{PointeeInfo, PointeeLayout}; @@ -20,15 +20,21 @@ use super::{PointeeInfo, PointeeLayout}; /// Memory initialization operations: set or get memory initialization state for a given pointer. #[derive(AsRefStr, Clone, Debug)] 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 }, + /// 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 }, /// Check memory initialization of data bytes in a memory region starting from the pointer /// `operand` and of length `count * sizeof(operand)` bytes. - Check { 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. - Set { 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 `count * sizeof(operand)` bytes. - SetRef { operand: Operand, count: Operand, value: bool, position: InsertPosition }, + /// `operand` and of length `sizeof(operand)` bytes. + SetRef { operand: Operand, value: bool, position: InsertPosition }, /// Unsupported memory initialization operation. Unsupported { reason: String }, } @@ -39,9 +45,10 @@ impl MemoryInitOp { /// `MemoryInitOp::SetRef`. pub fn mk_operand(&self, body: &mut MutableBody, source: &mut SourceInstruction) -> Operand { match self { - MemoryInitOp::Check { operand, .. } | MemoryInitOp::Set { operand, .. } => { - operand.clone() - } + MemoryInitOp::Check { operand, .. } + | MemoryInitOp::Set { operand, .. } + | MemoryInitOp::CheckSliceChunk { operand, .. } + | MemoryInitOp::SetSliceChunk { operand, .. } => operand.clone(), MemoryInitOp::SetRef { operand, .. } => Operand::Copy(Place { local: { let place = match operand { @@ -62,24 +69,34 @@ impl MemoryInitOp { pub fn expect_count(&self) -> Operand { match self { - MemoryInitOp::Check { count, .. } - | MemoryInitOp::Set { count, .. } - | MemoryInitOp::SetRef { count, .. } => count.clone(), - MemoryInitOp::Unsupported { .. } => unreachable!(), + MemoryInitOp::CheckSliceChunk { count, .. } + | MemoryInitOp::SetSliceChunk { count, .. } => count.clone(), + MemoryInitOp::Check { .. } + | MemoryInitOp::Set { .. } + | MemoryInitOp::SetRef { .. } + | MemoryInitOp::Unsupported { .. } => unreachable!(), } } pub fn expect_value(&self) -> bool { match self { - MemoryInitOp::Set { value, .. } | MemoryInitOp::SetRef { value, .. } => *value, - MemoryInitOp::Check { .. } | MemoryInitOp::Unsupported { .. } => unreachable!(), + MemoryInitOp::Set { value, .. } + | MemoryInitOp::SetSliceChunk { value, .. } + | MemoryInitOp::SetRef { value, .. } => *value, + MemoryInitOp::Check { .. } + | MemoryInitOp::CheckSliceChunk { .. } + | MemoryInitOp::Unsupported { .. } => unreachable!(), } } pub fn position(&self) -> InsertPosition { match self { - MemoryInitOp::Set { position, .. } | MemoryInitOp::SetRef { position, .. } => *position, - MemoryInitOp::Check { .. } | MemoryInitOp::Unsupported { .. } => InsertPosition::Before, + MemoryInitOp::Set { position, .. } + | MemoryInitOp::SetSliceChunk { position, .. } + | MemoryInitOp::SetRef { position, .. } => *position, + MemoryInitOp::Check { .. } + | MemoryInitOp::CheckSliceChunk { .. } + | MemoryInitOp::Unsupported { .. } => InsertPosition::Before, } } } @@ -158,12 +175,12 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { self.super_statement(stmt, location); // Source is a *const T and it must be initialized. - self.push_target(MemoryInitOp::Check { + self.push_target(MemoryInitOp::CheckSliceChunk { operand: copy.src.clone(), count: copy.count.clone(), }); // Destimation is a *mut T so it gets initialized. - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: copy.dst.clone(), count: copy.count.clone(), value: true, @@ -188,7 +205,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { { self.push_target(MemoryInitOp::Check { operand: Operand::Copy(place_to_add_projections.clone()), - count: mk_const_operand(1, location.span()), }); }; } @@ -197,7 +213,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { if place_without_deref.ty(&self.locals).unwrap().kind().is_raw_ptr() { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place_without_deref), - count: mk_const_operand(1, location.span()), value: true, position: InsertPosition::After, }); @@ -208,7 +223,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { if let Rvalue::AddressOf(..) = rvalue { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), - count: mk_const_operand(1, location.span()), value: true, position: InsertPosition::After, }); @@ -219,7 +233,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { self.super_statement(stmt, location); self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), - count: mk_const_operand(1, location.span()), value: false, position: InsertPosition::After, }); @@ -263,8 +276,14 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { /* Intrinsics that can be safely skipped */ } name if name.starts_with("atomic") => { - let num_args = - if name.starts_with("atomic_cxchg") { 3 } else { 2 }; + let num_args = match name { + // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments. + name if name.starts_with("atomic_cxchg") => 3, + // All `atomic_load` intrinsics take `src` as an argument. + name if name.starts_with("atomic_load") => 1, + // All other `atomic` intrinsics take `dst, src` as arguments. + _ => 2, + }; assert_eq!( args.len(), num_args, @@ -276,7 +295,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { )); self.push_target(MemoryInitOp::Check { operand: args[0].clone(), - count: mk_const_operand(1, location.span()), }); } "compare_bytes" => { @@ -293,11 +311,11 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { args[1].ty(self.locals).unwrap().kind(), TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) )); - self.push_target(MemoryInitOp::Check { + self.push_target(MemoryInitOp::CheckSliceChunk { operand: args[0].clone(), count: args[2].clone(), }); - self.push_target(MemoryInitOp::Check { + self.push_target(MemoryInitOp::CheckSliceChunk { operand: args[1].clone(), count: args[2].clone(), }); @@ -318,11 +336,11 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { args[1].ty(self.locals).unwrap().kind(), TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) )); - self.push_target(MemoryInitOp::Check { + self.push_target(MemoryInitOp::CheckSliceChunk { operand: args[0].clone(), count: args[2].clone(), }); - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: args[1].clone(), count: args[2].clone(), value: true, @@ -345,29 +363,12 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { )); self.push_target(MemoryInitOp::Check { operand: args[0].clone(), - count: mk_const_operand(1, location.span()), }); self.push_target(MemoryInitOp::Check { operand: args[1].clone(), - count: mk_const_operand(1, location.span()), }); } - "unaligned_volatile_load" => { - assert_eq!( - args.len(), - 1, - "Unexpected number of arguments for `unaligned_volatile_load`" - ); - assert!(matches!( - args[0].ty(self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) - )); - self.push_target(MemoryInitOp::Check { - operand: args[0].clone(), - count: mk_const_operand(1, location.span()), - }); - } - "volatile_load" => { + "volatile_load" | "unaligned_volatile_load" => { assert_eq!( args.len(), 1, @@ -379,7 +380,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { )); self.push_target(MemoryInitOp::Check { operand: args[0].clone(), - count: mk_const_operand(1, location.span()), }); } "volatile_store" => { @@ -394,7 +394,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { )); self.push_target(MemoryInitOp::Set { operand: args[0].clone(), - count: mk_const_operand(1, location.span()), value: true, position: InsertPosition::After, }); @@ -409,7 +408,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { args[0].ty(self.locals).unwrap().kind(), TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) )); - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: args[0].clone(), count: args[2].clone(), value: true, @@ -432,7 +431,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } "alloc::alloc::__rust_alloc_zeroed" => { /* Memory is initialized here, need to update shadow memory. */ - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: Operand::Copy(destination.clone()), count: args[0].clone(), value: true, @@ -441,7 +440,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } "alloc::alloc::__rust_dealloc" => { /* Memory is uninitialized here, need to update shadow memory. */ - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: args[0].clone(), count: args[1].clone(), value: false, @@ -458,18 +457,30 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { TerminatorKind::Drop { place, .. } => { self.super_terminator(term, location); let place_ty = place.ty(&self.locals).unwrap(); - // When drop is codegen'ed, a reference is taken to the place which is later implicitly coerced to a pointer. - // Hence, we need to bless this pointer as initialized. - self.push_target(MemoryInitOp::SetRef { - operand: Operand::Copy(place.clone()), - count: mk_const_operand(1, location.span()), - value: true, - position: InsertPosition::Before, - }); + + // When drop is codegen'ed for types that could define their own dropping + // behavior, a reference is taken to the place which is later implicitly coerced + // to a pointer. Hence, we need to bless this pointer as initialized. + match place + .ty(&self.locals) + .unwrap() + .kind() + .rigid() + .expect("should be working with monomorphized code") + { + RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { + self.push_target(MemoryInitOp::SetRef { + operand: Operand::Copy(place.clone()), + value: true, + position: InsertPosition::Before, + }); + } + _ => {} + } + if place_ty.kind().is_raw_ptr() { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), - count: mk_const_operand(1, location.span()), value: false, position: InsertPosition::After, }); @@ -497,7 +508,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { if ptr_ty.kind().is_raw_ptr() { self.push_target(MemoryInitOp::Check { operand: Operand::Copy(intermediate_place.clone()), - count: mk_const_operand(1, location.span()), }); } } @@ -528,12 +538,14 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { if let ConstantKind::Allocated(allocation) = constant.const_.kind() { for (_, prov) in &allocation.provenance.ptrs { if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) { - self.push_target(MemoryInitOp::Set { - operand: Operand::Constant(constant.clone()), - count: mk_const_operand(1, location.span()), - value: true, - position: InsertPosition::Before, - }); + if constant.ty().kind().is_raw_ptr() { + // If a static is a raw pointer, need to mark it as initialized. + self.push_target(MemoryInitOp::Set { + operand: Operand::Constant(constant.clone()), + value: true, + position: InsertPosition::Before, + }); + } }; } } @@ -679,6 +691,12 @@ fn can_skip_intrinsic(intrinsic_name: &str) -> bool { /* SIMD operations */ true } + name if name.starts_with("atomic_fence") + || name.starts_with("atomic_singlethreadfence") => + { + /* Atomic fences */ + true + } "copy_nonoverlapping" => unreachable!( "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`" ), @@ -705,15 +723,6 @@ fn can_skip_intrinsic(intrinsic_name: &str) -> bool { } } -/// Create a constant operand with a given value and span. -fn mk_const_operand(value: usize, span: Span) -> Operand { - Operand::Constant(ConstOperand { - span, - user_ty: None, - const_: MirConst::try_from_uint(value as u128, UintTy::Usize).unwrap(), - }) -} - /// Try removing a topmost deref projection from a place if it exists, returning a place without it. fn try_remove_topmost_deref(place: &Place) -> Option { let mut new_place = place.clone(); diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index ea7bf8625228..c4534bf11b4d 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -216,11 +216,7 @@ impl IntrinsicGeneratorPass { &is_ptr_initialized_instance, &mut terminator, InsertPosition::Before, - vec![ - Operand::Copy(Place::from(1)), - layout_operand, - Operand::Copy(Place::from(2)), - ], + vec![Operand::Copy(Place::from(1)), layout_operand], Place::from(ret_var), ); } diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 56ab0be493c4..26a95978fcaf 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -60,7 +60,7 @@ impl BodyTransformation { inst_passes: vec![], cache: Default::default(), }; - let check_type = CheckType::new(tcx); + let check_type = CheckType::new_assert_assume(tcx); transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); // This has to come after stubs since we want this to replace the stubbed body. @@ -73,7 +73,11 @@ impl BodyTransformation { // generated code for future instrumentation passes. transformer.add_pass( queries, - UninitPass { check_type: check_type.clone(), mem_init_fn_cache: HashMap::new() }, + UninitPass { + // Since this uses demonic non-determinism under the hood, should not assume the assertion. + check_type: CheckType::new_assert(tcx), + mem_init_fn_cache: HashMap::new(), + }, ); transformer.add_pass( queries, diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 7cbe150427e9..411dabb5270e 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -140,7 +140,10 @@ impl KaniSession { } if self.args.common_args.unstable_features.contains(UnstableFeature::UninitChecks) { - flags.push("--ub-check=uninit".into()) + // Automatically enable shadow memory, since the version of uninitialized memory checks + // without non-determinism depends on it. + flags.push("-Z ghost-state".into()); + flags.push("--ub-check=uninit".into()); } if self.args.ignore_locals_lifetime { diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 6eab2a331811..7487cc26b186 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -123,6 +123,30 @@ pub const fn assert(cond: bool, msg: &'static str) { assert!(cond, "{}", msg); } +/// Creates an assertion of the specified condition, but does not assume it afterwards. +/// +/// # Example: +/// +/// ```rust +/// let x: bool = kani::any(); +/// let y = !x; +/// kani::check(x || y, "ORing a boolean variable with its negation must be true") +/// ``` +#[cfg(not(feature = "concrete_playback"))] +#[inline(never)] +#[rustc_diagnostic_item = "KaniCheck"] +pub const fn check(cond: bool, msg: &'static str) { + let _ = cond; + let _ = msg; +} + +#[cfg(feature = "concrete_playback")] +#[inline(never)] +#[rustc_diagnostic_item = "KaniCheck"] +pub const fn check(cond: bool, msg: &'static str) { + assert!(cond, "{}", msg); +} + /// Creates a cover property with the specified condition and message. /// /// # Example: diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 0b390e74288d..f861f6b2ba25 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -118,9 +118,11 @@ where ::Metadata: PtrProperties, { let (thin_ptr, metadata) = ptr.to_raw_parts(); + // Need to assert `is_initialized` because non-determinism is used under the hood, so it does + // not make sense to use it inside assumption context. metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) - && is_initialized(ptr, 1) + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -148,7 +150,11 @@ where ::Metadata: PtrProperties, { let (thin_ptr, metadata) = ptr.to_raw_parts(); - is_inbounds(&metadata, thin_ptr) && is_initialized(ptr, 1) && unsafe { has_valid_value(ptr) } + // Need to assert `is_initialized` because non-determinism is used under the hood, so it does + // not make sense to use it inside assumption context. + is_inbounds(&metadata, thin_ptr) + && assert_is_initialized(ptr) + && unsafe { has_valid_value(ptr) } } /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. @@ -294,10 +300,16 @@ unsafe fn has_valid_value(_ptr: *const T) -> bool { /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. #[rustc_diagnostic_item = "KaniIsInitialized"] #[inline(never)] -pub fn is_initialized(_ptr: *const T, _len: usize) -> bool { +pub fn is_initialized(_ptr: *const T) -> bool { kani_intrinsic() } +/// A helper to assert `is_initialized` to use it as a part of other predicates. +fn assert_is_initialized(ptr: *const T) -> bool { + crate::check(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer"); + true +} + /// Get the object ID of the given pointer. #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index 37832ea32604..a09e515d7e17 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -1,20 +1,23 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module uses shadow memory API to track memory initialization of raw pointers. +//! This module provides instrumentation for tracking memory initialization of raw pointers. //! //! Currently, memory initialization is tracked on per-byte basis, so each byte of memory pointed to -//! by raw pointers could be either initialized or uninitialized. Compiler automatically inserts -//! calls to `is_xxx_initialized` and `set_xxx_initialized` at appropriate locations to get or set -//! the initialization status of the memory pointed to. Padding bytes are always considered -//! uninitialized: type layout is determined at compile time and statically injected into the -//! program (see `Layout`). +//! by raw pointers could be either initialized or uninitialized. Padding bytes are always +//! considered uninitialized when read as data bytes. Each type has a type layout to specify which +//! bytes are considered to be data and which -- padding. This is determined at compile time and +//! statically injected into the program (see `Layout`). +//! +//! Compiler automatically inserts calls to `is_xxx_initialized` and `set_xxx_initialized` at +//! appropriate locations to get or set the initialization status of the memory pointed to. +//! +//! Note that for each harness, tracked object and tracked offset are chosen non-deterministically, +//! so calls to `is_xxx_initialized` should be only used in assertion contexts. // Definitions in this module are not meant to be visible to the end user, only the compiler. #![allow(dead_code)] -use crate::shadow::ShadowMem; - /// Bytewise mask, representing which bytes of a type are data and which are padding. /// For example, for a type like this: /// ``` @@ -25,98 +28,243 @@ use crate::shadow::ShadowMem; /// } /// ``` /// the layout would be [true, true, true, false]; -type Layout = [bool; N]; - -/// Global shadow memory object for tracking memory initialization. -#[rustc_diagnostic_item = "KaniMemInitShadowMem"] -static mut MEM_INIT_SHADOW_MEM: ShadowMem = ShadowMem::new(false); - -/// Get initialization state of `len` items laid out according to the `layout` starting at address `ptr`. -#[rustc_diagnostic_item = "KaniIsUnitPtrInitialized"] -fn is_unit_ptr_initialized(ptr: *const (), layout: Layout, len: usize) -> bool { - let mut count: usize = 0; - while count < len { - let mut offset: usize = 0; - while offset < N { - unsafe { - if layout[offset] - && !MEM_INIT_SHADOW_MEM.get((ptr as *const u8).add(count * N + offset)) - { - return false; - } - offset += 1; - } +type Layout = [bool; LAYOUT_SIZE]; + +/// Currently tracked non-deterministically chosen memory initialization state. +struct MemoryInitializationState { + pub tracked_object_id: usize, + pub tracked_offset: usize, + pub value: bool, +} + +impl MemoryInitializationState { + /// This is a dummy initialization function -- the values will be eventually overwritten by a + /// call to `initialize_memory_initialization_state`. + pub const fn new() -> Self { + Self { tracked_object_id: 0, tracked_offset: 0, value: false } + } + + /// Return currently tracked memory initialization state if `ptr` points to the currently + /// tracked object and the tracked offset lies within `LAYOUT_SIZE` bytes of `ptr`. Return + /// `true` otherwise. + /// + /// Such definition is necessary since both tracked object and tracked offset are chosen + /// non-deterministically. + pub fn get( + &mut self, + ptr: *const u8, + layout: Layout, + ) -> bool { + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + if self.tracked_object_id == obj + && self.tracked_offset >= offset + && self.tracked_offset < offset + LAYOUT_SIZE + { + !layout[(self.tracked_offset - offset) % LAYOUT_SIZE] || self.value + } else { + true } - count += 1; } - true -} -/// Set initialization state to `value` for `len` items laid out according to the `layout` starting at address `ptr`. -#[rustc_diagnostic_item = "KaniSetUnitPtrInitialized"] -fn set_unit_ptr_initialized( - ptr: *const (), - layout: Layout, - len: usize, - value: bool, -) { - let mut count: usize = 0; - while count < len { - let mut offset: usize = 0; - while offset < N { - unsafe { - MEM_INIT_SHADOW_MEM - .set((ptr as *const u8).add(count * N + offset), value && layout[offset]); - } - offset += 1; + /// Set currently tracked memory initialization state if `ptr` points to the currently tracked + /// object and the tracked offset lies within `LAYOUT_SIZE` bytes of `ptr`. Do nothing + /// otherwise. + /// + /// Such definition is necessary since both tracked object and tracked offset are chosen + /// non-deterministically. + pub fn set( + &mut self, + ptr: *const u8, + layout: Layout, + value: bool, + ) { + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + if self.tracked_object_id == obj + && self.tracked_offset >= offset + && self.tracked_offset < offset + LAYOUT_SIZE + { + self.value = layout[(self.tracked_offset - offset) % LAYOUT_SIZE] && value; + } + } + + /// Return currently tracked memory initialization state if `ptr` points to the currently + /// tracked object and the tracked offset lies within `LAYOUT_SIZE * num_elts` bytes of `ptr`. + /// Return `true` otherwise. + /// + /// Such definition is necessary since both tracked object and tracked offset are chosen + /// non-deterministically. + pub fn get_slice( + &mut self, + ptr: *const u8, + layout: Layout, + num_elts: usize, + ) -> bool { + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + if self.tracked_object_id == obj + && self.tracked_offset >= offset + && self.tracked_offset < offset + num_elts * LAYOUT_SIZE + { + !layout[(self.tracked_offset - offset) % LAYOUT_SIZE] || self.value + } else { + true + } + } + + /// Set currently tracked memory initialization state if `ptr` points to the currently tracked + /// object and the tracked offset lies within `LAYOUT_SIZE * num_elts` bytes of `ptr`. Do + /// nothing otherwise. + /// + /// Such definition is necessary since both tracked object and tracked offset are chosen + /// non-deterministically. + pub fn set_slice( + &mut self, + ptr: *const u8, + layout: Layout, + num_elts: usize, + value: bool, + ) { + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + if self.tracked_object_id == obj + && self.tracked_offset >= offset + && self.tracked_offset < offset + num_elts * LAYOUT_SIZE + { + self.value = layout[(self.tracked_offset - offset) % LAYOUT_SIZE] && value; } - count += 1; } } -/// Get initialization state of `len` items laid out according to the `layout` starting at address `ptr`. +/// 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. +#[rustc_diagnostic_item = "KaniInitializeMemoryInitializationState"] +fn initialize_memory_initialization_state() { + unsafe { + MEM_INIT_STATE.tracked_object_id = crate::any(); + MEM_INIT_STATE.tracked_offset = crate::any(); + MEM_INIT_STATE.value = false; + } +} + +/// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`. #[rustc_diagnostic_item = "KaniIsPtrInitialized"] -fn is_ptr_initialized(ptr: *const T, layout: Layout, len: usize) -> bool { +fn is_ptr_initialized( + ptr: *const T, + layout: Layout, +) -> bool { + if LAYOUT_SIZE == 0 { + return true; + } let (ptr, _) = ptr.to_raw_parts(); - is_unit_ptr_initialized(ptr, layout, len) + unsafe { MEM_INIT_STATE.get(ptr as *const u8, layout) } } -/// Set initialization state to `value` for `len` items laid out according to the `layout` starting at address `ptr`. +/// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`. #[rustc_diagnostic_item = "KaniSetPtrInitialized"] -fn set_ptr_initialized( +fn set_ptr_initialized( + ptr: *const T, + layout: Layout, + value: bool, +) { + if LAYOUT_SIZE == 0 { + return; + } + let (ptr, _) = ptr.to_raw_parts(); + unsafe { + MEM_INIT_STATE.set(ptr as *const u8, layout, value); + } +} + +/// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`. +#[rustc_diagnostic_item = "KaniIsSliceChunkPtrInitialized"] +fn is_slice_chunk_ptr_initialized( + ptr: *const T, + layout: Layout, + num_elts: usize, +) -> bool { + if LAYOUT_SIZE == 0 { + return true; + } + let (ptr, _) = ptr.to_raw_parts(); + unsafe { MEM_INIT_STATE.get_slice(ptr as *const u8, layout, num_elts) } +} + +/// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`. +#[rustc_diagnostic_item = "KaniSetSliceChunkPtrInitialized"] +fn set_slice_chunk_ptr_initialized( ptr: *const T, - layout: Layout, - len: usize, + layout: Layout, + num_elts: usize, value: bool, ) { + if LAYOUT_SIZE == 0 { + return; + } let (ptr, _) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, len, value); + unsafe { + MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value); + } } /// Get initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr`. #[rustc_diagnostic_item = "KaniIsSlicePtrInitialized"] -fn is_slice_ptr_initialized(ptr: *const [T], layout: Layout) -> bool { - let (ptr, len) = ptr.to_raw_parts(); - is_unit_ptr_initialized(ptr, layout, len) +fn is_slice_ptr_initialized( + ptr: *const [T], + layout: Layout, +) -> bool { + if LAYOUT_SIZE == 0 { + return true; + } + let (ptr, num_elts) = ptr.to_raw_parts(); + unsafe { MEM_INIT_STATE.get_slice(ptr as *const u8, layout, num_elts) } } /// Set initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`. #[rustc_diagnostic_item = "KaniSetSlicePtrInitialized"] -fn set_slice_ptr_initialized(ptr: *const [T], layout: Layout, value: bool) { - let (ptr, len) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, len, value); +fn set_slice_ptr_initialized( + ptr: *const [T], + layout: Layout, + value: bool, +) { + if LAYOUT_SIZE == 0 { + return; + } + let (ptr, num_elts) = ptr.to_raw_parts(); + unsafe { + MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value); + } } /// Get initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr`. #[rustc_diagnostic_item = "KaniIsStrPtrInitialized"] -fn is_str_ptr_initialized(ptr: *const str, layout: Layout) -> bool { - let (ptr, len) = ptr.to_raw_parts(); - is_unit_ptr_initialized(ptr, layout, len) +fn is_str_ptr_initialized( + ptr: *const str, + layout: Layout, +) -> bool { + if LAYOUT_SIZE == 0 { + return true; + } + let (ptr, num_elts) = ptr.to_raw_parts(); + unsafe { MEM_INIT_STATE.get_slice(ptr as *const u8, layout, num_elts) } } /// Set initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`. #[rustc_diagnostic_item = "KaniSetStrPtrInitialized"] -fn set_str_ptr_initialized(ptr: *const str, layout: Layout, value: bool) { - let (ptr, len) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, len, value); +fn set_str_ptr_initialized( + ptr: *const str, + layout: Layout, + value: bool, +) { + if LAYOUT_SIZE == 0 { + return; + } + let (ptr, num_elts) = ptr.to_raw_parts(); + unsafe { + MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value); + } } diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 143fbb7ef825..68a8e79658f1 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -124,6 +124,30 @@ macro_rules! kani_intrinsics { assert!(cond, "{}", msg); } + /// Creates an assertion of the specified condition and message, but does not assume it afterwards. + /// + /// # Example: + /// + /// ```rust + /// let x: bool = kani::any(); + /// let y = !x; + /// kani::check(x || y, "ORing a boolean variable with its negation must be true") + /// ``` + #[cfg(not(feature = "concrete_playback"))] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + pub const fn check(cond: bool, msg: &'static str) { + let _ = cond; + let _ = msg; + } + + #[cfg(feature = "concrete_playback")] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + pub const fn check(cond: bool, msg: &'static str) { + assert!(cond, "{}", msg); + } + /// Creates a cover property with the specified condition and message. /// /// # Example: diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 3b10856765a5..bcf4cd2248a6 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -123,9 +123,11 @@ macro_rules! kani_mem { ::Metadata: PtrProperties, { let (thin_ptr, metadata) = ptr.to_raw_parts(); + // Need to assert `is_initialized` because non-determinism is used under the hood, so it + // does not make sense to use it inside assumption context. metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) - && is_initialized(ptr, 1) + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -154,8 +156,10 @@ macro_rules! kani_mem { ::Metadata: PtrProperties, { let (thin_ptr, metadata) = ptr.to_raw_parts(); + // Need to assert `is_initialized` because non-determinism is used under the hood, so it + // does not make sense to use it inside assumption context. is_inbounds(&metadata, thin_ptr) - && is_initialized(ptr, 1) + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -302,10 +306,19 @@ macro_rules! kani_mem { /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. #[rustc_diagnostic_item = "KaniIsInitialized"] #[inline(never)] - pub fn is_initialized(_ptr: *const T, _len: usize) -> bool { + pub fn is_initialized(_ptr: *const T) -> bool { kani_intrinsic() } + /// A helper to assert `is_initialized` to use it as a part of other predicates. + fn assert_is_initialized(ptr: *const T) -> bool { + super::check( + is_initialized(ptr), + "Undefined Behavior: Reading from an uninitialized pointer", + ); + true + } + /// Get the object ID of the given pointer. #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs index d6e735e219ad..8e65b95aefa2 100644 --- a/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr::addr_of; diff --git a/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs b/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs index b73bebc827bc..1604625fc54c 100644 --- a/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs +++ b/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; #[repr(C)] diff --git a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs index 3c4420f5791f..318f234c31be 100644 --- a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs +++ b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks -use std::alloc::{alloc, dealloc, Layout}; +use std::alloc::{alloc, Layout}; use std::slice::from_raw_parts; /// Checks that Kani catches an attempt to form a slice from uninitialized memory. diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs new file mode 100644 index 000000000000..63c85af41a3f --- /dev/null +++ b/tests/expected/uninit/atomic/atomic.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +#![feature(core_intrinsics)] + +use std::alloc::{alloc, Layout}; +use std::sync::atomic::{AtomicU8, Ordering}; + +// Checks if memory initialization checks correctly fail when uninitialized memory is passed to +// atomic intrinsics. +#[kani::proof] +fn local_atomic_uninit() { + // Get a pointer to an uninitialized value + let layout = Layout::from_size_align(16, 8).unwrap(); + let ptr: *mut u8 = unsafe { alloc(layout) }; + // Try accessing `ptr` via atomic intrinsics, should be UB in each case. + unsafe { + match kani::any() { + 0 => { + std::intrinsics::atomic_store_relaxed(ptr, 1); + } + 1 => { + std::intrinsics::atomic_load_relaxed(ptr as *const u8); + } + _ => { + std::intrinsics::atomic_cxchg_relaxed_relaxed(ptr, 1, 1); + } + }; + } +} diff --git a/tests/expected/uninit/atomic/expected b/tests/expected/uninit/atomic/expected new file mode 100644 index 000000000000..c7d9593f22a7 --- /dev/null +++ b/tests/expected/uninit/atomic/expected @@ -0,0 +1,13 @@ +SUMMARY: + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8` + +VERIFICATION:- FAILED + +Summary:\ +Verification failed for - local_atomic_uninit\ +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected new file mode 100644 index 000000000000..ffa98b6f1140 --- /dev/null +++ b/tests/expected/uninit/intrinsics/expected @@ -0,0 +1,70 @@ +Checking harness check_typed_swap_safe... + +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. + +VERIFICATION:- FAILED + +Checking harness check_typed_swap... + +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8` + +VERIFICATION:- FAILED + +Checking harness check_volatile_store_and_load_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_volatile_load... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +VERIFICATION:- FAILED + +Checking harness check_write_bytes_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_compare_bytes_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_compare_bytes... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +VERIFICATION:- FAILED + +Checking harness check_copy_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_copy... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +VERIFICATION:- FAILED + +Checking harness check_copy_nonoverlapping_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_copy_nonoverlapping... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +VERIFICATION:- FAILED + +Summary: +Verification failed for - check_typed_swap_safe +Verification failed for - check_typed_swap +Verification failed for - check_volatile_load +Verification failed for - check_compare_bytes +Verification failed for - check_copy +Verification failed for - check_copy_nonoverlapping +Complete - 5 successfully verified harnesses, 6 failures, 11 total. diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs new file mode 100644 index 000000000000..aa8a89b7b959 --- /dev/null +++ b/tests/expected/uninit/intrinsics/intrinsics.rs @@ -0,0 +1,127 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks +//! Checks that Kani supports memory initialization checks via intrinsics. + +#![feature(core_intrinsics)] + +use std::alloc::{alloc, alloc_zeroed, Layout}; +use std::intrinsics::*; + +#[kani::proof] +fn check_copy_nonoverlapping() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + let dst: *mut u8 = alloc(layout); + copy_nonoverlapping(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized. + } +} + +#[kani::proof] +fn check_copy_nonoverlapping_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc_zeroed(layout); + let dst: *mut u8 = alloc(layout); + // `src` is initialized here, `dst` is uninitialized, but it is fine since we are writing into it. + copy_nonoverlapping(src as *const u8, dst, 2); + } +} + +#[kani::proof] +fn check_copy() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + let dst: *mut u8 = alloc(layout); + copy(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized. + } +} + +#[kani::proof] +fn check_copy_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc_zeroed(layout); + let dst: *mut u8 = alloc(layout); + // `src` is initialized here, `dst` is uninitialized, but it is fine since we are writing into it. + copy(src as *const u8, dst, 2); + } +} + +#[kani::proof] +fn check_compare_bytes() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc(layout); + let right: *mut u8 = alloc(layout); + // ~ERROR: Accessing `left` and `right` here, both of which are uninitialized. + compare_bytes(left as *const u8, right as *const u8, 2); + } +} + +#[kani::proof] +fn check_compare_bytes_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc_zeroed(layout); + let right: *mut u8 = alloc_zeroed(layout); + // Both `left` and `right` are initialized here. + compare_bytes(left as *const u8, right as *const u8, 2); + } +} + +#[kani::proof] +fn check_write_bytes_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc(layout); + let right: *mut u8 = alloc(layout); + write_bytes(left, 0, 2); + write_bytes(right, 0, 2); + // Both `left` and `right` are initialized here. + compare_bytes(left as *const u8, right as *const u8, 2); + } +} + +#[kani::proof] +fn check_volatile_load() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + volatile_load(src as *const u8); // ~ERROR: Accessing `src` here, which is uninitialized. + } +} + +#[kani::proof] +fn check_volatile_store_and_load_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + volatile_store(src, 0); + volatile_load(src as *const u8); // `src` is initialized here. + } +} + +#[kani::proof] +fn check_typed_swap() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc(layout); + let right: *mut u8 = alloc(layout); + // ~ERROR: Accessing `left` and `right` here, both of which are uninitialized. + typed_swap(left, right); + } +} + +#[kani::proof] +fn check_typed_swap_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc_zeroed(layout); + let right: *mut u8 = alloc_zeroed(layout); + // Both `left` and `right` are initialized here. + typed_swap(left, right); + } +} diff --git a/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs b/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs index 9778bb11a277..f5cae82c5350 100644 --- a/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs +++ b/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ops::Index; diff --git a/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs b/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs index 4330f5f53023..2e007cabaced 100644 --- a/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs +++ b/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks /// Checks that Kani catches an attempt to read uninitialized memory from a semi-initialized vector. #[kani::proof] diff --git a/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs b/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs index c322b4d33bb2..e6daf80cd5e3 100644 --- a/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs +++ b/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks /// Checks that Kani catches an attempt to read uninitialized memory from an uninitialized vector. #[kani::proof] diff --git a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs b/tests/kani/Uninit/access-padding-enum-diverging-variants.rs index 7feb493a5b3f..fae491c40622 100644 --- a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs +++ b/tests/kani/Uninit/access-padding-enum-diverging-variants.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; use std::ptr::addr_of; diff --git a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs b/tests/kani/Uninit/access-padding-enum-multiple-variants.rs index fb8fae06ca59..dd6942252cb2 100644 --- a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs +++ b/tests/kani/Uninit/access-padding-enum-multiple-variants.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; use std::ptr::addr_of; diff --git a/tests/kani/Uninit/access-padding-enum-single-field.rs b/tests/kani/Uninit/access-padding-enum-single-field.rs index c283b603f705..63f7f6043905 100644 --- a/tests/kani/Uninit/access-padding-enum-single-field.rs +++ b/tests/kani/Uninit/access-padding-enum-single-field.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; use std::ptr::addr_of; diff --git a/tests/kani/Uninit/access-padding-enum-single-variant.rs b/tests/kani/Uninit/access-padding-enum-single-variant.rs index f33cfe7ce6fb..bb87d36d26c8 100644 --- a/tests/kani/Uninit/access-padding-enum-single-variant.rs +++ b/tests/kani/Uninit/access-padding-enum-single-variant.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; use std::ptr::addr_of; diff --git a/tests/kani/Uninit/access-padding-init.rs b/tests/kani/Uninit/access-padding-init.rs new file mode 100644 index 000000000000..7523622a6106 --- /dev/null +++ b/tests/kani/Uninit/access-padding-init.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::ptr::addr_of; + +#[repr(C)] +struct S(u32, u8); + +#[kani::proof] +fn access_padding_init() { + let s = S(0, 0); + let ptr: *const u8 = addr_of!(s) as *const u8; + let data = unsafe { *(ptr.add(3)) }; // Accessing data bytes is valid. +} diff --git a/tests/kani/Uninit/alloc-to-slice.rs b/tests/kani/Uninit/alloc-to-slice.rs new file mode 100644 index 000000000000..863d3b40b390 --- /dev/null +++ b/tests/kani/Uninit/alloc-to-slice.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::alloc::{alloc, Layout}; + +#[kani::proof] +fn alloc_to_slice() { + let layout = Layout::from_size_align(32, 8).unwrap(); + unsafe { + let ptr = alloc(layout); + *ptr = 0x41; + *ptr.add(1) = 0x42; + *ptr.add(2) = 0x43; + *ptr.add(3) = 0x44; + *ptr.add(16) = 0x00; + let val = *(ptr.add(2)); // Accessing previously initialized byte is valid. + } +} diff --git a/tests/kani/Uninit/alloc-zeroed-to-slice.rs b/tests/kani/Uninit/alloc-zeroed-to-slice.rs new file mode 100644 index 000000000000..d00ca4c6abff --- /dev/null +++ b/tests/kani/Uninit/alloc-zeroed-to-slice.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::alloc::{alloc_zeroed, Layout}; +use std::slice::from_raw_parts; + +#[kani::proof] +fn alloc_zeroed_to_slice() { + let layout = Layout::from_size_align(32, 8).unwrap(); + unsafe { + // This returns initialized memory, so any further accesses are valid. + let ptr = alloc_zeroed(layout); + *ptr = 0x41; + *ptr.add(1) = 0x42; + *ptr.add(2) = 0x43; + *ptr.add(3) = 0x44; + *ptr.add(16) = 0x00; + let slice1 = from_raw_parts(ptr, 16); + let slice2 = from_raw_parts(ptr.add(16), 16); + } +} diff --git a/tests/kani/Uninit/atomic.rs b/tests/kani/Uninit/atomic.rs new file mode 100644 index 000000000000..376f365d408c --- /dev/null +++ b/tests/kani/Uninit/atomic.rs @@ -0,0 +1,66 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::sync::atomic::{AtomicUsize, Ordering}; + +fn any_ordering() -> Ordering { + match kani::any() { + 0 => Ordering::Relaxed, + 1 => Ordering::Release, + 2 => Ordering::Acquire, + 3 => Ordering::AcqRel, + _ => Ordering::SeqCst, + } +} + +fn store_ordering() -> Ordering { + match kani::any() { + 0 => Ordering::Relaxed, + 1 => Ordering::Release, + _ => Ordering::SeqCst, + } +} + +fn load_ordering() -> Ordering { + match kani::any() { + 0 => Ordering::Relaxed, + 1 => Ordering::Acquire, + _ => Ordering::SeqCst, + } +} + +static GLOBAL_ATOMIC: AtomicUsize = AtomicUsize::new(0); + +// Checks if memory initialization checks work with atomics defined in the global scope. +#[kani::proof] +fn global_atomic() { + let old_value = GLOBAL_ATOMIC.fetch_add(1, any_ordering()); +} + +// Checks if memory initialization checks work with atomics. +#[kani::proof] +fn local_atomic() { + // Get a pointer to an allocated value + let ptr: *mut usize = Box::into_raw(Box::new(0)); + + // Create an atomic from the allocated value + let atomic = unsafe { AtomicUsize::from_ptr(ptr) }; + + // Use `atomic` for atomic operations + atomic.store(1, store_ordering()); + let old_val = atomic.load(load_ordering()); + let old_val = atomic.swap(2, any_ordering()); + + // Deallocate the value + unsafe { drop(Box::from_raw(ptr)) } +} + +// Checks if memory initialization checks work with compare-and-swap atomics. +#[kani::proof] +fn compare_exchange_atomic() { + // Create an atomic. + let some_var = AtomicUsize::new(5); + // Perform a `compare-and-swap` operation. + some_var.compare_exchange(5, 10, any_ordering(), load_ordering()); +} diff --git a/tests/kani/Uninit/struct-padding-and-arr-init.rs b/tests/kani/Uninit/struct-padding-and-arr-init.rs new file mode 100644 index 000000000000..c67b1177bfa3 --- /dev/null +++ b/tests/kani/Uninit/struct-padding-and-arr-init.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::ptr::addr_of_mut; + +#[repr(C)] +struct S(u32, u8); + +#[kani::proof] +fn struct_padding_and_arr_init() { + unsafe { + let mut s = S(0, 0); + let sptr = addr_of_mut!(s); + let sptr2 = sptr as *mut [u8; 4]; + *sptr2 = [0; 4]; + *sptr = S(0, 0); + // Both S(u32, u8) and [u8; 4] have the same layout, so the memory is initialized. + let val = *sptr2; + } +} diff --git a/tests/kani/Uninit/vec-read-init.rs b/tests/kani/Uninit/vec-read-init.rs new file mode 100644 index 000000000000..78812c59830e --- /dev/null +++ b/tests/kani/Uninit/vec-read-init.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +#[kani::proof] +fn vec_read_init() { + let mut v: Vec = Vec::with_capacity(10); + unsafe { *v.as_mut_ptr().add(5) = 0x42 }; + let def = unsafe { *v.as_ptr().add(5) }; // Accessing previously initialized byte is valid. + let x = def + 1; +} diff --git a/tests/perf/uninit/Cargo.toml b/tests/perf/uninit/Cargo.toml deleted file mode 100644 index 9f44cb3fe103..000000000000 --- a/tests/perf/uninit/Cargo.toml +++ /dev/null @@ -1,14 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "uninit" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] - -[package.metadata.kani] -unstable = { ghost-state = true, uninit-checks = true } diff --git a/tests/perf/uninit/expected b/tests/perf/uninit/expected deleted file mode 100644 index f7b4fd303a77..000000000000 --- a/tests/perf/uninit/expected +++ /dev/null @@ -1 +0,0 @@ -Complete - 5 successfully verified harnesses, 0 failures, 5 total. \ No newline at end of file diff --git a/tests/perf/uninit/src/lib.rs b/tests/perf/uninit/src/lib.rs deleted file mode 100644 index 86b101c0e5d8..000000000000 --- a/tests/perf/uninit/src/lib.rs +++ /dev/null @@ -1,68 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use std::alloc::{alloc, alloc_zeroed, Layout}; -use std::ptr; -use std::ptr::addr_of; -use std::slice::from_raw_parts; - -#[repr(C)] -struct S(u32, u8); - -#[kani::proof] -fn access_padding_init() { - let s = S(0, 0); - let ptr: *const u8 = addr_of!(s) as *const u8; - let data = unsafe { *(ptr.add(3)) }; // Accessing data bytes is valid. -} - -#[kani::proof] -fn alloc_to_slice() { - let layout = Layout::from_size_align(32, 8).unwrap(); - unsafe { - let ptr = alloc(layout); - *ptr = 0x41; - *ptr.add(1) = 0x42; - *ptr.add(2) = 0x43; - *ptr.add(3) = 0x44; - *ptr.add(16) = 0x00; - let val = *(ptr.add(2)); // Accessing previously initialized byte is valid. - } -} - -#[kani::proof] -fn alloc_zeroed_to_slice() { - let layout = Layout::from_size_align(32, 8).unwrap(); - unsafe { - // This returns initialized memory, so any further accesses are valid. - let ptr = alloc_zeroed(layout); - *ptr = 0x41; - *ptr.add(1) = 0x42; - *ptr.add(2) = 0x43; - *ptr.add(3) = 0x44; - *ptr.add(16) = 0x00; - let slice1 = from_raw_parts(ptr, 16); - let slice2 = from_raw_parts(ptr.add(16), 16); - } -} - -#[kani::proof] -fn struct_padding_and_arr_init() { - unsafe { - let mut s = S(0, 0); - let sptr = ptr::addr_of_mut!(s); - let sptr2 = sptr as *mut [u8; 4]; - *sptr2 = [0; 4]; - *sptr = S(0, 0); - // Both S(u32, u8) and [u8; 4] have the same layout, so the memory is initialized. - let val = *sptr2; - } -} - -#[kani::proof] -fn vec_read_init() { - let mut v: Vec = Vec::with_capacity(10); - unsafe { *v.as_mut_ptr().add(5) = 0x42 }; - let def = unsafe { *v.as_ptr().add(5) }; // Accessing previously initialized byte is valid. - let x = def + 1; -} diff --git a/tests/std-checks/core/slice.expected b/tests/std-checks/core/slice.expected index 01a90d50b557..4426ff6c02cd 100644 --- a/tests/std-checks/core/slice.expected +++ b/tests/std-checks/core/slice.expected @@ -1 +1 @@ -Complete - 1 successfully verified harnesses, 0 failures, 1 total. +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/std-checks/core/src/slice.rs b/tests/std-checks/core/src/slice.rs index 044f4bd38586..fe627f21a5ae 100644 --- a/tests/std-checks/core/src/slice.rs +++ b/tests/std-checks/core/src/slice.rs @@ -1,25 +1,30 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +extern crate kani; + /// Create wrapper functions to standard library functions that contains their contract. pub mod contracts { use kani::{mem::*, requires}; #[requires(can_dereference(std::ptr::slice_from_raw_parts(data, len)))] - #[requires(is_initialized(data, len))] pub unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T] { std::slice::from_raw_parts(data, len) } + + #[requires(can_dereference(std::ptr::slice_from_raw_parts(data, len)))] + pub unsafe fn from_raw_parts_mut<'a, T>(data: *mut T, len: usize) -> &'a mut [T] { + std::slice::from_raw_parts_mut(data, len) + } } #[cfg(kani)] mod verify { use super::*; - const MAX_LEN: usize = 2; + const MAX_LEN: usize = isize::MAX as usize; #[kani::proof_for_contract(contracts::from_raw_parts)] - #[kani::unwind(25)] pub fn check_from_raw_parts_primitive() { let len: usize = kani::any(); kani::assume(len < MAX_LEN); @@ -27,4 +32,13 @@ mod verify { let arr = vec![0u8; len]; let _slice = unsafe { contracts::from_raw_parts(arr.as_ptr(), len) }; } + + #[kani::proof_for_contract(contracts::from_raw_parts_mut)] + pub fn check_from_raw_parts_mut_primitive() { + let len: usize = kani::any(); + kani::assume(len < MAX_LEN); + + let mut arr = vec![0u8; len]; + let _slice = unsafe { contracts::from_raw_parts_mut(arr.as_mut_ptr(), len) }; + } }