ROSE
0.11.28.0
|
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.
Definition at line 462 of file SymbolicSemantics2.h.
#include <SymbolicSemantics2.h>
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 |
![]() | |
typedef std::list< MemoryCellPtr > | CellList |
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... | |
CellCompressor * | get_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... | |
![]() | |
virtual void | clear () ROSE_OVERRIDE |
virtual bool | merge (const MemoryStatePtr &other, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE |
virtual std::vector< MemoryCellPtr > | matchingCells (const MemoryCell::Predicate &) const ROSE_OVERRIDE |
Find all matching cells. More... | |
virtual std::vector< MemoryCellPtr > | leadingCells (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 CellList & | get_cells () const |
Returns the list of all memory cells. | |
virtual CellList & | get_cells () |
Returns the list of all memory cells. | |
![]() | |
void | eraseNonWritten () |
Erase cells that have no writers. More... | |
std::vector< MemoryCellPtr > | allCells () 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 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 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) |
![]() | |
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) |
![]() | |
MemoryCellState (const MemoryCellPtr &protocell) | |
MemoryCellState (const SValuePtr &addrProtoval, const SValuePtr &valProtoval) | |
MemoryCellState (const MemoryCellState &other) | |
Protected Attributes | |
CellCompressor * | cell_compressor |
Callback when a memory read aliases multiple memory cells. More... | |
![]() | |
CellList | cells |
bool | occlusionsErased_ |
![]() | |
MemoryCellPtr | protocell |
MemoryCellPtr | latestWrittenCell_ |
Static Protected Attributes | |
static CellCompressorChoice | cc_choice |
The default cell compressor. More... | |
|
inlinestatic |
Instantiates a new memory state having specified prototypical cells and value.
Definition at line 547 of file SymbolicSemantics2.h.
Referenced by create(), Rose::BinaryAnalysis::InstructionSemantics2::LlvmSemantics::RiscOperators::instance(), and Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::instance().
|
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.
|
inlinestatic |
Instantiates a new deep copy of an existing state.
Definition at line 559 of file SymbolicSemantics2.h.
|
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().
|
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().
|
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.
|
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 |
Read a byte from memory.
In order to read a multi-byte value, use RiscOperators::readMemory().
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.
|
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 |
Write a byte to memory.
In order to write a multi-byte value, use RiscOperators::writeMemory().
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.
|
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.
|
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.
|
protected |
Callback when a memory read aliases multiple memory cells.
Definition at line 512 of file SymbolicSemantics2.h.
Referenced by get_cell_compressor().
|
staticprotected |
The default cell compressor.
Static because we use its address.
Definition at line 513 of file SymbolicSemantics2.h.