ROSE  0.9.11.158
BinarySymbolicExpr.h
1 #ifndef ROSE_BinaryAnalysis_SymbolicExpr_H
2 #define ROSE_BinaryAnalysis_SymbolicExpr_H
3 
4 #ifndef __STDC_FORMAT_MACROS
5 #define __STDC_FORMAT_MACROS
6 #endif
7 
8 #include "Map.h"
9 
10 #include <boost/any.hpp>
11 #include <boost/lexical_cast.hpp>
12 #include <boost/logic/tribool.hpp>
13 #include <boost/serialization/access.hpp>
14 #include <boost/serialization/base_object.hpp>
15 #include <boost/serialization/export.hpp>
16 #include <boost/serialization/split_member.hpp>
17 #include <boost/serialization/string.hpp>
18 #include <boost/serialization/vector.hpp>
19 #include <boost/unordered_map.hpp>
20 #include <cassert>
21 #include <inttypes.h>
22 #include <RoseException.h>
23 #include <Sawyer/Attribute.h>
24 #include <Sawyer/BitVector.h>
25 #include <Sawyer/Optional.h>
26 #include <Sawyer/Set.h>
27 #include <Sawyer/SharedPointer.h>
28 #include <Sawyer/SmallObject.h>
29 #include <set>
30 #include <string>
31 #include <vector>
32 
33 namespace Rose {
34 namespace BinaryAnalysis {
35 
36 class SmtSolver;
38 
44 namespace SymbolicExpr {
45 
47 // Basic Types
49 
51 class Exception: public Rose::Exception {
52 public:
53  explicit Exception(const std::string &mesg): Rose::Exception(mesg) {}
54 };
55 
61 enum Operator {
133  OP_BV_AND = OP_AND, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
134  OP_BV_OR = OP_OR, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
135  OP_BV_XOR = OP_XOR // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
136 };
137 
138 std::string toStr(Operator);
139 
140 class Node;
141 class Interior;
142 class Leaf;
144 
147 
150 
153 
154 typedef std::vector<Ptr> Nodes;
156 
158 typedef uint64_t Hash;
159 
161 struct Formatter {
166  };
167  Formatter()
169  max_depth(0), cur_depth(0), show_width(true), show_flags(true) {}
171  bool do_rename;
172  bool add_renames;
174  size_t max_depth;
175  size_t cur_depth;
176  RenameMap renames;
177  bool show_width;
178  bool show_flags;
179 };
180 
186 };
187 
192 extern const uint64_t MAX_NNODES; // defined in .C so we don't pollute user namespace with limit macros
193 
198 class Visitor {
199 public:
200  virtual ~Visitor() {}
201  virtual VisitAction preVisit(const Ptr&) = 0;
202  virtual VisitAction postVisit(const Ptr&) = 0;
203 };
204 
205 
206 
208 // Expression type information
210 
212 class Type {
213 public:
215  enum TypeClass {
217  FP,
220  };
221 
222 private:
223  TypeClass typeClass_;
224  size_t totalWidth_;
225  size_t secondaryWidth_;
226 
227 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
228 private:
229  friend class boost::serialization::access;
230 
231  template<class S>
232  void serialize(S &s, const unsigned /*version*/) {
233  s & BOOST_SERIALIZATION_NVP(typeClass_);
234  s & BOOST_SERIALIZATION_NVP(totalWidth_);
235  s & BOOST_SERIALIZATION_NVP(secondaryWidth_);
236  }
237 #endif
238 
242 public:
244  : typeClass_(INVALID), totalWidth_(0), secondaryWidth_(0) {}
245 
246 private:
247  Type(TypeClass tc, size_t w1, size_t w2)
248  : typeClass_(tc), totalWidth_(w1), secondaryWidth_(w2) {}
249 
250 public:
254  static Type none() {
255  return Type();
256  }
257 
263  static Type integer(size_t nBits) {
264  return Type(INTEGER, nBits, 0);
265  }
266 
270  static Type memory(size_t addressWidth, size_t valueWidth) {
271  return Type(MEMORY, valueWidth, addressWidth);
272  }
273 
281  return Type(FP, exponentWidth + significandWidth, exponentWidth);
282  }
283 
287  bool isValid() const {
288  return typeClass_ != INVALID;
289  }
290 
295  return typeClass_;
296  }
297 
302  size_t nBits() const {
303  return totalWidth_;
304  }
305 
310  size_t addressWidth() const {
311  ASSERT_require(MEMORY == typeClass_);
312  return secondaryWidth_;
313  }
314 
319  size_t exponentWidth() const {
320  ASSERT_require(FP == typeClass_);
321  return secondaryWidth_;
322  }
323 
329  size_t significandWidth() const {
330  ASSERT_require(FP == typeClass_);
331  return totalWidth_ - exponentWidth();
332  }
333 
339  bool operator==(const Type &other) const {
340  return typeClass_ == other.typeClass_ && totalWidth_ == other.totalWidth_ && secondaryWidth_ == other.secondaryWidth_;
341  }
342  bool operator!=(const Type &other) const {
343  return !(*this == other);
344  }
348  bool operator<(const Type &other) const;
349 };
350 
351 
352 
353 
354 
356 // Base Node Type
358 
396 class Node
397  : public Sawyer::SharedObject,
398  public Sawyer::SharedFromThis<Node>,
399  public Sawyer::SmallObject,
400  public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
401 protected:
402  Type type_;
403  unsigned flags_;
404  std::string comment_;
405  Hash hashval_;
406  boost::any userData_;
408 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
409 private:
410  friend class boost::serialization::access;
411 
412  template<class S>
413  void serialize(S &s, const unsigned version) {
414  if (version < 1)
415  ASSERT_not_reachable("SymbolicExpr version " + boost::lexical_cast<std::string>(version) + " is no longer supported");
416  s & BOOST_SERIALIZATION_NVP(type_);
417  s & BOOST_SERIALIZATION_NVP(flags_);
418  s & BOOST_SERIALIZATION_NVP(comment_);
419  s & BOOST_SERIALIZATION_NVP(hashval_);
420  // s & userData_;
421  }
422 #endif
423 
424 public:
425  // Bit flags
426 
428  static const unsigned RESERVED_FLAGS = 0x0000ffff;
429 
431  static const unsigned INDETERMINATE = 0x00000001;
432 
437  static const unsigned UNSPECIFIED = 0x00000002;
438 
441  static const unsigned BOTTOM = 0x00000004;
442 
443 protected:
444  Node()
445  : type_(Type::integer(0)), flags_(0), hashval_(0) {}
446  explicit Node(const std::string &comment, unsigned flags=0)
447  : type_(Type::integer(0)), flags_(flags), comment_(comment), hashval_(0) {}
448 
449 public:
451  Type type() const {
452  return type_;
453  }
454 
461  static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
462 
468  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
469 
471  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
472 
478  virtual bool isEquivalentTo(const Ptr &other) = 0;
479 
485  virtual int compareStructure(const Ptr &other) = 0;
486 
492  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
493 
501  Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
502 
510  Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
511  const SmtSolverPtr &solver = SmtSolverPtr());
512 
516  virtual Operator getOperator() const = 0;
517 
521  virtual size_t nChildren() const = 0;
522 
527  virtual Ptr child(size_t idx) const = 0;
528 
532  virtual const Nodes& children() const = 0;
533 
538  virtual Sawyer::Optional<uint64_t> toUnsigned() const = 0;
539 
543  virtual Sawyer::Optional<int64_t> toSigned() const = 0;
544 
546  bool isIntegerExpr() const {
547  return type_.typeClass() == Type::INTEGER;
548  }
549 
551  bool isFloatingPointExpr() const {
552  return type_.typeClass() == Type::FP;
553  }
554 
556  bool isMemoryExpr() const {
557  return type_.typeClass() == Type::MEMORY;
558  }
559 
561  virtual bool isConstant() const = 0;
562 
564  bool isIntegerConstant() const {
565  return isIntegerExpr() && isConstant();
566  }
567 
569  bool isFloatingPointConstant() const {
570  return isFloatingPointExpr() && isConstant();
571  }
572 
574  bool isFloatingPointNan() const;
575 
581  virtual bool isVariable2() const = 0;
582 
584  bool isIntegerVariable() const {
585  return isIntegerExpr() && isVariable2();
586  }
587 
589  bool isFloatingPointVariable() const {
590  return isFloatingPointExpr() && isVariable2();
591  }
592 
594  bool isMemoryVariable() const {
595  return isMemoryExpr() && isVariable2();
596  }
597 
606  const std::string& comment() const {
607  return comment_;
608  }
609  void comment(const std::string &s) {
610  comment_ = s;
611  }
621  void userData(boost::any &data) {
622  userData_ = data;
623  }
624  const boost::any& userData() const {
625  return userData_;
626  }
632  size_t nBits() const {
633  return type_.nBits();
634  }
635 
640  unsigned flags() const {
641  return flags_;
642  }
643 
647  Ptr newFlags(unsigned flags) const;
648 
652  size_t domainWidth() const {
653  return type_.addressWidth();
654  }
655 
659  bool isScalar() const {
660  return type_.typeClass() != Type::MEMORY;
661  }
662 
667  virtual VisitAction depthFirstTraversal(Visitor&) const = 0;
668 
684  virtual uint64_t nNodes() const = 0;
685 
687  uint64_t nNodesUnique() const;
688 
690  std::set<LeafPtr> getVariables() const;
691 
695  InteriorPtr isInteriorNode() const;
696 
700  LeafPtr isLeafNode() const;
701 
705  bool isHashed() const {
706  return hashval_ != 0;
707  }
708 
711  Hash hash() const;
712 
713  // used internally to set the hash value
714  void hash(Hash);
715 
718  private:
719  Ptr node;
720  Formatter &formatter;
721  public:
722  WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
723  void print(std::ostream &stream) const { node->print(stream, formatter); }
724  };
725 
747  virtual void print(std::ostream&, Formatter&) const = 0;
748  void print(std::ostream &o) const { Formatter fmt; print(o, fmt); }
752  void assertAcyclic() const;
753 
759  std::vector<Ptr> findCommonSubexpressions() const;
760 
766  bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/) const;
767 
769  InteriorPtr isOperator(Operator) const;
770 
771 protected:
772  void printFlags(std::ostream &o, unsigned flags, char &bracket) const;
773 
774 public:
775  // Deprecated [Robb Matzke 2019-09-27]
776  bool isNumber() const ROSE_DEPRECATED("use isIntegerConstant instead") {
777  return isIntegerConstant();
778  }
779 
780  // Deprecated [Robb Matzke 2019-09-27]
781  uint64_t toInt() ROSE_DEPRECATED("use toUnsigned() instead") {
782  return toUnsigned().get();
783  }
784 };
785 
787 class Simplifier {
788 public:
789  virtual ~Simplifier() {}
790 
794  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
795  return Ptr();
796  }
797 
800  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
801  return Ptr();
802  }
803 };
804 
806  size_t operator()(const Ptr &expr) const {
807  return expr->hash();
808  }
809 };
810 
812  bool operator()(const Ptr &a, const Ptr &b) const {
813  return a->isEquivalentTo(b);
814  }
815 };
816 
819 public:
820  bool operator()(const Ptr &a, const Ptr &b);
821 };
822 
824 class ExprExprHashMap: public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
825  ExprExprHashMapHasher, ExprExprHashMapCompare> {
826 public:
827  ExprExprHashMap invert() const;
828 };
829 
832 
833 
835 // Simplification
837 
839  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
840  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
841 };
843  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
844  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
845 };
847  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
848  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
849 };
851  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
852  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
853 };
855  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
856 };
858  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
859 };
861  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
862  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
863 };
865  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
866 };
868  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
869 };
871  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
872 };
874  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
875 };
877  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
878 };
880  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
881 };
883  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
884 };
886  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
887 };
889  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
890 };
892  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
893 };
895  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
896 };
898  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
899 };
901  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
902 };
904  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
905 };
907  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
908 };
910  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
911 };
913  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
914 };
916  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
917 };
919  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
920 };
922  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
923 };
925  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
926 };
928  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
929 };
931  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
932 };
934  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
935 };
937  bool newbits;
938  ShiftSimplifier(bool newbits): newbits(newbits) {}
939  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
940 };
942  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
943  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
944 };
946  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
947  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
948 };
950  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
951 };
953  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
954 };
956  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
957 };
958 
959 
960 
962 // Interior Nodes
964 
971 class Interior: public Node {
972 private:
973  Operator op_;
974  Nodes children_;
975  uint64_t nnodes_; // total number of nodes; self + children's nnodes
976 
977  //--------------------------------------------------------
978  // Serialization
979  //--------------------------------------------------------
980 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
981 private:
982  friend class boost::serialization::access;
983 
984  template<class S>
985  void serialize(S &s, const unsigned /*version*/) {
986  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
987  s & BOOST_SERIALIZATION_NVP(op_);
988  s & BOOST_SERIALIZATION_NVP(children_);
989  s & BOOST_SERIALIZATION_NVP(nnodes_);
990  }
991 #endif
992 
993  //--------------------------------------------------------
994  // Real constructors
995  //--------------------------------------------------------
996 private:
997  Interior(); // needed for serialization
998  // Only constructs, does not simplify.
999  Interior(const Type&, Operator, const Nodes &arguments, const std::string &comment, unsigned flags);
1000 
1001  //--------------------------------------------------------
1002  // Allocating constructors
1003  //--------------------------------------------------------
1004 public:
1008  static Ptr instance(Operator op, const Ptr &a,
1009  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1010  static Ptr instance(const Type &type, Operator op, const Ptr &a,
1011  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1012  static Ptr instance(Operator op, const Ptr &a, const Ptr &b,
1013  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1014  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b,
1015  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1016  static Ptr instance(Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1017  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1018  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1019  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1020  static Ptr instance(Operator op, const Nodes &arguments,
1021  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1022  static Ptr instance(const Type &type, Operator op, const Nodes &arguments,
1023  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1026  //--------------------------------------------------------
1027  // Overrides
1028  //--------------------------------------------------------
1029 public:
1030  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1031  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1032  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1033  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1034  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1035  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1036  virtual uint64_t nNodes() const ROSE_OVERRIDE { return nnodes_; }
1037  virtual const Nodes& children() const ROSE_OVERRIDE { return children_; }
1038  virtual Operator getOperator() const ROSE_OVERRIDE { return op_; }
1039  virtual size_t nChildren() const ROSE_OVERRIDE { return children_.size(); }
1040  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return idx < children_.size() ? children_[idx] : Ptr(); }
1041  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1042  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1043  virtual bool isConstant() const ROSE_OVERRIDE { return false; }
1044  virtual bool isVariable2() const ROSE_OVERRIDE { return false; }
1045 
1046  //--------------------------------------------------------
1047  // Simplification
1048  //--------------------------------------------------------
1049 public:
1053  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
1054 
1057  Ptr foldConstants(const Simplifier&);
1058 
1063  InteriorPtr associative();
1064 
1069  InteriorPtr commutative();
1070 
1077  InteriorPtr idempotent(const SmtSolverPtr &solver = SmtSolverPtr());
1078 
1082  Ptr involutary();
1083 
1087  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
1088 
1092  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
1093 
1098  Ptr poisonNan(const SmtSolverPtr &solver = SmtSolverPtr());
1099 
1101  Ptr unaryNoOp();
1102 
1106  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
1107 
1108  //--------------------------------------------------------
1109  // Functions specific to internal nodes
1110  //--------------------------------------------------------
1111 public:
1112  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1113 
1114 protected:
1116  void addChild(const Ptr &child);
1117 
1119  void adjustWidth();
1120 
1123  void adjustBitFlags(unsigned extraFlags);
1124 
1125  //--------------------------------------------------------
1126  // Deprecated [Robb Matzke 2019-10-01]
1127  //--------------------------------------------------------
1128 public:
1129  static Ptr create(size_t nbits, Operator op, const Ptr &a,
1130  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1131  ROSE_DEPRECATED("use instance instead");
1132  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b,
1133  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1134  ROSE_DEPRECATED("use instance instead");
1135  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1136  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1137  ROSE_DEPRECATED("use instance instead");
1138  static Ptr create(size_t nbits, Operator op, const Nodes &children,
1139  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1140  ROSE_DEPRECATED("use instance instead");
1141 
1142 };
1143 
1144 
1146 // Leaf Nodes
1148 
1152 class Leaf: public Node {
1153 private:
1154  Sawyer::Container::BitVector bits_; // Value for constants if size > 0
1155  uint64_t name_; // Variable ID for variables when bits_.size() == 0
1156 
1157  //--------------------------------------------------------
1158  // Serialization
1159  //--------------------------------------------------------
1160 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1161 private:
1162  friend class boost::serialization::access;
1163 
1164  template<class S>
1165  void save(S &s, const unsigned /*version*/) const {
1166  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1167  s & BOOST_SERIALIZATION_NVP(bits_);
1168  s & BOOST_SERIALIZATION_NVP(name_);
1169  }
1170 
1171  template<class S>
1172  void load(S &s, const unsigned /*version*/) {
1173  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1174  s & BOOST_SERIALIZATION_NVP(bits_);
1175  s & BOOST_SERIALIZATION_NVP(name_);
1176  nextNameCounter(name_);
1177  }
1178 
1179  BOOST_SERIALIZATION_SPLIT_MEMBER();
1180 #endif
1181 
1182  //--------------------------------------------------------
1183  // Private constructors. Use create methods instead.
1184  //--------------------------------------------------------
1185 private:
1186  Leaf()
1187  : name_(0) {}
1188  explicit Leaf(const std::string &comment, unsigned flags=0)
1189  : Node(comment, flags), name_(0) {}
1190 
1191  // Allocating constructors.
1192 public:
1194  static LeafPtr createVariable(const Type&,
1195  const std::string &comment = "", unsigned flags = 0);
1196 
1198  static LeafPtr createVariable(const Type&, const uint64_t id,
1199  const std::string &comment = "", unsigned flags = 0);
1200 
1202  static LeafPtr createConstant(const Type&, const Sawyer::Container::BitVector&,
1203  const std::string &comment = "", unsigned flags = 0);
1204 
1205  //--------------------------------------------------------
1206  // Override base class implementations
1207  //--------------------------------------------------------
1208 public:
1209  virtual size_t nChildren() const ROSE_OVERRIDE { return 0; }
1210  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return Ptr(); }
1211  virtual const Nodes& children() const ROSE_OVERRIDE;
1212  virtual Operator getOperator() const ROSE_OVERRIDE { return OP_NONE; }
1213  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1214  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1215  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1216  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1217  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1218  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1219  virtual uint64_t nNodes() const ROSE_OVERRIDE { return 1; }
1220  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE;
1221  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE;
1222  virtual bool isConstant() const ROSE_OVERRIDE { return !bits_.isEmpty(); }
1223  virtual bool isVariable2() const ROSE_OVERRIDE { return !isConstant(); }
1224  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1225 
1226  //--------------------------------------------------------
1227  // Leaf-specific methods
1228  //--------------------------------------------------------
1229 public:
1231  const Sawyer::Container::BitVector& bits() const;
1232 
1234  bool isIntegerVariable() const {
1235  return type().typeClass() == Type::INTEGER && !isConstant();
1236  }
1237 
1240  return type().typeClass() == Type::FP && !isConstant();
1241  }
1242 
1244  bool isFloatingPointNan() const;
1245 
1247  bool isMemoryVariable() const {
1248  return type().typeClass() == Type::MEMORY && !isConstant();
1249  }
1250 
1255  uint64_t nameId() const;
1256 
1261  std::string toString() const;
1262 
1264  void printAsSigned(std::ostream&, Formatter&, bool asSigned = true) const;
1265 
1267  void printAsUnsigned(std::ostream &o, Formatter &f) const {
1268  printAsSigned(o, f, false);
1269  }
1270 
1271 private:
1272  // Obtain or register a name ID
1273  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1274 
1275  // Deprecated functions
1276 public:
1277  // Deprecated [Robb Matzke 2019-09-27]
1278  static LeafPtr createVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
1279  ROSE_DEPRECATED("use createVariable with type or makeIntegerVariable, etc.") {
1280  return createVariable(Type::integer(nBits), comment, flags);
1281  }
1282 
1283  // Deprecated [Robb Matzke 2019-09-27]
1284  static LeafPtr createExistingVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0)
1285  ROSE_DEPRECATED("use createVariable or makeIntegerVariable, etc.") {
1286  return createVariable(Type::integer(nBits), id, comment, flags);
1287  }
1288 
1289  // Deprecated [Robb Matzke 2019-09-27]
1290  static LeafPtr createInteger(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
1291  ROSE_DEPRECATED("use createConstant or makeIntegerConstant, etc.");
1292 
1293  // Deprecated [Robb Matzke 2019-09-27]
1294  static LeafPtr createConstant(const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0)
1295  ROSE_DEPRECATED("use createConstant with type or makeIntegerConstant, etc.") {
1296  return createConstant(Type::integer(bits.size()), bits, comment, flags);
1297  }
1298 
1299  // Deprecated [Robb Matzke 2019-09-27]
1300  static LeafPtr createBoolean(bool b, const std::string &comment="", unsigned flags=0)
1301  ROSE_DEPRECATED("use createConstant or makeBooleanConstant");
1302 
1303  // Deprecated [Robb Matzke 2019-09-27]
1304  static LeafPtr createMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
1305  ROSE_DEPRECATED("use createVariable with type or makeMemoryVariable") {
1306  return createVariable(Type::memory(addressWidth, valueWidth), comment, flags);
1307  }
1308 
1309  // Deprecated [Robb Matzke 2019-09-27]
1310  static LeafPtr createExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="",
1311  unsigned flags=0)
1312  ROSE_DEPRECATED("use createVariable with type or makeMemoryVariable") {
1313  return createVariable(Type::memory(addressWidth, valueWidth), id, comment, flags);
1314  }
1315 
1316  // Deprecated [Robb Matzke 2019-09-27]. The definition will eventually change to isVariable2()
1317  bool isVariable() const ROSE_DEPRECATED("use isIntegerVariable or isVariable2 instead") {
1318  return isIntegerVariable();
1319  }
1320 
1321  // Deprecated [Robb Matzke 2019-09-27]
1322  virtual bool isMemory() ROSE_DEPRECATED("use isMemoryVariable or isMemoryExpr instead") {
1323  return isMemoryVariable();
1324  }
1325 };
1326 
1328 // Factories
1330 
1336 LeafPtr makeVariable(const Type&, const std::string &comment="", unsigned flags=0);
1337 LeafPtr makeVariable(const Type&, uint64_t id, const std::string &comment="", unsigned flags=0);
1338 LeafPtr makeConstant(const Type&, const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1339 LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0);
1340 LeafPtr makeIntegerVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0);
1341 LeafPtr makeIntegerConstant(size_t nBits, uint64_t n, const std::string &comment="", unsigned flags=0);
1342 LeafPtr makeIntegerConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1343 LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0);
1344 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1345 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
1346 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1347 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, uint64_t id, const std::string &comment="", unsigned flags=0);
1348 LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0);
1349 LeafPtr makeFloatingPointConstant(double, const std::string &comment="", unsigned flags=0);
1350 LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1353 // Deprecated [Robb Matzke 2019-09-27]
1354 Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0)
1355  ROSE_DEPRECATED("use makeIntegerVariable instead");
1356 Ptr makeExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0)
1357  ROSE_DEPRECATED("use makeIntegerVariable instead");
1358 Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0)
1359  ROSE_DEPRECATED("use makeIntegerConstant instead");
1360 Ptr makeConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0)
1361  ROSE_DEPRECATED("use makeIntegerConstant instead");
1362 Ptr makeBoolean(bool, const std::string &comment="", unsigned flags=0)
1363  ROSE_DEPRECATED("use makeBooleanConstant instead");
1364 Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
1365  ROSE_DEPRECATED("use makeMemoryVariable instead");
1366 Ptr makeExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0)
1367  ROSE_DEPRECATED("use makeMemoryVariable instead");
1368 
1375 Ptr makeAdd(const Ptr&a, const Ptr &b,
1376  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1377 Ptr makeBooleanAnd(const Ptr &a, const Ptr &b,
1378  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1379  ROSE_DEPRECATED("use makeAnd instead"); // [Robb Matzke 2017-11-21]: deprecated
1380 Ptr makeAsr(const Ptr &sa, const Ptr &a,
1381  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1382 Ptr makeAnd(const Ptr &a, const Ptr &b,
1383  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1384 Ptr makeOr(const Ptr &a, const Ptr &b,
1385  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1386 Ptr makeXor(const Ptr &a, const Ptr &b,
1387  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1388 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1389  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1390 Ptr makeConvert(const Ptr &a,
1391  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1392 Ptr makeEq(const Ptr &a, const Ptr &b,
1393  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1394 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1395  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1396 Ptr makeInvert(const Ptr &a,
1397  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1398 Ptr makeIsInfinite(const Ptr &a,
1399  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1400 Ptr makeIsNan(const Ptr &a,
1401  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1402 Ptr makeIsNeg(const Ptr &a,
1403  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1404 Ptr makeIsNorm(const Ptr &a,
1405  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1406 Ptr makeIsPos(const Ptr &a,
1407  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1408 Ptr makeIsSubnorm(const Ptr &a,
1409  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1410 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1411  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1412 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1413  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1414 Ptr makeLssb(const Ptr &a,
1415  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1416 Ptr makeMax(const Ptr &a, const Ptr &b,
1417  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1418 Ptr makeMin(const Ptr &a, const Ptr &b,
1419  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1420 Ptr makeMssb(const Ptr &a,
1421  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1422 Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c,
1423  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1424 Ptr makeNe(const Ptr &a, const Ptr &b,
1425  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1426 Ptr makeNegate(const Ptr &a,
1427  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1428 Ptr makeBooleanOr(const Ptr &a, const Ptr &b,
1429  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1430  ROSE_DEPRECATED("use makeOr instead"); // [Robb Matzke 2017-11-21]: deprecated
1431 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1432  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1433 Ptr makeRol(const Ptr &sa, const Ptr &a,
1434  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1435 Ptr makeRor(const Ptr &sa, const Ptr &a,
1436  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1437 Ptr makeRound(const Ptr &a,
1438  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1439 Ptr makeSet(const Ptr &a, const Ptr &b,
1440  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1441 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1442  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1443 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1444  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1445 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1446  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1447 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1448  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1449 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1450  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1451 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1452  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1453 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1454  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1455 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1456  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1457 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1458  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1459 Ptr makeIsSignedPos(const Ptr &a,
1460  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1461 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1462  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1463 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1464  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1465 Ptr makeSignedMax(const Ptr &a, const Ptr &b,
1466  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1467 Ptr makeSignedMin(const Ptr &a, const Ptr &b,
1468  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1469 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1470  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1471 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1472  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1473 Ptr makeSqrt(const Ptr &a,
1474  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1475 Ptr makeDiv(const Ptr &a, const Ptr &b,
1476  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1477 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1478  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1479 Ptr makeGe(const Ptr &a, const Ptr &b,
1480  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1481 Ptr makeGt(const Ptr &a, const Ptr &b,
1482  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1483 Ptr makeLe(const Ptr &a, const Ptr &b,
1484  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1485 Ptr makeLt(const Ptr &a, const Ptr &b,
1486  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1487 Ptr makeMod(const Ptr &a, const Ptr &b,
1488  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1489 Ptr makeMul(const Ptr &a, const Ptr &b,
1490  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1491 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1492  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1493 Ptr makeZerop(const Ptr &a,
1494  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1498 // Miscellaneous functions
1501 
1502 
1503 std::ostream& operator<<(std::ostream &o, Node&);
1504 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1505 
1507 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1508 
1513 Hash hash(const std::vector<Ptr>&);
1514 
1519 template<typename InputIterator>
1520 uint64_t
1521 nNodes(InputIterator begin, InputIterator end) {
1522  uint64_t total = 0;
1523  for (InputIterator ii=begin; ii!=end; ++ii) {
1524  uint64_t n = (*ii)->nnodes();
1525  if (MAX_NNODES==n)
1526  return MAX_NNODES;
1527  if (total + n < total)
1528  return MAX_NNODES;
1529  total += n;
1530  }
1531  return total;
1532 }
1533 
1538 template<typename InputIterator>
1539 uint64_t
1540 nNodesUnique(InputIterator begin, InputIterator end)
1541 {
1542  struct T1: Visitor {
1543  typedef std::set<const Node*> SeenNodes;
1544 
1545  SeenNodes seen; // nodes that we've already seen, and the subtree size
1546  uint64_t nUnique; // number of unique nodes
1547 
1548  T1(): nUnique(0) {}
1549 
1550  VisitAction preVisit(const Ptr &node) {
1551  if (seen.insert(getRawPointer(node)).second) {
1552  ++nUnique;
1553  return CONTINUE; // this node has not been seen before; traverse into children
1554  } else {
1555  return TRUNCATE; // this node has been seen already; skip over the children
1556  }
1557  }
1558 
1559  VisitAction postVisit(const Ptr &node) {
1560  return CONTINUE;
1561  }
1562  } visitor;
1563 
1564  VisitAction status = CONTINUE;
1565  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1566  status = (*ii)->depthFirstTraversal(visitor);
1567  return visitor.nUnique;
1568 }
1569 
1576 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1577 
1578 template<typename InputIterator>
1579 std::vector<Ptr>
1580 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1581  typedef Sawyer::Container::Map<Ptr, size_t> NodeCounts;
1582  struct T1: Visitor {
1583  NodeCounts nodeCounts;
1584  std::vector<Ptr> result;
1585 
1586  VisitAction preVisit(const Ptr &node) ROSE_OVERRIDE {
1587  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1588  if (2 == ++nSeen)
1589  result.push_back(node);
1590  return nSeen>1 ? TRUNCATE : CONTINUE;
1591  }
1592 
1593  VisitAction postVisit(const Ptr&) ROSE_OVERRIDE {
1594  return CONTINUE;
1595  }
1596  } visitor;
1597 
1598  for (InputIterator ii=begin; ii!=end; ++ii)
1599  (*ii)->depthFirstTraversal(visitor);
1600  return visitor.result;
1601 }
1611 template<class Substitution>
1612 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1613  if (!src)
1614  return Ptr(); // no input implies no output
1615 
1616  // Try substituting the whole expression, returning the result.
1617  Ptr dst = subber(src, solver);
1618  ASSERT_not_null(dst);
1619  if (dst != src)
1620  return dst;
1621 
1622  // Try substituting all the subexpressions.
1623  InteriorPtr inode = src->isInteriorNode();
1624  if (!inode)
1625  return src;
1626  bool anyChildChanged = false;
1627  Nodes newChildren;
1628  newChildren.reserve(inode->nChildren());
1629  BOOST_FOREACH (const Ptr &child, inode->children()) {
1630  Ptr newChild = substitute(child, subber, solver);
1631  if (newChild != child)
1632  anyChildChanged = true;
1633  newChildren.push_back(newChild);
1634  }
1635  if (!anyChildChanged)
1636  return src;
1637 
1638  // Some subexpression changed, so build a new expression
1639  return Interior::instance(inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1640 }
1641 
1642 } // namespace
1643 } // namespace
1644 } // namespace
1645 
1646 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1647 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1648 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1649 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Node, 1);
1650 #endif
1651 
1652 #endif
Ptr renameVariables(ExprExprHashMap &index, size_t &nextVariableId, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite using lowest numbered variable names.
Operator-specific simplification methods.
virtual int compareStructure(const Ptr &other) ROSE_OVERRIDE
Compare two expressions structurally for sorting.
const std::string & comment() const
Property: Comment.
bool add_renames
Add additional entries to the renames as variables are encountered?
bool isFloatingPointExpr() const
True if this expression is of a floating-point type.
bool isHashed() const
Returns true if this node has a hash value computed and cached.
virtual uint64_t nNodes() const ROSE_OVERRIDE
Computes the size of an expression by counting the number of nodes.
ShowComments show_comments
Show node comments when printing?
Ordered set of values.
Definition: Set.h:46
Ptr makeSignedLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
std::string comment_
Optional comment.
virtual size_t nChildren() const ROSE_OVERRIDE
Number of arguments.
RenameMap renames
Map for renaming variables to use smaller integers.
virtual bool isVariable2() const ROSE_OVERRIDE
True if this expression is a variable.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
size_t max_depth
If non-zero, then replace deep parts of expressions with "...".
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.
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.
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.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
virtual bool isEquivalentTo(const Ptr &other)=0
Tests two expressions for structural equivalence.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
Continue the traversal as normal.
Interior node of an expression tree for instruction semantics.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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.
virtual Operator getOperator() const ROSE_OVERRIDE
Operator for interior nodes.
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. ...
Ptr makeRead(const Ptr &mem, const Ptr &addr, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeXor(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
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.
Floating-point round to integer as FP type.
void adjustWidth()
Adjust width based on operands.
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.
virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE
Tests two expressions for structural equivalence.
Mapping from expression to expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual size_t nChildren() const =0
Number of arguments.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const
Rewrite the entire expression to something simpler.
Shift left, introducing zeros at lsb.
LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0)
Leaf constructor.
bool isFloatingPointConstant() const
True if this epxression is a floating-point constant.
unsigned flags() const
Property: User-defined bit flags.
Ptr makeDiv(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
const boost::any & userData() const
Property: User-defined data.
virtual Ptr child(size_t idx) const ROSE_OVERRIDE
Argument.
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.
VisitAction
Return type for visitors.
void userData(boost::any &data)
Property: User-defined data.
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?
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isScalar() const
Check whether expression is scalar.
virtual size_t nChildren() const ROSE_OVERRIDE
Number of arguments.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeGt(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 ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Sawyer::Optional< uint64_t > toUnsigned() const ROSE_OVERRIDE
The unsigned integer value of the expression.
STL namespace.
Holds a value or nothing.
Definition: Optional.h:49
Sawyer::Container::Set< Ptr, ExpressionLessp > ExpressionSet
Set of expressions ordered by hash.
static const unsigned UNSPECIFIED
Value is somehow unspecified.
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 Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Shift right, introducing ones at msb.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual bool isConstant() const ROSE_OVERRIDE
True if this expression is a constant.
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.
Ptr involutary()
Simplifies involutary operators.
Ptr setToIte(const Ptr &, const SmtSolverPtr &solver=SmtSolverPtr(), const LeafPtr &var=LeafPtr())
Convert a set to an ite expression.
bool isIntegerConstant() const
True if this expression is an integer constant.
Main namespace for the ROSE library.
Floating-point greater-than or equal.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Controls formatting of expression trees when printing.
virtual bool isVariable2() const =0
True if this expression is a variable.
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.
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 rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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 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.
bool operator!=(const Type &other) const
Type equality.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isMemoryExpr() const
True if this expression is of a memory type.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Name space for the entire library.
virtual void print(std::ostream &, Formatter &) const ROSE_OVERRIDE
Print the expression to a stream.
Shift left, introducing ones at lsb.
Unsigned greater-than-or-equal.
InteriorPtr isInteriorNode() const
Dynamic cast of this object to an interior node.
uint64_t nNodesUnique() const
Number of unique nodes in expression.
Sawyer::SharedPointer< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
SharedPointer< Node > sharedFromThis()
Create a shared pointer from this.
TypeClass typeClass() const
Property: Type class.
Ptr makeOr(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 ROSE_OVERRIDE
The signed integer value of the expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Like CMT_AFTER, but show comments instead of variable names.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
InteriorPtr associative()
Simplifies non-associative operators by flattening the specified interior node with its children that...
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.
Ptr makeBooleanAnd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) ROSE_DEPRECATED("use makeAnd instead")
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_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.
Ptr makeRor(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr child(size_t idx) const =0
Argument.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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 ROSE_OVERRIDE
Traverse the expression.
virtual const Nodes & children() const ROSE_OVERRIDE
Arguments.
virtual VisitAction depthFirstTraversal(Visitor &) const =0
Traverse the expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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.
Ptr simplifyTop(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies the specified interior node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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?
bool show_width
Show width in bits inside square brackets.
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.
Ptr makeIsSubnorm(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
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.
virtual int compareStructure(const Ptr &other)=0
Compare two expressions structurally for sorting.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeMul(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 ROSE_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.
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.
virtual bool isVariable2() const ROSE_OVERRIDE
True if this expression is a variable.
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.
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.
Ptr makeBooleanOr(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) ROSE_DEPRECATED("use makeOr instead")
Interior node constructor.
void comment(const std::string &s)
Property: Comment.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t n, const std::string &comment="", unsigned flags=0)
Leaf constructor.
static const unsigned RESERVED_FLAGS
These flags are reserved for use within ROSE.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Floating-point less-than or equal.
void assertAcyclic() const
Asserts that expressions are acyclic.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
Type()
Create an invalid, empty type.
Sawyer::SharedPointer< Leaf > LeafPtr
Shared-ownership pointer to an expression Leaf node.
Base class for reference counted objects.
Definition: SharedObject.h:64
bool isIntegerVariable() const
True if this expression is an integer variable.
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.
Sawyer::SharedPointer< Interior > InteriorPtr
Shared-ownership pointer to an expression Interior node.
std::set< LeafPtr > getVariables() const
Returns the variables appearing in the expression.
Ptr makeMax(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isMemoryVariable() const
True if this expression is a memory state variable.
static Type integer(size_t nBits)
Create a new integer type.
Exceptions for symbolic expressions.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool use_hexadecimal
Show values in hexadecimal and decimal rather than just decimal.
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.
bool operator<(const Type &other) const
Type comparison.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Returns true if two expressions must be equal (cannot be unequal).
bool isFloatingPointVariable() const
True if this expression is a floating-point variable.
Base class for symbolic expression nodes.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Substitute one value for another.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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 print(std::ostream &o) const
Print the expression to a stream.
Operator
Operators for interior nodes of the expression tree.
Ptr makeMssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t addressWidth() const
Property: Width of memory addresses.
bool isEmpty() const
Determines if the vector is empty.
Definition: BitVector.h:184
bool operator==(const Type &other) const
Type equality.
Ptr unaryNoOp()
Replaces a binary operator with its only argument.
bool show_flags
Show user-defined flags inside square brackets.
API and storage for attributes.
Definition: Attribute.h:208
size_t significandWidth() const
Property: Significand width.
Compare two expressions for STL containers.
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 Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
WithFormatter withFormat(Formatter &fmt)
Combines a node with a formatter for printing.
WithFormatter operator+(Formatter &fmt)
Combines a node with a formatter for printing.
virtual Ptr child(size_t idx) const ROSE_OVERRIDE
Argument.
Represents no value.
Definition: Optional.h:32
Hash hash() const
Returns (and caches) the hash value for this node.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Base class for visiting nodes during expression traversal.
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.
Base class for all ROSE exceptions.
Definition: RoseException.h:9
Write (update) memory with a new value.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Returns true if two expressions might be equal, but not necessarily be equal.
Ptr makeSignedGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeConvert(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isIntegerExpr() const
True if this expression is of an integer type.
static Type memory(size_t addressWidth, size_t valueWidth)
Create a new memory type.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
std::vector< Ptr > findCommonSubexpressions() const
Find common subexpressions.
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
Ptr foldConstants(const Simplifier &)
Perform constant folding.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
size_t nBits() const
Property: Number of significant bits.
Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver=SmtSolverPtr())
Simplify an interior node.
InteriorPtr idempotent(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies idempotent operators.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeSignedMul(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
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.
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 Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const
Constant folding.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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.