ROSE  0.11.51.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 ROSE_OVERRIDE {
277  return instance_bottom(nbits);
278  }
279  virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE {
280  return instance_undefined(nbits);
281  }
282  virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE {
283  return instance_unspecified(nbits);
284  }
285  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE {
286  return instance_integer(nbits, value);
287  }
288  virtual BaseSemantics::SValuePtr boolean_(bool value) const ROSE_OVERRIDE {
289  return instance_integer(1, value?1:0);
290  }
291  virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_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 ROSE_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 ROSE_OVERRIDE;
315 
316  virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_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 ROSE_OVERRIDE;
323  virtual bool must_equal(const BaseSemantics::SValuePtr &other,
324  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_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) ROSE_OVERRIDE {
329  ASSERT_require(nbits==nBits());
330  }
331 
332  virtual bool is_number() const ROSE_OVERRIDE {
333  return expr->isIntegerConstant();
334  }
335 
336  virtual uint64_t get_number() const ROSE_OVERRIDE;
337 
338  virtual std::string get_comment() const ROSE_OVERRIDE;
339  virtual void set_comment(const std::string&) const ROSE_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 
481  struct CellCompressor {
482  virtual ~CellCompressor() {}
483  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
485  const MemoryCellList::CellList &cells) = 0;
486  };
487 
502  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
504  const CellList &cells) ROSE_OVERRIDE;
505  };
506 
509  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
511  const CellList &cells) ROSE_OVERRIDE;
512  };
513 
518  CellCompressorMcCarthy cc_mccarthy;
519  CellCompressorSimple cc_simple;
520  virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
522  const CellList &cells) ROSE_OVERRIDE;
523  };
524 
525 protected:
529  // Serialization
531 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
532 private:
533  friend class boost::serialization::access;
534 
535  template<class S>
536  void serialize(S &s, const unsigned /*version*/) {
537  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
538  }
539 #endif
540 
541 
543  // Real constructors
544 protected:
545  MemoryListState() // for serialization
546  : cell_compressor(&cc_choice) {}
547 
548  explicit MemoryListState(const BaseSemantics::MemoryCellPtr &protocell)
549  : BaseSemantics::MemoryCellList(protocell), cell_compressor(&cc_choice) {}
550 
551  MemoryListState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
552  : BaseSemantics::MemoryCellList(addrProtoval, valProtoval), cell_compressor(&cc_choice) {}
553 
554  MemoryListState(const MemoryListState &other)
555  : BaseSemantics::MemoryCellList(other), cell_compressor(other.cell_compressor) {}
556 
558  // Static allocating constructors
559 public:
561  static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
562  return MemoryListStatePtr(new MemoryListState(protocell));
563  }
564 
567  static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
568  const BaseSemantics::SValuePtr &valProtoval) {
569  return MemoryListStatePtr(new MemoryListState(addrProtoval, valProtoval));
570  }
571 
573  static MemoryListStatePtr instance(const MemoryListStatePtr &other) {
574  return MemoryListStatePtr(new MemoryListState(*other));
575  }
576 
578  // Virtual constructors
579 public:
583  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
584  return instance(addrProtoval, valProtoval);
585  }
586 
588  virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const ROSE_OVERRIDE {
589  return instance(protocell);
590  }
591 
593  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
595  }
596 
598  // Dynamic pointer casts
599 public:
602  static MemoryListStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
603  MemoryListStatePtr retval = boost::dynamic_pointer_cast<MemoryListState>(x);
604  ASSERT_not_null(retval);
605  return retval;
606  }
607 
609  // Methods we inherited
610 public:
616  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
617 
623  BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
624 
628  virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
629  BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
630 
631 protected:
632  BaseSemantics::SValuePtr readOrPeekMemory(const BaseSemantics::SValuePtr &address,
633  const BaseSemantics::SValuePtr &dflt,
636  AllowSideEffects::Flag allowSideEffects);
637 
639  // Methods first declared in this class
640 public:
645  void set_cell_compressor(CellCompressor *cc) { cell_compressor = cc; }
647 };
648 
649 
651 // Map-based Memory state
653 
655 typedef boost::shared_ptr<class MemoryMapState> MemoryMapStatePtr;
656 
675 public:
678 
681 
683  // Serialization
684 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
685 private:
686  friend class boost::serialization::access;
687 
688  template<class S>
689  void serialize(S &s, const unsigned /*version*/) {
690  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
691  }
692 #endif
693 
695  // Real constructors
696 protected:
697  MemoryMapState() {} // for serialization
698 
699  explicit MemoryMapState(const BaseSemantics::MemoryCellPtr &protocell)
700  : BaseSemantics::MemoryCellMap(protocell) {}
701 
702  MemoryMapState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
703  : BaseSemantics::MemoryCellMap(addrProtoval, valProtoval) {}
704 
706  // Static allocating constructors
707 public:
709  static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell) {
710  return MemoryMapStatePtr(new MemoryMapState(protocell));
711  }
712 
715  static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval,
716  const BaseSemantics::SValuePtr &valProtoval) {
717  return MemoryMapStatePtr(new MemoryMapState(addrProtoval, valProtoval));
718  }
719 
721  static MemoryMapStatePtr instance(const MemoryMapStatePtr &other) {
722  return MemoryMapStatePtr(new MemoryMapState(*other));
723  }
724 
726  // Virtual constructors
727 public:
731  const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
732  return instance(addrProtoval, valProtoval);
733  }
734 
737  return instance(protocell);
738  }
739 
741  virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE {
743  }
744 
746  // Dynamic pointer casts
747 public:
750  static MemoryMapStatePtr promote(const BaseSemantics::MemoryStatePtr &x) {
751  MemoryMapStatePtr retval = boost::dynamic_pointer_cast<MemoryMapState>(x);
752  ASSERT_not_null(retval);
753  return retval;
754  }
755 
757  // Methods we override from the super class (documented in the super class)
758 public:
759  virtual CellKey generateCellKey(const BaseSemantics::SValuePtr &addr_) const ROSE_OVERRIDE;
760 };
761 
762 
763 
765 // Default memory state
767 
768 // List-base memory was the type originally used by this domain. We must keep it that way because some analysis, including 3rd
769 // party, assumes that the state is list-based. New analysis can use the map-based state by instantiating it when the symbolic
770 // risc operators are constructed.
771 typedef MemoryListState MemoryState;
772 typedef MemoryListStatePtr MemoryStatePtr;
773 
775 // Complete state
777 
778 typedef BaseSemantics::State State;
779 typedef BaseSemantics::StatePtr StatePtr;
780 
781 
783 // RISC operators
785 
791 };
792 
798 };
799 
801 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
802 
823 public:
826 
829 
830 protected:
831  bool omit_cur_insn; // if true, do not include cur_insn as a definer
832  DefinersMode computingDefiners_; // whether to track definers (instruction VAs) of SValues
833  WritersMode computingMemoryWriters_; // whether to track writers (instruction VAs) to memory.
834  WritersMode computingRegisterWriters_; // whether to track writers (instruction VAs) to registers.
835  size_t trimThreshold_; // max size of expressions (zero means no maximimum)
836  bool reinterpretMemoryReads_; // cast data to unsigned integer when reading from memory
837  bool reinterpretRegisterReads_; // cast data to unsigned integer when reading from registers
838 
839 
841  // Serialization
842 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
843 private:
844  friend class boost::serialization::access;
845 
846  template<class S>
847  void serialize(S &s, const unsigned /*version*/) {
848  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
849  s & BOOST_SERIALIZATION_NVP(omit_cur_insn);
850  s & BOOST_SERIALIZATION_NVP(computingDefiners_);
851  s & BOOST_SERIALIZATION_NVP(computingMemoryWriters_);
852  s & BOOST_SERIALIZATION_NVP(computingRegisterWriters_);
853  s & BOOST_SERIALIZATION_NVP(trimThreshold_);
854  }
855 #endif
856 
858  // Real constructors
859 protected:
860  RiscOperators() // for serialization
861  : omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS), computingMemoryWriters_(TRACK_LATEST_WRITER),
862  computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0), reinterpretMemoryReads_(true),
863  reinterpretRegisterReads_(true) {}
864 
865  explicit RiscOperators(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr())
866  : BaseSemantics::RiscOperators(protoval, solver), omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS),
867  computingMemoryWriters_(TRACK_LATEST_WRITER), computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0),
868  reinterpretMemoryReads_(true), reinterpretRegisterReads_(true) {
869  name("Symbolic");
870  ASSERT_always_not_null(protoval);
871  ASSERT_always_not_null2(protoval.dynamicCast<SValue>(),
872  "SymbolicSemantics supports only symbolic SValue types or derivatives thereof");
873  }
874 
875  explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr())
876  : BaseSemantics::RiscOperators(state, solver), omit_cur_insn(false), computingDefiners_(TRACK_NO_DEFINERS),
877  computingMemoryWriters_(TRACK_LATEST_WRITER), computingRegisterWriters_(TRACK_LATEST_WRITER), trimThreshold_(0),
878  reinterpretMemoryReads_(true), reinterpretRegisterReads_(true) {
879  name("Symbolic");
880  ASSERT_always_not_null(state);
881  ASSERT_always_not_null(state->registerState());
882  ASSERT_always_not_null2(boost::dynamic_pointer_cast<RegisterState>(state->registerState()),
883  "SymbolicSemantics supports only RegisterStateGeneric or derivatives thereof");
884  ASSERT_always_not_null(state->protoval());
885  ASSERT_always_not_null2(state->protoval().dynamicCast<SValue>(),
886  "SymbolicSemantics supports only symbolic SValue types or derivatives thereof");
887  }
888 
890  // Static allocating constructors
891 public:
894  static RiscOperatorsPtr instance(const RegisterDictionary *regdict, const SmtSolverPtr &solver = SmtSolverPtr()) {
896  BaseSemantics::RegisterStatePtr registers = RegisterState::instance(protoval, regdict);
897  BaseSemantics::MemoryStatePtr memory = MemoryListState::instance(protoval, protoval);
898  BaseSemantics::StatePtr state = State::instance(registers, memory);
899  return RiscOperatorsPtr(new RiscOperators(state, solver));
900  }
901 
904  static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr()) {
905  return RiscOperatorsPtr(new RiscOperators(protoval, solver));
906  }
907 
910  static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr()) {
911  return RiscOperatorsPtr(new RiscOperators(state, solver));
912  }
913 
915  // Virtual constructors
916 public:
918  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
919  return instance(protoval, solver);
920  }
921 
923  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
924  return instance(state, solver);
925  }
926 
928  // Dynamic pointer casts
929 public:
932  static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
933  RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
934  ASSERT_not_null(retval);
935  return retval;
936  }
937 
939  // Inherited methods for constructing values.
940 public:
941  virtual BaseSemantics::SValuePtr boolean_(bool b) ROSE_OVERRIDE {
943  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
944  retval->defined_by(currentInstruction());
945  return retval;
946  }
947 
948  virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) ROSE_OVERRIDE {
949  SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
950  if (computingDefiners() != TRACK_NO_DEFINERS && !omit_cur_insn)
951  retval->defined_by(currentInstruction());
952  return retval;
953  }
954 
956  // New methods for constructing values, so we don't have to write so many SValue::promote calls in the RiscOperators
957  // implementations.
958  SValuePtr svalueExpr(const ExprPtr &expr, const InsnSet &defs=InsnSet()) {
959  SValuePtr newval = SValue::promote(protoval()->undefined_(expr->nBits()));
960  newval->set_expression(expr);
961  newval->set_defining_instructions(defs);
962  return newval;
963  }
964 
965 protected:
966  SValuePtr svalueUndefined(size_t nbits) {
967  return SValue::promote(undefined_(nbits));
968  }
969 
970  SValuePtr svalueBottom(size_t nbits) {
971  return SValue::promote(bottom_(nbits));
972  }
973 
974  SValuePtr svalueUnspecified(size_t nbits) {
975  return SValue::promote(unspecified_(nbits));
976  }
977 
978  SValuePtr svalueNumber(size_t nbits, uint64_t value) {
979  return SValue::promote(number_(nbits, value));
980  }
981 
982  SValuePtr svalueBoolean(bool b) {
983  return SValue::promote(boolean_(b));
984  }
985 
986  // [Robb Matzke 2021-03-18]: deprecated
987  SValuePtr svalue_number(size_t nbits, uint64_t value) ROSE_DEPRECATED("use svalueNumber instead") {
988  return svalueNumber(nbits, value);
989  }
990 
991  // [Robb Matzke 2021-03-18]: deprecated
992  SValuePtr svalue_boolean(bool b) ROSE_DEPRECATED("use svalueBoolean instead") {
993  return svalueBoolean(b);
994  }
995 
996  // [Robb Matzke 2021-03-18]: deprecated
997  SValuePtr svalue_unspecified(size_t nbits) ROSE_DEPRECATED("use svalueUnspecified instead") {
998  return svalueUnspecified(nbits);
999  }
1000 
1001  // [Robb Matzke 2021-03-18]: deprecated
1002  SValuePtr svalue_bottom(size_t nbits) ROSE_DEPRECATED("use svalueBottom instead") {
1003  return svalueBottom(nbits);
1004  }
1005 
1006  // [Robb Matzke 2021-03-18]: deprecated
1007  SValuePtr svalue_undefined(size_t nbits) ROSE_DEPRECATED("use svalueUndefined instead") {
1008  return svalueUndefined(nbits);
1009  }
1010 
1011  // [Robb Matzke 2021-03-18]: deprecated
1012  SValuePtr svalue_expr(const ExprPtr &expr, const InsnSet &defs=InsnSet()) ROSE_DEPRECATED("use svalueExpr instead") {
1013  return svalueExpr(expr, defs);
1014  }
1015 
1017  // Configuration properties
1018 public:
1019 
1037  void computingDefiners(DefinersMode m) { computingDefiners_ = m; }
1038  DefinersMode computingDefiners() const { return computingDefiners_; }
1059  void computingMemoryWriters(WritersMode m) { computingMemoryWriters_ = m; }
1060  WritersMode computingMemoryWriters() const { return computingMemoryWriters_; }
1084  void computingRegisterWriters(WritersMode m) { computingRegisterWriters_ = m; }
1085  WritersMode computingRegisterWriters() const { return computingRegisterWriters_; }
1088  // Used internally to control whether cur_insn should be omitted from the list of definers.
1089  bool getset_omit_cur_insn(bool b) { bool retval = omit_cur_insn; omit_cur_insn=b; return retval; }
1090 
1097  void trimThreshold(size_t n) { trimThreshold_ = n; }
1098  size_t trimThreshold() const { return trimThreshold_; }
1108  bool reinterpretMemoryReads() const { return reinterpretMemoryReads_; }
1109  void reinterpretMemoryReads(bool b) { reinterpretMemoryReads_ = b; }
1110  bool reinterpretRegisterReads() const { return reinterpretRegisterReads_; }
1111  void reinterpretRegisterReads(bool b) { reinterpretRegisterReads_ = b; }
1114  // Methods first defined at this level of the class hierarchy
1116 public:
1178  virtual void substitute(const SValuePtr &from, const SValuePtr &to);
1179 
1185 
1191 
1196 
1198  // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
1199 public:
1200  virtual void interrupt(int majr, int minr) ROSE_OVERRIDE;
1202  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1204  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1206  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1207  virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1209  size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
1211  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1215  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1217  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1219  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1221  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1223  const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE;
1224  virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1226  const BaseSemantics::SValuePtr &a_,
1227  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1228  virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
1229  virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE;
1231  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1233  const BaseSemantics::SValuePtr &b_,
1234  const BaseSemantics::SValuePtr &c_,
1235  BaseSemantics::SValuePtr &carry_out/*out*/) ROSE_OVERRIDE;
1236  virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1238  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1240  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1242  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1244  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1246  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1248  const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE;
1250  SgAsmFloatType *retType) ROSE_OVERRIDE;
1252  virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg,
1253  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
1254  virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg,
1255  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
1256  virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE;
1257  virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg,
1258  const BaseSemantics::SValuePtr &addr,
1259  const BaseSemantics::SValuePtr &dflt,
1260  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
1261  virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg,
1262  const BaseSemantics::SValuePtr &addr,
1263  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
1264  virtual void writeMemory(RegisterDescriptor segreg,
1265  const BaseSemantics::SValuePtr &addr,
1266  const BaseSemantics::SValuePtr &data,
1267  const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
1268 
1269 public:
1270  BaseSemantics::SValuePtr readOrPeekMemory(RegisterDescriptor segreg,
1271  const BaseSemantics::SValuePtr &addr,
1272  const BaseSemantics::SValuePtr &dflt,
1273  AllowSideEffects::Flag);
1274 };
1275 
1276 } // namespace
1277 } // namespace
1278 } // namespace
1279 } // namespace
1280 
1281 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1286 #endif
1287 
1288 #endif
1289 #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.
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.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
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.
bool reinterpretMemoryReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual SgAsmInstruction * currentInstruction() const
Property: 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.
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.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual API.
CellCompressor * cell_compressor
Callback when a memory read aliases multiple memory cells.
static CellCompressorChoice cc_choice
The default cell compressor.
static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified state.
virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const
Substitute one value for another throughout a value.
virtual BaseSemantics::SValuePtr filterResult(const BaseSemantics::SValuePtr &)
Filters results from RISC operators.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Divides two signed values.
virtual void set_comment(const std::string &) const ROSE_OVERRIDE
Some subclasses support the ability to add comments to values.
Base class for machine instructions.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
virtual BaseSemantics::MemoryStatePtr clone() const ROSE_OVERRIDE
Virtual copy constructor.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const ROSE_OVERRIDE
Virtual constructor.
virtual uint64_t get_number() const ROSE_OVERRIDE
Virtual API.
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.
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
Returns position of most significant set bit; zero when no bits are set.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual API.
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 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.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual allocating constructor.
STL namespace.
Holds a value or nothing.
Definition: Optional.h:49
static const unsigned UNSPECIFIED
Value is somehow unspecified.
Definition: SymbolicExpr.h:499
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.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x)
Run-time promotion of a base RiscOperators pointer to symbolic operators.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const ROSE_OVERRIDE
Create a new concrete semantic value.
Type of symbolic expression.
Definition: SymbolicExpr.h:225
virtual void interrupt(int majr, int minr) ROSE_OVERRIDE
Invoked for instructions that cause an interrupt.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
void reinterpretRegisterReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
Multiplies two signed values.
virtual 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.
Definition: SymbolicExpr.h:174
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 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 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.
static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
virtual SymbolicExpr::Type sgTypeToSymbolicType(SgAsmType *)
Convert a SgAsmType to a symbolic type.
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.
virtual Sawyer::Optional< BaseSemantics::SValuePtr > createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const ROSE_OVERRIDE
Possibly create a new value by merging two existing values.
void computingMemoryWriters(WritersMode m)
Property: Track which instructions write to each memory location.
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.
Definition: Dispatcher.h:18
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
Definition: SymbolicExpr.h:503
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.
Describes (part of) a physical CPU register.
Functor for handling a memory read that found more than one cell that might alias the requested addre...
boost::shared_ptr< class MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to symbolic memory state.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const
Virtual constructor.
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 BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
Virtual allocating constructor.
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.
static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
DefinersMode computingDefiners() const
Property: Track which instructions define a semantic value.
virtual std::string get_comment() const ROSE_OVERRIDE
Some subclasses support the ability to add comments to values.
virtual const ExprPtr & get_expression() const
Returns the expression stored in this value.
bool reinterpretRegisterReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified prototypical values.
virtual void substitute(const SValuePtr &from, const SValuePtr &to)
Substitute all occurrences of from with to in the current state.
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.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
Definition: RiscOperators.h:48
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.
boost::shared_ptr< MemoryCell > MemoryCellPtr
Shared-ownership pointer to a memory cell.
virtual void set_width(size_t nbits) ROSE_OVERRIDE
Virtual API.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
Rotate bits to the right.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
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.
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.
size_t trimThreshold() const
Property: Maximum size of expressions.
Type of values manipulated by the SymbolicSemantics domain.
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Write a byte to memory.
virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
Read memory without side effects.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1)
Adds instructions to the list of defining instructions.
static SValuePtr instance_unspecified(size_t nbits)
Instantiate a new unspecified value of specified width.
virtual BaseSemantics::SValuePtr reinterpret(const BaseSemantics::SValuePtr &, SgAsmType *) ROSE_OVERRIDE
Reinterpret an expression as a different type.
virtual BaseSemantics::SValuePtr boolean_(bool value) const ROSE_OVERRIDE
Create a new, Boolean value.
virtual CellKey generateCellKey(const BaseSemantics::SValuePtr &addr_) const ROSE_OVERRIDE
Generate a cell lookup key.
virtual SValuePtr unspecified_(size_t nbits)
Returns a new undefined value.
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.
Definition: SymbolicExpr.h:458
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE
Data-flow bottom value.
virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr &a, SgAsmFloatType *aType, SgAsmFloatType *retType) ROSE_OVERRIDE
Convert from one floating-point type to another.
virtual BaseSemantics::SValuePtr 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.
Defines registers available for a particular architecture.
Definition: Registers.h:37
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
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 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.
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.
MergerPtr Ptr
Shared-ownership pointer for a Merger object.
virtual BaseSemantics::SValuePtr peekMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
Read a byte from memory with no side effects.
Functor for handling a memory read whose address matches more than one memory cell.
virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE
Reads a value from memory.
Floating point types.
virtual BaseSemantics::SValuePtr 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.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
static SgAsmFloatType * sgIsIeee754(SgAsmType *)
Tests whether a SgAsmType is an IEEE-754 floating-point type.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:25
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).