Update OpenSMT to 2.9.0 and include support for proofs in the JNI bindings

build.xml

@@ -87,7 +87,7 @@ SPDX-License-Identifier: Apache-2.0
             <fileset dir="." includes="${libraryFiles} ${jarFiles} Javadoc-z3/"/>
             <fileset dir="lib/native/source/libmathsat5j" includes="*.so *.dll *.o"/>
             <fileset dir="lib/native/source/libbitwuzla" includes="install-linux/ install-linux-x64/ install-linux-arm64/ install-windows/ install-windows-x64/ build/ doc/ *.so *.dll bitwuzla_wrap.o"/>
-            <fileset dir="lib/native/source/opensmt" includes="install-linux-x64/ install-linux-arm64/ *.so"/>
+            <fileset dir="lib/native/source/opensmt" includes="build/ doc/ install-linux-x64/ install-linux-arm64/ *.o *.so version.h"/>
         </delete>
     </target>
 

build/build-publish-solvers/solver-opensmt.xml

@@ -20,19 +20,12 @@ SPDX-License-Identifier: Apache-2.0
     <target name="set-properties-for-opensmt">
         <checkPathOption pathOption="opensmt.path" defaultPath="/path/to/opensmt" targetName="OpenSMT source folder (git checkout from 'https://github.com/usi-verification-and-security/opensmt.git)"/>
 
-        <!--
-            Please provide GMP from http://gmplib.org/ in version 6.3.0 (version 6.2.1 also works) and build GMP:
-            For linux-x64:
-                ./configure -?-enable-cxx -?-with-pic -?-disable-shared -?-enable-static -?-enable-fat
-                make -j4
-            For linux-arm64:
-                ./configure -?-enable-cxx -?-with-pic -?-disable-shared -?-enable-static -?-enable-fat \
-                     -?-host=aarch64-linux-gnu \
-                     CC=aarch64-linux-gnu-gcc CXX=aarch64-linux-gnu-g++ LD=aarch64-linux-gnu-ld
-                make -j4
-        -->
-        <checkPathOption pathOption="gmp-linux-x64.path" defaultPath="/path/to/gmp" targetName="GMP directory (Linux x64)"/>
-        <checkPathOption pathOption="gmp-linux-arm64.path" defaultPath="/path/to/gmp" targetName="GMP directory (Linux arm64)"/>
+        <!-- Define paths to the GMP installation for x86 and arm64
+             When using the docker image the files are already included and can be found under
+             /dependencies/gmp-6.2.1/install -->
+        <checkPathOption pathOption="gmp-linux-x64.path" defaultPath="/path/to/gmp" targetName="GMP installation directory (Linux x64)"/>
+        <checkPathOption pathOption="gmp-linux-arm64.path" defaultPath="/path/to/gmp" targetName="GMP installation directory (Linux arm64)"/>
+
         <checkPathOption pathOption="jdk-linux-arm64.path" defaultPath="/path/to/jdk" targetName="JDK source folder (Linux arm64 version)"/>
 
         <fail unless="opensmt.customRev">
@@ -76,12 +69,17 @@ SPDX-License-Identifier: Apache-2.0
         </exec>
 
         <!-- Build OpenSMT,
-                     Make sure to remove the old 'build/' directory from OpenSMT!
-                     It keeps old build commands and previous cmake-flags. -->
+             Make sure to remove the old 'build/' directory from OpenSMT!
+             It keeps old build commands and previous cmake-flags. -->
         <delete dir="${opensmt.path}/build" quiet="true"/>
-        <exec executable="make" dir="${opensmt.path}" failonerror="true">
+        <exec executable="make" dir="${opensmt.path}" failonerror="false" resultproperty="build.returnCode">
             <arg value="INSTALL_DIR=${opensmt.installPath}"/>
-            <arg value="CMAKE_FLAGS=-DFORCE_STATIC_GMP=ON"/>
+            <!-- The next arg is ONE large parameter. If executed manually outside of ant, please wrap it in quotes. -->
+            <arg value="CMAKE_FLAGS=
+              -DFORCE_STATIC_GMP=ON
+              -DGMP_LIBRARY=${gmp-linux-x64.path}/lib/libgmp.a
+              -DGMPXX_LIBRARY=${gmp-linux-x64.path}/lib/libgmpxx.a
+              -DGMP_INCLUDE_DIR=${gmp-linux-x64.path}/include"/>
             <arg value="install"/>
         </exec>
 
@@ -92,6 +90,15 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="${source.path}/api.patch"/>
         </exec>
 
+        <!-- Abort if the build failed -->
+        <fail message="Failed to build OpenSMT">
+            <condition>
+                <not>
+                    <equals arg1="0" arg2="${build.returnCode}"/>
+                </not>
+            </condition>
+        </fail>
+
         <!-- copy OpenSMT include files to JavaSMT -->
         <copy todir="${source.installPathLinuxX64}">
             <fileset dir="${opensmt.installPath}"/>
@@ -112,10 +119,16 @@ SPDX-License-Identifier: Apache-2.0
              Make sure to remove the old 'build/' directory from OpenSMT!
              It keeps old build commands and previous cmake-flags. -->
         <delete dir="${opensmt.path}/build" quiet="true"/>
-        <exec executable="make" dir="${opensmt.path}" failonerror="true">
+        <exec executable="make" dir="${opensmt.path}" failonerror="false" resultproperty="build.returnCode">
             <arg value="INSTALL_DIR=${opensmt.installPath}"/>
             <!-- The next arg is ONE large parameter. If executed manually outside of ant, please wrap it in quotes. -->
-            <arg value="CMAKE_FLAGS=-DFORCE_STATIC_GMP=ON -DCMAKE_C_COMPILER=aarch64-linux-gnu-gcc -DCMAKE_CXX_COMPILER=aarch64-linux-gnu-g++ -DGMP_LIBRARY=${gmp-linux-arm64.path}/.libs/libgmp.a -DGMPXX_LIBRARY=${gmp-linux-arm64.path}/.libs/libgmpxx.a -DGMP_INCLUDE_DIR=${gmp-linux-arm64.path}"/>
+            <arg value="CMAKE_FLAGS=
+              -DFORCE_STATIC_GMP=ON
+              -DCMAKE_C_COMPILER=aarch64-linux-gnu-gcc
+              -DCMAKE_CXX_COMPILER=aarch64-linux-gnu-g++
+              -DGMP_LIBRARY=${gmp-linux-arm64.path}/lib/libgmp.a
+              -DGMPXX_LIBRARY=${gmp-linux-arm64.path}/lib/libgmpxx.a
+              -DGMP_INCLUDE_DIR=${gmp-linux-arm64.path}/include"/>
             <arg value="install"/>
         </exec>
 
@@ -126,6 +139,15 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="${source.path}/api.patch"/>
         </exec>
 
+        <!-- Abort if the build failed -->
+        <fail message="Failed to build OpenSMT">
+            <condition>
+                <not>
+                    <equals arg1="0" arg2="${build.returnCode}"/>
+                </not>
+            </condition>
+        </fail>
+
         <!-- copy OpenSMT include files to JavaSMT -->
         <copy todir="${source.installPathLinuxArm64}">
             <fileset dir="${opensmt.installPath}"/>
@@ -198,7 +220,7 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="-I${source.installPathLinuxX64}/include/opensmt"/>
             <arg value="-I${java.home}/include"/>
             <arg value="-I${java.home}/include/linux"/>
-            <arg value="-I${gmp-linux-x64.path}"/>
+            <arg value="-I${gmp-linux-x64.path}/include"/>
         </exec>
 
         <!-- link the wrapper to create libopensmtj-x64.so -->
@@ -216,7 +238,7 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="libopensmtj-x64.so"/>
             <arg value="opensmt-wrap.o"/>
             <arg value="-L${source.installPathLinuxX64}/lib"/>
-            <arg value="-L${gmp-linux-x64.path}/.libs"/>
+            <arg value="-L${gmp-linux-x64.path}/lib"/>
             <arg value="-Wl,-Bstatic"/>
             <arg value="-lopensmt"/>
             <arg value="-lgmpxx"/>
@@ -246,7 +268,7 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="-I${source.installPathLinuxArm64}/include/opensmt"/>
             <arg value="-I${jdk-linux-arm64.path}/include"/>
             <arg value="-I${jdk-linux-arm64.path}/include/linux"/>
-            <arg value="-I${gmp-linux-arm64.path}"/>
+            <arg value="-I${gmp-linux-arm64.path}/include"/>
         </exec>
 
         <!-- link the wrapper to create libopensmtj-arm64.so -->
