ROSE  0.11.109.0
Namespaces | Classes | Typedefs | Enumerations
Rose::BinaryAnalysis::InstructionSemantics::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.

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

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

Definition at line 73 of file SymbolicSemantics.h.

Shared-ownership pointer for symbolic semantic value.

Definition at line 120 of file SymbolicSemantics.h.

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

Definition at line 456 of file SymbolicSemantics.h.

Shared-ownership pointer to symbolic memory state.

Definition at line 688 of file SymbolicSemantics.h.

Shared-ownership pointer to symbolic RISC operations.

Definition at line 834 of file SymbolicSemantics.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 820 of file SymbolicSemantics.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 827 of file SymbolicSemantics.h.