ROSE  0.9.9.109
NullSemantics2.h
1 #ifndef Rose_NullSemantics2_H
2 #define Rose_NullSemantics2_H
3 
4 #include "BaseSemantics2.h"
5 
6 namespace Rose {
7 namespace BinaryAnalysis { // documented elsewhere
8 namespace InstructionSemantics2 { // documented elsewhere
9 
10 
15 namespace NullSemantics {
16 
18 // Semantic values
20 
23 
26 
28  // Real constructors.
29 protected:
30  explicit SValue(size_t nbits): BaseSemantics::SValue(nbits) {}
31 
33  // Static allocating constructors
34 public:
36  static SValuePtr instance() {
37  return SValuePtr(new SValue(1));
38  }
39 
41  static SValuePtr instance(size_t nbits) {
42  return SValuePtr(new SValue(nbits));
43  }
44 
46  static SValuePtr instance(size_t nbits, uint64_t number) {
47  return SValuePtr(new SValue(nbits)); // the number is not important in this domain
48  }
49 
51  static SValuePtr instance(const SValuePtr &other) {
52  return SValuePtr(new SValue(*other));
53  }
54 
56  // Virtual constructors
57 public:
58  virtual BaseSemantics::SValuePtr bottom_(size_t nBits) const ROSE_OVERRIDE {
59  return instance(nBits);
60  }
61  virtual BaseSemantics::SValuePtr undefined_(size_t nBits) const ROSE_OVERRIDE {
62  return instance(nBits);
63  }
64  virtual BaseSemantics::SValuePtr unspecified_(size_t nBits) const ROSE_OVERRIDE {
65  return instance(nBits);
66  }
67  virtual BaseSemantics::SValuePtr number_(size_t nBits, uint64_t number) const ROSE_OVERRIDE {
68  return instance(nBits, number);
69  }
70  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
71  SValuePtr retval(new SValue(*this));
72  if (new_width!=0 && new_width!=retval->get_width())
73  retval->set_width(new_width);
74  return retval;
75  }
78  SMTSolver*) const ROSE_OVERRIDE {
79  return Sawyer::Nothing();
80  }
81 
83  // Dynamic pointer casting
84 public:
86  static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
87  SValuePtr retval = v.dynamicCast<SValue>();
88  ASSERT_not_null(retval);
89  return retval;
90  }
91 
93  // Implementations of functions inherited
94 public:
95  virtual bool isBottom() const ROSE_OVERRIDE {
96  return false;
97  }
98 
99  virtual bool is_number() const ROSE_OVERRIDE {
100  return false;
101  }
102 
103  virtual uint64_t get_number() const ROSE_OVERRIDE {
104  ASSERT_not_reachable("not a number");
105  uint64_t retval;
106  return retval;
107  }
108 
109  virtual bool may_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE {
110  return true;
111  }
112 
113  virtual bool must_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE {
114  return this == getRawPointer(other); // must be equal if they're both the same object
115  }
116 
117  virtual void print(std::ostream &stream, BaseSemantics::Formatter&) const ROSE_OVERRIDE {
118  stream <<"VOID[" <<get_width() <<"]";
119  }
120 };
121 
122 
124 // Register state
126 
128 typedef boost::shared_ptr<class RegisterState> RegisterStatePtr;
129 
134 protected:
135  RegisterState(const RegisterState &other)
136  : BaseSemantics::RegisterState(other) {}
137 
139  : BaseSemantics::RegisterState(protoval, regdict) {}
140 
141 public:
142  static RegisterStatePtr instance(const BaseSemantics::SValuePtr &protoval, const RegisterDictionary *regdict) {
143  return RegisterStatePtr(new RegisterState(protoval, regdict));
144  }
145 
147  const RegisterDictionary *regdict) const ROSE_OVERRIDE {
148  return instance(protoval, regdict);
149  }
150 
151  virtual BaseSemantics::RegisterStatePtr clone() const ROSE_OVERRIDE {
152  return RegisterStatePtr(new RegisterState(*this));
153  }
154 
155  static RegisterStatePtr promote(const BaseSemantics::RegisterStatePtr &from) {
156  RegisterStatePtr retval = boost::dynamic_pointer_cast<RegisterState>(from);
157  ASSERT_not_null(retval);
158  return retval;
159  }
160 
161  virtual bool merge(const BaseSemantics::RegisterStatePtr &other_, BaseSemantics::RiscOperators*) ROSE_OVERRIDE {
162  return false;
163  }
164 
165  virtual void clear() ROSE_OVERRIDE {}
166  virtual void zero() ROSE_OVERRIDE {}
167 
170  BaseSemantics::RiscOperators *ops) ROSE_OVERRIDE {
171  return protoval()->undefined_(reg.get_nbits());
172  }
173 
175  BaseSemantics::RiscOperators *ops) ROSE_OVERRIDE {}
176 
177  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE {}
178 };
179 
180 
182 // Memory state
184 
186 typedef boost::shared_ptr<class MemoryState> MemoryStatePtr;
187 
192 protected:
193  MemoryState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
194  : BaseSemantics::MemoryState(addrProtoval, valProtoval) {}
195 
196  MemoryState(const MemoryStatePtr &other)
197  : BaseSemantics::MemoryState(other) {}
198 
199 public:
200  static MemoryStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) {
201  return MemoryStatePtr(new MemoryState(addrProtoval, valProtoval));
202  }
203 
204 public:
206  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
207  return instance(addrProtoval, valProtoval);
208  }
209 
210  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
211  return MemoryStatePtr(new MemoryState(*this));
212  }
213 
214 public:
215  static MemoryStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
216  MemoryStatePtr retval = boost::dynamic_pointer_cast<MemoryState>(x);
217  ASSERT_not_null(x);
218  return retval;
219  }
220 
221 public:
222  virtual void clear() ROSE_OVERRIDE {}
223 
226  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE {
227  return dflt->copy();
228  }
229 
230  virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
231  BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE {}
232 
233  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE {}
234 
236  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE {
237  return false;
238  }
239 };
240 
241 
243 // Complete state
245 
246 typedef BaseSemantics::State State;
247 typedef BaseSemantics::StatePtr StatePtr;
248 
249 
251 // RISC operators
253 
255 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
256 
259 
261  // Real constructors
262 protected:
264  : BaseSemantics::RiscOperators(protoval, solver) {
265  name("Null");
266  }
267  explicit RiscOperators(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL)
269  name("Null");
270  }
271 
273  // Static allocating constructors
274 public:
277  static RiscOperatorsPtr instance(const RegisterDictionary *regdict);
278 
280  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL) {
281  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
282  }
283 
285  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL) {
286  return RiscOperatorsPtr(new RiscOperators(state, solver));
287  }
288 
290  // Virtual constructors
291 public:
293  SMTSolver *solver=NULL) const ROSE_OVERRIDE {
294  return instance(protoval, solver);
295  }
296 
298  SMTSolver *solver=NULL) const ROSE_OVERRIDE {
299  return instance(state, solver);
300  }
301 
303  // Risc operators inherited
304 public:
306  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
307 
309  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
310 
312  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
313 
314  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
315 
317  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
318 
320  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
321 
323 
325 
327  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
328 
330  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
331 
333  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
334 
336  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
337 
339  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
340 
341  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
342 
344  const BaseSemantics::SValuePtr &a_,
345  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
346 
347  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
348 
350  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
351 
353  const BaseSemantics::SValuePtr &b_,
354  const BaseSemantics::SValuePtr &c_,
355  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
356 
357  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
358 
360  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
361 
363  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
364 
366  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
367 
369  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
370 
372  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
373 
375  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
376 
378  const BaseSemantics::SValuePtr &addr,
379  const BaseSemantics::SValuePtr &dflt,
380  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
381 
382  virtual void writeMemory(RegisterDescriptor segreg,
383  const BaseSemantics::SValuePtr &addr,
384  const BaseSemantics::SValuePtr &data,
385  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
386 };
387 
388 } // namespace
389 } // namespace
390 } // namespace
391 } // namespace
392 
393 #endif
virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE
Create a new value from an existing value, changing the width if new_width is non-zero.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Adds two integers of equal size.
virtual uint64_t get_number() const ROSE_OVERRIDE
Return the concrete number for this value.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print the register contents.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL)
Static allocating constructor.
virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted right arithmetically (with sign bit).
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise AND of two values.
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Concatenates the bits of two values.
virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *ops) ROSE_OVERRIDE
Read a value from a register.
virtual BaseSemantics::SValuePtr undefined_(size_t nBits) const ROSE_OVERRIDE
Create a new undefined semantic value.
virtual bool is_number() const ROSE_OVERRIDE
Determines if the value is a concrete number.
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) ROSE_OVERRIDE
Extracts bits from a value.
static SValuePtr instance()
Instantiate a new prototypical values.
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with signed values.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to null RISC operations.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Returns position of least significant set bit; zero when no bits are set.
Holds a value or nothing.
Definition: Optional.h:49
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Returns position of most significant set bit; zero when no bits are set.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the right.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to null register state.
Main namespace for the ROSE library.
virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
If-then-else.
static RiscOperatorsPtr instance(const RegisterDictionary *regdict)
Instantiate a new RiscOperators object and configures it to use semantic values and states that are d...
Describes (part of) a physical CPU register.
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Two's complement.
virtual BaseSemantics::RegisterStatePtr clone() const ROSE_OVERRIDE
Make a copy of this register state.
virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, const BaseSemantics::SValuePtr &c_, BaseSemantics::SValuePtr &carry_out) ROSE_OVERRIDE
Add two values of equal size and a carry bit.
virtual BaseSemantics::RegisterStatePtr create(const BaseSemantics::SValuePtr &protoval, const RegisterDictionary *regdict) const ROSE_OVERRIDE
Virtual constructor.
boost::shared_ptr< class RegisterState > RegisterStatePtr
Shared-ownership pointer to null register state.
static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL)
Constructor.
virtual void writeMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE
Writes a value to memory.
boost::shared_ptr< class RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
boost::shared_ptr< class State > StatePtr
Shared-ownership pointer to a semantic state.
virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Read a value from memory.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiply two unsigned values.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE
Sign extends a value.
virtual BaseSemantics::SValuePtr unspecified_(size_t nBits) const ROSE_OVERRIDE
Create a new unspecified semantic value.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual bool merge(const BaseSemantics::RegisterStatePtr &other_, BaseSemantics::RiscOperators *) ROSE_OVERRIDE
Merge register states for data flow analysis.
NullSemantics operators always return a new undefined value.
static SValuePtr instance(size_t nbits)
Instantiate a new undefined value.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiplies two signed values.
virtual void zero() ROSE_OVERRIDE
Set all registers to the zero.
virtual void print(std::ostream &stream, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print a value to a stream using default format.
virtual bool merge(const BaseSemantics::MemoryStatePtr &other, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Merge memory states for data flow analysis.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print a memory state to more than one line of output.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise XOR of two values.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two unsigned values.
Defines registers available for a particular architecture.
Definition: Registers.h:32
virtual BaseSemantics::SValuePtr number_(size_t nBits, uint64_t number) const ROSE_OVERRIDE
Create a new concrete semantic value.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
const RegisterDictionary * regdict
Registers that are able to be stored by this state.
virtual Sawyer::Optional< BaseSemantics::SValuePtr > createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr &, SMTSolver *) const ROSE_OVERRIDE
Possibly create a new value by merging two existing values.
static SValuePtr instance(size_t nbits, uint64_t number)
Instantiate a new concrete value.
virtual void clear() ROSE_OVERRIDE
Removes stored values from the register state.
static SValuePtr instance(const SValuePtr &other)
Instantiate a new copy of an existing value.
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
One's complement.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Returns true if two values must be equal.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted right logically (no sign bit).
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with unsigned values.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted left.
virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual allocating copy constructor.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Returns true if two values could be equal.
virtual size_t get_width() const
Accessor for value width.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two signed values.
virtual bool isBottom() const ROSE_OVERRIDE
Determines whether a value is a data-flow bottom.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer to a null semantic value.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the left.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a NullSemantics value.
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Write a value to memory.
Represents no value.
Definition: Optional.h:32
virtual SMTSolver * solver() const
Property: Satisfiability module theory (SMT) solver.
virtual const std::string & name() const
Property: Name used for debugging.
virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE
Reads a value from memory.
virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *ops) ROSE_OVERRIDE
Write a value to a register.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SMTSolver.h:19
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise OR of two values.
virtual BaseSemantics::SValuePtr bottom_(size_t nBits) const ROSE_OVERRIDE
Data-flow bottom value.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Determines whether a value is equal to zero.