A case where concrete values in trace/playback do not trigger an assertion violation

zpzigi754 commented 1 year ago

I tried this code:

#[derive(Debug)]
pub struct Data {
    pub _type: Type,
    pub array: [u8; MAX_ARRAY_LENGTH],
}

impl Data {
    fn is_valid(&self) -> bool {
        (self.array.len() == MAX_ARRAY_LENGTH)
            && ((self._type == Type::Apple) || (self._type == Type::Banana))
    }

    pub fn set_array(&mut self, idx: usize, array: [u8; 4]) -> Result<(), &str> {
        if idx >= MAX_U32_DATA_IDX {
            return Err("invalid input");
        }
        let start = idx * core::mem::size_of::<u32>();
        let end = start + core::mem::size_of::<u32>();
        self.array[start..end].copy_from_slice(&array);
        Ok(())
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
#[repr(u8)]
pub enum Type {
    Apple = 0,
    Banana = 1,
}

const MAX_ARRAY_LENGTH: usize = 8;
const MAX_U32_DATA_IDX: usize = 2;

#[kani::proof]
fn proof_harness() {
    let mut data = Data {
        _type: Type::Apple,
        array: [0; MAX_ARRAY_LENGTH],
    };
    let index = kani::any();
    let param = kani::any();
    let res = data.set_array(index, param);
    if let Ok(v) = res {
        assert!(data.is_valid());            // this point makes the verification fail, as `_type` field 
                                             // contain an unexpected value for some reasons
    }
}

fn main() {}

using the following command line invocation:

cargo kani --enable-unstable --concrete-playback=inplace
cargo test

with Kani version: 0.14.1, 0.15.0 (3c7e3fc9)

I expected to see this happen: I think that the verification should be successful, but it failed. If the verification has failed and concrete values have been generated with playback, using it should trigger the assertion violation like the below (I also have used the values in --visualize, but it does not trigger the assertion violation too.).

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

Instead, this happened:

The result for cargo kani

SUMMARY:
 ** 1 of 203 failed (2 unreachable)
Failed Checks: assertion failed: data.is_valid()
 File: "/home/xxx/test/kani-test/data/src/main.rs", line 44, in proof_harness

VERIFICATION:- FAILED
Verification Time: 0.53910637s

The result for cargo test with the generated concrete values

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

cargo test used the following genereted code

#[test]
fn kani_concrete_playback_proof_harness_8995903321428480627() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 1ul
        vec![1, 0, 0, 0, 0, 0, 0, 0],
        // 0
        vec![0],
        // 10
        vec![10],
        // 0
        vec![0],
        // 0
        vec![0],
    ];
    kani::concrete_playback_run(concrete_vals, proof_harness);
}

tedinski commented 1 year ago

Judging from the comment (and a very quick read of the code), this is a case of Kani spuriously failing on code that should successfully verify, right?

Just want to clarify, since the title kinda lead me to think it might be a concrete playback issue, but actually it looks like the opposite: the concrete playback succeeding is just evidence that this proof shouldn't be failing, right?

tedinski commented 1 year ago

Whoops, you already answered my question.

I expected to see this happen: I think that the verification should be successful, but it failed.

Tagging as high priority at least until we figure out if this is a mistranslation that could have soundness implications...

zpzigi754 commented 1 year ago

Judging from the comment (and a very quick read of the code), this is a case of Kani spuriously failing on code that should successfully verify, right?

I didn't know that there is a issue that kani could spuriously fail on code that should successfully verify (false positive case).

Just want to clarify, since the title kinda lead me to think it might be a concrete playback issue, but actually it looks like the opposite: the concrete playback succeeding is just evidence that this proof shouldn't be failing, right?

Your understanding is correct, but I am open towards both possibilities: 1) my code has a subtle bug and kani detected it correctly, but the concrete playback and trace couldn't reproduce it well. 2) my code does not have a bug but kani wrongly reported it as a failure.

zhassan-aws commented 1 year ago

This definitely looks like a bug in Kani's translation. This is a slightly smaller version that reproduces the same spurious failure:

pub struct Data {
    pub t: Type,
    pub array: [u8; 8],
}

impl Data {
    fn is_valid(&self) -> bool {
        (self.t == Type::Apple) || (self.t == Type::Banana)
    }

    pub fn set_array(&mut self, idx: usize, array: [u8; 4]) {
        let start = idx * 4;
        let end = start + 4;
        self.array[start..end].copy_from_slice(&array);
    }
}

