From aa8cc67c0d8c16388ebe670757327a81f774d0ee Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Wed, 16 Apr 2014 17:56:13 +0100 Subject: Removing a few more hard-coded values for domains and ranges of Array objects --- lib/Expr/Updates.cpp | 4 ++++ lib/Solver/FastCexSolver.cpp | 15 ++++++++------- lib/Solver/Solver.cpp | 5 +++-- 3 files changed, 15 insertions(+), 9 deletions(-) (limited to 'lib') 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::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::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 data; data.reserve(array->size); for (unsigned i=0; i < array->size; i++) { ref read = ReadExpr::create(UpdateList(array, 0), - ConstantExpr::create(i, Expr::Int32)); + ConstantExpr::create(i, array->getDomain())); ref value = cd.evaluatePossible(read); if (ConstantExpr *CE = dyn_cast(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 > bindings; for (unsigned i = 0; i != values.size(); ++i) { const Array *array = objects[i]; + assert(array); for (unsigned j=0; jsize; 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); -- cgit 1.4.1 From 2795655e567c3cdbfe3d4815edd83b4f4cdbb542 Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Wed, 23 Apr 2014 20:20:33 +0100 Subject: Asserting that update lists have non-NULL roots within ReadExpr objects (update lists can have NULL roots, e.g. in MemoryObject instances with concrete contents, where root is allocated lazily only when the updates are required). Also checking whether array updates are typed correctly in UpdateList::extend() rather than in the constructor of UpdateNode (only for update lists with non-NULL roots). --- include/klee/Expr.h | 4 ++-- lib/Expr/Updates.cpp | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 240c6220..a302591a 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -675,7 +675,7 @@ public: static ref create(const UpdateList &updates, ref i); - Width getWidth() const { return updates.root ? updates.root->getRange() : Expr::Int8; } + Width getWidth() const { assert(updates.root); return updates.root->getRange(); } Kind getKind() const { return Read; } unsigned getNumKids() const { return numKids; } @@ -691,7 +691,7 @@ public: private: ReadExpr(const UpdateList &_updates, const ref &_index) : - updates(_updates), index(_index) {} + updates(_updates), index(_index) { assert(updates.root); } public: static bool classof(const Expr *E) { diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp index 107cf9d4..bf7049ba 100644 --- a/lib/Expr/Updates.cpp +++ b/lib/Expr/Updates.cpp @@ -88,6 +88,12 @@ UpdateList &UpdateList::operator=(const UpdateList &b) { } void UpdateList::extend(const ref &index, const ref &value) { + + if (root) { + assert(root->getDomain() == index->getWidth()); + assert(root->getRange() == value->getWidth()); + } + if (head) --head->refCount; head = new UpdateNode(head, index, value); ++head->refCount; -- cgit 1.4.1