ArrayExprHash.h

Go to the documentation of this file.

//===-- ArrayExprHash.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_ARRAYEXPRHASH_H
#define KLEE_ARRAYEXPRHASH_H
 
#include "klee/Expr/Expr.h"
#include "klee/Statistics/TimerStatIncrementer.h"
#include "klee/Solver/SolverStats.h"
 
#include <map>
#include <unordered_map>
 
namespace klee {
  
struct ArrayHashFn  {
  unsigned operator()(const Array* array) const {
    return(array ? array->hash() : 0);
  }
};
    
struct ArrayCmpFn {
  bool operator()(const Array* array1, const Array* array2) const {
    return(array1 == array2);
  }
};  
  
struct UpdateNodeHashFn  {
  unsigned operator()(const UpdateNode* un) const {
    return(un ? un->hash() : 0);
  }
};
    
struct UpdateNodeCmpFn {
  bool operator()(const UpdateNode* un1, const UpdateNode* un2) const {
    return(un1 == un2);
  }
};  
 
template<class T>
class ArrayExprHash {  
public:
  
  ArrayExprHash() {};
  // Note: Extend the class and overload the destructor if the objects of type T
  // that are to be hashed need to be explicitly destroyed
  // As an example, see class STPArrayExprHash
  virtual ~ArrayExprHash() {};
   
  bool lookupArrayExpr(const Array* array, T& exp) const;
  void hashArrayExpr(const Array* array, T& exp);  
  
  bool lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const;
  void hashUpdateNodeExpr(const UpdateNode* un, T& exp);  
  
protected:
  typedef std::unordered_map<const Array*, T, ArrayHashFn, ArrayCmpFn> ArrayHash;
  typedef typename ArrayHash::iterator ArrayHashIter;
  typedef typename ArrayHash::const_iterator ArrayHashConstIter;
  
  typedef std::unordered_map<const UpdateNode*, T, UpdateNodeHashFn, UpdateNodeCmpFn> UpdateNodeHash;
  typedef typename UpdateNodeHash::iterator UpdateNodeHashIter;
  typedef typename UpdateNodeHash::const_iterator UpdateNodeHashConstIter;
  
  ArrayHash      _array_hash;
  UpdateNodeHash _update_node_hash;  
};
 
 
template<class T>
bool ArrayExprHash<T>::lookupArrayExpr(const Array* array, T& exp) const {
  bool res = false;
  
#ifdef KLEE_ARRAY_DEBUG
  TimerStatIncrementer t(stats::arrayHashTime);
#endif
  
  assert(array);  
  ArrayHashConstIter it = _array_hash.find(array);
  if (it != _array_hash.end()) {
    exp = it->second;
    res = true;
  }  
  return res;
}
 
template<class T>
void ArrayExprHash<T>::hashArrayExpr(const Array* array, T& exp) {
  
#ifdef KLEE_ARRAY_DEBUG
   TimerStatIncrementer t(stats::arrayHashTime);
#endif
   
   assert(array);
  _array_hash[array] = exp;
}
 
template<class T>
bool ArrayExprHash<T>::lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const
{
  bool res = false;
  
#ifdef KLEE_ARRAY_DEBUG
  TimerStatIncrementer t(stats::arrayHashTime);
#endif
  
  assert(un);
  UpdateNodeHashConstIter it = _update_node_hash.find(un);
  if (it != _update_node_hash.end()) {
    exp = it->second;
    res = true;
  }  
  return res;
}
 
template<class T>
void ArrayExprHash<T>::hashUpdateNodeExpr(const UpdateNode* un, T& exp) 
{
#ifdef KLEE_ARRAY_DEBUG
  TimerStatIncrementer t(stats::arrayHashTime);
#endif
  
  assert(un);
  _update_node_hash[un] = exp;
}
 
}
 
#undef unordered_map
#undef unordered_set
 
#endif /* KLEE_ARRAYEXPRHASH_H */