From f049ff3bc04daead8c3bb9f06e89e71e2054c82a Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 16 Feb 2015 13:16:12 -0500 Subject: Added factory method for Arrays + hid constructors from outside calls The way that Arrays were handled in the past led to the possibility of aliasing issues. This occured whenever a new branch discovered an array for the first time. Each branch would create a new instance of the same array without seeing if it had been created before. Therefore, should a new branch encounter the same state as some previous branch, the previous branch's solution wouldn't satisfy the new state since they didn't recognize they were referencing the same array. By creating an array factory that creates a single symbolic array, that problem is handled. Note: Concrete arrays should not be created by the factory method since their values are never shared between branches. The factory works by seeing if an array with a similar hash has been created before (the hash is based on the name and size of array). If there has been it then searches through all of the arrays with the same hash (stored in a vector) to see if there is one with an exact match. If there is one, the address of this previously created equivalent array is returned. Otherwise, the newly created array is unique, it is added to the map, and it's address is returned. This aliasing issue can be seen by comparing the output of the Dogfood/ImmutableSet.cpp test cases with and with out this commit. Both act correctly, but the number of queries making it to the solver in the previous version is much greater 244 vs 211. This is because the UBTree in the CexCachingSolver and the cache in the CachingSolver do not recognize queries whose solutions were previously calculated because it doesn't think the arrays in the two queries are the same. While this does not cause an error, it does mean that extra calls are made. --- lib/Expr/Expr.cpp | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) (limited to 'lib/Expr/Expr.cpp') diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index d54b8f4d..46ea30fc 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -490,10 +490,46 @@ unsigned Array::computeHash() { unsigned res = 0; for (unsigned i = 0, e = name.size(); i != e; ++i) res = (res * Expr::MAGIC_HASH_CONSTANT) + name[i]; + res = (res * Expr::MAGIC_HASH_CONSTANT) + size; hashValue = res; return hashValue; } +std::map *> Array::symbolicArraySingletonMap; + +const Array * Array::CreateArray(const std::string &_name, uint64_t _size, + const ref *constantValuesBegin, + const ref *constantValuesEnd, + Expr::Width _domain, + Expr::Width _range){ + + const Array * array = new Array(_name, _size, constantValuesBegin, constantValuesEnd, _domain,_range); + if(array->constantValues.size() == 0){ + //means is a symbolic array and we should look up the values; + unsigned hash = array->hash(); + std::vector * bucket = Array::symbolicArraySingletonMap[hash]; + if(bucket){ + for(std::vector::const_iterator it = bucket->begin(); + it != bucket->end(); it ++){ + const Array* prospect = *it; + if(prospect->size == array->size && prospect->name == array->name){ + delete array; + return prospect; + } + } + bucket->push_back(array); + return array; + }else{ + bucket = new std::vector(); + bucket->push_back(array); + Array::symbolicArraySingletonMap[hash] = bucket; + return array; + } + }else{ + return array; + } +} + /***/ ref ReadExpr::create(const UpdateList &ul, ref index) { -- cgit 1.4.1 From 1c10b2b52a4f91f62bc9ef632032d7f0ade0307c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 27 Feb 2015 19:03:46 +0000 Subject: Improved some comments and fixed some formatting issues in the Array factory patch. --- include/klee/Expr.h | 49 ++++++++++++++++++++++++++----------------------- lib/Core/Executor.cpp | 2 +- lib/Core/Memory.cpp | 4 ++-- lib/Expr/Expr.cpp | 17 ++++++++--------- lib/Expr/Parser.cpp | 2 +- 5 files changed, 38 insertions(+), 36 deletions(-) (limited to 'lib/Expr/Expr.cpp') diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 2ea7f40f..af8bf10f 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -601,7 +601,7 @@ private: class Array { public: - //Name of the array + // Name of the array const std::string name; // FIXME: Not 64-bit clean. @@ -620,18 +620,20 @@ private: unsigned hashValue; - /// The symbolic array singleton map is necessary to prevent aliasing issues on arrays. - /// A lot of the Solvers use maps such as >. - /// This causes problems because stored answers can't be easily recovered. - /// Even worse, in read expressions, such as (read array 32), array is a pointer, - /// meaning actual solutions don't "work" because the two instances of array + /// The symbolic array singleton map is necessary to allow sharing + /// of Arrays across states, essentially performing a (limited) form + /// of alpha renaming. Some Solvers use maps such as < const *Array, + /// std::vector >. This causes problems because stored + /// answers can't be easily recovered. Even worse, in read + /// expressions, such as (read array 32), array is a pointer, and + /// cached solutions are missed because the two Array instances /// aren't recognized as the same. - static std::map *> symbolicArraySingletonMap; + static std::map < unsigned, std::vector < const Array * > * > symbolicArraySingletonMap; - //This shouldn't be allowed since it's a singleton class + // This shouldn't be allowed since it is a singleton class Array(const Array& array); - //This shouldn't be allowed since it's a singleton class + // This shouldn't be allowed since it is a singleton class Array& operator =(const Array& array); ~Array(); @@ -644,11 +646,12 @@ private: /// not parse correctly since two arrays with the same name cannot be /// distinguished once printed. Array(const std::string &_name, uint64_t _size, - const ref *constantValuesBegin = 0, - const ref *constantValuesEnd = 0, - Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8) + const ref *constantValuesBegin = 0, + const ref *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8) : name(_name), size(_size), domain(_domain), range(_range), - constantValues(constantValuesBegin, constantValuesEnd) { + constantValues(constantValuesBegin, constantValuesEnd) { + assert((isSymbolicArray() || constantValues.size() == size) && "Invalid size for constant array!"); computeHash(); @@ -674,18 +677,18 @@ public: unsigned hash() const { return hashValue; } /* - * Fairly simple idea. Since by defn (see Array), symbolic arrays - * have constant values of size 0. Concrete Arrays have their respective - * values stored in each element. Therefore, each incoming call is tested. - * An array is created and, if it's concrete, it's simply returned. If - * instead it is symbolic, then a map is checked to see if it was created - * before, so there is only a single instance floating out there. + * Fairly simple idea. Symbolic arrays have constant values of size + * 0, while concrete arrays have constant values of size > 0. + * Therefore, on each call, an array is created and, if it is + * concrete, it is simply returned. If instead it is symbolic, then + * a map is checked to see if it was created before, so there is + * only a single instance floating out there. */ static const Array * CreateArray(const std::string &_name, uint64_t _size, - const ref *constantValuesBegin = 0, - const ref *constantValuesEnd = 0, - Expr::Width _domain = Expr::Int32, - Expr::Width _range = Expr::Int8); + const ref *constantValuesBegin = 0, + const ref *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, + Expr::Width _range = Expr::Int8); }; /// Class representing a complete list of updates into an array. diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8631061f..c78c9f8a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2925,7 +2925,7 @@ ref Executor::replaceReadWithSymbolic(ExecutionState &state, static unsigned id; const Array *array = Array::CreateArray("rrws_arr" + llvm::utostr(++id), - Expr::getMinBytesForWidth(e->getWidth())); + Expr::getMinBytesForWidth(e->getWidth())); ref res = Expr::createTempRead(array, e->getWidth()); ref eq = NotOptimizedExpr::create(EqExpr::create(e, res)); llvm::errs() << "Making symbolic: " << eq << "\n"; diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index b9f6afd0..1dd1e1fd 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -223,8 +223,8 @@ const UpdateList &ObjectState::getUpdates() const { // FIXME: Leaked. static unsigned id = 0; const Array *array = Array::CreateArray("const_arr" + llvm::utostr(++id), size, - &Contents[0], - &Contents[0] + Contents.size()); + &Contents[0], + &Contents[0] + Contents.size()); updates = UpdateList(array, 0); // Apply the remaining (non-constant) writes. diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 46ea30fc..baa85663 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -501,31 +501,30 @@ const Array * Array::CreateArray(const std::string &_name, uint64_t _size, const ref *constantValuesBegin, const ref *constantValuesEnd, Expr::Width _domain, - Expr::Width _range){ + Expr::Width _range) { const Array * array = new Array(_name, _size, constantValuesBegin, constantValuesEnd, _domain,_range); - if(array->constantValues.size() == 0){ - //means is a symbolic array and we should look up the values; + if (array->constantValues.size() == 0) { // symbolic array unsigned hash = array->hash(); std::vector * bucket = Array::symbolicArraySingletonMap[hash]; - if(bucket){ - for(std::vector::const_iterator it = bucket->begin(); - it != bucket->end(); it ++){ + if (bucket){ + for (std::vector::const_iterator it = bucket->begin(); + it != bucket->end(); it ++){ const Array* prospect = *it; - if(prospect->size == array->size && prospect->name == array->name){ + if (prospect->size == array->size && prospect->name == array->name){ delete array; return prospect; } } bucket->push_back(array); return array; - }else{ + } else { bucket = new std::vector(); bucket->push_back(array); Array::symbolicArraySingletonMap[hash] = bucket; return array; } - }else{ + } else { // concrete array return array; } } diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 9df08903..23a292fa 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -522,7 +522,7 @@ DeclResult ParserImpl::ParseArrayDecl() { const Array *Root; if (!Values.empty()) Root = Array::CreateArray(Label->Name, Size.get(), - &Values[0], &Values[0] + Values.size()); + &Values[0], &Values[0] + Values.size()); else Root = Array::CreateArray(Label->Name, Size.get()); ArrayDecl *AD = new ArrayDecl(Label, Size.get(), -- cgit 1.4.1