Skip to content

Commit

Permalink
Introduce STP_USE_LIB flag
Browse files Browse the repository at this point in the history
The new build flag STP_USE_LIB can be set to choose the STP library to be used.
Options are '', 'included', 'system', 'disable', and an absolute path starting with '/'.

The empty string defaults to the same behavior as 'included' which builds STP from the provided source.
'disable' has the same effect as STP_STUB=1, i.e. disabling STP at runtime.
'system' tries to find the system library (currently only in /usr/lib) and then copies it for building.
An absolute path starting with '/' can be provided and must point to the directory in which the desired STP library is located. Otherwise the
same as 'system'.

The options for precompiled STP libraries essentially do the same things as STP_STUB, except they copies the library
instead of compiling the stub. For compatibility reasons within the Makefiles, the library is linked to under
the soname libstp.so.1 eventhough technically it should be libstp.so.2.3 (for the newest versions), but STP is backwards-compatible
enough that this does not cause issues.

Enabling the flag reduced the build time by up to 25% (the time to compile STP from source), while `make TEST_BSC_OPTIONS="-sat-stp" smoke`
saw no reductions, both compared to the provided source and Yices.
  • Loading branch information
Vekhir committed Aug 11, 2023
1 parent 42fb7b6 commit 6e89063
Show file tree
Hide file tree
Showing 3 changed files with 546 additions and 2 deletions.
18 changes: 16 additions & 2 deletions src/vendor/stp/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,24 @@ PREFIX?=$(TOP)/inst

.PHONY: all install clean full_clean

ifeq ($(STP_STUB),)
ifneq ($(STP_STUB),) # If STP_STUB exists, disable STP. Otherwise check STP_USE_LIB
SRC = src_stub
else ifeq ($(STP_USE_LIB),) # default (compile from provided source)
SRC = src
else
else ifeq ($(STP_USE_LIB),included) # compile from provided source
SRC = src
else ifeq ($(STP_USE_LIB),disable) # disable STP at runtime
SRC = src_stub
else ifeq ($(STP_USE_LIB),system) # use system STP
SRC = src_sys
STP_LIBPATH = /usr/lib/
export STP_LIBPATH
else ifneq ($(shell echo "$(STP_USE_LIB)" | grep -E "^/*"),) # use STP at the absolute path provided by STP_USE_LIB
SRC = src_sys
STP_LIBPATH = $(STP_USE_LIB)
export STP_LIBPATH
else # unknown option for STP_USE_LIB
$(error Unknown option for STP_USE_LIB: $(STP_USE_LIB))
endif

ifeq ($(OSTYPE), Darwin)
Expand Down
47 changes: 47 additions & 0 deletions src/vendor/stp/src_sys/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
PWD:=$(shell pwd)
TOP:=$(PWD)/../../../..

include $(TOP)/platform.mk

RM ?= rm -rf
CP ?= cp

LIB_DIR=../lib
INC_DIR=../include

ifeq ($(OSTYPE), Darwin)
LDFLAGS = -dynamiclib -Wl,-install_name,libstp_sys.so
else
LDFLAGS = -shared -Wl,-soname,libstp_sys.so
endif

.PHONY: all
all: install


libstp_sys.so:
$(CP) "$(STP_LIBPATH)/libstp.so" ./libstp_sys.so

libstp.so: libstp_sys.so
$(RM) $@
ln -s $< $@

install: libstp_sys.so
mkdir -p $(LIB_DIR)
$(CP) libstp_sys.so $(LIB_DIR)/
ln -fsn libstp.so.1 $(LIB_DIR)/libstp.so
ln -fsn libstp_sys.so $(LIB_DIR)/libstp.so.1
mkdir -p $(INC_DIR)
$(CP) stp_c_interface.h $(INC_DIR)/

.PHONY: clean full_clean

clean:
$(RM) *.o *.so

full_clean: clean
$(RM) -R $(LIB_DIR)
$(RM) -R $(INC_DIR)



Loading

0 comments on commit 6e89063

Please sign in to comment.