ROSE  0.10.0.0
BinarySymbolicExpr.h
1 #ifndef ROSE_BinaryAnalysis_SymbolicExpr_H
2 #define ROSE_BinaryAnalysis_SymbolicExpr_H
3 #include <rosePublicConfig.h>
4 #ifdef ROSE_BUILD_BINARY_ANALYSIS_SUPPORT
5 
6 #ifndef __STDC_FORMAT_MACROS
7 #define __STDC_FORMAT_MACROS
8 #endif
9 
10 #include "Map.h"
11 
12 #include <boost/any.hpp>
13 #include <boost/lexical_cast.hpp>
14 #include <boost/logic/tribool.hpp>
15 #include <boost/serialization/access.hpp>
16 #include <boost/serialization/base_object.hpp>
17 #include <boost/serialization/export.hpp>
18 #include <boost/serialization/split_member.hpp>
19 #include <boost/serialization/string.hpp>
20 #include <boost/serialization/vector.hpp>
21 #include <boost/unordered_map.hpp>
22 #include <cassert>
23 #include <inttypes.h>
24 #include <RoseException.h>
25 #include <Sawyer/Attribute.h>
26 #include <Sawyer/BitVector.h>
27 #include <Sawyer/Optional.h>
28 #include <Sawyer/Set.h>
29 #include <Sawyer/SharedPointer.h>
30 #include <Sawyer/SmallObject.h>
31 #include <set>
32 #include <string>
33 #include <vector>
34 
35 namespace Rose {
36 namespace BinaryAnalysis {
37 
38 class SmtSolver;
40 
46 namespace SymbolicExpr {
47 
49 // Basic Types
51 
53 namespace TypeStyle {
55  enum Flag {
56  FULL,
58  };
59 }
60 
61 
63 class Exception: public Rose::Exception {
64 public:
65  explicit Exception(const std::string &mesg): Rose::Exception(mesg) {}
66 };
67 
73 enum Operator {
146  OP_BV_AND = OP_AND, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
147  OP_BV_OR = OP_OR, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
148  OP_BV_XOR = OP_XOR // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
149 };
150 
151 std::string toStr(Operator);
152 
153 class Node;
154 class Interior;
155 class Leaf;
157 
160 
163 
166 
167 typedef std::vector<Ptr> Nodes;
169 
171 typedef uint64_t Hash;
172 
174 struct Formatter {
179  };
180  Formatter()
182  max_depth(0), cur_depth(0), show_type(true), show_flags(true) {}
184  bool do_rename;
185  bool add_renames;
187  size_t max_depth;
188  size_t cur_depth;
189  RenameMap renames;
190  bool show_type;
191  bool show_flags;
192 };
193 
199 };
200 
205 extern const uint64_t MAX_NNODES; // defined in .C so we don't pollute user namespace with limit macros
206 
211 class Visitor {
212 public:
213  virtual ~Visitor() {}
214  virtual VisitAction preVisit(const Ptr&) = 0;
215  virtual VisitAction postVisit(const Ptr&) = 0;
216 };
217 
218 
219 
221 // Expression type information
223 
225 class Type {
226 public:
228  enum TypeClass {
230  FP,
233  };
234 
235 private:
236  // We use a 32-bit data member and pack into it the totalWidth (15 bits: 0 through 14), the secondaryWidth (15 bits: 15 through 29),
237  // and the type class (2 bits: 30 and 31).
238  uint32_t fields_;
239 
240 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
241 private:
242  friend class boost::serialization::access;
243 
244  template<class S>
245  void serialize(S &s, const unsigned version) {
246  if (version >= 1) {
247  s & BOOST_SERIALIZATION_NVP(fields_);
248  } else {
249  TypeClass t = typeClass();
250  size_t z1 = nBits();
251  size_t z2 = secondaryWidth();
252  s & boost::serialization::make_nvp("typeClass_", t);
253  s & boost::serialization::make_nvp("totalWidth_", z1);
254  s & boost::serialization::make_nvp("secondaryWidth_", z2);
255  typeClass(t);
256  nBits(z1);
257  secondaryWidth(z2);
258  }
259  }
260 #endif
261 
265 public:
266  Type() {
268  nBits(0);
269  secondaryWidth(0);
270  }
271 
272 private:
273  Type(TypeClass tc, size_t w1, size_t w2) {
274  typeClass(tc);
275  nBits(w1);
276  secondaryWidth(w2);
277  }
278 
279 public:
283  static Type none() {
284  return Type();
285  }
286 
292  static Type integer(size_t nBits) {
293  return Type(INTEGER, nBits, 0);
294  }
295 
299  static Type memory(size_t addressWidth, size_t valueWidth) {
300  return Type(MEMORY, valueWidth, addressWidth);
301  }
302 
312  return Type(FP, 1 /*sign bit*/ + exponentWidth + significandWidth - 1 /*implied bit*/, exponentWidth);
313  }
314 
318  bool isValid() const {
319  return typeClass() != INVALID;
320  }
321 
326  return (TypeClass)((fields_ >> 30) & 0x3);
327  }
328 
333  size_t nBits() const {
334  return fields_ & 0x7fff;
335  }
336 
341  size_t addressWidth() const {
342  ASSERT_require(MEMORY == typeClass());
343  return secondaryWidth();
344  }
345 
350  size_t exponentWidth() const {
351  ASSERT_require(FP == typeClass());
352  return secondaryWidth();
353  }
354 
360  size_t significandWidth() const {
361  ASSERT_require(FP == typeClass());
362  ASSERT_require(nBits() > 1 /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
363  return nBits() - (1 /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
364  }
365 
371  bool operator==(const Type &other) const {
372  return fields_ == other.fields_;
373  }
374  bool operator!=(const Type &other) const {
375  return !(*this == other);
376  }
380  bool operator<(const Type &other) const;
381 
383  void print(std::ostream&, TypeStyle::Flag style = TypeStyle::FULL) const;
384 
386  std::string toString(TypeStyle::Flag style = TypeStyle::FULL) const;
387 
388 private:
389  // mutators are all private
390  void typeClass(TypeClass tc) {
391  unsigned n = tc;
392  ASSERT_require(n <= 3);
393  fields_ = (fields_ & 0x3fffffff) | (n << 30);
394  }
395 
396  // mutators are all private
397  void nBits(size_t n) {
398  if (n > 0x7fff)
399  throw Exception("type width is out of range");
400  fields_ = (fields_ & 0xffff8000) | n;
401  }
402 
403  // mutators are all private
404  void secondaryWidth(size_t n) {
405  if (n > 0x7fff)
406  throw Exception("second width is out of range");
407  fields_ = (fields_ & 0xc0007fff) | (n << 15);
408  }
409 
410  size_t secondaryWidth() const {
411  return (fields_ >> 15) & 0x7fff;
412  }
413 };
414 
415 
416 
417 
418 
420 // Base Node Type
422 
460 class Node
461  : public Sawyer::SharedObject,
462  public Sawyer::SharedFromThis<Node>,
463  public Sawyer::SmallObject,
464  public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
465 protected:
466  Type type_;
467  unsigned flags_;
468  std::string comment_;
469  Hash hashval_;
470  boost::any userData_;
472 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
473 private:
474  friend class boost::serialization::access;
475 
476  template<class S>
477  void serialize(S &s, const unsigned version) {
478  if (version < 1)
479  ASSERT_not_reachable("SymbolicExpr version " + boost::lexical_cast<std::string>(version) + " is no longer supported");
480  s & BOOST_SERIALIZATION_NVP(type_);
481  s & BOOST_SERIALIZATION_NVP(flags_);
482  s & BOOST_SERIALIZATION_NVP(comment_);
483  s & BOOST_SERIALIZATION_NVP(hashval_);
484  // s & userData_;
485  }
486 #endif
487 
488 public:
489  // Bit flags
490 
492  static const unsigned RESERVED_FLAGS = 0x0000ffff;
493 
495  static const unsigned INDETERMINATE = 0x00000001;
496 
501  static const unsigned UNSPECIFIED = 0x00000002;
502 
505  static const unsigned BOTTOM = 0x00000004;
506 
507 protected:
508  Node()
509  : type_(Type::integer(0)), flags_(0), hashval_(0) {}
510  explicit Node(const std::string &comment, unsigned flags=0)
511  : type_(Type::integer(0)), flags_(flags), comment_(comment), hashval_(0) {}
512 
513 public:
515  Type type() const {
516  return type_;
517  }
518 
525  static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
526 
532  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
533 
535  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
536 
542  virtual bool isEquivalentTo(const Ptr &other) = 0;
543 
549  virtual int compareStructure(const Ptr &other) = 0;
550 
556  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
557 
565  Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
566 
574  Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
575  const SmtSolverPtr &solver = SmtSolverPtr());
576 
580  virtual Operator getOperator() const = 0;
581 
585  virtual size_t nChildren() const = 0;
586 
591  virtual Ptr child(size_t idx) const = 0;
592 
596  virtual const Nodes& children() const = 0;
597 
602  virtual Sawyer::Optional<uint64_t> toUnsigned() const = 0;
603 
607  virtual Sawyer::Optional<int64_t> toSigned() const = 0;
608 
610  bool isIntegerExpr() const {
611  return type_.typeClass() == Type::INTEGER;
612  }
613 
615  bool isFloatingPointExpr() const {
616  return type_.typeClass() == Type::FP;
617  }
618 
620  bool isMemoryExpr() const {
621  return type_.typeClass() == Type::MEMORY;
622  }
623 
627  bool isScalarExpr() const {
628  return isIntegerExpr() || isFloatingPointExpr();
629  }
630 
632  virtual bool isConstant() const = 0;
633 
635  bool isIntegerConstant() const {
636  return isIntegerExpr() && isConstant();
637  }
638 
640  bool isFloatingPointConstant() const {
641  return isFloatingPointExpr() && isConstant();
642  }
643 
647  bool isScalarConstant() const {
649  }
650 
652  bool isFloatingPointNan() const;
653 
659  virtual bool isVariable2() const = 0;
660 
665 
667  bool isIntegerVariable() const {
668  return isIntegerExpr() && isVariable2();
669  }
670 
672  bool isFloatingPointVariable() const {
673  return isFloatingPointExpr() && isVariable2();
674  }
675 
677  bool isMemoryVariable() const {
678  return isMemoryExpr() && isVariable2();
679  }
680 
684  bool isScalarVariable() const {
686  }
687 
696  const std::string& comment() const {
697  return comment_;
698  }
699  void comment(const std::string &s) {
700  comment_ = s;
701  }
711  void userData(boost::any &data) {
712  userData_ = data;
713  }
714  const boost::any& userData() const {
715  return userData_;
716  }
722  size_t nBits() const {
723  return type_.nBits();
724  }
725 
730  unsigned flags() const {
731  return flags_;
732  }
733 
737  Ptr newFlags(unsigned flags) const;
738 
742  size_t domainWidth() const {
743  return type_.addressWidth();
744  }
745 
749  bool isScalar() const {
750  return type_.typeClass() != Type::MEMORY;
751  }
752 
757  virtual VisitAction depthFirstTraversal(Visitor&) const = 0;
758 
774  virtual uint64_t nNodes() const = 0;
775 
777  uint64_t nNodesUnique() const;
778 
780  std::set<LeafPtr> getVariables() const;
781 
785  InteriorPtr isInteriorNode() const;
786 
790  LeafPtr isLeafNode() const;
791 
795  bool isHashed() const {
796  return hashval_ != 0;
797  }
798 
801  Hash hash() const;
802 
803  // used internally to set the hash value
804  void hash(Hash);
805 
808  private:
809  Ptr node;
810  Formatter &formatter;
811  public:
812  WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
813  void print(std::ostream &stream) const { node->print(stream, formatter); }
814  };
815 
837  virtual void print(std::ostream&, Formatter&) const = 0;
838  void print(std::ostream &o) const { Formatter fmt; print(o, fmt); }
842  void assertAcyclic() const;
843 
849  std::vector<Ptr> findCommonSubexpressions() const;
850 
856  bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/) const;
857 
859  InteriorPtr isOperator(Operator) const;
860 
861 protected:
862  void printFlags(std::ostream &o, unsigned flags, char &bracket) const;
863 
864 public:
865  // Deprecated [Robb Matzke 2019-09-27]
866  bool isNumber() const ROSE_DEPRECATED("use isIntegerConstant instead") {
867  return isIntegerConstant();
868  }
869 
870  // Deprecated [Robb Matzke 2019-09-27]
871  uint64_t toInt() ROSE_DEPRECATED("use toUnsigned() instead") {
872  return toUnsigned().get();
873  }
874 };
875 
877 class Simplifier {
878 public:
879  virtual ~Simplifier() {}
880 
884  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
885  return Ptr();
886  }
887 
890  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
891  return Ptr();
892  }
893 };
894 
896  size_t operator()(const Ptr &expr) const {
897  return expr->hash();
898  }
899 };
900 
902  bool operator()(const Ptr &a, const Ptr &b) const {
903  return a->isEquivalentTo(b);
904  }
905 };
906 
909 public:
910  bool operator()(const Ptr &a, const Ptr &b);
911 };
912 
914 class ExprExprHashMap: public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
915  ExprExprHashMapHasher, ExprExprHashMapCompare> {
916 public:
917  ExprExprHashMap invert() const;
918 };
919 
922 
923 
925 // Simplification
927 
929  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
930  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
931 };
933  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
934  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
935 };
937  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
938 };
940  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
941  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
942 };
944  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
945  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
946 };
948  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
949 };
951  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
952 };
954  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
955  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
956 };
958  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
959 };
961  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
962 };
964  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
965 };
967  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
968 };
970  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
971 };
973  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
974 };
976  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
977 };
979  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
980 };
982  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
983 };
985  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
986 };
988  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
989 };
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 };
1003  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1004 };
1006  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1007 };
1009  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1010 };
1012  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1013 };
1015  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1016 };
1018  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1019 };
1021  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1022 };
1024  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1025 };
1027  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1028 };
1030  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1031 };
1033  bool newbits;
1034  ShiftSimplifier(bool newbits): newbits(newbits) {}
1035  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
1036 };
1038  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1039  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1040 };
1042  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1043  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1044 };
1046  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1047 };
1049  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1050 };
1052  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1053 };
1054 
1055 
1056 
1058 // Interior Nodes
1060 
1067 class Interior: public Node {
1068 private:
1069  Operator op_;
1070  Nodes children_;
1071  uint64_t nnodes_; // total number of nodes; self + children's nnodes
1072 
1073  //--------------------------------------------------------
1074  // Serialization
1075  //--------------------------------------------------------
1076 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1077 private:
1078  friend class boost::serialization::access;
1079 
1080  template<class S>
1081  void serialize(S &s, const unsigned /*version*/) {
1082  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1083  s & BOOST_SERIALIZATION_NVP(op_);
1084  s & BOOST_SERIALIZATION_NVP(children_);
1085  s & BOOST_SERIALIZATION_NVP(nnodes_);
1086  }
1087 #endif
1088 
1089  //--------------------------------------------------------
1090  // Real constructors
1091  //--------------------------------------------------------
1092 private:
1093  Interior(); // needed for serialization
1094  // Only constructs, does not simplify.
1095  Interior(const Type&, Operator, const Nodes &arguments, const std::string &comment, unsigned flags);
1096 
1097  //--------------------------------------------------------
1098  // Allocating constructors
1099  //--------------------------------------------------------
1100 public:
1104  static Ptr instance(Operator op, const Ptr &a,
1105  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1106  static Ptr instance(const Type &type, Operator op, const Ptr &a,
1107  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1108  static Ptr instance(Operator op, const Ptr &a, const Ptr &b,
1109  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1110  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b,
1111  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1112  static Ptr instance(Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1113  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1114  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1115  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1116  static Ptr instance(Operator op, const Nodes &arguments,
1117  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1118  static Ptr instance(const Type &type, Operator op, const Nodes &arguments,
1119  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1122  //--------------------------------------------------------
1123  // Overrides
1124  //--------------------------------------------------------
1125 public:
1126  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1127  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1128  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1129  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1130  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1131  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1132  virtual uint64_t nNodes() const ROSE_OVERRIDE { return nnodes_; }
1133  virtual const Nodes& children() const ROSE_OVERRIDE { return children_; }
1134  virtual Operator getOperator() const ROSE_OVERRIDE { return op_; }
1135  virtual size_t nChildren() const ROSE_OVERRIDE { return children_.size(); }
1136  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return idx < children_.size() ? children_[idx] : Ptr(); }
1137  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1138  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1139  virtual bool isConstant() const ROSE_OVERRIDE { return false; }
1140  virtual bool isVariable2() const ROSE_OVERRIDE { return false; }
1141 
1142  //--------------------------------------------------------
1143  // Simplification
1144  //--------------------------------------------------------
1145 public:
1149  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
1150 
1153  Ptr foldConstants(const Simplifier&);
1154 
1159  InteriorPtr associative();
1160 
1165  InteriorPtr commutative();
1166 
1173  InteriorPtr idempotent(const SmtSolverPtr &solver = SmtSolverPtr());
1174 
1178  Ptr involutary();
1179 
1183  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
1184 
1188  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
1189 
1194  Ptr poisonNan(const SmtSolverPtr &solver = SmtSolverPtr());
1195 
1197  Ptr unaryNoOp();
1198 
1202  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
1203 
1204  //--------------------------------------------------------
1205  // Functions specific to internal nodes
1206  //--------------------------------------------------------
1207 public:
1208  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1209 
1210 protected:
1212  void addChild(const Ptr &child);
1213 
1217  void adjustWidth(const Type&);
1218 
1221  void adjustBitFlags(unsigned extraFlags);
1222 
1223  //--------------------------------------------------------
1224  // Deprecated [Robb Matzke 2019-10-01]
1225  //--------------------------------------------------------
1226 public:
1227  static Ptr create(size_t nbits, Operator op, const Ptr &a,
1228  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1229  ROSE_DEPRECATED("use instance instead");
1230  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b,
1231  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1232  ROSE_DEPRECATED("use instance instead");
1233  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1234  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1235  ROSE_DEPRECATED("use instance instead");
1236  static Ptr create(size_t nbits, Operator op, const Nodes &children,
1237  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1238  ROSE_DEPRECATED("use instance instead");
1239 
1240 };
1241 
1242 
1244 // Leaf Nodes
1246 
1250 class Leaf: public Node {
1251 private:
1252  Sawyer::Container::BitVector bits_; // Value for constants if size > 0
1253  uint64_t name_; // Variable ID for variables when bits_.size() == 0
1254 
1255  //--------------------------------------------------------
1256  // Serialization
1257  //--------------------------------------------------------
1258 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1259 private:
1260  friend class boost::serialization::access;
1261 
1262  template<class S>
1263  void save(S &s, const unsigned /*version*/) const {
1264  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1265  s & BOOST_SERIALIZATION_NVP(bits_);
1266  s & BOOST_SERIALIZATION_NVP(name_);
1267  }
1268 
1269  template<class S>
1270  void load(S &s, const unsigned /*version*/) {
1271  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1272  s & BOOST_SERIALIZATION_NVP(bits_);
1273  s & BOOST_SERIALIZATION_NVP(name_);
1274  nextNameCounter(name_);
1275  }
1276 
1277  BOOST_SERIALIZATION_SPLIT_MEMBER();
1278 #endif
1279 
1280  //--------------------------------------------------------
1281  // Private constructors. Use create methods instead.
1282  //--------------------------------------------------------
1283 private:
1284  Leaf()
1285  : name_(0) {}
1286  explicit Leaf(const std::string &comment, unsigned flags=0)
1287  : Node(comment, flags), name_(0) {}
1288 
1289  // Allocating constructors.
1290 public:
1292  static LeafPtr createVariable(const Type&,
1293  const std::string &comment = "", unsigned flags = 0);
1294 
1296  static LeafPtr createVariable(const Type&, const uint64_t id,
1297  const std::string &comment = "", unsigned flags = 0);
1298 
1300  static LeafPtr createConstant(const Type&, const Sawyer::Container::BitVector&,
1301  const std::string &comment = "", unsigned flags = 0);
1302 
1303  //--------------------------------------------------------
1304  // Override base class implementations
1305  //--------------------------------------------------------
1306 public:
1307  virtual size_t nChildren() const ROSE_OVERRIDE { return 0; }
1308  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return Ptr(); }
1309  virtual const Nodes& children() const ROSE_OVERRIDE;
1310  virtual Operator getOperator() const ROSE_OVERRIDE { return OP_NONE; }
1311  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1312  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1313  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1314  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1315  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1316  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1317  virtual uint64_t nNodes() const ROSE_OVERRIDE { return 1; }
1318  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE;
1319  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE;
1320  virtual bool isConstant() const ROSE_OVERRIDE { return !bits_.isEmpty(); }
1321  virtual bool isVariable2() const ROSE_OVERRIDE { return !isConstant(); }
1322  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1323 
1324  //--------------------------------------------------------
1325  // Leaf-specific methods
1326  //--------------------------------------------------------
1327 public:
1329  const Sawyer::Container::BitVector& bits() const;
1330 
1332  bool isIntegerVariable() const {
1333  return type().typeClass() == Type::INTEGER && !isConstant();
1334  }
1335 
1338  return type().typeClass() == Type::FP && !isConstant();
1339  }
1340 
1342  bool isFloatingPointNan() const;
1343 
1345  bool isMemoryVariable() const {
1346  return type().typeClass() == Type::MEMORY && !isConstant();
1347  }
1348 
1353  uint64_t nameId() const;
1354 
1359  std::string toString() const;
1360 
1362  void printAsSigned(std::ostream&, Formatter&, bool asSigned = true) const;
1363 
1365  void printAsUnsigned(std::ostream &o, Formatter &f) const {
1366  printAsSigned(o, f, false);
1367  }
1368 
1369 private:
1370  // Obtain or register a name ID
1371  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1372 
1373  // Deprecated functions
1374 public:
1375  // Deprecated [Robb Matzke 2019-09-27]
1376  static LeafPtr createVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
1377  ROSE_DEPRECATED("use createVariable with type or makeIntegerVariable, etc.") {
1378  return createVariable(Type::integer(nBits), comment, flags);
1379  }
1380 
1381  // Deprecated [Robb Matzke 2019-09-27]
1382  static LeafPtr createExistingVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0)
1383  ROSE_DEPRECATED("use createVariable or makeIntegerVariable, etc.") {
1384  return createVariable(Type::integer(nBits), id, comment, flags);
1385  }
1386 
1387  // Deprecated [Robb Matzke 2019-09-27]
1388  static LeafPtr createInteger(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
1389  ROSE_DEPRECATED("use createConstant or makeIntegerConstant, etc.");
1390 
1391  // Deprecated [Robb Matzke 2019-09-27]
1392  static LeafPtr createConstant(const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0)
1393  ROSE_DEPRECATED("use createConstant with type or makeIntegerConstant, etc.") {
1394  return createConstant(Type::integer(bits.size()), bits, comment, flags);
1395  }
1396 
1397  // Deprecated [Robb Matzke 2019-09-27]
1398  static LeafPtr createBoolean(bool b, const std::string &comment="", unsigned flags=0)
1399  ROSE_DEPRECATED("use createConstant or makeBooleanConstant");
1400 
1401  // Deprecated [Robb Matzke 2019-09-27]
1402  static LeafPtr createMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
1403  ROSE_DEPRECATED("use createVariable with type or makeMemoryVariable") {
1404  return createVariable(Type::memory(addressWidth, valueWidth), comment, flags);
1405  }
1406 
1407  // Deprecated [Robb Matzke 2019-09-27]
1408  static LeafPtr createExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="",
1409  unsigned flags=0)
1410  ROSE_DEPRECATED("use createVariable with type or makeMemoryVariable") {
1411  return createVariable(Type::memory(addressWidth, valueWidth), id, comment, flags);
1412  }
1413 
1414  // Deprecated [Robb Matzke 2019-09-27]. The definition will eventually change to isVariable2()
1415  bool isVariable() const ROSE_DEPRECATED("use isIntegerVariable or isVariable2 instead") {
1416  return isIntegerVariable();
1417  }
1418 
1419  // Deprecated [Robb Matzke 2019-09-27]
1420  virtual bool isMemory() ROSE_DEPRECATED("use isMemoryVariable or isMemoryExpr instead") {
1421  return isMemoryVariable();
1422  }
1423 };
1424 
1426 // Factories
1428 
1434 LeafPtr makeVariable(const Type&, const std::string &comment="", unsigned flags=0);
1435 LeafPtr makeVariable(const Type&, uint64_t id, const std::string &comment="", unsigned flags=0);
1436 LeafPtr makeConstant(const Type&, const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1437 LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0);
1438 LeafPtr makeIntegerVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0);
1439 LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0);
1440 LeafPtr makeIntegerConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1441 LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0);
1442 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1443 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
1444 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1445 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, uint64_t id, const std::string &comment="", unsigned flags=0);
1446 LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0);
1447 LeafPtr makeFloatingPointConstant(double, const std::string &comment="", unsigned flags=0);
1448 LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1451 // Deprecated [Robb Matzke 2019-09-27]
1452 Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0)
1453  ROSE_DEPRECATED("use makeIntegerVariable instead");
1454 Ptr makeExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0)
1455  ROSE_DEPRECATED("use makeIntegerVariable instead");
1456 Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0)
1457  ROSE_DEPRECATED("use makeIntegerConstant instead");
1458 Ptr makeConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0)
1459  ROSE_DEPRECATED("use makeIntegerConstant instead");
1460 Ptr makeBoolean(bool, const std::string &comment="", unsigned flags=0)
1461  ROSE_DEPRECATED("use makeBooleanConstant instead");
1462 Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
1463  ROSE_DEPRECATED("use makeMemoryVariable instead");
1464 Ptr makeExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0)
1465  ROSE_DEPRECATED("use makeMemoryVariable instead");
1466 
1473 Ptr makeAdd(const Ptr&a, const Ptr &b,
1474  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1475 Ptr makeBooleanAnd(const Ptr &a, const Ptr &b,
1476  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1477  ROSE_DEPRECATED("use makeAnd instead"); // [Robb Matzke 2017-11-21]: deprecated
1478 Ptr makeAsr(const Ptr &sa, const Ptr &a,
1479  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1480 Ptr makeAnd(const Ptr &a, const Ptr &b,
1481  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1482 Ptr makeOr(const Ptr &a, const Ptr &b,
1483  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1484 Ptr makeXor(const Ptr &a, const Ptr &b,
1485  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1486 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1487  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1488 Ptr makeConvert(const Ptr &a, const Type &b,
1489  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1490 Ptr makeEq(const Ptr &a, const Ptr &b,
1491  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1492 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1493  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1494 Ptr makeInvert(const Ptr &a,
1495  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1496 Ptr makeIsInfinite(const Ptr &a,
1497  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1498 Ptr makeIsNan(const Ptr &a,
1499  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1500 Ptr makeIsNeg(const Ptr &a,
1501  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1502 Ptr makeIsNorm(const Ptr &a,
1503  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1504 Ptr makeIsPos(const Ptr &a,
1505  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1506 Ptr makeIsSubnorm(const Ptr &a,
1507  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1508 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1509  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1510 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1511  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1512 Ptr makeLssb(const Ptr &a,
1513  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1514 Ptr makeMax(const Ptr &a, const Ptr &b,
1515  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1516 Ptr makeMin(const Ptr &a, const Ptr &b,
1517  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1518 Ptr makeMssb(const Ptr &a,
1519  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1520 Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c,
1521  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1522 Ptr makeNe(const Ptr &a, const Ptr &b,
1523  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1524 Ptr makeNegate(const Ptr &a,
1525  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1526 Ptr makeBooleanOr(const Ptr &a, const Ptr &b,
1527  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1528  ROSE_DEPRECATED("use makeOr instead"); // [Robb Matzke 2017-11-21]: deprecated
1529 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1530  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1531 Ptr makeReinterpret(const Ptr &a, const Type &b,
1532  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1533 Ptr makeRol(const Ptr &sa, const Ptr &a,
1534  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1535 Ptr makeRor(const Ptr &sa, const Ptr &a,
1536  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1537 Ptr makeRound(const Ptr &a,
1538  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1539 Ptr makeSet(const Ptr &a, const Ptr &b,
1540  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1541 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1542  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1543 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1544  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1545 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1546  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1547 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1548  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1549 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1550  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1551 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1552  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1553 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1554  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1555 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1556  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1557 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1558  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1559 Ptr makeIsSignedPos(const Ptr &a,
1560  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1561 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1562  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1563 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1564  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1565 Ptr makeSignedMax(const Ptr &a, const Ptr &b,
1566  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1567 Ptr makeSignedMin(const Ptr &a, const Ptr &b,
1568  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1569 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1570  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1571 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1572  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1573 Ptr makeSqrt(const Ptr &a,
1574  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1575 Ptr makeDiv(const Ptr &a, const Ptr &b,
1576  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1577 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1578  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1579 Ptr makeGe(const Ptr &a, const Ptr &b,
1580  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1581 Ptr makeGt(const Ptr &a, const Ptr &b,
1582  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1583 Ptr makeLe(const Ptr &a, const Ptr &b,
1584  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1585 Ptr makeLt(const Ptr &a, const Ptr &b,
1586  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1587 Ptr makeMod(const Ptr &a, const Ptr &b,
1588  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1589 Ptr makeMul(const Ptr &a, const Ptr &b,
1590  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1591 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1592  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1593 Ptr makeZerop(const Ptr &a,
1594  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1598 // Miscellaneous functions
1601 
1602 
1603 std::ostream& operator<<(std::ostream &o, Node&);
1604 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1605 
1607 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1608 
1613 Hash hash(const std::vector<Ptr>&);
1614 
1619 template<typename InputIterator>
1620 uint64_t
1621 nNodes(InputIterator begin, InputIterator end) {
1622  uint64_t total = 0;
1623  for (InputIterator ii=begin; ii!=end; ++ii) {
1624  uint64_t n = (*ii)->nnodes();
1625  if (MAX_NNODES==n)
1626  return MAX_NNODES;
1627  if (total + n < total)
1628  return MAX_NNODES;
1629  total += n;
1630  }
1631  return total;
1632 }
1633 
1638 template<typename InputIterator>
1639 uint64_t
1640 nNodesUnique(InputIterator begin, InputIterator end)
1641 {
1642  struct T1: Visitor {
1643  typedef std::set<const Node*> SeenNodes;
1644 
1645  SeenNodes seen; // nodes that we've already seen, and the subtree size
1646  uint64_t nUnique; // number of unique nodes
1647 
1648  T1(): nUnique(0) {}
1649 
1650  VisitAction preVisit(const Ptr &node) {
1651  if (seen.insert(getRawPointer(node)).second) {
1652  ++nUnique;
1653  return CONTINUE; // this node has not been seen before; traverse into children
1654  } else {
1655  return TRUNCATE; // this node has been seen already; skip over the children
1656  }
1657  }
1658 
1659  VisitAction postVisit(const Ptr &node) {
1660  return CONTINUE;
1661  }
1662  } visitor;
1663 
1664  VisitAction status = CONTINUE;
1665  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1666  status = (*ii)->depthFirstTraversal(visitor);
1667  return visitor.nUnique;
1668 }
1669 
1676 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1677 
1678 template<typename InputIterator>
1679 std::vector<Ptr>
1680 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1681  typedef Sawyer::Container::Map<Ptr, size_t> NodeCounts;
1682  struct T1: Visitor {
1683  NodeCounts nodeCounts;
1684  std::vector<Ptr> result;
1685 
1686  VisitAction preVisit(const Ptr &node) ROSE_OVERRIDE {
1687  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1688  if (2 == ++nSeen)
1689  result.push_back(node);
1690  return nSeen>1 ? TRUNCATE : CONTINUE;
1691  }
1692 
1693  VisitAction postVisit(const Ptr&) ROSE_OVERRIDE {
1694  return CONTINUE;
1695  }
1696  } visitor;
1697 
1698  for (InputIterator ii=begin; ii!=end; ++ii)
1699  (*ii)->depthFirstTraversal(visitor);
1700  return visitor.result;
1701 }
1711 template<class Substitution>
1712 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1713  if (!src)
1714  return Ptr(); // no input implies no output
1715 
1716  // Try substituting the whole expression, returning the result.
1717  Ptr dst = subber(src, solver);
1718  ASSERT_not_null(dst);
1719  if (dst != src)
1720  return dst;
1721 
1722  // Try substituting all the subexpressions.
1723  InteriorPtr inode = src->isInteriorNode();
1724  if (!inode)
1725  return src;
1726  bool anyChildChanged = false;
1727  Nodes newChildren;
1728  newChildren.reserve(inode->nChildren());
1729  BOOST_FOREACH (const Ptr &child, inode->children()) {
1730  Ptr newChild = substitute(child, subber, solver);
1731  if (newChild != child)
1732  anyChildChanged = true;
1733  newChildren.push_back(newChild);
1734  }
1735  if (!anyChildChanged)
1736  return src;
1737 
1738  // Some subexpression changed, so build a new expression
1739  return Interior::instance(inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1740 }
1741 
1742 } // namespace
1743 } // namespace
1744 } // namespace
1745 
1746 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1747 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1748 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1749 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Type, 1);
1750 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Node, 1);
1751 #endif
1752 
1753 #endif
1754 #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?
Sawyer::Optional< uint64_t > variableId() const
Variable ID number.
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.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
const boost::any & userData() const
Property: User-defined data.
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.
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.