37 return res ? res->second.get() :
nullptr;
50 newObjectState->copyOnWriteOwner =
cowKey;
52 return newObjectState.
get();
59 uint64_t address = addr->getZExtValue();
63 const auto &mo = res->first;
66 if ((mo->size==0 && address==mo->address) ||
67 (address - mo->address < mo->size)) {
68 result.first = res->first;
69 result.second = res->second.get();
81 bool &success)
const {
82 if (
ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
93 uint64_t example = cex->getZExtValue();
100 result.first = res->first;
101 result.second = res->second.get();
116 const auto &mo = oi->first;
120 mo->getBoundsCheckPointer(address), mayBeTrue,
124 result.first = oi->first;
125 result.second = oi->second.get();
131 UgeExpr::create(address, mo->getBaseExpr()),
140 for (oi=start; oi!=end; ++oi) {
141 const auto &mo = oi->first;
145 UltExpr::create(address, mo->getBaseExpr()),
154 mo->getBoundsCheckPointer(address), mayBeTrue,
158 result.first = oi->first;
159 result.second = oi->second.get();
174 unsigned maxResolutions)
const {
190 auto size = rl.size();
200 if (size == maxResolutions)
209 unsigned maxResolutions,
time::Span timeout)
const {
236 uint64_t example = cex->getZExtValue();
247 while (oi != begin) {
250 if (timeout && timeout < timer.
delta())
253 auto op = std::make_pair<>(mo, oi->second.get());
258 return incomplete ? true :
false;
270 for (oi = start; oi != end; ++oi) {
272 if (timeout && timeout < timer.
delta())
282 auto op = std::make_pair<>(mo, oi->second.get());
287 return incomplete ? true :
false;
306 const auto &os = it->second;
307 auto address =
reinterpret_cast<std::uint8_t*
>(mo->
address);
310 memcpy(address, os->concreteStore, mo->
size);
320 const auto &os = obj.second;
331 uint64_t src_address) {
332 auto address =
reinterpret_cast<std::uint8_t*
>(src_address);
void unbindObject(const MemoryObject *mo)
Remove a binding from the address space.
int checkPointerInObject(ExecutionState &state, TimingSolver *solver, ref< Expr > p, const ObjectPair &op, ResolutionList &rl, unsigned maxResolutions) const
bool resolveOne(const ref< ConstantExpr > &address, ObjectPair &result) const
bool copyInConcrete(const MemoryObject *mo, const ObjectState *os, uint64_t src_address)
bool resolve(ExecutionState &state, TimingSolver *solver, ref< Expr > p, ResolutionList &rl, unsigned maxResolutions=0, time::Span timeout=time::Span()) const
unsigned cowKey
Epoch counter used to control ownership of objects.
const ObjectState * findObject(const MemoryObject *mo) const
Lookup a binding from a MemoryObject.
ObjectState * getWriteable(const MemoryObject *mo, const ObjectState *os)
Obtain an ObjectState suitable for writing.
ExecutionState representing a path under exploration.
SolverQueryMetaData queryMetaData
Statistics and information.
ConstraintSet constraints
Constraints collected so far.
const value_type * lookup(const key_type &key) const
ImmutableMap replace(const value_type &value) const
ImmutableMap remove(const key_type &key) const
const value_type * lookup_previous(const key_type &key) const
iterator upper_bound(const key_type &key) const
unsigned size
size in bytes
ref< Expr > getBoundsCheckPointer(ref< Expr > pointer) const
ref< ConstantExpr > getBaseExpr() const
unsigned copyOnWriteOwner
uint8_t * concreteStore
Holds all known concrete bytes.
bool getValue(const ConstraintSet &, ref< Expr > expr, ref< ConstantExpr > &result, SolverQueryMetaData &metaData)
bool mayBeTrue(const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
bool mustBeTrue(const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
std::vector< ObjectPair > ResolutionList
std::pair< const MemoryObject *, const ObjectState * > ObjectPair
bool operator()(const MemoryObject *a, const MemoryObject *b) const