diff --git a/include/klee/ADT/ImmutableList.h b/include/klee/ADT/ImmutableList.h index 20cb225fd8..425036979e 100644 --- a/include/klee/ADT/ImmutableList.h +++ b/include/klee/ADT/ImmutableList.h @@ -10,6 +10,7 @@ #ifndef KLEE_IMMUTABLELIST_H #define KLEE_IMMUTABLELIST_H +#include #include #include @@ -96,6 +97,22 @@ template class ImmutableList { node->values.push_back(std::move(value)); } + void push_back(const T &value) { + if (!node) { + node = std::make_shared(); + } + node->values.push_back(value); + } + + bool empty() { return size() == 0; } + + const T &back() { + assert(node && "requiers not empty list"); + auto it = iterator(node.get()); + it.get = size() - 1; + return *it; + } + ImmutableList() : node(){}; ImmutableList(const ImmutableList &il) : node(std::make_shared(il)) {} diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h index d6f47e3d94..75769b3fb4 100644 --- a/include/klee/Expr/Constraints.h +++ b/include/klee/Expr/Constraints.h @@ -12,6 +12,7 @@ #include "klee/ADT/Ref.h" +#include "klee/ADT/PersistentMap.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" @@ -91,7 +92,7 @@ class ConstraintSet { class PathConstraints { public: using ordered_constraints_ty = - std::map; + PersistentMap; void advancePath(KInstruction *ki); void advancePath(const Path &path); diff --git a/include/klee/Expr/Path.h b/include/klee/Expr/Path.h index 48bb63ec47..a556a00213 100644 --- a/include/klee/Expr/Path.h +++ b/include/klee/Expr/Path.h @@ -1,6 +1,8 @@ #ifndef KLEE_PATH_H #define KLEE_PATH_H +#include "klee/ADT/ImmutableList.h" + #include #include #include @@ -16,7 +18,7 @@ using stackframe_ty = std::pair; class Path { public: - using path_ty = std::vector; + using path_ty = ImmutableList; enum class TransitionKind { StepInto, StepOut, None }; struct PathIndex { @@ -38,23 +40,6 @@ class Path { void advance(KInstruction *ki); - friend bool operator==(const Path &lhs, const Path &rhs) { - return lhs.KBlocks == rhs.KBlocks && - lhs.firstInstruction == rhs.firstInstruction && - lhs.lastInstruction == rhs.lastInstruction; - } - friend bool operator!=(const Path &lhs, const Path &rhs) { - return !(lhs == rhs); - } - - friend bool operator<(const Path &lhs, const Path &rhs) { - return lhs.KBlocks < rhs.KBlocks || - (lhs.KBlocks == rhs.KBlocks && - (lhs.firstInstruction < rhs.firstInstruction || - (lhs.firstInstruction == rhs.firstInstruction && - lhs.lastInstruction < rhs.lastInstruction))); - } - unsigned KBlockSize() const; const path_ty &getBlocks() const; unsigned getFirstIndex() const; @@ -64,7 +49,6 @@ class Path { std::vector getStack(bool reversed) const; - std::vector> asFunctionRanges() const; std::string toString() const; static Path concat(const Path &l, const Path &r); @@ -73,7 +57,7 @@ class Path { Path() = default; - Path(unsigned firstInstruction, std::vector kblocks, + Path(unsigned firstInstruction, const path_ty &kblocks, unsigned lastInstruction) : KBlocks(kblocks), firstInstruction(firstInstruction), lastInstruction(lastInstruction) {} diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 5ebcf17a74..7ae7d692cb 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -290,7 +290,7 @@ class ExecutionState { std::uint32_t depth = 0; /// @brief Exploration level, i.e., number of times KLEE cycled for this state - std::set level; + PersistentSet level; /// @brief Address space used by this state (e.g. Global and Heap) AddressSpace addressSpace; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index ae00a3303c..d349c9d0b2 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -330,10 +330,6 @@ PathConstraints::orderedCS() const { void PathConstraints::advancePath(KInstruction *ki) { _path.advance(ki); } -void PathConstraints::advancePath(const Path &path) { - _path = Path::concat(_path, path); -} - ExprHashSet PathConstraints::addConstraint(ref e, const Assignment &delta, Path::PathIndex currIndex) { auto expr = Simplificator::simplifyExpr(constraints, e); @@ -352,7 +348,9 @@ ExprHashSet PathConstraints::addConstraint(ref e, const Assignment &delta, added.insert(expr); pathIndexes.insert({expr, currIndex}); _simplificationMap[expr].insert(expr); - orderedConstraints[currIndex].insert(expr); + auto indexConstraints = orderedConstraints[currIndex].second; + indexConstraints.insert(expr); + orderedConstraints.replace({currIndex, indexConstraints}); constraints.addConstraint(expr, delta); } } @@ -389,29 +387,6 @@ void PathConstraints::rewriteConcretization(const Assignment &a) { constraints.rewriteConcretization(a); } -PathConstraints PathConstraints::concat(const PathConstraints &l, - const PathConstraints &r) { - // TODO : How to handle symcretes and concretization? - PathConstraints path = l; - path._path = Path::concat(l._path, r._path); - auto offset = l._path.KBlockSize(); - for (const auto &i : r._original) { - path._original.insert(i); - auto index = r.pathIndexes.at(i); - index.block += offset; - path.pathIndexes.insert({i, index}); - path.orderedConstraints[index].insert(i); - } - for (const auto &i : r.constraints.cs()) { - path.constraints.addConstraint(i, {}); - if (r._simplificationMap.count(i)) { - path._simplificationMap.insert({i, r._simplificationMap.at(i)}); - } - } - // Run the simplificator on the newly constructed set? - return path; -} - Simplificator::ExprResult Simplificator::simplifyExpr(const constraints_ty &constraints, const ref &expr) { diff --git a/lib/Expr/Path.cpp b/lib/Expr/Path.cpp index e67abd51b4..829e73b374 100644 --- a/lib/Expr/Path.cpp +++ b/lib/Expr/Path.cpp @@ -39,67 +39,6 @@ Path::PathIndex Path::getCurrentIndex() const { return {KBlocks.size() - 1, lastInstruction}; } -std::vector Path::getStack(bool reversed) const { - std::vector stack; - for (unsigned i = 0; i < KBlocks.size(); i++) { - auto current = reversed ? KBlocks[KBlocks.size() - 1 - i] : KBlocks[i]; - // Previous for reversed is the next - KBlock *prev = nullptr; - if (i != 0) { - prev = reversed ? KBlocks[KBlocks.size() - i] : KBlocks[i - 1]; - } - if (i == 0) { - stack.push_back({nullptr, current->parent}); - continue; - } - if (reversed) { - auto kind = getTransitionKind(current, prev); - if (kind == TransitionKind::StepInto) { - if (!stack.empty()) { - stack.pop_back(); - } - } else if (kind == TransitionKind::StepOut) { - assert(isa(prev)); - stack.push_back({prev->getFirstInstruction(), current->parent}); - } - } else { - auto kind = getTransitionKind(prev, current); - if (kind == TransitionKind::StepInto) { - stack.push_back({prev->getFirstInstruction(), current->parent}); - } else if (kind == TransitionKind::StepOut) { - if (!stack.empty()) { - stack.pop_back(); - } - } - } - } - return stack; -} - -std::vector> -Path::asFunctionRanges() const { - assert(!KBlocks.empty()); - std::vector> ranges; - BlockRange range{0, 0}; - KFunction *function = KBlocks[0]->parent; - for (unsigned i = 1; i < KBlocks.size(); i++) { - if (getTransitionKind(KBlocks[i - 1], KBlocks[i]) == TransitionKind::None) { - if (i == KBlocks.size() - 1) { - range.last = i; - ranges.push_back({function, range}); - return ranges; - } else { - continue; - } - } - range.last = i - 1; - ranges.push_back({function, range}); - range.first = i; - function = KBlocks[i]->parent; - } - llvm_unreachable("asFunctionRanges reached the end of the for!"); -} - Path Path::concat(const Path &l, const Path &r) { Path path = l; for (auto block : r.KBlocks) { @@ -112,11 +51,16 @@ Path Path::concat(const Path &l, const Path &r) { std::string Path::toString() const { std::string blocks = ""; unsigned depth = 0; - for (unsigned i = 0; i < KBlocks.size(); i++) { - auto current = KBlocks[i]; + std::vector KBlocksVector; + KBlocksVector.reserve(KBlocks.size()); + for (auto kblock : KBlocks) { + KBlocksVector.push_back(kblock); + } + for (size_t i = 0; i < KBlocksVector.size(); i++) { + auto current = KBlocksVector[i]; KBlock *prev = nullptr; if (i != 0) { - prev = KBlocks[i - 1]; + prev = KBlocksVector[i - 1]; } auto kind = i == 0 ? TransitionKind::StepInto : getTransitionKind(prev, current);