[ASan] Potential leak when running C examples.

[delcypher]

As part of my work in PR #1289 I've been running ASan. ASan includes the "LeakSanitizer" which checks for memory leaks on program exit.

The LeakSanitizer currently reports the following leaks when running the C API examples.

I say potential leaks because I don't really understand them.

=================================================================
==141==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 513 byte(s) in 1 object(s) allocated from:
    #0 0x5086a0 in operator new(unsigned long) (/home/user/z3_build/examples/c_example_build_dir/c_example+0x5086a0)
    #1 0x7fffdedff87c in std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::reserve(unsigned long) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x11f87c)
    #2 0x7fffefdce0ce in _fini (/home/user/z3_build/libz3.so.4.5+0x10d6c0ce)

I believe _fini is an automatically generated function that calls various destructors. It seems a string is being allocated that the LeakSanitizer doesn't see deallocated. We don't control this generated code so I'm not sure what's going on here.

Direct leak of 168 byte(s) in 1 object(s) allocated from:
    #0 0x4d0838 in __interceptor_malloc (/home/user/z3_build/examples/c_example_build_dir/c_example+0x4d0838)
    #1 0x7fffded6c41f in __cxa_allocate_exception (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x8c41f)
    #2 0x7fffe7adf72c in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) /home/user/z3_src/src/ast/ast.cpp:2142:13
    #3 0x7fffe7ad510a in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) /home/user/z3_src/src/ast/ast.cpp:2237:13
    #4 0x7fffe7ad28a2 in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) /home/user/z3_src/src/ast/ast.cpp:1908:16
    #5 0x7fffefad8b37 in Z3_mk_iff /home/user/z3_src/src/api/api_ast.cpp:193:5
    #6 0x512b5a in error_code_example2 /home/user/z3_src/examples/c/test_capi.c:1613:15
    #7 0x520b6f in main /home/user/z3_src/examples/c/test_capi.c:2855:5
    #8 0x7fffdddee82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)

Indirect leak of 96 byte(s) in 1 object(s) allocated from:
    #0 0x5086a0 in operator new(unsigned long) (/home/user/z3_build/examples/c_example_build_dir/c_example+0x5086a0)
    #1 0x7fffef418fa4 in void std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::_M_construct<char*>(char*, char*, std::forward_iterator_tag) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/basic_string.tcc:223:14
    #2 0x7fffdee019ce in std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::basic_string(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x1219ce)
    #3 0x7fffe7b2d5f6 in ast_exception::ast_exception(char const*) /home/user/z3_src/src/ast/ast.h:66:37
    #4 0x7fffe7ae1cc7 in ast_manager::check_args(func_decl*, unsigned int, expr* const*) /home/user/z3_src/src/ast/ast.cpp:2181:19
    #5 0x7fffe7adf72c in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) /home/user/z3_src/src/ast/ast.cpp:2142:13
    #6 0x7fffe7ad510a in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) /home/user/z3_src/src/ast/ast.cpp:2237:13
    #7 0x7fffe7ad28a2 in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) /home/user/z3_src/src/ast/ast.cpp:1908:16
    #8 0x7fffefad8b37 in Z3_mk_iff /home/user/z3_src/src/api/api_ast.cpp:193:5
    #9 0x512b5a in error_code_example2 /home/user/z3_src/examples/c/test_capi.c:1613:15
    #10 0x520b6f in main /home/user/z3_src/examples/c/test_capi.c:2855:5
    #11 0x7fffdddee82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)

SUMMARY: AddressSanitizer: 777 byte(s) leaked in 3 allocation(s).

These two leaks are related. It looks like an exception is being leaked and that leaked exception itself allocates an std::string. I don't understand why the exception is being leaked. At a glance (there are rather a lot of macros) it looks like the exception ought to be caught ( I need to double check this though).

We are right on the C/C++ boundary in Z3_mk_iff so I wonder if there's a bug where Clang doesn't generate the right clean up code.

[delcypher]

To aid debugging for the _fini issue, here's the stack trace (different execution) when in the _fini function in libz3.

#0  0x00007fffefd9e9c0 in _fini () from /home/user/z3_build/libz3.so.4.5
#1  0x00007ffff7de7e05 in _dl_fini () at dl-fini.c:240
#2  0x00007fffdde07ff8 in __run_exit_handlers (status=0, listp=0x7fffde1925f8 <__exit_funcs>, run_list_atexit=run_list_atexit@entry=true) at exit.c:82
#3  0x00007fffdde08045 in __GI_exit (status=<optimized out>) at exit.c:104
#4  0x00007fffdddee837 in __libc_start_main (main=0x520af0 <main>, argc=1, argv=0x7fffffffe1f8, init=<optimized out>, fini=<optimized out>, rtld_fini=<optimized out>,
    stack_end=0x7fffffffe1e8) at ../csu/libc-start.c:325
#5  0x000000000041d539 in _start ()

Something weird is going on because the _fini function in libz3 doesn't do anything (other than adjust the %rsp) register, so the LeakSanitizer stack trace must be wrong.

0x7fffefd9e9c0 <_fini>          sub    $0x8,%rsp                                                                                                                                         
0x7fffefd9e9c4 <_fini+4>        add    $0x8,%rsp                                                                                                                                         
0x7fffefd9e9c8 <_fini+8>        retq 

[delcypher]

@NikolajBjorner With regards to the _fini leak. I think there's a bug in LSan's stack walking code. If I set ASAN_OPTIONS="${ASAN_OPTIONS},fast_unwind_on_malloc=0" (environment variables) a different (slower) method is used for recording stacks and I get this instead.

Direct leak of 513 byte(s) in 1 object(s) allocated from:
    #0 0x4d0458 in __interceptor_malloc (/home/user/z3_build/examples/c_example_build_dir/c_example+0x4d0458)
    #1 0x7ffff250ee77 in operator new(unsigned long) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x8de77)
    #2 0x7ffff25a087c in std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::reserve(unsigned long) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x11f87c)
    #3 0x7ffff2594cd4 in std::__cxx11::basic_stringbuf<char, std::char_traits<char>, std::allocator<char> >::overflow(int) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x113cd4)
    #4 0x7ffff259ee78 in std::basic_streambuf<char, std::char_traits<char> >::xsputn(char const*, long) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x11de78)
    #5 0x7ffff258fec5 in std::basic_ostream<char, std::char_traits<char> >& std::__ostream_insert<char, std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*, long) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x10eec5)
    #6 0x7ffff2590236 in std::basic_ostream<char, std::char_traits<char> >& std::operator<< <std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x10f236)
    #7 0x7ffff6a4284b in smtparser::error_prefix(proto_expr*) /home/user/z3_src/src/parsers/smt/smtparser.cpp:805:23
    #8 0x7ffff6a451ff in void smtparser::set_error<char const*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, char const*>(char const*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, char const*, proto_expr*) /home/user/z3_src/src/parsers/smt/smtparser.cpp:830:9
    #9 0x7ffff6a43c7b in smtparser::make_sort(proto_expr*, obj_ref<sort, ast_manager>&) /home/user/z3_src/src/parsers/smt/smtparser.cpp:1700:17
    #10 0x7ffff6a4c5f2 in smtparser::declare_fun(proto_expr*) /home/user/z3_src/src/parsers/smt/smtparser.cpp:2062:14
    #11 0x7ffff6a32ed1 in smtparser::declare_funs(proto_expr*) /home/user/z3_src/src/parsers/smt/smtparser.cpp:1898:18
    #12 0x7ffff6a2c7e4 in smtparser::make_benchmark(symbol&, proto_expr* const*) /home/user/z3_src/src/parsers/smt/smtparser.cpp:975:22
    #13 0x7ffff6a27cbc in smtparser::parse(proto_expr_parser&) /home/user/z3_src/src/parsers/smt/smtparser.cpp:786:26
    #14 0x7ffff6a2764c in smtparser::parse_stream(std::istream&) /home/user/z3_src/src/parsers/smt/smtparser.cpp:649:16
    #15 0x7ffff6a24756 in smtparser::parse_string(char const*) /home/user/z3_src/src/parsers/smt/smtparser.cpp:669:16
    #16 0x7ffff6b7e8dc in Z3_parse_smtlib_string /home/user/z3_src/src/api/api_parsers.cpp:66:44
    #17 0x50f195 in parser_example5 /home/user/z3_src/examples/c/test_capi.c:1796:9
    #18 0x518de8 in main /home/user/z3_src/examples/c/test_capi.c:2860:5
    #19 0x7ffff282382f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #20 0x41d158 in _start (/home/user/z3_build/examples/c_example_build_dir/c_example+0x41d158)

Does the above look like a leak to you?

[NikolajBjorner]

At first it did not look like a leak, but let's see:

• The memory is allocated inside the methods that print to a stream.
• The stream object is a local variable inside of parse_smtlib_string in api_parsers.
• When there is an error, which is the case here, a string is extracted from the buffer and stored in an error buffer (std::string).
• This gets printed.
  The reported leak is for some facility that extends a stream buffer (std::ostringstream).

The particular behavior of C callers in the c_example is that they set a longjump when an error is set inside the API methods. So this could explain the phenomenon: the destructor on the stack allocated ostringstream is not called and therefore the memory on that object is leaked.

I have added a commit that calls clear on the buffer object. I haven't reviewed the semantics of clear, but assuming it may free up memory. Could you try it out?

[delcypher]

@NikolajBjorner Unfortunately the leak is still reported.

Calling clear() is the wrong thing to do here because that just clears the error flags on the stream.

You could change the underlying storage by doing

outs.str("");

Such a fix seems a bit fragile though. Perhaps the std::ostringstream should be heap allocated so you can deallocate it (and there by call the destructor) before calling the user defined error handler?

This still doesn't seem like a great fix. Any stack allocated data and clean up might not get called in any of Z3's API functions if the error handler is allowed to use longjmp. In fact I think the other leaks that I've seen (and suppressed) are likely related to this. In these leaks exceptions (look for __cxa_allocate_exception) and are allocated but don't get deallocated like they should.

Perhaps we should document that longjmp should be avoided in error handlers and that its use might leave Z3 in an unspecified state? Then we could change the C API example to not use longjmp.

[NikolajBjorner]

Thanks, I have to say it makes sense. There are other places that are broken wrt longjump. Other APIs use the error codes. Documentation has not yet been updated.

[delcypher]

@NikolajBjorner Thanks for the fixes. The memory leaks are all gone now :)

Would you like me to submit a PR to update Z3's documentation?

[NikolajBjorner]

I would say you can hold off for now: I am not sure what is appropriate for the documentation and it may be a fringe thing given that the C-API really should not be used in mainstream.
I will be trying to harden the API so that it works also with longjumps. The test_capi example could now use longjumps as it is, except that it may not be advisable as other bugs may be uncovered.