Close memory leaks on CVC5 and Bitwuzla

[daniel-raffler]

Hello,

this PR aims to fix memory leaks on CVC5 and Bitwuzla

• CVC5 We now use Context.deletePointers to make sure all solver memory is freed. Context is a utility class in the CVC5 JNI bindings that tracks all solver objects. The deletePointers method can then be called at the end of the program to free native memory. It is not tied to a TermManager and will delete Objects from all remaining CVC5 SolverContexts, which is why it can only be used when closing the last solver instance.
  We used to only close Solver and TermManager when a CVC5 SolverContext is closed. While this approach is more fine-grained, it also leads to memory leaks as Terms and Sorts are never freed, even after the SolverContext is closed. Our new solution is to check in SolverContext.close() if we're closing the last CVC5 instance and then delete all Objects with deletePointers. Otherwise only the Solver object is deleted right away, and all other Objects will be collected at the end of the Program. (Thanks to @baierd for the suggestion)
• Bitwuzla We adopt a very similar approach to CVC5. Unlike CVC5, Bitwuzla does not come with its own Java bindings, and we use SWIG to generate our own JNI headers. SWIG uses finalizers to release native memory when it is no longer needed. This allows for more fine-grained control, but is also error-prone, and we had to disable several of the finalizers to avoid random crashes in Bitwuzla. This lead to memory leaks, which have now been closed by tracking all solver objects, similar to how it is done in CVC5

Here are some benchmarks to show that the leaks have indeed been closed. The program executes the same JavaSMT trace in a loop while monitoring total memory usage of the process:

CVC5 (before)

CVC5 (after)

Bitwuzla (before)

Bitwuzla (after)

@kfriedberger
We will need to recompile the Bitwuzla bindings for this PR. Could you handle this, please?

[kfriedberger]

Well done. Thanks for the analysis and solution.

I will try to find some time soon for updating the solver library.

Side note: Which tool was used to generate the graphs for measurements? JProfiler or similar?

[daniel-raffler]

Well done. Thanks for the analysis and solution.

Thanks!

Side note: Which tool was used to generate the graphs for measurements? JProfiler or similar?

I used procpath for the graphs and wrote a small program to repeatably run the same JavaSMT trace so that we can monitor its memory usage. Here is the source for the tool. If needed, this could also be integrated into JavaSMT for benchmarking. The other approach is to use CPA-Daemon to look for memory leaks, but then it's not entirely clear if the problem is with JavaSMT or CPAchecker. Profilers weren't too useful as they can only see the Java heap, and not what is going on in native memory when using JNI

[daniel-raffler]

Our new solution is to check in SolverContext.close() if we're closing the last CVC5 instance and then delete all Objects with deletePointers. Otherwise only the Solver object is deleted right away, and all other Objects will be collected at the end of the Program

One more note: This solution works well if there is only a single SolverContext, or when only using SolverContexts sequentially (i.e closing the last SolverContext before opening a new one). It might work less well in a parallel setting when SolverContexts keep being opened and closed in parallel. While the code should be thread-safe, memory will only be freed whenever we get to a point where all SolverContexts are closed. If there are multiple busy threads this might not happen until the end of the program, and memory will still pile up in the mean time

We could fix this by managing references for each TermManager, rather than using a global queue. However, this adds additional overhead, and for CVC5 we would have to ask the developers for a fix as we don't use our own JNI bindings