From b07fc4e09acb6eb86b5bce90191c6990c6d05ffb Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 6 Jun 2024 16:58:11 -0700 Subject: [PATCH 1/2] Add a few examples of using shadow memory to check initialization of slices --- .../shadow/slices/slice_of_array/expected | 1 + .../shadow/slices/slice_of_array/test.rs | 30 ++++++++++++++++++ .../shadow/slices/slice_reverse/expected | 1 + .../shadow/slices/slice_reverse/test.rs | 24 ++++++++++++++ .../shadow/slices/slice_split/expected | 1 + .../shadow/slices/slice_split/test.rs | 31 +++++++++++++++++++ 6 files changed, 88 insertions(+) create mode 100644 tests/expected/shadow/slices/slice_of_array/expected create mode 100644 tests/expected/shadow/slices/slice_of_array/test.rs create mode 100644 tests/expected/shadow/slices/slice_reverse/expected create mode 100644 tests/expected/shadow/slices/slice_reverse/test.rs create mode 100644 tests/expected/shadow/slices/slice_split/expected create mode 100644 tests/expected/shadow/slices/slice_split/test.rs diff --git a/tests/expected/shadow/slices/slice_of_array/expected b/tests/expected/shadow/slices/slice_of_array/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/shadow/slices/slice_of_array/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/shadow/slices/slice_of_array/test.rs b/tests/expected/shadow/slices/slice_of_array/test.rs new file mode 100644 index 000000000000..d004ab3df19b --- /dev/null +++ b/tests/expected/shadow/slices/slice_of_array/test.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zghost-state + +// Check that every element of an arbitrary slice of an array is initialized + +const N: usize = 16; + +static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(false); + +#[kani::proof] +#[kani::unwind(31)] +fn check_slice_init() { + let arr: [char; N] = kani::any(); + // tag every element of the array as initialized + for i in &arr { + unsafe { + SM.set(i as *const char, true); + } + } + // create an arbitrary slice of the array + let end: usize = kani::any_where(|x| *x <= N); + let begin: usize = kani::any_where(|x| *x < end); + let slice = &arr[begin..end]; + + // verify that all elements of the slice are initialized + for i in slice { + assert!(unsafe { SM.get(i as *const char) }); + } +} diff --git a/tests/expected/shadow/slices/slice_reverse/expected b/tests/expected/shadow/slices/slice_reverse/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/shadow/slices/slice_reverse/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/shadow/slices/slice_reverse/test.rs b/tests/expected/shadow/slices/slice_reverse/test.rs new file mode 100644 index 000000000000..9ab833619ef3 --- /dev/null +++ b/tests/expected/shadow/slices/slice_reverse/test.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zghost-state + +// Check that every element of a reversed slice are initialized + +const N: usize = 32; + +static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(false); + +#[kani::proof] +fn check_reverse() { + let mut a: [u16; N] = kani::any(); + for i in &a { + unsafe { SM.set(i as *const u16, true) }; + } + a.reverse(); + + for i in &a { + unsafe { + assert!(SM.get(i as *const u16)); + } + } +} diff --git a/tests/expected/shadow/slices/slice_split/expected b/tests/expected/shadow/slices/slice_split/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/shadow/slices/slice_split/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/shadow/slices/slice_split/test.rs b/tests/expected/shadow/slices/slice_split/test.rs new file mode 100644 index 000000000000..a14298b7add2 --- /dev/null +++ b/tests/expected/shadow/slices/slice_split/test.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zghost-state + +// Check that every element of a slice split into two is initialized + +const N: usize = 16; + +static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(false); + +#[kani::proof] +#[kani::unwind(17)] +fn check_reverse() { + let a: [bool; N] = kani::any(); + for i in &a { + unsafe { SM.set(i as *const bool, true) }; + } + let index: usize = kani::any_where(|x| *x <= N); + let (s1, s2) = a.split_at_checked(index).unwrap(); + + for i in s1 { + unsafe { + assert!(SM.get(i as *const bool)); + } + } + for i in s2 { + unsafe { + assert!(SM.get(i as *const bool)); + } + } +} From ca50c918c5b7b4060f6b2d8c321d7e45a92d728c Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 16 Jul 2024 16:13:36 -0700 Subject: [PATCH 2/2] Clarify what the tests are checking --- tests/expected/shadow/slices/slice_of_array/test.rs | 6 +++++- tests/expected/shadow/slices/slice_reverse/test.rs | 6 +++++- tests/expected/shadow/slices/slice_split/test.rs | 6 +++++- 3 files changed, 15 insertions(+), 3 deletions(-) diff --git a/tests/expected/shadow/slices/slice_of_array/test.rs b/tests/expected/shadow/slices/slice_of_array/test.rs index d004ab3df19b..b5ac3abae126 100644 --- a/tests/expected/shadow/slices/slice_of_array/test.rs +++ b/tests/expected/shadow/slices/slice_of_array/test.rs @@ -2,7 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zghost-state -// Check that every element of an arbitrary slice of an array is initialized +// This test demonstrates a possible usage of the shadow memory API to check that +// every element of an arbitrary slice of an array is initialized. +// Since the instrumentation is done manually in the harness only but not inside +// the library functions, the test only verifies that the slices point to memory +// that is within the original array. const N: usize = 16; diff --git a/tests/expected/shadow/slices/slice_reverse/test.rs b/tests/expected/shadow/slices/slice_reverse/test.rs index 9ab833619ef3..4810958e2fe1 100644 --- a/tests/expected/shadow/slices/slice_reverse/test.rs +++ b/tests/expected/shadow/slices/slice_reverse/test.rs @@ -2,7 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zghost-state -// Check that every element of a reversed slice are initialized +// This test demonstrates a possible usage of the shadow memory API to check that +// every element of a reversed array is initialized. +// Since the instrumentation is done manually in the harness only but not inside +// the `reverse` function, the test only verifies that the resulting array +// occupies the same memory as the original one. const N: usize = 32; diff --git a/tests/expected/shadow/slices/slice_split/test.rs b/tests/expected/shadow/slices/slice_split/test.rs index a14298b7add2..273d717572d1 100644 --- a/tests/expected/shadow/slices/slice_split/test.rs +++ b/tests/expected/shadow/slices/slice_split/test.rs @@ -2,7 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zghost-state -// Check that every element of a slice split into two is initialized +// This test demonstrates a possible usage of the shadow memory API to check that +// every element of an array split into two slices is initialized. +// Since the instrumentation is done manually in the harness only but not inside +// the `split_at_checked` function, the test only verifies that the resulting +// slices occupy the same memory as the original array. const N: usize = 16;