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: [PATCH] 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(-)

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 */
-- 
2.30.2