ROSE  0.9.11.56
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 
805  InteriorPtr idempotent(const SmtSolverPtr &solver = SmtSolverPtr());
806 
810  Ptr involutary();
811 
815  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
816 
820  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
821 
823  Ptr unaryNoOp();
824 
828  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
829 
830  virtual void print(std::ostream&, Formatter&) ROSE_OVERRIDE;
831 
832 protected:
834  void addChild(const Ptr &child);
835 
837  void adjustWidth();
838 
841  void adjustBitFlags(unsigned extraFlags);
842 };
843 
844 
846 // Leaf Nodes
848 
852 class Leaf: public Node {
853 private:
854  enum LeafType { CONSTANT, BITVECTOR, MEMORY };
855  LeafType leafType_;
857  uint64_t name_;
859 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
860 private:
861  friend class boost::serialization::access;
862 
863  template<class S>
864  void save(S &s, const unsigned /*version*/) const {
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  }
870 
871  template<class S>
872  void load(S &s, const unsigned /*version*/) {
873  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
874  s & BOOST_SERIALIZATION_NVP(leafType_);
875  s & BOOST_SERIALIZATION_NVP(bits_);
876  s & BOOST_SERIALIZATION_NVP(name_);
877  nextNameCounter(name_);
878  }
879 
880  BOOST_SERIALIZATION_SPLIT_MEMBER();
881 #endif
882 
883  // Private to help prevent creating pointers to leaf nodes. See create_* methods instead.
884 private:
885  Leaf()
886  : Node(""), leafType_(CONSTANT), name_(0) {}
887  explicit Leaf(const std::string &comment, unsigned flags=0)
888  : Node(comment, flags), leafType_(CONSTANT), name_(0) {}
889 
890 public:
892  static LeafPtr createVariable(size_t nbits, const std::string &comment="", unsigned flags=0);
893 
897  static LeafPtr createExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0);
898 
901  static LeafPtr createInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0);
902 
904  static LeafPtr createConstant(const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0);
905 
907  static LeafPtr createBoolean(bool b, const std::string &comment="", unsigned flags=0) {
908  return createInteger(1, (uint64_t)(b?1:0), comment, flags);
909  }
910 
912  static LeafPtr createMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
913 
917  static LeafPtr createExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="",
918  unsigned flags=0);
919 
920  // from base class
921  virtual bool isNumber() ROSE_OVERRIDE;
922  virtual uint64_t toInt() ROSE_OVERRIDE;
923  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
924  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
925  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
926  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
927  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
928  virtual VisitAction depthFirstTraversal(Visitor&) ROSE_OVERRIDE;
929  virtual uint64_t nNodes() ROSE_OVERRIDE { return 1; }
930 
932  const Sawyer::Container::BitVector& bits();
933 
935  virtual bool isVariable();
936 
938  virtual bool isMemory();
939 
944  uint64_t nameId();
945 
950  std::string toString();
951 
952  // documented in super class
953  virtual void print(std::ostream&, Formatter&) ROSE_OVERRIDE;
954 
956  void printAsSigned(std::ostream&, Formatter&, bool asSigned=true);
957 
959  void printAsUnsigned(std::ostream &o, Formatter &f) {
960  printAsSigned(o, f, false);
961  }
962 
963 private:
964  // Obtain or register a name ID
965  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
966 };
967 
969 // Factories
971 
977 Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0);
978 Ptr makeExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0);
979 Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0);
980 Ptr makeConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
981 Ptr makeBoolean(bool, const std::string &comment="", unsigned flags=0);
982 Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
983 Ptr makeExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
992 Ptr makeAdd(const Ptr&a, const Ptr &b,
993  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
994 Ptr makeBooleanAnd(const Ptr &a, const Ptr &b,
995  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
996  ROSE_DEPRECATED("use makeAnd instead"); // [Robb Matzke 2017-11-21]: deprecated
997 Ptr makeAsr(const Ptr &sa, const Ptr &a,
998  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
999 Ptr makeAnd(const Ptr &a, const Ptr &b,
1000  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1001 Ptr makeOr(const Ptr &a, const Ptr &b,
1002  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1003 Ptr makeXor(const Ptr &a, const Ptr &b,
1004  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1005 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1006  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1007 Ptr makeEq(const Ptr &a, const Ptr &b,
1008  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1009 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1010  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1011 Ptr makeInvert(const Ptr &a,
1012  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1013 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1014  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1015 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1016  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1017 Ptr makeLssb(const Ptr &a,
1018  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1019 Ptr makeMssb(const Ptr &a,
1020  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1021 Ptr makeNe(const Ptr &a, const Ptr &b,
1022  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1023 Ptr makeNegate(const Ptr &a,
1024  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1025 Ptr makeBooleanOr(const Ptr &a, const Ptr &b,
1026  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1027  ROSE_DEPRECATED("use makeOr instead"); // [Robb Matzke 2017-11-21]: deprecated
1028 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1029  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1030 Ptr makeRol(const Ptr &sa, const Ptr &a,
1031  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1032 Ptr makeRor(const Ptr &sa, const Ptr &a,
1033  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1034 Ptr makeSet(const Ptr &a, const Ptr &b,
1035  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1036 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1037  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1038 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1039  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1040 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1041  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1042 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1043  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1044 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1045  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1046 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1047  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1048 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1049  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1050 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1051  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1052 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1053  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1054 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1055  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1056 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1057  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1058 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1059  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1060 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1061  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1062 Ptr makeDiv(const Ptr &a, const Ptr &b,
1063  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1064 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1065  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1066 Ptr makeGe(const Ptr &a, const Ptr &b,
1067  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1068 Ptr makeGt(const Ptr &a, const Ptr &b,
1069  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1070 Ptr makeLe(const Ptr &a, const Ptr &b,
1071  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1072 Ptr makeLt(const Ptr &a, const Ptr &b,
1073  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1074 Ptr makeMod(const Ptr &a, const Ptr &b,
1075  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1076 Ptr makeMul(const Ptr &a, const Ptr &b,
1077  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1078 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1079  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1080 Ptr makeZerop(const Ptr &a,
1081  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1085 // Miscellaneous functions
1088 
1089 
1090 std::ostream& operator<<(std::ostream &o, Node&);
1091 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1092 
1094 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1095 
1100 Hash hash(const std::vector<Ptr>&);
1101 
1106 template<typename InputIterator>
1107 uint64_t
1108 nNodes(InputIterator begin, InputIterator end) {
1109  uint64_t total = 0;
1110  for (InputIterator ii=begin; ii!=end; ++ii) {
1111  uint64_t n = (*ii)->nnodes();
1112  if (MAX_NNODES==n)
1113  return MAX_NNODES;
1114  if (total + n < total)
1115  return MAX_NNODES;
1116  total += n;
1117  }
1118  return total;
1119 }
1120 
1125 template<typename InputIterator>
1126 uint64_t
1127 nNodesUnique(InputIterator begin, InputIterator end)
1128 {
1129  struct T1: Visitor {
1130  typedef std::set<const Node*> SeenNodes;
1131 
1132  SeenNodes seen; // nodes that we've already seen, and the subtree size
1133  uint64_t nUnique; // number of unique nodes
1134 
1135  T1(): nUnique(0) {}
1136 
1137  VisitAction preVisit(const Ptr &node) {
1138  if (seen.insert(getRawPointer(node)).second) {
1139  ++nUnique;
1140  return CONTINUE; // this node has not been seen before; traverse into children
1141  } else {
1142  return TRUNCATE; // this node has been seen already; skip over the children
1143  }
1144  }
1145 
1146  VisitAction postVisit(const Ptr &node) {
1147  return CONTINUE;
1148  }
1149  } visitor;
1150 
1151  VisitAction status = CONTINUE;
1152  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1153  status = (*ii)->depthFirstTraversal(visitor);
1154  return visitor.nUnique;
1155 }
1156 
1163 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1164 
1165 template<typename InputIterator>
1166 std::vector<Ptr>
1167 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1168  typedef Sawyer::Container::Map<Ptr, size_t> NodeCounts;
1169  struct T1: Visitor {
1170  NodeCounts nodeCounts;
1171  std::vector<Ptr> result;
1172 
1173  VisitAction preVisit(const Ptr &node) ROSE_OVERRIDE {
1174  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1175  if (2 == ++nSeen)
1176  result.push_back(node);
1177  return nSeen>1 ? TRUNCATE : CONTINUE;
1178  }
1179 
1180  VisitAction postVisit(const Ptr&) ROSE_OVERRIDE {
1181  return CONTINUE;
1182  }
1183  } visitor;
1184 
1185  for (InputIterator ii=begin; ii!=end; ++ii)
1186  (*ii)->depthFirstTraversal(visitor);
1187  return visitor.result;
1188 }
1198 template<class Substitution>
1199 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1200  if (!src)
1201  return Ptr(); // no input implies no output
1202 
1203  // Try substituting the whole expression, returning the result.
1204  Ptr dst = subber(src, solver);
1205  ASSERT_not_null(dst);
1206  if (dst != src)
1207  return dst;
1208 
1209  // Try substituting all the subexpressions.
1210  InteriorPtr inode = src->isInteriorNode();
1211  if (!inode)
1212  return src;
1213  bool anyChildChanged = false;
1214  Nodes newChildren;
1215  newChildren.reserve(inode->nChildren());
1216  BOOST_FOREACH (const Ptr &child, inode->children()) {
1217  Ptr newChild = substitute(child, subber, solver);
1218  if (newChild != child)
1219  anyChildChanged = true;
1220  newChildren.push_back(newChild);
1221  }
1222  if (!anyChildChanged)
1223  return src;
1224 
1225  // Some subexpression changed, so build a new expression
1226  return Interior::create(0, inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1227 }
1228 
1229 } // namespace
1230 } // namespace
1231 } // namespace
1232 
1233 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1234 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1235 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1236 #endif
1237 
1238 #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.
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 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.