diff options
| -rw-r--r-- | include/klee/Expr.h | 6 | ||||
| -rw-r--r-- | include/klee/util/Assignment.h | 7 | ||||
| -rw-r--r-- | include/klee/util/ExprRangeEvaluator.h | 2 | ||||
| -rw-r--r-- | lib/Expr/Updates.cpp | 4 | ||||
| -rw-r--r-- | lib/Solver/FastCexSolver.cpp | 15 | ||||
| -rw-r--r-- | lib/Solver/Solver.cpp | 5 |
6 files changed, 23 insertions, 16 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index ee3c3253..240c6220 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -675,15 +675,15 @@ public: static ref<Expr> create(const UpdateList &updates, ref<Expr> i); - Width getWidth() const { return updates.root->getRange(); } + Width getWidth() const { return updates.root ? updates.root->getRange() : Expr::Int8; } Kind getKind() const { return Read; } unsigned getNumKids() const { return numKids; } - ref<Expr> getKid(unsigned i) const { return !i ? index : 0; } + ref<Expr> getKid(unsigned i) const { return !i ? index : 0; } int compareContents(const Expr &b) const; - virtual ref<Expr> rebuild(ref<Expr> kids[]) const { + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(updates, kids[0]); } diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 838d03bd..63df4b65 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -67,15 +67,16 @@ namespace klee { inline ref<Expr> Assignment::evaluate(const Array *array, unsigned index) const { + assert(array); bindings_ty::const_iterator it = bindings.find(array); if (it!=bindings.end() && index<it->second.size()) { - return ConstantExpr::alloc(it->second[index], Expr::Int8); + return ConstantExpr::alloc(it->second[index], array->getRange()); } else { if (allowFreeValues) { return ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array->getDomain())); } else { - return ConstantExpr::alloc(0, Expr::Int8); + return ConstantExpr::alloc(0, array->getRange()); } } } diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h index 34b85520..fea30b5b 100644 --- a/include/klee/util/ExprRangeEvaluator.h +++ b/include/klee/util/ExprRangeEvaluator.h @@ -102,7 +102,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) { const ReadExpr *re = cast<ReadExpr>(e); T index = evaluate(re->index); - assert(re->getWidth()==Expr::Int8 && "unexpected multibyte read"); + assert(re->updates.root && re->getWidth() == re->updates.root->range && "unexpected multibyte read"); return evalRead(re->updates, index); } diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp index 14fd8308..107cf9d4 100644 --- a/lib/Expr/Updates.cpp +++ b/lib/Expr/Updates.cpp @@ -22,8 +22,12 @@ UpdateNode::UpdateNode(const UpdateNode *_next, next(_next), index(_index), value(_value) { + // FIXME: What we need to check here instead is that _value is of the same width + // as the range of the array that the update node is part of. + /* assert(_value->getWidth() == Expr::Int8 && "Update value should be 8-bit wide."); + */ computeHash(); if (next) { ++next->refCount; diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 08a9ef7c..6e52dc32 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -363,12 +363,12 @@ protected: // value cannot be part of the assignment. if (index >= array.size) return ReadExpr::create(UpdateList(&array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array.getDomain())); std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array); return ConstantExpr::alloc((it == objects.end() ? 127 : it->second->getPossibleValue(index)), - Expr::Int8); + array.getRange()); } public: @@ -384,19 +384,19 @@ protected: // value cannot be part of the assignment. if (index >= array.size) return ReadExpr::create(UpdateList(&array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array.getDomain())); std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array); if (it == objects.end()) return ReadExpr::create(UpdateList(&array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array.getDomain())); CexValueData cvd = it->second->getExactValues(index); if (!cvd.isFixed()) return ReadExpr::create(UpdateList(&array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array.getDomain())); - return ConstantExpr::alloc(cvd.min(), Expr::Int8); + return ConstantExpr::alloc(cvd.min(), array.getRange()); } public: @@ -1109,13 +1109,14 @@ FastCexSolver::computeInitialValues(const Query& query, // Propogation found a satisfying assignment, compute the initial values. for (unsigned i = 0; i != objects.size(); ++i) { const Array *array = objects[i]; + assert(array); std::vector<unsigned char> data; data.reserve(array->size); for (unsigned i=0; i < array->size; i++) { ref<Expr> read = ReadExpr::create(UpdateList(array, 0), - ConstantExpr::create(i, Expr::Int32)); + ConstantExpr::create(i, array->getDomain())); ref<Expr> value = cd.evaluatePossible(read); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) { diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 22b1545f..c61b6b1c 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -407,11 +407,12 @@ ValidatingSolver::computeInitialValues(const Query& query, std::vector< ref<Expr> > bindings; for (unsigned i = 0; i != values.size(); ++i) { const Array *array = objects[i]; + assert(array); for (unsigned j=0; j<array->size; j++) { unsigned char value = values[i][j]; bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(j, Expr::Int32)), - ConstantExpr::alloc(value, Expr::Int8))); + ConstantExpr::alloc(j, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); } } ConstraintManager tmp(bindings); |