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

diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
new file mode 100644
index 00000000..0f09b162
--- /dev/null
+++ b/lib/Core/Memory.h
@@ -0,0 +1,239 @@
+//===-- Memory.h ------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_MEMORY_H
+#define KLEE_MEMORY_H
+
+#include "klee/Expr.h"
+
+#include <vector>
+#include <string>
+
+namespace llvm {
+  class Value;
+}
+
+namespace klee {
+
+class BitArray;
+class MemoryManager;
+class Solver;
+
+class MemoryObject {
+  friend class STPBuilder;
+
+private:
+  static int counter;
+
+public:
+  unsigned id;
+  uint64_t address;
+  Array *array;
+
+  /// size in bytes
+  unsigned size;
+  std::string name;
+
+  bool isLocal;
+  bool isGlobal;
+  bool isFixed;
+
+  /// true if created by us.
+  bool fake_object;
+  bool isUserSpecified;
+
+  /// "Location" for which this memory object was allocated. This
+  /// should be either the allocating instruction or the global object
+  /// it was allocated for (or whatever else makes sense).
+  const llvm::Value *allocSite;
+  
+  /// A list of boolean expressions the user has requested be true of
+  /// a counterexample. Mutable since we play a little fast and loose
+  /// with allowing it to be added to during execution (although
+  /// should sensibly be only at creation time).
+  mutable std::vector< ref<Expr> > cexPreferences;
+
+  // DO NOT IMPLEMENT
+  MemoryObject(const MemoryObject &b);
+  MemoryObject &operator=(const MemoryObject &b);
+
+public:
+  // XXX this is just a temp hack, should be removed
+  explicit
+  MemoryObject(uint64_t _address) 
+    : id(counter++),
+      address(_address),
+      array(new Array(this, 0, id)),
+      size(0),
+      isFixed(true),
+      allocSite(0) {
+  }
+
+  MemoryObject(uint64_t _address, unsigned _size, 
+               bool _isLocal, bool _isGlobal, bool _isFixed,
+               const llvm::Value *_allocSite) 
+    : id(counter++),
+      address(_address),
+      array(new Array(this, id, _size)),
+      size(_size),
+      name("unnamed"),
+      isLocal(_isLocal),
+      isGlobal(_isGlobal),
+      isFixed(_isFixed),
+      fake_object(false),
+      isUserSpecified(false),
+      allocSite(_allocSite) {
+  }
+
+  ~MemoryObject();
+
+  /// Get an identifying string for this allocation.
+  void getAllocInfo(std::string &result) const;
+
+  void setName(std::string name) {
+    this->name = name;
+  }
+
+  ref<Expr> getBaseExpr() const { 
+    return ConstantExpr::create(address, kMachinePointerType);
+  }
+  ref<Expr> getSizeExpr() const { 
+    return ConstantExpr::create(size, kMachinePointerType);
+  }
+  ref<Expr> getOffsetExpr(ref<Expr> pointer) const {
+    return SubExpr::create(pointer, getBaseExpr());
+  }
+  ref<Expr> getBoundsCheckPointer(ref<Expr> pointer) const {
+    return getBoundsCheckOffset(getOffsetExpr(pointer));
+  }
+  ref<Expr> getBoundsCheckPointer(ref<Expr> pointer, unsigned bytes) const {
+    return getBoundsCheckOffset(getOffsetExpr(pointer), bytes);
+  }
+
+  ref<Expr> getBoundsCheckOffset(ref<Expr> offset) const {
+    if (size==0) {
+      return EqExpr::create(offset, ref<Expr>(0, kMachinePointerType));
+    } else {
+      return UltExpr::create(offset, getSizeExpr());
+    }
+  }
+  ref<Expr> getBoundsCheckOffset(ref<Expr> offset, unsigned bytes) const {
+    if (bytes<=size) {
+      return UltExpr::create(offset, 
+                             ref<Expr>(size - bytes + 1, kMachinePointerType));
+    } else {
+      return ref<Expr>(0, Expr::Bool);
+    }
+  }
+};
+
+class ObjectState {
+private:
+  friend class AddressSpace;
+  unsigned copyOnWriteOwner; // exclusively for AddressSpace
+
+  friend class ObjectHolder;
+  unsigned refCount;
+
+  const MemoryObject *object;
+
+  uint8_t *concreteStore;
+  // XXX cleanup name of flushMask (its backwards or something)
+  BitArray *concreteMask;
+
+  // mutable because may need flushed during read of const
+  mutable BitArray *flushMask;
+
+  ref<Expr> *knownSymbolics;
+
+public:
+  unsigned size;
+
+  // mutable because we may need flush during read of const
+  mutable UpdateList updates;
+
+  bool readOnly;
+
+public:
+  // initial contents are undefined but concrete, it is the creators
+  // responsibility to initialize the object contents appropriate
+  ObjectState(const MemoryObject *mo, unsigned size);
+  ObjectState(const ObjectState &os);
+  ~ObjectState();
+
+  const MemoryObject *getObject() const { return object; }
+
+  void setReadOnly(bool ro) { readOnly = ro; }
+
+  // make all bytes are concrete with undefined values
+  void makeConcrete();
+
+  void makeSymbolic();
+
+  // make contents all concrete and zero
+  void initializeToZero();
+  // make contents all concrete and random
+  void initializeToRandom();
+
+  ref<Expr> read(ref<Expr> offset, Expr::Width width) const;
+  ref<Expr> read(unsigned offset, Expr::Width width) const;
+  ref<Expr> read1(unsigned offset) const;
+  ref<Expr> read8(unsigned offset) const;
+  ref<Expr> read16(unsigned offset) const;
+  ref<Expr> read32(unsigned offset) const;
+  ref<Expr> read64(unsigned offset) const;
+
+  // return bytes written.
+  void write(unsigned offset, ref<Expr> value);
+  void write(ref<Expr> offset, ref<Expr> value);
+
+  void write8(unsigned offset, uint8_t value);
+  void write16(unsigned offset, uint16_t value);
+  void write32(unsigned offset, uint32_t value);
+  void write64(unsigned offset, uint64_t value);
+
+private:
+  ref<Expr> read1(ref<Expr> offset) const;
+  ref<Expr> read8(ref<Expr> offset) const;
+  ref<Expr> read16(ref<Expr> offset) const;
+  ref<Expr> read32(ref<Expr> offset) const;
+  ref<Expr> read64(ref<Expr> offset) const;
+
+  void write1(unsigned offset, ref<Expr> value);
+  void write1(ref<Expr> offset, ref<Expr> value);
+  void write8(unsigned offset, ref<Expr> value);
+  void write8(ref<Expr> offset, ref<Expr> value);
+  void write16(unsigned offset, ref<Expr> value);
+  void write16(ref<Expr> offset, ref<Expr> value);
+  void write32(unsigned offset, ref<Expr> value);
+  void write32(ref<Expr> offset, ref<Expr> value);
+  void write64(unsigned offset, ref<Expr> value);
+  void write64(ref<Expr> offset, ref<Expr> value);
+
+  
+  void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r, unsigned *size_r) const;
+  void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const;
+  void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize);
+
+  bool isByteConcrete(unsigned offset) const;
+  bool isByteFlushed(unsigned offset) const;
+  bool isByteKnownSymbolic(unsigned offset) const;
+
+  void markByteConcrete(unsigned offset);
+  void markByteSymbolic(unsigned offset);
+  void markByteFlushed(unsigned offset);
+  void markByteUnflushed(unsigned offset);
+  void setKnownSymbolic(unsigned offset, Expr *value);
+
+  void print();
+};
+  
+} // End klee namespace
+
+#endif