Merge pull request #426 from sosy-lab/update-openSMT-to-2.8

Update OpenSMT to version 2.8.0

Author: kfriedberger

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

@@ -39,9 +39,9 @@ SPDX-License-Identifier: Apache-2.0
         <echo message="Building OpenSMT in version '${opensmt.version}'"/>
 
         <!-- Create build directories -->
-        <property name="path.build"   value="${opensmt.path}/build"/>
+        <property name="path.build" value="${opensmt.path}/build"/>
         <property name="path.install" value="${opensmt.path}/install"/>
-        <property name="path.source"  value="${user.dir}/lib/native/source/opensmt"/>
+        <property name="path.source" value="${user.dir}/lib/native/source/opensmt"/>
 
         <mkdir dir="${path.build}"/>
         <mkdir dir="${path.install}"/>
@@ -71,13 +71,10 @@ SPDX-License-Identifier: Apache-2.0
         </exec>
 
         <!-- Copy swig files to the install directory -->
-        <copy todir="${path.install}" >
-          <fileset dir="${path.source}" includes="**"/>
+        <copy todir="${path.install}">
+            <fileset dir="${path.source}" includes="swig/**/*"/>
         </copy>
 
-        <!-- Dump ${opensmt.version} to a file so that we can use it from swig -->
-        <echo file="${path.install}/Version.h">#define VERSION "${opensmt.version}"</echo>
-
         <!-- Run swig to generate java proxies and the jni wrapper -->
         <mkdir dir="${path.install}/java/opensmt"/>
         <exec executable="swig" dir="${path.install}" failonerror="true">
@@ -93,8 +90,7 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="swig/opensmt.i"/>
         </exec>
 
-        <!-- Copy (only!) the required java files to the source tree. This should make sure that compilation fails
-             if the OpenSMT interface changed, but the swig header wasn't updated  -->
+        <!-- Copy the generated Java classes and the c++ wrapper to the source tree  -->
         <copy todir="${path.source}/src/org/sosy_lab/java_smt/solvers/opensmt/api">
             <fileset dir="${path.install}/java/opensmt">
                 <include name="ArithLogic.java"/>
@@ -124,6 +120,13 @@ SPDX-License-Identifier: Apache-2.0
                 <include name="VectorVectorInt.java"/>
             </fileset>
         </copy>
+        <copy file="${path.install}/opensmt-wrap.cpp" toFile="${path.source}/opensmt-wrap.cpp"/>
+
+        <!-- Apply the patch to add the license headers -->
+        <exec executable="git" failonerror="true">
+            <arg value="apply"/>
+            <arg value="${path.source}/swigWrapper.patch"/>
+        </exec>
 
         <!-- Package swig generated source code -->
         <jar destfile="opensmt-${opensmt.version}-sources.jar" basedir="${path.source}/src"/>
@@ -134,35 +137,39 @@ SPDX-License-Identifier: Apache-2.0
         <jar destfile="opensmt-${opensmt.version}-javadoc.jar" basedir="${path.source}/doc"/>
         <delete dir="${path.source}/doc"/>
 
-        <!-- Copy the lib to the root directory for later packaging-->
-        <copy file="${path.install}/lib/libopensmt.so" toFile="libopensmt-${opensmt.version}.so"/>
+        <!-- Dump ${opensmt.version} to a file so that we can use it for the swig wrapper -->
+        <echo file="${path.source}/version.h">#define VERSION "${opensmt.version}"</echo>
 
-        <!-- Compile the wrapper and move the object file the source tree -->
-        <exec executable="gcc" dir="${path.install}" failonerror="true">
+        <!-- Compile the swig wrapper to create the library -->
+        <exec executable="gcc" dir="${path.source}" failonerror="true">
             <arg value="-fPIC"/>
-            <arg value="-std=c++17"/>
+            <arg value="-std=c++20"/>
             <arg value="-o"/>
-            <arg value="${path.source}/opensmt-wrap.o"/>
+            <arg value="opensmt-wrap.o"/>
             <arg value="-c"/>
             <arg value="opensmt-wrap.cpp"/>
