Yices2 MacOS Support

lib/native/source/yices2j/compile.sh

@@ -42,71 +42,100 @@ GMP_LIB_DIR=$GMP_HEADER_DIR/.libs
 GPERF_HEADER_DIR=$RELATIVE_ROOT_DIR/"$3"
 GPERF_LIB_DIR=$GPERF_HEADER_DIR/lib
 
+LDFLAGS="-L. $LDFLAGS"
+add_include_lib() {
+    [ -d "$1" ] && CFLAGS="$CFLAGS -I$1"
+    [ -d "$2" ] && LDFLAGS="$LDFLAGS -L$2"
+}
+add_include_lib "$YICES_SRC_DIR" "$YICES_LIB_DIR"
+add_include_lib "$GMP_HEADER_DIR" "$GMP_LIB_DIR"
+add_include_lib "$GPERF_HEADER_DIR" "$GPERF_LIB_DIR"
+
+command_exists() {
+    command -v "$1" >/dev/null 2>&1
+}
+header_exists() {
+    for F in ${CFLAGS} -I/usr/include -I/include; do
+        [ "${F}" != "${F#-I}" ] && [ -f "${F#-I}/$1" ] && return 0
+    done
+    echo "Missing path to header \"$1\" in CFLAGS."
+    return 1
+}
+find_library() {
+    for F in ${LDFLAGS} -L/usr/lib -L/lib; do
+        [ "${F}" != "${F#-L}" ] && [ -f "${F#-L}/$1" ] && echo "${F#-L}/$1" && return 0
+    done
+    return 1
+}
+library_exists() {
+    find_library "$1" >/dev/null && return 0
+    echo "Missing path to library \"$1\" in LDFLAGS."
+    return 1
+}
+
 # check requirements
-if [ ! -f "$YICES_LIB_DIR/libyices.a" ]; then
-    echo "You need to specify the directory with the downloaded and compiled Yices on the command line!"
-    echo "Can not find $YICES_LIB_DIR/libyices.a"
-	exit 1
-fi
-if [ ! -f "$GMP_LIB_DIR/libgmp.a" ]; then
-    echo "You need to specify the GMP directory on the command line!"
-    echo "Can not find $GMP_LIB_DIR/libgmp.a"
-    exit 1
-fi
-if [ ! -f "$GPERF_LIB_DIR/libgp.a" ]; then
-    echo "You need to specify the GPERF directory on the command line!"
-    echo "Can not find $GPERF_LIB_DIR/libgp.a"
-	exit 1
-fi
+command_exists cc
+header_exists gmp.h
+header_exists yices.h
+header_exists jni.h
+library_exists libyices.a
+library_exists libgmp.a
+[ $(uname -s) != "Darwin" ] && [ $(uname -m) == "x86_64" ] && library_exists libgp.a
 
-SRC_FILES="org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c"
-OBJ_FILES="org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.o"
+SRC_FILE="org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c"
+OBJ_FILE="org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.o"
 
 OUT_FILE="libyices2j.so"
+[ $(uname -s) = "Darwin" ] && OUT_FILE="libyices2j.dylib"
 
 echo "Compiling the C wrapper code and creating the \"$OUT_FILE\" library..."
 
 # This will compile the JNI wrapper part, given the JNI and the Yices header files
-gcc -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno-unused-parameter \
-    $JNI_HEADERS -I$YICES_SRC_DIR -I$GMP_HEADER_DIR -I$GPERF_HEADER_DIR $SRC_FILES -fPIC -c
+cc -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno-unused-parameter \
+    $CFLAGS $JNI_HEADERS $SRC_FILE -fPIC -c -o $OBJ_FILE
 
 echo "Compilation Done"
 echo "Linking libraries together into one file..."
 
 # This will link together the file produced above, the Yices library, the GMP library and the standard libraries.
 # Everything except the standard libraries is included statically.
 # The result is a single shared library containing all necessary components.
-if [ `uname -m` = "x86_64" ]; then
-    gcc -Wall -g -o $OUT_FILE -shared -Wl,-soname,libyices2j.so \
-    -L. -L$YICES_LIB_DIR -L$GMP_LIB_DIR -L$GPERF_LIB_DIR \
-    -I$GMP_HEADER_DIR -I$GPERF_HEADER_DIR $OBJ_FILES -Wl,-Bstatic \
-    -lyices -lgmpxx -lgmp -lgp -static-libstdc++ -lstdc++ \
-    -Wl,-Bdynamic -lc -lm -Wl,--version-script=libyices2j.version
+if [ $(uname -s) = "Darwin" ]; then
+    LDFLAGS="$LDFLAGS -dynamiclib $(find_library libyices.a) $(find_library libgmp.a)"
+elif [ $(uname -m) = "x86_64" ]; then
+    LDFLAGS="$LDFLAGS -shared -Wl,-soname,libyices2j.so
+    -Wl,-Bstatic -lyices -lgmpxx -lgmp -lgp -static-libstdc++ -lstdc++
+    -Wl,-Bdynamic -lc -lm
+    -Wl,--version-script=libyices2j.version"
 else
     # TODO compiling for/on a 32bit system was not done for quite a long time. We should drop it.
