ROSE  0.11.83.2
SymbolicExpr.h
1 #ifndef ROSE_BinaryAnalysis_SymbolicExpr_H
2 #define ROSE_BinaryAnalysis_SymbolicExpr_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 
10 #include "Map.h"
11 
12 #include <boost/any.hpp>
13 #include <boost/lexical_cast.hpp>
14 #include <boost/logic/tribool.hpp>
15 #include <boost/serialization/access.hpp>
16 #include <boost/serialization/base_object.hpp>
17 #include <boost/serialization/export.hpp>
18 #include <boost/serialization/split_member.hpp>
19 #include <boost/serialization/string.hpp>
20 #include <boost/serialization/vector.hpp>
21 #include <boost/unordered_map.hpp>
22 #include <cassert>
23 #include <inttypes.h>
24 #include <Rose/Exception.h>
25 #include <Sawyer/Attribute.h>
26 #include <Sawyer/BitVector.h>
27 #include <Sawyer/Optional.h>
28 #include <Sawyer/Set.h>
29 #include <Sawyer/SharedPointer.h>
30 #include <Sawyer/SmallObject.h>
31 #include <set>
32 #include <string>
33 #include <vector>
34 
35 namespace Rose {
36 namespace BinaryAnalysis {
37 
38 class SmtSolver;
39 using SmtSolverPtr = std::shared_ptr<SmtSolver>;
40 
46 namespace SymbolicExpr {
47 
49 // Basic Types and settings
51 
60 extern bool serializeVariableIds;
61 
63 namespace TypeStyle {
65  enum Flag {
66  FULL,
68  };
69 }
70 
71 
73 class Exception: public Rose::Exception {
74 public:
75  explicit Exception(const std::string &mesg): Rose::Exception(mesg) {}
76 };
77 
83 enum Operator {
156  OP_BV_AND = OP_AND, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
157  OP_BV_OR = OP_OR, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
158  OP_BV_XOR = OP_XOR // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
159 };
160 
161 std::string toStr(Operator);
162 
163 class Node;
164 class Interior;
165 class Leaf;
167 
170 
173 
176 
177 typedef std::vector<Ptr> Nodes;
179 
181 typedef uint64_t Hash;
182 
184 struct Formatter {
189  };
190  Formatter()
192  max_depth(0), cur_depth(0), show_type(true), show_flags(true) {}
194  bool do_rename;
195  bool add_renames;
197  size_t max_depth;
198  size_t cur_depth;
199  RenameMap renames;
200  bool show_type;
201  bool show_flags;
202 };
203 
209 };
210 
215 extern const uint64_t MAX_NNODES; // defined in .C so we don't pollute user namespace with limit macros
216 
228 class Visitor {
229 public:
230  virtual ~Visitor() {}
231 
232  virtual VisitAction preVisit(const Ptr&);
233  virtual VisitAction postVisit(const Ptr&);
234 
235  virtual VisitAction preVisit(const Node*);
236  virtual VisitAction postVisit(const Node*);
237 };
238 
240 // Expression type information
242 
244 class Type {
245 public:
247  enum TypeClass {
249  FP,
252  };
253 
254 private:
255  // We use a 32-bit data member and pack into it the totalWidth (15 bits: 0 through 14), the secondaryWidth (15 bits: 15 through 29),
256  // and the type class (2 bits: 30 and 31).
257  uint32_t fields_;
258 
259 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
260 private:
261  friend class boost::serialization::access;
262 
263  template<class S>
264  void serialize(S &s, const unsigned version) {
265  if (version >= 1) {
266  s & BOOST_SERIALIZATION_NVP(fields_);
267  } else {
268  TypeClass t = typeClass();
269  size_t z1 = nBits();
270  size_t z2 = secondaryWidth();
271  s & boost::serialization::make_nvp("typeClass_", t);
272  s & boost::serialization::make_nvp("totalWidth_", z1);
273  s & boost::serialization::make_nvp("secondaryWidth_", z2);
274  typeClass(t);
275  nBits(z1);
276  secondaryWidth(z2);
277  }
278  }
279 #endif
280 
284 public:
286  : fields_(0) {
288  nBits(0);
289  secondaryWidth(0);
290  }
291 
292 private:
293  Type(TypeClass tc, size_t w1, size_t w2)
294  : fields_(0) {
295  typeClass(tc);
296  nBits(w1);
297  secondaryWidth(w2);
298  }
299 
300 public:
304  static Type none() {
305  return Type();
306  }
307 
313  static Type integer(size_t nBits) {
314  return Type(INTEGER, nBits, 0);
315  }
316 
320  static Type memory(size_t addressWidth, size_t valueWidth) {
321  return Type(MEMORY, valueWidth, addressWidth);
322  }
323 
333  return Type(FP, 1 /*sign bit*/ + exponentWidth + significandWidth - 1 /*implied bit*/, exponentWidth);
334  }
335 
339  bool isValid() const {
340  return typeClass() != INVALID;
341  }
342 
347  return (TypeClass)((fields_ >> 30) & 0x3);
348  }
349 
354  size_t nBits() const {
355  return fields_ & 0x7fff;
356  }
357 
362  size_t addressWidth() const {
363  ASSERT_require(MEMORY == typeClass());
364  return secondaryWidth();
365  }
366 
371  size_t exponentWidth() const {
372  ASSERT_require(FP == typeClass());
373  return secondaryWidth();
374  }
375 
381  size_t significandWidth() const {
382  ASSERT_require(FP == typeClass());
383  ASSERT_require(nBits() > 1 /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
384  return nBits() - (1 /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
385  }
386 
392  bool operator==(const Type &other) const {
393  return fields_ == other.fields_;
394  }
395  bool operator!=(const Type &other) const {
396  return !(*this == other);
397  }
401  bool operator<(const Type &other) const;
402 
404  void print(std::ostream&, TypeStyle::Flag style = TypeStyle::FULL) const;
405 
407  std::string toString(TypeStyle::Flag style = TypeStyle::FULL) const;
408 
409 private:
410  // mutators are all private
411  void typeClass(TypeClass tc) {
412  unsigned n = tc;
413  ASSERT_require(n <= 3);
414  fields_ = (fields_ & 0x3fffffff) | (n << 30);
415  }
416 
417  // mutators are all private
418  void nBits(size_t n) {
419  if (n > 0x7fff)
420  throw Exception("type width is out of range");
421  fields_ = (fields_ & 0xffff8000) | n;
422  }
423 
424  // mutators are all private
425  void secondaryWidth(size_t n) {
426  if (n > 0x7fff)
427  throw Exception("second width is out of range");
428  fields_ = (fields_ & 0xc0007fff) | (n << 15);
429  }
430 
431  size_t secondaryWidth() const {
432  return (fields_ >> 15) & 0x7fff;
433  }
434 };
435 
437 // Base Node Type
439 
477 class Node
478  : public Sawyer::SharedObject,
479  public Sawyer::SharedFromThis<Node>,
480  public Sawyer::SmallObject,
481  public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
482 protected:
483  Type type_;
484  unsigned flags_;
485  std::string comment_;
486  mutable Hash hashval_;
487  boost::any userData_;
489 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
490 private:
491  friend class boost::serialization::access;
492 
493  template<class S>
494  void serialize(S &s, const unsigned version) {
495  if (version < 1)
496  ASSERT_not_reachable("SymbolicExpr version " + boost::lexical_cast<std::string>(version) + " is no longer supported");
497  s & BOOST_SERIALIZATION_NVP(type_);
498  s & BOOST_SERIALIZATION_NVP(flags_);
499  s & BOOST_SERIALIZATION_NVP(comment_);
500  s & BOOST_SERIALIZATION_NVP(hashval_);
501  // s & userData_;
502  }
503 #endif
504 
505 public:
506  // Bit flags
507 
509  static const unsigned RESERVED_FLAGS = 0x0000ffff;
510 
512  static const unsigned INDETERMINATE = 0x00000001;
513 
518  static const unsigned UNSPECIFIED = 0x00000002;
519 
522  static const unsigned BOTTOM = 0x00000004;
523 
524 protected:
525  Node()
526  : type_(Type::integer(0)), flags_(0), hashval_(0) {}
527  explicit Node(const std::string &comment, unsigned flags=0)
528  : type_(Type::integer(0)), flags_(flags), comment_(comment), hashval_(0) {}
529 
530 public:
532  Type type() const {
533  return type_;
534  }
535 
542  static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
543 
549  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
550 
552  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
553 
559  virtual bool isEquivalentTo(const Ptr &other) = 0;
560 
566  virtual int compareStructure(const Ptr &other) = 0;
567 
573  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
574 
582  Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
583 
591  Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
592  const SmtSolverPtr &solver = SmtSolverPtr());
593 
597  virtual Operator getOperator() const = 0;
598 
602  virtual size_t nChildren() const = 0;
603 
610  virtual const Ptr& child(size_t idx) const = 0;
611  virtual const Node* childRaw(size_t idx) const = 0;
617  virtual const Nodes& children() const = 0;
618 
623  virtual Sawyer::Optional<uint64_t> toUnsigned() const = 0;
624 
628  virtual Sawyer::Optional<int64_t> toSigned() const = 0;
629 
631  bool isIntegerExpr() const {
632  return type_.typeClass() == Type::INTEGER;
633  }
634 
636  bool isFloatingPointExpr() const {
637  return type_.typeClass() == Type::FP;
638  }
639 
641  bool isMemoryExpr() const {
642  return type_.typeClass() == Type::MEMORY;
643  }
644 
648  bool isScalarExpr() const {
649  return isIntegerExpr() || isFloatingPointExpr();
650  }
651 
653  virtual bool isConstant() const = 0;
654 
656  bool isIntegerConstant() const {
657  return isIntegerExpr() && isConstant();
658  }
659 
661  bool isFloatingPointConstant() const {
662  return isFloatingPointExpr() && isConstant();
663  }
664 
668  bool isScalarConstant() const {
670  }
671 
673  bool isFloatingPointNan() const;
674 
680  virtual bool isVariable2() const = 0;
681 
686 
688  bool isIntegerVariable() const {
689  return isIntegerExpr() && isVariable2();
690  }
691 
693  bool isFloatingPointVariable() const {
694  return isFloatingPointExpr() && isVariable2();
695  }
696 
698  bool isMemoryVariable() const {
699  return isMemoryExpr() && isVariable2();
700  }
701 
705  bool isScalarVariable() const {
707  }
708 
717  const std::string& comment() const {
718  return comment_;
719  }
720  void comment(const std::string &s) {
721  comment_ = s;
722  }
732  void userData(boost::any &data) {
733  userData_ = data;
734  }
735  const boost::any& userData() const {
736  return userData_;
737  }
743  size_t nBits() const {
744  return type_.nBits();
745  }
746 
751  unsigned flags() const {
752  return flags_;
753  }
754 
758  Ptr newFlags(unsigned flags) const;
759 
763  size_t domainWidth() const {
764  return type_.addressWidth();
765  }
766 
770  bool isScalar() const {
771  return type_.typeClass() != Type::MEMORY;
772  }
773 
778  virtual VisitAction depthFirstTraversal(Visitor&) const = 0;
779 
795  virtual uint64_t nNodes() const = 0;
796 
798  uint64_t nNodesUnique() const;
799 
801  std::set<LeafPtr> getVariables() const;
802 
808  InteriorPtr isInteriorNode() const;
809  Interior* isInteriorNodeRaw() const;
817  LeafPtr isLeafNode() const;
818  Leaf* isLeafNodeRaw() const;
824  bool isHashed() const {
825  return hashval_ != 0;
826  }
827 
830  Hash hash() const;
831 
832  // used internally to set the hash value
833  void hash(Hash) const;
834 
837  private:
838  Ptr node;
839  Formatter &formatter;
840  public:
841  WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
842  void print(std::ostream &stream) const { node->print(stream, formatter); }
843  };
844 
866  virtual void print(std::ostream&, Formatter&) const = 0;
867  void print(std::ostream &o) const { Formatter fmt; print(o, fmt); }
871  std::string toString() const;
872 
874  void assertAcyclic() const;
875 
881  std::vector<Ptr> findCommonSubexpressions() const;
882 
888  bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/) const;
889 
891  InteriorPtr isOperator(Operator) const;
892 
893 protected:
894  void printFlags(std::ostream &o, unsigned flags, char &bracket) const;
895 
896 public: // only used internally
897  using EquivPairs = std::map<Node*, std::vector<std::pair<Node*, bool>>>;
898  virtual bool isEquivalentHelper(Node*, EquivPairs&) = 0;
899 };
900 
902 class Simplifier {
903 public:
904  virtual ~Simplifier() {}
905 
909  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
910  return Ptr();
911  }
912 
915  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
916  return Ptr();
917  }
918 };
919 
921  size_t operator()(const Ptr &expr) const {
922  return expr->hash();
923  }
924 };
925 
927  bool operator()(const Ptr &a, const Ptr &b) const {
928  return a->isEquivalentTo(b);
929  }
930 };
931 
934 public:
935  bool operator()(const Ptr &a, const Ptr &b) const;
936 };
937 
939 class ExprExprHashMap: public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
940  ExprExprHashMapHasher, ExprExprHashMapCompare> {
941 public:
942  ExprExprHashMap invert() const;
943 };
944 
947 
948 
950 // Simplification
952 
954  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
955  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
956 };
958  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
959  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
960 };
962  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
963 };
965  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
966  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
967 };
969  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
970  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
971 };
973  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
974 };
976  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
977 };
979  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
980  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
981 };
983  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
984 };
986  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
987 };
989  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
990 };
992  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
993 };
995  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
996 };
998  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
999 };
1001  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1002 };
1004  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1005 };
1007  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1008 };
1010  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1011 };
1013  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1014 };
1016  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1017 };
1019  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1020 };
1022  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1023 };
1025  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1026 };
1028  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1029 };
1031  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1032 };
1034  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1035 };
1037  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1038 };
1040  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1041 };
1043  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1044 };
1046  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1047 };
1049  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1050 };
1052  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1053 };
1055  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1056 };
1058  bool newbits;
1059  ShiftSimplifier(bool newbits): newbits(newbits) {}
1060  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
1061 };
1063  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1064  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1065 };
1067  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1068  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1069 };
1071  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1072 };
1074  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1075 };
1077  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1078 };
1079 
1080 
1081 
1083 // Interior Nodes
1085 
1092 class Interior: public Node {
1093 private:
1094  Operator op_;
1095  Nodes children_;
1096  uint64_t nnodes_; // total number of nodes; self + children's nnodes
1097 
1098  //--------------------------------------------------------
1099  // Serialization
1100  //--------------------------------------------------------
1101 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1102 private:
1103  friend class boost::serialization::access;
1104 
1105  template<class S>
1106  void serialize(S &s, const unsigned /*version*/) {
1107  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1108  s & BOOST_SERIALIZATION_NVP(op_);
1109  s & BOOST_SERIALIZATION_NVP(children_);
1110  s & BOOST_SERIALIZATION_NVP(nnodes_);
1111  }
1112 #endif
1113 
1114  //--------------------------------------------------------
1115  // Real constructors
1116  //--------------------------------------------------------
1117 private:
1118  Interior(); // needed for serialization
1119  // Only constructs, does not simplify.
1120  Interior(const Type&, Operator, const Nodes &arguments, const std::string &comment, unsigned flags);
1121 
1122  //--------------------------------------------------------
1123  // Allocating constructors
1124  //--------------------------------------------------------
1125 public:
1129  static Ptr instance(Operator op, const Ptr &a,
1130  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1131  static Ptr instance(const Type &type, Operator op, const Ptr &a,
1132  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1133  static Ptr instance(Operator op, const Ptr &a, const Ptr &b,
1134  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1135  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b,
1136  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1137  static Ptr instance(Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1138  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1139  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1140  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1141  static Ptr instance(Operator op, const Nodes &arguments,
1142  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1143  static Ptr instance(const Type &type, Operator op, const Nodes &arguments,
1144  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1147  //--------------------------------------------------------
1148  // Overrides
1149  //--------------------------------------------------------
1150 public:
1151  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1152  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1153  virtual bool isEquivalentTo(const Ptr &other) override;
1154  virtual bool isEquivalentHelper(Node*, EquivPairs&) override;
1155  virtual int compareStructure(const Ptr& other) override;
1156  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1157  virtual VisitAction depthFirstTraversal(Visitor&) const override;
1158  virtual uint64_t nNodes() const override { return nnodes_; }
1159  virtual const Nodes& children() const override { return children_; }
1160  virtual Operator getOperator() const override { return op_; }
1161  virtual size_t nChildren() const override { return children_.size(); }
1162  virtual const Ptr& child(size_t idx) const override;
1163  virtual Node* childRaw(size_t idx) const override;
1164  virtual Sawyer::Optional<uint64_t> toUnsigned() const override { return Sawyer::Nothing(); }
1165  virtual Sawyer::Optional<int64_t> toSigned() const override { return Sawyer::Nothing(); }
1166  virtual bool isConstant() const override { return false; }
1167  virtual bool isVariable2() const override { return false; }
1168 
1169  //--------------------------------------------------------
1170  // Simplification
1171  //--------------------------------------------------------
1172 public:
1176  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
1177 
1180  Ptr foldConstants(const Simplifier&);
1181 
1186  InteriorPtr associative();
1187 
1192  InteriorPtr commutative();
1193 
1200  InteriorPtr idempotent(const SmtSolverPtr &solver = SmtSolverPtr());
1201 
1205  Ptr involutary();
1206 
1210  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
1211 
1215  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
1216 
1221  Ptr poisonNan(const SmtSolverPtr &solver = SmtSolverPtr());
1222 
1224  Ptr unaryNoOp();
1225 
1229  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
1230 
1231  //--------------------------------------------------------
1232  // Functions specific to internal nodes
1233  //--------------------------------------------------------
1234 public:
1235  virtual void print(std::ostream&, Formatter&) const override;
1236 
1237 protected:
1239  void addChild(const Ptr &child);
1240 
1244  void adjustWidth(const Type&);
1245 
1248  void adjustBitFlags(unsigned extraFlags);
1249 };
1250 
1251 
1253 // Leaf Nodes
1255 
1259 class Leaf: public Node {
1260 private:
1261  Sawyer::Container::BitVector bits_; // Value for constants if size > 0
1262  uint64_t name_; // Variable ID for variables when bits_.size() == 0
1263 
1264  //--------------------------------------------------------
1265  // Serialization
1266  //--------------------------------------------------------
1267 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1268 private:
1269  friend class boost::serialization::access;
1270 
1271  template<class S>
1272  void save(S &s, const unsigned /*version*/) const {
1273  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1274  s & BOOST_SERIALIZATION_NVP(bits_);
1275  s & BOOST_SERIALIZATION_NVP(name_);
1276  }
1277 
1278  template<class S>
1279  void load(S &s, const unsigned /*version*/) {
1280  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1281  s & BOOST_SERIALIZATION_NVP(bits_);
1282  s & BOOST_SERIALIZATION_NVP(name_);
1283  nextNameCounter(name_);
1284  }
1285 
1286  BOOST_SERIALIZATION_SPLIT_MEMBER();
1287 #endif
1288 
1289  //--------------------------------------------------------
1290  // Private constructors. Use create methods instead.
1291  //--------------------------------------------------------
1292 private:
1293  Leaf()
1294  : name_(0) {}
1295  explicit Leaf(const std::string &comment, unsigned flags=0)
1296  : Node(comment, flags), name_(0) {}
1297 
1298  // Allocating constructors.
1299 public:
1301  static LeafPtr createVariable(const Type&,
1302  const std::string &comment = "", unsigned flags = 0);
1303 
1305  static LeafPtr createVariable(const Type&, const uint64_t id,
1306  const std::string &comment = "", unsigned flags = 0);
1307 
1309  static LeafPtr createConstant(const Type&, const Sawyer::Container::BitVector&,
1310  const std::string &comment = "", unsigned flags = 0);
1311 
1312  //--------------------------------------------------------
1313  // Override base class implementations
1314  //--------------------------------------------------------
1315 public:
1316  virtual size_t nChildren() const override { return 0; }
1317  virtual const Ptr& child(size_t idx) const override;
1318  virtual const Node* childRaw(size_t idx) const override { return nullptr; }
1319  virtual const Nodes& children() const override;
1320  virtual Operator getOperator() const override { return OP_NONE; }
1321  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1322  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1323  virtual bool isEquivalentTo(const Ptr &other) override;
1324  virtual bool isEquivalentHelper(Node*, EquivPairs&) override;
1325  virtual int compareStructure(const Ptr& other) override;
1326  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1327  virtual VisitAction depthFirstTraversal(Visitor&) const override;
1328  virtual uint64_t nNodes() const override { return 1; }
1329  virtual Sawyer::Optional<uint64_t> toUnsigned() const override;
1330  virtual Sawyer::Optional<int64_t> toSigned() const override;
1331  virtual bool isConstant() const override { return !bits_.isEmpty(); }
1332  virtual bool isVariable2() const override { return !isConstant(); }
1333  virtual void print(std::ostream&, Formatter&) const override;
1334 
1335  //--------------------------------------------------------
1336  // Leaf-specific methods
1337  //--------------------------------------------------------
1338 public:
1340  const Sawyer::Container::BitVector& bits() const;
1341 
1343  bool isIntegerVariable() const {
1344  return type().typeClass() == Type::INTEGER && !isConstant();
1345  }
1346 
1349  return type().typeClass() == Type::FP && !isConstant();
1350  }
1351 
1353  bool isFloatingPointNan() const;
1354 
1356  bool isMemoryVariable() const {
1357  return type().typeClass() == Type::MEMORY && !isConstant();
1358  }
1359 
1364  uint64_t nameId() const;
1365 
1370  std::string toString() const;
1371 
1373  void printAsSigned(std::ostream&, Formatter&, bool asSigned = true) const;
1374 
1376  void printAsUnsigned(std::ostream &o, Formatter &f) const {
1377  printAsSigned(o, f, false);
1378  }
1379 
1380 private:
1381  // Obtain or register a name ID
1382  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1383 };
1384 
1386 // Factories
1388 
1394 LeafPtr makeVariable(const Type&, const std::string &comment="", unsigned flags=0);
1395 LeafPtr makeVariable(const Type&, uint64_t id, const std::string &comment="", unsigned flags=0);
1396 LeafPtr makeConstant(const Type&, const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1397 LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0);
1398 LeafPtr makeIntegerVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0);
1399 LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0);
1400 LeafPtr makeIntegerConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1401 LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0);
1402 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1403 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
1404 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1405 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, uint64_t id, const std::string &comment="", unsigned flags=0);
1406 LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0);
1407 LeafPtr makeFloatingPointConstant(double, const std::string &comment="", unsigned flags=0);
1408 LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1417 Ptr makeAdd(const Ptr&a, const Ptr &b,
1418  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1419 Ptr makeAsr(const Ptr &sa, const Ptr &a,
1420  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1421 Ptr makeAnd(const Ptr &a, const Ptr &b,
1422  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1423 Ptr makeOr(const Ptr &a, const Ptr &b,
1424  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1425 Ptr makeXor(const Ptr &a, const Ptr &b,
1426  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1427 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1428  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1429 Ptr makeConvert(const Ptr &a, const Type &b,
1430  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1431 Ptr makeEq(const Ptr &a, const Ptr &b,
1432  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1433 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1434  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1435 Ptr makeInvert(const Ptr &a,
1436  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1437 Ptr makeIsInfinite(const Ptr &a,
1438  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1439 Ptr makeIsNan(const Ptr &a,
1440  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1441 Ptr makeIsNeg(const Ptr &a,
1442  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1443 Ptr makeIsNorm(const Ptr &a,
1444  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1445 Ptr makeIsPos(const Ptr &a,
1446  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1447 Ptr makeIsSubnorm(const Ptr &a,
1448  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1449 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1450  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1451 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1452  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1453 Ptr makeLssb(const Ptr &a,
1454  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1455 Ptr makeMax(const Ptr &a, const Ptr &b,
1456  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1457 Ptr makeMin(const Ptr &a, const Ptr &b,
1458  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1459 Ptr makeMssb(const Ptr &a,
1460  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1461 Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c,
1462  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1463 Ptr makeNe(const Ptr &a, const Ptr &b,
1464  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1465 Ptr makeNegate(const Ptr &a,
1466  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1467 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1468  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1469 Ptr makeReinterpret(const Ptr &a, const Type &b,
1470  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1471 Ptr makeRol(const Ptr &sa, const Ptr &a,
1472  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1473 Ptr makeRor(const Ptr &sa, const Ptr &a,
1474  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1475 Ptr makeRound(const Ptr &a,
1476  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1477 Ptr makeSet(const Ptr &a, const Ptr &b,
1478  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1479 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1480  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1481 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1482  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1483 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1484  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1485 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1486  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1487 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1488  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1489 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1490  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1491 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1492  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1493 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1494  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1495 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1496  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1497 Ptr makeIsSignedPos(const Ptr &a,
1498  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1499 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1500  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1501 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1502  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1503 Ptr makeSignedMax(const Ptr &a, const Ptr &b,
1504  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1505 Ptr makeSignedMin(const Ptr &a, const Ptr &b,
1506  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1507 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1508  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1509 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1510  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1511 Ptr makeSqrt(const Ptr &a,
1512  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1513 Ptr makeDiv(const Ptr &a, const Ptr &b,
1514  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1515 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1516  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1517 Ptr makeGe(const Ptr &a, const Ptr &b,
1518  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1519 Ptr makeGt(const Ptr &a, const Ptr &b,
1520  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1521 Ptr makeLe(const Ptr &a, const Ptr &b,
1522  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1523 Ptr makeLt(const Ptr &a, const Ptr &b,
1524  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1525 Ptr makeMod(const Ptr &a, const Ptr &b,
1526  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1527 Ptr makeMul(const Ptr &a, const Ptr &b,
1528  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1529 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1530  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1531 Ptr makeZerop(const Ptr &a,
1532  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1536 // Miscellaneous functions
1539 
1540 
1541 std::ostream& operator<<(std::ostream &o, const Node&);
1542 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1543 
1545 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1546 
1551 Hash hash(const std::vector<Ptr>&);
1552 
1557 template<typename InputIterator>
1558 uint64_t
1559 nNodes(InputIterator begin, InputIterator end) {
1560  uint64_t total = 0;
1561  for (InputIterator ii=begin; ii!=end; ++ii) {
1562  uint64_t n = (*ii)->nnodes();
1563  if (MAX_NNODES==n)
1564  return MAX_NNODES;
1565  if (total + n < total)
1566  return MAX_NNODES;
1567  total += n;
1568  }
1569  return total;
1570 }
1571 
1576 template<typename InputIterator>
1577 uint64_t
1578 nNodesUnique(InputIterator begin, InputIterator end)
1579 {
1580  struct T1: Visitor {
1581  typedef std::set<const Node*> SeenNodes;
1582 
1583  SeenNodes seen; // nodes that we've already seen, and the subtree size
1584  uint64_t nUnique; // number of unique nodes
1585 
1586  T1(): nUnique(0) {}
1587 
1588  VisitAction preVisit(const Node *node) override {
1589  ASSERT_not_null(node);
1590  if (seen.insert(node).second) {
1591  ++nUnique;
1592  return CONTINUE; // this node has not been seen before; traverse into children
1593  } else {
1594  return TRUNCATE; // this node has been seen already; skip over the children
1595  }
1596  }
1597 
1598  VisitAction postVisit(const Node*) override {
1599  return CONTINUE;
1600  }
1601  } visitor;
1602 
1603  VisitAction status = CONTINUE;
1604  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1605  status = (*ii)->depthFirstTraversal(visitor);
1606  return visitor.nUnique;
1607 }
1608 
1615 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1616 
1617 template<typename InputIterator>
1618 std::vector<Ptr>
1619 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1621  struct T1: Visitor {
1622  NodeCounts nodeCounts;
1623  std::vector<Ptr> result;
1624 
1625  VisitAction preVisit(const Node *node) override {
1626  ASSERT_not_null(node);
1627  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1628  if (2 == ++nSeen)
1629  result.push_back(Ptr(const_cast<Node*>(node)));
1630  return nSeen>1 ? TRUNCATE : CONTINUE;
1631  }
1632 
1633  VisitAction postVisit(const Node*) override {
1634  return CONTINUE;
1635  }
1636  } visitor;
1637 
1638  for (InputIterator ii=begin; ii!=end; ++ii)
1639  (*ii)->depthFirstTraversal(visitor);
1640  return visitor.result;
1641 }
1651 template<class Substitution>
1652 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1653  if (!src)
1654  return Ptr(); // no input implies no output
1655 
1656  // Try substituting the whole expression, returning the result.
1657  Ptr dst = subber(src, solver);
1658  ASSERT_not_null(dst);
1659  if (dst != src)
1660  return dst;
1661 
1662  // Try substituting all the subexpressions.
1663  const Interior *inode = src->isInteriorNodeRaw();
1664  if (!inode)
1665  return src;
1666  bool anyChildChanged = false;
1667  Nodes newChildren;
1668  newChildren.reserve(inode->nChildren());
1669  for (const Ptr &child: inode->children()) {
1670  Ptr newChild = substitute(child, subber, solver);
1671  if (newChild != child)
1672  anyChildChanged = true;
1673  newChildren.push_back(newChild);
1674  }
1675  if (!anyChildChanged)
1676  return src;
1677 
1678  // Some subexpression changed, so build a new expression
1679  return Interior::instance(inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1680 }
1681 
1682 } // namespace
1683 
1684 using SymbolicExprPtr = SymbolicExpr::Ptr;
1685 
1686 } // namespace
1687 } // namespace
1688 
1689 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1690 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1691 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1692 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Type, 1);
1693 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Node, 1);
1694 #endif
1695 
1696 #endif
1697 #endif
Ptr renameVariables(ExprExprHashMap &index, size_t &nextVariableId, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite using lowest numbered variable names.
Operator-specific simplification methods.
Definition: SymbolicExpr.h:902
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
const std::string & comment() const
Property: Comment.
Definition: SymbolicExpr.h:717
bool add_renames
Add additional entries to the renames as variables are encountered?
Definition: SymbolicExpr.h:195
Sawyer::Optional< uint64_t > variableId() const
Variable ID number.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions might be equal, but not necessarily be equal.
bool isFloatingPointExpr() const
True if this expression is of a floating-point type.
Definition: SymbolicExpr.h:636
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
static LeafPtr createVariable(const Type &, const std::string &comment="", unsigned flags=0)
Create a new variable.
virtual const Node * childRaw(size_t idx) const =0
Argument.
bool isHashed() const
Returns true if this node has a hash value computed and cached.
Definition: SymbolicExpr.h:824
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Bitwise exclusive disjunction.
Definition: SymbolicExpr.h:124
ShowComments show_comments
Show node comments when printing?
Definition: SymbolicExpr.h:193
Ordered set of values.
Definition: Set.h:52
Ptr makeSignedLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual bool isConstant() const override
True if this expression is a constant.
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
Definition: SymbolicExpr.h:166
std::string comment_
Optional comment.
Definition: SymbolicExpr.h:485
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
RenameMap renames
Map for renaming variables to use smaller integers.
Definition: SymbolicExpr.h:199
virtual Sawyer::Optional< uint64_t > toUnsigned() const override
The unsigned integer value of the expression.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions must be equal (cannot be unequal).
size_t max_depth
If non-zero, then replace deep parts of expressions with "...".
Definition: SymbolicExpr.h:197
bool matchAddVariableConstant(LeafPtr &variable, LeafPtr &constant) const
Determine whether an expression is a variable plus a constant.
static Type floatingPoint(size_t exponentWidth, size_t significandWidth)
Create a new floating-point type.
Definition: SymbolicExpr.h:332
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr())=0
Returns true if two expressions must be equal (cannot be unequal).
uint64_t Hash
Hash of symbolic expression.
Definition: SymbolicExpr.h:181
Leaf node of an expression tree for instruction semantics.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr())=0
Substitute one value for another.
size_t nBits() const
Property: Total width of values.
Definition: SymbolicExpr.h:354
virtual bool isEquivalentTo(const Ptr &other)=0
Tests two expressions for structural equivalence.
Ptr makeReinterpret(const Ptr &a, const Type &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Continue the traversal as normal.
Definition: SymbolicExpr.h:206
Interior node of an expression tree for instruction semantics.
virtual Sawyer::Optional< uint64_t > toUnsigned() const =0
The unsigned integer value of the expression.
Ptr makeIsInfinite(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
boost::any userData_
Additional user-specified data.
Definition: SymbolicExpr.h:487
bool isFloatingPointVariable() const
Is this node a floating-point variable?
Hash hashval_
Optional hash used as a quick way to indicate that two expressions are different. ...
Definition: SymbolicExpr.h:486
virtual const Ptr & child(size_t idx) const override
Argument.
Ptr makeRead(const Ptr &mem, const Ptr &addr, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
Ptr makeXor(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
uint64_t nNodesUnique(InputIterator begin, InputIterator end)
Counts the number of unique nodes.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeSignedMod(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual void print(std::ostream &, Formatter &) const =0
Print the expression to a stream.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Floating-point round to integer as FP type.
Definition: SymbolicExpr.h:135
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Leaf * isLeafNodeRaw() const
Dynamic cast of this object to a leaf node.
Ptr makeSignedMin(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual bool isConstant() const =0
True if this expression is a constant.
Mapping from expression to expression.
Definition: SymbolicExpr.h:939
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
uint64_t nameId() const
Returns the name ID of a free variable.
virtual size_t nChildren() const =0
Number of arguments.
virtual Node * childRaw(size_t idx) const override
Argument.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const
Rewrite the entire expression to something simpler.
Definition: SymbolicExpr.h:915
Shift left, introducing zeros at lsb.
Definition: SymbolicExpr.h:107
LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool isFloatingPointConstant() const
True if this epxression is a floating-point constant.
Definition: SymbolicExpr.h:661
unsigned flags() const
Property: User-defined bit flags.
Definition: SymbolicExpr.h:751
Ptr makeDiv(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
const boost::any & userData() const
Property: User-defined data.
Definition: SymbolicExpr.h:735
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
Ptr makeMin(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
static Ptr instance(Operator op, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Create a new expression node.
virtual size_t nChildren() const override
Number of arguments.
virtual VisitAction depthFirstTraversal(Visitor &) const override
Traverse the expression.
VisitAction
Return type for visitors.
Definition: SymbolicExpr.h:205
void userData(boost::any &data)
Property: User-defined data.
Definition: SymbolicExpr.h:732
InteriorPtr isOperator(Operator) const
True (non-null) if this node is the specified operator.
void printAsUnsigned(std::ostream &o, Formatter &f) const
Prints an integer constant interpreted as an unsigned value.
bool do_rename
Use the renames map to rename variables to shorter names?
Definition: SymbolicExpr.h:194
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool isScalar() const
Check whether expression is scalar.
Definition: SymbolicExpr.h:770
std::string toString() const
Convert expression to string.
Ptr makeLt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Most significant set bit or zero.
Definition: SymbolicExpr.h:94
bool isScalarVariable() const
True if this expression is a scalar variable.
Definition: SymbolicExpr.h:705
Ptr makeGt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver=SmtSolverPtr())
On-the-fly substitutions.
bool isIntegerVariable() const
Is this node an integer variable?
Sawyer::Container::Set< Ptr, ExpressionLessp > ExpressionSet
Set of expressions ordered by hash.
Definition: SymbolicExpr.h:946
static const unsigned UNSPECIFIED
Value is somehow unspecified.
Definition: SymbolicExpr.h:518
Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Operator getOperator() const =0
Operator for interior nodes.
Small object support.
Definition: SmallObject.h:19
virtual bool isConstant() const override
True if this expression is a constant.
Shift right, introducing ones at msb.
Definition: SymbolicExpr.h:110
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual const Nodes & children() const override
Arguments.
Type of symbolic expression.
Definition: SymbolicExpr.h:244
virtual Sawyer::Optional< int64_t > toSigned() const override
The signed integer value of the expression.
Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
virtual int compareStructure(const Ptr &other) override
Compare two expressions structurally for sorting.
Ptr involutary()
Simplifies involutary operators.
virtual void print(std::ostream &, Formatter &) const override
Print the expression to a stream.
Ptr setToIte(const Ptr &, const SmtSolverPtr &solver=SmtSolverPtr(), const LeafPtr &var=LeafPtr())
Convert a set to an ite expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool isIntegerConstant() const
True if this expression is an integer constant.
Definition: SymbolicExpr.h:656
bool isScalarExpr() const
True if the expression is a scalar type.
Definition: SymbolicExpr.h:648
Main namespace for the ROSE library.
Floating-point greater-than or equal.
Definition: SymbolicExpr.h:140
Controls formatting of expression trees when printing.
Definition: SymbolicExpr.h:184
Interpret the value as a different type without converting.
Definition: SymbolicExpr.h:152
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool isVariable2() const =0
True if this expression is a variable.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Sawyer::Optional< int64_t > toSigned() const override
The signed integer value of the expression.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
Ptr makeShr1(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Shift right, introducing zeros at msb.
Definition: SymbolicExpr.h:109
virtual bool isEquivalentTo(const Ptr &other) override
Tests two expressions for structural equivalence.
virtual size_t nChildren() const override
Number of arguments.
void adjustBitFlags(unsigned extraFlags)
Adjust user-defined bit flags.
Ptr makeIsNeg(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
Ptr makeExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual const Nodes & children() const =0
Arguments.
Ptr makeSignedMax(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Least significant set bit or zero.
Definition: SymbolicExpr.h:93
bool operator!=(const Type &other) const
Type equality.
Definition: SymbolicExpr.h:395
Ptr poisonNan(const SmtSolverPtr &solver=SmtSolverPtr())
Returns NaN if any argument is NaN.
Ptr makeShl0(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeSignedGt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
static LeafPtr createConstant(const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0)
Create a constant.
Flag
Flag to pass as type stringification style.
Definition: SymbolicExpr.h:65
bool isMemoryExpr() const
True if this expression is of a memory type.
Definition: SymbolicExpr.h:641
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Shift left, introducing ones at lsb.
Definition: SymbolicExpr.h:108
Unsigned greater-than-or-equal.
Definition: SymbolicExpr.h:117
InteriorPtr isInteriorNode() const
Dynamic cast of this object to an interior node.
uint64_t nNodesUnique() const
Number of unique nodes in expression.
SharedPointer< Node > sharedFromThis()
Create a shared pointer from this.
TypeClass typeClass() const
Property: Type class.
Definition: SymbolicExpr.h:346
Ptr makeOr(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual VisitAction depthFirstTraversal(Visitor &) const override
Traverse the expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Like CMT_AFTER, but show comments instead of variable names.
Definition: SymbolicExpr.h:188
Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr additiveNesting(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies nested shift-like operators.
InteriorPtr associative()
Simplifies non-associative operators by flattening the specified interior node with its children that...
bool serializeVariableIds
Whether to serialize variable IDs.
static Type none()
Create no type.
Definition: SymbolicExpr.h:304
Ptr makeInvert(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeShr0(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual uint64_t nNodes() const =0
Computes the size of an expression by counting the number of nodes.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool isFloatingPointNan() const
True if this expression is a floating-point NaN constant.
static const unsigned INDETERMINATE
Value is somehow indeterminate.
Definition: SymbolicExpr.h:512
Ptr makeRor(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
Definition: SymbolicExpr.h:522
virtual bool isVariable2() const override
True if this expression is a variable.
Ptr makeConcat(const Ptr &hi, const Ptr &lo, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeConvert(const Ptr &a, const Type &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr())=0
Returns true if two expressions might be equal, but not necessarily be equal.
virtual VisitAction depthFirstTraversal(Visitor &) const =0
Traverse the expression.
Convert from one type to another.
Definition: SymbolicExpr.h:151
LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr identity(uint64_t ident, const SmtSolverPtr &solver=SmtSolverPtr())
Removes identity arguments.
Ptr newFlags(unsigned flags) const
Sets flags.
static boost::logic::tribool(* mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr &)
User-supplied predicate to augment alias checking.
Definition: SymbolicExpr.h:542
Ptr simplifyTop(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies the specified interior node.
Ptr makeSqrt(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeLssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isMemoryVariable() const
Is this node a memory variable?
Creates SharedPointer from this.
Ptr makeEq(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeRol(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
std::string toString(TypeStyle::Flag style=TypeStyle::FULL) const
Print the type to a string.
Ptr makeIsSubnorm(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual const Node * childRaw(size_t idx) const override
Argument.
void print(std::ostream &, TypeStyle::Flag style=TypeStyle::FULL) const
Print the type.
Ptr makeSignedDiv(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeShl1(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
uint64_t nNodes(InputIterator begin, InputIterator end)
Counts the number of nodes.
bool isScalarConstant() const
True if this expression is a scalar constant.
Definition: SymbolicExpr.h:668
virtual int compareStructure(const Ptr &other)=0
Compare two expressions structurally for sorting.
Ptr makeMul(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions might be equal, but not necessarily be equal.
Signed greater-than-or-equal.
Definition: SymbolicExpr.h:105
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeNe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Sawyer::Optional< int64_t > toSigned() const =0
The signed integer value of the expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeIsSignedPos(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t exponentWidth() const
Property: Exponent width.
Definition: SymbolicExpr.h:371
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) override
Substitute one value for another.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeNegate(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual int compareStructure(const Ptr &other) override
Compare two expressions structurally for sorting.
Ptr makeIsNan(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
InteriorPtr commutative()
Simplifies commutative operators by sorting arguments.
Ptr makeSignExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
void comment(const std::string &s)
Property: Comment.
Definition: SymbolicExpr.h:720
static const unsigned RESERVED_FLAGS
These flags are reserved for use within ROSE.
Definition: SymbolicExpr.h:509
Floating-point less-than or equal.
Definition: SymbolicExpr.h:138
void assertAcyclic() const
Asserts that expressions are acyclic.
Type()
Create an invalid, empty type.
Definition: SymbolicExpr.h:285
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
Sawyer::SharedPointer< Leaf > LeafPtr
Shared-ownership pointer to an expression Leaf node.
Definition: SymbolicExpr.h:175
Base class for reference counted objects.
Definition: SharedObject.h:64
bool isIntegerVariable() const
True if this expression is an integer variable.
Definition: SymbolicExpr.h:688
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeAnd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeIsPos(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Sawyer::SharedPointer< Interior > InteriorPtr
Shared-ownership pointer to an expression Interior node.
Definition: SymbolicExpr.h:172
std::set< LeafPtr > getVariables() const
Returns the variables appearing in the expression.
virtual Sawyer::Optional< uint64_t > toUnsigned() const override
The unsigned integer value of the expression.
Ptr makeMax(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool isMemoryVariable() const
True if this expression is a memory state variable.
Definition: SymbolicExpr.h:698
void printAsSigned(std::ostream &, Formatter &, bool asSigned=true) const
Prints an integer constant interpreted as a signed value.
static Type integer(size_t nBits)
Create a new integer type.
Definition: SymbolicExpr.h:313
Exceptions for symbolic expressions.
Definition: SymbolicExpr.h:73
bool use_hexadecimal
Show values in hexadecimal and decimal rather than just decimal.
Definition: SymbolicExpr.h:196
Ptr makeSignedLt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0)
Leaf constructor.
bool isValid() const
Check whether this object is valid.
Definition: SymbolicExpr.h:339
bool operator<(const Type &other) const
Type comparison.
bool isFloatingPointVariable() const
True if this expression is a floating-point variable.
Definition: SymbolicExpr.h:693
Base class for symbolic expression nodes.
Definition: SymbolicExpr.h:477
LeafPtr makeConstant(const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite expression by substituting subexpressions.
Ptr makeSet(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
void adjustWidth(const Type &)
Adjust width based on operands.
void print(std::ostream &o) const
Print the expression to a stream.
Definition: SymbolicExpr.h:867
Operator
Operators for interior nodes of the expression tree.
Definition: SymbolicExpr.h:83
Ptr makeMssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Floating-point absolute value.
Definition: SymbolicExpr.h:127
size_t addressWidth() const
Property: Width of memory addresses.
Definition: SymbolicExpr.h:362
bool isFloatingPointNan() const
Is this node a floating-point NaN constant?
bool isEmpty() const
Determines if the vector is empty.
Definition: BitVector.h:184
virtual uint64_t nNodes() const override
Computes the size of an expression by counting the number of nodes.
bool operator==(const Type &other) const
Type equality.
Definition: SymbolicExpr.h:392
Ptr unaryNoOp()
Replaces a binary operator with its only argument.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool show_flags
Show user-defined flags inside square brackets.
Definition: SymbolicExpr.h:201
API and storage for attributes.
Definition: Attribute.h:208
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
size_t significandWidth() const
Property: Significand width.
Definition: SymbolicExpr.h:381
Compare two expressions for STL containers.
Definition: SymbolicExpr.h:933
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions must be equal (cannot be unequal).
void addChild(const Ptr &child)
Appends child as a new child of this node.
const uint64_t MAX_NNODES
Maximum number of nodes that can be reported.
virtual const Nodes & children() const override
Arguments.
WithFormatter withFormat(Formatter &fmt)
Combines a node with a formatter for printing.
Definition: SymbolicExpr.h:858
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
WithFormatter operator+(Formatter &fmt)
Combines a node with a formatter for printing.
Definition: SymbolicExpr.h:859
Represents no value.
Definition: Optional.h:32
bool show_type
Show data type inside square brackets.
Definition: SymbolicExpr.h:200
Type type() const
Type of value.
Definition: SymbolicExpr.h:532
Hash hash() const
Returns (and caches) the hash value for this node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Interior * isInteriorNodeRaw() const
Dynamic cast of this object to an interior node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Base class for visiting nodes during expression traversal.
Definition: SymbolicExpr.h:228
Ptr makeGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t domainWidth() const
Property: Width for memory expressions.
Definition: SymbolicExpr.h:763
Base class for all ROSE exceptions.
Definition: Rose/Exception.h:9
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Write (update) memory with a new value.
Definition: SymbolicExpr.h:123
virtual Operator getOperator() const override
Operator for interior nodes.
Ptr makeSignedGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Unsigned less-than-or-equal.
Definition: SymbolicExpr.h:119
std::vector< Ptr > findCommonSubexpressions(const std::vector< Ptr > &)
Find common subexpressions.
virtual const Ptr & child(size_t idx) const =0
Argument.
bool isIntegerExpr() const
True if this expression is of an integer type.
Definition: SymbolicExpr.h:631
static Type memory(size_t addressWidth, size_t valueWidth)
Create a new memory type.
Definition: SymbolicExpr.h:320
virtual void print(std::ostream &, Formatter &) const override
Print the expression to a stream.
std::vector< Ptr > findCommonSubexpressions() const
Find common subexpressions.
virtual Operator getOperator() const override
Operator for interior nodes.
LeafPtr isLeafNode() const
Dynamic cast of this object to a leaf node.
Ptr makeAdd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeMod(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Container associating values with keys.
Definition: Sawyer/Map.h:66
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr foldConstants(const Simplifier &)
Perform constant folding.
virtual bool isVariable2() const override
True if this expression is a variable.
size_t nBits() const
Property: Number of significant bits.
Definition: SymbolicExpr.h:743
Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver=SmtSolverPtr())
Simplify an interior node.
virtual uint64_t nNodes() const override
Computes the size of an expression by counting the number of nodes.
InteriorPtr idempotent(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies idempotent operators.
Ptr makeSignedMul(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual const Ptr & child(size_t idx) const override
Argument.
Ptr makeRound(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeAsr(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:26
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) override
Substitute one value for another.
Ptr makeIsNorm(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeZerop(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual bool isEquivalentTo(const Ptr &other) override
Tests two expressions for structural equivalence.
std::string toString() const
Returns a string for the leaf.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const
Constant folding.
Definition: SymbolicExpr.h:909
const Sawyer::Container::BitVector & bits() const
Property: Bits stored for numeric constants.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.
LeafPtr makeVariable(const Type &, const std::string &comment="", unsigned flags=0)
Leaf constructor.
For a pre-order depth-first visit, do not descend into children.
Definition: SymbolicExpr.h:207