z3 - 跟踪 z3 内存泄漏

Question

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

通过最新不稳定的 ScalaZ3，我们创建了很多重新计数的上下文（400-500），我们很少有求解器（<5），检查几个公式，然后删除所有内容。我们尝试在删除上下文本身之前删除所有内容。我们目睹的是内存占用不断增加（高达几 Gb），即使我们一次只使用 5 或 6 个新鲜和小型上下文。

1) 当上下文被删除时，Z3 是否释放上下文中所有对象的内存？（即使是那些 refcount > 0 的）如果不是，原因可能是我们忘记了 del-ref 几个对象。

2) 你有什么工具/提示可以帮助我们追踪内存中的内容吗？也许在 open_log 生成的文件之上有一些东西？或者在 gcc 下重放日志时在哪里看？

谢谢！

Answer 1

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

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

       valgrind z3 z3.log

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