ROSE  0.11.2.0
NullSemantics2.h
1 #ifndef Rose_NullSemantics2_H
2 #define Rose_NullSemantics2_H
3 #include <rosePublicConfig.h>
4 #ifdef ROSE_BUILD_BINARY_ANALYSIS_SUPPORT
5 
6 #include "BaseSemantics2.h"
7 
8 namespace Rose {
9 namespace BinaryAnalysis { // documented elsewhere
10 namespace InstructionSemantics2 { // documented elsewhere
11 
12 
17 namespace NullSemantics {
18 
20 // Semantic values
22 
25 
28 
30  // Real constructors.
31 protected:
32  explicit SValue(size_t nbits): BaseSemantics::SValue(nbits) {}
33 
35  // Static allocating constructors
36 public:
38  static SValuePtr instance() {
39  return SValuePtr(new SValue(1));
40  }
41 
43  static SValuePtr instance(size_t nbits) {
44  return SValuePtr(new SValue(nbits));
45  }
46 
48  static SValuePtr instance(size_t nbits, uint64_t number) {
49  return SValuePtr(new SValue(nbits)); // the number is not important in this domain
50  }
51 
53  static SValuePtr instance(const SValuePtr &other) {
54  return SValuePtr(new SValue(*other));
55  }
56 
58  // Virtual constructors
59 public:
60  virtual BaseSemantics::SValuePtr bottom_(size_t nBits) const ROSE_OVERRIDE {
61  return instance(nBits);
62  }
63  virtual BaseSemantics::SValuePtr undefined_(size_t nBits) const ROSE_OVERRIDE {
64  return instance(nBits);
65  }
66  virtual BaseSemantics::SValuePtr unspecified_(size_t nBits) const ROSE_OVERRIDE {
67  return instance(nBits);
68  }
69  virtual BaseSemantics::SValuePtr number_(size_t nBits, uint64_t number) const ROSE_OVERRIDE {
70  return instance(nBits, number);
71  }
72  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
73  SValuePtr retval(new SValue(*this));
74  if (new_width!=0 && new_width!=retval->get_width())
75  retval->set_width(new_width);
76  return retval;
77  }
80  const SmtSolverPtr&) const ROSE_OVERRIDE {
81  return Sawyer::Nothing();
82  }
83 
85  // Dynamic pointer casting
86 public:
88  static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
89  SValuePtr retval = v.dynamicCast<SValue>();
90  ASSERT_not_null(retval);
91  return retval;
92  }
93 
95  // Implementations of functions inherited
96 public:
97  virtual bool isBottom() const ROSE_OVERRIDE {
98  return false;
99  }
100 
101  virtual bool is_number() const ROSE_OVERRIDE {
102  return false;
103  }
104 
105  virtual uint64_t get_number() const ROSE_OVERRIDE {
106  ASSERT_not_reachable("not a number");
107  uint64_t retval;
108  return retval;
109  }
110 
111  virtual bool may_equal(const BaseSemantics::SValuePtr &other,
112  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
113  return true;
114  }
115 
116  virtual bool must_equal(const BaseSemantics::SValuePtr &other,
117  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
118  return this == getRawPointer(other); // must be equal if they're both the same object
119  }
120 
121  virtual void print(std::ostream &stream, BaseSemantics::Formatter&) const ROSE_OVERRIDE {
122  stream <<"VOID[" <<get_width() <<"]";
123  }
124 };
125 
126 
128 // Register state
130 
132 typedef boost::shared_ptr<class RegisterState> RegisterStatePtr;
133 
137 class RegisterState: public BaseSemantics::RegisterState {
138 protected:
139  RegisterState(const RegisterState &other)
140  : BaseSemantics::RegisterState(other) {}
141 
142  RegisterState(const BaseSemantics::SValuePtr &protoval, const RegisterDictionary *regdict)
143  : BaseSemantics::RegisterState(protoval, regdict) {}
144 
145 public:
146  static RegisterStatePtr instance(const BaseSemantics::SValuePtr &protoval, const RegisterDictionary *regdict) {
147  return RegisterStatePtr(new RegisterState(protoval, regdict));
148  }
149 
150  virtual BaseSemantics::RegisterStatePtr create(const BaseSemantics::SValuePtr &protoval,
151  const RegisterDictionary *regdict) const ROSE_OVERRIDE {
152  return instance(protoval, regdict);
153  }
154 
155  virtual BaseSemantics::RegisterStatePtr clone() const ROSE_OVERRIDE {
156  return RegisterStatePtr(new RegisterState(*this));
157  }
158 
159  static RegisterStatePtr promote(const BaseSemantics::RegisterStatePtr &from) {
160  RegisterStatePtr retval = boost::dynamic_pointer_cast<RegisterState>(from);
161  ASSERT_not_null(retval);
162  return retval;
163  }
164 
165  virtual bool merge(const BaseSemantics::RegisterStatePtr &other_, BaseSemantics::RiscOperators*) ROSE_OVERRIDE {
166  return false;
167  }
168 
169  virtual void clear() ROSE_OVERRIDE {}
170  virtual void zero() ROSE_OVERRIDE {}
171 
173  readRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt,
174  BaseSemantics::RiscOperators *ops) ROSE_OVERRIDE {
175  return protoval()->undefined_(reg.nBits());
176  }
177 
179  peekRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt,
180  BaseSemantics::RiscOperators *ops) ROSE_OVERRIDE {
181  return protoval()->undefined_(reg.nBits());
182  }
183 
184  virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &value,
185  BaseSemantics::RiscOperators *ops) ROSE_OVERRIDE {}
186 
187  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE {}
188 };
189 
190 
192 // Memory state
194 
196 typedef boost::shared_ptr<class MemoryState> MemoryStatePtr;
197 
201 class MemoryState: public BaseSemantics::MemoryState {
202 protected:
203  MemoryState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
204  : BaseSemantics::MemoryState(addrProtoval, valProtoval) {}
205 
206  MemoryState(const MemoryStatePtr &other)
207  : BaseSemantics::MemoryState(other) {}
208 
209 public:
210  static MemoryStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) {
211  return MemoryStatePtr(new MemoryState(addrProtoval, valProtoval));
212  }
213 
214 public:
215  virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval,
216  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
217  return instance(addrProtoval, valProtoval);
218  }
219 
220  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
221  return MemoryStatePtr(new MemoryState(*this));
222  }
223 
224 public:
225  static MemoryStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
226  MemoryStatePtr retval = boost::dynamic_pointer_cast<MemoryState>(x);
227  ASSERT_not_null(x);
228  return retval;
229  }
230 
231 public:
232  virtual void clear() ROSE_OVERRIDE {}
233 
234  virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
236  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE {
237  return dflt->copy();
238  }
239 
240  virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
241  BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE {}
242 
243  virtual BaseSemantics::SValuePtr peekMemory(const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
245  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE {
246  return dflt->copy();
247  }
248 
249  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE {}
250 
251  virtual bool merge(const BaseSemantics::MemoryStatePtr &other, BaseSemantics::RiscOperators *addrOps,
252  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE {
253  return false;
254  }
255 };
256 
257 
259 // Complete state
261 
262 typedef BaseSemantics::State State;
263 typedef BaseSemantics::StatePtr StatePtr;
264 
265 
267 // RISC operators
269 
271 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
272 
275 
277  // Real constructors
278 protected:
280  : BaseSemantics::RiscOperators(protoval, solver) {
281  name("Null");
282  }
283  explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr())
285  name("Null");
286  }
287 
289  // Static allocating constructors
290 public:
293  static RiscOperatorsPtr instance(const RegisterDictionary *regdict);
294 
296  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr()) {
297  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
298  }
299 
301  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr()) {
302  return RiscOperatorsPtr(new RiscOperators(state, solver));
303  }
304 
306  // Virtual constructors
307 public:
309  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
310  return instance(protoval, solver);
311  }
312 
314  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
315  return instance(state, solver);
316  }
317 
319  // Risc operators inherited
320 public:
321  virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
322  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
323 
325  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
326 
327  virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
328  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
329 
330  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
331 
332  virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
333  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
334 
335  virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_,
336  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
337 
338  virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
339 
340  virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
341 
342  virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_,
343  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
344 
345  virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_,
346  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
347 
348  virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_,
349  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
350 
351  virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_,
352  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
353 
354  virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_,
355  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
356 
357  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
358 
359  virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
360  const BaseSemantics::SValuePtr &a_,
361  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
362 
363  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
364 
366  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
367 
369  const BaseSemantics::SValuePtr &b_,
370  const BaseSemantics::SValuePtr &c_,
371  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
372 
373  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
374 
376  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
377 
379  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
380 
382  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
383 
385  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
386 
388  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
389 
391  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
392 
394  const BaseSemantics::SValuePtr &addr,
395  const BaseSemantics::SValuePtr &dflt,
396  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
397 
399  const BaseSemantics::SValuePtr &addr,
400  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
401 
402  virtual void writeMemory(RegisterDescriptor segreg,
403  const BaseSemantics::SValuePtr &addr,
404  const BaseSemantics::SValuePtr &data,
405  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
406 };
407 
408 } // namespace
409 } // namespace
410 } // namespace
411 } // namespace
412 
413 #endif
414 #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.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual uint64_t get_number() const ROSE_OVERRIDE
Return the concrete number for this value.
virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
Read memory without side effects.
static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr())
Constructor.
size_t nBits() const
Property: Size in bits.
virtual BaseSemantics::SValuePtr undefined_(size_t nBits) const ROSE_OVERRIDE
Create a new undefined semantic value.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual bool is_number() const ROSE_OVERRIDE
Determines if the value is a concrete number.
virtual Sawyer::Optional< BaseSemantics::SValuePtr > createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const ROSE_OVERRIDE
Possibly create a new value by merging two existing values.
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.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
Holds a value or nothing.
Definition: Optional.h:49
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.
static RiscOperatorsPtr instance(const RegisterDictionary *regdict)
Instantiate a new RiscOperators object and configures it to use semantic values and states that are d...
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Two's complement.
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, const BaseSemantics::SValuePtr &c_, BaseSemantics::SValuePtr &carry_out) ROSE_OVERRIDE
Used for printing RISC operators with formatting.
boost::shared_ptr< class RegisterState > RegisterStatePtr
Shared-ownership pointer to null register state.
Sawyer::SharedPointer< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
virtual void writeMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE
Writes a value to memory.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiply two unsigned values.
virtual BaseSemantics::SValuePtr unspecified_(size_t nBits) const ROSE_OVERRIDE
Create a new unspecified semantic value.
Describes (part of) a physical CPU register.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Returns true if two values could be equal.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Static allocating constructor.
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 bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Returns true if two values must be equal.
virtual void print(std::ostream &stream, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print a value to a stream using default format.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two unsigned values.
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.
static SValuePtr instance(size_t nbits, uint64_t number)
Instantiate a new concrete value.
static SValuePtr instance(const SValuePtr &other)
Instantiate a new copy of an existing value.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with unsigned values.
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.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a NullSemantics value.
Defines registers available for a particular architecture.
Definition: Registers.h:38
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
Represents no value.
Definition: Optional.h:32
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.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
virtual BaseSemantics::SValuePtr bottom_(size_t nBits) const ROSE_OVERRIDE
Data-flow bottom value.