Opened 5 years ago

Closed 5 years ago

#93 closed defect (fixed)

Memory leak in stdio tracing code.

Reported by: Lukáš Zaoral Owned by: mornfall
Priority: major Milestone: 4.3
Component: DiOS Keywords:
Cc: kdudka@…, jamartis@…, lzaoral@…


Divine (both 4.3.6 and next) does not correctly simulate failures of malloc, fopen and related functions. Verifying following code with leak check turned on

#include <stdio.h>
#include <stdlib.h>

int main(void)
    void* ptr = malloc(5);
    if (ptr == NULL) {
        return EXIT_FAILURE;

    return EXIT_SUCCESS;

results in

$ divine verify --leakcheck exit malloc.c
compiling malloc.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 714.286                                                        
state count: 15
mips: 0.85

error found: yes
error trace: |
  [0] malloc: Success
  LEAK: weak* fbe0520f 0
  [0] FATAL: memory leak in userspace

active stack:
  - symbol: void __dios::FaultBase::handler<__dios::Upcall<__dios::fs::VFS<__dios::ProcessManager<__dios::Fault<__dios::Scheduler<__dios::Base> > > > > >(_VM_Fault, _VM_Frame*, void (*)())
    location: /dios/include/dios/sys/fault.hpp:118
  - symbol: __dios_fault
    location: /dios/src/arch/divm/fault.c:12
  - symbol: _exit
    location: /dios/src/libc/sys/start.cpp:61
  - symbol: _Exit
    location: /dios/src/libc/stdlib/_Exit.c:19
  - symbol: exit
    location: /dios/src/libc/stdlib/exit.c:6
  - symbol: __dios_start
    location: /dios/src/libc/sys/start.cpp:108
a report was written to

It seems, that the allocation itself is performed every time regardless of the failure simulation setting, because otherwise errno would have a non-zero value and no leaks would be reported. The case with fopen is similar.

Attachments (1) (7.5 KB) - added by Lukáš Zaoral 5 years ago.

Download all attachments as: .zip

Change History (3)

Changed 5 years ago by Lukáš Zaoral

Attachment: added

comment:1 Changed 5 years ago by mornfall

Owner: set to mornfall
Status: newaccepted

This appears to be unrelated to the malloc() call or anything else regarding failure simulation. The minimal reproducer for me is below. Both the 'return 1' and the '%d' in printf are required to reproduce, so I suspect a leak in the stdio code that is cleaned up upon a clean exit, but not on exit( 1 ).

#include <stdio.h>

int main()
    printf( "foobar: %d\n", 0 );
    return 1; /* ERROR */

comment:2 Changed 5 years ago by mornfall

Resolution: fixed
Status: acceptedclosed
Summary: Divine verify incorrectly simulates failuresMemory leak in stdio tracing code.

The problem was due to a memory leak in code that transcribes stdout/stderr writes into traces. Should be fixed in next.

Note: See TracTickets for help on using tickets.