diff options
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/Expr.h | 31 | ||||
-rw-r--r-- | include/klee/util/ArrayCache.h | 89 |
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 */ |