Skip to content

path-based symex throws map out of range error #2866

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
polgreen opened this issue Aug 30, 2018 · 8 comments · Fixed by #2879
Closed

path-based symex throws map out of range error #2866

polgreen opened this issue Aug 30, 2018 · 8 comments · Fixed by #2879

Comments

@polgreen
Copy link
Contributor

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
Copy link
Collaborator

karkhaz commented Aug 30, 2018

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

@tautschnig
Copy link
Collaborator

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
Copy link
Collaborator

karkhaz commented Sep 1, 2018

@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
Copy link
Collaborator

karkhaz commented Sep 1, 2018

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

karkhaz added a commit to karkhaz/cbmc that referenced this issue Sep 1, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
5bfbba3 
The map of safe pointers are now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
karkhaz added a commit to karkhaz/cbmc that referenced this issue Sep 1, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
58db2a1 
The map of safe pointers are now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
@karkhaz karkhaz mentioned this issue Sep 1, 2018
Merged
@polgreen
Copy link
Contributor Author

polgreen commented Sep 1, 2018

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
Copy link
Collaborator

karkhaz commented Sep 1, 2018

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

karkhaz added a commit to karkhaz/cbmc that referenced this issue Sep 1, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
0c9f069 
The map of safe pointers is now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
@polgreen
Copy link
Contributor Author

polgreen commented Sep 1, 2018

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 added a commit to karkhaz/cbmc that referenced this issue Sep 1, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
a1c387e 
The map of safe pointers is now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
karkhaz added a commit to karkhaz/cbmc that referenced this issue Sep 1, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
1e867b6 
The map of safe pointers is now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
karkhaz added a commit to karkhaz/cbmc that referenced this issue Sep 1, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
bd42010 
The map of safe pointers is now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
@karkhaz
Copy link
Collaborator

karkhaz commented Sep 1, 2018

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

karkhaz added a commit to karkhaz/cbmc that referenced this issue Sep 1, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
bf1076f 
The map of safe pointers is now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
karkhaz added a commit to karkhaz/cbmc that referenced this issue Sep 3, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
122f0a9 
The map of safe pointers is now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
karkhaz added a commit to karkhaz/cbmc that referenced this issue Sep 3, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
959c7a5 
The map of safe pointers is now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
karkhaz added a commit to karkhaz/cbmc that referenced this issue Sep 16, 2018
@karkhaz
Bugfix: Maintain safe_pointers per-path
4690ea5 
The map of safe pointers is now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Bugfix: Maintain safe_pointers per-path karkhaz/cbmc
3 participants
@tautschnig @karkhaz @polgreen