ROSE  0.11.51.0
BaseSemantics/SymbolicMemory.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 #ifndef ROSE_BinaryAnalysis_InstructionSemantics2_BaseSemantics_SymbolicMemory_H
4 #define ROSE_BinaryAnalysis_InstructionSemantics2_BaseSemantics_SymbolicMemory_H
5 #include <featureTests.h>
6 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
7 
8 #include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics/MemoryState.h>
9 #include <Rose/BinaryAnalysis/SymbolicExpr.h>
10 
11 namespace Rose {
12 namespace BinaryAnalysis {
13 namespace InstructionSemantics2 {
14 namespace BaseSemantics {
15 
17 typedef boost::shared_ptr<class SymbolicMemory> SymbolicMemoryPtr;
18 
24 class SymbolicMemory: public MemoryState {
25 public:
27  using Super = MemoryState;
28 
31 
32 private:
33  SymbolicExpr::Ptr mem_;
34 
35 protected:
36  // All memory states should be heap allocated; use instance(), create(), or clone() instead.
37  explicit SymbolicMemory(const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
38  : MemoryState(addrProtoval, valProtoval) {
39  // Initially assume that addresses are 32 bits wide and values are 8 bits wide. We can change this on the first access.
41  }
42 
43 public:
45  static SymbolicMemoryPtr instance(const SValuePtr &addrProtoval, const SValuePtr &valProtoval) {
46  return SymbolicMemoryPtr(new SymbolicMemory(addrProtoval, valProtoval));
47  }
48 
49 public:
50  // documented in base class
51  virtual MemoryStatePtr create(const SValuePtr &addrProtoval, const SValuePtr &valProtoval) const ROSE_OVERRIDE {
52  return instance(addrProtoval, valProtoval);
53  }
54 
55  // documented in base class
56  virtual MemoryStatePtr clone() const ROSE_OVERRIDE {
57  return SymbolicMemoryPtr(new SymbolicMemory(*this));
58  }
59 
63  static SymbolicMemoryPtr promote(const MemoryStatePtr &x) {
64  SymbolicMemoryPtr retval = boost::dynamic_pointer_cast<SymbolicMemory>(x);
65  ASSERT_not_null(retval);
66  return retval;
67  }
68 
69 public:
73  SymbolicExpr::Ptr expression() const { return mem_; }
74  void expression(const SymbolicExpr::Ptr &mem);
77 public:
78  virtual bool merge(const MemoryStatePtr &other, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;
79 
80  virtual void clear() ROSE_OVERRIDE;
81 
82  virtual SValuePtr readMemory(const SValuePtr &address, const SValuePtr &dflt,
83  RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;
84 
85  virtual void writeMemory(const SValuePtr &address, const SValuePtr &value,
86  RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;
87 
88  virtual SValuePtr peekMemory(const SValuePtr &address, const SValuePtr &dflt,
89  RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;
90 
91 public:
92  virtual void hash(Combinatorics::Hasher&, RiscOperators *addrOps, RiscOperators *valOps) const override;
93 
94  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
95 };
96 
97 } // namespace
98 } // namespace
99 } // namespace
100 } // namespace
101 
102 #endif
103 #endif
virtual void hash(Combinatorics::Hasher &, RiscOperators *addrOps, RiscOperators *valOps) const override
Calculate a hash for this memory state.
virtual void print(std::ostream &, Formatter &) const ROSE_OVERRIDE
Print a memory state to more than one line of output.
virtual bool merge(const MemoryStatePtr &other, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE
Merge memory states for data flow analysis.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
static SymbolicMemoryPtr instance(const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
Instantiate a new empty memory state on the heap.
MemoryStatePtr Ptr
Shared-ownership pointer for a MemoryState.
Definition: MemoryState.h:28
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.
virtual SValuePtr peekMemory(const SValuePtr &address, const SValuePtr &dflt, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE
Read a value from memory without side effects.
Base classes for instruction semantics.
Definition: Dispatcher.h:18
virtual MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual allocating copy constructor.
Base class for most instruction semantics RISC operators.
Definition: RiscOperators.h:48
virtual SValuePtr readMemory(const SValuePtr &address, const SValuePtr &dflt, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE
Read a value from memory.
LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Leaf constructor.