ROSE  0.9.10.91
Classes | Public Member Functions | Static Public Attributes | Protected Member Functions | Protected Attributes | List of all members
Rose::BinaryAnalysis::SymbolicExpr::Node Class Referenceabstract

Description

Base class for symbolic expression nodes.

Every node has a specified width measured in bits that is constant over the life of the node. The width is always a concrete, positive value stored in a 64-bit field. The corollary of this invariant is that if an expression's result width depends on the values of some of its arguments, those arguments must be concrete and not wider than 64 bits. Only a few operators fall into this category since most expressions depend on the widths of their arguments rather than the values of their arguments.

In order that subtrees can be freely assigned as children of other nodes (provided the structure as a whole remains a lattice and not a graph with cycles), two things are required: First, tree nodes are always referenced through shared-ownership pointers that collectively own the expression node (expressions are never explicitly deleted). Second, expression nodes are immutable once they're instantiated. There are a handful of exceptions to the immutable rule: comments and attributes are allowed to change since they're not significant to hashing or arithmetic operations.

Each node has a bit flags property, the bits of which are defined by the user. New nodes are created having all bits cleared unless the user specifies a value in the constructor. Bits are significant for hashing. Simplifiers produce result expressions whose bits are set in a predictable manner with the following rules:

Definition at line 215 of file BinarySymbolicExpr.h.

#include <BinarySymbolicExpr.h>

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

Classes

class  WithFormatter
 A node with formatter. More...
 

Public Member Functions

virtual bool mustEqual (const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr())=0
 Returns true if two expressions must be equal (cannot be unequal). More...
 
virtual bool mayEqual (const Ptr &other, const SmtSolverPtr &solver=SmtSolverPtr())=0
 Returns true if two expressions might be equal, but not necessarily be equal. More...
 
virtual bool isEquivalentTo (const Ptr &other)=0
 Tests two expressions for structural equivalence. More...
 
virtual int compareStructure (const Ptr &other)=0
 Compare two expressions structurally for sorting. More...
 
virtual Ptr substitute (const Ptr &from, const Ptr &to, const SmtSolverPtr &solver=SmtSolverPtr())=0
 Substitute one value for another. 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...
 
virtual bool isNumber ()=0
 Returns true if the expression is a known numeric value. More...
 
bool is_known () ROSE_DEPRECATED("use isNumber instead")
 
virtual uint64_t toInt ()=0
 Property: integer value of expression node. More...
 
uint64_t get_value () ROSE_DEPRECATED("use toInt instead")
 
const std::string & get_comment () ROSE_DEPRECATED("use 'comment' property instead")
 
void set_comment (const std::string &s) ROSE_DEPRECATED("use 'comment' property instead")
 
size_t nBits ()
 Property: Number of significant bits. More...
 
size_t get_nbits () ROSE_DEPRECATED("use 'nBits' property instead")
 
unsigned flags ()
 Property: User-defined bit flags. More...
 
unsigned get_flags () ROSE_DEPRECATED("use 'flags' property instead")
 
Ptr newFlags (unsigned flags)
 Sets flags. More...
 
size_t domainWidth ()
 Property: Width for memory expressions. More...
 
bool isScalar ()
 Check whether expression is scalar. More...
 
virtual VisitAction depthFirstTraversal (Visitor &)=0
 Traverse the expression. More...
 
VisitAction depth_first_traversal (Visitor &v) ROSE_DEPRECATED("use depthFirstTraversal instead")
 
virtual uint64_t nNodes ()=0
 Computes the size of an expression by counting the number of nodes. More...
 
uint64_t nnodes () ROSE_DEPRECATED("use nNodes() instead")
 
uint64_t nNodesUnique ()
 Number of unique nodes in expression. More...
 
uint64_t nnodesUnique () ROSE_DEPRECATED("use nNodesUnique instead")
 
std::set< LeafPtrgetVariables ()
 Returns the variables appearing in the expression. More...
 
std::set< LeafPtrget_variables () ROSE_DEPRECATED("use getVariables instead")
 
InteriorPtr isInteriorNode ()
 Dynamic cast of this object to an interior node. More...
 
InteriorPtr isInternalNode () ROSE_DEPRECATED("use isInteriorNode instead")
 
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...
 
bool is_hashed () ROSE_DEPRECATED("use isHashed instead")
 
Hash hash ()
 Returns (and caches) the hash value for this node. More...
 
void hash (Hash)
 
WithFormatter with_format (Formatter &fmt) ROSE_DEPRECATED("use withFormat instead")
 
void assertAcyclic ()
 Asserts that expressions are acyclic. More...
 
void assert_acyclic ()
 
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...
 
virtual void print (std::ostream &, Formatter &)=0
 Print the expression to a stream. 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 Attributes

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

 Node (const std::string &comment, unsigned flags=0)
 
void printFlags (std::ostream &o, unsigned flags, char &bracket)
 

Protected Attributes

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...
 

Additional Inherited Members

- Public Types inherited from Sawyer::Attribute::Storage<>
typedef SynchronizationTraits< Sawyer::SingleThreadedTagSync
 
- 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)
 

Member Function Documentation

virtual bool Rose::BinaryAnalysis::SymbolicExpr::Node::mustEqual ( const Ptr other,
const SmtSolverPtr solver = SmtSolverPtr() 
)
pure 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).

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

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

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

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

virtual bool Rose::BinaryAnalysis::SymbolicExpr::Node::isEquivalentTo ( const Ptr other)
pure 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.

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

virtual int Rose::BinaryAnalysis::SymbolicExpr::Node::compareStructure ( const Ptr other)
pure 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.

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

virtual Ptr Rose::BinaryAnalysis::SymbolicExpr::Node::substitute ( const Ptr from,
const Ptr to,
const SmtSolverPtr solver = SmtSolverPtr() 
)
pure 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.

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

Ptr Rose::BinaryAnalysis::SymbolicExpr::Node::substituteMultiple ( const ExprExprHashMap substitutions,
const SmtSolverPtr solver = SmtSolverPtr() 
)

Rewrite expression by substituting subexpressions.

This expression is rewritten by doing a depth-first traversal. At each step of the traversal, the subexpression is looked up by hash in the supplied substitutions table. If found, a new expression is created using the value found in the table and the traversal does not descend into the new expression. If no substitutions were performed then this expression is returned, otherwise a new expression is returned. An optional solver, which may be null, is used during the simplification step.

Ptr Rose::BinaryAnalysis::SymbolicExpr::Node::renameVariables ( ExprExprHashMap index,
size_t &  nextVariableId,
const SmtSolverPtr solver = SmtSolverPtr() 
)

Rewrite using lowest numbered variable names.

Given an expression, use the specified index to rewrite variables. The index uses expression hashes to look up the replacement expression. If the traversal finds a variable which is not in the index then a new variable is created. The new variable has the same type as the original variable, but it's name is generated starting at nextVariableId and incrementing after each replacement is generated. The optional solver is used during the simplification process and may be null.

virtual bool Rose::BinaryAnalysis::SymbolicExpr::Node::isNumber ( )
pure virtual

Returns true if the expression is a known numeric value.

The value itself is stored in the number property.

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

virtual uint64_t Rose::BinaryAnalysis::SymbolicExpr::Node::toInt ( )
pure 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.

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

const std::string& Rose::BinaryAnalysis::SymbolicExpr::Node::comment ( )
inline

Property: Comment.

Comments can be changed after a node has been created since the comment is not intended to be used for anything but annotation and/or debugging. If many expressions are sharing the same node, then the comment is changed in all those expressions. Changing the comment property is allowed even though nodes are generally immutable because comments are not considered significant for comparisons, computing hash values, etc.

Definition at line 356 of file BinarySymbolicExpr.h.

References comment_.

Referenced by Rose::BinaryAnalysis::SymbolicExpr::Interior::create().

void Rose::BinaryAnalysis::SymbolicExpr::Node::comment ( const std::string &  s)
inline

Property: Comment.

Comments can be changed after a node has been created since the comment is not intended to be used for anything but annotation and/or debugging. If many expressions are sharing the same node, then the comment is changed in all those expressions. Changing the comment property is allowed even though nodes are generally immutable because comments are not considered significant for comparisons, computing hash values, etc.

Definition at line 357 of file BinarySymbolicExpr.h.

void Rose::BinaryAnalysis::SymbolicExpr::Node::userData ( boost::any &  data)
inline

Property: User-defined data.

User defined data is always optional and does not contribute to the hash value of an expression. The user-defined data can be changed at any time by the user even if the expression node to which it is attached is shared between many expressions.

Definition at line 377 of file BinarySymbolicExpr.h.

const boost::any& Rose::BinaryAnalysis::SymbolicExpr::Node::userData ( )
inline

Property: User-defined data.

User defined data is always optional and does not contribute to the hash value of an expression. The user-defined data can be changed at any time by the user even if the expression node to which it is attached is shared between many expressions.

Definition at line 380 of file BinarySymbolicExpr.h.

References userData_.

size_t Rose::BinaryAnalysis::SymbolicExpr::Node::nBits ( )
inline

Property: Number of significant bits.

An expression with a known value is guaranteed to have all higher-order bits cleared.

Definition at line 388 of file BinarySymbolicExpr.h.

References nBits_.

unsigned Rose::BinaryAnalysis::SymbolicExpr::Node::flags ( )
inline

Property: User-defined bit flags.

This property is significant for hashing, comparisons, and possibly other operations, therefore it is immutable. To change the flags one must create a new expression; see newFlags.

