From 428165a3f010f4a8f21c786e0b18eb6483c6527b Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 1 Jul 2024 11:16:20 -0700 Subject: [PATCH 01/26] Implement memory initialization checks using demonic non-determinism. --- .../codegen_cprover_gotoc/codegen/contract.rs | 2 +- .../kani_middle/transform/check_uninit/mod.rs | 67 +++++- library/kani/src/mem_init.rs | 207 ++++++++++++------ 3 files changed, 205 insertions(+), 71 deletions(-) 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/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 6665ab697287..366c74f732ab 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -59,8 +59,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 +74,44 @@ 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) { + // First statement or terminator in the harness. + let mut source = if new_body.blocks()[0].statements.len() != 0 { + 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", + &mut self.mem_init_fn_cache, + ), + &GenericArgs(vec![]), + ) + .unwrap(); + new_body.add_call( + &memory_initialization_init, + &mut source, + InsertPosition::Before, + vec![], + ret_place.clone(), + ); + } + // 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 @@ -171,8 +209,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, @@ -252,8 +290,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, @@ -426,3 +464,20 @@ 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 = &[ + &[ + rustc_span::symbol::Symbol::intern("kanitool"), + rustc_span::symbol::Symbol::intern("proof_for_contract"), + ], + &[ + 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) + }) +} diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index 37832ea32604..f1624210b522 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,174 @@ use crate::shadow::ShadowMem; /// } /// ``` /// the layout would be [true, true, true, false]; -type Layout = [bool; N]; +type Layout = [bool; LAYOUT_SIZE]; -/// Global shadow memory object for tracking memory initialization. -#[rustc_diagnostic_item = "KaniMemInitShadowMem"] -static mut MEM_INIT_SHADOW_MEM: ShadowMem = ShadowMem::new(false); +/// Currently tracked non-deterministically chosen memory initialization state. +struct MemoryInitializationState { + pub tracked_object_id: usize, + pub tracked_offset: usize, + pub value: bool, +} -/// 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; - } +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 * 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( + &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( + &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; } - true } -/// Set initialization state to `value` for `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 = "KaniIsUnitPtrInitialized"] +fn is_unit_ptr_initialized( + ptr: *const (), + layout: Layout, + num_elts: usize, +) -> bool { + if LAYOUT_SIZE == 0 { + return true; + } + unsafe { MEM_INIT_STATE.get(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 = "KaniSetUnitPtrInitialized"] -fn set_unit_ptr_initialized( +fn set_unit_ptr_initialized( ptr: *const (), - layout: Layout, - len: usize, + layout: Layout, + num_elts: 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; - } - count += 1; + if LAYOUT_SIZE == 0 { + return; + } + unsafe { + MEM_INIT_STATE.set(ptr as *const u8, layout, num_elts, value); } } -/// Get initialization state of `len` items laid out according to the `layout` starting at address `ptr`. +/// 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, + num_elts: usize, +) -> bool { let (ptr, _) = ptr.to_raw_parts(); - is_unit_ptr_initialized(ptr, layout, len) + is_unit_ptr_initialized(ptr, layout, num_elts) } -/// 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, - len: usize, + layout: Layout, + num_elts: usize, value: bool, ) { let (ptr, _) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, len, value); + set_unit_ptr_initialized(ptr, 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 { + let (ptr, num_elts) = ptr.to_raw_parts(); + is_unit_ptr_initialized(ptr, 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, +) { + let (ptr, num_elts) = ptr.to_raw_parts(); + set_unit_ptr_initialized(ptr, 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 { + let (ptr, num_elts) = ptr.to_raw_parts(); + is_unit_ptr_initialized(ptr, 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, +) { + let (ptr, num_elts) = ptr.to_raw_parts(); + set_unit_ptr_initialized(ptr, layout, num_elts, value); } From 54d049310b3d40020be7e32d05e355bcc899bf67 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 1 Jul 2024 11:52:16 -0700 Subject: [PATCH 02/26] Fix formatting --- .../src/kani_middle/transform/check_uninit/mod.rs | 10 +++++----- library/kani/src/mem_init.rs | 10 +++++----- 2 files changed, 10 insertions(+), 10 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 366c74f732ab..8a79d3a1793b 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -77,7 +77,7 @@ impl TransformPass for UninitPass { // Inject a call to set-up memory initialization state if the function is a harness. if is_harness(instance, tcx) { // First statement or terminator in the harness. - let mut source = if new_body.blocks()[0].statements.len() != 0 { + let mut source = if !new_body.blocks()[0].statements.is_empty() { SourceInstruction::Statement { idx: 0, bb: 0 } } else { SourceInstruction::Terminator { bb: 0 } @@ -467,17 +467,17 @@ pub fn resolve_mem_init_fn(fn_def: FnDef, layout_size: usize, associated_type: T /// Checks if the instance is a harness -- an entry point of Kani analysis. fn is_harness(instance: Instance, tcx: TyCtxt) -> bool { - let harness_identifiers = &[ - &[ + 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) + tcx.has_attrs_with_path(rustc_internal::internal(tcx, instance.def.def_id()), attr_path) }) } diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index f1624210b522..b05fb2a60308 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -8,10 +8,10 @@ //! 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. -//! +//! 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. @@ -47,7 +47,7 @@ impl MemoryInitializationState { /// 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( @@ -71,7 +71,7 @@ impl MemoryInitializationState { /// 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( From 8967662af7287ec948d6d000c3db400fafa735ce Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 1 Jul 2024 13:48:36 -0700 Subject: [PATCH 03/26] Make memory initialization checks work better with atomics; add more tests --- .../transform/check_uninit/uninit_visitor.rs | 27 +++++--- .../uninit/alloc-to-slice/alloc-to-slice.rs | 2 +- tests/expected/uninit/atomic/atomic.rs | 31 +++++++++ tests/expected/uninit/atomic/expected | 13 ++++ 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 ------------------- 13 files changed, 218 insertions(+), 92 deletions(-) create mode 100644 tests/expected/uninit/atomic/atomic.rs create mode 100644 tests/expected/uninit/atomic/expected 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/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs index 19b13c6ab8b6..cadb91365f5c 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 @@ -261,8 +261,11 @@ 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 { + name if name.starts_with("atomic_cxchg") => 3, + name if name.starts_with("atomic_load") => 1, + _ => 2, + }; assert_eq!( args.len(), num_args, @@ -526,12 +529,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() { + self.push_target(MemoryInitOp::Set { + operand: Operand::Constant(constant.clone()), + count: mk_const_operand(1, location.span()), + value: true, + position: InsertPosition::Before, + }); + } }; } } @@ -656,6 +661,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`" ), 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..01bf17ca4e67 100644 --- a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs +++ b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Z ghost-state -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..84e6612d6d56 --- /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 ghost-state -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) }; + + 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/kani/Uninit/access-padding-init.rs b/tests/kani/Uninit/access-padding-init.rs new file mode 100644 index 000000000000..d98af78ea91c --- /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 ghost-state -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..195ebf9488fd --- /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 ghost-state -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..f4eaad598716 --- /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 ghost-state -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..ee9471375f68 --- /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 ghost-state -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() { + let some_var = AtomicUsize::new(5); + some_var.compare_exchange(5, 10, any_ordering(), load_ordering()); + let val = some_var.load(load_ordering()); + assert!(val == 10); +} 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..63e245415c21 --- /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 ghost-state -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..c4a418db93e5 --- /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 ghost-state -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; -} From c7f1d20e32757cb09735bbfcff500e75c1c99dfb Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 1 Jul 2024 14:02:23 -0700 Subject: [PATCH 04/26] Enable `uninit-checks` in `std-checks` --- tests/std-checks/core/Cargo.toml | 2 +- tests/std-checks/core/src/slice.rs | 20 +++++++++++++++++--- 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml index f6e1645c3a39..a1496a0c81a7 100644 --- a/tests/std-checks/core/Cargo.toml +++ b/tests/std-checks/core/Cargo.toml @@ -7,7 +7,7 @@ edition = "2021" description = "This crate contains contracts and harnesses for core library" [package.metadata.kani] -unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true } +unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true, uninit-checks = true } [package.metadata.kani.flags] output-format = "terse" 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) }; + } } From 8af4c07339a93703a3cb65feefc110810a047209 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 1 Jul 2024 14:35:04 -0700 Subject: [PATCH 05/26] More tests for interaction between memory initialization and intrinsics --- .../transform/check_uninit/uninit_visitor.rs | 17 +-- tests/expected/uninit/atomic/atomic.rs | 2 +- tests/expected/uninit/intrinsics/expected | 70 ++++++++++ .../expected/uninit/intrinsics/intrinsics.rs | 127 ++++++++++++++++++ tests/kani/Uninit/atomic.rs | 4 +- 5 files changed, 201 insertions(+), 19 deletions(-) create mode 100644 tests/expected/uninit/intrinsics/expected create mode 100644 tests/expected/uninit/intrinsics/intrinsics.rs 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 cadb91365f5c..0bd9ea4704fe 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 @@ -353,22 +353,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { 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, diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs index 84e6612d6d56..b3a632ddc67e 100644 --- a/tests/expected/uninit/atomic/atomic.rs +++ b/tests/expected/uninit/atomic/atomic.rs @@ -14,7 +14,7 @@ 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 => { diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected new file mode 100644 index 000000000000..1f9681837483 --- /dev/null +++ b/tests/expected/uninit/intrinsics/expected @@ -0,0 +1,70 @@ +Checking harness check_typed_swap_safe... + +Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit. + +VERIFICATION:- FAILED + +Checking harness check_typed_swap... + +Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit. + +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..c5e0181b27b9 --- /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 ghost-state -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/kani/Uninit/atomic.rs b/tests/kani/Uninit/atomic.rs index ee9471375f68..6de5460d57ca 100644 --- a/tests/kani/Uninit/atomic.rs +++ b/tests/kani/Uninit/atomic.rs @@ -59,8 +59,8 @@ fn local_atomic() { // 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()); - let val = some_var.load(load_ordering()); - assert!(val == 10); } From 068b9af8cca3e8795bcd0ad331125a10e3623c58 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 1 Jul 2024 15:00:24 -0700 Subject: [PATCH 06/26] Fix issues with `std-checks` --- .../kani_middle/transform/check_uninit/mod.rs | 2 +- library/kani/src/internal.rs | 1 + tests/std-checks/core/mem.expected | 25 ++++++++++++++++++- tests/std-checks/core/slice.expected | 2 +- 4 files changed, 27 insertions(+), 3 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 8a79d3a1793b..23c81a8f8c39 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -30,7 +30,7 @@ pub use ty_layout::{PointeeInfo, PointeeLayout}; use uninit_visitor::{CheckUninitVisitor, InitRelevantInstruction, MemoryInitOp}; const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = - &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized"]; + &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized", "KaniContractsApplyClosure"]; /// Instrument the code with checks for uninitialized memory. #[derive(Debug)] diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 509f2cf51962..1bde65230384 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -94,6 +94,7 @@ pub fn init_contracts() {} /// This should only be used within contracts. The intent is to /// perform type inference on a closure's argument #[doc(hidden)] +#[rustc_diagnostic_item = "KaniContractsApplyClosure"] pub fn apply_closure bool>(f: U, x: &T) -> bool { f(x) } diff --git a/tests/std-checks/core/mem.expected b/tests/std-checks/core/mem.expected index 1484c83901fc..cdf1da0e9f52 100644 --- a/tests/std-checks/core/mem.expected +++ b/tests/std-checks/core/mem.expected @@ -1,7 +1,30 @@ +Checking harness mem::verify::check_swap_large_adt_no_drop... + +Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit>. + +VERIFICATION:- FAILED + +Checking harness mem::verify::check_swap_adt_no_drop... + +Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit>. + +VERIFICATION:- FAILED + Checking harness mem::verify::check_swap_unit... Failed Checks: ptr NULL or writable up to size +VERIFICATION:- FAILED + +Checking harness mem::verify::check_swap_primitive... + +Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit. + +VERIFICATION:- FAILED + Summary: +Verification failed for - mem::verify::check_swap_large_adt_no_drop +Verification failed for - mem::verify::check_swap_adt_no_drop Verification failed for - mem::verify::check_swap_unit -Complete - 6 successfully verified harnesses, 1 failures, 7 total. +Verification failed for - mem::verify::check_swap_primitive +Complete - 3 successfully verified harnesses, 4 failures, 7 total. 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. From 0723510e01ec53651ad734eccc822ee245ee82ac Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 1 Jul 2024 15:03:06 -0700 Subject: [PATCH 07/26] Fix formatting --- .../src/kani_middle/transform/check_uninit/uninit_visitor.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 0bd9ea4704fe..57d767b10ea8 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 @@ -353,7 +353,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { count: mk_const_operand(1, location.span()), }); } - "volatile_load" | "unaligned_volatile_load" => { + "volatile_load" | "unaligned_volatile_load" => { assert_eq!( args.len(), 1, From a939e5552fca14055db30580f94d827461896ad4 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 3 Jul 2024 09:02:15 -0700 Subject: [PATCH 08/26] Only bless drop for Adt's --- .../transform/check_uninit/uninit_visitor.rs | 30 ++++++++++++++----- 1 file changed, 22 insertions(+), 8 deletions(-) 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 57d767b10ea8..64cafcec1173 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 @@ -444,14 +444,28 @@ 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()), + count: mk_const_operand(1, location.span()), + value: true, + position: InsertPosition::Before, + }); + } + _ => {} + } + if place_ty.kind().is_raw_ptr() { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), From fb2aa14547a2b4e649c46cc0e5c374d605635ff7 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 3 Jul 2024 09:09:59 -0700 Subject: [PATCH 09/26] Assert `is_initialized` in predicates --- library/kani/src/mem.rs | 9 +++++++-- library/kani_core/src/mem.rs | 11 +++++++---- 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 0b390e74288d..0588a35df72f 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. + assert!(is_initialized(ptr, 1)); metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) - && is_initialized(ptr, 1) && unsafe { has_valid_value(ptr) } } @@ -148,7 +150,10 @@ 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. + assert!(is_initialized(ptr, 1)); + is_inbounds(&metadata, thin_ptr) && unsafe { has_valid_value(ptr) } } /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 3b10856765a5..3f396ad89340 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. + assert!(is_initialized(ptr, 1)); metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) - && is_initialized(ptr, 1) && unsafe { has_valid_value(ptr) } } @@ -154,9 +156,10 @@ macro_rules! kani_mem { ::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. + assert!(is_initialized(ptr, 1)); + is_inbounds(&metadata, thin_ptr) && unsafe { has_valid_value(ptr) } } /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. From bb2a02b922b1d0abd7ea25d695ae5a2d2d819752 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 3 Jul 2024 09:45:21 -0700 Subject: [PATCH 10/26] Add more comments, remove unnecessary checks --- kani-compiler/src/kani_middle/transform/check_uninit/mod.rs | 2 +- .../src/kani_middle/transform/check_uninit/uninit_visitor.rs | 4 ++++ library/kani/src/internal.rs | 1 - 3 files changed, 5 insertions(+), 2 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 23c81a8f8c39..8a79d3a1793b 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -30,7 +30,7 @@ pub use ty_layout::{PointeeInfo, PointeeLayout}; use uninit_visitor::{CheckUninitVisitor, InitRelevantInstruction, MemoryInitOp}; const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = - &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized", "KaniContractsApplyClosure"]; + &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized"]; /// Instrument the code with checks for uninitialized memory. #[derive(Debug)] 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 64cafcec1173..34befce23ce2 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 @@ -262,8 +262,11 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } name if name.starts_with("atomic") => { 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!( @@ -529,6 +532,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { for (_, prov) in &allocation.provenance.ptrs { if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) { 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()), count: mk_const_operand(1, location.span()), diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 1bde65230384..509f2cf51962 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -94,7 +94,6 @@ pub fn init_contracts() {} /// This should only be used within contracts. The intent is to /// perform type inference on a closure's argument #[doc(hidden)] -#[rustc_diagnostic_item = "KaniContractsApplyClosure"] pub fn apply_closure bool>(f: U, x: &T) -> bool { f(x) } From ed11c8e1d8252de23d2ab000dff8b65e12ef7d5f Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 3 Jul 2024 11:32:30 -0700 Subject: [PATCH 11/26] Fix assert order --- library/kani/src/mem.rs | 19 ++++++++++++++++--- library/kani_core/src/mem.rs | 19 ++++++++++++++++--- 2 files changed, 32 insertions(+), 6 deletions(-) diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 0588a35df72f..f06bf36f7e38 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -120,9 +120,15 @@ where 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. - assert!(is_initialized(ptr, 1)); metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) + && { + crate::assert( + is_initialized(ptr, 1), + "Undefined Behavior: Reading from an uninitialized pointer", + ); + true + } && unsafe { has_valid_value(ptr) } } @@ -152,8 +158,15 @@ where 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. - assert!(is_initialized(ptr, 1)); - is_inbounds(&metadata, thin_ptr) && unsafe { has_valid_value(ptr) } + is_inbounds(&metadata, thin_ptr) + && { + crate::assert( + is_initialized(ptr, 1), + "Undefined Behavior: Reading from an uninitialized pointer", + ); + true + } + && unsafe { has_valid_value(ptr) } } /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 3f396ad89340..a2d50002e189 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -125,9 +125,15 @@ macro_rules! kani_mem { 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. - assert!(is_initialized(ptr, 1)); metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) + && { + crate::assert( + is_initialized(ptr, 1), + "Undefined Behavior: Reading from an uninitialized pointer", + ); + true + } && unsafe { has_valid_value(ptr) } } @@ -158,8 +164,15 @@ macro_rules! kani_mem { 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. - assert!(is_initialized(ptr, 1)); - is_inbounds(&metadata, thin_ptr) && unsafe { has_valid_value(ptr) } + is_inbounds(&metadata, thin_ptr) + && { + crate::assert( + is_initialized(ptr, 1), + "Undefined Behavior: Reading from an uninitialized pointer", + ); + true + } + && unsafe { has_valid_value(ptr) } } /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. From cb93dcbb1f3d7079b20c25b1ca2163202deac568 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 3 Jul 2024 11:43:35 -0700 Subject: [PATCH 12/26] Make clippy happy --- library/kani_core/src/mem.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index a2d50002e189..e887e3f66642 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -128,7 +128,7 @@ macro_rules! kani_mem { metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) && { - crate::assert( + assert!( is_initialized(ptr, 1), "Undefined Behavior: Reading from an uninitialized pointer", ); @@ -166,7 +166,7 @@ macro_rules! kani_mem { // does not make sense to use it inside assumption context. is_inbounds(&metadata, thin_ptr) && { - crate::assert( + assert!( is_initialized(ptr, 1), "Undefined Behavior: Reading from an uninitialized pointer", ); From fcb99ad61029c8f3e1b3573def37007600d5a091 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 5 Jul 2024 15:16:35 -0700 Subject: [PATCH 13/26] Remove unnecessary clone --- kani-compiler/src/kani_middle/transform/check_uninit/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 8a79d3a1793b..dc86e5ab8f48 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -108,7 +108,7 @@ impl TransformPass for UninitPass { &mut source, InsertPosition::Before, vec![], - ret_place.clone(), + ret_place, ); } From 3bf51f0fbce68867d3213f3e02ba839e281332ad Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 5 Jul 2024 15:22:48 -0700 Subject: [PATCH 14/26] Wrap memory initialization set-up in a separate function --- .../kani_middle/transform/check_uninit/mod.rs | 74 ++++++++++--------- 1 file changed, 40 insertions(+), 34 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 dc86e5ab8f48..5f4610076bf1 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -76,40 +76,7 @@ impl TransformPass for UninitPass { // Inject a call to set-up memory initialization state if the function is a harness. if is_harness(instance, tcx) { - // 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", - &mut self.mem_init_fn_cache, - ), - &GenericArgs(vec![]), - ) - .unwrap(); - new_body.add_call( - &memory_initialization_init, - &mut source, - InsertPosition::Before, - vec![], - ret_place, - ); + 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. @@ -481,3 +448,42 @@ fn is_harness(instance: Instance, tcx: TyCtxt) -> bool { 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, + ); +} From 898dd0b52d993c057f07e3d7d1834c4313ae3c9e Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 5 Jul 2024 15:29:02 -0700 Subject: [PATCH 15/26] Wrap `assert!(is_initialized(...))` into a separate function --- library/kani/src/mem.rs | 25 +++++++++++-------------- library/kani_core/src/mem.rs | 25 +++++++++++-------------- 2 files changed, 22 insertions(+), 28 deletions(-) diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index f06bf36f7e38..201d027124d0 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -122,13 +122,7 @@ where // not make sense to use it inside assumption context. metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) - && { - crate::assert( - is_initialized(ptr, 1), - "Undefined Behavior: Reading from an uninitialized pointer", - ); - true - } + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -159,13 +153,7 @@ where // 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) - && { - crate::assert( - is_initialized(ptr, 1), - "Undefined Behavior: Reading from an uninitialized pointer", - ); - true - } + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -316,6 +304,15 @@ pub fn is_initialized(_ptr: *const T, _len: usize) -> bool { kani_intrinsic() } +/// A helper to to assert `is_initialized` to use it as a part of other predicates. +fn assert_is_initialized(ptr: *const T) -> bool { + crate::assert( + is_initialized(ptr, 1), + "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_core/src/mem.rs b/library/kani_core/src/mem.rs index e887e3f66642..de6c535be8dc 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -127,13 +127,7 @@ macro_rules! kani_mem { // does not make sense to use it inside assumption context. metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) - && { - assert!( - is_initialized(ptr, 1), - "Undefined Behavior: Reading from an uninitialized pointer", - ); - true - } + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -165,13 +159,7 @@ macro_rules! kani_mem { // 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, 1), - "Undefined Behavior: Reading from an uninitialized pointer", - ); - true - } + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -322,6 +310,15 @@ macro_rules! kani_mem { kani_intrinsic() } + /// A helper to to assert `is_initialized` to use it as a part of other predicates. + fn assert_is_initialized(ptr: *const T) -> bool { + assert!( + is_initialized(ptr, 1), + "Undefined Behavior: Reading from an uninitialized pointer", + ); + true + } + /// Get the object ID of the given pointer. #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] From b38845845c2535b6faeb43be214bf926da7be156 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 8 Jul 2024 09:25:41 -0700 Subject: [PATCH 16/26] `-Z uninit-checks` automatically enables shadow memory --- kani-driver/src/call_single_file.rs | 5 ++++- .../uninit/access-padding-uninit/access-padding-uninit.rs | 2 +- .../access-padding-via-cast/access-padding-via-cast.rs | 2 +- tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs | 2 +- tests/expected/uninit/atomic/atomic.rs | 2 +- tests/expected/uninit/intrinsics/intrinsics.rs | 2 +- tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs | 2 +- .../expected/uninit/vec-read-semi-init/vec-read-semi-init.rs | 2 +- tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs | 2 +- tests/kani/Uninit/access-padding-enum-diverging-variants.rs | 2 +- tests/kani/Uninit/access-padding-enum-multiple-variants.rs | 2 +- tests/kani/Uninit/access-padding-enum-single-field.rs | 2 +- tests/kani/Uninit/access-padding-enum-single-variant.rs | 2 +- tests/kani/Uninit/access-padding-init.rs | 2 +- tests/kani/Uninit/alloc-to-slice.rs | 2 +- tests/kani/Uninit/alloc-zeroed-to-slice.rs | 2 +- tests/kani/Uninit/atomic.rs | 2 +- tests/kani/Uninit/struct-padding-and-arr-init.rs | 2 +- tests/kani/Uninit/vec-read-init.rs | 2 +- 19 files changed, 22 insertions(+), 19 deletions(-) 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/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 01bf17ca4e67..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,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::alloc::{alloc, Layout}; use std::slice::from_raw_parts; diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs index b3a632ddc67e..63c85af41a3f 100644 --- a/tests/expected/uninit/atomic/atomic.rs +++ b/tests/expected/uninit/atomic/atomic.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 #![feature(core_intrinsics)] diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs index c5e0181b27b9..aa8a89b7b959 100644 --- a/tests/expected/uninit/intrinsics/intrinsics.rs +++ b/tests/expected/uninit/intrinsics/intrinsics.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 supports memory initialization checks via intrinsics. #![feature(core_intrinsics)] 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 index d98af78ea91c..7523622a6106 100644 --- a/tests/kani/Uninit/access-padding-init.rs +++ b/tests/kani/Uninit/access-padding-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 use std::ptr::addr_of; diff --git a/tests/kani/Uninit/alloc-to-slice.rs b/tests/kani/Uninit/alloc-to-slice.rs index 195ebf9488fd..863d3b40b390 100644 --- a/tests/kani/Uninit/alloc-to-slice.rs +++ b/tests/kani/Uninit/alloc-to-slice.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::alloc::{alloc, Layout}; diff --git a/tests/kani/Uninit/alloc-zeroed-to-slice.rs b/tests/kani/Uninit/alloc-zeroed-to-slice.rs index f4eaad598716..d00ca4c6abff 100644 --- a/tests/kani/Uninit/alloc-zeroed-to-slice.rs +++ b/tests/kani/Uninit/alloc-zeroed-to-slice.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::alloc::{alloc_zeroed, Layout}; use std::slice::from_raw_parts; diff --git a/tests/kani/Uninit/atomic.rs b/tests/kani/Uninit/atomic.rs index 6de5460d57ca..376f365d408c 100644 --- a/tests/kani/Uninit/atomic.rs +++ b/tests/kani/Uninit/atomic.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::sync::atomic::{AtomicUsize, Ordering}; diff --git a/tests/kani/Uninit/struct-padding-and-arr-init.rs b/tests/kani/Uninit/struct-padding-and-arr-init.rs index 63e245415c21..c67b1177bfa3 100644 --- a/tests/kani/Uninit/struct-padding-and-arr-init.rs +++ b/tests/kani/Uninit/struct-padding-and-arr-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 use std::ptr::addr_of_mut; diff --git a/tests/kani/Uninit/vec-read-init.rs b/tests/kani/Uninit/vec-read-init.rs index c4a418db93e5..78812c59830e 100644 --- a/tests/kani/Uninit/vec-read-init.rs +++ b/tests/kani/Uninit/vec-read-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 #[kani::proof] fn vec_read_init() { From 7abb003b287ce0ac14d7cc8eba2fe9062335f286 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 8 Jul 2024 10:50:26 -0700 Subject: [PATCH 17/26] Inject `UnsupportedCheck` when observing mutable pointer casts --- .../transform/check_uninit/uninit_visitor.rs | 31 +++++++++++++++---- 1 file changed, 25 insertions(+), 6 deletions(-) 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 34befce23ce2..801e2fd65928 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 @@ -548,13 +548,32 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { - if let Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), _, ty) = rvalue { - if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { - if pointee_ty.kind().is_trait() { - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), - }); + if let Rvalue::Cast(cast_kind, operand, ty) = rvalue { + match cast_kind { + CastKind::PointerCoercion(PointerCoercion::Unsize) => { + if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { + if pointee_ty.kind().is_trait() { + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), + }); + } + } + } + CastKind::PtrToPtr => { + let operand_ty = operand.ty(&self.locals).unwrap(); + if let ( + RigidTy::RawPtr(_, Mutability::Mut), + RigidTy::RawPtr(_, Mutability::Mut), + ) = (operand_ty.kind().rigid().unwrap(), ty.kind().rigid().unwrap()) + { + // If casting from a mutable pointer to a mutable pointer, delayed UB could + // occur, which we do not support. + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts.".to_string(), + }); + } } + _ => {} } }; self.super_rvalue(rvalue, location); From 5a7a6b2db3e4bc857203186567056d8671cc90b3 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 8 Jul 2024 11:55:52 -0700 Subject: [PATCH 18/26] Revert "Inject `UnsupportedCheck` when observing mutable pointer casts" This reverts commit 7abb003b287ce0ac14d7cc8eba2fe9062335f286. --- .../transform/check_uninit/uninit_visitor.rs | 31 ++++--------------- 1 file changed, 6 insertions(+), 25 deletions(-) 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 801e2fd65928..34befce23ce2 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 @@ -548,32 +548,13 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { - if let Rvalue::Cast(cast_kind, operand, ty) = rvalue { - match cast_kind { - CastKind::PointerCoercion(PointerCoercion::Unsize) => { - if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { - if pointee_ty.kind().is_trait() { - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), - }); - } - } - } - CastKind::PtrToPtr => { - let operand_ty = operand.ty(&self.locals).unwrap(); - if let ( - RigidTy::RawPtr(_, Mutability::Mut), - RigidTy::RawPtr(_, Mutability::Mut), - ) = (operand_ty.kind().rigid().unwrap(), ty.kind().rigid().unwrap()) - { - // If casting from a mutable pointer to a mutable pointer, delayed UB could - // occur, which we do not support. - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts.".to_string(), - }); - } + if let Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), _, ty) = rvalue { + if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { + if pointee_ty.kind().is_trait() { + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), + }); } - _ => {} } }; self.super_rvalue(rvalue, location); From 5f149bf7a04d2a485fc58eaee987e189d94b4323 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 8 Jul 2024 12:58:13 -0700 Subject: [PATCH 19/26] Separate calls to checking/setting memory initialization of slice chunks --- .../kani_middle/transform/check_uninit/mod.rs | 88 +++++++++++--- .../transform/check_uninit/uninit_visitor.rs | 95 +++++++-------- .../kani_middle/transform/kani_intrinsics.rs | 6 +- library/kani/src/mem.rs | 7 +- library/kani/src/mem_init.rs | 113 ++++++++++++++---- library/kani_core/src/mem.rs | 4 +- 6 files changed, 210 insertions(+), 103 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 5f4610076bf1..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)] @@ -164,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 { .. } => { @@ -194,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(), ); } @@ -277,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, ); } 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 34befce23ce2..f4af8ee6e3b4 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,25 +8,31 @@ 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, TyKind, UintTy}; +use stable_mir::ty::{ConstantKind, RigidTy, TyKind}; use strum_macros::AsRefStr; /// 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 }, } @@ -37,9 +43,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 { @@ -60,24 +67,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, } } } @@ -156,12 +173,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, @@ -186,7 +203,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()), }); }; } @@ -195,7 +211,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, }); @@ -206,7 +221,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, }); @@ -217,7 +231,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, }); @@ -280,7 +293,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" => { @@ -297,11 +309,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(), }); @@ -322,11 +334,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, @@ -349,11 +361,9 @@ 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()), }); } "volatile_load" | "unaligned_volatile_load" => { @@ -368,7 +378,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" => { @@ -383,7 +392,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, }); @@ -398,7 +406,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, @@ -421,7 +429,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, @@ -430,7 +438,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, @@ -461,7 +469,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), - count: mk_const_operand(1, location.span()), value: true, position: InsertPosition::Before, }); @@ -472,7 +479,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { 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, }); @@ -500,7 +506,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()), }); } } @@ -535,7 +540,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { // If a static is a raw pointer, need to mark it as initialized. self.push_target(MemoryInitOp::Set { operand: Operand::Constant(constant.clone()), - count: mk_const_operand(1, location.span()), value: true, position: InsertPosition::Before, }); @@ -696,15 +700,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/library/kani/src/mem.rs b/library/kani/src/mem.rs index 201d027124d0..be6a80ee0fe2 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -300,16 +300,13 @@ 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 to assert `is_initialized` to use it as a part of other predicates. fn assert_is_initialized(ptr: *const T) -> bool { - crate::assert( - is_initialized(ptr, 1), - "Undefined Behavior: Reading from an uninitialized pointer", - ); + crate::assert(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer"); true } diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index b05fb2a60308..a09e515d7e17 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -44,13 +44,58 @@ impl MemoryInitializationState { 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 + } + } + + /// 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( + pub fn get_slice( &mut self, ptr: *const u8, layout: Layout, @@ -74,7 +119,7 @@ impl MemoryInitializationState { /// /// Such definition is necessary since both tracked object and tracked offset are chosen /// non-deterministically. - pub fn set( + pub fn set_slice( &mut self, ptr: *const u8, layout: Layout, @@ -107,55 +152,63 @@ fn initialize_memory_initialization_state() { } /// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`. -#[rustc_diagnostic_item = "KaniIsUnitPtrInitialized"] -fn is_unit_ptr_initialized( - ptr: *const (), +#[rustc_diagnostic_item = "KaniIsPtrInitialized"] +fn is_ptr_initialized( + ptr: *const T, layout: Layout, - num_elts: usize, ) -> bool { if LAYOUT_SIZE == 0 { return true; } - unsafe { MEM_INIT_STATE.get(ptr as *const u8, layout, num_elts) } + let (ptr, _) = ptr.to_raw_parts(); + unsafe { MEM_INIT_STATE.get(ptr as *const u8, layout) } } /// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`. -#[rustc_diagnostic_item = "KaniSetUnitPtrInitialized"] -fn set_unit_ptr_initialized( - ptr: *const (), +#[rustc_diagnostic_item = "KaniSetPtrInitialized"] +fn set_ptr_initialized( + ptr: *const T, layout: Layout, - num_elts: usize, value: bool, ) { if LAYOUT_SIZE == 0 { return; } + let (ptr, _) = ptr.to_raw_parts(); unsafe { - MEM_INIT_STATE.set(ptr as *const u8, layout, num_elts, value); + 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 = "KaniIsPtrInitialized"] -fn is_ptr_initialized( +#[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(); - is_unit_ptr_initialized(ptr, layout, num_elts) + 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 = "KaniSetPtrInitialized"] -fn set_ptr_initialized( +#[rustc_diagnostic_item = "KaniSetSliceChunkPtrInitialized"] +fn set_slice_chunk_ptr_initialized( ptr: *const T, layout: Layout, num_elts: usize, value: bool, ) { + if LAYOUT_SIZE == 0 { + return; + } let (ptr, _) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, num_elts, 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`. @@ -164,8 +217,11 @@ 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(); - is_unit_ptr_initialized(ptr, layout, num_elts) + 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`. @@ -175,8 +231,13 @@ fn set_slice_ptr_initialized( layout: Layout, value: bool, ) { + if LAYOUT_SIZE == 0 { + return; + } let (ptr, num_elts) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, num_elts, value); + 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`. @@ -185,8 +246,11 @@ 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(); - is_unit_ptr_initialized(ptr, layout, num_elts) + 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`. @@ -196,6 +260,11 @@ fn set_str_ptr_initialized( layout: Layout, value: bool, ) { + if LAYOUT_SIZE == 0 { + return; + } let (ptr, num_elts) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, num_elts, value); + unsafe { + MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value); + } } diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index de6c535be8dc..74061d07404b 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -306,14 +306,14 @@ 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 to assert `is_initialized` to use it as a part of other predicates. fn assert_is_initialized(ptr: *const T) -> bool { assert!( - is_initialized(ptr, 1), + is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer", ); true From fb07b8ac418935bc0a7df8b5f400815026d4bc92 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Tue, 9 Jul 2024 11:55:38 -0700 Subject: [PATCH 20/26] Remove unnecessary imports --- .../src/kani_middle/transform/check_uninit/uninit_visitor.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 895dbc8d5eb9..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 @@ -12,7 +12,7 @@ use stable_mir::mir::{ 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}; From 853ed2447c151e4568a2dede8c9f22338ae1ed54 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 10 Jul 2024 08:07:14 -0700 Subject: [PATCH 21/26] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/kani/src/mem.rs | 2 +- library/kani_core/src/mem.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index be6a80ee0fe2..33a9405d4e9b 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -304,7 +304,7 @@ pub fn is_initialized(_ptr: *const T) -> bool { kani_intrinsic() } -/// A helper to to assert `is_initialized` to use it as a part of other predicates. +/// A helper to assert `is_initialized` to use it as a part of other predicates. fn assert_is_initialized(ptr: *const T) -> bool { crate::assert(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer"); true diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 74061d07404b..1d97035beed1 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -310,7 +310,7 @@ macro_rules! kani_mem { kani_intrinsic() } - /// A helper to to assert `is_initialized` to use it as a part of other predicates. + /// A helper to assert `is_initialized` to use it as a part of other predicates. fn assert_is_initialized(ptr: *const T) -> bool { assert!( is_initialized(ptr), From 351e5926d2749524cfe59f1d23f1aa7ac1a6b372 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 10 Jul 2024 09:32:11 -0700 Subject: [PATCH 22/26] Fix regressions --- tests/expected/uninit/intrinsics/expected | 4 ++-- tests/std-checks/core/mem.expected | 8 +++++--- tests/std-checks/core/ptr.expected | 16 +++++++++++++++- 3 files changed, 22 insertions(+), 6 deletions(-) diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index 1f9681837483..ffa98b6f1140 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -1,12 +1,12 @@ Checking harness check_typed_swap_safe... -Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit. +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 currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit. +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` diff --git a/tests/std-checks/core/mem.expected b/tests/std-checks/core/mem.expected index cdf1da0e9f52..0276f285807f 100644 --- a/tests/std-checks/core/mem.expected +++ b/tests/std-checks/core/mem.expected @@ -1,24 +1,26 @@ Checking harness mem::verify::check_swap_large_adt_no_drop... -Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit>. +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 mem::verify::check_swap_adt_no_drop... -Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit>. +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 mem::verify::check_swap_unit... +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. + Failed Checks: ptr NULL or writable up to size VERIFICATION:- FAILED Checking harness mem::verify::check_swap_primitive... -Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit. +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. VERIFICATION:- FAILED diff --git a/tests/std-checks/core/ptr.expected b/tests/std-checks/core/ptr.expected index 43d3bd6baf60..a5ef62af8036 100644 --- a/tests/std-checks/core/ptr.expected +++ b/tests/std-checks/core/ptr.expected @@ -1,4 +1,18 @@ +Checking harness ptr::verify::check_new_unchecked... + +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 ptr::verify::check_new... + +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. + +VERIFICATION:- FAILED + Summary: Verification failed for - ptr::verify::check_replace_unit Verification failed for - ptr::verify::check_as_ref_dangling -Complete - 4 successfully verified harnesses, 2 failures, 6 total. +Verification failed for - ptr::verify::check_new_unchecked +Verification failed for - ptr::verify::check_new +Complete - 2 successfully verified harnesses, 4 failures, 6 total. From d094aaf307df016cf349614d1669e6a458ca8925 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 10 Jul 2024 13:38:19 -0700 Subject: [PATCH 23/26] Ensure that non-determinism is not used in assumption context --- .../codegen_cprover_gotoc/overrides/hooks.rs | 41 +++++++++++++++++++ .../src/kani_middle/transform/body.rs | 21 +++++++++- .../src/kani_middle/transform/mod.rs | 8 +++- library/kani/src/lib.rs | 24 +++++++++++ library/kani/src/mem.rs | 2 +- library/kani_core/src/lib.rs | 24 +++++++++++ library/kani_core/src/mem.rs | 2 +- 7 files changed, 116 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index fc245fc6f4c9..66a7130ac05a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -143,6 +143,46 @@ 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); + + // Since `cond` might have side effects, assign it to a temporary + // variable so that it's evaluated once, then assert it + // TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps + let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc); + Stmt::block( + vec![ + reach_stmt, + decl, + gcx.codegen_assert(tmp, PropertyClass::Assertion, &msg, caller_loc), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) + } +} + struct Nondet; impl GotocHook for Nondet { @@ -510,6 +550,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/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/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 33a9405d4e9b..f861f6b2ba25 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -306,7 +306,7 @@ pub fn is_initialized(_ptr: *const T) -> bool { /// A helper to assert `is_initialized` to use it as a part of other predicates. fn assert_is_initialized(ptr: *const T) -> bool { - crate::assert(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer"); + crate::check(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer"); true } 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 1d97035beed1..bbae19db65c5 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -312,7 +312,7 @@ macro_rules! kani_mem { /// A helper to assert `is_initialized` to use it as a part of other predicates. fn assert_is_initialized(ptr: *const T) -> bool { - assert!( + $crate::check( is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer", ); From 630f6c3d142d1869da4a5deb718a05ae71b1d4b2 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 10 Jul 2024 13:43:12 -0700 Subject: [PATCH 24/26] Rollback changes in `std-checks` --- tests/std-checks/core/Cargo.toml | 2 +- tests/std-checks/core/mem.expected | 27 +-------------------------- tests/std-checks/core/ptr.expected | 16 +--------------- 3 files changed, 3 insertions(+), 42 deletions(-) diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml index a1496a0c81a7..f6e1645c3a39 100644 --- a/tests/std-checks/core/Cargo.toml +++ b/tests/std-checks/core/Cargo.toml @@ -7,7 +7,7 @@ edition = "2021" description = "This crate contains contracts and harnesses for core library" [package.metadata.kani] -unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true, uninit-checks = true } +unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true } [package.metadata.kani.flags] output-format = "terse" diff --git a/tests/std-checks/core/mem.expected b/tests/std-checks/core/mem.expected index 0276f285807f..1484c83901fc 100644 --- a/tests/std-checks/core/mem.expected +++ b/tests/std-checks/core/mem.expected @@ -1,32 +1,7 @@ -Checking harness mem::verify::check_swap_large_adt_no_drop... - -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 mem::verify::check_swap_adt_no_drop... - -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 mem::verify::check_swap_unit... -Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. - Failed Checks: ptr NULL or writable up to size -VERIFICATION:- FAILED - -Checking harness mem::verify::check_swap_primitive... - -Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. - -VERIFICATION:- FAILED - Summary: -Verification failed for - mem::verify::check_swap_large_adt_no_drop -Verification failed for - mem::verify::check_swap_adt_no_drop Verification failed for - mem::verify::check_swap_unit -Verification failed for - mem::verify::check_swap_primitive -Complete - 3 successfully verified harnesses, 4 failures, 7 total. +Complete - 6 successfully verified harnesses, 1 failures, 7 total. diff --git a/tests/std-checks/core/ptr.expected b/tests/std-checks/core/ptr.expected index a5ef62af8036..43d3bd6baf60 100644 --- a/tests/std-checks/core/ptr.expected +++ b/tests/std-checks/core/ptr.expected @@ -1,18 +1,4 @@ -Checking harness ptr::verify::check_new_unchecked... - -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 ptr::verify::check_new... - -Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. - -VERIFICATION:- FAILED - Summary: Verification failed for - ptr::verify::check_replace_unit Verification failed for - ptr::verify::check_as_ref_dangling -Verification failed for - ptr::verify::check_new_unchecked -Verification failed for - ptr::verify::check_new -Complete - 2 successfully verified harnesses, 4 failures, 6 total. +Complete - 4 successfully verified harnesses, 2 failures, 6 total. From 0b24435641fdf266374ec9dbdc9b8ef8d1b81fc1 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 10 Jul 2024 14:30:18 -0700 Subject: [PATCH 25/26] Try substituting `$crate` with `super` to make `verify_std_cmd` pass on CI --- library/kani_core/src/mem.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index bbae19db65c5..bcf4cd2248a6 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -312,7 +312,7 @@ macro_rules! kani_mem { /// 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( + super::check( is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer", ); From 19cf0917ada681a9ba211d956ae2542929186b37 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 12 Jul 2024 08:23:20 -0700 Subject: [PATCH 26/26] Remove unnecessary temporary variable in `hooks.rs` --- kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 66a7130ac05a..c0df279932f6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -167,15 +167,10 @@ impl GotocHook for Check { let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span); - // Since `cond` might have side effects, assign it to a temporary - // variable so that it's evaluated once, then assert it - // TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps - let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc); Stmt::block( vec![ reach_stmt, - decl, - gcx.codegen_assert(tmp, PropertyClass::Assertion, &msg, caller_loc), + gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc), Stmt::goto(bb_label(target), caller_loc), ], caller_loc,