Отслеживание утечек памяти z3

Question

Мы сталкиваемся с несколькими проблемами, связанными с утечкой памяти. Мы используем контексты с ref-counting сборкой мусора. Вот краткое описание ситуации:

С помощью ScalaZ3 на последнем неустойчивом мы создаем много перерасчетных контекстов (400-500), на которых у нас мало решателей (< 5), проверьте пару формул, а затем удалить все. Мы пытаемся отменить все до удаления самого контекста. Мы свидетельствуем, что объем памяти увеличивается (до нескольких Гб), хотя мы используем только 5 или 6 свежих и небольших контекстов за раз.

1) Z3 освобождает память всех объектов в контексте, когда этот контекст удаляется? (Даже те, у кого есть refcount> 0). Если нет, причина, вероятно, в том, что мы забыли обработать несколько объектов.

2) У вас есть инструмент/наконечник, который поможет нам отследить, что осталось в памяти. Может быть, что-то поверх открытого файла open_log? Или где искать при воспроизведении журнала под gcc?

Спасибо!

Answer 1

1) Z3 освободит часть памяти при удалении контекста, но у нас нет гарантии, что вся память будет удалена, если счетчики ссылок не будут правильно использоваться.

2) Обычно я использую Valgrind для отслеживания утечек памяти. Я думаю, это потрясающе. Мы можем создать журнал выполнения в файле z3.log, а затем выполнить

 valgrind z3 z3.log 

BTW, компиляции в режиме отладки также может помочь. В режиме отладки Z3 также сообщит список АСТ, которые все еще живы, когда контекст удален.