ROSE  0.11.2.0
SymbolicSemantics2.h
1 #ifndef Rose_SymbolicSemantics2_H
2 #define Rose_SymbolicSemantics2_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 "BaseSemantics2.h"
12 #include "Cxx_GrammarSerialization.h"
13 #include "BinarySmtSolver.h"
14 #include "BinarySymbolicExpr.h"
15 #include "RegisterStateGeneric.h"
16 #include "MemoryCellList.h"
17 #include "MemoryCellMap.h"
18 
19 #include <boost/serialization/access.hpp>
20 #include <boost/serialization/base_object.hpp>
21 #include <boost/serialization/export.hpp>
22 #include <boost/serialization/set.hpp>
23 
24 #include <map>
25 #include <vector>
26 
27 namespace Rose {
28 namespace BinaryAnalysis { // documented elsewhere
29 namespace InstructionSemantics2 { // documented elsewhere
30 
49 namespace SymbolicSemantics {
50 
57 typedef std::set<SgAsmInstruction*> InsnSet;
58 
60 // Boolean flags
62 
64 namespace AllowSideEffects {
65  enum Flag {NO, YES};
66 }
67 
68 
70 // Merging symbolic values
72 
75 
78  size_t setSizeLimit_;
79 protected:
80  Merger(): BaseSemantics::Merger(), setSizeLimit_(1) {}
81 
82 public:
84  typedef MergerPtr Ptr;
85 
87  static Ptr instance() {
88  return Ptr(new Merger);
89  }
90 
92  static Ptr instance(size_t n) {
93  Ptr retval = Ptr(new Merger);
94  retval->setSizeLimit(n);
95  return retval;
96  }
97 
109  size_t setSizeLimit() const { return setSizeLimit_; }
110  void setSizeLimit(size_t n) { setSizeLimit_ = n; }
112 };
113 
114 
115 
117 // Semantic values
119 
122 
125 public:
126  SymbolicExpr::Formatter expr_formatter;
127 };
128 
198 public:
200 
201 protected:
203  ExprPtr expr;
204 
207  InsnSet defs;
208 
210  // Serialization
211 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
212 private:
213  friend class boost::serialization::access;
214 
215  template<class S>
216  void serialize(S &s, const unsigned /*version*/) {
217  roseAstSerializationRegistration(s); // "defs" has SgAsmInstruction ASTs
218  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
219  s & BOOST_SERIALIZATION_NVP(expr);
220  s & BOOST_SERIALIZATION_NVP(defs);
221  }
222 #endif
223 
225  // Real constructors
226 protected:
227  SValue() {} // needed for serialization
228  explicit SValue(size_t nbits): BaseSemantics::SValue(nbits) {
229  expr = SymbolicExpr::makeIntegerVariable(nbits);
230  }
231  SValue(size_t nbits, uint64_t number): BaseSemantics::SValue(nbits) {
232  expr = SymbolicExpr::makeIntegerConstant(nbits, number);
233  }
234  SValue(ExprPtr expr): BaseSemantics::SValue(expr->nBits()) {
235  this->expr = expr;
236  }
237 
239  // Static allocating constructors
240 public:
242  static SValuePtr instance() {
244  }
245 
247  static SValuePtr instance_bottom(size_t nbits) {
249  }
250 
252  static SValuePtr instance_undefined(size_t nbits) {
254  }
255 
257  static SValuePtr instance_unspecified(size_t nbits) {
259  }
260 
262  static SValuePtr instance_integer(size_t nbits, uint64_t value) {
263  return SValuePtr(new SValue(SymbolicExpr::makeIntegerConstant(nbits, value)));
264  }
265 
267  // Virtual allocating constructors
268 public:
269  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE {
270  return instance_bottom(nbits);
271  }
272  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE {
273  return instance_undefined(nbits);
274  }
275  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE {
276  return instance_unspecified(nbits);
277  }
278  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE {
279  return instance_integer(nbits, value);
280  }
281  virtual BaseSemantics::SValuePtr boolean_(bool value) const ROSE_OVERRIDE {
282  return instance_integer(1, value?1:0);
283  }
284  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
285  SValuePtr retval(new SValue(*this));
286  if (new_width!=0 && new_width!=retval->get_width())
287  retval->set_width(new_width);
288  return retval;
289  }
292  const SmtSolverPtr&) const ROSE_OVERRIDE;
293 
295  // Dynamic pointer casts
296 public:
298  static SValuePtr promote(const BaseSemantics::SValuePtr &v) { // hot
299  SValuePtr retval = v.dynamicCast<SValue>();
300  ASSERT_not_null(retval);
301  return retval;
302  }
303 
305  // Override virtual methods...
306 public:
307  virtual bool may_equal(const BaseSemantics::SValuePtr &other,
308  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;
309  virtual bool must_equal(const BaseSemantics::SValuePtr &other,
310  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;
311 
312  // It's not possible to change the size of a symbolic expression in place. That would require that we recursively change
313  // the size of the SymbolicExpr, which might be shared with many unrelated values whose size we don't want to affect.
314  virtual void set_width(size_t nbits) ROSE_OVERRIDE {
315  ASSERT_require(nbits==get_width());
316  }
317 
318  virtual bool isBottom() const ROSE_OVERRIDE;
319 
320  virtual bool is_number() const ROSE_OVERRIDE {
321  return expr->isIntegerConstant();
322  }
323 
324  virtual uint64_t get_number() const ROSE_OVERRIDE;
325 
326  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
327 
328  virtual std::string get_comment() const ROSE_OVERRIDE;
329  virtual void set_comment(const std::string&) const ROSE_OVERRIDE;
330 
332  // Additional methods first declared in this class...
333 public:
341  virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const;
342 
349  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3) {
351  defined_by(insn, set1, set2);
352  }
353  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2) {
355  defined_by(insn, set1);
356  }
357  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1) {
359  defined_by(insn);
360  }
361  virtual void defined_by(SgAsmInstruction *insn) {
363  }
369  virtual const ExprPtr& get_expression() const {
370  return expr;
371  }
372 
375  virtual void set_expression(const ExprPtr &new_expr) {
376  ASSERT_not_null(new_expr);
377  expr = new_expr;
378  width = new_expr->nBits();
379  }
380  virtual void set_expression(const SValuePtr &source) {
381  set_expression(source->get_expression());
382  }
399  virtual const InsnSet& get_defining_instructions() const {
400  return defs;
401  }
402 
408  virtual size_t add_defining_instructions(const InsnSet &to_add);
409  virtual size_t add_defining_instructions(const SValuePtr &source) {
410  return add_defining_instructions(source->get_defining_instructions());
411  }
412  virtual size_t add_defining_instructions(SgAsmInstruction *insn);
420  virtual void set_defining_instructions(const InsnSet &new_defs) {
421  defs = new_defs;
422  }
423  virtual void set_defining_instructions(const SValuePtr &source) {
424  set_defining_instructions(source->get_defining_instructions());
425  }
426  virtual void set_defining_instructions(SgAsmInstruction *insn);
428 };
429 
430 
432 // Register state
434 
435 typedef BaseSemantics::RegisterStateGeneric RegisterState;
436 typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;
437 
438 
440 // List-based Memory state
442 
444 typedef boost::shared_ptr<class MemoryListState> MemoryListStatePtr;
445 
463 public:
464  typedef BaseSemantics::MemoryCellList Super;
465 
467  struct CellCompressor {
468  virtual ~CellCompressor() {}
469  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
471  const MemoryCellList::CellList &cells) = 0;
472  };
473 
488  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
490  const CellList &cells) ROSE_OVERRIDE;
491  };
492 
495  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
497  const CellList &cells) ROSE_OVERRIDE;
498  };
499 
504  CellCompressorMcCarthy cc_mccarthy;
505  CellCompressorSimple cc_simple;
506  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
508  const CellList &cells) ROSE_OVERRIDE;
509  };
510 
511 protected:
515  // Serialization
517 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
518 private:
519  friend class boost::serialization::access;
520 
521  template<class S>
522  void serialize(S &s, const unsigned /*version*/) {
523  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
524  }
525 #endif
526 
527 
529  // Real constructors
530 protected:
531  MemoryListState() // for serialization
532  : cell_compressor(&cc_choice) {}
533 
534  explicit MemoryListState(const BaseSemantics::MemoryCellPtr &protocell)
535  : BaseSemantics::MemoryCellList(protocell), cell_compressor(&cc_choice) {}
536 
537  MemoryListState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
538  : BaseSemantics::MemoryCellList(addrProtoval, valProtoval), cell_compressor(&cc_choice) {}
539 
540  MemoryListState(const MemoryListState &other)
541  : BaseSemantics::MemoryCellList(other), cell_compressor(other.cell_compressor) {}
542 
544  // Static allocating constructors
545 public:
547  static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
548  return MemoryListStatePtr(new MemoryListState(protocell));
549  }
550 
553  static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
554  const BaseSemantics::SValuePtr &valProtoval) {
555  return MemoryListStatePtr(new MemoryListState(addrProtoval, valProtoval));
556  }
557 
559  static MemoryListStatePtr instance(const MemoryListStatePtr &other) {
560  return MemoryListStatePtr(new MemoryListState(*other));
561  }
562 
564  // Virtual constructors
565 public:
569  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
570  return instance(addrProtoval, valProtoval);
571  }
572 
574  virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const ROSE_OVERRIDE {
575  return instance(protocell);
576  }
577 
579  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
581  }
582 
584  // Dynamic pointer casts
585 public:
588  static MemoryListStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
589  MemoryListStatePtr retval = boost::dynamic_pointer_cast<MemoryListState>(x);
590  ASSERT_not_null(retval);
591  return retval;
592  }
593 
595  // Methods we inherited
596 public:
602  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
603 
609  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
610 
614  virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
615  BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
616 
617 protected:
618  BaseSemantics::SValuePtr readOrPeekMemory(const BaseSemantics::SValuePtr &address,
619  const BaseSemantics::SValuePtr &dflt,
622  AllowSideEffects::Flag allowSideEffects);
623 
625  // Methods first declared in this class
626 public:
631  void set_cell_compressor(CellCompressor *cc) { cell_compressor = cc; }
633 };
634 
635 
637 // Map-based Memory state
639 
641 typedef boost::shared_ptr<class MemoryMapState> MemoryMapStatePtr;
642 
661 public:
662  typedef BaseSemantics::MemoryCellMap Super;
663 
665  // Serialization
666 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
667 private:
668  friend class boost::serialization::access;
669 
670  template<class S>
671  void serialize(S &s, const unsigned /*version*/) {
672  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
673  }
674 #endif
675 
677  // Real constructors
678 protected:
679  MemoryMapState() {} // for serialization
680 
681  explicit MemoryMapState(const BaseSemantics::MemoryCellPtr &protocell)
682  : BaseSemantics::MemoryCellMap(protocell) {}
683 
684  MemoryMapState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
685  : BaseSemantics::MemoryCellMap(addrProtoval, valProtoval) {}
686 
688  // Static allocating constructors
689 public:
691  static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
692  return MemoryMapStatePtr(new MemoryMapState(protocell));
693  }
694 
697  static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
698  const BaseSemantics::SValuePtr &valProtoval) {
699  return MemoryMapStatePtr(new MemoryMapState(addrProtoval, valProtoval));
700  }
701 
703  static MemoryMapStatePtr instance(const MemoryMapStatePtr &other) {
704  return MemoryMapStatePtr(new MemoryMapState(*other));
705  }
706 
708  // Virtual constructors
709 public:
713  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
714  return instance(addrProtoval, valProtoval);
715  }
716 
719  return instance(protocell);
720  }
721 
723  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
725  }
726 
728  // Dynamic pointer casts
729 public:
732  static MemoryMapStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
733  MemoryMapStatePtr retval = boost::dynamic_pointer_cast<MemoryMapState>(x);
734  ASSERT_not_null(retval);
735  return retval;
736  }
737 
739  // Methods we override from the super class (documented in the super class)
740 public:
741  virtual CellKey generateCellKey(const BaseSemantics::SValuePtr &addr_) const ROSE_OVERRIDE;
742 };
743 
744 
745 
747 // Default memory state
749 
750 // List-base memory was the type originally used by this domain. We must keep it that way because some analysis, including 3rd
751 // party, assumes that the state is list-based. New analysis can use the map-based state by instantiating it when the symbolic
752 // risc operators are constructed.
753 typedef MemoryListState MemoryState;
754 typedef MemoryListStatePtr MemoryStatePtr;
755 
757 // Complete state
759 
760 typedef BaseSemantics::State State;
761 typedef BaseSemantics::StatePtr StatePtr;
762 
763 
765 // RISC operators
767 
773 };
774 
780 };
781 
783 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
784 
805 public:
806  typedef BaseSemantics::RiscOperators Super;
807 
808 protected:
809  bool omit_cur_insn; // if true, do not include cur_insn as a definer
810  DefinersMode computingDefiners_; // whether to track definers (instruction VAs) of SValues
811  WritersMode computingMemoryWriters_; // whether to track writers (instruction VAs) to memory.
812  WritersMode computingRegisterWriters_; // whether to track writers (instruction VAs) to registers.
813  size_t trimThreshold_; // max size of expressions (zero means no maximimum)
814  bool reinterpretMemoryReads_; // cast data to unsigned integer when reading from memory
815  bool reinterpretRegisterReads_; // cast data to unsigned integer when reading from registers
816 
817 
819  // Serialization
820 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
821 private:
822  friend class boost::serialization::access;
823 
824  template<class S>
825  void serialize(S &s, const unsigned /*version*/) {
826  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
827  s & BOOST_SERIALIZATION_NVP(omit_cur_insn);
828  s & BOOST_SERIALIZATION_NVP(computingDefiners_);
829  s & BOOST_SERIALIZATION_NVP(computingMemoryWriters_);
830  s & BOOST_SERIALIZATION_NVP(computingRegisterWriters_);
831  s & BOOST_SERIALIZATION_NVP(trimThreshold_);
832  }
833 #endif
834 
836  // Real constructors
837 protected:
838  RiscOperators() // for serialization
839  : omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS), computingMemoryWriters_(TRACK_LATEST_WRITER),
840  computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0), reinterpretMemoryReads_(true),
841  reinterpretRegisterReads_(true) {}
842 
844  : BaseSemantics::RiscOperators(protoval, solver), omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS),
845  computingMemoryWriters_(TRACK_LATEST_WRITER), computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0),
846  reinterpretMemoryReads_(true), reinterpretRegisterReads_(true) {
847  name("Symbolic");
848  ASSERT_always_not_null(protoval);
849  ASSERT_always_not_null2(protoval.dynamicCast<SValue>(),
850  "SymbolicSemantics supports only symbolic SValue types or derivatives thereof");
851  }
852 
853  explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr())
854  : BaseSemantics::RiscOperators(state, solver), omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS),
855  computingMemoryWriters_(TRACK_LATEST_WRITER), computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0),
856  reinterpretMemoryReads_(true), reinterpretRegisterReads_(true) {
857  name("Symbolic");
858  ASSERT_always_not_null(state);
859  ASSERT_always_not_null(state->registerState());
860  ASSERT_always_not_null2(boost::dynamic_pointer_cast<RegisterState>(state->registerState()),
861  "SymbolicSemantics supports only RegisterStateGeneric or derivatives thereof");
862  ASSERT_always_not_null(state->protoval());
863  ASSERT_always_not_null2(state->protoval().dynamicCast<SValue>(),
864  "SymbolicSemantics supports only symbolic SValue types or derivatives thereof");
865  }
866 
868  // Static allocating constructors
869 public:
872  static RiscOperatorsPtr instance(const RegisterDictionary *regdict, const SmtSolverPtr &solver = SmtSolverPtr()) {
874  BaseSemantics::RegisterStatePtr registers = RegisterState::instance(protoval, regdict);
875  BaseSemantics::MemoryStatePtr memory = MemoryListState::instance(protoval, protoval);
876  BaseSemantics::StatePtr state = State::instance(registers, memory);
877  return RiscOperatorsPtr(new RiscOperators(state, solver));
878  }
879 
882  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr()) {
883  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
884  }
885 
888  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr()) {
889  return RiscOperatorsPtr(new RiscOperators(state, solver));
890  }
891 
893  // Virtual constructors
894 public:
896  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
897  return instance(protoval, solver);
898  }
899 
901  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
902  return instance(state, solver);
903  }
904 
906  // Dynamic pointer casts
907 public:
910  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
911  RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
912  ASSERT_not_null(retval);
913  return retval;
914  }
915 
917  // Inherited methods for constructing values.
918 public:
919  virtual BaseSemantics::SValuePtr boolean_(bool b) ROSE_OVERRIDE {
920  SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::boolean_(b));
921  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
922  retval->defined_by(currentInstruction());
923  return retval;
924  }
925 
926  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) ROSE_OVERRIDE {
927  SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
928  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
929  retval->defined_by(currentInstruction());
930  return retval;
931  }
932 
934  // New methods for constructing values, so we don't have to write so many SValue::promote calls in the RiscOperators
935  // implementations.
936 protected:
937  SValuePtr svalue_expr(const ExprPtr &expr, const InsnSet &defs=InsnSet()) {
938  SValuePtr newval = SValue::promote(protoval()->undefined_(expr->nBits()));
939  newval->set_expression(expr);
940  newval->set_defining_instructions(defs);
941  return newval;
942  }
943 
944  SValuePtr svalue_undefined(size_t nbits) {
945  return SValue::promote(undefined_(nbits));
946  }
947 
948  SValuePtr svalue_bottom(size_t nbits) {
949  return SValue::promote(bottom_(nbits));
950  }
951 
952  SValuePtr svalue_unspecified(size_t nbits) {
953  return SValue::promote(unspecified_(nbits));
954  }
955 
956  SValuePtr svalue_number(size_t nbits, uint64_t value) {
957  return SValue::promote(number_(nbits, value));
958  }
959 
960  SValuePtr svalue_boolean(bool b) {
961  return SValue::promote(boolean_(b));
962  }
963 
965  // Configuration properties
966 public:
967 
985  void computingDefiners(DefinersMode m) { computingDefiners_ = m; }
986  DefinersMode computingDefiners() const { return computingDefiners_; }
1007  void computingMemoryWriters(WritersMode m) { computingMemoryWriters_ = m; }
1008  WritersMode computingMemoryWriters() const { return computingMemoryWriters_; }
1032  void computingRegisterWriters(WritersMode m) { computingRegisterWriters_ = m; }
1033  WritersMode computingRegisterWriters() const { return computingRegisterWriters_; }
1036  // Used internally to control whether cur_insn should be omitted from the list of definers.
1037  bool getset_omit_cur_insn(bool b) { bool retval = omit_cur_insn; omit_cur_insn=b; return retval; }
1038 
1045  void trimThreshold(size_t n) { trimThreshold_ = n; }
1046  size_t trimThreshold() const { return trimThreshold_; }
1056  bool reinterpretMemoryReads() const { return reinterpretMemoryReads_; }
1057  void reinterpretMemoryReads(bool b) { reinterpretMemoryReads_ = b; }
1058  bool reinterpretRegisterReads() const { return reinterpretRegisterReads_; }
1059  void reinterpretRegisterReads(bool b) { reinterpretRegisterReads_ = b; }
1062  // Methods first defined at this level of the class hierarchy
1064 public:
1126  virtual void substitute(const SValuePtr &from, const SValuePtr &to);
1127 
1133 
1139 
1144 
1146  // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
1147 public:
1148  virtual void interrupt(int majr, int minr) ROSE_OVERRIDE;
1149  virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
1150  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1151  virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_,
1152  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1153  virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
1154  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1155  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1156  virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
1157  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
1158  virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_,
1159  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1160  virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1161  virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1162  virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_,
1163  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1164  virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_,
1165  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1166  virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_,
1167  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1168  virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_,
1169  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1170  virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_,
1171  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1172  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1173  virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
1174  const BaseSemantics::SValuePtr &a_,
1175  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1176  virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
1177  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
1178  virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_,
1179  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1181  const BaseSemantics::SValuePtr &b_,
1182  const BaseSemantics::SValuePtr &c_,
1183  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
1184  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1186  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1188  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1190  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1192  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1194  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1196  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1198  SgAsmFloatType *retType) ROSE_OVERRIDE;
1200  virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg,
1201  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
1202  virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg,
1203  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
1204  virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1205  virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg,
1206  const BaseSemantics::SValuePtr &addr,
1207  const BaseSemantics::SValuePtr &dflt,
1208  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
1209  virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg,
1210  const BaseSemantics::SValuePtr &addr,
1211  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
1212  virtual void writeMemory(RegisterDescriptor segreg,
1213  const BaseSemantics::SValuePtr &addr,
1214  const BaseSemantics::SValuePtr &data,
1215  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
1216 
1217 public:
1218  BaseSemantics::SValuePtr readOrPeekMemory(RegisterDescriptor segreg,
1219  const BaseSemantics::SValuePtr &addr,
1220  const BaseSemantics::SValuePtr &dflt,
1221  AllowSideEffects::Flag);
1222 };
1223 
1224 } // namespace
1225 } // namespace
1226 } // namespace
1227 } // namespace
1228 
1229 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1234 #endif
1235 
1236 #endif
1237 #endif
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with signed values.
Sawyer::SharedPointer< class Merger > MergerPtr
Shared-ownership pointer for a merge control object.
void computingDefiners(DefinersMode m)
Property: Track which instructions define a semantic value.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const ROSE_OVERRIDE
Print a value to a stream using default format.
virtual void writeMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE
Writes a value to memory.
static RegisterStateGenericPtr instance(const SValuePtr &protoval, const RegisterDictionary *regdict)
Instantiate a new register state.
boost::shared_ptr< class MemoryCell > MemoryCellPtr
Shared-ownership pointer to a semantic memory cell.
Definition: MemoryCell.h:17
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< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual void set_defining_instructions(const InsnSet &new_defs)
Set defining instructions.
bool reinterpretMemoryReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
static SValuePtr instance_integer(size_t nbits, uint64_t value)
Instantiate a new concrete value.
Leaf node of an expression tree for instruction semantics.
Defines RISC operators for the SymbolicSemantics domain.
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
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 void set_expression(const SValuePtr &source)
Changes the expression stored in the value.
static MemoryMapStatePtr promote(const BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
Interior node of an expression tree for instruction semantics.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Returns true if two values must be equal.
CellCompressor * cell_compressor
Callback when a memory read aliases multiple memory cells.
static CellCompressorChoice cc_choice
The default cell compressor.
static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified state.
virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const
Substitute one value for another throughout a value.
virtual BaseSemantics::SValuePtr filterResult(const BaseSemantics::SValuePtr &)
Filters results from RISC operators.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two signed values.
virtual void set_comment(const std::string &) const ROSE_OVERRIDE
Some subclasses support the ability to add comments to values.
Base class for machine instructions.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual copy constructor.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const ROSE_OVERRIDE
Virtual constructor.
virtual uint64_t get_number() const ROSE_OVERRIDE
Return the concrete number for this value.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2)
Adds instructions to the list of defining instructions.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Returns true if two values could be equal.
static RiscOperatorsPtr instance(const RegisterDictionary *regdict, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object and configures it to use semantic values and states that are ...
void computingRegisterWriters(WritersMode m)
Property: Track latest writer to each register.
virtual bool is_number() const ROSE_OVERRIDE
Determines if the value is a concrete number.
Functor for handling a memory read whose address matches more than one memory cell.
virtual size_t add_defining_instructions(const SValuePtr &source)
Adds definitions to the list of defining instructions.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a SymbolicSemantics value.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual allocating constructor.
STL namespace.
Holds a value or nothing.
Definition: Optional.h:49
static const unsigned UNSPECIFIED
Value is somehow unspecified.
virtual void set_defining_instructions(const SValuePtr &source)
Set defining instructions.
void set_cell_compressor(CellCompressor *cc)
Callback for handling a memory read whose address matches more than one memory cell.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x)
Run-time promotion of a base RiscOperators pointer to symbolic operators.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE
Create a new concrete semantic value.
virtual void interrupt(int majr, int minr) ROSE_OVERRIDE
Invoked for instructions that cause an interrupt.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
void reinterpretRegisterReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiplies two signed values.
virtual void defined_by(SgAsmInstruction *insn)
Adds instructions to the list of defining instructions.
Main namespace for the ROSE library.
Functor for handling a memory read whose address matches more than one memory cell.
Controls formatting of expression trees when printing.
virtual void set_expression(const ExprPtr &new_expr)
Changes the expression stored in the value.
static MemoryListStatePtr promote(const BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
virtual bool isBottom() const ROSE_OVERRIDE
Determines whether a value is a data-flow bottom.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE
Virtual constructor.
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
void reinterpretMemoryReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
Reads a value from a register.
virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Writes a value to a register.
Sawyer::SharedPointer< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
static SValuePtr instance_bottom(size_t nbits)
Instantiate a new data-flow bottom value of specified width.
WritersMode computingMemoryWriters() const
Property: Track which instructions write to each memory location.
static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
virtual SymbolicExpr::Type sgTypeToSymbolicType(SgAsmType *)
Convert a SgAsmType to a symbolic type.
static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
DefinersMode
How to update the list of definers stored in each semantic value.
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.
void computingMemoryWriters(WritersMode m)
Property: Track which instructions write to each memory location.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
WritersMode computingRegisterWriters() const
Property: Track latest writer to each register.
static SValuePtr instance_undefined(size_t nbits)
Instantiate a new undefined value of specified width.
Describes (part of) a physical CPU register.
Functor for handling a memory read that found more than one cell that might alias the requested addre...
boost::shared_ptr< class MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to symbolic memory state.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const
Virtual constructor.
static SValuePtr instance()
Instantiate a new prototypical value.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual const InsnSet & get_defining_instructions() const
Returns the set of instructions that defined this value.
static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
DefinersMode computingDefiners() const
Property: Track which instructions define a semantic value.
virtual std::string get_comment() const ROSE_OVERRIDE
Some subclasses support the ability to add comments to values.
virtual const ExprPtr & get_expression() const
Returns the expression stored in this value.
bool reinterpretRegisterReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified prototypical values.
virtual void substitute(const SValuePtr &from, const SValuePtr &to)
Substitute all occurrences of from with to in the current state.
WritersMode
How to update the list of writers stored at each abstract location.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
CellCompressor * get_cell_compressor() const
Callback for handling a memory read whose address matches more than one memory cell.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiply two unsigned values.
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Two's complement.
virtual void set_width(size_t nbits) ROSE_OVERRIDE
Accessor for value width.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE
Virtual constructor.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE
Create a new unspecified semantic value.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two unsigned values.
std::list< MemoryCellPtr > CellList
List of memory cells.
Base class for binary types.
size_t trimThreshold() const
Property: Maximum size of expressions.
Type of values manipulated by the SymbolicSemantics domain.
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::SValuePtr peekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
Read memory without side effects.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1)
Adds instructions to the list of defining instructions.
static SValuePtr instance_unspecified(size_t nbits)
Instantiate a new unspecified value of specified width.
virtual BaseSemantics::SValuePtr reinterpret(const BaseSemantics::SValuePtr &, SgAsmType *) ROSE_OVERRIDE
Reinterpret an expression as a different type.
virtual BaseSemantics::SValuePtr boolean_(bool value) const ROSE_OVERRIDE
Create a new, Boolean value.
virtual CellKey generateCellKey(const BaseSemantics::SValuePtr &addr_) const ROSE_OVERRIDE
Generate a cell lookup key.
virtual size_t get_width() const
Accessor for value width.
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 BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE
Create a new undefined semantic value.
virtual size_t add_defining_instructions(const InsnSet &to_add)
Adds definitions to the list of defining instructions.
static MemoryMapStatePtr instance(const MemoryMapStatePtr &other)
Instantiates a new deep copy of an existing state.
Base class for symbolic expression nodes.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE
Data-flow bottom value.
virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr &a, SgAsmFloatType *aType, SgAsmFloatType *retType) ROSE_OVERRIDE
Convert from one floating-point type to another.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with unsigned values.
Defines registers available for a particular architecture.
Definition: Registers.h:38
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual copy constructor.
virtual const std::string & name() const
Property: Name used for debugging.
void trimThreshold(size_t n)
Property: Maximum size of expressions.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3)
Adds instructions to the list of defining instructions.
static MemoryListStatePtr instance(const MemoryListStatePtr &other)
Instantiates a new deep copy of an existing state.
MergerPtr Ptr
Shared-ownership pointer for a Merger object.
virtual BaseSemantics::SValuePtr peekMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Read a byte from memory with no side effects.
Functor for handling a memory read whose address matches more than one memory cell.
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.
Floating point types.
virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
Obtain a register value without side effects.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
static SgAsmFloatType * sgIsIeee754(SgAsmType *)
Tests whether a SgAsmType is an IEEE-754 floating-point type.
boost::shared_ptr< class MemoryListState > MemoryListStatePtr
Shared-ownership pointer for symbolic list-based memory state.