Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Modify setup-picosat.sh to avoid race-condition in PicoSAT's makefiles #40

Closed aytey closed 5 years ago

aytey commented 5 years ago

When performing a build of PicoSAT, I frequently (every time?) have issues when running:

rm -rf deps/ && ./contrib/setup-picosat.sh

which results in:

#
# SNIP
#
gcc -Wall -Wextra -DNDEBUG -O3 -fPIC -shared -o libpicosat.so picosat.o version.o -Xlinker -soname -Xlinker libpicosat.so
ranlib libpicosat.a
gcc -Wall -Wextra -DNDEBUG -O3 -fPIC -o picosat main.o app.o -L. -lpicosat
gcc -Wall -Wextra -DNDEBUG -O3 -fPIC -o picomcs picomcs.o -L. -lpicosat
gcc -Wall -Wextra -DNDEBUG -O3 -fPIC -o picomus picomus.o -L. -lpicosat
gcc -Wall -Wextra -DNDEBUG -O3 -fPIC -o picogcnf picogcnf.o -L. -lpicosat
./libpicosat.so: file not recognized: File truncated
collect2: error: ld returned 1 exit status
makefile:22: recipe for target 'picomus' failed
make: *** [picomus] Error 1
make: *** Waiting for unfinished jobs....
./libpicosat.so: file not recognized: File truncated
collect2: error: ld returned 1 exit status
./libpicosat.so: file not recognized: File truncated
collect2: error: ld returned 1 exit status
makefile:16: recipe for target 'picosat' failed
make: *** [picosat] Error 1
makefile:25: recipe for target 'picogcnf' failed
make: *** [picogcnf] Error 1
./libpicosat.so: file not recognized: File truncated
collect2: error: ld returned 1 exit status
makefile:19: recipe for target 'picomcs' failed
make: *** [picomcs] Error 1

I believe the issue here is that when Boolector builds PicoSAT with the -shared flag, that the relationship between (e.g.,) picosat (the executable) and libpicosat.so is not specified. The build issue is related to the fact that the linker tries to use the shared objects, rather than the archives. Consequently, if the shared objects have not finished being created by the time make tries to link the binaries with -lpicosat, then ld reads an incomplete .so.

Given that the Boolector does not need these executables (it only needs the .a and .so) the easiest fix here is to make Boolector's setup-picosat.sh only build what it needs (i.e., libpicosat.a and libpicosat.so), and not the ancillary binaries.

This is what this PR achieves.