Divine produces unusable memory leak reports

[Kamil Dudka]

% divine check test-0010.c 
compiling test-0010.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 48.6111                                                        
state count: 7
mips: 0.051
error found: no
a report was written to test-0010.report

% divine verify -o nofail:malloc test-0010.c              
compiling test-0010.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 67.9612                                                        
state count: 7
mips: 0.071
error found: no
a report was written to test-0010.report

% gcc -g test-0010.c && valgrind --leak-check=full ./a.out
==30421== Memcheck, a memory error detector
==30421== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==30421== Using Valgrind-3.15.0 and LibVEX; rerun with -h for copyright info
==30421== Command: ./a.out
==30421== 
==30421== 
==30421== HEAP SUMMARY:
==30421==     in use at exit: 80 bytes in 10 blocks
==30421==   total heap usage: 13 allocs, 3 frees, 104 bytes allocated
==30421== 
==30421== 8 bytes in 1 blocks are definitely lost in loss record 9 of 10
==30421==    at 0x483880B: malloc (vg_replace_malloc.c:309)
==30421==    by 0x40115B: create_item (test-0010.c:13)
==30421==    by 0x4011BB: insert_item (test-0010.c:28)
==30421==    by 0x40127F: main (test-0010.c:59)
==30421== 
==30421== 72 (8 direct, 64 indirect) bytes in 1 blocks are definitely lost in loss record 10 of 10
==30421==    at 0x483880B: malloc (vg_replace_malloc.c:309)
==30421==    by 0x40115B: create_item (test-0010.c:13)
==30421==    by 0x4011BB: insert_item (test-0010.c:28)
==30421==    by 0x401303: main (test-0010.c:72)
==30421== 
==30421== LEAK SUMMARY:
==30421==    definitely lost: 16 bytes in 2 blocks
==30421==    indirectly lost: 64 bytes in 8 blocks
==30421==      possibly lost: 0 bytes in 0 blocks
==30421==    still reachable: 0 bytes in 0 blocks
==30421==         suppressed: 0 bytes in 0 blocks
==30421== 
==30421== For lists of detected and suppressed errors, rerun with: -s
==30421== ERROR SUMMARY: 2 errors from 2 contexts (suppressed: 0 from 0)

[Kamil Dudka]

test-0010.c

[Kamil Dudka]

As suggested by Lukáš Zaoral, I tried running divine with --leakcheck exit and it reported that some memory leaked on exit. But this does not tell the user where in the source code the memory is leaked.

Is there any option of divine to get a report similar to the one provided by valgrind?

[mornfall]

Yes, you need to enable leak checking to get leak reports. Improvements in the report output are possible with: --leakcheck return instead of exit (may catch the leak earlier) and --autotrace allocs or even --autotrace allocs,calls for some basic origin information. For a more user-friendly and comprehensive solution, see ticket #35.

[Kamil Dudka]

Thank you for replying! I tried --leakcheck return --autotrace allocs,calls to no avail:

% divine check --leakcheck return --autotrace allocs,calls test-0010.c
compiling test-0010.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 95.2381                                                        
state count: 2
mips: 0.41

error found: yes
error trace: |
  (0) call __dios_start: 0, 1, 0xdc52d5c200000000, 0xa181d00500000000
  (0)   call __lart_globals_initialize
  (0)   call __pthread_initialize
  (0)     call __dios::__init_thread(__dios_tls*, int): 0x7ed15df800000000, 1
  (0)       call _PThread::operator new(unsigned long): 40
  (0)         allocated 0x8b4d085a00000000 in _ZN8_PThreadnwEm
  (0)       call memset: 0x8b4d085a00000000, 0, 40
  (0)     call __dios::getThread()
  (0)     call __dios::getThread()
  (0)   call __dios_call_global_ctors
  (0)     call __tainted_init()
  (0)     call init_stdio
  (0)       call mtx_init: 0x20f00000010, 1
  (0)         call pthread_mutexattr_init: 0x1b4266e00000000
  (0)         call pthread_mutexattr_settype: 0x1b4266e00000000, 1
  (0)         call pthread_mutex_init: 0x20f00000010, 0x1b4266e00000000
  (0)           call memset: 0x20f0000001c, 0, 28
  (0)         call pthread_mutexattr_destroy: 0x1b4266e00000000
  (0)       call mtx_init: 0x21100000010, 1
  (0)         call pthread_mutexattr_init: 0xd59863e00000000
  (0)         call pthread_mutexattr_settype: 0xd59863e00000000, 1
  (0)         call pthread_mutex_init: 0x21100000010, 0xd59863e00000000
  (0)           call memset: 0x2110000001c, 0, 28
  (0)         call pthread_mutexattr_destroy: 0xd59863e00000000
  (0)       call mtx_init: 0x21300000010, 1
  (0)         call pthread_mutexattr_init: 0x9199ce900000000
  (0)         call pthread_mutexattr_settype: 0x9199ce900000000, 1
  (0)         call pthread_mutex_init: 0x21300000010, 0x9199ce900000000
  (0)           call memset: 0x2130000001c, 0, 28
  (0)         call pthread_mutexattr_destroy: 0x9199ce900000000
  (0)   call main
  (0)     call create_item: 0
  (0)       call malloc: 8
  (0)         allocated 0x75086c9600000000 in malloc
  (0)     call destroy_cyclic_sll: 0xadf23e00000000
  (0)       call free: 0x75086c9600000000
  (0)         call __dios_check_free: 0x75086c9600000000
  (0)         deleted 0x75086c9600000000 in free
  (0)     call destroy_cyclic_sll: 0xadf23e00000000
  (0)     call insert_item: 0xadf23e00000000
  (0)       call create_item: 0
  (0)         call malloc: 8
  (0)           allocated 0x45185cf800000000 in malloc
  (0)     call insert_item: 0xadf23e00000000
  (0)       call create_item: 0x45185cf800000000
  (0)         call malloc: 8
  (0)           allocated 0x751ad01c00000000 in malloc
  (0)     call destroy_cyclic_sll: 0xadf23e00000000
  (0)       call free: 0x45185cf800000000
  (0)         call __dios_check_free: 0x45185cf800000000
  (0)         deleted 0x45185cf800000000 in free
  (0)     call void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)()): 5, 0xc0ebf84500000000, 0x8000100000012
  FAULT: object heap* 751ad01c 0 leaked
  [0]       FATAL: memory leak in userspace

active stack:
  - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)())
    location: /opt/divine/include/dios/sys/fault.hpp:115
  - symbol: main
    location: test-0010.c:60
  - symbol: __dios_start
    location: /opt/divine/include/dios/libc/sys/start.cpp:89
a report was written to test-0010.report

So what is the recommended way to make divine report memory leaks usefully?

[mornfall]

The relevant part of the trace (i.e. the origin of the allocation):

  (0)     call insert_item: 0xadf23e00000000
  (0)       call create_item: 0x45185cf800000000
  (0)         call malloc: 8
  (0)           allocated 0x751ad01c00000000 in malloc

What I usually do is grep through an --autotrace for the identifier of the leaked object.

[Kamil Dudka]

This output could be useful for developers of Divine itself but it is hardly useful for users of Divine. It does not provide any reference to the source code. Even if it did, it does not provide any information that the programmer would not know already. There is only one call to malloc() in the whole program, so it is not surprising that the leak is caused by the call to malloc(). The programmer may figure it out without using Divine at all. It would be much more useful if Divine told the user _where_ the memory is leaked.

To be clear, I expect to get output like this for the attached program:

Error: DIVINE_WARNING:
test-0010.c:49:9: warning: memory leak detected while destroying a heap object
test-0010.c:60:5: note: from call of destroy_cyclic_sll()
test-0010.c:54:5: note: from call of main()

Error: DIVINE_WARNING:
test-0010.c:49:9: warning: memory leak detected while destroying a heap object
test-0010.c:74:9: note: from call of destroy_cyclic_sll()
test-0010.c:54:5: note: from call of main()

[Kamil Dudka]

I am reopening this ticket because Divine's output format for reporting leaked memory is still unusable. How could one make Divine report memory leaks in a format similar to the example shown in comment:6?

We are able to to transform the output format as long as the needed information is contained in Divine's output. But this is apparently not the case.

[mornfall]

Improvements in leak reporting fall under #35 and related tickets. As for precision of the stack trace: your case is probably imprecise because destroy_cyclic_sll keeps references to the leaked object in registers. You did get the test-0010.c:60 location in the backtrace, only test-0010.c:49 is missing (because at that point, the object is probably still technically reachable... if this is your concern, then I suggest that you open a separate ticket -- perhaps discarding dead registers might discover the leak one step earlier).

And please keep inflammatory language out of the issue tracker.

[Kamil Dudka]

As I understand it, --leakcheck return makes Divine report a warning whenever there is allocated but unreachable memory when returning from a function. test.c:60 is source code location where the function was called. The attached example is simple but imagine a function with body consisting of 1024 lines (yes, this is common in practice). How would the user know where the memory is leaked?

I would expect Divine to tell me which variable contained the last reference to the allocated memory and the exact location in source code where the last reference was lost, including the backtrace.

[Vladimír Štill]

Well backtraces are again related to #35/#34. We know that large functions exist. The granularity is a matter of tuning performance versus precision (it would be easy to run leach check after each store, but that would probably slow DIVINE down a lot). But I think origin tracking is higher priority.

[Kamil Dudka]

I do not know how Divine represents program states but it sounds like your check for memory leaks is expensive because it operates on the global program state. If it checked just the part of the program state that is actually modified by the currently examined program instruction, it would be possible to run it for each instruction, yet in some cases it would still be cheaper than running it on the global state each time you return from a function. Note that memory leaks are not limited to store instructions. They can be triggered, for example, by calling free().