Opened 4 months ago

Closed 4 months ago

Last modified 4 months ago

#42 closed defect (invalid)

DIVINE sim crashes after only six states

Reported by: John Lång Owned by: mornfall
Priority: major Milestone: 5.0
Component: sim Keywords:
Cc:

Description (last modified by mornfall)

I'm using the static binary version 4.1.20+2018.12.17 of DIVINE. I'm trying to debug my program by running "divine sim", but it seems that it crashes after ony six steps. I've tried with four different programs and it seems to always happen the same way. Here's my latest output:

divine sim examples/ToyApplication/ToyApplication.bc 
No entry for terminal type "xterm-256color";
using dumb terminal settings.
    
           ^       —————.   —.—  .     .  —.—  .     .  .—————    .    .
          ———      |     |   |   |     |   |   |\    |  |         |    |
         —(o)—     |     |   |   |     |   |   |  \  |  |————     '————|
        ———————    |     |   |    \   /    |   |    \|  |              |
       —————————   —————'   —'—     '     —'—  '     '  '—————         '

Welcome to 'divine sim', an interactive debugger. Type 'help' to get started.
# executing __boot at /home/xrockai/src/divine/static/dios/sys/dios.cpp:156
> start
# a new program state was stored as #1
# active threads: [0:0]
T: FAULT: invalid pointer passed to __vm_obj_free
T: FAULT: invalid pointer passed to __vm_obj_free
T: FAULT: invalid pointer passed to __vm_obj_free
# a new program state was stored as #2
# active threads: [0:0]
# a new program state was stored as #3
# active threads: [0:0]
# a new program state was stored as #4
# active threads: [0:0]
# a new program state was stored as #5
# active threads: [0:0]
# a new program state was stored as #6
# active threads: [0:0]
T: (0) terminating with uncaught exception of type std::bad_alloc: std::bad_alloc
T: [0] FAULT: Uncaught signal.
T: [0] FATAL: control error in kernel
# executing __dios::FaultBase::fault_handler(int, _VM_Frame*, int)
#        at /home/xrockai/src/divine/static/dios/sys/fault.cpp:60
> backtrace
  __dios::FaultBase::fault_handler(int, _VM_Frame*, int)
     at /home/xrockai/src/divine/static/dios/sys/fault.cpp:60
  void __dios::FaultBase::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)())
     at /dios/include/dios/sys/fault.hpp:99
  __dios_fault at /dios/src/libc/sys/fault.c:14
  int {Scheduler}::_kill<{ProcMan}::kill(int, int)::'lambda'({Fault}*)>(int, int, {Fault})
     at /dios/include/dios/sys/scheduling.hpp:514
  {ProcMan}::kill(int, int) at /dios/include/dios/sys/procmanager.hpp:270
  {BaseContext}::SysEnter<{Context} >::kill(int, int)
     at /dios/include/sys/argpad.hpp:53
  kill at /dios/include/sys/argpad.hpp:53
  raise at /dios/src/libc/_PDCLIB/glue.c:125
  abort at /home/xrockai/src/divine/static/dios/libc/stdlib/abort.c:14
  abort_message
     at /home/xrockai/src/divine/static/dios/libcxxabi/src/abort_message.cpp:86
  default_terminate_handler() at /dios/src/libcxxabi/src/cxa_default_handlers.cpp:63
  std::__terminate(void (*)()) at /dios/src/libcxxabi/src/cxa_handlers.cpp:68
  std::terminate() at /dios/src/libcxxabi/src/cxa_handlers.cpp:99
  __clang_call_terminate at (unknown location)
  std::__2::locale::locale() at /dios/src/libcxx/src/locale.cpp:498
  std::__2::basic_streambuf<char, std::__2::char_traits<char> >::basic_streambuf()
     at /dios/include/libcxx/include/streambuf:227
  std::__2::__stdinbuf<char>::__stdinbuf(_PDCLIB_file*, _PDCLIB_mbstate*)
     at /dios/include/libcxx/include/__std_stream:44
  std::__2::ios_base::Init::Init() at /dios/src/libcxx/src/iostream.cpp:81
  _GLOBAL__sub_I_iostream.cpp at /dios/src/libcxx/src/iostream.cpp:76
  (anonymous namespace)::run_ctors_dtors(char const*, bool)
     at /dios/src/libc/sys/start.cpp:42
  __dios_run_ctors at /dios/src/libc/sys/start.cpp:62
  _start at /dios/src/libc/sys/start.cpp:76
# executing __dios::FaultBase::fault_handler(int, _VM_Frame*, int)
#        at /home/xrockai/src/divine/static/dios/sys/fault.cpp:60
> 

Change History (5)

comment:1 Changed 4 months ago by John Lång

I was trying to debug my ADAPRO WorkerModel? application. You can git clone the code from:

git@…:jllang/adapro.git

If you have all the requirements installed, the model should compile by running "make_divine_cc_worker_model" and after that "divine sim models/divine/WorkerModel.bc" at the project top directory.

comment:2 Changed 4 months ago by John Lång

Whoops, I meant "make divine_cc_worker_model". That's the name of my make target.

comment:3 Changed 4 months ago by John Lång

I created a trivial program:

int main(int argc, char argv)
{

return 0;

}

It seems that this problem is not reproducible with that one.

comment:4 Changed 4 months ago by mornfall

Description: modified (diff)
Resolution: invalid
Status: newclosed

This is not something we can really fix -- it is a genuine violation of the property you asked for. Basically, the question you pose is, 'can this program fail assuming memory might run out' and the answer is yes, it may fail in the above way, with an unhandled exception. Perhaps you mean to pass -o nofail:malloc, which would make this go away, because you then assume memory never runs out; alternately, you may want to say that you don't care about running out of memory in the constructors and you can set nofail:malloc using a high-priority constructor and reset it using a low-priority one (see also dios_configure_fault). Perhaps you do not consider an unhandled exception a problem: maybe use std::set_terminate with a handler that just calls vm_cancel in that case.

comment:5 Changed 4 months ago by mornfall

Milestone: future5.0

Milestone renamed

Note: See TracTickets for help on using tickets.