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, 812 insertions, 0 deletions

diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
new file mode 100644
index 00000000..cd563551
--- /dev/null
+++ b/lib/Core/Memory.cpp
@@ -0,0 +1,812 @@
+//===-- Memory.cpp --------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "Common.h"
+
+#include "Memory.h"
+
+#include "klee/Expr.h"
+#include "klee/Machine.h"
+#include "klee/Solver.h"
+#include "klee/util/BitArray.h"
+
+#include "ObjectHolder.h"
+
+#include <llvm/Function.h>
+#include <llvm/Instruction.h>
+#include <llvm/Value.h>
+
+#include <iostream>
+#include <cassert>
+#include <sstream>
+
+using namespace llvm;
+using namespace klee;
+
+/***/
+
+ObjectHolder::ObjectHolder(const ObjectHolder &b) : os(b.os) { 
+  if (os) ++os->refCount; 
+}
+
+ObjectHolder::ObjectHolder(ObjectState *_os) : os(_os) { 
+  if (os) ++os->refCount; 
+}
+
+ObjectHolder::~ObjectHolder() { 
+  if (os && --os->refCount==0) delete os; 
+}
+  
+ObjectHolder &ObjectHolder::operator=(const ObjectHolder &b) {
+  if (b.os) ++b.os->refCount;
+  if (os && --os->refCount==0) delete os;
+  os = b.os;
+  return *this;
+}
+
+/***/
+
+int MemoryObject::counter = 0;
+
+extern "C" void vc_DeleteExpr(void*);
+
+MemoryObject::~MemoryObject() {
+  // FIXME: This shouldn't be necessary. Array's should be ref-counted
+  // just like everything else, and the interaction with the STP array
+  // should hide at least inside the Expr/Solver layers.
+  if (array) {
+    if (array->stpInitialArray) {
+      ::vc_DeleteExpr(array->stpInitialArray);
+      array->stpInitialArray = 0;
+    }
+    delete array;
+  }
+}
+
+void MemoryObject::getAllocInfo(std::string &result) const {
+  std::ostringstream info;
+
+  info << "MO" << id << "[" << size << "]";
+
+  if (allocSite) {
+    info << " allocated at ";
+    if (const Instruction *i = dyn_cast<Instruction>(allocSite)) {
+      info << i->getParent()->getParent()->getName() << "():";
+      info << *i;
+    } else if (const GlobalValue *gv = dyn_cast<GlobalValue>(allocSite)) {
+      info << "global:" << gv->getName();
+    } else {
+      info << "value:" << *allocSite;
+    }
+  } else {
+    info << " (no allocation info)";
+  }
+  
+  result = info.str();
+}
+
+/***/
+
+ObjectState::ObjectState(const MemoryObject *mo, unsigned _size)
+  : copyOnWriteOwner(0),
+    refCount(0),
+    object(mo),
+    concreteStore(new uint8_t[_size]),
+    concreteMask(0),
+    flushMask(0),
+    knownSymbolics(0),
+    size(_size),
+    updates(mo->array, false, 0),
+    readOnly(false) {
+}
+
+ObjectState::ObjectState(const ObjectState &os) 
+  : copyOnWriteOwner(0),
+    refCount(0),
+    object(os.object),
+    concreteStore(new uint8_t[os.size]),
+    concreteMask(os.concreteMask ? new BitArray(*os.concreteMask, os.size) : 0),
+    flushMask(os.flushMask ? new BitArray(*os.flushMask, os.size) : 0),
+    knownSymbolics(0),
+    size(os.size),
+    updates(os.updates),
+    readOnly(false) {
+  assert(!os.readOnly && "no need to copy read only object?");
+
+  if (os.knownSymbolics) {
+    knownSymbolics = new ref<Expr>[size];
+    for (unsigned i=0; i<size; i++)
+      knownSymbolics[i] = os.knownSymbolics[i];
+  }
+
+  memcpy(concreteStore, os.concreteStore, size*sizeof(*concreteStore));
+}
+
+ObjectState::~ObjectState() {
+  if (concreteMask) delete concreteMask;
+  if (flushMask) delete flushMask;
+  if (knownSymbolics) delete[] knownSymbolics;
+  delete[] concreteStore;
+}
+
+/***/
+
+void ObjectState::makeConcrete() {
+  if (concreteMask) delete concreteMask;
+  if (flushMask) delete flushMask;
+  if (knownSymbolics) delete[] knownSymbolics;
+  concreteMask = 0;
+  flushMask = 0;
+  knownSymbolics = 0;
+}
+
+void ObjectState::makeSymbolic() {
+  assert(!updates.head &&
+         "XXX makeSymbolic of objects with symbolic values is unsupported");
+  updates.isRooted = true;
+
+  // XXX simplify this, can just delete various arrays I guess
+  for (unsigned i=0; i<size; i++) {
+    markByteSymbolic(i);
+    setKnownSymbolic(i, 0);
+    markByteFlushed(i);
+  }
+}
+
+void ObjectState::initializeToZero() {
+  makeConcrete();
+  memset(concreteStore, 0, size);
+}
+
+void ObjectState::initializeToRandom() {  
+  makeConcrete();
+  for (unsigned i=0; i<size; i++) {
+    // randomly selected by 256 sided die
+    concreteStore[i] = 0xAB;
+  }
+}
+
+/*
+Cache Invariants
+--
+isByteKnownSymbolic(i) => !isByteConcrete(i)
+isByteConcrete(i) => !isByteKnownSymbolic(i)
+!isByteFlushed(i) => (isByteConcrete(i) || isByteKnownSymbolic(i))
+ */
+
+void ObjectState::fastRangeCheckOffset(ref<Expr> offset,
+                                       unsigned *base_r,
+                                       unsigned *size_r) const {
+  *base_r = 0;
+  *size_r = size;
+}
+
+void ObjectState::flushRangeForRead(unsigned rangeBase, 
+                                    unsigned rangeSize) const {
+  if (!flushMask) flushMask = new BitArray(size, true);
+ 
+  for (unsigned offset=rangeBase; offset<rangeBase+rangeSize; offset++) {
+    if (!isByteFlushed(offset)) {
+      if (isByteConcrete(offset)) {
+        updates.extend(ConstantExpr::create(offset, kMachinePointerType),
+                       ConstantExpr::create(concreteStore[offset], Expr::Int8));
+      } else {
+        assert(isByteKnownSymbolic(offset) && "invalid bit set in flushMask");
+        updates.extend(ConstantExpr::create(offset, kMachinePointerType),
+                       knownSymbolics[offset]);
+      }
+
+      flushMask->unset(offset);
+    }
+  } 
+}
+
+void ObjectState::flushRangeForWrite(unsigned rangeBase, 
+                                     unsigned rangeSize) {
+  if (!flushMask) flushMask = new BitArray(size, true);
+
+  for (unsigned offset=rangeBase; offset<rangeBase+rangeSize; offset++) {
+    if (!isByteFlushed(offset)) {
+      if (isByteConcrete(offset)) {
+        updates.extend(ConstantExpr::create(offset, kMachinePointerType),
+                       ConstantExpr::create(concreteStore[offset], Expr::Int8));
+        markByteSymbolic(offset);
+      } else {
+        assert(isByteKnownSymbolic(offset) && "invalid bit set in flushMask");
+        updates.extend(ConstantExpr::create(offset, kMachinePointerType),
+                       knownSymbolics[offset]);
+        setKnownSymbolic(offset, 0);
+      }
+
+      flushMask->unset(offset);
+    } else {
+      // flushed bytes that are written over still need
+      // to be marked out
+      if (isByteConcrete(offset)) {
+        markByteSymbolic(offset);
+      } else if (isByteKnownSymbolic(offset)) {
+        setKnownSymbolic(offset, 0);
+      }
+    }
+  } 
+}
+
+bool ObjectState::isByteConcrete(unsigned offset) const {
+  return !concreteMask || concreteMask->get(offset);
+}
+
+bool ObjectState::isByteFlushed(unsigned offset) const {
+  return flushMask && !flushMask->get(offset);
+}
+
+bool ObjectState::isByteKnownSymbolic(unsigned offset) const {
+  return knownSymbolics && knownSymbolics[offset].get();
+}
+
+void ObjectState::markByteConcrete(unsigned offset) {
+  if (concreteMask)
+    concreteMask->set(offset);
+}
+
+void ObjectState::markByteSymbolic(unsigned offset) {
+  if (!concreteMask)
+    concreteMask = new BitArray(size, true);
+  concreteMask->unset(offset);
+}
+
+void ObjectState::markByteUnflushed(unsigned offset) {
+  if (flushMask)
+    flushMask->set(offset);
+}
+
+void ObjectState::markByteFlushed(unsigned offset) {
+  if (!flushMask) {
+    flushMask = new BitArray(size, false);
+  } else {
+    flushMask->unset(offset);
+  }
+}
+
+void ObjectState::setKnownSymbolic(unsigned offset, 
+                                   Expr *value /* can be null */) {
+  if (knownSymbolics) {
+    knownSymbolics[offset] = value;
+  } else {
+    if (value) {
+      knownSymbolics = new ref<Expr>[size];
+      knownSymbolics[offset] = value;
+    }
+  }
+}
+
+/***/
+
+ref<Expr> ObjectState::read8(unsigned offset) const {
+  if (isByteConcrete(offset)) {
+    return ConstantExpr::create(concreteStore[offset], Expr::Int8);
+  } else if (isByteKnownSymbolic(offset)) {
+    return knownSymbolics[offset];
+  } else {
+    assert(isByteFlushed(offset) && "unflushed byte without cache value");
+    
+    return ReadExpr::create(updates, 
+                            ConstantExpr::create(offset, kMachinePointerType));
+  }    
+}
+
+ref<Expr> ObjectState::read8(ref<Expr> offset) const {
+  assert(!offset.isConstant() && "constant offset passed to symbolic read8");
+  unsigned base, size;
+  fastRangeCheckOffset(offset, &base, &size);
+  flushRangeForRead(base, size);
+
+  if (size>4096) {
+    std::string allocInfo;
+    object->getAllocInfo(allocInfo);
+    klee_warning_once(0, "flushing %d bytes on read, may be slow and/or crash: %s", 
+                      size,
+                      allocInfo.c_str());
+  }
+  
+  return ReadExpr::create(updates, offset);
+}
+
+void ObjectState::write8(unsigned offset, uint8_t value) {
+  //assert(read_only == false && "writing to read-only object!");
+  concreteStore[offset] = value;
+  setKnownSymbolic(offset, 0);
+
+  markByteConcrete(offset);
+  markByteUnflushed(offset);
+}
+
+void ObjectState::write8(unsigned offset, ref<Expr> value) {
+  // can happen when ExtractExpr special cases
+  if (value.isConstant()) {
+    write8(offset, (uint8_t) value.getConstantValue());
+  } else {
+    setKnownSymbolic(offset, value.get());
+      
+    markByteSymbolic(offset);
+    markByteUnflushed(offset);
+  }
+}
+
+void ObjectState::write8(ref<Expr> offset, ref<Expr> value) {
+  assert(!offset.isConstant() && "constant offset passed to symbolic write8");
+  unsigned base, size;
+  fastRangeCheckOffset(offset, &base, &size);
+  flushRangeForWrite(base, size);
+
+  if (size>4096) {
+    std::string allocInfo;
+    object->getAllocInfo(allocInfo);
+    klee_warning_once(0, "flushing %d bytes on read, may be slow and/or crash: %s", 
+                      size,
+                      allocInfo.c_str());
+  }
+  
+  updates.extend(offset, value);
+}
+
+/***/
+
+ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
+  if (offset.isConstant()) {
+    return read((unsigned) offset.getConstantValue(), width);
+  } else { 
+    switch (width) {
+    case  Expr::Bool: return  read1(offset);
+    case  Expr::Int8: return  read8(offset);
+    case Expr::Int16: return read16(offset);
+    case Expr::Int32: return read32(offset);
+    case Expr::Int64: return read64(offset);
+    default: assert(0 && "invalid type");
+    }
+  }
+}
+
+ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const {
+  switch (width) {
+  case  Expr::Bool: return  read1(offset);
+  case  Expr::Int8: return  read8(offset);
+  case Expr::Int16: return read16(offset);
+  case Expr::Int32: return read32(offset);
+  case Expr::Int64: return read64(offset);
+  default: assert(0 && "invalid type");
+  }
+}
+
+ref<Expr> ObjectState::read1(unsigned offset) const {
+  return ExtractExpr::createByteOff(read8(offset), 0, Expr::Bool);
+}
+
+ref<Expr> ObjectState::read1(ref<Expr> offset) const {
+  return ExtractExpr::createByteOff(read8(offset), 0, Expr::Bool);
+}
+
+ref<Expr> ObjectState::read16(unsigned offset) const {
+  if (kMachineByteOrder == machine::MSB) {
+    return ConcatExpr::create(read8(offset+0),
+			      read8(offset+1));
+  } else {
+    return ConcatExpr::create(read8(offset+1),
+			      read8(offset+0));
+  }
+}
+
+ref<Expr> ObjectState::read16(ref<Expr> offset) const {
+  if (kMachineByteOrder == machine::MSB) {
+    return ConcatExpr::create
+      (read8(AddExpr::create(offset,
+                             ConstantExpr::create(0,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(1,
+                                                  kMachinePointerType))));
+  } else {
+    return ConcatExpr::create
+      (read8(AddExpr::create(offset,
+                             ConstantExpr::create(1,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(0,
+                                                  kMachinePointerType))));
+  }
+}
+
+ref<Expr> ObjectState::read32(unsigned offset) const {
+  if (kMachineByteOrder == machine::MSB) {
+    return ConcatExpr::create4(read8(offset+0),
+                               read8(offset+1),
+                               read8(offset+2),
+                               read8(offset+3));
+  } else {
+    return ConcatExpr::create4(read8(offset+3),
+                               read8(offset+2),
+                               read8(offset+1),
+                               read8(offset+0));
+  }
+}
+
+ref<Expr> ObjectState::read32(ref<Expr> offset) const {
+  if (kMachineByteOrder == machine::MSB) {
+    return ConcatExpr::create4
+      (read8(AddExpr::create(offset,
+                             ConstantExpr::create(0,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(1,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(2,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(3,
+                                                  kMachinePointerType))));
+  } else {
+    return ConcatExpr::create4
+      (read8(AddExpr::create(offset,
+                             ConstantExpr::create(3,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(2,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(1,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(0,
+                                                  kMachinePointerType))));
+  }
+}
+
+ref<Expr> ObjectState::read64(unsigned offset) const {
+  if (kMachineByteOrder == machine::MSB) {
+    return ConcatExpr::create8(read8(offset+0),
+                               read8(offset+1),
+                               read8(offset+2),
+                               read8(offset+3),
+                               read8(offset+4),
+                               read8(offset+5),
+                               read8(offset+6),
+                               read8(offset+7));
+  } else {
+    return ConcatExpr::create8(read8(offset+7),
+                               read8(offset+6),
+                               read8(offset+5),
+                               read8(offset+4),
+                               read8(offset+3),
+                               read8(offset+2),
+                               read8(offset+1),
+                               read8(offset+0));
+  }
+}
+
+ref<Expr> ObjectState::read64(ref<Expr> offset) const {
+  if (kMachineByteOrder == machine::MSB) {
+    return ConcatExpr::create8
+      (read8(AddExpr::create(offset,
+                             ConstantExpr::create(0,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(1,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(2,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(3,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(4,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(5,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(6,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(7,
+                                                  kMachinePointerType))));
+  } else {
+    return ConcatExpr::create8
+      (read8(AddExpr::create(offset,
+                             ConstantExpr::create(7,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(6,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(5,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(4,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(3,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(2,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(1,
+                                                  kMachinePointerType))),
+       read8(AddExpr::create(offset,
+                             ConstantExpr::create(0,
+                                                  kMachinePointerType))));
+  }
+}
+
+void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
+  Expr::Width w = value.getWidth();
+  if (offset.isConstant()) {
+    write(offset.getConstantValue(), value);
+  } else {
+    switch(w) {
+    case  Expr::Bool:  write1(offset, value); break;
+    case  Expr::Int8:  write8(offset, value); break;
+    case Expr::Int16: write16(offset, value); break;
+    case Expr::Int32: write32(offset, value); break;
+    case Expr::Int64: write64(offset, value); break;
+    default: assert(0 && "invalid number of bytes in write");
+    }
+  }
+}
+
+void ObjectState::write(unsigned offset, ref<Expr> value) {
+  Expr::Width w = value.getWidth();
+  if (value.isConstant()) {
+    uint64_t val = value.getConstantValue();
+    switch(w) {
+    case  Expr::Bool:
+    case  Expr::Int8:  write8(offset, val); break;
+    case Expr::Int16: write16(offset, val); break;
+    case Expr::Int32: write32(offset, val); break;
+    case Expr::Int64: write64(offset, val); break;
+    default: assert(0 && "invalid number of bytes in write");
+    }
+  } else {
+    switch(w) {
+    case  Expr::Bool:  write1(offset, value); break;
+    case  Expr::Int8:  write8(offset, value); break;
+    case Expr::Int16: write16(offset, value); break;
+    case Expr::Int32: write32(offset, value); break;
+    case Expr::Int64: write64(offset, value); break;
+    default: assert(0 && "invalid number of bytes in write");
+    }
+  }
+}
+
+void ObjectState::write1(unsigned offset, ref<Expr> value) {
+  write8(offset, ZExtExpr::create(value, Expr::Int8));
+}
+
+void ObjectState::write1(ref<Expr> offset, ref<Expr> value) {
+  write8(offset, ZExtExpr::create(value, Expr::Int8));
+}
+
+void ObjectState::write16(unsigned offset, uint16_t value) {
+  if (kMachineByteOrder == machine::MSB) {
+    write8(offset+0, (uint8_t) (value >>  8));
+    write8(offset+1, (uint8_t) (value >>  0));
+  } else {
+    write8(offset+1, (uint8_t) (value >>  8));
+    write8(offset+0, (uint8_t) (value >>  0));
+  }
+}
+
+void ObjectState::write16(unsigned offset, ref<Expr> value) {
+  if (kMachineByteOrder == machine::MSB) {
+    write8(offset+0, ExtractExpr::createByteOff(value, 1));
+    write8(offset+1, ExtractExpr::createByteOff(value, 0));
+  } else {
+    write8(offset+1, ExtractExpr::createByteOff(value, 1));
+    write8(offset+0, ExtractExpr::createByteOff(value, 0));
+  }
+}
+
+
+void ObjectState::write16(ref<Expr> offset, ref<Expr> value) {
+  if (kMachineByteOrder == machine::MSB) {
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(0, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,1));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(0, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,0));
+  } else {
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(1, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,1));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(0, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,0));
+  }
+}
+
+void ObjectState::write32(unsigned offset, uint32_t value) {
+  if (kMachineByteOrder == machine::MSB) {
+    write8(offset+0, (uint8_t) (value >>  24));
+    write8(offset+1, (uint8_t) (value >>  16));
+    write8(offset+2, (uint8_t) (value >>  8));
+    write8(offset+3, (uint8_t) (value >>  0));
+  } else {
+    write8(offset+3, (uint8_t) (value >>  24));
+    write8(offset+2, (uint8_t) (value >>  16));
+    write8(offset+1, (uint8_t) (value >>  8));
+    write8(offset+0, (uint8_t) (value >>  0));
+  }
+}
+
+void ObjectState::write32(unsigned offset, ref<Expr> value) {
+  if (kMachineByteOrder == machine::MSB) {
+    write8(offset+0, ExtractExpr::createByteOff(value, 3));
+    write8(offset+1, ExtractExpr::createByteOff(value, 2));
+    write8(offset+2, ExtractExpr::createByteOff(value, 1));
+    write8(offset+3, ExtractExpr::createByteOff(value, 0));
+  } else {
+    write8(offset+3, ExtractExpr::createByteOff(value, 3));
+    write8(offset+2, ExtractExpr::createByteOff(value, 2));
+    write8(offset+1, ExtractExpr::createByteOff(value, 1));
+    write8(offset+0, ExtractExpr::createByteOff(value, 0));
+  }
+}
+
+void ObjectState::write32(ref<Expr> offset, ref<Expr> value) {
+  if (kMachineByteOrder == machine::MSB) {
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(0, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,3));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(1, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,2));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(2, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,1));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(3, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,0));
+  } else {
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(3, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,3));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(2, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,2));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(1, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,1));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(0, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,0));
+  }
+}
+
+void ObjectState::write64(unsigned offset, uint64_t value) {
+  if (kMachineByteOrder == machine::MSB) {
+    write8(offset+0, (uint8_t) (value >>  56));
+    write8(offset+1, (uint8_t) (value >>  48));
+    write8(offset+2, (uint8_t) (value >>  40));
+    write8(offset+3, (uint8_t) (value >>  32));
+    write8(offset+4, (uint8_t) (value >>  24));
+    write8(offset+5, (uint8_t) (value >>  16));
+    write8(offset+6, (uint8_t) (value >>  8));
+    write8(offset+7, (uint8_t) (value >>  0));
+  } else {
+    write8(offset+7, (uint8_t) (value >>  56));
+    write8(offset+6, (uint8_t) (value >>  48));
+    write8(offset+5, (uint8_t) (value >>  40));
+    write8(offset+4, (uint8_t) (value >>  32));
+    write8(offset+3, (uint8_t) (value >>  24));
+    write8(offset+2, (uint8_t) (value >>  16));
+    write8(offset+1, (uint8_t) (value >>  8));
+    write8(offset+0, (uint8_t) (value >>  0));
+  }
+}
+
+void ObjectState::write64(unsigned offset, ref<Expr> value) {
+  if (kMachineByteOrder == machine::MSB) {
+    write8(offset+0, ExtractExpr::createByteOff(value, 7));
+    write8(offset+1, ExtractExpr::createByteOff(value, 6));
+    write8(offset+2, ExtractExpr::createByteOff(value, 5));
+    write8(offset+3, ExtractExpr::createByteOff(value, 4));
+    write8(offset+4, ExtractExpr::createByteOff(value, 3));
+    write8(offset+5, ExtractExpr::createByteOff(value, 2));
+    write8(offset+6, ExtractExpr::createByteOff(value, 1));
+    write8(offset+7, ExtractExpr::createByteOff(value, 0));
+  } else {
+    write8(offset+7, ExtractExpr::createByteOff(value, 7));
+    write8(offset+6, ExtractExpr::createByteOff(value, 6));
+    write8(offset+5, ExtractExpr::createByteOff(value, 5));
+    write8(offset+4, ExtractExpr::createByteOff(value, 4));
+    write8(offset+3, ExtractExpr::createByteOff(value, 3));
+    write8(offset+2, ExtractExpr::createByteOff(value, 2));
+    write8(offset+1, ExtractExpr::createByteOff(value, 1));
+    write8(offset+0, ExtractExpr::createByteOff(value, 0));
+  }
+}
+
+void ObjectState::write64(ref<Expr> offset, ref<Expr> value) {
+  if (kMachineByteOrder == machine::MSB) {
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(0, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,7));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(1, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,6));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(2, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,5));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(3, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,4));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(4, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,3));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(5, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,2));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(6, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,1));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(7, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,0));
+  } else {
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(7, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,7));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(6, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,6));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(5, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,5));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(4, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,4));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(3, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,3));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(2, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,2));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(1, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,1));
+    write8(AddExpr::create(offset,
+                           ConstantExpr::create(0, kMachinePointerType)), 
+           ExtractExpr::createByteOff(value,0));
+  }
+}
+
+void ObjectState::print() {
+  llvm::cerr << "-- ObjectState --\n";
+  llvm::cerr << "\tMemoryObject ID: " << object->id << "\n";
+  llvm::cerr << "\tRoot Object: " << updates.root << "\n";
+  llvm::cerr << "\tIs Rooted? " << updates.isRooted << "\n";
+  llvm::cerr << "\tSize: " << size << "\n";
+
+  llvm::cerr << "\tBytes:\n";
+  for (unsigned i=0; i<size; i++) {
+    llvm::cerr << "\t\t["<<i<<"]"
+               << " concrete? " << isByteConcrete(i)
+               << " known-sym? " << isByteKnownSymbolic(i)
+               << " flushed? " << isByteFlushed(i) << " = ";
+    ref<Expr> e = read8(i);
+    llvm::cerr << e << "\n";
+  }
+
+  llvm::cerr << "\tUpdates:\n";
+  for (const UpdateNode *un=updates.head; un; un=un->next) {
+    llvm::cerr << "\t\t[" << un->index << "] = " << un->value << "\n";
+  }
+}