ROSE  0.11.109.0
SymbolicExpression.h
1 #ifndef ROSE_BinaryAnalysis_SymbolicExpression_H
2 #define ROSE_BinaryAnalysis_SymbolicExpression_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #ifndef __STDC_FORMAT_MACROS
7 #define __STDC_FORMAT_MACROS
8 #endif
9 
10 #include "Map.h"
11 
12 #include <boost/any.hpp>
13 #include <boost/lexical_cast.hpp>
14 #include <boost/logic/tribool.hpp>
15 #include <boost/serialization/access.hpp>
16 #include <boost/serialization/base_object.hpp>
17 #include <boost/serialization/export.hpp>
18 #include <boost/serialization/split_member.hpp>
19 #include <boost/serialization/string.hpp>
20 #include <boost/serialization/vector.hpp>
21 #include <boost/unordered_map.hpp>
22 #include <cassert>
23 #include <inttypes.h>
24 #include <Rose/Exception.h>
25 #include <Sawyer/Attribute.h>
26 #include <Sawyer/BitVector.h>
27 #include <Sawyer/Optional.h>
28 #include <Sawyer/Set.h>
29 #include <Sawyer/SharedPointer.h>
30 #include <Sawyer/SmallObject.h>
31 #include <set>
32 #include <string>
33 #include <vector>
34 
35 namespace Rose {
36 namespace BinaryAnalysis {
37 
43 namespace SymbolicExpression {
44 
46 // Basic Types and settings
48 
57 extern bool serializeVariableIds;
58 
60 namespace TypeStyle {
62  enum Flag {
63  FULL,
65  };
66 }
67 
68 
70 class Exception: public Rose::Exception {
71 public:
72  explicit Exception(const std::string &mesg): Rose::Exception(mesg) {}
73 };
74 
80 enum Operator {
152 };
153 
154 std::string toStr(Operator);
155 
156 using Nodes = std::vector<Ptr>;
157 using RenameMap = Map<uint64_t, uint64_t>;
158 
160 using Hash = uint64_t;
161 
163 class Formatter {
164 public:
169  };
170  Formatter()
172  max_depth(0), cur_depth(0), show_type(true), show_flags(true) {}
174  bool do_rename;
175  bool add_renames;
177  size_t max_depth;
178  size_t cur_depth;
180  bool show_type;
181  bool show_flags;
182 };
183 
189 };
190 
195 extern const uint64_t MAX_NNODES; // defined in .C so we don't pollute user namespace with limit macros
196 
208 class Visitor {
209 public:
210  virtual ~Visitor() {}
211 
212  virtual VisitAction preVisit(const Ptr&);
213  virtual VisitAction postVisit(const Ptr&);
214 
215  virtual VisitAction preVisit(const Node*);
216  virtual VisitAction postVisit(const Node*);
217 };
218 
220 // Expression type information
222 
224 class Type {
225 public:
227  enum TypeClass {
229  FP,
232  };
233 
234 private:
235  // 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),
236  // and the type class (2 bits: 30 and 31).
237  uint32_t fields_;
238 
239 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
240 private:
241  friend class boost::serialization::access;
242 
243  template<class S>
244  void serialize(S &s, const unsigned version) {
245  if (version >= 1) {
246  s & BOOST_SERIALIZATION_NVP(fields_);
247  } else {
248  TypeClass t = typeClass();
249  size_t z1 = nBits();
250  size_t z2 = secondaryWidth();
251  s & boost::serialization::make_nvp("typeClass_", t);
252  s & boost::serialization::make_nvp("totalWidth_", z1);
253  s & boost::serialization::make_nvp("secondaryWidth_", z2);
254  typeClass(t);
255  nBits(z1);
256  secondaryWidth(z2);
257  }
258  }
259 #endif
260 
264 public:
266  : fields_(0) {
268  nBits(0);
269  secondaryWidth(0);
270  }
271 
272 private:
273  Type(TypeClass tc, size_t w1, size_t w2)
274  : fields_(0) {
275  typeClass(tc);
276  nBits(w1);
277  secondaryWidth(w2);
278  }
279 
280 public:
284  static Type none() {
285  return Type();
286  }
287 
293  static Type integer(size_t nBits) {
294  return Type(INTEGER, nBits, 0);
295  }
296 
300  static Type memory(size_t addressWidth, size_t valueWidth) {
301  return Type(MEMORY, valueWidth, addressWidth);
302  }
303 
313  return Type(FP, 1 /*sign bit*/ + exponentWidth + significandWidth - 1 /*implied bit*/, exponentWidth);
314  }
315 
319  bool isValid() const {
320  return typeClass() != INVALID;
321  }
322 
327  return (TypeClass)((fields_ >> 30) & 0x3);
328  }
329 
334  size_t nBits() const {
335  return fields_ & 0x7fff;
336  }
337 
342  size_t addressWidth() const {
343  ASSERT_require(MEMORY == typeClass());
344  return secondaryWidth();
345  }
346 
351  size_t exponentWidth() const {
352  ASSERT_require(FP == typeClass());
353  return secondaryWidth();
354  }
355 
361  size_t significandWidth() const {
362  ASSERT_require(FP == typeClass());
363  ASSERT_require(nBits() > 1 /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
364  return nBits() - (1 /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
365  }
366 
372  bool operator==(const Type &other) const {
373  return fields_ == other.fields_;
374  }
375  bool operator!=(const Type &other) const {
376  return !(*this == other);
377  }
381  bool operator<(const Type &other) const;
382 
384  void print(std::ostream&, TypeStyle::Flag style = TypeStyle::FULL) const;
385 
387  std::string toString(TypeStyle::Flag style = TypeStyle::FULL) const;
388 
389 private:
390  // mutators are all private
391  void typeClass(TypeClass tc) {
392  unsigned n = tc;
393  ASSERT_require(n <= 3);
394  fields_ = (fields_ & 0x3fffffff) | (n << 30);
395  }
396 
397  // mutators are all private
398  void nBits(size_t n) {
399  if (n > 0x7fff)
400  throw Exception("type width is out of range");
401  fields_ = (fields_ & 0xffff8000) | n;
402  }
403 
404  // mutators are all private
405  void secondaryWidth(size_t n) {
406  if (n > 0x7fff)
407  throw Exception("second width is out of range");
408  fields_ = (fields_ & 0xc0007fff) | (n << 15);
409  }
410 
411  size_t secondaryWidth() const {
412  return (fields_ >> 15) & 0x7fff;
413  }
414 };
415 
417 // Base Node Type
419 
457 class Node
458  : public Sawyer::SharedObject,
459  public Sawyer::SharedFromThis<Node>,
460  public Sawyer::SmallObject,
461  public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
462 protected:
463  Type type_;
464  unsigned flags_;
465  std::string comment_;
466  mutable Hash hashval_;
467  boost::any userData_;
469 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
470 private:
471  friend class boost::serialization::access;
472 
473  template<class S>
474  void serialize(S &s, const unsigned version) {
475  if (version < 1)
476  ASSERT_not_reachable("SymbolicExpression version " + boost::lexical_cast<std::string>(version) + " is no longer supported");
477  s & BOOST_SERIALIZATION_NVP(type_);
478  s & BOOST_SERIALIZATION_NVP(flags_);
479  s & BOOST_SERIALIZATION_NVP(comment_);
480  s & BOOST_SERIALIZATION_NVP(hashval_);
481  // s & userData_;
482  }
483 #endif
484 
485 public:
486  // Bit flags
487 
489  static const unsigned RESERVED_FLAGS = 0x0000ffff;
490 
492  static const unsigned INDETERMINATE = 0x00000001;
493 
498  static const unsigned UNSPECIFIED = 0x00000002;
499 
502  static const unsigned BOTTOM = 0x00000004;
503 
504 protected:
505  Node()
506  : type_(Type::integer(0)), flags_(0), hashval_(0) {}
507  explicit Node(const std::string &comment, unsigned flags=0)
508  : type_(Type::integer(0)), flags_(flags), comment_(comment), hashval_(0) {}
509 
510 public:
512  Type type() const {
513  return type_;
514  }
515 
522  static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
523 
529  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
530 
532  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
533 
539  virtual bool isEquivalentTo(const Ptr &other) = 0;
540 
546  virtual int compareStructure(const Ptr &other) = 0;
547 
553  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
554 
562  Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
563 
571  Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
572  const SmtSolverPtr &solver = SmtSolverPtr());
573 
577  virtual Operator getOperator() const = 0;
578 
582  virtual size_t nChildren() const = 0;
583 
590  virtual const Ptr& child(size_t idx) const = 0;
591  virtual const Node* childRaw(size_t idx) const = 0;
597  virtual const Nodes& children() const = 0;
598 
603  virtual Sawyer::Optional<uint64_t> toUnsigned() const = 0;
604 
608  virtual Sawyer::Optional<int64_t> toSigned() const = 0;
609 
611  bool isIntegerExpr() const {
612  return type_.typeClass() == Type::INTEGER;
613  }
614 
616  bool isFloatingPointExpr() const {
617  return type_.typeClass() == Type::FP;
618  }
619 
621  bool isMemoryExpr() const {
622  return type_.typeClass() == Type::MEMORY;
623  }
624 
628  bool isScalarExpr() const {
629  return isIntegerExpr() || isFloatingPointExpr();
630  }
631 
633  virtual bool isConstant() const = 0;
634 
636  bool isIntegerConstant() const {
637  return isIntegerExpr() && isConstant();
638  }
639 
641  bool isFloatingPointConstant() const {
642  return isFloatingPointExpr() && isConstant();
643  }
644 
648  bool isScalarConstant() const {
650  }
651 
653  bool isFloatingPointNan() const;
654 
660  virtual bool isVariable2() const = 0;
661 
666 
668  bool isIntegerVariable() const {
669  return isIntegerExpr() && isVariable2();
670  }
671 
673  bool isFloatingPointVariable() const {
674  return isFloatingPointExpr() && isVariable2();
675  }
676 
678  bool isMemoryVariable() const {
679  return isMemoryExpr() && isVariable2();
680  }
681 
685  bool isScalarVariable() const {
687  }
688 
697  const std::string& comment() const {
698  return comment_;
699  }
700  void comment(const std::string &s) {
701  comment_ = s;
702  }
712  void userData(boost::any &data) {
713  userData_ = data;
714  }
715  const boost::any& userData() const {
716  return userData_;
717  }
723  size_t nBits() const {
724  return type_.nBits();
725  }
726 
731  unsigned flags() const {
732  return flags_;
733  }
734 
738  Ptr newFlags(unsigned flags) const;
739 
743  size_t domainWidth() const {
744  return type_.addressWidth();
745  }
746 
750  bool isScalar() const {
751  return type_.typeClass() != Type::MEMORY;
752  }
753 
758  virtual VisitAction depthFirstTraversal(Visitor&) const = 0;
759 
775  virtual uint64_t nNodes() const = 0;
776 
778  uint64_t nNodesUnique() const;
779 
781  std::set<LeafPtr> getVariables() const;
782 
788  InteriorPtr isInteriorNode() const;
789  Interior* isInteriorNodeRaw() const;
797  LeafPtr isLeafNode() const;
798  Leaf* isLeafNodeRaw() const;
804  bool isHashed() const {
805  return hashval_ != 0;
806  }
807 
810  Hash hash() const;
811 
812  // used internally to set the hash value
813  void hash(Hash) const;
814 
817  private:
818  Ptr node;
819  Formatter &formatter;
820  public:
821  WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
822  void print(std::ostream &stream) const { node->print(stream, formatter); }
823  };
824 
846  virtual void print(std::ostream&, Formatter&) const = 0;
847  void print(std::ostream &o) const { Formatter fmt; print(o, fmt); }
851  std::string toString() const;
852 
854  void assertAcyclic() const;
855 
861  std::vector<Ptr> findCommonSubexpressions() const;
862 
868  bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/) const;
869 
872 
873 protected:
874  void printFlags(std::ostream &o, unsigned flags, char &bracket) const;
875 
876 public: // only used internally
877  using EquivPairs = std::map<Node*, std::vector<std::pair<Node*, bool>>>;
878  virtual bool isEquivalentHelper(Node*, EquivPairs&) = 0;
879 };
880 
882 class Simplifier {
883 public:
884  virtual ~Simplifier() {}
885 
889  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
890  return Ptr();
891  }
892 
895  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
896  return Ptr();
897  }
898 };
899 
901  size_t operator()(const Ptr &expr) const {
902  return expr->hash();
903  }
904 };
905 
907  bool operator()(const Ptr &a, const Ptr &b) const {
908  return a->isEquivalentTo(b);
909  }
910 };
911 
914 public:
915  bool operator()(const Ptr &a, const Ptr &b) const;
916 };
917 
919 class ExprExprHashMap: public boost::unordered_map<SymbolicExpression::Ptr, SymbolicExpression::Ptr,
920  ExprExprHashMapHasher, ExprExprHashMapCompare> {
921 public:
922  ExprExprHashMap invert() const;
923 };
924 
927 
928 
930 // Simplification
932 
934  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
935  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
936 };
938  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
939  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
940 };
942  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
943 };
945  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
946  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
947 };
949  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
950  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
951 };
953  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
954 };
956  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
957 };
959  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
960  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
961 };
963  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
964 };
966  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
967 };
969  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
970 };
972  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
973 };
975  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
976 };
978  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
979 };
981  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
982 };
984  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
985 };
987  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
988 };
990  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
991 };
993  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
994 };
996  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
997 };
999  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1000 };
1002  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1003 };
1005  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1006 };
1008  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1009 };
1011  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1012 };
1014  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1015 };
1017  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1018 };
1020  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1021 };
1023  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1024 };
1026  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1027 };
1029  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1030 };
1032  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1033 };
1035  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1036 };
1038  bool newbits;
1039  ShiftSimplifier(bool newbits): newbits(newbits) {}
1040  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
1041 };
1043  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1044  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1045 };
1047  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1048  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1049 };
1051  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1052 };
1054  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1055 };
1057  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
1058 };
1059 
1060 
1061 
1063 // Interior Nodes
1065 
1072 class Interior: public Node {
1073 private:
1074  Operator op_;
1075  Nodes children_;
1076  uint64_t nnodes_; // total number of nodes; self + children's nnodes
1077 
1078  //--------------------------------------------------------
1079  // Serialization
1080  //--------------------------------------------------------
1081 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1082 private:
1083  friend class boost::serialization::access;
1084 
1085  template<class S>
1086  void serialize(S &s, const unsigned /*version*/) {
1087  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1088  s & BOOST_SERIALIZATION_NVP(op_);
1089  s & BOOST_SERIALIZATION_NVP(children_);
1090  s & BOOST_SERIALIZATION_NVP(nnodes_);
1091  }
1092 #endif
1093 
1094  //--------------------------------------------------------
1095  // Real constructors
1096  //--------------------------------------------------------
1097 private:
1098  Interior(); // needed for serialization
1099  // Only constructs, does not simplify.
1100  Interior(const Type&, Operator, const Nodes &arguments, const std::string &comment, unsigned flags);
1101 
1102  //--------------------------------------------------------
1103  // Allocating constructors
1104  //--------------------------------------------------------
1105 public:
1109  static Ptr instance(Operator op, const Ptr &a,
1110  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1111  static Ptr instance(const Type &type, Operator op, const Ptr &a,
1112  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1113  static Ptr instance(Operator op, const Ptr &a, const Ptr &b,
1114  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1115  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b,
1116  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1117  static Ptr instance(Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1118  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1119  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1120  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1121  static Ptr instance(Operator op, const Nodes &arguments,
1122  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1123  static Ptr instance(const Type &type, Operator op, const Nodes &arguments,
1124  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1127  //--------------------------------------------------------
1128  // Overrides
1129  //--------------------------------------------------------
1130 public:
1131  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1132  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1133  virtual bool isEquivalentTo(const Ptr &other) override;
1134  virtual bool isEquivalentHelper(Node*, EquivPairs&) override;
1135  virtual int compareStructure(const Ptr& other) override;
1136  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1137  virtual VisitAction depthFirstTraversal(Visitor&) const override;
1138  virtual uint64_t nNodes() const override { return nnodes_; }
1139  virtual const Nodes& children() const override { return children_; }
1140  virtual Operator getOperator() const override { return op_; }
1141  virtual size_t nChildren() const override { return children_.size(); }
1142  virtual const Ptr& child(size_t idx) const override;
1143  virtual Node* childRaw(size_t idx) const override;
1144  virtual Sawyer::Optional<uint64_t> toUnsigned() const override { return Sawyer::Nothing(); }
1145  virtual Sawyer::Optional<int64_t> toSigned() const override { return Sawyer::Nothing(); }
1146  virtual bool isConstant() const override { return false; }
1147  virtual bool isVariable2() const override { return false; }
1148 
1149  //--------------------------------------------------------
1150  // Simplification
1151  //--------------------------------------------------------
1152 public:
1156  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
1157 
1160  Ptr foldConstants(const Simplifier&);
1161 
1167 
1173 
1180  InteriorPtr idempotent(const SmtSolverPtr &solver = SmtSolverPtr());
1181 
1185  Ptr involutary();
1186 
1190  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
1191 
1195  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
1196 
1201  Ptr poisonNan(const SmtSolverPtr &solver = SmtSolverPtr());
1202 
1204  Ptr unaryNoOp();
1205 
1209  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
1210 
1211  //--------------------------------------------------------
1212  // Functions specific to internal nodes
1213  //--------------------------------------------------------
1214 public:
1215  virtual void print(std::ostream&, Formatter&) const override;
1216 
1217 protected:
1219  void addChild(const Ptr &child);
1220 
1224  void adjustWidth(const Type&);
1225 
1228  void adjustBitFlags(unsigned extraFlags);
1229 };
1230 
1231 
1233 // Leaf Nodes
1235 
1239 class Leaf: public Node {
1240 private:
1241  Sawyer::Container::BitVector bits_; // Value for constants if size > 0
1242  uint64_t name_; // Variable ID for variables when bits_.size() == 0
1243 
1244  //--------------------------------------------------------
1245  // Serialization
1246  //--------------------------------------------------------
1247 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1248 private:
1249  friend class boost::serialization::access;
1250 
1251  template<class S>
1252  void save(S &s, const unsigned /*version*/) const {
1253  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1254  s & BOOST_SERIALIZATION_NVP(bits_);
1255  s & BOOST_SERIALIZATION_NVP(name_);
1256  }
1257 
1258  template<class S>
1259  void load(S &s, const unsigned /*version*/) {
1260  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1261  s & BOOST_SERIALIZATION_NVP(bits_);
1262  s & BOOST_SERIALIZATION_NVP(name_);
1263  nextNameCounter(name_);
1264  }
1265 
1266  BOOST_SERIALIZATION_SPLIT_MEMBER();
1267 #endif
1268 
1269  //--------------------------------------------------------
1270  // Private constructors. Use create methods instead.
1271  //--------------------------------------------------------
1272 private:
1273  Leaf()
1274  : name_(0) {}
1275  explicit Leaf(const std::string &comment, unsigned flags=0)
1276  : Node(comment, flags), name_(0) {}
1277 
1278  // Allocating constructors.
1279 public:
1281  static LeafPtr createVariable(const Type&,
1282  const std::string &comment = "", unsigned flags = 0);
1283 
1285  static LeafPtr createVariable(const Type&, const uint64_t id,
1286  const std::string &comment = "", unsigned flags = 0);
1287 
1290  const std::string &comment = "", unsigned flags = 0);
1291 
1292  //--------------------------------------------------------
1293  // Override base class implementations
1294  //--------------------------------------------------------
1295 public:
1296  virtual size_t nChildren() const override { return 0; }
1297  virtual const Ptr& child(size_t idx) const override;
1298  virtual const Node* childRaw(size_t) const override { return nullptr; }
1299  virtual const Nodes& children() const override;
1300  virtual Operator getOperator() const override { return OP_NONE; }
1301  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1302  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1303  virtual bool isEquivalentTo(const Ptr &other) override;
1304  virtual bool isEquivalentHelper(Node*, EquivPairs&) override;
1305  virtual int compareStructure(const Ptr& other) override;
1306  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) override;
1307  virtual VisitAction depthFirstTraversal(Visitor&) const override;
1308  virtual uint64_t nNodes() const override { return 1; }
1309  virtual Sawyer::Optional<uint64_t> toUnsigned() const override;
1310  virtual Sawyer::Optional<int64_t> toSigned() const override;
1311  virtual bool isConstant() const override { return !bits_.isEmpty(); }
1312  virtual bool isVariable2() const override { return !isConstant(); }
1313  virtual void print(std::ostream&, Formatter&) const override;
1314 
1315  //--------------------------------------------------------
1316  // Leaf-specific methods
1317  //--------------------------------------------------------
1318 public:
1320  const Sawyer::Container::BitVector& bits() const;
1321 
1323  bool isIntegerVariable() const {
1324  return type().typeClass() == Type::INTEGER && !isConstant();
1325  }
1326 
1329  return type().typeClass() == Type::FP && !isConstant();
1330  }
1331 
1333  bool isFloatingPointNan() const;
1334 
1336  bool isMemoryVariable() const {
1337  return type().typeClass() == Type::MEMORY && !isConstant();
1338  }
1339 
1344  uint64_t nameId() const;
1345 
1350  std::string toString() const;
1351 
1353  void printAsSigned(std::ostream&, Formatter&, bool asSigned = true) const;
1354 
1356  void printAsUnsigned(std::ostream &o, Formatter &f) const {
1357  printAsSigned(o, f, false);
1358  }
1359 
1360 private:
1361  // Obtain or register a name ID
1362  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1363 };
1364 
1366 // Factories
1368 
1374 LeafPtr makeVariable(const Type&, const std::string &comment="", unsigned flags=0);
1375 LeafPtr makeVariable(const Type&, uint64_t id, const std::string &comment="", unsigned flags=0);
1376 LeafPtr makeConstant(const Type&, const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1377 LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0);
1378 LeafPtr makeIntegerVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0);
1379 LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0);
1380 LeafPtr makeIntegerConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1381 LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0);
1382 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1383 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
1384 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1385 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, uint64_t id, const std::string &comment="", unsigned flags=0);
1386 LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0);
1387 LeafPtr makeFloatingPointConstant(double, const std::string &comment="", unsigned flags=0);
1388 LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1397 Ptr makeAdd(const Ptr&a, const Ptr &b,
1398  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1399 Ptr makeAsr(const Ptr &sa, const Ptr &a,
1400  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1401 Ptr makeAnd(const Ptr &a, const Ptr &b,
1402  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1403 Ptr makeOr(const Ptr &a, const Ptr &b,
1404  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1405 Ptr makeXor(const Ptr &a, const Ptr &b,
1406  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1407 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1408  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1409 Ptr makeConvert(const Ptr &a, const Type &b,
1410  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1411 Ptr makeEq(const Ptr &a, const Ptr &b,
1412  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1413 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1414  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1415 Ptr makeInvert(const Ptr &a,
1416  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1417 Ptr makeIsInfinite(const Ptr &a,
1418  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1419 Ptr makeIsNan(const Ptr &a,
1420  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1421 Ptr makeIsNeg(const Ptr &a,
1422  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1423 Ptr makeIsNorm(const Ptr &a,
1424  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1425 Ptr makeIsPos(const Ptr &a,
1426  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1427 Ptr makeIsSubnorm(const Ptr &a,
1428  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1429 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1430  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1431 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1432  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1433 Ptr makeLssb(const Ptr &a,
1434  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1435 Ptr makeMax(const Ptr &a, const Ptr &b,
1436  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1437 Ptr makeMin(const Ptr &a, const Ptr &b,
1438  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1439 Ptr makeMssb(const Ptr &a,
1440  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1441 Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c,
1442  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1443 Ptr makeNe(const Ptr &a, const Ptr &b,
1444  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1445 Ptr makeNegate(const Ptr &a,
1446  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1447 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1448  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1449 Ptr makeReinterpret(const Ptr &a, const Type &b,
1450  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1451 Ptr makeRol(const Ptr &sa, const Ptr &a,
1452  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1453 Ptr makeRor(const Ptr &sa, const Ptr &a,
1454  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1455 Ptr makeRound(const Ptr &a,
1456  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1457 Ptr makeSet(const Ptr &a, const Ptr &b,
1458  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1459 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1460  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1461 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1462  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1463 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1464  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1465 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1466  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1467 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1468  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1469 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1470  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1471 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1472  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1473 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1474  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1475 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1476  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1477 Ptr makeIsSignedPos(const Ptr &a,
1478  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1479 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1480  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1481 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1482  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1483 Ptr makeSignedMax(const Ptr &a, const Ptr &b,
1484  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1485 Ptr makeSignedMin(const Ptr &a, const Ptr &b,
1486  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1487 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1488  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1489 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1490  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1491 Ptr makeSqrt(const Ptr &a,
1492  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1493 Ptr makeDiv(const Ptr &a, const Ptr &b,
1494  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1495 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1496  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1497 Ptr makeGe(const Ptr &a, const Ptr &b,
1498  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1499 Ptr makeGt(const Ptr &a, const Ptr &b,
1500  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1501 Ptr makeLe(const Ptr &a, const Ptr &b,
1502  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1503 Ptr makeLt(const Ptr &a, const Ptr &b,
1504  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1505 Ptr makeMod(const Ptr &a, const Ptr &b,
1506  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1507 Ptr makeMul(const Ptr &a, const Ptr &b,
1508  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1509 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1510  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1511 Ptr makeZerop(const Ptr &a,
1512  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1516 // Miscellaneous functions
1519 
1520 
1521 std::ostream& operator<<(std::ostream &o, const Node&);
1522 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1523 
1525 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1526 
1531 Hash hash(const std::vector<Ptr>&);
1532 
1537 template<typename InputIterator>
1538 uint64_t
1539 nNodes(InputIterator begin, InputIterator end) {
1540  uint64_t total = 0;
1541  for (InputIterator ii=begin; ii!=end; ++ii) {
1542  uint64_t n = (*ii)->nnodes();
1543  if (MAX_NNODES==n)
1544  return MAX_NNODES;
1545  if (total + n < total)
1546  return MAX_NNODES;
1547  total += n;
1548  }
1549  return total;
1550 }
1551 
1556 template<typename InputIterator>
1557 uint64_t
1558 nNodesUnique(InputIterator begin, InputIterator end)
1559 {
1560  struct T1: Visitor {
1561  typedef std::set<const Node*> SeenNodes;
1562 
1563  SeenNodes seen; // nodes that we've already seen, and the subtree size
1564  uint64_t nUnique; // number of unique nodes
1565 
1566  T1(): nUnique(0) {}
1567 
1568  VisitAction preVisit(const Node *node) override {
1569  ASSERT_not_null(node);
1570  if (seen.insert(node).second) {
1571  ++nUnique;
1572  return CONTINUE; // this node has not been seen before; traverse into children
1573  } else {
1574  return TRUNCATE; // this node has been seen already; skip over the children
1575  }
1576  }
1577 
1578  VisitAction postVisit(const Node*) override {
1579  return CONTINUE;
1580  }
1581  } visitor;
1582 
1583  VisitAction status = CONTINUE;
1584  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1585  status = (*ii)->depthFirstTraversal(visitor);
1586  return visitor.nUnique;
1587 }
1588 
1595 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1596 
1597 template<typename InputIterator>
1598 std::vector<Ptr>
1599 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1601  struct T1: Visitor {
1602  NodeCounts nodeCounts;
1603  std::vector<Ptr> result;
1604 
1605  VisitAction preVisit(const Node *node) override {
1606  ASSERT_not_null(node);
1607  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1608  if (2 == ++nSeen)
1609  result.push_back(Ptr(const_cast<Node*>(node)));
1610  return nSeen>1 ? TRUNCATE : CONTINUE;
1611  }
1612 
1613  VisitAction postVisit(const Node*) override {
1614  return CONTINUE;
1615  }
1616  } visitor;
1617 
1618  for (InputIterator ii=begin; ii!=end; ++ii)
1619  (*ii)->depthFirstTraversal(visitor);
1620  return visitor.result;
1621 }
1631 template<class Substitution>
1632 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1633  if (!src)
1634  return Ptr(); // no input implies no output
1635 
1636  // Try substituting the whole expression, returning the result.
1637  Ptr dst = subber(src, solver);
1638  ASSERT_not_null(dst);
1639  if (dst != src)
1640  return dst;
1641 
1642  // Try substituting all the subexpressions.
1643  const Interior *inode = src->isInteriorNodeRaw();
1644  if (!inode)
1645  return src;
1646  bool anyChildChanged = false;
1647  Nodes newChildren;
1648  newChildren.reserve(inode->nChildren());
1649  for (const Ptr &child: inode->children()) {
1650  Ptr newChild = substitute(child, subber, solver);
1651  if (newChild != child)
1652  anyChildChanged = true;
1653  newChildren.push_back(newChild);
1654  }
1655  if (!anyChildChanged)
1656  return src;
1657 
1658  // Some subexpression changed, so build a new expression
1659  return Interior::instance(inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1660 }
1661 
1662 } // namespace
1663 
1664 using SymbolicExpressionPtr = SymbolicExpression::Ptr;
1665 
1666 } // namespace
1667 } // namespace
1668 
1669 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1671 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpression::Leaf);
1672 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpression::Type, 1);
1673 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpression::Node, 1);
1674 #endif
1675 
1676 #endif
1677 #endif
Ptr makeAsr(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
std::vector< Ptr > findCommonSubexpressions(const std::vector< Ptr > &)
Find common subexpressions.
uint64_t nameId() const
Returns the name ID of a free variable.
static const unsigned INDETERMINATE
Value is somehow indeterminate.
static const unsigned UNSPECIFIED
Value is somehow unspecified.
virtual Operator getOperator() const =0
Operator for interior nodes.
Ptr makeConvert(const Ptr &a, const Type &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) override
Substitute one value for another.
static LeafPtr createConstant(const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0)
Create a constant.
Ordered set of values.
Definition: Set.h:52
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.
void addChild(const Ptr &child)
Appends child as a new child of this node.
bool isFloatingPointVariable() const
True if this expression is a floating-point variable.
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.
void printAsSigned(std::ostream &, Formatter &, bool asSigned=true) const
Prints an integer constant interpreted as a signed value.
Hash hash() const
Returns (and caches) the hash value for this node.
LeafPtr isLeafNode() const
Dynamic cast of this object to a leaf node.
Floating-point greater-than or equal.
virtual size_t nChildren() const override
Number of arguments.
virtual VisitAction depthFirstTraversal(Visitor &) const override
Traverse the expression.
bool isFloatingPointConstant() const
True if this epxression is a floating-point constant.
virtual bool isConstant() const =0
True if this expression is a constant.
virtual bool isVariable2() const override
True if this expression is a variable.
virtual Sawyer::Optional< int64_t > toSigned() const override
The signed integer value of the expression.
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 override
Rewrite the entire expression to something simpler.
Compare two expressions for STL containers.
virtual Sawyer::Optional< uint64_t > toUnsigned() const =0
The unsigned integer value of the expression.
LeafPtr makeConstant(const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr makeIsNeg(const Ptr &a, 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.
Base class for visiting nodes during expression traversal.
virtual Sawyer::Optional< int64_t > toSigned() const override
The signed integer value of the expression.
Ptr makeSignedMin(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeGt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual uint64_t nNodes() const override
Computes the size of an expression by counting the number of nodes.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
std::string toString() const
Convert expression to string.
Floating-point round to integer as FP type.
virtual size_t nChildren() const override
Number of arguments.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool isMemoryExpr() const
True if this expression is of a memory type.
Ptr makeReinterpret(const Ptr &a, const Type &b, 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.
virtual Node * childRaw(size_t idx) const override
Argument.
Ptr makeSignedMul(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeXor(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isFloatingPointVariable() const
Is this node a floating-point variable?
void print(std::ostream &o) const
Print the expression to a stream.
const boost::any & userData() const
Property: User-defined data.
InteriorPtr idempotent(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies idempotent operators.
Like CMT_AFTER, but show comments instead of variable names.
Ptr makeIsInfinite(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
bool matchAddVariableConstant(LeafPtr &variable, LeafPtr &constant) const
Determine whether an expression is a variable plus a constant.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Leaf constructor.
LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Operator
Operators for interior nodes of the expression tree.
Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite expression by substituting subexpressions.
Ptr makeSignedMod(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 makeSignedGt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeSignedLt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
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.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
static LeafPtr createVariable(const Type &, const std::string &comment="", unsigned flags=0)
Create a new variable.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual VisitAction depthFirstTraversal(Visitor &) const override
Traverse the expression.
Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver=SmtSolverPtr())
On-the-fly substitutions.
size_t max_depth
If non-zero, then replace deep parts of expressions with "...".
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool isFloatingPointExpr() const
True if this expression is of a floating-point type.
Base class for symbolic expression nodes.
Hash hashval_
Optional hash used as a quick way to indicate that two expressions are different. ...
Sawyer::SharedPointer< Leaf > LeafPtr
Reference counting pointer.
LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual void print(std::ostream &, Formatter &) const =0
Print the expression to a stream.
bool isMemoryVariable() const
Is this node a memory variable?
Ptr simplifyTop(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies the specified interior node.
Small object support.
Definition: SmallObject.h:19
static Type floatingPoint(size_t exponentWidth, size_t significandWidth)
Create a new floating-point type.
static Type integer(size_t nBits)
Create a new integer type.
virtual bool isVariable2() const override
True if this expression is a variable.
virtual const Nodes & children() const override
Arguments.
bool isFloatingPointNan() const
True if this expression is a floating-point NaN constant.
Ptr foldConstants(const Simplifier &)
Perform constant folding.
ShowComments show_comments
Show node comments when printing?
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isIntegerConstant() const
True if this expression is an integer constant.
virtual VisitAction depthFirstTraversal(Visitor &) const =0
Traverse the expression.
LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Main namespace for the ROSE library.
Ptr makeLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
static const unsigned RESERVED_FLAGS
These flags are reserved for use within ROSE.
bool isScalar() const
Check whether expression is scalar.
bool isIntegerVariable() const
Is this node an integer variable?
InteriorPtr isInteriorNode() const
Dynamic cast of this object to an interior node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeEq(const Ptr &a, const Ptr &b, 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.
Ptr makeSignedDiv(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.
void printAsUnsigned(std::ostream &o, Formatter &f) const
Prints an integer constant interpreted as an unsigned value.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions must be equal (cannot be unequal).
bool operator!=(const Type &other) const
Type equality.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions might be equal, but not necessarily be equal.
Ptr makeMod(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeOr(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Interior * isInteriorNodeRaw() const
Dynamic cast of this object to an interior node.
bool isValid() const
Check whether this object is valid.
Ptr identity(uint64_t ident, const SmtSolverPtr &solver=SmtSolverPtr())
Removes identity arguments.
Ptr makeIsPos(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Leaf * isLeafNodeRaw() const
Dynamic cast of this object to a leaf node.
size_t significandWidth() const
Property: Significand width.
Interpret the value as a different type without converting.
Ptr involutary()
Simplifies involutary operators.
bool isMemoryVariable() const
True if this expression is a memory state variable.
SharedPointer< Node > sharedFromThis()
Create a shared pointer from this.
Ptr makeLt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Operator-specific simplification methods.
TypeClass typeClass() const
Property: Type class.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
WithFormatter operator+(Formatter &fmt)
Combines a node with a formatter for printing.
virtual bool isEquivalentTo(const Ptr &other) override
Tests two expressions for structural equivalence.
virtual void print(std::ostream &, Formatter &) const override
Print the expression to a stream.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr())=0
Returns true if two expressions must be equal (cannot be unequal).
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) override
Substitute one value for another.
bool isScalarVariable() const
True if this expression is a scalar variable.
static Type memory(size_t addressWidth, size_t valueWidth)
Create a new memory type.
Ptr makeSignedMax(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Shift right, introducing zeros at msb.
virtual int compareStructure(const Ptr &other)=0
Compare two expressions structurally for sorting.
Ptr makeMax(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
void userData(boost::any &data)
Property: User-defined data.
virtual Sawyer::Optional< int64_t > toSigned() const =0
The signed integer value of the expression.
Ptr renameVariables(ExprExprHashMap &index, size_t &nextVariableId, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite using lowest numbered variable names.
virtual uint64_t nNodes() const override
Computes the size of an expression by counting the number of nodes.
bool show_flags
Show user-defined flags inside square brackets.
Ptr makeConcat(const Ptr &hi, const Ptr &lo, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeIsNan(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
size_t exponentWidth() const
Property: Exponent width.
Ptr makeInvert(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
static boost::logic::tribool(* mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr &)
User-supplied predicate to augment alias checking.
size_t nBits() const
Property: Total width of values.
void assertAcyclic() const
Asserts that expressions are acyclic.
Ptr makeSqrt(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
static Ptr instance(Operator op, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Create a new expression node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Creates SharedPointer from this.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool isConstant() const override
True if this expression is a constant.
Write (update) memory with a new value.
virtual uint64_t nNodes() const =0
Computes the size of an expression by counting the number of nodes.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
InteriorPtr commutative()
Simplifies commutative operators by sorting arguments.
virtual void print(std::ostream &, Formatter &) const override
Print the expression to a stream.
Ptr newFlags(unsigned flags) const
Sets flags.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Flag
Flag to pass as type stringification style.
std::set< LeafPtr > getVariables() const
Returns the variables appearing in the expression.
Ptr makeIsSignedPos(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual int compareStructure(const Ptr &other) override
Compare two expressions structurally for sorting.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
virtual bool isVariable2() const =0
True if this expression is a variable.
Ptr makeSignedLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isIntegerExpr() const
True if this expression is of an integer type.
Shift left, introducing ones at lsb.
virtual size_t nChildren() const =0
Number of arguments.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
void adjustWidth(const Type &)
Adjust width based on operands.
InteriorPtr associative()
Simplifies non-associative operators by flattening the specified interior node with its children that...
Ptr makeLssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t nBits() const
Property: Number of significant bits.
Ptr makeSet(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isHashed() const
Returns true if this node has a hash value computed and cached.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const
Constant folding.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions might be equal, but not necessarily be equal.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool isEquivalentTo(const Ptr &other)=0
Tests two expressions for structural equivalence.
virtual const Ptr & child(size_t idx) const override
Argument.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
uint64_t Hash
Hash of symbolic expression.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions must be equal (cannot be unequal).
bool isFloatingPointNan() const
Is this node a floating-point NaN constant?
const uint64_t MAX_NNODES
Maximum number of nodes that can be reported.
bool serializeVariableIds
Whether to serialize variable IDs.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool isConstant() const override
True if this expression is a constant.
Ptr makeSignExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual const Node * childRaw(size_t) const override
Argument.
Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver=SmtSolverPtr())
Simplify an interior node.
Ptr makeRol(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool use_hexadecimal
Show values in hexadecimal and decimal rather than just decimal.
Ptr makeMssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual int compareStructure(const Ptr &other) override
Compare two expressions structurally for sorting.
bool add_renames
Add additional entries to the renames as variables are encountered?
Ptr makeZerop(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Operator getOperator() const override
Operator for interior nodes.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr())=0
Substitute one value for another.
WithFormatter withFormat(Formatter &fmt)
Combines a node with a formatter for printing.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr makeIsSubnorm(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool do_rename
Use the renames map to rename variables to shorter names?
boost::any userData_
Additional user-specified data.
Base class for reference counted objects.
Definition: SharedObject.h:64
virtual const Node * childRaw(size_t idx) const =0
Argument.
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 makeShr1(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const
Rewrite the entire expression to something simpler.
Ptr unaryNoOp()
Replaces a binary operator with its only argument.
virtual const Ptr & child(size_t idx) const =0
Argument.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
virtual Sawyer::Optional< uint64_t > toUnsigned() const override
The unsigned integer value of the expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
void comment(const std::string &s)
Property: Comment.
Ptr setToIte(const Ptr &, const SmtSolverPtr &solver=SmtSolverPtr(), const LeafPtr &var=LeafPtr())
Convert a set to an ite expression.
InteriorPtr isOperator(Operator) const
True (non-null) if this node is the specified operator.
Controls formatting of expression trees when printing.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
Ptr makeShl1(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeShl0(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Sawyer::Optional< uint64_t > toUnsigned() const override
The unsigned integer value of the expression.
uint64_t nNodesUnique() const
Number of unique nodes in expression.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
Leaf node of an expression tree for instruction semantics.
const std::string & comment() const
Property: Comment.
Ptr makeRor(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool show_type
Show data type inside square brackets.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeIsNorm(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
LeafPtr makeVariable(const Type &, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeShr0(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
For a pre-order depth-first visit, do not descend into children.
virtual const Nodes & children() const override
Arguments.
LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Interior node of an expression tree for instruction semantics.
bool isEmpty() const
Determines if the vector is empty.
Definition: BitVector.h:184
bool isScalarExpr() const
True if the expression is a scalar type.
virtual bool isEquivalentTo(const Ptr &other) override
Tests two expressions for structural equivalence.
API and storage for attributes.
Definition: Attribute.h:208
Ptr poisonNan(const SmtSolverPtr &solver=SmtSolverPtr())
Returns NaN if any argument is NaN.
std::string toString(TypeStyle::Flag style=TypeStyle::FULL) const
Print the type to a string.
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 makeSignedGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeDiv(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Represents no value.
Definition: Optional.h:32
Shift right, introducing ones at msb.
Shift left, introducing zeros at lsb.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
Ptr makeAnd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Sawyer::Container::Set< Ptr, ExpressionLessp > ExpressionSet
Set of expressions ordered by hash.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr additiveNesting(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies nested shift-like operators.
Base class for all ROSE exceptions.
Definition: Rose/Exception.h:9
virtual Operator getOperator() const override
Operator for interior nodes.
void adjustBitFlags(unsigned extraFlags)
Adjust user-defined bit flags.
std::vector< Ptr > findCommonSubexpressions() const
Find common subexpressions.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeAdd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual const Nodes & children() const =0
Arguments.
uint64_t nNodes(InputIterator begin, InputIterator end)
Counts the number of nodes.
virtual const Ptr & child(size_t idx) const override
Argument.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
unsigned flags() const
Property: User-defined bit flags.
bool operator<(const Type &other) const
Type comparison.
Ptr makeMin(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t addressWidth() const
Property: Width of memory addresses.
Ptr makeNe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isIntegerVariable() const
True if this expression is an integer variable.
std::string toString() const
Returns a string for the leaf.
const Sawyer::Container::BitVector & bits() const
Property: Bits stored for numeric constants.
Container associating values with keys.
Definition: Sawyer/Map.h:66
Ptr makeRead(const Ptr &mem, const Ptr &addr, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
uint64_t nNodesUnique(InputIterator begin, InputIterator end)
Counts the number of unique nodes.
RenameMap renames
Map for renaming variables to use smaller integers.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.
Sawyer::Optional< uint64_t > variableId() const
Variable ID number.
bool operator==(const Type &other) const
Type equality.
size_t domainWidth() const
Property: Width for memory expressions.