Invariant failed when generating SMT

[kaiboy05]

CBMC version: (cbmc-5.35.0) 64-bit x86_64 linux Operating system: Ubuntu 20.04 (WSL 1, with windows 10) Exact command line resulting in the issue: cbmc test.c --function totest --smt2 --outfile o What behaviour did you expect: Generate the SMT What happened instead: Invariant check failed

Hi,

I was trying to do the union casting between the uint and the float numbers. However, when I tried to generate the smt, it gives the invariant check failed error. Here is the code that I checked with cbmc, and the error message that I got.

test.c:

#include <stdint.h>

typedef union cfloat_uint32 {
    float f;
    uint32_t v;
} cfloat_uint32;

uint32_t totest(uint32_t a, uint32_t b) {
    cfloat_uint32 c_fa, c_fb;
    c_fa.v = a; c_fb.v = b;
    cfloat_uint32 c_result;
    c_result.f = c_fa.f + c_fb.f;

    assert(0 == c_result.v);

    return 0;
}

Error message:

--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/smt2/smt2_conv.cpp:939 function: type2id
Condition: false
Reason: Unreachable
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x7f6fe9b18de0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x7f6fe9b19389]
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) [0x7f6fe94017d8]
cbmc(smt2_convt::type2id[abi:cxx11](typet const&) const+0x6f5) [0x7f6fe996b095]
cbmc(smt2_convt::floatbv_suffix[abi:cxx11](exprt const&) const+0x60) [0x7f6fe996b300]
cbmc(smt2_convt::find_symbols(exprt const&)+0x1f7) [0x7f6fe9982867]
cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f6fe99826f3]
cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f6fe99826f3]
cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f6fe99826f3]
cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f6fe99826f3]
cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f6fe99826f3]
cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f6fe99826f3]
cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f6fe99826f3]
cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f6fe99826f3]
cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f6fe99826f3]
cbmc(smt2_convt::prepare_for_convert_expr(exprt const&)+0x48) [0x7f6fe99842a8]
cbmc(smt2_convt::set_to(exprt const&, bool)+0x36c) [0x7f6fe9985d2c]
cbmc(symex_target_equationt::convert_assignments(decision_proceduret&)+0xd1) [0x7f6fe9624211]
cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0x7a) [0x7f6fe962ca9a]
cbmc(symex_target_equationt::convert(decision_proceduret&)+0x42) [0x7f6fe962d5e2]
cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x334) [0x7f6fe941d164]
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) [0x7f6fe941d5e5]
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) [0x7f6fe942d555]
cbmc(stop_on_fail_verifiert<multi_path_symex_checkert>::operator()()+0x35) [0x7f6fe940a625]
cbmc(cbmc_parse_optionst::doit()+0xcfb) [0x7f6fe9408ecb]
cbmc(parse_options_baset::main()+0x8f) [0x7f6fe93ff99f]
cbmc(main+0x39) [0x7f6fe93eefc9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f6fe8bf70b3]
cbmc(_start+0x2e) [0x7f6fe94011ee]

May I know am I not supposed to do the union casting like this?

Thank you very much.

[martin-cs]

Thanks for this. Have you tried using the SAT back-end?

@thomasspriggs This is a lovely example of type-unsafe things that are a pain in SMT back-ends.

Also @TGWDB who has been working on this.

[kaiboy05]

Do you mean the normal invoke of cbmc like: "cbmc --function "? If that is the case, then it does work.

[martin-cs]

Yes and that is good because it means that it is an SMT back-end issue rather than anything more serious.