ROSE  0.11.50.0
SymbolicExpr.h
1 #ifndef ROSE_BinaryAnalysis_SymbolicExpr_H
2 #define ROSE_BinaryAnalysis_SymbolicExpr_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 
38 class SmtSolver;
39 using SmtSolverPtr = std::shared_ptr<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 
868 class Simplifier {
869 public:
870  virtual ~Simplifier() {}
871 
875  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
876  return Ptr();
877  }
878 
881  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
882  return Ptr();
883  }
884 };
885 
887  size_t operator()(const Ptr &expr) const {
888  return expr->hash();
889  }
890 };
891 
893  bool operator()(const Ptr &a, const Ptr &b) const {
894  return a->isEquivalentTo(b);
895  }
896 };
897 
900 public:
901  bool operator()(const Ptr &a, const Ptr &b) const;
902 };
903 
905 class ExprExprHashMap: public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
906  ExprExprHashMapHasher, ExprExprHashMapCompare> {
907 public:
908  ExprExprHashMap invert() const;
909 };
910 
913 
914 
916 // Simplification
918 
920  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
921  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
922 };
924  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
925  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
926 };
928  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
929 };
931  virtual Ptr 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 fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
940 };
942  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
943 };
945  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
946  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
947 };
949  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
950 };
952  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
953 };
955  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
956 };
958  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
959 };
961  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
962 };
964  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
965 };
967  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
968 };
970  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
971 };
973  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
974 };
976  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
977 };
979  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
980 };
982  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
983 };
985  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
986 };
988  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
989 };
991  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
992 };
994  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
995 };
997  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
998 };
1000  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1001 };
1003  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1004 };
1006  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1007 };
1009  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1010 };
1012  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1013 };
1015  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1016 };
1018  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1019 };
1021  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1022 };
1024  bool newbits;
1025  ShiftSimplifier(bool newbits): newbits(newbits) {}
1026  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
1027 };
1029  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1030  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1031 };
1033  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
1034  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1035 };
1037  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1038 };
1040  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1041 };
1043  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
1044 };
1045 
1046 
1047 
1049 // Interior Nodes
1051 
1058 class Interior: public Node {
1059 private:
1060  Operator op_;
1061  Nodes children_;
1062  uint64_t nnodes_; // total number of nodes; self + children's nnodes
1063 
1064  //--------------------------------------------------------
1065  // Serialization
1066  //--------------------------------------------------------
1067 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1068 private:
1069  friend class boost::serialization::access;
1070 
1071  template<class S>
1072  void serialize(S &s, const unsigned /*version*/) {
1073  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1074  s & BOOST_SERIALIZATION_NVP(op_);
1075  s & BOOST_SERIALIZATION_NVP(children_);
1076  s & BOOST_SERIALIZATION_NVP(nnodes_);
1077  }
1078 #endif
1079 
1080  //--------------------------------------------------------
1081  // Real constructors
1082  //--------------------------------------------------------
1083 private:
1084  Interior(); // needed for serialization
1085  // Only constructs, does not simplify.
1086  Interior(const Type&, Operator, const Nodes &arguments, const std::string &comment, unsigned flags);
1087 
1088  //--------------------------------------------------------
1089  // Allocating constructors
1090  //--------------------------------------------------------
1091 public:
1095  static Ptr instance(Operator op, const Ptr &a,
1096  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1097  static Ptr instance(const Type &type, Operator op, const Ptr &a,
1098  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1099  static Ptr instance(Operator op, const Ptr &a, const Ptr &b,
1100  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1101  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b,
1102  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1103  static Ptr instance(Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1104  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1105  static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1106  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1107  static Ptr instance(Operator op, const Nodes &arguments,
1108  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1109  static Ptr instance(const Type &type, Operator op, const Nodes &arguments,
1110  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1113  //--------------------------------------------------------
1114  // Overrides
1115  //--------------------------------------------------------
1116 public:
1117  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1118  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1119  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1120  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1121  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1122  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1123  virtual uint64_t nNodes() const ROSE_OVERRIDE { return nnodes_; }
1124  virtual const Nodes& children() const ROSE_OVERRIDE { return children_; }
1125  virtual Operator getOperator() const ROSE_OVERRIDE { return op_; }
1126  virtual size_t nChildren() const ROSE_OVERRIDE { return children_.size(); }
1127  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return idx < children_.size() ? children_[idx] : Ptr(); }
1128  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1129  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE { return Sawyer::Nothing(); }
1130  virtual bool isConstant() const ROSE_OVERRIDE { return false; }
1131  virtual bool isVariable2() const ROSE_OVERRIDE { return false; }
1132 
1133  //--------------------------------------------------------
1134  // Simplification
1135  //--------------------------------------------------------
1136 public:
1140  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
1141 
1144  Ptr foldConstants(const Simplifier&);
1145 
1150  InteriorPtr associative();
1151 
1156  InteriorPtr commutative();
1157 
1164  InteriorPtr idempotent(const SmtSolverPtr &solver = SmtSolverPtr());
1165 
1169  Ptr involutary();
1170 
1174  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
1175 
1179  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
1180 
1185  Ptr poisonNan(const SmtSolverPtr &solver = SmtSolverPtr());
1186 
1188  Ptr unaryNoOp();
1189 
1193  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
1194 
1195  //--------------------------------------------------------
1196  // Functions specific to internal nodes
1197  //--------------------------------------------------------
1198 public:
1199  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1200 
1201 protected:
1203  void addChild(const Ptr &child);
1204 
1208  void adjustWidth(const Type&);
1209 
1212  void adjustBitFlags(unsigned extraFlags);
1213 };
1214 
1215 
1217 // Leaf Nodes
1219 
1223 class Leaf: public Node {
1224 private:
1225  Sawyer::Container::BitVector bits_; // Value for constants if size > 0
1226  uint64_t name_; // Variable ID for variables when bits_.size() == 0
1227 
1228  //--------------------------------------------------------
1229  // Serialization
1230  //--------------------------------------------------------
1231 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1232 private:
1233  friend class boost::serialization::access;
1234 
1235  template<class S>
1236  void save(S &s, const unsigned /*version*/) const {
1237  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1238  s & BOOST_SERIALIZATION_NVP(bits_);
1239  s & BOOST_SERIALIZATION_NVP(name_);
1240  }
1241 
1242  template<class S>
1243  void load(S &s, const unsigned /*version*/) {
1244  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1245  s & BOOST_SERIALIZATION_NVP(bits_);
1246  s & BOOST_SERIALIZATION_NVP(name_);
1247  nextNameCounter(name_);
1248  }
1249 
1250  BOOST_SERIALIZATION_SPLIT_MEMBER();
1251 #endif
1252 
1253  //--------------------------------------------------------
1254  // Private constructors. Use create methods instead.
1255  //--------------------------------------------------------
1256 private:
1257  Leaf()
1258  : name_(0) {}
1259  explicit Leaf(const std::string &comment, unsigned flags=0)
1260  : Node(comment, flags), name_(0) {}
1261 
1262  // Allocating constructors.
1263 public:
1265  static LeafPtr createVariable(const Type&,
1266  const std::string &comment = "", unsigned flags = 0);
1267 
1269  static LeafPtr createVariable(const Type&, const uint64_t id,
1270  const std::string &comment = "", unsigned flags = 0);
1271 
1273  static LeafPtr createConstant(const Type&, const Sawyer::Container::BitVector&,
1274  const std::string &comment = "", unsigned flags = 0);
1275 
1276  //--------------------------------------------------------
1277  // Override base class implementations
1278  //--------------------------------------------------------
1279 public:
1280  virtual size_t nChildren() const ROSE_OVERRIDE { return 0; }
1281  virtual Ptr child(size_t idx) const ROSE_OVERRIDE { return Ptr(); }
1282  virtual const Nodes& children() const ROSE_OVERRIDE;
1283  virtual Operator getOperator() const ROSE_OVERRIDE { return OP_NONE; }
1284  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1285  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1286  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1287  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1288  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1289  virtual VisitAction depthFirstTraversal(Visitor&) const ROSE_OVERRIDE;
1290  virtual uint64_t nNodes() const ROSE_OVERRIDE { return 1; }
1291  virtual Sawyer::Optional<uint64_t> toUnsigned() const ROSE_OVERRIDE;
1292  virtual Sawyer::Optional<int64_t> toSigned() const ROSE_OVERRIDE;
1293  virtual bool isConstant() const ROSE_OVERRIDE { return !bits_.isEmpty(); }
1294  virtual bool isVariable2() const ROSE_OVERRIDE { return !isConstant(); }
1295  virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
1296 
1297  //--------------------------------------------------------
1298  // Leaf-specific methods
1299  //--------------------------------------------------------
1300 public:
1302  const Sawyer::Container::BitVector& bits() const;
1303 
1305  bool isIntegerVariable() const {
1306  return type().typeClass() == Type::INTEGER && !isConstant();
1307  }
1308 
1311  return type().typeClass() == Type::FP && !isConstant();
1312  }
1313 
1315  bool isFloatingPointNan() const;
1316 
1318  bool isMemoryVariable() const {
1319  return type().typeClass() == Type::MEMORY && !isConstant();
1320  }
1321 
1326  uint64_t nameId() const;
1327 
1332  std::string toString() const;
1333 
1335  void printAsSigned(std::ostream&, Formatter&, bool asSigned = true) const;
1336 
1338  void printAsUnsigned(std::ostream &o, Formatter &f) const {
1339  printAsSigned(o, f, false);
1340  }
1341 
1342 private:
1343  // Obtain or register a name ID
1344  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1345 };
1346 
1348 // Factories
1350 
1356 LeafPtr makeVariable(const Type&, const std::string &comment="", unsigned flags=0);
1357 LeafPtr makeVariable(const Type&, uint64_t id, const std::string &comment="", unsigned flags=0);
1358 LeafPtr makeConstant(const Type&, const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1359 LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0);
1360 LeafPtr makeIntegerVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0);
1361 LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0);
1362 LeafPtr makeIntegerConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1363 LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0);
1364 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1365 LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
1366 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1367 LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, uint64_t id, const std::string &comment="", unsigned flags=0);
1368 LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0);
1369 LeafPtr makeFloatingPointConstant(double, const std::string &comment="", unsigned flags=0);
1370 LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
1379 Ptr makeAdd(const Ptr&a, const Ptr &b,
1380  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1381 Ptr makeAsr(const Ptr &sa, const Ptr &a,
1382  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1383 Ptr makeAnd(const Ptr &a, const Ptr &b,
1384  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1385 Ptr makeOr(const Ptr &a, const Ptr &b,
1386  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1387 Ptr makeXor(const Ptr &a, const Ptr &b,
1388  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1389 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1390  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1391 Ptr makeConvert(const Ptr &a, const Type &b,
1392  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1393 Ptr makeEq(const Ptr &a, const Ptr &b,
1394  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1395 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1396  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1397 Ptr makeInvert(const Ptr &a,
1398  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1399 Ptr makeIsInfinite(const Ptr &a,
1400  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1401 Ptr makeIsNan(const Ptr &a,
1402  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1403 Ptr makeIsNeg(const Ptr &a,
1404  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1405 Ptr makeIsNorm(const Ptr &a,
1406  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1407 Ptr makeIsPos(const Ptr &a,
1408  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1409 Ptr makeIsSubnorm(const Ptr &a,
1410  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1411 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1412  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1413 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1414  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1415 Ptr makeLssb(const Ptr &a,
1416  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1417 Ptr makeMax(const Ptr &a, const Ptr &b,
1418  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1419 Ptr makeMin(const Ptr &a, const Ptr &b,
1420  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1421 Ptr makeMssb(const Ptr &a,
1422  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1423 Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c,
1424  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1425 Ptr makeNe(const Ptr &a, const Ptr &b,
1426  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1427 Ptr makeNegate(const Ptr &a,
1428  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1429 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1430  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1431 Ptr makeReinterpret(const Ptr &a, const Type &b,
1432  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1433 Ptr makeRol(const Ptr &sa, const Ptr &a,
1434  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1435 Ptr makeRor(const Ptr &sa, const Ptr &a,
1436  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1437 Ptr makeRound(const Ptr &a,
1438  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1439 Ptr makeSet(const Ptr &a, const Ptr &b,
1440  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1441 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1442  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1443 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1444  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1445 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1446  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1447 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1448  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1449 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1450  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1451 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1452  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1453 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1454  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1455 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1456  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1457 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1458  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1459 Ptr makeIsSignedPos(const Ptr &a,
1460  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1461 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1462  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1463 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1464  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1465 Ptr makeSignedMax(const Ptr &a, const Ptr &b,
1466  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1467 Ptr makeSignedMin(const Ptr &a, const Ptr &b,
1468  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1469 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1470  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1471 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1472  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1473 Ptr makeSqrt(const Ptr &a,
1474  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1475 Ptr makeDiv(const Ptr &a, const Ptr &b,
1476  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1477 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1478  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1479 Ptr makeGe(const Ptr &a, const Ptr &b,
1480  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1481 Ptr makeGt(const Ptr &a, const Ptr &b,
1482  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1483 Ptr makeLe(const Ptr &a, const Ptr &b,
1484  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1485 Ptr makeLt(const Ptr &a, const Ptr &b,
1486  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1487 Ptr makeMod(const Ptr &a, const Ptr &b,
1488  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1489 Ptr makeMul(const Ptr &a, const Ptr &b,
1490  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1491 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1492  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1493 Ptr makeZerop(const Ptr &a,
1494  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1498 // Miscellaneous functions
1501 
1502 
1503 std::ostream& operator<<(std::ostream &o, const Node&);
1504 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1505 
1507 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1508 
1513 Hash hash(const std::vector<Ptr>&);
1514 
1519 template<typename InputIterator>
1520 uint64_t
1521 nNodes(InputIterator begin, InputIterator end) {
1522  uint64_t total = 0;
1523  for (InputIterator ii=begin; ii!=end; ++ii) {
1524  uint64_t n = (*ii)->nnodes();
1525  if (MAX_NNODES==n)
1526  return MAX_NNODES;
1527  if (total + n < total)
1528  return MAX_NNODES;
1529  total += n;
1530  }
1531  return total;
1532 }
1533 
1538 template<typename InputIterator>
1539 uint64_t
1540 nNodesUnique(InputIterator begin, InputIterator end)
1541 {
1542  struct T1: Visitor {
1543  typedef std::set<const Node*> SeenNodes;
1544 
1545  SeenNodes seen; // nodes that we've already seen, and the subtree size
1546  uint64_t nUnique; // number of unique nodes
1547 
1548  T1(): nUnique(0) {}
1549 
1550  VisitAction preVisit(const Ptr &node) {
1551  if (seen.insert(getRawPointer(node)).second) {
1552  ++nUnique;
1553  return CONTINUE; // this node has not been seen before; traverse into children
1554  } else {
1555  return TRUNCATE; // this node has been seen already; skip over the children
1556  }
1557  }
1558 
1559  VisitAction postVisit(const Ptr &node) {
1560  return CONTINUE;
1561  }
1562  } visitor;
1563 
1564  VisitAction status = CONTINUE;
1565  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1566  status = (*ii)->depthFirstTraversal(visitor);
1567  return visitor.nUnique;
1568 }
1569 
1576 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1577 
1578 template<typename InputIterator>
1579 std::vector<Ptr>
1580 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1581  typedef Sawyer::Container::Map<Ptr, size_t> NodeCounts;
1582  struct T1: Visitor {
1583  NodeCounts nodeCounts;
1584  std::vector<Ptr> result;
1585 
1586  VisitAction preVisit(const Ptr &node) ROSE_OVERRIDE {
1587  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1588  if (2 == ++nSeen)
1589  result.push_back(node);
1590  return nSeen>1 ? TRUNCATE : CONTINUE;
1591  }
1592 
1593  VisitAction postVisit(const Ptr&) ROSE_OVERRIDE {
1594  return CONTINUE;
1595  }
1596  } visitor;
1597 
1598  for (InputIterator ii=begin; ii!=end; ++ii)
1599  (*ii)->depthFirstTraversal(visitor);
1600  return visitor.result;
1601 }
1611 template<class Substitution>
1612 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1613  if (!src)
1614  return Ptr(); // no input implies no output
1615 
1616  // Try substituting the whole expression, returning the result.
1617  Ptr dst = subber(src, solver);
1618  ASSERT_not_null(dst);
1619  if (dst != src)
1620  return dst;
1621 
1622  // Try substituting all the subexpressions.
1623  InteriorPtr inode = src->isInteriorNode();
1624  if (!inode)
1625  return src;
1626  bool anyChildChanged = false;
1627  Nodes newChildren;
1628  newChildren.reserve(inode->nChildren());
1629  BOOST_FOREACH (const Ptr &child, inode->children()) {
1630  Ptr newChild = substitute(child, subber, solver);
1631  if (newChild != child)
1632  anyChildChanged = true;
1633  newChildren.push_back(newChild);
1634  }
1635  if (!anyChildChanged)
1636  return src;
1637 
1638  // Some subexpression changed, so build a new expression
1639  return Interior::instance(inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1640 }
1641 
1642 } // namespace
1643 
1644 using SymbolicExprPtr = SymbolicExpr::Ptr;
1645 
1646 } // namespace
1647 } // namespace
1648 
1649 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1650 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1651 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1652 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Type, 1);
1653 BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpr::Node, 1);
1654 #endif
1655 
1656 #endif
1657 #endif
Ptr renameVariables(ExprExprHashMap &index, size_t &nextVariableId, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite using lowest numbered variable names.
Operator-specific simplification methods.
Definition: SymbolicExpr.h:868
virtual int compareStructure(const Ptr &other) ROSE_OVERRIDE
Compare two expressions structurally for sorting.
const std::string & comment() const
Property: Comment.
Definition: SymbolicExpr.h:698
bool add_renames
Add additional entries to the renames as variables are encountered?
Definition: SymbolicExpr.h:185
Sawyer::Optional< uint64_t > variableId() const
Variable ID number.
bool isFloatingPointExpr() const
True if this expression is of a floating-point type.
Definition: SymbolicExpr.h:617
bool isHashed() const
Returns true if this node has a hash value computed and cached.
Definition: SymbolicExpr.h:797
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.
Bitwise exclusive disjunction.
Definition: SymbolicExpr.h:114
ShowComments show_comments
Show node comments when printing?
Definition: SymbolicExpr.h:183
Ordered set of values.
Definition: Set.h:52
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.
Definition: SymbolicExpr.h:156
std::string comment_
Optional comment.
Definition: SymbolicExpr.h:470
virtual size_t nChildren() const ROSE_OVERRIDE
Number of arguments.
RenameMap renames
Map for renaming variables to use smaller integers.
Definition: SymbolicExpr.h:189
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 "...".
Definition: SymbolicExpr.h:187
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.
Definition: SymbolicExpr.h:313
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.
Definition: SymbolicExpr.h:171
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.
Definition: SymbolicExpr.h:335
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.
Definition: SymbolicExpr.h:196
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.
Definition: SymbolicExpr.h:472
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. ...
Definition: SymbolicExpr.h:471
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.
Definition: SymbolicExpr.h:125
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.
Definition: SymbolicExpr.h:905
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.
Definition: SymbolicExpr.h:881
Shift left, introducing zeros at lsb.
Definition: SymbolicExpr.h:97
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.
Definition: SymbolicExpr.h:642
unsigned flags() const
Property: User-defined bit flags.
Definition: SymbolicExpr.h:732
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.
Definition: SymbolicExpr.h:716
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.
Definition: SymbolicExpr.h:195
void userData(boost::any &data)
Property: User-defined data.
Definition: SymbolicExpr.h:713
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?
Definition: SymbolicExpr.h:184
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isScalar() const
Check whether expression is scalar.
Definition: SymbolicExpr.h:751
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.
Definition: SymbolicExpr.h:84
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.
Definition: SymbolicExpr.h:686
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.
Sawyer::Container::Set< Ptr, ExpressionLessp > ExpressionSet
Set of expressions ordered by hash.
Definition: SymbolicExpr.h:912
static const unsigned UNSPECIFIED
Value is somehow unspecified.
Definition: SymbolicExpr.h:503
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.
Definition: SymbolicExpr.h:100
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.
Type of symbolic expression.
Definition: SymbolicExpr.h:225
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.
Definition: SymbolicExpr.h:637
bool isScalarExpr() const
True if the expression is a scalar type.
Definition: SymbolicExpr.h:629
Main namespace for the ROSE library.
Floating-point greater-than or equal.
Definition: SymbolicExpr.h:130
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Controls formatting of expression trees when printing.
Definition: SymbolicExpr.h:174
Interpret the value as a different type without converting.
Definition: SymbolicExpr.h:142
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.
Definition: SymbolicExpr.h:99
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.
Definition: SymbolicExpr.h:83
bool operator!=(const Type &other) const
Type equality.
Definition: SymbolicExpr.h:376
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.
Definition: SymbolicExpr.h:55
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.
Definition: SymbolicExpr.h:622
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Name space for the entire library.
Definition: FeasiblePath.h:787
virtual void print(std::ostream &, Formatter &) const ROSE_OVERRIDE
Print the expression to a stream.
Shift left, introducing ones at lsb.
Definition: SymbolicExpr.h:98
Unsigned greater-than-or-equal.
Definition: SymbolicExpr.h:107
InteriorPtr isInteriorNode() const
Dynamic cast of this object to an interior node.
uint64_t nNodesUnique() const
Number of unique nodes in expression.
SharedPointer< Node > sharedFromThis()
Create a shared pointer from this.
TypeClass typeClass() const
Property: Type class.
Definition: SymbolicExpr.h:327
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.
Definition: SymbolicExpr.h:178
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...
static Type none()
Create no type.
Definition: SymbolicExpr.h:285
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.
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.
Definition: SymbolicExpr.h:497
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.
Definition: SymbolicExpr.h:507
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.
Convert from one type to another.
Definition: SymbolicExpr.h:141
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.
Definition: SymbolicExpr.h:527
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.
Definition: SymbolicExpr.h:649
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.
Signed greater-than-or-equal.
Definition: SymbolicExpr.h:95
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.
Definition: SymbolicExpr.h:352
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.
void comment(const std::string &s)
Property: Comment.
Definition: SymbolicExpr.h:701
static const unsigned RESERVED_FLAGS
These flags are reserved for use within ROSE.
Definition: SymbolicExpr.h:494
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Floating-point less-than or equal.
Definition: SymbolicExpr.h:128
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.
Definition: SymbolicExpr.h:266
Sawyer::SharedPointer< Leaf > LeafPtr
Shared-ownership pointer to an expression Leaf node.
Definition: SymbolicExpr.h:165
Base class for reference counted objects.
Definition: SharedObject.h:64
bool isIntegerVariable() const
True if this expression is an integer variable.
Definition: SymbolicExpr.h:669
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.
Definition: SymbolicExpr.h:162
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.
Definition: SymbolicExpr.h:679
static Type integer(size_t nBits)
Create a new integer type.
Definition: SymbolicExpr.h:294
Exceptions for symbolic expressions.
Definition: SymbolicExpr.h:63
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.
Definition: SymbolicExpr.h:186
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.
Definition: SymbolicExpr.h:320
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.
Definition: SymbolicExpr.h:674
Base class for symbolic expression nodes.
Definition: SymbolicExpr.h:462
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.
Definition: SymbolicExpr.h:840
Operator
Operators for interior nodes of the expression tree.
Definition: SymbolicExpr.h:73
Ptr makeMssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Floating-point absolute value.
Definition: SymbolicExpr.h:117
size_t addressWidth() const
Property: Width of memory addresses.
Definition: SymbolicExpr.h:343
bool isEmpty() const
Determines if the vector is empty.
Definition: BitVector.h:184
bool operator==(const Type &other) const
Type equality.
Definition: SymbolicExpr.h:373
Ptr unaryNoOp()
Replaces a binary operator with its only argument.
bool show_flags
Show user-defined flags inside square brackets.
Definition: SymbolicExpr.h:191
API and storage for attributes.
Definition: Attribute.h:208
size_t significandWidth() const
Property: Significand width.
Definition: SymbolicExpr.h:362
Compare two expressions for STL containers.
Definition: SymbolicExpr.h:899
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.
Definition: SymbolicExpr.h:831
WithFormatter operator+(Formatter &fmt)
Combines a node with a formatter for printing.
Definition: SymbolicExpr.h:832
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.
Definition: SymbolicExpr.h:190
Type type() const
Type of value.
Definition: SymbolicExpr.h:517
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.
Definition: SymbolicExpr.h:211
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.
Definition: SymbolicExpr.h:744
Base class for all ROSE exceptions.
Definition: Rose/Exception.h:9
Write (update) memory with a new value.
Definition: SymbolicExpr.h:113
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.
Unsigned less-than-or-equal.
Definition: SymbolicExpr.h:109
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.
Definition: SymbolicExpr.h:612
static Type memory(size_t addressWidth, size_t valueWidth)
Create a new memory type.
Definition: SymbolicExpr.h:301
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.
Definition: SymbolicExpr.h:724
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.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:25
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.
Definition: SymbolicExpr.h:875
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.
Definition: SymbolicExpr.h:197