klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
AddressSpace.h
Go to the documentation of this file.
1 //===-- AddressSpace.h ------------------------------------------*- C++ -*-===//
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 #ifndef KLEE_ADDRESSSPACE_H
11 #define KLEE_ADDRESSSPACE_H
12 
13 #include "ObjectHolder.h"
14 
15 #include "klee/Expr.h"
17 
18 namespace klee {
19  class ExecutionState;
20  class MemoryObject;
21  class ObjectState;
22  class TimingSolver;
23 
24  template<class T> class ref;
25 
26  typedef std::pair<const MemoryObject*, const ObjectState*> ObjectPair;
27  typedef std::vector<ObjectPair> ResolutionList;
28 
30  struct MemoryObjectLT {
31  bool operator()(const MemoryObject *a, const MemoryObject *b) const;
32  };
33 
35 
36  class AddressSpace {
37  private:
39  mutable unsigned cowKey;
40 
43 
44  public:
53 
54  public:
55  AddressSpace() : cowKey(1) {}
58 
61  bool resolveOne(const ref<ConstantExpr> &address,
62  ObjectPair &result);
63 
73  bool resolveOne(ExecutionState &state,
74  TimingSolver *solver,
75  ref<Expr> address,
76  ObjectPair &result,
77  bool &success);
78 
85  bool resolve(ExecutionState &state,
86  TimingSolver *solver,
87  ref<Expr> address,
88  ResolutionList &rl,
89  unsigned maxResolutions=0,
90  double timeout=0.);
91 
92  /***/
93 
95  void bindObject(const MemoryObject *mo, ObjectState *os);
96 
98  void unbindObject(const MemoryObject *mo);
99 
101  const ObjectState *findObject(const MemoryObject *mo) const;
102 
113  ObjectState *getWriteable(const MemoryObject *mo, const ObjectState *os);
114 
117  void copyOutConcretes();
118 
127  bool copyInConcretes();
128  };
129 } // End klee namespace
130 
131 #endif
Function object ordering MemoryObject's by address.
Definition: AddressSpace.h:30
std::pair< const MemoryObject *, const ObjectState * > ObjectPair
Definition: AddressSpace.h:24
unsigned cowKey
Epoch counter used to control ownership of objects.
Definition: AddressSpace.h:39
bool operator()(const MemoryObject *a, const MemoryObject *b) const
ObjectState * getWriteable(const MemoryObject *mo, const ObjectState *os)
Obtain an ObjectState suitable for writing.
bool resolveOne(const ref< ConstantExpr > &address, ObjectPair &result)
AddressSpace(const AddressSpace &b)
Definition: AddressSpace.h:56
void bindObject(const MemoryObject *mo, ObjectState *os)
Add a binding to the address space.
std::vector< ObjectPair > ResolutionList
Definition: AddressSpace.h:27
AddressSpace & operator=(const AddressSpace &)
Unsupported, use copy constructor.
bool resolve(ExecutionState &state, TimingSolver *solver, ref< Expr > address, ResolutionList &rl, unsigned maxResolutions=0, double timeout=0.)
ImmutableMap< const MemoryObject *, ObjectHolder, MemoryObjectLT > MemoryMap
Definition: AddressSpace.h:34
const ObjectState * findObject(const MemoryObject *mo) const
Lookup a binding from a MemoryObject.
void unbindObject(const MemoryObject *mo)
Remove a binding from the address space.