ROSE  0.11.101.0
SymbolicSemantics.h
1 #ifndef ROSE_BinaryAnalysis_InstructionSemantics_SymbolicSemantics_H
2 #define ROSE_BinaryAnalysis_InstructionSemantics_SymbolicSemantics_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #ifndef __STDC_FORMAT_MACROS
7 #define __STDC_FORMAT_MACROS
8 #endif
9 #include <inttypes.h>
10 
11 #include <Rose/BinaryAnalysis/BasicTypes.h>
12 #include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics.h>
13 #include <Rose/BinaryAnalysis/SmtSolver.h>
14 #include <Rose/BinaryAnalysis/SymbolicExpression.h>
15 
16 #include "Cxx_GrammarSerialization.h"
17 
18 #include <boost/serialization/access.hpp>
19 #include <boost/serialization/base_object.hpp>
20 #include <boost/serialization/export.hpp>
21 #include <boost/serialization/set.hpp>
22 
23 #include <map>
24 #include <vector>
25 
26 namespace Rose {
27 namespace BinaryAnalysis { // documented elsewhere
28 namespace InstructionSemantics { // documented elsewhere
29 
48 namespace SymbolicSemantics {
49 
56 using InsnSet = std::set<SgAsmInstruction*>;
57 
59 // Boolean flags
61 
63 namespace AllowSideEffects {
64  enum Flag {NO, YES};
65 }
66 
67 
69 // Merging symbolic values
71 
74 
77  size_t setSizeLimit_;
78 protected:
79  Merger(): BaseSemantics::Merger(), setSizeLimit_(1) {}
80 
81 public:
83  typedef MergerPtr Ptr;
84 
86  static Ptr instance() {
87  return Ptr(new Merger);
88  }
89 
91  static Ptr instance(size_t n) {
92  Ptr retval = Ptr(new Merger);
93  retval->setSizeLimit(n);
94  return retval;
95  }
96 
108  size_t setSizeLimit() const { return setSizeLimit_; }
109  void setSizeLimit(size_t n) { setSizeLimit_ = n; }
111 };
112 
113 
114 
116 // Semantic values
118 
121 
124 public:
125  SymbolicExpression::Formatter expr_formatter;
126 };
127 
197 public:
200 
202  using Ptr = SValuePtr;
203 
204 protected:
207 
210  InsnSet defs;
211 
213  // Serialization
214 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
215 private:
216  friend class boost::serialization::access;
217 
218  template<class S>
219  void serialize(S &s, const unsigned /*version*/) {
220  roseAstSerializationRegistration(s); // "defs" has SgAsmInstruction ASTs
221  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
222  s & BOOST_SERIALIZATION_NVP(expr);
223  s & BOOST_SERIALIZATION_NVP(defs);
224  }
225 #endif
226 
228  // Real constructors
229 protected:
230  SValue() {} // needed for serialization
231  explicit SValue(size_t nbits): BaseSemantics::SValue(nbits) {
233  }
234  SValue(size_t nbits, uint64_t number): BaseSemantics::SValue(nbits) {
235  expr = SymbolicExpression::makeIntegerConstant(nbits, number);
236  }
237  SValue(ExprPtr expr): BaseSemantics::SValue(expr->nBits()) {
238  this->expr = expr;
239  }
240 
242  // Static allocating constructors
243 public:
245  static SValuePtr instance() {
247  }
248 
250  static SValuePtr instance_bottom(size_t nbits) {
252  }
253 
255  static SValuePtr instance_undefined(size_t nbits) {
257  }
258 
260  static SValuePtr instance_unspecified(size_t nbits) {
262  }
263 
265  static SValuePtr instance_integer(size_t nbits, uint64_t value) {
266  return SValuePtr(new SValue(SymbolicExpression::makeIntegerConstant(nbits, value)));
267  }
268 
270  static SValuePtr instance_symbolic(const SymbolicExpression::Ptr &value) {
271  ASSERT_not_null(value);
272  return SValuePtr(new SValue(value));
273  }
274 
276  // Virtual allocating constructors
277 public:
278  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override {
279  return instance_bottom(nbits);
280  }
281  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override {
282  return instance_undefined(nbits);
283  }
284  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override {
285  return instance_unspecified(nbits);
286  }
287  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override {
288  return instance_integer(nbits, value);
289  }
290  virtual BaseSemantics::SValuePtr boolean_(bool value) const override {
291  return instance_integer(1, value?1:0);
292  }
293  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override {
294  SValuePtr retval(new SValue(*this));
295  if (new_width!=0 && new_width!=retval->nBits())
296  retval->set_width(new_width);
297  return retval;
298  }
301  const SmtSolverPtr&) const override;
302 
304  // Dynamic pointer casts
305 public:
307  static SValuePtr promote(const BaseSemantics::SValuePtr &v) { // hot
308  SValuePtr retval = v.dynamicCast<SValue>();
309  ASSERT_not_null(retval);
310  return retval;
311  }
312 
314  // Override virtual methods...
315 public:
316  virtual bool isBottom() const override;
317 
318  virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
319 
320  virtual void hash(Combinatorics::Hasher&) const override;
321 
322 protected: // when implementing use these names; but when calling, use the camelCase names
323  virtual bool may_equal(const BaseSemantics::SValuePtr &other,
324  const SmtSolverPtr &solver = SmtSolverPtr()) const override;
325  virtual bool must_equal(const BaseSemantics::SValuePtr &other,
326  const SmtSolverPtr &solver = SmtSolverPtr()) const override;
327 
328  // It's not possible to change the size of a symbolic expression in place. That would require that we recursively change
329  // the size of the SymbolicExpression, which might be shared with many unrelated values whose size we don't want to affect.
330  virtual void set_width(size_t nbits) override {
331  ASSERT_require(nbits==nBits());
332  }
333 
334  virtual bool is_number() const override {
335  return expr->isIntegerConstant();
336  }
337 
338  virtual uint64_t get_number() const override;
339 
340  virtual std::string get_comment() const override;
341  virtual void set_comment(const std::string&) const override;
342 
344  // Additional methods first declared in this class...
345 public:
353  virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const;
354 
361  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3) {
363  defined_by(insn, set1, set2);
364  }
365  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2) {
367  defined_by(insn, set1);
368  }
369  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1) {
371  defined_by(insn);
372  }
373  virtual void defined_by(SgAsmInstruction *insn) {
375  }
381  virtual const ExprPtr& get_expression() const {
382  return expr;
383  }
384 
387  virtual void set_expression(const ExprPtr &new_expr) {
388  ASSERT_not_null(new_expr);
389  expr = new_expr;
390  width = new_expr->nBits();
391  }
392  virtual void set_expression(const SValuePtr &source) {
393  set_expression(source->get_expression());
394  }
411  virtual const InsnSet& get_defining_instructions() const {
412  return defs;
413  }
414 
420  virtual size_t add_defining_instructions(const InsnSet &to_add);
421  virtual size_t add_defining_instructions(const SValuePtr &source) {
422  return add_defining_instructions(source->get_defining_instructions());
423  }
424  virtual size_t add_defining_instructions(SgAsmInstruction *insn);
432  virtual void set_defining_instructions(const InsnSet &new_defs) {
433  defs = new_defs;
434  }
435  virtual void set_defining_instructions(const SValuePtr &source) {
436  set_defining_instructions(source->get_defining_instructions());
437  }
438  virtual void set_defining_instructions(SgAsmInstruction *insn);
440 };
441 
442 
444 // Register state
446 
447 typedef BaseSemantics::RegisterStateGeneric RegisterState;
448 typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;
449 
450 
452 // List-based Memory state
454 
456 typedef boost::shared_ptr<class MemoryListState> MemoryListStatePtr;
457 
475 public:
478 
481 
484  public:
486  protected:
487  CellCompressor() {}
488  public:
489  virtual ~CellCompressor() {}
490 
492  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
494  const MemoryCellList::CellList &cells) = 0;
495  };
496 
511  public:
512  static Ptr instance();
513  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
515  const CellList &cells) override;
516  };
517 
520  public:
521  static Ptr instance();
522  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
524  const CellList &cells) override;
525  };
526 
531  CellCompressor::Ptr mccarthy_;
532  CellCompressor::Ptr simple_;
533  protected:
535  public:
536  static Ptr instance();
537  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
539  const CellList &cells) override;
540  };
541 
546  public:
547  static Ptr instance();
548  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
550  const CellList &cells) override;
551  };
552 
553 private:
554  CellCompressor::Ptr cellCompressor_; // Callback when a memory read aliases multiple memory cells.
555 
557  // Serialization
558 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
559 private:
560  friend class boost::serialization::access;
561 
562  template<class S>
563  void serialize(S &s, const unsigned /*version*/) {
564  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
565  }
566 #endif
567 
568 
570  // Real constructors
571 protected:
572  MemoryListState() // for serialization
573  : cellCompressor_(CellCompressorChoice::instance()) {}
574 
575  explicit MemoryListState(const BaseSemantics::MemoryCellPtr &protocell)
576  : BaseSemantics::MemoryCellList(protocell), cellCompressor_(CellCompressorChoice::instance()) {}
577 
578  MemoryListState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
579  : BaseSemantics::MemoryCellList(addrProtoval, valProtoval), cellCompressor_(CellCompressorChoice::instance()) {}
580 
581  MemoryListState(const MemoryListState &other)
582  : BaseSemantics::MemoryCellList(other), cellCompressor_(other.cellCompressor_) {}
583 
585  // Static allocating constructors
586 public:
588  static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
589  return MemoryListStatePtr(new MemoryListState(protocell));
590  }
591 
594  static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
595  const BaseSemantics::SValuePtr &valProtoval) {
596  return MemoryListStatePtr(new MemoryListState(addrProtoval, valProtoval));
597  }
598 
600  static MemoryListStatePtr instance(const MemoryListStatePtr &other) {
601  return MemoryListStatePtr(new MemoryListState(*other));
602  }
603 
605  // Virtual constructors
606 public:
610  const BaseSemantics::SValuePtr &valProtoval) const override {
611  return instance(addrProtoval, valProtoval);
612  }
613 
615  virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const override {
616  return instance(protocell);
617  }
618 
620  virtual BaseSemantics::MemoryStatePtr clone() const override {
622  }
623 
625  // Dynamic pointer casts
626 public:
629  static MemoryListStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
630  MemoryListStatePtr retval = boost::dynamic_pointer_cast<MemoryListState>(x);
631  ASSERT_not_null(retval);
632  return retval;
633  }
634 
636  // Methods we inherited
637 public:
643  BaseSemantics::RiscOperators *valOps) override;
644 
650  BaseSemantics::RiscOperators *valOps) override;
651 
655  virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
657 
658 protected:
659  BaseSemantics::SValuePtr readOrPeekMemory(const BaseSemantics::SValuePtr &address,
660  const BaseSemantics::SValuePtr &dflt,
663  AllowSideEffects::Flag allowSideEffects);
664 
666  // Methods first declared in this class
667 public:
673  CellCompressor::Ptr cellCompressor() const;
674  void cellCompressor(const CellCompressor::Ptr&);
677  // Deprecated [Robb Matzke 2021-12-15]
678  CellCompressor::Ptr get_cell_compressor() const ROSE_DEPRECATED("use cellCompressor");
679  void set_cell_compressor(const CellCompressor::Ptr&) ROSE_DEPRECATED("use cellCompressor");
680 };
681 
682 
684 // Map-based Memory state
686 
688 typedef boost::shared_ptr<class MemoryMapState> MemoryMapStatePtr;
689 
707 class MemoryMapState: public BaseSemantics::MemoryCellMap {
708 public:
711 
714 
716  // Serialization
717 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
718 private:
719  friend class boost::serialization::access;
720 
721  template<class S>
722  void serialize(S &s, const unsigned /*version*/) {
723  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
724  }
725 #endif
726 
728  // Real constructors
729 protected:
730  MemoryMapState() {} // for serialization
731 
732  explicit MemoryMapState(const BaseSemantics::MemoryCellPtr &protocell)
733  : BaseSemantics::MemoryCellMap(protocell) {}
734 
735  MemoryMapState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
736  : BaseSemantics::MemoryCellMap(addrProtoval, valProtoval) {}
737 
739  // Static allocating constructors
740 public:
742  static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
743  return MemoryMapStatePtr(new MemoryMapState(protocell));
744  }
745 
748  static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
749  const BaseSemantics::SValuePtr &valProtoval) {
750  return MemoryMapStatePtr(new MemoryMapState(addrProtoval, valProtoval));
751  }
752 
754  static MemoryMapStatePtr instance(const MemoryMapStatePtr &other) {
755  return MemoryMapStatePtr(new MemoryMapState(*other));
756  }
757 
759  // Virtual constructors
760 public:
764  const BaseSemantics::SValuePtr &valProtoval) const override {
765  return instance(addrProtoval, valProtoval);
766  }
767 
770  return instance(protocell);
771  }
772 
774  virtual BaseSemantics::MemoryStatePtr clone() const override {
776  }
777 
779  // Dynamic pointer casts
780 public:
783  static MemoryMapStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
784  MemoryMapStatePtr retval = boost::dynamic_pointer_cast<MemoryMapState>(x);
785  ASSERT_not_null(retval);
786  return retval;
787  }
788 
790  // Methods we override from the super class (documented in the super class)
791 public:
792  virtual CellKey generateCellKey(const BaseSemantics::SValuePtr &addr_) const override;
793 };
794 
795 
796 
798 // Default memory state
800 
801 // List-base memory was the type originally used by this domain. We must keep it that way because some analysis, including 3rd
802 // party, assumes that the state is list-based. New analysis can use the map-based state by instantiating it when the symbolic
803 // risc operators are constructed.
804 typedef MemoryListState MemoryState;
805 typedef MemoryListStatePtr MemoryStatePtr;
806 
808 // Complete state
810 
811 typedef BaseSemantics::State State;
812 typedef BaseSemantics::StatePtr StatePtr;
813 
814 
816 // RISC operators
818 
824 };
825 
831 };
832 
834 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
835 
856 public:
859 
862 
863 protected:
864  bool omit_cur_insn; // if true, do not include cur_insn as a definer
865  DefinersMode computingDefiners_; // whether to track definers (instruction VAs) of SValues
866  WritersMode computingMemoryWriters_; // whether to track writers (instruction VAs) to memory.
867  WritersMode computingRegisterWriters_; // whether to track writers (instruction VAs) to registers.
868  uint64_t trimThreshold_; // max size of expressions (zero means no maximimum)
869  bool reinterpretMemoryReads_; // cast data to unsigned integer when reading from memory
870  bool reinterpretRegisterReads_; // cast data to unsigned integer when reading from registers
871  size_t nTrimmed_ = 0; // number of expressions trimmed down to a new variable
872 
873 
875  // Serialization
876 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
877 private:
878  friend class boost::serialization::access;
879 
880  template<class S>
881  void serialize(S &s, const unsigned /*version*/) {
882  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
883  s & BOOST_SERIALIZATION_NVP(omit_cur_insn);
884  s & BOOST_SERIALIZATION_NVP(computingDefiners_);
885  s & BOOST_SERIALIZATION_NVP(computingMemoryWriters_);
886  s & BOOST_SERIALIZATION_NVP(computingRegisterWriters_);
887  s & BOOST_SERIALIZATION_NVP(trimThreshold_);
888  }
889 #endif
890 
892  // Real constructors
893 protected:
894  RiscOperators(); // for serialization
895 
896  explicit RiscOperators(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver);
897 
898  explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver);
899 
901  // Static allocating constructors
902 public:
903  ~RiscOperators();
904 
907  static RiscOperatorsPtr instanceFromRegisters(const RegisterDictionaryPtr&, const SmtSolverPtr &solver = SmtSolverPtr());
908 
911  static RiscOperatorsPtr instanceFromProtoval(const BaseSemantics::SValuePtr &protoval,
912  const SmtSolverPtr &solver = SmtSolverPtr());
913 
916  static RiscOperatorsPtr instanceFromState(const BaseSemantics::StatePtr&, const SmtSolverPtr &solver = SmtSolverPtr());
917 
919  // Virtual constructors
920 public:
922  const SmtSolverPtr &solver = SmtSolverPtr()) const override;
923 
925  const SmtSolverPtr &solver = SmtSolverPtr()) const override;
926 
928  // Dynamic pointer casts
929 public:
932  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr&);
933 
935  // Inherited methods for constructing values.
936 public:
937  virtual BaseSemantics::SValuePtr boolean_(bool b) override {
939  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
940  retval->defined_by(currentInstruction());
941  return retval;
942  }
943 
944  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) override {
945  SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
946  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
947  retval->defined_by(currentInstruction());
948  return retval;
949  }
950 
952  // New methods for constructing values, so we don't have to write so many SValue::promote calls in the RiscOperators
953  // implementations.
954  SValuePtr svalueExpr(const ExprPtr &expr, const InsnSet &defs=InsnSet()) {
955  SValuePtr newval = SValue::promote(protoval()->undefined_(expr->nBits()));
956  newval->set_expression(expr);
957  newval->set_defining_instructions(defs);
958  return newval;
959  }
960 
961 protected:
962  SValuePtr svalueUndefined(size_t nbits) {
963  return SValue::promote(undefined_(nbits));
964  }
965 
966  SValuePtr svalueBottom(size_t nbits) {
967  return SValue::promote(bottom_(nbits));
968  }
969 
970  SValuePtr svalueUnspecified(size_t nbits) {
971  return SValue::promote(unspecified_(nbits));
972  }
973 
974  SValuePtr svalueNumber(size_t nbits, uint64_t value) {
975  return SValue::promote(number_(nbits, value));
976  }
977 
978  SValuePtr svalueBoolean(bool b) {
979  return SValue::promote(boolean_(b));
980  }
981 
983  // Configuration properties
984 public:
985 
1003  void computingDefiners(DefinersMode m) { computingDefiners_ = m; }
1004  DefinersMode computingDefiners() const { return computingDefiners_; }
1025  void computingMemoryWriters(WritersMode m) { computingMemoryWriters_ = m; }
1026  WritersMode computingMemoryWriters() const { return computingMemoryWriters_; }
1050  void computingRegisterWriters(WritersMode m) { computingRegisterWriters_ = m; }
1051  WritersMode computingRegisterWriters() const { return computingRegisterWriters_; }
1054  // Used internally to control whether cur_insn should be omitted from the list of definers.
1055  bool getset_omit_cur_insn(bool b) { bool retval = omit_cur_insn; omit_cur_insn=b; return retval; }
1056 
1063  void trimThreshold(uint64_t n) { trimThreshold_ = n; }
1064  uint64_t trimThreshold() const { return trimThreshold_; }
1073  size_t nTrimmed() const { return nTrimmed_; }
1074  void nTrimmed(size_t n) { nTrimmed_ = n; }
1084  bool reinterpretMemoryReads() const { return reinterpretMemoryReads_; }
1085  void reinterpretMemoryReads(bool b) { reinterpretMemoryReads_ = b; }
1086  bool reinterpretRegisterReads() const { return reinterpretRegisterReads_; }
1087  void reinterpretRegisterReads(bool b) { reinterpretRegisterReads_ = b; }
1090  // Methods first defined at this level of the class hierarchy
1092 public:
1154  virtual void substitute(const SValuePtr &from, const SValuePtr &to);
1155 
1160  virtual BaseSemantics::SValuePtr filterResult(const BaseSemantics::SValuePtr&);
1161 
1166  static SgAsmFloatType* sgIsIeee754(SgAsmType*);
1167 
1171  virtual SymbolicExpression::Type sgTypeToSymbolicType(SgAsmType*);
1172 
1174  // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
1175 public:
1176  virtual void interrupt(int majr, int minr) override;
1177  virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
1178  const BaseSemantics::SValuePtr &b_) override;
1179  virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_,
1180  const BaseSemantics::SValuePtr &b_) override;
1181  virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
1182  const BaseSemantics::SValuePtr &b_) override;
1183  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) override;
1184  virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
1185  size_t begin_bit, size_t end_bit) override;
1186  virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_,
1187  const BaseSemantics::SValuePtr &b_) override;
1188  virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) override;
1189  virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) override;
1190  virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_,
1191  const BaseSemantics::SValuePtr &sa_) override;
1192  virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_,
1193  const BaseSemantics::SValuePtr &sa_) override;
1194  virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_,
1195  const BaseSemantics::SValuePtr &sa_) override;
1196  virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_,
1197  const BaseSemantics::SValuePtr &sa_) override;
1198  virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_,
1199  const BaseSemantics::SValuePtr &sa_) override;
1200  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) override;
1201  virtual BaseSemantics::SValuePtr iteWithStatus(const BaseSemantics::SValuePtr &sel_,
1202  const BaseSemantics::SValuePtr &a_,
1203  const BaseSemantics::SValuePtr &b_,
1204  IteStatus&) override;
1205  virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
1206  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
1207  virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_,
1208  const BaseSemantics::SValuePtr &b_) override;
1209  virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_,
1210  const BaseSemantics::SValuePtr &b_,
1211  const BaseSemantics::SValuePtr &c_,
1212  BaseSemantics::SValuePtr &carry_out/*out*/) override;
1213  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) override;
1214  virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_,
1215  const BaseSemantics::SValuePtr &b_) override;
1216  virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_,
1217  const BaseSemantics::SValuePtr &b_) override;
1218  virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_,
1219  const BaseSemantics::SValuePtr &b_) override;
1220  virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_,
1221  const BaseSemantics::SValuePtr &b_) override;
1222  virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_,
1223  const BaseSemantics::SValuePtr &b_) override;
1224  virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_,
1225  const BaseSemantics::SValuePtr &b_) override;
1226  virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr &a, SgAsmFloatType *aType,
1227  SgAsmFloatType *retType) override;
1228  virtual BaseSemantics::SValuePtr reinterpret(const BaseSemantics::SValuePtr&, SgAsmType*) override;
1229  virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg,
1230  const BaseSemantics::SValuePtr &dflt) override;
1231  virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg,
1232  const BaseSemantics::SValuePtr &dflt) override;
1233  virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) override;
1235  const BaseSemantics::SValuePtr &addr,
1236  const BaseSemantics::SValuePtr &dflt,
1237  const BaseSemantics::SValuePtr &cond) override;
1239  const BaseSemantics::SValuePtr &addr,
1240  const BaseSemantics::SValuePtr &dflt) override;
1241  virtual void writeMemory(RegisterDescriptor segreg,
1242  const BaseSemantics::SValuePtr &addr,
1243  const BaseSemantics::SValuePtr &data,
1244  const BaseSemantics::SValuePtr &cond) override;
1245 
1246 public:
1247  BaseSemantics::SValuePtr readOrPeekMemory(RegisterDescriptor segreg,
1248  const BaseSemantics::SValuePtr &addr,
1249  const BaseSemantics::SValuePtr &dflt,
1250  AllowSideEffects::Flag);
1251 };
1252 
1253 } // namespace
1254 } // namespace
1255 } // namespace
1256 } // namespace
1257 
1258 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1263 #endif
1264 
1265 #endif
1266 #endif
MergerPtr Ptr
Shared-ownership pointer for a Merger object.
Base classes for instruction semantics.
Definition: Dispatcher.h:18
static const unsigned UNSPECIFIED
Value is somehow unspecified.
Sawyer::SharedPointer< Interior > InteriorPtr
Reference counting pointer.
virtual void set_expression(const ExprPtr &new_expr)
Changes the expression stored in the value.
virtual size_t add_defining_instructions(const InsnSet &to_add)
Adds definitions to the list of defining instructions.
virtual BaseSemantics::SValuePtr peekMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) 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 bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
Functor for handling a memory read whose address matches more than one memory cell.
virtual BaseSemantics::SValuePtr boolean_(bool b) override
Returns a Boolean value.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
static MemoryMapStatePtr promote(const BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
Base class for machine instructions.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override
Create a new undefined semantic value.
static MemoryMapStatePtr instance(const MemoryMapStatePtr &other)
Instantiates a new deep copy of an existing state.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
static SValuePtr instance_integer(size_t nbits, uint64_t value)
Instantiate a new concrete value.
void computingDefiners(DefinersMode m)
Property: Track which instructions define a semantic value.
Functor for handling a memory read whose address matches more than one memory cell.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a SymbolicSemantics value.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
Base class for symbolic expression nodes.
Sawyer::SharedPointer< Leaf > LeafPtr
Reference counting pointer.
Holds a value or nothing.
Definition: Optional.h:49
void computingRegisterWriters(WritersMode m)
Property: Track latest writer to each register.
static MemoryListStatePtr promote(const BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
void reinterpretRegisterReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
std::list< MemoryCellPtr > CellList
List of memory cells.
DefinersMode computingDefiners() const
Property: Track which instructions define a semantic value.
bool reinterpretMemoryReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
Main namespace for the ROSE library.
WritersMode computingMemoryWriters() const
Property: Track which instructions write to each memory location.
boost::shared_ptr< MemoryCell > MemoryCellPtr
Shared-ownership pointer to a memory cell.
static MemoryListStatePtr instance(const MemoryListStatePtr &other)
Instantiates a new deep copy of an existing state.
virtual SValuePtr number_(size_t nbits, uint64_t value)
Returns a number of the specified bit width.
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Write a byte to memory.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const MemoryCellList::CellList &cells)=0
Compress the cells into a single value.
Functor for handling a memory read that found more than one cell that might alias the requested addre...
static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
void reinterpretMemoryReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1)
Adds instructions to the list of defining instructions.
virtual BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
WritersMode
How to update the list of writers stored at each abstract location.
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
Functor for handling a memory read whose address matches more than one memory cell.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
boost::shared_ptr< class MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to symbolic memory state.
static SValuePtr instance_bottom(size_t nbits)
Instantiate a new data-flow bottom value of specified width.
CellCompressor::Ptr cellCompressor() const
Callback for handling a memory read whose address matches more than one memory cell.
virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override
Create a new value from an existing value, changing the width if new_width is non-zero.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
virtual BaseSemantics::MemoryStatePtr clone() const override
Virtual copy constructor.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override
Create a new unspecified semantic value.
static SValuePtr instance_unspecified(size_t nbits)
Instantiate a new unspecified value of specified width.
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override
Data-flow bottom value.
virtual size_t add_defining_instructions(const SValuePtr &source)
Adds definitions to the list of defining instructions.
virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const
Substitute one value for another throughout a value.
static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
virtual bool isBottom() const override
Determines whether a value is a data-flow bottom.
DefinersMode
How to update the list of definers stored in each semantic value.
virtual void set_comment(const std::string &) const override
Some subclasses support the ability to add comments to values.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override
Create a new concrete semantic value.
Describes (part of) a physical CPU register.
virtual Sawyer::Optional< BaseSemantics::SValuePtr > createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
Possibly create a new value by merging two existing values.
WritersMode computingRegisterWriters() const
Property: Track latest writer to each register.
size_t nTrimmed() const
Property: Number of symbolic expressions trimmed.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) override
Returns a number of the specified bit width.
virtual uint64_t get_number() const override
Virtual API.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Type of values manipulated by the SymbolicSemantics domain.
static SValuePtr instance_symbolic(const SymbolicExpression::Ptr &value)
Instantiate a new symbolic value.
static SValuePtr instance()
Instantiate a new prototypical value.
boost::shared_ptr< class MemoryListState > MemoryListStatePtr
Shared-ownership pointer for symbolic list-based memory state.
virtual void set_expression(const SValuePtr &source)
Changes the expression stored in the value.
void computingMemoryWriters(WritersMode m)
Property: Track which instructions write to each memory location.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
SharedPointer< U > dynamicCast() const
Dynamic cast.
virtual void set_width(size_t nbits) override
Virtual API.
Binary analysis.
Defines RISC operators for the SymbolicSemantics domain.
virtual void set_defining_instructions(const InsnSet &new_defs)
Set defining instructions.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2)
Adds instructions to the list of defining instructions.
static SValuePtr instance_undefined(size_t nbits)
Instantiate a new undefined value of specified width.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Base class for binary types.
Base class for reference counted objects.
Definition: SharedObject.h:64
virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Read a byte from memory.
static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
virtual SValuePtr boolean_(bool value)
Returns a Boolean value.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const override
Virtual constructor.
virtual const InsnSet & get_defining_instructions() const
Returns the set of instructions that defined this value.
Controls formatting of expression trees when printing.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
virtual void defined_by(SgAsmInstruction *insn)
Adds instructions to the list of defining instructions.
Leaf node of an expression tree for instruction semantics.
void nTrimmed(size_t n)
Property: Number of symbolic expressions trimmed.
virtual std::string get_comment() const override
Some subclasses support the ability to add comments to values.
void trimThreshold(uint64_t n)
Property: Maximum size of expressions.
virtual const ExprPtr & get_expression() const
Returns the expression stored in this value.
Interior node of an expression tree for instruction semantics.
bool reinterpretRegisterReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
uint64_t trimThreshold() const
Property: Maximum size of expressions.
Base class for most instruction semantics RISC operators.
Definition: RiscOperators.h:48
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const
Virtual constructor.
Base class for semantics machine states.
Definition: State.h:39
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 BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
Floating point types.
virtual void set_defining_instructions(const SValuePtr &source)
Set defining instructions.
virtual BaseSemantics::MemoryStatePtr clone() const override
Virtual copy constructor.