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
|
//===-- 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 (root) {
assert(root->getDomain() == index->getWidth());
assert(root->getRange() == value->getWidth());
}
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;
}
|
