From 9b7ba1603b2d6ff4c13182655ca8af32966570aa Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 23 Mar 2019 13:30:35 -0700 Subject: Fix memory leak when using subsolvers (#2893) ASAN was reporting memory leaks in regression tests that were using subsolvers. First, I am going to describe the origin of the leaks and then the solution implemented in this commit. Recall an `Expr` stores the `NodeManager` that the internal node is associated with. `Node::toExpr()` converts a `Node` to an `Expr` and assumes that the active `NodeManager` (returned by `NodeManager::currentNM()` is the one associated with the node. In `ExportPrivate::exportInternal()`, when we were exporting a skolem, we created a skolem in the target `NodeManager` by calling `NodeManager::mkSkolem()` (`ExprManager`s do not support the creation of skolems) but then we called `Node::toExpr()` on the resulting skolem while the origin `NodeManager` was the active `NodeManager`. One of the issues of having the wrong `NodeManager` in the `Expr` is that when the `Expr` is destroyed and the internal node's refcount reaches zero in destructor of `Expr`, then the node value associated with the node is added to the set of zombie nodes (nodes waiting to be garbage collected or resurrected) of the wrong `NodeManager`. The problem here is that the set of zombie nodes uses the node id to hash and compare nodes. Node ids, however, are only unique within a given `NodeManager`. Thus, if we have two nodes with the same id from different `NodeManager`s and both reach refcount zero in the context of the same `NodeManager`, only one of them will end up in the set of zombies and thus only that one will be freed. Using a subsolver realiably triggered this issue. `ExportPrivate::exportInternal()` stored the `Expr` with the wrong `NodeManager` in an `ExprManagerMapCollection` which associates variables in the original `ExprManager` with the variables in the target `ExprManager`. When we created a subsolver, we created the `ExprManagerMapCollection` before creating our subsolver, so it was deleted after the subsolver and so deleting the `ExprManagerMapCollection` deleted the last reference to `Expr`s holding skolem nodes associated with the wrong `NodeManager`. This commit fixes the issue by making sure that the correct `NodeManager` is in scope when converting the skolem/bound variable nodes to an `Expr`. It also swaps the creation order of `ExprManagerMapCollection` and `ExprManager` to make sure that `ExprManagerMapCollection` is deleted before the `ExprManager` that the `Expr`s belong to. Additionally, the commit makes it harder to make a similar mistake by asserting that the `Expr`s in the `ExprManagerMapCollection` are associated with the expected `ExprManager`s. Finally, it adds an assertion that tries to identify such issues by checking whether the list of zombies contains a node with the same id but located at a different address. --- src/theory/quantifiers/expr_miner.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/quantifiers/expr_miner.cpp') diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 65678f674..e8984f40e 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -131,9 +131,9 @@ Result ExprMiner::doCheck(Node query) } NodeManager* nm = NodeManager::currentNM(); bool needExport = false; - ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr smte; + ExprManagerMapCollection varMap; initializeChecker(smte, em, varMap, queryr, needExport); return smte->checkSat(); } -- cgit v1.2.3