-    gcc -Wall -g -o ${OUT_FILE} -shared -Wl,-soname,libyices2j.so \
-    -L${YICES_LIB_DIR} -L${GMP_LIB_DIR} -L${GPERF_LIB_DIR} \
-    -I${GMP_HEADER_DIR} -I${GPERF_HEADER_DIR} ${OBJ_FILES} \
-    -Wl,-Bstatic -lyices -lgmpxx -lgmp -Wl,-Bdynamic -lc -lm -lstdc++
+    LDFLAGS="$LDFLAGS -shared -Wl,-soname,libyices2j.so
+    -Wl,-Bstatic -lyices -lgmpxx -lgmp
+    -Wl,-Bdynamic -lc -lm -lstdc++"
 fi
+cc -Wall -g -o "$OUT_FILE" $LDFLAGS "$OBJ_FILE"
 
 if [ $? -ne 0 ]; then
-    echo "There was a problem during compilation of \"org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c\""
+    echo "There was a problem during compilation of \"$SRC_FILE\""
     exit 1
 fi
 
 echo "Linking Done"
 echo "Reducing file size by dropping unused symbols..."
 
-strip ${OUT_FILE}
+STRIP_FLAGS=""
+[ $(uname -s) = "Darwin" ] && STRIP_FLAGS="-u"
+strip $STRIP_FLAGS "$OUT_FILE"
 
 echo "Reduction Done"
 
-MISSING_SYMBOLS="$(readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND)"
-if [ ! -z "$MISSING_SYMBOLS" ]; then
-    echo "Warning: There are the following unresolved dependencies in libyices2j.so:"
-    readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND
-    exit 1
+if command_exists readelf; then
+    MISSING_SYMBOLS="$(readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND)"
+    if [ ! -z "$MISSING_SYMBOLS" ]; then
+        echo "Warning: There are the following unresolved dependencies in libyices2j.so:"
+        readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND
+        exit 1
+    fi
 fi
 
 echo "All Done"

lib/native/source/yices2j/includes/defines.h

@@ -188,6 +188,14 @@ typedef void jvoid; // for symmetry to jint, jlong etc.
   (*jenv)->ReleaseLongArrayElements(jenv, arg##num, m_arg##num, 0); \
   out##num:
 
+#define INT_INIT \
+  int retval = -1;
+
+#define TERM_VECTOR_ARG_INIT INT_INIT
+
+#define POINTER_INIT(type) \
+  type* retval = NULL;
+
 //may cause memory leak through yices_error_string
 #define INT_RETURN \
   if (retval <= 0 && yices_error_code() != 0){ \
@@ -305,7 +313,7 @@ typedef void jvoid; // for symmetry to jint, jlong etc.
   int yval[2]; \
   yval[0] = s_arg##num.node_id; \
   yval[1] = s_arg##num.node_tag; \
-  jintArray jretval; \
+  jintArray jretval = 0; \
   if (!(*jenv)->ExceptionCheck(jenv)) { \
     jretval = (*jenv)->NewIntArray(jenv, 2); \
     if(jretval != NULL){ \
@@ -418,11 +426,13 @@ typedef jlong jjparam;
 typedef jint jjterm;
 #define TERM_ARG(num) SIMPLE_ARG(term_t, num)
 #define TERM_ARG_VOID(num) SIMPLE_ARG(term_t, num)
+#define TERM_INIT INT_INIT
 #define TERM_RETURN INT_RETURN
 
 typedef jlong jjmodel;
 #define MODEL_ARG(num) POINTER_ARG(model_t, num)
 #define MODEL_ARG_VOID(num) POINTER_ARG(model_t, num)
+#define MODEL_INIT POINTER_INIT(model_t)
 #define MODEL_RETURN POINTER_RETURN
 //For things like model_t **
 #define MODEL_ARG_POINTER(num) POINTER_POINTER_ARG(model_t, num)
@@ -434,6 +444,7 @@ typedef jintArray jjtermArray;
 
 typedef jint jjtype;
 #define TYPE_ARG(num) SIMPLE_ARG(type_t, num)
+#define TYPE_INIT INT_INIT
 #define TYPE_RETURN INT_RETURN
 
 typedef jintArray jjtypeArray;