#[derive(PartialEq, Eq)]
pub enum Type {
    Apple = 0,
    Banana = 1,
}

#[kani::proof]
fn proof_harness() {
    let mut data = Data {
        t: Type::Apple,
        array: [0; 8],
    };
    let index = kani::any();
    if index < 2 {
        let param = [0, 0, 0, 0];
        data.set_array(index, param);
        assert!(data.is_valid());
    }
}

What's interesting is that if I replace the kani::any() with 0 or 1 (which are the only two possible values that can trigger the issue), verification is successful!

zhassan-aws commented 1 year ago

There's a warning from CBMC that might be indicating what Kani is doing wrong:

converting SSA
warning: ignoring typecast
  * type: struct_tag
      * identifier: tag-_13923551032953076959
  0: constant
      * type: bv
          * width: 8
      * value: 0
warning: ignoring typecast
  * type: struct_tag
      * identifier: tag-_13923551032953076959
  0: typecast
      * type: bv
          * width: 8
      0: index
          * type: signedbv
              * width: 8
          0: symbol
              * type: array
                  * #source_location: 
                    * file: <builtin-library-memcpy>
                    * line: 44
                    * function: memcpy
                    * working_directory: /home/ubuntu/examples
                  * #index_type: signedbv
                      * width: 64
                      * #c_type: signed_long_int
                  * size: symbol
                      * type: unsignedbv
                          * #source_location: 
                            * file: <built-in-additions>
                            * line: 1
                            * working_directory: /home/ubuntu/examples
                          * width: 64
                          * #typedef: __CPROVER_size_t
                          * #c_type: unsigned_long_int
                      * identifier: memcpy::1::1::src_n$array_size::src_n$array_size!0@1#2
                      * expression: symbol
                          * type: unsignedbv
                              * #source_location: 
                                * file: <built-in-additions>
                                * line: 1
                                * working_directory: /home/ubuntu/examples
                              * width: 64
                              * #typedef: __CPROVER_size_t
                              * #c_type: unsigned_long_int
                          * identifier: memcpy::1::1::src_n$array_size::src_n$array_size
                      * #SSA_symbol: 1
                      * L0: 0
                      * L1: 1
                      * L2: 2
                      * L1_object_identifier: memcpy::1::1::src_n$array_size::src_n$array_size!0@1
                  0: signedbv
                      * width: 8
              * identifier: memcpy::1::1::src_n!0@1#2
              * expression: symbol
                  * type: array
                      * #source_location: 
                        * file: <builtin-library-memcpy>
                        * line: 44
                        * function: memcpy
                        * working_directory: /home/ubuntu/examples
                      * #index_type: signedbv
                          * width: 64
                          * #c_type: signed_long_int
                      * size: symbol
                          * type: unsignedbv
                              * #source_location: 
                                * file: <built-in-additions>
                                * line: 1
                                * working_directory: /home/ubuntu/examples
                              * width: 64
                              * #typedef: __CPROVER_size_t
                              * #c_type: unsigned_long_int
                          * identifier: memcpy::1::1::src_n$array_size::src_n$array_size!0@1#2
                          * expression: symbol
                              * type: unsignedbv
                                  * #source_location: 
                                    * file: <built-in-additions>
                                    * line: 1
                                    * working_directory: /home/ubuntu/examples
                                  * width: 64
                                  * #typedef: __CPROVER_size_t
                                  * #c_type: unsigned_long_int
                              * identifier: memcpy::1::1::src_n$array_size::src_n$array_size
                          * #SSA_symbol: 1
                          * L0: 0
                          * L1: 1
                          * L2: 2
                          * L1_object_identifier: memcpy::1::1::src_n$array_size::src_n$array_size!0@1
                      0: signedbv
                          * width: 8
                  * #source_location: 
                    * file: <builtin-library-memcpy>
                    * line: 44
                    * function: memcpy
                    * working_directory: /home/ubuntu/examples
                  * identifier: memcpy::1::1::src_n
              * #SSA_symbol: 1
              * L0: 0
              * L1: 1
              * L2: 2
              * L1_object_identifier: memcpy::1::1::src_n!0@1
          1: unary-
              * type: signedbv
                  * width: 64
                  * #c_type: signed_long_int
              0: pointer_offset
                  * type: signedbv
                      * width: 64
                      * #c_type: signed_long_int
                  0: symbol
                      * type: pointer
                          * #source_location: 
                            * file: <built-in-additions>
                            * line: 19
                            * function: 
                            * working_directory: /home/ubuntu/examples
                          * width: 64
                          0: empty
                              * #source_location: 
                                * file: <built-in-additions>
                                * line: 19
                                * function: 
                                * working_directory: /home/ubuntu/examples
                              * #constant: 1
                      * identifier: memcpy::dst!0@1#1
                      * expression: symbol
                          * type: pointer
                              * #source_location: 
                                * file: <built-in-additions>
                                * line: 19
                                * function: 
                                * working_directory: /home/ubuntu/examples
                              * width: 64
                              0: empty
                                  * #source_location: 
                                    * file: <built-in-additions>
                                    * line: 19
                                    * function: 
                                    * working_directory: /home/ubuntu/examples
                                  * #constant: 1
                          * identifier: memcpy::dst
                      * #SSA_symbol: 1
                      * L0: 0
                      * L1: 1
                      * L2: 1
                      * L1_object_identifier: memcpy::dst!0@1

