klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Memory.h
Go to the documentation of this file.
1 //===-- Memory.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_MEMORY_H
11 #define KLEE_MEMORY_H
12 
13 #include "Context.h"
14 #include "klee/Expr.h"
15 
16 #include "llvm/ADT/StringExtras.h"
17 
18 #include <vector>
19 #include <string>
20 
21 namespace llvm {
22  class Value;
23 }
24 
25 namespace klee {
26 
27 class BitArray;
28 class MemoryManager;
29 class Solver;
30 
31 class MemoryObject {
32  friend class STPBuilder;
33  friend class ObjectState;
34  friend class ExecutionState;
35 
36 private:
37  static int counter;
38  mutable unsigned refCount;
39 
40 public:
41  unsigned id;
42  uint64_t address;
43 
45  unsigned size;
46  mutable std::string name;
47 
48  bool isLocal;
49  mutable bool isGlobal;
50  bool isFixed;
51 
55 
57 
61  const llvm::Value *allocSite;
62 
67  mutable std::vector< ref<Expr> > cexPreferences;
68 
69  // DO NOT IMPLEMENT
70  MemoryObject(const MemoryObject &b);
72 
73 public:
74  // XXX this is just a temp hack, should be removed
75  explicit
76  MemoryObject(uint64_t _address)
77  : refCount(0),
78  id(counter++),
79  address(_address),
80  size(0),
81  isFixed(true),
82  parent(NULL),
83  allocSite(0) {
84  }
85 
86  MemoryObject(uint64_t _address, unsigned _size,
87  bool _isLocal, bool _isGlobal, bool _isFixed,
88  const llvm::Value *_allocSite,
89  MemoryManager *_parent)
90  : refCount(0),
91  id(counter++),
92  address(_address),
93  size(_size),
94  name("unnamed"),
95  isLocal(_isLocal),
96  isGlobal(_isGlobal),
97  isFixed(_isFixed),
98  fake_object(false),
99  isUserSpecified(false),
100  parent(_parent),
101  allocSite(_allocSite) {
102  }
103 
104  ~MemoryObject();
105 
107  void getAllocInfo(std::string &result) const;
108 
109  void setName(std::string name) const {
110  this->name = name;
111  }
112 
114  return ConstantExpr::create(address, Context::get().getPointerWidth());
115  }
117  return ConstantExpr::create(size, Context::get().getPointerWidth());
118  }
120  return SubExpr::create(pointer, getBaseExpr());
121  }
123  return getBoundsCheckOffset(getOffsetExpr(pointer));
124  }
125  ref<Expr> getBoundsCheckPointer(ref<Expr> pointer, unsigned bytes) const {
126  return getBoundsCheckOffset(getOffsetExpr(pointer), bytes);
127  }
128 
130  if (size==0) {
131  return EqExpr::create(offset,
132  ConstantExpr::alloc(0, Context::get().getPointerWidth()));
133  } else {
134  return UltExpr::create(offset, getSizeExpr());
135  }
136  }
137  ref<Expr> getBoundsCheckOffset(ref<Expr> offset, unsigned bytes) const {
138  if (bytes<=size) {
139  return UltExpr::create(offset,
140  ConstantExpr::alloc(size - bytes + 1,
141  Context::get().getPointerWidth()));
142  } else {
143  return ConstantExpr::alloc(0, Expr::Bool);
144  }
145  }
146 };
147 
148 class ObjectState {
149 private:
150  friend class AddressSpace;
151  unsigned copyOnWriteOwner; // exclusively for AddressSpace
152 
153  friend class ObjectHolder;
154  unsigned refCount;
155 
157 
158  uint8_t *concreteStore;
159  // XXX cleanup name of flushMask (its backwards or something)
161 
162  // mutable because may need flushed during read of const
163  mutable BitArray *flushMask;
164 
166 
167  // mutable because we may need flush during read of const
169 
170 public:
171  unsigned size;
172 
173  bool readOnly;
174 
175 public:
179  ObjectState(const MemoryObject *mo);
180 
183  ObjectState(const MemoryObject *mo, const Array *array);
184 
185  ObjectState(const ObjectState &os);
186  ~ObjectState();
187 
188  const MemoryObject *getObject() const { return object; }
189 
190  void setReadOnly(bool ro) { readOnly = ro; }
191 
192  // make contents all concrete and zero
193  void initializeToZero();
194  // make contents all concrete and random
195  void initializeToRandom();
196 
197  ref<Expr> read(ref<Expr> offset, Expr::Width width) const;
198  ref<Expr> read(unsigned offset, Expr::Width width) const;
199  ref<Expr> read8(unsigned offset) const;
200 
201  // return bytes written.
202  void write(unsigned offset, ref<Expr> value);
203  void write(ref<Expr> offset, ref<Expr> value);
204 
205  void write8(unsigned offset, uint8_t value);
206  void write16(unsigned offset, uint16_t value);
207  void write32(unsigned offset, uint32_t value);
208  void write64(unsigned offset, uint64_t value);
209 
210 private:
211  const UpdateList &getUpdates() const;
212 
213  void makeConcrete();
214 
215  void makeSymbolic();
216 
217  ref<Expr> read8(ref<Expr> offset) const;
218  void write8(unsigned offset, ref<Expr> value);
219  void write8(ref<Expr> offset, ref<Expr> value);
220 
221  void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r,
222  unsigned *size_r) const;
223  void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const;
224  void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize);
225 
226  bool isByteConcrete(unsigned offset) const;
227  bool isByteFlushed(unsigned offset) const;
228  bool isByteKnownSymbolic(unsigned offset) const;
229 
230  void markByteConcrete(unsigned offset);
231  void markByteSymbolic(unsigned offset);
232  void markByteFlushed(unsigned offset);
233  void markByteUnflushed(unsigned offset);
234  void setKnownSymbolic(unsigned offset, Expr *value);
235 
236  void print();
237 };
238 
239 } // End klee namespace
240 
241 #endif
MemoryObject & operator=(const MemoryObject &b)
void setReadOnly(bool ro)
Definition: Memory.h:190
ref< ConstantExpr > getBaseExpr() const
Definition: Memory.h:113
bool fake_object
true if created by us.
Definition: Memory.h:53
MemoryObject(uint64_t _address)
Definition: Memory.h:76
ref< Expr > getBoundsCheckOffset(ref< Expr > offset) const
Definition: Memory.h:129
const UpdateList & getUpdates() const
Definition: Memory.cpp:182
MemoryManager * parent
Definition: Memory.h:56
bool isByteFlushed(unsigned offset) const
Definition: Memory.cpp:341
void setKnownSymbolic(unsigned offset, Expr *value)
Definition: Memory.cpp:373
std::vector< ref< Expr > > cexPreferences
Definition: Memory.h:67
MemoryObject(uint64_t _address, unsigned _size, bool _isLocal, bool _isGlobal, bool _isFixed, const llvm::Value *_allocSite, MemoryManager *_parent)
Definition: Memory.h:86
void fastRangeCheckOffset(ref< Expr > offset, unsigned *base_r, unsigned *size_r) const
Definition: Memory.cpp:280
Class representing a complete list of updates into an array.
Definition: Expr.h:655
const llvm::Value * allocSite
Definition: Memory.h:61
std::string name
Definition: Memory.h:46
unsigned size
size in bytes
Definition: Memory.h:45
Class representing symbolic expressions.
Definition: Expr.h:88
const MemoryObject * object
Definition: Memory.h:156
bool isByteConcrete(unsigned offset) const
Definition: Memory.cpp:337
uint64_t address
Definition: Memory.h:42
void write(unsigned offset, ref< Expr > value)
Definition: Memory.cpp:529
static const Context & get()
get - Return the global singleton instance of the Context.
Definition: Context.cpp:35
ObjectState(const MemoryObject *mo)
Definition: Memory.cpp:101
void markByteFlushed(unsigned offset)
Definition: Memory.cpp:365
void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize)
Definition: Memory.cpp:307
void initializeToZero()
Definition: Memory.cpp:259
ref< Expr > getBoundsCheckPointer(ref< Expr > pointer) const
Definition: Memory.h:122
ref< ConstantExpr > getSizeExpr() const
Definition: Memory.h:116
static ref< ConstantExpr > create(uint64_t v, Width w)
Definition: Expr.h:412
ref< Expr > getOffsetExpr(ref< Expr > pointer) const
Definition: Memory.h:119
unsigned id
Definition: Memory.h:41
void markByteConcrete(unsigned offset)
Definition: Memory.cpp:349
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
void makeConcrete()
Definition: Memory.cpp:238
const MemoryObject * getObject() const
Definition: Memory.h:188
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
BitArray * concreteMask
Definition: Memory.h:160
ref< Expr > getBoundsCheckOffset(ref< Expr > offset, unsigned bytes) const
Definition: Memory.h:137
void markByteUnflushed(unsigned offset)
Definition: Memory.cpp:360
MemoryObject(const MemoryObject &b)
ref< Expr > * knownSymbolics
Definition: Memory.h:165
void write8(unsigned offset, uint8_t value)
Definition: Memory.cpp:417
unsigned refCount
Definition: Memory.h:38
unsigned refCount
Definition: Memory.h:154
static const Width Bool
Definition: Expr.h:97
unsigned size
Definition: Memory.h:171
void write32(unsigned offset, uint32_t value)
Definition: Memory.cpp:570
void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const
Definition: Memory.cpp:287
void markByteSymbolic(unsigned offset)
Definition: Memory.cpp:354
ref< Expr > getBoundsCheckPointer(ref< Expr > pointer, unsigned bytes) const
Definition: Memory.h:125
bool isByteKnownSymbolic(unsigned offset) const
Definition: Memory.cpp:345
static int counter
Definition: Memory.h:37
uint8_t * concreteStore
Definition: Memory.h:158
unsigned copyOnWriteOwner
Definition: Memory.h:151
void getAllocInfo(std::string &result) const
Get an identifying string for this allocation.
Definition: Memory.cpp:77
void write64(unsigned offset, uint64_t value)
Definition: Memory.cpp:578
UpdateList updates
Definition: Memory.h:168
ref< Expr > read8(unsigned offset) const
Definition: Memory.cpp:387
BitArray * flushMask
Definition: Memory.h:163
void write16(unsigned offset, uint16_t value)
Definition: Memory.cpp:562
ref< Expr > read(ref< Expr > offset, Expr::Width width) const
Definition: Memory.cpp:457
bool isUserSpecified
Definition: Memory.h:54
void makeSymbolic()
Definition: Memory.cpp:247
void setName(std::string name) const
Definition: Memory.h:109
void initializeToRandom()
Definition: Memory.cpp:264