使用 Z3 的 Java 中的分段错误答案

【问题标题】：Segmentation Fault in Java using Z3使用 Z3 的 Java 中的分段错误
【发布时间】：2013-01-20 09:28:57
【问题描述】：

我正在使用 Java JNI 将 Z3 Solver C-Api 集成到我们正在使用的框架中。现在，我收到以下消息的分段错误 -

#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x664c4af0, pid=10878, tid=3060636480
#
# JRE version: 7.0_09-b30
# Java VM: OpenJDK Server VM (23.2-b09 mixed mode linux-x86 )
# Problematic frame:
# C  [libSpdfZ3.so+0x634af0]  small_object_allocator::allocate(unsigned int)+0x40
#
# Failed to write core dump. Core dumps have been disabled. To enable core dumping, try "ulimit -c unlimited" before starting Java again
#
# An error report file with more information is saved as:
# /home/rajtendulkar/workspace/Java-WorkSpace/spdf-compiler_with_Yices_and_Z3_StaticLib/hs_err_pid10878.log
#
# If you would like to submit a bug report, please include
# instructions on how to reproduce the bug and visit:
#   https://bugs.launchpad.net/ubuntu/+source/openjdk-7/
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.
#

在日志文件中，它指向一个调用 Z3 的上下文被分配的地方。基本上它是一个带有一些内存分配的初始化例程。

我想尝试了解导致此分段错误的原因。我想提一下，我的程序运行一次就可以正常工作。但是，如果我在这样的 for 循环中运行它-

for (int i=0;i<5;i++)
{
     // create z3 context
     Z3Object obj = new Z3Object();
     ...
     ... 
     .. do some exploration here ..
     ...  
     ...
     ...     
}

我只是在想这是否与内存分配或内存不足或类似的事情有关？

感谢任何有关如何调试的指针。

编辑：

当我有时尝试调试代码并慢慢单步执行时，我没有遇到这个问题。同样，如果我在 for 循环结束时延迟 5 秒，我不会得到任何 seg。过错。那么它是否与任何并发问题有关？

【问题讨论】：

我怀疑该库假定包装器仅创建一次或在销毁后不创建。即你打破了一些假设，这意味着你正在使用处于无效状态的对象。
如果您的工作环境允许将 Java 与其他基于 JVM 的语言混合使用，那么您可以将 ScalaZ3 (github.com/psuter/ScalaZ3) 集成到您的框架中。这样您就可以避免完全编写自己的 Java 绑定。
@PeterLawrey 感谢您的回复！我想我没有使用处于无效状态的对象。原因是，我在帖子中提到的 for 循环末尾放置了 5 秒的睡眠时间。我发现没有段。如果代码像这样运行就出错了！所以也许不是睡眠，我需要等待 for 循环的当前迭代完成，然后再开始下一个。我不确定，我所说的是否正确，但这是基于观察。
@mhs 我可以将 scala 集成到我的框架中，但是，我认为现在这对我来说将是大量的工作，这就是为什么我不会把它作为高优先级的原因。我已经围绕这个 JNI 库构建了大量代码。不过感谢您的建议！
我喜欢它，native 代码失败并带走了 jvm。

标签： java c java-native-interface z3

【解决方案1】：

您似乎正在为 Z3 开发自定义 JNI 绑定。请注意，Z3 将在下一个版本中附带它自己的绑定。这已经包含在Codeplex 的“不稳定”分支中，可以作为灵感甚至替代。

请注意，从 z3.dll 获得的对象必须正确地进行引用计数，这取决于所使用的垃圾收集器类型，这可能会非常棘手。我的第一个怀疑是（由 Z3 收集）对象而您的程序没有意识到它（例如，因为引用计数不同步），或者您的垃圾收集器试图以 Z3 没有的顺序销毁对象t 预期（例如，在所有关联对象被销毁之前销毁上下文）。

并发问题可能不是因为你自己的程序，而是因为垃圾收集器是并发的（如果我没记错的话，Java的更高版本实际上有4个不同的版本，并根据主机系统在它们之间进行选择，这可能是问题的根源）。

【讨论】：

我认为你的观点非常好。我一定会检查这件事！谢谢！
请问这个Java版本什么时候正式发布？
我计划在我们发布它之前进行更多测试（出于与您遇到的非常相似的原因），但这实际上可能会在接下来的两周内发生。您已经可以通过从 Codeplex 下载“不稳定”分支来尝试预览；这带有 Java API，您可以通过运行 python scripts\mk_make.py --java（然后 make 等）来启用它。