diff options
| -rw-r--r-- | include/klee/Expr.h | 24 | ||||
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 6 | ||||
| -rw-r--r-- | lib/Expr/Expr.cpp | 12 | ||||
| -rw-r--r-- | lib/Expr/Updates.cpp | 6 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 82 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.h | 17 | ||||
| -rw-r--r-- | lib/Solver/SolverStats.cpp | 4 | ||||
| -rw-r--r-- | lib/Solver/SolverStats.h | 4 |
8 files changed, 109 insertions, 46 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 2852bf81..41d980a6 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -535,12 +535,9 @@ public: /// Class representing a byte update of an array. class UpdateNode { - friend class UpdateList; - friend class STPBuilder; // for setting STPArray + friend class UpdateList; mutable unsigned refCount; - // gross - mutable void *stpArray; // cache instead of recalc unsigned hashValue; @@ -563,7 +560,7 @@ public: unsigned hash() const { return hashValue; } private: - UpdateNode() : refCount(0), stpArray(0) {} + UpdateNode() : refCount(0) {} ~UpdateNode(); unsigned computeHash(); @@ -573,16 +570,13 @@ class Array { public: const std::string name; // FIXME: Not 64-bit clean. - unsigned size; + unsigned size; /// constantValues - The constant initial values for this array, or empty for /// a symbolic array. If non-empty, this size of this array is equivalent to /// the array size. const std::vector< ref<ConstantExpr> > constantValues; - - // FIXME: This does not belong here. - mutable void *stpInitialArray; - + public: /// Array - Construct a new array object. /// @@ -595,10 +589,10 @@ public: const ref<ConstantExpr> *constantValuesBegin = 0, const ref<ConstantExpr> *constantValuesEnd = 0) : name(_name), size(_size), - constantValues(constantValuesBegin, constantValuesEnd), - stpInitialArray(0) { + constantValues(constantValuesBegin, constantValuesEnd) { assert((isSymbolicArray() || constantValues.size() == size) && "Invalid size for constant array!"); + computeHash(); #ifndef NDEBUG for (const ref<ConstantExpr> *it = constantValuesBegin; it != constantValuesEnd; ++it) @@ -613,6 +607,12 @@ public: Expr::Width getDomain() const { return Expr::Int32; } Expr::Width getRange() const { return Expr::Int8; } + + unsigned computeHash(); + unsigned hash() const { return hashValue; } + +private: + unsigned hashValue; }; /// Class representing a complete list of updates into an array. diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index e2fa0d35..f81d19d8 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -372,6 +372,9 @@ void StatsTracker::writeStatsHeader() { << "'CexCacheTime'," << "'ForkTime'," << "'ResolveTime'," +#ifdef DEBUG + << "'ArrayHashTime'," +#endif << ")\n"; statsFile->flush(); } @@ -399,6 +402,9 @@ void StatsTracker::writeStatsLine() { << "," << stats::cexCacheTime / 1000000. << "," << stats::forkTime / 1000000. << "," << stats::resolveTime / 1000000. +#ifdef DEBUG + << "," << stats::arrayHashTime / 1000000. +#endif << ")\n"; statsFile->flush(); } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 089e78b3..fa8525b6 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -488,11 +488,13 @@ ref<Expr> NotOptimizedExpr::create(ref<Expr> src) { extern "C" void vc_DeleteExpr(void*); Array::~Array() { - // FIXME: This shouldn't be necessary. - if (stpInitialArray) { - ::vc_DeleteExpr(stpInitialArray); - stpInitialArray = 0; - } +} + +unsigned Array::computeHash() { + unsigned res = 0; + for (unsigned i = 0, e = name.size(); i != e; ++i) + res = (res * Expr::MAGIC_HASH_CONSTANT) + name[i]; + return res; } /***/ diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp index 379f1c8d..14fd8308 100644 --- a/lib/Expr/Updates.cpp +++ b/lib/Expr/Updates.cpp @@ -18,8 +18,7 @@ using namespace klee; UpdateNode::UpdateNode(const UpdateNode *_next, const ref<Expr> &_index, const ref<Expr> &_value) - : refCount(0), - stpArray(0), + : refCount(0), next(_next), index(_index), value(_value) { @@ -36,9 +35,6 @@ UpdateNode::UpdateNode(const UpdateNode *_next, extern "C" void vc_DeleteExpr(void*); UpdateNode::~UpdateNode() { - // XXX gross - if (stpArray) - ::vc_DeleteExpr(stpArray); } int UpdateNode::compare(const UpdateNode &b) const { diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index b1289f8d..789eb244 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -50,6 +50,32 @@ namespace { /// + +STPArrayExprHash::~STPArrayExprHash() { + + // Design decision: STPArrayExprHash is destroyed from the destructor of STPBuilder at the end of the KLEE run; + // Therefore, freeing memory allocated for STP::VCExpr's is currently disabled. + + /* + for (ArrayHashIter it = _array_hash.begin(); it != _array_hash.end(); ++it) { + ::VCExpr array_expr = it->second; + if (array_expr) { + ::vc_DeleteExpr(array_expr); + array_expr = 0; + } + } + + + for (UpdateNodeHashConstIter it = _update_node_hash.begin(); it != _update_node_hash.end(); ++it) { + ::VCExpr un_expr = it->second; + if (un_expr) { + ::vc_DeleteExpr(un_expr); + un_expr = 0; + } + } + */ +} + /***/ STPBuilder::STPBuilder(::VC _vc, bool _optimizeDivides) @@ -62,6 +88,7 @@ STPBuilder::STPBuilder(::VC _vc, bool _optimizeDivides) } STPBuilder::~STPBuilder() { + } /// @@ -399,9 +426,12 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width } ::VCExpr STPBuilder::getInitialArray(const Array *root) { - if (root->stpInitialArray) { - return root->stpInitialArray; - } else { + + assert(root); + ::VCExpr array_expr; + bool hashed = _arr_hash.lookupArrayExpr(root, array_expr); + + if (!hashed) { // STP uniques arrays by name, so we make sure the name is unique by // including the address. char buf[32]; @@ -410,24 +440,25 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width memmove(buf + space, buf, addrlen); // moving the address part to the end memcpy(buf, root->name.c_str(), space); // filling out the name part - root->stpInitialArray = buildArray(buf, 32, 8); - + array_expr = buildArray(buf, 32, 8); + if (root->isConstantArray()) { // FIXME: Flush the concrete values into STP. Ideally we would do this // using assertions, which is much faster, but we need to fix the caching // to work correctly in that case. for (unsigned i = 0, e = root->size; i != e; ++i) { - ::VCExpr prev = root->stpInitialArray; - root->stpInitialArray = - vc_writeExpr(vc, prev, + ::VCExpr prev = array_expr; + array_expr = vc_writeExpr(vc, prev, construct(ConstantExpr::alloc(i, root->getDomain()), 0), construct(root->constantValues[i], 0)); - vc_DeleteExpr(prev); + vc_DeleteExpr(prev); } } - - return root->stpInitialArray; + + _arr_hash.hashArrayExpr(root, array_expr); } + + return(array_expr); } ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) { @@ -437,16 +468,23 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) { ::VCExpr STPBuilder::getArrayForUpdate(const Array *root, const UpdateNode *un) { if (!un) { - return getInitialArray(root); - } else { - // FIXME: This really needs to be non-recursive. - if (!un->stpArray) - un->stpArray = vc_writeExpr(vc, - getArrayForUpdate(root, un->next), - construct(un->index, 0), - construct(un->value, 0)); - - return un->stpArray; + return(getInitialArray(root)); + } + else { + // FIXME: This really needs to be non-recursive. + ::VCExpr un_expr; + bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); + + if (!hashed) { + un_expr = vc_writeExpr(vc, + getArrayForUpdate(root, un->next), + construct(un->index, 0), + construct(un->value, 0)); + + _arr_hash.hashUpdateNodeExpr(un, un_expr); + } + + return(un_expr); } } @@ -884,3 +922,5 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { return vc_trueExpr(vc); } } + + diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 3a19a639..0a99b753 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -11,10 +11,10 @@ #define __UTIL_STPBUILDER_H__ #include "klee/util/ExprHashMap.h" +#include "klee/util/ArrayExprHash.h" #include "klee/Config/config.h" #include <vector> -#include <map> #define Expr VCExpr #include <stp/c_interface.h> @@ -56,6 +56,15 @@ namespace klee { operator bool () { return H->expr; } operator ::VCExpr () { return H->expr; } }; + + class STPArrayExprHash : public ArrayExprHash< ::VCExpr > { + + friend class STPBuilder; + + public: + STPArrayExprHash() {}; + virtual ~STPArrayExprHash(); + }; class STPBuilder { ::VC vc; @@ -67,7 +76,9 @@ class STPBuilder { /// use. bool optimizeDivides; -private: + STPArrayExprHash _arr_hash; + +private: unsigned getShiftBits(unsigned amount) { unsigned bits = 1; amount--; @@ -109,7 +120,7 @@ private: ::VCExpr buildVar(const char *name, unsigned width); ::VCExpr buildArray(const char *name, unsigned indexWidth, unsigned valueWidth); - + public: STPBuilder(::VC _vc, bool _optimizeDivides=true); ~STPBuilder(); diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp index 9d48792a..1f85fe88 100644 --- a/lib/Solver/SolverStats.cpp +++ b/lib/Solver/SolverStats.cpp @@ -21,3 +21,7 @@ Statistic stats::queryConstructTime("QueryConstructTime", "QBtime") ; Statistic stats::queryConstructs("QueriesConstructs", "QB"); Statistic stats::queryCounterexamples("QueriesCEX", "Qcex"); Statistic stats::queryTime("QueryTime", "Qtime"); + +#ifdef DEBUG +Statistic stats::arrayHashTime("ArrayHashTime", "AHtime"); +#endif diff --git a/lib/Solver/SolverStats.h b/lib/Solver/SolverStats.h index 6fee7699..56bdf999 100644 --- a/lib/Solver/SolverStats.h +++ b/lib/Solver/SolverStats.h @@ -25,6 +25,10 @@ namespace stats { extern Statistic queryConstructs; extern Statistic queryCounterexamples; extern Statistic queryTime; + +#ifdef DEBUG + extern Statistic arrayHashTime; +#endif } } |