@@ -264,7 +286,7 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="libopensmtj-arm64.so"/>
             <arg value="opensmt-wrap.o"/>
             <arg value="-L${source.installPathLinuxArm64}/lib"/>
-            <arg value="-L${gmp-linux-arm64.path}/.libs"/>
+            <arg value="-L${gmp-linux-arm64.path}/lib"/>
             <arg value="-Wl,-Bstatic"/>
             <arg value="-lopensmt"/>
             <arg value="-lgmpxx"/>

doc/Developers-How-to-Release-into-Ivy.md

@@ -156,6 +156,9 @@ Please provide GMP from http://gmplib.org/ in version 6.3.0 (version 6.2.1 also
   make -j4
   ```
 
+When using the docker container GMP is already included and can be found
+under `/dependencies/gmp-6.2.1/install` for `x64-linux` and `arm64-linux`.
+
 For linux-arm64, provide JNI headers in a reasonable LTS version.
 Download the zip archive from https://jdk.java.net/ and unpack it into $JDK_DIR_LINUX_ARM64
 (e.g., https://download.java.net/java/GA/jdk17.0.2/dfd4a8d0985749f896bed50d7138ee7f/8/GPL/openjdk-17.0.2_linux-aarch64_bin.tar.gz).
@@ -182,7 +185,7 @@ ant publish-opensmt \
 The build scripts for OpenSMT ... :
 - run for about 20 minutes (we build everything from scratch, two times).
 - download Google-based test components (requires internet access).
-- append the git revision of Bitwuzla.
+- append the git revision of OpenSMT.
 - produce two Linux (x64 and arm64) libraries, and publish them.
 
 Finally, follow the instructions shown in the message at the end of the command.

docker/ubuntu1804.Dockerfile

@@ -56,31 +56,58 @@ RUN pip3 install --upgrade meson
 # OpenSMT requires swig, gmp, flex and bison
 # - swig needs to built manually to get version 4.1 for unique_ptr support
 # - libpcre2-dev is a dependency of swig
-# - gmp needs to be recompiled to generate PIC code
+# - gmp needs to be recompiled to generate PIC code (see below)
 # - lzip is required to unpack the gmp tar ball
 RUN apt-get update \
  && apt-get install -y \
         flex bison libpcre2-dev lzip \
  && apt-get clean
 
 WORKDIR /dependencies
+
+# Install SWIG in a recent enough version
 RUN wget http://prdownloads.sourceforge.net/swig/swig-4.1.1.tar.gz \
  && tar xf swig-4.1.1.tar.gz \
+ && rm swig-4.1.1.tar.gz \
  && cd swig-4.1.1 \
  && ./configure \
  && make -j4 \
  && make install \
- && rm -rf swig-4.1.1.tar.gz swig-4.1.1 \
- && cd --
+ && cd .. \
+ && rm -rf swig-4.1.1
 
+# Install GMP for linux on x64 and arm64
+# We could add another build for windows when needed
 RUN wget https://gmplib.org/download/gmp/gmp-6.2.1.tar.lz \
  && tar xf gmp-6.2.1.tar.lz \
+ && rm gmp-6.2.1.tar.lz \
  && cd gmp-6.2.1 \
- && ./configure --enable-cxx --with-pic --disable-shared --enable-fat \
+ && ./configure \
+      --enable-cxx \
+      --with-pic \
+      --disable-shared \
+      --enable-fat \
+      --prefix=/dependencies/gmp-6.2.1/install/x64-linux \
  && make -j4 \
  && make install \
- && rm -rf gmp-6.2.1.tar.lz gmp-6.2.1 \
- && cd --
+ && make clean \
+ && ./configure \
+      --enable-cxx \
+      --with-pic \
+      --disable-shared \
+      --enable-fat \
+      --host=aarch64-linux-gnu \
+      --prefix=/dependencies/gmp-6.2.1/install/arm64-linux \
+ && CC=aarch64-linux-gnu-gcc CXX=aarch64-linux-gnu-g++ LD=aarch64-linux-gnu-ld make -j4 \
+ && make install \
+ && make clean
+
+# Install the Jdk for Windows x64
+# Builds for arm64 are only available with an Oracle account and have to be downloaded manually
+RUN wget https://download.java.net/openjdk/jdk11/ri/openjdk-11+28_windows-x64_bin.zip \
+ && unzip openjdk-11+28_windows-x64_bin.zip \
+ && mv jdk-11 jdk11-windows-x64 \
+ && rm openjdk-11+28_windows-x64_bin.zip
 
 # JNI is not found when compiling Boolector in the image, so we need to set JAVA_HOME
 ENV JAVA_HOME=/usr/lib/jvm/java-11-openjdk-amd64/

docker/ubuntu2204.Dockerfile

@@ -51,34 +51,57 @@ RUN pip3 install --upgrade meson
 # OpenSMT requires swig, gmp, flex and bison
 # - swig needs to built manually to get version 4.1 for unique_ptr support
 # - libpcre2-dev is a dependency of swig
-# - gmp needs to be recompiled to generate PIC code
+# - gmp needs to be recompiled to generate PIC code (see below)
 # - lzip is required to unpack the gmp tar ball
 RUN apt-get update \
  && apt-get install -y \
         flex bison libpcre2-dev lzip \
  && apt-get clean
 
 WORKDIR /dependencies
+
+# Install SWIG in a recent enough version
 RUN wget http://prdownloads.sourceforge.net/swig/swig-4.1.1.tar.gz \
  && tar xf swig-4.1.1.tar.gz \
+ && rm swig-4.1.1.tar.gz \
  && cd swig-4.1.1 \
  && ./configure \
  && make -j4 \
  && make install \
- && rm -rf swig-4.1.1.tar.gz swig-4.1.1 \
- && cd --
+ && cd .. \
+ && rm -rf swig-4.1.1
 
+# Install GMP for linux on x64 and arm64
+# We could add another build for windows when needed
 RUN wget https://gmplib.org/download/gmp/gmp-6.2.1.tar.lz \
  && tar xf gmp-6.2.1.tar.lz \
+ && rm gmp-6.2.1.tar.lz \
  && cd gmp-6.2.1 \
- && ./configure --enable-cxx --with-pic --disable-shared --enable-fat \
+ && ./configure \
+      --enable-cxx \
+      --with-pic \
+      --disable-shared \
+      --enable-fat \
+      --prefix=/dependencies/gmp-6.2.1/install/x64-linux \
  && make -j4 \
  && make install \
- && rm -rf gmp-6.2.1.tar.lz gmp-6.2.1 \
- && cd --
+ && make clean \
+ && ./configure \
+      --enable-cxx \
+      --with-pic \
+      --disable-shared \
+      --enable-fat \
+      --host=aarch64-linux-gnu \
+      --prefix=/dependencies/gmp-6.2.1/install/arm64-linux \
+ && CC=aarch64-linux-gnu-gcc CXX=aarch64-linux-gnu-g++ LD=aarch64-linux-gnu-ld make -j4 \
+ && make install \
+ && make clean
 
+# Install the Jdk for Windows x64
+# Builds for arm64 are only available with an Oracle account and have to be downloaded manually
 RUN wget https://download.java.net/openjdk/jdk11/ri/openjdk-11+28_windows-x64_bin.zip \
  && unzip openjdk-11+28_windows-x64_bin.zip \
+ && mv jdk-11 jdk11-windows-x64 \
  && rm openjdk-11+28_windows-x64_bin.zip
 
 # JNI is not found when compiling Boolector in the image, so we need to set JAVA_HOME

lib/ivy.xml

@@ -188,7 +188,7 @@ SPDX-License-Identifier: Apache-2.0
         <!-- Solver Binaries -->
         <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.11-sosy1" conf="runtime-mathsat-x64->solver-mathsat-x64; runtime-mathsat-arm64->solver-mathsat-arm64" />
         <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.14.0" conf="runtime-z3-x64->solver-z3-x64; runtime-z3-arm64->solver-z3-arm64; contrib->sources,javadoc" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.8.0-sosy0-ge831bf23" conf="runtime-opensmt-x64->solver-opensmt-x64; runtime-opensmt-arm64->solver-opensmt-arm64; contrib->sources,javadoc"/>
+        <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.9.0-gef441e1c" conf="runtime-opensmt-x64->solver-opensmt-x64; runtime-opensmt-arm64->solver-opensmt-arm64; contrib->sources,javadoc"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.3-sosy1" conf="runtime-optimathsat->solver-optimathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.0.5-g4cb2ab9eb" conf="runtime-cvc5->solver-cvc5" />