aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h24
-rw-r--r--lib/Core/StatsTracker.cpp6
-rw-r--r--lib/Expr/Expr.cpp12
-rw-r--r--lib/Expr/Updates.cpp6
-rw-r--r--lib/Solver/STPBuilder.cpp82
-rw-r--r--lib/Solver/STPBuilder.h17
-rw-r--r--lib/Solver/SolverStats.cpp4
-rw-r--r--lib/Solver/SolverStats.h4
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
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-15 20:24:28 +0000