Invariant violation in boolbv_width.cpp

[danielsn]

CBMC version: 5.30
Operating system: OSX
Exact command line resulting in the issue:
Using this branch of RMC https://github.com/danielsn/rmc/tree/thread-lo
On this test: https://github.com/danielsn/rmc/blob/thread-lo/rust-tests/cbmc-reg/Static/fixme_thread_local.rs

╰─$ rmc --keep-temps --gen-c fixme_thread_local.rs
CBMC version 5.30.0 (cbmc-5.30.0) 64-bit x86_64 macos
Parsing /Users/dsn/ws/rmc/library/rmc/rmc_lib.c
Converting
Type-checking rmc_lib
Reading GOTO program from file
Reading: fixme_thread_local.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
replacing function pointer by 1 possible targets
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Unwinding loop _RINvMs_NtNtNtCskeHm4v7Nni3_3std6thread5local4fastINtB5_3KeymE14try_initializeNvNvCs1eoHebAXHQh_18fixme_thread_local3FOO6___initEB1h_.0 iteration 1  thread 0
Unwinding loop _RINvMs_NtNtNtCskeHm4v7Nni3_3std6thread5local4fastINtB5_3KeymE14try_initializeNvNvCs1eoHebAXHQh_18fixme_thread_local3FOO6___initEB1h_.1 iteration 1  thread 0
**** WARNING: no body for function _ZN3std3sys4unix17thread_local_dtor13register_dtor17h0f484916b69ea58fE
Unwinding loop _RINvMs_NtNtNtCskeHm4v7Nni3_3std6thread5local4fastINtB5_3KeymE14try_initializeNvNvCs1eoHebAXHQh_18fixme_thread_local3FOO6___initEB1h_.2 iteration 1 file /Users/dsn/ws/rmc/library/std/src/thread/local.rs line 608 column 16 function _RINvMs_NtNtNtCskeHm4v7Nni3_3std6thread5local4fastINtB5_3KeymE14try_initializeNvNvCs1eoHebAXHQh_18fixme_thread_local3FOO6___initEB1h_ thread 0
Unwinding loop _RINvMs_NtNtNtCskeHm4v7Nni3_3std6thread5local4fastINtB5_3KeymE14try_initializeNvNvCs1eoHebAXHQh_18fixme_thread_local3FOO6___initEB1h_.3 iteration 1  thread 0
Unwinding loop _RINvMs_NtNtNtCskeHm4v7Nni3_3std6thread5local4fastINtB5_3KeymE3getNvNvCs1eoHebAXHQh_18fixme_thread_local3FOO6___initEB15_.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsklTF4tl7UoN_4core6optionINtB3_6OptionRmE5ok_orNtNtNtCskeHm4v7Nni3_3std6thread5local11AccessErrorECs1eoHebAXHQh_18fixme_thread_local.0 iteration 1  thread 0
Runtime Symex: 0.0411644s
size of program expression: 826 steps
simple slicing removed 13 assignments
Generated 12 VCC(s), 12 remaining after simplification
Runtime Postprocess Equation: 7.2536e-05s
Passing problem to propositional reduction
converting SSA
warning: ignoring nil
--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20210513-58586-1vd9noc/src/solvers/flattening/boolbv_width.cpp:197 function: get_entry
Condition: false
Reason: Unimplemented
Backtrace:
0   cbmc                                0x00000001015e2fda _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   cbmc                                0x00000001015e34cb _Z13get_backtracev + 167
2   cbmc                                0x000000010164e39c _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
3   cbmc                                0x00000001015f4d29 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 9
4   cbmc                                0x000000010149281c _ZNK13boolbv_widtht9get_entryERK5typet + 3316
5   cbmc                                0x0000000101495eef _ZNK12bv_pointerst18bv_pointers_widthtclERK5typet + 143
6   cbmc                                0x000000010146d066 _ZN7boolbvt17conversion_failedERK5exprt + 64
7   cbmc                                0x000000010146db29 _ZN7boolbvt17convert_bitvectorERK5exprt + 2721
8   cbmc                                0x000000010149a881 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 3407
9   cbmc                                0x000000010146ccfa _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 702
10  cbmc                                0x00000001014765f3 _ZN7boolbvt19convert_byte_updateERK17byte_update_exprt + 371
11  cbmc                                0x000000010146d708 _ZN7boolbvt17convert_bitvectorERK5exprt + 1664
12  cbmc                                0x000000010149a881 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 3407
13  cbmc                                0x000000010146ccfa _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 702
14  cbmc                                0x00000001014706c8 _ZN7boolbvt27boolbv_set_equality_to_trueERK11equal_exprt + 206
15  cbmc                                0x000000010147079d _ZN7boolbvt6set_toERK5exprtb + 101
16  cbmc                                0x00000001012c6e57 _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 243
17  cbmc                                0x00000001012c6ae8 _ZN22symex_target_equationt26convert_without_assertionsER19decision_proceduret + 116
18  cbmc                                0x00000001012c7f55 _ZN22symex_target_equationt7convertER19decision_proceduret + 35
19  cbmc                                0x00000001011b7662 _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 125
20  cbmc                                0x00000001011b8bb6 _Z24prepare_property_deciderRNSt3__113unordered_mapI8dstringt14property_infotNS_4hashIS1_EENS_8equal_toIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 223
21  cbmc                                0x00000001011beb38 _ZN25multi_path_symex_checkertclERNSt3__113unordered_mapI8dstringt14property_infotNS0_4hashIS2_EENS0_8equal_toIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 218
22  cbmc                                0x00000001011b6071 _ZN43all_properties_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 55
23  cbmc                                0x00000001011aff52 _ZN19cbmc_parse_optionst4doitEv + 3560
24  cbmc                                0x00000001015f906c _ZN19parse_options_baset4mainEv + 136
25  cbmc                                0x00000001011a7d8c main + 44
26  libdyld.dylib                       0x00007fff6c521cc9 start + 1


