klee
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/Expr.h"
11
12#include <cassert>
13
14using namespace klee;
15
17
18UpdateNode::UpdateNode(const ref<UpdateNode> &_next, const ref<Expr> &_index,
19 const ref<Expr> &_value)
20 : next(_next), index(_index), value(_value) {
21 // FIXME: What we need to check here instead is that _value is of the same width
22 // as the range of the array that the update node is part of.
23 /*
24 assert(_value->getWidth() == Expr::Int8 &&
25 "Update value should be 8-bit wide.");
26 */
28 size = next ? next->size + 1 : 1;
29}
30
31extern "C" void vc_DeleteExpr(void*);
32
33int UpdateNode::compare(const UpdateNode &b) const {
34 if (int i = index.compare(b.index))
35 return i;
36 return value.compare(b.value);
37}
38
40 hashValue = index->hash() ^ value->hash();
41 if (next)
42 hashValue ^= next->hash();
43 return hashValue;
44}
45
47
48UpdateList::UpdateList(const Array *_root, const ref<UpdateNode> &_head)
49 : root(_root), head(_head) {}
50
51void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
52
53 if (root) {
54 assert(root->getDomain() == index->getWidth());
55 assert(root->getRange() == value->getWidth());
56 }
57
58 head = new UpdateNode(head, index, value);
59}
60
61int UpdateList::compare(const UpdateList &b) const {
62 if (root->name != b.root->name)
63 return root->name < b.root->name ? -1 : 1;
64
65 // Check the root itself in case we have separate objects with the
66 // same name.
67 if (root != b.root)
68 return root < b.root ? -1 : 1;
69
70 if (getSize() < b.getSize()) return -1;
71 else if (getSize() > b.getSize()) return 1;
72
73 // XXX build comparison into update, make fast
74 const auto *an = head.get(), *bn = b.head.get();
75 for (; an && bn; an = an->next.get(), bn = bn->next.get()) {
76 if (an==bn) { // exploit shared list structure
77 return 0;
78 } else {
79 if (int res = an->compare(*bn))
80 return res;
81 }
82 }
83 assert(!an && !bn);
84 return 0;
85}
86
87unsigned UpdateList::hash() const {
88 unsigned res = 0;
89 for (unsigned i = 0, e = root->name.size(); i != e; ++i)
90 res = (res * Expr::MAGIC_HASH_CONSTANT) + root->name[i];
91 if (head)
92 res ^= head->hash();
93 return res;
94}
void vc_DeleteExpr(void *)
Expr::Width getRange() const
Definition: Expr.h:530
const std::string name
Definition: Expr.h:486
Expr::Width getDomain() const
Definition: Expr.h:529
static const unsigned MAGIC_HASH_CONSTANT
Definition: Expr.h:94
virtual unsigned hash() const
Returns the pre-computed hash of the current expression.
Definition: Expr.h:222
virtual Width getWidth() const =0
Class representing a complete list of updates into an array.
Definition: Expr.h:539
void extend(const ref< Expr > &index, const ref< Expr > &value)
Definition: Updates.cpp:51
UpdateList(const Array *_root, const ref< UpdateNode > &_head)
Definition: Updates.cpp:48
ref< UpdateNode > head
pointer to the most recent update node
Definition: Expr.h:546
unsigned getSize() const
size of this update list
Definition: Expr.h:556
int compare(const UpdateList &b) const
Definition: Updates.cpp:61
unsigned hash() const
Definition: Updates.cpp:87
const Array * root
Definition: Expr.h:543
Class representing a byte update of an array.
Definition: Expr.h:451
unsigned hashValue
Definition: Expr.h:455
ref< Expr > index
Definition: Expr.h:459
unsigned size
size of this update sequence, including this update
Definition: Expr.h:466
unsigned computeHash()
Definition: Updates.cpp:39
int compare(const UpdateNode &b) const
Definition: Updates.cpp:33
const ref< UpdateNode > next
Definition: Expr.h:458
ref< Expr > value
Definition: Expr.h:459
Definition: Ref.h:82
int compare(const ref &rhs) const
Definition: Ref.h:217
Definition: main.cpp:291