Build with ASAN and check leaks

[senier]

Build z3 and our test suite with ASAN and enable resource leak checks:

   package Builder is                                                                                                   
      for Global_Compilation_Switches ("Ada") use ("-fsanitize=address", "-fno-omit-frame-pointer");      
   end Builder; 

   package Linker is                                                                                                    
      for Default_Switches ("Ada") use ("-lasan");                                                            
   end Linker; 

[jklmnn]

-lasan seems to be the wrong way, since it causes the following error message:

ASan runtime does not come first in initial library list; you should either link runtime to your application or manually preload it with LD_PRELOAD.

There is an issue about this (google/sanitizers#796) and as we're using GCC the correct linker flags are -fsanitize=address -static-libasan. This solution works for me.

As expected we leak memory:

==1798369==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 410 byte(s) in 202 object(s) allocated from:
    #0 0x4978df in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7f888bcf701e in __gnat_malloc (/.../AZ3/obj/tests/../../../..//opt/GNAT-Community-2021/lib/gcc/x86_64-pc-linux-gnu/10.3.1/adalib/libgnat-2021.so+0x30701e)

Direct leak of 104 byte(s) in 1 object(s) allocated from:
    #0 0x4978df in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7f888d5892d1 in memory::allocate(unsigned long) (/.../AZ3/obj/tests/../..//z3/z3/build/libz3.so+0x14952d1)

Indirect leak of 17200748 byte(s) in 454 object(s) allocated from:
    #0 0x4978df in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7f888d5892d1 in memory::allocate(unsigned long) (/.../AZ3/obj/tests/../..//z3/z3/build/libz3.so+0x14952d1)

Indirect leak of 3376 byte(s) in 14 object(s) allocated from:
    #0 0x4978df in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7f888d5892d1 in memory::allocate(unsigned long) (/.../AZ3/obj/tests/../..//z3/z3/build/libz3.so+0x14952d1)
    #2 0x60b000413ba7  (<unknown module>)

Indirect leak of 2864 byte(s) in 7 object(s) allocated from:
    #0 0x497c48 in __interceptor_realloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:164
    #1 0x7f888d58939a in memory::reallocate(void*, unsigned long) (/.../AZ3/obj/tests/../..//z3/z3/build/libz3.so+0x149539a)

Indirect leak of 1600 byte(s) in 20 object(s) allocated from:
    #0 0x4978df in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7f888bcf701e in __gnat_malloc (/.../AZ3/obj/tests/../../../..//opt/GNAT-Community-2021/lib/gcc/x86_64-pc-linux-gnu/10.3.1/adalib/libgnat-2021.so+0x30701e)
    #2 0x607000003e3f  (<unknown module>)

Indirect leak of 1600 byte(s) in 20 object(s) allocated from:
    #0 0x4978df in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7f888bcf701e in __gnat_malloc (/.../AZ3/obj/tests/../../../..//opt/GNAT-Community-2021/lib/gcc/x86_64-pc-linux-gnu/10.3.1/adalib/libgnat-2021.so+0x30701e)
    #2 0x607000094c8f  (<unknown module>)

Indirect leak of 496 byte(s) in 23 object(s) allocated from:
    #0 0x4978df in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7f888bcf701e in __gnat_malloc (/.../AZ3/obj/tests/../../../..//opt/GNAT-Community-2021/lib/gcc/x86_64-pc-linux-gnu/10.3.1/adalib/libgnat-2021.so+0x30701e)

Indirect leak of 22 byte(s) in 1 object(s) allocated from:
    #0 0x499097 in operator new(unsigned long) ../../../../src/libsanitizer/asan/asan_new_delete.cpp:99
    #1 0x7f888c3572e0 in smt_params::smt_params(params_ref const&) (/.../AZ3/obj/tests/../..//z3/z3/build/libz3.so+0x2632e0)

SUMMARY: AddressSanitizer: 17211220 byte(s) leaked in 742 allocation(s).

[jklmnn]

With z3 built with address sanitize we get the following result:

SUMMARY: AddressSanitizer: 17211220 byte(s) leaked in 742 allocation(s).

(I omitted the few hundred lines of traces).

[jklmnn]

The memory leaks come from 2 sources

• Non-freed strings when creating constants
• Z3 configurations and contexts have to be deleted explicitly

The non-freed memory has been fixed. To solve the memory issues caused by contexts and configs these types have to be implemented as controlled types. As controlled types seem to be difficult to use as constants if defined in the same package (since the body of Finalize needs to be seen) we decided to not provide a default context anymore.

[jklmnn]

I'm relatively confident that we now have a working implementation. There are no further memory leaks in z3. However there are still some calls to __gnat_malloc that leak memory. I have the suspicion that these come from AUnit. Running a single empty test already leaks memory. Also I have a separate (small) test that does some operations on the context and expressions and that doesn't leak any memory. I guess we have to implement some separate test to check for memory leaks.

[senier]

Creating a separate test without AUnit is probably not worth the effort right now. We could suppress the leak instead.

[jklmnn]

The following 3 leaks happen even with empty tests:

==745382==ERROR: LeakSanitizer: detected memory leaks

Indirect leak of 1520 byte(s) in 19 object(s) allocated from:
    #0 0x49821f in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7fc7a656c01e in __gnat_malloc (/.../AZ3/obj/tests/../../../..//opt/GNAT-Community-2021/lib/gcc/x86_64-pc-linux-gnu/10.3.1/adalib/libgnat-2021.so+0x30701e)
    #2 0x607000004f4f  (<unknown module>)

Indirect leak of 1520 byte(s) in 19 object(s) allocated from:
    #0 0x49821f in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7fc7a656c01e in __gnat_malloc (/.../AZ3/obj/tests/../../../..//opt/GNAT-Community-2021/lib/gcc/x86_64-pc-linux-gnu/10.3.1/adalib/libgnat-2021.so+0x30701e)
    #2 0x607000003e3f  (<unknown module>)

Indirect leak of 480 byte(s) in 22 object(s) allocated from:
    #0 0x49821f in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7fc7a656c01e in __gnat_malloc (/.../AZ3/obj/tests/../../../..//opt/GNAT-Community-2021/lib/gcc/x86_64-pc-linux-gnu/10.3.1/adalib/libgnat-2021.so+0x30701e)

SUMMARY: AddressSanitizer: 3520 byte(s) leaked in 60 allocation(s).

The 4th leak seems to happen in Optimize.Set_Timeout:

Direct leak of 8 byte(s) in 1 object(s) allocated from:      
    #0 0x49821f in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x7f77d66cb01e in __gnat_malloc (/.../AZ3/obj/tests/../../../..//opt/GNAT-Community-2021/lib/gcc/x86_64-pc-linux-gnu/10.3.1/adalib/libgnat-2021.so+0x30701e)

I looked into supressing the Aunit leaks. The problem is we can only suppress leaks by symbol, source or binary name. In this exact case the only information we have is that it happens in libgnat.so in __gnat_malloc. If we suppress this we will miss all memory leaks from Ada. The best method to distinguish between Aunit leaks and our leaks I have is that Aunit leaks all seem to be indirect leaks while ours are direct leaks. However Asan doesn't provide any useful tool to suppress only indirect leaks (see google/sanitizers#1250). Turning off all leaks that include __gnat_malloc will force us to check for directl leaks manually every time we change something which completely defeats the purpose of adding it to the tests and CI in the first place.

[jklmnn]

Result of a separate discussion: Let's try to use AUnit as a submodule and build it from sources with asan and debug symbols enabled. If all of the remaining leaks can be traced back to AUnit either suppress or fix them.