Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Crash when running with CBMC's SMT solver option #1748

Closed
zhassan-aws opened this issue Oct 4, 2022 · 4 comments · Fixed by #1941
Closed

Crash when running with CBMC's SMT solver option #1748

zhassan-aws opened this issue Oct 4, 2022 · 4 comments · Fixed by #1941
Assignees
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-CBMC Issue related to an existing CBMC issue

Comments

@zhassan-aws
Copy link
Contributor

I tried this code:

#[kani::proof]
fn main() {
    let x: i32 = kani::any();
    let y = x;
    assert!(x == y);
}

using the following command line invocation:

kani test.rs --enable-unstable --cbmc-args --z3

with Kani version: 07092de

I expected to see this happen: Verification succeeded

Instead, this happened:

$ kani test.rs --enable-unstable --cbmc-args --z3
file /home/ubuntu/git/kani/library/kani/src/arbitrary.rs line 21 column 26 function <i32 as kani::Arbitrary>::any: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/git/kani/library/kani/src/lib.rs line 85 column 5 function kani::any::<i32>: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 342 column 42 function std::fmt::ArgumentV1::new_display::<std::fmt::Arguments>: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 342 column 68 function std::fmt::ArgumentV1::new_display::<std::fmt::Arguments>: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/macros/mod.rs line 709 column 47 function kani::any_raw_inner::<i32>: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/macros/mod.rs line 709 column 47 function kani::any_raw_inner::<i32>: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panic.rs line 57 column 38 function kani::any_raw_inner::<i32>: adding goto-destructor code on jump to 'bb3'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb3'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb3'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb6'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb4'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panic.rs line 57 column 38 function std::fmt::Arguments::new_v1: adding goto-destructor code on jump to 'bb5'
file /home/ubuntu/examples/trivial/test.rs line 3 column 18 function main: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/examples/trivial/test.rs line 5 column 5 function main: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/git/kani/library/kani/src/lib.rs line 108 column 5 function kani::any_raw_internal::<i32, 4>: adding goto-destructor code on jump to 'bb1'
Checking harness main...
CBMC 5.67.0 (cbmc-5.67.0)
CBMC version 5.67.0 (cbmc-5.67.0) 64-bit x86_64 linux
Reading GOTO program from file test.for-main.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.0073559s
size of program expression: 492 steps
slicing removed 283 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 4.6592e-05s
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Runtime Convert SSA: 0.000348786s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.11375s
Runtime decision procedure: 0.114173s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.0168971s
Runtime decision procedure: 0.0169387s
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/json_goto_trace.cpp:121 function: convert_decl
Condition: step.full_lhs_value.is_not_nil()
Reason: full_lhs_value in assignment must not be nil
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x5564ec6b0da0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x5564ec6b1349]
cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x48) [0x5564ebe14738]
cbmc(convert_decl(json_objectt&, conversion_dependenciest const&, trace_optionst const&)+0x3aa6) [0x5564ec2b0116]
cbmc(void convert<json_stream_arrayt>(namespacet const&, goto_tracet const&, json_stream_arrayt&, trace_optionst)+0x5c2) [0x5564ebf6a382]
cbmc(output_properties_with_traces(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > > const&, goto_trace_storaget const&, trace_optionst const&, unsigned long, ui_message_handlert&)+0xbec) [0x5564ebf843dc]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::report()+0x94) [0x5564ebe1bac4]
cbmc(cbmc_parse_optionst::doit()+0xf9a) [0x5564ebe1af9a]
cbmc(parse_options_baset::main()+0x8f) [0x5564ebe1284f]
cbmc(main+0x39) [0x5564ebdfe859]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f60311e80b3]
cbmc(_start+0x2e) [0x5564ebe1414e]


--- end invariant violation report ---
Verification Time: 1.3128812s
@zhassan-aws zhassan-aws added the [C] Bug This is a bug. Something isn't working. label Oct 4, 2022
@zhassan-aws
Copy link
Contributor Author

This seems to be related to CBMC's --json-ui: if I use the old output format, it doesn't crash:

$ kani test.rs --output-format old --enable-unstable --cbmc-args --z3
file /home/ubuntu/git/kani/library/kani/src/arbitrary.rs line 21 column 26 function <i32 as kani::Arbitrary>::any: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/git/kani/library/kani/src/lib.rs line 85 column 5 function kani::any::<i32>: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 342 column 42 function std::fmt::ArgumentV1::new_display::<std::fmt::Arguments>: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 342 column 68 function std::fmt::ArgumentV1::new_display::<std::fmt::Arguments>: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/macros/mod.rs line 709 column 47 function kani::any_raw_inner::<i32>: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/macros/mod.rs line 709 column 47 function kani::any_raw_inner::<i32>: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panic.rs line 57 column 38 function kani::any_raw_inner::<i32>: adding goto-destructor code on jump to 'bb3'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb3'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb3'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb6'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-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: adding goto-destructor code on jump to 'bb4'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panic.rs line 57 column 38 function std::fmt::Arguments::new_v1: adding goto-destructor code on jump to 'bb5'
file /home/ubuntu/examples/trivial/test.rs line 3 column 18 function main: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/examples/trivial/test.rs line 5 column 5 function main: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/git/kani/library/kani/src/lib.rs line 108 column 5 function kani::any_raw_internal::<i32, 4>: adding goto-destructor code on jump to 'bb1'
Checking harness main...
CBMC version 5.67.0 (cbmc-5.67.0) 64-bit x86_64 linux
Reading GOTO program from file test.for-main.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.00723471s
size of program expression: 492 steps
slicing removed 283 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 8.8554e-05s
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Runtime Convert SSA: 0.000349986s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.0175763s
Runtime decision procedure: 0.0180192s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.0168569s
Runtime decision procedure: 0.0169007s

** Results:
/home/ubuntu/examples/trivial/test.rs function main
[main.assertion.1] line 5 [KANI_CHECK_ID_test.77c3a4fc::test_0] assertion failed: x == y: SUCCESS
[main.cover.1] line 5 [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_test.77c3a4fc::test_0: FAILURE

** 1 of 2 failed (2 iterations)
VERIFICATION FAILED
Verification Time: 0.057107072s

@zhassan-aws
Copy link
Contributor Author

Tracked by diffblue/cbmc#7185

@tedinski
Copy link
Contributor

tedinski commented Oct 4, 2022

--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/json_goto_trace.cpp:121 function: convert_decl

That file name makes it sound like the problem is with translating the results back into a trace (which --json-ui seems to request implicitly)

@zhassan-aws
Copy link
Contributor Author

diffblue/cbmc#7185 was fixed in CBMC 5.69.1, but CBMC still crashes. The new issue is tracked in diffblue/cbmc#7308.

@tedinski tedinski added the [F] Crash Kani crashed label Nov 28, 2022
@zhassan-aws zhassan-aws added the T-CBMC Issue related to an existing CBMC issue label Dec 2, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-CBMC Issue related to an existing CBMC issue
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants