Skip to content

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

Closed
@reuk

Description

@reuk

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions