ROSE  0.10.12.0
Classes | Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | Static Protected Attributes | List of all members
Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState Class Reference

Description

Byte-addressable memory.

This class represents an entire state of memory via a list of memory cells. The memory cell list is sorted in reverse chronological order and addresses that satisfy a "must-alias" predicate are pruned so that only the must recent such memory cell is in the table.

A memory write operation prunes away any existing memory cell that must-alias the newly written address, then adds a new memory cell to the front of the memory cell list.

A memory read operation scans the memory cell list in reverse chronological order to obtain the list of cells that may-alias the address being read (stopping when it hits a must-alias cell). If no must-alias cell is found, then a new cell is added to the memory and the may-alias list. In any case, if the may-alias list contains exactly one cell, that cell's value is returned; otherwise a CellCompressor is called. The default CellCompressor either returns a McCarthy expression or the default value depending on whether an SMT solver is being used.

See also
MemoryMapState

Definition at line 462 of file SymbolicSemantics2.h.

#include <SymbolicSemantics2.h>

Inheritance diagram for Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState:
Inheritance graph
[legend]
Collaboration diagram for Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState:
Collaboration graph
[legend]

Classes

struct  CellCompressor
 Functor for handling a memory read that found more than one cell that might alias the requested address. More...
 
struct  CellCompressorChoice
 Functor for handling a memory read whose address matches more than one memory cell. More...
 
struct  CellCompressorMcCarthy
 Functor for handling a memory read whose address matches more than one memory cell. More...
 
struct  CellCompressorSimple
 Functor for handling a memory read whose address matches more than one memory cell. More...
 

Public Types

typedef BaseSemantics::MemoryCellList Super
 
- Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList
typedef std::list< MemoryCellPtrCellList
 List of memory cells. More...
 
typedef Sawyer::Container::Set< rose_addr_t > AddressSet
 Set of concrete virtual addresses. More...
 

Public Member Functions

virtual BaseSemantics::MemoryStatePtr create (const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE
 Virtual constructor. More...
 
virtual BaseSemantics::MemoryStatePtr create (const BaseSemantics::MemoryCellPtr &protocell) const ROSE_OVERRIDE
 Virtual constructor. More...
 
virtual BaseSemantics::MemoryStatePtr clone () const ROSE_OVERRIDE
 Virtual copy constructor. More...
 
virtual BaseSemantics::SValuePtr readMemory (const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
 Read a byte from memory. More...
 
virtual BaseSemantics::SValuePtr peekMemory (const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
 Read a byte from memory with no side effects. More...
 
virtual void writeMemory (const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE
 Write a byte to memory. More...
 
CellCompressorget_cell_compressor () const
 Callback for handling a memory read whose address matches more than one memory cell. More...
 
void set_cell_compressor (CellCompressor *cc)
 Callback for handling a memory read whose address matches more than one memory cell. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList
virtual void clear () ROSE_OVERRIDE
 
virtual bool merge (const MemoryStatePtr &other, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE
 
virtual std::vector< MemoryCellPtrmatchingCells (const MemoryCell::Predicate &) const ROSE_OVERRIDE
 Find all matching cells. More...
 
virtual std::vector< MemoryCellPtrleadingCells (const MemoryCell::Predicate &) const ROSE_OVERRIDE
 Find leading matching cells. More...
 
virtual void eraseMatchingCells (const MemoryCell::Predicate &) ROSE_OVERRIDE
 Remove all matching cells. More...
 
virtual void eraseLeadingCells (const MemoryCell::Predicate &) ROSE_OVERRIDE
 Remove leading matching cells. More...
 
virtual void traverse (MemoryCell::Visitor &) ROSE_OVERRIDE
 Traverse and modify cells. More...
 
virtual void print (std::ostream &, Formatter &) const ROSE_OVERRIDE
 
bool mergeNoAliasing (const MemoryStatePtr &other, RiscOperators *addrOps, RiscOperators *valOps)
 Merge two states without aliasing. More...
 
bool mergeWithAliasing (const MemoryStatePtr &other, RiscOperators *addrOps, RiscOperators *valOps)
 Merge two states with aliasing. More...
 
virtual bool isAllPresent (const SValuePtr &address, size_t nBytes, RiscOperators *addrOps, RiscOperators *valOps) const
 Predicate to determine whether all bytes are present. More...
 
template<class Iterator >
CellList scan (Iterator &cursor, const SValuePtr &addr, size_t nBits, RiscOperators *addrOps, RiscOperators *valOps) const
 Scan cell list to find matching cells. More...
 
virtual MemoryCell::AddressSet getWritersUnion (const SValuePtr &addr, size_t nBits, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE
 Writers for an address. More...
 
virtual MemoryCell::AddressSet getWritersIntersection (const SValuePtr &addr, size_t nBits, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE
 Writers for an address. More...
 
bool occlusionsErased () const
 Property: erase occluded cells. More...
 
void occlusionsErased (bool b)
 Property: erase occluded cells. More...
 
virtual const CellListget_cells () const
 Returns the list of all memory cells.
 
virtual CellListget_cells ()
 Returns the list of all memory cells.
 
- Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellState
void eraseNonWritten ()
 Erase cells that have no writers. More...
 
std::vector< MemoryCellPtrallCells () const
 All cells. More...
 
virtual MemoryCellPtr latestWrittenCell () const
 Property: Cell most recently written.
 
virtual void latestWrittenCell (const MemoryCellPtr &cell)
 Property: Cell most recently written.
 

Static Public Member Functions

static MemoryListStatePtr instance (const BaseSemantics::MemoryCellPtr &protocell)
 Instantiates a new memory state having specified prototypical cells and value. More...
 
static MemoryListStatePtr instance (const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
 Instantiates a new memory state having specified prototypical value. More...
 
static MemoryListStatePtr instance (const MemoryListStatePtr &other)
 Instantiates a new deep copy of an existing state. More...
 
static MemoryListStatePtr promote (const BaseSemantics::MemoryStatePtr &x)
 Recasts a base pointer to a symbolic memory state. More...
 
- Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList
static MemoryCellListPtr instance (const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
 Instantiate a new prototypical memory state. More...
 
static MemoryCellListPtr instance (const MemoryCellPtr &protocell)
 Instantiate a new memory state with prototypical memory cell. More...
 
static MemoryCellListPtr instance (const MemoryCellListPtr &other)
 Instantiate a new copy of an existing memory state. More...
 
static MemoryCellListPtr promote (const BaseSemantics::MemoryStatePtr &m)
 Promote a base memory state pointer to a BaseSemantics::MemoryCellList pointer. More...
 
- Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellState
static MemoryCellStatePtr promote (const BaseSemantics::MemoryStatePtr &m)
 Promote a base memory state pointer to a BaseSemantics::MemoryCellState pointer. More...
 

Protected Member Functions

 MemoryListState (const BaseSemantics::MemoryCellPtr &protocell)
 
 MemoryListState (const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
 
 MemoryListState (const MemoryListState &other)
 
BaseSemantics::SValuePtr readOrPeekMemory (const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, AllowSideEffects::Flag allowSideEffects)
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList
 MemoryCellList (const MemoryCellPtr &protocell)
 
 MemoryCellList (const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
 
 MemoryCellList (const MemoryCellList &other)
 
virtual SValuePtr mergeCellValues (const CellList &cells, const SValuePtr &dflt, RiscOperators *addrOps, RiscOperators *valOps)
 
virtual AddressSet mergeCellWriters (const CellList &cells)
 
virtual InputOutputPropertySet mergeCellProperties (const CellList &cells)
 
virtual void updateReadProperties (CellList &cells)
 
virtual MemoryCellPtr insertReadCell (const SValuePtr &addr, const SValuePtr &value)
 
virtual MemoryCellPtr insertReadCell (const SValuePtr &addr, const SValuePtr &value, const AddressSet &writers, const InputOutputPropertySet &props)
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellState
 MemoryCellState (const MemoryCellPtr &protocell)
 
 MemoryCellState (const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
 
 MemoryCellState (const MemoryCellState &other)
 

Protected Attributes

CellCompressorcell_compressor
 Callback when a memory read aliases multiple memory cells. More...
 
- Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList
CellList cells
 
bool occlusionsErased_
 
- Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellState
MemoryCellPtr protocell
 
MemoryCellPtr latestWrittenCell_
 

Static Protected Attributes

static CellCompressorChoice cc_choice
 The default cell compressor. More...
 

Member Function Documentation

static MemoryListStatePtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::instance ( const BaseSemantics::MemoryCellPtr protocell)
inlinestatic
static MemoryListStatePtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::instance ( const BaseSemantics::SValuePtr addrProtoval,
const BaseSemantics::SValuePtr valProtoval 
)
inlinestatic

Instantiates a new memory state having specified prototypical value.

This constructor uses BaseSemantics::MemoryCell as the cell type.

Definition at line 553 of file SymbolicSemantics2.h.

static MemoryListStatePtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::instance ( const MemoryListStatePtr other)
inlinestatic

Instantiates a new deep copy of an existing state.

Definition at line 559 of file SymbolicSemantics2.h.

virtual BaseSemantics::MemoryStatePtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::create ( const BaseSemantics::SValuePtr addrProtoval,
const BaseSemantics::SValuePtr valProtoval 
) const
inlinevirtual

Virtual constructor.

Creates a memory state having specified prototypical value. This constructor uses BaseSemantics::MemoryCell as the cell type.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.

Definition at line 568 of file SymbolicSemantics2.h.

References instance().

virtual BaseSemantics::MemoryStatePtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::create ( const BaseSemantics::MemoryCellPtr protocell) const
inlinevirtual

Virtual constructor.

Creates a new memory state having specified prototypical cells and value.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.

Definition at line 574 of file SymbolicSemantics2.h.

References instance().

virtual BaseSemantics::MemoryStatePtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::clone ( ) const
inlinevirtual

Virtual copy constructor.

Creates a new deep copy of this memory state.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.

Definition at line 579 of file SymbolicSemantics2.h.

static MemoryListStatePtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::promote ( const BaseSemantics::MemoryStatePtr x)
inlinestatic

Recasts a base pointer to a symbolic memory state.

This is a checked cast that will fail if the specified pointer does not have a run-time type that is a SymbolicSemantics::MemoryListState or subclass thereof.

Definition at line 588 of file SymbolicSemantics2.h.

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::readMemory ( const BaseSemantics::SValuePtr addr,
const BaseSemantics::SValuePtr dflt,
BaseSemantics::RiscOperators addrOps,
BaseSemantics::RiscOperators valOps 
)
virtual

Read a byte from memory.

In order to read a multi-byte value, use RiscOperators::readMemory().

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::peekMemory ( const BaseSemantics::SValuePtr addr,
const BaseSemantics::SValuePtr dflt,
BaseSemantics::RiscOperators addrOps,
BaseSemantics::RiscOperators valOps 
)
virtual

Read a byte from memory with no side effects.

In order to read a multi-byte value, use RiscOperators::peekMemory().

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.

virtual void Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::writeMemory ( const BaseSemantics::SValuePtr addr,
const BaseSemantics::SValuePtr value,
BaseSemantics::RiscOperators addrOps,
BaseSemantics::RiscOperators valOps 
)
virtual

Write a byte to memory.

In order to write a multi-byte value, use RiscOperators::writeMemory().

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.

CellCompressor* Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::get_cell_compressor ( ) const
inline

Callback for handling a memory read whose address matches more than one memory cell.

See also, cell_compression_mccarthy(), cell_compression_simple(), cell_compression_choice().

Definition at line 630 of file SymbolicSemantics2.h.

References cell_compressor.

void Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::set_cell_compressor ( CellCompressor cc)
inline

Callback for handling a memory read whose address matches more than one memory cell.

See also, cell_compression_mccarthy(), cell_compression_simple(), cell_compression_choice().

Definition at line 631 of file SymbolicSemantics2.h.

Member Data Documentation

CellCompressor* Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::cell_compressor
protected

Callback when a memory read aliases multiple memory cells.

Definition at line 512 of file SymbolicSemantics2.h.

Referenced by get_cell_compressor().

CellCompressorChoice Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::cc_choice
staticprotected

The default cell compressor.

Static because we use its address.

Definition at line 513 of file SymbolicSemantics2.h.


The documentation for this class was generated from the following file: