1 #ifndef ROSE_BinaryAnalysis_SymbolicExpression_H
2 #define ROSE_BinaryAnalysis_SymbolicExpression_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 <Rose/Exception.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>
36 namespace BinaryAnalysis {
43 namespace SymbolicExpression {
156 using Nodes = std::vector<Ptr>;
239 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
241 friend class boost::serialization::access;
244 void serialize(S &s,
const unsigned version) {
246 s & BOOST_SERIALIZATION_NVP(fields_);
250 size_t z2 = secondaryWidth();
251 s & boost::serialization::make_nvp(
"typeClass_", t);
252 s & boost::serialization::make_nvp(
"totalWidth_", z1);
253 s & boost::serialization::make_nvp(
"secondaryWidth_", z2);
301 return Type(
MEMORY, valueWidth, addressWidth);
313 return Type(
FP, 1 + exponentWidth + significandWidth - 1 , exponentWidth);
327 return (
TypeClass)((fields_ >> 30) & 0x3);
335 return fields_ & 0x7fff;
344 return secondaryWidth();
353 return secondaryWidth();
373 return fields_ == other.fields_;
376 return !(*
this == other);
393 ASSERT_require(n <= 3);
394 fields_ = (fields_ & 0x3fffffff) | (n << 30);
398 void nBits(
size_t n) {
400 throw Exception(
"type width is out of range");
401 fields_ = (fields_ & 0xffff8000) | n;
405 void secondaryWidth(
size_t n) {
407 throw Exception(
"second width is out of range");
408 fields_ = (fields_ & 0xc0007fff) | (n << 15);
411 size_t secondaryWidth()
const {
412 return (fields_ >> 15) & 0x7fff;
469 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
471 friend class boost::serialization::access;
474 void serialize(S &s,
const unsigned version) {
476 ASSERT_not_reachable(
"SymbolicExpression version " + boost::lexical_cast<std::string>(version) +
" is no longer supported");
477 s & BOOST_SERIALIZATION_NVP(type_);
478 s & BOOST_SERIALIZATION_NVP(flags_);
479 s & BOOST_SERIALIZATION_NVP(comment_);
480 s & BOOST_SERIALIZATION_NVP(hashval_);
502 static const unsigned BOTTOM = 0x00000004;
506 : type_(
Type::integer(0)), flags_(0), hashval_(0) {}
508 : type_(
Type::integer(0)), flags_(
flags), comment_(comment), hashval_(0) {}
590 virtual const Ptr&
child(
size_t idx)
const = 0;
597 virtual const Nodes&
children()
const = 0;
724 return type_.
nBits();
775 virtual uint64_t
nNodes()
const = 0;
805 return hashval_ != 0;
822 void print(std::ostream &stream)
const { node->print(stream, formatter); }
874 void printFlags(std::ostream &o,
unsigned flags,
char &bracket)
const;
877 using EquivPairs = std::map<Node*, std::vector<std::pair<Node*, bool>>>;
878 virtual bool isEquivalentHelper(
Node*, EquivPairs&) = 0;
889 virtual Ptr fold(Nodes::const_iterator , Nodes::const_iterator )
const {
901 size_t operator()(
const Ptr &expr)
const {
907 bool operator()(
const Ptr &a,
const Ptr &b)
const {
908 return a->isEquivalentTo(b);
915 bool operator()(
const Ptr &a,
const Ptr &b)
const;
919 class ExprExprHashMap:
public boost::unordered_map<SymbolicExpression::Ptr, SymbolicExpression::Ptr,
920 ExprExprHashMapHasher, ExprExprHashMapCompare> {
934 virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
938 virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
945 virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
949 virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
953 virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
956 virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
959 virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
1040 Ptr combine_strengths(
Ptr strength1,
Ptr strength2,
size_t value_width,
const SmtSolverPtr &solver)
const;
1081 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1083 friend class boost::serialization::access;
1086 void serialize(S &s,
const unsigned ) {
1087 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Node);
1088 s & BOOST_SERIALIZATION_NVP(op_);
1089 s & BOOST_SERIALIZATION_NVP(children_);
1090 s & BOOST_SERIALIZATION_NVP(nnodes_);
1134 virtual bool isEquivalentHelper(
Node*, EquivPairs&)
override;
1138 virtual uint64_t
nNodes()
const override {
return nnodes_; }
1139 virtual const Nodes&
children()
const override {
return children_; }
1141 virtual size_t nChildren()
const override {
return children_.size(); }
1142 virtual const Ptr&
child(
size_t idx)
const override;
1247 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1249 friend class boost::serialization::access;
1252 void save(S &s,
const unsigned )
const {
1253 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Node);
1254 s & BOOST_SERIALIZATION_NVP(bits_);
1255 s & BOOST_SERIALIZATION_NVP(name_);
1259 void load(S &s,
const unsigned ) {
1260 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Node);
1261 s & BOOST_SERIALIZATION_NVP(bits_);
1262 s & BOOST_SERIALIZATION_NVP(name_);
1263 nextNameCounter(name_);
1266 BOOST_SERIALIZATION_SPLIT_MEMBER();
1275 explicit Leaf(
const std::string &comment,
unsigned flags=0)
1276 :
Node(comment, flags), name_(0) {}
1282 const std::string &comment =
"",
unsigned flags = 0);
1286 const std::string &comment =
"",
unsigned flags = 0);
1290 const std::string &comment =
"",
unsigned flags = 0);
1297 virtual const Ptr&
child(
size_t idx)
const override;
1299 virtual const Nodes&
children()
const override;
1304 virtual bool isEquivalentHelper(
Node*, EquivPairs&)
override;
1308 virtual uint64_t
nNodes()
const override {
return 1; }
1362 static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1375 LeafPtr makeVariable(
const Type&, uint64_t
id,
const std::string &comment=
"",
unsigned flags=0);
1383 LeafPtr makeMemoryVariable(
size_t addressWidth,
size_t valueWidth, uint64_t
id,
const std::string &comment=
"",
unsigned flags=0);
1521 std::ostream& operator<<(std::ostream &o,
const Node&);
1522 std::ostream& operator<<(std::ostream &o,
const Node::WithFormatter&);
1531 Hash hash(
const std::vector<Ptr>&);
1537 template<
typename InputIterator>
1539 nNodes(InputIterator begin, InputIterator end) {
1541 for (InputIterator ii=begin; ii!=end; ++ii) {
1542 uint64_t n = (*ii)->nnodes();
1545 if (total + n < total)
1556 template<
typename InputIterator>
1561 typedef std::set<const Node*> SeenNodes;
1569 ASSERT_not_null(node);
1570 if (seen.insert(node).second) {
1584 for (InputIterator ii=begin; ii!=end &&
TERMINATE!=status; ++ii)
1585 status = (*ii)->depthFirstTraversal(visitor);
1586 return visitor.nUnique;
1597 template<
typename InputIterator>
1602 NodeCounts nodeCounts;
1603 std::vector<Ptr> result;
1606 ASSERT_not_null(node);
1607 size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1609 result.push_back(
Ptr(const_cast<Node*>(node)));
1618 for (InputIterator ii=begin; ii!=end; ++ii)
1619 (*ii)->depthFirstTraversal(visitor);
1620 return visitor.result;
1631 template<
class Substitution>
1637 Ptr dst = subber(src, solver);
1638 ASSERT_not_null(dst);
1646 bool anyChildChanged =
false;
1648 newChildren.reserve(inode->
nChildren());
1651 if (newChild != child)
1652 anyChildChanged =
true;
1653 newChildren.push_back(newChild);
1655 if (!anyChildChanged)
1669 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
Ptr makeAsr(const Ptr &sa, const Ptr &a, 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.
uint64_t nameId() const
Returns the name ID of a free variable.
static const unsigned INDETERMINATE
Value is somehow indeterminate.
static const unsigned UNSPECIFIED
Value is somehow unspecified.
virtual Operator getOperator() const =0
Operator for interior nodes.
Ptr makeConvert(const Ptr &a, const Type &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) override
Substitute one value for another.
static LeafPtr createConstant(const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0)
Create a constant.
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.
void addChild(const Ptr &child)
Appends child as a new child of this node.
bool isFloatingPointVariable() const
True if this expression is a floating-point variable.
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.
void printAsSigned(std::ostream &, Formatter &, bool asSigned=true) const
Prints an integer constant interpreted as a signed value.
Unsigned less-than-or-equal.
Hash hash() const
Returns (and caches) the hash value for this node.
LeafPtr isLeafNode() const
Dynamic cast of this object to a leaf node.
Floating-point square root.
Floating-point greater-than or equal.
virtual size_t nChildren() const override
Number of arguments.
virtual VisitAction depthFirstTraversal(Visitor &) const override
Traverse the expression.
bool isFloatingPointConstant() const
True if this epxression is a floating-point constant.
virtual bool isConstant() const =0
True if this expression is a constant.
std::string comment_
Optional comment.
Floating-point positive class.
virtual bool isVariable2() const override
True if this expression is a variable.
virtual Sawyer::Optional< int64_t > toSigned() const override
The signed integer value of the expression.
Ptr makeMul(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Continue the traversal as normal.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Compare two expressions for STL containers.
virtual Sawyer::Optional< uint64_t > toUnsigned() const =0
The unsigned integer value of the expression.
LeafPtr makeConstant(const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr makeIsNeg(const Ptr &a, 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.
Base class for visiting nodes during expression traversal.
virtual Sawyer::Optional< int64_t > toSigned() const override
The signed integer value of the expression.
Ptr makeSignedMin(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeGt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual uint64_t nNodes() const override
Computes the size of an expression by counting the number of nodes.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
std::string toString() const
Convert expression to string.
Floating-point round to integer as FP type.
virtual size_t nChildren() const override
Number of arguments.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
bool isMemoryExpr() const
True if this expression is of a memory type.
Ptr makeReinterpret(const Ptr &a, const Type &b, 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.
virtual Node * childRaw(size_t idx) const override
Argument.
Ptr makeSignedMul(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 override
Rewrite the entire expression to something simpler.
Ptr makeXor(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isFloatingPointVariable() const
Is this node a floating-point variable?
void print(std::ostream &o) const
Print the expression to a stream.
const boost::any & userData() const
Property: User-defined data.
InteriorPtr idempotent(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies idempotent operators.
Floating-point greater than.
Ptr makeIsInfinite(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 override
Constant folding.
bool matchAddVariableConstant(LeafPtr &variable, LeafPtr &constant) const
Determine whether an expression is a variable plus a constant.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Leaf constructor.
LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Operator
Operators for interior nodes of the expression tree.
Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite expression by substituting subexpressions.
Ptr makeSignedMod(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 makeSignedGt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeSignedLt(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
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.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
static LeafPtr createVariable(const Type &, const std::string &comment="", unsigned flags=0)
Create a new variable.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual VisitAction depthFirstTraversal(Visitor &) const override
Traverse the expression.
Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver=SmtSolverPtr())
On-the-fly substitutions.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Floating-point less-than or equal.
bool isFloatingPointExpr() const
True if this expression is of a floating-point type.
Base class for symbolic expression nodes.
Hash hashval_
Optional hash used as a quick way to indicate that two expressions are different. ...
Sawyer::SharedPointer< Leaf > LeafPtr
Reference counting pointer.
LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual void print(std::ostream &, Formatter &) const =0
Print the expression to a stream.
Mapping from expression to expression.
bool isMemoryVariable() const
Is this node a memory variable?
Ptr simplifyTop(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies the specified interior node.
static Type floatingPoint(size_t exponentWidth, size_t significandWidth)
Create a new floating-point type.
static Type integer(size_t nBits)
Create a new integer type.
VisitAction
Return type for visitors.
virtual bool isVariable2() const override
True if this expression is a variable.
Floating-point remainder.
virtual const Nodes & children() const override
Arguments.
Least significant set bit or zero.
bool isFloatingPointNan() const
True if this expression is a floating-point NaN constant.
Ptr foldConstants(const Simplifier &)
Perform constant folding.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isIntegerConstant() const
True if this expression is an integer constant.
virtual VisitAction depthFirstTraversal(Visitor &) const =0
Traverse the expression.
LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Main namespace for the ROSE library.
Ptr makeLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
static const unsigned RESERVED_FLAGS
These flags are reserved for use within ROSE.
bool isScalar() const
Check whether expression is scalar.
bool isIntegerVariable() const
Is this node an integer variable?
InteriorPtr isInteriorNode() const
Dynamic cast of this object to an interior node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeEq(const Ptr &a, const Ptr &b, 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.
Ptr makeSignedDiv(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.
void printAsUnsigned(std::ostream &o, Formatter &f) const
Prints an integer constant interpreted as an unsigned value.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions must be equal (cannot be unequal).
bool operator!=(const Type &other) const
Type equality.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions might be equal, but not necessarily be equal.
Ptr makeMod(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeOr(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
unsigned flags_
Bit flags.
Interior * isInteriorNodeRaw() const
Dynamic cast of this object to an interior node.
bool isValid() const
Check whether this object is valid.
Ptr identity(uint64_t ident, const SmtSolverPtr &solver=SmtSolverPtr())
Removes identity arguments.
Ptr makeIsPos(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Leaf * isLeafNodeRaw() const
Dynamic cast of this object to a leaf node.
size_t significandWidth() const
Property: Significand width.
Interpret the value as a different type without converting.
Ptr involutary()
Simplifies involutary operators.
bool isMemoryVariable() const
True if this expression is a memory state variable.
SharedPointer< Node > sharedFromThis()
Create a shared pointer from this.
Ptr makeLt(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 override
Rewrite the entire expression to something simpler.
Operator-specific simplification methods.
TypeClass typeClass() const
Property: Type class.
Type type() const
Type of value.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
WithFormatter operator+(Formatter &fmt)
Combines a node with a formatter for printing.
virtual bool isEquivalentTo(const Ptr &other) override
Tests two expressions for structural equivalence.
virtual void print(std::ostream &, Formatter &) const override
Print the expression to a stream.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr())=0
Returns true if two expressions must be equal (cannot be unequal).
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) override
Substitute one value for another.
bool isScalarVariable() const
True if this expression is a scalar variable.
static Type memory(size_t addressWidth, size_t valueWidth)
Create a new memory type.
Ptr makeSignedMax(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Shift right, introducing zeros at msb.
virtual int compareStructure(const Ptr &other)=0
Compare two expressions structurally for sorting.
Ptr makeMax(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
void userData(boost::any &data)
Property: User-defined data.
virtual Sawyer::Optional< int64_t > toSigned() const =0
The signed integer value of the expression.
Ptr renameVariables(ExprExprHashMap &index, size_t &nextVariableId, const SmtSolverPtr &solver=SmtSolverPtr())
Rewrite using lowest numbered variable names.
virtual uint64_t nNodes() const override
Computes the size of an expression by counting the number of nodes.
Ptr makeConcat(const Ptr &hi, const Ptr &lo, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Floating-point zero class.
Ptr makeIsNan(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 override
Constant folding.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
size_t exponentWidth() const
Property: Exponent width.
Ptr makeInvert(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Read a value from memory.
Extract subsequence of bits.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
static boost::logic::tribool(* mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr &)
User-supplied predicate to augment alias checking.
Use abbreviated names if possible.
size_t nBits() const
Property: Total width of values.
void assertAcyclic() const
Asserts that expressions are acyclic.
Ptr makeSqrt(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Floating-point negative class.
static Ptr instance(Operator op, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Create a new expression node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Creates SharedPointer from this.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool isConstant() const override
True if this expression is a constant.
Write (update) memory with a new value.
virtual uint64_t nNodes() const =0
Computes the size of an expression by counting the number of nodes.
Floating-point less-than.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
InteriorPtr commutative()
Simplifies commutative operators by sorting arguments.
virtual void print(std::ostream &, Formatter &) const override
Print the expression to a stream.
Ptr newFlags(unsigned flags) const
Sets flags.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Flag
Flag to pass as type stringification style.
std::set< LeafPtr > getVariables() const
Returns the variables appearing in the expression.
Ptr makeIsSignedPos(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual int compareStructure(const Ptr &other) override
Compare two expressions structurally for sorting.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
virtual bool isVariable2() const =0
True if this expression is a variable.
Ptr makeSignedLe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isIntegerExpr() const
True if this expression is of an integer type.
Shift left, introducing ones at lsb.
virtual size_t nChildren() const =0
Number of arguments.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
void adjustWidth(const Type &)
Adjust width based on operands.
InteriorPtr associative()
Simplifies non-associative operators by flattening the specified interior node with its children that...
Ptr makeLssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t nBits() const
Property: Number of significant bits.
Ptr makeSet(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isHashed() const
Returns true if this node has a hash value computed and cached.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const
Constant folding.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions might be equal, but not necessarily be equal.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool isEquivalentTo(const Ptr &other)=0
Tests two expressions for structural equivalence.
virtual const Ptr & child(size_t idx) const override
Argument.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Floating-point subnormal class.
uint64_t Hash
Hash of symbolic expression.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions must be equal (cannot be unequal).
bool isFloatingPointNan() const
Is this node a floating-point NaN constant?
const uint64_t MAX_NNODES
Maximum number of nodes that can be reported.
bool serializeVariableIds
Whether to serialize variable IDs.
Signed less-than-or-equal.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool isConstant() const override
True if this expression is a constant.
Ptr makeSignExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual const Node * childRaw(size_t) const override
Argument.
Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver=SmtSolverPtr())
Simplify an interior node.
Ptr makeRol(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeMssb(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual int compareStructure(const Ptr &other) override
Compare two expressions structurally for sorting.
Most significant set bit or zero.
Ptr makeZerop(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Operator getOperator() const override
Operator for interior nodes.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr())=0
Substitute one value for another.
WithFormatter withFormat(Formatter &fmt)
Combines a node with a formatter for printing.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr makeIsSubnorm(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
boost::any userData_
Additional user-specified data.
Base class for reference counted objects.
virtual const Node * childRaw(size_t idx) const =0
Argument.
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 makeShr1(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const
Rewrite the entire expression to something simpler.
Ptr unaryNoOp()
Replaces a binary operator with its only argument.
virtual const Ptr & child(size_t idx) const =0
Argument.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
virtual Sawyer::Optional< uint64_t > toUnsigned() const override
The unsigned integer value of the expression.
Exceptions for symbolic expressions.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Floating-point absolute value.
void comment(const std::string &s)
Property: Comment.
Ptr setToIte(const Ptr &, const SmtSolverPtr &solver=SmtSolverPtr(), const LeafPtr &var=LeafPtr())
Convert a set to an ite expression.
InteriorPtr isOperator(Operator) const
True (non-null) if this node is the specified operator.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
Floating-point NaN class.
Ptr makeShl1(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeShl0(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Sawyer::Optional< uint64_t > toUnsigned() const override
The unsigned integer value of the expression.
uint64_t nNodesUnique() const
Number of unique nodes in expression.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
Leaf node of an expression tree for instruction semantics.
const std::string & comment() const
Property: Comment.
Ptr makeRor(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeExtend(const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeIsNorm(const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
LeafPtr makeVariable(const Type &, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr makeShr0(const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
For a pre-order depth-first visit, do not descend into children.
virtual const Nodes & children() const override
Arguments.
Floating-point multiply-add.
LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Interior node of an expression tree for instruction semantics.
bool isEmpty() const
Determines if the vector is empty.
bool isScalarExpr() const
True if the expression is a scalar type.
virtual bool isEquivalentTo(const Ptr &other) override
Tests two expressions for structural equivalence.
API and storage for attributes.
Ptr poisonNan(const SmtSolverPtr &solver=SmtSolverPtr())
Returns NaN if any argument is NaN.
std::string toString(TypeStyle::Flag style=TypeStyle::FULL) const
Print the type to a string.
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.
Unsigned extention at msb.
Ptr makeSignedGe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Ptr makeDiv(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Shift right, introducing ones at msb.
Shift left, introducing zeros at lsb.
Type of symbolic expression.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
Floating-point normal class.
Ptr makeAnd(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
Sawyer::Container::Set< Ptr, ExpressionLessp > ExpressionSet
Set of expressions ordered by hash.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr additiveNesting(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies nested shift-like operators.
Base class for all ROSE exceptions.
virtual Operator getOperator() const override
Operator for interior nodes.
void adjustBitFlags(unsigned extraFlags)
Adjust user-defined bit flags.
std::vector< Ptr > findCommonSubexpressions() const
Find common subexpressions.
static Type none()
Create no type.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const 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.
virtual const Nodes & children() const =0
Arguments.
uint64_t nNodes(InputIterator begin, InputIterator end)
Counts the number of nodes.
virtual const Ptr & child(size_t idx) const override
Argument.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
unsigned flags() const
Property: User-defined bit flags.
Unsigned greater-than-or-equal.
bool operator<(const Type &other) const
Type comparison.
Ptr makeMin(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
size_t addressWidth() const
Property: Width of memory addresses.
Ptr makeNe(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
bool isIntegerVariable() const
True if this expression is an integer variable.
std::string toString() const
Returns a string for the leaf.
const Sawyer::Container::BitVector & bits() const
Property: Bits stored for numeric constants.
Container associating values with keys.
Ptr makeRead(const Ptr &mem, const Ptr &addr, 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.
Floating-point infinity class.
Type()
Create an invalid, empty type.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.
Convert from one type to another.
Bitwise exclusive disjunction.
Sawyer::Optional< uint64_t > variableId() const
Variable ID number.
bool operator==(const Type &other) const
Type equality.
size_t domainWidth() const
Property: Width for memory expressions.
Signed greater-than-or-equal.