kani-driver panic in cbmc_output_parser when using z3, bitwuzla, or cvc5 #4519
Description
I tried this code:
#[kani::proof]
#[kani::solver(SOLVER)]
pub fn main() {
assert!(false)
}Where SOLVER is one of:
z3cvc5bitwuzla
(As in I tried all three separately - I'm not trying to pass the solver as a constant or something like that)
This is the result of trying to find a minimal reproducible example from more complicated proofs. It seems like anything that doesn't get optimized away (assert!(true) is a no-op) is enough to trigger this (including proofs which pass).
Using minisat, cadical, kissat, or excluding the kani::solver attribute and just using the default all work correctly and lead to the expected result.
using the following command line invocation:
cargo kaniwith Kani version: 0.67
I expected to see this happen:
Kani should complete with VERIFICATION FAILED.
Instead, this happened:
(bitwuzla example - all crash in the same manner, same file, same line and column)
Kani Rust Verifier 0.67.0 (cargo plugin)
Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.05s
Checking harness main...
CBMC 6.8.0 (cbmc-6.8.0)
CBMC version 6.8.0 (cbmc-6.8.0) 64-bit x86_64 linux
Reading GOTO program from file /var/home/<redacted>/<redacted>/<redacted>/target/kani/x86_64-unknown-linux-gnu/debug/deps/<redacted>-3147251ddcda2374__RNvCsgrEEiWXMNIF_23<redacted>4main.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.000449269s
size of program expression: 70 steps
slicing removed 37 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 9.54e-06s
Passing problem to SMT2 QF_AUFBV (with FPA) using Bitwuzla
converting SSA
Runtime Convert SSA: 2.888e-05s
Running SMT2 QF_AUFBV (with FPA) using Bitwuzla
Runtime Solver: 0.000847048s
Runtime decision procedure: 0.000905938s
thread '<unnamed>' (77345) panicked at kani-driver/src/cbmc_output_parser.rs:470:25:
called `Result::unwrap()` on an `Err` value: Error("unknown variant `ERROR`, expected one of `FAILURE`, `COVERED`, `SATISFIED`, `SUCCESS`, `UNDETERMINED`, `UNKNOWN`, `UNREACHABLE`, `UNCOVERED`, `UNSATISFIABLE`", line: 16, column: 25)
RUST_BACKTRACE=1
stack backtrace:
0: __rustc::rust_begin_unwind
1: core::panicking::panic_fmt
2: core::result::unwrap_failed
3: <kani_driver::cbmc_output_parser::Parser>::process_line
4: <kani_driver::session::KaniSession>::run_cbmc_piped::{closure#0}
5: <tokio::runtime::context::scoped::Scoped<tokio::runtime::scheduler::Context>>::set::<<tokio::runtime::scheduler::current_thread::CoreGuard>::enter<<tokio::runtime::scheduler::current_thread::CoreGuard>::block_on<core::pin::Pin<&mut <kani_driver::session::KaniSession>::run_cbmc_piped::{closure#0}>>::{closure#0}, core::option::Option<core::result::Result<kani_driver::call_cbmc::VerificationResult, anyhow::Error>>>::{closure#0}, (alloc::boxed::Box<tokio::runtime::scheduler::current_thread::Core>, core::option::Option<core::result::Result<kani_driver::call_cbmc::VerificationResult, anyhow::Error>>)>
6: <tokio::runtime::scheduler::current_thread::CurrentThread>::block_on::<<kani_driver::session::KaniSession>::run_cbmc_piped::{closure#0}>
7: <tokio::runtime::runtime::Runtime>::block_on::<<kani_driver::session::KaniSession>::run_cbmc_piped::{closure#0}>
8: <kani_driver::session::KaniSession>::check_harness
9: <&<kani_driver::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0} as core::ops::function::FnMut<((usize, &&kani_metadata::harness::HarnessMetadata),)>>::call_mut
10: <alloc::vec::Vec<kani_driver::harness_runner::HarnessResult> as alloc::vec::spec_extend::SpecExtend<kani_driver::harness_runner::HarnessResult, core::iter::adapters::map::Map<core::iter::adapters::take_while::TakeWhile<core::iter::adapters::map::Map<core::iter::adapters::map::Map<core::iter::adapters::zip::Zip<core::ops::range::Range<usize>, core::slice::iter::Iter<&kani_metadata::harness::HarnessMetadata>>, &<kani_driver::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>, &<core::result::Result<_, _> as rayon::iter::FromParallelIterator<core::result::Result<_, _>>>::from_par_iter::ok<kani_driver::harness_runner::HarnessResult, anyhow::Error>::{closure#0}>, <rayon::iter::while_some::WhileSomeFolder<_> as rayon::iter::plumbing::Folder<core::option::Option<_>>>::consume_iter::some<kani_driver::harness_runner::HarnessResult>::{closure#0}>, <core::option::Option<kani_driver::harness_runner::HarnessResult>>::unwrap>>>::spec_extend
11: rayon::iter::plumbing::bridge_producer_consumer::helper::<rayon::iter::enumerate::EnumerateProducer<rayon::slice::IterProducer<&kani_metadata::harness::HarnessMetadata>>, rayon::iter::map::MapConsumer<rayon::iter::map::MapConsumer<rayon::iter::while_some::WhileSomeConsumer<rayon::iter::extend::ListVecConsumer>, <core::result::Result<_, _> as rayon::iter::FromParallelIterator<core::result::Result<_, _>>>::from_par_iter::ok<kani_driver::harness_runner::HarnessResult, anyhow::Error>::{closure#0}>, <kani_driver::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>>
12: <rayon::iter::plumbing::bridge::Callback<rayon::iter::map::MapConsumer<rayon::iter::map::MapConsumer<rayon::iter::while_some::WhileSomeConsumer<rayon::iter::extend::ListVecConsumer>, <core::result::Result<_, _> as rayon::iter::FromParallelIterator<core::result::Result<_, _>>>::from_par_iter::ok<kani_driver::harness_runner::HarnessResult, anyhow::Error>::{closure#0}>, <kani_driver::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>> as rayon::iter::plumbing::ProducerCallback<(usize, &&kani_metadata::harness::HarnessMetadata)>>::callback::<rayon::iter::enumerate::EnumerateProducer<rayon::slice::IterProducer<&kani_metadata::harness::HarnessMetadata>>>
13: <alloc::vec::Vec<kani_driver::harness_runner::HarnessResult> as rayon::iter::ParallelExtend<kani_driver::harness_runner::HarnessResult>>::par_extend::<rayon::iter::while_some::WhileSome<rayon::iter::map::Map<rayon::iter::map::Map<rayon::iter::enumerate::Enumerate<rayon::slice::Iter<&kani_metadata::harness::HarnessMetadata>>, <kani_driver::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>, <core::result::Result<_, _> as rayon::iter::FromParallelIterator<core::result::Result<_, _>>>::from_par_iter::ok<kani_driver::harness_runner::HarnessResult, anyhow::Error>::{closure#0}>>>
14: <core::result::Result<alloc::vec::Vec<kani_driver::harness_runner::HarnessResult>, anyhow::Error> as rayon::iter::FromParallelIterator<core::result::Result<kani_driver::harness_runner::HarnessResult, anyhow::Error>>>::from_par_iter::<rayon::iter::map::Map<rayon::iter::enumerate::Enumerate<rayon::slice::Iter<&kani_metadata::harness::HarnessMetadata>>, <kani_driver::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>>
15: <rayon_core::job::StackJob<rayon_core::latch::LatchRef<rayon_core::latch::LockLatch>, <rayon_core::registry::Registry>::in_worker_cold<<rayon_core::thread_pool::ThreadPool>::install<<kani_driver::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}, core::result::Result<alloc::vec::Vec<kani_driver::harness_runner::HarnessResult>, anyhow::Error>>::{closure#0}, core::result::Result<alloc::vec::Vec<kani_driver::harness_runner::HarnessResult>, anyhow::Error>>::{closure#0}::{closure#0}, core::result::Result<alloc::vec::Vec<kani_driver::harness_runner::HarnessResult>, anyhow::Error>> as rayon_core::job::Job>::execute
16: <rayon_core::registry::WorkerThread>::wait_until_cold
17: <rayon_core::registry::ThreadBuilder>::run
RUST_BACKTRACE=full
stack backtrace:
0: 0x564bf7bde1a2 - <std::sys::backtrace::BacktraceLock::print::DisplayBacktrace as core::fmt::Display>::fmt::hefb8f4075f5287aa
1: 0x564bf7bf0117 - core::fmt::write::h9efc4df57a83a2be
2: 0x564bf7ba7ab6 - std::io::Write::write_fmt::ha441154b7754443a
3: 0x564bf7bba714 - std::panicking::default_hook::{{closure}}::hca02991224f6e328
4: 0x564bf7bba539 - std::panicking::default_hook::hac7a1b948746b127
5: 0x564bf7bbacdb - std::panicking::panic_with_hook::h99bd9d6fda5058b9
6: 0x564bf7bbaaa8 - std::panicking::panic_handler::{{closure}}::hce691e3283d81aa4
7: 0x564bf7bb4c59 - std::sys::backtrace::__rust_end_short_backtrace::h123b3c6fed40e660
8: 0x564bf7b9b1ad - __rustc[f01a1aa1bacb466]::rust_begin_unwind
9: 0x564bf7bf9bac - core::panicking::panic_fmt::he767e81dad5ec5d0
10: 0x564bf7bf9172 - core::result::unwrap_failed::hea1c2583327c1d25
11: 0x564bf78d42d2 - <kani_driver[fdb88ce1931fef6d]::cbmc_output_parser::Parser>::process_line
12: 0x564bf79472f2 - <kani_driver[fdb88ce1931fef6d]::session::KaniSession>::run_cbmc_piped::{closure#0}
13: 0x564bf78cb889 - <tokio[eeb8f5742a18f4f7]::runtime::context::scoped::Scoped<tokio[eeb8f5742a18f4f7]::runtime::scheduler::Context>>::set::<<tokio[eeb8f5742a18f4f7]::runtime::scheduler::current_thread::CoreGuard>::enter<<tokio[eeb8f5742a18f4f7]::runtime::scheduler::current_thread::CoreGuard>::block_on<core[2cc081e1ca4e22ab]::pin::Pin<&mut <kani_driver[fdb88ce1931fef6d]::session::KaniSession>::run_cbmc_piped::{closure#0}>>::{closure#0}, core[2cc081e1ca4e22ab]::option::Option<core[2cc081e1ca4e22ab]::result::Result<kani_driver[fdb88ce1931fef6d]::call_cbmc::VerificationResult, anyhow[f4d019122e47c51f]::Error>>>::{closure#0}, (alloc[b38a0b67e7b55095]::boxed::Box<tokio[eeb8f5742a18f4f7]::runtime::scheduler::current_thread::Core>, core[2cc081e1ca4e22ab]::option::Option<core[2cc081e1ca4e22ab]::result::Result<kani_driver[fdb88ce1931fef6d]::call_cbmc::VerificationResult, anyhow[f4d019122e47c51f]::Error>>)>
14: 0x564bf78cc835 - <tokio[eeb8f5742a18f4f7]::runtime::scheduler::current_thread::CurrentThread>::block_on::<<kani_driver[fdb88ce1931fef6d]::session::KaniSession>::run_cbmc_piped::{closure#0}>
15: 0x564bf78dc275 - <tokio[eeb8f5742a18f4f7]::runtime::runtime::Runtime>::block_on::<<kani_driver[fdb88ce1931fef6d]::session::KaniSession>::run_cbmc_piped::{closure#0}>
16: 0x564bf797d885 - <kani_driver[fdb88ce1931fef6d]::session::KaniSession>::check_harness
17: 0x564bf78ca8b0 - <&<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0} as core[2cc081e1ca4e22ab]::ops::function::FnMut<((usize, &&kani_metadata[b136932edba6d502]::harness::HarnessMetadata),)>>::call_mut
18: 0x564bf78614b8 - <alloc[b38a0b67e7b55095]::vec::Vec<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult> as alloc[b38a0b67e7b55095]::vec::spec_extend::SpecExtend<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult, core[2cc081e1ca4e22ab]::iter::adapters::map::Map<core[2cc081e1ca4e22ab]::iter::adapters::take_while::TakeWhile<core[2cc081e1ca4e22ab]::iter::adapters::map::Map<core[2cc081e1ca4e22ab]::iter::adapters::map::Map<core[2cc081e1ca4e22ab]::iter::adapters::zip::Zip<core[2cc081e1ca4e22ab]::ops::range::Range<usize>, core[2cc081e1ca4e22ab]::slice::iter::Iter<&kani_metadata[b136932edba6d502]::harness::HarnessMetadata>>, &<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>, &<core[2cc081e1ca4e22ab]::result::Result<_, _> as rayon[422a4a25e8530bbf]::iter::FromParallelIterator<core[2cc081e1ca4e22ab]::result::Result<_, _>>>::from_par_iter::ok<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult, anyhow[f4d019122e47c51f]::Error>::{closure#0}>, <rayon[422a4a25e8530bbf]::iter::while_some::WhileSomeFolder<_> as rayon[422a4a25e8530bbf]::iter::plumbing::Folder<core[2cc081e1ca4e22ab]::option::Option<_>>>::consume_iter::some<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult>::{closure#0}>, <core[2cc081e1ca4e22ab]::option::Option<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult>>::unwrap>>>::spec_extend
19: 0x564bf78b3207 - rayon[422a4a25e8530bbf]::iter::plumbing::bridge_producer_consumer::helper::<rayon[422a4a25e8530bbf]::iter::enumerate::EnumerateProducer<rayon[422a4a25e8530bbf]::slice::IterProducer<&kani_metadata[b136932edba6d502]::harness::HarnessMetadata>>, rayon[422a4a25e8530bbf]::iter::map::MapConsumer<rayon[422a4a25e8530bbf]::iter::map::MapConsumer<rayon[422a4a25e8530bbf]::iter::while_some::WhileSomeConsumer<rayon[422a4a25e8530bbf]::iter::extend::ListVecConsumer>, <core[2cc081e1ca4e22ab]::result::Result<_, _> as rayon[422a4a25e8530bbf]::iter::FromParallelIterator<core[2cc081e1ca4e22ab]::result::Result<_, _>>>::from_par_iter::ok<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult, anyhow[f4d019122e47c51f]::Error>::{closure#0}>, <kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>>
20: 0x564bf78b3515 - <rayon[422a4a25e8530bbf]::iter::plumbing::bridge::Callback<rayon[422a4a25e8530bbf]::iter::map::MapConsumer<rayon[422a4a25e8530bbf]::iter::map::MapConsumer<rayon[422a4a25e8530bbf]::iter::while_some::WhileSomeConsumer<rayon[422a4a25e8530bbf]::iter::extend::ListVecConsumer>, <core[2cc081e1ca4e22ab]::result::Result<_, _> as rayon[422a4a25e8530bbf]::iter::FromParallelIterator<core[2cc081e1ca4e22ab]::result::Result<_, _>>>::from_par_iter::ok<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult, anyhow[f4d019122e47c51f]::Error>::{closure#0}>, <kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>> as rayon[422a4a25e8530bbf]::iter::plumbing::ProducerCallback<(usize, &&kani_metadata[b136932edba6d502]::harness::HarnessMetadata)>>::callback::<rayon[422a4a25e8530bbf]::iter::enumerate::EnumerateProducer<rayon[422a4a25e8530bbf]::slice::IterProducer<&kani_metadata[b136932edba6d502]::harness::HarnessMetadata>>>
21: 0x564bf785feb9 - <alloc[b38a0b67e7b55095]::vec::Vec<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult> as rayon[422a4a25e8530bbf]::iter::ParallelExtend<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult>>::par_extend::<rayon[422a4a25e8530bbf]::iter::while_some::WhileSome<rayon[422a4a25e8530bbf]::iter::map::Map<rayon[422a4a25e8530bbf]::iter::map::Map<rayon[422a4a25e8530bbf]::iter::enumerate::Enumerate<rayon[422a4a25e8530bbf]::slice::Iter<&kani_metadata[b136932edba6d502]::harness::HarnessMetadata>>, <kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>, <core[2cc081e1ca4e22ab]::result::Result<_, _> as rayon[422a4a25e8530bbf]::iter::FromParallelIterator<core[2cc081e1ca4e22ab]::result::Result<_, _>>>::from_par_iter::ok<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult, anyhow[f4d019122e47c51f]::Error>::{closure#0}>>>
22: 0x564bf78fcd8d - <core[2cc081e1ca4e22ab]::result::Result<alloc[b38a0b67e7b55095]::vec::Vec<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult>, anyhow[f4d019122e47c51f]::Error> as rayon[422a4a25e8530bbf]::iter::FromParallelIterator<core[2cc081e1ca4e22ab]::result::Result<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult, anyhow[f4d019122e47c51f]::Error>>>::from_par_iter::<rayon[422a4a25e8530bbf]::iter::map::Map<rayon[422a4a25e8530bbf]::iter::enumerate::Enumerate<rayon[422a4a25e8530bbf]::slice::Iter<&kani_metadata[b136932edba6d502]::harness::HarnessMetadata>>, <kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}::{closure#0}>>
23: 0x564bf78b5172 - <rayon_core[794db04526e6cbbd]::job::StackJob<rayon_core[794db04526e6cbbd]::latch::LatchRef<rayon_core[794db04526e6cbbd]::latch::LockLatch>, <rayon_core[794db04526e6cbbd]::registry::Registry>::in_worker_cold<<rayon_core[794db04526e6cbbd]::thread_pool::ThreadPool>::install<<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessRunner>::check_all_harnesses::{closure#0}, core[2cc081e1ca4e22ab]::result::Result<alloc[b38a0b67e7b55095]::vec::Vec<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult>, anyhow[f4d019122e47c51f]::Error>>::{closure#0}, core[2cc081e1ca4e22ab]::result::Result<alloc[b38a0b67e7b55095]::vec::Vec<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult>, anyhow[f4d019122e47c51f]::Error>>::{closure#0}::{closure#0}, core[2cc081e1ca4e22ab]::result::Result<alloc[b38a0b67e7b55095]::vec::Vec<kani_driver[fdb88ce1931fef6d]::harness_runner::HarnessResult>, anyhow[f4d019122e47c51f]::Error>> as rayon_core[794db04526e6cbbd]::job::Job>::execute
24: 0x564bf79ac254 - <rayon_core[794db04526e6cbbd]::registry::WorkerThread>::wait_until_cold
25: 0x564bf79abe8b - <rayon_core[794db04526e6cbbd]::registry::ThreadBuilder>::run
26: 0x564bf79b168a - std[7d326e869719067]::sys::backtrace::__rust_begin_short_backtrace::<<rayon_core[794db04526e6cbbd]::registry::DefaultSpawn as rayon_core[794db04526e6cbbd]::registry::ThreadSpawn>::spawn::{closure#0}, ()>
27: 0x564bf79b04ef - <<std[7d326e869719067]::thread::Builder>::spawn_unchecked_<<rayon_core[794db04526e6cbbd]::registry::DefaultSpawn as rayon_core[794db04526e6cbbd]::registry::ThreadSpawn>::spawn::{closure#0}, ()>::{closure#1} as core[2cc081e1ca4e22ab]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
28: 0x564bf7bafb2f - std::sys::thread::unix::Thread::new::thread_start::hb1c7ce44d9ca47bd
29: 0x7fe390904464 - start_thread
30: 0x7fe3909875ac - __clone3
31: 0x0 - <unknown>