Comments (7)
jklmnn
commented on September 28, 2024
-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).
from az3.
jklmnn
commented on September 28, 2024
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).
from az3.
jklmnn
commented on September 28, 2024
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.
from az3.
jklmnn
commented on September 28, 2024
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.
from az3.
senier
commented on September 28, 2024
Creating a separate test without AUnit is probably not worth the effort right now. We could suppress the leak instead.
from az3.
jklmnn
commented on September 28, 2024
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.
from az3.
jklmnn
commented on September 28, 2024
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.
from az3.
Related Issues (20)
- Update Z3 to 4.8.9 HOT 1
- Iterators HOT 1
- Create Int objects from strings for arbitrary large integers
- Support solvers with specific logics
- Support bit vector representation of integers HOT 1
- Use Ada.Interfaces instead of custom types HOT 1
- Implement push and pop API for Optimize HOT 1
- Fix CI HOT 2
- Update Z3 to current release HOT 2
- Support Real type
- Remove default context
- Splitting packages HOT 1
- Build separate library versions with and without asan
- Make Solver and Optimize constrained types
- Moving contexts HOT 3
- Proper equality check HOT 1
- Failing comparisons HOT 1
- Bind Optimize API HOT 6
- Proper reference counting
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from az3.