ROSE  0.9.9.139
SymbolicMemory2.h
1 // Symbolic memory -- a memory state where memory is represented by an SMT function whose domain is the address space and whose
2 // range are the bytes stored at those addresses.
3 
4 #ifndef Rose_SymbolicMemory_H
5 #define Rose_SymbolicMemory_H
6 
7 #include <BaseSemantics2.h>
8 
9 namespace Rose {
10 namespace BinaryAnalysis {
11 namespace InstructionSemantics2 {
12 namespace BaseSemantics {
13 
15 typedef boost::shared_ptr<class SymbolicMemory> SymbolicMemoryPtr;
16 
22 class SymbolicMemory: public MemoryState {
23  SymbolicExpr::Ptr mem_;
24 protected:
25  // All memory states should be heap allocated; use instance(), create(), or clone() instead.
26  explicit SymbolicMemory(const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
27  : MemoryState(addrProtoval, valProtoval) {
28  // Initially assume that addresses are 32 bits wide and values are 8 bits wide. We can change this on the first access.
29  mem_ = SymbolicExpr::makeMemory(32, 8);
30  }
31 
32 public:
34  static SymbolicMemoryPtr instance(const SValuePtr &addrProtoval, const SValuePtr &valProtoval) {
35  return SymbolicMemoryPtr(new SymbolicMemory(addrProtoval, valProtoval));
36  }
37 
38 public:
39  // documented in base class
40  virtual MemoryStatePtr create(const SValuePtr &addrProtoval, const SValuePtr &valProtoval) const ROSE_OVERRIDE {
41  return instance(addrProtoval, valProtoval);
42  }
43 
44  // documented in base class
45  virtual MemoryStatePtr clone() const ROSE_OVERRIDE {
46  return SymbolicMemoryPtr(new SymbolicMemory(*this));
47  }
48 
52  static SymbolicMemoryPtr promote(const MemoryStatePtr &x) {
53  SymbolicMemoryPtr retval = boost::dynamic_pointer_cast<SymbolicMemory>(x);
54  ASSERT_not_null(retval);
55  return retval;
56  }
57 
58 public:
62  SymbolicExpr::Ptr expression() const { return mem_; }
63  void expression(const SymbolicExpr::Ptr &mem);
66 public:
67  virtual bool
69  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
70 
71  virtual void clear() ROSE_OVERRIDE;
72 
73  virtual SValuePtr readMemory(const SValuePtr &address, const SValuePtr &dflt,
74  RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;
75 
76  virtual void writeMemory(const SValuePtr &address, const SValuePtr &value,
77  RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;
78 
79 public:
80  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
81 };
82 
83 } // namespace
84 } // namespace
85 } // namespace
86 } // namespace
87 
88 #endif
virtual void print(std::ostream &, Formatter &) const ROSE_OVERRIDE
Print a memory state to more than one line of output.
static SymbolicMemoryPtr instance(const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
Instantiate a new empty memory state on the heap.
STL namespace.
virtual void writeMemory(const SValuePtr &address, const SValuePtr &value, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE
Write a value to memory.
Main namespace for the ROSE library.
static SymbolicMemoryPtr promote(const MemoryStatePtr &x)
Convert pointer to a SymbolicMemory pointer.
SymbolicExpr::Ptr expression() const
Property: the symbolic expression for the memory.
boost::shared_ptr< class SymbolicMemory > SymbolicMemoryPtr
Shared-ownership pointer for symbolic memory state.
virtual MemoryStatePtr create(const SValuePtr &addrProtoval, const SValuePtr &valProtoval) const ROSE_OVERRIDE
Virtual allocating constructor.
Base classes for instruction semantics.
virtual MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual allocating copy constructor.
Base class for most instruction semantics RISC operators.
virtual SValuePtr readMemory(const SValuePtr &address, const SValuePtr &dflt, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE
Read a value from memory.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual bool merge(const BaseSemantics::MemoryStatePtr &other, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Merge memory states for data flow analysis.