search

ahumenberger / Z3.jl

Julia interface to Z3
MIT License
57 stars 7 forks source link

Segfault with jemalloc #28

Open remysucre opened 5 months ago

remysucre commented 5 months ago

When using LD_PRELOAD to use jemalloc as the memory allocator, Z3 calls malloc_usable_size from glibc instead of jemalloc, triggering a segfault. To reproduce on linux, run LD_PRELOAD=$JEMALLOC_LIB julia --project where $JEMALLOC_LIB is the path to jemalloc, then run the following in the REPL: 

malloc_usable_size(ptr::Ptr{Cvoid}) = ccall(:malloc_usable_size, Csize_t, (Ptr{Cvoid},), ptr)
ptr = ccall(:malloc, Ptr{Cvoid}, (Csize_t,), 1024)
size = malloc_usable_size(ptr)
println("Usable size of allocated memory: ", size)

Z3 is known to not work well with third party allocators, and one workaround is to disable HAS_MALLOC_USABLE_SIZE to remove the calls to malloc_usable_size.