ROSE  0.9.9.139
IntervalSemantics2.h
1 #ifndef Rose_IntervalSemantics_H
2 #define Rose_IntervalSemantics_H
3 #include <stdint.h>
4 
5 #ifndef __STDC_FORMAT_MACROS
6 #define __STDC_FORMAT_MACROS
7 #endif
8 #include <inttypes.h>
9 
10 #include "BaseSemantics2.h"
11 #include "integerOps.h"
12 #include "RegisterStateGeneric.h"
13 #include "MemoryCellList.h"
14 
15 namespace Rose {
16 namespace BinaryAnalysis { // documented elsewhere
17 namespace InstructionSemantics2 { // documented elsewhere
18 
19 
21 namespace IntervalSemantics {
22 
23 /* Single contiguous interval. */
25 
28 
30 // Semantic values
32 
35 
38 protected:
39  Intervals intervals_;
40  bool isBottom_;
41 
42 protected:
43  // Protected constructors. See base class and public members for documentation
44  explicit SValue(size_t nbits):
45  BaseSemantics::SValue(nbits), isBottom_(false){
46  intervals_.insert(Interval::hull(0, IntegerOps::genMask<uint64_t>(nbits)));
47  }
48  SValue(size_t nbits, uint64_t number)
49  : BaseSemantics::SValue(nbits), isBottom_(false) {
50  number &= IntegerOps::genMask<uint64_t>(nbits);
51  intervals_.insert(number);
52  }
53  SValue(size_t nbits, uint64_t v1, uint64_t v2):
54  BaseSemantics::SValue(nbits), isBottom_(false) {
55  v1 &= IntegerOps::genMask<uint64_t>(nbits);
56  v2 &= IntegerOps::genMask<uint64_t>(nbits);
57  ASSERT_require(v1<=v2);
58  intervals_.insert(Interval::hull(v1, v2));
59  }
60  SValue(size_t nbits, const Intervals &intervals):
61  BaseSemantics::SValue(nbits), isBottom_(false) {
62  ASSERT_require(!intervals.isEmpty());
63  ASSERT_require((intervals.greatest() <= IntegerOps::genMask<uint64_t>(nbits)));
64  intervals_ = intervals;
65  }
66 
68  // Static allocating constructors
69 public:
71  static SValuePtr instance() {
72  return SValuePtr(new SValue(1));
73  }
74 
76  static SValuePtr instance_bottom(size_t nbits) {
77  SValue *self = new SValue(nbits);
78  self->isBottom_ = true;
79  return SValuePtr(self);
80  }
81 
84  static SValuePtr instance_undefined(size_t nbits) {
85  return SValuePtr(new SValue(nbits));
86  }
87 
92  static SValuePtr instance_unspecified(size_t nbits) {
93  return SValuePtr(new SValue(nbits));
94  }
95 
97  static SValuePtr instance_integer(size_t nbits, uint64_t number) {
98  return SValuePtr(new SValue(nbits, number));
99  }
100 
102  static SValuePtr instance_intervals(size_t nbits, const Intervals &intervals) {
103  return SValuePtr(new SValue(nbits, intervals));
104  }
105 
107  static SValuePtr instance_hull(size_t nbits, uint64_t v1, uint64_t v2) {
108  return SValuePtr(new SValue(nbits, v1, v2));
109  }
110 
112  static SValuePtr instance_copy(const SValuePtr &other) {
113  return SValuePtr(new SValue(*other));
114  }
115 
117  static SValuePtr instance_from_bits(size_t nbits, uint64_t possible_bits);
118 
120  static SValuePtr promote(const BaseSemantics::SValuePtr &v) { // hot
121  SValuePtr retval = v.dynamicCast<SValue>();
122  ASSERT_not_null(retval);
123  return retval;
124  }
125 
127  // Virtual allocating constructors inherited from the super class
128 public:
129  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE {
130  return instance_bottom(nbits);
131  }
132  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE {
133  return instance_undefined(nbits);
134  }
135  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE {
136  return instance_unspecified(nbits);
137  }
138 
139  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t number) const ROSE_OVERRIDE {
140  return instance_integer(nbits, number);
141  }
142  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
143  SValuePtr retval(new SValue(*this));
144  if (new_width!=0 && new_width!=retval->get_width())
145  retval->set_width(new_width);
146  return retval;
147  }
148 
150  createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&, SmtSolver*) const ROSE_OVERRIDE;
151 
153  // Virtual allocating constructors first defined at this level of the class hierarchy
154 public:
156  virtual SValuePtr create(size_t nbits, uint64_t v1, uint64_t v2) {
157  return instance_hull(nbits, v1, v2);
158  }
159 
162  virtual SValuePtr create(size_t nbits, const Intervals &intervals) {
163  return instance_intervals(nbits, intervals);
164  }
165 
169  virtual SValuePtr create_from_bits(size_t nbits, uint64_t possible_bits) {
170  return instance_from_bits(nbits, possible_bits);
171  }
172 
173 
175  // Override virtual methods...
176 public:
177  virtual bool may_equal(const BaseSemantics::SValuePtr &other, SmtSolver *solver=NULL) const ROSE_OVERRIDE;
178  virtual bool must_equal(const BaseSemantics::SValuePtr &other, SmtSolver *solver=NULL) const ROSE_OVERRIDE;
179 
180  virtual bool isBottom() const ROSE_OVERRIDE {
181  return isBottom_;
182  }
183 
184  virtual bool is_number() const ROSE_OVERRIDE {
185  return 1==intervals_.size();
186  }
187 
188  virtual uint64_t get_number() const ROSE_OVERRIDE {
189  ASSERT_require(1==intervals_.size());
190  return intervals_.least();
191  }
192 
193  virtual void print(std::ostream &output, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
194 
196  // Additional methods introduced at this level of the class hierarchy
197 public:
199  const Intervals& get_intervals() const {
200  return intervals_;
201  }
202 
204  void set_intervals(const Intervals &intervals) {
205  intervals_ = intervals;
206  }
207 
209  uint64_t possible_bits() const;
210 
211 };
212 
213 
215 // Register state
217 
218 typedef BaseSemantics::RegisterStateGeneric RegisterState;
219 typedef BaseSemantics::RegisterStateGenericPtr RegisterStateGenericPtr;
220 
221 
223 // Memory state
225 
227 typedef boost::shared_ptr<class MemoryState> MemoryStatePtr;
228 
240 
242  // Real constructors
243 protected:
244  MemoryState(const BaseSemantics::MemoryCellPtr &protocell)
245  : BaseSemantics::MemoryCellList(protocell) {}
246 
247  MemoryState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
248  : BaseSemantics::MemoryCellList(addrProtoval, valProtoval) {}
249 
250  MemoryState(const MemoryState &other)
252 
254  // Static allocating constructors
255 public:
257  static MemoryStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
258  return MemoryStatePtr(new MemoryState(protocell));
259  }
260 
263  static MemoryStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) {
264  return MemoryStatePtr(new MemoryState(addrProtoval, valProtoval));
265  }
266 
268  // Virtual constructors
269 public:
270  virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const ROSE_OVERRIDE {
271  return instance(protocell);
272  }
273 
275  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
276  return instance(addrProtoval, valProtoval);
277  }
278 
279  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
280  return MemoryStatePtr(new MemoryState(*this));
281  }
282 
284  // Methods we inherited
285 public:
291  BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
292 
296  virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
297  BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
298 };
299 
300 
302 // Complete state
304 
305 typedef BaseSemantics::State State;
306 typedef BaseSemantics::StatePtr StatePtr;
307 
308 
310 // RISC operators
312 
314 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
315 
319  // Real constructors
320 protected:
322  : BaseSemantics::RiscOperators(protoval, solver) {
323  name("Interval");
324  (void) SValue::promote(protoval); // make sure its dynamic type is an IntervalSemantics::SValue or subclass thereof
325  }
326 
327  explicit RiscOperators(const BaseSemantics::StatePtr &state, SmtSolver *solver=NULL)
329  name("Interval");
330  (void) SValue::promote(state->protoval()); // dynamic type must be IntervalSemantics::SValue or subclass thereof
331  };
332 
334  // Static allocating constructors
335 public:
338  static RiscOperatorsPtr instance(const RegisterDictionary *regdict, SmtSolver *solver=NULL) {
340  BaseSemantics::RegisterStatePtr registers = RegisterState::instance(protoval, regdict);
341  BaseSemantics::MemoryStatePtr memory = MemoryState::instance(protoval, protoval);
342  BaseSemantics::StatePtr state = State::instance(registers, memory);
343  return RiscOperatorsPtr(new RiscOperators(state, solver));
344  }
345 
348  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, SmtSolver *solver=NULL) {
349  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
350  }
351 
354  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SmtSolver *solver=NULL) {
355  return RiscOperatorsPtr(new RiscOperators(state, solver));
356  }
357 
359  // Virtual constructors
360 public:
362  SmtSolver *solver=NULL) const ROSE_OVERRIDE {
363  return instance(protoval, solver);
364  }
365 
367  SmtSolver *solver=NULL) const ROSE_OVERRIDE {
368  return instance(state, solver);
369  }
370 
372  // Dynamic pointer casts
373 public:
376  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
377  RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
378  ASSERT_not_null(retval);
379  return retval;
380  }
381 
383  // Methods first introduced at this level of the class hierarchy.
384 public:
385 
388  virtual SValuePtr svalue_from_bits(size_t nbits, uint64_t possible_bits) {
389  return SValue::promote(protoval())->create_from_bits(nbits, possible_bits);
390  }
391 
394  virtual SValuePtr svalue_from_intervals(size_t nbits, const Intervals &intervals) {
395  return SValue::promote(protoval())->create(nbits, intervals);
396  }
397 
399  // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
400 public:
402  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
404  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
406  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
407  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
409  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
411  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
415  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
417  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
419  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
421  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
423  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
424  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
426  const BaseSemantics::SValuePtr &a_,
427  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
428  virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
429  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
431  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
433  const BaseSemantics::SValuePtr &b_,
434  const BaseSemantics::SValuePtr &c_,
435  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
436  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
438  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
440  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
442  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
444  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
446  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
448  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
450  const BaseSemantics::SValuePtr &addr,
451  const BaseSemantics::SValuePtr &dflt,
452  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
453  virtual void writeMemory(RegisterDescriptor segreg,
454  const BaseSemantics::SValuePtr &addr,
455  const BaseSemantics::SValuePtr &data,
456  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
457 };
458 
459 } // namespace
460 } // namespace
461 } // namespace
462 } // namespace
463 
464 #endif
const Intervals & get_intervals() const
Returns the rangemap stored in this value.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE
Virtual allocating constructor.
static RegisterStateGenericPtr instance(const SValuePtr &protoval, const RegisterDictionary *regdict)
Instantiate a new register state.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two signed values.
boost::shared_ptr< class MemoryCell > MemoryCellPtr
Shared-ownership pointer to a semantic memory cell.
Definition: MemoryCell.h:15
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE
Create a new undefined semantic value.
virtual SmtSolver * solver() const
Property: Satisfiability module theory (SMT) solver.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, SmtSolver *solver=NULL)
Instantiates a new RiscOperators object with specified prototypical value.
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x)
Run-time promotion of a base RiscOperators pointer to interval operators.
virtual SValuePtr create(size_t nbits, uint64_t v1, uint64_t v2)
Construct a ValueType that's constrained to be between two unsigned values, inclusive.
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const ROSE_OVERRIDE
Virtual allocating 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::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted right logically (no sign bit).
static SValuePtr instance_copy(const SValuePtr &other)
Instantiate a new copy of an existing value.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiply two unsigned values.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, SmtSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
static SValuePtr instance_integer(size_t nbits, uint64_t number)
Instantiate a new concrete value of particular width.
virtual bool is_number() const ROSE_OVERRIDE
Determines if the value is a concrete number.
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Returns position of most significant set bit; zero when no bits are set.
static SValuePtr instance_bottom(size_t nbits)
Instantiate a new data-flow-bottom value of specified width.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to an interval memory state.
bool isEmpty() const
Determine whether the container is empty.
Definition: IntervalSet.h:299
virtual uint64_t get_number() const ROSE_OVERRIDE
Return the concrete number for this value.
Holds a value or nothing.
Definition: Optional.h:49
static MemoryStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiate a new memory state with prototypical value.
virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Returns position of least significant set bit; zero when no bits are set.
static SValuePtr instance_hull(size_t nbits, uint64_t v1, uint64_t v2)
Instantiate a new value that's constrained to be between two unsigned values, inclusive.
virtual bool isBottom() const ROSE_OVERRIDE
Determines whether a value is a data-flow bottom.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE
Sign extends a value.
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 unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two unsigned 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.
virtual SValuePtr svalue_from_intervals(size_t nbits, const Intervals &intervals)
Create a new SValue from a set of intervals.
Main namespace for the ROSE library.
Describes (part of) a physical CPU register.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE
Data-flow bottom 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.
void insert(const Interval2 &interval)
Insert specified values.
Definition: IntervalSet.h:532
static SValuePtr instance_unspecified(size_t nbits)
Instantiate a new unspecified value of specific width.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise XOR of two values.
boost::shared_ptr< class RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
virtual void print(std::ostream &output, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print a value to a stream using default format.
boost::shared_ptr< class State > StatePtr
Shared-ownership pointer to a semantic state.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the right.
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 ...
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) ROSE_OVERRIDE
Extracts bits from a value.
static SValuePtr instance_intervals(size_t nbits, const Intervals &intervals)
Instantiate a new value from a set of intervals.
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.
Base classes for instruction semantics.
virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
If-then-else.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with unsigned values.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
static Interval hull(T v1, T v2)
Construct an interval from two endpoints.
Definition: Interval.h:150
static SValuePtr instance_undefined(size_t nbits)
Instantiate a new undefined value of particular width.
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Two's complement.
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise OR of two values.
static SValuePtr instance()
Instantiate a new prototypical value.
Sawyer::Container::IntervalSet< Interval > Intervals
Set of intervals.
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 concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Concatenates the bits of two values.
Defines registers available for a particular architecture.
Definition: Registers.h:32
static MemoryStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiate a new memory state with specified prototypical cells and values.
void set_intervals(const Intervals &intervals)
Changes the rangemap stored in the value.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
static SValuePtr instance_from_bits(size_t nbits, uint64_t possible_bits)
Create a value from a set of possible bits.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to an IntevalSemantics value.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Determines whether a value is equal to zero.
static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SmtSolver *solver=NULL)
Instantiates a new RiscOperators with specified state.
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Write a byte to memory.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, SmtSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual SValuePtr create_from_bits(size_t nbits, uint64_t possible_bits)
Generate ranges from bits.
Scalar least() const
Returns the minimum scalar contained in this set.
Definition: IntervalSet.h:408
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer to an interval semantic value.
static StatePtr instance(const RegisterStatePtr &registers, const MemoryStatePtr &memory)
Instantiate a new state object with specified register and memory states.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
Range of values delimited by endpoints.
Definition: Interval.h:33
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 number_(size_t nbits, uint64_t number) const ROSE_OVERRIDE
Create a new concrete semantic value.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiplies two signed values.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to interval RISC operations.
uint64_t possible_bits() const
Returns all possible bits that could be set.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the left.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Adds two integers of equal size.
virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual allocating copy constructor.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted left.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Interval::Value size() const
Number of scalar elements represented.
Definition: IntervalSet.h:308
virtual SValuePtr create(size_t nbits, const Intervals &intervals)
Construct a ValueType from a rangemap.
virtual const std::string & name() const
Property: Name used for debugging.
Scalar greatest() const
Returns the maximum scalar contained in this set.
Definition: IntervalSet.h:414
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE
Create a new unspecified semantic value.
Type of values manipulated by the IntervalSemantics domain.
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 readMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Read a byte from memory.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, SmtSolver *solver=NULL) const ROSE_OVERRIDE
Returns true if two values must be equal.
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
One'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 SValuePtr svalue_from_bits(size_t nbits, uint64_t possible_bits)
Create a new SValue from a set of possible bits.