ROSE  0.9.9.109
MultiSemantics2.h
1 #ifndef Rose_MultiSemantics2_H
2 #define Rose_MultiSemantics2_H
3 
4 #include "BaseSemantics2.h"
5 
6 namespace Rose { // documented elsewhere
7 namespace BinaryAnalysis { // documented elsewhere
8 namespace InstructionSemantics2 { // documented elsewhere
9 
57 namespace MultiSemantics {
58 
61 public:
62  std::vector<std::string> subdomain_names;
63 };
64 
66 // Semantic values
68 
71 
82 protected:
83  typedef std::vector<BaseSemantics::SValuePtr> Subvalues;
84  Subvalues subvalues;
85 
86 protected:
87  // Protected constructors
88  explicit SValue(size_t nbits)
89  : BaseSemantics::SValue(nbits) {}
90 
91  SValue(const SValue &other)
92  : BaseSemantics::SValue(other.get_width()) {
93  init(other);
94  }
95 
96  void init(const SValue &other);
97 
99  // Static allocating constructors
100 public:
102  static SValuePtr instance() {
103  return SValuePtr(new SValue(1));
104  }
105 
107  static SValuePtr promote(const BaseSemantics::SValuePtr &v) { // hot
108  SValuePtr retval = v.dynamicCast<SValue>();
109  ASSERT_not_null(retval);
110  return retval;
111  }
112 
114  // Virtual allocating constructors
115 public:
116 
117  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE;
118 
122  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE;
123 
127  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE;
128 
131  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t number) const ROSE_OVERRIDE;
132 
135  virtual SValuePtr create_empty(size_t nbits) const {
136  return SValuePtr(new SValue(nbits));
137  }
138 
139  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
140  return BaseSemantics::SValuePtr(new SValue(*this));
141  }
142 
144  createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&, SMTSolver*) const ROSE_OVERRIDE;
145 
147  // Override virtual methods
148 public:
151  virtual bool may_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE;
152 
156  virtual bool must_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE;
157 
158  virtual void set_width(size_t nbits) ROSE_OVERRIDE;
159 
160  virtual bool isBottom() const ROSE_OVERRIDE;
161 
165  virtual bool is_number() const ROSE_OVERRIDE;
166 
167  virtual uint64_t get_number() const ROSE_OVERRIDE;
168 
169  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
170 
172  // Additional methods first declared at this level of the class hierarchy
173 public:
176  virtual bool is_valid(size_t idx) const { // hot
177  return idx<subvalues.size() && subvalues[idx]!=NULL;
178  }
179 
182  virtual void invalidate(size_t idx);
183 
185  virtual BaseSemantics::SValuePtr get_subvalue(size_t idx) const { // hot
186  ASSERT_require(idx<subvalues.size() && subvalues[idx]!=NULL); // you should have called is_valid() first
187  return subvalues[idx];
188  }
189 
193  virtual void set_subvalue(size_t idx, const BaseSemantics::SValuePtr &value) { // hot
194  ASSERT_require(value==NULL || value->get_width()==get_width());
195  if (idx>=subvalues.size())
196  subvalues.resize(idx+1);
197  subvalues[idx] = value;
198  }
199 };
200 
201 
203 // Register states
205 
206 typedef void RegisterState;
207 
209 typedef boost::shared_ptr<void> RegisterStatePtr;
210 
212 // Memory states
214 
215 typedef void MemoryState;
216 
218 typedef boost::shared_ptr<void> MemoryStatePtr;
219 
221 // Complete state
223 
224 typedef void State;
225 
227 typedef boost::shared_ptr<void> StatePtr;
228 
230 // RISC operators
232 
234 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
235 
241 protected:
242  typedef std::vector<BaseSemantics::RiscOperatorsPtr> Subdomains;
243  Subdomains subdomains;
244  std::vector<bool> active;
245  Formatter formatter; // contains names for the subdomains
246 
248  // Real constructors
249 protected:
251  : BaseSemantics::RiscOperators(protoval, solver) {
252  name("Multi");
253  (void) SValue::promote(protoval); // check that its dynamic type is a MultiSemantics::SValue
254  }
255 
256  explicit RiscOperators(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL)
258  name("Multi");
259  (void) SValue::promote(state->protoval()); // dynamic type must be a MultiSemantics::SValue
260  }
261 
263  // Static allocating constructors
264 public:
268  static RiscOperatorsPtr instance(const RegisterDictionary *regdict) {
270  return RiscOperatorsPtr(new RiscOperators(protoval));
271  }
272 
273  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL) {
274  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
275  }
276 
277  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL) {
278  return RiscOperatorsPtr(new RiscOperators(state, solver));
279  }
280 
282  // Virtual constructors
283 public:
285  SMTSolver *solver=NULL) const ROSE_OVERRIDE {
286  return instance(protoval, solver);
287  }
288 
290  SMTSolver *solver=NULL) const ROSE_OVERRIDE {
291  return instance(state, solver);
292  }
293 
295  // Dynamic pointer casts
296 public:
297  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &ops);
298 
300  // Methods first defined at this level of the class hiearchy
301 public:
307  virtual size_t add_subdomain(const BaseSemantics::RiscOperatorsPtr &subdomain, const std::string &name, bool activate=true);
308 
311  return formatter;
312  }
313 
315  virtual size_t nsubdomains() const {
316  return subdomains.size();
317  }
318 
320  virtual BaseSemantics::RiscOperatorsPtr get_subdomain(size_t idx) const;
321 
325  virtual bool is_active(size_t idx) const {
326  return idx<subdomains.size() && subdomains[idx]!=NULL && active[idx];
327  }
328 
331  virtual void clear_active(size_t idx) {
332  set_active(idx, false);
333  }
334 
338  virtual void set_active(size_t idx, bool status);
339 
342  virtual void before(size_t idx) {}
343 
346  virtual void after(size_t idx) {}
347 
349  virtual SValuePtr svalue_empty(size_t nbits) {
350  return SValue::promote(protoval())->create_empty(nbits);
351  }
352 
368  class Cursor {
369  public:
370  typedef std::vector<SValuePtr> Inputs;
371  protected:
372  RiscOperators *ops_;
373  Inputs inputs_;
374  size_t idx_;
375  public:
376  Cursor(RiscOperators *ops, const SValuePtr &arg1=SValuePtr(), const SValuePtr &arg2=SValuePtr(),
377  const SValuePtr &arg3=SValuePtr())
378  : ops_(ops), idx_(0) {
379  init(arg1, arg2, arg3);
380  }
381  Cursor(RiscOperators *ops, const Inputs &inputs)
382  : ops_(ops), inputs_(inputs), idx_(0) {
383  init();
384  }
385 
389  static Inputs inputs(const BaseSemantics::SValuePtr &arg1=BaseSemantics::SValuePtr(),
392 
393  bool at_end() const;
394  void next();
395  size_t idx() const;
401 
402  protected:
403  void init(const SValuePtr &arg1, const SValuePtr &arg2, const SValuePtr &arg3);
404  void init();
405  void skip_invalid();
406  bool inputs_are_valid() const;
407  };
408 
410  // RISC operations and other overrides
411 public:
412  virtual void print(std::ostream &o, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
413  virtual void startInstruction(SgAsmInstruction *insn) ROSE_OVERRIDE;
414  virtual void finishInstruction(SgAsmInstruction *insn) ROSE_OVERRIDE;
415  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) ROSE_OVERRIDE;
416  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) ROSE_OVERRIDE;
417  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) ROSE_OVERRIDE;
418  virtual BaseSemantics::SValuePtr boolean_(bool) ROSE_OVERRIDE;
419  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) ROSE_OVERRIDE;
420  virtual BaseSemantics::SValuePtr filterCallTarget(const BaseSemantics::SValuePtr&) ROSE_OVERRIDE;
421  virtual BaseSemantics::SValuePtr filterReturnTarget(const BaseSemantics::SValuePtr&) ROSE_OVERRIDE;
422  virtual BaseSemantics::SValuePtr filterIndirectJumpTarget(const BaseSemantics::SValuePtr&) ROSE_OVERRIDE;
423  virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
424  virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
425  virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
426  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
427  virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a, size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
428  virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
429  virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
430  virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
431  virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a,
432  const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
433  virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a,
434  const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
435  virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a,
436  const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
437  virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a,
438  const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
439  virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a,
440  const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
441  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
442  virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &cond, const BaseSemantics::SValuePtr &a,
443  const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
444  virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a, size_t new_width) ROSE_OVERRIDE;
445  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a, size_t new_width) ROSE_OVERRIDE;
446  virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
447  virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b,
448  const BaseSemantics::SValuePtr &c,
449  BaseSemantics::SValuePtr &carry_out/*output*/) ROSE_OVERRIDE;
450  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
451  virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a,
452  const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
453  virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a,
454  const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
455  virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a,
456  const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
457  virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a,
458  const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
459  virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a,
460  const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
461  virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a,
462  const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
463  virtual BaseSemantics::SValuePtr fpFromInteger(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
464  virtual BaseSemantics::SValuePtr fpToInteger(const BaseSemantics::SValuePtr&, SgAsmFloatType*,
465  const BaseSemantics::SValuePtr&) ROSE_OVERRIDE;
466  virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr&, SgAsmFloatType*, SgAsmFloatType*) ROSE_OVERRIDE;
467  virtual BaseSemantics::SValuePtr fpIsNan(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
468  virtual BaseSemantics::SValuePtr fpIsDenormalized(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
469  virtual BaseSemantics::SValuePtr fpIsZero(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
470  virtual BaseSemantics::SValuePtr fpIsInfinity(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
471  virtual BaseSemantics::SValuePtr fpSign(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
472  virtual BaseSemantics::SValuePtr fpEffectiveExponent(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
473  virtual BaseSemantics::SValuePtr fpAdd(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
474  SgAsmFloatType*) ROSE_OVERRIDE;
475  virtual BaseSemantics::SValuePtr fpSubtract(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
476  SgAsmFloatType*) ROSE_OVERRIDE;
477  virtual BaseSemantics::SValuePtr fpMultiply(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
478  SgAsmFloatType*) ROSE_OVERRIDE;
479  virtual BaseSemantics::SValuePtr fpDivide(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
480  SgAsmFloatType*) ROSE_OVERRIDE;
481  virtual BaseSemantics::SValuePtr fpSquareRoot(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
482  virtual BaseSemantics::SValuePtr fpRoundTowardZero(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
483  virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg,
484  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
485  virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
486  virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr,
487  const BaseSemantics::SValuePtr &dflt,
488  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
489  virtual void writeMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr,
490  const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
491 };
492 
493 } // namespace
494 } // namespace
495 } // namespace
496 } // namespace
497 
498 #endif
virtual BaseSemantics::SValuePtr fpSign(const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Sign of floating-point value.
BaseSemantics::RiscOperatorsPtr operator->() const
Return the subdomain for the current cursor position.
boost::shared_ptr< void > MemoryStatePtr
Shared-ownership pointer to a multi-semantics memory state.
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 bottom_(size_t nbits) ROSE_OVERRIDE
Returns a data-flow bottom value.
boost::shared_ptr< void > StatePtr
Shared-ownership pointer to a multi-semantics state.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE
Determines whether a value is equal to zero.
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Computes bit-wise OR of two values.
static SValuePtr instance()
Construct a prototypical value.
virtual SValuePtr svalue_empty(size_t nbits)
Convenience function for SValue::create_empty().
virtual BaseSemantics::SValuePtr fpIsZero(const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Whether a floating-point value is equal to zero.
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE
Two's complement.
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::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a, size_t new_width) ROSE_OVERRIDE
Extend (or shrink) operand a so it is nbits wide by adding or removing high-order bits...
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE
One's complement.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Determines if two multidomain values might be equal.
virtual bool isBottom() const ROSE_OVERRIDE
Determines whether a value is a data-flow bottom.
virtual Formatter & get_formatter()
Returns a formatter containing the names of the subdomains.
Base class for machine instructions.
virtual bool is_active(size_t idx) const
Returns true if a subdomain is active.
virtual void startInstruction(SgAsmInstruction *insn) ROSE_OVERRIDE
Called at the beginning of every instruction.
virtual BaseSemantics::SValuePtr fpIsInfinity(const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Whether a floating-point value is infinity.
virtual BaseSemantics::SValuePtr fpAdd(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Add two floating-point values.
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 RiscOperatorsPtr instance(const RegisterDictionary *regdict)
Static allocating constructor.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr filterIndirectJumpTarget(const BaseSemantics::SValuePtr &) ROSE_OVERRIDE
Invoked to filter indirect jumps.
virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr &, SgAsmFloatType *, SgAsmFloatType *) ROSE_OVERRIDE
Convert from one floating-point type to another.
virtual BaseSemantics::SValuePtr fpIsDenormalized(const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Whether a floating-point value is denormalized.
STL namespace.
Holds a value or nothing.
Definition: Optional.h:49
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Concatenates the bits of two values.
virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &cond, const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
If-then-else.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a, size_t new_width) ROSE_OVERRIDE
Sign extends a value.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
Helps printing multidomain values by allowing the user to specify a name for each subdomain...
virtual bool is_number() const ROSE_OVERRIDE
Determines if the value is a concrete number.
Main namespace for the ROSE library.
virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE
Returns arg shifted right arithmetically (with sign bit).
Describes (part of) a physical CPU register.
virtual BaseSemantics::SValuePtr fpToInteger(const BaseSemantics::SValuePtr &, SgAsmFloatType *, const BaseSemantics::SValuePtr &) ROSE_OVERRIDE
Construct an integer value from a floating-point value.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to multi-semantics RISC operators.
virtual BaseSemantics::SValuePtr fpSubtract(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Subtract one floating-point value from another.
virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
Reads a value from a register.
Defines RISC operators for the MultiSemantics domain.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Divides two signed values.
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 filterCallTarget(const BaseSemantics::SValuePtr &) ROSE_OVERRIDE
Invoked to filter call targets.
virtual void clear_active(size_t idx)
Makes a subdomain inactive.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Computes bit-wise XOR of two values.
BaseSemantics::RiscOperatorsPtr operator*() const
Return the subdomain for the current cursor position.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
boost::shared_ptr< class State > StatePtr
Shared-ownership pointer to a semantic state.
virtual BaseSemantics::SValuePtr fpMultiply(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Multiply two floating-point values.
virtual void before(size_t idx)
Called before each subdomain RISC operation.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE
Returns arg shifted left.
virtual uint64_t get_number() const ROSE_OVERRIDE
Return the concrete number for this value.
Base classes for instruction semantics.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a MultiSemantics value.
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 void set_active(size_t idx, bool status)
Makes a subdomain active or inactive.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) ROSE_OVERRIDE
Returns a new undefined value.
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< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual void set_subvalue(size_t idx, const BaseSemantics::SValuePtr &value)
Insert a subdomain value.
virtual BaseSemantics::SValuePtr filterReturnTarget(const BaseSemantics::SValuePtr &) ROSE_OVERRIDE
Invoked to filter return targets.
BaseSemantics::SValuePtr operator()(const BaseSemantics::SValuePtr &) const
Returns subdomain value of its multidomain argument.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Determines if two multidomain values must be equal.
virtual void finishInstruction(SgAsmInstruction *insn) ROSE_OVERRIDE
Called at the end of every instruction.
virtual bool is_valid(size_t idx) const
Returns true if a subdomain value is valid.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer to a multi-semantic value.
virtual void after(size_t idx)
Called after each subdomain RISC operation.
virtual size_t add_subdomain(const BaseSemantics::RiscOperatorsPtr &subdomain, const std::string &name, bool activate=true)
Add a subdomain to this MultiSemantics domain.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer to a semantic value in any domain.
boost::shared_ptr< void > RegisterStatePtr
Shared-ownership pointer to a multi-semantics register state.
virtual void invalidate(size_t idx)
Removes a subdomain value and marks it as invalid.
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::RiscOperatorsPtr get_subdomain(size_t idx) const
Returns the RiscOperators for a subdomain.
Defines registers available for a particular architecture.
Definition: Registers.h:32
virtual BaseSemantics::SValuePtr fpIsNan(const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Whether a floating-point value is a special not-a-number bit pattern.
virtual BaseSemantics::SValuePtr fpRoundTowardZero(const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Round toward zero.
virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE
Writes a value to a register.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
virtual size_t nsubdomains() const
Returns the number of subdomains added to this MultiDomain.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE
Data-flow bottom value.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE
Create a new unspecified MultiSemantics value.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Adds two integers of equal size.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Divides two unsigned values.
virtual BaseSemantics::SValuePtr fpFromInteger(const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Construct a floating-point value from an integer value.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE
Rotate bits to the right.
static Inputs inputs(const BaseSemantics::SValuePtr &arg1=BaseSemantics::SValuePtr(), const BaseSemantics::SValuePtr &arg2=BaseSemantics::SValuePtr(), const BaseSemantics::SValuePtr &arg3=BaseSemantics::SValuePtr())
Class method to construct the array of inputs from a variable number of arguments.
virtual void set_width(size_t nbits) ROSE_OVERRIDE
Accessor for value width.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE
Create a new undefined MultiSemantics value.
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 BaseSemantics::SValuePtr boolean_(bool) ROSE_OVERRIDE
Returns a Boolean value.
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE
Returns arg shifted right logically (no sign bit).
virtual size_t get_width() const
Accessor for value width.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE
Rotate bits to the left.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) ROSE_OVERRIDE
Returns a number of the specified bit width.
Type of values manipulated by the MultiSemantics domain.
virtual BaseSemantics::SValuePtr get_subvalue(size_t idx) const
Return a subdomain value.
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Calculates modulo with signed values.
virtual void print(std::ostream &o, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print multi-line output for this object.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Multiply two unsigned values.
virtual SMTSolver * solver() const
Property: Satisfiability module theory (SMT) solver.
virtual const std::string & name() const
Property: Name used for debugging.
virtual BaseSemantics::SValuePtr fpSquareRoot(const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Square root.
virtual BaseSemantics::SValuePtr fpEffectiveExponent(const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Exponent of floating-point value.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t number) const ROSE_OVERRIDE
Create a MultiSemantics value holding a concrete value.
virtual SValuePtr create_empty(size_t nbits) const
Create a new MultiSemantics value with no valid subvalues.
Floating point types.
virtual BaseSemantics::SValuePtr fpDivide(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &, SgAsmFloatType *) ROSE_OVERRIDE
Divide one floating-point value by another.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Multiplies two signed values.
size_t idx() const
Return the subdomain index for the current cursor position.
bool at_end() const
Returns true when the cursor has gone past the last valid subdomain.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Calculates modulo with unsigned values.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SMTSolver.h:19
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE
Computes bit-wise AND of two values.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print a value to a stream using default format.