ROSE  0.9.10.230
BinarySymbolicExpr.h
1 #ifndef ROSE_BinaryAnalysis_SymbolicExpr_H
2 #define ROSE_BinaryAnalysis_SymbolicExpr_H
3 
4 #ifndef __STDC_FORMAT_MACROS
5 #define __STDC_FORMAT_MACROS
6 #endif
7 
8 #include "Map.h"
9 
10 #include <boost/any.hpp>
11 #include <boost/logic/tribool.hpp>
12 #include <boost/serialization/access.hpp>
13 #include <boost/serialization/base_object.hpp>
14 #include <boost/serialization/export.hpp>
15 #include <boost/serialization/split_member.hpp>
16 #include <boost/serialization/string.hpp>
17 #include <boost/serialization/vector.hpp>
18 #include <boost/unordered_map.hpp>
19 #include <cassert>
20 #include <inttypes.h>
21 #include <RoseException.h>
22 #include <Sawyer/Attribute.h>
23 #include <Sawyer/BitVector.h>
24 #include <Sawyer/Set.h>
25 #include <Sawyer/SharedPointer.h>
26 #include <Sawyer/SmallObject.h>
27 #include <set>
28 
29 namespace Rose {
30 namespace BinaryAnalysis {
31 
32 class SmtSolver;
34 
40 namespace SymbolicExpr {
41 
43 // Basic Types
45 
47 class Exception: public Rose::Exception {
48 public:
49  explicit Exception(const std::string &mesg): Rose::Exception(mesg) {}
50 };
51 
57 enum Operator {
101  OP_BV_AND = OP_AND, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
102  OP_BV_OR = OP_OR, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
103  OP_BV_XOR = OP_XOR // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
104 };
105 
106 std::string toStr(Operator);
107 
108 class Node;
109 class Interior;
110 class Leaf;
112 
115 
118 
121 
122 typedef std::vector<Ptr> Nodes;
124 
126 typedef uint64_t Hash;
127 
129 struct Formatter {
134  };
135  Formatter()
137  max_depth(0), cur_depth(0), show_width(true), show_flags(true) {}
139  bool do_rename;
140  bool add_renames;
142  size_t max_depth;
143  size_t cur_depth;
144  RenameMap renames;
145  bool show_width;
146  bool show_flags;
147 };
148 
154 };
155 
160 extern const uint64_t MAX_NNODES; // defined in .C so we don't pollute user namespace with limit macros
161 
166 class Visitor {
167 public:
168  virtual ~Visitor() {}
169  virtual VisitAction preVisit(const Ptr&) = 0;
170  virtual VisitAction postVisit(const Ptr&) = 0;
171 };
172 
173 
174 
176 // Base Node Type
178 
216 class Node
217  : public Sawyer::SharedObject,
218  public Sawyer::SharedFromThis<Node>,
219  public Sawyer::SmallObject,
220  public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
221 protected:
222  size_t nBits_;
223  size_t domainWidth_;
224  unsigned flags_;
225  std::string comment_;
226  Hash hashval_;
227  boost::any userData_;
229 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
230 private:
231  friend class boost::serialization::access;
232 
233  template<class S>
234  void serialize(S &s, const unsigned /*version*/) {
235  s & BOOST_SERIALIZATION_NVP(nBits_);
236  s & BOOST_SERIALIZATION_NVP(domainWidth_);
237  s & BOOST_SERIALIZATION_NVP(flags_);
238  s & BOOST_SERIALIZATION_NVP(comment_);
239  s & BOOST_SERIALIZATION_NVP(hashval_);
240  // s & userData_;
241  }
242 #endif
243 
244 public:
245  // Bit flags
246 
248  static const unsigned RESERVED_FLAGS = 0x0000ffff;
249 
251  static const unsigned INDETERMINATE = 0x00000001;
252 
257  static const unsigned UNSPECIFIED = 0x00000002;
258 
261  static const unsigned BOTTOM = 0x00000004;
262 
263 protected:
264  Node()
265  : nBits_(0), domainWidth_(0), flags_(0), hashval_(0) {}
266  explicit Node(const std::string &comment, unsigned flags=0)
267  : nBits_(0), domainWidth_(0), flags_(flags), comment_(comment), hashval_(0) {}
268 
269 public:
276  static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
277 
283  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
284 
286  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
287 
293  virtual bool isEquivalentTo(const Ptr &other) = 0;
294 
300  virtual int compareStructure(const Ptr &other) = 0;
301 
307  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
308 
316  Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
317 
325  Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
326  const SmtSolverPtr &solver = SmtSolverPtr());
327 
331  virtual bool isNumber() = 0;
332 
337  virtual uint64_t toInt() = 0;
338 
347  const std::string& comment() { return comment_; }
348  void comment(const std::string &s) { comment_ = s; }
358  void userData(boost::any &data) {
359  userData_ = data;
360  }
361  const boost::any& userData() {
362  return userData_;
363  }
369  size_t nBits() { return nBits_; }
370 
375  unsigned flags() { return flags_; }
376 
380  Ptr newFlags(unsigned flags);
381 
385  size_t domainWidth() { return domainWidth_; }
386 
390  bool isScalar() { return 0 == domainWidth_; }
391 
397 
413  virtual uint64_t nNodes() = 0;
414 
416  uint64_t nNodesUnique();
417 
419  std::set<LeafPtr> getVariables();
420 
424  InteriorPtr isInteriorNode() {
425  return sharedFromThis().dynamicCast<Interior>();
426  }
427 
431  LeafPtr isLeafNode() {
432  return sharedFromThis().dynamicCast<Leaf>();
433  }
434 
438  bool isHashed() { return hashval_ != 0; }
439 
442  Hash hash();
443 
444  // used internally to set the hash value
445  void hash(Hash);
446 
449  private:
450  Ptr node;
451  Formatter &formatter;
452  public:
453  WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
454  void print(std::ostream &stream) const { node->print(stream, formatter); }
455  };
456 
478  virtual void print(std::ostream&, Formatter&) = 0;
479  void print(std::ostream &o) { Formatter fmt; print(o, fmt); }
483  void assertAcyclic();
484 
490  std::vector<Ptr> findCommonSubexpressions();
491 
497  bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/);
498 
500  InteriorPtr isOperator(Operator);
501 
502 protected:
503  void printFlags(std::ostream &o, unsigned flags, char &bracket);
504 };
505 
507 class Simplifier {
508 public:
509  virtual ~Simplifier() {}
510 
514  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
515  return Ptr();
516  }
517 
520  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
521  return Ptr();
522  }
523 };
524 
526  size_t operator()(const Ptr &expr) const {
527  return expr->hash();
528  }
529 };
530 
532  bool operator()(const Ptr &a, const Ptr &b) const {
533  return a->isEquivalentTo(b);
534  }
535 };
536 
539 public:
540  bool operator()(const Ptr &a, const Ptr &b);
541 };
542 
544 class ExprExprHashMap: public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
545  ExprExprHashMapHasher, ExprExprHashMapCompare> {
546 public:
547  ExprExprHashMap invert() const;
548 };
549 
552 
553 
555 // Simplification
557 
559  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
560  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
561 };
563  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
564  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
565 };
567  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
568  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
569 };
571  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
572  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
573 };
575  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
576 };
578  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
579 };
581  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
582  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
583 };
585  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
586 };
588  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
589 };
591  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
592 };
594  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
595 };
597  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
598 };
600  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
601 };
603  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
604 };
606  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
607 };
609  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
610 };
612  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
613 };
615  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
616 };
618  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
619 };
621  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
622 };
624  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
625 };
627  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
628 };
630  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
631 };
633  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
634 };
636  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
637 };
639  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
640 };
642  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
643 };
645  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
646 };
648  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
649 };
651  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
652 };
654  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
655 };
657  bool newbits;
658  ShiftSimplifier(bool newbits): newbits(newbits) {}
659  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
660 };
662  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
663  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
664 };
666  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
667  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
668 };
670  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
671 };
673  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
674 };
676  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
677 };
678 
679 
680 
682 // Interior Nodes
684 
689 class Interior: public Node {
690 private:
691  Operator op_;
692  Nodes children_;
693  uint64_t nnodes_; // total number of nodes; self + children's nnodes
694 
695  // Constructors should not be called directly. Use the create() class method instead. This is to help prevent
696  // accidently using pointers to these objects -- all access should be through shared-ownership pointers.
697  Interior(): op_(OP_ADD), nnodes_(1) {} // needed for serialization
698  Interior(size_t nbits, Operator op, const Ptr &a, const std::string &comment="", unsigned flags=0);
699  Interior(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const std::string &comment="", unsigned flags=0);
700  Interior(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c, const std::string &comment="",
701  unsigned flags=0);
702  Interior(size_t nbits, Operator op, const Nodes &children, const std::string &comment="", unsigned flags=0);
703 
704 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
705 private:
706  friend class boost::serialization::access;
707 
708  template<class S>
709  void serialize(S &s, const unsigned /*version*/) {
710  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
711  s & BOOST_SERIALIZATION_NVP(op_);
712  s & BOOST_SERIALIZATION_NVP(children_);
713  s & BOOST_SERIALIZATION_NVP(nnodes_);
714  }
715 #endif
716 
717 public:
729  static Ptr create(size_t nbits, Operator op, const Ptr &a,
730  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
731  InteriorPtr retval(new Interior(nbits, op, a, comment, flags));
732  return retval->simplifyTop(solver);
733  }
734  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b,
735  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
736  InteriorPtr retval(new Interior(nbits, op, a, b, comment, flags));
737  return retval->simplifyTop(solver);
738  }
739  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
740  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
741  InteriorPtr retval(new Interior(nbits, op, a, b, c, comment, flags));
742  return retval->simplifyTop(solver);
743  }
744  static Ptr create(size_t nbits, Operator op, const Nodes &children,
745  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
746  InteriorPtr retval(new Interior(nbits, op, children, comment, flags));
747  return retval->simplifyTop(solver);
748  }
751  /* see superclass, where these are pure virtual */
752  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
753  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
754  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
755  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
756  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
757  virtual bool isNumber() ROSE_OVERRIDE {
758  return false; /*if it's known, then it would have been folded to a leaf*/
759  }
760  virtual uint64_t toInt() ROSE_OVERRIDE { ASSERT_forbid2(true, "not a number"); return 0;}
761  virtual VisitAction depthFirstTraversal(Visitor&) ROSE_OVERRIDE;
762  virtual uint64_t nNodes() ROSE_OVERRIDE { return nnodes_; }
763 
765  size_t nChildren() { return children_.size(); }
766 
768  Ptr child(size_t idx) { ASSERT_require(idx<children_.size()); return children_[idx]; }
769 
773  const Nodes& children() { return children_; }
774 
776  Operator getOperator() { return op_; }
777 
781  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
782 
785  Ptr foldConstants(const Simplifier&);
786 
791  InteriorPtr associative();
792 
797  InteriorPtr commutative();
798 
802  Ptr involutary();
803 
807  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
808 
812  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
813 
815  Ptr unaryNoOp();
816 
820  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
821 
822  virtual void print(std::ostream&, Formatter&) ROSE_OVERRIDE;
823 
824 protected:
826  void addChild(const Ptr &child);
827 
829  void adjustWidth();
830 
833  void adjustBitFlags(unsigned extraFlags);
834 };
835 
836 
838 // Leaf Nodes
840 
844 class Leaf: public Node {
845 private:
846  enum LeafType { CONSTANT, BITVECTOR, MEMORY };
847  LeafType leafType_;
849  uint64_t name_;
851 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
852 private:
853  friend class boost::serialization::access;
854 
855  template<class S>
856  void save(S &s, const unsigned /*version*/) const {
857  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
858  s & BOOST_SERIALIZATION_NVP(leafType_);
859  s & BOOST_SERIALIZATION_NVP(bits_);
860  s & BOOST_SERIALIZATION_NVP(name_);
861  }
862 
863  template<class S>
864  void load(S &s, const unsigned /*version*/) {
865  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
866  s & BOOST_SERIALIZATION_NVP(leafType_);
867  s & BOOST_SERIALIZATION_NVP(bits_);
868  s & BOOST_SERIALIZATION_NVP(name_);
869  nextNameCounter(name_);
870  }
871 
872  BOOST_SERIALIZATION_SPLIT_MEMBER();
873 #endif
874 
875  // Private to help prevent creating pointers to leaf nodes. See create_* methods instead.
876 private:
877  Leaf()
878  : Node(""), leafType_(CONSTANT), name_(0) {}
879  explicit Leaf(const std::string &comment, unsigned flags=0)
880  : Node(comment, flags), leafType_(CONSTANT), name_(0) {}
881 
882 public:
884  static LeafPtr createVariable(size_t nbits, const std::string &comment="", unsigned flags=0);
885 
889  static LeafPtr createExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0);
890 
893  static LeafPtr createInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0);
894 
896  static LeafPtr createConstant(const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0);
897 
899  static LeafPtr createBoolean(bool b, const std::string &comment="", unsigned flags=0) {
900  return createInteger(1, (uint64_t)(b?1:0), comment, flags);
901  }
902 
904  static LeafPtr createMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
905 
909  static LeafPtr createExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="",
910  unsigned flags=0);
911 
912  // from base class
913  virtual bool isNumber() ROSE_OVERRIDE;
914  virtual uint64_t toInt() ROSE_OVERRIDE;
915  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
916  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
917  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
918  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
919  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
920  virtual VisitAction depthFirstTraversal(Visitor&) ROSE_OVERRIDE;
921  virtual uint64_t nNodes() ROSE_OVERRIDE { return 1; }
922 
924  const Sawyer::Container::BitVector& bits();
925 
927  virtual bool isVariable();
928 
930  virtual bool isMemory();
931 
936  uint64_t nameId();
937 
942  std::string toString();
943 
944  // documented in super class
945  virtual void print(std::ostream&, Formatter&) ROSE_OVERRIDE;
946 
948  void printAsSigned(std::ostream&, Formatter&, bool asSigned=true);
949 
951  void printAsUnsigned(std::ostream &o, Formatter &f) {
952  printAsSigned(o, f, false);
953  }
954 
955 private:
956  // Obtain or register a name ID
957  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
958 };
959 
961 // Factories
963 
969 Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0);
970 Ptr makeExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0);
971 Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0);
972 Ptr makeConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
973 Ptr makeBoolean(bool, const std::string &comment="", unsigned flags=0);
974 Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
975 Ptr makeExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
984 Ptr makeAdd(const Ptr&a, const Ptr &b,
985  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
986 Ptr makeBooleanAnd(const Ptr &a, const Ptr &b,
987  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
988  ROSE_DEPRECATED("use makeAnd instead"); // [Robb Matzke 2017-11-21]: deprecated
989 Ptr makeAsr(const Ptr &sa, const Ptr &a,
990  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
991 Ptr makeAnd(const Ptr &a, const Ptr &b,
992  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
993 Ptr makeOr(const Ptr &a, const Ptr &b,
994  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
995 Ptr makeXor(const Ptr &a, const Ptr &b,
996  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
997 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
998  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
999 Ptr makeEq(const Ptr &a, const Ptr &b,
1000  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1001 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1002  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1003 Ptr makeInvert(const Ptr &a,
1004  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1005 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1006  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1007 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1008  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1009 Ptr makeLssb(const Ptr &a,
1010  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1011 Ptr makeMssb(const Ptr &a,
1012  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1013 Ptr makeNe(const Ptr &a, const Ptr &b,
1014  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1015 Ptr makeNegate(const Ptr &a,
1016  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1017 Ptr makeBooleanOr(const Ptr &a, const Ptr &b,
1018  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1019  ROSE_DEPRECATED("use makeOr instead"); // [Robb Matzke 2017-11-21]: deprecated
1020 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1021  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1022 Ptr makeRol(const Ptr &sa, const Ptr &a,
1023  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1024 Ptr makeRor(const Ptr &sa, const Ptr &a,
1025  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1026 Ptr makeSet(const Ptr &a, const Ptr &b,
1027  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1028 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1029  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1030 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1031  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1032 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1033  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1034 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1035  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1036 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1037  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1038 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1039  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1040 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1041  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1042 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1043  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1044 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1045  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1046 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1047  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1048 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1049  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1050 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1051  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1052 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1053  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1054 Ptr makeDiv(const Ptr &a, const Ptr &b,
1055  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1056 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1057  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1058 Ptr makeGe(const Ptr &a, const Ptr &b,
1059  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1060 Ptr makeGt(const Ptr &a, const Ptr &b,
1061  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1062 Ptr makeLe(const Ptr &a, const Ptr &b,
1063  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1064 Ptr makeLt(const Ptr &a, const Ptr &b,
1065  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1066 Ptr makeMod(const Ptr &a, const Ptr &b,
1067  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1068 Ptr makeMul(const Ptr &a, const Ptr &b,
1069  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1070 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1071  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1072 Ptr makeZerop(const Ptr &a,
1073  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1077 // Miscellaneous functions
1080 
1081 
1082 std::ostream& operator<<(std::ostream &o, Node&);
1083 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1084 
1086 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1087 
1092 Hash hash(const std::vector<Ptr>&);
1093 
1098 template<typename InputIterator>
1099 uint64_t
1100 nNodes(InputIterator begin, InputIterator end) {
1101  uint64_t total = 0;
1102  for (InputIterator ii=begin; ii!=end; ++ii) {
1103  uint64_t n = (*ii)->nnodes();
1104  if (MAX_NNODES==n)
1105  return MAX_NNODES;
1106  if (total + n < total)
1107  return MAX_NNODES;
1108  total += n;
1109  }
1110  return total;
1111 }
1112 
1117 template<typename InputIterator>
1118 uint64_t
1119 nNodesUnique(InputIterator begin, InputIterator end)
1120 {
1121  struct T1: Visitor {
1122  typedef std::set<const Node*> SeenNodes;
1123 
1124  SeenNodes seen; // nodes that we've already seen, and the subtree size
1125  uint64_t nUnique; // number of unique nodes
1126 
1127  T1(): nUnique(0) {}
1128 
1129  VisitAction preVisit(const Ptr &node) {
1130  if (seen.insert(getRawPointer(node)).second) {
1131  ++nUnique;
1132  return CONTINUE; // this node has not been seen before; traverse into children
1133  } else {
1134  return TRUNCATE; // this node has been seen already; skip over the children
1135  }
1136  }
1137 
1138  VisitAction postVisit(const Ptr &node) {
1139  return CONTINUE;
1140  }
1141  } visitor;
1142 
1143  VisitAction status = CONTINUE;
1144  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1145  status = (*ii)->depthFirstTraversal(visitor);
1146  return visitor.nUnique;
1147 }
1148 
1155 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1156 
1157 template<typename InputIterator>
1158 std::vector<Ptr>
1159 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1160  typedef Sawyer::Container::Map<Ptr, size_t> NodeCounts;
1161  struct T1: Visitor {
1162  NodeCounts nodeCounts;
1163  std::vector<Ptr> result;
1164 
1165  VisitAction preVisit(const Ptr &node) ROSE_OVERRIDE {
1166  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1167  if (2 == ++nSeen)
1168  result.push_back(node);
1169  return nSeen>1 ? TRUNCATE : CONTINUE;
1170  }
1171 
1172  VisitAction postVisit(const Ptr&) ROSE_OVERRIDE {
1173  return CONTINUE;
1174  }
1175  } visitor;
1176 
1177  for (InputIterator ii=begin; ii!=end; ++ii)
1178  (*ii)->depthFirstTraversal(visitor);
1179  return visitor.result;
1180 }
1190 template<class Substitution>
1191 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1192  if (!src)
1193  return Ptr(); // no input implies no output
1194 
1195  // Try substituting the whole expression, returning the result.
1196  Ptr dst = subber(src, solver);
1197  ASSERT_not_null(dst);
1198  if (dst != src)
1199  return dst;
1200 
1201  // Try substituting all the subexpressions.
1202  InteriorPtr inode = src->isInteriorNode();
1203  if (!inode)
1204  return src;
1205  bool anyChildChanged = false;
1206  Nodes newChildren;
1207  newChildren.reserve(inode->nChildren());
1208  BOOST_FOREACH (const Ptr &child, inode->children()) {
1209  Ptr newChild = substitute(child, subber, solver);
1210  if (newChild != child)
1211  anyChildChanged = true;
1212  newChildren.push_back(newChild);
1213  }
1214  if (!anyChildChanged)
1215  return src;
1216 
1217  // Some subexpression changed, so build a new expression
1218  return Interior::create(0, inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1219 }
1220 
1221 } // namespace
1222 } // namespace
1223 } // namespace
1224 
1225 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1226 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1227 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1228 #endif
1229 
1230 #endif
Ptr renameVariables(ExprExprHashMap &index, size_t &nextVariableId, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite using lowest numbered variable names.
Operator-specific simplification methods.
virtual int compareStructure(const Ptr &other) ROSE_OVERRIDE
Compare two expressions structurally for sorting.
bool add_renames
Add additional entries to the renames as variables are encountered?
virtual uint64_t toInt() ROSE_OVERRIDE
Property: integer value of expression node.
ShowComments show_comments
Show node comments when printing?
Ordered set of values.
Definition: Set.h:46
Ptr makeSignedLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
std::string comment_
Optional comment.
RenameMap renames
Map for renaming variables to use smaller integers.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
Ptr makeExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0)
Leaf constructor.
size_t max_depth
If non-zero, then replace deep parts of expressions with "...".
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr())=0
Returns true if two expressions must be equal (cannot be unequal).
uint64_t Hash
Hash of symbolic expression.
Leaf node of an expression tree for instruction semantics.
Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Operator getOperator()
Returns the operator.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr())=0
Substitute one value for another.
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.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
Continue the traversal as normal.
Interior node of an expression tree for instruction semantics.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
boost::any userData_
Additional user-specified data.
Hash hashval_
Optional hash used as a quick way to indicate that two expressions are different. ...
virtual bool isNumber() ROSE_OVERRIDE
Returns true if the expression is a known numeric value.
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.
void adjustWidth()
Adjust width based on operands.
virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE
Tests two expressions for structural equivalence.
Mapping from expression to expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isScalar()
Check whether expression is scalar.
static LeafPtr createBoolean(bool b, const std::string &comment="", unsigned flags=0)
Create a new Boolean, a single-bit integer.
InteriorPtr isInteriorNode()
Dynamic cast of this object to an interior node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const
Rewrite the entire expression to something simpler.
Shift left, introducing zeros at lsb.
Ptr makeDiv(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
VisitAction
Return type for visitors.
virtual VisitAction depthFirstTraversal(Visitor &)=0
Traverse the expression.
void userData(boost::any &data)
Property: User-defined data.
bool do_rename
Use the renames map to rename variables to shorter names?
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeLt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Most significant set bit or zero.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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.
STL namespace.
Sawyer::Container::Set< Ptr, ExpressionLessp > ExpressionSet
Set of expressions ordered by hash.
static const unsigned UNSPECIFIED
Value is somehow unspecified.
Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
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.
size_t domainWidth()
Property: Width for memory expressions.
virtual uint64_t toInt()=0
Property: integer value of expression node.
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 makeConstant(const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0)
Leaf 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.
Main namespace for the ROSE library.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Controls formatting of expression trees when printing.
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.
InteriorPtr isOperator(Operator)
True (non-null) if this node is the specified operator.
size_t nBits_
Number of significant bits.
void adjustBitFlags(unsigned extraFlags)
Adjust user-defined bit flags.
virtual void print(std::ostream &, Formatter &) ROSE_OVERRIDE
Print the expression to a stream.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Hash hash()
Returns (and caches) the hash value for this node.
Ptr makeExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Least significant set bit or zero.
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.
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 left, introducing ones at lsb.
Unsigned greater-than-or-equal.
Sawyer::SharedPointer< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
SharedPointer< Node > sharedFromThis()
Create a shared pointer from this.
Ptr makeOr(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t domainWidth_
Width of domain for unary functions.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Like CMT_AFTER, but show comments instead of variable names.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
const boost::any & userData()
Property: User-defined data.
Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr additiveNesting(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies nested shift-like operators.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
InteriorPtr associative()
Simplifies non-associative operators by flattening the specified interior node with its children that...
Ptr makeInvert(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeShr0(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
uint64_t nNodesUnique()
Number of unique nodes in expression.
Ptr makeBooleanAnd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) ROSE_DEPRECATED("use makeAnd instead")
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
static const unsigned INDETERMINATE
Value is somehow indeterminate.
Ptr makeRor(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
Ptr makeConcat(const Ptr &hi, const Ptr &lo, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
void print(std::ostream &o)
Print the expression to a stream.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
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.
std::vector< Ptr > findCommonSubexpressions()
Find common subexpressions.
static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Create a new expression node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr identity(uint64_t ident, const SmtSolverPtr &solver=SmtSolverPtr())
Removes identity arguments.
static boost::logic::tribool(* mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr &)
User-supplied predicate to augment alias checking.
Ptr simplifyTop(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies the specified interior node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeLssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
unsigned flags()
Property: User-defined bit flags.
bool show_width
Show width in bits inside square brackets.
virtual void print(std::ostream &, Formatter &)=0
Print the expression to a stream.
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.
std::set< LeafPtr > getVariables()
Returns the variables appearing in the expression.
Ptr makeRol(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
static Ptr create(size_t nbits, Operator op, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Create a new expression node.
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.
Ptr makeExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual int compareStructure(const Ptr &other)=0
Compare two expressions structurally for sorting.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeMul(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeNe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
SharedPointer< U > dynamicCast() const
Dynamic cast.
static Ptr create(size_t nbits, Operator op, const Nodes &children, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Create a new expression node.
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.
InteriorPtr commutative()
Simplifies commutative operators by sorting arguments.
Ptr makeSignExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeBooleanOr(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) ROSE_DEPRECATED("use makeOr instead")
Interior node constructor.
void comment(const std::string &s)
Property: Comment.
static const unsigned RESERVED_FLAGS
These flags are reserved for use within ROSE.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual bool isNumber()=0
Returns true if the expression is a known numeric value.
Ptr child(size_t idx)
Returns the specified child.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
size_t nBits()
Property: Number of significant bits.
Ptr newFlags(unsigned flags)
Sets flags.
Sawyer::SharedPointer< Leaf > LeafPtr
Shared-ownership pointer to an expression Leaf node.
Base class for reference counted objects.
Definition: SharedObject.h:64
Ptr makeAnd(const Ptr &a, const Ptr &b, 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.
Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr makeBoolean(bool, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Exceptions for symbolic expressions.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool use_hexadecimal
Show values in hexadecimal and decimal rather than just decimal.
Ptr makeSignedLt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Returns true if two expressions must be equal (cannot be unequal).
static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Create a new expression node.
size_t nChildren()
Returns the number of children.
Base class for symbolic expression nodes.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Substitute one value for another.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isHashed()
Returns true if this node has a hash value computed and cached.
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.
Operator
Operators for interior nodes of the expression tree.
Ptr makeMssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool matchAddVariableConstant(LeafPtr &variable, LeafPtr &constant)
Determine whether an expression is a variable plus a constant.
Ptr unaryNoOp()
Replaces a binary operator with its only argument.
bool show_flags
Show user-defined flags inside square brackets.
virtual uint64_t nNodes() ROSE_OVERRIDE
Computes the size of an expression by counting the number of nodes.
API and storage for attributes.
Definition: Attribute.h:208
Compare two expressions for STL containers.
void addChild(const Ptr &child)
Appends child as a new child of this node.
const uint64_t MAX_NNODES
Maximum number of nodes that can be reported.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
WithFormatter withFormat(Formatter &fmt)
Combines a node with a formatter for printing.
WithFormatter operator+(Formatter &fmt)
Combines a node with a formatter for printing.
const Nodes & children()
Property: Children.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Base class for visiting nodes during expression traversal.
Ptr makeGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
const std::string & comment()
Property: Comment.
Base class for all ROSE exceptions.
Definition: RoseException.h:9
void assertAcyclic()
Asserts that expressions are acyclic.
Write (update) memory with a new value.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Returns true if two expressions might be equal, but not necessarily be equal.
LeafPtr isLeafNode()
Dynamic cast of this object to a leaf node.
Ptr makeSignedGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual uint64_t nNodes()=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.
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.
Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver=SmtSolverPtr())
Simplify an interior node.
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 makeAsr(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeZerop(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const
Constant folding.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual VisitAction depthFirstTraversal(Visitor &) ROSE_OVERRIDE
Traverse the expression.
For a pre-order depth-first visit, do not descend into children.