Memory.h

Go to the documentation of this file.

//===-- Memory.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_MEMORY_H
#define KLEE_MEMORY_H
 
#include "Context.h"
#include "TimingSolver.h"
 
#include "klee/Expr/Expr.h"
 
#include "llvm/ADT/StringExtras.h"
 
#include <string>
#include <vector>
 
namespace llvm {
  class Value;
}
 
namespace klee {
 
class ArrayCache;
class BitArray;
class ExecutionState;
class MemoryManager;
class Solver;
 
class MemoryObject {
  friend class STPBuilder;
  friend class ObjectState;
  friend class ExecutionState;
  friend class ref<MemoryObject>;
  friend class ref<const MemoryObject>;
 
private:
  static int counter;
  mutable class ReferenceCounter _refCount;
 
public:
  unsigned id;
  uint64_t address;
 
  unsigned size;
  mutable std::string name;
 
  bool isLocal;
  mutable bool isGlobal;
  bool isFixed;
 
  bool isUserSpecified;
 
  MemoryManager *parent;
 
  const llvm::Value *allocSite;
 
  // DO NOT IMPLEMENT
  MemoryObject(const MemoryObject &b);
  MemoryObject &operator=(const MemoryObject &b);
 
public:
  // XXX this is just a temp hack, should be removed
  explicit
  MemoryObject(uint64_t _address) 
    : id(counter++),
      address(_address),
      size(0),
      isFixed(true),
      parent(NULL),
      allocSite(0) {
  }
 
  MemoryObject(uint64_t _address, unsigned _size, 
               bool _isLocal, bool _isGlobal, bool _isFixed,
               const llvm::Value *_allocSite,
               MemoryManager *_parent)
    : id(counter++),
      address(_address),
      size(_size),
      name("unnamed"),
      isLocal(_isLocal),
      isGlobal(_isGlobal),
      isFixed(_isFixed),
      isUserSpecified(false),
      parent(_parent), 
      allocSite(_allocSite) {
  }
 
  ~MemoryObject();
 
  void getAllocInfo(std::string &result) const;
 
  void setName(std::string name) const {
    this->name = name;
  }
 
  ref<ConstantExpr> getBaseExpr() const { 
    return ConstantExpr::create(address, Context::get().getPointerWidth());
  }
  ref<ConstantExpr> getSizeExpr() const { 
    return ConstantExpr::create(size, Context::get().getPointerWidth());
  }
  ref<Expr> getOffsetExpr(ref<Expr> pointer) const {
    return SubExpr::create(pointer, getBaseExpr());
  }
  ref<Expr> getBoundsCheckPointer(ref<Expr> pointer) const {
    return getBoundsCheckOffset(getOffsetExpr(pointer));
  }
  ref<Expr> getBoundsCheckPointer(ref<Expr> pointer, unsigned bytes) const {
    return getBoundsCheckOffset(getOffsetExpr(pointer), bytes);
  }
 
  ref<Expr> getBoundsCheckOffset(ref<Expr> offset) const {
    if (size==0) {
      return EqExpr::create(offset, 
                            ConstantExpr::alloc(0, Context::get().getPointerWidth()));
    } else {
      return UltExpr::create(offset, getSizeExpr());
    }
  }
  ref<Expr> getBoundsCheckOffset(ref<Expr> offset, unsigned bytes) const {
    if (bytes<=size) {
      return UltExpr::create(offset, 
                             ConstantExpr::alloc(size - bytes + 1, 
                                                 Context::get().getPointerWidth()));
    } else {
      return ConstantExpr::alloc(0, Expr::Bool);
    }
  }
 
  int compare(const MemoryObject &b) const {
    // Short-cut with id
    if (id == b.id)
      return 0;
    if (address != b.address)
      return (address < b.address ? -1 : 1);
 
    if (size != b.size)
      return (size < b.size ? -1 : 1);
 
    if (allocSite != b.allocSite)
      return (allocSite < b.allocSite ? -1 : 1);
 
    return 0;
  }
};
 
class ObjectState {
private:
  friend class AddressSpace;
  friend class ref<ObjectState>;
 
  unsigned copyOnWriteOwner; // exclusively for AddressSpace
 
  class ReferenceCounter _refCount;
 
  ref<const MemoryObject> object;
 
  uint8_t *concreteStore;
 
  BitArray *concreteMask;
 
  ref<Expr> *knownSymbolics;
 
  mutable BitArray *unflushedMask;
 
  // mutable because we may need flush during read of const
  mutable UpdateList updates;
 
public:
  unsigned size;
 
  bool readOnly;
 
public:
  ObjectState(const MemoryObject *mo);
 
  ObjectState(const MemoryObject *mo, const Array *array);
 
  ObjectState(const ObjectState &os);
  ~ObjectState();
 
  const MemoryObject *getObject() const { return object.get(); }
 
  void setReadOnly(bool ro) { readOnly = ro; }
 
  void initializeToZero();
 
  void initializeToRandom();
 
  ref<Expr> read(ref<Expr> offset, Expr::Width width) const;
  ref<Expr> read(unsigned offset, Expr::Width width) const;
  ref<Expr> read8(unsigned offset) const;
 
  void write(unsigned offset, ref<Expr> value);
  void write(ref<Expr> offset, ref<Expr> value);
 
  void write8(unsigned offset, uint8_t value);
  void write16(unsigned offset, uint16_t value);
  void write32(unsigned offset, uint32_t value);
  void write64(unsigned offset, uint64_t value);
  void print() const;
 
  /*
    Looks at all the symbolic bytes of this object, gets a value for them
    from the solver and puts them in the concreteStore.
  */
  void flushToConcreteStore(TimingSolver *solver,
                            const ExecutionState &state) const;
 
private:
  const UpdateList &getUpdates() const;
 
  void makeConcrete();
 
  void makeSymbolic();
 
  ref<Expr> read8(ref<Expr> offset) const;
  void write8(unsigned offset, ref<Expr> value);
  void write8(ref<Expr> offset, ref<Expr> value);
 
  void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r, 
                            unsigned *size_r) const;
  void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const;
  void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize);
 
  bool isByteConcrete(unsigned offset) const;
 
  bool isByteKnownSymbolic(unsigned offset) const;
 
  bool isByteUnflushed(unsigned offset) const;
 
  void markByteConcrete(unsigned offset);
  void markByteSymbolic(unsigned offset);
  void markByteFlushed(unsigned offset);
  void markByteUnflushed(unsigned offset);
  void setKnownSymbolic(unsigned offset, Expr *value);
 
  ArrayCache *getArrayCache() const;
};
  
} // End klee namespace
 
#endif /* KLEE_MEMORY_H */