From 8086b0dceebc8a35ef62b4e601b5d265606896e6 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 24 May 2024 17:03:20 -0700 Subject: [PATCH 01/12] Add simple API for shadow memory --- .../codegen/foreign_function.rs | 2 + library/kani/kani_lib.c | 8 ++++ library/kani/src/lib.rs | 1 + library/kani/src/shadow.rs | 38 ++++++++++++++++ tests/expected/shadow/uninit_array/expected | 3 ++ tests/expected/shadow/uninit_array/test.rs | 44 +++++++++++++++++++ 6 files changed, 96 insertions(+) create mode 100644 library/kani/src/shadow.rs create mode 100644 tests/expected/shadow/uninit_array/expected create mode 100644 tests/expected/shadow/uninit_array/test.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 4ab72eb3a705..4584daa57c23 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -35,6 +35,8 @@ lazy_static! { "__rust_alloc_zeroed".into(), "__rust_dealloc".into(), "__rust_realloc".into(), + "__KANI_pointer_object".into(), + "__KANI_pointer_offset".into(), ]) }; } diff --git a/library/kani/kani_lib.c b/library/kani/kani_lib.c index b077547b10d7..f9f13ab1c21e 100644 --- a/library/kani/kani_lib.c +++ b/library/kani/kani_lib.c @@ -118,3 +118,11 @@ uint8_t *__rust_realloc(uint8_t *ptr, size_t old_size, size_t align, size_t new_ return result; } + +size_t __KANI_pointer_object(uint8_t *ptr) { + return __CPROVER_POINTER_OBJECT(ptr); +} + +size_t __KANI_pointer_offset(uint8_t *ptr) { + return __CPROVER_POINTER_OFFSET(ptr); +} diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 25b1b389a2b1..341dd6752916 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -24,6 +24,7 @@ pub mod arbitrary; mod concrete_playback; pub mod futures; pub mod mem; +pub mod shadow; pub mod slice; pub mod tuple; pub mod vec; diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs new file mode 100644 index 000000000000..7c20e068b1fe --- /dev/null +++ b/library/kani/src/shadow.rs @@ -0,0 +1,38 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern "C" { + pub fn __KANI_pointer_object(ptr: *const u8) -> usize; + pub fn __KANI_pointer_offset(ptr: *const u8) -> usize; +} + +pub struct ShadowMem { + is_init: [[bool; 64]; 1024], +} + + +impl ShadowMem { + pub const fn new() -> Self { + Self { is_init: [[false; 64]; 1024] } + } + + pub fn is_init(&self, ptr: *const u8) -> bool { + read(&self.is_init, ptr) + } + + pub fn set_init(&mut self, ptr: *const u8, init: bool) { + write(&mut self.is_init, ptr, init); + } +} + +pub fn read(sm: &[[bool; 64]; 1024], ptr: *const u8) -> bool { + let obj = unsafe { __KANI_pointer_object(ptr) }; + let offset = unsafe { __KANI_pointer_offset(ptr) }; + sm[obj][offset] +} + +pub fn write(sm: &mut [[bool; 64]; 1024], ptr: *const u8, val: bool) { + let obj = unsafe { __KANI_pointer_object(ptr) }; + let offset = unsafe { __KANI_pointer_offset(ptr) }; + sm[obj][offset] = val; +} diff --git a/tests/expected/shadow/uninit_array/expected b/tests/expected/shadow/uninit_array/expected new file mode 100644 index 000000000000..14c64787704e --- /dev/null +++ b/tests/expected/shadow/uninit_array/expected @@ -0,0 +1,3 @@ +Failed Checks: assertion failed: SM.is_init(p as *mut u8) +Verification failed for - check_init_any +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/shadow/uninit_array/test.rs b/tests/expected/shadow/uninit_array/test.rs new file mode 100644 index 000000000000..49e0e992ba6d --- /dev/null +++ b/tests/expected/shadow/uninit_array/test.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use std::alloc::{alloc, dealloc, Layout}; + +static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(); + +fn write(ptr: *mut i32, offset: usize, x: i32) { + unsafe { + let p = ptr.offset(offset as isize); + p.write(x); + SM.set_init(p as *mut u8, true); + }; +} + +fn check_init(b: bool) { + let layout = Layout::array::(5).unwrap(); + let ptr = unsafe { alloc(layout) as *mut i32}; + write(ptr, 0, 0); + write(ptr, 1, 1); + if b { write(ptr, 2, 2) }; + write(ptr, 3, 3); + write(ptr, 4, 4); + let index: usize = kani::any(); + if index < 5 { + unsafe { + let p = ptr.offset(index as isize); + let x = p.read(); + assert!(SM.is_init(p as *mut u8)); + assert_eq!(x, index as i32); + } + } + unsafe { dealloc(ptr as *mut u8, layout) }; +} + +#[kani::proof] +fn check_init_true() { + check_init(true); +} + +#[kani::proof] +fn check_init_any() { + check_init(kani::any()); +} From 5fe13da54badccc687367130b0b114689b57a141 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 28 May 2024 09:18:14 -0700 Subject: [PATCH 02/12] Formatting --- library/kani/src/shadow.rs | 1 - tests/expected/shadow/uninit_array/test.rs | 8 +++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index 7c20e068b1fe..11cbae6ef440 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -10,7 +10,6 @@ pub struct ShadowMem { is_init: [[bool; 64]; 1024], } - impl ShadowMem { pub const fn new() -> Self { Self { is_init: [[false; 64]; 1024] } diff --git a/tests/expected/shadow/uninit_array/test.rs b/tests/expected/shadow/uninit_array/test.rs index 49e0e992ba6d..ca91734a798b 100644 --- a/tests/expected/shadow/uninit_array/test.rs +++ b/tests/expected/shadow/uninit_array/test.rs @@ -6,7 +6,7 @@ use std::alloc::{alloc, dealloc, Layout}; static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(); fn write(ptr: *mut i32, offset: usize, x: i32) { - unsafe { + unsafe { let p = ptr.offset(offset as isize); p.write(x); SM.set_init(p as *mut u8, true); @@ -15,10 +15,12 @@ fn write(ptr: *mut i32, offset: usize, x: i32) { fn check_init(b: bool) { let layout = Layout::array::(5).unwrap(); - let ptr = unsafe { alloc(layout) as *mut i32}; + let ptr = unsafe { alloc(layout) as *mut i32 }; write(ptr, 0, 0); write(ptr, 1, 1); - if b { write(ptr, 2, 2) }; + if b { + write(ptr, 2, 2) + }; write(ptr, 3, 3); write(ptr, 4, 4); let index: usize = kani::any(); From ab0d482a646c559f9baafaf7eac2090096162c30 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 28 May 2024 09:24:13 -0700 Subject: [PATCH 03/12] Mark as unsafe --- library/kani/src/shadow.rs | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index 11cbae6ef440..70dc678988a2 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -15,22 +15,34 @@ impl ShadowMem { Self { is_init: [[false; 64]; 1024] } } - pub fn is_init(&self, ptr: *const u8) -> bool { - read(&self.is_init, ptr) + /// # Safety + /// + /// `ptr` must be valid + pub unsafe fn is_init(&self, ptr: *const u8) -> bool { + unsafe { read(&self.is_init, ptr) } } - pub fn set_init(&mut self, ptr: *const u8, init: bool) { - write(&mut self.is_init, ptr, init); + /// # Safety + /// + /// `ptr` must be valid + pub unsafe fn set_init(&mut self, ptr: *const u8, init: bool) { + unsafe { write(&mut self.is_init, ptr, init) }; } } -pub fn read(sm: &[[bool; 64]; 1024], ptr: *const u8) -> bool { +/// # Safety +/// +/// `ptr` must be valid +pub unsafe fn read(sm: &[[bool; 64]; 1024], ptr: *const u8) -> bool { let obj = unsafe { __KANI_pointer_object(ptr) }; let offset = unsafe { __KANI_pointer_offset(ptr) }; sm[obj][offset] } -pub fn write(sm: &mut [[bool; 64]; 1024], ptr: *const u8, val: bool) { +/// # Safety +/// +/// `ptr` must be valid +pub unsafe fn write(sm: &mut [[bool; 64]; 1024], ptr: *const u8, val: bool) { let obj = unsafe { __KANI_pointer_object(ptr) }; let offset = unsafe { __KANI_pointer_offset(ptr) }; sm[obj][offset] = val; From cad8f44df515a749899e478ac7cd6bce1bf4abfe Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 28 May 2024 10:03:40 -0700 Subject: [PATCH 04/12] Format --- library/kani/src/shadow.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index 70dc678988a2..08dac290e988 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -16,14 +16,14 @@ impl ShadowMem { } /// # Safety - /// + /// /// `ptr` must be valid pub unsafe fn is_init(&self, ptr: *const u8) -> bool { unsafe { read(&self.is_init, ptr) } } /// # Safety - /// + /// /// `ptr` must be valid pub unsafe fn set_init(&mut self, ptr: *const u8, init: bool) { unsafe { write(&mut self.is_init, ptr, init) }; @@ -31,7 +31,7 @@ impl ShadowMem { } /// # Safety -/// +/// /// `ptr` must be valid pub unsafe fn read(sm: &[[bool; 64]; 1024], ptr: *const u8) -> bool { let obj = unsafe { __KANI_pointer_object(ptr) }; @@ -40,7 +40,7 @@ pub unsafe fn read(sm: &[[bool; 64]; 1024], ptr: *const u8) -> bool { } /// # Safety -/// +/// /// `ptr` must be valid pub unsafe fn write(sm: &mut [[bool; 64]; 1024], ptr: *const u8, val: bool) { let obj = unsafe { __KANI_pointer_object(ptr) }; From aca7c2c9d40edc06040af5d0cabc199307420d45 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 28 May 2024 17:43:26 -0700 Subject: [PATCH 05/12] Assert that object id and offset are within supported limits --- library/kani/src/shadow.rs | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index 08dac290e988..d5ad0a41aacb 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -6,13 +6,16 @@ extern "C" { pub fn __KANI_pointer_offset(ptr: *const u8) -> usize; } +const MAX_NUM_OBJECTS: usize = 1024; +const MAX_OBJECT_SIZE: usize = 64; + pub struct ShadowMem { - is_init: [[bool; 64]; 1024], + is_init: [[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], } impl ShadowMem { pub const fn new() -> Self { - Self { is_init: [[false; 64]; 1024] } + Self { is_init: [[false; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] } } /// # Safety @@ -33,17 +36,21 @@ impl ShadowMem { /// # Safety /// /// `ptr` must be valid -pub unsafe fn read(sm: &[[bool; 64]; 1024], ptr: *const u8) -> bool { +pub unsafe fn read(sm: &[[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], ptr: *const u8) -> bool { let obj = unsafe { __KANI_pointer_object(ptr) }; let offset = unsafe { __KANI_pointer_offset(ptr) }; + assert!(obj < MAX_NUM_OBJECTS, "Object index exceeds the maximum number of objects supported by Kani's shadow memory model ({MAX_NUM_OBJECTS})"); + assert!(offset < MAX_OBJECT_SIZE, "Offset into object exceeds the maximum object size supported by Kani's shadow memory model ({MAX_OBJECT_SIZE})"); sm[obj][offset] } /// # Safety /// /// `ptr` must be valid -pub unsafe fn write(sm: &mut [[bool; 64]; 1024], ptr: *const u8, val: bool) { +pub unsafe fn write(sm: &mut [[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], ptr: *const u8, val: bool) { let obj = unsafe { __KANI_pointer_object(ptr) }; let offset = unsafe { __KANI_pointer_offset(ptr) }; + assert!(obj < MAX_NUM_OBJECTS, "Object index exceeds the maximum number of objects supported by Kani's shadow memory model (1024)"); + assert!(offset < MAX_OBJECT_SIZE, "Offset into object exceeds the maximum object size supported by Kani's shadow memory model (64)"); sm[obj][offset] = val; } From 021b25547b7557b08c18151c51e63d615da3fbdc Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 30 May 2024 10:40:18 -0700 Subject: [PATCH 06/12] Add tests that check the limits of the shadow memory model --- library/kani/src/shadow.rs | 18 ++++++-- .../shadow/unsupported_num_objects/expected | 3 ++ .../shadow/unsupported_num_objects/test.rs | 46 +++++++++++++++++++ .../shadow/unsupported_object_size/expected | 3 ++ .../shadow/unsupported_object_size/test.rs | 28 +++++++++++ 5 files changed, 93 insertions(+), 5 deletions(-) create mode 100644 tests/expected/shadow/unsupported_num_objects/expected create mode 100644 tests/expected/shadow/unsupported_num_objects/test.rs create mode 100644 tests/expected/shadow/unsupported_object_size/expected create mode 100644 tests/expected/shadow/unsupported_object_size/test.rs diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index d5ad0a41aacb..d10abedd7c91 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -33,24 +33,32 @@ impl ShadowMem { } } +const MAX_NUM_OBJECTS_ASSERT_MSG: &str = "The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024)"; +const MAX_OBJECT_SIZE_ASSERT_MSG: &str = + "The object size exceeds the maximum size supported by Kani's shadow memory model (64)"; + /// # Safety /// /// `ptr` must be valid pub unsafe fn read(sm: &[[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], ptr: *const u8) -> bool { let obj = unsafe { __KANI_pointer_object(ptr) }; let offset = unsafe { __KANI_pointer_offset(ptr) }; - assert!(obj < MAX_NUM_OBJECTS, "Object index exceeds the maximum number of objects supported by Kani's shadow memory model ({MAX_NUM_OBJECTS})"); - assert!(offset < MAX_OBJECT_SIZE, "Offset into object exceeds the maximum object size supported by Kani's shadow memory model ({MAX_OBJECT_SIZE})"); + crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); + crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG); sm[obj][offset] } /// # Safety /// /// `ptr` must be valid -pub unsafe fn write(sm: &mut [[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], ptr: *const u8, val: bool) { +pub unsafe fn write( + sm: &mut [[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], + ptr: *const u8, + val: bool, +) { let obj = unsafe { __KANI_pointer_object(ptr) }; let offset = unsafe { __KANI_pointer_offset(ptr) }; - assert!(obj < MAX_NUM_OBJECTS, "Object index exceeds the maximum number of objects supported by Kani's shadow memory model (1024)"); - assert!(offset < MAX_OBJECT_SIZE, "Offset into object exceeds the maximum object size supported by Kani's shadow memory model (64)"); + crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); + crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG); sm[obj][offset] = val; } diff --git a/tests/expected/shadow/unsupported_num_objects/expected b/tests/expected/shadow/unsupported_num_objects/expected new file mode 100644 index 000000000000..da3b5a671969 --- /dev/null +++ b/tests/expected/shadow/unsupported_num_objects/expected @@ -0,0 +1,3 @@ +Failed Checks: The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024) +Verification failed for - check_max_objects_fail +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs new file mode 100644 index 000000000000..70aa80166ef6 --- /dev/null +++ b/tests/expected/shadow/unsupported_num_objects/test.rs @@ -0,0 +1,46 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks the maximum number of objects supported by Kani's shadow +// memory model (currently 1024) + +static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(); + +fn check_max_objects() { + let mut i = 0; + // A dummy loop that creates `N`` objects. + // After the loop, CBMC's object ID counter should be at `N` + 2: + // - `N` created in the loop + + // - the NULL pointer whose object ID is 0, and + // - the object ID for `i` + while i < N { + let x = i; + assert_eq!( + unsafe { kani::shadow::__KANI_pointer_object(&x as *const usize as *const u8) }, + i + 2 + ); + i += 1; + } + + // create a new object whose ID is `N` + 2 + let x = 42; + assert_eq!( + unsafe { kani::shadow::__KANI_pointer_object(&x as *const i32 as *const u8) }, + N + 2 + ); + // the following call to `set_init` would fail if the object ID for `x` + // exceeds the maximum allowed by Kani's shadow memory model + unsafe { + SM.set_init(&x as *const i32 as *const u8, true); + } +} + +#[kani::proof] +fn check_max_objects_pass() { + check_max_objects::<1021>(); +} + +#[kani::proof] +fn check_max_objects_fail() { + check_max_objects::<1022>(); +} diff --git a/tests/expected/shadow/unsupported_object_size/expected b/tests/expected/shadow/unsupported_object_size/expected new file mode 100644 index 000000000000..a4598b5aac82 --- /dev/null +++ b/tests/expected/shadow/unsupported_object_size/expected @@ -0,0 +1,3 @@ +Failed Checks: The object size exceeds the maximum size supported by Kani's shadow memory model (64) +Verification failed for - check_max_object_size_fail +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/shadow/unsupported_object_size/test.rs b/tests/expected/shadow/unsupported_object_size/test.rs new file mode 100644 index 000000000000..3179469101c9 --- /dev/null +++ b/tests/expected/shadow/unsupported_object_size/test.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks the maximum object size supported by Kani's shadow +// memory model (currently 64) + +static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(); + +fn check_max_objects() { + let arr: [u8; N] = [0; N]; + let last = &arr[N - 1]; + assert_eq!(unsafe { kani::shadow::__KANI_pointer_offset(last as *const u8) }, N - 1); + // the following call to `set_init` would fail if the object offset for + // `last` exceeds the maximum allowed by Kani's shadow memory model + unsafe { + SM.set_init(last as *const u8, true); + } +} + +#[kani::proof] +fn check_max_object_size_pass() { + check_max_objects::<64>(); +} + +#[kani::proof] +fn check_max_object_size_fail() { + check_max_objects::<65>(); +} From 48f118e7e12a2f11f2235a83a6f0a3d1cfd1e022 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 31 May 2024 14:56:55 -0700 Subject: [PATCH 07/12] Reimplement using hooks for pointer object and offset --- .../codegen_cprover_gotoc/overrides/hooks.rs | 72 +++++++++++++++++++ library/kani/kani_lib.c | 8 --- library/kani/src/mem.rs | 14 ++++ library/kani/src/shadow.rs | 51 ++++--------- .../shadow/unsupported_num_objects/test.rs | 4 +- .../shadow/unsupported_object_size/test.rs | 2 +- 6 files changed, 103 insertions(+), 48 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 9f70c16430e5..522e3a961362 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -242,6 +242,76 @@ impl GotocHook for IsAllocated { } } +/// Encodes __CPROVER_pointer_object(ptr) +struct PointerObject; +impl GotocHook for PointerObject { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + matches_function(tcx, instance.def, "KaniPointerObject") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 1); + let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer()); + let target = target.unwrap(); + let loc = gcx.codegen_caller_span_stable(span); + let ret_place = + unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to)); + let ret_type = ret_place.goto_expr.typ().clone(); + + Stmt::block( + vec![ + ret_place.goto_expr.assign(Expr::pointer_object(ptr).cast_to(ret_type), loc), + Stmt::goto(bb_label(target), loc), + ], + loc, + ) + } +} + +/// Encodes __CPROVER_pointer_offset(ptr) +struct PointerOffset; +impl GotocHook for PointerOffset { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + matches_function(tcx, instance.def, "KaniPointerOffset") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 1); + let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer()); + let target = target.unwrap(); + let loc = gcx.codegen_caller_span_stable(span); + let ret_place = + unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to)); + let ret_type = ret_place.goto_expr.typ().clone(); + + Stmt::block( + vec![ + ret_place.goto_expr.assign(Expr::pointer_offset(ptr).cast_to(ret_type), loc), + Stmt::goto(bb_label(target), loc), + ], + loc, + ) + } +} + + + struct RustAlloc; // Removing this hook causes regression failures. // https://github.com/model-checking/kani/issues/1170 @@ -399,6 +469,8 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(Cover), Rc::new(Nondet), Rc::new(IsAllocated), + Rc::new(PointerObject), + Rc::new(PointerOffset), Rc::new(RustAlloc), Rc::new(MemCmp), Rc::new(UntrackedDeref), diff --git a/library/kani/kani_lib.c b/library/kani/kani_lib.c index f9f13ab1c21e..b077547b10d7 100644 --- a/library/kani/kani_lib.c +++ b/library/kani/kani_lib.c @@ -118,11 +118,3 @@ uint8_t *__rust_realloc(uint8_t *ptr, size_t old_size, size_t align, size_t new_ return result; } - -size_t __KANI_pointer_object(uint8_t *ptr) { - return __CPROVER_POINTER_OBJECT(ptr); -} - -size_t __KANI_pointer_offset(uint8_t *ptr) { - return __CPROVER_POINTER_OFFSET(ptr); -} diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index c485ee16a562..c40a1aa696e3 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -290,6 +290,20 @@ unsafe fn has_valid_value(_ptr: *const T) -> bool { kani_intrinsic() } +/// Get the object ID of the given pointer. +#[rustc_diagnostic_item = "KaniPointerObject"] +#[inline(never)] +pub fn pointer_object(_ptr: *const T) -> usize { + kani_intrinsic() +} + +/// Get the object offset of the given pointer. +#[rustc_diagnostic_item = "KaniPointerOffset"] +#[inline(never)] +pub fn pointer_offset(_ptr: *const T) -> usize { + kani_intrinsic() +} + #[cfg(test)] mod tests { use super::{can_dereference, can_write, PtrProperties}; diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index d10abedd7c91..81e3a4c98f9d 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -1,14 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -extern "C" { - pub fn __KANI_pointer_object(ptr: *const u8) -> usize; - pub fn __KANI_pointer_offset(ptr: *const u8) -> usize; -} - const MAX_NUM_OBJECTS: usize = 1024; const MAX_OBJECT_SIZE: usize = 64; +const MAX_NUM_OBJECTS_ASSERT_MSG: &str = "The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024)"; +const MAX_OBJECT_SIZE_ASSERT_MSG: &str = + "The object size exceeds the maximum size supported by Kani's shadow memory model (64)"; + pub struct ShadowMem { is_init: [[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], } @@ -22,43 +21,21 @@ impl ShadowMem { /// /// `ptr` must be valid pub unsafe fn is_init(&self, ptr: *const u8) -> bool { - unsafe { read(&self.is_init, ptr) } + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); + crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG); + self.is_init[obj][offset] } /// # Safety /// /// `ptr` must be valid pub unsafe fn set_init(&mut self, ptr: *const u8, init: bool) { - unsafe { write(&mut self.is_init, ptr, init) }; + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); + crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG); + self.is_init[obj][offset] = init; } } - -const MAX_NUM_OBJECTS_ASSERT_MSG: &str = "The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024)"; -const MAX_OBJECT_SIZE_ASSERT_MSG: &str = - "The object size exceeds the maximum size supported by Kani's shadow memory model (64)"; - -/// # Safety -/// -/// `ptr` must be valid -pub unsafe fn read(sm: &[[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], ptr: *const u8) -> bool { - let obj = unsafe { __KANI_pointer_object(ptr) }; - let offset = unsafe { __KANI_pointer_offset(ptr) }; - crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); - crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG); - sm[obj][offset] -} - -/// # Safety -/// -/// `ptr` must be valid -pub unsafe fn write( - sm: &mut [[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], - ptr: *const u8, - val: bool, -) { - let obj = unsafe { __KANI_pointer_object(ptr) }; - let offset = unsafe { __KANI_pointer_offset(ptr) }; - crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); - crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG); - sm[obj][offset] = val; -} diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs index 70aa80166ef6..d97af5477e82 100644 --- a/tests/expected/shadow/unsupported_num_objects/test.rs +++ b/tests/expected/shadow/unsupported_num_objects/test.rs @@ -16,7 +16,7 @@ fn check_max_objects() { while i < N { let x = i; assert_eq!( - unsafe { kani::shadow::__KANI_pointer_object(&x as *const usize as *const u8) }, + kani::mem::pointer_object(&x as *const usize as *const u8), i + 2 ); i += 1; @@ -25,7 +25,7 @@ fn check_max_objects() { // create a new object whose ID is `N` + 2 let x = 42; assert_eq!( - unsafe { kani::shadow::__KANI_pointer_object(&x as *const i32 as *const u8) }, + kani::mem::pointer_object(&x as *const i32 as *const u8), N + 2 ); // the following call to `set_init` would fail if the object ID for `x` diff --git a/tests/expected/shadow/unsupported_object_size/test.rs b/tests/expected/shadow/unsupported_object_size/test.rs index 3179469101c9..1b460696dd34 100644 --- a/tests/expected/shadow/unsupported_object_size/test.rs +++ b/tests/expected/shadow/unsupported_object_size/test.rs @@ -9,7 +9,7 @@ static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(); fn check_max_objects() { let arr: [u8; N] = [0; N]; let last = &arr[N - 1]; - assert_eq!(unsafe { kani::shadow::__KANI_pointer_offset(last as *const u8) }, N - 1); + assert_eq!(kani::mem::pointer_offset(last as *const u8), N - 1); // the following call to `set_init` would fail if the object offset for // `last` exceeds the maximum allowed by Kani's shadow memory model unsafe { From fe78b69cecb4aa805a17b7672c260aa6b3ecbde4 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 31 May 2024 15:01:45 -0700 Subject: [PATCH 08/12] Make shadow memory struct generic --- library/kani/src/shadow.rs | 26 ++++++++----------- tests/expected/shadow/uninit_array/test.rs | 6 ++--- .../shadow/unsupported_num_objects/test.rs | 8 +++--- .../shadow/unsupported_object_size/test.rs | 4 +-- 4 files changed, 20 insertions(+), 24 deletions(-) diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index 81e3a4c98f9d..f103f51ce33e 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -8,34 +8,30 @@ const MAX_NUM_OBJECTS_ASSERT_MSG: &str = "The number of objects exceeds the maxi const MAX_OBJECT_SIZE_ASSERT_MSG: &str = "The object size exceeds the maximum size supported by Kani's shadow memory model (64)"; -pub struct ShadowMem { - is_init: [[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], +pub struct ShadowMem { + mem: [[T; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], } -impl ShadowMem { - pub const fn new() -> Self { - Self { is_init: [[false; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] } +impl ShadowMem { + pub const fn new(val: T) -> Self { + Self { mem: [[val; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] } } - /// # Safety - /// - /// `ptr` must be valid - pub unsafe fn is_init(&self, ptr: *const u8) -> bool { + /// Get the shadow memory value of the given pointer + pub fn get(&self, ptr: *const u8) -> T { let obj = crate::mem::pointer_object(ptr); let offset = crate::mem::pointer_offset(ptr); crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG); - self.is_init[obj][offset] + self.mem[obj][offset] } - /// # Safety - /// - /// `ptr` must be valid - pub unsafe fn set_init(&mut self, ptr: *const u8, init: bool) { + /// Set the shadow memory value of the given pointer + pub fn set(&mut self, ptr: *const u8, val: T) { let obj = crate::mem::pointer_object(ptr); let offset = crate::mem::pointer_offset(ptr); crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG); - self.is_init[obj][offset] = init; + self.mem[obj][offset] = val; } } diff --git a/tests/expected/shadow/uninit_array/test.rs b/tests/expected/shadow/uninit_array/test.rs index ca91734a798b..59fdb46267b5 100644 --- a/tests/expected/shadow/uninit_array/test.rs +++ b/tests/expected/shadow/uninit_array/test.rs @@ -3,13 +3,13 @@ use std::alloc::{alloc, dealloc, Layout}; -static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(); +static mut SM: kani::shadow::ShadowMem:: = kani::shadow::ShadowMem::new(false); fn write(ptr: *mut i32, offset: usize, x: i32) { unsafe { let p = ptr.offset(offset as isize); p.write(x); - SM.set_init(p as *mut u8, true); + SM.set(p as *mut u8, true); }; } @@ -28,7 +28,7 @@ fn check_init(b: bool) { unsafe { let p = ptr.offset(index as isize); let x = p.read(); - assert!(SM.is_init(p as *mut u8)); + assert!(SM.get(p as *mut u8)); assert_eq!(x, index as i32); } } diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs index d97af5477e82..8206508ca171 100644 --- a/tests/expected/shadow/unsupported_num_objects/test.rs +++ b/tests/expected/shadow/unsupported_num_objects/test.rs @@ -4,7 +4,7 @@ // This test checks the maximum number of objects supported by Kani's shadow // memory model (currently 1024) -static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(); +static mut SM: kani::shadow::ShadowMem:: = kani::shadow::ShadowMem::new(false); fn check_max_objects() { let mut i = 0; @@ -28,10 +28,10 @@ fn check_max_objects() { kani::mem::pointer_object(&x as *const i32 as *const u8), N + 2 ); - // the following call to `set_init` would fail if the object ID for `x` - // exceeds the maximum allowed by Kani's shadow memory model + // the following call to `set` would fail if the object ID for `x` exceeds + // the maximum allowed by Kani's shadow memory model unsafe { - SM.set_init(&x as *const i32 as *const u8, true); + SM.set(&x as *const i32 as *const u8, true); } } diff --git a/tests/expected/shadow/unsupported_object_size/test.rs b/tests/expected/shadow/unsupported_object_size/test.rs index 1b460696dd34..c29cb7a6cbd1 100644 --- a/tests/expected/shadow/unsupported_object_size/test.rs +++ b/tests/expected/shadow/unsupported_object_size/test.rs @@ -4,7 +4,7 @@ // This test checks the maximum object size supported by Kani's shadow // memory model (currently 64) -static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(); +static mut SM: kani::shadow::ShadowMem:: = kani::shadow::ShadowMem::new(false); fn check_max_objects() { let arr: [u8; N] = [0; N]; @@ -13,7 +13,7 @@ fn check_max_objects() { // the following call to `set_init` would fail if the object offset for // `last` exceeds the maximum allowed by Kani's shadow memory model unsafe { - SM.set_init(last as *const u8, true); + SM.set(last as *const u8, true); } } From 14bfd965add8156d2d43cbed579acb3052e1befa Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 31 May 2024 15:31:05 -0700 Subject: [PATCH 09/12] Make pointer generic --- library/kani/src/shadow.rs | 4 ++-- tests/expected/shadow/uninit_array/expected | 2 +- tests/expected/shadow/uninit_array/test.rs | 24 ++++++++++++++----- .../shadow/unsupported_num_objects/test.rs | 6 ++--- 4 files changed, 24 insertions(+), 12 deletions(-) diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index f103f51ce33e..f21def49e919 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -18,7 +18,7 @@ impl ShadowMem { } /// Get the shadow memory value of the given pointer - pub fn get(&self, ptr: *const u8) -> T { + pub fn get(&self, ptr: *const U) -> T { let obj = crate::mem::pointer_object(ptr); let offset = crate::mem::pointer_offset(ptr); crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); @@ -27,7 +27,7 @@ impl ShadowMem { } /// Set the shadow memory value of the given pointer - pub fn set(&mut self, ptr: *const u8, val: T) { + pub fn set(&mut self, ptr: *const U, val: T) { let obj = crate::mem::pointer_object(ptr); let offset = crate::mem::pointer_offset(ptr); crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG); diff --git a/tests/expected/shadow/uninit_array/expected b/tests/expected/shadow/uninit_array/expected index 14c64787704e..1d5f70698010 100644 --- a/tests/expected/shadow/uninit_array/expected +++ b/tests/expected/shadow/uninit_array/expected @@ -1,3 +1,3 @@ -Failed Checks: assertion failed: SM.is_init(p as *mut u8) +Failed Checks: assertion failed: SM.get(p) Verification failed for - check_init_any Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/shadow/uninit_array/test.rs b/tests/expected/shadow/uninit_array/test.rs index 59fdb46267b5..604481312c74 100644 --- a/tests/expected/shadow/uninit_array/test.rs +++ b/tests/expected/shadow/uninit_array/test.rs @@ -1,21 +1,28 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// This is a basic test for the shadow memory implementation. +// It checks that shadow memory can be used to track whether a memory location +// is initialized. + use std::alloc::{alloc, dealloc, Layout}; static mut SM: kani::shadow::ShadowMem:: = kani::shadow::ShadowMem::new(false); -fn write(ptr: *mut i32, offset: usize, x: i32) { +fn write(ptr: *mut i8, offset: usize, x: i8) { unsafe { let p = ptr.offset(offset as isize); p.write(x); - SM.set(p as *mut u8, true); + SM.set(p as *const i8, true); }; } fn check_init(b: bool) { - let layout = Layout::array::(5).unwrap(); - let ptr = unsafe { alloc(layout) as *mut i32 }; + // allocate an array of 5 i8's + let layout = Layout::array::(5).unwrap(); + let ptr = unsafe { alloc(layout) as *mut i8 }; + + // unconditionally write to all 5 locations except for the middle element write(ptr, 0, 0); write(ptr, 1, 1); if b { @@ -23,13 +30,18 @@ fn check_init(b: bool) { }; write(ptr, 3, 3); write(ptr, 4, 4); + + // non-deterministically read from any of the elements and assert that: + // 1. The memory location is initialized + // 2. It has the expected value + // This would fail if `b` is false and `index == 2` let index: usize = kani::any(); if index < 5 { unsafe { let p = ptr.offset(index as isize); let x = p.read(); - assert!(SM.get(p as *mut u8)); - assert_eq!(x, index as i32); + assert!(SM.get(p)); + assert_eq!(x, index as i8); } } unsafe { dealloc(ptr as *mut u8, layout) }; diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs index 8206508ca171..7a069e651f45 100644 --- a/tests/expected/shadow/unsupported_num_objects/test.rs +++ b/tests/expected/shadow/unsupported_num_objects/test.rs @@ -16,7 +16,7 @@ fn check_max_objects() { while i < N { let x = i; assert_eq!( - kani::mem::pointer_object(&x as *const usize as *const u8), + kani::mem::pointer_object(&x as *const usize), i + 2 ); i += 1; @@ -25,13 +25,13 @@ fn check_max_objects() { // create a new object whose ID is `N` + 2 let x = 42; assert_eq!( - kani::mem::pointer_object(&x as *const i32 as *const u8), + kani::mem::pointer_object(&x as *const i32), N + 2 ); // the following call to `set` would fail if the object ID for `x` exceeds // the maximum allowed by Kani's shadow memory model unsafe { - SM.set(&x as *const i32 as *const u8, true); + SM.set(&x as *const i32, true); } } From 3ff7da0117cc6bb5e89ec20451be8bd069d399a4 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 31 May 2024 15:55:00 -0700 Subject: [PATCH 10/12] Mark APIs as unstable --- .../src/codegen_cprover_gotoc/overrides/hooks.rs | 2 -- kani_metadata/src/unstable.rs | 2 ++ library/kani/src/shadow.rs | 16 ++++++++++++++++ tests/expected/shadow/uninit_array/test.rs | 3 ++- .../shadow/unsupported_num_objects/test.rs | 13 ++++--------- .../shadow/unsupported_object_size/test.rs | 3 ++- 6 files changed, 26 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 522e3a961362..9b2f9e770d32 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -310,8 +310,6 @@ impl GotocHook for PointerOffset { } } - - struct RustAlloc; // Removing this hook causes regression failures. // https://github.com/model-checking/kani/issues/1170 diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 878b468dbdc3..d7b73678a836 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -87,6 +87,8 @@ pub enum UnstableFeature { /// Automatically check that no invalid value is produced which is considered UB in Rust. /// Note that this does not include checking uninitialized value. ValidValueChecks, + /// Ghost state and shadow memory APIs + GhostState, } impl UnstableFeature { diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index f21def49e919..3c51757a4125 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -13,11 +13,22 @@ pub struct ShadowMem { } impl ShadowMem { + /// Create a new shadow memory instance initialized with the given value + #[crate::unstable( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" + )] pub const fn new(val: T) -> Self { Self { mem: [[val; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] } } /// Get the shadow memory value of the given pointer + #[crate::unstable( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" + )] pub fn get(&self, ptr: *const U) -> T { let obj = crate::mem::pointer_object(ptr); let offset = crate::mem::pointer_offset(ptr); @@ -27,6 +38,11 @@ impl ShadowMem { } /// Set the shadow memory value of the given pointer + #[crate::unstable( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" + )] pub fn set(&mut self, ptr: *const U, val: T) { let obj = crate::mem::pointer_object(ptr); let offset = crate::mem::pointer_offset(ptr); diff --git a/tests/expected/shadow/uninit_array/test.rs b/tests/expected/shadow/uninit_array/test.rs index 604481312c74..8a9536e5a8e8 100644 --- a/tests/expected/shadow/uninit_array/test.rs +++ b/tests/expected/shadow/uninit_array/test.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zghost-state // This is a basic test for the shadow memory implementation. // It checks that shadow memory can be used to track whether a memory location @@ -7,7 +8,7 @@ use std::alloc::{alloc, dealloc, Layout}; -static mut SM: kani::shadow::ShadowMem:: = kani::shadow::ShadowMem::new(false); +static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(false); fn write(ptr: *mut i8, offset: usize, x: i8) { unsafe { diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs index 7a069e651f45..f60d0020e989 100644 --- a/tests/expected/shadow/unsupported_num_objects/test.rs +++ b/tests/expected/shadow/unsupported_num_objects/test.rs @@ -1,10 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zghost-state // This test checks the maximum number of objects supported by Kani's shadow // memory model (currently 1024) -static mut SM: kani::shadow::ShadowMem:: = kani::shadow::ShadowMem::new(false); +static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(false); fn check_max_objects() { let mut i = 0; @@ -15,19 +16,13 @@ fn check_max_objects() { // - the object ID for `i` while i < N { let x = i; - assert_eq!( - kani::mem::pointer_object(&x as *const usize), - i + 2 - ); + assert_eq!(kani::mem::pointer_object(&x as *const usize), i + 2); i += 1; } // create a new object whose ID is `N` + 2 let x = 42; - assert_eq!( - kani::mem::pointer_object(&x as *const i32), - N + 2 - ); + assert_eq!(kani::mem::pointer_object(&x as *const i32), N + 2); // the following call to `set` would fail if the object ID for `x` exceeds // the maximum allowed by Kani's shadow memory model unsafe { diff --git a/tests/expected/shadow/unsupported_object_size/test.rs b/tests/expected/shadow/unsupported_object_size/test.rs index c29cb7a6cbd1..d22ff1a6ca41 100644 --- a/tests/expected/shadow/unsupported_object_size/test.rs +++ b/tests/expected/shadow/unsupported_object_size/test.rs @@ -1,10 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zghost-state // This test checks the maximum object size supported by Kani's shadow // memory model (currently 64) -static mut SM: kani::shadow::ShadowMem:: = kani::shadow::ShadowMem::new(false); +static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(false); fn check_max_objects() { let arr: [u8; N] = [0; N]; From 4afa0955786003a9c8114e6d3aad42dc2d61e328 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 31 May 2024 15:58:41 -0700 Subject: [PATCH 11/12] Removed foreign functions which are no longer necessary --- .../src/codegen_cprover_gotoc/codegen/foreign_function.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 4584daa57c23..4ab72eb3a705 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -35,8 +35,6 @@ lazy_static! { "__rust_alloc_zeroed".into(), "__rust_dealloc".into(), "__rust_realloc".into(), - "__KANI_pointer_object".into(), - "__KANI_pointer_offset".into(), ]) }; } From 4490c38a1c980f0e32054d691330ae2172efd306 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 31 May 2024 16:26:23 -0700 Subject: [PATCH 12/12] Add module documentation --- library/kani/src/shadow.rs | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index 3c51757a4125..a7ea57c6fd40 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -1,6 +1,32 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains an API for shadow memory. +//! Shadow memory is a mechanism by which we can store metadata on memory +//! locations, e.g. whether a memory location is initialized. +//! +//! The main data structure provided by this module is the `ShadowMem` struct, +//! which allows us to store metadata on a given memory location. +//! +//! # Example +//! +//! ``` +//! use kani::shadow::ShadowMem; +//! use std::alloc::{alloc, Layout}; +//! +//! let mut sm = ShadowMem::new(false); +//! +//! unsafe { +//! let ptr = alloc(Layout::new::()); +//! // assert the memory location is not initialized +//! assert!(!sm.get(ptr)); +//! // write to the memory location +//! *ptr = 42; +//! // update the shadow memory to indicate that this location is now initialized +//! sm.set(ptr, true); +//! } +//! ``` + const MAX_NUM_OBJECTS: usize = 1024; const MAX_OBJECT_SIZE: usize = 64; @@ -8,6 +34,10 @@ const MAX_NUM_OBJECTS_ASSERT_MSG: &str = "The number of objects exceeds the maxi const MAX_OBJECT_SIZE_ASSERT_MSG: &str = "The object size exceeds the maximum size supported by Kani's shadow memory model (64)"; +/// A shadow memory data structure that contains a two-dimensional array of a +/// generic type `T`. +/// Each element of the outer array represents an object, and each element of +/// the inner array represents a byte in the object. pub struct ShadowMem { mem: [[T; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], }