ROSE  0.9.9.139
Classes | Typedefs | Enumerations
Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics Namespace Reference

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.

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.

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 MergerMergerPtr
 Shared-ownership pointer for a merge control object. More...
 
typedef Sawyer::SharedPointer< class SValueSValuePtr
 Shared-ownership pointer for symbolic semantic value. More...
 
typedef BaseSemantics::RegisterStateGeneric RegisterState
 
typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr
 
typedef boost::shared_ptr< class MemoryListStateMemoryListStatePtr
 Shared-ownership pointer for symbolic list-based memory state. More...
 
typedef boost::shared_ptr< class MemoryMapStateMemoryMapStatePtr
 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 RiscOperatorsRiscOperatorsPtr
 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 Documentation

Shared-ownership pointer for a merge control object.

See Shared ownership.

Definition at line 64 of file SymbolicSemantics2.h.

Shared-ownership pointer for symbolic semantic value.

See Shared ownership.

Definition at line 111 of file SymbolicSemantics2.h.

Shared-ownership pointer for symbolic list-based memory state.

See Shared ownership.

Definition at line 431 of file SymbolicSemantics2.h.

Shared-ownership pointer to symbolic memory state.

See Shared ownership.

Definition at line 614 of file SymbolicSemantics2.h.

Shared-ownership pointer to symbolic RISC operations.

See Shared ownership.

Definition at line 756 of file SymbolicSemantics2.h.

Enumeration Type Documentation

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 742 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 749 of file SymbolicSemantics2.h.