SIGSEGV with --staticbin

[SaswatPadhi]

A statically linked z3 binary compiled from the master branch fails to run and terminates with a segmentation fault (SIGSEGV signal).

Steps to reproduce: (tested on Debian 10)

1. git checkout master
2. python scripts/mk_make.py --staticbin
3. cd build && make
4. ./z3 -v

Without the --staticbin flag, the compiled z3 binary runs as expected.

[NikolajBjorner]

Perhaps related to recent use of lpthread.
https://stackoverflow.com/questions/35116327/when-g-static-link-pthread-cause-segmentation-fault-why

[fpoli]

Is there any workaround to statically link z3? I get the same error on Ubuntu 16.04.

[fpoli]

The python scripts/mk_make.py --staticbin command generates a build/config.mk containing LINK_EXTRA_FLAGS= -lpthread. If I manually modify this to LINK_EXTRA_FLAGS= -Wl,--whole-archive -lpthread -Wl,--no-whole-archive (as suggested in the SO question) then the compiled z3 runs fine. However, I'm not sure how to generate this modified configuration using the mx_make.py script.

[NikolajBjorner]

Could you change

z3/scripts/mk_util.py

Line 2634 in a78f899

config.write('LINK_EXTRA_FLAGS= -lpthread %s\n' % LDFLAGS)

and add pull request as appropriate?

We have utilities;

   def build_static_lib():
          return STATIC_LIB

    def build_static_bin():
           return STATIC_BIN

to get the configuration properties.
My test setup for ubuntu isn't too agile.

[SaswatPadhi]

I pulled the latest changes and rebuilt z3 on my Debian machine -- works as expected with both --staticbin and --staticlib.

Thanks @NikolajBjorner and @fpoli.

[SaswatPadhi]

Actually, I just noticed that although the build was successful, the z3 binary still fails on my Debian machine with SIGSEGV ...

@fpoli: Does z3 run as expected on your Ubuntu machine?

Sorry for the confusion!

[fpoli]

@SaswatPadhi on various Ubuntu 16.04 computers that I tried yes, it runs as expected. Before, z3 --version was enough to cause a segmentation fault.

Have you checked if your build/config.mk actually contains LINK_EXTRA_FLAGS= -Wl,--whole-archive -lpthread -Wl,--no-whole-archive?

[SaswatPadhi]

Hello,

Sorry for the delay in getting back -- I had a deadline.

I pulled the latest changes and checked again that build/config.mk contains LINK_EXTRA_FLAGS= -Wl,--whole-archive -lpthread -Wl,--no-whole-archive. Here is my config.mk file:

PREFIX=/usr
CC=gcc
CXX=g++
CXXFLAGS= -D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE -D_USE_THREAD_LOCAL  -std=c++11 -fvisibility=hidden -c -mfpmath=sse -msse -msse2 -O3 -D_LINUX_ -fPIC
CFLAGS= -D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE -D_USE_THREAD_LOCAL   -fvisibility=hidden -c -mfpmath=sse -msse -msse2 -O3 -D_LINUX_ -fPIC
EXAMP_DEBUG_FLAG=
CXX_OUT_FLAG=-o 
C_OUT_FLAG=-o 
OBJ_EXT=.o
LIB_EXT=.a
AR=ar
AR_FLAGS=rcs
AR_OUTFLAG=
EXE_EXT=
LINK=g++
LINK_FLAGS=
LINK_OUT_FLAG=-o 
LINK_EXTRA_FLAGS=-Wl,--whole-archive -lpthread -Wl,--no-whole-archive 
SO_EXT=.so
SLINK=g++
SLINK_FLAGS=-shared
SLINK_EXTRA_FLAGS=-lpthread  -Wl,-soname,libz3.so
SLINK_OUT_FLAG=-o 
OS_DEFINES=-D_LINUX_

But I still get:

$ ./z3 --version
"./z3 --version" terminated by signal SIGSEGV (Address boundary error)

I am running Debian 10.2 with Linux kernel 5.3.9 and glibc version 2.28.

[NikolajBjorner]

Could you if possible dig deeper? e.g., modify the SLINK_EXTRA_FLAGS

The update worked for my ubuntu 16 VM.

[SaswatPadhi]

I tried to modify the SLINK_EXTRA_FLAGS as well, as below

SLINK_EXTRA_FLAGS=-Wl,--whole-archive -lpthread -Wl,--no-whole-archive -Wl,-soname,libz3.so

but it did not help.

Also, this issue is reproducible on Ubuntu 19.04 as well.

[fpoli]

I can reproduce the issue by using an Ubuntu 19.04 Docker image

[fpoli]

This SO question seems to explain the difference between Ubuntu 16.04 and 19.04, but no solution is provided.

On Ubuntu 16.04, indeed, the output of nm z3 | grep pthread_mutex_lock contains T pthread_mutex_lock, while on 19.04 it contains W pthread_mutex_lock.

[fpoli]

@SaswatPadhi Can you try on Debian with LINK_EXTRA_FLAGS=-Wl,--whole-archive -lpthread -lrt -Wl,--no-whole-archive? That should work.

[SaswatPadhi]

Awesome! I confirm that z3 compiles and runs as expected on both Debian 10.2 and Ubuntu 19.04.

Thanks @fpoli, @NikolajBjorner.