klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Updates.cpp
Go to the documentation of this file.
1 //===-- Updates.cpp -------------------------------------------------------===//
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 #include "klee/Expr.h"
11 
12 #include <cassert>
13 
14 using namespace klee;
15 
17 
19  const ref<Expr> &_index,
20  const ref<Expr> &_value)
21  : refCount(0),
22  next(_next),
23  index(_index),
24  value(_value) {
25  // FIXME: What we need to check here instead is that _value is of the same width
26  // as the range of the array that the update node is part of.
27  /*
28  assert(_value->getWidth() == Expr::Int8 &&
29  "Update value should be 8-bit wide.");
30  */
31  computeHash();
32  if (next) {
33  ++next->refCount;
34  size = 1 + next->size;
35  }
36  else size = 1;
37 }
38 
39 extern "C" void vc_DeleteExpr(void*);
40 
42 }
43 
44 int UpdateNode::compare(const UpdateNode &b) const {
45  if (int i = index.compare(b.index))
46  return i;
47  return value.compare(b.value);
48 }
49 
51  hashValue = index->hash() ^ value->hash();
52  if (next)
53  hashValue ^= next->hash();
54  return hashValue;
55 }
56 
58 
59 UpdateList::UpdateList(const Array *_root, const UpdateNode *_head)
60  : root(_root),
61  head(_head) {
62  if (head) ++head->refCount;
63 }
64 
66  : root(b.root),
67  head(b.head) {
68  if (head) ++head->refCount;
69 }
70 
72  // We need to be careful and avoid recursion here. We do this in
73  // cooperation with the private dtor of UpdateNode which does not
74  // recursively free its tail.
75  while (head && --head->refCount==0) {
76  const UpdateNode *n = head->next;
77  delete head;
78  head = n;
79  }
80 }
81 
83  if (b.head) ++b.head->refCount;
84  if (head && --head->refCount==0) delete head;
85  root = b.root;
86  head = b.head;
87  return *this;
88 }
89 
90 void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
91 
92  if (root) {
93  assert(root->getDomain() == index->getWidth());
94  assert(root->getRange() == value->getWidth());
95  }
96 
97  if (head) --head->refCount;
98  head = new UpdateNode(head, index, value);
99  ++head->refCount;
100 }
101 
102 int UpdateList::compare(const UpdateList &b) const {
103  if (root->name != b.root->name)
104  return root->name < b.root->name ? -1 : 1;
105 
106  // Check the root itself in case we have separate objects with the
107  // same name.
108  if (root != b.root)
109  return root < b.root ? -1 : 1;
110 
111  if (getSize() < b.getSize()) return -1;
112  else if (getSize() > b.getSize()) return 1;
113 
114  // XXX build comparison into update, make fast
115  const UpdateNode *an=head, *bn=b.head;
116  for (; an && bn; an=an->next,bn=bn->next) {
117  if (an==bn) { // exploit shared list structure
118  return 0;
119  } else {
120  if (int res = an->compare(*bn))
121  return res;
122  }
123  }
124  assert(!an && !bn);
125  return 0;
126 }
127 
128 unsigned UpdateList::hash() const {
129  unsigned res = 0;
130  for (unsigned i = 0, e = root->name.size(); i != e; ++i)
131  res = (res * Expr::MAGIC_HASH_CONSTANT) + root->name[i];
132  if (head)
133  res ^= head->hash();
134  return res;
135 }
int compare(const ref &rhs) const
Definition: Ref.h:102
void extend(const ref< Expr > &index, const ref< Expr > &value)
Definition: Updates.cpp:90
unsigned hash() const
Definition: Updates.cpp:128
static const unsigned MAGIC_HASH_CONSTANT
Definition: Expr.h:91
ref< Expr > index
Definition: Expr.h:578
UpdateList(const Array *_root, const UpdateNode *_head)
Definition: Updates.cpp:59
virtual unsigned hash() const
Returns the pre-computed hash of the current expression.
Definition: Expr.h:192
Class representing a complete list of updates into an array.
Definition: Expr.h:655
ref< Expr > value
Definition: Expr.h:578
unsigned hash() const
Definition: Expr.h:592
virtual Width getWidth() const =0
unsigned hashValue
Definition: Expr.h:574
UpdateList & operator=(const UpdateList &b)
Definition: Updates.cpp:82
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
const std::string name
Definition: Expr.h:603
Expr::Width getRange() const
Definition: Expr.h:645
const UpdateNode * next
Definition: Expr.h:577
Expr::Width getDomain() const
Definition: Expr.h:644
unsigned getSize() const
size of this update list
Definition: Expr.h:672
unsigned size
size of this update sequence, including this update
Definition: Expr.h:582
const Array * root
Definition: Expr.h:659
void vc_DeleteExpr(void *)
Class representing a byte update of an array.
Definition: Expr.h:569
unsigned computeHash()
Definition: Updates.cpp:50
int compare(const UpdateList &b) const
Definition: Updates.cpp:102
unsigned refCount
Definition: Expr.h:572
int compare(const UpdateNode &b) const
Definition: Updates.cpp:44