ROSE  0.10.0.0
PartialSymbolicSemantics2.h
1 #ifndef Rose_PartialSymbolicSemantics2_H
2 #define Rose_PartialSymbolicSemantics2_H
3 #include <rosePublicConfig.h>
4 #ifdef ROSE_BUILD_BINARY_ANALYSIS_SUPPORT
5 
6 #ifndef __STDC_FORMAT_MACROS
7 #define __STDC_FORMAT_MACROS
8 #endif
9 #include <inttypes.h>
10 
11 #include <map>
12 #include <stdint.h>
13 #include <vector>
14 
15 #include "rosePublicConfig.h"
16 #ifdef ROSE_HAVE_LIBGCRYPT
17 #include <gcrypt.h>
18 #endif
19 
20 #include "BaseSemantics2.h"
21 #include "integerOps.h"
22 #include "MemoryMap.h"
23 #include "FormatRestorer.h"
24 #include "RegisterStateGeneric.h"
25 #include "MemoryCellList.h"
26 
27 namespace Rose {
28 namespace BinaryAnalysis { // documented elsewhere
29 namespace InstructionSemantics2 { // documented elsewhere
30 
44 namespace PartialSymbolicSemantics {
45 
46 extern uint64_t name_counter;
47 
49 // Print formatter
51 
55 protected:
56  typedef std::map<uint64_t, uint64_t> Map;
57  Map renames;
58  size_t next_name;
59 public:
60  Formatter(): next_name(1) {}
61  uint64_t rename(uint64_t orig_name);
62 };
63 
64 
66 // Semantic values
68 
71 
75 public:
76  uint64_t name;
77  uint64_t offset;
78  bool negate;
80  // Real constructors
82 protected:
83  explicit SValue(size_t nbits)
84  : BaseSemantics::SValue(nbits), name(++name_counter), offset(0), negate(false) {}
85 
86  SValue(size_t nbits, uint64_t number)
87  : BaseSemantics::SValue(nbits), name(0), offset(number), negate(false) {
88  if (nbits <= 64) {
89  this->offset &= IntegerOps::genMask<uint64_t>(nbits);
90  } else {
91  name = ++name_counter;
92  offset = 0;
93  }
94  }
95 
96  SValue(size_t nbits, uint64_t name, uint64_t offset, bool negate)
97  : BaseSemantics::SValue(nbits), name(name), offset(offset), negate(negate) {
98  this->offset &= IntegerOps::genMask<uint64_t>(nbits);
99  }
100 
102  // Static allocating constructors
103 public:
105  static SValuePtr instance() {
106  return SValuePtr(new SValue(1));
107  }
108 
110  static SValuePtr instance(size_t nbits) {
111  return SValuePtr(new SValue(nbits));
112  }
113 
115  static SValuePtr instance(size_t nbits, uint64_t value) {
116  return SValuePtr(new SValue(nbits, value));
117  }
118 
120  static SValuePtr instance(size_t nbits, uint64_t name, uint64_t offset, bool negate) {
121  return SValuePtr(new SValue(nbits, name, offset, negate));
122  }
123 
125  // Virtual constructors
126 public:
127  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE {
128  return instance(nbits);
129  }
130  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE {
131  return instance(nbits);
132  }
133  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE {
134  return instance(nbits);
135  }
136 
137  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE {
138  return instance(nbits, value);
139  }
140 
141  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
142  SValuePtr retval(new SValue(*this));
143  if (new_width!=0 && new_width!=retval->get_width())
144  retval->set_width(new_width);
145  return retval;
146  }
147 
150  const SmtSolverPtr&) const ROSE_OVERRIDE;
151 
153  virtual BaseSemantics::SValuePtr create(size_t nbits, uint64_t name, uint64_t offset, bool negate) const {
154  return instance(nbits, name, offset, negate);
155  }
156 
158  // Dynamic pointer casts
159 public:
162  static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
163  SValuePtr retval = v.dynamicCast<SValue>();
164  ASSERT_not_null(retval);
165  return retval;
166  }
167 
169  // Other stuff we inherited from the super class
170 public:
171  virtual void set_width(size_t nbits) ROSE_OVERRIDE {
173  offset &= IntegerOps::genMask<uint64_t>(nbits);
174  }
175 
176  virtual bool may_equal(const BaseSemantics::SValuePtr &other,
177  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;
178  virtual bool must_equal(const BaseSemantics::SValuePtr &other,
179  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;
180 
181  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
182 
183  virtual bool isBottom() const ROSE_OVERRIDE {
184  return false;
185  }
186 
187  virtual bool is_number() const ROSE_OVERRIDE {
188  return 0==name;
189  }
190 
191  virtual uint64_t get_number() const ROSE_OVERRIDE {
192  ASSERT_require(is_number());
193  return offset;
194  }
195 };
196 
197 
199 // Register state
201 
202 typedef BaseSemantics::RegisterStateGeneric RegisterState;
203 typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;
204 
205 
207 // Memory state
209 
210 // PartialSymbolicSemantics uses BaseSemantics::MemoryCellList (or subclass) as its memory state, and does not expect the
211 // MemoryCellList to be byte-restricted (i.e., the cells can store multi-byte values).
212 
213 typedef BaseSemantics::MemoryCellList MemoryState;
214 typedef BaseSemantics::MemoryCellListPtr MemoryStatePtr;
215 
216 
218 // Complete state
220 
222 typedef boost::shared_ptr<class State> StatePtr;
223 
226 class State: public BaseSemantics::State {
227 
229  // Real constructors
230 protected:
231  State(const BaseSemantics::RegisterStatePtr &registers,
232  const BaseSemantics::MemoryStatePtr &memory)
233  : BaseSemantics::State(registers, memory) {
234  // This state should use PartialSymbolicSemantics values (or subclasses thereof)
235  ASSERT_not_null(registers);
236  (void) SValue::promote(registers->protoval());
237  ASSERT_not_null(memory);
238  (void) SValue::promote(memory->get_addr_protoval());
239  (void) SValue::promote(memory->get_val_protoval());
240 
241  // This state should use a memory that is not byte restricted.
242  MemoryStatePtr mcl = MemoryState::promote(memory);
243  ASSERT_require(!mcl->byteRestricted());
244  }
245 
246  State(const State &other): BaseSemantics::State(other) {}
247 
249  // Static allocating constructors
250 public:
252  static StatePtr instance(const BaseSemantics::RegisterStatePtr &registers,
253  const BaseSemantics::MemoryStatePtr &memory) {
254  return StatePtr(new State(registers, memory));
255  }
256 
258  static StatePtr instance(const StatePtr &other) {
259  return StatePtr(new State(*other));
260  }
261 
263  // Virtual constructors
264 public:
265  virtual BaseSemantics::StatePtr create(const BaseSemantics::RegisterStatePtr &registers,
266  const BaseSemantics::MemoryStatePtr &memory) const ROSE_OVERRIDE {
267  return instance(registers, memory);
268  }
269 
270  virtual BaseSemantics::StatePtr clone() const ROSE_OVERRIDE {
271  StatePtr self = promote(boost::const_pointer_cast<BaseSemantics::State>(shared_from_this()));
272  return instance(self);
273  }
274 
276  // Dynamic pointer casts
277 public:
278  static StatePtr promote(const BaseSemantics::StatePtr &x) {
279  StatePtr retval = boost::dynamic_pointer_cast<State>(x);
280  ASSERT_not_null(x);
281  return retval;
282  }
283 
285  // Methods first declared at this level of the class hierarchy
286 public:
289  virtual void print_diff_registers(std::ostream&, const StatePtr &other_state, Formatter&) const;
290 
292  virtual bool equal_registers(const StatePtr &other) const;
293 
296  virtual void discard_popped_memory();
297 };
298 
299 
301 // RISC operators
303 
305 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
306 
309 protected:
310  MemoryMap::Ptr map;
311 
313  // Real constructors
314 protected:
316  : BaseSemantics::RiscOperators(protoval, solver) {
317  name("PartialSymbolic");
318  }
319  explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr())
321  name("PartialSymbolic");
322  }
323 
325  // Static allocating constructors
326 public:
329  static RiscOperatorsPtr instance(const RegisterDictionary *regdict);
330 
332  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr()) {
333  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
334  }
335 
337  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr()) {
338  return RiscOperatorsPtr(new RiscOperators(state, solver));
339  }
340 
342  // Virtual constructors
343 public:
345  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
346  return instance(protoval, solver);
347  }
348 
350  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
351  return instance(state, solver);
352  }
353 
355  // Dynamic pointer casts
356 public:
359  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
360  RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
361  ASSERT_not_null(retval);
362  return retval;
363  }
364 
366  // Methods first declared at this level of the class hierarchy
367 public:
372  const MemoryMap::Ptr get_memory_map() const { return map; }
373  void set_memory_map(const MemoryMap::Ptr &m) { map = m; }
376  // Risc operators inherited
378 public:
379  virtual void interrupt(int majr, int minr) ROSE_OVERRIDE;
380  virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
381  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
383  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
384  virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
385  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
386  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
387  virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
388  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
389  virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_,
390  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
391  virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
392  virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
393  virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_,
394  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
395  virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_,
396  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
397  virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_,
398  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
399  virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_,
400  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
401  virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_,
402  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
403  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
404  virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
405  const BaseSemantics::SValuePtr &a_,
406  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
407  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
409  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
411  const BaseSemantics::SValuePtr &b_,
412  const BaseSemantics::SValuePtr &c_,
413  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
414  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
416  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
418  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
420  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
422  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
424  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
426  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
428  const BaseSemantics::SValuePtr &addr,
429  const BaseSemantics::SValuePtr &dflt,
430  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
432  const BaseSemantics::SValuePtr &addr,
433  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
434  virtual void writeMemory(RegisterDescriptor segreg,
435  const BaseSemantics::SValuePtr &addr,
436  const BaseSemantics::SValuePtr &data,
437  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
438 
439 protected:
440  BaseSemantics::SValuePtr readOrPeekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &address,
441  const BaseSemantics::SValuePtr &dflt_, bool allowSideEffects);
442 };
443 
444 } // namespace
445 } // namespace
446 } // namespace
447 } // namespace
448 
449 #endif
450 #endif
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with signed values.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual BaseSemantics::SValuePtr 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 bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Returns true if two values could be equal.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE
Create a new unspecified semantic value.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE
Create a new undefined semantic value.
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.
Holds a value or nothing.
Definition: Optional.h:49
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer to a partial-symbolic semantic value.
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 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 create(size_t nbits, uint64_t name, uint64_t offset, bool negate) const
Virtual allocating constructor.
static SValuePtr instance(size_t nbits)
Instantiate a new undefined value of specified width.
Reference-counting smart pointer.
Definition: SharedPointer.h:67
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.
virtual void set_width(size_t nbits) ROSE_OVERRIDE
Accessor for value width.
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.
void set_memory_map(const MemoryMap::Ptr &m)
A memory map can be used to provide default values for memory cells that are read before being writte...
static StatePtr instance(const BaseSemantics::RegisterStatePtr &registers, const BaseSemantics::MemoryStatePtr &memory)
Instantiates a new instance of memory state with specified register and memory states.
Describes (part of) a physical CPU register.
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
Used for printing RISC operators with formatting.
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.
virtual bool is_number() const ROSE_OVERRIDE
Determines if the value is a concrete number.
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.
Defines registers available for a particular architecture.
Definition: Registers.h:38
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
virtual const std::string & name() const
Property: Name used for debugging.
static StatePtr instance(const StatePtr &other)
Instantiates a new copy of an existing state.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print a value to a stream using default format.
virtual void discard_popped_memory()
Removes from memory those values at addresses below the current stack pointer.
static SValuePtr instance(size_t nbits, uint64_t value)
Instantiate a new concrete value.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a PartialSymbolicSemantics value.