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 452 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 |
 Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList | |
| 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 Types inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryState | |
| typedef MemoryStatePtr | Ptr |
| Shared-ownership pointer for a MemoryState. 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... | |
| Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList | |
| virtual void | clear () ROSE_OVERRIDE |
| Clear memory. More... | |
| virtual bool | merge (const MemoryStatePtr &other, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE |
| Merge memory states for data flow analysis. More... | |
| 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 |
| Print a memory state to more than one line of output. | |
| 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 CellList | scan (const SValuePtr &address, size_t nbits, RiscOperators *addrOps, RiscOperators *valOps, bool &short_circuited) const ROSE_DEPRECATED("use the cursor-based scan instead") |
| virtual MemoryCellPtr | get_latest_written_cell () const ROSE_DEPRECATED("use latestWrittenCell instead") |
| 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... | |
| virtual std::set< rose_addr_t > | get_latest_writers (const SValuePtr &addr, size_t nbits, RiscOperators *addrOps, RiscOperators *valOps) ROSE_DEPRECATED("use getWritersUnion instead") |
| 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. | |
| Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellState | |
| 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. | |
| Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryState | |
| SValuePtr | get_addr_protoval () const |
| Return the address protoval. More... | |
| SValuePtr | get_val_protoval () const |
| Return the value protoval. More... | |
| MergerPtr | merger () const |
| Property: Merger. More... | |
| void | merger (const MergerPtr &m) |
| Property: Merger. More... | |
| bool | byteRestricted () const |
| Indicates whether memory cell values are required to be eight bits wide. More... | |
| void | byteRestricted (bool b) |
| Indicates whether memory cell values are required to be eight bits wide. More... | |
| ByteOrder::Endianness | get_byteOrder () const |
| Memory byte order. | |
| void | set_byteOrder (ByteOrder::Endianness bo) |
| Memory byte order. | |
| void | print (std::ostream &stream, const std::string prefix="") const |
| Print a memory state to more than one line of output. | |
| WithFormatter | with_format (Formatter &fmt) |
| Used for printing memory states with formatting. More... | |
| WithFormatter | operator+ (Formatter &fmt) |
| Used for printing memory states with formatting. More... | |
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... | |
| Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryState | |
| static MemoryStatePtr | promote (const MemoryStatePtr &x) |
Protected Member Functions | |
| MemoryListState (const BaseSemantics::MemoryCellPtr &protocell) | |
| MemoryListState (const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) | |
| MemoryListState (const MemoryListState &other) | |
| virtual BaseSemantics::SValuePtr | readOrPeekMemory (const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, bool 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 Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryState | |
| MemoryState (const SValuePtr &addrProtoval, const SValuePtr &valProtoval) | |
| MemoryState (const MemoryStatePtr &other) | |
Protected Attributes | |
| CellCompressor * | cell_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
|
inlinestatic |
Instantiates a new memory state having specified prototypical cells and value.
Definition at line 537 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 543 of file SymbolicSemantics2.h.
|
inlinestatic |
Instantiates a new deep copy of an existing state.
Definition at line 549 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 558 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 564 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 569 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 578 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 620 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 621 of file SymbolicSemantics2.h.
Member Data Documentation
|
protected |
Callback when a memory read aliases multiple memory cells.
Definition at line 502 of file SymbolicSemantics2.h.
Referenced by get_cell_compressor().
|
staticprotected |
The default cell compressor.
Static because we use its address.
Definition at line 503 of file SymbolicSemantics2.h.
The documentation for this class was generated from the following file:
