Skip to content

Commit

Permalink
Add tests where an instruction gets instrumented more than once
Browse files Browse the repository at this point in the history
  • Loading branch information
artemagvanian committed Aug 22, 2024
1 parent db25dca commit f3553cf
Show file tree
Hide file tree
Showing 2 changed files with 62 additions and 0 deletions.
20 changes: 20 additions & 0 deletions tests/expected/uninit/multiple-instrumentations.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
multiple_instrumentations_different_vars.assertion.3\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

multiple_instrumentations_different_vars.assertion.4\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"

multiple_instrumentations.assertion.2\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

multiple_instrumentations.assertion.3\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

Summary:
Verification failed for - multiple_instrumentations_different_vars
Verification failed for - multiple_instrumentations
Complete - 0 successfully verified harnesses, 2 failures, 2 total.
42 changes: 42 additions & 0 deletions tests/expected/uninit/multiple-instrumentations.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Z uninit-checks

/// Ensure instrumentation works correctly when a single instruction gets multiple instrumentations.
#[kani::proof]
fn multiple_instrumentations() {
unsafe {
let mut value: u128 = 0;
// Cast between two pointers of different padding.
let ptr = &mut value as *mut _ as *mut (u8, u32, u64);
*ptr = (4, 4, 4);
// Here, instrumentation is added 2 times before the function call and 1 time after.
value = helper_1(value, value);
}
}

fn helper_1(a: u128, b: u128) -> u128 {
a + b
}

/// Ensure instrumentation works correctly when a single instruction gets multiple instrumentations
/// (and variables are different).
#[kani::proof]
fn multiple_instrumentations_different_vars() {
unsafe {
let mut a: u128 = 0;
let mut b: u64 = 0;
// Cast between two pointers of different padding.
let ptr_a = &mut a as *mut _ as *mut (u8, u32, u64);
*ptr_a = (4, 4, 4);
// Cast between two pointers of different padding.
let ptr_b = &mut b as *mut _ as *mut (u8, u32);
*ptr_b = (4, 4);
// Here, instrumentation is added 2 times before the function call and 1 time after.
a = helper_2(a, b);
}
}

fn helper_2(a: u128, b: u64) -> u128 {
a + (b as u128)
}

0 comments on commit f3553cf

Please sign in to comment.