From: Andres Noetzli Date: Sat, 23 Mar 2019 20:30:35 +0000 (-0700) Subject: Fix memory leak when using subsolvers (#2893) X-Git-Tag: cvc5-1.0.0~4219 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b7ba1603b2d6ff4c13182655ca8af32966570aa;p=cvc5.git 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. --- 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 { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 7cafb6e11..619098e5e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -276,6 +276,17 @@ class NodeManager { Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") << std::endl; } + + // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies` + // already contains a node value with the same id as `nv`, but the pointers + // are different, then the wrong `NodeManager` was in scope for one of the + // two nodes when it reached refcount zero. This can happen for example if + // you create a node with a `NodeManager` n1 and then call `Node::toExpr()` + // on that node while a different `NodeManager` n2 is in scope. When that + // `Expr` is deleted and the node reaches refcount zero in the `Expr`'s + // destructor, then `markForDeletion()` will be called on n2. + Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv); + d_zombies.insert(nv); // FIXME multithreading if(safeToReclaimZombies()) { diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 3e613cde5..1b123393b 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -137,9 +137,9 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // options as the SmtEngine we belong to, where we ensure that // produce-models is set. bool needExport = false; - ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr rrChecker; + ExprManagerMapCollection varMap; initializeChecker(rrChecker, em, varMap, crr, needExport); Result r = rrChecker->checkSat(); Trace("rr-check") << "...result : " << r << std::endl; 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(); } diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index e62f3513c..00ec67169 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -185,9 +185,9 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) NodeManager* nm = NodeManager::currentNM(); // make the satisfiability query bool needExport = false; - ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr queryChecker; + ExprManagerMapCollection varMap; initializeChecker(queryChecker, em, varMap, qy, needExport); Result r = queryChecker->checkSat(); Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl; diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy index 278c10339..f310396d2 100644 --- a/test/regress/regress1/rr-verify/bv-term.sy +++ b/test/regress/regress1/rr-verify/bv-term.sy @@ -1,4 +1,3 @@ -; REQUIRES: no-asan ; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break ; COMMAND-LINE: --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy index 61dc19fbb..cca2487d4 100644 --- a/test/regress/regress1/rr-verify/fp-arith.sy +++ b/test/regress/regress1/rr-verify/fp-arith.sy @@ -1,4 +1,3 @@ -; REQUIRES: no-asan ; REQUIRES: symfpu ; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy index 8e404668e..8792a594c 100644 --- a/test/regress/regress1/rr-verify/fp-bool.sy +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -1,4 +1,3 @@ -; REQUIRES: no-asan ; REQUIRES: symfpu ; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")