Using native solvers from a dependent Maven package

[jasper-vb]

I have two Maven packages: In project1 I use java-smt with native solvers (specifically Z3). I then install project1 to my local Maven repository, and use it in project2 (where I set up the solver context etc.).

When I run project1 directly, I can successfully create the solver context by following the method outlined in the Example-Maven-Project, i.e. copying the org.sosy_lab.common JAR and the native libraries to the same directory and setting the classpath there.

However, this fails when I create an uber-JAR (JAR with dependencies) using maven-shade-plugin and try to run that, or when I try to run project2. As far as I can tell, this happens because org.sosy_lab.common.NativeLibraries.loadLibrary() tries to find the native libraries in the directory of the org.sosy_lab.common JAR, or in java.library.path, and project2 doesn't have the native libraries copied to a dependency directory with the org.sosy_lab.common JAR.

Is there a way to get native solvers working with either uber-JARs or dependent packages?

---

Alternatively, is there some way to load the libraries from a custom path? Usually when I depend on a native library, I package it as a resource, extract that to a temporary file and then load it using System.loadLibrary() with the absolute path. I've tried doing that, but it seems that java-smt tries to load the native libraries again anyways (and fails). I've also tried extracting the libraries to a temporary directory and adding that to java.library.path, but adding library directories at runtime doesn't seem to work.

[ThomasHaas]

Towards the second solution: SolverContextFactory. I haven't tried it myself, but it seems you can pass a path (pLoader argument) to look for native libraries in custom locations.

[jasper-vb]

Thank you, that seems to work. For reference, this is my solution now:

Creating the SolverContext

public class Util {
  private static void loadLibrary(String library) {
    if (library.equals("z3") || library.equals("z3java")) {
      System.out.println("Loading library: " + library);
      String filename = System.mapLibraryName(library);
      int pos = filename.lastIndexOf('.');
      Path file;
      try {
        file = Files.createTempFile(filename.substring(0, pos), filename.substring(pos));
        file.toFile().deleteOnExit();
        try (var in = Util.class.getClassLoader().getResourceAsStream(filename);
            var out = Files.newOutputStream(file)) {
          in.transferTo(out);
        }
        System.load(file.toAbsolutePath().toString());
      } catch (IOException e) {
        throw new UnsatisfiedLinkError(e.getMessage());
      }
    } else {
      System.out.println("Loading other library: " + library);
      System.loadLibrary(library);
    }
  }

  public static SolverContext createSolverContext(Solvers solvers)
      throws InvalidConfigurationException {
    return SolverContextFactory.createSolverContext(Configuration.defaultConfiguration(),
        org.sosy_lab.common.log.LogManager.createNullLogManager(), ShutdownNotifier.createDummy(),
        solvers, Util::loadLibrary);
  }
}

pom.xml

  <build>
    <plugins>
      <plugin>
        <groupId>org.apache.maven.plugins</groupId>
        <artifactId>maven-dependency-plugin</artifactId>
        <version>3.1.1</version>
        <executions>
          <!-- "copy" renames the native dependencies from their internal Maven name to the normal
          library name -->
          <execution>
            <id>copy</id>
            <phase>initialize</phase>
            <goals>
              <goal>copy</goal>
            </goals>
          </execution>
        </executions>
        <configuration>
          <outputDirectory>${project.dependency.path}</outputDirectory>
          <overWriteReleases>true</overWriteReleases>
          <artifactItems>
            <artifactItem>
              <groupId>org.sosy-lab</groupId>
              <artifactId>javasmt-solver-z3</artifactId>
              <type>so</type>
              <classifier>libz3java</classifier>
              <destFileName>libz3java.so</destFileName>
            </artifactItem>
            <artifactItem>
              <groupId>org.sosy-lab</groupId>
              <artifactId>javasmt-solver-z3</artifactId>
              <type>so</type>
              <classifier>libz3</classifier>
              <destFileName>libz3.so</destFileName>
            </artifactItem>
          </artifactItems>
        </configuration>
      </plugin>
    </plugins>
    <resources>
      <resource>
        <directory>${project.dependency.path}</directory>
      </resource>
    </resources>
  </build>

This seems rather convoluted, though. Is there a better/intended way to do this?

[baierd]

When i created the Maven example i also tried to build an example with FAT-Jars and found it to be rather hard with the way we load libs. (In some cases is was even impossible) Since we have a use-case and an example now, we should take a look at how we can improve this in my opinion. @kfriedberger do you agree?

[kfriedberger]

I also thought about providing a fat JAR via Maven, depending on architecture (x64 vs arm64), operating system (Linux vs Windows vs MacOS) and licence (GPL-included vs non-GPL). This would make at least 6 fat JARs. Technically, this is no big issue, as long as a users does not include multiple fat JARs at once.

We would need to provide:

• a small wrapper class for the loading mechanism that extracts the native library from JAR and loads them.
• a Maven package and upload task as configuration for Ant.
• testing.