Definition at line 399 of file BinarySymbolicExpr.h.

References flags_.

Referenced by Rose::BinaryAnalysis::SymbolicExpr::Interior::create(), and Rose::BinaryAnalysis::SymbolicExpr::Leaf::createBoolean().

Ptr Rose::BinaryAnalysis::SymbolicExpr::Node::newFlags ( unsigned  flags)

Sets flags.

Since symbolic expressions are immutable it is not possible to change the flags directly. Therefore if the desired flags are different than the current flags a new expression is created that is the same in every other respect. If the flags are not changed then the original expression is returned.

size_t Rose::BinaryAnalysis::SymbolicExpr::Node::domainWidth ( )
inline

Property: Width for memory expressions.

The return value is non-zero if and only if this tree node is a memory expression.

Definition at line 413 of file BinarySymbolicExpr.h.

References domainWidth_.

bool Rose::BinaryAnalysis::SymbolicExpr::Node::isScalar ( )
inline

Check whether expression is scalar.

Everything is scalar except for memory.

Definition at line 418 of file BinarySymbolicExpr.h.

References domainWidth_.

virtual VisitAction Rose::BinaryAnalysis::SymbolicExpr::Node::depthFirstTraversal ( Visitor )
pure 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.

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

virtual uint64_t Rose::BinaryAnalysis::SymbolicExpr::Node::nNodes ( )
pure virtual

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

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

uint64_t Rose::BinaryAnalysis::SymbolicExpr::Node::nNodesUnique ( )

Number of unique nodes in expression.

std::set<LeafPtr> Rose::BinaryAnalysis::SymbolicExpr::Node::getVariables ( )

Returns the variables appearing in the expression.

InteriorPtr Rose::BinaryAnalysis::SymbolicExpr::Node::isInteriorNode ( )
inline

Dynamic cast of this object to an interior node.

Returns null if the cast is not valid.

Definition at line 472 of file BinarySymbolicExpr.h.

References Sawyer::SharedPointer< T >::dynamicCast(), and Sawyer::SharedFromThis< Node >::sharedFromThis().

Referenced by Rose::BinaryAnalysis::SymbolicExpr::substitute().

LeafPtr Rose::BinaryAnalysis::SymbolicExpr::Node::isLeafNode ( )
inline

Dynamic cast of this object to a leaf node.

Returns null if the cast is not valid.

Definition at line 484 of file BinarySymbolicExpr.h.

References Sawyer::SharedPointer< T >::dynamicCast(), and Sawyer::SharedFromThis< Node >::sharedFromThis().

bool Rose::BinaryAnalysis::SymbolicExpr::Node::isHashed ( )
inline

Returns true if this node has a hash value computed and cached.

The hash value zero is reserved to indicate that no hash has been computed; if a node happens to actually hash to zero, it will not be cached and will be recomputed for every call to hash().

Definition at line 491 of file BinarySymbolicExpr.h.

Hash Rose::BinaryAnalysis::SymbolicExpr::Node::hash ( )

Returns (and caches) the hash value for this node.

If a hash value is not cached in this node, then a new hash value is computed and cached.

WithFormatter Rose::BinaryAnalysis::SymbolicExpr::Node::withFormat ( Formatter fmt)
inline

Combines a node with a formatter for printing.

This is used for convenient printing with the "<<" operator. For instance:

fmt.show_comments = Formatter::CMT_AFTER; //show comments after the variable
Ptr expression = ...;
std::cout <<"method 1: "; expression->print(std::cout, fmt); std::cout <<"\n";
std::cout <<"method 2: " <<expression->withFormat(fmt) <<"\n";
std::cout <<"method 3: " <<*expression+fmt <<"\n";

Definition at line 528 of file BinarySymbolicExpr.h.

References Sawyer::SharedFromThis< Node >::sharedFromThis().

Referenced by operator+().

WithFormatter Rose::BinaryAnalysis::SymbolicExpr::Node::operator+ ( Formatter fmt)
inline

Combines a node with a formatter for printing.

This is used for convenient printing with the "<<" operator. For instance:

fmt.show_comments = Formatter::CMT_AFTER; //show comments after the variable
Ptr expression = ...;
std::cout <<"method 1: "; expression->print(std::cout, fmt); std::cout <<"\n";
std::cout <<"method 2: " <<expression->withFormat(fmt) <<"\n";
std::cout <<"method 3: " <<*expression+fmt <<"\n";

Definition at line 529 of file BinarySymbolicExpr.h.

References withFormat().

virtual void Rose::BinaryAnalysis::SymbolicExpr::Node::print ( std::ostream &  ,
Formatter  
)
pure 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.

Implemented in Rose::BinaryAnalysis::SymbolicExpr::Leaf, and Rose::BinaryAnalysis::SymbolicExpr::Interior.

