klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ArrayExprHash.h
Go to the documentation of this file.
1 //===-- ArrayExprHash.h --------------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef __UTIL_ARRAYEXPRHASH_H__
11 #define __UTIL_ARRAYEXPRHASH_H__
12 
13 #include "klee/Expr.h"
15 #include "SolverStats.h"
16 
17 #include <map>
18 #include <tr1/unordered_map>
19 
20 namespace klee {
21 
22 struct ArrayHashFn {
23  unsigned operator()(const Array* array) const {
24  return(array ? array->hash() : 0);
25  }
26 };
27 
28 struct ArrayCmpFn {
29  bool operator()(const Array* array1, const Array* array2) const {
30  return(array1 == array2);
31  }
32 };
33 
35  unsigned operator()(const UpdateNode* un) const {
36  return(un ? un->hash() : 0);
37  }
38 };
39 
41  bool operator()(const UpdateNode* un1, const UpdateNode* un2) const {
42  return(un1 == un2);
43  }
44 };
45 
46 template<class T>
47 class ArrayExprHash {
48 public:
49 
51  // Note: Extend the class and overload the destructor if the objects of type T
52  // that are to be hashed need to be explicitly destroyed
53  // As an example, see class STPArrayExprHash
54  virtual ~ArrayExprHash() {};
55 
56  bool lookupArrayExpr(const Array* array, T& exp) const;
57  void hashArrayExpr(const Array* array, T& exp);
58 
59  bool lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const;
60  void hashUpdateNodeExpr(const UpdateNode* un, T& exp);
61 
62 protected:
63  typedef std::tr1::unordered_map<const Array*, T, ArrayHashFn, ArrayCmpFn> ArrayHash;
64  typedef typename ArrayHash::iterator ArrayHashIter;
65  typedef typename ArrayHash::const_iterator ArrayHashConstIter;
66 
67  typedef std::tr1::unordered_map<const UpdateNode*, T, UpdateNodeHashFn, UpdateNodeCmpFn> UpdateNodeHash;
68  typedef typename UpdateNodeHash::iterator UpdateNodeHashIter;
69  typedef typename UpdateNodeHash::const_iterator UpdateNodeHashConstIter;
70 
73 };
74 
75 
76 template<class T>
77 bool ArrayExprHash<T>::lookupArrayExpr(const Array* array, T& exp) const {
78  bool res = false;
79 
80 #ifdef DEBUG
81  TimerStatIncrementer t(stats::arrayHashTime);
82 #endif
83 
84  assert(array);
85  ArrayHashConstIter it = _array_hash.find(array);
86  if (it != _array_hash.end()) {
87  exp = it->second;
88  res = true;
89  }
90  return(res);
91 }
92 
93 template<class T>
94 void ArrayExprHash<T>::hashArrayExpr(const Array* array, T& exp) {
95 
96 #ifdef DEBUG
97  TimerStatIncrementer t(stats::arrayHashTime);
98 #endif
99 
100  assert(array);
101  _array_hash[array] = exp;
102 }
103 
104 template<class T>
106 {
107  bool res = false;
108 
109 #ifdef DEBUG
110  TimerStatIncrementer t(stats::arrayHashTime);
111 #endif
112 
113  assert(un);
114  UpdateNodeHashConstIter it = _update_node_hash.find(un);
115  if (it != _update_node_hash.end()) {
116  exp = it->second;
117  res = true;
118  }
119  return(res);
120 }
121 
122 template<class T>
124 {
125 #ifdef DEBUG
126  TimerStatIncrementer t(stats::arrayHashTime);
127 #endif
128 
129  assert(un);
130  _update_node_hash[un] = exp;
131 }
132 
133 }
134 
135 #endif
std::tr1::unordered_map< const UpdateNode *, T, UpdateNodeHashFn, UpdateNodeCmpFn > UpdateNodeHash
Definition: ArrayExprHash.h:67
unsigned operator()(const UpdateNode *un) const
Definition: ArrayExprHash.h:35
void hashArrayExpr(const Array *array, T &exp)
Definition: ArrayExprHash.h:94
std::tr1::unordered_map< const Array *, T, ArrayHashFn, ArrayCmpFn > ArrayHash
Definition: ArrayExprHash.h:63
unsigned hash() const
Definition: Expr.h:592
void hashUpdateNodeExpr(const UpdateNode *un, T &exp)
UpdateNodeHash _update_node_hash
Definition: ArrayExprHash.h:72
UpdateNodeHash::iterator UpdateNodeHashIter
Definition: ArrayExprHash.h:68
unsigned hash() const
Definition: Expr.h:648
bool lookupUpdateNodeExpr(const UpdateNode *un, T &exp) const
unsigned operator()(const Array *array) const
Definition: ArrayExprHash.h:23
Class representing a byte update of an array.
Definition: Expr.h:569
ArrayHash::iterator ArrayHashIter
Definition: ArrayExprHash.h:64
virtual ~ArrayExprHash()
Definition: ArrayExprHash.h:54
UpdateNodeHash::const_iterator UpdateNodeHashConstIter
Definition: ArrayExprHash.h:69
bool lookupArrayExpr(const Array *array, T &exp) const
Definition: ArrayExprHash.h:77
ArrayHash::const_iterator ArrayHashConstIter
Definition: ArrayExprHash.h:65
bool operator()(const UpdateNode *un1, const UpdateNode *un2) const
Definition: ArrayExprHash.h:41
bool operator()(const Array *array1, const Array *array2) const
Definition: ArrayExprHash.h:29