Invariant violation 'convert_mult'

[tedinski]

CBMC version: HEAD (cbmc-5.36.0-72-gf917b98e8) and cbmc-5.30.1
Operating system: Ubuntu 20.04
Exact command line resulting in the issue:

build/bin/symtab2gb unsigned.json --out prog
build/bin/cbmc prog --function main

What behaviour did you expect: CBMC to successfully verify
What happened instead:

CBMC version 5.36.0 (cbmc-5.36.0-72-gf917b98e8) 64-bit x86_64 linux
Reading GOTO program from file
...SNIPPED...
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: /home/ubuntu/cbmc/src/solvers/flattening/boolbv_mult.cpp:73 function: convert_mult
Condition: it->type() == expr.type()
Reason: multiplication operands should have same type as expression

Click to expand Backtrace:

build/bin/cbmc(print_backtrace(std::ostream&)+0x50) [0x560900ba02c0]
build/bin/cbmc(get_backtrace[abi:cxx11]()+0x169) [0x560900ba0869]
build/bin/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) [0x5609004837b8]
build/bin/cbmc(boolbvt::convert_mult(mult_exprt const&)+0xbbc) [0x5609009866cc]
build/bin/cbmc(boolbvt::convert_bitvector(exprt const&)+0x6a5) [0x560900957dc5]
build/bin/cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x56090099f9d1]
build/bin/cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x56090095ae70]
build/bin/cbmc(boolbvt::convert_equality(equal_exprt const&)+0xd2) [0x56090096ec42]
build/bin/cbmc(boolbvt::convert_rest(exprt const&)+0x24d) [0x56090095868d]
build/bin/cbmc(bv_pointerst::convert_rest(exprt const&)+0xab) [0x56090099b5eb]
build/bin/cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x2db) [0x5609009d83bb]
build/bin/cbmc(prop_conv_solvert::convert(exprt const&)+0x127) [0x5609009da187]
build/bin/cbmc(boolbvt::convert_byte_extract(byte_extract_exprt const&)+0x8ae) [0x56090096610e]
build/bin/cbmc(boolbvt::convert_bitvector(exprt const&)+0x8ef) [0x56090095800f]
build/bin/cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x56090099f9d1]
build/bin/cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x56090095ae70]
build/bin/cbmc(boolbvt::convert_bv_typecast(typecast_exprt const&)+0x4b) [0x560900991d5b]
build/bin/cbmc(boolbvt::convert_bitvector(exprt const&)+0x2b6) [0x5609009579d6]
build/bin/cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x56090099f9d1]
build/bin/cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x56090095ae70]
build/bin/cbmc(boolbvt::convert_bv_rel(binary_relation_exprt const&)+0x60) [0x5609009648c0]
build/bin/cbmc(boolbvt::convert_rest(exprt const&)+0x24d) [0x56090095868d]
build/bin/cbmc(bv_pointerst::convert_rest(exprt const&)+0xab) [0x56090099b5eb]
build/bin/cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x2db) [0x5609009d83bb]
build/bin/cbmc(prop_conv_solvert::convert(exprt const&)+0x127) [0x5609009da187]
build/bin/cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x67d) [0x5609009d875d]
build/bin/cbmc(prop_conv_solvert::convert(exprt const&)+0x127) [0x5609009da187]
build/bin/cbmc(prop_conv_solvert::set_equality_to_true(equal_exprt const&)+0x9c) [0x5609009d667c]
build/bin/cbmc(prop_conv_solvert::add_constraints_to_prop(exprt const&, bool)+0x239) [0x5609009d6f39]
build/bin/cbmc(prop_conv_solvert::set_to(exprt const&, bool)+0x4c7) [0x5609009d7a07]
build/bin/cbmc(boolbvt::set_to(exprt const&, bool)+0x8a) [0x56090095748a]
build/bin/cbmc(symex_target_equationt::convert_assignments(decision_proceduret&)+0xd1) [0x5609006a6f91]
build/bin/cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0x7a) [0x5609006af82a]
build/bin/cbmc(symex_target_equationt::convert(decision_proceduret&)+0x42) [0x5609006b0372]
build/bin/cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x334) [0x56090049f194]
build/bin/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) [0x56090049f615]
build/bin/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) [0x5609004af5e5]
build/bin/cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x92) [0x560900492662]
build/bin/cbmc(cbmc_parse_optionst::doit()+0xd0e) [0x56090048af0e]
build/bin/cbmc(parse_options_baset::main()+0x8f) [0x56090048197f]
build/bin/cbmc(main+0x39) [0x560900470f29]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f2a2de8a0b3]
build/bin/cbmc(_start+0x2e) [0x5609004831ce]

I've attached two files: unsigned.json and signed.json. These files are generated by RMC (Rust Model Checker), which generates symbol tables to send as inputs to CBMC. The unsigned file exhibits this crash in CBMC, and signed shows the "fix" (or workaround?) that does not. The difference between these is simply choice of type for some values that are used as array/vector indexes. (i.e. one does a more complicated version of a[x] where x is unsigned, and the other a[x] but now x is signed. But I haven't been able to reproduce this from C code, so it must be more complicated than that, somehow.) I'm not skilled at debugging CBMC, so I'm asking for some help here.

The code in RMC that generates the constructs in question is in a pull request here if that's helpful in understanding what's going on:
https://github.com/model-checking/rmc/pull/417/files#diff-6d72a804aa90eefd32b74c247e51a3b501a686a3a2c137dbcfff59b932a209deR860-R862

It very well could be the error is on RMC's side (generating a bad symbol table), but I'm unable to figure out exactly what it might be. A multiply doesn't appear in our symbol table, I'm guessing it's generated as part of array/vector indexing. However:

1. I think there's at least an error message problem with CBMC. (It'd be nice if the invariant error were spotted earlier than this presumably generated code, since we don't emit any mult constructs.)
2. I think there's a bug with how the CBMC back-end is handling types, possibly one that is not even triggerable from the C front-end of CBMC. We should be able to index an array with an unsigned integer type, right?
3. I might be barking up the wrong tree thinking it's about array/vector indexing!

The original input Rust files were minimized before running them through RMC to generate the attached file, but it's still a large symbol table file. I'm hoping this bug will be easy to spot if someone skilled with debugging CBMC looks into this crash for me. But if it's necessary to try to minimize the generated symbol table file, let me know and I'll see what I can do.

Files

• signed.json.gz
• unsigned.json.gz

[jimgrundy]

Dropping AWS label after review with @danielsn as there is no particular AWS interest.