ROSE  0.11.82.0
SymbolicSemantics.h
1 #ifndef ROSE_BinaryAnalysis_InstructionSemantics2_SymbolicSemantics_H
2 #define ROSE_BinaryAnalysis_InstructionSemantics2_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/InstructionSemantics2/BaseSemantics.h>
12 #include "Cxx_GrammarSerialization.h"
13 #include <Rose/BinaryAnalysis/SmtSolver.h>
14 #include <Rose/BinaryAnalysis/SymbolicExpr.h>
15 
16 #include <boost/serialization/access.hpp>
17 #include <boost/serialization/base_object.hpp>
18 #include <boost/serialization/export.hpp>
19 #include <boost/serialization/set.hpp>
20 
21 #include <map>
22 #include <vector>
23 
24 namespace Rose {
25 namespace BinaryAnalysis { // documented elsewhere
26 namespace InstructionSemantics2 { // documented elsewhere
27 
46 namespace SymbolicSemantics {
47 
54 typedef std::set<SgAsmInstruction*> InsnSet;
55 
57 // Boolean flags
59 
61 namespace AllowSideEffects {
62  enum Flag {NO, YES};
63 }
64 
65 
67 // Merging symbolic values
69 
72 
75  size_t setSizeLimit_;
76 protected:
77  Merger(): BaseSemantics::Merger(), setSizeLimit_(1) {}
78 
79 public:
81  typedef MergerPtr Ptr;
82 
84  static Ptr instance() {
85  return Ptr(new Merger);
86  }
87 
89  static Ptr instance(size_t n) {
90  Ptr retval = Ptr(new Merger);
91  retval->setSizeLimit(n);
92  return retval;
93  }
94 
106  size_t setSizeLimit() const { return setSizeLimit_; }
107  void setSizeLimit(size_t n) { setSizeLimit_ = n; }
109 };
110 
111 
112 
114 // Semantic values
116 
119 
122 public:
123  SymbolicExpr::Formatter expr_formatter;
124 };
125 
195 public:
198 
200  using Ptr = SValuePtr;
201 
202 protected:
204  ExprPtr expr;
205 
208  InsnSet defs;
209 
211  // Serialization
212 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
213 private:
214  friend class boost::serialization::access;
215 
216  template<class S>
217  void serialize(S &s, const unsigned /*version*/) {
218  roseAstSerializationRegistration(s); // "defs" has SgAsmInstruction ASTs
219  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
220  s & BOOST_SERIALIZATION_NVP(expr);
221  s & BOOST_SERIALIZATION_NVP(defs);
222  }
223 #endif
224 
226  // Real constructors
227 protected:
228  SValue() {} // needed for serialization
229  explicit SValue(size_t nbits): BaseSemantics::SValue(nbits) {
230  expr = SymbolicExpr::makeIntegerVariable(nbits);
231  }
232  SValue(size_t nbits, uint64_t number): BaseSemantics::SValue(nbits) {
233  expr = SymbolicExpr::makeIntegerConstant(nbits, number);
234  }
235  SValue(ExprPtr expr): BaseSemantics::SValue(expr->nBits()) {
236  this->expr = expr;
237  }
238 
240  // Static allocating constructors
241 public:
243  static SValuePtr instance() {
245  }
246 
248  static SValuePtr instance_bottom(size_t nbits) {
250  }
251 
253  static SValuePtr instance_undefined(size_t nbits) {
255  }
256 
258  static SValuePtr instance_unspecified(size_t nbits) {
260  }
261 
263  static SValuePtr instance_integer(size_t nbits, uint64_t value) {
264  return SValuePtr(new SValue(SymbolicExpr::makeIntegerConstant(nbits, value)));
265  }
266 
268  static SValuePtr instance_symbolic(const SymbolicExpr::Ptr &value) {
269  ASSERT_not_null(value);
270  return SValuePtr(new SValue(value));
271  }
272 
274  // Virtual allocating constructors
275 public:
276  virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override {
277  return instance_bottom(nbits);
278  }
279  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override {
280  return instance_undefined(nbits);
281  }
282  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override {
283  return instance_unspecified(nbits);
284  }
285  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override {
286  return instance_integer(nbits, value);
287  }
288  virtual BaseSemantics::SValuePtr boolean_(bool value) const override {
289  return instance_integer(1, value?1:0);
290  }
291  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override {
292  SValuePtr retval(new SValue(*this));
293  if (new_width!=0 && new_width!=retval->nBits())
294  retval->set_width(new_width);
295  return retval;
296  }
299  const SmtSolverPtr&) const override;
300 
302  // Dynamic pointer casts
303 public:
305  static SValuePtr promote(const BaseSemantics::SValuePtr &v) { // hot
306  SValuePtr retval = v.dynamicCast<SValue>();
307  ASSERT_not_null(retval);
308  return retval;
309  }
310 
312  // Override virtual methods...
313 public:
314  virtual bool isBottom() const override;
315 
316  virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
317 
318  virtual void hash(Combinatorics::Hasher&) const override;
319 
320 protected: // when implementing use these names; but when calling, use the camelCase names
321  virtual bool may_equal(const BaseSemantics::SValuePtr &other,
322  const SmtSolverPtr &solver = SmtSolverPtr()) const override;
323  virtual bool must_equal(const BaseSemantics::SValuePtr &other,
324  const SmtSolverPtr &solver = SmtSolverPtr()) const override;
325 
326  // It's not possible to change the size of a symbolic expression in place. That would require that we recursively change
327  // the size of the SymbolicExpr, which might be shared with many unrelated values whose size we don't want to affect.
328  virtual void set_width(size_t nbits) override {
329  ASSERT_require(nbits==nBits());
330  }
331 
332  virtual bool is_number() const override {
333  return expr->isIntegerConstant();
334  }
335 
336  virtual uint64_t get_number() const override;
337 
338  virtual std::string get_comment() const override;
339  virtual void set_comment(const std::string&) const override;
340 
342  // Additional methods first declared in this class...
343 public:
351  virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const;
352 
359  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3) {
361  defined_by(insn, set1, set2);
362  }
363  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2) {
365  defined_by(insn, set1);
366  }
367  virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1) {
369  defined_by(insn);
370  }
371  virtual void defined_by(SgAsmInstruction *insn) {
373  }
379  virtual const ExprPtr& get_expression() const {
380  return expr;
381  }
382 
385  virtual void set_expression(const ExprPtr &new_expr) {
386  ASSERT_not_null(new_expr);
387  expr = new_expr;
388  width = new_expr->nBits();
389  }
390  virtual void set_expression(const SValuePtr &source) {
391  set_expression(source->get_expression());
392  }
409  virtual const InsnSet& get_defining_instructions() const {
410  return defs;
411  }
412 
418  virtual size_t add_defining_instructions(const InsnSet &to_add);
419  virtual size_t add_defining_instructions(const SValuePtr &source) {
420  return add_defining_instructions(source->get_defining_instructions());
421  }
422  virtual size_t add_defining_instructions(SgAsmInstruction *insn);
430  virtual void set_defining_instructions(const InsnSet &new_defs) {
431  defs = new_defs;
432  }
433  virtual void set_defining_instructions(const SValuePtr &source) {
434  set_defining_instructions(source->get_defining_instructions());
435  }
436  virtual void set_defining_instructions(SgAsmInstruction *insn);
438 };
439 
440 
442 // Register state
444 
445 typedef BaseSemantics::RegisterStateGeneric RegisterState;
446 typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;
447 
448 
450 // List-based Memory state
452 
454 typedef boost::shared_ptr<class MemoryListState> MemoryListStatePtr;
455 
473 public:
476 
479 
482  public:
484  protected:
485  CellCompressor() {}
486  public:
487  virtual ~CellCompressor() {}
488 
490  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
492  const MemoryCellList::CellList &cells) = 0;
493  };
494 
509  public:
510  static Ptr instance();
511  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
513  const CellList &cells) override;
514  };
515 
518  public:
519  static Ptr instance();
520  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
522  const CellList &cells) override;
523  };
524 
529  CellCompressor::Ptr mccarthy_;
530  CellCompressor::Ptr simple_;
531  protected:
533  public:
534  static Ptr instance();
535  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
537  const CellList &cells) override;
538  };
539 
544  public:
545  static Ptr instance();
546  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
548  const CellList &cells) override;
549  };
550 
551 private:
552  CellCompressor::Ptr cellCompressor_; // Callback when a memory read aliases multiple memory cells.
553 
555  // Serialization
556 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
557 private:
558  friend class boost::serialization::access;
559 
560  template<class S>
561  void serialize(S &s, const unsigned /*version*/) {
562  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
563  }
564 #endif
565 
566 
568  // Real constructors
569 protected:
570  MemoryListState() // for serialization
571  : cellCompressor_(CellCompressorChoice::instance()) {}
572 
573  explicit MemoryListState(const BaseSemantics::MemoryCellPtr &protocell)
574  : BaseSemantics::MemoryCellList(protocell), cellCompressor_(CellCompressorChoice::instance()) {}
575 
576  MemoryListState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
577  : BaseSemantics::MemoryCellList(addrProtoval, valProtoval), cellCompressor_(CellCompressorChoice::instance()) {}
578 
579  MemoryListState(const MemoryListState &other)
580  : BaseSemantics::MemoryCellList(other), cellCompressor_(other.cellCompressor_) {}
581 
583  // Static allocating constructors
584 public:
586  static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
587  return MemoryListStatePtr(new MemoryListState(protocell));
588  }
589 
592  static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
593  const BaseSemantics::SValuePtr &valProtoval) {
594  return MemoryListStatePtr(new MemoryListState(addrProtoval, valProtoval));
595  }
596 
598  static MemoryListStatePtr instance(const MemoryListStatePtr &other) {
599  return MemoryListStatePtr(new MemoryListState(*other));
600  }
601 
603  // Virtual constructors
604 public:
608  const BaseSemantics::SValuePtr &valProtoval) const override {
609  return instance(addrProtoval, valProtoval);
610  }
611 
613  virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const override {
614  return instance(protocell);
615  }
616 
618  virtual BaseSemantics::MemoryStatePtr clone() const override {
620  }
621 
623  // Dynamic pointer casts
624 public:
627  static MemoryListStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
628  MemoryListStatePtr retval = boost::dynamic_pointer_cast<MemoryListState>(x);
629  ASSERT_not_null(retval);
630  return retval;
631  }
632 
634  // Methods we inherited
635 public:
641  BaseSemantics::RiscOperators *valOps) override;
642 
648  BaseSemantics::RiscOperators *valOps) override;
649 
653  virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
655 
656 protected:
657  BaseSemantics::SValuePtr readOrPeekMemory(const BaseSemantics::SValuePtr &address,
658  const BaseSemantics::SValuePtr &dflt,
661  AllowSideEffects::Flag allowSideEffects);
662 
664  // Methods first declared in this class
665 public:
671  CellCompressor::Ptr cellCompressor() const;
672  void cellCompressor(const CellCompressor::Ptr&);
675  // Deprecated [Robb Matzke 2021-12-15]
676  CellCompressor::Ptr get_cell_compressor() const ROSE_DEPRECATED("use cellCompressor");
677  void set_cell_compressor(const CellCompressor::Ptr&) ROSE_DEPRECATED("use cellCompressor");
678 };
679 
680 
682 // Map-based Memory state
684 
686 typedef boost::shared_ptr<class MemoryMapState> MemoryMapStatePtr;
687 
705 class MemoryMapState: public BaseSemantics::MemoryCellMap {
706 public:
709 
712 
714  // Serialization
715 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
716 private:
717  friend class boost::serialization::access;
718 
719  template<class S>
720  void serialize(S &s, const unsigned /*version*/) {
721  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
722  }
723 #endif
724 
726  // Real constructors
727 protected:
728  MemoryMapState() {} // for serialization
729 
730  explicit MemoryMapState(const BaseSemantics::MemoryCellPtr &protocell)
731  : BaseSemantics::MemoryCellMap(protocell) {}
732 
733  MemoryMapState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
734  : BaseSemantics::MemoryCellMap(addrProtoval, valProtoval) {}
735 
737  // Static allocating constructors
738 public:
740  static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
741  return MemoryMapStatePtr(new MemoryMapState(protocell));
742  }
743 
746  static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
747  const BaseSemantics::SValuePtr &valProtoval) {
748  return MemoryMapStatePtr(new MemoryMapState(addrProtoval, valProtoval));
749  }
750 
752  static MemoryMapStatePtr instance(const MemoryMapStatePtr &other) {
753  return MemoryMapStatePtr(new MemoryMapState(*other));
754  }
755 
757  // Virtual constructors
758 public:
762  const BaseSemantics::SValuePtr &valProtoval) const override {
763  return instance(addrProtoval, valProtoval);
764  }
765 
768  return instance(protocell);
769  }
770 
772  virtual BaseSemantics::MemoryStatePtr clone() const override {
774  }
775 
777  // Dynamic pointer casts
778 public:
781  static MemoryMapStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
782  MemoryMapStatePtr retval = boost::dynamic_pointer_cast<MemoryMapState>(x);
783  ASSERT_not_null(retval);
784  return retval;
785  }
786 
788  // Methods we override from the super class (documented in the super class)
789 public:
790  virtual CellKey generateCellKey(const BaseSemantics::SValuePtr &addr_) const override;
791 };
792 
793 
794 
796 // Default memory state
798 
799 // List-base memory was the type originally used by this domain. We must keep it that way because some analysis, including 3rd
800 // party, assumes that the state is list-based. New analysis can use the map-based state by instantiating it when the symbolic
801 // risc operators are constructed.
802 typedef MemoryListState MemoryState;
803 typedef MemoryListStatePtr MemoryStatePtr;
804 
806 // Complete state
808 
809 typedef BaseSemantics::State State;
810 typedef BaseSemantics::StatePtr StatePtr;
811 
812 
814 // RISC operators
816 
822 };
823 
829 };
830 
832 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
833 
854 public:
857 
860 
861 protected:
862  bool omit_cur_insn; // if true, do not include cur_insn as a definer
863  DefinersMode computingDefiners_; // whether to track definers (instruction VAs) of SValues
864  WritersMode computingMemoryWriters_; // whether to track writers (instruction VAs) to memory.
865  WritersMode computingRegisterWriters_; // whether to track writers (instruction VAs) to registers.
866  uint64_t trimThreshold_; // max size of expressions (zero means no maximimum)
867  bool reinterpretMemoryReads_; // cast data to unsigned integer when reading from memory
868  bool reinterpretRegisterReads_; // cast data to unsigned integer when reading from registers
869  size_t nTrimmed_ = 0; // number of expressions trimmed down to a new variable
870 
871 
873  // Serialization
874 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
875 private:
876  friend class boost::serialization::access;
877 
878  template<class S>
879  void serialize(S &s, const unsigned /*version*/) {
880  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
881  s & BOOST_SERIALIZATION_NVP(omit_cur_insn);
882  s & BOOST_SERIALIZATION_NVP(computingDefiners_);
883  s & BOOST_SERIALIZATION_NVP(computingMemoryWriters_);
884  s & BOOST_SERIALIZATION_NVP(computingRegisterWriters_);
885  s & BOOST_SERIALIZATION_NVP(trimThreshold_);
886  }
887 #endif
888 
890  // Real constructors
891 protected:
892  RiscOperators() // for serialization
893  : omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS), computingMemoryWriters_(TRACK_LATEST_WRITER),
894  computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0), reinterpretMemoryReads_(true),
895  reinterpretRegisterReads_(true) {}
896 
897  explicit RiscOperators(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr())
898  : BaseSemantics::RiscOperators(protoval, solver), omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS),
899  computingMemoryWriters_(TRACK_LATEST_WRITER), computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0),
900  reinterpretMemoryReads_(true), reinterpretRegisterReads_(true) {
901  name("Symbolic");
902  ASSERT_always_not_null(protoval);
903  ASSERT_always_not_null2(protoval.dynamicCast<SValue>(),
904  "SymbolicSemantics supports only symbolic SValue types or derivatives thereof");
905  }
906 
907  explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr())
908  : BaseSemantics::RiscOperators(state, solver), omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS),
909  computingMemoryWriters_(TRACK_LATEST_WRITER), computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0),
910  reinterpretMemoryReads_(true), reinterpretRegisterReads_(true) {
911  name("Symbolic");
912  ASSERT_always_not_null(state);
913  ASSERT_always_not_null(state->registerState());
914  ASSERT_always_not_null2(boost::dynamic_pointer_cast<RegisterState>(state->registerState()),
915  "SymbolicSemantics supports only RegisterStateGeneric or derivatives thereof");
916  ASSERT_always_not_null(state->protoval());
917  ASSERT_always_not_null2(state->protoval().dynamicCast<SValue>(),
918  "SymbolicSemantics supports only symbolic SValue types or derivatives thereof");
919  }
920 
922  // Static allocating constructors
923 public:
926  static RiscOperatorsPtr instance(const RegisterDictionary *regdict, const SmtSolverPtr &solver = SmtSolverPtr()) {
928  BaseSemantics::RegisterStatePtr registers = RegisterState::instance(protoval, regdict);
929  BaseSemantics::MemoryStatePtr memory = MemoryListState::instance(protoval, protoval);
930  BaseSemantics::StatePtr state = State::instance(registers, memory);
931  return RiscOperatorsPtr(new RiscOperators(state, solver));
932  }
933 
936  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr()) {
937  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
938  }
939 
942  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr()) {
943  return RiscOperatorsPtr(new RiscOperators(state, solver));
944  }
945 
947  // Virtual constructors
948 public:
950  const SmtSolverPtr &solver = SmtSolverPtr()) const override {
951  return instance(protoval, solver);
952  }
953 
955  const SmtSolverPtr &solver = SmtSolverPtr()) const override {
956  return instance(state, solver);
957  }
958 
960  // Dynamic pointer casts
961 public:
964  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
965  RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
966  ASSERT_not_null(retval);
967  return retval;
968  }
969 
971  // Inherited methods for constructing values.
972 public:
973  virtual BaseSemantics::SValuePtr boolean_(bool b) override {
975  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
976  retval->defined_by(currentInstruction());
977  return retval;
978  }
979 
980  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) override {
981  SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
982  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
983  retval->defined_by(currentInstruction());
984  return retval;
985  }
986 
988  // New methods for constructing values, so we don't have to write so many SValue::promote calls in the RiscOperators
989  // implementations.
990  SValuePtr svalueExpr(const ExprPtr &expr, const InsnSet &defs=InsnSet()) {
991  SValuePtr newval = SValue::promote(protoval()->undefined_(expr->nBits()));
992  newval->set_expression(expr);
993  newval->set_defining_instructions(defs);
994  return newval;
995  }
996 
997 protected:
998  SValuePtr svalueUndefined(size_t nbits) {
999  return SValue::promote(undefined_(nbits));
1000  }
1001 
1002  SValuePtr svalueBottom(size_t nbits) {
1003  return SValue::promote(bottom_(nbits));
1004  }
1005 
1006  SValuePtr svalueUnspecified(size_t nbits) {
1007  return SValue::promote(unspecified_(nbits));
1008  }
1009 
1010  SValuePtr svalueNumber(size_t nbits, uint64_t value) {
1011  return SValue::promote(number_(nbits, value));
1012  }
1013 
1014  SValuePtr svalueBoolean(bool b) {
1015  return SValue::promote(boolean_(b));
1016  }
1017 
1018  // [Robb Matzke 2021-03-18]: deprecated
1019  SValuePtr svalue_number(size_t nbits, uint64_t value) ROSE_DEPRECATED("use svalueNumber instead") {
1020  return svalueNumber(nbits, value);
1021  }
1022 
1023  // [Robb Matzke 2021-03-18]: deprecated
1024  SValuePtr svalue_boolean(bool b) ROSE_DEPRECATED("use svalueBoolean instead") {
1025  return svalueBoolean(b);
1026  }
1027 
1028  // [Robb Matzke 2021-03-18]: deprecated
1029  SValuePtr svalue_unspecified(size_t nbits) ROSE_DEPRECATED("use svalueUnspecified instead") {
1030  return svalueUnspecified(nbits);
1031  }
1032 
1033  // [Robb Matzke 2021-03-18]: deprecated
1034  SValuePtr svalue_bottom(size_t nbits) ROSE_DEPRECATED("use svalueBottom instead") {
1035  return svalueBottom(nbits);
1036  }
1037 
1038  // [Robb Matzke 2021-03-18]: deprecated
1039  SValuePtr svalue_undefined(size_t nbits) ROSE_DEPRECATED("use svalueUndefined instead") {
1040  return svalueUndefined(nbits);
1041  }
1042 
1043  // [Robb Matzke 2021-03-18]: deprecated
1044  SValuePtr svalue_expr(const ExprPtr &expr, const InsnSet &defs=InsnSet()) ROSE_DEPRECATED("use svalueExpr instead") {
1045  return svalueExpr(expr, defs);
1046  }
1047 
1049  // Configuration properties
1050 public:
1051 
1069  void computingDefiners(DefinersMode m) { computingDefiners_ = m; }
1070  DefinersMode computingDefiners() const { return computingDefiners_; }
1091  void computingMemoryWriters(WritersMode m) { computingMemoryWriters_ = m; }
1092  WritersMode computingMemoryWriters() const { return computingMemoryWriters_; }
1116  void computingRegisterWriters(WritersMode m) { computingRegisterWriters_ = m; }
1117  WritersMode computingRegisterWriters() const { return computingRegisterWriters_; }
1120  // Used internally to control whether cur_insn should be omitted from the list of definers.
1121  bool getset_omit_cur_insn(bool b) { bool retval = omit_cur_insn; omit_cur_insn=b; return retval; }
1122 
1129  void trimThreshold(uint64_t n) { trimThreshold_ = n; }
1130  uint64_t trimThreshold() const { return trimThreshold_; }
1139  size_t nTrimmed() const { return nTrimmed_; }
1140  void nTrimmed(size_t n) { nTrimmed_ = n; }
1150  bool reinterpretMemoryReads() const { return reinterpretMemoryReads_; }
1151  void reinterpretMemoryReads(bool b) { reinterpretMemoryReads_ = b; }
1152  bool reinterpretRegisterReads() const { return reinterpretRegisterReads_; }
1153  void reinterpretRegisterReads(bool b) { reinterpretRegisterReads_ = b; }
1156  // Methods first defined at this level of the class hierarchy
1158 public:
1220  virtual void substitute(const SValuePtr &from, const SValuePtr &to);
1221 
1226  virtual BaseSemantics::SValuePtr filterResult(const BaseSemantics::SValuePtr&);
1227 
1232  static SgAsmFloatType* sgIsIeee754(SgAsmType*);
1233 
1237  virtual SymbolicExpr::Type sgTypeToSymbolicType(SgAsmType*);
1238 
1240  // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
1241 public:
1242  virtual void interrupt(int majr, int minr) override;
1243  virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
1244  const BaseSemantics::SValuePtr &b_) override;
1245  virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_,
1246  const BaseSemantics::SValuePtr &b_) override;
1247  virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
1248  const BaseSemantics::SValuePtr &b_) override;
1249  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) override;
1250  virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
1251  size_t begin_bit, size_t end_bit) override;
1252  virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_,
1253  const BaseSemantics::SValuePtr &b_) override;
1254  virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) override;
1255  virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) override;
1256  virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_,
1257  const BaseSemantics::SValuePtr &sa_) override;
1258  virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_,
1259  const BaseSemantics::SValuePtr &sa_) override;
1260  virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_,
1261  const BaseSemantics::SValuePtr &sa_) override;
1262  virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_,
1263  const BaseSemantics::SValuePtr &sa_) override;
1264  virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_,
1265  const BaseSemantics::SValuePtr &sa_) override;
1266  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) override;
1267  virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
1268  const BaseSemantics::SValuePtr &a_,
1269  const BaseSemantics::SValuePtr &b_) override;
1270  virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
1271  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
1272  virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_,
1273  const BaseSemantics::SValuePtr &b_) override;
1274  virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_,
1275  const BaseSemantics::SValuePtr &b_,
1276  const BaseSemantics::SValuePtr &c_,
1277  BaseSemantics::SValuePtr &carry_out/*out*/) override;
1278  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) override;
1279  virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_,
1280  const BaseSemantics::SValuePtr &b_) override;
1281  virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_,
1282  const BaseSemantics::SValuePtr &b_) override;
1283  virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_,
1284  const BaseSemantics::SValuePtr &b_) override;
1285  virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_,
1286  const BaseSemantics::SValuePtr &b_) override;
1287  virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_,
1288  const BaseSemantics::SValuePtr &b_) override;
1289  virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_,
1290  const BaseSemantics::SValuePtr &b_) override;
1291  virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr &a, SgAsmFloatType *aType,
1292  SgAsmFloatType *retType) override;
1293  virtual BaseSemantics::SValuePtr reinterpret(const BaseSemantics::SValuePtr&, SgAsmType*) override;
1294  virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg,
1295  const BaseSemantics::SValuePtr &dflt) override;
1296  virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg,
1297  const BaseSemantics::SValuePtr &dflt) override;
1298  virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) override;
1300  const BaseSemantics::SValuePtr &addr,
1301  const BaseSemantics::SValuePtr &dflt,
1302  const BaseSemantics::SValuePtr &cond) override;
1304  const BaseSemantics::SValuePtr &addr,
1305  const BaseSemantics::SValuePtr &dflt) override;
1306  virtual void writeMemory(RegisterDescriptor segreg,
1307  const BaseSemantics::SValuePtr &addr,
1308  const BaseSemantics::SValuePtr &data,
1309  const BaseSemantics::SValuePtr &cond) override;
1310 
1311 public:
1312  BaseSemantics::SValuePtr readOrPeekMemory(RegisterDescriptor segreg,
1313  const BaseSemantics::SValuePtr &addr,
1314  const BaseSemantics::SValuePtr &dflt,
1315  AllowSideEffects::Flag);
1316 };
1317 
1318 } // namespace
1319 } // namespace
1320 } // namespace
1321 } // namespace
1322 
1323 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1328 #endif
1329 
1330 #endif
1331 #endif
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.
static RegisterStateGenericPtr instance(const SValuePtr &protoval, const RegisterDictionary *regdict)
Instantiate a new register state.
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.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
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.
virtual void set_width(size_t nbits) override
Virtual API.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
Leaf node of an expression tree for instruction semantics.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
Defines RISC operators for the SymbolicSemantics domain.
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
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 BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
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.
Base class for machine instructions.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
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.
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 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 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.
Holds a value or nothing.
Definition: Optional.h:49
static const unsigned UNSPECIFIED
Value is somehow unspecified.
Definition: SymbolicExpr.h:518
virtual void set_defining_instructions(const SValuePtr &source)
Set defining instructions.
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.
Type of symbolic expression.
Definition: SymbolicExpr.h:244
virtual BaseSemantics::SValuePtr boolean_(bool b) override
Returns a Boolean value.
void reinterpretRegisterReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual void defined_by(SgAsmInstruction *insn)
Adds instructions to the list of defining instructions.
void trimThreshold(uint64_t n)
Property: Maximum size of expressions.
virtual void set_comment(const std::string &) const override
Some subclasses support the ability to add comments to values.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override
Data-flow bottom value.
Main namespace for the ROSE library.
Controls formatting of expression trees when printing.
Definition: SymbolicExpr.h:184
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 readMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Read a byte from memory.
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
virtual SValuePtr boolean_(bool value)
Returns a Boolean value.
void reinterpretMemoryReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual std::string get_comment() const override
Some subclasses support the ability to add comments to values.
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.
static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override
Create a new unspecified semantic value.
DefinersMode
How to update the list of definers stored in each semantic value.
virtual uint64_t get_number() const override
Virtual API.
void computingMemoryWriters(WritersMode m)
Property: Track which instructions write to each memory location.
Base classes for instruction semantics.
Definition: Dispatcher.h:18
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
Definition: SymbolicExpr.h:522
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 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.
Describes (part of) a physical CPU register.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
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.
size_t nTrimmed() const
Property: Number of symbolic expressions trimmed.
Base class for semantics machine states.
Definition: State.h:39
virtual const InsnSet & get_defining_instructions() const
Returns the set of instructions that defined this value.
Functor for handling a memory read whose address matches more than one memory cell.
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 BaseSemantics::MemoryStatePtr clone() const override
Virtual copy constructor.
virtual const ExprPtr & get_expression() const
Returns the expression stored in this value.
CellCompressor::Ptr cellCompressor() const
Callback for handling a memory read whose address matches more than one memory cell.
bool reinterpretRegisterReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
uint64_t trimThreshold() const
Property: Maximum size of expressions.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified prototypical values.
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.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) override
Returns a number of the specified bit width.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override
Create a new concrete semantic value.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
Definition: RiscOperators.h:48
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const override
Virtual constructor.
boost::shared_ptr< MemoryCell > MemoryCellPtr
Shared-ownership pointer to a memory cell.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
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.
static StatePtr instance(const RegisterStatePtr &registers, const MemoryStatePtr &memory)
Instantiate a new state object with specified register and memory states.
Definition: State.h:81
Base class for binary types.
Base class for reference counted objects.
Definition: SharedObject.h:64
Type of values manipulated by the SymbolicSemantics domain.
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 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.
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.
Definition: SymbolicExpr.h:477
virtual bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
Functor for handling a memory read that found more than one cell that might alias the requested addre...
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override
Create a new undefined semantic value.
Defines registers available for a particular architecture.
Definition: Registers.h:37
Functor for handling a memory read whose address matches more than one memory cell.
virtual SValuePtr number_(size_t nbits, uint64_t value)
Returns a number of the specified bit width.
static SValuePtr instance_symbolic(const SymbolicExpr::Ptr &value)
Instantiate a new symbolic value.
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::MemoryStatePtr clone() const override
Virtual copy constructor.
MergerPtr Ptr
Shared-ownership pointer for a Merger object.
virtual BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
void nTrimmed(size_t n)
Property: Number of symbolic expressions trimmed.
Floating point types.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
Functor for handling a memory read whose address matches more than one memory cell.
Functor for handling a memory read whose address matches more than one memory cell.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:26
virtual bool isBottom() const override
Determines whether a value is a data-flow bottom.
boost::shared_ptr< class MemoryListState > MemoryListStatePtr
Shared-ownership pointer for symbolic list-based memory state.