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/ArrayCache.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/ArrayCache.cpp')
| -rw-r--r-- | lib/Expr/ArrayCache.cpp | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/lib/Expr/ArrayCache.cpp b/lib/Expr/ArrayCache.cpp new file mode 100644 index 00000000..b669f237 --- /dev/null +++ b/lib/Expr/ArrayCache.cpp @@ -0,0 +1,47 @@ +#include "klee/util/ArrayCache.h" + +namespace klee { + +ArrayCache::~ArrayCache() { + // Free Allocated Array objects + for (ArrayHashMap::iterator ai = cachedSymbolicArrays.begin(), + e = cachedSymbolicArrays.end(); + ai != e; ++ai) { + delete *ai; + } + for (ArrayPtrVec::iterator ai = concreteArrays.begin(), + e = concreteArrays.end(); + ai != e; ++ai) { + delete *ai; + } +} + +const Array * +ArrayCache::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->isSymbolicArray()) { + std::pair<ArrayHashMap::const_iterator, bool> success = + cachedSymbolicArrays.insert(array); + if (success.second) { + // Cache miss + return array; + } + // Cache hit + delete array; + array = *(success.first); + assert(array->isSymbolicArray() && + "Cached symbolic array is no longer symbolic"); + return array; + } else { + // Treat every constant array as distinct so we never cache them + assert(array->isConstantArray()); + concreteArrays.push_back(array); // For deletion later + return array; + } +} +} |