void Rose::BinaryAnalysis::SymbolicExpr::Node::print ( std::ostream &  o)
inline

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.

Definition at line 542 of file BinarySymbolicExpr.h.

References print().

Referenced by print().

void Rose::BinaryAnalysis::SymbolicExpr::Node::assertAcyclic ( )

Asserts that expressions are acyclic.

This is intended only for debugging.

std::vector<Ptr> Rose::BinaryAnalysis::SymbolicExpr::Node::findCommonSubexpressions ( )

Find common subexpressions.

Returns a vector of the largest common subexpressions. The list is computed by performing a depth-first search on this expression and adding expressions to the return vector whenever a subtree is encountered a second time. Therefore the if a common subexpression A contains another common subexpression B then B will appear earlier in the list than A.

bool Rose::BinaryAnalysis::SymbolicExpr::Node::matchAddVariableConstant ( LeafPtr variable,
LeafPtr constant 
)

Determine whether an expression is a variable plus a constant.

If this expression is of the form V + X or X + V where V is a variable and X is a constant, return true and make variable point to the variable and constant point to the constant. If the expression is not one of these forms, then return false without modifying the arguments.

InteriorPtr Rose::BinaryAnalysis::SymbolicExpr::Node::isOperator ( Operator  )

True (non-null) if this node is the specified operator.

Member Data Documentation

size_t Rose::BinaryAnalysis::SymbolicExpr::Node::nBits_
protected

Number of significant bits.

Constant over the life of the node.

Definition at line 221 of file BinarySymbolicExpr.h.

Referenced by nBits().

size_t Rose::BinaryAnalysis::SymbolicExpr::Node::domainWidth_
protected

Width of domain for unary functions.

E.g., memory.

Definition at line 222 of file BinarySymbolicExpr.h.

Referenced by domainWidth(), and isScalar().

unsigned Rose::BinaryAnalysis::SymbolicExpr::Node::flags_
protected

Bit flags.

Meaning of flags is up to the user. Low-order 16 bits are reserved.

Definition at line 223 of file BinarySymbolicExpr.h.

Referenced by flags().

std::string Rose::BinaryAnalysis::SymbolicExpr::Node::comment_
protected

Optional comment.

Only for debugging; not significant for any calculation.

Definition at line 224 of file BinarySymbolicExpr.h.

Referenced by comment().

Hash Rose::BinaryAnalysis::SymbolicExpr::Node::hashval_
protected

Optional hash used as a quick way to indicate that two expressions are different.

Definition at line 225 of file BinarySymbolicExpr.h.

boost::any Rose::BinaryAnalysis::SymbolicExpr::Node::userData_
protected

Additional user-specified data.

This is not part of the hash.

Definition at line 226 of file BinarySymbolicExpr.h.

Referenced by userData().

const unsigned Rose::BinaryAnalysis::SymbolicExpr::Node::RESERVED_FLAGS = 0x0000ffff
static

These flags are reserved for use within ROSE.

Definition at line 247 of file BinarySymbolicExpr.h.

const unsigned Rose::BinaryAnalysis::SymbolicExpr::Node::INDETERMINATE = 0x00000001
static

Value is somehow indeterminate.

E.g., read from writable memory.

Definition at line 250 of file BinarySymbolicExpr.h.

const unsigned Rose::BinaryAnalysis::SymbolicExpr::Node::UNSPECIFIED = 0x00000002
static

Value is somehow unspecified.

A value that is intantiated as part of processing a machine instruction where the ISA documentation is incomplete or says that some result is unspecified or undefined. Intel documentation for the x86 shift and rotate instructions, for example, states that certain status bits have "undefined" values after the instruction executes.

Definition at line 256 of file BinarySymbolicExpr.h.

Referenced by Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue::instance_unspecified().

const unsigned Rose::BinaryAnalysis::SymbolicExpr::Node::BOTTOM = 0x00000004
static

Value represents bottom in dataflow analysis.

If this flag is used by ROSE's dataflow engine to represent a bottom value in a lattice.

Definition at line 260 of file BinarySymbolicExpr.h.

Referenced by Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue::instance_bottom().

boost::logic::tribool(* Rose::BinaryAnalysis::SymbolicExpr::Node::mayEqualCallback) (const Ptr &a, const Ptr &b, const SmtSolverPtr &)
static

User-supplied predicate to augment alias checking.

If this pointer is non-null, then the mayEqual methods invoke this function. If this function returns true or false, then its return value becomes the return value of mayEqual, otherwise mayEqual continues as it normally would. This user-defined function is invoked by mayEqual after trivial situations are checked and before any calls to an SMT solver. The SMT solver argument is optional (may be null).

Definition at line 275 of file BinarySymbolicExpr.h.


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