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