DIVINE sim crashes after only six states

[John Lång]

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
> 

[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.

[John Lång]

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

[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.

[mornfall]

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.