ROSE  0.9.10.44
PartialSymbolicSemantics2.h
1 #ifndef Rose_PartialSymbolicSemantics2_H
2 #define Rose_PartialSymbolicSemantics2_H
3 
4 
5 #ifndef __STDC_FORMAT_MACROS
6 #define __STDC_FORMAT_MACROS
7 #endif
8 #include <inttypes.h>
9 
10 #include <map>
11 #include <stdint.h>
12 #include <vector>
13 
14 #include "rosePublicConfig.h"
15 #ifdef ROSE_HAVE_LIBGCRYPT
16 #include <gcrypt.h>
17 #endif
18 
19 #include "BaseSemantics2.h"
20 #include "integerOps.h"
21 #include "MemoryMap.h"
22 #include "FormatRestorer.h"
23 #include "RegisterStateGeneric.h"
24 #include "MemoryCellList.h"
25 
26 namespace Rose {
27 namespace BinaryAnalysis { // documented elsewhere
28 namespace InstructionSemantics2 { // documented elsewhere
29 
43 namespace PartialSymbolicSemantics {
44 
45 extern uint64_t name_counter;
46 
48 // Print formatter
50 
54 protected:
55  typedef std::map<uint64_t, uint64_t> Map;
56  Map renames;
57  size_t next_name;
58 public:
59  Formatter(): next_name(1) {}
60  uint64_t rename(uint64_t orig_name);
61 };
62 
63 
65 // Semantic values
67 
70 
74 public:
75  uint64_t name;
76  uint64_t offset;
77  bool negate;
79  // Real constructors
81 protected:
82  explicit SValue(size_t nbits)
83  : BaseSemantics::SValue(nbits), name(++name_counter), offset(0), negate(false) {}
84 
85  SValue(size_t nbits, uint64_t number)
86  : BaseSemantics::SValue(nbits), name(0), offset(number), negate(false) {
87  if (nbits <= 64) {
88  this->offset &= IntegerOps::genMask<uint64_t>(nbits);
89  } else {
90  name = ++name_counter;
91  offset = 0;
92  }
93  }
94 
95  SValue(size_t nbits, uint64_t name, uint64_t offset, bool negate)
96  : BaseSemantics::SValue(nbits), name(name), offset(offset), negate(negate) {
97  this->offset &= IntegerOps::genMask<uint64_t>(nbits);
98  }
99 
101  // Static allocating constructors
102 public:
104  static SValuePtr instance() {
105  return SValuePtr(new SValue(1));
106  }
107 
109  static SValuePtr instance(size_t nbits) {
110  return SValuePtr(new SValue(nbits));
111  }
112 
114  static SValuePtr instance(size_t nbits, uint64_t value) {
115  return SValuePtr(new SValue(nbits, value));
116  }
117 
119  static SValuePtr instance(size_t nbits, uint64_t name, uint64_t offset, bool negate) {
120  return SValuePtr(new SValue(nbits, name, offset, negate));
121  }
122 
124  // Virtual constructors
125 public:
126  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE {
127  return instance(nbits);
128  }
129  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE {
130  return instance(nbits);
131  }
132  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE {
133  return instance(nbits);
134  }
135 
136  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE {
137  return instance(nbits, value);
138  }
139 
140  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
141  SValuePtr retval(new SValue(*this));
142  if (new_width!=0 && new_width!=retval->get_width())
143  retval->set_width(new_width);
144  return retval;
145  }
146 
149  const SmtSolverPtr&) const ROSE_OVERRIDE;
150 
152  virtual BaseSemantics::SValuePtr create(size_t nbits, uint64_t name, uint64_t offset, bool negate) const {
153  return instance(nbits, name, offset, negate);
154  }
155 
157  // Dynamic pointer casts
158 public:
161  static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
162  SValuePtr retval = v.dynamicCast<SValue>();
163  ASSERT_not_null(retval);
164  return retval;
165  }
166 
168  // Other stuff we inherited from the super class
169 public:
170  virtual void set_width(size_t nbits) ROSE_OVERRIDE {
172  offset &= IntegerOps::genMask<uint64_t>(nbits);
173  }
174 
175  virtual bool may_equal(const BaseSemantics::SValuePtr &other,
176  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;
177  virtual bool must_equal(const BaseSemantics::SValuePtr &other,
178  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;
179 
180  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
181 
182  virtual bool isBottom() const ROSE_OVERRIDE {
183  return false;
184  }
185 
186  virtual bool is_number() const ROSE_OVERRIDE {
187  return 0==name;
188  }
189 
190  virtual uint64_t get_number() const ROSE_OVERRIDE {
191  ASSERT_require(is_number());
192  return offset;
193  }
194 };
195 
196 
198 // Register state
200 
201 typedef BaseSemantics::RegisterStateGeneric RegisterState;
202 typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;
203 
204 
206 // Memory state
208 
209 // PartialSymbolicSemantics uses BaseSemantics::MemoryCellList (or subclass) as its memory state, and does not expect the
210 // MemoryCellList to be byte-restricted (i.e., the cells can store multi-byte values).
211 
212 typedef BaseSemantics::MemoryCellList MemoryState;
213 typedef BaseSemantics::MemoryCellListPtr MemoryStatePtr;
214 
215 
217 // Complete state
219 
221 typedef boost::shared_ptr<class State> StatePtr;
222 
226 
228  // Real constructors
229 protected:
230  State(const BaseSemantics::RegisterStatePtr &registers,
231  const BaseSemantics::MemoryStatePtr &memory)
232  : BaseSemantics::State(registers, memory) {
233  // This state should use PartialSymbolicSemantics values (or subclasses thereof)
234  ASSERT_not_null(registers);
235  (void) SValue::promote(registers->protoval());
236  ASSERT_not_null(memory);
237  (void) SValue::promote(memory->get_addr_protoval());
238  (void) SValue::promote(memory->get_val_protoval());
239 
240  // This state should use a memory that is not byte restricted.
241  MemoryStatePtr mcl = MemoryState::promote(memory);
242  ASSERT_require(!mcl->byteRestricted());
243  }
244 
245  State(const State &other): BaseSemantics::State(other) {}
246 
248  // Static allocating constructors
249 public:
251  static StatePtr instance(const BaseSemantics::RegisterStatePtr &registers,
252  const BaseSemantics::MemoryStatePtr &memory) {
253  return StatePtr(new State(registers, memory));
254  }
255 
257  static StatePtr instance(const StatePtr &other) {
258  return StatePtr(new State(*other));
259  }
260 
262  // Virtual constructors
263 public:
265  const BaseSemantics::MemoryStatePtr &memory) const ROSE_OVERRIDE {
266  return instance(registers, memory);
267  }
268 
269  virtual BaseSemantics::StatePtr clone() const ROSE_OVERRIDE {
270  StatePtr self = promote(boost::const_pointer_cast<BaseSemantics::State>(shared_from_this()));
271  return instance(self);
272  }
273 
275  // Dynamic pointer casts
276 public:
277  static StatePtr promote(const BaseSemantics::StatePtr &x) {
278  StatePtr retval = boost::dynamic_pointer_cast<State>(x);
279  ASSERT_not_null(x);
280  return retval;
281  }
282 
284  // Methods first declared at this level of the class hierarchy
285 public:
288  virtual void print_diff_registers(std::ostream&, const StatePtr &other_state, Formatter&) const;
289 
291  virtual bool equal_registers(const StatePtr &other) const;
292 
295  virtual void discard_popped_memory();
296 };
297 
298 
300 // RISC operators
302 
304 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
305 
308 protected:
309  MemoryMap::Ptr map;
310 
312  // Real constructors
313 protected:
315  : BaseSemantics::RiscOperators(protoval, solver) {
316  name("PartialSymbolic");
317  }
318  explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr())
320  name("PartialSymbolic");
321  }
322 
324  // Static allocating constructors
325 public:
328  static RiscOperatorsPtr instance(const RegisterDictionary *regdict);
329 
331  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr()) {
332  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
333  }
334 
336  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr()) {
337  return RiscOperatorsPtr(new RiscOperators(state, solver));
338  }
339 
341  // Virtual constructors
342 public:
344  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
345  return instance(protoval, solver);
346  }
347 
349  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
350  return instance(state, solver);
351  }
352 
354  // Dynamic pointer casts
355 public:
358  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
359  RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
360  ASSERT_not_null(retval);
361  return retval;
362  }
363 
365  // Methods first declared at this level of the class hierarchy
366 public:
371  const MemoryMap::Ptr get_memory_map() const { return map; }
372  void set_memory_map(const MemoryMap::Ptr &m) { map = m; }
375  // Risc operators inherited
377 public:
378  virtual void interrupt(int majr, int minr) ROSE_OVERRIDE;
380  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
382  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
384  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
385  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
387  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
389  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
393  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
395  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
397  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
399  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
401  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
402  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
404  const BaseSemantics::SValuePtr &a_,
405  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
406  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
408  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
410  const BaseSemantics::SValuePtr &b_,
411  const BaseSemantics::SValuePtr &c_,
412  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
413  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
415  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
417  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
419  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
421  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
423  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
425  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
427  const BaseSemantics::SValuePtr &addr,
428  const BaseSemantics::SValuePtr &dflt,
429  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
431  const BaseSemantics::SValuePtr &addr,
432  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
433  virtual void writeMemory(RegisterDescriptor segreg,
434  const BaseSemantics::SValuePtr &addr,
435  const BaseSemantics::SValuePtr &data,
436  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
437 
438 protected:
439  virtual BaseSemantics::SValuePtr readOrPeekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &address,
440  const BaseSemantics::SValuePtr &dflt_, bool allowSideEffects);
441 };
442 
443 } // namespace
444 } // namespace
445 } // namespace
446 } // namespace
447 
448 #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.
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)
Accessor for value width.
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
Returns true if two values could be equal.
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.
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 uint64_t get_number() const ROSE_OVERRIDE
Return the concrete number for this value.
STL namespace.
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.
Describes (part of) a physical CPU register.
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.
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.
Sawyer::SharedPointer< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
bool negate
Switch between name+offset and (-name)+offset; should be false for constants.
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 void set_width(size_t nbits) ROSE_OVERRIDE
Accessor for value width.
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.
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.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the left.
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.
Defines registers available for a particular architecture.
Definition: Registers.h:32
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.
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.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
virtual bool is_number() const ROSE_OVERRIDE
Determines if the value is a concrete number.
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 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
Returns true if two values must be equal.
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.
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.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a PartialSymbolicSemantics value.