+            <arg value="-I${path.install}/include/opensmt/"/>
             <arg value="-I${java.home}/include/"/>
             <arg value="-I${java.home}/include/linux"/>
         </exec>
+        <delete file="${path.source}/version.h"/>
 
         <!-- Link the wrapper and create a new lib -->
-        <symlink link="libopensmt.so" resource="libopensmt-${opensmt.version}.so"/>
         <exec executable="gcc" dir="${path.source}" failonerror="true">
             <arg value="-shared"/>
             <arg value="-o"/>
             <arg value="${user.dir}/libopensmtjava-${opensmt.version}.so"/>
             <arg value="opensmt-wrap.o"/>
-            <arg value="-L${user.dir}"/>
-            <arg value="-lopensmt"/>
             <arg value="-lstdc++"/>
-            <arg value="-l:libgmp.a"/>
+            <arg value="-Wl,--whole-archive"/>
+            <arg value="/dependencies/gmp-6.2.1/.libs/libgmp.a"/>
+            <arg value="/dependencies/gmp-6.2.1/.libs/libgmpxx.a"/>
+            <arg value="${path.install}/lib/libopensmt.a"/>
+            <arg value="-Wl,--no-whole-archive"/>
+            <arg value="-lm"/>
+            <arg value="-Wl,-z,defs"/>
         </exec>
-        <delete file="libopensmt.so"/>
-        <delete file="lib/native/source/opensmt/opensmt-wrap.o"/>
+        <delete file="${path.source}/opensmt-wrap.o"/>
 
         <!-- Compile java proxies and create jar file -->
         <mkdir dir="${path.source}/bin"/>
@@ -171,12 +178,10 @@ SPDX-License-Identifier: Apache-2.0
         </javac>
         <jar destfile="opensmt-${opensmt.version}.jar" basedir="${path.source}/bin"/>
         <delete dir="${path.source}/bin"/>
-        <delete dir="lib/native/source/opensmt/src"/>
     </target>
 
-    <target name="publish-opensmt" depends="package-opensmt, load-ivy"
-        description="Publish OpenSMT binaries to Ivy repository.">
-        <ivy:resolve conf="solver-opensmt" file="solvers_ivy_conf/ivy_opensmt.xml" />
+    <target name="publish-opensmt" depends="package-opensmt, load-ivy" description="Publish OpenSMT binaries to Ivy repository.">
+        <ivy:resolve conf="solver-opensmt" file="solvers_ivy_conf/ivy_opensmt.xml"/>
         <publishToRepository solverName="OpenSMT" solverVersion="${opensmt.version}"/>
     </target>
 </project>

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

@@ -114,16 +114,17 @@ Finally, follow the instructions shown in the message at the end.
 
 ### Publishing OpenSMT
 
-We prefer/need to compile our own OpenSMT2 binaries and Java bindings.
+We prefer/need to compile our own OpenSMT2 binaries and Java bindings on Ubuntu 22.04 or later.
 For simple usage, we provide a Docker definition/environment under `/docker`,
 in which the following command can be run.
 
