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
|
//===-- Updates.cpp -------------------------------------------------------===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#include "klee/Expr.h"
#include <cassert>
using namespace klee;
///
UpdateNode::UpdateNode(const UpdateNode *_next,
const ref<Expr> &_index,
const ref<Expr> &_value)
: refCount(0),
next(_next),
index(_index),
value(_value) {
// FIXME: What we need to check here instead is that _value is of the same width
// as the range of the array that the update node is part of.
/*
assert(_value->getWidth() == Expr::Int8 &&
"Update value should be 8-bit wide.");
*/
computeHash();
if (next) {
++next->refCount;
size = 1 + next->size;
}
else size = 1;
}
extern "C" void vc_DeleteExpr(void*);
UpdateNode::~UpdateNode() {
}
int UpdateNode::compare(const UpdateNode &b) const {
if (int i = index.compare(b.index))
return i;
return value.compare(b.value);
}
unsigned UpdateNode::computeHash() {
hashValue = index->hash() ^ value->hash();
if (next)
hashValue ^= next->hash();
return hashValue;
}
///
UpdateList::UpdateList(const Array *_root, const UpdateNode *_head)
: root(_root),
head(_head) {
if (head) ++head->refCount;
}
UpdateList::UpdateList(const UpdateList &b)
: root(b.root),
head(b.head) {
if (head) ++head->refCount;
}
UpdateList::~UpdateList() {
// We need to be careful and avoid recursion here. We do this in
// cooperation with the private dtor of UpdateNode which does not
// recursively free its tail.
while (head && --head->refCount==0) {
const UpdateNode *n = head->next;
delete head;
head = n;
}
}
UpdateList &UpdateList::operator=(const UpdateList &b) {
if (b.head) ++b.head->refCount;
if (head && --head->refCount==0) delete head;
root = b.root;
head = b.head;
return *this;
}
void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
if (head) --head->refCount;
head = new UpdateNode(head, index, value);
++head->refCount;
}
int UpdateList::compare(const UpdateList &b) const {
if (root->name != b.root->name)
return root->name < b.root->name ? -1 : 1;
// Check the root itself in case we have separate objects with the
// same name.
if (root != b.root)
return root < b.root ? -1 : 1;
if (getSize() < b.getSize()) return -1;
else if (getSize() > b.getSize()) return 1;
// XXX build comparison into update, make fast
const UpdateNode *an=head, *bn=b.head;
for (; an && bn; an=an->next,bn=bn->next) {
if (an==bn) { // exploit shared list structure
return 0;
} else {
if (int res = an->compare(*bn))
return res;
}
}
assert(!an && !bn);
return 0;
}
unsigned UpdateList::hash() const {
unsigned res = 0;
for (unsigned i = 0, e = root->name.size(); i != e; ++i)
res = (res * Expr::MAGIC_HASH_CONSTANT) + root->name[i];
if (head)
res ^= head->hash();
return res;
}
|
