为什么 Java segfaulting 中的 Z3 优化？答案

【问题标题】：Why is Z3 optimization in Java segfaulting?为什么 Java segfaulting 中的 Z3 优化？
【发布时间】：2020-04-02 20:06:59
【问题描述】：

在我正在处理的一个 Java 项目中，我有一个围绕 Z3 的包装类。当我测试优化时，我的程序因段错误而崩溃。经过一些实验，我找到了这个最小的可重现示例，它只是创建了一个上下文和优化器，并检查了优化器：

import com.microsoft.z3.*;

public class Z3Test {

  public static void main(String[] args) {
    try (Context ctx = new Context()) {
      Optimize opt = ctx.mkOptimize();
      System.out.println("Check: " + opt.Check());
    }
  }
}

请注意，如果没有 try 块，程序仍然会出现段错误，即

Context ctx = new Context();
Optimize opt = ctx.mkOptimize();
System.out.println("Check: " + opt.Check());

另一方面，在不优化的情况下求解，运行良好：

try (Context ctx = new Context()) {
  Solver opt = ctx.mkSolver();
  System.out.println("Check: " + opt.check());
}

检查：满意

我可能做错了什么？一些可能相关的信息：

操作系统：

macOS 10.15.3

Java 版本：

openjdk 14 2020-03-17
OpenJDK Runtime Environment (build 14+36-1461)
OpenJDK 64-Bit Server VM (build 14+36-1461, mixed mode, sharing)

我在运行代码的目录中有 libz3.dylib 和 libz3java.dylib。

来自日志文件的堆栈跟踪：

Native frames: (J=compiled Java code, A=aot compiled Java code, j=interpreted, Vv=VM code, C=native code)
C  [libz3.dylib+0x79f96]  Z3_optimize_check+0x76
C  [libz3java.dylib+0x8425]  Java_com_microsoft_z3_Native_INTERNALoptimizeCheck+0x45
j  com.microsoft.z3.Native.INTERNALoptimizeCheck(JJ)I+0
j  com.microsoft.z3.Native.optimizeCheck(JJ)I+2
j  com.microsoft.z3.Optimize.Check()Lcom/microsoft/z3/Status;+11
j  jaedmax.Main.main([Ljava/lang/String;)V+17
v  ~StubRoutines::call_stub
V  [libjvm.dylib+0x34b082]  JavaCalls::call_helper(JavaValue*, methodHandle const&, JavaCallArguments*, Thread*)+0x256
V  [libjvm.dylib+0x38f7f1]  jni_invoke_static(JNIEnv_*, JavaValue*, _jobject*, JNICallType, _jmethodID*, JNI_ArgumentPusher*, Thread*)+0x11c
V  [libjvm.dylib+0x3930d4]  jni_CallStaticVoidMethod+0x1b3
C  [libjli.dylib+0x4ac2]  JavaMain+0xab4
C  [libjli.dylib+0x6d6a]  ThreadJavaMain+0x9
C  [libsystem_pthread.dylib+0x5e65]  _pthread_start+0x94
C  [libsystem_pthread.dylib+0x183b]  thread_start+0xf

项目目录结构：

.
├── build.xml
├── lib
│   └── com.microsoft.z3-4.7.1.jar
├── libz3.dylib
├── libz3java.dylib
└── src
    └── Z3Test.java

Ant 构建文件：

<project name="Z3Test" basedir="." default="run">

  <path id="lib.path">
    <pathelement location="lib/com.microsoft.z3-4.7.1.jar"/>
  </path>

  <path id="class.path">
    <path refid="lib.path"/>
    <pathelement location="build"/>
  </path>

  <target name="clean">
    <delete dir="build"/>
    <delete>
      <fileset dir="." includes="**/*.log"/>
    </delete>
  </target>

  <target name="compile" depends="clean">
    <mkdir dir="build"/>
    <javac srcdir="src" destdir="build" classpathref="lib.path" includeantruntime="no"/>
  </target>

  <target name="run" depends="compile">
    <java classname="Z3Test" classpathref="class.path" fork="yes"/>
  </target>

</project>

【问题讨论】：

请发布一个完全独立的程序（即，具有main 函数等），包括您用于编译它的命令行标志。
我发布的代码是主要方法，我只是没有包含样板。该项目是使用 Ant 的 javac 任务编译的。
嗯，就是这样。您认为样板文件是人们必须为您重建的内容，以便他们可以解决您的问题来帮助您。此外，通常是您认为有问题的“样板”。有关如何发布良好的堆栈溢出问题（也称为 MVCE）的信息，请参阅以下指南：stackoverflow.com/help/minimal-reproducible-example
好的，感谢您的反馈。编辑更详细

标签： java z3

【解决方案1】：

看来您的 z3 和/或 Java 安装可能存在问题。为了简单起见，我做了以下操作：

$ cat Z3Test.java
import com.microsoft.z3.*;

public class Z3Test {

  public static void main(String[] args) {
    try (Context ctx = new Context()) {
      Optimize opt = ctx.mkOptimize();
      System.out.println("Check: " + opt.Check());
    }
  }
}

然后：

$ javac -cp /usr/local/z3/build/com.microsoft.z3.jar:. Z3Test.java
$ java -Djava.library.path=/usr/local/z3/build -cp /usr/local/z3/build/com.microsoft.z3.jar:. Z3Test
Check: SATISFIABLE

所以一切都很顺利。看看你是否可以在你的命令行上复制它。如果是这样，问题必须在您的构建系统中的其他地方。如果失败，最好的办法是从头开始使用 java 绑定重新安装 z3。

【讨论】：

【解决方案2】：

想通了！原始项目中出现错误的 Maven 工件之一是将 com.microsoft.z3-4.7.1.jar 作为依赖项下载，这与我从源代码构建的本机库不兼容。这个问题在最小的例子中仍然存在，因为我复制了 jar。解决方法是摆脱该工件，并使用我从源代码构建的 jar。

【讨论】：