From 78b1df8bd1664931fe32d186a21a7ebf58ad9489 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Tue, 9 Jun 2009 06:47:06 +0000 Subject: Remove Array::object. - The sole remaining client was IVC, which is currently disabled for other correctness issues. I patched it to compile and left a FIXME that we will have to resolve this before we can reenable IVC. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73129 91177308-0d34-0410-b5e6-96231b3b80d8 --- include/klee/Expr.h | 9 +++------ lib/Core/Executor.cpp | 4 +++- lib/Core/Memory.h | 4 ++-- lib/Expr/Parser.cpp | 4 ++-- unittests/Expr/ExprTest.cpp | 8 ++++---- unittests/Solver/SolverTest.cpp | 2 +- 6 files changed, 15 insertions(+), 16 deletions(-) diff --git a/include/klee/Expr.h b/include/klee/Expr.h index f13ab6d5..73734da3 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -29,7 +29,6 @@ namespace klee { class Array; class ConstantExpr; class ObjectState; -class MemoryObject; template class ref; @@ -474,8 +473,6 @@ private: class Array { public: const std::string name; - // FIXME: This does not belong here. - const MemoryObject *object; // FIXME: Not 64-bit clean. unsigned size; @@ -485,13 +482,13 @@ public: public: /// Array - Construct a new array object. /// - /// \param _name - The name for this arrays. Names should generally be unique + /// \param _name - The name for this array. Names should generally be unique /// across an application, but this is not necessary for correctness, except /// when printing expressions. When expressions are printed the output will /// not parse correctly since two arrays with the same name cannot be /// distinguished once printed. - Array(const std::string &_name, const MemoryObject *_object, uint64_t _size) - : name(_name), object(_object), size(_size), stpInitialArray(0) {} + Array(const std::string &_name, uint64_t _size) + : name(_name), size(_size), stpInitialArray(0) {} ~Array() { // FIXME: This relies on caller to delete the STP array. assert(!stpInitialArray && "Array must be deleted by caller!"); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ab2e106a..e47dcfc0 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3199,6 +3199,8 @@ void Executor::getCoveredLines(const ExecutionState &state, void Executor::doImpliedValueConcretization(ExecutionState &state, ref e, ref value) { + abort(); // FIXME: Broken until we sort out how to do the write back. + if (DebugCheckForImpliedValues) ImpliedValue::checkForImpliedValues(solver->solver, e, value); @@ -3211,7 +3213,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state, if (ConstantExpr *CE = dyn_cast(re->index)) { // FIXME: This is the sole remaining usage of the Array object // variable. Kill me. - const MemoryObject *mo = re->updates.root->object; + const MemoryObject *mo = 0; //re->updates.root->object; const ObjectState *os = state.addressSpace.findObject(mo); if (!os) { diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 141060d0..b6ea81d7 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -71,7 +71,7 @@ public: MemoryObject(uint64_t _address) : id(counter++), address(_address), - array(new Array("arr" + llvm::utostr(id), this, id)), + array(new Array("arr" + llvm::utostr(id), id)), size(0), isFixed(true), allocSite(0) { @@ -82,7 +82,7 @@ public: const llvm::Value *_allocSite) : id(counter++), address(_address), - array(new Array("arr" + llvm::utostr(id), this, _size)), + array(new Array("arr" + llvm::utostr(id), _size)), size(_size), name("unnamed"), isLocal(_isLocal), diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 856541ee..8e5349c5 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -519,7 +519,7 @@ DeclResult ParserImpl::ParseArrayDecl() { // FIXME: Array should take domain and range. const Identifier *Label = GetOrCreateIdentifier(Name); - Array *Root = new Array(Label->Name, 0, Size.get()); + Array *Root = new Array(Label->Name, Size.get()); ArrayDecl *AD = new ArrayDecl(Label, Size.get(), DomainType.get(), RangeType.get(), Root); @@ -1298,7 +1298,7 @@ VersionResult ParserImpl::ParseVersionSpecifier() { VersionResult Res = ParseVersion(); // Define update list to avoid use-of-undef errors. if (!Res.isValid()) { - Res = VersionResult(true, UpdateList(new Array("", 0, 0), NULL)); + Res = VersionResult(true, UpdateList(new Array("", 0), NULL)); } if (Label) diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp index b5f02b83..4b56f472 100644 --- a/unittests/Expr/ExprTest.cpp +++ b/unittests/Expr/ExprTest.cpp @@ -28,9 +28,9 @@ TEST(ExprTest, BasicConstruction) { } TEST(ExprTest, ConcatExtract) { - Array *array = new Array("arr0", 0, 256); + Array *array = new Array("arr0", 256); ref read8 = Expr::createTempRead(array, 8); - Array *array2 = new Array("arr1", 0, 256); + Array *array2 = new Array("arr1", 256); ref read8_2 = Expr::createTempRead(array2, 8); ref c100 = getConstant(100, 8); @@ -80,10 +80,10 @@ TEST(ExprTest, ConcatExtract) { } TEST(ExprTest, ExtractConcat) { - Array *array = new Array("arr2", 0, 256); + Array *array = new Array("arr2", 256); ref read64 = Expr::createTempRead(array, 64); - Array *array2 = new Array("arr3", 0, 256); + Array *array2 = new Array("arr3", 256); ref read8_2 = Expr::createTempRead(array2, 8); ref extract1 = ExtractExpr::create(read64, 36, 4); diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index 87ec63ef..cda0cf96 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -45,7 +45,7 @@ void testOperation(Solver &solver, unsigned size = Expr::getMinBytesForWidth(operandWidth); static uint64_t id = 0; - Array *array = new Array("arr" + llvm::utostr(++id), 0, size); + Array *array = new Array("arr" + llvm::utostr(++id), size); symbolicArgs.push_back(Expr::CreateArg(Expr::createTempRead(array, operandWidth))); } -- cgit 1.4.1