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 <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 {
46 namespace SymbolicExpr {
177 typedef std::vector<Ptr> Nodes;
259 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
261 friend class boost::serialization::access;
264 void serialize(S &s,
const unsigned version) {
266 s & BOOST_SERIALIZATION_NVP(fields_);
270 size_t z2 = secondaryWidth();
271 s & boost::serialization::make_nvp(
"typeClass_", t);
272 s & boost::serialization::make_nvp(
"totalWidth_", z1);
273 s & boost::serialization::make_nvp(
"secondaryWidth_", z2);
321 return Type(
MEMORY, valueWidth, addressWidth);
333 return Type(
FP, 1 + exponentWidth + significandWidth - 1 , exponentWidth);
347 return (
TypeClass)((fields_ >> 30) & 0x3);
355 return fields_ & 0x7fff;
364 return secondaryWidth();
373 return secondaryWidth();
393 return fields_ == other.fields_;
396 return !(*
this == other);
413 ASSERT_require(n <= 3);
414 fields_ = (fields_ & 0x3fffffff) | (n << 30);
418 void nBits(
size_t n) {
420 throw Exception(
"type width is out of range");
421 fields_ = (fields_ & 0xffff8000) | n;
425 void secondaryWidth(
size_t n) {
427 throw Exception(
"second width is out of range");
428 fields_ = (fields_ & 0xc0007fff) | (n << 15);
431 size_t secondaryWidth()
const {
432 return (fields_ >> 15) & 0x7fff;
489 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
491 friend class boost::serialization::access;
494 void serialize(S &s,
const unsigned version) {
496 ASSERT_not_reachable(
"SymbolicExpr version " + boost::lexical_cast<std::string>(version) +
" is no longer supported");
497 s & BOOST_SERIALIZATION_NVP(type_);
498 s & BOOST_SERIALIZATION_NVP(flags_);
499 s & BOOST_SERIALIZATION_NVP(comment_);
500 s & BOOST_SERIALIZATION_NVP(hashval_);
522 static const unsigned BOTTOM = 0x00000004;
526 : type_(
Type::integer(0)), flags_(0), hashval_(0) {}
528 : type_(
Type::integer(0)), flags_(
flags), comment_(comment), hashval_(0) {}
610 virtual const Ptr&
child(
size_t idx)
const = 0;
617 virtual const Nodes&
children()
const = 0;
744 return type_.
nBits();
795 virtual uint64_t
nNodes()
const = 0;
825 return hashval_ != 0;
833 void hash(Hash)
const;
842 void print(std::ostream &stream)
const { node->print(stream, formatter); }
894 void printFlags(std::ostream &o,
unsigned flags,
char &bracket)
const;
897 using EquivPairs = std::map<Node*, std::vector<std::pair<Node*, bool>>>;
898 virtual bool isEquivalentHelper(
Node*, EquivPairs&) = 0;
909 virtual Ptr
fold(Nodes::const_iterator , Nodes::const_iterator )
const {
921 size_t operator()(
const Ptr &expr)
const {
927 bool operator()(
const Ptr &a,
const Ptr &b)
const {
928 return a->isEquivalentTo(b);
935 bool operator()(
const Ptr &a,
const Ptr &b)
const;
939 class ExprExprHashMap:
public boost::unordered_map<SymbolicExpr::Ptr, SymbolicExpr::Ptr,
940 ExprExprHashMapHasher, ExprExprHashMapCompare> {
954 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
958 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
965 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
969 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
973 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
976 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
979 virtual Ptr
fold(Nodes::const_iterator, Nodes::const_iterator)
const override;
1060 Ptr combine_strengths(Ptr strength1, Ptr strength2,
size_t value_width,
const SmtSolverPtr &solver)
const;
1101 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1103 friend class boost::serialization::access;
1106 void serialize(S &s,
const unsigned ) {
1107 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Node);
1108 s & BOOST_SERIALIZATION_NVP(op_);
1109 s & BOOST_SERIALIZATION_NVP(children_);
1110 s & BOOST_SERIALIZATION_NVP(nnodes_);
1154 virtual bool isEquivalentHelper(
Node*, EquivPairs&)
override;
1158 virtual uint64_t
nNodes()
const override {
return nnodes_; }
1159 virtual const Nodes&
children()
const override {
return children_; }
1161 virtual size_t nChildren()
const override {
return children_.size(); }
1162 virtual const Ptr&
child(
size_t idx)
const override;
1267 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
1269 friend class boost::serialization::access;
1272 void save(S &s,
const unsigned )
const {
1273 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Node);
1274 s & BOOST_SERIALIZATION_NVP(bits_);
1275 s & BOOST_SERIALIZATION_NVP(name_);
1279 void load(S &s,
const unsigned ) {
1280 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Node);
1281 s & BOOST_SERIALIZATION_NVP(bits_);
1282 s & BOOST_SERIALIZATION_NVP(name_);
1283 nextNameCounter(name_);
1286 BOOST_SERIALIZATION_SPLIT_MEMBER();
1295 explicit Leaf(
const std::string &comment,
unsigned flags=0)
1296 :
Node(comment, flags), name_(0) {}
1302 const std::string &comment =
"",
unsigned flags = 0);
1306 const std::string &comment =
"",
unsigned flags = 0);
1310 const std::string &comment =
"",
unsigned flags = 0);
1317 virtual const Ptr&
child(
size_t idx)
const override;
1318 virtual const Node*
childRaw(
size_t idx)
const override {
return nullptr; }
1319 virtual const Nodes&
children()
const override;
1324 virtual bool isEquivalentHelper(
Node*, EquivPairs&)
override;
1328 virtual uint64_t
nNodes()
const override {
return 1; }
1382 static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
1394 LeafPtr
makeVariable(
const Type&,
const std::string &comment=
"",
unsigned flags=0);
1395 LeafPtr
makeVariable(
const Type&, uint64_t
id,
const std::string &comment=
"",
unsigned flags=0);
1397 LeafPtr
makeIntegerVariable(
size_t nBits,
const std::string &comment=
"",
unsigned flags=0);
1398 LeafPtr
makeIntegerVariable(
size_t nBits, uint64_t
id,
const std::string &comment=
"",
unsigned flags=0);
1399 LeafPtr
makeIntegerConstant(
size_t nBits, uint64_t value,
const std::string &comment=
"",
unsigned flags=0);
1402 LeafPtr
makeMemoryVariable(
size_t addressWidth,
size_t valueWidth,
const std::string &comment=
"",
unsigned flags=0);
1403 LeafPtr
makeMemoryVariable(
size_t addressWidth,
size_t valueWidth, uint64_t
id,
const std::string &comment=
"",
unsigned flags=0);
1408 LeafPtr
makeFloatingPointNan(
size_t eb,
size_t sb,
const std::string &comment=
"",
unsigned flags=0);
1417 Ptr
makeAdd(
const Ptr&a,
const Ptr &b,
1419 Ptr
makeAsr(
const Ptr &sa,
const Ptr &a,
1421 Ptr
makeAnd(
const Ptr &a,
const Ptr &b,
1423 Ptr
makeOr(
const Ptr &a,
const Ptr &b,
1425 Ptr
makeXor(
const Ptr &a,
const Ptr &b,
1431 Ptr
makeEq(
const Ptr &a,
const Ptr &b,
1433 Ptr
makeExtract(
const Ptr &begin,
const Ptr &end,
const Ptr &a,
1449 Ptr
makeIte(
const Ptr &cond,
const Ptr &a,
const Ptr &b,
1451 Ptr
makeLet(
const Ptr &a,
const Ptr &b,
const Ptr &c,
1455 Ptr
makeMax(
const Ptr &a,
const Ptr &b,
1457 Ptr
makeMin(
const Ptr &a,
const Ptr &b,
1463 Ptr
makeNe(
const Ptr &a,
const Ptr &b,
1467 Ptr
makeRead(
const Ptr &mem,
const Ptr &addr,
1471 Ptr
makeRol(
const Ptr &sa,
const Ptr &a,
1473 Ptr
makeRor(
const Ptr &sa,
const Ptr &a,
1477 Ptr
makeSet(
const Ptr &a,
const Ptr &b,
1479 Ptr
makeSet(
const Ptr &a,
const Ptr &b,
const Ptr &c,
1489 Ptr
makeShl0(
const Ptr &sa,
const Ptr &a,
1491 Ptr
makeShl1(
const Ptr &sa,
const Ptr &a,
1493 Ptr
makeShr0(
const Ptr &sa,
const Ptr &a,
1495 Ptr
makeShr1(
const Ptr &sa,
const Ptr &a,
1513 Ptr
makeDiv(
const Ptr &a,
const Ptr &b,
1515 Ptr
makeExtend(
const Ptr &newSize,
const Ptr &a,
1517 Ptr
makeGe(
const Ptr &a,
const Ptr &b,
1519 Ptr
makeGt(
const Ptr &a,
const Ptr &b,
1521 Ptr
makeLe(
const Ptr &a,
const Ptr &b,
1523 Ptr
makeLt(
const Ptr &a,
const Ptr &b,
1525 Ptr
makeMod(
const Ptr &a,
const Ptr &b,
1527 Ptr
makeMul(
const Ptr &a,
const Ptr &b,
1529 Ptr
makeWrite(
const Ptr &mem,
const Ptr &addr,
const Ptr &a,
1541 std::ostream& operator<<(std::ostream &o,
const Node&);
1542 std::ostream& operator<<(std::ostream &o,
const Node::WithFormatter&);
1551 Hash
hash(
const std::vector<Ptr>&);
1557 template<
typename InputIterator>
1559 nNodes(InputIterator begin, InputIterator end) {
1561 for (InputIterator ii=begin; ii!=end; ++ii) {
1562 uint64_t n = (*ii)->nnodes();
1565 if (total + n < total)
1576 template<
typename InputIterator>
1581 typedef std::set<const Node*> SeenNodes;
1589 ASSERT_not_null(node);
1590 if (seen.insert(node).second) {
1604 for (InputIterator ii=begin; ii!=end &&
TERMINATE!=status; ++ii)
1605 status = (*ii)->depthFirstTraversal(visitor);
1606 return visitor.nUnique;
1617 template<
typename InputIterator>
1622 NodeCounts nodeCounts;
1623 std::vector<Ptr> result;
1626 ASSERT_not_null(node);
1627 size_t &nSeen = nodeCounts.insertMaybe(node, 0);
1629 result.push_back(
Ptr(const_cast<Node*>(node)));
1638 for (InputIterator ii=begin; ii!=end; ++ii)
1639 (*ii)->depthFirstTraversal(visitor);
1640 return visitor.result;
1651 template<
class Substitution>
1657 Ptr dst = subber(src, solver);
1658 ASSERT_not_null(dst);
1666 bool anyChildChanged =
false;
1668 newChildren.reserve(inode->
nChildren());
1669 for (
const Ptr &child: inode->
children()) {
1670 Ptr newChild =
substitute(child, subber, solver);
1671 if (newChild != child)
1672 anyChildChanged =
true;
1673 newChildren.push_back(newChild);
1675 if (!anyChildChanged)
1689 #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 Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
const std::string & comment() const
Property: Comment.
Sawyer::Optional< uint64_t > variableId() const
Variable ID number.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions might be equal, but not necessarily be equal.
bool isFloatingPointExpr() const
True if this expression is of a floating-point type.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
static LeafPtr createVariable(const Type &, const std::string &comment="", unsigned flags=0)
Create a new variable.
virtual const Node * childRaw(size_t idx) const =0
Argument.
bool isHashed() const
Returns true if this node has a hash value computed and cached.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const 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.
virtual bool isConstant() const override
True if this expression is a constant.
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
std::string comment_
Optional comment.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Sawyer::Optional< uint64_t > toUnsigned() const override
The unsigned integer value of the expression.
Use abbreviated names if possible.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions must be equal (cannot be unequal).
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 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 rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Continue the traversal as normal.
Interior node of an expression tree for instruction semantics.
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.
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. ...
virtual const Ptr & child(size_t idx) const override
Argument.
Ptr makeRead(const Ptr &mem, const Ptr &addr, 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.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
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.
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.
Floating-point round to integer as FP type.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Leaf * isLeafNodeRaw() const
Dynamic cast of this object to a leaf node.
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.
Mapping from expression to expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
uint64_t nameId() const
Returns the name ID of a free variable.
virtual size_t nChildren() const =0
Number of arguments.
virtual Node * childRaw(size_t idx) const override
Argument.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
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 fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
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.
virtual size_t nChildren() const override
Number of arguments.
virtual VisitAction depthFirstTraversal(Visitor &) const override
Traverse the expression.
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 override
Rewrite the entire expression to something simpler.
bool isScalar() const
Check whether expression is scalar.
std::string toString() const
Convert expression to string.
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.
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.
Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver=SmtSolverPtr())
On-the-fly substitutions.
bool isIntegerVariable() const
Is this node an integer variable?
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 bool isConstant() const override
True if this expression is a constant.
Shift right, introducing ones at msb.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
virtual const Nodes & children() const override
Arguments.
Type of symbolic expression.
virtual Sawyer::Optional< int64_t > toSigned() const override
The signed integer value of the 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.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
virtual int compareStructure(const Ptr &other) override
Compare two expressions structurally for sorting.
Ptr involutary()
Simplifies involutary operators.
virtual void print(std::ostream &, Formatter &) const override
Print the expression to a stream.
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.
Interpret the value as a different type without converting.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual bool isVariable2() const =0
True if this expression is a variable.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
virtual Sawyer::Optional< int64_t > toSigned() const override
The signed integer value of the expression.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
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.
virtual bool isEquivalentTo(const Ptr &other) override
Tests two expressions for structural equivalence.
virtual size_t nChildren() const override
Number of arguments.
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 fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
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 Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
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.
static LeafPtr createConstant(const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0)
Create a constant.
Flag
Flag to pass as type stringification style.
bool isMemoryExpr() const
True if this expression is of a memory 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.
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.
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 VisitAction depthFirstTraversal(Visitor &) const override
Traverse the expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const 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.
InteriorPtr associative()
Simplifies non-associative operators by flattening the specified interior node with its children that...
bool serializeVariableIds
Whether to serialize variable IDs.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const 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.
Floating-point subnormal class.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
virtual bool isVariable2() const override
True if this expression is a variable.
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.
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 =0
Traverse the expression.
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.
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.
virtual const Node * childRaw(size_t idx) const override
Argument.
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.
uint64_t nNodes(InputIterator begin, InputIterator end)
Counts the number of nodes.
bool isScalarConstant() const
True if this expression is a scalar constant.
virtual int compareStructure(const Ptr &other)=0
Compare two expressions structurally for sorting.
Ptr makeMul(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()) override
Returns true if two expressions might be equal, but not necessarily be equal.
Signed greater-than-or-equal.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const 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.
virtual Sawyer::Optional< int64_t > toSigned() const =0
The signed integer value of the expression.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
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 Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) override
Substitute one value for another.
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 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.
virtual int compareStructure(const Ptr &other) override
Compare two expressions structurally for sorting.
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.
void comment(const std::string &s)
Property: Comment.
static const unsigned RESERVED_FLAGS
These flags are reserved for use within ROSE.
Floating-point less-than or equal.
void assertAcyclic() const
Asserts that expressions are acyclic.
Floating-point zero class.
Type()
Create an invalid, empty type.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override
Constant folding.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Sawyer::SharedPointer< Interior > InteriorPtr
Shared-ownership pointer to an expression Interior node.
std::set< LeafPtr > getVariables() const
Returns the variables appearing in the expression.
virtual Sawyer::Optional< uint64_t > toUnsigned() const override
The unsigned integer value of the expression.
Ptr makeMax(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.
bool isMemoryVariable() const
True if this expression is a memory state variable.
void printAsSigned(std::ostream &, Formatter &, bool asSigned=true) const
Prints an integer constant interpreted as a signed value.
Floating-point normal class.
static Type integer(size_t nBits)
Create a new integer type.
Exceptions for symbolic expressions.
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.
bool isFloatingPointVariable() const
True if this expression is a floating-point variable.
Base class for symbolic expression nodes.
Floating-point square root.
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 isFloatingPointNan() const
Is this node a floating-point NaN constant?
bool isEmpty() const
Determines if the vector is empty.
virtual uint64_t nNodes() const override
Computes the size of an expression by counting the number of nodes.
bool operator==(const Type &other) const
Type equality.
Ptr unaryNoOp()
Replaces a binary operator with its only argument.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
API and storage for attributes.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
size_t significandWidth() const
Property: Significand width.
Compare two expressions for STL containers.
virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override
Returns true if two expressions must be equal (cannot be unequal).
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 const Nodes & children() const override
Arguments.
Floating-point negative class.
WithFormatter withFormat(Formatter &fmt)
Combines a node with a formatter for printing.
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.
Type type() const
Type of value.
Hash hash() const
Returns (and caches) the hash value for this node.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Floating-point multiply-add.
Interior * isInteriorNodeRaw() 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.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Write (update) memory with a new value.
virtual Operator getOperator() const override
Operator for interior nodes.
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.
std::vector< Ptr > findCommonSubexpressions(const std::vector< Ptr > &)
Find common subexpressions.
virtual const Ptr & child(size_t idx) const =0
Argument.
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 void print(std::ostream &, Formatter &) const override
Print the expression to a stream.
std::vector< Ptr > findCommonSubexpressions() const
Find common subexpressions.
virtual Operator getOperator() const override
Operator for interior nodes.
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.
virtual Ptr rewrite(Interior *, const SmtSolverPtr &) const override
Rewrite the entire expression to something simpler.
Ptr foldConstants(const Simplifier &)
Perform constant folding.
virtual bool isVariable2() const override
True if this expression is a variable.
size_t nBits() const
Property: Number of significant bits.
Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver=SmtSolverPtr())
Simplify an interior node.
virtual uint64_t nNodes() const override
Computes the size of an expression by counting the number of nodes.
InteriorPtr idempotent(const SmtSolverPtr &solver=SmtSolverPtr())
Simplifies idempotent operators.
Ptr makeSignedMul(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
virtual const Ptr & child(size_t idx) const override
Argument.
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.
virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) override
Substitute one value for another.
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 bool isEquivalentTo(const Ptr &other) override
Tests two expressions for structural equivalence.
std::string toString() const
Returns a string for the leaf.
virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const
Constant folding.
const Sawyer::Container::BitVector & bits() const
Property: Bits stored for numeric constants.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.
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.