 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
0.0% |
0 / 0 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
0.0% |
0 / 0 |
| |
|
Line Coverage: |
100.0% |
3 / 3 |
| |
 |
|
 |
1 : //===- AddressSpace.h - --*- C++ -*-===//
2 :
3 : #ifndef KLEE_ADDRESSSPACE_H
4 : #define KLEE_ADDRESSSPACE_H
5 :
6 : #include "ObjectHolder.h"
7 :
8 : #include "klee/Expr.h"
9 : #include "klee/Internal/ADT/ImmutableMap.h"
10 :
11 : namespace klee {
12 : class ExecutionState;
13 : class MemoryObject;
14 : class ObjectState;
15 : class TimingSolver;
16 :
17 : template<class T> class ref;
18 :
19 : typedef std::pair<const MemoryObject*, const ObjectState*> ObjectPair;
20 : typedef std::vector<ObjectPair> ResolutionList;
21 :
22 : /// Function object ordering MemoryObject's by address.
23 : struct MemoryObjectLT {
24 : bool operator()(const MemoryObject *a, const MemoryObject *b) const;
25 : };
26 :
27 : typedef ImmutableMap<const MemoryObject*, ObjectHolder, MemoryObjectLT> MemoryMap;
28 :
29 : class AddressSpace {
30 : private:
31 : /// Epoch counter used to control ownership of objects.
32 : mutable unsigned cowKey;
33 :
34 : /// Unsupported, use copy constructor
35 : AddressSpace &operator=(const AddressSpace&);
36 :
37 : public:
38 : /// The MemoryObject -> ObjectState map that constitutes the address space.
39 : ///
40 : /// The set of objects where o->copyOnWriteOwner == cowKey are the objects that we own.
41 : ///
42 : /// \invariant forall o in objects, o->copyOnWriteOwner <= cowKey
43 : MemoryMap objects;
44 :
45 : public:
46 103: AddressSpace() : cowKey(1) {}
47 1350: AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects) { }
48 1453: ~AddressSpace() {}
49 :
50 : /// Resolve address to an ObjectPair in result.
51 : /// \return true iff an object was found.
52 : bool resolveOne(uint64_t address,
53 : ObjectPair &result);
54 :
55 : /// Resolve address to an ObjectPair in result.
56 : ///
57 : /// \param state The state this address space is part of.
58 : /// \param solver A solver used to determine possible
59 : /// locations of the \a address.
60 : /// \param address The address to search for.
61 : /// \param[out] result An ObjectPair this address can resolve to
62 : /// (when returning true).
63 : /// \return true iff an object was found at \a address.
64 : bool resolveOne(ExecutionState &state,
65 : TimingSolver *solver,
66 : ref<Expr> address,
67 : ObjectPair &result,
68 : bool &success);
69 :
70 : /// Resolve address to a list of ObjectPairs it can point to. If
71 : /// maxResolutions is non-zero then no more than that many pairs
72 : /// will be returned.
73 : ///
74 : /// \return true iff the resolution is incomplete (maxResolutions
75 : /// is non-zero and the search terminated early, or a query timed out).
76 : bool resolve(ExecutionState &state,
77 : TimingSolver *solver,
78 : ref<Expr> address,
79 : ResolutionList &rl,
80 : unsigned maxResolutions=0,
81 : double timeout=0.);
82 :
83 : /***/
84 :
85 : /// Add a binding to the address space.
86 : void bindObject(const MemoryObject *mo, ObjectState *os);
87 :
88 : /// Remove a binding from the address space.
89 : void unbindObject(const MemoryObject *mo);
90 :
91 : /// Lookup a binding from a MemoryObject.
92 : const ObjectState *findObject(const MemoryObject *mo) const;
93 :
94 : /// \brief Obtain an ObjectState suitable for writing.
95 : ///
96 : /// This returns a writeable object state, creating a new copy of
97 : /// the given ObjectState if necessary. If the address space owns
98 : /// the ObjectState then this routine effectively just strips the
99 : /// const qualifier it.
100 : ///
101 : /// \param mo The MemoryObject to get a writeable ObjectState for.
102 : /// \param os The current binding of the MemoryObject.
103 : /// \return A writeable ObjectState (\a os or a copy).
104 : ObjectState *getWriteable(const MemoryObject *mo, const ObjectState *os);
105 :
106 : /// Copy the concrete values of all managed ObjectStates into the
107 : /// actual system memory location they were allocated at.
108 : void copyOutConcretes();
109 :
110 : /// Copy the concrete values of all managed ObjectStates back from
111 : /// the actual system memory location they were allocated
112 : /// at. ObjectStates will only be written to (and thus,
113 : /// potentially copied) if the memory values are different from
114 : /// the current concrete values.
115 : ///
116 : /// \retval true The copy succeeded.
117 : /// \retval false The copy failed because a read-only object was modified.
118 : bool copyInConcretes();
119 : };
120 : } // End klee namespace
121 :
122 : #endif
Generated: 2009-05-17 22:47 by zcov