ROSE  0.11.51.0
PartialSymbolicSemantics.h
1 #ifndef ROSE_BinaryAnalysis_InstructionSemantics2_PartialSymbolicSemantics_H
2 #define ROSE_BinaryAnalysis_InstructionSemantics2_PartialSymbolicSemantics_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #ifndef __STDC_FORMAT_MACROS
7 #define __STDC_FORMAT_MACROS
8 #endif
9 #include <inttypes.h>
10 
11 #include <map>
12 #include <stdint.h>
13 #include <vector>
14 
15 #include "rosePublicConfig.h"
16 #ifdef ROSE_HAVE_LIBGCRYPT
17 #include <gcrypt.h>
18 #endif
19 
20 #include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics.h>
21 #include "integerOps.h"
22 #include <Rose/BinaryAnalysis/MemoryMap.h>
23 #include <Rose/FormatRestorer.h>
24 
25 namespace Rose {
26 namespace BinaryAnalysis { // documented elsewhere
27 namespace InstructionSemantics2 { // documented elsewhere
28 
42 namespace PartialSymbolicSemantics {
43 
45 // Print formatter
47 
51 protected:
52  typedef std::map<uint64_t, uint64_t> Map;
53  Map renames;
54  size_t next_name;
55 public:
56  Formatter(): next_name(1) {}
57  uint64_t rename(uint64_t orig_name);
58 };
59 
60 
62 // Semantic values
64 
67 
71 public:
74 
76  using Ptr = SValuePtr;
77 
78 public:
79  uint64_t name;
80  uint64_t offset;
81  bool negate;
83  // Real constructors
85 protected:
86  explicit SValue(size_t nbits)
87  : BaseSemantics::SValue(nbits), name(nextName()), offset(0), negate(false) {}
88 
89  SValue(size_t nbits, uint64_t number)
90  : BaseSemantics::SValue(nbits), name(0), offset(number), negate(false) {
91  if (nbits <= 64) {
92  this->offset &= IntegerOps::genMask<uint64_t>(nbits);
93  } else {
94  name = nextName();
95  offset = 0;
96  }
97  }
98 
99  SValue(size_t nbits, uint64_t name, uint64_t offset, bool negate)
100  : BaseSemantics::SValue(nbits), name(name), offset(offset), negate(negate) {
101  this->offset &= IntegerOps::genMask<uint64_t>(nbits);
102  ASSERT_require(nbits <= 64 || name != 0);
103  }
104 
105 public:
111  static uint64_t nextName();
112 
114  // Static allocating constructors
115 public:
117  static SValuePtr instance() {
118  return SValuePtr(new SValue(1));
119  }
120 
122  static SValuePtr instance(size_t nbits) {
123  return SValuePtr(new SValue(nbits));
124  }
125 
127  static SValuePtr instance(size_t nbits, uint64_t value) {
128  return SValuePtr(new SValue(nbits, value));
129  }
130 
132  static SValuePtr instance(size_t nbits, uint64_t name, uint64_t offset, bool negate) {
133  return SValuePtr(new SValue(nbits, name, offset, negate));
134  }
135 
137  // Virtual constructors
138 public:
139  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE {
140  return instance(nbits);
141  }
142  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE {
143  return instance(nbits);
144  }
145  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE {
146  return instance(nbits);
147  }
148 
149  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE {
150  return instance(nbits, value);
151  }
152 
153  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
154  SValuePtr retval(new SValue(*this));
155  if (new_width!=0 && new_width!=retval->nBits())
156  retval->set_width(new_width);
157  return retval;
158  }
159 
162  const SmtSolverPtr&) const ROSE_OVERRIDE;
163 
165  virtual BaseSemantics::SValuePtr create(size_t nbits, uint64_t name, uint64_t offset, bool negate) const {
166  return instance(nbits, name, offset, negate);
167  }
168 
170  // Dynamic pointer casts
171 public:
174  static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
175  SValuePtr retval = v.dynamicCast<SValue>();
176  ASSERT_not_null(retval);
177  return retval;
178  }
179 
181  // Other stuff we inherited from the super class
182 public:
183  virtual void hash(Combinatorics::Hasher&) const override;
184  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
185 
186  virtual bool isBottom() const ROSE_OVERRIDE {
187  return false;
188  }
189 
191  // Override legacy members. These have similar non-virtual camelCase names in the base class, and eventually we'll remoe
192  // these snake_case names and change the camelCase names to be the virtual functions. Therefore, be sure to use "override"
193  // in your own code so you know when we make this change.
194 public:
195  // See nBits
196  virtual void set_width(size_t nbits) ROSE_OVERRIDE {
197  if (nbits > 64 && name == 0) {
198  *this = SValue(nbits);
199  } else {
200  ASSERT_require(nbits <= 64 || name != 0);
202  offset &= IntegerOps::genMask<uint64_t>(nbits);
203  }
204  }
205 
206  // See mayEqual
207  virtual bool may_equal(const BaseSemantics::SValuePtr &other,
208  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;
209 
210  // See mustEqual
211  virtual bool must_equal(const BaseSemantics::SValuePtr &other,
212  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;
213 
214  // See isConcrete
215  virtual bool is_number() const ROSE_OVERRIDE {
216  return 0==name;
217  }
218 
219  // See toUnsigned and toSigned.
220  virtual uint64_t get_number() const ROSE_OVERRIDE {
221  ASSERT_require(is_number());
222  return offset;
223  }
224 };
225 
226 
228 // Register state
230 
231 typedef BaseSemantics::RegisterStateGeneric RegisterState;
232 typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;
233 
234 
236 // Memory state
238 
239 // PartialSymbolicSemantics uses BaseSemantics::MemoryCellList (or subclass) as its memory state, and does not expect the
240 // MemoryCellList to be byte-restricted (i.e., the cells can store multi-byte values).
241 
242 typedef BaseSemantics::MemoryCellList MemoryState;
243 typedef BaseSemantics::MemoryCellListPtr MemoryStatePtr;
244 
245 
247 // Complete state
249 
251 typedef boost::shared_ptr<class State> StatePtr;
252 
256 public:
259 
261  using Ptr = StatePtr;
262 
264  // Real constructors
265 protected:
266  State(const BaseSemantics::RegisterStatePtr &registers,
267  const BaseSemantics::MemoryStatePtr &memory)
268  : BaseSemantics::State(registers, memory) {
269  // This state should use PartialSymbolicSemantics values (or subclasses thereof)
270  ASSERT_not_null(registers);
271  (void) SValue::promote(registers->protoval());
272  ASSERT_not_null(memory);
273  (void) SValue::promote(memory->get_addr_protoval());
274  (void) SValue::promote(memory->get_val_protoval());
275 
276  // This state should use a memory that is not byte restricted.
277  MemoryStatePtr mcl = MemoryState::promote(memory);
278  ASSERT_require(!mcl->byteRestricted());
279  }
280 
281  State(const State &other): BaseSemantics::State(other) {}
282 
284  // Static allocating constructors
285 public:
287  static StatePtr instance(const BaseSemantics::RegisterStatePtr &registers,
288  const BaseSemantics::MemoryStatePtr &memory) {
289  return StatePtr(new State(registers, memory));
290  }
291 
293  static StatePtr instance(const StatePtr &other) {
294  return StatePtr(new State(*other));
295  }
296 
298  // Virtual constructors
299 public:
301  const BaseSemantics::MemoryStatePtr &memory) const ROSE_OVERRIDE {
302  return instance(registers, memory);
303  }
304 
305  virtual BaseSemantics::StatePtr clone() const ROSE_OVERRIDE {
306  StatePtr self = promote(boost::const_pointer_cast<BaseSemantics::State>(shared_from_this()));
307  return instance(self);
308  }
309 
311  // Dynamic pointer casts
312 public:
313  static StatePtr promote(const BaseSemantics::StatePtr &x) {
314  StatePtr retval = boost::dynamic_pointer_cast<State>(x);
315  ASSERT_not_null(x);
316  return retval;
317  }
318 
320  // Methods first declared at this level of the class hierarchy
321 public:
324  virtual void print_diff_registers(std::ostream&, const StatePtr &other_state, Formatter&) const;
325 
327  virtual bool equal_registers(const StatePtr &other) const;
328 
331  virtual void discard_popped_memory();
332 };
333 
334 
336 // RISC operators
338 
340 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
341 
344 public:
347 
350 
351 protected:
352  MemoryMap::Ptr map;
353 
355  // Real constructors
356 protected:
358  : BaseSemantics::RiscOperators(protoval, solver) {
359  name("PartialSymbolic");
360  }
361  explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr())
362  : BaseSemantics::RiscOperators(state, solver) {
363  name("PartialSymbolic");
364  }
365 
367  // Static allocating constructors
368 public:
371  static RiscOperatorsPtr instance(const RegisterDictionary *regdict);
372 
374  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr()) {
375  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
376  }
377 
379  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr()) {
380  return RiscOperatorsPtr(new RiscOperators(state, solver));
381  }
382 
384  // Virtual constructors
385 public:
387  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
388  return instance(protoval, solver);
389  }
390 
392  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
393  return instance(state, solver);
394  }
395 
397  // Dynamic pointer casts
398 public:
401  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
402  RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
403  ASSERT_not_null(retval);
404  return retval;
405  }
406 
408  // Methods first declared at this level of the class hierarchy
409 public:
414  const MemoryMap::Ptr get_memory_map() const { return map; }
415  void set_memory_map(const MemoryMap::Ptr &m) { map = m; }
418  // Risc operators inherited
420 public:
421  virtual void interrupt(int majr, int minr) ROSE_OVERRIDE;
423  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
425  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
427  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
428  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
430  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
432  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
436  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
438  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
440  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
442  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
444  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
445  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
447  const BaseSemantics::SValuePtr &a_,
448  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
449  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
451  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
453  const BaseSemantics::SValuePtr &b_,
454  const BaseSemantics::SValuePtr &c_,
455  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
456  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
458  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
460  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
462  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
464  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
466  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
468  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
470  const BaseSemantics::SValuePtr &addr,
471  const BaseSemantics::SValuePtr &dflt,
472  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
474  const BaseSemantics::SValuePtr &addr,
475  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
476  virtual void writeMemory(RegisterDescriptor segreg,
477  const BaseSemantics::SValuePtr &addr,
478  const BaseSemantics::SValuePtr &data,
479  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
480 
481 protected:
482  BaseSemantics::SValuePtr readOrPeekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &address,
483  const BaseSemantics::SValuePtr &dflt_, bool allowSideEffects);
484 };
485 
486 } // namespace
487 } // namespace
488 } // namespace
489 } // namespace
490 
491 #endif
492 #endif
virtual BaseSemantics::StatePtr clone() const ROSE_OVERRIDE
Virtual copy constructor.
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with signed values.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise AND of two values.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE
Data-flow bottom value.
static RiscOperatorsPtr instance(const RegisterDictionary *regdict)
Instantiates a new RiscOperators object and configures it to use semantic values and states that are ...
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
virtual void set_width(size_t nbits)
Virtual API.
Definition: SValue.h:303
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two signed values.
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise OR of two values.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual API.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the right.
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Concatenates the bits of two values.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE
Create a new unspecified semantic value.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise XOR of two values.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE
Create a new undefined semantic value.
virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Returns position of least significant set bit; zero when no bits are set.
virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
Read memory without side effects.
virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
If-then-else.
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.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer to a partial-symbolic semantic value.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted left.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiplies two signed values.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
Main namespace for the ROSE library.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Adds two integers of equal size.
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) ROSE_OVERRIDE
Extracts bits from a value.
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
One's complement.
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.
uint64_t name
Zero for constants; non-zero ID number for everything else.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Determines whether a value is equal to zero.
virtual BaseSemantics::SValuePtr create(size_t nbits, uint64_t name, uint64_t offset, bool negate) const
Virtual allocating constructor.
static SValuePtr instance(size_t nbits)
Instantiate a new undefined value of specified width.
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Two's complement.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiply two unsigned values.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with unsigned values.
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.
bool negate
Switch between name+offset and (-name)+offset; should be false for constants.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE
Sign extends a value.
Type of values manipulated by the PartialSymbolicSemantics domain.
virtual void interrupt(int majr, int minr) ROSE_OVERRIDE
Invoked for instructions that cause an interrupt.
boost::shared_ptr< class MemoryCellList > MemoryCellListPtr
Shared-ownership pointer to a list-based memory state.
Base classes for instruction semantics.
Definition: Dispatcher.h:18
void set_memory_map(const MemoryMap::Ptr &m)
A memory map can be used to provide default values for memory cells that are read before being writte...
static StatePtr instance(const BaseSemantics::RegisterStatePtr &registers, const BaseSemantics::MemoryStatePtr &memory)
Instantiates a new instance of memory state with specified register and memory states.
Describes (part of) a physical CPU register.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the left.
Base class for semantics machine states.
Definition: State.h:39
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x)
Run-time promotion of a base RiscOperators pointer to partial symbolic operators. ...
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 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::StatePtr create(const BaseSemantics::RegisterStatePtr &registers, const BaseSemantics::MemoryStatePtr &memory) const ROSE_OVERRIDE
Virtual 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::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual allocating constructor.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
Definition: RiscOperators.h:48
const MemoryMap::Ptr get_memory_map() const
A memory map can be used to provide default values for memory cells that are read before being writte...
virtual bool isBottom() const ROSE_OVERRIDE
Determines whether a value is a data-flow bottom.
static SValuePtr instance(size_t nbits, uint64_t name, uint64_t offset, bool negate)
Insantiate a new value with all the necessary parts.
boost::shared_ptr< class State > StatePtr
Shared-ownership pointer to partial symbolic semantics state.
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 bool equal_registers(const StatePtr &other) const
Tests registers of two states for equality.
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted right logically (no sign bit).
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE
Create a new concrete semantic value.
static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators with specified state.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to partial symbolic semantics RISC operations.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual API.
static MemoryCellListPtr promote(const BaseSemantics::MemoryStatePtr &m)
Promote a base memory state pointer to a BaseSemantics::MemoryCellList pointer.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two unsigned values.
virtual void print_diff_registers(std::ostream &, const StatePtr &other_state, Formatter &) const
Print info about how registers differ.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified prototypical values.
Defines registers available for a particular architecture.
Definition: Registers.h:37
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
virtual const std::string & name() const
Property: Name used for debugging.
static StatePtr instance(const StatePtr &other)
Instantiates a new copy of an existing state.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print a value to a stream using default format.
virtual void discard_popped_memory()
Removes from memory those values at addresses below the current stack pointer.
static SValuePtr instance(size_t nbits, uint64_t value)
Instantiate a new concrete value.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:25
static uint64_t nextName()
Returns the next available name.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a PartialSymbolicSemantics value.