diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-23 13:30:35 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-23 13:30:35 -0700 |
commit | 9b7ba1603b2d6ff4c13182655ca8af32966570aa (patch) | |
tree | ecf234c1b0286a87963bee61c44a7690381caedd /src/expr/expr_template.cpp | |
parent | 3df45c5613bcd4c81d4cabae4bb7c98ce69d7141 (diff) |
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.
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 96bdb2d04..6f02d4c6a 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -200,6 +200,10 @@ public: TypeNode typeNode = TypeNode::fromType(type); NodeManager* to_nm = NodeManager::fromExprManager(to); Node n = to_nm->mkBoundVar(name, typeNode); // FIXME thread safety + + // Make sure that the correct `NodeManager` is in scope while + // converting the node to an expression. + NodeManagerScope to_nms(to_nm); to_e = n.toExpr(); } else if(n.getKind() == kind::VARIABLE) { bool isGlobal; @@ -214,6 +218,10 @@ public: TypeNode typeNode = TypeNode::fromType(type); NodeManager* to_nm = NodeManager::fromExprManager(to); Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety + + // Make sure that the correct `NodeManager` is in scope while + // converting the node to an expression. + NodeManagerScope to_nms(to_nm); to_e = n.toExpr(); } else { Unhandled(); @@ -228,6 +236,10 @@ public: TypeNode typeNode = TypeNode::fromType(type); NodeManager* to_nm = NodeManager::fromExprManager(to); Node n = to_nm->mkBoundVar(typeNode); // FIXME thread safety + + // Make sure that the correct `NodeManager` is in scope while + // converting the node to an expression. + NodeManagerScope to_nms(to_nm); to_e = n.toExpr(); } else @@ -244,6 +256,11 @@ public: vmap.d_from[to_int] = from_int; vmap.d_to[from_int] = to_int; vmap.d_typeMap[to_e] = from_e;// insert other direction too + + // Make sure that the expressions are associated with the correct + // `ExprManager`s. + Assert(from_e.getExprManager() == from); + Assert(to_e.getExprManager() == to); return Node::fromExpr(to_e); } } else { |