--- end invariant violation report ---

What behaviour did you expect: CBMC to run on the generated file
What happened instead: The invariant violation

[danielsn]

Archive.zip

[zhassan-aws]

A crash with a similar signature can be reproduced on the json files in the attached tarball with the following steps:

1. tar xvzf get_entry.tar.gz
2. cd get_entry
3. symtab2gb bolero_engine-05c3719b9f62187e.json --out bolero_engine-05c3719b9f62187e.out
4. symtab2gb foo-3a660a6bba412286.json --out foo-3a660a6bba412286.out
5. goto-cc --function foo foo-3a660a6bba412286.out bolero_engine-05c3719b9f62187e.out -o a.out
6. cbmc a.out

Produces:

$ cbmc a.out 
CBMC version 5.30.1 (cbmc-5.30.1) 64-bit x86_64 linux
Reading GOTO program from file
Reading: a.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
replacing function pointer by 1 possible targets
replacing function pointer by 19 possible targets
replacing function pointer by 19 possible targets
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
**** WARNING: no body for function _ZN6bolero4test17hce23b7f8c0aff3afE
Unwinding loop gen-repeat<_8485061407329205194>.0 iteration 1  thread 0
**** WARNING: no body for function _ZN79_$LT$bolero_rmc..lib..RmcDriver$u20$as$u20$bolero_generator..driver..Driver$GT$10fill_bytes17hc5343827f6b15aafE
**** WARNING: no body for function _ZN75_$LT$core..option..Option$LT$T$GT$$u20$as$u20$core..ops..try_trait..Try$GT$6branch17h9f33f850d02c8e6bE
**** WARNING: no body for function _ZN84_$LT$core..option..Option$LT$T$GT$$u20$as$u20$core..ops..try_trait..FromResidual$GT$13from_residual17h3edf690493790d87E
**** WARNING: no body for function _ZN4core6option15Option$LT$T$GT$6as_ref17hc27381a897716995E
Unwinding loop _ZN163_$LT$bolero_engine..test..ClonedGeneratorTest$LT$F$C$G$C$$LT$G$u20$as$u20$bolero_generator..ValueGenerator$GT$..Output$GT$$u20$as$u20$bolero_engine..test..Test$GT$4test28_$u7b$$u7b$closure$u7d$$u7d$17h928d6c23e08148e7E.0 iteration 1 file /home/ubuntu/examples/iss479-2/bolero/bolero-engine/src/test.rs line 146 column 13 function <bolero::bolero_engine::ClonedGeneratorTest<F, G, <G as bolero::generator::ValueGenerator>::Output> as bolero::Test>::test::{closure#0} thread 0
aborting path on assume(false) at file /home/ubuntu/tools/rmc/library/std/src/panicking.rs line 367 column 19 function std::panicking::r#try thread 0
Unwinding loop _ZN6bolero45TestTarget$LT$G$C$E$C$bolero..ClonedInput$GT$8for_each17h4903cd54f6cee8f1E.4 iteration 1 file /home/ubuntu/examples/iss479-2/bolero/bolero/src/lib.rs line 393 column 13 function bolero::TestTarget::<G, E, bolero::ClonedInput>::for_each thread 0
Unwinding loop gen-repeat<_8485061407329205194>.0 iteration 1  thread 0
Unwinding loop _ZN163_$LT$bolero_engine..test..ClonedGeneratorTest$LT$F$C$G$C$$LT$G$u20$as$u20$bolero_generator..ValueGenerator$GT$..Output$GT$$u20$as$u20$bolero_engine..test..Test$GT$4test28_$u7b$$u7b$closure$u7d$$u7d$17h928d6c23e08148e7E.0 iteration 1 file /home/ubuntu/examples/iss479-2/bolero/bolero-engine/src/test.rs line 146 column 13 function <bolero::bolero_engine::ClonedGeneratorTest<F, G, <G as bolero::generator::ValueGenerator>::Output> as bolero::Test>::test::{closure#0} thread 0
aborting path on assume(false) at file /home/ubuntu/tools/rmc/library/std/src/panicking.rs line 367 column 19 function std::panicking::r#try thread 0
Runtime Symex: 0.0646082s
size of program expression: 2292 steps
simple slicing removed 60 assignments
Generated 23 VCC(s), 8 remaining after simplification
Runtime Postprocess Equation: 0.000193453s
Passing problem to propositional reduction
converting SSA
warning: ignoring nil
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/flattening/boolbv_width.cpp:197 function: get_entry
Condition: false
Reason: Unimplemented
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x55fc155784b0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x55fc15578a59]
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) [0x55fc14e6ac78]
cbmc(boolbv_widtht::get_entry(typet const&) const+0x278) [0x55fc15370de8]
cbmc(bv_pointerst::bv_pointers_widtht::operator()(typet const&) const+0x3d) [0x55fc1537891d]
cbmc(boolbvt::conversion_failed(exprt const&)+0xa6) [0x55fc153375f6]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x653) [0x55fc15338b53]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x55fc1537b791]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x55fc1533ae50]
cbmc(boolbvt::convert_byte_update(byte_update_exprt const&)+0x2c4) [0x55fc15347cb4]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x869) [0x55fc15338d69]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x55fc1537b791]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x55fc1533ae50]
cbmc(boolbvt::boolbv_set_equality_to_true(equal_exprt const&)+0xea) [0x55fc15337a8a]
cbmc(boolbvt::set_to(exprt const&, bool)+0x78) [0x55fc15337b58]
cbmc(symex_target_equationt::convert_assignments(decision_proceduret&)+0xd1) [0x55fc1508cb91]
cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0x7a) [0x55fc1509541a]
cbmc(symex_target_equationt::convert(decision_proceduret&)+0x42) [0x55fc15095f62]
cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x334) [0x55fc14e86574]
cbmc(prepare_property_decider(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&, symex_target_equationt&, goto_symex_property_decidert&, ui_message_handlert&)+0x3c5) [0x55fc14e869f5]
cbmc(multi_path_symex_checkert::operator()(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x155) [0x55fc14e967c5]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x92) [0x55fc14e79a52]
cbmc(cbmc_parse_optionst::doit()+0xc6a) [0x55fc14e7224a]
cbmc(parse_options_baset::main()+0x8f) [0x55fc14e68e3f]
cbmc(main+0x39) [0x55fc14e584e9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f28d959c0b3]
cbmc(_start+0x2e) [0x55fc14e6a68e]


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

