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

diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
new file mode 100644
index 00000000..a281714c
--- /dev/null
+++ b/lib/Core/AddressSpace.h
@@ -0,0 +1,131 @@
+//===-- AddressSpace.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_ADDRESSSPACE_H
+#define KLEE_ADDRESSSPACE_H
+
+#include "ObjectHolder.h"
+
+#include "klee/Expr.h"
+#include "klee/Internal/ADT/ImmutableMap.h"
+
+namespace klee {
+  class ExecutionState;
+  class MemoryObject;
+  class ObjectState;
+  class TimingSolver;
+
+  template<class T> class ref;
+
+  typedef std::pair<const MemoryObject*, const ObjectState*> ObjectPair;
+  typedef std::vector<ObjectPair> ResolutionList;  
+
+  /// Function object ordering MemoryObject's by address.
+  struct MemoryObjectLT {
+    bool operator()(const MemoryObject *a, const MemoryObject *b) const;
+  };
+  
+  typedef ImmutableMap<const MemoryObject*, ObjectHolder, MemoryObjectLT> MemoryMap;
+  
+  class AddressSpace {
+  private:
+    /// Epoch counter used to control ownership of objects.
+    mutable unsigned cowKey;
+
+    /// Unsupported, use copy constructor
+    AddressSpace &operator=(const AddressSpace&); 
+    
+  public:
+    /// The MemoryObject -> ObjectState map that constitutes the
+    /// address space.
+    ///
+    /// The set of objects where o->copyOnWriteOwner == cowKey are the
+    /// objects that we own.
+    ///
+    /// \invariant forall o in objects, o->copyOnWriteOwner <= cowKey
+    MemoryMap objects;
+    
+  public:
+    AddressSpace() : cowKey(1) {}
+    AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects) { }
+    ~AddressSpace() {}
+
+    /// Resolve address to an ObjectPair in result.
+    /// \return true iff an object was found.
+    bool resolveOne(uint64_t address, 
+                    ObjectPair &result);
+
+    /// Resolve address to an ObjectPair in result.
+    ///
+    /// \param state The state this address space is part of.
+    /// \param solver A solver used to determine possible 
+    ///               locations of the \a address.
+    /// \param address The address to search for.
+    /// \param[out] result An ObjectPair this address can resolve to 
+    ///               (when returning true).
+    /// \return true iff an object was found at \a address.
+    bool resolveOne(ExecutionState &state, 
+                    TimingSolver *solver,
+                    ref<Expr> address,
+                    ObjectPair &result,
+                    bool &success);
+
+    /// Resolve address to a list of ObjectPairs it can point to. If
+    /// maxResolutions is non-zero then no more than that many pairs
+    /// will be returned. 
+    ///
+    /// \return true iff the resolution is incomplete (maxResolutions
+    /// is non-zero and the search terminated early, or a query timed out).
+    bool resolve(ExecutionState &state,
+                 TimingSolver *solver,
+                 ref<Expr> address, 
+                 ResolutionList &rl, 
+                 unsigned maxResolutions=0,
+                 double timeout=0.);
+
+    /***/
+
+    /// Add a binding to the address space.
+    void bindObject(const MemoryObject *mo, ObjectState *os);
+
+    /// Remove a binding from the address space.
+    void unbindObject(const MemoryObject *mo);
+
+    /// Lookup a binding from a MemoryObject.
+    const ObjectState *findObject(const MemoryObject *mo) const;
+
+    /// \brief Obtain an ObjectState suitable for writing.
+    ///
+    /// This returns a writeable object state, creating a new copy of
+    /// the given ObjectState if necessary. If the address space owns
+    /// the ObjectState then this routine effectively just strips the
+    /// const qualifier it.
+    ///
+    /// \param mo The MemoryObject to get a writeable ObjectState for.
+    /// \param os The current binding of the MemoryObject.
+    /// \return A writeable ObjectState (\a os or a copy).
+    ObjectState *getWriteable(const MemoryObject *mo, const ObjectState *os);
+
+    /// Copy the concrete values of all managed ObjectStates into the
+    /// actual system memory location they were allocated at.
+    void copyOutConcretes();
+
+    /// Copy the concrete values of all managed ObjectStates back from
+    /// the actual system memory location they were allocated
+    /// at. ObjectStates will only be written to (and thus,
+    /// potentially copied) if the memory values are different from
+    /// the current concrete values.
+    ///
+    /// \retval true The copy succeeded. 
+    /// \retval false The copy failed because a read-only object was modified.
+    bool copyInConcretes();
+  };
+} // End klee namespace
+
+#endif