1 #ifndef ROSE_BinaryAnalysis_SymbolicExpr_H
2 #define ROSE_BinaryAnalysis_SymbolicExpr_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #ifndef __STDC_FORMAT_MACROS
7 #define __STDC_FORMAT_MACROS
12 #include <boost/any.hpp>
13 #include <boost/lexical_cast.hpp>
14 #include <boost/logic/tribool.hpp>
15 #include <boost/serialization/access.hpp>
16 #include <boost/serialization/base_object.hpp>
17 #include <boost/serialization/export.hpp>
18 #include <boost/serialization/split_member.hpp>
19 #include <boost/serialization/string.hpp>
20 #include <boost/serialization/vector.hpp>
21 #include <boost/unordered_map.hpp>
24 #include <RoseException.h>
25 #include <Sawyer/Attribute.h>
26 #include <Sawyer/BitVector.h>
27 #include <Sawyer/Optional.h>
28 #include <Sawyer/Set.h>
29 #include <Sawyer/SharedPointer.h>
30 #include <Sawyer/SmallObject.h>
46 namespace SymbolicExpr {
167 typedef std::vector<Ptr> Nodes;
240 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
242 friend class boost::serialization::access;
245 void serialize(S &s,
const unsigned version) {
247 s & BOOST_SERIALIZATION_NVP(fields_);
251 size_t z2 = secondaryWidth();
252 s & boost::serialization::make_nvp(
"typeClass_", t);
253 s & boost::serialization::make_nvp(
"totalWidth_", z1);
254 s & boost::serialization::make_nvp(
"secondaryWidth_", z2);
302 return Type(
MEMORY, valueWidth, addressWidth);
314 return Type(
FP, 1 + exponentWidth + significandWidth - 1 , exponentWidth);
328 return (
TypeClass)((fields_ >> 30) & 0x3);
336 return fields_ & 0x7fff;
345 return secondaryWidth();
354 return secondaryWidth();
374 return fields_ == other.fields_;
377 return !(*
this == other);
394 ASSERT_require(n <= 3);
395 fields_ = (fields_ & 0x3fffffff) | (n << 30);
399 void nBits(
size_t n) {
401 throw Exception(
"type width is out of range");
402 fields_ = (fields_ & 0xffff8000) | n;
406 void secondaryWidth(
size_t n) {
408 throw Exception(
"second width is out of range");
409 fields_ = (fields_ & 0xc0007fff) | (n << 15);
412 size_t secondaryWidth()
const {
413 return (fields_ >> 15) & 0x7fff;
474 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
476 friend class boost::serialization::access;
479 void serialize(S &s,
const unsigned version) {
481 ASSERT_not_reachable(
"SymbolicExpr version " + boost::lexical_cast<std::string>(version) +
" is no longer supported");
482 s & BOOST_SERIALIZATION_NVP(type_);
483 s & BOOST_SERIALIZATION_NVP(flags_);
484 s & BOOST_SERIALIZATION_NVP(comment_);
485 s & BOOST_SERIALIZATION_NVP(hashval_);
507 static const unsigned BOTTOM = 0x00000004;
511 : type_(
Type::integer(0)), flags_(0), hashval_(0) {}
513 : type_(
Type::integer(0)), flags_(
flags), comment_(comment), hashval_(0) {}
593 virtual Ptr
child(
size_t idx)
const = 0;
598 virtual const Nodes&
children()
const = 0;
725 return type_.
nBits();
776 virtual uint64_t
nNodes()
const = 0;
798 return hashval_ != 0;
815 void print(std::ostream &stream)
const { node->print(stream, formatter); }
864 void printFlags(std::ostream &o,
unsigned flags,
char &bracket)
const;
873 uint64_t toInt() ROSE_DEPRECATED("use
toUnsigned() instead") {
886 virtual Ptr
fold(Nodes::const_iterator , Nodes::const_iterator )
const {
898 size_t operator()(
const Ptr &expr)
const {
904 bool operator()(
const Ptr &a,
const Ptr &b)
const {
905 return a->isEquivalentTo(b);
912 bool operator()(
const Ptr &a,
const Ptr &b)
const;
916 class ExprExprHashMap:
public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
917 ExprExprHashMapHasher, ExprExprHashMapCompare> {
931 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const ROSE_OVERRIDE;
935 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const ROSE_OVERRIDE;
942 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const ROSE_OVERRIDE;
946 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const ROSE_OVERRIDE;
950 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const ROSE_OVERRIDE;
953 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const ROSE_OVERRIDE;
956 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const ROSE_OVERRIDE;
1037 Ptr combine_strengths(Ptr strength1, Ptr strength2,
size_t value_width,
const SmtSolverPtr &solver)
const;
1078 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1080 friend class boost::serialization::access;
1083 void serialize(S &s,
const unsigned ) {
1084 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Node);
1085 s & BOOST_SERIALIZATION_NVP(op_);
1086 s & BOOST_SERIALIZATION_NVP(children_);
1087 s & BOOST_SERIALIZATION_NVP(nnodes_);
1134 virtual uint64_t
nNodes() const ROSE_OVERRIDE {
return nnodes_; }
1135 virtual const Nodes&
children() const ROSE_OVERRIDE {
return children_; }
1137 virtual size_t nChildren() const ROSE_OVERRIDE {
return children_.size(); }
1138 virtual Ptr
child(
size_t idx)
const ROSE_OVERRIDE {
return idx < children_.size() ? children_[idx] :
Ptr(); }
1210 virtual void print(std::ostream&,
Formatter&) const ROSE_OVERRIDE;
1229 static Ptr create(
size_t nbits,
Operator op, const Ptr &a,
1231 ROSE_DEPRECATED("use instance instead");
1232 static Ptr create(
size_t nbits,
Operator op, const Ptr &a, const Ptr &b,
1233 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0)
1234 ROSE_DEPRECATED("use instance instead");
1235 static Ptr create(
size_t nbits,
Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
1236 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0)
1237 ROSE_DEPRECATED("use instance instead");
1239 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0)
1240 ROSE_DEPRECATED("use instance instead");
1260 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1262 friend class boost::serialization::access;
1265 void save(S &s,
const unsigned )
const {
1266 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1267 s & BOOST_SERIALIZATION_NVP(bits_);
1268 s & BOOST_SERIALIZATION_NVP(name_);
1272 void load(S &s,
const unsigned ) {
1273 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
1274 s & BOOST_SERIALIZATION_NVP(bits_);
1275 s & BOOST_SERIALIZATION_NVP(name_);
1276 nextNameCounter(name_);
1279 BOOST_SERIALIZATION_SPLIT_MEMBER();
1288 explicit Leaf(
const std::string &comment,
unsigned flags=0)
1289 : Node(comment, flags), name_(0) {}
1294 static LeafPtr createVariable(
const Type&,
1295 const std::string &comment =
"",
unsigned flags = 0);
1298 static LeafPtr createVariable(
const Type&,
const uint64_t
id,
1299 const std::string &comment =
"",
unsigned flags = 0);
1303 const std::string &comment =
"",
unsigned flags = 0);
1309 virtual size_t nChildren() const ROSE_OVERRIDE {
return 0; }
1310 virtual Ptr
child(
size_t idx)
const ROSE_OVERRIDE {
return Ptr(); }
1311 virtual const Nodes&
children() const ROSE_OVERRIDE;
1313 virtual bool mustEqual(
const Ptr &other,
const SmtSolverPtr &solver =
SmtSolverPtr()) ROSE_OVERRIDE;
1314 virtual
bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1317 virtual Ptr
substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) ROSE_OVERRIDE;
1319 virtual uint64_t
nNodes() const ROSE_OVERRIDE {
return 1; }
1321 virtual
Sawyer::Optional<int64_t>
toSigned() const ROSE_OVERRIDE;
1324 virtual void print(std::ostream&,
Formatter&) const ROSE_OVERRIDE;
1331 const
Sawyer::Container::BitVector& bits() const;
1355 uint64_t nameId()
const;
1361 std::string toString()
const;
1364 void printAsSigned(std::ostream&,
Formatter&,
bool asSigned =
true)
const;
1368 printAsSigned(o, f,
false);
1373 static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1378 static LeafPtr createVariable(
size_t nBits,
const std::string &comment=
"",
unsigned flags=0)
1380 return createVariable(
Type::integer(nBits), comment, flags);
1384 static LeafPtr createExistingVariable(
size_t nBits, uint64_t
id,
const std::string &comment=
"",
unsigned flags=0)
1385 ROSE_DEPRECATED("use createVariable or makeIntegerVariable, etc.") {
1386 return createVariable(
Type::integer(nBits),
id, comment, flags);
1390 static LeafPtr createInteger(
size_t nBits, uint64_t value,
const std::string &comment=
"",
unsigned flags=0)
1394 static LeafPtr createConstant(const
Sawyer::Container::BitVector &bits, const
std::
string &comment="",
unsigned flags=0)
1395 ROSE_DEPRECATED("use createConstant with type or makeIntegerConstant, etc.") {
1396 return createConstant(
Type::integer(bits.size()), bits, comment, flags);
1400 static LeafPtr createBoolean(
bool b,
const std::string &comment=
"",
unsigned flags=0)
1404 static LeafPtr createMemory(
size_t addressWidth,
size_t valueWidth, const
std::
string &comment="",
unsigned flags=0)
1406 return createVariable(
Type::memory(addressWidth, valueWidth), comment, flags);
1410 static LeafPtr createExistingMemory(
size_t addressWidth,
size_t valueWidth, uint64_t
id,
const std::string &comment=
"",
1412 ROSE_DEPRECATED("use createVariable with type or makeMemoryVariable") {
1413 return createVariable(
Type::memory(addressWidth, valueWidth),
id, comment, flags);
1436 LeafPtr
makeVariable(
const Type&,
const std::string &comment=
"",
unsigned flags=0);
1437 LeafPtr
makeVariable(
const Type&, uint64_t
id,
const std::string &comment=
"",
unsigned flags=0);
1439 LeafPtr
makeIntegerVariable(
size_t nBits,
const std::string &comment=
"",
unsigned flags=0);
1440 LeafPtr
makeIntegerVariable(
size_t nBits, uint64_t
id,
const std::string &comment=
"",
unsigned flags=0);
1441 LeafPtr
makeIntegerConstant(
size_t nBits, uint64_t value,
const std::string &comment=
"",
unsigned flags=0);
1444 LeafPtr
makeMemoryVariable(
size_t addressWidth,
size_t valueWidth,
const std::string &comment=
"",
unsigned flags=0);
1445 LeafPtr
makeMemoryVariable(
size_t addressWidth,
size_t valueWidth, uint64_t
id,
const std::string &comment=
"",
unsigned flags=0);
1450 LeafPtr
makeFloatingPointNan(
size_t eb,
size_t sb,
const std::string &comment=
"",
unsigned flags=0);
1454 Ptr
makeVariable(
size_t nbits,
const std::string &comment=
"",
unsigned flags=0)
1455 ROSE_DEPRECATED("use makeIntegerVariable instead");
1456 Ptr makeExistingVariable(
size_t nbits, uint64_t
id, const
std::
string &comment="",
unsigned flags=0)
1457 ROSE_DEPRECATED("use makeIntegerVariable instead");
1458 Ptr makeInteger(
size_t nbits, uint64_t n, const
std::
string &comment="",
unsigned flags=0)
1459 ROSE_DEPRECATED("use makeIntegerConstant instead");
1460 Ptr
makeConstant(const
Sawyer::Container::BitVector&, const
std::
string &comment="",
unsigned flags=0)
1461 ROSE_DEPRECATED("use makeIntegerConstant instead");
1462 Ptr makeBoolean(
bool, const
std::
string &comment="",
unsigned flags=0)
1463 ROSE_DEPRECATED("use makeBooleanConstant instead");
1464 Ptr makeMemory(
size_t addressWidth,
size_t valueWidth, const
std::
string &comment="",
unsigned flags=0)
1465 ROSE_DEPRECATED("use makeMemoryVariable instead");
1466 Ptr makeExistingMemory(
size_t addressWidth,
size_t valueWidth, uint64_t
id, const
std::
string &comment="",
unsigned flags=0)
1467 ROSE_DEPRECATED("use makeMemoryVariable instead");
1475 Ptr
makeAdd(const Ptr&a, const Ptr &b,
1476 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1478 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0)
1479 ROSE_DEPRECATED("use
makeAnd instead");
1480 Ptr
makeAsr(const Ptr &sa, const Ptr &a,
1481 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1482 Ptr
makeAnd(const Ptr &a, const Ptr &b,
1483 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1484 Ptr
makeOr(const Ptr &a, const Ptr &b,
1485 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1486 Ptr
makeXor(const Ptr &a, const Ptr &b,
1487 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1489 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1491 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1492 Ptr
makeEq(const Ptr &a, const Ptr &b,
1493 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1494 Ptr
makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
1495 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1497 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1499 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1501 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1503 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1505 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1507 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1509 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1510 Ptr
makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
1511 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1512 Ptr
makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
1513 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1515 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1516 Ptr
makeMax(const Ptr &a, const Ptr &b,
1517 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1518 Ptr
makeMin(const Ptr &a, const Ptr &b,
1519 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1521 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1523 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1524 Ptr
makeNe(const Ptr &a, const Ptr &b,
1525 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1527 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1529 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0)
1530 ROSE_DEPRECATED("use
makeOr instead");
1531 Ptr
makeRead(const Ptr &mem, const Ptr &addr,
1532 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1534 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1535 Ptr
makeRol(const Ptr &sa, const Ptr &a,
1536 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1537 Ptr
makeRor(const Ptr &sa, const Ptr &a,
1538 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1540 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1541 Ptr
makeSet(const Ptr &a, const Ptr &b,
1542 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1543 Ptr
makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
1544 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1546 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1548 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1550 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1552 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1553 Ptr
makeShl0(const Ptr &sa, const Ptr &a,
1554 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1555 Ptr
makeShl1(const Ptr &sa, const Ptr &a,
1556 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1557 Ptr
makeShr0(const Ptr &sa, const Ptr &a,
1558 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1559 Ptr
makeShr1(const Ptr &sa, const Ptr &a,
1560 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1562 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1564 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1566 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1568 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1570 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1572 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1574 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1576 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1577 Ptr
makeDiv(const Ptr &a, const Ptr &b,
1578 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1579 Ptr
makeExtend(const Ptr &newSize, const Ptr &a,
1580 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1581 Ptr
makeGe(const Ptr &a, const Ptr &b,
1582 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1583 Ptr
makeGt(const Ptr &a, const Ptr &b,
1584 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1585 Ptr
makeLe(const Ptr &a, const Ptr &b,
1586 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1587 Ptr
makeLt(const Ptr &a, const Ptr &b,
1588 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1589 Ptr
makeMod(const Ptr &a, const Ptr &b,
1590 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1591 Ptr
makeMul(const Ptr &a, const Ptr &b,
1592 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1593 Ptr
makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
1594 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1596 const SmtSolverPtr &solver = SmtSolverPtr(), const
std::
string &comment="",
unsigned flags=0);
1605 std::ostream& operator<<(
std::ostream &o, const Node&);
1606 std::ostream& operator<<(
std::ostream &o, const Node::WithFormatter&);
1609 Ptr
setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
1615 Hash
hash(const
std::vector<Ptr>&);
1621 template<typename InputIterator>
1623 nNodes(InputIterator begin, InputIterator end) {
1625 for (InputIterator ii=begin; ii!=end; ++ii) {
1626 uint64_t n = (*ii)->nnodes();
1629 if (total + n < total)
1640 template<
typename InputIterator>
1645 typedef std::set<const Node*> SeenNodes;
1653 if (seen.insert(getRawPointer(node)).second) {
1667 for (InputIterator ii=begin; ii!=end &&
TERMINATE!=status; ++ii)
1668 status = (*ii)->depthFirstTraversal(visitor);
1669 return visitor.nUnique;
1680 template<
typename InputIterator>
1685 NodeCounts nodeCounts;
1686 std::vector<Ptr> result;
1688 VisitAction preVisit(
const Ptr &node) ROSE_OVERRIDE {
1689 size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1691 result.push_back(node);
1700 for (InputIterator ii=begin; ii!=end; ++ii)
1701 (*ii)->depthFirstTraversal(visitor);
1702 return visitor.result;
1713 template<
class Substitution>
1719 Ptr dst = subber(src, solver);
1720 ASSERT_not_null(dst);
1725 InteriorPtr inode = src->isInteriorNode();
1728 bool anyChildChanged =
false;
1730 newChildren.reserve(inode->nChildren());
1731 BOOST_FOREACH (
const Ptr &child, inode->children()) {
1732 Ptr newChild =
substitute(child, subber, solver);
1733 if (newChild != child)
1734 anyChildChanged =
true;
1735 newChildren.push_back(newChild);
1737 if (!anyChildChanged)
1741 return Interior::instance(inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
1748 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
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.
const std::string & comment() const
Property: Comment.
Sawyer::Optional< uint64_t > variableId() const
Variable ID number.
bool isFloatingPointExpr() const
True if this expression is of a floating-point type.
bool isHashed() const
Returns true if this node has a hash value computed and cached.
virtual uint64_t nNodes() const ROSE_OVERRIDE
Computes the size of an expression by counting the number of nodes.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Bitwise exclusive disjunction.
Ptr makeSignedLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
std::string comment_
Optional comment.
virtual size_t nChildren() const ROSE_OVERRIDE
Number of arguments.
virtual bool isVariable2() const ROSE_OVERRIDE
True if this expression is a variable.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
Use abbreviated names if possible.
bool matchAddVariableConstant(LeafPtr &variable, LeafPtr &constant) const
Determine whether an expression is a variable plus a constant.
static Type floatingPoint(size_t exponentWidth, size_t significandWidth)
Create a new floating-point type.
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.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr())=0
Substitute one value for another.
size_t nBits() const
Property: Total width of values.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
virtual bool isEquivalentTo(const Ptr &other)=0
Tests two expressions for structural equivalence.
Ptr makeReinterpret(const Ptr &a, const Type &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
Continue the traversal as normal.
Interior node of an expression tree for instruction semantics.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Sawyer::Optional< uint64_t > toUnsigned() const =0
The unsigned integer value of the expression.
Floating-point infinity class.
Ptr makeIsInfinite(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
boost::any userData_
Additional user-specified data.
virtual Operator getOperator() const ROSE_OVERRIDE
Operator for interior nodes.
bool isFloatingPointVariable() const
Is this node a floating-point variable?
Hash hashval_
Optional hash used as a quick way to indicate that two expressions are different. ...
Ptr makeRead(const Ptr &mem, const Ptr &addr, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeXor(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeSignedMod(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual void print(std::ostream &, Formatter &) const =0
Print the expression to a stream.
Floating-point greater than.
Floating-point round to integer as FP type.
Ptr makeSignedMin(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual bool isConstant() const =0
True if this expression is a constant.
virtual bool isEquivalentTo(const Ptr &other) ROSE_OVERRIDE
Tests two expressions for structural equivalence.
Mapping from expression to expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual size_t nChildren() const =0
Number of arguments.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const
Rewrite the entire expression to something simpler.
Shift left, introducing zeros at lsb.
LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0)
Leaf constructor.
bool isFloatingPointConstant() const
True if this epxression is a floating-point constant.
unsigned flags() const
Property: User-defined bit flags.
Ptr makeDiv(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
const boost::any & userData() const
Property: User-defined data.
virtual Ptr child(size_t idx) const ROSE_OVERRIDE
Argument.
Ptr makeMin(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
static Ptr instance(Operator op, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Create a new expression node.
VisitAction
Return type for visitors.
void userData(boost::any &data)
Property: User-defined data.
InteriorPtr isOperator(Operator) const
True (non-null) if this node is the specified operator.
void printAsUnsigned(std::ostream &o, Formatter &f) const
Prints an integer constant interpreted as an unsigned value.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isScalar() const
Check whether expression is scalar.
virtual size_t nChildren() const ROSE_OVERRIDE
Number of arguments.
Ptr makeLt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Most significant set bit or zero.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isScalarVariable() const
True if this expression is a scalar variable.
Ptr makeGt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Sawyer::Optional< uint64_t > toUnsigned() const ROSE_OVERRIDE
The unsigned integer value of the expression.
Sawyer::Container::Set< Ptr, ExpressionLessp > ExpressionSet
Set of expressions ordered by hash.
static const unsigned UNSPECIFIED
Value is somehow unspecified.
Read a value from memory.
Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Operator getOperator() const =0
Operator for interior nodes.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Shift right, introducing ones at msb.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual bool isConstant() const ROSE_OVERRIDE
True if this expression is a constant.
Type of symbolic expression.
Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr involutary()
Simplifies involutary operators.
Floating-point remainder.
Ptr setToIte(const Ptr &, const SmtSolverPtr &solver=SmtSolverPtr(), const LeafPtr &var=LeafPtr())
Convert a set to an ite expression.
bool isIntegerConstant() const
True if this expression is an integer constant.
bool isScalarExpr() const
True if the expression is a scalar type.
Main namespace for the ROSE library.
Floating-point greater-than or equal.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Interpret the value as a different type without converting.
virtual bool isVariable2() const =0
True if this expression is a variable.
Floating-point positive class.
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.
void adjustBitFlags(unsigned extraFlags)
Adjust user-defined bit flags.
Ptr makeIsNeg(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual const Nodes & children() const =0
Arguments.
Ptr makeSignedMax(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Least significant set bit or zero.
bool operator!=(const Type &other) const
Type equality.
Ptr poisonNan(const SmtSolverPtr &solver=SmtSolverPtr())
Returns NaN if any argument is NaN.
Ptr makeShl0(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeSignedGt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Flag
Flag to pass as type stringification style.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isMemoryExpr() const
True if this expression is of a memory type.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Name space for the entire library.
virtual void print(std::ostream &, Formatter &) const ROSE_OVERRIDE
Print the expression to a stream.
Shift left, introducing ones at lsb.
Unsigned greater-than-or-equal.
InteriorPtr isInteriorNode() const
Dynamic cast of this object to an interior node.
uint64_t nNodesUnique() const
Number of unique nodes in expression.
SharedPointer< Node > sharedFromThis()
Create a shared pointer from this.
TypeClass typeClass() const
Property: Type class.
Ptr makeOr(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Sawyer::Optional< int64_t > toSigned() const ROSE_OVERRIDE
The signed integer value of the expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr additiveNesting(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies nested shift-like operators.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
InteriorPtr associative()
Simplifies non-associative operators by flattening the specified interior node with its children that...
static Type none()
Create no type.
Ptr makeInvert(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeShr0(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual uint64_t nNodes() const =0
Computes the size of an expression by counting the number of nodes.
unsigned flags_
Bit flags.
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.
bool isFloatingPointNan() const
True if this expression is a floating-point NaN constant.
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.
virtual Ptr child(size_t idx) const =0
Argument.
Floating-point subnormal class.
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.
Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeConvert(const Ptr &a, const Type &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr())=0
Returns true if two expressions might be equal, but not necessarily be equal.
Floating-point less-than.
virtual VisitAction depthFirstTraversal(Visitor &) const ROSE_OVERRIDE
Traverse the expression.
virtual const Nodes & children() const ROSE_OVERRIDE
Arguments.
virtual VisitAction depthFirstTraversal(Visitor &) const =0
Traverse the expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Convert from one type to another.
LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr identity(uint64_t ident, const SmtSolverPtr &solver=SmtSolverPtr())
Removes identity arguments.
Ptr newFlags(unsigned flags) const
Sets flags.
static boost::logic::tribool(* mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr &)
User-supplied predicate to augment alias checking.
Ptr simplifyTop(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies the specified interior node.
Signed less-than-or-equal.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeSqrt(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeLssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isMemoryVariable() const
Is this node a memory variable?
Creates SharedPointer from this.
Ptr makeEq(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Unsigned extention at msb.
Ptr makeRol(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
std::string toString(TypeStyle::Flag style=TypeStyle::FULL) const
Print the type to a string.
Extract subsequence of bits.
Ptr makeIsSubnorm(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
void print(std::ostream &, TypeStyle::Flag style=TypeStyle::FULL) const
Print the type.
Floating-point NaN class.
Ptr makeSignedDiv(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeShl1(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isScalarConstant() const
True if this expression is a scalar constant.
virtual int compareStructure(const Ptr &other)=0
Compare two expressions structurally for sorting.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeMul(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Signed greater-than-or-equal.
Ptr makeNe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Sawyer::Optional< int64_t > toSigned() const =0
The signed integer value of the expression.
Ptr makeIsSignedPos(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t exponentWidth() const
Property: Exponent width.
virtual bool isVariable2() const ROSE_OVERRIDE
True if this expression is a variable.
Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeNegate(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeIsNan(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
InteriorPtr commutative()
Simplifies commutative operators by sorting arguments.
Ptr makeSignExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
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.
Floating-point less-than or equal.
void assertAcyclic() const
Asserts that expressions are acyclic.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
Floating-point zero class.
Type()
Create an invalid, empty type.
Sawyer::SharedPointer< Leaf > LeafPtr
Shared-ownership pointer to an expression Leaf node.
Base class for reference counted objects.
bool isIntegerVariable() const
True if this expression is an integer variable.
Ptr makeAnd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeIsPos(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
const Value & get() const
Dereference to obtain value.
Sawyer::SharedPointer< Interior > InteriorPtr
Shared-ownership pointer to an expression Interior node.
std::set< LeafPtr > getVariables() const
Returns the variables appearing in the expression.
Ptr makeMax(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isMemoryVariable() const
True if this expression is a memory state variable.
Floating-point normal class.
static Type integer(size_t nBits)
Create a new integer type.
Exceptions for symbolic expressions.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeSignedLt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0)
Leaf constructor.
bool isValid() const
Check whether this object is valid.
bool operator<(const Type &other) const
Type comparison.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Returns true if two expressions must be equal (cannot be unequal).
bool isFloatingPointVariable() const
True if this expression is a floating-point variable.
Base class for symbolic expression nodes.
Floating-point square root.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
Substitute one value for another.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
LeafPtr makeConstant(const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite expression by substituting subexpressions.
Ptr makeSet(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
void adjustWidth(const Type &)
Adjust width based on operands.
void print(std::ostream &o) const
Print the expression to a stream.
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.
Floating-point absolute value.
size_t addressWidth() const
Property: Width of memory addresses.
bool isEmpty() const
Determines if the vector is empty.
bool operator==(const Type &other) const
Type equality.
Ptr unaryNoOp()
Replaces a binary operator with its only argument.
API and storage for attributes.
size_t significandWidth() const
Property: Significand width.
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.
Floating-point negative class.
WithFormatter withFormat(Formatter &fmt)
Combines a node with a formatter for printing.
WithFormatter operator+(Formatter &fmt)
Combines a node with a formatter for printing.
virtual Ptr child(size_t idx) const ROSE_OVERRIDE
Argument.
Type type() const
Type of value.
Hash hash() const
Returns (and caches) the hash value for this node.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Floating-point multiply-add.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Base class for visiting nodes during expression traversal.
Ptr makeGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t domainWidth() const
Property: Width for memory expressions.
Base class for all ROSE exceptions.
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.
Ptr makeSignedGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Unsigned less-than-or-equal.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
bool isIntegerExpr() const
True if this expression is of an integer type.
static Type memory(size_t addressWidth, size_t valueWidth)
Create a new memory type.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
std::vector< Ptr > findCommonSubexpressions() const
Find common subexpressions.
LeafPtr isLeafNode() const
Dynamic cast of this object to a leaf node.
Ptr makeAdd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeMod(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Container associating values with keys.
Ptr foldConstants(const Simplifier &)
Perform constant folding.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const ROSE_OVERRIDE
Constant folding.
size_t nBits() const
Property: Number of significant bits.
Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver=SmtSolverPtr())
Simplify an interior node.
InteriorPtr idempotent(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies idempotent operators.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
Ptr makeSignedMul(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeRound(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeAsr(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Ptr makeIsNorm(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeZerop(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const
Constant folding.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const ROSE_OVERRIDE
Rewrite the entire expression to something simpler.
LeafPtr makeVariable(const Type &, const std::string &comment="", unsigned flags=0)
Leaf constructor.
For a pre-order depth-first visit, do not descend into children.