ROSE  0.9.9.109
ConcreteSemantics2.h
1 #ifndef Rose_ConcreteSemantics2_H
2 #define Rose_ConcreteSemantics2_H
3 
4 #ifndef __STDC_FORMAT_MACROS
5 #define __STDC_FORMAT_MACROS
6 #endif
7 #include <inttypes.h>
8 
9 #include "integerOps.h"
10 #include "BaseSemantics2.h"
11 #include "RegisterStateGeneric.h"
12 #include <Sawyer/BitVector.h>
13 
14 namespace Rose {
15 namespace BinaryAnalysis { // documented elsewhere
16 namespace InstructionSemantics2 { // documented elsewhere
17 
22 namespace ConcreteSemantics {
23 
25 // Value type
27 
30 
32 typedef BaseSemantics::Formatter Formatter; // we might extend this in the future
33 
42 protected:
44 
46  // Real constructors
47 protected:
48  explicit SValue(size_t nbits): BaseSemantics::SValue(nbits), bits_(nbits) {}
49 
50  SValue(size_t nbits, uint64_t number): BaseSemantics::SValue(nbits) {
51  bits_ = Sawyer::Container::BitVector(nbits);
52  bits_.fromInteger(number);
53  }
54 
56  // Static allocating constructors
57 public:
59  static SValuePtr instance() {
60  return SValuePtr(new SValue(1));
61  }
62 
67  static SValuePtr instance(size_t nbits) {
68  return SValuePtr(new SValue(nbits));
69  }
70 
72  static SValuePtr instance(size_t nbits, uint64_t value) {
73  return SValuePtr(new SValue(nbits, value));
74  }
75 
77  // Virtual allocating constructors
78 public:
79  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE {
80  return instance(nbits);
81  }
82  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE {
83  return instance(nbits);
84  }
85  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE {
86  return instance(nbits);
87  }
88  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE {
89  return instance(nbits, value);
90  }
91  virtual BaseSemantics::SValuePtr boolean_(bool value) const ROSE_OVERRIDE {
92  return instance(1, value ? 1 : 0);
93  }
94  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
95  SValuePtr retval(new SValue(*this));
96  if (new_width!=0 && new_width!=retval->get_width())
97  retval->set_width(new_width);
98  return retval;
99  }
101  createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&, SMTSolver*) const ROSE_OVERRIDE;
102 
104  // Dynamic pointer casts
105 public:
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  // Override virtual methods...
115 public:
116  virtual bool may_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE;
117  virtual bool must_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE;
118 
119  virtual void set_width(size_t nbits) ROSE_OVERRIDE;
120 
121  virtual bool isBottom() const ROSE_OVERRIDE {
122  return false;
123  }
124 
125  virtual bool is_number() const ROSE_OVERRIDE {
126  return true;
127  }
128 
129  virtual uint64_t get_number() const ROSE_OVERRIDE;
130 
131  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
132 
134  // Additional methods first declared in this class...
135 public:
139  virtual const Sawyer::Container::BitVector& bits() const { return bits_; }
140  virtual void bits(const Sawyer::Container::BitVector&);
142 };
143 
144 
146 // Register State
148 
149 typedef BaseSemantics::RegisterStateGeneric RegisterState;
150 typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;
151 
152 
154 // Memory State
156 
158 typedef boost::shared_ptr<class MemoryState> MemoryStatePtr;
159 
165  MemoryMap::Ptr map_;
166  rose_addr_t pageSize_;
167 
169  // Real constructors
170 protected:
171  explicit MemoryState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
172  : BaseSemantics::MemoryState(addrProtoval, valProtoval), pageSize_(4096) {
173  (void) SValue::promote(addrProtoval); // for its checking side effects
174  (void) SValue::promote(valProtoval);
175  }
176 
177  MemoryState(const MemoryState &other)
178  : BaseSemantics::MemoryState(other), map_(other.map_), pageSize_(other.pageSize_) {
179  if (map_) {
180  BOOST_FOREACH (MemoryMap::Segment &segment, map_->values())
181  segment.buffer()->copyOnWrite(true);
182  }
183  }
184 
186  // Static allocating constructors
187 public:
191  static MemoryStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) {
192  return MemoryStatePtr(new MemoryState(addrProtoval, valProtoval));
193  }
194 
199  static MemoryStatePtr instance(const MemoryStatePtr &other) {
200  return MemoryStatePtr(new MemoryState(*other));
201  }
202 
204  // Virtual constructors
205 public:
211  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
212  return instance(addrProtoval, valProtoval);
213  }
214 
220  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
221  return MemoryStatePtr(new MemoryState(*this));
222  }
223 
225  // Dynamic pointer casts
226 public:
229  static MemoryStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
230  MemoryStatePtr retval = boost::dynamic_pointer_cast<MemoryState>(x);
231  ASSERT_not_null(retval);
232  return retval;
233  }
234 
236  // Methods we inherited
237 public:
238  virtual void clear() ROSE_OVERRIDE {
239  map_ = MemoryMap::Ptr();
240  }
241 
242  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
243 
244  virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt,
245  BaseSemantics::RiscOperators *addrOps,
246  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
247 
248  virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
249  BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
250 
251  virtual bool merge(const BaseSemantics::MemoryStatePtr &other, BaseSemantics::RiscOperators *addrOps,
252  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
253 
255  // Methods first declared in this class
256 public:
258  const MemoryMap::Ptr memoryMap() const { return map_; }
259 
266 
273  rose_addr_t pageSize() const { return pageSize_; }
274  void pageSize(rose_addr_t nBytes);
281  void allocatePage(rose_addr_t va);
282 
283 };
284 
285 
287 // Complete semantic state
289 
290 typedef BaseSemantics::State State;
291 typedef BaseSemantics::StatePtr StatePtr;
292 
293 
295 // RISC operators
297 
299 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
300 
320  // Real constructors
321 protected:
323  : BaseSemantics::RiscOperators(protoval, solver) {
324  name("Concrete");
325  (void) SValue::promote(protoval); // make sure its dynamic type is a ConcreteSemantics::SValue
326  }
327 
328  RiscOperators(const BaseSemantics::StatePtr &state, SMTSolver *solver)
329  : BaseSemantics::RiscOperators(state, solver) {
330  name("Concrete");
331  (void) SValue::promote(state->protoval()); // values must have ConcreteSemantics::SValue dynamic type
332  }
333 
335  // Static allocating constructors
336 public:
339  static RiscOperatorsPtr instance(const RegisterDictionary *regdict, SMTSolver *solver=NULL) {
341  BaseSemantics::RegisterStatePtr registers = RegisterState::instance(protoval, regdict);
342  BaseSemantics::MemoryStatePtr memory = MemoryState::instance(protoval, protoval);
343  BaseSemantics::StatePtr state = State::instance(registers, memory);
344  return RiscOperatorsPtr(new RiscOperators(state, solver));
345  }
346 
350  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL) {
351  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
352  }
353 
356  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL) {
357  return RiscOperatorsPtr(new RiscOperators(state, solver));
358  }
359 
361  // Virtual constructors
362 public:
364  SMTSolver *solver=NULL) const ROSE_OVERRIDE {
365  return instance(protoval, solver);
366  }
367 
369  SMTSolver *solver=NULL) const ROSE_OVERRIDE {
370  return instance(state, solver);
371  }
372 
374  // Dynamic pointer casts
375 public:
378  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
379  RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
380  ASSERT_not_null(retval);
381  return retval;
382  }
383 
385  // New methods for constructing values, so we don't have to write so many SValue::promote calls in the RiscOperators
386  // implementations.
387 protected:
388  SValuePtr svalue_number(size_t nbits, uint64_t value) {
389  return SValue::promote(number_(nbits, value));
390  }
391 
392  SValuePtr svalue_number(const Sawyer::Container::BitVector&);
393 
394  SValuePtr svalue_boolean(bool b) {
395  return SValue::promote(boolean_(b));
396  }
397 
398  SValuePtr svalue_zero(size_t nbits) {
399  return SValue::promote(number_(nbits, 0));
400  }
401 
403  // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
404 public:
405  virtual void interrupt(int majr, int minr) ROSE_OVERRIDE;
407  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
409  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
411  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
412  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
414  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
416  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
420  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
422  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
424  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
426  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
428  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
429  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
431  const BaseSemantics::SValuePtr &a_,
432  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
433  virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
434  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
436  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
438  const BaseSemantics::SValuePtr &b_,
439  const BaseSemantics::SValuePtr &c_,
440  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
441  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
443  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
445  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
447  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
449  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
451  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
453  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
454 
455  virtual BaseSemantics::SValuePtr fpFromInteger(const BaseSemantics::SValuePtr &intValue, SgAsmFloatType*) ROSE_OVERRIDE;
456  virtual BaseSemantics::SValuePtr fpToInteger(const BaseSemantics::SValuePtr &fpValue, SgAsmFloatType *fpType,
457  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
458  virtual BaseSemantics::SValuePtr fpAdd(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b,
459  SgAsmFloatType*) ROSE_OVERRIDE;
460  virtual BaseSemantics::SValuePtr fpSubtract(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b,
461  SgAsmFloatType*) ROSE_OVERRIDE;
462  virtual BaseSemantics::SValuePtr fpMultiply(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b,
463  SgAsmFloatType*) ROSE_OVERRIDE;
464  virtual BaseSemantics::SValuePtr fpRoundTowardZero(const BaseSemantics::SValuePtr &a, SgAsmFloatType*) ROSE_OVERRIDE;
465 
466  virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg,
467  const BaseSemantics::SValuePtr &addr,
468  const BaseSemantics::SValuePtr &dflt,
469  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
470  virtual void writeMemory(RegisterDescriptor segreg,
471  const BaseSemantics::SValuePtr &addr,
472  const BaseSemantics::SValuePtr &data,
473  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
474 
475 protected:
476  // Convert expression to double
477  double exprToDouble(const BaseSemantics::SValuePtr &expr, SgAsmFloatType*);
478 
479  // Convert double to expression
480  BaseSemantics::SValuePtr doubleToExpr(double d, SgAsmFloatType*);
481 };
482 
483 } // namespace
484 } // namespace
485 } // namespace
486 } // namespace
487 
488 #endif
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Write a value to memory.
virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted right arithmetically (with sign bit).
static RegisterStateGenericPtr instance(const SValuePtr &protoval, const RegisterDictionary *regdict)
Instantiate a new register state.
Defines RISC operators for the ConcreteSemantics domain.
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Concatenates the bits of two values.
static MemoryStatePtr instance(const MemoryStatePtr &other)
Instantiates a new deep copy of an existing state.
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 void print(std::ostream &, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print a value to a stream using default format.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to concrete RISC operations.
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise OR of two values.
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
static SValuePtr instance()
Instantiate a new prototypical value.
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Two's complement.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two signed values.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise XOR of two values.
virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Read a value from memory.
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted right logically (no sign bit).
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 fpRoundTowardZero(const BaseSemantics::SValuePtr &a, SgAsmFloatType *) ROSE_OVERRIDE
Round toward zero.
Type of values manipulated by the concrete domain.
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) ROSE_OVERRIDE
Extracts bits from a value.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Returns true if two values must be equal.
MemoryStatePtr Ptr
Shared-ownership pointer for a MemoryState.
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x)
Run-time promotion of a base RiscOperators pointer to concrete operators.
STL namespace.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Determines whether a value is equal to zero.
Holds a value or nothing.
Definition: Optional.h:49
Buffer< A, T >::Ptr buffer() const
Property: buffer.
virtual const Sawyer::Container::BitVector & bits() const
Returns the bit vector storing the concrete 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 uint64_t get_number() const ROSE_OVERRIDE
Return the concrete number for this value.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with unsigned values.
bool copyOnWrite() const
Property: Copy on write.
Definition: Buffer.h:127
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL)
Instantiates a new RiscOperators object with specified prototypical values.
virtual BaseSemantics::SValuePtr fpMultiply(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b, SgAsmFloatType *) ROSE_OVERRIDE
Multiply two floating-point values.
virtual bool is_number() const ROSE_OVERRIDE
Determines if the value is a concrete number.
Main namespace for the ROSE library.
Describes (part of) a physical CPU register.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE
Virtual constructor.
virtual bool merge(const BaseSemantics::MemoryStatePtr &other, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Merge memory states for data flow analysis.
virtual void interrupt(int majr, int minr) ROSE_OVERRIDE
Invoked for instructions that cause an interrupt.
virtual SValuePtr boolean_(bool value)
Returns a Boolean value.
BitVector & fromInteger(const BitRange &range, boost::uint64_t value)
Obtain bits from an integer.
Definition: BitVector.h:1180
Name space for the entire library.
Definition: Access.h:11
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with signed values.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Adds two integers of equal size.
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Returns position of most significant set bit; zero when no bits are set.
boost::shared_ptr< class RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
boost::shared_ptr< class State > StatePtr
Shared-ownership pointer to a semantic state.
virtual BaseSemantics::SValuePtr fpToInteger(const BaseSemantics::SValuePtr &fpValue, SgAsmFloatType *fpType, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
Construct an integer value from a floating-point value.
virtual BaseSemantics::SValuePtr boolean_(bool value) const ROSE_OVERRIDE
Create a new, Boolean value.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two unsigned values.
Base classes for instruction semantics.
Sawyer::SharedPointer< class SValue > SValuePtr
Smart-ownership pointer to a concrete semantic value.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE
Create a new concrete semantic value.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE
Sign extends a value.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE
Create a new undefined semantic value.
static SValuePtr instance(size_t nbits)
Instantiate a new undefined value of specified width.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to a concrete memory state.
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
One's complement.
virtual BaseSemantics::SValuePtr fpFromInteger(const BaseSemantics::SValuePtr &intValue, SgAsmFloatType *) ROSE_OVERRIDE
Construct a floating-point value from an integer value.
virtual void set_width(size_t nbits) ROSE_OVERRIDE
Accessor for value width.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual BaseSemantics::SValuePtr fpAdd(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b, SgAsmFloatType *) ROSE_OVERRIDE
Add two floating-point values.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted left.
An efficient mapping from an address space to stored data.
Definition: MemoryMap.h:96
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.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a SymbolicSemantics 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.
static MemoryStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
Defines registers available for a particular architecture.
Definition: Registers.h:32
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.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL)
Instantiates a new RiscOperators object with specified state.
static RiscOperatorsPtr instance(const RegisterDictionary *regdict, SMTSolver *solver=NULL)
Instantiates a new RiscOperators object and configures it to use semantic values and states that are ...
static StatePtr instance(const RegisterStatePtr &registers, const MemoryStatePtr &memory)
Instantiate a new state object with specified register and memory states.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the right.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
const MemoryMap::Ptr memoryMap() const
Returns the memory map.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
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...
static SValuePtr instance(size_t nbits, uint64_t value)
Instantiate a new concrete value.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE
Data-flow bottom value.
Represents no value.
Definition: Optional.h:32
virtual SMTSolver * solver() const
Property: Satisfiability module theory (SMT) solver.
void allocatePage(rose_addr_t va)
Allocate a page of memory.
virtual const std::string & name() const
Property: Name used for debugging.
virtual SValuePtr number_(size_t nbits, uint64_t value)
Returns a number of the specified bit width.
BaseSemantics::Formatter Formatter
Formatter for symbolic values.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiplies two signed values.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Returns true if two values could be equal.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the left.
Floating point types.
virtual void print(std::ostream &, Formatter &) const ROSE_OVERRIDE
Print a memory state to more than one line of output.
virtual BaseSemantics::SValuePtr fpSubtract(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b, SgAsmFloatType *) ROSE_OVERRIDE
Subtract one floating-point value from another.
virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual copy constructor.
static MemoryStatePtr promote(const BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a concrete memory state.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SMTSolver.h:19
virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
If-then-else.
virtual bool isBottom() const ROSE_OVERRIDE
Determines whether a value is a data-flow bottom.
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise AND of two values.