ROSE  0.9.10.196
Public Member Functions | Static Public Member Functions | List of all members
Rose::BinaryAnalysis::SymbolicExpr::Leaf Class Reference

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 843 of file BinarySymbolicExpr.h.

#include <BinarySymbolicExpr.h>

Inheritance diagram for Rose::BinaryAnalysis::SymbolicExpr::Leaf:
Inheritance graph
[legend]
Collaboration diagram for Rose::BinaryAnalysis::SymbolicExpr::Leaf:
Collaboration graph
[legend]

Public Member Functions

virtual bool isNumber () ROSE_OVERRIDE
 Returns true if the expression is a known numeric value. More...
 
virtual uint64_t toInt () ROSE_OVERRIDE
 Property: integer value of expression node. More...
 
virtual bool mustEqual (const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
 Returns true if two expressions must be equal (cannot be unequal). More...
 
virtual bool mayEqual (const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
 Returns true if two expressions might be equal, but not necessarily be equal. More...
 
virtual bool isEquivalentTo (const Ptr &other) ROSE_OVERRIDE
 Tests two expressions for structural equivalence. More...
 
virtual int compareStructure (const Ptr &other) ROSE_OVERRIDE
 Compare two expressions structurally for sorting. More...
 
virtual Ptr substitute (const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr()) ROSE_OVERRIDE
 Substitute one value for another. More...
 
virtual VisitAction depthFirstTraversal (Visitor &) ROSE_OVERRIDE
 Traverse the expression. More...
 
virtual uint64_t nNodes () ROSE_OVERRIDE
 Computes the size of an expression by counting the number of nodes. More...
 
const Sawyer::Container::BitVectorbits ()
 Property: Bits stored for numeric values. More...
 
virtual bool isVariable ()
 Is the node a bitvector variable?
 
virtual bool isMemory ()
 Does the node represent memory?
 
uint64_t nameId ()
 Returns the name ID of a free variable. More...
 
std::string toString ()
 Returns a string for the leaf. More...
 
virtual void print (std::ostream &, Formatter &) ROSE_OVERRIDE
 Print the expression to a stream. More...
 
void printAsSigned (std::ostream &, Formatter &, bool asSigned=true)
 Prints an integer interpreted as a signed value. More...
 
void printAsUnsigned (std::ostream &o, Formatter &f)
 Prints an integer interpreted as an unsigned value. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::SymbolicExpr::Node
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...
 
size_t nBits ()
 Property: Number of significant bits. More...
 
unsigned flags ()
 Property: User-defined bit flags. More...
 
Ptr newFlags (unsigned flags)
 Sets flags. More...
 
size_t domainWidth ()
 Property: Width for memory expressions. More...
 
bool isScalar ()
 Check whether expression is scalar. More...
 
uint64_t nNodesUnique ()
 Number of unique nodes in expression. More...
 
std::set< LeafPtrgetVariables ()
 Returns the variables appearing in the expression. More...
 
InteriorPtr isInteriorNode ()
 Dynamic cast of this object to an interior node. More...
 
LeafPtr isLeafNode ()
 Dynamic cast of this object to a leaf node. More...
 
bool isHashed ()
 Returns true if this node has a hash value computed and cached. More...
 
Hash hash ()
 Returns (and caches) the hash value for this node. More...
 
void hash (Hash)
 
void assertAcyclic ()
 Asserts that expressions are acyclic. More...
 
std::vector< PtrfindCommonSubexpressions ()
 Find common subexpressions. More...
 
bool matchAddVariableConstant (LeafPtr &variable, LeafPtr &constant)
 Determine whether an expression is a variable plus a constant. More...
 
InteriorPtr isOperator (Operator)
 True (non-null) if this node is the specified operator. More...
 
const std::string & comment ()
 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 ()
 Property: User-defined data. 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)
 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...
 
SharedObjectoperator= (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...
 
Storageoperator= (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...
 
getAttribute (Id id) const
 Get an attribute that is known to exist. More...
 
attributeOrElse (Id id, const T &dflt) const
 Return an attribute or a specified value. More...
 
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< IdattributeIds () const
 Returns ID numbers for all IDs stored in this container. More...
 

Static Public Member Functions

static LeafPtr createVariable (size_t nbits, const std::string &comment="", unsigned flags=0)
 Construct a new free variable with a specified number of significant bits. More...
 
static LeafPtr createExistingVariable (size_t nbits, uint64_t id, const std::string &comment="", unsigned flags=0)
 Construct another reference to an existing variable. More...
 
static LeafPtr createInteger (size_t nbits, uint64_t n, const std::string &comment="", unsigned flags=0)
 Construct a new integer with the specified number of significant bits. More...
 
static LeafPtr createConstant (const Sawyer::Container::BitVector &bits, const std::string &comment="", unsigned flags=0)
 Construct a new known value with the specified bits. More...
 
static LeafPtr createBoolean (bool b, const std::string &comment="", unsigned flags=0)
 Create a new Boolean, a single-bit integer. More...
 
static LeafPtr createMemory (size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0)
 Construct a new memory state. More...
 
static LeafPtr createExistingMemory (size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0)
 Construct another reference to an existing variable. More...
 
- Static Public Member Functions inherited from Sawyer::SmallObject
static SynchronizedPoolAllocatorpoolAllocator ()
 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 Sawyer::Attribute::Storage<>
typedef SynchronizationTraits< Sawyer::SingleThreadedTagSync
 
- 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)
 
- Protected Attributes inherited from Rose::BinaryAnalysis::SymbolicExpr::Node
size_t nBits_
 Number of significant bits. More...
 
size_t domainWidth_
 Width of domain for unary functions. More...
 
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 LeafPtr Rose::BinaryAnalysis::SymbolicExpr::Leaf::createVariable ( size_t  nbits,
const std::string &  comment = "",
unsigned  flags = 0 
)
static

Construct a new free variable with a specified number of significant bits.

static LeafPtr Rose::BinaryAnalysis::SymbolicExpr::Leaf::createExistingVariable ( size_t  nbits,
uint64_t  id,
const std::string &  comment = "",
unsigned  flags = 0 
)
static

Construct another reference to an existing variable.

This method is used internally by the expression parsing mechanism to produce a new instance of some previously existing variable – both instances are the same variable and therefore should be given the same size (although this consistency cannot be checked automatically).

static LeafPtr Rose::BinaryAnalysis::SymbolicExpr::Leaf::createInteger ( size_t  nbits,
uint64_t  n,
const std::string &  comment = "",
unsigned  flags = 0 
)
static

Construct a new integer with the specified number of significant bits.

Any high-order bits beyond the specified size will be zeroed.

static LeafPtr Rose::BinaryAnalysis::SymbolicExpr::Leaf::createConstant ( const Sawyer::Container::BitVector bits,
const std::string &  comment = "",
unsigned  flags = 0 
)
static

Construct a new known value with the specified bits.

static LeafPtr Rose::BinaryAnalysis::SymbolicExpr::Leaf::createBoolean ( bool  b,
const std::string &  comment = "",
unsigned  flags = 0 
)
inlinestatic

Create a new Boolean, a single-bit integer.

Definition at line 898 of file BinarySymbolicExpr.h.

References Rose::BinaryAnalysis::SymbolicExpr::Node::flags().

static LeafPtr Rose::BinaryAnalysis::SymbolicExpr::Leaf::createMemory ( size_t  addressWidth,
size_t  valueWidth,
const std::string &  comment = "",
unsigned  flags = 0 
)
static

Construct a new memory state.

A memory state is a function that maps addresses to values.

static LeafPtr Rose::BinaryAnalysis::SymbolicExpr::Leaf::createExistingMemory ( size_t  addressWidth,
size_t  valueWidth,
uint64_t  id,
const std::string &  comment = "",
unsigned  flags = 0 
)
static

Construct another reference to an existing variable.

This method is used internally by the expression parsing mechanism to produce a new instance of some previously existing memory state. Both instances are the same state and therefore should be given the same domain and range size (although this consistency cannot be checked automatically.)

virtual bool Rose::BinaryAnalysis::SymbolicExpr::Leaf::isNumber ( )
virtual

Returns true if the expression is a known numeric value.

The value itself is stored in the number property.

Implements Rose::BinaryAnalysis::SymbolicExpr::Node.

virtual uint64_t Rose::BinaryAnalysis::SymbolicExpr::Leaf::toInt ( )
virtual

Property: integer value of expression node.

Returns the integer value of a node for which isKnown returns true. The high-order bits, those beyond the number of significant bits returned by the nBits propert, are guaranteed to be zero.

Implements Rose::BinaryAnalysis::SymbolicExpr::Node.

virtual bool Rose::BinaryAnalysis::SymbolicExpr::Leaf::mustEqual ( const Ptr other,
const SmtSolverPtr solver = SmtSolverPtr() 
)
virtual

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.

virtual bool Rose::BinaryAnalysis::SymbolicExpr::Leaf::mayEqual ( const Ptr other,
const SmtSolverPtr solver = SmtSolverPtr() 
)
virtual

Returns true if two expressions might be equal, but not necessarily be equal.

Implements Rose::BinaryAnalysis::SymbolicExpr::Node.

virtual bool Rose::BinaryAnalysis::SymbolicExpr::Leaf::isEquivalentTo ( const Ptr other)
virtual

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.

virtual int Rose::BinaryAnalysis::SymbolicExpr::Leaf::compareStructure ( const Ptr other)
virtual

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.

virtual Ptr Rose::BinaryAnalysis::SymbolicExpr::Leaf::substitute ( const Ptr from,
const Ptr to,
const SmtSolverPtr solver = SmtSolverPtr() 
)
virtual

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.

virtual VisitAction Rose::BinaryAnalysis::SymbolicExpr::Leaf::depthFirstTraversal ( Visitor )
virtual

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.

virtual uint64_t Rose::BinaryAnalysis::SymbolicExpr::Leaf::nNodes ( )
inlinevirtual

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:

SymbolicExpr expr = Leaf::createVariable(32);
for(size_t i=0; i<64; ++i)
expr = Interior::create(32, OP_ADD, expr, expr)

When an overflow occurs the result is meaningless.

See also
nNodesUnique

Implements Rose::BinaryAnalysis::SymbolicExpr::Node.

Definition at line 920 of file BinarySymbolicExpr.h.

const Sawyer::Container::BitVector& Rose::BinaryAnalysis::SymbolicExpr::Leaf::bits ( )

Property: Bits stored for numeric values.

uint64_t Rose::BinaryAnalysis::SymbolicExpr::Leaf::nameId ( )

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 isNumber returns false.

std::string Rose::BinaryAnalysis::SymbolicExpr::Leaf::toString ( )

Returns a string for the leaf.

Variables are returned as "vN", memory is returned as "mN", and constants are returned as a hexadecimal string, where N is a variable or memory number.

virtual void Rose::BinaryAnalysis::SymbolicExpr::Leaf::print ( std::ostream &  ,
Formatter  
)
virtual

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.

void Rose::BinaryAnalysis::SymbolicExpr::Leaf::printAsSigned ( std::ostream &  ,
Formatter ,
bool  asSigned = true 
)

Prints an integer interpreted as a signed value.

void Rose::BinaryAnalysis::SymbolicExpr::Leaf::printAsUnsigned ( std::ostream &  o,
Formatter f 
)
inline

Prints an integer interpreted as an unsigned value.

Definition at line 950 of file BinarySymbolicExpr.h.


The documentation for this class was generated from the following file: