From 8be2d02f510e329d88e38889720334c277bf268c Mon Sep 17 00:00:00 2001
From: Tim King <taking@google.com>
Date: Sun, 6 Nov 2016 16:05:29 -0800
Subject: This switches the ZombieSet in the NodeManager to use NodeValue's id
 for equality comparison. The previously used function NodeValueEq incorrectly
 identified VARIABLE nodes as being equal. This meant that on hash collisions
 these nodes could leak memory.

---
 src/expr/metakind_template.h |  9 +--------
 src/expr/node_manager.h      |  4 ++--
 src/expr/node_value.h        | 12 ++++++++++++
 3 files changed, 15 insertions(+), 10 deletions(-)

(limited to 'src')

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 9025aa02a..75521e901 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -149,13 +149,6 @@ static const unsigned MAX_CHILDREN =
 
 namespace expr {
 
-// Comparison predicate
-struct NodeValueEq {
-  inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
-    return ::CVC4::kind::metakind::NodeValueCompare::compare<false>(nv1, nv2);
-  }
-};
-
 // Comparison predicate
 struct NodeValuePoolEq {
   inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
@@ -345,7 +338,7 @@ ${metakind_operatorKinds}
 
 }/* CVC4::kind namespace */
 
-#line 349 "${template}"
+#line 341 "${template}"
 
 namespace theory {
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0b3830f4b..aaffeb322 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -96,7 +96,7 @@ class NodeManager {
                               expr::NodeValuePoolEq> NodeValuePool;
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
                               expr::NodeValueIDHashFunction,
-                              expr::NodeValueEq> ZombieSet;
+                              expr::NodeValueIDEquality> ZombieSet;
 
   static CVC4_THREADLOCAL(NodeManager*) s_current;
 
@@ -268,7 +268,7 @@ class NodeManager {
       Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
                   << std::endl;
     }
-    d_zombies.insert(nv);// FIXME multithreading
+    d_zombies.insert(nv);  // FIXME multithreading
 
     if(safeToReclaimZombies()) {
       if(d_zombies.size() > 5000) {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index fbf3ff76e..b403d0c86 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -372,6 +372,18 @@ struct NodeValueIDHashFunction {
   }
 };/* struct NodeValueIDHashFunction */
 
+
+/**
+ * An equality predicate that is applicable between pointers to fully
+ * constructed NodeValues.
+ */
+struct NodeValueIDEquality {
+  inline bool operator()(const NodeValue* a, const NodeValue* b) const {
+    return a->getId() == b->getId();
+  }
+};
+
+
 inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 
 }/* CVC4::expr namespace */
-- 
cgit v1.2.3