CBMC 5.12 crashes on converting structs to SMT2

amosr commented 4 years ago

CBMC version: 5.12 (pilot_release_3_1_6-352-g0e8fb44063-dirty) and current head (cbmc-5.12-161-g48b8c90dd), though 5.11 works Operating system: OSX and Ubuntu Linux Exact command line resulting in the issue: cbmc smt_failure.c --smt2 What behaviour did you expect: verification should fail What happened instead: CBMC crashes with the error map::at: key not found:

CBMC version 5.12 (cbmc-5.12-161-g48b8c90dd) 64-bit x86_64 macos
Parsing smt_failure.c
Converting
Type-checking smt_failure
file smt_failure.c line 8 function main: function 'assert' is not declared
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
size of program expression: 45 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
map::at:  key not found

Test case smt_failure.c:

struct tiny {
    char field;
};

int main()
{
    struct tiny x;
    assert(x.field == 0);
}

Hi, Sorry if this is a known issue – on the surface it looks similar to #4206, but I think it's different because this test case doesn't include flexible structs and only fails on the most recent version.

jackhumphries commented 4 years ago

I'm seeing this issue, too. Is this a new issue (i.e., has CBMC worked in previous versions?) or has it always existed? This is a real bummer for me because I want to use the SMT backend rather than the SAT backend. Have you found a workaround?

martin-cs commented 4 years ago

@amosr and @jackhumphries : sorry that no-one responded to this sooner.

I have managed to replicate this issue with the latest develop so I think this is definitely a problem. I note that running with --smt2 --outfile whatever.smt2 seems to produce valid SMT so I don't think the problem is with conversion. --smt2 --outfile whatever.smt2 --z3 gives the same issue but --smt2 --outfile whatever.smt2 --cvc4 works so I think the issue is with the Z3 specific code.

martin-cs commented 4 years ago

Z3 uses the use_datatypes option in smt2_convt and that seems to have been broken.

martin-cs commented 4 years ago

As a work-around setting use_datatypes = false on smt2_conv.cpp:98 should work.

martin-cs commented 4 years ago

I think I have tracked down what is going on.

The following backtrace is useful:

#0  0x00007fc5b420aafd in __cxa_throw () from /lib/x86_64-linux-gnu/libstdc++.so.6
#1  0x00007fc5b420686b in ?? () from /lib/x86_64-linux-gnu/libstdc++.so.6
#2  0x0000557b4ec00f2c in std::map<typet, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::less<typet>, std::allocator<st$
    at /usr/include/c++/8/bits/stl_function.h:385
#3  0x0000557b4ebeb175 in smt2_convt::convert_type (this=0x557b5033fdb0, type=...) at smt2/smt2_conv.cpp:4616
#4  0x0000557b4ebfe993 in smt2_convt::find_symbols (this=0x557b5033fdb0, expr=...) at ../util/expr.h:84
#5  0x0000557b4ebfe2fc in smt2_convt::find_symbols (this=0x557b5033fdb0, expr=...) at smt2/smt2_conv.cpp:4291
#6  0x0000557b4ebff7d3 in smt2_convt::prepare_for_convert_expr (this=0x557b5033fdb0, expr=...) at smt2/smt2_conv.cpp:4266
#7  0x0000557b4ec00645 in smt2_convt::convert (this=0x557b5033fdb0, expr=...) at smt2/smt2_conv.cpp:715
#8  0x0000557b4ec00818 in smt2_convt::handle (this=0x557b5033fdb0, expr=...) at smt2/smt2_conv.cpp:736
#9  0x0000557b4eac115a in symex_target_equationt::convert_decls (this=0x557b503a7628, decision_procedure=...) at symex_target_equation.cpp:385
#10 0x0000557b4eac7400 in symex_target_equationt::convert_without_assertions (this=0x557b503a7628, decision_procedure=...) at symex_target_equation.cpp:339
#11 0x0000557b4eac7e31 in symex_target_equationt::convert (this=0x557b503a7628, decision_procedure=...) at symex_target_equation.cpp:349
#12 0x0000557b4e918348 in convert_symex_target_equation (equation=..., decision_procedure=..., message_handler=...) at bmc_util.cpp:158
#13 0x0000557b4e91877c in prepare_property_decider (properties=std::unordered_map with 1 element = {...}, equation=..., property_decider=..., ui_message_handl$
    at bmc_util.cpp:363
#14 0x0000557b4e927114 in multi_path_symex_checkert::operator() (this=this@entry=0x557b503a7398, properties=std::unordered_map with 1 element = {...})
    at multi_path_symex_checker.cpp:61
#15 0x0000557b4e750d72 in all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator() (this=0x557b503a71a0)
    at /usr/include/c++/8/bits/unordered_set.h:97
#16 0x0000557b4e74baa7 in cbmc_parse_optionst::doit (this=0x7fff4f3dcf10) at cbmc_parse_options.cpp:776
#17 0x0000557b4e5cf35b in parse_options_baset::main (this=this@entry=0x7fff4f3dcf10) at parse_options.cpp:98
#18 0x0000557b4e5bd9a1 in main (argc=argc@entry=0x3, argv=argv@entry=0x7fff4f3dd368) at cbmc_main.cpp:46
#19 0x00007fc5b3e3e09b in __libc_start_main (main=0x557b4e5bd980 <main(int, char const**)>, argc=0x3, argv=0x7fff4f3dd368, init=<optimized out>, fini=<optimiz$
    rtld_fini=<optimized out>, stack_end=0x7fff4f3dd358) at ../csu/libc-start.c:308
#20 0x0000557b4e5cfe3a in _start () at /usr/include/c++/8/ext/new_allocator.h:79

but note some of the line numbers are wrong, caused, I think by polymorphic dispatch on find_symbols and rr interacting badly.

The exception is thrown from: https://github.com/diffblue/cbmc/blob/a46f12d66e049e97940deaa2ad58c42dbd301819/src/solvers/smt2/smt2_conv.cpp#L4531 (and handled badly by the top level catch but that is a different issue) because there is not an appropriate entry in datatype_map for something of type ID_struct_tag.

How does this happen? If find_symbols(const exprt &expr) https://github.com/diffblue/cbmc/blob/a46f12d66e049e97940deaa2ad58c42dbd301819/src/solvers/smt2/smt2_conv.cpp#L4271 is called on a ID_symbol with type ID_struct_tag then the recursion into find_symbols(const typet &type) https://github.com/diffblue/cbmc/blob/a46f12d66e049e97940deaa2ad58c42dbd301819/src/solvers/smt2/smt2_conv.cpp#L4274 is supposed to populate the datatype_map but doesn't. So when you get to https://github.com/diffblue/cbmc/blob/a46f12d66e049e97940deaa2ad58c42dbd301819/src/solvers/smt2/smt2_conv.cpp#L4321 it's all going to go wrong.

Why doesn't it populate it correctly? find_symbols_rec 's handling of ID_struct_tag https://github.com/diffblue/cbmc/blob/a46f12d66e049e97940deaa2ad58c42dbd301819/src/solvers/smt2/smt2_conv.cpp#L4823 recurses correctly but doesn't add to the map.

This was broken by a change in how structs are represented. It may be @kroening 's change https://github.com/diffblue/cbmc/commit/170c5223f6caa66c977e6dde53f91dc257aa9b1f or the subsequent "future change whereby these types are no longer expanded by the program analyzer".

Work-arounds:

Give --outfile whatever.smt2
Use a solver other than z3
Change https://github.com/diffblue/cbmc/blob/a46f12d66e049e97940deaa2ad58c42dbd301819/src/solvers/smt2/smt2_conv.cpp#L98 to set it to false (or just remove this line entirely).

Thought on patches most welcome.

thomasspriggs commented 3 years ago

~I think this issue may have been fixed by https://github.com/diffblue/cbmc/commit/fa657acfb8e43161a0cceab9c8ed61a10193b31c~ The fix is in this PR - https://github.com/diffblue/cbmc/pull/5904 Your specific test case needs to be tried with this fix in place in order to check this.

tautschnig commented 3 years ago

Your specific test case needs to be tried with this fix in place in order to check this.

Confirmed, thus closing the issue.

diffblue / cbmc

CBMC 5.12 crashes on converting structs to SMT2 #5297