1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
//===-- 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/TimerStatIncrementer.h"
#include "klee/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 */
|
