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