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.

2 files changed, 93 insertions, 27 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index c5a110f8..731aa446 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -32,6 +32,7 @@ namespace llvm {
 namespace klee {
 
 class Array;
+class ArrayCache;
 class ConstantExpr;
 class ObjectState;
 
@@ -619,21 +620,10 @@ public:
 private:
   unsigned hashValue;
 
-
-  /// 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<unsigned> >.  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 < unsigned, std::vector < const Array * > * > symbolicArraySingletonMap;
-
-  // This shouldn't be allowed since it is a singleton class
+  // FIXME: Make =delete when we switch to C++11
   Array(const Array& array);
 
-  // This shouldn't be allowed since it is a singleton class
+  // FIXME: Make =delete when we switch to C++11
   Array& operator =(const Array& array);
 
   ~Array();
@@ -675,20 +665,7 @@ public:
   /// ComputeHash must take into account the name, the size, the domain, and the range
   unsigned computeHash();
   unsigned hash() const { return hashValue; }
-
-  /*
-   * 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<ConstantExpr> *constantValuesBegin = 0,
-				   const ref<ConstantExpr> *constantValuesEnd = 0,
-				   Expr::Width _domain = Expr::Int32,
-				   Expr::Width _range = Expr::Int8);
+  friend class ArrayCache;
 };
 
 /// Class representing a complete list of updates into an array.
diff --git a/include/klee/util/ArrayCache.h b/include/klee/util/ArrayCache.h
new file mode 100644
index 00000000..3dd88a11
--- /dev/null
+++ b/include/klee/util/ArrayCache.h
@@ -0,0 +1,89 @@
+//===-- ArrayCache.h --------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_ARRAY_CACHE_H
+#define KLEE_ARRAY_CACHE_H
+
+#include "klee/Expr.h"
+
+// FIXME: Remove this hack when we switch to C++11
+#ifdef _LIBCPP_VERSION
+#include <unordered_set>
+#define unordered_set std::unordered_set
+#else
+#include <tr1/unordered_set>
+#define unordered_set std::tr1::unordered_set
+#endif
+
+#include <string>
+#include <vector>
+
+namespace klee {
+
+// FIXME: This is copied from ``klee/util/ArrayExprHash.h``.
+// We can't include it here becaues the includes are messed up
+// in that file.
+struct EquivArrayHashFn {
+  unsigned operator()(const Array *array) const {
+    return (array ? array->hash() : 0);
+  }
+};
+
+struct EquivArrayCmpFn {
+  bool operator()(const Array *array1, const Array *array2) const {
+    if (array1 == NULL || array2 == NULL)
+      return false;
+    return (array1->size == array2->size) && (array1->name == array2->name);
+  }
+};
+
+/// Provides an interface for creating and destroying Array objects.
+class ArrayCache {
+public:
+  ArrayCache() {}
+  ~ArrayCache();
+  /// Create an Array object.
+  //
+  /// Symbolic Arrays are cached so that only one instance exists. This
+  /// provides a limited form of "alpha-renaming". Constant arrays are not
+  /// cached.
+  ///
+  /// This class retains ownership of Array object so that upon destruction
+  /// of this object all allocated Array objects are deleted.
+  ///
+  /// \param _name The name of the array
+  /// \param _size The size of the array in bytes
+  /// \param constantValuesBegin A pointer to the beginning of a block of
+  //         memory that constains a ``ref<ConstantExpr>`` (i.e. concrete values
+  //         for the //array). This should be NULL for symbolic arrays.
+  /// for symbolic arrays.
+  /// \param constantValuesEnd A pointer +1 pass the end of a block of memory
+  ///        that contains a ``ref<ConstantExpr>``. This should be NULL for a
+  ///        symbolic array.
+  /// \param _domain The size of the domain (i.e. the bitvector used to index
+  /// the array)
+  /// \param _range The size of range (i.e. the bitvector that is indexed to)
+  const Array *CreateArray(const std::string &_name, uint64_t _size,
+                           const ref<ConstantExpr> *constantValuesBegin = 0,
+                           const ref<ConstantExpr> *constantValuesEnd = 0,
+                           Expr::Width _domain = Expr::Int32,
+                           Expr::Width _range = Expr::Int8);
+
+private:
+  typedef unordered_set<const Array *, klee::EquivArrayHashFn,
+                        klee::EquivArrayCmpFn> ArrayHashMap;
+  ArrayHashMap cachedSymbolicArrays;
+  typedef std::vector<const Array *> ArrayPtrVec;
+  ArrayPtrVec concreteArrays;
+};
+}
+
+#undef unordered_set
+
+#endif /* KLEE_ARRAY_CACHE__H */