Concrete playback feature generates tests that fail Kani assertions #3787

gogdavz · 2024-12-16T20:25:16Z

I came across some scenarios where concrete playback in Kani generates tests that fail assertions in Kani, instead of the code being analyzed. This seems to be mismatch in expected deterministic values captured in the Kani verifier failures.

This was reproduced in the following test file. Reproduced in simple test file included below.

The two errors encountered are:

assertion left == right failed
Not enough det vals found

This occurred on:

$ rustup show 
[...]

active toolchain
----------------

nightly-x86_64-unknown-linux-gnu (default)
rustc 1.85.0-nightly (c26db435b 2024-12-15)

(same results with stable)

$ cargo kani --version

cargo-kani 0.56.0

Test file: main.rs

use std::result::Result;

pub static mut buffer: [u8; MEM_SIZE] = [0; MEM_SIZE];
pub const MEM_BASE: *mut u8 = unsafe{buffer.as_mut_ptr()};
pub const MEM_SIZE: usize = 0x100;


#[derive(Debug)]
pub enum err {
    err_1,
    err_2,
}

fn test(num: u8) -> Result<u8,err> {
    match num {
        0 => Ok(num),
        _ => Err(err::err_1),
    }
}

#[kani::proof]
fn main() {

    let mut newbuf: [u8; MEM_SIZE] = kani::any();
    unsafe{buffer.clone_from(&newbuf)};

    /*for i in (0..unsafe{buffer.len()-1}){
        unsafe{buffer[i] = kani::any()};
    }*/

    let size: usize = kani::any();
    println!("\nabc {:?}", unsafe{buffer[size]});
}

/// Test generated for harness `main`
///
/// Check for `assertion`: "index out of bounds: the length is less than or equal to the given index"

#[test]
fn kani_concrete_playback_main_12005999010690294499() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 9223372036854775807ul
        vec![255, 255, 255, 255, 255, 255, 255, 127],
    ];
    kani::concrete_playback_run(concrete_vals, main);
}

#[kani::proof]
fn expect(){
    let mut newbuf: [u8; MEM_SIZE] = kani::any();
    unsafe{buffer.clone_from(&newbuf)};
    let a = test(unsafe{*MEM_BASE}).expect("error");
}

/// Test generated for harness `expect`
///
/// Check for `assertion`: "This is a placeholder message; Kani doesn't support message formatted at runtime"

#[test]
fn kani_concrete_playback_expect_1935534694730255327() {
    let concrete_vals: Vec<Vec<u8>> = vec![
    ];
    kani::concrete_playback_run(concrete_vals, expect);
}

Tests were generated with:

cargo kani --harness main --concrete-playback inplace -Z concrete-playback
cargo kani --harness expect --concrete-playback inplace -Z concrete-playback

$ RUST_BACKTRACE=1 cargo kani playback -Z concrete-playback -- kani_concrete_playback_main_12005999010690294499
running 1 test
test kani_concrete_playback_main_12005999010690294499 ... FAILED

failures:

---- kani_concrete_playback_main_12005999010690294499 stdout ----
thread 'kani_concrete_playback_main_12005999010690294499' panicked at /__w/kani/kani/library/kani/src/concrete_playback.rs:66:5:
assertion `left == right` failed: Expected 1 bytes in the following det vals vec
  left: 8
 right: 1
stack backtrace:
   0: rust_begin_unwind
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panicking.rs:665:5
   1: core::panicking::panic_fmt
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panicking.rs:74:14
   2: core::panicking::assert_failed_inner
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panicking.rs:407:23
   3: core::panicking::assert_failed
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panicking.rs:367:5
   4: kani::concrete_playback::any_raw_internal
             at /__w/kani/kani/library/kani/src/concrete_playback.rs:66:5
   5: kani::concrete_playback::any_raw_array::{{closure}}
             at /__w/kani/kani/library/kani/src/concrete_playback.rs:45:21
   6: core::ops::try_trait::NeverShortCircuit<T>::wrap_mut_1::{{closure}}
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/try_trait.rs:387:36
   7: <core::iter::adapters::map::Map<I,F> as core::iter::traits::unchecked_iterator::UncheckedIterator>::next_unchecked
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:206:9
   8: core::array::try_from_trusted_iterator::next::{{closure}}
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:814:22
   9: core::array::try_from_fn_erased
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:845:20
  10: core::array::try_from_fn
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:130:11
  11: core::array::try_from_trusted_iterator
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:818:5
  12: core::array::<impl [T; N]>::try_map::{{closure}}
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:566:39
  13: core::array::drain::drain_array_with
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/drain.rs:26:5
  14: core::array::<impl [T; N]>::try_map
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:566:9
  15: core::array::<impl [T; N]>::map
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:528:9
  16: kani::concrete_playback::any_raw_array
             at /__w/kani/kani/library/kani/src/concrete_playback.rs:45:5
  17: <u8 as kani::Arbitrary>::any_array
             at /__w/kani/kani/library/kani_core/src/arbitrary.rs:42:34
  18: <[T; N] as kani::Arbitrary>::any
             at /__w/kani/kani/library/kani_core/src/arbitrary.rs:130:17
  19: kani::any
             at /__w/kani/kani/library/kani_core/src/lib.rs:196:13
  20: mem_test::main
             at ./src/main.rs:24:38
  21: core::ops::function::Fn::call
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:79:5
  22: kani::concrete_playback::concrete_playback_run
             at /__w/kani/kani/library/kani/src/concrete_playback.rs:26:5
  23: mem_test::kani_concrete_playback_main_12005999010690294499
             at ./src/main.rs:45:5
  24: mem_test::kani_concrete_playback_main_12005999010690294499::{{closure}}
             at ./src/main.rs:40:54
  25: core::ops::function::FnOnce::call_once
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
  26: core::ops::function::FnOnce::call_once
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.


