diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-12-16 18:13:11 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-12-18 11:22:50 +0000 |
commit | 53ff7a002a8213a5d5e778bef2a895998d9890e1 (patch) | |
tree | 026a4f1b16c1996755954f7824e0d10f8ed0ef8e /lib/Expr/Expr.cpp | |
parent | 7e75fa79b2e76251c2cd417a7eae8a7620b014ae (diff) | |
download | klee-53ff7a002a8213a5d5e778bef2a895998d9890e1.tar.gz |
Fix memory leaks of ``Array`` objects detected by ASan.
Some of these leaks were introduced by the factory constructor for Array objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have been around for far longer. This leak was fixed by introducing a ``ArrayCache`` object which has two purposes * Retains ownership of all created ``Array`` objects and destroys them when the ``ArrayCache`` destructor is called. * Mimic the caching behaviour for symbolic arrays that was introduced by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same name and size get "uniqued". The Executor now maintains a ``arrayCache`` member that it uses and passes by pointer to objects that need to construct ``Array`` objects (i.e. ``ObjectState``). This way when the Executor is destroyed all the ``Array`` objects get freed which seems like the right time to do this. For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is used for building ``Array`` objects. This means that the Parser must live as long as the built expressions will be used otherwise we will have a use after free. I'm not sure this is the right design choice. It might be better to transfer ownership of the ``Array`` objects to the root ``Decl`` returned by the parser.
Diffstat (limited to 'lib/Expr/Expr.cpp')
-rw-r--r-- | lib/Expr/Expr.cpp | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index baa85663..2c64aff4 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -494,41 +494,6 @@ unsigned Array::computeHash() { hashValue = res; return hashValue; } - -std::map<unsigned, std::vector<const Array *> *> Array::symbolicArraySingletonMap; - -const Array * Array::CreateArray(const std::string &_name, uint64_t _size, - const ref<ConstantExpr> *constantValuesBegin, - const ref<ConstantExpr> *constantValuesEnd, - Expr::Width _domain, - Expr::Width _range) { - - const Array * array = new Array(_name, _size, constantValuesBegin, constantValuesEnd, _domain,_range); - if (array->constantValues.size() == 0) { // symbolic array - unsigned hash = array->hash(); - std::vector<const Array *> * bucket = Array::symbolicArraySingletonMap[hash]; - if (bucket){ - for (std::vector<const Array*>::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<const Array *>(); - bucket->push_back(array); - Array::symbolicArraySingletonMap[hash] = bucket; - return array; - } - } else { // concrete array - return array; - } -} - /***/ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) { |