Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 126 insertions, 0 deletions

diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
new file mode 100644
index 00000000..b2ceeaf1
--- /dev/null
+++ b/lib/Expr/Updates.cpp
@@ -0,0 +1,126 @@
+//===-- 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),
+    stpArray(0),
+    next(_next),
+    index(_index),
+    value(_value) {
+  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() {
+  // XXX gross
+  if (stpArray)
+    ::vc_DeleteExpr(stpArray);
+}
+
+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, bool _isRooted,
+                       const UpdateNode *_head)
+  : root(_root),
+    head(_head),
+    isRooted(_isRooted) {
+  if (head) ++head->refCount;
+}
+
+UpdateList::UpdateList(const UpdateList &b)
+  : root(b.root),
+    head(b.head),
+    isRooted(b.isRooted) {
+  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;
+  isRooted = b.isRooted;
+  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 {
+  // use object id to increase determinism
+  if (root->id != b.root->id) 
+    return root->id < b.root->id ? -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 = root->id * Expr::MAGIC_HASH_CONSTANT;
+  if (head)
+    res ^= head->hash();
+  return res;
+}