Yices2 windows support

lib/native/source/yices2j/compileForWindows.sh

@@ -0,0 +1,186 @@
+#!/usr/bin/env bash
+
+# This file is part of JavaSMT,
+# an API wrapper for a collection of SMT solvers:
+# https://github.com/sosy-lab/java-smt
+#
+# SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+# #########################################
+#
+# INFO:
+# This script has to be used with the Yices2 and GMP installed as explained
+# below in Windows with Cygwin!
+#
+# #########################################
+# 
+# Information as to how to compile Yices2 for Windows: https://github.com/SRI-CSL/yices2/blob/master/doc/COMPILING
+# Information as to how to compile GMP for Windows for Yices2: https://github.com/SRI-CSL/yices2/blob/master/doc/GMP
+# Note: Cygwin is needed for compiliation, but the binary can be build in a way that it is not needed for execution.
+# 
+# Install Cygwin https://www.cygwin.com/
+# Note: choose to install "mingw64-x86_64-gcc-..." (at least core and g++), 
+#   "mingw64-x86_64-headers", "mingw64-x86_64-runtime", "gcc-core", "gcc-g++",
+#   "libgcc", "cmake", "bash", "m4" and "make", "automake", "autoconf2.1",
+#   "autoconf2.5", "autoconf" (the wrapper thingy), "libtool" and "gperf"
+# If you miss to install them, just restart the installation file and you can choose them.
+# 
+# It might be possible that you need to install MinGW first 
+# and the cross-compiler in Cygwin ("mingw64-x86_64-gcc-...") after that.
+# 
+# Install MinGW http://www.mingw.org
+# Note: Do not install MinGW in any location with spaces in the path name!
+# The preferred installation target directory is C:\MinGW
+# 
+# Yices2 needs the static and dynamic version of GMP 
+# and Windows doesn't allow both to be installed in the same dir, so we need to install it twice.
+# 
+# Building GMP(shared) 64:
+# 
+#     Download GMP https://gmplib.org/
+#     Switch to Cygwin
+# 
+#     Unzip/Untar your GMP download to a location ${gmp_build} with for example:
+#     cd ${gmp_build}
+#     tar -xf ${gmp_download}/gmp-x.x.x.tar.gz //for a tar.xz ball
+# 
+#     cd into/new/gmp/dir
+#     We need to set mingw64 as compiler. 
+#     CC NM and AR need to match your installed mingw (located at /usr/bin ).
+#     The --prefix is the install location. You can change it, but remember where you put it.
+# 
+#     ./configure --disable-static --enable-shared --prefix=/usr/tools/shared-gmp \
+#     --host=x86_64-pc-mingw32 --build=i686-pc-cygwin CC=/usr/bin/x86_64-w64-mingw32-gcc \
+#     NM=/usr/bin/x86_64-w64-mingw32-nm AR=/usr/bin/x86_64-w64-mingw32-ar CC_FOR_BUILD=gcc
+#
+#     make
+#     make check
+#     make install
+# 
+#     That should have "installed" the following files that we need:
+# 
+#     /usr/tools/static-gmp/bin/libgmp-10.dll (DLL)
+#     /usr/tools/static-gmp/lib/libgmp.dll.a (import library)
+#     /usr/tools/static-gmp/lib/libgmp.la (stuff used by libtool)
+#     /usr/tools/static-gmp/include/gmp.h
+# 
+# Building GMP (static) 32:
+# 
+#     Go back to the dir you Unzipped the tarball (same as shared)
+# 
+#     The following installs the static GMP to /tools/static_gmp but you can change that of course:
+#     You need to use "make clean" after a failed make or it might not configure correctly!
+#
+#     ./configure --disable-shared --enable-static --prefix=/usr/tools/static-gmp \
+#     --host=x86_64-pc-mingw32 --build=i686-pc-cygwin CC=/usr/bin/x86_64-w64-mingw32-gcc \
+#     NM=/usr/bin/x86_64-w64-mingw32-nm AR=/usr/bin/x86_64-w64-mingw32-ar CC_FOR_BUILD=gcc
+#
+#     make
+#     make check
+#     make install
+# 
+#     This should have installed:
+# 
+#     /usr/tools/static-gmp/lib/libgmp.a
+#     /usr/tools/static-gmp/include/gmp.h
+# 
+# 
+# Now we build Yices2 (The Yices2 documentation gives 2 options to configure yices2 here. I used the second.)
+#     You may need to edit the compiler etc. just like in step 5 + specify where you have installed your GMP
+#     (CPPFLAGS, LDFLAGS point to the shared GMP. with-static-gmp, with-static-gmp-include-dir point to the static GMP.
+#      On Windows a static GMP is also PIC per default.)
+#     After using configure you need to give 'OPTION=mingw64' to every make command. 
+#     (including make clean)
+#     adding "static-dist" linkds gmp statically into yices. This means that binaries etc. are in the build folders static_bin/ and no longer in bin/ in yices2.
+# 
+#     ./configure --build=x86_64-pc-mingw32 CC=/usr/bin/x86_64-w64-mingw32-gcc \
+#     LD=/usr/bin/x86_64-w64-mingw32-ld STRIP=/usr/bin/x86_64-w64-mingw32-strip \
+#     RANLIB=/usr/bin/x86_64-w64-mingw32-ranlib CPPFLAGS=-I/usr/tools/shared-gmp/include \
+#     LDFLAGS=-L/usr/tools/shared-gmp/lib --with-static-gmp=/usr/tools/static-gmp/lib/libgmp.a \
+#     --with-static-gmp-include-dir=/usr/tools/static-gmp/include --host=x86_64-w64-mingw32
+# 
+#     make static-dist OPTION=mingw64
+# 
+# Build the JNI wrapper dll:
+#     To build yices2 bindings: ./compileForWindows.sh $YICES_SRC_DIR $SHARED_GMP_SRC_DIR $STATIC_GMP_SRC_DIR $JNI_DIR
+#
+#  Note: You must change the line/file endings of this script on your Windows
+#        environment to Unix style so that you can run it in Cygwin
+#     
+#     After running the script, copy the libyices.dll from the Yices2 folder 
+#     (yices2/build/x86_64-unknown-mingw32-release/bin) and the libyices2j.dll 
+#     to java-smt\lib\native\x86_64-windows and/or publish it.
+# 
+
+
+SOURCE="${BASH_SOURCE[0]}"
+while [ -h "$SOURCE" ]; do # resolve $SOURCE until the file is no longer a symlink
+  DIR="$( cd -P "$( dirname "$SOURCE" )" && pwd )"
+  SOURCE="$(readlink "$SOURCE")"
+  [[ ${SOURCE} != /* ]] && SOURCE="$DIR/$SOURCE" # if $SOURCE was a relative symlink, we need to resolve it relative to the path where the symlink file was located
+done
+DIR="$( cd -P "$( dirname "$SOURCE" )" && pwd )"
+
+cd ${DIR}
+
+JNI_HEADERS="-I${JNI_DIR}/ -I${JNI_DIR}/win32/"
+
+YICES_SRC_DIR="$1"
+YICES_RLS_DIR="$1"/build/x86_64-unknown-mingw32-release
+
+SHARED_GMP_SRC_DIR="$2"
+STATIC_GMP_SRC_DIR="$2"
+
+JNI_DIR="$3"/include
+
+SRC_FILES="org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c"
+
+# check requirements
+if [ ! -f "$YICES_RLS_DIR/bin/libyices.dll" ]; then
+    echo "You need to specify the directory with the built yices2 on the command line!"
+    echo "Can not find $YICES_RLS_DIR/static_bin/libyices.dll"
+    exit 1
+fi
+if [ ! -f "$JNI_DIR/jni.h" ]; then
+    echo "You need to specify the directory with the downloaded JNI headers on the command line!"
+    echo "Can not find $JNI_DIR/jni.h"
+    exit 1
+fi
+
+OUT_FILE="libyices2j.dll"
+
+echo "Compiling the C wrapper code..."
+
+x86_64-w64-mingw32-gcc \
+    -D_JNI_IMPLEMENTATION_ -Wl,--kill-at $JNI_HEADERS \
+    -I$YICES_RLS_DIR/static_dist/include -L$YICES_RLS_DIR/static_lib -L. -I$STATIC_GMP_SRC_DIR/include -I. -Iincludes -I$SHARED_GMP_SRC_DIR/include \
+    -c org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c -o org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.o
+
+echo "Compilation Done"
+echo "Creating the \"$OUT_FILE\" library..."
+
+# This will compile the JNI wrapper part, given the JNI and the Yices2 header files
+x86_64-w64-mingw32-gcc -Wredundant-decls -Wno-format -O3 -fomit-frame-pointer -fno-stack-protector -Wall -g -o $OUT_FILE -shared -Wl,-soname,$OUT_FILE \
+  -Wl,--out-implib=$YICES_RLS_DIR/static_lib/libyices.dll.a -Wl,--no-undefined \
+  -L. -L$YICES_RLS_DIR/static_lib -L$SHARED_GMP_SRC_DIR/lib -L$STATIC_GMP_SRC_DIR/lib \
+  -I$SHARED_GMP_SRC_DIR/include org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.o -Wl,-Bdynamic -lyices $YICES_RLS_DIR/static_bin/libyices.dll \
+  -Wl,-Bstatic -static-libstdc++ -lstdc++ -lgmp -L$STATIC_GMP_SRC_DIR/lib -lm
+
+echo "Linking Done"
+echo "Reducing file size by dropping unused symbols..."
+# pwinthread is linked into yices2, but sometimes this doesn't work properly as it only links against symbols used by compile time not runtime!
+# You can try to not strip and if that doesn't work you need to add the --whole-archive flag to the linking process like so:
+#    -Wl,-Bstatic,--whole-archive 
+# Note that you should deactivate the flag after pwinthread with: -Wl,-Bdynamic (or -Wl,-Bstatic if you prefer to link statically but not the whole archive)
+echo "Note: If in the future multithread support fails, please refer to the compiliation script for help!"
+
+strip ${OUT_FILE}
+
+echo "Reduction Done"
+echo "All Done"
+
+echo "Please check the following dependencies that will be required at runtime by $OUT_FILE:"
+echo "(DLLs like 'kernel32' and 'msvcrt' are provided by Windows)"
+objdump -p $OUT_FILE | grep "DLL Name"

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

@@ -181,7 +181,7 @@ typedef void jvoid; // for symmetry to jint, jlong etc.
   out##num:
 
 #define FREE_INT_ARRAY_ARG(num) \
-  (*jenv)->ReleaseIntArrayElements(jenv, arg##num, m_arg##num, 0); \
+  (*jenv)->ReleaseIntArrayElements(jenv, arg##num, (jint *)m_arg##num, 0); \
   out##num:
 
 #define FREE_LONG_ARRAY_ARG(num) \
@@ -235,7 +235,7 @@ typedef void jvoid; // for symmetry to jint, jlong etc.
     throwException(jenv, "java/lang/IllegalArgumentException", msg); \
     return 0; \
   } \
-  return (long) retval; \
+  return (size_t) retval; \
 }
 
 #define POINTER_ARG_RETURN(num) \
@@ -309,7 +309,7 @@ typedef void jvoid; // for symmetry to jint, jlong etc.
   if (!(*jenv)->ExceptionCheck(jenv)) { \
     jretval = (*jenv)->NewIntArray(jenv, 2); \
     if(jretval != NULL){ \
-      (*jenv)->SetIntArrayRegion(jenv, jretval, 0, 2, yval); \
+      (*jenv)->SetIntArrayRegion(jenv, jretval, 0, 2, (jint *)yval); \
     } \
   } \
   return jretval; \
@@ -325,7 +325,7 @@ typedef void jvoid; // for symmetry to jint, jlong etc.
   if (!(*jenv)->ExceptionCheck(jenv)) { \
     jretval = (*jenv)->NewIntArray(jenv, sz); \
     if(jretval != NULL){ \
-      (*jenv)->SetIntArrayRegion(jenv, jretval, 0, sz, m_arg##num); \
+      (*jenv)->SetIntArrayRegion(jenv, jretval, 0, sz, (jint *)m_arg##num); \
     } \
   } \
   out: \

lib/native/source/yices2j/org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c

@@ -1143,7 +1143,7 @@ if ((*jenv)->ExceptionCheck(jenv)) {
 }
 jretval = (*jenv)->NewIntArray(jenv, sz);
 if (jretval != NULL) {
-  (*jenv)->SetIntArrayRegion(jenv, jretval, 0, sz, m_arg3);
+  (*jenv)->SetIntArrayRegion(jenv, jretval, 0, sz, (jint *)m_arg3);
 }
 out:
 free(m_arg3);

src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java

@@ -106,7 +106,6 @@
 import org.junit.Before;
 import org.junit.BeforeClass;
 import org.junit.Test;
-import org.sosy_lab.common.NativeLibraries;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.Model;
 
@@ -118,7 +117,7 @@ public class Yices2NativeApiTest {
   @BeforeClass
   public static void loadYices() {
     try {
-      NativeLibraries.loadLibrary("yices2j");
+      Yices2SolverContext.loadLibrary();
     } catch (UnsatisfiedLinkError e) {
       throw new AssumptionViolatedException("Yices2 is not available", e);
     }

src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java

@@ -14,6 +14,9 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_version;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_init;
 
+import com.google.common.annotations.VisibleForTesting;
+import com.google.common.collect.ImmutableList;
+import java.util.List;
 import java.util.Set;
 import org.sosy_lab.common.NativeLibraries;
 import org.sosy_lab.common.ShutdownNotifier;
@@ -49,7 +52,7 @@ public Yices2SolverContext(
   public static Yices2SolverContext create(
       NonLinearArithmetic pNonLinearArithmetic, ShutdownNotifier pShutdownManager) {
 
-    NativeLibraries.loadLibrary("yices2j");
+    loadLibrary();
 
     synchronized (Yices2SolverContext.class) {
       if (numLoadedInstances == 0) {
@@ -75,6 +78,35 @@ public static Yices2SolverContext create(
     return new Yices2SolverContext(manager, creator, booleanTheory, pShutdownManager);
   }
 
+  @VisibleForTesting
+  static void loadLibrary() {
+    loadLibrary(ImmutableList.of("yices2j"), ImmutableList.of("libyices", "libyices2j"));
+  }
+
+  /**
+   * This method loads the given library, depending on the operating system. Each list is applied in
+   * the given ordering.
+   */
+  private static void loadLibrary(List<String> linuxLibrary, List<String> windowsLibrary) {
+    // we try Linux first, and then Windows.
+    // TODO we could simply switch over the OS-name.
+    // TODO move this method upwards? more solvers could use it.
+    try {
+      for (String libraryName : linuxLibrary) {
+        NativeLibraries.loadLibrary(libraryName);
+      }
+    } catch (UnsatisfiedLinkError e1) {
+      try {
+        for (String libraryName : windowsLibrary) {
+          NativeLibraries.loadLibrary(libraryName);
+        }
+      } catch (UnsatisfiedLinkError e2) {
+        e1.addSuppressed(e2);
+        throw e1;
+      }
+    }
+  }
+
   @Override
   public String getVersion() {
     return String.format(