ROSE  0.10.12.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:
267  : fields_(0) {
269  nBits(0);
270  secondaryWidth(0);
271  }
272 
273 private:
274  Type(TypeClass tc, size_t w1, size_t w2)
275  : fields_(0) {
276  typeClass(tc);
277  nBits(w1);
278  secondaryWidth(w2);
279  }
280 
281 public:
285  static Type none() {
286  return Type();
287  }
288 
294  static Type integer(size_t nBits) {
295  return Type(INTEGER, nBits, 0);
296  }
297 
301  static Type memory(size_t addressWidth, size_t valueWidth) {
302  return Type(MEMORY, valueWidth, addressWidth);
303  }
304 
314  return Type(FP, 1 /*sign bit*/ + exponentWidth + significandWidth - 1 /*implied bit*/, exponentWidth);
315  }
316 
320  bool isValid() const {
321  return typeClass() != INVALID;
322  }
323 
328  return (TypeClass)((fields_ >> 30) & 0x3);
329  }
330 
335  size_t nBits() const {
336  return fields_ & 0x7fff;
337  }
338 
343  size_t addressWidth() const {
344  ASSERT_require(MEMORY == typeClass());
345  return secondaryWidth();
346  }
347 
352  size_t exponentWidth() const {
353  ASSERT_require(FP == typeClass());
354  return secondaryWidth();
355  }
356 
362  size_t significandWidth() const {
363  ASSERT_require(FP == typeClass());
364  ASSERT_require(nBits() > 1 /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
365  return nBits() - (1 /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
366  }
367 
373  bool operator==(const Type &other) const {
374  return fields_ == other.fields_;
375  }
376  bool operator!=(const Type &other) const {
377  return !(*this == other);
378  }
382  bool operator<(const Type &other) const;
383 
385  void print(std::ostream&, TypeStyle::Flag style = TypeStyle::FULL) const;
386 
388  std::string toString(TypeStyle::Flag style = TypeStyle::FULL) const;
389 
390 private:
391  // mutators are all private
392  void typeClass(TypeClass tc) {
393  unsigned n = tc;
394  ASSERT_require(n <= 3);
395  fields_ = (fields_ & 0x3fffffff) | (n << 30);
396  }
397 
398  // mutators are all private
399  void nBits(size_t n) {
400  if (n > 0x7fff)
401  throw Exception("type width is out of range");
402  fields_ = (fields_ & 0xffff8000) | n;
403  }
404 
405  // mutators are all private
406  void secondaryWidth(size_t n) {
407  if (n > 0x7fff)
408  throw Exception("second width is out of range");
409  fields_ = (fields_ & 0xc0007fff) | (n << 15);
410  }
411 
412  size_t secondaryWidth() const {
413  return (fields_ >> 15) & 0x7fff;
414  }
415 };
416 
417 
418 
419 
420 
422 // Base Node Type
424 
462 class Node
463  : public Sawyer::SharedObject,
464  public Sawyer::SharedFromThis<Node>,
465  public Sawyer::SmallObject,
466  public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
467 protected:
468  Type type_;
469  unsigned flags_;
470  std::string comment_;
471  Hash hashval_;
472  boost::any userData_;
474 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
475 private:
476  friend class boost::serialization::access;
477 
478  template<class S>
479  void serialize(S &s, const unsigned version) {
480  if (version < 1)
481  ASSERT_not_reachable("SymbolicExpr version " + boost::lexical_cast<std::string>(version) + " is no longer supported");
482  s & BOOST_SERIALIZATION_NVP(type_);
483  s & BOOST_SERIALIZATION_NVP(flags_);
484  s & BOOST_SERIALIZATION_NVP(comment_);
485  s & BOOST_SERIALIZATION_NVP(hashval_);
486  // s & userData_;
487  }
488 #endif
489 
490 public:
491  // Bit flags
492 
494  static const unsigned RESERVED_FLAGS = 0x0000ffff;
495 
497  static const unsigned INDETERMINATE = 0x00000001;
498 
503  static const unsigned UNSPECIFIED = 0x00000002;
504 
507  static const unsigned BOTTOM = 0x00000004;
508 
509 protected:
510  Node()
511  : type_(Type::integer(0)), flags_(0), hashval_(0) {}
512  explicit Node(const std::string &comment, unsigned flags=0)
513  : type_(Type::integer(0)), flags_(flags), comment_(comment), hashval_(0) {}
514 
515 public:
517  Type type() const {
518  return type_;
519  }
520 
527  static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
528 
534  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
535 
537  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
538 
544  virtual bool isEquivalentTo(const Ptr &other) = 0;
545 
551  virtual int compareStructure(const Ptr &other) = 0;
552 
558  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
559 
567  Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
568 
576  Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
577  const SmtSolverPtr &solver = SmtSolverPtr());
578 
582  virtual Operator getOperator() const = 0;
583 
587  virtual size_t nChildren() const = 0;
588 
593  virtual Ptr child(size_t idx) const = 0;
594 
598  virtual const Nodes& children() const = 0;
599 
604  virtual Sawyer::Optional<uint64_t> toUnsigned() const = 0;
605 
609  virtual Sawyer::Optional<int64_t> toSigned() const = 0;
610 
612  bool isIntegerExpr() const {
613  return type_.typeClass() == Type::INTEGER;
614  }
615 
617  bool isFloatingPointExpr() const {
618  return type_.typeClass() == Type::FP;
619  }
620 
622  bool isMemoryExpr() const {
623  return type_.typeClass() == Type::MEMORY;
624  }
625 
629  bool isScalarExpr() const {
630  return isIntegerExpr() || isFloatingPointExpr();
631  }
632 
634  virtual bool isConstant() const = 0;
635 
637  bool isIntegerConstant() const {
638  return isIntegerExpr() && isConstant();
639  }
640 
642  bool isFloatingPointConstant() const {
643  return isFloatingPointExpr() && isConstant();
644  }
645 
649  bool isScalarConstant() const {
651  }
652 
654  bool isFloatingPointNan() const;
655 
661  virtual bool isVariable2() const = 0;
662 
667 
669  bool isIntegerVariable() const {
670  return isIntegerExpr() && isVariable2();
671  }
672 
674  bool isFloatingPointVariable() const {
675  return isFloatingPointExpr() && isVariable2();
676  }
677 
679  bool isMemoryVariable() const {
680  return isMemoryExpr() && isVariable2();
681  }
682 
686  bool isScalarVariable() const {
688  }
689 
698  const std::string& comment() const {
699  return comment_;
700  }
701  void comment(const std::string &s) {
702  comment_ = s;
703  }
713  void userData(boost::any &data) {
714  userData_ = data;
715  }
716  const boost::any& userData() const {
717  return userData_;
718  }
724  size_t nBits() const {
725  return type_.nBits();
726  }
727 
732  unsigned flags() const {
733  return flags_;
734  }
735 
739  Ptr newFlags(unsigned flags) const;
740 
744  size_t domainWidth() const {
745  return type_.addressWidth();
746  }
747 
751  bool isScalar() const {
752  return type_.typeClass() != Type::MEMORY;
753  }
754 
759  virtual VisitAction depthFirstTraversal(Visitor&) const = 0;
760 
776  virtual uint64_t nNodes() const = 0;
777 
779  uint64_t nNodesUnique() const;
780 
782  std::set<LeafPtr> getVariables() const;
783 
787  InteriorPtr isInteriorNode() const;
788 
792  LeafPtr isLeafNode() const;
793 
797  bool isHashed() const {
798  return hashval_ != 0;
799  }
800 
803  Hash hash() const;
804 
805  // used internally to set the hash value
806  void hash(Hash);
807 
810  private:
811  Ptr node;
812  Formatter &formatter;
813  public:
814  WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
815  void print(std::ostream &stream) const { node->print(stream, formatter); }
816  };
817 
839  virtual void print(std::ostream&, Formatter&) const = 0;
840  void print(std::ostream &o) const { Formatter fmt; print(o, fmt); }
844  void assertAcyclic() const;
845 
851  std::vector<Ptr> findCommonSubexpressions() const;
852 
858  bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/) const;
859 
861  InteriorPtr isOperator(Operator) const;
862 
863 protected:
864  void printFlags(std::ostream &o, unsigned flags, char &bracket) const;
865 
866 public:
867  // Deprecated [Robb Matzke 2019-09-27]
868  bool isNumber() const ROSE_DEPRECATED("use isIntegerConstant instead") {
869  return isIntegerConstant();
870  }
871 
872  // Deprecated [Robb Matzke 2019-09-27]
873  uint64_t toInt() ROSE_DEPRECATED("use toUnsigned() instead") {
874  return toUnsigned().get();
875  }
876 };
877 
879 class Simplifier {
880 public:
881  virtual ~Simplifier() {}
882 
886  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
887  return Ptr();
888  }
889 
892  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
893  return Ptr();
894  }
895 };
896 
898  size_t operator()(const Ptr &expr) const {
899  return expr->hash();
900  }
901 };
902 
904  bool operator()(const Ptr &a, const Ptr &b) const {
905  return a->isEquivalentTo(b);
906  }
907 };
908 
911 public:
912  bool operator()(const Ptr &a, const Ptr &b) const;
913 };
914 
916 class ExprExprHashMap: public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
917  ExprExprHashMapHasher, ExprExprHashMapCompare> {
918 public:
919  ExprExprHashMap invert() const;
920 };
921 
924 
925 
927 // Simplification
929 
931  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
932  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
933 };
935  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
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 fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
943  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
944 };
946  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
947  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
948 };
950  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
951 };
953  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
954 };
956  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
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  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
982 };
984  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
985 };
987  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
988 };
990  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
991 };
993  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
994 };
996  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
997 };
999  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1000 };
1002  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1003 };
1005  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1006 };
1008  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1009 };
1011  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1012 };
1014  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1015 };
1017  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1018 };
1020  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1021 };
1023  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1024 };
1026  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1027 };
1029  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1030 };
1032  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1033 };
1035  bool newbits;
1036  ShiftSimplifier(bool newbits): newbits(newbits) {}
1037  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
1038 };
1040  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1041  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1042 };
1044  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1045  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1046 };
1048  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1049 };
1051  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1052 };
1054  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1055 };
1056 
1057 
1058 
1060 // Interior Nodes
1062 
1069 class Interior: public Node {
1070 private:
1071  Operator op_;
1072  Nodes children_;
1073  uint64_t nnodes_; // total number of nodes; self + children's nnodes
1074 
1075  //--------------------------------------------------------
1076  // Serialization
1077  //--------------------------------------------------------
1078 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1079 private:
1080  friend class boost::serialization::access;
1081 
1082  template<class S>
1083  void serialize(S &s, const unsigned /*version*/) {
1084  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1085  s & BOOST_SERIALIZATION_NVP(op_);
1086  s & BOOST_SERIALIZATION_NVP(children_);
1087  s & BOOST_SERIALIZATION_NVP(nnodes_);
1088  }
1089 #endif
1090 
1091  //--------------------------------------------------------
1092  // Real constructors
1093  //--------------------------------------------------------
1094 private:
1095  Interior(); // needed for serialization
1096  // Only constructs, does not simplify.
1097  Interior(const Type&, Operator, const Nodes &arguments, const std::string &comment, unsigned flags);
1098 
1099  //--------------------------------------------------------
1100  // Allocating constructors
1101  //--------------------------------------------------------
1102 public:
1106  static Ptr instance(Operator op, const Ptr &a,
1107  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1108  static Ptr instance(const Type &type, Operator op, const Ptr &a,
1109  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1110  static Ptr instance(Operator op, const Ptr &a, const Ptr &b,
1111  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1112  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b,
1113  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1114  static Ptr instance(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(const Type &type, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1117  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1118  static Ptr instance(Operator op, const Nodes &arguments,
1119  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1120  static Ptr instance(const Type &type, Operator op, const Nodes &arguments,
1121  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1124  //--------------------------------------------------------
1125  // Overrides
1126  //--------------------------------------------------------
1127 public:
1128  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1129  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1130  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1131  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1132  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1133  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1134  virtual uint64_t nNodes() const ROSE_OVERRIDE { return nnodes_; }
1135  virtual const Nodes& children() const ROSE_OVERRIDE { return children_; }
1136  virtual Operator getOperator() const ROSE_OVERRIDE { return op_; }
1137  virtual size_t nChildren() const ROSE_OVERRIDE { return children_.size(); }
1138  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return idx < children_.size() ? children_[idx] : Ptr(); }
1139  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1140  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1141  virtual bool isConstant() const ROSE_OVERRIDE { return false; }
1142  virtual bool isVariable2() const ROSE_OVERRIDE { return false; }
1143 
1144  //--------------------------------------------------------
1145  // Simplification
1146  //--------------------------------------------------------
1147 public:
1151  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
1152 
1155  Ptr foldConstants(const Simplifier&);
1156 
1161  InteriorPtr associative();
1162 
1167  InteriorPtr commutative();
1168 
1175  InteriorPtr idempotent(const SmtSolverPtr &solver = SmtSolverPtr());
1176 
1180  Ptr involutary();
1181 
1185  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
1186 
1190  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
1191 
1196  Ptr poisonNan(const SmtSolverPtr &solver = SmtSolverPtr());
1197 
1199  Ptr unaryNoOp();
1200 
1204  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
1205 
1206  //--------------------------------------------------------
1207  // Functions specific to internal nodes
1208  //--------------------------------------------------------
1209 public:
1210  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1211 
1212 protected:
1214  void addChild(const Ptr &child);
1215 
1219  void adjustWidth(const Type&);
1220 
1223  void adjustBitFlags(unsigned extraFlags);
1224 
1225  //--------------------------------------------------------
1226  // Deprecated [Robb Matzke 2019-10-01]
1227  //--------------------------------------------------------
1228 public:
1229  static Ptr create(size_t nbits, Operator op, const Ptr &a,
1230  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1231  ROSE_DEPRECATED("use instance instead");
1232  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b,
1233  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1234  ROSE_DEPRECATED("use instance instead");
1235  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1236  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1237  ROSE_DEPRECATED("use instance instead");
1238  static Ptr create(size_t nbits, Operator op, const Nodes &children,
1239  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1240  ROSE_DEPRECATED("use instance instead");
1241 
1242 };
1243 
1244 
1246 // Leaf Nodes
1248 
1252 class Leaf: public Node {
1253 private:
1254  Sawyer::Container::BitVector bits_; // Value for constants if size > 0
1255  uint64_t name_; // Variable ID for variables when bits_.size() == 0
1256 
1257  //--------------------------------------------------------
1258  // Serialization
1259  //--------------------------------------------------------
1260 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1261 private:
1262  friend class boost::serialization::access;
1263 
1264  template<class S>
1265  void save(S &s, const unsigned /*version*/) const {
1266  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1267  s & BOOST_SERIALIZATION_NVP(bits_);
1268  s & BOOST_SERIALIZATION_NVP(name_);
1269  }
1270 
1271  template<class S>
1272  void load(S &s, const unsigned /*version*/) {
1273  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1274  s & BOOST_SERIALIZATION_NVP(bits_);
1275  s & BOOST_SERIALIZATION_NVP(name_);
1276  nextNameCounter(name_);
1277  }
1278 
1279  BOOST_SERIALIZATION_SPLIT_MEMBER();
1280 #endif
1281 
1282  //--------------------------------------------------------
1283  // Private constructors. Use create methods instead.
1284  //--------------------------------------------------------
1285 private:
1286  Leaf()
1287  : name_(0) {}
1288  explicit Leaf(const std::string &comment, unsigned flags=0)
1289  : Node(comment, flags), name_(0) {}
1290 
1291  // Allocating constructors.
1292 public:
1294  static LeafPtr createVariable(const Type&,
1295  const std::string &comment = "", unsigned flags = 0);
1296 
1298  static LeafPtr createVariable(const Type&, const uint64_t id,
1299  const std::string &comment = "", unsigned flags = 0);
1300 
1302  static LeafPtr createConstant(const Type&, const Sawyer::Container::BitVector&,
1303  const std::string &comment = "", unsigned flags = 0);
1304 
1305  //--------------------------------------------------------
1306  // Override base class implementations
1307  //--------------------------------------------------------
1308 public:
1309  virtual size_t nChildren() const ROSE_OVERRIDE { return 0; }
1310  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return Ptr(); }
1311  virtual const Nodes& children() const ROSE_OVERRIDE;
1312  virtual Operator getOperator() const ROSE_OVERRIDE { return OP_NONE; }
1313  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1314  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1315  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1316  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1317  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1318  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1319  virtual uint64_t nNodes() const ROSE_OVERRIDE { return 1; }
1320  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE;
1321  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE;
1322  virtual bool isConstant() const ROSE_OVERRIDE { return !bits_.isEmpty(); }
1323  virtual bool isVariable2() const ROSE_OVERRIDE { return !isConstant(); }
1324  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1325 
1326  //--------------------------------------------------------
1327  // Leaf-specific methods
1328  //--------------------------------------------------------
1329 public:
1331  const Sawyer::Container::BitVector& bits() const;
1332 
1334  bool isIntegerVariable() const {
1335  return type().typeClass() == Type::INTEGER && !isConstant();
1336  }
1337 
1340  return type().typeClass() == Type::FP && !isConstant();
1341  }
1342 
1344  bool isFloatingPointNan() const;
1345 
1347  bool isMemoryVariable() const {
1348  return type().typeClass() == Type::MEMORY && !isConstant();
1349  }
1350 
1355  uint64_t nameId() const;
1356 
1361  std::string toString() const;
1362 
1364  void printAsSigned(std::ostream&, Formatter&, bool asSigned = true) const;
1365 
1367  void printAsUnsigned(std::ostream &o, Formatter &f) const {
1368  printAsSigned(o, f, false);
1369  }
1370 
1371 private:
1372  // Obtain or register a name ID
1373  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1374 
1375  // Deprecated functions
1376 public:
1377  // Deprecated [Robb Matzke 2019-09-27]
1378  static LeafPtr createVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
1379  ROSE_DEPRECATED("use createVariable with type or makeIntegerVariable, etc.") {
1380  return createVariable(Type::integer(nBits), comment, flags);
1381  }
1382 
1383  // Deprecated [Robb Matzke 2019-09-27]
1384  static LeafPtr createExistingVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0)
1385  ROSE_DEPRECATED("use createVariable or makeIntegerVariable, etc.") {
1386  return createVariable(Type::integer(nBits), id, comment, flags);
1387  }
1388 
1389  // Deprecated [Robb Matzke 2019-09-27]
1390  static LeafPtr createInteger(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
1391  ROSE_DEPRECATED("use createConstant or makeIntegerConstant, etc.");
1392 
1393  // Deprecated [Robb Matzke 2019-09-27]
1394  static LeafPtr createConstant(const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0)
1395  ROSE_DEPRECATED("use createConstant with type or makeIntegerConstant, etc.") {
1396  return createConstant(Type::integer(bits.size()), bits, comment, flags);
1397  }
1398 
1399  // Deprecated [Robb Matzke 2019-09-27]
1400  static LeafPtr createBoolean(bool b, const std::string &comment="", unsigned flags=0)
1401  ROSE_DEPRECATED("use createConstant or makeBooleanConstant");
1402 
1403  // Deprecated [Robb Matzke 2019-09-27]
1404  static LeafPtr createMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
1405  ROSE_DEPRECATED("use createVariable with type or makeMemoryVariable") {
1406  return createVariable(Type::memory(addressWidth, valueWidth), comment, flags);
1407  }
1408 
1409  // Deprecated [Robb Matzke 2019-09-27]
1410  static LeafPtr createExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="",
1411  unsigned flags=0)
1412  ROSE_DEPRECATED("use createVariable with type or makeMemoryVariable") {
1413  return createVariable(Type::memory(addressWidth, valueWidth), id, comment, flags);
1414  }
1415 
1416  // Deprecated [Robb Matzke 2019-09-27]. The definition will eventually change to isVariable2()
1417  bool isVariable() const ROSE_DEPRECATED("use isIntegerVariable or isVariable2 instead") {
1418  return isIntegerVariable();
1419  }
1420 
1421  // Deprecated [Robb Matzke 2019-09-27]
1422  virtual bool isMemory() ROSE_DEPRECATED("use isMemoryVariable or isMemoryExpr instead") {
1423  return isMemoryVariable();
1424  }
1425 };
1426 
1428 // Factories
1430 
1436 LeafPtr makeVariable(const Type&, const std::string &comment="", unsigned flags=0);
1437 LeafPtr makeVariable(const Type&, uint64_t id, const std::string &comment="", unsigned flags=0);
1438 LeafPtr makeConstant(const Type&, const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1439 LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0);
1440 LeafPtr makeIntegerVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0);
1441 LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0);
1442 LeafPtr makeIntegerConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1443 LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0);
1444 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1445 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
1446 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1447 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, uint64_t id, const std::string &comment="", unsigned flags=0);
1448 LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0);
1449 LeafPtr makeFloatingPointConstant(double, const std::string &comment="", unsigned flags=0);
1450 LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1453 // Deprecated [Robb Matzke 2019-09-27]
1454 Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0)
1455  ROSE_DEPRECATED("use makeIntegerVariable instead");
1456 Ptr makeExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0)
1457  ROSE_DEPRECATED("use makeIntegerVariable instead");
1458 Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0)
1459  ROSE_DEPRECATED("use makeIntegerConstant instead");
1460 Ptr makeConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0)
1461  ROSE_DEPRECATED("use makeIntegerConstant instead");
1462 Ptr makeBoolean(bool, const std::string &comment="", unsigned flags=0)
1463  ROSE_DEPRECATED("use makeBooleanConstant instead");
1464 Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
1465  ROSE_DEPRECATED("use makeMemoryVariable instead");
1466 Ptr makeExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0)
1467  ROSE_DEPRECATED("use makeMemoryVariable instead");
1468 
1475 Ptr makeAdd(const Ptr&a, const Ptr &b,
1476  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1477 Ptr makeBooleanAnd(const Ptr &a, const Ptr &b,
1478  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1479  ROSE_DEPRECATED("use makeAnd instead"); // [Robb Matzke 2017-11-21]: deprecated
1480 Ptr makeAsr(const Ptr &sa, const Ptr &a,
1481  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1482 Ptr makeAnd(const Ptr &a, const Ptr &b,
1483  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1484 Ptr makeOr(const Ptr &a, const Ptr &b,
1485  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1486 Ptr makeXor(const Ptr &a, const Ptr &b,
1487  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1488 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1489  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1490 Ptr makeConvert(const Ptr &a, const Type &b,
1491  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1492 Ptr makeEq(const Ptr &a, const Ptr &b,
1493  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1494 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1495  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1496 Ptr makeInvert(const Ptr &a,
1497  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1498 Ptr makeIsInfinite(const Ptr &a,
1499  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1500 Ptr makeIsNan(const Ptr &a,
1501  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1502 Ptr makeIsNeg(const Ptr &a,
1503  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1504 Ptr makeIsNorm(const Ptr &a,
1505  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1506 Ptr makeIsPos(const Ptr &a,
1507  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1508 Ptr makeIsSubnorm(const Ptr &a,
1509  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1510 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1511  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1512 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1513  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1514 Ptr makeLssb(const Ptr &a,
1515  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1516 Ptr makeMax(const Ptr &a, const Ptr &b,
1517  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1518 Ptr makeMin(const Ptr &a, const Ptr &b,
1519  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1520 Ptr makeMssb(const Ptr &a,
1521  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1522 Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c,
1523  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1524 Ptr makeNe(const Ptr &a, const Ptr &b,
1525  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1526 Ptr makeNegate(const Ptr &a,
1527  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1528 Ptr makeBooleanOr(const Ptr &a, const Ptr &b,
1529  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1530  ROSE_DEPRECATED("use makeOr instead"); // [Robb Matzke 2017-11-21]: deprecated
1531 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1532  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1533 Ptr makeReinterpret(const Ptr &a, const Type &b,
1534  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1535 Ptr makeRol(const Ptr &sa, const Ptr &a,
1536  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1537 Ptr makeRor(const Ptr &sa, const Ptr &a,
1538  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1539 Ptr makeRound(const Ptr &a,
1540  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1541 Ptr makeSet(const Ptr &a, const Ptr &b,
1542  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1543 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1544  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1545 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1546  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1547 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1548  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1549 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1550  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1551 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1552  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1553 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1554  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1555 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1556  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1557 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1558  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1559 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1560  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1561 Ptr makeIsSignedPos(const Ptr &a,
1562  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1563 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1564  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1565 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1566  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1567 Ptr makeSignedMax(const Ptr &a, const Ptr &b,
1568  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1569 Ptr makeSignedMin(const Ptr &a, const Ptr &b,
1570  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1571 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1572  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1573 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1574  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1575 Ptr makeSqrt(const Ptr &a,
1576  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1577 Ptr makeDiv(const Ptr &a, const Ptr &b,
1578  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1579 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1580  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1581 Ptr makeGe(const Ptr &a, const Ptr &b,
1582  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1583 Ptr makeGt(const Ptr &a, const Ptr &b,
1584  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1585 Ptr makeLe(const Ptr &a, const Ptr &b,
1586  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1587 Ptr makeLt(const Ptr &a, const Ptr &b,
1588  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1589 Ptr makeMod(const Ptr &a, const Ptr &b,
1590  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1591 Ptr makeMul(const Ptr &a, const Ptr &b,
1592  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1593 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1594  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1595 Ptr makeZerop(const Ptr &a,
1596  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1600 // Miscellaneous functions
1603 
1604 
1605 std::ostream& operator<<(std::ostream &o, Node&);
1606 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1607 
1609 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1610 
1615 Hash hash(const std::vector<Ptr>&);
1616 
1621 template<typename InputIterator>
1622 uint64_t
1623 nNodes(InputIterator begin, InputIterator end) {
1624  uint64_t total = 0;
1625  for (InputIterator ii=begin; ii!=end; ++ii) {
1626  uint64_t n = (*ii)->nnodes();
1627  if (MAX_NNODES==n)
1628  return MAX_NNODES;
1629  if (total + n < total)
1630  return MAX_NNODES;
1631  total += n;
1632  }
1633  return total;
1634 }
1635 
1640 template<typename InputIterator>
1641 uint64_t
1642 nNodesUnique(InputIterator begin, InputIterator end)
1643 {
1644  struct T1: Visitor {
1645  typedef std::set<const Node*> SeenNodes;
1646 
1647  SeenNodes seen; // nodes that we've already seen, and the subtree size
1648  uint64_t nUnique; // number of unique nodes
1649 
1650  T1(): nUnique(0) {}
1651 
1652  VisitAction preVisit(const Ptr &node) {
1653  if (seen.insert(getRawPointer(node)).second) {
1654  ++nUnique;
1655  return CONTINUE; // this node has not been seen before; traverse into children
1656  } else {
1657  return TRUNCATE; // this node has been seen already; skip over the children
1658  }
1659  }
1660 
1661  VisitAction postVisit(const Ptr &node) {
1662  return CONTINUE;
1663  }
1664  } visitor;
1665 
1666  VisitAction status = CONTINUE;
1667  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1668  status = (*ii)->depthFirstTraversal(visitor);
1669  return visitor.nUnique;
1670 }
1671 
1678 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1679 
1680 template<typename InputIterator>
1681 std::vector<Ptr>
1682 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1683  typedef Sawyer::Container::Map<Ptr, size_t> NodeCounts;
1684  struct T1: Visitor {
1685  NodeCounts nodeCounts;
1686  std::vector<Ptr> result;
1687 
1688  VisitAction preVisit(const Ptr &node) ROSE_OVERRIDE {
1689  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1690  if (2 == ++nSeen)
1691  result.push_back(node);
1692  return nSeen>1 ? TRUNCATE : CONTINUE;
1693  }
1694 
1695  VisitAction postVisit(const Ptr&) ROSE_OVERRIDE {
1696  return CONTINUE;
1697  }
1698  } visitor;
1699 
1700  for (InputIterator ii=begin; ii!=end; ++ii)
1701  (*ii)->depthFirstTraversal(visitor);
1702  return visitor.result;
1703 }
1713 template<class Substitution>
1714 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1715  if (!src)
1716  return Ptr(); // no input implies no output
1717 
1718  // Try substituting the whole expression, returning the result.
1719  Ptr dst = subber(src, solver);
1720  ASSERT_not_null(dst);
1721  if (dst != src)
1722  return dst;
1723 
1724  // Try substituting all the subexpressions.
1725  InteriorPtr inode = src->isInteriorNode();
1726  if (!inode)
1727  return src;
1728  bool anyChildChanged = false;
1729  Nodes newChildren;
1730  newChildren.reserve(inode->nChildren());
1731  BOOST_FOREACH (const Ptr &child, inode->children()) {
1732  Ptr newChild = substitute(child, subber, solver);
1733  if (newChild != child)
1734  anyChildChanged = true;
1735  newChildren.push_back(newChild);
1736  }
1737  if (!anyChildChanged)
1738  return src;
1739 
1740  // Some subexpression changed, so build a new expression
1741  return Interior::instance(inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1742 }
1743 
1744 } // namespace
1745 } // namespace
1746 } // namespace
1747 
1748 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1749 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1750 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1751 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Type, 1);
1752 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Node, 1);
1753 #endif
1754 
1755 #endif
1756 #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.