From d81def4916ae589de9dbca093bec67595572b0cc Mon Sep 17 00:00:00 2001 From: Vekhir Date: Fri, 11 Aug 2023 23:02:27 +0200 Subject: [PATCH 1/8] Introduce STP_USE_LIB flag 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. --- src/vendor/stp/Makefile | 18 +- src/vendor/stp/src_sys/Makefile | 47 +++ src/vendor/stp/src_sys/stp_c_interface.h | 483 +++++++++++++++++++++++ 3 files changed, 546 insertions(+), 2 deletions(-) create mode 100644 src/vendor/stp/src_sys/Makefile create mode 100644 src/vendor/stp/src_sys/stp_c_interface.h diff --git a/src/vendor/stp/Makefile b/src/vendor/stp/Makefile index 092995d7f..44c09a3c9 100644 --- a/src/vendor/stp/Makefile +++ b/src/vendor/stp/Makefile @@ -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) diff --git a/src/vendor/stp/src_sys/Makefile b/src/vendor/stp/src_sys/Makefile new file mode 100644 index 000000000..025b04ce7 --- /dev/null +++ b/src/vendor/stp/src_sys/Makefile @@ -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) + + + diff --git a/src/vendor/stp/src_sys/stp_c_interface.h b/src/vendor/stp/src_sys/stp_c_interface.h new file mode 100644 index 000000000..c1b42f64a --- /dev/null +++ b/src/vendor/stp/src_sys/stp_c_interface.h @@ -0,0 +1,483 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. In particular: + * + * - The above copyright notice and this permission notice must appear + * in all copies of the software and related documentation. + * + * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, + * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. + ********************************************************************/ +// -*- c++ -*- + +#ifndef _cvcl__include__c_interface_h_ +#define _cvcl__include__c_interface_h_ + +#ifdef __cplusplus +#define _CVCL_DEFAULT_ARG(v) =v +#else +#define _CVCL_DEFAULT_ARG(v) +#endif + +#ifdef __cplusplus +extern "C" { +#endif + +#include + +#ifdef STP_STRONG_TYPING +#else + //This gives absolutely no pointer typing at compile-time. Most C + //users prefer this over stronger typing. User is the king. A + //stronger typed interface is in the works. + typedef void* VC; + typedef void* Expr; + typedef void* Type; + typedef void* WholeCounterExample; +#endif + + // o : optimizations + // c : check counterexample + // p : print counterexample + // h : help + // s : stats + // v : print nodes + + // The "num_absrefine" argument isn't used at all. It's left for compatibility with existing code. + void vc_setFlags(VC vc, char c, int num_absrefine _CVCL_DEFAULT_ARG(0)); + void vc_setFlag(VC vc, char c); + + //! Interface-only flags. + enum ifaceflag_t { + /*! EXPRDELETE: boolean, default true. For objects created by + vc_arrayType, vc_bvType, vc_bv32Type, vc_bvConstExprFromInt, if + this flag is set both at the time the objects are created and at + the time that vc_Destroy is called, vc_Destroy will automatically + delete them. */ + EXPRDELETE, + MS, + SMS, + CMS2, + MSP + + }; + void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value); + + // defines division by zero to equal 1, x%0 to equal x. + // avoids division by zero errors. + void make_division_total(VC vc); + + //! Flags can be NULL + VC vc_createValidityChecker(void); + + // Basic types + Type vc_boolType(VC vc); + + //! Create an array type + Type vc_arrayType(VC vc, Type typeIndex, Type typeData); + + ///////////////////////////////////////////////////////////////////////////// + // Expr manipulation methods // + ///////////////////////////////////////////////////////////////////////////// + + //! Create a variable with a given name and type + /*! The type cannot be a function type. The var name can contain + only variables, numerals and underscore. If you use any other + symbol, you will get a segfault. */ + Expr vc_varExpr(VC vc, const char * name, Type type); + + //The var name can contain only variables, numerals and + //underscore. If you use any other symbol, you will get a segfault. + Expr vc_varExpr1(VC vc, const char* name, + int indexwidth, int valuewidth); + + //! Get the expression and type associated with a name. + /*! If there is no such Expr, a NULL Expr is returned. */ + //Expr vc_lookupVar(VC vc, char* name, Type* type); + + //! Get the type of the Expr. + Type vc_getType(VC vc, Expr e); + + int vc_getBVLength(VC vc, Expr e); + + //! Create an equality expression. The two children must have the same type. + Expr vc_eqExpr(VC vc, Expr child0, Expr child1); + + // Boolean expressions + + // The following functions create Boolean expressions. The children + // provided as arguments must be of type Boolean (except for the + // function vc_iteExpr(). In the case of vc_iteExpr() the + // conditional must always be Boolean, but the ifthenpart + // (resp. elsepart) can be bit-vector or Boolean type. But, the + // ifthenpart and elsepart must be both of the same type) + Expr vc_trueExpr(VC vc); + Expr vc_falseExpr(VC vc); + Expr vc_notExpr(VC vc, Expr child); + Expr vc_andExpr(VC vc, Expr left, Expr right); + Expr vc_andExprN(VC vc, Expr* children, int numOfChildNodes); + Expr vc_orExpr(VC vc, Expr left, Expr right); + Expr vc_xorExpr(VC vc, Expr left, Expr right); + Expr vc_orExprN(VC vc, Expr* children, int numOfChildNodes); + Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc); + Expr vc_iffExpr(VC vc, Expr left, Expr right); + //The output type of vc_iteExpr can be Boolean (formula-level ite) + //or bit-vector (word-level ite) + Expr vc_iteExpr(VC vc, Expr conditional, Expr ifthenpart, Expr elsepart); + + //Boolean to single bit BV Expression + Expr vc_boolToBVExpr(VC vc, Expr form); + + //Parameterized Boolean Expression (PARAMBOOL, Boolean_Var, parameter) + Expr vc_paramBoolExpr(VC vc, Expr var, Expr param); + + // Arrays + + //! Create an expression for the value of array at the given index + Expr vc_readExpr(VC vc, Expr array, Expr index); + + //! Array update; equivalent to "array WITH [index] := newValue" + Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue); + + // Expr I/O: Parses directly from file in the c_interface. pretty cool!! + Expr vc_parseExpr(VC vc, const char* s); + + //! Prints 'e' to stdout. + void vc_printExpr(VC vc, Expr e); + + //! Prints 'e' to stdout as C code + void vc_printExprCCode(VC vc, Expr e); + + //! print in smtlib format + char * vc_printSMTLIB(VC vc, Expr e); + + //! Prints 'e' into an open file descriptor 'fd' + void vc_printExprFile(VC vc, Expr e, int fd); + + //! Prints state of 'vc' into malloc'd buffer '*buf' and stores the + // length into '*len'. It is the responsibility of the caller to + // free the buffer. + //void vc_printStateToBuffer(VC vc, char **buf, unsigned long *len); + + //! Prints 'e' to malloc'd buffer '*buf'. Sets '*len' to the length of + // the buffer. It is the responsibility of the caller to free the buffer. + void vc_printExprToBuffer(VC vc, Expr e, char **buf, unsigned long * len); + + //! Prints counterexample to stdout. + void vc_printCounterExample(VC vc); + + //! Prints variable declarations to stdout. + void vc_printVarDecls(VC vc); + + //! Clear the internal list of variables to declare maintained for + // vc_printVarDecls. Do this after you've printed them, or if you + // never want to print them, to prevent a memory leak. + void vc_clearDecls(VC vc); + + //! Prints asserts to stdout. The flag simplify_print must be set to + //"1" if you wish simplification to occur dring printing. It must be + //set to "0" otherwise + void vc_printAsserts(VC vc, int simplify_print _CVCL_DEFAULT_ARG(0)); + + //! Prints the state of the query to malloc'd buffer '*buf' and + //stores ! the length of the buffer to '*len'. It is the + //responsibility of the caller to free the buffer. The flag + //simplify_print must be set to "1" if you wish simplification to + //occur dring printing. It must be set to "0" otherwise + void vc_printQueryStateToBuffer(VC vc, Expr e, + char **buf, unsigned long *len, int simplify_print); + + //! Similar to vc_printQueryStateToBuffer() + void vc_printCounterExampleToBuffer(VC vc, char **buf,unsigned long *len); + + //! Prints query to stdout. + void vc_printQuery(VC vc); + + ///////////////////////////////////////////////////////////////////////////// + // Context-related methods // + ///////////////////////////////////////////////////////////////////////////// + + //! Assert a new formula in the current context. + /*! The formula must have Boolean type. */ + void vc_assertFormula(VC vc, Expr e); + + //! Simplify e with respect to the current context + Expr vc_simplify(VC vc, Expr e); + + //! Check validity of e in the current context. e must be a FORMULA + //returns 0 -> the input is INVALID + //returns 1 -> the input is VALID + //returns 2 -> then ERROR + //returns 3 -> then TIMEOUT + + // NB. The timeout is a soft timeout, use the -g flag for a hard timeout that + // will abort automatically. The soft timeout is checked sometimes in the code, + // and if the time has passed, then "timeout" will be returned. It's only checked + // sometimes though, so the actual timeout may be larger. Cryptominisat doesn't check + // the timeout yet.. + + // The C-language doesn't allow default arguments, so to get it compiling, I've split + // it into two functions. + int vc_query_with_timeout(VC vc, Expr e, int timeout_ms); + int vc_query(VC vc, Expr e); + + + //! Return the counterexample after a failed query. + Expr vc_getCounterExample(VC vc, Expr e); + + //! Return an array from a counterexample after a failed query. + void vc_getCounterExampleArray(VC vc, Expr e, Expr **indices, Expr **values, int *size); + + //! get size of counterexample, i.e. the number of variables/array + //locations in the counterexample. + int vc_counterexample_size(VC vc); + + //! Checkpoint the current context and increase the scope level + void vc_push(VC vc); + + //! Restore the current context to its state at the last checkpoint + void vc_pop(VC vc); + + //! Return an int from a constant bitvector expression + int getBVInt(Expr e); + //! Return an unsigned int from a constant bitvector expression + unsigned int getBVUnsigned(Expr e); + //! Return an unsigned long long int from a constant bitvector expressions + unsigned long long int getBVUnsignedLongLong(Expr e); + + /**************************/ + /* BIT VECTOR OPERATIONS */ + /**************************/ + Type vc_bvType(VC vc, int no_bits); + Type vc_bv32Type(VC vc); + + Expr vc_bvConstExprFromDecStr(VC vc, int width, const char* decimalInput ); + Expr vc_bvConstExprFromStr(VC vc, const char* binary_repr); + Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value); + Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long long value); + Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value); + + Expr vc_bvConcatExpr(VC vc, Expr left, Expr right); + Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right); + Expr vc_bvPlusExprN(VC vc, int n_bits, Expr* children, int numOfChildNodes); + Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right); + Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right); + Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right); + Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right); + Expr vc_bv32MultExpr(VC vc, Expr left, Expr right); + // left divided by right i.e. left/right + Expr vc_bvDivExpr(VC vc, int n_bits, Expr left, Expr right); + // left modulo right i.e. left%right + Expr vc_bvModExpr(VC vc, int n_bits, Expr left, Expr right); + // signed left divided by right i.e. left/right + Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right); + // signed left modulo right i.e. left%right + Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right); + Expr vc_sbvRemExpr(VC vc, int n_bits, Expr left, Expr right); + + Expr vc_bvLtExpr(VC vc, Expr left, Expr right); + Expr vc_bvLeExpr(VC vc, Expr left, Expr right); + Expr vc_bvGtExpr(VC vc, Expr left, Expr right); + Expr vc_bvGeExpr(VC vc, Expr left, Expr right); + + Expr vc_sbvLtExpr(VC vc, Expr left, Expr right); + Expr vc_sbvLeExpr(VC vc, Expr left, Expr right); + Expr vc_sbvGtExpr(VC vc, Expr left, Expr right); + Expr vc_sbvGeExpr(VC vc, Expr left, Expr right); + + Expr vc_bvUMinusExpr(VC vc, Expr child); + + // bitwise operations: these are terms not formulas + Expr vc_bvAndExpr(VC vc, Expr left, Expr right); + Expr vc_bvOrExpr(VC vc, Expr left, Expr right); + Expr vc_bvXorExpr(VC vc, Expr left, Expr right); + Expr vc_bvNotExpr(VC vc, Expr child); + + // Shift an expression by another expression. This is newstyle. + Expr vc_bvLeftShiftExprExpr(VC vc, int n_bits, Expr left, Expr right); + Expr vc_bvRightShiftExprExpr(VC vc, int n_bits, Expr left, Expr right); + Expr vc_bvSignedRightShiftExprExpr(VC vc, int n_bits, Expr left, Expr right); + + // These shifts are old-style. Kept for compatability---oldstyle. + Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child); + Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child); + /* Same as vc_bvLeftShift only that the answer in 32 bits long */ + Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child); + /* Same as vc_bvRightShift only that the answer in 32 bits long */ + Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child); + Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child); + Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child); + Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs); + + Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no); + + //accepts a bitvector and position, and returns a boolean + //corresponding to that position. More precisely, it return the + //equation (x[bit_no:bit_no] == 0) + Expr vc_bvBoolExtract(VC vc, Expr x, int bit_no); + Expr vc_bvBoolExtract_Zero(VC vc, Expr x, int bit_no); + + //accepts a bitvector and position, and returns a boolean + //corresponding to that position. More precisely, it return the + //equation (x[bit_no:bit_no] == 1) + Expr vc_bvBoolExtract_One(VC vc, Expr x, int bit_no); + Expr vc_bvSignExtend(VC vc, Expr child, int nbits); + + /*C pointer support: C interface to support C memory arrays in CVCL */ + Expr vc_bvCreateMemoryArray(VC vc, const char * arrayName); + Expr vc_bvReadMemoryArray(VC vc, + Expr array, Expr byteIndex, int numOfBytes); + Expr vc_bvWriteToMemoryArray(VC vc, + Expr array, Expr byteIndex, + Expr element, int numOfBytes); + Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value); + + // return a string representation of the Expr e. The caller is responsible + // for deallocating the string with free() + char* exprString(Expr e); + + // return a string representation of the Type t. The caller is responsible + // for deallocating the string with free() + char* typeString(Type t); + + Expr getChild(Expr e, int i); + + //1.if input expr is TRUE then the function returns 1; + // + //2.if input expr is FALSE then function returns 0; + // + //3.otherwise the function returns -1 + int vc_isBool(Expr e); + + /* Register the given error handler to be called for each fatal error.*/ + void vc_registerErrorHandler(void (*error_hdlr)(const char* err_msg)); + + int vc_getHashQueryStateToBuffer(VC vc, Expr query); + + //destroys the STP instance, and removes all the created expressions + void vc_Destroy(VC vc); + + //deletes the expression e + void vc_DeleteExpr(Expr e); + + //Get the whole counterexample from the current context + WholeCounterExample vc_getWholeCounterExample(VC vc); + + //Get the value of a term expression from the CounterExample + Expr vc_getTermFromCounterExample(VC vc, Expr e, WholeCounterExample c); + + + // Free the return value of vc_getWholeCounterExample + void vc_deleteWholeCounterExample(WholeCounterExample cc); + + //Kinds of Expr + enum exprkind_t{ + UNDEFINED, + SYMBOL, + BVCONST, + BVNEG, + BVCONCAT, + BVOR, + BVAND, + BVXOR, + BVNAND, + BVNOR, + BVXNOR, + BVEXTRACT, + BVLEFTSHIFT, + BVRIGHTSHIFT, + BVSRSHIFT, + BVVARSHIFT, + BVPLUS, + BVSUB, + BVUMINUS, + BVMULTINVERSE, + BVMULT, + BVDIV, + BVMOD, + SBVDIV, + SBVREM, + SBVMOD, + BVSX, + BVZX, + ITE, + BVGETBIT, + BVLT, + BVLE, + BVGT, + BVGE, + BVSLT, + BVSLE, + BVSGT, + BVSGE, + EQ, + FALSE, + TRUE, + NOT, + AND, + OR, + NAND, + NOR, + XOR, + IFF, + IMPLIES, + PARAMBOOL, + READ, + WRITE, + ARRAY, + BITVECTOR, + BOOLEAN + } ; + + // type of expression + enum type_t { + BOOLEAN_TYPE = 0, + BITVECTOR_TYPE, + ARRAY_TYPE, + UNKNOWN_TYPE + }; + + // get the kind of the expression + enum exprkind_t getExprKind (Expr e); + + // get the number of children nodes + int getDegree (Expr e); + + // get the bv length + int getBVLength(Expr e); + + // get expression type + enum type_t getType (Expr e); + + // get value bit width + int getVWidth (Expr e); + + // get index bit width + int getIWidth (Expr e); + + // Prints counterexample to an open file descriptor 'fd' + void vc_printCounterExampleFile(VC vc, int fd); + + // get name of expression. must be a variable. + const char* exprName(Expr e); + + // get the node ID of an Expr. + int getExprID (Expr ex); + + // parse the expr from memory string! + int vc_parseMemExpr(VC vc, const char* s, Expr* oquery, Expr* oasserts ); +#ifdef __cplusplus +} +#endif + +#undef _CVCL_DEFAULT_ARG + +#endif + + From d3b34e39f2cae078df2d83da339756666b164da6 Mon Sep 17 00:00:00 2001 From: Vekhir Date: Sat, 12 Aug 2023 15:37:41 +0200 Subject: [PATCH 2/8] Prohibit STP_STUB in favor of STP_USE_LIB=disable Defining STP_STUB now creates an error with a hint to use STP_USE_LIB=disable. The new way is more readable and clearer in intent. Since STP_STUB had a bug that made it effectively unusable for 3 years, replacing the option likely affects few users while those that worked around the bug have to change things anyway. This change also enabled some minor refactoring work for better readability. --- src/vendor/stp/Makefile | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/src/vendor/stp/Makefile b/src/vendor/stp/Makefile index 44c09a3c9..db96e07f7 100644 --- a/src/vendor/stp/Makefile +++ b/src/vendor/stp/Makefile @@ -5,11 +5,19 @@ PREFIX?=$(TOP)/inst .PHONY: all install clean full_clean -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 ifeq ($(STP_USE_LIB),included) # compile from provided source +ifneq ($(STP_STUB),) # STP_STUB didn't work for 3 years anyway +$(error STP_STUB is deprecated: Use STP_USE_LIB=disable instead) +endif + +ifeq ($(STP_USE_LIB),) # use default +STP_USE_LIB=included +endif + +define ispath +$(shell echo "$1" | grep -E "^/*") +endef + +ifeq ($(STP_USE_LIB),included) # compile from provided source SRC = src else ifeq ($(STP_USE_LIB),disable) # disable STP at runtime SRC = src_stub @@ -17,7 +25,7 @@ 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 +else ifneq ($(call ispath,"$(STP_USE_LIB)"),) # use STP at the absolute path provided by STP_USE_LIB SRC = src_sys STP_LIBPATH = $(STP_USE_LIB) export STP_LIBPATH From 0feb6b8db9fed6941710881ac82fbd3561c157c2 Mon Sep 17 00:00:00 2001 From: Vekhir Date: Sat, 12 Aug 2023 15:38:37 +0200 Subject: [PATCH 3/8] Add MacOS support to STP_USE_LIB On MacOS, libraries have a different suffix and the filesystem is structured differently. This commit adds the relevant bits and pieces for the option STP_USE_LIB to work on MacOS in principle. Also fixes the issue with STP_STUB (which is used with STP_USE_LIB=disable), where the wrong library file is copied, resulting in a linking error down the line. --- src/vendor/stp/Makefile | 32 ++++++++++++++++++++++++-------- src/vendor/stp/src_stub/Makefile | 14 ++++++-------- src/vendor/stp/src_sys/Makefile | 20 ++++---------------- 3 files changed, 34 insertions(+), 32 deletions(-) diff --git a/src/vendor/stp/Makefile b/src/vendor/stp/Makefile index db96e07f7..cea829cd2 100644 --- a/src/vendor/stp/Makefile +++ b/src/vendor/stp/Makefile @@ -19,25 +19,41 @@ endef ifeq ($(STP_USE_LIB),included) # compile from provided source SRC = src +ifeq ($(OSTYPE), Darwin) +SNAME=libstp.dylib +else +SNAME=libstp.so.1 +endif else ifeq ($(STP_USE_LIB),disable) # disable STP at runtime SRC = src_stub +ifeq ($(OSTYPE), Darwin) +SNAME=libstp_disabled.dylib +else +SNAME=libstp_disabled.so +endif else ifeq ($(STP_USE_LIB),system) # use system STP SRC = src_sys -STP_LIBPATH = /usr/lib/ +ifeq ($(OSTYPE), Darwin) +# untested +SNAME=libstp_sys.dylib +STP_LIBPATH = /usr/local/opt/stp@ +else +SNAME=libstp_sys.so +STP_LIBPATH = /usr/lib/libstp.so +endif export STP_LIBPATH else ifneq ($(call ispath,"$(STP_USE_LIB)"),) # use STP at the absolute path provided by STP_USE_LIB SRC = src_sys +SNAME=$(shell echo $(STP_USE_LIB) | grep -o "[a-z0-9.]*$$") +ifeq ($(SNAME),) +$(error invalid library name: $(STP_USE_LIB)) +endif 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) -SNAME=libstp.dylib -else -SNAME=libstp.so.1 -endif +export SNAME all: install @@ -45,7 +61,7 @@ install: $(MAKE) -C $(SRC) install ln -fsn HaskellIfc include_hs install -m 755 -d $(PREFIX)/lib/SAT - install -m 644 lib/$(SNAME) $(PREFIX)/lib/SAT + install -m 644 "lib/$(SNAME)" $(PREFIX)/lib/SAT clean: $(MAKE) -C $(SRC) clean diff --git a/src/vendor/stp/src_stub/Makefile b/src/vendor/stp/src_stub/Makefile index fe24c4b0e..cee9815ef 100644 --- a/src/vendor/stp/src_stub/Makefile +++ b/src/vendor/stp/src_stub/Makefile @@ -10,9 +10,9 @@ LIB_DIR=../lib INC_DIR=../include ifeq ($(OSTYPE), Darwin) -LDFLAGS = -dynamiclib -Wl,-install_name,libstp_stub.so +LDFLAGS = -dynamiclib -Wl,-install_name,$(SNAME) else -LDFLAGS = -shared -Wl,-soname,libstp_stub.so +LDFLAGS = -shared -Wl,-soname,$(SNAME) endif .PHONY: all @@ -21,18 +21,16 @@ all: install stp_stub.o: stp_stub.c stp_c_interface.h $(CC) $(CFLAGS) -c -o $@ $< -libstp_stub.so: stp_stub.o +$(SNAME): stp_stub.o $(CC) $(CFLAGS) $(LDFLAGS) -o $@ $< -libstp.so: libstp_stub.so +libstp.so: $(SNAME) $(RM) $@ ln -s $< $@ -install: libstp_stub.so +install: $(SNAME) mkdir -p $(LIB_DIR) - $(CP) libstp_stub.so $(LIB_DIR)/ - ln -fsn libstp.so.1 $(LIB_DIR)/libstp.so - ln -fsn libstp_stub.so $(LIB_DIR)/libstp.so.1 + $(CP) $(SNAME) $(LIB_DIR)/ mkdir -p $(INC_DIR) $(CP) stp_c_interface.h $(INC_DIR)/ diff --git a/src/vendor/stp/src_sys/Makefile b/src/vendor/stp/src_sys/Makefile index 025b04ce7..b18467411 100644 --- a/src/vendor/stp/src_sys/Makefile +++ b/src/vendor/stp/src_sys/Makefile @@ -9,28 +9,16 @@ 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 $< $@ +$(SNAME): + $(CP) "$(STP_LIBPATH)" ./$(SNAME) -install: libstp_sys.so +install: $(SNAME) 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 + $(CP) $(SNAME) $(LIB_DIR)/ mkdir -p $(INC_DIR) $(CP) stp_c_interface.h $(INC_DIR)/ From a4536b80f7bd3f84343e48416c4c56c3bc9ad574 Mon Sep 17 00:00:00 2001 From: Vekhir Date: Sat, 12 Aug 2023 17:39:12 +0200 Subject: [PATCH 4/8] Generalize search for STP system library On Linux, use find in /usr/lib to find the correct library. Only consider the first result; all results should point to the same source anyway. The results are also cleaned to ensure reliable behavior (the library name must only contain alphanumerics + colon) Improve cleaning of user input when a path is passed in --- src/vendor/stp/Makefile | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/vendor/stp/Makefile b/src/vendor/stp/Makefile index cea829cd2..863efac07 100644 --- a/src/vendor/stp/Makefile +++ b/src/vendor/stp/Makefile @@ -39,12 +39,15 @@ SNAME=libstp_sys.dylib STP_LIBPATH = /usr/local/opt/stp@ else SNAME=libstp_sys.so -STP_LIBPATH = /usr/lib/libstp.so +STP_LIBPATH=$(shell find /usr/lib/ -name "libstp.so*" -type f -print0 | grep "/[a-z0-9.]*$$" | head -n 1) +ifeq ($(STP_LIBPATH),) +$(error invalid library name: $(STP_USE_LIB)) +endif endif export STP_LIBPATH else ifneq ($(call ispath,"$(STP_USE_LIB)"),) # use STP at the absolute path provided by STP_USE_LIB SRC = src_sys -SNAME=$(shell echo $(STP_USE_LIB) | grep -o "[a-z0-9.]*$$") +SNAME=$(shell echo $(STP_USE_LIB) | grep -o "/[a-z0-9.]*$$" | cut -f2- -d/) ifeq ($(SNAME),) $(error invalid library name: $(STP_USE_LIB)) endif From fcb8e05ca427e70b62f29bbc6f3100afe5909cfd Mon Sep 17 00:00:00 2001 From: Vekhir Date: Sat, 12 Aug 2023 18:55:42 +0200 Subject: [PATCH 5/8] Improve readability in stp/Makefile The logic for STP_USE_LIB has been indented to improve the readability and make the different cases more obvious. Also, minor fixes. `find` ends with NUL byte, so replace that with newline. The BSC linker needs at least a symlink named libstp.so The SNAME is completely independent from the library name, so just choose a fitting one --- src/vendor/stp/Makefile | 62 ++++++++++++++++++++--------------------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/src/vendor/stp/Makefile b/src/vendor/stp/Makefile index 863efac07..eaf413d3f 100644 --- a/src/vendor/stp/Makefile +++ b/src/vendor/stp/Makefile @@ -17,44 +17,42 @@ define ispath $(shell echo "$1" | grep -E "^/*") endef -ifeq ($(STP_USE_LIB),included) # compile from provided source -SRC = src ifeq ($(OSTYPE), Darwin) -SNAME=libstp.dylib +SO=dylib else -SNAME=libstp.so.1 +SO=so endif + +ifeq ($(STP_USE_LIB),included) # compile from provided source + SRC = src + ifeq ($(OSTYPE), Darwin) + SNAME=libstp_incl.dylib + else + SNAME=libstp_incl.so.1 + endif else ifeq ($(STP_USE_LIB),disable) # disable STP at runtime -SRC = src_stub -ifeq ($(OSTYPE), Darwin) -SNAME=libstp_disabled.dylib -else -SNAME=libstp_disabled.so -endif + SRC = src_stub + SNAME=libstp_disabled.$(SO) else ifeq ($(STP_USE_LIB),system) # use system STP -SRC = src_sys -ifeq ($(OSTYPE), Darwin) -# untested -SNAME=libstp_sys.dylib -STP_LIBPATH = /usr/local/opt/stp@ -else -SNAME=libstp_sys.so -STP_LIBPATH=$(shell find /usr/lib/ -name "libstp.so*" -type f -print0 | grep "/[a-z0-9.]*$$" | head -n 1) -ifeq ($(STP_LIBPATH),) -$(error invalid library name: $(STP_USE_LIB)) -endif -endif -export STP_LIBPATH + SRC = src_sys + ifeq ($(OSTYPE), Darwin) + SNAME=libstp_sys.dylib + STP_LIBPATH = /usr/local/opt/stp@ + else # Linux + SNAME=libstp_sys.so + STP_LIBPATH=$(shell find /usr/lib/ -name "libstp.so*" -type f -print0 | tr '\0' '\n' | grep "/[a-z0-9.]*$$" | head -n 1) + ifeq ($(STP_LIBPATH),) + $(error No valid library found in /usr/lib) + endif + endif + export STP_LIBPATH else ifneq ($(call ispath,"$(STP_USE_LIB)"),) # use STP at the absolute path provided by STP_USE_LIB -SRC = src_sys -SNAME=$(shell echo $(STP_USE_LIB) | grep -o "/[a-z0-9.]*$$" | cut -f2- -d/) -ifeq ($(SNAME),) -$(error invalid library name: $(STP_USE_LIB)) -endif -STP_LIBPATH = $(STP_USE_LIB) -export STP_LIBPATH + SRC = src_sys + SNAME=libstp_custom.$(SO) + 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)) + $(error Unknown option for STP_USE_LIB: $(STP_USE_LIB)) endif export SNAME @@ -63,6 +61,8 @@ all: install install: $(MAKE) -C $(SRC) install ln -fsn HaskellIfc include_hs + @# necessary for bsc linker (src/comp/Makefile:51) + ln -s "$(SNAME)" lib/libstp.$(SO) install -m 755 -d $(PREFIX)/lib/SAT install -m 644 "lib/$(SNAME)" $(PREFIX)/lib/SAT From 4866ecfe5519df3c77654a4d7267ef7ab031e11c Mon Sep 17 00:00:00 2001 From: Vekhir Date: Sun, 13 Aug 2023 03:39:30 +0200 Subject: [PATCH 6/8] Clean up STP src The SNAME is exported in the general stp Makefile. The symbolic link is created there too. Remove both actions from the special case as they are handled in the general case. --- src/vendor/stp/src/Makefile | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/src/vendor/stp/src/Makefile b/src/vendor/stp/src/Makefile index 988253af1..5f05463d2 100644 --- a/src/vendor/stp/src/Makefile +++ b/src/vendor/stp/src/Makefile @@ -14,13 +14,7 @@ else CP = cp -df endif -ifeq ($(OSTYPE), Darwin) -LIBRARIES=lib/libstp.dylib -SNAME = libstp.dylib -else -LIBRARIES=lib/libstp.so.1 lib/libstp.so -SNAME = libstp.so.1 -endif +LIBRARIES=lib/$(SNAME) .PHONY: all all: $(LIBRARIES) @@ -72,12 +66,6 @@ lib/$(SNAME): c_interface/c_interface.o \ @# We use --whole-archive to ensure that all symbols in to-sat are used $(CXX) $(CFLAGS) $(SHAREDFLAG) -Wl,$(SONAMEFLAG),$(SNAME) -o $@ $(LIBCCARGS) -ifneq ($(OSTYPE), Darwin) -lib/libstp.so: lib/libstp.so.1 - -rm -f $@ - (cd lib; ln -s libstp.so.1 libstp.so) -endif - # During the build of AST some classes are built that most of the other # classes depend upon. So in a parallel make, AST should be made first. From cf03829c503e2ce178eef981ab0248dcb724c550 Mon Sep 17 00:00:00 2001 From: Vekhir Date: Sun, 13 Aug 2023 20:27:42 +0200 Subject: [PATCH 7/8] Minor fixes for STP handling --- src/vendor/stp/Makefile | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/vendor/stp/Makefile b/src/vendor/stp/Makefile index eaf413d3f..ee54458a5 100644 --- a/src/vendor/stp/Makefile +++ b/src/vendor/stp/Makefile @@ -30,7 +30,7 @@ ifeq ($(STP_USE_LIB),included) # compile from provided source else SNAME=libstp_incl.so.1 endif -else ifeq ($(STP_USE_LIB),disable) # disable STP at runtime +else ifeq ($(STP_USE_LIB),disable) # disable STP SRC = src_stub SNAME=libstp_disabled.$(SO) else ifeq ($(STP_USE_LIB),system) # use system STP @@ -63,8 +63,11 @@ install: ln -fsn HaskellIfc include_hs @# necessary for bsc linker (src/comp/Makefile:51) ln -s "$(SNAME)" lib/libstp.$(SO) +# put self-compiled library in path where it can be found at runtime +ifeq ($(SRC), $(findstring $(SRC), src src_stub)) install -m 755 -d $(PREFIX)/lib/SAT install -m 644 "lib/$(SNAME)" $(PREFIX)/lib/SAT +endif clean: $(MAKE) -C $(SRC) clean From aed005b0414800e488cc1aaab7bbb1d0ba4500ae Mon Sep 17 00:00:00 2001 From: Vekhir Date: Wed, 16 Aug 2023 14:23:30 +0200 Subject: [PATCH 8/8] Introduce placeholder option to STP Using STP_USE_LIB=placeholder means that the stub is compiled with a generic name and copied to the installation, but is supposed to be replaced at a later date. To make the intentions clear, the library is renamed to *_placeholder with a symlink created with the original name pointing to the library. --- src/vendor/stp/Makefile | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/vendor/stp/Makefile b/src/vendor/stp/Makefile index ee54458a5..a2b62e95d 100644 --- a/src/vendor/stp/Makefile +++ b/src/vendor/stp/Makefile @@ -33,6 +33,9 @@ ifeq ($(STP_USE_LIB),included) # compile from provided source else ifeq ($(STP_USE_LIB),disable) # disable STP SRC = src_stub SNAME=libstp_disabled.$(SO) +else ifeq ($(STP_USE_LIB),placeholder) # use stub to be replaced by real library later + SRC = src_stub + SNAME=libstp.$(SO) else ifeq ($(STP_USE_LIB),system) # use system STP SRC = src_sys ifeq ($(OSTYPE), Darwin) @@ -62,12 +65,17 @@ install: $(MAKE) -C $(SRC) install ln -fsn HaskellIfc include_hs @# necessary for bsc linker (src/comp/Makefile:51) - ln -s "$(SNAME)" lib/libstp.$(SO) + ln -s "$(SNAME)" lib/libstp.$(SO) || true # put self-compiled library in path where it can be found at runtime -ifeq ($(SRC), $(findstring $(SRC), src src_stub)) +ifeq ($(STP_USE_LIB), $(findstring $(STP_USE_LIB), included disable placeholder)) install -m 755 -d $(PREFIX)/lib/SAT install -m 644 "lib/$(SNAME)" $(PREFIX)/lib/SAT endif +# make it obvious that the library is a placeholder +ifeq ($(STP_USE_LIB), $(findstring $(STP_USE_LIB), placeholder)) + mv "$(PREFIX)/lib/SAT/$(SNAME)" libstp_placeholder.$(SO) + ln -s libstp_placeholder.$(SO) "$(PREFIX)/lib/SAT/$(SNAME)" +endif clean: $(MAKE) -C $(SRC) clean