Z3 JNI library fails to load in Eclipse PDE environment

[gravemalte]

When using JavaSMT with Z3 in an Eclipse PDE launch environment, the solver fails to initialize with the following exception:

org.sosy_lab.common.configuration.InvalidConfigurationException: The SMT solver Z3 is not available on this machine because of missing libraries ('long com.microsoft.z3.Native.INTERNALmkConfig()')..

Caused by: java.lang.UnsatisfiedLinkError: 'long com.microsoft.z3.Native.INTERNALmkConfig()' at com.microsoft.z3.Native.INTERNALmkConfig(Native Method) at com.microsoft.z3.Native.mkConfig(Native.java:895)

Steps to reproduce:

1. Create an Eclipse plugin project.
2. Include all necessary dependencies for JavaSMT and Z3.
3. Include the native library bundle containing:
   • libz3.so
   • libz3java.so
4. Launch the product via PDE (Run As → Eclipse Application) with a VM argument pointing to the bundle containing the native libs
5. Attempt to create a solver context:

SolverContext context = SolverContextFactory.createSolverContext(SolverContextFactory.Solvers.Z3);

6. Observe an exception throw:

org.sosy_lab.common.configuration.InvalidConfigurationException: The SMT solver Z3 is not available on this machine because of missing libraries ('long com.microsoft.z3.Native.INTERNALmkConfig()')..
...
Caused by: java.lang.UnsatisfiedLinkError: 'long com.microsoft.z3.Native.INTERNALmkConfig()' at com.microsoft.z3.Native.INTERNALmkConfig(Native Method) at com.microsoft.z3.Native.mkConfig(Native.java:895)

JavaSMT can't create the solver even though the native .so files are present and visible in /proc/<YOURPID>/maps or cat /proc/$(pgrep -f eclipse)/maps | grep z3.

When running the Eclipse PDE with LD_DEBUG=bindings you get the following output:

121431: /usr/lib/jvm/java-21-openjdk/bin/java: error: symbol lookup error: undefined symbol: JNI_OnLoad_z3 (fatal) 
121431: /usr/lib/jvm/java-21-openjdk/bin/java: error: symbol lookup error: undefined symbol: JNI_OnLoad_z3 (fatal) 
121431: /home/.../z3.bundle/lib/libz3.so: error: symbol lookup error: undefined symbol: JNI_OnLoad (fatal)

What's interesting here is, that JavaSMT tries to load an JNI symbol JNI_OnLoad in the libz3.so first, before loading libz3java.so (where the symbol is defined).

When using Z3 without JavaSMT (exactly the same setup but using the com.microsoft.z3.* API) everything works as expected.
I suspect a load issue where the libz3.so is first loaded before the libz3java.so.

I think the issue is how the common-lib does the library loading here: https://github.com/sosy-lab/java-common-lib/blob/main/src/org/sosy_lab/common/NativeLibraries.java#L174

[daniel-raffler]

Hello Malte
If you're having issues with the NativeLibraries loader you could try using System.loadLibrary:

SolverContext context =
        SolverContextFactory.createSolverContext(Configuration.defaultConfiguration(),
            LogManager.createNullLogManager(),
            ShutdownNotifier.createDummy(),
            SolverContextFactory.Solvers.Z3,
            System::loadLibrary);

This should find the binaries as long as they have been included in LD_LIBRARY_PATH. The NativeLibrary loader expects the binaries to be in the same folder as the common-lib .jar (or in a folder ../native/<arch>-<os>/ relative to the .jar file of the common-lib library)

[gravemalte]

Hi @daniel-raffler thanks for your answer. I already tried to provide a custom Consumer<String> loader using System.loadLibrary(...) internally. But I had the same problem, I will try tomorrow with your proposed lambda expression.

A question that I have, could System.setProperty("z3.skipLibraryLoad", "true"); (in https://github.com/sosy-lab/java-smt/blob/master/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java#L131C4-L131C54) cause the problem in the Eclipse OSGI context?

[gravemalte]

I tried your proposed solution, but unfortunately what I expected.

Caused by: java.lang.UnsatisfiedLinkError: 'long com.microsoft.z3.Native.INTERNALmkConfig()'
	at com.microsoft.z3.Native.INTERNALmkConfig(Native Method)
	at com.microsoft.z3.Native.mkConfig(Native.java:885)
	at org.sosy_lab.java_smt.solvers.z3.Z3SolverContext.create(Z3SolverContext.java:143)
	at org.sosy_lab.java_smt.SolverContextFactory.generateContext0(SolverContextFactory.java:283)
	at org.sosy_lab.java_smt.SolverContextFactory.generateContext(SolverContextFactory.java:214)

I would like to test it with setting z3.skipLibraryLoad to false but I can't because it's always set to true in Z3SolverContext create(...).

[gravemalte]

Update:

I hacked the library a bit. So I commented out

loadLibrariesWithFallback(pLoader, ImmutableList.of("z3", "z3java"), ImmutableList.of("libz3", "libz3java"));

Because it never found the libz3java.so lib, even it is in my java.library.path. I also set the z3.skipLibraryLoad to false. After that, I firstly load up z3 with the com.microsoft.z3.* API and after that, JavaSMT is able to find it. But this is very hacky. And its only happening in the OSGi context. "Normal" jar applications run just fine with JavaSMT.

[gravemalte]

I have a bug fix that works for the Eclipse PDE platform. @daniel-raffler please tell if it's appropriate for the java-smt project.

if(System.getProperty("z3.skipLibraryLoad") == null){
    loadLibrariesWithFallback(
        pLoader, ImmutableList.of("z3", "z3java"), ImmutableList.of("libz3", "libz3java"));

    // disable Z3's own loading mechanism, see com.microsoft.z3.Native
    System.setProperty("z3.skipLibraryLoad", "true");
}

That way, the user can specify if the library loading mechanism should be skipped. It's necessary in the OSGi context. I still dont know why, I guess I have to dig into the OSGi loader for that.

[baierd]

Sorry for the late reply.

We disable Z3s loading mechanism in JavaSMT, as it only loads libz3java, but not libz3. Hence when we try to load everything ourselves.

Which Z3 version did you use? Did you compile it yourself, or did you use one of our binaries?

Where are the binaries located, i.e. is the default path chosen by Ivy correct?
If not, you need to provide a custom loader that resolves the path to your binaries.

Maybe @PhilippWendler or @kfriedberger know more about OSGi, as they use Eclipse AFAIK.

[gravemalte]

Sorry for the late reply.

We disable Z3s loading mechanism in JavaSMT, as it only loads libz3java, but not libz3. Hence when we try to load everything ourselves.

Which Z3 version did you use? Did you compile it yourself, or did you use one of our binaries?

Where are the binaries located, i.e. is the default path chosen by Ivy correct? If not, you need to provide a custom loader that resolves the path to your binaries.

Maybe @PhilippWendler or @kfriedberger know more about OSGi, as they use Eclipse AFAIK.

Thanks for your reply.

I tried different Z3 version. I was testing now with 4.15.3 from your Ivy repository but also with 4.14.0. I also tested my own self compiled Z3, same result when using java-smt.

My setup:

• One bundle (named org.example.z3.bundle) which contains a lib folder with the libraries libz3.so and libz3java.so.
• A .target platform file to manage all my dependencies. Likewise, there is java-smt and javasmt-solver-z3 from the mvn central.
• -Djava.library.path and LD_LIBRARY_PATH pointing to the lib folder of my bundle.

This works flawlessly when using the Z3 java bindings from the Z3 repo.

I also tried different approaches with a custom loader all based on the Consumer<String> interface, none of them worked.

The solution that works is the above-mentioned. Set the property in the Eclipse platform look for it in java-smt when it's found active, do not skip the loading mechanism from Z3. This way java-smt works for me.

[daniel-raffler]

Hello Malte,
great to hear that you found a workaround! When z3.skipLibraryLoad is set to false the Z3 Java package will try to load the binaries itself. The code for that looks something like this:

package com.microsoft.z3;

public final class Native {
  static {
    if (!Boolean.parseBoolean(System.getProperty("z3.skipLibraryLoad"))) {
      try {
        System.loadLibrary("z3java");
      } catch (UnsatisfiedLinkError ex) {
        System.loadLibrary("libz3java");
      }
    }
  }
  ...
}

So this is quite similar to what we're doing when System.loadLibrary is used to load the libraries. However, unlike Z3 we will load libz3.so first, before then loading libz3java.so as the main library. The reasoning here is that libz3java.so depends on libz3.so and by loading the latter first we can solve the dependency for the OS. When only libz3java.so is loaded the OS will have to figure out where to find libz3.so. This works when LD_LIBRARY_PATH is set by the user, but can cause problems otherwise. As a library we don't want to overwrite environment variables that may have been set by the user, and so preloading the dependency seemed like the best option

I'm still not quite sure why this fails for your build, but from the debug messages in your post it seems like the preloaded symbols from libz3.so are somehow not available when trying to load libz3java.so

I have a bug fix that works for the Eclipse PDE platform. @daniel-raffler please tell if it's appropriate for the java-smt project.

We could certainly add such an option, but I'd prefer to look for a more general solution first as this may also affect other solvers

My setup:

* One bundle (named `org.example.z3.bundle`) which contains a `lib` folder with the libraries `libz3.so` and `libz3java.so`.

* A `.target` platform file to manage all my dependencies. Likewise, there is `java-smt` and `javasmt-solver-z3` from the mvn central.

* `-Djava.library.path` and `LD_LIBRARY_PATH` pointing to the `lib` folder of my bundle.

Could you maybe upload the project files? I've installed Eclipse and the PDE plugin. However, I'm not familiar with Eclipse and don't know how to set up the project with the dependencies

[baierd]

This works flawlessly when using the Z3 java bindings from the Z3 repo.

Please define what works and what does not work more precisely.
Could you load JavaSMT with Z3 when using the binaries from the Z3 repo, or could you use Z3 without JavaSMT when using them? (Note: we use the official binaries for Z3 in JavaSMT)

Did you try using Ant/Ivy to build your project and resolve the dependencies?
Do you use/change the lib folder located in the JavaSMT project/main folder by any other means than by using Ant/Ivy? (Because the build system will just remove all your changes per default)

Could you maybe upload the project files? I've installed Eclipse and the PDE plugin. However, I'm not familiar with Eclipse and don't know how to set up the project with the dependencies

A minimal example is always better than an entire project.

[gravemalte]

Hi @daniel-raffler and @baierd.

A minimal example is always better than an entire project.

I create a minimal example which you can clone:

https://github.com/litcpslab/eclipse-javasmt-demo/tree/main

After the clone, go to the z3.bundle/lib and place the com.microsoft.z3-4.14.0.jar, libz3.so and lib3java.so in the directory.

Give the PDE the following VM argument: -Djava.library.path=${workspace_loc:/z3.bundle/lib} and in the Environment: LD_LIBRARY_PATH ${workspace_loc:/z3.bundle/lib}.

After starting the platform, press STRG+6 and observe the crash.

Did you try using Ant/Ivy to build your project and resolve the dependencies? Do you use/change the lib folder located in the JavaSMT project/main folder by any other means than by using Ant/Ivy? (Because the build system will just remove all your changes per default)

I use the Eclipse target platform resolution in conjunction with maven. So there is no Ant involved.

Please define what works and what does not work more precisely.

A simple example for solving an equation. At the context creation (see the above error messages).
Or see here https://github.com/litcpslab/eclipse-javasmt-demo/blob/main/solver/src/sovler/handlers/SampleHandler.java#L44

[daniel-raffler]

Hello Malte,
thanks for the example project! Unfortunately I still have some issues running it. So far I've:

• Installed Eclipse 4.27, the PDE extension and the M2P plugin to use Maven with PDE
• Downloaded the eclipse-javasmt-demo repository and added the missing binaries in solver/lib
• Imported the project with File/Open Projecects from filesystem.. in Eclipse
• Set the platform in test.target: this seems to load the Maven dependencies and the imports in SampleHandler.java are now working
• I then tries to run the PDE by going to test.product by clicking on the little green arrow at the top. This does start a new Eclipse platform, however, pressing Ctrl+6 seems to have no effect

Do you know what could be going wrong here?

[gravemalte]

Hi Daniel, thanks for trying out!

I suspect that you Run Configuration is not loading the plugins. Can you check the following:

• Click the arrow next to the green Run button
• Click Run Configurations ...
• Go to the Plugins tab of the Eclipse Application product
• Select by Launch with: Features selected below
• Check all the Features
• Click apply and run

Here is a screenshot:

[daniel-raffler]

Thanks for the hint! It's working now and I'm seeing the same linking errors that you described

The issue seems to be that solver and z3.bundle are different bundles, and each one uses it's own class loader. We load the libraries in solver, but the actual JNI calls happen in z3.bundle. Since that's a different bundle the library is not available and we get a linking error

I was able to fix this in the example by making z3.bundle a fragment of solver. For this I added Fragment-Host: solver;bundle-version=1.0.0.qualifier to MANIFEST.MF in z3.solver:

Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: Bundle
Bundle-SymbolicName: z3.bundle
Bundle-Version: 1.0.0.qualifier
Export-Package: com.microsoft.z3,
 com.microsoft.z3.enumerations
Automatic-Module-Name: z3.bundle
Bundle-ClassPath: lib/com.microsoft.z3-4.14.0.jar
Bundle-RequiredExecutionEnvironment: JavaSE-21
Bundle-NativeCode: lib/libz3.so;lib/libz3java.so;osname=Linux;processor=x86-64
Fragment-Host: solver;bundle-version=1.0.0.qualifier

Then I removed the bundle dependency z3.bundle;bundle-version="1.0.0" from the MANIFEST.MF file for solver:

Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: Solver
Bundle-SymbolicName: solver;singleton:=true
Bundle-Version: 1.0.0.qualifier
Require-Bundle: org.eclipse.ui,
 wrapped.org.sosy-lab.java-smt;bundle-version="5.0.1",
 wrapped.org.sosy-lab.common;bundle-version="0.3000.0",
 com.google.guava;bundle-version="31.0.1"
Automatic-Module-Name: sovler
Bundle-RequiredExecutionEnvironment: JavaSE-21

Notice that I also changed the Bundle-NativeCode line in the z3.solver manifest. This seems to be necessary as libz3java.so depends on libz3.so, so both libraries should be part of the same clause.

If you now change the call to SolverContextFactory.createSolverContext(SolverContextFactory.Solvers.Z3) in SampleHandler.java to

SolverContextFactory.createSolverContext(Configuration.defaultConfiguration(),
		                LogManager.createNullLogManager(),
		                ShutdownNotifier.createDummy(),
		                SolverContextFactory.Solvers.Z3,
		                System::loadLibrary)

there should be no more linking errors

Note that this should also work without setting LD_LIBRARY_PATH or java.library.path: When Bundle-NativeCode is used any call to System.loadLibrary that tries to load a bundled library will be redirected to fetch the library directly from the bundle. Setting the variables will only work locally, but not when you're trying to ship the plugin

[daniel-raffler]

Here is the full patch: eclipse-javasmt-demo.patch