Description

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.

SValue: the values stored in registers and memory and used for memory addresses.
MemoryCell: an address-expression/value-expression pair for memory.
MemoryState: the collection of MemoryCells that form a complete memory state.
RegisterState: the collection of registers that form a complete register state.
FrameState: the collection operands and local variables that form a complete frame state.
State: represents the state of the virtual machine—its registers and memory.
RiscOperators: the low-level operators called by instruction dispatchers (e.g., DispatcherX86).

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
namespace	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
using	LeafNode = SymbolicExpression::Leaf

using	LeafPtr = SymbolicExpression::LeafPtr

using	InteriorNode = SymbolicExpression::Interior

using	InteriorPtr = SymbolicExpression::InteriorPtr

using	ExprNode = SymbolicExpression::Node

using	ExprPtr = SymbolicExpression::Ptr

using	InsnSet = std::set< SgAsmInstruction * >

using	MergerPtr = Sawyer::SharedPointer< class Merger >
	Shared-ownership pointer for a merge control object.

typedef Sawyer::SharedPointer< class SValue >	SValuePtr
	Shared-ownership pointer for symbolic semantic value.

typedef BaseSemantics::RegisterStateGeneric	RegisterState

typedef BaseSemantics::RegisterStateGenericPtr	RegisterStatePtr

typedef BaseSemantics::FrameState	FrameState

typedef BaseSemantics::FrameStatePtr	FrameStatePtr

typedef boost::shared_ptr< class MemoryListState >	MemoryListStatePtr
	Shared-ownership pointer for symbolic list-based memory state.

typedef boost::shared_ptr< class MemoryMapState >	MemoryMapStatePtr
	Shared-ownership pointer to symbolic memory state.

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.

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