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 472 of file SymbolicSemantics.h.
#include <Rose/BinaryAnalysis/InstructionSemantics2/SymbolicSemantics.h>
Classes | |
| class | CellCompressor |
| Functor for handling a memory read that found more than one cell that might alias the requested address. More... | |
| class | CellCompressorChoice |
| Functor for handling a memory read whose address matches more than one memory cell. More... | |
| class | CellCompressorMcCarthy |
| Functor for handling a memory read whose address matches more than one memory cell. More... | |
| class | CellCompressorSet |
| Functor for handling a memory read whose address matches more than one memory cell. More... | |
| class | CellCompressorSimple |
| Functor for handling a memory read whose address matches more than one memory cell. More... | |
Public Types | |
| using | Super = BaseSemantics::MemoryCellList |
| Base type. More... | |
| using | Ptr = MemoryListStatePtr |
| Shared-ownership pointer. More... | |
 Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList | |
| using | Super = MemoryCellState |
| Base type. More... | |
| using | Ptr = MemoryCellStatePtr |
| Shared-ownership pointer. More... | |
| typedef std::list< MemoryCellPtr > | CellList |
| List of memory cells. More... | |
| Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellState | |
| using | Super = MemoryState |
| Base type. More... | |
| using | Ptr = MemoryCellStatePtr |
| Shared-ownership pointer. 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 override |
| Virtual constructor. More... | |
| virtual BaseSemantics::MemoryStatePtr | create (const BaseSemantics::MemoryCellPtr &protocell) const override |
| Virtual constructor. More... | |
| virtual BaseSemantics::MemoryStatePtr | clone () const override |
| Virtual copy constructor. More... | |
| virtual BaseSemantics::SValuePtr | readMemory (const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) 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) 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) override |
| Write a byte to memory. More... | |
| CellCompressor::Ptr | get_cell_compressor () const ROSE_DEPRECATED("use cellCompressor") |
| void | set_cell_compressor (const CellCompressor::Ptr &) ROSE_DEPRECATED("use cellCompressor") |
| CellCompressor::Ptr | cellCompressor () const |
| Callback for handling a memory read whose address matches more than one memory cell. More... | |
| void | cellCompressor (const CellCompressor::Ptr &) |
| 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 () override |
| Clear memory. More... | |
| virtual bool | merge (const MemoryStatePtr &other, RiscOperators *addrOps, RiscOperators *valOps) override |
| Merge memory states for data flow analysis. More... | |
| virtual std::vector< MemoryCellPtr > | matchingCells (MemoryCell::Predicate &) const override |
| Find all matching cells. More... | |
| virtual std::vector< MemoryCellPtr > | leadingCells (MemoryCell::Predicate &) const override |
| Find leading matching cells. More... | |
| virtual void | eraseMatchingCells (MemoryCell::Predicate &) override |
| Remove all matching cells. More... | |
| virtual void | eraseLeadingCells (MemoryCell::Predicate &) override |
| Remove leading matching cells. More... | |
| virtual void | traverse (MemoryCell::Visitor &) override |
| Traverse and modify cells. More... | |
| virtual void | hash (Combinatorics::Hasher &, RiscOperators *addrOps, RiscOperators *valOps) const override |
| Calculate a hash for this memory state. More... | |
| virtual void | print (std::ostream &, Formatter &) const 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 AddressSet | getWritersUnion (const SValuePtr &addr, size_t nBits, RiscOperators *addrOps, RiscOperators *valOps) override |
| Writers for an address. More... | |
| virtual AddressSet | getWritersIntersection (const SValuePtr &addr, size_t nBits, RiscOperators *addrOps, RiscOperators *valOps) 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. | |
| 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 &) |
| 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 &, 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... | |
| WithFormatter | operator+ (const std::string &linePrefix) |
| 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) | |
| 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 Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryState | |
| MemoryState (const SValuePtr &addrProtoval, const SValuePtr &valProtoval) | |
| MemoryState (const MemoryStatePtr &other) | |
Additional Inherited Members | |
| 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_ |
Member Typedef Documentation
| using Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::Super = BaseSemantics::MemoryCellList |
Base type.
Definition at line 475 of file SymbolicSemantics.h.
| using Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::Ptr = MemoryListStatePtr |
Shared-ownership pointer.
Definition at line 478 of file SymbolicSemantics.h.
Member Function Documentation
|
inlinestatic |
Instantiates a new memory state having specified prototypical cells and value.
Definition at line 586 of file SymbolicSemantics.h.
Referenced by create(), Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryMapState::create(), Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::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 592 of file SymbolicSemantics.h.
|
inlinestatic |
Instantiates a new deep copy of an existing state.
Definition at line 598 of file SymbolicSemantics.h.
|
inlineoverridevirtual |
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 607 of file SymbolicSemantics.h.
References instance().
|
inlineoverridevirtual |
Virtual constructor.
Creates a new memory state having specified prototypical cells and value.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.
Definition at line 613 of file SymbolicSemantics.h.
References instance().
|
inlineoverridevirtual |
Virtual copy constructor.
Creates a new deep copy of this memory state.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.
Definition at line 618 of file SymbolicSemantics.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 627 of file SymbolicSemantics.h.
|
overridevirtual |
Read a byte from memory.
In order to read a multi-byte value, use RiscOperators::readMemory().
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.
|
overridevirtual |
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.
|
overridevirtual |
Write a byte to memory.
In order to write a multi-byte value, use RiscOperators::writeMemory().
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::MemoryCellList.
| CellCompressor::Ptr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::cellCompressor | ( | ) | const |
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().
| void Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::MemoryListState::cellCompressor | ( | const CellCompressor::Ptr & | ) |
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().
The documentation for this class was generated from the following file:
