path-based symex throws map out of range error

[polgreen]

Path based symex throws the following error with :

terminate called after throwing an instance of 'std::out_of_range'
  what():  _Map_base::at

Stack trace

#0  0x0000000000a9e2b8 in raise ()
#1  0x0000000000a9e7ea in abort ()
#2  0x0000000000a6c18d in __gnu_cxx::__verbose_terminate_handler() ()
#3  0x00000000009dd7d6 in __cxxabiv1::__terminate(void (*)()) ()
#4  0x00000000009dd821 in std::terminate() ()
#5  0x00000000009dc9d9 in __cxa_throw ()
#6  0x0000000000a14dff in std::__throw_out_of_range(char const*) ()
#7  0x000000000080be83 in std::__detail::_Map_base<dstringt, std::pair<dstringt const, local_safe_pointerst>, std::allocator<std::pair<dstringt const, local_safe_pointerst> >, std::__detail::_Select1st, std::equal_to<dstringt>, std::hash<dstringt>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, false, true>, true>::at(dstringt const&) () at /usr/include/c++/5/bits/hashtable_policy.h:646
#8  0x000000000080be09 in std::unordered_map<dstringt, local_safe_pointerst, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, local_safe_pointerst> > >::at(dstringt const&) () at /usr/include/c++/5/bits/unordered_map.h:685
#9  0x000000000080adc7 in goto_symext::dereference_rec(exprt&, goto_symex_statet&, guardt&, bool) () at symex_dereference.cpp:250
#10 0x000000000080b79d in goto_symext::dereference_rec(exprt&, goto_symex_statet&, guardt&, bool) () at symex_dereference.cpp:355
#11 0x000000000080b79d in goto_symext::dereference_rec(exprt&, goto_symex_statet&, guardt&, bool) () at symex_dereference.cpp:355
#12 0x000000000080b79d in goto_symext::dereference_rec(exprt&, goto_symex_statet&, guardt&, bool) () at symex_dereference.cpp:355
#13 0x000000000080bb3b in goto_symext::dereference(exprt&, goto_symex_statet&, bool) () at symex_dereference.cpp:373
#14 0x0000000000806910 in goto_symext::clean_expr(exprt&, goto_symex_statet&, bool) () at symex_clean_expr.cpp:144
#15 0x000000000081517a in goto_symext::symex_goto(goto_symex_statet&) () at symex_goto.cpp:28
#16 0x000000000081e662 in goto_symext::symex_step(std::function<goto_functiont const& ()(dstringt const&)> const&, goto_symex_statet&) () at symex_main.cpp:349
#17 0x00000000005ca4af in symex_bmct::symex_step(std::function<goto_functiont const& ()(dstringt const&)> const&, goto_symex_statet&) () at symex_bmc.cpp:66
#18 0x000000000081d7e6 in goto_symext::symex_threaded_step(goto_symex_statet&, std::function<goto_functiont const& ()(dstringt const&)> const&) () at symex_main.cpp:151
#19 0x000000000081db28 in goto_symext::symex_with_state(goto_symex_statet&, std::function<goto_functiont const& ()(dstringt const&)> const&, symbol_tablet&) () at symex_main.cpp:201
#20 0x000000000081dd51 in goto_symext::resume_symex_from_saved_state(std::function<goto_functiont const& ()(dstringt const&)> const&, goto_symex_statet const&, symex_target_equationt*, symbol_tablet&) ()
    at symex_main.cpp:242
#21 0x00000000005913bb in path_explorert::perform_symbolic_execution(std::function<goto_functiont const& ()(dstringt const&)>) () at bmc.cpp:709
#22 0x000000000058e439 in bmct::execute(abstract_goto_modelt&) () at bmc.cpp:334
#23 0x000000000058f423 in bmct::run(abstract_goto_modelt&) () at bmc.cpp:486
#24 0x000000000059061b in bmct::do_language_agnostic_bmc(path_strategy_choosert const&, optionst const&, abstract_goto_modelt&, ui_message_handlert::uit const&, messaget&, std::function<void ()(bmct&, symbol_tablet const&)>, std::function<bool ()()>) () at bmc.cpp:648
#25 0x00000000005aee90 in cbmc_parse_optionst::doit() () at cbmc_parse_options.cpp:539
#26 0x00000000009ca528 in parse_options_baset::main() () at parse_options.cpp:66
#27 0x00000000005a9f8c in main () at cbmc_main.cpp:46

Binary:
https://s3.amazonaws.com/cbmc-public-bucket/pathsymex_test.binary

Command:

cbmc --paths fifo pathsymex_test.binary

(Error is independent of whether fifo or lifo is used)

Maybe of interest to @karkhaz

[karkhaz]

Oooh, thanks. I'll take a look over the weekend.

[tautschnig]

My hunch is that goto_symext::safe_pointers is not actually in the right place as this needs to be maintained per path. Pinging @smowton to work with @karkhaz.

[karkhaz]

@polgreen I'm going to try debugging this blindly, but I can't actually run CBMC on the binary that you linked to.

> cbmc --paths fifo pathsymex_test.binary
CBMC version 5.9 () 64-bit x86_64 linux
Reading GOTO program from file
Reading: pathsymex_test.binary
The input was compiled with an unsupported version of goto-cc; please recompile
Numeric exception : 0
> cbmc --version
5.9 ()
> goto-cc --version
gcc (goto-cc 5.9 ()) 8.1.1

Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger
CBMC version: 5.9 ()
Architecture: x86_64
OS: linux
gcc: 8.1.1

@tautschnig do you know what might be causing this? @polgreen would you mind checking what version of goto-cc you're using; if it's different to mine, would you rebuild with tip-of-tree goto-cc?

[karkhaz]

OK, can reproduce with

int foo(int *x)
{
  if(*x)
  {
    int y = 9;
  }
  else
  {
    int z = 4;
  }
}

int main()
{
  int x;
  foo(&x);
}

backtrace:

terminate called after throwing an instance of 'std::out_of_range'
  what():  _Map_base::at

Program received signal SIGABRT, Aborted.
0x00007ffff711c86b in raise () from /usr/lib/libc.so.6
#0  0x00007ffff711c86b in raise () from /usr/lib/libc.so.6
#1  0x00007ffff710740e in abort () from /usr/lib/libc.so.6
#2  0x00007ffff7ad844a in __gnu_cxx::__verbose_terminate_handler ()
    at /build/gcc/src/gcc/libstdc++-v3/libsupc++/vterminate.cc:95
#3  0x00007ffff7ade9d6 in __cxxabiv1::__terminate(void (*)()) ()
    at /build/gcc/src/gcc/libstdc++-v3/libsupc++/eh_terminate.cc:47
#4  0x00007ffff7adea13 in std::terminate ()
    at /build/gcc/src/gcc/libstdc++-v3/libsupc++/eh_terminate.cc:57
#5  0x00007ffff7adec48 in __cxxabiv1::__cxa_throw (obj=obj@entry=0x555556663730,
    tinfo=0x7ffff7dcb038 <typeinfo for std::out_of_range>,
    dest=0x7ffff7af4200 <std::out_of_range::~out_of_range()>)
    at /build/gcc/src/gcc/libstdc++-v3/libsupc++/eh_throw.cc:95
#6  0x00007ffff7ada575 in std::__throw_out_of_range (__s=0x5555562696e4 "_Map_base::at")
   from /usr/lib/libstdc++.so.6
#7  0x0000555555da78b9 in std::__detail::_Map_base<dstringt, std::pair<dstringt const, local_safe_pointerst>, std::allocator<std::pair<dstringt const, local_safe_pointerst> >, std::__detail::_Select1st, std::equal_to<dstringt>, std::hash<dstringt>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, false, true>, true>::at (this=0x7fffffffccb8,
    __k=...)
    at /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/8.1.1/../../../../include/c++/8.1.1/bits/hashtable_policy.h:760
#8  0x0000555555da7198 in std::unordered_map<dstringt, local_safe_pointerst, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, local_safe_pointerst> > >::at (this=0x7fffffffccb8, __k=...)
    at /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/8.1.1/../../../../include/c++/8.1.1/bits/unordered_map.h:994
#9  0x0000555555da3a41 in goto_symext::dereference_rec (this=0x7fffffffcaa8, expr=...,
    state=..., guard=..., write=false)
    at /home/kareem/doc/cbmc/src/goto-symex/symex_dereference.cpp:250
#10 0x0000555555da48ab in goto_symext::dereference_rec (this=0x7fffffffcaa8, expr=...,
    state=..., guard=..., write=false)
    at /home/kareem/doc/cbmc/src/goto-symex/symex_dereference.cpp:355
#11 0x0000555555da48ab in goto_symext::dereference_rec (this=0x7fffffffcaa8, expr=...,
    state=..., guard=..., write=false)
    at /home/kareem/doc/cbmc/src/goto-symex/symex_dereference.cpp:355
#12 0x0000555555da6a0a in goto_symext::dereference (this=0x7fffffffcaa8, expr=...,
    state=..., write=false)
    at /home/kareem/doc/cbmc/src/goto-symex/symex_dereference.cpp:373
#13 0x0000555555d9fab7 in goto_symext::clean_expr (this=0x7fffffffcaa8, expr=...,
    state=..., write=false)
    at /home/kareem/doc/cbmc/src/goto-symex/symex_clean_expr.cpp:144
#14 0x0000555555db1b64 in goto_symext::symex_goto (this=0x7fffffffcaa8, state=...)
    at /home/kareem/doc/cbmc/src/goto-symex/symex_goto.cpp:28
#15 0x0000555555dbcc5b in goto_symext::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&) (this=0x7fffffffcaa8, get_goto_function=...,
    state=...) at /home/kareem/doc/cbmc/src/goto-symex/symex_main.cpp:349
#16 0x0000555555b0c733 in symex_bmct::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&) (this=0x7fffffffcaa8, get_goto_function=...,
    state=...) at /home/kareem/doc/cbmc/src/cbmc/symex_bmc.cpp:66
#17 0x0000555555dbb941 in goto_symext::symex_threaded_step(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&) (this=0x7fffffffcaa8, state=...,
    get_goto_function=...) at /home/kareem/doc/cbmc/src/goto-symex/symex_main.cpp:151
#18 0x0000555555dbbd88 in goto_symext::symex_with_state(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&, symbol_tablet&) (this=0x7fffffffcaa8,
    state=..., get_goto_function=..., new_symbol_table=...)
    at /home/kareem/doc/cbmc/src/goto-symex/symex_main.cpp:201
#19 0x0000555555dbbf68 in goto_symext::resume_symex_from_saved_state(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet const&, symex_target_equationt*, symbol_tablet&) (this=0x7fffffffcaa8, get_goto_function=..., saved_state=...,
    saved_equation=0x7fffffffca48, new_symbol_table=...)
    at /home/kareem/doc/cbmc/src/goto-symex/symex_main.cpp:239
#20 0x0000555555ac5741 in path_explorert::perform_symbolic_execution(std::function<goto_functiont const& (dstringt const&)>) (this=0x7fffffffc7a0, get_goto_function=...)
    at /home/kareem/doc/cbmc/src/cbmc/bmc.cpp:709
#21 0x0000555555ac16e4 in bmct::execute (this=0x7fffffffc7a0, goto_model=...)
    at /home/kareem/doc/cbmc/src/cbmc/bmc.cpp:334
#22 0x0000555555ac2ccd in bmct::run (this=0x7fffffffc7a0, goto_model=...)
    at /home/kareem/doc/cbmc/src/cbmc/bmc.cpp:486
#23 0x0000555555ac48ea in bmct::do_language_agnostic_bmc(path_strategy_choosert const&, optionst const&, abstract_goto_modelt&, ui_message_handlert::uit const&, messaget&, std::function<void (bmct&, symbol_tablet const&)>, std::function<bool ()>) (
    path_strategy_chooser=..., opts=..., model=...,
    ui=@0x7fffffffddac: ui_message_handlert::uit::PLAIN, message=...,
    driver_configure_bmc=..., callback_after_symex=...)
    at /home/kareem/doc/cbmc/src/cbmc/bmc.cpp:649
#24 0x0000555555ab1e22 in cbmc_parse_optionst::doit (this=0x7fffffffe0f0)
    at /home/kareem/doc/cbmc/src/cbmc/cbmc_parse_options.cpp:543
#25 0x00005555561b62a8 in parse_options_baset::main (this=0x7fffffffe0f0)
    at /home/kareem/doc/cbmc/src/util/parse_options.cpp:66
#26 0x0000555555aa7f7e in main (argc=4, argv=0x7fffffffe558)
    at /home/kareem/doc/cbmc/src/cbmc/cbmc_main.cpp:46

[polgreen]

I think i compiled that binary with CBMC 5.10, which I guess would explain that? (think...I've got a lot of binaries and a lot of different versions of CBMC at the moment).

[karkhaz]

@polgreen I just posted a patch (#2879). Please apply it and let me know if that fixes the issue.

[polgreen]

Great, that was quick, thanks! It's been running for ~10 minutes and not thrown any exceptions, so I'd say that's fixed. I'll let you know if it finds a path.

(pathsymex_test was a 5.10 binary, I can run your branch on it without any changes, so I'm running that instead of patching)

Looks like some java library changes have snuck into the PR by accident?

[karkhaz]

Yes, not sure why the submodule change got included in the patch; fixed now. Thanks for the report.