search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
853 stars 265 forks source link

Invariant check failure with `--z3` #7442

Closed zhassan-aws closed 1 year ago

zhassan-aws commented 1 year ago

CBMC version: 5.72.0 Operating system: Ubuntu 20.04 Exact command line resulting in the issue: cbmc test1.for-main.out --z3 What behaviour did you expect: Verification successful What happened instead: CBMC crashed:

$ cbmc test1.for-main.out --z3
CBMC version 5.72.0 (cbmc-5.72.0) 64-bit x86_64 linux
Reading GOTO program from file test1.for-main.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 _RINvMNtCsirh5c5pMozQ_4core6optionINtB3_6OptionjE3mapuNCNvXs0_NtNtB5_5array4iterINtBX_8IntoIteruKj1_ENtNtNtNtB5_4iter6traits8iterator8Iterator4next0ECsblmgPdRjkL6_5test1.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 928 column 5 function std::option::Option::<usize>::map::<(), [closure@<std::array::IntoIter<(), 1> as std::iter::Iterator>::next::{closure#0}]> thread 0
Unwinding loop _RINvMNtCsirh5c5pMozQ_4core6optionINtB3_6OptionuE3mapbQNCNvXs0_NtCsdu1D5ETyiLn_4kani9arbitraryAbj1_NtBY_9Arbitrary3any0ECsblmgPdRjkL6_5test1.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 928 column 5 function std::option::Option::<()>::map::<bool, &mut [closure@<[bool; 1] as kani::Arbitrary>::any::{closure#0}]> thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 924 column 15 function std::option::Option::<bool>::map::<std::ops::try_trait::NeverShortCircuit<bool>, &mut fn(bool) -> std::ops::try_trait::NeverShortCircuit<bool> {std::ops::try_trait::NeverShortCircuit::<bool>}> thread 0
Unwinding loop _RINvMNtCsirh5c5pMozQ_4core6optionINtB3_6OptionbE3mapINtNtNtB5_3ops9try_trait17NeverShortCircuitbEQNcBO_0ECsblmgPdRjkL6_5test1.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 928 column 5 function std::option::Option::<bool>::map::<std::ops::try_trait::NeverShortCircuit<bool>, &mut fn(bool) -> std::ops::try_trait::NeverShortCircuit<bool> {std::ops::try_trait::NeverShortCircuit::<bool>}> thread 0
Unwinding loop _RINvMNtCsirh5c5pMozQ_4core6optionINtB3_6OptionbE3mapINtNtNtB5_3ops9try_trait17NeverShortCircuitbEQNcBO_0ECsblmgPdRjkL6_5test1.1 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 928 column 5 function std::option::Option::<bool>::map::<std::ops::try_trait::NeverShortCircuit<bool>, &mut fn(bool) -> std::ops::try_trait::NeverShortCircuit<bool> {std::ops::try_trait::NeverShortCircuit::<bool>}> thread 0
Unwinding loop _RINvMNtCsirh5c5pMozQ_4core6optionINtB3_6OptionbE3mapINtNtNtB5_3ops9try_trait17NeverShortCircuitbEQNcBO_0ECsblmgPdRjkL6_5test1.0 iteration 2 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 928 column 5 function std::option::Option::<bool>::map::<std::ops::try_trait::NeverShortCircuit<bool>, &mut fn(bool) -> std::ops::try_trait::NeverShortCircuit<bool> {std::ops::try_trait::NeverShortCircuit::<bool>}> thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs line 872 column 15 function std::array::try_collect_into_array::<std::iter::Map<&mut std::iter::Map<std::array::IntoIter<(), 1>, [closure@<[bool; 1] as kani::Arbitrary>::any::{closure#0}]>, fn(bool) -> std::ops::try_trait::NeverShortCircuit<bool> {std::ops::try_trait::NeverShortCircuit::<bool>}>, bool, std::ops::try_trait::NeverShortCircuitResidual, 1> thread 0
Unwinding loop _RINvNtCsirh5c5pMozQ_4core5array22try_collect_into_arrayINtNtNtNtB4_4iter8adapters3map3MapQIBS_INtNtB2_4iter8IntoIteruKj1_ENCNvXs0_NtCsdu1D5ETyiLn_4kani9arbitraryAbB1S_NtB24_9Arbitrary3any0ENcINtNtNtB4_3ops9try_trait17NeverShortCircuitbE0EbNtB36_25NeverShortCircuitResidualKB1S_ECsblmgPdRjkL6_5test1.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs line 884 column 21 function std::array::try_collect_into_array::<std::iter::Map<&mut std::iter::Map<std::array::IntoIter<(), 1>, [closure@<[bool; 1] as kani::Arbitrary>::any::{closure#0}]>, fn(bool) -> std::ops::try_trait::NeverShortCircuit<bool> {std::ops::try_trait::NeverShortCircuit::<bool>}>, bool, std::ops::try_trait::NeverShortCircuitResidual, 1> thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 105 column 9 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 1536 column 32 function std::result::Result::<std::ops::try_trait::NeverShortCircuit<[bool; 1]>, std::array::IntoIter<bool, 1>>::unwrap_unchecked thread 0
aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 1533 column 15 function std::result::Result::<std::ops::try_trait::NeverShortCircuit<[bool; 1]>, std::array::IntoIter<bool, 1>>::unwrap_unchecked thread 0
Unwinding loop _RINvNtCsirh5c5pMozQ_4core3ptr13drop_in_placeINtNtB4_6result6ResultINtNtNtB4_3ops9try_trait17NeverShortCircuitAbj1_EINtNtNtB4_5array4iter8IntoIterbKB1L_EEECsblmgPdRjkL6_5test1.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs line 490 column 1 function std::ptr::drop_in_place::<std::result::Result<std::ops::try_trait::NeverShortCircuit<[bool; 1]>, std::array::IntoIter<bool, 1>>> thread 0
Unwinding loop _RNvMNtCsirh5c5pMozQ_4core6resultINtB2_6ResultINtNtNtB4_3ops9try_trait17NeverShortCircuitAbj1_EINtNtNtB4_5array4iter8IntoIterbKB1q_EE16unwrap_uncheckedCsblmgPdRjkL6_5test1.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 1538 column 5 function std::result::Result::<std::ops::try_trait::NeverShortCircuit<[bool; 1]>, std::array::IntoIter<bool, 1>>::unwrap_unchecked thread 0
Runtime Symex: 0.103049s
size of program expression: 4114 steps
simple slicing removed 412 assignments
Generated 43 VCC(s), 10 remaining after simplification
Runtime Postprocess Equation: 0.000413639s
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/smt2/smt2_conv.cpp:5643 function: convert_type
Condition: Check return value
Reason: to_union_type(ns.follow(type)).components().empty() || width != 0
Backtrace:
cbmc(+0xa955f0) [0x5637875bc5f0]
cbmc(+0xa95b99) [0x5637875bcb99]
cbmc(+0x224de4) [0x563786d4bde4]
cbmc(+0x8b38b6) [0x5637873da8b6]
cbmc(+0x88e107) [0x5637873b5107]
cbmc(+0x8adc37) [0x5637873d4c37]
cbmc(+0x8ae4fd) [0x5637873d54fd]
cbmc(+0x8ae448) [0x5637873d5448]
cbmc(+0x8ae474) [0x5637873d5474]
cbmc(+0x8adaf6) [0x5637873d4af6]
cbmc(+0x8ae4fd) [0x5637873d54fd]
cbmc(+0x8ae474) [0x5637873d5474]
cbmc(+0x8adaf6) [0x5637873d4af6]
cbmc(+0x8ae4fd) [0x5637873d54fd]
cbmc(+0x8adaf6) [0x5637873d4af6]
cbmc(+0x8ae4fd) [0x5637873d54fd]
cbmc(+0x8ae474) [0x5637873d5474]
cbmc(+0x8ae413) [0x5637873d5413]
cbmc(+0x8ae474) [0x5637873d5474]
cbmc(+0x8ae82f) [0x5637873d582f]
cbmc(+0x8af513) [0x5637873d6513]
cbmc(+0x54fd41) [0x563787076d41]
cbmc(+0x5584f6) [0x56378707f4f6]
cbmc(+0x5590a2) [0x5637870800a2]
cbmc(+0x3480f4) [0x563786e6f0f4]
cbmc(+0x348575) [0x563786e6f575]
cbmc(+0x35a005) [0x563786e81005]
cbmc(+0x2004f9) [0x563786d274f9]
cbmc(+0x1fca1e) [0x563786d23a1e]
cbmc(+0x1f420f) [0x563786d1b20f]
cbmc(+0x1e0239) [0x563786d07239]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7fb6cfbcf0b3]
cbmc(+0x1f5b8e) [0x563786d1cb8e]

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
failed to get width of union
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---
Aborted (core dumped)
zhassan-aws commented 1 year ago

test1.tar.gz