ROSE
0.11.22.0
|
A fully symbolic semantic domain.
This semantic domain can be used to emulate the execution of a single basic block of instructions. It is similar in nature to PartialSymbolicSemantics, but with a different type of semantics value (SValue): instead of values being a constant or variable with offset, values here are expression trees.
If an SMT solver is supplied a to the RiscOperators then that SMT solver will be used to answer various questions such as when two memory addresses can alias one another. When an SMT solver is lacking, the questions will be answered by very naive comparison of the expression trees.
Namespaces | |
AllowSideEffects | |
Boolean for allowing side effects. | |
Classes | |
class | Formatter |
Formatter for symbolic values. More... | |
class | MemoryListState |
Byte-addressable memory. More... | |
class | MemoryMapState |
Byte-addressable memory. More... | |
class | Merger |
Controls merging of symbolic values. More... | |
class | RiscOperators |
Defines RISC operators for the SymbolicSemantics domain. More... | |
class | SValue |
Type of values manipulated by the SymbolicSemantics domain. More... | |
Typedefs | |
typedef SymbolicExpr::Leaf | LeafNode |
typedef SymbolicExpr::LeafPtr | LeafPtr |
typedef SymbolicExpr::Interior | InteriorNode |
typedef SymbolicExpr::InteriorPtr | InteriorPtr |
typedef SymbolicExpr::Node | ExprNode |
typedef SymbolicExpr::Ptr | ExprPtr |
typedef std::set< SgAsmInstruction * > | InsnSet |
typedef Sawyer::SharedPointer< class Merger > | MergerPtr |
Shared-ownership pointer for a merge control object. More... | |
typedef Sawyer::SharedPointer< class SValue > | SValuePtr |
Shared-ownership pointer for symbolic semantic value. More... | |
typedef BaseSemantics::RegisterStateGeneric | RegisterState |
typedef BaseSemantics::RegisterStateGenericPtr | RegisterStatePtr |
typedef boost::shared_ptr< class MemoryListState > | MemoryListStatePtr |
Shared-ownership pointer for symbolic list-based memory state. More... | |
typedef boost::shared_ptr< class MemoryMapState > | MemoryMapStatePtr |
Shared-ownership pointer to symbolic memory state. More... | |
typedef MemoryListState | MemoryState |
typedef MemoryListStatePtr | MemoryStatePtr |
typedef BaseSemantics::State | State |
typedef BaseSemantics::StatePtr | StatePtr |
typedef boost::shared_ptr< class RiscOperators > | RiscOperatorsPtr |
Shared-ownership pointer to symbolic RISC operations. More... | |
Enumerations | |
enum | WritersMode { TRACK_NO_WRITERS, TRACK_LATEST_WRITER, TRACK_ALL_WRITERS } |
How to update the list of writers stored at each abstract location. More... | |
enum | DefinersMode { TRACK_NO_DEFINERS, TRACK_LATEST_DEFINER, TRACK_ALL_DEFINERS } |
How to update the list of definers stored in each semantic value. More... | |
typedef Sawyer::SharedPointer<class Merger> Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MergerPtr |
Shared-ownership pointer for a merge control object.
See Shared ownership.
Definition at line 74 of file SymbolicSemantics2.h.
typedef Sawyer::SharedPointer<class SValue> Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValuePtr |
Shared-ownership pointer for symbolic semantic value.
See Shared ownership.
Definition at line 121 of file SymbolicSemantics2.h.
typedef boost::shared_ptr<class MemoryListState> Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListStatePtr |
Shared-ownership pointer for symbolic list-based memory state.
See Shared ownership.
Definition at line 444 of file SymbolicSemantics2.h.
typedef boost::shared_ptr<class MemoryMapState> Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryMapStatePtr |
Shared-ownership pointer to symbolic memory state.
See Shared ownership.
Definition at line 641 of file SymbolicSemantics2.h.
typedef boost::shared_ptr<class RiscOperators> Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperatorsPtr |
Shared-ownership pointer to symbolic RISC operations.
See Shared ownership.
Definition at line 783 of file SymbolicSemantics2.h.
How to update the list of writers stored at each abstract location.
Enumerator | |
---|---|
TRACK_NO_WRITERS |
Do not track writers. |
TRACK_LATEST_WRITER |
Save only the latest writer. |
TRACK_ALL_WRITERS |
Save all writers. |
Definition at line 769 of file SymbolicSemantics2.h.
How to update the list of definers stored in each semantic value.
Enumerator | |
---|---|
TRACK_NO_DEFINERS |
Do not track definers. |
TRACK_LATEST_DEFINER |
Save only the latest definer. |
TRACK_ALL_DEFINERS |
Save all definers. |
Definition at line 776 of file SymbolicSemantics2.h.