-Download [OpenSMT](https://github.com/usi-verification-and-security/opensmt) using Git into a
-file of your choice. The following command patches the OpenSMT2 API, generates Java bindings
+Download [OpenSMT](https://github.com/usi-verification-and-security/opensmt) using Git and
+checkout the required version, e.g., the tag "v2.8.0".
+The following command patches the OpenSMT2 API, generates Java bindings
 with SWIG, builds the library, and packages it.
 
 ```
-ant publish-opensmt -Dopensmt.path=/workspace/opensmt -Dopensmt.customRev=2.5.2
+ant publish-opensmt -Dopensmt.path=/workspace/opensmt -Dopensmt.customRev=2.8.0
 ```
 Then upload the binaries to the Ivy repository using SVN as described in the message on the screen.
 

doc/Example-Maven-Project/pom.xml

@@ -248,21 +248,14 @@ SPDX-License-Identifier: Apache-2.0
       <classifier>libyices2j</classifier>
     </dependency>
 
-    <!-- OpenSMT has three dependencies (on Linux) -->
+    <!-- OpenSMT has two dependencies (on Linux) -->
     <dependency>
       <groupId>org.sosy-lab</groupId>
       <artifactId>javasmt-solver-opensmt</artifactId>
       <version>${opensmt.version}</version>
       <type>jar</type>
       <classifier>opensmt</classifier>
     </dependency>
-    <dependency>
-      <groupId>org.sosy-lab</groupId>
-      <artifactId>javasmt-solver-opensmt</artifactId>
-      <version>${opensmt.version}</version>
-      <type>so</type>
-      <classifier>libopensmt</classifier>
-    </dependency>
     <dependency>
       <groupId>org.sosy-lab</groupId>
       <artifactId>javasmt-solver-opensmt</artifactId>
@@ -498,13 +491,6 @@ SPDX-License-Identifier: Apache-2.0
                 <classifier>libopensmtjava</classifier>
                 <destFileName>libopensmtjava.so</destFileName>
               </artifactItem>
-              <artifactItem>
-                <groupId>org.sosy-lab</groupId>
-                <artifactId>javasmt-solver-opensmt</artifactId>
-                <type>so</type>
-                <classifier>libopensmt</classifier>
-                <destFileName>libopensmt.so</destFileName>
-              </artifactItem>
             </artifactItems>
           </configuration>
       </plugin>

doc/Example-Maven-Web-Project/pom.xml

@@ -249,21 +249,14 @@ SPDX-License-Identifier: Apache-2.0
       <classifier>libyices2j</classifier>
     </dependency>
 
-    <!-- OpenSMT has three dependencies (on Linux) -->
+    <!-- OpenSMT has two dependencies (on Linux) -->
     <dependency>
       <groupId>org.sosy-lab</groupId>
       <artifactId>javasmt-solver-opensmt</artifactId>
       <version>${opensmt.version}</version>
       <type>jar</type>
       <classifier>opensmt</classifier>
     </dependency>
-    <dependency>
-      <groupId>org.sosy-lab</groupId>
-      <artifactId>javasmt-solver-opensmt</artifactId>
-      <version>${opensmt.version}</version>
-      <type>so</type>
-      <classifier>libopensmt</classifier>
-    </dependency>
     <dependency>
       <groupId>org.sosy-lab</groupId>
       <artifactId>javasmt-solver-opensmt</artifactId>
@@ -334,7 +327,6 @@ SPDX-License-Identifier: Apache-2.0
                   <include>libpoly.so</include>
                   <include>libpolyxx.so</include>
                   <include>libyices2j.so</include>
-                  <include>libopensmt.so</include>
                   <include>libopensmtjava.so</include>
                 </includes>
                 <targetPath>WEB-INF/lib</targetPath>
@@ -545,13 +537,6 @@ SPDX-License-Identifier: Apache-2.0
               <classifier>libopensmtjava</classifier>
               <destFileName>libopensmtjava.so</destFileName>
             </artifactItem>
-            <artifactItem>
-              <groupId>org.sosy-lab</groupId>
-              <artifactId>javasmt-solver-opensmt</artifactId>
-              <type>so</type>
-              <classifier>libopensmt</classifier>
-              <destFileName>libopensmt.so</destFileName>
-            </artifactItem>
           </artifactItems>
         </configuration>
       </plugin>

lib/ivy.xml

@@ -169,7 +169,7 @@ SPDX-License-Identifier: Apache-2.0
         <!-- Solver Binaries -->
         <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.11-glibc2.27" conf="runtime-mathsat->solver-mathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.13.0" conf="runtime-z3->solver-z3; contrib->sources,javadoc" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.6.0-g2f72cc0e" conf="runtime-opensmt->solver-opensmt; contrib->sources,javadoc" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.8.0-ge831bf23" conf="runtime-opensmt->solver-opensmt; contrib->sources,javadoc"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.1-sosy0" 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" />