Почему оптимизация Z3 в Java segfaulting? - PullRequest
Новая
       13

Почему оптимизация Z3 в Java segfaulting?

3 голосов
/ 02 апреля 2020

В проекте 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 и libz3 java .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>

Ответы [ 2 ]

1 голос
/ 07 апреля 2020

Возможно, у вас проблемы с установкой 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

Так что все получилось просто отлично. Посмотрите, сможете ли вы повторить это в командной строке. Если это так, проблема должна быть где-то еще в вашей системе сборки. Если это не удастся, возможно, лучше всего переустановить z3 с java привязками с нуля.

0 голосов
/ 09 апреля 2020

Разобрался! Одним из артефактов Maven в исходном проекте, где у меня была ошибка, была загрузка com.microsoft.z3-4.7.1.jar в качестве зависимости, которая была несовместима с собственными библиотеками, которые я создал из исходных текстов. Проблема сохранилась в минимальном примере, потому что я скопировал банку. Решением было избавиться от этого артефакта и использовать банку, которую я построил из источника.

...