ArrayCache.h

Go to the documentation of this file.

//===-- 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_ARRAYCACHE_H
#define KLEE_ARRAYCACHE_H
 
#include "klee/Expr/Expr.h"
#include "klee/Expr/ArrayExprHash.h" // For klee::ArrayHashFn
 
#include <string>
#include <unordered_set>
#include <vector>
 
namespace klee {
 
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);
  }
};
 
class ArrayCache {
public:
  ArrayCache() {}
  ~ArrayCache();
  //
  //         memory that constains a ``ref<ConstantExpr>`` (i.e. concrete values
  //         for the //array). This should be NULL for symbolic arrays.
  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 std::unordered_set<const Array *, klee::ArrayHashFn,
                             klee::EquivArrayCmpFn>
      ArrayHashMap;
  ArrayHashMap cachedSymbolicArrays;
  typedef std::vector<const Array *> ArrayPtrVec;
  ArrayPtrVec concreteArrays;
};
}
 
#endif /* KLEE_ARRAYCACHE_H */