z3 - 跟踪 z3 内存泄漏

Question

我们遇到了一些与内存泄漏相关的问题。我们正在使用具有引用计数垃圾收集的上下文。以下是对情况的简短描述:

通过在最新的 unstable 上使用 ScalaZ3，我们创建了大量的重新计数上下文(400-500)，我们在这些上下文中使用了很少的求解器(<5)，检查了几个公式，然后删除了所有内容。我们尝试在删除上下文本身之前删除所有内容。我们看到内存占用量不断增加(高达几 Gb)，即使我们一次只使用 5 或 6 个新鲜的小上下文。

1) 当上下文被删除时，Z3 会释放上下文中所有对象的内存吗？ (即使是 refcount > 0 的那些)如果不是，原因可能是我们忘记删除引用几个对象。

2) 您是否有任何工具/提示可以帮助我们追踪内存中剩余的内容。也许在 open_log 生成的文件之上？或者在 gcc 下重放日志时要看哪里？

谢谢!

Answer 1

1) Z3 会在删除上下文时释放部分内存，但我们不保证在引用计数器未正确使用时会删除所有内存。

2) 我通常使用 Valgrind 来跟踪内存泄漏。我认为这太棒了。我们可以在文件z3.log中创建执行日志，然后执行

       valgrind z3 z3.log

顺便说一句，在 Debug模式下编译也可能有帮助。在 Debug模式下，Z3 还会报告删除上下文时仍然存在的 AST 列表。