From d591cba305cb86ee8c520b7ff427651d8f9e0f31 Mon Sep 17 00:00:00 2001
From: Timotej Kapus <tk1713@ic.ac.uk>
Date: Thu, 17 Oct 2019 15:58:26 +0100
Subject: Enable subsets for RandomPathSearcher

---
 lib/Core/PTree.h | 26 ++++++++++++++++++++++----
 1 file changed, 22 insertions(+), 4 deletions(-)

(limited to 'lib/Core/PTree.h')

diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h
index 115ea83f..b1b6e9fc 100644
--- a/lib/Core/PTree.h
+++ b/lib/Core/PTree.h
@@ -11,13 +11,19 @@
 #define KLEE_PTREE_H
 
 #include "klee/Expr/Expr.h"
+#include "klee/Support/ErrorHandling.h"
 #include "llvm/ADT/PointerIntPair.h"
 
 namespace klee {
   class ExecutionState;
   class PTreeNode;
-  using PTreeNodePtr = llvm::PointerIntPair<PTreeNode*,3,uint8_t>;
-
+  /* PTreeNodePtr is used by the Random Path Searcher object to efficiently
+  record which PTreeNode belongs to it. PTree is a global structure that
+  captures all  states, whereas a Random Path Searcher might only care about
+  a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which
+  Random Path Searchers PTreeNode belongs to. */
+  constexpr int PtrBitCount = 3;
+  using PTreeNodePtr = llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>;
 
   class PTreeNode {
   public:
@@ -33,14 +39,26 @@ namespace klee {
   };
 
   class PTree {
+    // Number of registered ID
+    int registeredIds = 0;
+
   public:
-    PTreeNode * root = nullptr;
+    PTreeNodePtr root;
     explicit PTree(ExecutionState *initialState);
     ~PTree() = default;
 
-    static void attach(PTreeNode *node, ExecutionState *leftState, ExecutionState *rightState);
+    void attach(PTreeNode *node, ExecutionState *leftState,
+                ExecutionState *rightState);
     static void remove(PTreeNode *node);
     void dump(llvm::raw_ostream &os);
+    std::uint8_t getNextId() {
+      std::uint8_t id = 1 << registeredIds++;
+      if (registeredIds > PtrBitCount) {
+        klee_error("PTree cannot support more than %d RandomPathSearchers",
+                   PtrBitCount);
+      }
+      return id;
+    }
   };
 }
 
-- 
cgit 1.4.1