zhassan-aws commented 1 year ago

This is a minimal reproducer:

pub struct Data {
    pub t: Type,
    pub array: [u8; 8],
}

#[derive(PartialEq, Eq)]
pub enum Type {
    Apple,
    Banana,
}

#[kani::proof]
fn proof_harness() {
    let mut data = Data {
        t: Type::Apple,
        array: [0; 8],
    };
    let coin = kani::any();
    let param = [0, 0, 0, 0];
    let start = if coin { 4 } else { 0 };
    data.array[start..start+4].copy_from_slice(&param);
    assert!(data.t == Type::Apple || data.t == Type::Banana);
}

$ kani iss1911.rs

# -- snip --

SUMMARY:
 ** 1 of 31 failed (1 unreachable)
Failed Checks: assertion failed: data.t == Type::Apple || data.t == Type::Banana
 File: "/home/ubuntu/examples/iss1911.rs", line 22, in proof_harness

VERIFICATION:- FAILED

zhassan-aws commented 1 year ago

More weirdness! This program fails:

pub struct Data {
    pub t: Type,
    pub array: [u8; 8],
}

#[derive(PartialEq, Eq)]
pub enum Type {
    Apple,
    Banana,
}

fn copy_from_slice(src: &[u8], dst: &mut [u8]) {
    assert_eq!(src.len(), dst.len());
    unsafe {
        std::ptr::copy_nonoverlapping(src.as_ptr(), dst.as_mut_ptr(), dst.len());
        //std::ptr::copy_nonoverlapping(src.as_ptr(), dst.as_mut_ptr(), src.len());
    }
}

#[kani::proof]
fn proof_harness() {
    let mut data = Data {
        t: Type::Apple,
        array: [0; 8],
    };
    let coin = kani::any();
    let param = [0, 0, 0, 0];
    let start = if coin { 4 } else { 0 };
    copy_from_slice(&param, &mut data.array[start..start+4]);
    assert!(data.t == Type::Apple || data.t == Type::Banana);
}

but if I use the commented copy_nonoverlapping line instead, it passes! The only difference is that one uses dst.len(), and the other uses src.len(), which are the same (as verified by the assertion above)!

Is this possibly an issue with fat pointer handling?

zhassan-aws commented 1 year ago

@tautschnig need your input on this one. The dump C output between the two programs is identical other than a single line:

4823c4823
<   var_9 = src;
---
>   var_9 = (struct &[u8]){ .data=dst.data, .len=dst.len };

so it's not clear why this is failing. I'm also not sure whether the typecast warning CBMC is emitting is related.

danielsn commented 1 year ago

If I recall correctly "Ignoring Typecast" means: "Replacing with Nondet". So that would make sense

tedinski commented 1 year ago

If I recall correctly "Ignoring Typecast" means: "Replacing with Nondet"

😮

tedinski commented 1 year ago

On the plus side, if that's what's happening there then at least this isn't a soundness bug, just mistranslation (presumably we're mistranslating something to cause the "ignoring typecast") causing false positives.

But uh, we should figure out how to turn that into an error and not a warning. At least.

tedinski commented 1 year ago

Does goto-instrument --validate-goto-model on that goto binary complain?

zhassan-aws commented 1 year ago

Interestingly, it doesn't complain:

$ goto-instrument --validate-goto-model iss1911.for-proof_harness.out  a.out
Reading GOTO program from 'iss1911.for-proof_harness.out'
Writing GOTO program to 'a.out'

