ROSE  0.9.10.47
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 {
99  OP_BV_AND = OP_AND, // [Robb Matzke 2017-11-14]: deprecated
100  OP_BV_OR = OP_OR, // [Robb Matzke 2017-11-14]: deprecated
101  OP_BV_XOR = OP_XOR // [Robb Matzke 2017-11-14]: deprecated
102 };
103 
104 std::string toStr(Operator);
105 
106 class Node;
107 class Interior;
108 class Leaf;
110 
113 
116 
119 
120 typedef std::vector<Ptr> Nodes;
122 
124 typedef uint64_t Hash;
125 
127 struct Formatter {
132  };
133  Formatter()
135  max_depth(0), cur_depth(0), show_width(true), show_flags(true) {}
137  bool do_rename;
138  bool add_renames;
140  size_t max_depth;
141  size_t cur_depth;
143  bool show_width;
144  bool show_flags;
145 };
146 
152 };
153 
158 extern const uint64_t MAX_NNODES; // defined in .C so we don't pollute user namespace with limit macros
159 
164 class Visitor {
165 public:
166  virtual ~Visitor() {}
167  virtual VisitAction preVisit(const Ptr&) = 0;
168  virtual VisitAction postVisit(const Ptr&) = 0;
169 };
170 
171 
172 
174 // Base Node Type
176 
214 class Node
215  : public Sawyer::SharedObject,
216  public Sawyer::SharedFromThis<Node>,
217  public Sawyer::SmallObject,
218  public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
219 protected:
220  size_t nBits_;
221  size_t domainWidth_;
222  unsigned flags_;
223  std::string comment_;
225  boost::any userData_;
227 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
228 private:
229  friend class boost::serialization::access;
230 
231  template<class S>
232  void serialize(S &s, const unsigned /*version*/) {
233  s & BOOST_SERIALIZATION_NVP(nBits_);
234  s & BOOST_SERIALIZATION_NVP(domainWidth_);
235  s & BOOST_SERIALIZATION_NVP(flags_);
236  s & BOOST_SERIALIZATION_NVP(comment_);
237  s & BOOST_SERIALIZATION_NVP(hashval_);
238  // s & userData_;
239  }
240 #endif
241 
242 public:
243  // Bit flags
244 
246  static const unsigned RESERVED_FLAGS = 0x0000ffff;
247 
249  static const unsigned INDETERMINATE = 0x00000001;
250 
255  static const unsigned UNSPECIFIED = 0x00000002;
256 
259  static const unsigned BOTTOM = 0x00000004;
260 
261 protected:
262  Node()
263  : nBits_(0), domainWidth_(0), flags_(0), hashval_(0) {}
264  explicit Node(const std::string &comment, unsigned flags=0)
265  : nBits_(0), domainWidth_(0), flags_(flags), comment_(comment), hashval_(0) {}
266 
267 public:
274  static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
275 
281  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
282 
284  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
285 
291  virtual bool isEquivalentTo(const Ptr &other) = 0;
292 
298  virtual int compareStructure(const Ptr &other) = 0;
299 
305  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
306 
314  Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
315 
323  Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
324  const SmtSolverPtr &solver = SmtSolverPtr());
325 
329  virtual bool isNumber() = 0;
330 
331  // [Robb P. Matzke 2015-10-08]: deprecated
332  bool is_known() ROSE_DEPRECATED("use isNumber instead") {
333  return isNumber();
334  }
335 
340  virtual uint64_t toInt() = 0;
341 
342  // [Robb P. Matzke 2015-10-08]: deprecated
343  uint64_t get_value() ROSE_DEPRECATED("use toInt instead") {
344  return toInt();
345  }
346 
355  const std::string& comment() { return comment_; }
356  void comment(const std::string &s) { comment_ = s; }
359  // [Robb P. Matzke 2015-10-08]: deprecated
360  const std::string& get_comment() ROSE_DEPRECATED("use 'comment' property instead") {
361  return comment();
362  }
363 
364  // [Robb P. Matzke 2015-10-08]: deprecated
365  void set_comment(const std::string &s) ROSE_DEPRECATED("use 'comment' property instead") {
366  comment(s);
367  }
368 
376  void userData(boost::any &data) {
377  userData_ = data;
378  }
379  const boost::any& userData() {
380  return userData_;
381  }
387  size_t nBits() { return nBits_; }
388 
389  // [Robb P. Matzke 2015-10-08]: deprecated
390  size_t get_nbits() ROSE_DEPRECATED("use 'nBits' property instead") {
391  return nBits();
392  }
393 
398  unsigned flags() { return flags_; }
399 
400  unsigned get_flags() ROSE_DEPRECATED("use 'flags' property instead") {
401  return flags();
402  }
403 
407  Ptr newFlags(unsigned flags);
408 
412  size_t domainWidth() { return domainWidth_; }
413 
417  bool isScalar() { return 0 == domainWidth_; }
418 
424 
425  // [Robb P. Matzke 2015-10-08]: deprecated
426  VisitAction depth_first_traversal(Visitor &v) ROSE_DEPRECATED("use depthFirstTraversal instead") {
427  return depthFirstTraversal(v);
428  }
429 
445  virtual uint64_t nNodes() = 0;
446 
447  // [Robb P. Matzke 2015-10-08]: deprecated
448  uint64_t nnodes() ROSE_DEPRECATED("use nNodes() instead") {
449  return nNodes();
450  }
451 
453  uint64_t nNodesUnique();
454 
455  // [Robb P. Matzke 2015-10-08]: deprecated
456  uint64_t nnodesUnique() ROSE_DEPRECATED("use nNodesUnique instead") {
457  return nNodesUnique();
458  }
459 
461  std::set<LeafPtr> getVariables();
462 
463  // [Robb P. Matzke 2015-10-08]: deprecated
464  std::set<LeafPtr> get_variables() ROSE_DEPRECATED("use getVariables instead") {
465  return getVariables();
466  }
467 
472  return sharedFromThis().dynamicCast<Interior>();
473  }
474 
475  // [Robb P. Matzke 2015-10-09]: deprecated
476  InteriorPtr isInternalNode() ROSE_DEPRECATED("use isInteriorNode instead") {
477  return isInteriorNode();
478  }
479 
484  return sharedFromThis().dynamicCast<Leaf>();
485  }
486 
490  bool isHashed() { return hashval_ != 0; }
491 
492  // [Robb P. Matzke 2015-10-08]: deprecated
493  bool is_hashed() ROSE_DEPRECATED("use isHashed instead") {
494  return isHashed();
495  }
496 
499  Hash hash();
500 
501  // used internally to set the hash value
502  void hash(Hash);
503 
506  private:
507  Ptr node;
508  Formatter &formatter;
509  public:
510  WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
511  void print(std::ostream &stream) const { node->print(stream, formatter); }
512  };
513 
532  // [Robb P. Matzke 2015-10-08]: deprecated
533  WithFormatter with_format(Formatter &fmt) ROSE_DEPRECATED("use withFormat instead") {
534  return withFormat(fmt);
535  }
536 
540  virtual void print(std::ostream&, Formatter&) = 0;
541  void print(std::ostream &o) { Formatter fmt; print(o, fmt); }
545  void assertAcyclic();
546 
547  // [Robb P. Matzke 2015-10-08]: deprecated
548  void assert_acyclic() {
549  return assertAcyclic();
550  }
551 
557  std::vector<Ptr> findCommonSubexpressions();
558 
564  bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/);
565 
568 
569 protected:
570  void printFlags(std::ostream &o, unsigned flags, char &bracket);
571 };
572 
574 class Simplifier {
575 public:
576  virtual ~Simplifier() {}
577 
581  virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
582  return Ptr();
583  }
584 
587  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
588  return Ptr();
589  }
590 };
591 
593  size_t operator()(const Ptr &expr) const {
594  return expr->hash();
595  }
596 };
597 
599  bool operator()(const Ptr &a, const Ptr &b) const {
600  return a->isEquivalentTo(b);
601  }
602 };
603 
606 public:
607  bool operator()(const Ptr &a, const Ptr &b);
608 };
609 
611 class ExprExprHashMap: public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
612  ExprExprHashMapHasher, ExprExprHashMapCompare> {
613 public:
614  ExprExprHashMap invert() const;
615 };
616 
619 
620 
622 // Simplification
624 
626  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
627  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
628 };
630  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
631  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
632 };
634  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
635  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
636 };
638  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
639  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
640 };
642  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
643 };
645  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
646 };
648  virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE;
649  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
650 };
652  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
653 };
655  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
656 };
658  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
659 };
661  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
662 };
664  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
665 };
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 };
679  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
680 };
682  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
683 };
685  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
686 };
688  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
689 };
691  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
692 };
694  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
695 };
697  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
698 };
700  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
701 };
703  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
704 };
706  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
707 };
709  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
710 };
712  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
713 };
715  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
716 };
718  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
719 };
721  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
722 };
724  bool newbits;
725  ShiftSimplifier(bool newbits): newbits(newbits) {}
726  Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
727 };
729  ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
730  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
731 };
733  ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
734  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
735 };
737  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
738 };
740  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
741 };
743  virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const ROSE_OVERRIDE;
744 };
745 
746 
747 
749 // Interior Nodes
751 
756 class Interior: public Node {
757 private:
758  Operator op_;
759  Nodes children_;
760  uint64_t nnodes_; // total number of nodes; self + children's nnodes
761 
762  // Constructors should not be called directly. Use the create() class method instead. This is to help prevent
763  // accidently using pointers to these objects -- all access should be through shared-ownership pointers.
764  Interior(): op_(OP_ADD), nnodes_(1) {} // needed for serialization
765  Interior(size_t nbits, Operator op, const Ptr &a, const std::string &comment="", unsigned flags=0);
766  Interior(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const std::string &comment="", unsigned flags=0);
767  Interior(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c, const std::string &comment="",
768  unsigned flags=0);
769  Interior(size_t nbits, Operator op, const Nodes &children, const std::string &comment="", unsigned flags=0);
770 
771 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
772 private:
773  friend class boost::serialization::access;
774 
775  template<class S>
776  void serialize(S &s, const unsigned /*version*/) {
777  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
778  s & BOOST_SERIALIZATION_NVP(op_);
779  s & BOOST_SERIALIZATION_NVP(children_);
780  s & BOOST_SERIALIZATION_NVP(nnodes_);
781  }
782 #endif
783 
784 public:
796  static Ptr create(size_t nbits, Operator op, const Ptr &a,
797  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
798  InteriorPtr retval(new Interior(nbits, op, a, comment, flags));
799  return retval->simplifyTop(solver);
800  }
801  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b,
802  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
803  InteriorPtr retval(new Interior(nbits, op, a, b, comment, flags));
804  return retval->simplifyTop(solver);
805  }
806  static Ptr create(size_t nbits, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
807  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
808  InteriorPtr retval(new Interior(nbits, op, a, b, c, comment, flags));
809  return retval->simplifyTop(solver);
810  }
811  static Ptr create(size_t nbits, Operator op, const Nodes &children,
812  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0) {
813  InteriorPtr retval(new Interior(nbits, op, children, comment, flags));
814  return retval->simplifyTop(solver);
815  }
818  /* see superclass, where these are pure virtual */
819  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
820  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
821  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
822  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
823  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
824  virtual bool isNumber() ROSE_OVERRIDE {
825  return false; /*if it's known, then it would have been folded to a leaf*/
826  }
827  virtual uint64_t toInt() ROSE_OVERRIDE { ASSERT_forbid2(true, "not a number"); return 0;}
828  virtual VisitAction depthFirstTraversal(Visitor&) ROSE_OVERRIDE;
829  virtual uint64_t nNodes() ROSE_OVERRIDE { return nnodes_; }
830 
832  size_t nChildren() { return children_.size(); }
833 
834  // [Robb P. Matzke 2015-10-09]: deprecated
835  size_t nchildren() ROSE_DEPRECATED("use nChildren instead") {
836  return nChildren();
837  }
838 
840  Ptr child(size_t idx) { ASSERT_require(idx<children_.size()); return children_[idx]; }
841 
845  const Nodes& children() { return children_; }
846 
847  // [Robb P. Matzke 2015-10-09]: deprecated
848  Nodes get_children() ROSE_DEPRECATED("use 'children' property instead") {
849  return children();
850  }
851 
853  Operator getOperator() { return op_; }
854 
855  // [Robb P. Matzke 2015-10-09]: deprecated
856  Operator get_operator() ROSE_DEPRECATED("use getOperator instead") {
857  return getOperator();
858  }
859 
863  Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
864 
867  Ptr foldConstants(const Simplifier&);
868 
869  // [Robb P. Matzke 2015-10-09]: deprecated
870  Ptr constant_folding(const Simplifier &simplifier) ROSE_DEPRECATED("use foldConstants instead") {
871  return foldConstants(simplifier);
872  }
873 
879 
880  // [Robb P. Matzke 2015-10-09]: deprecated
881  InteriorPtr nonassociative() ROSE_DEPRECATED("use 'associative' instead") {
882  return associative();
883  }
884 
890 
894  Ptr involutary();
895 
899  Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
900 
904  Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
905 
907  Ptr unaryNoOp();
908 
912  Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
913 
914  virtual void print(std::ostream&, Formatter&) ROSE_OVERRIDE;
915 
916 protected:
918  void addChild(const Ptr &child);
919 
920  // [Robb P. Matzke 2015-10-09]: deprecated
921  void add_child(const Ptr &child) ROSE_DEPRECATED("use addChild instead") {
922  addChild(child);
923  }
924 
926  void adjustWidth();
927 
930  void adjustBitFlags(unsigned extraFlags);
931 };
932 
933 
935 // Leaf Nodes
937 
941 class Leaf: public Node {
942 private:
943  enum LeafType { CONSTANT, BITVECTOR, MEMORY };
944  LeafType leafType_;
946  uint64_t name_;
948 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
949 private:
950  friend class boost::serialization::access;
951 
952  template<class S>
953  void save(S &s, const unsigned /*version*/) const {
954  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
955  s & BOOST_SERIALIZATION_NVP(leafType_);
956  s & BOOST_SERIALIZATION_NVP(bits_);
957  s & BOOST_SERIALIZATION_NVP(name_);
958  }
959 
960  template<class S>
961  void load(S &s, const unsigned /*version*/) {
962  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
963  s & BOOST_SERIALIZATION_NVP(leafType_);
964  s & BOOST_SERIALIZATION_NVP(bits_);
965  s & BOOST_SERIALIZATION_NVP(name_);
966  nextNameCounter(name_);
967  }
968 
969  BOOST_SERIALIZATION_SPLIT_MEMBER();
970 #endif
971 
972  // Private to help prevent creating pointers to leaf nodes. See create_* methods instead.
973 private:
974  Leaf()
975  : Node(""), leafType_(CONSTANT), name_(0) {}
976  explicit Leaf(const std::string &comment, unsigned flags=0)
977  : Node(comment, flags), leafType_(CONSTANT), name_(0) {}
978 
979 public:
981  static LeafPtr createVariable(size_t nbits, const std::string &comment="", unsigned flags=0);
982 
983  // [Robb P. Matzke 2015-10-09]: deprecated
984  static LeafPtr create_variable(size_t nbits, std::string comment="", unsigned flags=0)
985  ROSE_DEPRECATED("use createVariable instead") {
986  return createVariable(nbits, comment, flags);
987  }
988 
992  static LeafPtr createExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0);
993 
994  // [Robb P. Matzke 2015-10-09]: deprecated
995  static LeafPtr create_existing_variable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0)
996  ROSE_DEPRECATED("use createExistingVariable instead") {
997  return createExistingVariable(nbits, id, comment, flags);
998  }
999 
1002  static LeafPtr createInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0);
1003 
1004  // [Robb P. Matzke 2015-10-09]: deprecated
1005  static LeafPtr create_integer(size_t nbits, uint64_t n, std::string comment="", unsigned flags=0)
1006  ROSE_DEPRECATED("use createInteger instead") {
1007  return createInteger(nbits, n, comment, flags);
1008  }
1009 
1011  static LeafPtr createConstant(const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0);
1012 
1013  // [Robb P. Matzke 2015-10-09]: deprecated
1014  static LeafPtr create_constant(const Sawyer::Container::BitVector &bits, std::string comment="", unsigned flags=0)
1015  ROSE_DEPRECATED("use createConstant instead") {
1016  return createConstant(bits, comment, flags);
1017  }
1018 
1020  static LeafPtr createBoolean(bool b, const std::string &comment="", unsigned flags=0) {
1021  return createInteger(1, (uint64_t)(b?1:0), comment, flags);
1022  }
1023 
1024  // [Robb P. Matzke 2015-10-09]: deprecated
1025  static LeafPtr create_boolean(bool b, std::string comment="", unsigned flags=0)
1026  ROSE_DEPRECATED("use createBoolean instead") {
1027  return createBoolean(b, comment, flags);
1028  }
1029 
1031  static LeafPtr createMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1032 
1036  static LeafPtr createExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="",
1037  unsigned flags=0);
1038 
1039  // [Robb P. Matzke 2015-10-09]: deprecated
1040  static LeafPtr create_memory(size_t addressWidth, size_t valueWidth, std::string comment="", unsigned flags=0)
1041  ROSE_DEPRECATED("use createMemory instead") {
1042  return createMemory(addressWidth, valueWidth, comment, flags);
1043  }
1044 
1045  // from base class
1046  virtual bool isNumber() ROSE_OVERRIDE;
1047  virtual uint64_t toInt() ROSE_OVERRIDE;
1048  virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1049  virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1050  virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE;
1051  virtual int compareStructure(const Ptr& other) ROSE_OVERRIDE;
1052  virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1053  virtual VisitAction depthFirstTraversal(Visitor&) ROSE_OVERRIDE;
1054  virtual uint64_t nNodes() ROSE_OVERRIDE { return 1; }
1055 
1058 
1059  // [Robb P. Matzke 2015-10-09]: deprecated
1060  const Sawyer::Container::BitVector& get_bits() ROSE_DEPRECATED("use 'bits' property instead") {
1061  return bits();
1062  }
1063 
1065  virtual bool isVariable();
1066 
1067  // [Robb P. Matzke 2015-10-09]: deprecated
1068  bool is_variable() ROSE_DEPRECATED("use isVariable instead") {
1069  return isVariable();
1070  }
1071 
1073  virtual bool isMemory();
1074 
1075  // [Robb P. Matzke 2015-10-09]: deprecated
1076  bool is_memory() ROSE_DEPRECATED("use isMemory instead") {
1077  return isMemory();
1078  }
1079 
1084  uint64_t nameId();
1085 
1086  // [Robb P. Matzke 2015-10-09]: deprecated
1087  uint64_t get_name() ROSE_DEPRECATED("use nameId instead") {
1088  return nameId();
1089  }
1090 
1095  std::string toString();
1096 
1097  // documented in super class
1098  virtual void print(std::ostream&, Formatter&) ROSE_OVERRIDE;
1099 
1101  void printAsSigned(std::ostream&, Formatter&, bool asSigned=true);
1102 
1103  // [Robb P. Matzke 2015-10-09]: deprecated
1104  void print_as_signed(std::ostream &stream, Formatter &formatter, bool as_signed=true)
1105  ROSE_DEPRECATED("use printAsSigned instead") {
1106  printAsSigned(stream, formatter, as_signed);
1107  }
1108 
1110  void printAsUnsigned(std::ostream &o, Formatter &f) {
1111  printAsSigned(o, f, false);
1112  }
1113 
1114  // [Robb P. Matzke 2015-10-09]: deprecated
1115  void print_as_unsigned(std::ostream &o, Formatter &f) ROSE_DEPRECATED("use printAsUnsigned instead") {
1116  printAsUnsigned(o, f);
1117  }
1118 
1119 private:
1120  // Obtain or register a name ID
1121  static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1122 };
1123 
1125 // Factories
1127 
1133 Ptr makeVariable(size_t nbits, const std::string &comment="", unsigned flags=0);
1134 Ptr makeExistingVariable(size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0);
1135 Ptr makeInteger(size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0);
1136 Ptr makeConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
1137 Ptr makeBoolean(bool, const std::string &comment="", unsigned flags=0);
1138 Ptr makeMemory(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
1139 Ptr makeExistingMemory(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
1148 Ptr makeAdd(const Ptr&a, const Ptr &b,
1149  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1150 Ptr makeBooleanAnd(const Ptr &a, const Ptr &b,
1151  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1152  ROSE_DEPRECATED("use makeAnd instead"); // [Robb Matzke 2017-11-21]: deprecated
1153 Ptr makeAsr(const Ptr &sa, const Ptr &a,
1154  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1155 Ptr makeAnd(const Ptr &a, const Ptr &b,
1156  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1157 Ptr makeOr(const Ptr &a, const Ptr &b,
1158  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1159 Ptr makeXor(const Ptr &a, const Ptr &b,
1160  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1161 Ptr makeConcat(const Ptr &hi, const Ptr &lo,
1162  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1163 Ptr makeEq(const Ptr &a, const Ptr &b,
1164  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1165 Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1166  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1167 Ptr makeInvert(const Ptr &a,
1168  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1169 Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1170  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1171 Ptr makeLssb(const Ptr &a,
1172  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1173 Ptr makeMssb(const Ptr &a,
1174  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1175 Ptr makeNe(const Ptr &a, const Ptr &b,
1176  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1177 Ptr makeNegate(const Ptr &a,
1178  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1179 Ptr makeBooleanOr(const Ptr &a, const Ptr &b,
1180  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
1181  ROSE_DEPRECATED("use makeOr instead"); // [Robb Matzke 2017-11-21]: deprecated
1182 Ptr makeRead(const Ptr &mem, const Ptr &addr,
1183  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1184 Ptr makeRol(const Ptr &sa, const Ptr &a,
1185  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1186 Ptr makeRor(const Ptr &sa, const Ptr &a,
1187  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1188 Ptr makeSet(const Ptr &a, const Ptr &b,
1189  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1190 Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1191  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1192 Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
1193  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1194 Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
1195  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1196 Ptr makeSignedGe(const Ptr &a, const Ptr &b,
1197  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1198 Ptr makeSignedGt(const Ptr &a, const Ptr &b,
1199  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1200 Ptr makeShl0(const Ptr &sa, const Ptr &a,
1201  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1202 Ptr makeShl1(const Ptr &sa, const Ptr &a,
1203  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1204 Ptr makeShr0(const Ptr &sa, const Ptr &a,
1205  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1206 Ptr makeShr1(const Ptr &sa, const Ptr &a,
1207  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1208 Ptr makeSignedLe(const Ptr &a, const Ptr &b,
1209  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1210 Ptr makeSignedLt(const Ptr &a, const Ptr &b,
1211  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1212 Ptr makeSignedMod(const Ptr &a, const Ptr &b,
1213  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1214 Ptr makeSignedMul(const Ptr &a, const Ptr &b,
1215  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1216 Ptr makeDiv(const Ptr &a, const Ptr &b,
1217  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1218 Ptr makeExtend(const Ptr &newSize, const Ptr &a,
1219  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1220 Ptr makeGe(const Ptr &a, const Ptr &b,
1221  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1222 Ptr makeGt(const Ptr &a, const Ptr &b,
1223  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1224 Ptr makeLe(const Ptr &a, const Ptr &b,
1225  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1226 Ptr makeLt(const Ptr &a, const Ptr &b,
1227  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1228 Ptr makeMod(const Ptr &a, const Ptr &b,
1229  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1230 Ptr makeMul(const Ptr &a, const Ptr &b,
1231  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1232 Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1233  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1234 Ptr makeZerop(const Ptr &a,
1235  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
1239 // Miscellaneous functions
1242 
1243 
1244 std::ostream& operator<<(std::ostream &o, Node&);
1245 std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
1246 
1248 Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1249 
1254 Hash hash(const std::vector<Ptr>&);
1255 
1260 template<typename InputIterator>
1261 uint64_t
1262 nNodes(InputIterator begin, InputIterator end) {
1263  uint64_t total = 0;
1264  for (InputIterator ii=begin; ii!=end; ++ii) {
1265  uint64_t n = (*ii)->nnodes();
1266  if (MAX_NNODES==n)
1267  return MAX_NNODES;
1268  if (total + n < total)
1269  return MAX_NNODES;
1270  total += n;
1271  }
1272  return total;
1273 }
1274 
1275 // [Robb P. Matzke 2015-10-08]: deprecated
1276 template<typename InputIterator>
1277 uint64_t
1278 nnodes(InputIterator begin, InputIterator end) ROSE_DEPRECATED("use nNodes instead");
1279 template<typename InputIterator>
1280 uint64_t
1281 nnodes(InputIterator begin, InputIterator end) {
1282  return nNodes(begin, end);
1283 }
1284 
1289 template<typename InputIterator>
1290 uint64_t
1291 nNodesUnique(InputIterator begin, InputIterator end)
1292 {
1293  struct T1: Visitor {
1294  typedef std::set<const Node*> SeenNodes;
1295 
1296  SeenNodes seen; // nodes that we've already seen, and the subtree size
1297  uint64_t nUnique; // number of unique nodes
1298 
1299  T1(): nUnique(0) {}
1300 
1301  VisitAction preVisit(const Ptr &node) {
1302  if (seen.insert(getRawPointer(node)).second) {
1303  ++nUnique;
1304  return CONTINUE; // this node has not been seen before; traverse into children
1305  } else {
1306  return TRUNCATE; // this node has been seen already; skip over the children
1307  }
1308  }
1309 
1310  VisitAction postVisit(const Ptr &node) {
1311  return CONTINUE;
1312  }
1313  } visitor;
1314 
1315  VisitAction status = CONTINUE;
1316  for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
1317  status = (*ii)->depthFirstTraversal(visitor);
1318  return visitor.nUnique;
1319 }
1320 
1321 // [Robb P. Matzke 2015-10-08]: deprecated
1322 template<typename InputIterator>
1323 uint64_t
1324 nnodesUnique(InputIterator begin, InputIterator end) ROSE_DEPRECATED("use nNodesUnique instead");
1325 template<typename InputIterator>
1326 uint64_t
1327 nnodesUnique(InputIterator begin, InputIterator end) {
1328  return nNodesUnique(begin, end);
1329 }
1330 
1337 std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
1338 
1339 template<typename InputIterator>
1340 std::vector<Ptr>
1341 findCommonSubexpressions(InputIterator begin, InputIterator end) {
1342  typedef Sawyer::Container::Map<Ptr, size_t> NodeCounts;
1343  struct T1: Visitor {
1344  NodeCounts nodeCounts;
1345  std::vector<Ptr> result;
1346 
1347  VisitAction preVisit(const Ptr &node) ROSE_OVERRIDE {
1348  size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1349  if (2 == ++nSeen)
1350  result.push_back(node);
1351  return nSeen>1 ? TRUNCATE : CONTINUE;
1352  }
1353 
1354  VisitAction postVisit(const Ptr&) ROSE_OVERRIDE {
1355  return CONTINUE;
1356  }
1357  } visitor;
1358 
1359  for (InputIterator ii=begin; ii!=end; ++ii)
1360  (*ii)->depthFirstTraversal(visitor);
1361  return visitor.result;
1362 }
1365 } // namespace
1366 } // namespace
1367 } // namespace
1368 
1369 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1370 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Interior);
1371 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpr::Leaf);
1372 #endif
1373 
1374 #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 &quot;...&quot;.
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.
Sawyer::Container::Set< Ptr, ExpressionLessp > ExpressionSet
Set of expressions ordered by hash.
static const unsigned UNSPECIFIED
Value is somehow unspecified.
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.
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.
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.
static boost::logic::tribool(* mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr &)
User-supplied predicate to augment alias checking.
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:64
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.