1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
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(const ref<ConstantExpr> &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
|