However, (more interestingly), if I run CBMC directly on it, it crashes!

$ cbmc iss1911.for-proof_harness.out 
CBMC version 5.70.0 (cbmc-5.70.0) 64-bit x86_64 linux
Reading GOTO program from file iss1911.for-proof_harness.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Unwinding loop _RNvMs2_NtCsdMIzxSrmMZ9_4core3fmtNtB5_9Arguments6new_v1Cs3sHPiOR40Bj_7iss1911.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 395 column 12 function std::fmt::Arguments::<'_>::new_v1 thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/index.rs line 97 column 5 function core::slice::index::slice_index_order_fail_rt thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/index.rs line 91 column 14 function core::slice::index::slice_index_order_fail thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/index.rs line 417 column 13 function <std::ops::Range<usize> as std::slice::SliceIndex<[u8]>>::index_mut thread 0
Unwinding loop _RNvMs2_NtCsdMIzxSrmMZ9_4core3fmtNtB5_9Arguments6new_v1Cs3sHPiOR40Bj_7iss1911.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 395 column 12 function std::fmt::Arguments::<'_>::new_v1 thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/index.rs line 76 column 5 function core::slice::index::slice_end_index_len_fail_rt thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/index.rs line 69 column 9 function core::slice::index::slice_end_index_len_fail thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/index.rs line 419 column 13 function <std::ops::Range<usize> as std::slice::SliceIndex<[u8]>>::index_mut thread 0
Unwinding loop proof_harness.0 iteration 1 file /home/ubuntu/examples/iss1911.rs line 29 column 13 function proof_harness thread 0
Unwinding loop proof_harness.1 iteration 1 file /home/ubuntu/examples/iss1911.rs line 29 column 13 function proof_harness thread 0
Unwinding loop proof_harness.2 iteration 1 file /home/ubuntu/examples/iss1911.rs line 29 column 13 function proof_harness thread 0
Runtime Symex: 0.0793953s
size of program expression: 4458 steps
simple slicing removed 12 assignments
Generated 24 VCC(s), 15 remaining after simplification
Runtime Postprocess Equation: 0.000391738s
Passing problem to propositional reduction
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/flattening/boolbv_width.cpp:226 function: get_entry
Condition: false
Reason: Reached unimplemented boolbv_widtht::get_entry(integer)
Backtrace:
cbmc(+0xa8ea70) [0x5556b66c0a70]
cbmc(+0xa8f019) [0x5556b66c1019]
cbmc(+0x1e8d08) [0x5556b5e1ad08]
cbmc(+0x82a6c9) [0x5556b645c6c9]
cbmc(+0x7fd4e9) [0x5556b642f4e9]
cbmc(+0x7e5bbe) [0x5556b6417bbe]
cbmc(+0x830886) [0x5556b6462886]
cbmc(+0x7e9210) [0x5556b641b210]
cbmc(+0x7e516a) [0x5556b641716a]
cbmc(+0x7e5238) [0x5556b6417238]
cbmc(+0x5390c1) [0x5556b616b0c1]
cbmc(+0x541876) [0x5556b6173876]
cbmc(+0x542422) [0x5556b6174422]
cbmc(+0x338814) [0x5556b5f6a814]
cbmc(+0x338c95) [0x5556b5f6ac95]
cbmc(+0x34a725) [0x5556b5f7c725]
cbmc(+0x1f3039) [0x5556b5e25039]
cbmc(+0x1ef55e) [0x5556b5e2155e]
cbmc(+0x1e6d9f) [0x5556b5e18d9f]
cbmc(+0x1d2da9) [0x5556b5e04da9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f95508ec0b3]
cbmc(+0x1e871e) [0x5556b5e1a71e]

--- end invariant violation report ---
Aborted (core dumped)

Not sure why running kani on the rust file directly doesn't produce the same crash.

zhassan-aws commented 1 year ago

Looks like the crash happened because I didn't pass --slice-formula (similar to #1810).

tautschnig commented 1 year ago

Thank you all for the helpful reproducers! The root cause is a bug in CBMC, which is fixed once https://github.com/diffblue/cbmc/pull/7360 gets merged.

tautschnig commented 1 year ago

CBMC PR merged, will be part of the next release (due 2022-11-24).

zpzigi754 commented 1 year ago

I've confirmed that the example works well with the latest cbmc (verification successful). Thank you all for the help!

model-checking / kani

A case where concrete values in trace/playback do not trigger an assertion violation #1911