summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_template.cpp17
-rw-r--r--src/expr/node_manager.h11
-rw-r--r--src/theory/quantifiers/candidate_rewrite_database.cpp2
-rw-r--r--src/theory/quantifiers/expr_miner.cpp2
-rw-r--r--src/theory/quantifiers/query_generator.cpp2
-rw-r--r--test/regress/regress1/rr-verify/bv-term.sy1
-rw-r--r--test/regress/regress1/rr-verify/fp-arith.sy1
-rw-r--r--test/regress/regress1/rr-verify/fp-bool.sy1
8 files changed, 31 insertions, 6 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 {
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<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 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<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 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<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 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.")
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback