Description
Leaf node of an expression tree for instruction semantics.
A leaf node is either a known bit vector value, a free bit vector variable, or a memory state.
Definition at line 1238 of file SymbolicExpr.h.
#include <Rose/BinaryAnalysis/SymbolicExpr.h>
Public Member Functions | |
| virtual size_t | nChildren () const override |
| Number of arguments. More... | |
| virtual const Ptr & | child (size_t idx) const override |
| Argument. More... | |
| virtual const Node * | childRaw (size_t idx) const override |
| Argument. More... | |
| virtual const Nodes & | children () const override |
| Arguments. More... | |
| virtual Operator | getOperator () const override |
| Operator for interior nodes. More... | |
| virtual bool | mustEqual (const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override |
| Returns true if two expressions must be equal (cannot be unequal). More... | |
| virtual bool | mayEqual (const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) override |
| Returns true if two expressions might be equal, but not necessarily be equal. More... | |
| virtual bool | isEquivalentTo (const Ptr &other) override |
| Tests two expressions for structural equivalence. More... | |
| virtual bool | isEquivalentHelper (Node *, EquivPairs &) override |
| virtual int | compareStructure (const Ptr &other) override |
| Compare two expressions structurally for sorting. More... | |
| virtual Ptr | substitute (const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) override |
| Substitute one value for another. More... | |
| virtual VisitAction | depthFirstTraversal (Visitor &) const override |
| Traverse the expression. More... | |
| virtual uint64_t | nNodes () const override |
| Computes the size of an expression by counting the number of nodes. More... | |
| virtual Sawyer::Optional< uint64_t > | toUnsigned () const override |
| The unsigned integer value of the expression. More... | |
| virtual Sawyer::Optional< int64_t > | toSigned () const override |
| The signed integer value of the expression. More... | |
| virtual bool | isConstant () const override |
| True if this expression is a constant. More... | |
| virtual bool | isVariable2 () const override |
| True if this expression is a variable. More... | |
| virtual void | print (std::ostream &, Formatter &) const override |
| Print the expression to a stream. More... | |
| const Sawyer::Container::BitVector & | bits () const |
| Property: Bits stored for numeric constants. More... | |
| bool | isIntegerVariable () const |
| Is this node an integer variable? | |
| bool | isFloatingPointVariable () const |
| Is this node a floating-point variable? | |
| bool | isFloatingPointNan () const |
| Is this node a floating-point NaN constant? | |
| bool | isMemoryVariable () const |
| Is this node a memory variable? | |
| uint64_t | nameId () const |
| Returns the name ID of a free variable. More... | |
| std::string | toString () const |
| Returns a string for the leaf. More... | |
| void | printAsSigned (std::ostream &, Formatter &, bool asSigned=true) const |
| Prints an integer constant interpreted as a signed value. More... | |
| void | printAsUnsigned (std::ostream &o, Formatter &f) const |
| Prints an integer constant interpreted as an unsigned value. More... | |
 Public Member Functions inherited from Rose::BinaryAnalysis::SymbolicExpr::Node | |
| Type | type () const |
| Type of value. More... | |
| Ptr | substituteMultiple (const ExprExprHashMap &substitutions, const SmtSolverPtr &solver=SmtSolverPtr()) |
| Rewrite expression by substituting subexpressions. More... | |
| Ptr | renameVariables (ExprExprHashMap &index, size_t &nextVariableId, const SmtSolverPtr &solver=SmtSolverPtr()) |
| Rewrite using lowest numbered variable names. More... | |
| bool | isIntegerExpr () const |
| True if this expression is of an integer type. More... | |
| bool | isFloatingPointExpr () const |
| True if this expression is of a floating-point type. More... | |
| bool | isMemoryExpr () const |
| True if this expression is of a memory type. More... | |
| bool | isScalarExpr () const |
| True if the expression is a scalar type. More... | |
| bool | isIntegerConstant () const |
| True if this expression is an integer constant. More... | |
| bool | isFloatingPointConstant () const |
| True if this epxression is a floating-point constant. More... | |
| bool | isScalarConstant () const |
| True if this expression is a scalar constant. More... | |
| bool | isFloatingPointNan () const |
| True if this expression is a floating-point NaN constant. More... | |
| Sawyer::Optional< uint64_t > | variableId () const |
| Variable ID number. More... | |
| bool | isIntegerVariable () const |
| True if this expression is an integer variable. More... | |
| bool | isFloatingPointVariable () const |
| True if this expression is a floating-point variable. More... | |
| bool | isMemoryVariable () const |
| True if this expression is a memory state variable. More... | |
| bool | isScalarVariable () const |
| True if this expression is a scalar variable. More... | |
| size_t | nBits () const |
| Property: Number of significant bits. More... | |
| unsigned | flags () const |
| Property: User-defined bit flags. More... | |
| Ptr | newFlags (unsigned flags) const |
| Sets flags. More... | |
| size_t | domainWidth () const |
| Property: Width for memory expressions. More... | |
| bool | isScalar () const |
| Check whether expression is scalar. More... | |
| uint64_t | nNodesUnique () const |
| Number of unique nodes in expression. More... | |
| std::set< LeafPtr > | getVariables () const |
| Returns the variables appearing in the expression. More... | |
| bool | isHashed () const |
| Returns true if this node has a hash value computed and cached. More... | |
| Hash | hash () const |
| Returns (and caches) the hash value for this node. More... | |
| void | hash (Hash) const |
| std::string | toString () const |
| Convert expression to string. More... | |
| void | assertAcyclic () const |
| Asserts that expressions are acyclic. More... | |
| std::vector< Ptr > | findCommonSubexpressions () const |
| Find common subexpressions. More... | |
| bool | matchAddVariableConstant (LeafPtr &variable, LeafPtr &constant) const |
| Determine whether an expression is a variable plus a constant. More... | |
| InteriorPtr | isOperator (Operator) const |
| True (non-null) if this node is the specified operator. More... | |
| const std::string & | comment () const |
| Property: Comment. More... | |
| void | comment (const std::string &s) |
| Property: Comment. More... | |
| void | userData (boost::any &data) |
| Property: User-defined data. More... | |
| const boost::any & | userData () const |
| Property: User-defined data. More... | |
| InteriorPtr | isInteriorNode () const |
| Dynamic cast of this object to an interior node. More... | |
| Interior * | isInteriorNodeRaw () const |
| Dynamic cast of this object to an interior node. More... | |
| LeafPtr | isLeafNode () const |
| Dynamic cast of this object to a leaf node. More... | |
| Leaf * | isLeafNodeRaw () const |
| Dynamic cast of this object to a leaf node. More... | |
| WithFormatter | withFormat (Formatter &fmt) |
| Combines a node with a formatter for printing. More... | |
| WithFormatter | operator+ (Formatter &fmt) |
| Combines a node with a formatter for printing. More... | |
| void | print (std::ostream &o) const |
| Print the expression to a stream. More... | |
| Public Member Functions inherited from Sawyer::SharedObject | |
| SharedObject () | |
| Default constructor. More... | |
| SharedObject (const SharedObject &) | |
| Copy constructor. More... | |
| virtual | ~SharedObject () |
| Virtual destructor. More... | |
| SharedObject & | operator= (const SharedObject &) |
| Assignment. More... | |
| Public Member Functions inherited from Sawyer::SharedFromThis< Node > | |
| SharedPointer< Node > | sharedFromThis () |
Create a shared pointer from this. More... | |
| SharedPointer< const Node > | sharedFromThis () const |
Create a shared pointer from this. More... | |
| Public Member Functions inherited from Sawyer::Attribute::Storage<> | |
| Storage () | |
| Default constructor. More... | |
| Storage (const Storage &other) | |
| Copy constructor. More... | |
| Storage & | operator= (const Storage &other) |
| Assignment operator. More... | |
| bool | attributeExists (Id id) const |
| Check attribute existence. More... | |
| void | eraseAttribute (Id id) |
| Erase an attribute. More... | |
| void | clearAttributes () |
| Erase all attributes. More... | |
| void | setAttribute (Id id, const T &value) |
| Store an attribute. More... | |
| bool | setAttributeMaybe (Id id, const T &value) |
| Store an attribute if not already present. More... | |
| T | getAttribute (Id id) const |
| Get an attribute that is known to exist. More... | |
| T | attributeOrElse (Id id, const T &dflt) const |
| Return an attribute or a specified value. More... | |
| T | attributeOrDefault (Id id) const |
| Return an attribute or a default-constructed value. More... | |
| Sawyer::Optional< T > | optionalAttribute (Id id) const |
| Return the attribute as an optional value. More... | |
| size_t | nAttributes () const |
| Number of attributes stored. More... | |
| std::vector< Id > | attributeIds () const |
| Returns ID numbers for all IDs stored in this container. More... | |
Static Public Member Functions | |
| static LeafPtr | createVariable (const Type &, const std::string &comment="", unsigned flags=0) |
| Create a new variable. More... | |
| static LeafPtr | createVariable (const Type &, const uint64_t id, const std::string &comment="", unsigned flags=0) |
| Create an existing variable. More... | |
| static LeafPtr | createConstant (const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0) |
| Create a constant. More... | |
| Static Public Member Functions inherited from Sawyer::SmallObject | |
| static SynchronizedPoolAllocator & | poolAllocator () |
| Return the pool allocator for this class. More... | |
| static void * | operator new (size_t size) |
| static void | operator delete (void *ptr, size_t size) |
Additional Inherited Members | |
| Public Types inherited from Rose::BinaryAnalysis::SymbolicExpr::Node | |
| using | EquivPairs = std::map< Node *, std::vector< std::pair< Node *, bool >>> |
| Public Types inherited from Sawyer::Attribute::Storage<> | |
| typedef SynchronizationTraits< Sawyer::SingleThreadedTag > | Sync |
| Static Public Attributes inherited from Rose::BinaryAnalysis::SymbolicExpr::Node | |
| static const unsigned | RESERVED_FLAGS = 0x0000ffff |
| These flags are reserved for use within ROSE. More... | |
| static const unsigned | INDETERMINATE = 0x00000001 |
| Value is somehow indeterminate. More... | |
| static const unsigned | UNSPECIFIED = 0x00000002 |
| Value is somehow unspecified. More... | |
| static const unsigned | BOTTOM = 0x00000004 |
| Value represents bottom in dataflow analysis. More... | |
| static boost::logic::tribool(* | mayEqualCallback )(const Ptr &a, const Ptr &b, const SmtSolverPtr &) |
| User-supplied predicate to augment alias checking. More... | |
| Protected Member Functions inherited from Rose::BinaryAnalysis::SymbolicExpr::Node | |
| Node (const std::string &comment, unsigned flags=0) | |
| void | printFlags (std::ostream &o, unsigned flags, char &bracket) const |
| Protected Attributes inherited from Rose::BinaryAnalysis::SymbolicExpr::Node | |
| Type | type_ |
| unsigned | flags_ |
| Bit flags. More... | |
| std::string | comment_ |
| Optional comment. More... | |
| Hash | hashval_ |
| Optional hash used as a quick way to indicate that two expressions are different. More... | |
| boost::any | userData_ |
| Additional user-specified data. More... | |
Member Function Documentation
|
static |
Create a new variable.
|
static |
Create an existing variable.
|
static |
Create a constant.
|
inlineoverridevirtual |
Number of arguments.
Returns the number of children for an interior node, zero for leaf nodes.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
Definition at line 1295 of file SymbolicExpr.h.
|
overridevirtual |
Argument.
Returns the specified argument by index. If the index is out of range, then returns null. A leaf node always returns null since it never has children.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
inlineoverridevirtual |
Argument.
Returns the specified argument by index. If the index is out of range, then returns null. A leaf node always returns null since it never has children.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
Definition at line 1297 of file SymbolicExpr.h.
|
overridevirtual |
Arguments.
Returns the arguments of an operation for an interior node, or an empty list for a leaf node.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
inlineoverridevirtual |
Operator for interior nodes.
Return the operator for interior nodes, or OP_NONE for leaf nodes that have no operator.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
Definition at line 1299 of file SymbolicExpr.h.
References Rose::BinaryAnalysis::SymbolicExpr::OP_NONE.
|
overridevirtual |
Returns true if two expressions must be equal (cannot be unequal).
If an SMT solver is specified then that solver is used to answer this question, otherwise equality is established by looking only at the structure of the two expressions. Two expressions can be equal without being the same width (e.g., a 32-bit constant zero is equal to a 16-bit constant zero).
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
overridevirtual |
Returns true if two expressions might be equal, but not necessarily be equal.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
overridevirtual |
Tests two expressions for structural equivalence.
Two leaf nodes are equivalent if they are the same width and have equal values or are the same variable. Two interior nodes are equivalent if they are the same width, the same operation, have the same number of children, and those children are all pairwise equivalent.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
overridevirtual |
Compare two expressions structurally for sorting.
Returns -1 if this is less than other, 0 if they are structurally equal, and 1 if this is greater than other. This function returns zero when an only when isEquivalentTo returns zero, but isEquivalentTo can be much faster since it uses hashing.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
overridevirtual |
Substitute one value for another.
Finds all occurrances of from in this expression and replace them with to. If a substitution occurs, then a new expression is returned. The matching of from to sub-parts of this expression uses structural equivalence, the isEquivalentTo predicate. The from and to expressions must have the same width.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
overridevirtual |
Traverse the expression.
The expression is traversed in a depth-first visit. The final return value is the final return value of the last call to the visitor.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
inlineoverridevirtual |
Computes the size of an expression by counting the number of nodes.
Operates in constant time. Note that it is possible (even likely) for the 64-bit return value to overflow in expressions when many nodes are shared. For instance, the following loop will create an expression that contains more than 2^64 nodes:
When an overflow occurs the result is meaningless.
- See also
- nNodesUnique
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
Definition at line 1307 of file SymbolicExpr.h.
|
overridevirtual |
The unsigned integer value of the expression.
Returns nothing if the expression is not a concrete integer value or the value is too wide to be represented by the return type.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
overridevirtual |
The signed integer value of the expression.
Returns nothing if the expression is not a concrete integer value or the value doesn't fit in the return type.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
|
inlineoverridevirtual |
True if this expression is a constant.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
Definition at line 1310 of file SymbolicExpr.h.
References Sawyer::Container::BitVector::isEmpty().
Referenced by isFloatingPointVariable(), isIntegerVariable(), isMemoryVariable(), and isVariable2().
|
inlineoverridevirtual |
True if this expression is a variable.
Warning: Leaf nodes have a deprecated isVariable method that returns false for memory state variables, thus this method has a "2" appended to its name. After a suitable period of deprecation for Leaf::isVariable, a new isVariable will be added to this class hiearchy and will have the same semantics as isVariable2, which will become deprecated.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
Definition at line 1311 of file SymbolicExpr.h.
References isConstant().
|
overridevirtual |
Print the expression to a stream.
The output is an S-expression with no line-feeds. The format of the output is controlled by the mutable Formatter argument.
Implements Rose::BinaryAnalysis::SymbolicExpr::Node.
| const Sawyer::Container::BitVector& Rose::BinaryAnalysis::SymbolicExpr::Leaf::bits | ( | ) | const |
Property: Bits stored for numeric constants.
| uint64_t Rose::BinaryAnalysis::SymbolicExpr::Leaf::nameId | ( | ) | const |
Returns the name ID of a free variable.
The output functions print variables as "vN" where N is an integer. It is this N that this method returns. It should only be invoked on leaf nodes for which isConstant returns false.
| std::string Rose::BinaryAnalysis::SymbolicExpr::Leaf::toString | ( | ) | const |
Returns a string for the leaf.
Integer and floating-point variables are returned as "vN", memory variables are returned as "mN", and constants are returned as a hexadecimal string, where N is a variable identification number.
| void Rose::BinaryAnalysis::SymbolicExpr::Leaf::printAsSigned | ( | std::ostream & | , |
| Formatter & | , | ||
| bool | asSigned = true |
||
| ) | const |
Prints an integer constant interpreted as a signed value.
Referenced by printAsUnsigned().
|
inline |
Prints an integer constant interpreted as an unsigned value.
Definition at line 1355 of file SymbolicExpr.h.
References printAsSigned().
The documentation for this class was generated from the following file:
