1

我正在使用 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。过错。那么它是否与任何并发问题有关？

4

1 回答 1

2

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

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

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

于 2013-02-05T17:15:37.863 回答