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 96bdb2d046b1ec10638189e6e2f5b66836520431..6f02d4c6a382926f51df2a80f1264736ef1ae507 100644 (file)
--- 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 7cafb6e113247574330f9c64433a5dfcb1f078a8..619098e5ec255beee36bd001eb1839690052d738 100644 (file)
--- 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 3e613cde5c6ed9e551f4e026a092b5f431fb5139..1b123393b6806b6559391fbf42c40e25b0f9b65f 100644 (file)
--- 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<SmtEngine> 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 65678f674eb051a8de761490007d60c677ea7b37..e8984f40ee1313fb0a37afb2aaa47c217ebd7a46 100644 (file)
--- 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<SmtEngine> 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 e62f3513c93e73bb5a995944575ec98a2614e781..00ec6716999d306edae95df0fa3a0a9ef12b8ec4 100644 (file)
--- 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<SmtEngine> 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 278c1033957d7cf404c8d6e7fe1a163e0886a319..f310396d220e46cd68129c1c2320dfcb076b94ec 100644 (file)
--- 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 61dc19fbb75f5de9835e0d88f6efb17bb87383b5..cca2487d4ea2e9eaed82570cd7fff5126b854a9d 100644 (file)
--- 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 8e404668eba9bad741debe1dccf7598519cd3631..8792a594c10b22044b11d8b7474b371d1692dfa9 100644 (file)
--- 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.")