failures:
    kani_concrete_playback_main_12005999010690294499

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 1 filtered out; finished in 1.19s

error: test failed, to rerun pass `--bin mem_test`
error: ~/.kani/kani-0.56.0/toolchain/bin/cargo exited with status exit status: 101

$ RUST_BACKTRACE=1 cargo kani playback -Z concrete-playback -- kani_concrete_playback_expect_1935534694730255327

running 1 test
test kani_concrete_playback_expect_1935534694730255327 ... FAILED
                                               
failures:                                                                                     

---- kani_concrete_playback_expect_1935534694730255327 stdout ----                                                                                                                           
thread 'kani_concrete_playback_expect_1935534694730255327' panicked at /__w/kani/kani/library/kani/src/concrete_playback.rs:61:46:
Not enough det vals found
stack backtrace:
   0: rust_begin_unwind
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panicking.rs:665:5
   1: core::panicking::panic_fmt
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panicking.rs:74:14
   2: core::panicking::panic_display
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panicking.rs:264:5
   3: core::option::expect_failed
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:2014:5
   4: core::option::Option<T>::expect
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:931:21
   5: kani::concrete_playback::any_raw_internal::{{closure}}
             at /__w/kani/kani/library/kani/src/concrete_playback.rs:61:13
   6: std::thread::local::LocalKey<T>::try_with
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:283:12
   7: std::thread::local::LocalKey<T>::with
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:260:9
   8: kani::concrete_playback::any_raw_internal
             at /__w/kani/kani/library/kani/src/concrete_playback.rs:58:5
   9: kani::concrete_playback::any_raw_array::{{closure}}
             at /__w/kani/kani/library/kani/src/concrete_playback.rs:45:21
  10: core::ops::try_trait::NeverShortCircuit<T>::wrap_mut_1::{{closure}}
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/try_trait.rs:387:36
  11: <core::iter::adapters::map::Map<I,F> as core::iter::traits::unchecked_iterator::UncheckedIterator>::next_unchecked
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:206:9
  12: core::array::try_from_trusted_iterator::next::{{closure}}
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:814:22
  13: core::array::try_from_fn_erased
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:845:20
  14: core::array::try_from_fn
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:130:11
  15: core::array::try_from_trusted_iterator
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:818:5
  16: core::array::<impl [T; N]>::try_map::{{closure}}
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:566:39
  17: core::array::drain::drain_array_with
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/drain.rs:26:5
  18: core::array::<impl [T; N]>::try_map
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:566:9
  19: core::array::<impl [T; N]>::map
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:528:9
  20: kani::concrete_playback::any_raw_array
             at /__w/kani/kani/library/kani/src/concrete_playback.rs:45:5
  21: <u8 as kani::Arbitrary>::any_array
             at /__w/kani/kani/library/kani_core/src/arbitrary.rs:42:34
  22: <[T; N] as kani::Arbitrary>::any
             at /__w/kani/kani/library/kani_core/src/arbitrary.rs:130:17
  23: kani::any
             at /__w/kani/kani/library/kani_core/src/lib.rs:196:13
  24: mem_test::expect
             at ./src/main.rs:50:38
  25: core::ops::function::Fn::call
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:79:5
  26: kani::concrete_playback::concrete_playback_run
             at /__w/kani/kani/library/kani/src/concrete_playback.rs:26:5
  27: mem_test::kani_concrete_playback_expect_1935534694730255327
             at ./src/main.rs:63:5
  28: mem_test::kani_concrete_playback_expect_1935534694730255327::{{closure}}
             at ./src/main.rs:60:55
  29: core::ops::function::FnOnce::call_once
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
  30: core::ops::function::FnOnce::call_once
             at /github/home/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.


failures:
    kani_concrete_playback_expect_1935534694730255327

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 1 filtered out; finished in 1.20s

error: test failed, to rerun pass `--bin mem_test`
error: ~/.kani/kani-0.56.0/toolchain/bin/cargo exited with status exit status: 101

Small aside, I know this feature is experimental, but with --visualize being deprecated, is there any other recommended means of tracing errors in more complex code bases?

The text was updated successfully, but these errors were encountered:

zhassan-aws · 2024-12-17T16:51:54Z

Thanks for filing this issue. This is likely a duplicate of #2566 .

gogdavz added the [C] Bug This is a bug. Something isn't working. label Dec 16, 2024

carolynzech self-assigned this Dec 17, 2024

zhassan-aws added the T-User Tag user issues / requests label Dec 17, 2024

carolynzech removed their assignment Dec 26, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Concrete playback feature generates tests that fail Kani assertions #3787

Concrete playback feature generates tests that fail Kani assertions #3787

gogdavz commented Dec 16, 2024

zhassan-aws commented Dec 17, 2024

Concrete playback feature generates tests that fail Kani assertions #3787

Concrete playback feature generates tests that fail Kani assertions #3787

Comments

gogdavz commented Dec 16, 2024

zhassan-aws commented Dec 17, 2024