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