ROSE  0.9.9.109
SymbolicSemantics2.h
1 #ifndef Rose_SymbolicSemantics2_H
2 #define Rose_SymbolicSemantics2_H
3 
4 #ifndef __STDC_FORMAT_MACROS
5 #define __STDC_FORMAT_MACROS
6 #endif
7 #include <inttypes.h>
8 
9 #include "BaseSemantics2.h"
10 #include "Cxx_GrammarSerialization.h"
11 #include "SMTSolver.h"
12 #include "BinarySymbolicExpr.h"
13 #include "RegisterStateGeneric.h"
14 #include "MemoryCellList.h"
15 #include "MemoryCellMap.h"
16 
17 #include <boost/serialization/access.hpp>
18 #include <boost/serialization/base_object.hpp>
19 #include <boost/serialization/export.hpp>
20 #include <boost/serialization/set.hpp>
21 
22 #include <map>
23 #include <vector>
24 
25 namespace Rose {
26 namespace BinaryAnalysis { // documented elsewhere
27 namespace InstructionSemantics2 { // documented elsewhere
28 
47 namespace SymbolicSemantics {
48 
55 typedef std::set<SgAsmInstruction*> InsnSet;
56 
57 
58 
60 // Merging symbolic values
62 
65 
68  size_t setSizeLimit_;
69 protected:
70  Merger(): BaseSemantics::Merger(), setSizeLimit_(1) {}
71 
72 public:
74  typedef MergerPtr Ptr;
75 
77  static Ptr instance() {
78  return Ptr(new Merger);
79  }
80 
82  static Ptr instance(size_t n) {
83  Ptr retval = Ptr(new Merger);
84  retval->setSizeLimit(n);
85  return retval;
86  }
87 
99  size_t setSizeLimit() const { return setSizeLimit_; }
100  void setSizeLimit(size_t n) { setSizeLimit_ = n; }
102 };
103 
104 
105 
107 // Semantic values
109 
112 
115 public:
116  SymbolicExpr::Formatter expr_formatter;
117 };
118 
188 public:
190 
191 protected:
193  ExprPtr expr;
194 
197  InsnSet defs;
198 
200  // Serialization
201 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
202 private:
203  friend class boost::serialization::access;
204 
205  template<class S>
206  void serialize(S &s, const unsigned version) {
207  roseAstSerializationRegistration(s); // "defs" has SgAsmInstruction ASTs
208  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
209  s & BOOST_SERIALIZATION_NVP(expr);
210  s & BOOST_SERIALIZATION_NVP(defs);
211  }
212 #endif
213 
215  // Real constructors
216 protected:
217  SValue() {} // needed for serialization
218  explicit SValue(size_t nbits): BaseSemantics::SValue(nbits) {
219  expr = SymbolicExpr::makeVariable(nbits);
220  }
221  SValue(size_t nbits, uint64_t number): BaseSemantics::SValue(nbits) {
222  expr = SymbolicExpr::makeInteger(nbits, number);
223  }
224  SValue(ExprPtr expr): BaseSemantics::SValue(expr->nBits()) {
225  this->expr = expr;
226  }
227 
229  // Static allocating constructors
230 public:
232  static SValuePtr instance() {
234  }
235 
237  static SValuePtr instance_bottom(size_t nbits) {
239  }
240 
242  static SValuePtr instance_undefined(size_t nbits) {
243  return SValuePtr(new SValue(SymbolicExpr::makeVariable(nbits)));
244  }
245 
247  static SValuePtr instance_unspecified(size_t nbits) {
249  }
250 
252  static SValuePtr instance_integer(size_t nbits, uint64_t value) {
253  return SValuePtr(new SValue(SymbolicExpr::makeInteger(nbits, value)));
254  }
255 
257  // Virtual allocating constructors
258 public:
259  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE {
260  return instance_bottom(nbits);
261  }
262  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE {
263  return instance_undefined(nbits);
264  }
265  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE {
266  return instance_unspecified(nbits);
267  }
268  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE {
269  return instance_integer(nbits, value);
270  }
271  virtual BaseSemantics::SValuePtr boolean_(bool value) const ROSE_OVERRIDE {
272  return instance_integer(1, value?1:0);
273  }
274  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
275  SValuePtr retval(new SValue(*this));
276  if (new_width!=0 && new_width!=retval->get_width())
277  retval->set_width(new_width);
278  return retval;
279  }
282  SMTSolver*) const ROSE_OVERRIDE;
283 
285  // Dynamic pointer casts
286 public:
288  static SValuePtr promote(const BaseSemantics::SValuePtr &v) { // hot
289  SValuePtr retval = v.dynamicCast<SValue>();
290  ASSERT_not_null(retval);
291  return retval;
292  }
293 
295  // Override virtual methods...
296 public:
297  virtual bool may_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE;
298  virtual bool must_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE;
299 
300  // It's not possible to change the size of a symbolic expression in place. That would require that we recursively change
301  // the size of the SymbolicExpr, which might be shared with many unrelated values whose size we don't want to affect.
302  virtual void set_width(size_t nbits) ROSE_OVERRIDE {
303  ASSERT_require(nbits==get_width());
304  }
305 
306  virtual bool isBottom() const ROSE_OVERRIDE;
307 
308  virtual bool is_number() const ROSE_OVERRIDE {
309  return expr->isNumber();
310  }
311 
312  virtual uint64_t get_number() const ROSE_OVERRIDE;
313 
314  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
315 
316  virtual std::string get_comment() const ROSE_OVERRIDE;
317  virtual void set_comment(const std::string&) const ROSE_OVERRIDE;
318 
320  // Additional methods first declared in this class...
321 public:
328  virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to) const;
329 
336  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3) {
338  defined_by(insn, set1, set2);
339  }
340  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2) {
342  defined_by(insn, set1);
343  }
344  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1) {
346  defined_by(insn);
347  }
348  virtual void defined_by(SgAsmInstruction *insn) {
350  }
356  virtual const ExprPtr& get_expression() const {
357  return expr;
358  }
359 
362  virtual void set_expression(const ExprPtr &new_expr) {
363  ASSERT_not_null(new_expr);
364  expr = new_expr;
365  width = new_expr->nBits();
366  }
367  virtual void set_expression(const SValuePtr &source) {
368  set_expression(source->get_expression());
369  }
386  virtual const InsnSet& get_defining_instructions() const {
387  return defs;
388  }
389 
395  virtual size_t add_defining_instructions(const InsnSet &to_add);
396  virtual size_t add_defining_instructions(const SValuePtr &source) {
397  return add_defining_instructions(source->get_defining_instructions());
398  }
399  virtual size_t add_defining_instructions(SgAsmInstruction *insn);
407  virtual void set_defining_instructions(const InsnSet &new_defs) {
408  defs = new_defs;
409  }
410  virtual void set_defining_instructions(const SValuePtr &source) {
411  set_defining_instructions(source->get_defining_instructions());
412  }
413  virtual void set_defining_instructions(SgAsmInstruction *insn);
415 };
416 
417 
419 // Register state
421 
422 typedef BaseSemantics::RegisterStateGeneric RegisterState;
423 typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;
424 
425 
427 // List-based Memory state
429 
431 typedef boost::shared_ptr<class MemoryListState> MemoryListStatePtr;
432 
450 public:
452 
454  struct CellCompressor {
455  virtual ~CellCompressor() {}
456  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
458  const MemoryCellList::CellList &cells) = 0;
459  };
460 
475  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
477  const CellList &cells) ROSE_OVERRIDE;
478  };
479 
482  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
484  const CellList &cells) ROSE_OVERRIDE;
485  };
486 
491  CellCompressorMcCarthy cc_mccarthy;
492  CellCompressorSimple cc_simple;
493  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
495  const CellList &cells) ROSE_OVERRIDE;
496  };
497 
498 protected:
502  // Serialization
504 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
505 private:
506  friend class boost::serialization::access;
507 
508  template<class S>
509  void serialize(S &s, const unsigned version) {
510  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
511  }
512 #endif
513 
514 
516  // Real constructors
517 protected:
518  MemoryListState() // for serialization
519  : cell_compressor(&cc_choice) {}
520 
521  explicit MemoryListState(const BaseSemantics::MemoryCellPtr &protocell)
522  : BaseSemantics::MemoryCellList(protocell), cell_compressor(&cc_choice) {}
523 
524  MemoryListState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
525  : BaseSemantics::MemoryCellList(addrProtoval, valProtoval), cell_compressor(&cc_choice) {}
526 
527  MemoryListState(const MemoryListState &other)
528  : BaseSemantics::MemoryCellList(other), cell_compressor(other.cell_compressor) {}
529 
531  // Static allocating constructors
532 public:
534  static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
535  return MemoryListStatePtr(new MemoryListState(protocell));
536  }
537 
540  static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
541  const BaseSemantics::SValuePtr &valProtoval) {
542  return MemoryListStatePtr(new MemoryListState(addrProtoval, valProtoval));
543  }
544 
546  static MemoryListStatePtr instance(const MemoryListStatePtr &other) {
547  return MemoryListStatePtr(new MemoryListState(*other));
548  }
549 
551  // Virtual constructors
552 public:
556  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
557  return instance(addrProtoval, valProtoval);
558  }
559 
561  virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const ROSE_OVERRIDE {
562  return instance(protocell);
563  }
564 
566  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
568  }
569 
571  // Dynamic pointer casts
572 public:
575  static MemoryListStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
576  MemoryListStatePtr retval = boost::dynamic_pointer_cast<MemoryListState>(x);
577  ASSERT_not_null(retval);
578  return retval;
579  }
580 
582  // Methods we inherited
583 public:
589  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
590 
594  virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
595  BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
596 
598  // Methods first declared in this class
599 public:
604  void set_cell_compressor(CellCompressor *cc) { cell_compressor = cc; }
606 };
607 
608 
610 // Map-based Memory state
612 
614 typedef boost::shared_ptr<class MemoryMapState> MemoryMapStatePtr;
615 
634 public:
636 
638  // Serialization
639 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
640 private:
641  friend class boost::serialization::access;
642 
643  template<class S>
644  void serialize(S &s, const unsigned version) {
645  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
646  }
647 #endif
648 
650  // Real constructors
651 protected:
652  MemoryMapState() {} // for serialization
653 
654  explicit MemoryMapState(const BaseSemantics::MemoryCellPtr &protocell)
655  : BaseSemantics::MemoryCellMap(protocell) {}
656 
657  MemoryMapState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
658  : BaseSemantics::MemoryCellMap(addrProtoval, valProtoval) {}
659 
661  // Static allocating constructors
662 public:
664  static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
665  return MemoryMapStatePtr(new MemoryMapState(protocell));
666  }
667 
670  static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
671  const BaseSemantics::SValuePtr &valProtoval) {
672  return MemoryMapStatePtr(new MemoryMapState(addrProtoval, valProtoval));
673  }
674 
676  static MemoryMapStatePtr instance(const MemoryMapStatePtr &other) {
677  return MemoryMapStatePtr(new MemoryMapState(*other));
678  }
679 
681  // Virtual constructors
682 public:
686  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
687  return instance(addrProtoval, valProtoval);
688  }
689 
692  return instance(protocell);
693  }
694 
696  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
698  }
699 
701  // Dynamic pointer casts
702 public:
705  static MemoryMapStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
706  MemoryMapStatePtr retval = boost::dynamic_pointer_cast<MemoryMapState>(x);
707  ASSERT_not_null(retval);
708  return retval;
709  }
710 
712  // Methods we override from the super class (documented in the super class)
713 public:
714  virtual CellKey generateCellKey(const BaseSemantics::SValuePtr &addr_) const ROSE_OVERRIDE;
715 };
716 
717 
718 
720 // Default memory state
722 
723 // List-base memory was the type originally used by this domain. We must keep it that way because some analysis, including 3rd
724 // party, assumes that the state is list-based. New analysis can use the map-based state by instantiating it when the symbolic
725 // risc operators are constructed.
726 typedef MemoryListState MemoryState;
727 typedef MemoryListStatePtr MemoryStatePtr;
728 
730 // Complete state
732 
733 typedef BaseSemantics::State State;
734 typedef BaseSemantics::StatePtr StatePtr;
735 
736 
738 // RISC operators
740 
746 };
747 
753 };
754 
756 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
757 
778 public:
780 
781 protected:
782  bool omit_cur_insn; // if true, do not include cur_insn as a definer
783  DefinersMode computingDefiners_; // whether to track definers (instruction VAs) of SValues
784  WritersMode computingMemoryWriters_; // whether to track writers (instruction VAs) to memory.
785  WritersMode computingRegisterWriters_; // whether to track writers (instruction VAs) to registers.
786  size_t trimThreshold_; // max size of expressions (zero means no maximimum)
787 
789  // Serialization
790 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
791 private:
792  friend class boost::serialization::access;
793 
794  template<class S>
795  void serialize(S &s, const unsigned version) {
796  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
797  s & BOOST_SERIALIZATION_NVP(omit_cur_insn);
798  s & BOOST_SERIALIZATION_NVP(computingDefiners_);
799  s & BOOST_SERIALIZATION_NVP(computingMemoryWriters_);
800  s & BOOST_SERIALIZATION_NVP(computingRegisterWriters_);
801  s & BOOST_SERIALIZATION_NVP(trimThreshold_);
802  }
803 #endif
804 
806  // Real constructors
807 protected:
808  RiscOperators() // for serialization
809  : omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS), computingMemoryWriters_(TRACK_LATEST_WRITER),
810  computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0) {}
811 
813  : BaseSemantics::RiscOperators(protoval, solver), omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS),
814  computingMemoryWriters_(TRACK_LATEST_WRITER), computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0) {
815  name("Symbolic");
816  (void) SValue::promote(protoval); // make sure its dynamic type is a SymbolicSemantics::SValue
817  }
818 
819  explicit RiscOperators(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL)
820  : BaseSemantics::RiscOperators(state, solver), omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS),
821  computingMemoryWriters_(TRACK_LATEST_WRITER), computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0) {
822  name("Symbolic");
823  (void) SValue::promote(state->protoval()); // values must have SymbolicSemantics::SValue dynamic type
824  }
825 
827  // Static allocating constructors
828 public:
831  static RiscOperatorsPtr instance(const RegisterDictionary *regdict, SMTSolver *solver=NULL) {
833  BaseSemantics::RegisterStatePtr registers = RegisterState::instance(protoval, regdict);
834  BaseSemantics::MemoryStatePtr memory = MemoryListState::instance(protoval, protoval);
835  BaseSemantics::StatePtr state = State::instance(registers, memory);
836  return RiscOperatorsPtr(new RiscOperators(state, solver));
837  }
838 
841  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL) {
842  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
843  }
844 
847  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL) {
848  return RiscOperatorsPtr(new RiscOperators(state, solver));
849  }
850 
852  // Virtual constructors
853 public:
855  SMTSolver *solver=NULL) const ROSE_OVERRIDE {
856  return instance(protoval, solver);
857  }
858 
860  SMTSolver *solver=NULL) const ROSE_OVERRIDE {
861  return instance(state, solver);
862  }
863 
865  // Dynamic pointer casts
866 public:
869  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
870  RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
871  ASSERT_not_null(retval);
872  return retval;
873  }
874 
876  // Inherited methods for constructing values.
877 public:
878  virtual BaseSemantics::SValuePtr boolean_(bool b) ROSE_OVERRIDE {
880  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
881  retval->defined_by(currentInstruction());
882  return retval;
883  }
884 
885  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) ROSE_OVERRIDE {
886  SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
887  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
888  retval->defined_by(currentInstruction());
889  return retval;
890  }
891 
893  // New methods for constructing values, so we don't have to write so many SValue::promote calls in the RiscOperators
894  // implementations.
895 protected:
896  SValuePtr svalue_expr(const ExprPtr &expr, const InsnSet &defs=InsnSet()) {
897  SValuePtr newval = SValue::promote(protoval()->undefined_(expr->nBits()));
898  newval->set_expression(expr);
899  newval->set_defining_instructions(defs);
900  return newval;
901  }
902 
903  SValuePtr svalue_undefined(size_t nbits) {
904  return SValue::promote(undefined_(nbits));
905  }
906 
907  SValuePtr svalue_bottom(size_t nbits) {
908  return SValue::promote(bottom_(nbits));
909  }
910 
911  SValuePtr svalue_unspecified(size_t nbits) {
912  return SValue::promote(unspecified_(nbits));
913  }
914 
915  SValuePtr svalue_number(size_t nbits, uint64_t value) {
916  return SValue::promote(number_(nbits, value));
917  }
918 
919  SValuePtr svalue_boolean(bool b) {
920  return SValue::promote(boolean_(b));
921  }
922 
924  // Configuration properties
925 public:
926 
927  // [Robb P. Matzke 2015-09-17] deprecated API
928  bool computingUseDef() const ROSE_DEPRECATED("use computingDefiners instead") {
930  }
931  void computingUseDef(bool b) ROSE_DEPRECATED("use computingDefiners instead") {
933  }
934 
935  // [Robb P. Matzke 2015-08-10] deprecated API
936  void set_compute_usedef(bool b=true) ROSE_DEPRECATED("use computingDefiners instead") {
938  }
939  void clear_compute_usedef() ROSE_DEPRECATED("use computingDefiners instead") {
941  }
942  bool get_compute_usedef() ROSE_DEPRECATED("use computingDefiners instead") {
944  }
945 
963  void computingDefiners(DefinersMode m) { computingDefiners_ = m; }
964  DefinersMode computingDefiners() const { return computingDefiners_; }
985  void computingMemoryWriters(WritersMode m) { computingMemoryWriters_ = m; }
986  WritersMode computingMemoryWriters() const { return computingMemoryWriters_; }
989  // [Robb P. Matzke 2015-08-10] deprecated API
990  void set_compute_memwriters(bool b = true) ROSE_DEPRECATED("use computingMemoryWriters instead") {
992  }
993  void clear_compute_memwriters() ROSE_DEPRECATED("use computingMemoryWriters instead") {
995  }
996  bool get_compute_memwriters() const ROSE_DEPRECATED("use computingMemoryWriters instead") {
998  }
999 
1021  void computingRegisterWriters(WritersMode m) { computingRegisterWriters_ = m; }
1022  WritersMode computingRegisterWriters() const { return computingRegisterWriters_; }
1025  // Used internally to control whether cur_insn should be omitted from the list of definers.
1026  bool getset_omit_cur_insn(bool b) { bool retval = omit_cur_insn; omit_cur_insn=b; return retval; }
1027 
1034  void trimThreshold(size_t n) { trimThreshold_ = n; }
1035  size_t trimThreshold() const { return trimThreshold_; }
1038  // Methods first defined at this level of the class hierarchy
1040 public:
1102  virtual void substitute(const SValuePtr &from, const SValuePtr &to);
1103 
1109 
1111  // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
1112 public:
1113  virtual void interrupt(int majr, int minr) ROSE_OVERRIDE;
1115  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1117  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1119  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1120  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1122  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
1124  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1128  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1130  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1132  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1134  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1136  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1137  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1139  const BaseSemantics::SValuePtr &a_,
1140  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1141  virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
1142  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
1144  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1146  const BaseSemantics::SValuePtr &b_,
1147  const BaseSemantics::SValuePtr &c_,
1148  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
1149  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1151  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1153  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1155  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1157  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1159  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1161  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1163  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
1165  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
1166  virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1168  const BaseSemantics::SValuePtr &addr,
1169  const BaseSemantics::SValuePtr &dflt,
1170  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
1171  virtual void writeMemory(RegisterDescriptor segreg,
1172  const BaseSemantics::SValuePtr &addr,
1173  const BaseSemantics::SValuePtr &data,
1174  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
1175 };
1176 
1177 } // namespace
1178 } // namespace
1179 } // namespace
1180 } // namespace
1181 
1182 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1187 #endif
1188 
1189 #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 BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Returns position of least significant set bit; zero when no bits are set.
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:15
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 or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise OR of two values.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE
Sign extends a value.
virtual void set_defining_instructions(const InsnSet &new_defs)
Set defining instructions.
virtual SgAsmInstruction * currentInstruction() const
Returns current instruction.
static SValuePtr instance_integer(size_t nbits, uint64_t value)
Instantiate a new concrete value.
Leaf node of an expression tree for instruction semantics.
Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Defines RISC operators for the SymbolicSemantics domain.
virtual SValuePtr undefined_(size_t nbits)
Returns a new undefined value.
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
Add two values of equal size and a carry bit.
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.
CellCompressor * cell_compressor
Callback when a memory read aliases multiple memory cells.
static CellCompressorChoice cc_choice
The default cell compressor.
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.
static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL)
Instantiates a new RiscOperators object with specified state.
virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual copy constructor.
Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0)
Leaf 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.
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Returns position of most significant set bit; zero when no bits are set.
virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to) const
Substitute one value for another throughout a value.
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.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Determines whether a value is equal to zero.
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.
virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
If-then-else.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a SymbolicSemantics value.
STL namespace.
Holds a value or nothing.
Definition: Optional.h:49
static const unsigned UNSPECIFIED
Value is somehow unspecified.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Adds two integers of equal size.
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.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL)
Instantiates a new RiscOperators object with specified prototypical values.
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.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiplies two signed values.
virtual BaseSemantics::SValuePtr boolean_(bool b) ROSE_OVERRIDE
Returns a Boolean value.
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.
Describes (part of) a physical CPU register.
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 BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
One's complement.
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 smart pointer.
Definition: SharedPointer.h:34
virtual SValuePtr boolean_(bool value)
Returns a Boolean value.
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.
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.
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.
static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Concatenates the bits of two values.
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.
void computingMemoryWriters(WritersMode m)
Property: Track which instructions write to each memory location.
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted right logically (no sign bit).
Base classes for instruction semantics.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Returns true if two values could be equal.
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.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted left.
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.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const
Virtual constructor.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) ROSE_OVERRIDE
Returns a number of the specified bit width.
static SValuePtr instance()
Instantiate a new prototypical value.
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.
virtual void substitute(const SValuePtr &from, const SValuePtr &to)
Substitute all occurrences of from with to in the current state.
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise AND of two values.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the left.
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.
Defines registers available for a particular architecture.
Definition: Registers.h:32
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 ...
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 bool must_equal(const BaseSemantics::SValuePtr &other, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Returns true if two values must be equal.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
virtual void set_width(size_t nbits) ROSE_OVERRIDE
Accessor for value width.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the right.
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.
static StatePtr instance(const RegisterStatePtr &registers, const MemoryStatePtr &memory)
Instantiate a new state object with specified register and memory states.
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.
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.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
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 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 SValuePtr bottom_(size_t nbits)
Returns a data-flow bottom value.
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 extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) ROSE_OVERRIDE
Extracts bits from a value.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Calculates modulo with unsigned values.
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::MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual copy constructor.
virtual SMTSolver * solver() const
Property: Satisfiability module theory (SMT) solver.
virtual const std::string & name() const
Property: Name used for debugging.
void trimThreshold(size_t n)
Property: Maximum size of expressions.
virtual SValuePtr number_(size_t nbits, uint64_t value)
Returns a number of the specified bit width.
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.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, SMTSolver *solver=NULL) const ROSE_OVERRIDE
Virtual allocating constructor.
MergerPtr Ptr
Shared-ownership pointer for a Merger object.
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.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Computes bit-wise XOR of two values.
virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
Obtain a register value without side effects.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SMTSolver.h:19
boost::shared_ptr< class MemoryListState > MemoryListStatePtr
Shared-ownership pointer for symbolic list-based memory state.
virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Returns arg shifted right arithmetically (with sign bit).