get_entry.tar.gz

[tautschnig]

It seems initialisation of globals introduces a nil value, but I am yet to find out why that is the case:

// 1888 file /home/ubuntu/tools/rmc/library/std/src/thread/local.rs line 297 column 17
        ASSIGN _ZN13bolero_engine5panic11THREAD_NAME7__getit5__KEY17hcf3c235a4e519e6eE := { { { { { { { {  }, { {  }, NULL }, 0 }, 0 } } } } }, { { { 0, byte_update_little_endian(side_effect #source_location="" statement="nondet" is_nondet_nullable="1", 0, nil, union tag-_4825330555408575969-union) } } }, 0 }

[tautschnig]

There seems to be an empty union at play, and the following C example reproduces this same problem:

union U {};
union U u;

int main()
{
  __CPROVER_assert(0, "");
}

I'll try to come up with a fix.

[tautschnig]

This will need some further discussion as we need to figure out what the most appropriate way of handling empty unions is. It's an extension supported by at least GCC and Clang.

[kroening]

We do already do empty structs -- be symmetric here, and do whatever we did for that?

[tautschnig]

@kroening What would you think about introducing an empty_union_exprt to cope with empty unions? Edit: empty structs are still well-formed expressions as struct expressions have an arbitrary number of operands. union_exprt, on the other hand, is a unary_exprt.