Skip to content

Memory error when org.cprover.jar is on the classpath #850

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
reuk opened this issue Apr 20, 2017 · 1 comment
Closed

Memory error when org.cprover.jar is on the classpath #850

reuk opened this issue Apr 20, 2017 · 1 comment

Comments

@reuk
Copy link
Contributor

reuk commented Apr 20, 2017 •
edited
Loading

With 7cbe566 built with ASan, analysing the following program while org.cprover.jar is on the classpath results in a memory error. It looks like I made a mistake with the nondet support somewhere. This blocks the java library modelling, as org.cprover.jar should probably be built into the java library.

cmdline:

cbmc NondetLazy.class --classpath ../../../src/org.cprover.jar:.

program:

import org.cprover.CProver;

public class NondetLazy
{
  class Foo
  {
    int bar;
  }

  static Foo go()
  {
    return CProver.nondetWithoutNull();
  }

  public static void main()
  {
    assert go() != null;
  }
}

output:

CBMC version 5.7 64-bit x86_64 linux
Parsing NondetLazy.class
Java main class: NondetLazy
read class file org/cprover/CProver.class from ../../../src/org.cprover.jar
failed to load class `java.lang.AssertionError'
failed to load class `java.lang.Object'
failed to load class `java.lang.RuntimeException'
failed to load class `java.lang.String'
failed to load class `java.lang.Class'
Converting
Generating GOTO Program
Adding goto-destructor code on jump to pc20
Adding goto-destructor code on jump to pc12
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
=================================================================
==25311==ERROR: AddressSanitizer: heap-use-after-free on address 0x60f000001378 at pc 0x00000075595d bp 0x7ffcfb8da2f0 sp 0x7ffcfb8da2e8
READ of size 8 at 0x60f000001378 thread T0
    #0 0x75595c in std::_Rb_tree<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_Identity<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, std::less<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, std::allocator<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> > >::_M_begin() /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:652:64
    #1 0x885535 in std::_Rb_tree<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_Identity<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, std::less<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, std::allocator<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> > >::_M_get_insert_unique_pos(std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> const&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:1804:24
    #2 0x88476e in std::pair<std::_Rb_tree_iterator<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, bool> std::_Rb_tree<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_Identity<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, std::less<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, std::allocator<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> > >::_M_insert_unique<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> const&>(std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> const&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:1863:4
    #3 0x88216e in std::set<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::less<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, std::allocator<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> > >::insert(std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> const&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_set.h:485:4
    #4 0x87ef33 in goto_program_templatet<codet, exprt>::compute_incoming_edges() /home/reuben/development/cbmc/src/goto-instrument/../goto-programs/goto_program_template.h:762:9
    #5 0x257d3ab in goto_program_templatet<codet, exprt>::update() /home/reuben/development/cbmc/src/goto-programs/./goto_program_template.h:620:3
    #6 0x2a68f95 in check_and_replace_target(goto_programt&, std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont> const&) /home/reuben/development/cbmc/src/goto-programs/replace_java_nondet.cpp:279:3
    #7 0x2a665f4 in replace_java_nondet(goto_programt&) /home/reuben/development/cbmc/src/goto-programs/replace_java_nondet.cpp:304:26
    #8 0x2a65e72 in replace_java_nondet(goto_functionst&) /home/reuben/development/cbmc/src/goto-programs/replace_java_nondet.cpp:316:5
    #9 0x100c1f9 in cbmc_parse_optionst::process_goto_program(optionst const&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:935:5
    #10 0x10061b8 in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:752:8
    #11 0xff7bb0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:549:5
    #12 0x3924be0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #13 0xfcb0e1 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #14 0x7fc709fdc82f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291
    #15 0x484038 in _start (/home/reuben/development/cbmc/src/cbmc/cbmc+0x484038)

0x60f000001378 is located 120 bytes inside of 168-byte region [0x60f000001300,0x60f0000013a8)
freed by thread T0 here:
    #0 0x555d30 in operator delete(void*) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x555d30)
    #1 0x757adb in __gnu_cxx::new_allocator<std::_List_node<goto_program_templatet<codet, exprt>::instructiont> >::deallocate(std::_List_node<goto_program_templatet<codet, exprt>::instructiont>*, unsigned long) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/ext/new_allocator.h:110:9
    #2 0x754f86 in std::__cxx11::_List_base<goto_program_templatet<codet, exprt>::instructiont, std::allocator<goto_program_templatet<codet, exprt>::instructiont> >::_M_put_node(std::_List_node<goto_program_templatet<codet, exprt>::instructiont>*) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_list.h:396:9
    #3 0x772109 in std::__cxx11::list<goto_program_templatet<codet, exprt>::instructiont, std::allocator<goto_program_templatet<codet, exprt>::instructiont> >::_M_erase(std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_list.h:1781:9
    #4 0x25ae7c2 in std::__cxx11::list<goto_program_templatet<codet, exprt>::instructiont, std::allocator<goto_program_templatet<codet, exprt>::instructiont> >::erase(std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont>) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/list.tcc:156:7
    #5 0x2a6e7a3 in std::__cxx11::list<goto_program_templatet<codet, exprt>::instructiont, std::allocator<goto_program_templatet<codet, exprt>::instructiont> >::erase(std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont>) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_list.h:1330:14
    #6 0x2a68260 in check_and_replace_target(goto_programt&, std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont> const&) /home/reuben/development/cbmc/src/goto-programs/replace_java_nondet.cpp:266:27
    #7 0x2a665f4 in replace_java_nondet(goto_programt&) /home/reuben/development/cbmc/src/goto-programs/replace_java_nondet.cpp:304:26
    #8 0x2a65e72 in replace_java_nondet(goto_functionst&) /home/reuben/development/cbmc/src/goto-programs/replace_java_nondet.cpp:316:5
    #9 0x100c1f9 in cbmc_parse_optionst::process_goto_program(optionst const&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:935:5
    #10 0x10061b8 in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:752:8
    #11 0xff7bb0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:549:5
    #12 0x3924be0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #13 0xfcb0e1 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #14 0x7fc709fdc82f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

previously allocated by thread T0 here:
    #0 0x555730 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x555730)
    #1 0x765306 in __gnu_cxx::new_allocator<std::_List_node<goto_program_templatet<codet, exprt>::instructiont> >::allocate(unsigned long, void const*) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/ext/new_allocator.h:104:27
    #2 0x765112 in std::__cxx11::_List_base<goto_program_templatet<codet, exprt>::instructiont, std::allocator<goto_program_templatet<codet, exprt>::instructiont> >::_M_get_node() /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_list.h:392:16
    #3 0x764a8e in std::_List_node<goto_program_templatet<codet, exprt>::instructiont>* std::__cxx11::list<goto_program_templatet<codet, exprt>::instructiont, std::allocator<goto_program_templatet<codet, exprt>::instructiont> >::_M_create_node<goto_program_templatet<codet, exprt>::instructiont>(goto_program_templatet<codet, exprt>::instructiont&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_list.h:571:17
    #4 0x764738 in void std::__cxx11::list<goto_program_templatet<codet, exprt>::instructiont, std::allocator<goto_program_templatet<codet, exprt>::instructiont> >::_M_insert<goto_program_templatet<codet, exprt>::instructiont>(std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, goto_program_templatet<codet, exprt>::instructiont&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_list.h:1763:18
    #5 0x763907 in std::__cxx11::list<goto_program_templatet<codet, exprt>::instructiont, std::allocator<goto_program_templatet<codet, exprt>::instructiont> >::push_back(goto_program_templatet<codet, exprt>::instructiont&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_list.h:1094:9
    #6 0x74b06e in goto_program_templatet<codet, exprt>::add_instruction(goto_program_instruction_typet) /home/reuben/development/cbmc/src/pointer-analysis/../goto-programs/goto_program_template.h:414:5
    #7 0x2a8efbe in goto_convertt::copy(codet const&, goto_program_instruction_typet, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:405:28
    #8 0x26a244e in goto_convertt::do_function_call_symbol(exprt const&, symbol_exprt const&, std::vector<exprt, std::allocator<exprt> > const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/builtin_functions.cpp:2054:5
    #9 0x2b24123 in goto_convertt::do_function_call(exprt const&, exprt const&, std::vector<exprt, std::allocator<exprt> > const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_function_call.cpp:92:5
    #10 0x2b22560 in goto_convertt::convert_function_call(code_function_callt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_function_call.cpp:37:3
    #11 0x2a818d4 in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:607:5
    #12 0x2a965c7 in goto_convertt::convert_block(code_blockt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:742:5
    #13 0x2a7ff28 in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:591:5
    #14 0x2a965c7 in goto_convertt::convert_block(code_blockt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:742:5
    #15 0x2a7ff28 in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:591:5
    #16 0x2a90e8a in goto_convertt::convert_label(code_labelt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:448:5
    #17 0x2a81c21 in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:609:5
    #18 0x2a965c7 in goto_convertt::convert_block(code_blockt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:742:5
    #19 0x2a7ff28 in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:591:5
    #20 0x2a7f183 in goto_convertt::goto_convert_rec(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:380:3
    #21 0x25c2472 in goto_convert_functionst::convert_function(dstringt const&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:256:3
    #22 0x25be319 in goto_convert_functionst::goto_convert() /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:91:5
    #23 0x25c7d4d in goto_convert(symbol_tablet&, goto_functionst&, message_handlert&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:338:5
    #24 0x1005f7f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:750:5
    #25 0xff7bb0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:549:5
    #26 0x3924be0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #27 0xfcb0e1 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #28 0x7fc709fdc82f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

SUMMARY: AddressSanitizer: heap-use-after-free /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:652:64 in std::_Rb_tree<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_Identity<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, std::less<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> >, std::allocator<std::_List_iterator<goto_program_templatet<codet, exprt>::instructiont> > >::_M_begin()
Shadow bytes around the buggy address:
  0x0c1e7fff8210: fd fd fd fd fd fd fd fd fd fd fd fa fa fa fa fa
  0x0c1e7fff8220: fa fa fa fa fd fd fd fd fd fd fd fd fd fd fd fd
  0x0c1e7fff8230: fd fd fd fd fd fd fd fd fd fa fa fa fa fa fa fa
  0x0c1e7fff8240: fa fa fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x0c1e7fff8250: fd fd fd fd fd fd fd fa fa fa fa fa fa fa fa fa
=>0x0c1e7fff8260: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd[fd]
  0x0c1e7fff8270: fd fd fd fd fd fa fa fa fa fa fa fa fa fa 00 00
  0x0c1e7fff8280: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c1e7fff8290: 00 00 00 fa fa fa fa fa fa fa fa fa 00 00 00 00
  0x0c1e7fff82a0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c1e7fff82b0: 00 fa fa fa fa fa fa fa fa fa 00 00 00 00 00 00
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07
  Heap left redzone:       fa
  Heap right redzone:      fb
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack partial redzone:   f4
  Stack after return:      f5
  Stack use after scope:   f8
  Global redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Container overflow:      fc
  Array cookie:            ac
  Intra object redzone:    bb
  ASan internal:           fe
  Left alloca redzone:     ca
  Right alloca redzone:    cb
==25311==ABORTING
@reuk reuk mentioned this issue Apr 24, 2017
Merged
forejtv added a commit that referenced this issue Apr 27, 2017
@forejtv
Merge pull request #860 from reuk/nondet-memory-fix
d117475 
Remove 'erase' in replace_java_nondet.cpp, fixes #850
@tautschnig
Copy link
Collaborator

Fixed via #860.

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

No branches or pull requests
2 participants
@tautschnig @reuk