[fix]

Author: misonijnik

include/klee/Module/KModule.h

@@ -187,6 +187,9 @@ struct KFunction : public KCallable {
   /// Unique index for KFunction and KInstruction inside KModule
   /// from 0 to [KFunction + KInstruction]
   [[nodiscard]] inline unsigned getGlobalIndex() const { return globalIndex; }
+
+  bool operator<(const KFunction &rhs) const { return id < rhs.id; }
+  bool operator<(const KFunction *rhs) const { return id < rhs->id; }
 };
 
 struct KBlockCompare {

lib/Core/ExecutionState.cpp

@@ -443,7 +443,7 @@ void ExecutionState::increaseLevel() {
   KFunction *kf = prevPC->parent->parent;
   KModule *kmodule = kf->parent;
 
-  if (prevPC->inst->isTerminator()) {
+  if (prevPC->inst->isTerminator() && kmodule->inMainModule(*kf->function)) {
     auto srcLevel = stack.infoStack().back().multilevel[srcbb].second;
     stack.infoStack().back().multilevel.replace({srcbb, srcLevel + 1});
     stack.infoStack().back().maxMultilevel =

lib/Core/Searcher.cpp

@@ -824,17 +824,37 @@ ExecutionState &BlockLevelSearcher::selectState() {
                 ->second.begin());
 }
 
+void BlockLevelSearcher::clear(ExecutionState &state) {
+  KFunction *kf = state.initPC->parent->parent;
+  BlockLevel &bl = stateToBlockLevel[&state];
+  auto &sizeTo = data[kf];
+  auto &sizesTo = sizeTo[bl.sizeOfLevel];
+  auto &levelTo = sizesTo[bl.sizesOfFrameLevels];
+  auto &multilevelTo = levelTo[bl.level];
+  auto &states = multilevelTo[bl.maxMultilevel];
+
+  states.erase(&state);
+  if (states.size() == 0) {
+    multilevelTo.erase(bl.maxMultilevel);
+  }
+  if (multilevelTo.size() == 0) {
+    levelTo.erase(bl.level);
+  }
+  if (levelTo.size() == 0) {
+    sizesTo.erase(bl.sizesOfFrameLevels);
+  }
+  if (sizesTo.size() == 0) {
+    sizeTo.erase(bl.sizeOfLevel);
+  }
+}
+
 void BlockLevelSearcher::update(ExecutionState *current,
                                 const StateIterable &addedStates,
                                 const StateIterable &removedStates) {
   if (current && std::find(removedStates.begin(), removedStates.end(),
                            current) == removedStates.end()) {
     KFunction *kf = current->initPC->parent->parent;
-    auto &sizesTo = data[kf];
-    auto &sizeTo = sizesTo[stateToSize[current]];
-    auto &levelTo = sizeTo[stateToSizes[current]];
-    auto &multilevelTo = levelTo[stateToLevel[current]];
-    auto &states = multilevelTo[stateToMultilevel[current]];
+    BlockLevel &bl = stateToBlockLevel[current];
     sizes.clear();
     unsigned long long maxMultilevel = 0u;
     for (auto &infoFrame : current->stack.infoStack()) {
@@ -844,36 +864,21 @@ void BlockLevelSearcher::update(ExecutionState *current,
     for (auto &kfLevel : current->stack.multilevel) {
       maxMultilevel = std::max(maxMultilevel, kfLevel.second);
     }
-    if (sizes != stateToSizes[current] ||
-        current->level.size() != stateToLevel[current].size() ||
-        maxMultilevel != stateToMultilevel[current]) {
-      states.erase(current);
-      if (states.size() == 0) {
-        multilevelTo.erase(stateToMultilevel[current]);
-      }
-      if (multilevelTo.size() == 0) {
-        levelTo.erase(stateToLevel[current]);
-      }
-      if (levelTo.size() == 0) {
-        sizeTo.erase(stateToSizes[current]);
-      }
-      if (sizeTo.size() == 0) {
-        sizesTo.erase(stateToSize[current]);
-      }
+    if (sizes != bl.sizesOfFrameLevels ||
+        current->level.size() != bl.sizeOfLevel ||
+        maxMultilevel != bl.maxMultilevel) {
+      clear(*current);
 
-      sizesTo[current->level.size()][sizes][current->level][maxMultilevel]
+      data[kf][current->level.size()][sizes][current->level][maxMultilevel]
           .insert(current);
 
-      stateToLevel[current] = current->level;
-      stateToMultilevel[current] = maxMultilevel;
-      stateToSizes[current] = sizes;
-      stateToSize[current] = current->level.size();
+      stateToBlockLevel[current] = BlockLevel(kf, current->level.size(), sizes,
+                                              current->level, maxMultilevel);
     }
   }
 
   for (const auto state : addedStates) {
     KFunction *kf = state->initPC->parent->parent;
-    auto &sizesTo = data[kf];
 
     sizes.clear();
     unsigned long long maxMultilevel = 0u;
@@ -885,49 +890,21 @@ void BlockLevelSearcher::update(ExecutionState *current,
       maxMultilevel = std::max(maxMultilevel, kfLevel.second);
     }
 
-    sizesTo[state->level.size()][sizes][state->level][maxMultilevel].insert(
+    data[kf][state->level.size()][sizes][state->level][maxMultilevel].insert(
         state);
 
-    stateToLevel[state] = state->level;
-    stateToMultilevel[state] = maxMultilevel;
-    stateToSize[state] = state->level.size();
-    stateToSizes[state] = sizes;
+    stateToBlockLevel[state] =
+        BlockLevel(kf, state->level.size(), sizes, state->level, maxMultilevel);
   }
 
   // remove states
   for (const auto state : removedStates) {
-    KFunction *kf = state->initPC->parent->parent;
-    auto &sizesTo = data[kf];
-    auto &sizeTo = sizesTo[stateToSize[state]];
-    auto &levelTo = sizeTo[stateToSizes[state]];
-    auto &multilevelTo = levelTo[stateToLevel[state]];
-    auto &states = multilevelTo[stateToMultilevel[state]];
-
-    states.erase(state);
-    if (states.size() == 0) {
-      multilevelTo.erase(stateToMultilevel[state]);
-    }
-    if (multilevelTo.size() == 0) {
-      levelTo.erase(stateToLevel[state]);
-    }
-    if (levelTo.size() == 0) {
-      sizeTo.erase(stateToSizes[state]);
-    }
-    if (sizeTo.size() == 0) {
-      sizesTo.erase(stateToSize[state]);
-    }
-    if (sizesTo.size() == 0) {
-      data.erase(kf);
-    }
-
-    stateToLevel.erase(state);
-    stateToMultilevel.erase(state);
-    stateToSizes.erase(state);
-    stateToSize.erase(state);
+    clear(*state);
+    stateToBlockLevel.erase(state);
   }
 }
 
-bool BlockLevelSearcher::empty() { return stateToLevel.empty(); }
+bool BlockLevelSearcher::empty() { return stateToBlockLevel.empty(); }
 
 void BlockLevelSearcher::printName(llvm::raw_ostream &os) {
   os << "BlockLevelSearcher\n";

lib/Core/Searcher.h

@@ -366,21 +366,14 @@ class InterleavedSearcher final : public Searcher {
 };
 
 class BlockLevelSearcher final : public Searcher {
+private:
   struct KBlockSetsCompare {
     bool operator()(const std::set<KBlock *, KBlockCompare> &a,
                     const std::set<KBlock *, KBlockCompare> &b) const {
       return a.size() > b.size() || (a.size() == b.size() && a > b);
     }
   };
 
-  struct MultilevelCompare {
-    bool operator()(
-        const std::map<KBlock *, unsigned long long, KBlockCompare> &a,
-        const std::map<KBlock *, unsigned long long, KBlockCompare> &b) const {
-      return a < b;
-    }
-  };
-
   struct VectorsCompare {
     bool operator()(const std::vector<unsigned> &a,
                     const std::vector<unsigned> &b) const {
@@ -394,35 +387,40 @@ class BlockLevelSearcher final : public Searcher {
     }
   };
 
-  using MultilevelsToStates =
-      std::map<unsigned long long,
-               std::set<ExecutionState *, ExecutionStateIDCompare>,
-               std::less<unsigned long long>>;
-
-  using LevelToMultilevelsToStates =
-      std::map<std::set<KBlock *, KBlockCompare>, MultilevelsToStates,
-               KBlockSetsCompare>;
-
-  using SizesToLevelToMultilevelsToStates =
-      std::map<std::vector<unsigned>, LevelToMultilevelsToStates,
-               VectorsCompare>;
-  using SizeToSizesToLevelToMultilevelsToStates =
-      std::map<unsigned, SizesToLevelToMultilevelsToStates,
-               std::greater<unsigned>>;
-
-  using FunctionToSizeToSizesToLevelToMultilevelsToStates =
-      std::map<KFunction *, SizeToSizesToLevelToMultilevelsToStates,
-               KFunctionCompare>;
-
-  FunctionToSizeToSizesToLevelToMultilevelsToStates data;
-  std::unordered_map<ExecutionState *, std::set<KBlock *, KBlockCompare>>
-      stateToLevel;
-  std::unordered_map<ExecutionState *, unsigned long long> stateToMultilevel;
-  std::unordered_map<ExecutionState *, std::vector<unsigned>> stateToSizes;
-  std::unordered_map<ExecutionState *, unsigned> stateToSize;
+  struct BlockLevel {
+    KFunction *kf;
+    unsigned sizeOfLevel;
+    std::vector<unsigned> sizesOfFrameLevels;
+    std::set<KBlock *, KBlockCompare> level;
+    unsigned long long maxMultilevel;
+    BlockLevel(KFunction *kf, unsigned sizeOfLevel,
+               const std::vector<unsigned> &sizesOfFrameLevels,
+               const std::set<KBlock *, KBlockCompare> &level,
+               unsigned long long maxMultilevel)
+        : kf(kf), sizeOfLevel(sizeOfLevel),
+          sizesOfFrameLevels(sizesOfFrameLevels), level(level),
+          maxMultilevel(maxMultilevel) {}
+    BlockLevel() : kf(nullptr), sizeOfLevel(0), maxMultilevel(0){};
+  };
+
+  using states_ty = std::set<ExecutionState *, ExecutionStateIDCompare>;
+  using kblocks_ty = std::set<KBlock *, KBlockCompare>;
+
+  using ForthLayer =
+      std::map<unsigned long long, states_ty, std::less<unsigned long long>>;
+  using ThirdLayer = std::map<kblocks_ty, ForthLayer, KBlockSetsCompare>;
+  using SecondLayer =
+      std::map<std::vector<unsigned>, ThirdLayer, VectorsCompare>;
+  using FirstLayer = std::map<unsigned, SecondLayer, std::greater<unsigned>>;
+  using Data = std::map<KFunction *, FirstLayer, KFunctionCompare>;
+
+  Data data;
+  std::unordered_map<ExecutionState *, BlockLevel> stateToBlockLevel;
   std::vector<unsigned> sizes;
   RNG &theRNG;
 
+  void clear(ExecutionState &state);
+
 public:
   explicit BlockLevelSearcher(RNG &rng);
   ExecutionState &selectState() override;