ROSE 0.11.145.192
|
Namespace supplying types and functions for symbolic expressions.
These are used by certain instruction semantics policies and satisfiability modulo theory (SMT) solvers. These expressions are tailored to bit-vector and integer difference logics, whereas the expression nodes in other parts of ROSE have different goals.
Namespaces | |
namespace | TypeStyle |
Whether to use abbreviated or full output. | |
Classes | |
struct | AddSimplifier |
struct | AndSimplifier |
struct | AsrSimplifier |
struct | ConcatSimplifier |
struct | ConvertSimplifier |
struct | EqSimplifier |
class | Exception |
Exceptions for symbolic expressions. More... | |
class | ExpressionLessp |
Compare two expressions for STL containers. More... | |
class | ExprExprHashMap |
Mapping from expression to expression. More... | |
struct | ExprExprHashMapCompare |
struct | ExprExprHashMapHasher |
struct | ExtractSimplifier |
class | Formatter |
Controls formatting of expression trees when printing. More... | |
class | Interior |
Interior node of an expression tree for instruction semantics. More... | |
struct | InvertSimplifier |
struct | IteSimplifier |
class | Leaf |
Leaf node of an expression tree for instruction semantics. More... | |
struct | LssbSimplifier |
struct | MssbSimplifier |
struct | NegateSimplifier |
class | Node |
Base class for symbolic expression nodes. More... | |
struct | NoopSimplifier |
struct | OrSimplifier |
struct | ReinterpretSimplifier |
struct | RolSimplifier |
struct | RorSimplifier |
struct | SdivSimplifier |
struct | SetSimplifier |
struct | SextendSimplifier |
struct | SgeSimplifier |
struct | SgtSimplifier |
struct | ShiftSimplifier |
struct | ShlSimplifier |
struct | ShrSimplifier |
class | Simplifier |
Operator-specific simplification methods. More... | |
struct | SleSimplifier |
struct | SltSimplifier |
struct | SmodSimplifier |
struct | SmulSimplifier |
class | Type |
Type of symbolic expression. More... | |
struct | UdivSimplifier |
struct | UextendSimplifier |
struct | UgeSimplifier |
struct | UgtSimplifier |
struct | UleSimplifier |
struct | UltSimplifier |
struct | UmodSimplifier |
struct | UmulSimplifier |
class | Visitor |
Base class for visiting nodes during expression traversal. More... | |
struct | XorSimplifier |
struct | ZeropSimplifier |
Typedefs | |
using | InteriorPtr = Sawyer::SharedPointer< Interior > |
Reference counting pointer. | |
using | LeafPtr = Sawyer::SharedPointer< Leaf > |
Reference counting pointer. | |
using | Ptr = Sawyer::SharedPointer< Node > |
Reference counting pointer. | |
using | Nodes = std::vector< Ptr > |
using | RenameMap = Map< uint64_t, uint64_t > |
using | Hash = uint64_t |
Hash of symbolic expression. | |
typedef Sawyer::Container::Set< Ptr, ExpressionLessp > | ExpressionSet |
Set of expressions ordered by hash. | |
Enumerations | |
enum | Operator { OP_ADD , OP_AND , OP_ASR , OP_CONCAT , OP_EQ , OP_EXTRACT , OP_INVERT , OP_ITE , OP_LET , OP_LSSB , OP_MSSB , OP_NE , OP_NEGATE , OP_NOOP , OP_OR , OP_READ , OP_ROL , OP_ROR , OP_SDIV , OP_SET , OP_SEXTEND , OP_SGE , OP_SGT , OP_SHL0 , OP_SHL1 , OP_SHR0 , OP_SHR1 , OP_SLE , OP_SLT , OP_SMOD , OP_SMUL , OP_UDIV , OP_UEXTEND , OP_UGE , OP_UGT , OP_ULE , OP_ULT , OP_UMOD , OP_UMUL , OP_WRITE , OP_XOR , OP_ZEROP , OP_FP_ABS , OP_FP_NEGATE , OP_FP_ADD , OP_FP_MUL , OP_FP_DIV , OP_FP_MULADD , OP_FP_SQRT , OP_FP_MOD , OP_FP_ROUND , OP_FP_MIN , OP_FP_MAX , OP_FP_LE , OP_FP_LT , OP_FP_GE , OP_FP_GT , OP_FP_EQ , OP_FP_ISNORM , OP_FP_ISSUBNORM , OP_FP_ISZERO , OP_FP_ISINFINITE , OP_FP_ISNAN , OP_FP_ISNEG , OP_FP_ISPOS , OP_CONVERT , OP_REINTERPRET , OP_NONE } |
Operators for interior nodes of the expression tree. More... | |
enum | VisitAction { CONTINUE , TRUNCATE , TERMINATE } |
Return type for visitors. More... | |
Functions | |
std::string | toStr (Operator) |
std::ostream & | operator<< (std::ostream &o, const Node &) |
std::ostream & | operator<< (std::ostream &o, const Node::WithFormatter &) |
Ptr | setToIte (const Ptr &, const SmtSolverPtr &solver=SmtSolverPtr(), const LeafPtr &var=LeafPtr()) |
Convert a set to an ite expression. | |
Hash | hash (const std::vector< Ptr > &) |
Hash zero or more expressions. | |
template<typename InputIterator > | |
uint64_t | nNodes (InputIterator begin, InputIterator end) |
Counts the number of nodes. | |
template<typename InputIterator > | |
uint64_t | nNodesUnique (InputIterator begin, InputIterator end) |
Counts the number of unique nodes. | |
template<class Substitution > | |
Ptr | substitute (const Ptr &src, Substitution &subber, const SmtSolverPtr &solver=SmtSolverPtr()) |
On-the-fly substitutions. | |
LeafPtr | makeVariable (const Type &, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeVariable (const Type &, uint64_t id, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeConstant (const Type &, const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeIntegerVariable (size_t nBits, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeIntegerVariable (size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeIntegerConstant (size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeIntegerConstant (const Sawyer::Container::BitVector &, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeBooleanConstant (bool, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeMemoryVariable (size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeMemoryVariable (size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeFloatingPointVariable (size_t eb, size_t sb, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeFloatingPointVariable (size_t eb, size_t sb, uint64_t id, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeFloatingPointConstant (float, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeFloatingPointConstant (double, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
LeafPtr | makeFloatingPointNan (size_t eb, size_t sb, const std::string &comment="", unsigned flags=0) |
Leaf constructor. | |
Ptr | makeAdd (const Ptr &a, const Ptr &b, 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. | |
Ptr | makeAnd (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeOr (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeXor (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeConcat (const Ptr &hi, const Ptr &lo, 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 | makeEq (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
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. | |
Ptr | makeInvert (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeIsInfinite (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeIsNan (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeIsNeg (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeIsNorm (const Ptr &a, 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. | |
Ptr | makeIsSubnorm (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
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 | makeLet (const Ptr &a, const Ptr &b, const Ptr &c, 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. | |
Ptr | makeMax (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeMin (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeMssb (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
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 | makeNe (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. | |
Ptr | makeRead (const Ptr &mem, const Ptr &addr, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeReinterpret (const Ptr &a, const Type &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeRol (const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeRor (const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeRound (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSet (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSet (const Ptr &a, const Ptr &b, const Ptr &c, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignedDiv (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignExtend (const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignedGe (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignedGt (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeShl0 (const Ptr &sa, const Ptr &a, 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. | |
Ptr | makeShr0 (const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeShr1 (const Ptr &sa, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeIsSignedPos (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignedLe (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignedLt (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignedMax (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignedMin (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignedMod (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSignedMul (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeSqrt (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeDiv (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeExtend (const Ptr &newSize, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeGe (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeGt (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeLe (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeLt (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. | |
Ptr | makeMul (const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeWrite (const Ptr &mem, const Ptr &addr, const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
Ptr | makeZerop (const Ptr &a, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0) |
Interior node constructor. | |
std::vector< Ptr > | findCommonSubexpressions (const std::vector< Ptr > &) |
Find common subexpressions. | |
template<typename InputIterator > | |
std::vector< Ptr > | findCommonSubexpressions (InputIterator begin, InputIterator end) |
Find common subexpressions. | |
Variables | |
bool | serializeVariableIds |
Whether to serialize variable IDs. | |
const uint64_t | MAX_NNODES |
Maximum number of nodes that can be reported. | |
using Rose::BinaryAnalysis::SymbolicExpression::InteriorPtr = typedef Sawyer::SharedPointer<Interior> |
Reference counting pointer.
Definition at line 108 of file Rose/BinaryAnalysis/BasicTypes.h.
using Rose::BinaryAnalysis::SymbolicExpression::LeafPtr = typedef Sawyer::SharedPointer<Leaf> |
Reference counting pointer.
Definition at line 110 of file Rose/BinaryAnalysis/BasicTypes.h.
using Rose::BinaryAnalysis::SymbolicExpression::Ptr = typedef Sawyer::SharedPointer<Node> |
Reference counting pointer.
Definition at line 112 of file Rose/BinaryAnalysis/BasicTypes.h.
using Rose::BinaryAnalysis::SymbolicExpression::Nodes = typedef std::vector<Ptr> |
Definition at line 153 of file SymbolicExpression.h.
using Rose::BinaryAnalysis::SymbolicExpression::RenameMap = typedef Map<uint64_t, uint64_t> |
Definition at line 154 of file SymbolicExpression.h.
using Rose::BinaryAnalysis::SymbolicExpression::Hash = typedef uint64_t |
Hash of symbolic expression.
Definition at line 157 of file SymbolicExpression.h.
typedef Sawyer::Container::Set<Ptr, ExpressionLessp> Rose::BinaryAnalysis::SymbolicExpression::ExpressionSet |
Set of expressions ordered by hash.
Definition at line 927 of file SymbolicExpression.h.
Operators for interior nodes of the expression tree.
Commutative operators generally take one or more operands. Operators such as shifting, extending, and truncating have the size operand appearing before the bit vector on which to operate (this makes the output more human-readable since the size operand is often a constant).
Definition at line 77 of file SymbolicExpression.h.
Return type for visitors.
Enumerator | |
---|---|
CONTINUE | Continue the traversal as normal. |
TRUNCATE | For a pre-order depth-first visit, do not descend into children. |
TERMINATE | Terminate the traversal. |
Definition at line 183 of file SymbolicExpression.h.
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeConstant | ( | const Type & | , |
const Sawyer::Container::BitVector & | , | ||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeIntegerVariable | ( | size_t | nBits, |
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeIntegerVariable | ( | size_t | nBits, |
uint64_t | id, | ||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeIntegerConstant | ( | size_t | nBits, |
uint64_t | value, | ||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeIntegerConstant | ( | const Sawyer::Container::BitVector & | , |
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeBooleanConstant | ( | bool | , |
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeMemoryVariable | ( | size_t | addressWidth, |
size_t | valueWidth, | ||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeMemoryVariable | ( | size_t | addressWidth, |
size_t | valueWidth, | ||
uint64_t | id, | ||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeFloatingPointVariable | ( | size_t | eb, |
size_t | sb, | ||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeFloatingPointVariable | ( | size_t | eb, |
size_t | sb, | ||
uint64_t | id, | ||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeFloatingPointConstant | ( | float | , |
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeFloatingPointConstant | ( | double | , |
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
LeafPtr Rose::BinaryAnalysis::SymbolicExpression::makeFloatingPointNan | ( | size_t | eb, |
size_t | sb, | ||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeAdd | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeAsr | ( | const Ptr & | sa, |
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeAnd | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeOr | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeXor | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeConcat | ( | const Ptr & | hi, |
const Ptr & | lo, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeConvert | ( | const Ptr & | a, |
const Type & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeEq | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeExtract | ( | const Ptr & | begin, |
const Ptr & | end, | ||
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeInvert | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeIsInfinite | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeIsNan | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeIsNeg | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeIsNorm | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeIsPos | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeIsSubnorm | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeIte | ( | const Ptr & | cond, |
const Ptr & | a, | ||
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeLet | ( | const Ptr & | a, |
const Ptr & | b, | ||
const Ptr & | c, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeLssb | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeMax | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeMin | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeMssb | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeMultiplyAdd | ( | const Ptr & | a, |
const Ptr & | b, | ||
const Ptr & | c, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeNe | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeNegate | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeRead | ( | const Ptr & | mem, |
const Ptr & | addr, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeReinterpret | ( | const Ptr & | a, |
const Type & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeRol | ( | const Ptr & | sa, |
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeRor | ( | const Ptr & | sa, |
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeRound | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSet | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSet | ( | const Ptr & | a, |
const Ptr & | b, | ||
const Ptr & | c, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignedDiv | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignExtend | ( | const Ptr & | newSize, |
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignedGe | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignedGt | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeShl0 | ( | const Ptr & | sa, |
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeShl1 | ( | const Ptr & | sa, |
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeShr0 | ( | const Ptr & | sa, |
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeShr1 | ( | const Ptr & | sa, |
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeIsSignedPos | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignedLe | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignedLt | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignedMax | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignedMin | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignedMod | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSignedMul | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeSqrt | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeDiv | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeExtend | ( | const Ptr & | newSize, |
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeGe | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeGt | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeLe | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeLt | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeMod | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeMul | ( | const Ptr & | a, |
const Ptr & | b, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeWrite | ( | const Ptr & | mem, |
const Ptr & | addr, | ||
const Ptr & | a, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
Ptr Rose::BinaryAnalysis::SymbolicExpression::makeZerop | ( | const Ptr & | a, |
const SmtSolverPtr & | solver = SmtSolverPtr() , |
||
const std::string & | comment = "" , |
||
unsigned | flags = 0 |
||
) |
uint64_t Rose::BinaryAnalysis::SymbolicExpression::nNodes | ( | InputIterator | begin, |
InputIterator | end | ||
) |
Counts the number of nodes.
Counts the total number of nodes in multiple expressions. The return value is a saturated sum, returning MAX_NNODES if an overflow occurs.
Definition at line 1540 of file SymbolicExpression.h.
References MAX_NNODES.
uint64_t Rose::BinaryAnalysis::SymbolicExpression::nNodesUnique | ( | InputIterator | begin, |
InputIterator | end | ||
) |
Counts the number of unique nodes.
Counts the number of unique nodes across a number of expressions. Nodes shared between two expressions are counted only one time, whereas the Node::nnodes virtual method counts shared nodes multiple times.
Definition at line 1559 of file SymbolicExpression.h.
std::vector< Ptr > Rose::BinaryAnalysis::SymbolicExpression::findCommonSubexpressions | ( | const std::vector< Ptr > & | ) |
Find common subexpressions.
This is similar to Node::findCommonSubexpressions except the analysis is over a collection of expressions rather than a single expression.
std::vector< Ptr > Rose::BinaryAnalysis::SymbolicExpression::findCommonSubexpressions | ( | InputIterator | begin, |
InputIterator | end | ||
) |
Find common subexpressions.
This is similar to Node::findCommonSubexpressions except the analysis is over a collection of expressions rather than a single expression.
Definition at line 1600 of file SymbolicExpression.h.
Ptr Rose::BinaryAnalysis::SymbolicExpression::substitute | ( | const Ptr & | src, |
Substitution & | subber, | ||
const SmtSolverPtr & | solver = SmtSolverPtr() |
||
) |
On-the-fly substitutions.
This function uses a user-defined substitutor to generate values that are substituted into the specified expression. This operates by performing a depth-first search of the specified expression and calling the subber
at each node. The subber
is invoked with two arguments: an expression to be replaced, and an optional SMT solver for simplifications. It should return either the expression unmodified, or a new expression. The return value of the substitute
function as a whole is either the original expression (if no substitutions were performed) or a new expression.
Definition at line 1633 of file SymbolicExpression.h.
References Rose::BinaryAnalysis::SymbolicExpression::Interior::children(), Rose::BinaryAnalysis::SymbolicExpression::Node::comment(), Rose::BinaryAnalysis::SymbolicExpression::Node::flags(), Rose::BinaryAnalysis::SymbolicExpression::Interior::getOperator(), Rose::BinaryAnalysis::SymbolicExpression::Interior::instance(), Rose::BinaryAnalysis::SymbolicExpression::Node::isInteriorNodeRaw(), Rose::BinaryAnalysis::SymbolicExpression::Interior::nChildren(), and substitute().
Referenced by substitute().
|
extern |
Whether to serialize variable IDs.
If set, then all threads will coordinate so that variable IDs are allocated in a monotonic fashion. This should only be set when necessary in order to make test results more deterministic. The default is to clear, which means variable IDs are allocated from some number of pools in order to reduce lock contention.
Thread safety: This property is not thread safe. If reproducible results are desired, it should be set before any analysis begins.
|
extern |