Reworking expression cache method

UnitTestBot · Mar 6, 2023 · 6e7a91f · 6e7a91f
1 parent 4d057e3
commit 6e7a91f
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 34 deletions.
diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h
@@ -106,30 +106,24 @@ class Expr {
     }
   };
 
-  class ExprCacheSet {
-  public:
-    typedef std::unordered_set<Expr *, ExprHash, ExprCmp> CacheType;
-    CacheType cache;
+  typedef std::unordered_set<Expr *, ExprHash, ExprCmp> CacheType;
 
+  struct ExprCacheSet {
+    CacheType cache;
     ~ExprCacheSet() {
-      for (auto &p : cache) {
-        p->cached = false;
+      while (cache.size() != 0) {
+        ref<Expr> tmp = *cache.begin();
+        tmp->isCached = false;
+        cache.erase(cache.begin());
       }
     }
   };
 
-  static std::unique_ptr<Expr::ExprCacheSet> cachedExpressions;
+  static ExprCacheSet cachedExpressions;
   static ref<Expr> createCachedExpr(const ref<Expr> &e);
-  bool cached = false;
+  bool isCached = false;
   bool toBeCleared = false;
 
-public:
-  static void enableCache() {
-    cachedExpressions =
-        std::unique_ptr<Expr::ExprCacheSet>(new Expr::ExprCacheSet());
-  }
-  bool isCached() const { return cached; }
-
 public:
   static unsigned count;
   static const unsigned MAGIC_HASH_CONSTANT = 39;

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -514,8 +514,6 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
 
   initializeSearchOptions();
 
-  Expr::enableCache();
-
   if (OnlyOutputStatesCoveringNew && !StatsTracker::useIStats())
     klee_error("To use --only-output-states-covering-new, you need to enable "
                "--output-istats.");

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
@@ -133,7 +133,7 @@ int Expr::compare(const Expr &b, ExprEquivSet &equivs) const {
   if (hashValue != b.hashValue)
     return (hashValue < b.hashValue) ? -1 : 1;
 
-  if (isCached() && b.isCached())
+  if (isCached && b.isCached)
     return (this < &b) ? -1 : 1;
 
   const Expr *ap, *bp;
@@ -501,30 +501,28 @@ std::string Expr::toString() const {
 
 /***/
 
-std::unique_ptr<Expr::ExprCacheSet> Expr::cachedExpressions;
+Expr::ExprCacheSet Expr::cachedExpressions;
 
 Expr::~Expr() {
   Expr::count--;
-  toBeCleared = true;
-  if (cachedExpressions) {
-    cachedExpressions->cache.erase(this);
+  if (isCached) {
+    toBeCleared = true;
+    cachedExpressions.cache.erase(this);
   }
 }
 
 ref<Expr> Expr::createCachedExpr(const ref<Expr> &e) {
-  if (cachedExpressions) {
-    std::pair<ExprCacheSet::CacheType::const_iterator, bool> success =
-        cachedExpressions->cache.insert(e.get());
-
-    if (success.second) {
-      // Cache miss
-      e->cached = true;
-      return e;
-    }
-    // Cache hit
-    return (ref<Expr>)*(success.first);
+
+  std::pair<CacheType::const_iterator, bool> success =
+      cachedExpressions.cache.insert(e.get());
+
+  if (success.second) {
+    // Cache miss
+    e->isCached = true;
+    return e;
   }
-  return e;
+  // Cache hit
+  return (ref<Expr>)*(success.first);
 }
 /***/