ROSE  0.9.12.28
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 namespace TypeStyle {
53  enum Flag {
54  FULL,
56  };
57 }
58 
59 
61 class Exception: public Rose::Exception {
62 public:
63  explicit Exception(const std::string &mesg): Rose::Exception(mesg) {}
64 };
65 
71 enum Operator {
144  OP_BV_AND = OP_AND, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
145  OP_BV_OR = OP_OR, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
146  OP_BV_XOR = OP_XOR // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
147 };
148 
149 std::string toStr(Operator);
150 
151 class Node;
152 class Interior;
153 class Leaf;
155 
158 
161 
164 
165 typedef std::vector<Ptr> Nodes;
167 
169 typedef uint64_t Hash;
170 
172 struct Formatter {
177  };
178  Formatter()
180  max_depth(0), cur_depth(0), show_type(true), show_flags(true) {}
182  bool do_rename;
183  bool add_renames;
185  size_t max_depth;
186  size_t cur_depth;
187  RenameMap renames;
188  bool show_type;
189  bool show_flags;
190 };
191 
197 };
198 
203 extern const uint64_t MAX_NNODES; // defined in .C so we don't pollute user namespace with limit macros
204 
209 class Visitor {
210 public:
211  virtual ~Visitor() {}
212  virtual VisitAction preVisit(const Ptr&) = 0;
213  virtual VisitAction postVisit(const Ptr&) = 0;
214 };
215 
216 
217 
219 // Expression type information
221 
223 class Type {
224 public:
226  enum TypeClass {
228  FP,
231  };
232 
233 private:
234  TypeClass typeClass_;
235  size_t totalWidth_;
236  size_t secondaryWidth_;
237 
238 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
239 private:
240  friend class boost::serialization::access;
241 
242  template<class S>
243  void serialize(S &s, const unsigned /*version*/) {
244  s & BOOST_SERIALIZATION_NVP(typeClass_);
245  s & BOOST_SERIALIZATION_NVP(totalWidth_);
246  s & BOOST_SERIALIZATION_NVP(secondaryWidth_);
247  }
248 #endif
249 
253 public:
255  : typeClass_(INVALID), totalWidth_(0), secondaryWidth_(0) {}
256 
257 private:
258  Type(TypeClass tc, size_t w1, size_t w2)
259  : typeClass_(tc), totalWidth_(w1), secondaryWidth_(w2) {}
260 
261 public:
265  static Type none() {
266  return Type();
267  }
268 
274  static Type integer(size_t nBits) {
275  return Type(INTEGER, nBits, 0);
276  }
277 
281  static Type memory(size_t addressWidth, size_t valueWidth) {
282  return Type(MEMORY, valueWidth, addressWidth);
283  }
284 
292  return Type(FP, 1 /*sign bit*/ + exponentWidth + significandWidth - 1 /*implied bit*/, exponentWidth);
293  }
294 
298  bool isValid() const {
299  return typeClass_ != INVALID;
300  }
301 
306  return typeClass_;
307  }
308 
313  size_t nBits() const {
314  return totalWidth_;
315  }
316 
321  size_t addressWidth() const {
322  ASSERT_require(MEMORY == typeClass_);
323  return secondaryWidth_;
324  }
325 
330  size_t exponentWidth() const {
331  ASSERT_require(FP == typeClass_);
332  return secondaryWidth_;
333  }
334 
340  size_t significandWidth() const {
341  ASSERT_require(FP == typeClass_);
342  return totalWidth_ - (1 /* sign bit */ + exponentWidth() - 1 /*implied bit*/);
343  }
344 
350  bool operator==(const Type &other) const {
351  return typeClass_ == other.typeClass_ && totalWidth_ == other.totalWidth_ && secondaryWidth_ == other.secondaryWidth_;
352  }
353  bool operator!=(const Type &other) const {
354  return !(*this == other);
355  }
359  bool operator<(const Type &other) const;
360 
362  void print(std::ostream&, TypeStyle::Flag style = TypeStyle::FULL) const;
363 
365  std::string toString(TypeStyle::Flag style = TypeStyle::FULL) const;
366 };
367 
368 
369 
370 
371 
373 // Base Node Type
375 
413 class Node
414  : public Sawyer::SharedObject,
415  public Sawyer::SharedFromThis<Node>,
416  public Sawyer::SmallObject,
417  public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
418 protected:
419  Type type_;
420  unsigned flags_;
421  std::string comment_;
422  Hash hashval_;
423  boost::any userData_;
425 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
426 private:
427  friend class boost::serialization::access;
428 
429  template<class S>
430  void serialize(S &s, const unsigned version) {
431  if (version < 1)
432  ASSERT_not_reachable("SymbolicExpr version " + boost::lexical_cast<std::string>(version) + " is no longer supported");
433  s & BOOST_SERIALIZATION_NVP(type_);
434  s & BOOST_SERIALIZATION_NVP(flags_);
435  s & BOOST_SERIALIZATION_NVP(comment_);
436  s & BOOST_SERIALIZATION_NVP(hashval_);
437  // s & userData_;
438  }
439 #endif
440 
441 public:
442  // Bit flags
443 
445  static const unsigned RESERVED_FLAGS = 0x0000ffff;
446 
448  static const unsigned INDETERMINATE = 0x00000001;
449 
454  static const unsigned UNSPECIFIED = 0x00000002;
455 
458  static const unsigned BOTTOM = 0x00000004;
459 
460 protected:
461  Node()
462  : type_(Type::integer(0)), flags_(0), hashval_(0) {}
463  explicit Node(const std::string &comment, unsigned flags=0)
464  : type_(Type::integer(0)), flags_(flags), comment_(comment), hashval_(0) {}
465 
466 public:
468  Type type() const {
469  return type_;
470  }
471 
478  static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
479 
485  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
486 
488  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
489 
495  virtual bool isEquivalentTo(const Ptr &other) = 0;
496 
502  virtual int compareStructure(const Ptr &other) = 0;
503 
509  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
510 
518  Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
519 
527  Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
528  const SmtSolverPtr &solver = SmtSolverPtr());
529 
533  virtual Operator getOperator() const = 0;
534 
538  virtual size_t nChildren() const = 0;
539 
544  virtual Ptr child(size_t idx) const = 0;
545 
549  virtual const Nodes& children() const = 0;
550 
555  virtual Sawyer::Optional<uint64_t> toUnsigned() const = 0;
556 
560  virtual Sawyer::Optional<int64_t> toSigned() const = 0;
561 
563  bool isIntegerExpr() const {
564  return type_.typeClass() == Type::INTEGER;
565  }
566 
568  bool isFloatingPointExpr() const {
569  return type_.typeClass() == Type::FP;
570  }
571 
573  bool isMemoryExpr() const {
574  return type_.typeClass() == Type::MEMORY;
575  }
576 
580  bool isScalarExpr() const {
581  return isIntegerExpr() || isFloatingPointExpr();
582  }
583 
585  virtual bool isConstant() const = 0;
586 
588  bool isIntegerConstant() const {
589  return isIntegerExpr() && isConstant();
590  }
591 
593  bool isFloatingPointConstant() const {
594  return isFloatingPointExpr() && isConstant();
595  }
596 
600  bool isScalarConstant() const {
602  }
603 
605  bool isFloatingPointNan() const;
606 
612  virtual bool isVariable2() const = 0;
613 
615  bool isIntegerVariable() const {
616  return isIntegerExpr() && isVariable2();
617  }
618 
620  bool isFloatingPointVariable() const {
621  return isFloatingPointExpr() && isVariable2();
622  }
623 
625  bool isMemoryVariable() const {
626  return isMemoryExpr() && isVariable2();
627  }
628 
632  bool isScalarVariable() const {
634  }
635 
644  const std::string& comment() const {
645  return comment_;
646  }
647  void comment(const std::string &s) {
648  comment_ = s;
649  }
659  void userData(boost::any &data) {
660  userData_ = data;
661  }
662  const boost::any& userData() const {
663  return userData_;
664  }
670  size_t nBits() const {
671  return type_.nBits();
672  }
673 
678  unsigned flags() const {
679  return flags_;
680  }
681 
685  Ptr newFlags(unsigned flags) const;
686 
690  size_t domainWidth() const {
691  return type_.addressWidth();
692  }
693 
697  bool isScalar() const {
698  return type_.typeClass() != Type::MEMORY;
699  }
700 
705  virtual VisitAction depthFirstTraversal(Visitor&) const = 0;
706 
722  virtual uint64_t nNodes() const = 0;
723 
725  uint64_t nNodesUnique() const;
726 
728  std::set<LeafPtr> getVariables() const;
729 
733  InteriorPtr isInteriorNode() const;
734 
738  LeafPtr isLeafNode() const;
739 
743  bool isHashed() const {
744  return hashval_ != 0;
745  }
746 
749  Hash hash() const;
750 
751  // used internally to set the hash value
752  void hash(Hash);
753 
756  private:
757  Ptr node;
758  Formatter &formatter;
759  public:
760  WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
761  void print(std::ostream &stream) const { node->print(stream, formatter); }
762  };
763 
785  virtual void print(std::ostream&, Formatter&) const = 0;
786  void print(std::ostream &o) const { Formatter fmt; print(o, fmt); }
790  void assertAcyclic() const;
791 
797  std::vector<Ptr> findCommonSubexpressions() const;
798 
804  bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/) const;
805 
807  InteriorPtr isOperator(Operator) const;
808 
809 protected:
810  void printFlags(std::ostream &o, unsigned flags, char &bracket) const;
811 
812 public:
813  // Deprecated [Robb Matzke 2019-09-27]
814  bool isNumber() const ROSE_DEPRECATED("use isIntegerConstant instead") {
815  return isIntegerConstant();
816  }
817 
818  // Deprecated [Robb Matzke 2019-09-27]
819  uint64_t toInt() ROSE_DEPRECATED("use toUnsigned() instead") {
820  return toUnsigned().get();
821  }
822 };
823 
825 class Simplifier {
826 public:
827  virtual ~Simplifier() {}
828 
832  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
833  return Ptr();
834  }
835 
838  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
839  return Ptr();
840  }
841 };
842 
844  size_t operator()(const Ptr &expr) const {
845  return expr->hash();
846  }
847 };
848 
850  bool operator()(const Ptr &a, const Ptr &b) const {
851  return a->isEquivalentTo(b);
852  }
853 };
854 
857 public:
858  bool operator()(const Ptr &a, const Ptr &b);
859 };
860 
862 class ExprExprHashMap: public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
863  ExprExprHashMapHasher, ExprExprHashMapCompare> {
864 public:
865  ExprExprHashMap invert() const;
866 };
867 
870 
871 
873 // Simplification
875 
877  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
878  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
879 };
881  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
882  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
883 };
885  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
886 };
888  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
889  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
890 };
892  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
893  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
894 };
896  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
897 };
899  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
900 };
902  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
903  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
904 };
906  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
907 };
909  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
910 };
912  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
913 };
915  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
916 };
918  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
919 };
921  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
922 };
924  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
925 };
927  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
928 };
930  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
931 };
933  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
934 };
936  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
937 };
939  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
940 };
942  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
943 };
945  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
946 };
948  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
949 };
951  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
952 };
954  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
955 };
957  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
958 };
960  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
961 };
963  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
964 };
966  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
967 };
969  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
970 };
972  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
973 };
975  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
976 };
978  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
979 };
981  bool newbits;
982  ShiftSimplifier(bool newbits): newbits(newbits) {}
983  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
984 };
986  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
987  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
988 };
990  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
991  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
992 };
994  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
995 };
997  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
998 };
1000  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1001 };
1002 
1003 
1004 
1006 // Interior Nodes
1008 
1015 class Interior: public Node {
1016 private:
1017  Operator op_;
1018  Nodes children_;
1019  uint64_t nnodes_; // total number of nodes; self + children's nnodes
1020 
1021  //--------------------------------------------------------
1022  // Serialization
1023  //--------------------------------------------------------
1024 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1025 private:
1026  friend class boost::serialization::access;
1027 
1028  template<class S>
1029  void serialize(S &s, const unsigned /*version*/) {
1030  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1031  s & BOOST_SERIALIZATION_NVP(op_);
1032  s & BOOST_SERIALIZATION_NVP(children_);
1033  s & BOOST_SERIALIZATION_NVP(nnodes_);
1034  }
1035 #endif
1036 
1037  //--------------------------------------------------------
1038  // Real constructors
1039  //--------------------------------------------------------
1040 private:
1041  Interior(); // needed for serialization
1042  // Only constructs, does not simplify.
1043  Interior(const Type&, Operator, const Nodes &arguments, const std::string &comment, unsigned flags);
1044 
1045  //--------------------------------------------------------
1046  // Allocating constructors
1047  //--------------------------------------------------------
1048 public:
1052  static Ptr instance(Operator op, const Ptr &a,
1053  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1054  static Ptr instance(const Type &type, Operator op, const Ptr &a,
1055  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1056  static Ptr instance(Operator op, const Ptr &a, const Ptr &b,
1057  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1058  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b,
1059  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1060  static Ptr instance(Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1061  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1062  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1063  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1064  static Ptr instance(Operator op, const Nodes &arguments,
1065  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1066  static Ptr instance(const Type &type, Operator op, const Nodes &arguments,
1067  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1070  //--------------------------------------------------------
1071  // Overrides
1072  //--------------------------------------------------------
1073 public:
1074  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1075  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1076  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1077  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1078  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1079  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1080  virtual uint64_t nNodes() const ROSE_OVERRIDE { return nnodes_; }
1081  virtual const Nodes& children() const ROSE_OVERRIDE { return children_; }
1082  virtual Operator getOperator() const ROSE_OVERRIDE { return op_; }
1083  virtual size_t nChildren() const ROSE_OVERRIDE { return children_.size(); }
1084  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return idx < children_.size() ? children_[idx] : Ptr(); }
1085  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1086  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1087  virtual bool isConstant() const ROSE_OVERRIDE { return false; }
1088  virtual bool isVariable2() const ROSE_OVERRIDE { return false; }
1089 
1090  //--------------------------------------------------------
1091  // Simplification
1092  //--------------------------------------------------------
1093 public:
1097  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
1098 
1101  Ptr foldConstants(const Simplifier&);
1102 
1107  InteriorPtr associative();
1108 
1113  InteriorPtr commutative();
1114 
1121  InteriorPtr idempotent(const SmtSolverPtr &solver = SmtSolverPtr());
1122 
1126  Ptr involutary();
1127 
1131  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
1132 
1136  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
1137 
1142  Ptr poisonNan(const SmtSolverPtr &solver = SmtSolverPtr());
1143 
1145  Ptr unaryNoOp();
1146 
1150  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
1151 
1152  //--------------------------------------------------------
1153  // Functions specific to internal nodes
1154  //--------------------------------------------------------
1155 public:
1156  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1157 
1158 protected:
1160  void addChild(const Ptr &child);
1161 
1165  void adjustWidth(const Type&);
1166 
1169  void adjustBitFlags(unsigned extraFlags);
1170 
1171  //--------------------------------------------------------
1172  // Deprecated [Robb Matzke 2019-10-01]
1173  //--------------------------------------------------------
1174 public:
1175  static Ptr create(size_t nbits, Operator op, const Ptr &a,
1176  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1177  ROSE_DEPRECATED("use instance instead");
1178  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b,
1179  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1180  ROSE_DEPRECATED("use instance instead");
1181  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1182  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1183  ROSE_DEPRECATED("use instance instead");
1184  static Ptr create(size_t nbits, Operator op, const Nodes &children,
1185  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1186  ROSE_DEPRECATED("use instance instead");
1187 
1188 };
1189 
1190 
1192 // Leaf Nodes
1194 
1198 class Leaf: public Node {
1199 private:
1200  Sawyer::Container::BitVector bits_; // Value for constants if size > 0
1201  uint64_t name_; // Variable ID for variables when bits_.size() == 0
1202 
1203  //--------------------------------------------------------
1204  // Serialization
1205  //--------------------------------------------------------
1206 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1207 private:
1208  friend class boost::serialization::access;
1209 
1210  template<class S>
1211  void save(S &s, const unsigned /*version*/) const {
1212  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1213  s & BOOST_SERIALIZATION_NVP(bits_);
1214  s & BOOST_SERIALIZATION_NVP(name_);
1215  }
1216 
1217  template<class S>
1218  void load(S &s, const unsigned /*version*/) {
1219  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1220  s & BOOST_SERIALIZATION_NVP(bits_);
1221  s & BOOST_SERIALIZATION_NVP(name_);
1222  nextNameCounter(name_);
1223  }
1224 
1225  BOOST_SERIALIZATION_SPLIT_MEMBER();
1226 #endif
1227 
1228  //--------------------------------------------------------
1229  // Private constructors. Use create methods instead.
1230  //--------------------------------------------------------
1231 private:
1232  Leaf()
1233  : name_(0) {}
1234  explicit Leaf(const std::string &comment, unsigned flags=0)
1235  : Node(comment, flags), name_(0) {}
1236 
1237  // Allocating constructors.
1238 public:
1240  static LeafPtr createVariable(const Type&,
1241  const std::string &comment = "", unsigned flags = 0);
1242 
1244  static LeafPtr createVariable(const Type&, const uint64_t id,
1245  const std::string &comment = "", unsigned flags = 0);
1246 
1248  static LeafPtr createConstant(const Type&, const Sawyer::Container::BitVector&,
1249  const std::string &comment = "", unsigned flags = 0);
1250 
1251  //--------------------------------------------------------
1252  // Override base class implementations
1253  //--------------------------------------------------------
1254 public:
1255  virtual size_t nChildren() const ROSE_OVERRIDE { return 0; }
1256  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return Ptr(); }
1257  virtual const Nodes& children() const ROSE_OVERRIDE;
1258  virtual Operator getOperator() const ROSE_OVERRIDE { return OP_NONE; }
1259  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1260  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1261  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1262  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1263  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1264  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1265  virtual uint64_t nNodes() const ROSE_OVERRIDE { return 1; }
1266  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE;
1267  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE;
1268  virtual bool isConstant() const ROSE_OVERRIDE { return !bits_.isEmpty(); }
1269  virtual bool isVariable2() const ROSE_OVERRIDE { return !isConstant(); }
1270  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1271 
1272  //--------------------------------------------------------
1273  // Leaf-specific methods
1274  //--------------------------------------------------------
1275 public:
1277  const Sawyer::Container::BitVector& bits() const;
1278 
1280  bool isIntegerVariable() const {
1281  return type().typeClass() == Type::INTEGER && !isConstant();
1282  }
1283 
1286  return type().typeClass() == Type::FP && !isConstant();
1287  }
1288 
1290  bool isFloatingPointNan() const;
1291 
1293  bool isMemoryVariable() const {
1294  return type().typeClass() == Type::MEMORY && !isConstant();
1295  }
1296 
1301  uint64_t nameId() const;
1302 
1307  std::string toString() const;
1308 
1310  void printAsSigned(std::ostream&, Formatter&, bool asSigned = true) const;
1311 
1313  void printAsUnsigned(std::ostream &o, Formatter &f) const {
1314  printAsSigned(o, f, false);
1315  }
1316 
1317 private:
1318  // Obtain or register a name ID
1319  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1320 
1321  // Deprecated functions
1322 public:
1323  // Deprecated [Robb Matzke 2019-09-27]
1324  static LeafPtr createVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
1325  ROSE_DEPRECATED("use createVariable with type or makeIntegerVariable, etc.") {
1326  return createVariable(Type::integer(nBits), comment, flags);
1327  }
1328 
1329  // Deprecated [Robb Matzke 2019-09-27]
1330  static LeafPtr createExistingVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0)
1331  ROSE_DEPRECATED("use createVariable or makeIntegerVariable, etc.") {
1332  return createVariable(Type::integer(nBits), id, comment, flags);
1333  }
1334 
1335  // Deprecated [Robb Matzke 2019-09-27]
1336  static LeafPtr createInteger(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
1337  ROSE_DEPRECATED("use createConstant or makeIntegerConstant, etc.");
1338 
1339  // Deprecated [Robb Matzke 2019-09-27]
1340  static LeafPtr createConstant(const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0)
1341  ROSE_DEPRECATED("use createConstant with type or makeIntegerConstant, etc.") {
1342  return createConstant(Type::integer(bits.size()), bits, comment, flags);
1343  }
1344 
1345  // Deprecated [Robb Matzke 2019-09-27]
1346  static LeafPtr createBoolean(bool b, const std::string &comment="", unsigned flags=0)
1347  ROSE_DEPRECATED("use createConstant or makeBooleanConstant");
1348 
1349  // Deprecated [Robb Matzke 2019-09-27]
1350  static LeafPtr createMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
1351  ROSE_DEPRECATED("use createVariable with type or makeMemoryVariable") {
1352  return createVariable(Type::memory(addressWidth, valueWidth), comment, flags);
1353  }
1354 
1355  // Deprecated [Robb Matzke 2019-09-27]
1356  static LeafPtr createExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="",
1357  unsigned flags=0)
1358  ROSE_DEPRECATED("use createVariable with type or makeMemoryVariable") {
1359  return createVariable(Type::memory(addressWidth, valueWidth), id, comment, flags);
1360  }
1361 
1362  // Deprecated [Robb Matzke 2019-09-27]. The definition will eventually change to isVariable2()
1363  bool isVariable() const ROSE_DEPRECATED("use isIntegerVariable or isVariable2 instead") {
1364  return isIntegerVariable();
1365  }
1366 
1367  // Deprecated [Robb Matzke 2019-09-27]
1368  virtual bool isMemory() ROSE_DEPRECATED("use isMemoryVariable or isMemoryExpr instead") {
1369  return isMemoryVariable();
1370  }
1371 };
1372 
1374 // Factories
1376 
1382 LeafPtr makeVariable(const Type&, const std::string &comment="", unsigned flags=0);
1383 LeafPtr makeVariable(const Type&, uint64_t id, const std::string &comment="", unsigned flags=0);
1384 LeafPtr makeConstant(const Type&, const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1385 LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0);
1386 LeafPtr makeIntegerVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0);
1387 LeafPtr makeIntegerConstant(size_t nBits, uint64_t n, const std::string &comment="", unsigned flags=0);
1388 LeafPtr makeIntegerConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1389 LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0);
1390 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1391 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
1392 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1393 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, uint64_t id, const std::string &comment="", unsigned flags=0);
1394 LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0);
1395 LeafPtr makeFloatingPointConstant(double, const std::string &comment="", unsigned flags=0);
1396 LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1399 // Deprecated [Robb Matzke 2019-09-27]
1400 Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0)
1401  ROSE_DEPRECATED("use makeIntegerVariable instead");
1402 Ptr makeExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0)
1403  ROSE_DEPRECATED("use makeIntegerVariable instead");
1404 Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0)
1405  ROSE_DEPRECATED("use makeIntegerConstant instead");
1406 Ptr makeConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0)
1407  ROSE_DEPRECATED("use makeIntegerConstant instead");
1408 Ptr makeBoolean(bool, const std::string &comment="", unsigned flags=0)
1409  ROSE_DEPRECATED("use makeBooleanConstant instead");
1410 Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
1411  ROSE_DEPRECATED("use makeMemoryVariable instead");
1412 Ptr makeExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0)
1413  ROSE_DEPRECATED("use makeMemoryVariable instead");
1414 
1421 Ptr makeAdd(const Ptr&a, const Ptr &b,
1422  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1423 Ptr makeBooleanAnd(const Ptr &a, const Ptr &b,
1424  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1425  ROSE_DEPRECATED("use makeAnd instead"); // [Robb Matzke 2017-11-21]: deprecated
1426 Ptr makeAsr(const Ptr &sa, const Ptr &a,
1427  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1428 Ptr makeAnd(const Ptr &a, const Ptr &b,
1429  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1430 Ptr makeOr(const Ptr &a, const Ptr &b,
1431  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1432 Ptr makeXor(const Ptr &a, const Ptr &b,
1433  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1434 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1435  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1436 Ptr makeConvert(const Ptr &a, const Type &b,
1437  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1438 Ptr makeEq(const Ptr &a, const Ptr &b,
1439  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1440 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1441  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1442 Ptr makeInvert(const Ptr &a,
1443  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1444 Ptr makeIsInfinite(const Ptr &a,
1445  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1446 Ptr makeIsNan(const Ptr &a,
1447  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1448 Ptr makeIsNeg(const Ptr &a,
1449  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1450 Ptr makeIsNorm(const Ptr &a,
1451  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1452 Ptr makeIsPos(const Ptr &a,
1453  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1454 Ptr makeIsSubnorm(const Ptr &a,
1455  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1456 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1457  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1458 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1459  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1460 Ptr makeLssb(const Ptr &a,
1461  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1462 Ptr makeMax(const Ptr &a, const Ptr &b,
1463  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1464 Ptr makeMin(const Ptr &a, const Ptr &b,
1465  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1466 Ptr makeMssb(const Ptr &a,
1467  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1468 Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c,
1469  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1470 Ptr makeNe(const Ptr &a, const Ptr &b,
1471  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1472 Ptr makeNegate(const Ptr &a,
1473  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1474 Ptr makeBooleanOr(const Ptr &a, const Ptr &b,
1475  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1476  ROSE_DEPRECATED("use makeOr instead"); // [Robb Matzke 2017-11-21]: deprecated
1477 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1478  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1479 Ptr makeReinterpret(const Ptr &a, const Type &b,
1480  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1481 Ptr makeRol(const Ptr &sa, const Ptr &a,
1482  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1483 Ptr makeRor(const Ptr &sa, const Ptr &a,
1484  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1485 Ptr makeRound(const Ptr &a,
1486  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1487 Ptr makeSet(const Ptr &a, const Ptr &b,
1488  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1489 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1490  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1491 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1492  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1493 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1494  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1495 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1496  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1497 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1498  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1499 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1500  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1501 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1502  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1503 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1504  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1505 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1506  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1507 Ptr makeIsSignedPos(const Ptr &a,
1508  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1509 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1510  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1511 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1512  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1513 Ptr makeSignedMax(const Ptr &a, const Ptr &b,
1514  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1515 Ptr makeSignedMin(const Ptr &a, const Ptr &b,
1516  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1517 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1518  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1519 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1520  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1521 Ptr makeSqrt(const Ptr &a,
1522  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1523 Ptr makeDiv(const Ptr &a, const Ptr &b,
1524  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1525 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1526  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1527 Ptr makeGe(const Ptr &a, const Ptr &b,
1528  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1529 Ptr makeGt(const Ptr &a, const Ptr &b,
1530  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1531 Ptr makeLe(const Ptr &a, const Ptr &b,
1532  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1533 Ptr makeLt(const Ptr &a, const Ptr &b,
1534  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1535 Ptr makeMod(const Ptr &a, const Ptr &b,
1536  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1537 Ptr makeMul(const Ptr &a, const Ptr &b,
1538  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1539 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1540  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1541 Ptr makeZerop(const Ptr &a,
1542  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1546 // Miscellaneous functions
1549 
1550 
1551 std::ostream& operator<<(std::ostream &o, Node&);
1552 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1553 
1555 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1556 
1561 Hash hash(const std::vector<Ptr>&);
1562 
1567 template<typename InputIterator>
1568 uint64_t
1569 nNodes(InputIterator begin, InputIterator end) {
1570  uint64_t total = 0;
1571  for (InputIterator ii=begin; ii!=end; ++ii) {
1572  uint64_t n = (*ii)->nnodes();
1573  if (MAX_NNODES==n)
1574  return MAX_NNODES;
1575  if (total + n < total)
1576  return MAX_NNODES;
1577  total += n;
1578  }
1579  return total;
1580 }
1581 
1586 template<typename InputIterator>
1587 uint64_t
1588 nNodesUnique(InputIterator begin, InputIterator end)
1589 {
1590  struct T1: Visitor {
1591  typedef std::set<const Node*> SeenNodes;
1592 
1593  SeenNodes seen; // nodes that we've already seen, and the subtree size
1594  uint64_t nUnique; // number of unique nodes
1595 
1596  T1(): nUnique(0) {}
1597 
1598  VisitAction preVisit(const Ptr &node) {
1599  if (seen.insert(getRawPointer(node)).second) {
1600  ++nUnique;
1601  return CONTINUE; // this node has not been seen before; traverse into children
1602  } else {
1603  return TRUNCATE; // this node has been seen already; skip over the children
1604  }
1605  }
1606 
1607  VisitAction postVisit(const Ptr &node) {
1608  return CONTINUE;
1609  }
1610  } visitor;
1611 
1612  VisitAction status = CONTINUE;
1613  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1614  status = (*ii)->depthFirstTraversal(visitor);
1615  return visitor.nUnique;
1616 }
1617 
1624 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1625 
1626 template<typename InputIterator>
1627 std::vector<Ptr>
1628 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1629  typedef Sawyer::Container::Map<Ptr, size_t> NodeCounts;
1630  struct T1: Visitor {
1631  NodeCounts nodeCounts;
1632  std::vector<Ptr> result;
1633 
1634  VisitAction preVisit(const Ptr &node) ROSE_OVERRIDE {
1635  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1636  if (2 == ++nSeen)
1637  result.push_back(node);
1638  return nSeen>1 ? TRUNCATE : CONTINUE;
1639  }
1640 
1641  VisitAction postVisit(const Ptr&) ROSE_OVERRIDE {
1642  return CONTINUE;
1643  }
1644  } visitor;
1645 
1646  for (InputIterator ii=begin; ii!=end; ++ii)
1647  (*ii)->depthFirstTraversal(visitor);
1648  return visitor.result;
1649 }
1659 template<class Substitution>
1660 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1661  if (!src)
1662  return Ptr(); // no input implies no output
1663 
1664  // Try substituting the whole expression, returning the result.
1665  Ptr dst = subber(src, solver);
1666  ASSERT_not_null(dst);
1667  if (dst != src)
1668  return dst;
1669 
1670  // Try substituting all the subexpressions.
1671  InteriorPtr inode = src->isInteriorNode();
1672  if (!inode)
1673  return src;
1674  bool anyChildChanged = false;
1675  Nodes newChildren;
1676  newChildren.reserve(inode->nChildren());
1677  BOOST_FOREACH (const Ptr &child, inode->children()) {
1678  Ptr newChild = substitute(child, subber, solver);
1679  if (newChild != child)
1680  anyChildChanged = true;
1681  newChildren.push_back(newChild);
1682  }
1683  if (!anyChildChanged)
1684  return src;
1685 
1686  // Some subexpression changed, so build a new expression
1687  return Interior::instance(inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1688 }
1689 
1690 } // namespace
1691 } // namespace
1692 } // namespace
1693 
1694 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1695 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1696 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1697 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Node, 1);
1698 #endif
1699 
1700 #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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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.
Ptr makeReinterpret(const Ptr &a, const Type &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
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.
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.
bool isScalarVariable() const
True if this expression is a scalar variable.
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.
bool isScalarExpr() const
True if the expression is a scalar type.
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.
Interpret the value as a different type without converting.
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.
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.
Flag
Flag to pass as type stringification style.
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 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 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?
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.
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.
bool isScalarConstant() const
True if this expression is a scalar constant.
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 adjustWidth(const Type &)
Adjust width based on operands.
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
bool show_type
Show data type inside square brackets.
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.
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.