ROSE  0.9.10.89
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 <Sawyer/Attribute.h>
22 #include <Sawyer/BitVector.h>
23 #include <Sawyer/Set.h>
24 #include <Sawyer/SharedPointer.h>
25 #include <Sawyer/SmallObject.h>
26 #include <set>
27 
28 namespace Rose {
29 namespace BinaryAnalysis {
30 
31 class SmtSolver;
33 
39 namespace SymbolicExpr {
40 
42 // Basic Types
44 
46 class Exception: public std::runtime_error {
47 public:
48  explicit Exception(const std::string &mesg): std::runtime_error(mesg) {}
49 };
50 
56 enum Operator {
100  OP_BV_AND = OP_AND, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
101  OP_BV_OR = OP_OR, // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
102  OP_BV_XOR = OP_XOR // [Robb Matzke 2017-11-14]: deprecated NO_STRINGIFY
103 };
104 
105 std::string toStr(Operator);
106 
107 class Node;
108 class Interior;
109 class Leaf;
111 
114 
117 
120 
121 typedef std::vector<Ptr> Nodes;
123 
125 typedef uint64_t Hash;
126 
128 struct Formatter {
133  };
134  Formatter()
136  max_depth(0), cur_depth(0), show_width(true), show_flags(true) {}
138  bool do_rename;
139  bool add_renames;
141  size_t max_depth;
142  size_t cur_depth;
143  RenameMap renames;
144  bool show_width;
145  bool show_flags;
146 };
147 
153 };
154 
159 extern const uint64_t MAX_NNODES; // defined in .C so we don't pollute user namespace with limit macros
160 
165 class Visitor {
166 public:
167  virtual ~Visitor() {}
168  virtual VisitAction preVisit(const Ptr&) = 0;
169  virtual VisitAction postVisit(const Ptr&) = 0;
170 };
171 
172 
173 
175 // Base Node Type
177 
215 class Node
216  : public Sawyer::SharedObject,
217  public Sawyer::SharedFromThis<Node>,
218  public Sawyer::SmallObject,
219  public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
220 protected:
221  size_t nBits_;
222  size_t domainWidth_;
223  unsigned flags_;
224  std::string comment_;
225  Hash hashval_;
226  boost::any userData_;
228 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
229 private:
230  friend class boost::serialization::access;
231 
232  template<class S>
233  void serialize(S &s, const unsigned /*version*/) {
234  s & BOOST_SERIALIZATION_NVP(nBits_);
235  s & BOOST_SERIALIZATION_NVP(domainWidth_);
236  s & BOOST_SERIALIZATION_NVP(flags_);
237  s & BOOST_SERIALIZATION_NVP(comment_);
238  s & BOOST_SERIALIZATION_NVP(hashval_);
239  // s & userData_;
240  }
241 #endif
242 
243 public:
244  // Bit flags
245 
247  static const unsigned RESERVED_FLAGS = 0x0000ffff;
248 
250  static const unsigned INDETERMINATE = 0x00000001;
251 
256  static const unsigned UNSPECIFIED = 0x00000002;
257 
260  static const unsigned BOTTOM = 0x00000004;
261 
262 protected:
263  Node()
264  : nBits_(0), domainWidth_(0), flags_(0), hashval_(0) {}
265  explicit Node(const std::string &comment, unsigned flags=0)
266  : nBits_(0), domainWidth_(0), flags_(flags), comment_(comment), hashval_(0) {}
267 
268 public:
275  static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
276 
282  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
283 
285  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
286 
292  virtual bool isEquivalentTo(const Ptr &other) = 0;
293 
299  virtual int compareStructure(const Ptr &other) = 0;
300 
306  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
307 
315  Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
316 
324  Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
325  const SmtSolverPtr &solver = SmtSolverPtr());
326 
330  virtual bool isNumber() = 0;
331 
332  // [Robb P. Matzke 2015-10-08]: deprecated
333  bool is_known() ROSE_DEPRECATED("use isNumber instead") {
334  return isNumber();
335  }
336 
341  virtual uint64_t toInt() = 0;
342 
343  // [Robb P. Matzke 2015-10-08]: deprecated
344  uint64_t get_value() ROSE_DEPRECATED("use toInt instead") {
345  return toInt();
346  }
347 
356  const std::string& comment() { return comment_; }
357  void comment(const std::string &s) { comment_ = s; }
360  // [Robb P. Matzke 2015-10-08]: deprecated
361  const std::string& get_comment() ROSE_DEPRECATED("use 'comment' property instead") {
362  return comment();
363  }
364 
365  // [Robb P. Matzke 2015-10-08]: deprecated
366  void set_comment(const std::string &s) ROSE_DEPRECATED("use 'comment' property instead") {
367  comment(s);
368  }
369 
377  void userData(boost::any &data) {
378  userData_ = data;
379  }
380  const boost::any& userData() {
381  return userData_;
382  }
388  size_t nBits() { return nBits_; }
389 
390  // [Robb P. Matzke 2015-10-08]: deprecated
391  size_t get_nbits() ROSE_DEPRECATED("use 'nBits' property instead") {
392  return nBits();
393  }
394 
399  unsigned flags() { return flags_; }
400 
401  unsigned get_flags() ROSE_DEPRECATED("use 'flags' property instead") {
402  return flags();
403  }
404 
408  Ptr newFlags(unsigned flags);
409 
413  size_t domainWidth() { return domainWidth_; }
414 
418  bool isScalar() { return 0 == domainWidth_; }
419 
425 
426  // [Robb P. Matzke 2015-10-08]: deprecated
427  VisitAction depth_first_traversal(Visitor &v) ROSE_DEPRECATED("use depthFirstTraversal instead") {
428  return depthFirstTraversal(v);
429  }
430 
446  virtual uint64_t nNodes() = 0;
447 
448  // [Robb P. Matzke 2015-10-08]: deprecated
449  uint64_t nnodes() ROSE_DEPRECATED("use nNodes() instead") {
450  return nNodes();
451  }
452 
454  uint64_t nNodesUnique();
455 
456  // [Robb P. Matzke 2015-10-08]: deprecated
457  uint64_t nnodesUnique() ROSE_DEPRECATED("use nNodesUnique instead") {
458  return nNodesUnique();
459  }
460 
462  std::set<LeafPtr> getVariables();
463 
464  // [Robb P. Matzke 2015-10-08]: deprecated
465  std::set<LeafPtr> get_variables() ROSE_DEPRECATED("use getVariables instead") {
466  return getVariables();
467  }
468 
472  InteriorPtr isInteriorNode() {
473  return sharedFromThis().dynamicCast<Interior>();
474  }
475 
476  // [Robb P. Matzke 2015-10-09]: deprecated
477  InteriorPtr isInternalNode() ROSE_DEPRECATED("use isInteriorNode instead") {
478  return isInteriorNode();
479  }
480 
484  LeafPtr isLeafNode() {
485  return sharedFromThis().dynamicCast<Leaf>();
486  }
487 
491  bool isHashed() { return hashval_ != 0; }
492 
493  // [Robb P. Matzke 2015-10-08]: deprecated
494  bool is_hashed() ROSE_DEPRECATED("use isHashed instead") {
495  return isHashed();
496  }
497 
500  Hash hash();
501 
502  // used internally to set the hash value
503  void hash(Hash);
504 
507  private:
508  Ptr node;
509  Formatter &formatter;
510  public:
511  WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
512  void print(std::ostream &stream) const { node->print(stream, formatter); }
513  };
514 
533  // [Robb P. Matzke 2015-10-08]: deprecated
534  WithFormatter with_format(Formatter &fmt) ROSE_DEPRECATED("use withFormat instead") {
535  return withFormat(fmt);
536  }
537 
541  virtual void print(std::ostream&, Formatter&) = 0;
542  void print(std::ostream &o) { Formatter fmt; print(o, fmt); }
546  void assertAcyclic();
547 
548  // [Robb P. Matzke 2015-10-08]: deprecated
549  void assert_acyclic() {
550  return assertAcyclic();
551  }
552 
558  std::vector<Ptr> findCommonSubexpressions();
559 
565  bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/);
566 
568  InteriorPtr isOperator(Operator);
569 
570 protected:
571  void printFlags(std::ostream &o, unsigned flags, char &bracket);
572 };
573 
575 class Simplifier {
576 public:
577  virtual ~Simplifier() {}
578 
582  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
583  return Ptr();
584  }
585 
588  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
589  return Ptr();
590  }
591 };
592 
594  size_t operator()(const Ptr &expr) const {
595  return expr->hash();
596  }
597 };
598 
600  bool operator()(const Ptr &a, const Ptr &b) const {
601  return a->isEquivalentTo(b);
602  }
603 };
604 
607 public:
608  bool operator()(const Ptr &a, const Ptr &b);
609 };
610 
612 class ExprExprHashMap: public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
613  ExprExprHashMapHasher, ExprExprHashMapCompare> {
614 public:
615  ExprExprHashMap invert() const;
616 };
617 
620 
621 
623 // Simplification
625 
627  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
628  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
629 };
631  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
632  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
633 };
635  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
636  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
637 };
639  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
640  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
641 };
643  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
644 };
646  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
647 };
649  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
650  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
651 };
653  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
654 };
656  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
657 };
659  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
660 };
662  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
663 };
665  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
666 };
668  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
669 };
671  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
672 };
674  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
675 };
677  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
678 };
680  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
681 };
683  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
684 };
686  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
687 };
689  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
690 };
692  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
693 };
695  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
696 };
698  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
699 };
701  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
702 };
704  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
705 };
707  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
708 };
710  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
711 };
713  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
714 };
716  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
717 };
719  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
720 };
722  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
723 };
725  bool newbits;
726  ShiftSimplifier(bool newbits): newbits(newbits) {}
727  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
728 };
730  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
731  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
732 };
734  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
735  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
736 };
738  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
739 };
741  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
742 };
744  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
745 };
746 
747 
748 
750 // Interior Nodes
752 
757 class Interior: public Node {
758 private:
759  Operator op_;
760  Nodes children_;
761  uint64_t nnodes_; // total number of nodes; self + children's nnodes
762 
763  // Constructors should not be called directly. Use the create() class method instead. This is to help prevent
764  // accidently using pointers to these objects -- all access should be through shared-ownership pointers.
765  Interior(): op_(OP_ADD), nnodes_(1) {} // needed for serialization
766  Interior(size_t nbits, Operator op, const Ptr &a, const std::string &comment="", unsigned flags=0);
767  Interior(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const std::string &comment="", unsigned flags=0);
768  Interior(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c, const std::string &comment="",
769  unsigned flags=0);
770  Interior(size_t nbits, Operator op, const Nodes &children, const std::string &comment="", unsigned flags=0);
771 
772 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
773 private:
774  friend class boost::serialization::access;
775 
776  template<class S>
777  void serialize(S &s, const unsigned /*version*/) {
778  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
779  s & BOOST_SERIALIZATION_NVP(op_);
780  s & BOOST_SERIALIZATION_NVP(children_);
781  s & BOOST_SERIALIZATION_NVP(nnodes_);
782  }
783 #endif
784 
785 public:
797  static Ptr create(size_t nbits, Operator op, const Ptr &a,
798  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
799  InteriorPtr retval(new Interior(nbits, op, a, comment, flags));
800  return retval->simplifyTop(solver);
801  }
802  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b,
803  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
804  InteriorPtr retval(new Interior(nbits, op, a, b, comment, flags));
805  return retval->simplifyTop(solver);
806  }
807  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
808  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
809  InteriorPtr retval(new Interior(nbits, op, a, b, c, comment, flags));
810  return retval->simplifyTop(solver);
811  }
812  static Ptr create(size_t nbits, Operator op, const Nodes &children,
813  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
814  InteriorPtr retval(new Interior(nbits, op, children, comment, flags));
815  return retval->simplifyTop(solver);
816  }
819  /* see superclass, where these are pure virtual */
820  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
821  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
822  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
823  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
824  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
825  virtual bool isNumber() ROSE_OVERRIDE {
826  return false; /*if it's known, then it would have been folded to a leaf*/
827  }
828  virtual uint64_t toInt() ROSE_OVERRIDE { ASSERT_forbid2(true, "not a number"); return 0;}
829  virtual VisitAction depthFirstTraversal(Visitor&) ROSE_OVERRIDE;
830  virtual uint64_t nNodes() ROSE_OVERRIDE { return nnodes_; }
831 
833  size_t nChildren() { return children_.size(); }
834 
835  // [Robb P. Matzke 2015-10-09]: deprecated
836  size_t nchildren() ROSE_DEPRECATED("use nChildren instead") {
837  return nChildren();
838  }
839 
841  Ptr child(size_t idx) { ASSERT_require(idx<children_.size()); return children_[idx]; }
842 
846  const Nodes& children() { return children_; }
847 
848  // [Robb P. Matzke 2015-10-09]: deprecated
849  Nodes get_children() ROSE_DEPRECATED("use 'children' property instead") {
850  return children();
851  }
852 
854  Operator getOperator() { return op_; }
855 
856  // [Robb P. Matzke 2015-10-09]: deprecated
857  Operator get_operator() ROSE_DEPRECATED("use getOperator instead") {
858  return getOperator();
859  }
860 
864  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
865 
868  Ptr foldConstants(const Simplifier&);
869 
870  // [Robb P. Matzke 2015-10-09]: deprecated
871  Ptr constant_folding(const Simplifier &simplifier) ROSE_DEPRECATED("use foldConstants instead") {
872  return foldConstants(simplifier);
873  }
874 
879  InteriorPtr associative();
880 
881  // [Robb P. Matzke 2015-10-09]: deprecated
882  InteriorPtr nonassociative() ROSE_DEPRECATED("use 'associative' instead") {
883  return associative();
884  }
885 
890  InteriorPtr commutative();
891 
895  Ptr involutary();
896 
900  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
901 
905  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
906 
908  Ptr unaryNoOp();
909 
913  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
914 
915  virtual void print(std::ostream&, Formatter&) ROSE_OVERRIDE;
916 
917 protected:
919  void addChild(const Ptr &child);
920 
921  // [Robb P. Matzke 2015-10-09]: deprecated
922  void add_child(const Ptr &child) ROSE_DEPRECATED("use addChild instead") {
923  addChild(child);
924  }
925 
927  void adjustWidth();
928 
931  void adjustBitFlags(unsigned extraFlags);
932 };
933 
934 
936 // Leaf Nodes
938 
942 class Leaf: public Node {
943 private:
944  enum LeafType { CONSTANT, BITVECTOR, MEMORY };
945  LeafType leafType_;
947  uint64_t name_;
949 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
950 private:
951  friend class boost::serialization::access;
952 
953  template<class S>
954  void save(S &s, const unsigned /*version*/) const {
955  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
956  s & BOOST_SERIALIZATION_NVP(leafType_);
957  s & BOOST_SERIALIZATION_NVP(bits_);
958  s & BOOST_SERIALIZATION_NVP(name_);
959  }
960 
961  template<class S>
962  void load(S &s, const unsigned /*version*/) {
963  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
964  s & BOOST_SERIALIZATION_NVP(leafType_);
965  s & BOOST_SERIALIZATION_NVP(bits_);
966  s & BOOST_SERIALIZATION_NVP(name_);
967  nextNameCounter(name_);
968  }
969 
970  BOOST_SERIALIZATION_SPLIT_MEMBER();
971 #endif
972 
973  // Private to help prevent creating pointers to leaf nodes. See create_* methods instead.
974 private:
975  Leaf()
976  : Node(""), leafType_(CONSTANT), name_(0) {}
977  explicit Leaf(const std::string &comment, unsigned flags=0)
978  : Node(comment, flags), leafType_(CONSTANT), name_(0) {}
979 
980 public:
982  static LeafPtr createVariable(size_t nbits, const std::string &comment="", unsigned flags=0);
983 
984  // [Robb P. Matzke 2015-10-09]: deprecated
985  static LeafPtr create_variable(size_t nbits, std::string comment="", unsigned flags=0)
986  ROSE_DEPRECATED("use createVariable instead") {
987  return createVariable(nbits, comment, flags);
988  }
989 
993  static LeafPtr createExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0);
994 
995  // [Robb P. Matzke 2015-10-09]: deprecated
996  static LeafPtr create_existing_variable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0)
997  ROSE_DEPRECATED("use createExistingVariable instead") {
998  return createExistingVariable(nbits, id, comment, flags);
999  }
1000 
1003  static LeafPtr createInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0);
1004 
1005  // [Robb P. Matzke 2015-10-09]: deprecated
1006  static LeafPtr create_integer(size_t nbits, uint64_t n, std::string comment="", unsigned flags=0)
1007  ROSE_DEPRECATED("use createInteger instead") {
1008  return createInteger(nbits, n, comment, flags);
1009  }
1010 
1012  static LeafPtr createConstant(const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0);
1013 
1014  // [Robb P. Matzke 2015-10-09]: deprecated
1015  static LeafPtr create_constant(const Sawyer::Container::BitVector &bits, std::string comment="", unsigned flags=0)
1016  ROSE_DEPRECATED("use createConstant instead") {
1017  return createConstant(bits, comment, flags);
1018  }
1019 
1021  static LeafPtr createBoolean(bool b, const std::string &comment="", unsigned flags=0) {
1022  return createInteger(1, (uint64_t)(b?1:0), comment, flags);
1023  }
1024 
1025  // [Robb P. Matzke 2015-10-09]: deprecated
1026  static LeafPtr create_boolean(bool b, std::string comment="", unsigned flags=0)
1027  ROSE_DEPRECATED("use createBoolean instead") {
1028  return createBoolean(b, comment, flags);
1029  }
1030 
1032  static LeafPtr createMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1033 
1037  static LeafPtr createExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="",
1038  unsigned flags=0);
1039 
1040  // [Robb P. Matzke 2015-10-09]: deprecated
1041  static LeafPtr create_memory(size_t addressWidth, size_t valueWidth, std::string comment="", unsigned flags=0)
1042  ROSE_DEPRECATED("use createMemory instead") {
1043  return createMemory(addressWidth, valueWidth, comment, flags);
1044  }
1045 
1046  // from base class
1047  virtual bool isNumber() ROSE_OVERRIDE;
1048  virtual uint64_t toInt() ROSE_OVERRIDE;
1049  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1050  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1051  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1052  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1053  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1054  virtual VisitAction depthFirstTraversal(Visitor&) ROSE_OVERRIDE;
1055  virtual uint64_t nNodes() ROSE_OVERRIDE { return 1; }
1056 
1059 
1060  // [Robb P. Matzke 2015-10-09]: deprecated
1061  const Sawyer::Container::BitVector& get_bits() ROSE_DEPRECATED("use 'bits' property instead") {
1062  return bits();
1063  }
1064 
1066  virtual bool isVariable();
1067 
1068  // [Robb P. Matzke 2015-10-09]: deprecated
1069  bool is_variable() ROSE_DEPRECATED("use isVariable instead") {
1070  return isVariable();
1071  }
1072 
1074  virtual bool isMemory();
1075 
1076  // [Robb P. Matzke 2015-10-09]: deprecated
1077  bool is_memory() ROSE_DEPRECATED("use isMemory instead") {
1078  return isMemory();
1079  }
1080 
1085  uint64_t nameId();
1086 
1087  // [Robb P. Matzke 2015-10-09]: deprecated
1088  uint64_t get_name() ROSE_DEPRECATED("use nameId instead") {
1089  return nameId();
1090  }
1091 
1096  std::string toString();
1097 
1098  // documented in super class
1099  virtual void print(std::ostream&, Formatter&) ROSE_OVERRIDE;
1100 
1102  void printAsSigned(std::ostream&, Formatter&, bool asSigned=true);
1103 
1104  // [Robb P. Matzke 2015-10-09]: deprecated
1105  void print_as_signed(std::ostream &stream, Formatter &formatter, bool as_signed=true)
1106  ROSE_DEPRECATED("use printAsSigned instead") {
1107  printAsSigned(stream, formatter, as_signed);
1108  }
1109 
1111  void printAsUnsigned(std::ostream &o, Formatter &f) {
1112  printAsSigned(o, f, false);
1113  }
1114 
1115  // [Robb P. Matzke 2015-10-09]: deprecated
1116  void print_as_unsigned(std::ostream &o, Formatter &f) ROSE_DEPRECATED("use printAsUnsigned instead") {
1117  printAsUnsigned(o, f);
1118  }
1119 
1120 private:
1121  // Obtain or register a name ID
1122  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1123 };
1124 
1126 // Factories
1128 
1134 Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0);
1135 Ptr makeExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0);
1136 Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0);
1137 Ptr makeConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1138 Ptr makeBoolean(bool, const std::string &comment="", unsigned flags=0);
1139 Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1140 Ptr makeExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
1149 Ptr makeAdd(const Ptr&a, const Ptr &b,
1150  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1151 Ptr makeBooleanAnd(const Ptr &a, const Ptr &b,
1152  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1153  ROSE_DEPRECATED("use makeAnd instead"); // [Robb Matzke 2017-11-21]: deprecated
1154 Ptr makeAsr(const Ptr &sa, const Ptr &a,
1155  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1156 Ptr makeAnd(const Ptr &a, const Ptr &b,
1157  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1158 Ptr makeOr(const Ptr &a, const Ptr &b,
1159  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1160 Ptr makeXor(const Ptr &a, const Ptr &b,
1161  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1162 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1163  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1164 Ptr makeEq(const Ptr &a, const Ptr &b,
1165  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1166 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1167  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1168 Ptr makeInvert(const Ptr &a,
1169  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1170 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1171  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1172 Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1173  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1174 Ptr makeLssb(const Ptr &a,
1175  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1176 Ptr makeMssb(const Ptr &a,
1177  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1178 Ptr makeNe(const Ptr &a, const Ptr &b,
1179  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1180 Ptr makeNegate(const Ptr &a,
1181  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1182 Ptr makeBooleanOr(const Ptr &a, const Ptr &b,
1183  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1184  ROSE_DEPRECATED("use makeOr instead"); // [Robb Matzke 2017-11-21]: deprecated
1185 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1186  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1187 Ptr makeRol(const Ptr &sa, const Ptr &a,
1188  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1189 Ptr makeRor(const Ptr &sa, const Ptr &a,
1190  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1191 Ptr makeSet(const Ptr &a, const Ptr &b,
1192  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1193 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1194  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1195 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1196  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1197 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1198  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1199 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1200  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1201 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1202  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1203 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1204  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1205 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1206  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1207 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1208  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1209 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1210  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1211 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1212  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1213 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1214  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1215 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1216  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1217 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1218  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1219 Ptr makeDiv(const Ptr &a, const Ptr &b,
1220  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1221 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1222  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1223 Ptr makeGe(const Ptr &a, const Ptr &b,
1224  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1225 Ptr makeGt(const Ptr &a, const Ptr &b,
1226  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1227 Ptr makeLe(const Ptr &a, const Ptr &b,
1228  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1229 Ptr makeLt(const Ptr &a, const Ptr &b,
1230  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1231 Ptr makeMod(const Ptr &a, const Ptr &b,
1232  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1233 Ptr makeMul(const Ptr &a, const Ptr &b,
1234  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1235 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1236  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1237 Ptr makeZerop(const Ptr &a,
1238  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1242 // Miscellaneous functions
1245 
1246 
1247 std::ostream& operator<<(std::ostream &o, Node&);
1248 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1249 
1251 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1252 
1257 Hash hash(const std::vector<Ptr>&);
1258 
1263 template<typename InputIterator>
1264 uint64_t
1265 nNodes(InputIterator begin, InputIterator end) {
1266  uint64_t total = 0;
1267  for (InputIterator ii=begin; ii!=end; ++ii) {
1268  uint64_t n = (*ii)->nnodes();
1269  if (MAX_NNODES==n)
1270  return MAX_NNODES;
1271  if (total + n < total)
1272  return MAX_NNODES;
1273  total += n;
1274  }
1275  return total;
1276 }
1277 
1278 // [Robb P. Matzke 2015-10-08]: deprecated
1279 template<typename InputIterator>
1280 uint64_t
1281 nnodes(InputIterator begin, InputIterator end) ROSE_DEPRECATED("use nNodes instead");
1282 template<typename InputIterator>
1283 uint64_t
1284 nnodes(InputIterator begin, InputIterator end) {
1285  return nNodes(begin, end);
1286 }
1287 
1292 template<typename InputIterator>
1293 uint64_t
1294 nNodesUnique(InputIterator begin, InputIterator end)
1295 {
1296  struct T1: Visitor {
1297  typedef std::set<const Node*> SeenNodes;
1298 
1299  SeenNodes seen; // nodes that we've already seen, and the subtree size
1300  uint64_t nUnique; // number of unique nodes
1301 
1302  T1(): nUnique(0) {}
1303 
1304  VisitAction preVisit(const Ptr &node) {
1305  if (seen.insert(getRawPointer(node)).second) {
1306  ++nUnique;
1307  return CONTINUE; // this node has not been seen before; traverse into children
1308  } else {
1309  return TRUNCATE; // this node has been seen already; skip over the children
1310  }
1311  }
1312 
1313  VisitAction postVisit(const Ptr &node) {
1314  return CONTINUE;
1315  }
1316  } visitor;
1317 
1318  VisitAction status = CONTINUE;
1319  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1320  status = (*ii)->depthFirstTraversal(visitor);
1321  return visitor.nUnique;
1322 }
1323 
1324 // [Robb P. Matzke 2015-10-08]: deprecated
1325 template<typename InputIterator>
1326 uint64_t
1327 nnodesUnique(InputIterator begin, InputIterator end) ROSE_DEPRECATED("use nNodesUnique instead");
1328 template<typename InputIterator>
1329 uint64_t
1330 nnodesUnique(InputIterator begin, InputIterator end) {
1331  return nNodesUnique(begin, end);
1332 }
1333 
1340 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1341 
1342 template<typename InputIterator>
1343 std::vector<Ptr>
1344 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1345  typedef Sawyer::Container::Map<Ptr, size_t> NodeCounts;
1346  struct T1: Visitor {
1347  NodeCounts nodeCounts;
1348  std::vector<Ptr> result;
1349 
1350  VisitAction preVisit(const Ptr &node) ROSE_OVERRIDE {
1351  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1352  if (2 == ++nSeen)
1353  result.push_back(node);
1354  return nSeen>1 ? TRUNCATE : CONTINUE;
1355  }
1356 
1357  VisitAction postVisit(const Ptr&) ROSE_OVERRIDE {
1358  return CONTINUE;
1359  }
1360  } visitor;
1361 
1362  for (InputIterator ii=begin; ii!=end; ++ii)
1363  (*ii)->depthFirstTraversal(visitor);
1364  return visitor.result;
1365 }
1375 template<class Substitution>
1376 Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
1377  if (!src)
1378  return Ptr(); // no input implies no output
1379 
1380  // Try substituting the whole expression, returning the result.
1381  Ptr dst = subber(src, solver);
1382  ASSERT_not_null(dst);
1383  if (dst != src)
1384  return dst;
1385 
1386  // Try substituting all the subexpressions.
1387  InteriorPtr inode = src->isInteriorNode();
1388  if (!inode)
1389  return src;
1390  bool anyChildChanged = false;
1391  Nodes newChildren;
1392  newChildren.reserve(inode->nChildren());
1393  BOOST_FOREACH (const Ptr &child, inode->children()) {
1394  Ptr newChild = subber(child, solver);
1395  if (newChild != child)
1396  anyChildChanged = true;
1397  newChildren.push_back(newChild);
1398  }
1399  if (!anyChildChanged)
1400  return src;
1401 
1402  // Some subexpression changed, so build a new expression
1403  return Interior::create(0, inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1404 }
1405 
1406 } // namespace
1407 } // namespace
1408 } // namespace
1409 
1410 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1411 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1412 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1413 #endif
1414 
1415 #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.
virtual bool isMemory()
Does the node represent memory?
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.
const Sawyer::Container::BitVector & bits()
Property: Bits stored for numeric values.
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 bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Returns true if two expressions must be equal (cannot be unequal).
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.
static LeafPtr createMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Construct a new memory state.
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.
uint64_t nNodesUnique(InputIterator begin, InputIterator end)
Counts the number of unique nodes.
Ptr makeSignedMod(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual bool isVariable()
Is the node a bitvector variable?
static LeafPtr createVariable(size_t nbits, const std::string &comment="", unsigned flags=0)
Construct a new free variable with a specified number of significant bits.
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.
virtual uint64_t nNodes() ROSE_OVERRIDE
Computes the size of an expression by counting the number of nodes.
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.
static LeafPtr createExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0)
Construct another reference to an existing variable.
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.
Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver=SmtSolverPtr())
On-the-fly substitutions.
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.
virtual int compareStructure(const Ptr &other) ROSE_OVERRIDE
Compare two expressions structurally for sorting.
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.
void printAsSigned(std::ostream &, Formatter &, bool asSigned=true)
Prints an integer interpreted as a signed value.
static LeafPtr createInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0)
Construct a new integer with the specified number of significant bits.
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.
std::string toString()
Returns a string for the leaf.
Reference-counting smart pointer.
Definition: SharedPointer.h:34
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 uint64_t toInt() ROSE_OVERRIDE
Property: integer value of expression node.
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.
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.
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.
virtual VisitAction depthFirstTraversal(Visitor &) ROSE_OVERRIDE
Traverse the expression.
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.
uint64_t nNodes(InputIterator begin, InputIterator end)
Counts the number of nodes.
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.
uint64_t nameId()
Returns the name ID of a free variable.
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:22
Ptr makeAnd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Substitute one value for another.
virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE
Tests two expressions for structural equivalence.
Sawyer::SharedPointer< Interior > InteriorPtr
Shared-ownership pointer to an expression Interior node.
virtual void print(std::ostream &, Formatter &) ROSE_OVERRIDE
Print the expression to a stream.
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 bool isNumber() ROSE_OVERRIDE
Returns true if the expression is a known numeric value.
static LeafPtr createConstant(const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0)
Construct a new known value with the specified bits.
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.
static LeafPtr createExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0)
Construct another reference to an existing variable.
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.
void printAsUnsigned(std::ostream &o, Formatter &f)
Prints an integer interpreted as an unsigned value.
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.
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.
std::vector< Ptr > findCommonSubexpressions(const std::vector< Ptr > &)
Find common subexpressions.
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.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.
For a pre-order depth-first visit, do not descend into children.