about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorSebastian Poeplau <sebastian.poeplau@eurecom.fr>2018-07-25 14:56:39 +0200
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-09-03 19:16:15 +0100
commit5a4823df4f3ead642e4a6e84a972db5ed61a075a (patch)
tree040ae71f53609017471f568095de24c3359a5d5f /lib
parent97e87ce0bed503b3e13b4d161e25bed1e47cd31e (diff)
downloadklee-5a4823df4f3ead642e4a6e84a972db5ed61a075a.tar.gz
Fix PTree::remove to clean the tree properly
The previous version left unnecessary intermediate nodes behind, sometimes
leading to very long paths in the tree.
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/PTree.cpp23
-rw-r--r--lib/Core/PTree.h2
2 files changed, 24 insertions, 1 deletions
diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp
index 244e8520..4d2931cb 100644
--- a/lib/Core/PTree.cpp
+++ b/lib/Core/PTree.cpp
@@ -54,6 +54,29 @@ void PTree::remove(PTreeNode *n) {
     delete n;
     n = p;
   } while (n && !n->left.getPointer() && !n->right.getPointer());
+
+  if (n) {
+    // We're now at a node that has exactly one child; we've just deleted the
+    // other one. Eliminate the node and connect its child to the parent
+    // directly (if it's not the root).
+    PTreeNodePtr child = n->left.getPointer() ? n->left : n->right;
+    PTreeNode *parent = n->parent;
+
+    child.getPointer()->parent = parent;
+    if (!parent) {
+      // We're at the root.
+      root = child;
+    } else {
+      if (n == parent->left.getPointer()) {
+        parent->left = child;
+      } else {
+        assert(n == parent->right.getPointer());
+        parent->right = child;
+      }
+    }
+
+    delete n;
+  }
 }
 
 void PTree::dump(llvm::raw_ostream &os) {
diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h
index b1b6e9fc..3d87611d 100644
--- a/lib/Core/PTree.h
+++ b/lib/Core/PTree.h
@@ -49,7 +49,7 @@ namespace klee {
 
     void attach(PTreeNode *node, ExecutionState *leftState,
                 ExecutionState *rightState);
-    static void remove(PTreeNode *node);
+    void remove(PTreeNode *node);
     void dump(llvm::raw_ostream &os);
     std::uint8_t getNextId() {
       std::uint8_t id = 1 << registeredIds++;