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 400 of file SymbolicSemantics.h.

#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>

Inheritance diagram for Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::MemoryListState:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::MemoryListState:

[legend]

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.

using	Ptr = MemoryListStatePtr
	Shared-ownership pointer.

Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryCellList
using	Super = MemoryCellState
	Base type.

using	Ptr = MemoryCellListPtr
	Shared-ownership pointer.

Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryCellState
using	Super = MemoryState
	Base type.

using	Ptr = MemoryCellStatePtr
	Shared-ownership pointer.

Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState
typedef MemoryStatePtr	Ptr
	Shared-ownership pointer.

Public Member Functions
virtual BaseSemantics::MemoryStatePtr	create (const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
	Virtual constructor.

virtual BaseSemantics::MemoryStatePtr	create (const BaseSemantics::MemoryCellPtr &protocell) const override
	Virtual constructor.

virtual BaseSemantics::MemoryStatePtr	clone () const override
	Virtual copy constructor.

virtual BaseSemantics::SValuePtr	readMemory (const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators addrOps, BaseSemantics::RiscOperators valOps) override
	Read a byte from memory.

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.

virtual void	writeMemory (const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators addrOps, BaseSemantics::RiscOperators valOps) override
	Write a byte to memory.

CellCompressor::Ptr	get_cell_compressor () const

void	set_cell_compressor (const CellCompressor::Ptr &)


CellCompressor::Ptr	cellCompressor () const
	Callback for handling a memory read whose address matches more than one memory cell.

void	cellCompressor (const CellCompressor::Ptr &)
	Callback for handling a memory read whose address matches more than one memory cell.

Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryCellList
virtual void	clear () override
	Clear memory.

virtual bool	merge (const MemoryStatePtr &other, RiscOperators addrOps, RiscOperators valOps) override
	Merge memory states for data flow analysis.

virtual std::vector< MemoryCellPtr >	matchingCells (MemoryCell::Predicate &) const override
	Find all matching cells.

virtual std::vector< MemoryCellPtr >	leadingCells (MemoryCell::Predicate &) const override
	Find leading matching cells.

virtual void	eraseMatchingCells (MemoryCell::Predicate &) override
	Remove all matching cells.

virtual void	eraseLeadingCells (MemoryCell::Predicate &) override
	Remove leading matching cells.

virtual void	traverse (MemoryCell::Visitor &) override
	Traverse and modify cells.

virtual void	hash (Combinatorics::Hasher &, RiscOperators addrOps, RiscOperators valOps) const override
	Calculate a hash for this memory state.

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.

bool	mergeWithAliasing (const MemoryStatePtr &other, RiscOperators addrOps, RiscOperators valOps)
	Merge two states with aliasing.

virtual bool	isAllPresent (const SValuePtr &address, size_t nBytes, RiscOperators addrOps, RiscOperators valOps) const
	Predicate to determine whether all bytes are present.

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.

virtual AddressSet	getWritersUnion (const SValuePtr &addr, size_t nBits, RiscOperators addrOps, RiscOperators valOps) override
	Writers for an address.

virtual AddressSet	getWritersIntersection (const SValuePtr &addr, size_t nBits, RiscOperators addrOps, RiscOperators valOps) override
	Writers for an address.

bool	occlusionsErased () const
	Property: erase occluded cells.

void	occlusionsErased (bool b)
	Property: erase occluded cells.

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::InstructionSemantics::BaseSemantics::MemoryCellState
virtual void	updateReadProperties (const CellList &)
	Adjust I/O properties after reading memory.

virtual void	updateWriteProperties (const CellList &, InputOutputPropertySet)
	Adjust I/O properties after writing memory.

void	eraseNonWritten ()
	Erase cells that have no writers.

std::vector< MemoryCellPtr >	allCells () const
	All cells.

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::InstructionSemantics::BaseSemantics::MemoryState
SValuePtr	get_addr_protoval () const
	Return the address protoval.

SValuePtr	get_val_protoval () const
	Return the value protoval.

MergerPtr	merger () const
	Property: Merger.

void	merger (const MergerPtr &)
	Property: Merger.

bool	byteRestricted () const
	Indicates whether memory cell values are required to be eight bits wide.

void	byteRestricted (bool)
	Indicates whether memory cell values are required to be eight bits wide.

ByteOrder::Endianness	get_byteOrder () const
	Memory byte order.

void	set_byteOrder (ByteOrder::Endianness)
	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 &)
	Used for printing memory states with formatting.

WithFormatter	operator+ (Formatter &)
	Used for printing memory states with formatting.

WithFormatter	operator+ (const std::string &linePrefix)
	Used for printing memory states with formatting.

Static Public Member Functions
static MemoryListStatePtr	instance (const BaseSemantics::MemoryCellPtr &protocell)
	Instantiates a new memory state having specified prototypical cells and value.

static MemoryListStatePtr	instance (const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
	Instantiates a new memory state having specified prototypical value.

static MemoryListStatePtr	instance (const MemoryListStatePtr &other)
	Instantiates a new deep copy of an existing state.

static MemoryListStatePtr	promote (const BaseSemantics::MemoryStatePtr &)
	Recasts a base pointer to a symbolic memory state.

Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryCellList
static MemoryCellListPtr	instance (const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
	Instantiate a new prototypical memory state.

static MemoryCellListPtr	instance (const MemoryCellPtr &protocell)
	Instantiate a new memory state with prototypical memory cell.

static MemoryCellListPtr	instance (const MemoryCellListPtr &other)
	Instantiate a new copy of an existing memory state.

static MemoryCellListPtr	promote (const BaseSemantics::MemoryStatePtr &m)
	Promote a base memory state pointer to a BaseSemantics::MemoryCellList pointer.

Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryCellState
static MemoryCellStatePtr	promote (const BaseSemantics::MemoryStatePtr &m)
	Promote a base memory state pointer to a BaseSemantics::MemoryCellState pointer.

Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState
static MemoryStatePtr	promote (const MemoryStatePtr &)

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::InstructionSemantics::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 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::InstructionSemantics::BaseSemantics::MemoryCellState
	MemoryCellState (const MemoryCellPtr &protocell)

	MemoryCellState (const SValuePtr &addrProtoval, const SValuePtr &valProtoval)

	MemoryCellState (const MemoryCellState &other)

Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState
	MemoryState (const SValuePtr &addrProtoval, const SValuePtr &valProtoval)

	MemoryState (const MemoryStatePtr &other)

Additional Inherited Members
Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryCellList
CellList	cells

bool	occlusionsErased_

Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryCellState
MemoryCellPtr	protocell

MemoryCellPtr	latestWrittenCell_

Member Typedef Documentation

◆ Super

using Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::MemoryListState::Super = BaseSemantics::MemoryCellList

Base type.

Definition at line 403 of file SymbolicSemantics.h.

◆ Ptr

using Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::MemoryListState::Ptr = MemoryListStatePtr

Shared-ownership pointer.

Definition at line 406 of file SymbolicSemantics.h.

Member Function Documentation

◆ instance()

static MemoryListStatePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::MemoryListState::instance	(	const BaseSemantics::SValuePtr &	addrProtoval,
		const BaseSemantics::SValuePtr &	valProtoval
	)

static

Instantiates a new memory state having specified prototypical value.

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

◆ create() [1/2]

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

overridevirtual

Virtual constructor.

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

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

Reimplemented in Rose::BinaryAnalysis::Partitioner2::Semantics::MemoryState< Super >.

◆ create() [2/2]

virtual BaseSemantics::MemoryStatePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::MemoryListState::create ( const BaseSemantics::MemoryCellPtr & protocell ) const

overridevirtual

Virtual constructor.

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

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

Reimplemented in Rose::BinaryAnalysis::Partitioner2::Semantics::MemoryState< Super >.

◆ clone()

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

overridevirtual

Virtual copy constructor.

Creates a new deep copy of this memory state.

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

Reimplemented in Rose::BinaryAnalysis::Partitioner2::Semantics::MemoryState< Super >.

◆ promote()

static MemoryListStatePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::MemoryListState::promote ( const BaseSemantics::MemoryStatePtr & )

static

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.

◆ readMemory()

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

overridevirtual

Read a byte from memory.

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

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

Reimplemented in Rose::BinaryAnalysis::Partitioner2::Semantics::MemoryState< Super >.

◆ peekMemory()

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

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::InstructionSemantics::BaseSemantics::MemoryCellList.

Reimplemented in Rose::BinaryAnalysis::Partitioner2::Semantics::MemoryState< Super >.

◆ writeMemory()

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

overridevirtual

Write a byte to memory.

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

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

Reimplemented in Rose::BinaryAnalysis::Partitioner2::Semantics::MemoryState< Super >.

◆ cellCompressor() [1/2]

CellCompressor::Ptr Rose::BinaryAnalysis::InstructionSemantics::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().

◆ cellCompressor() [2/2]

void Rose::BinaryAnalysis::InstructionSemantics::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:

SymbolicSemantics.h

Description

Classes

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Additional Inherited Members

Member Typedef Documentation

◆ Super

◆ Ptr

Member Function Documentation

◆ instance()

◆ create() [1/2]

◆ create() [2/2]

◆ clone()

◆ promote()

◆ readMemory()

◆ peekMemory()

◆ writeMemory()

◆ cellCompressor() [1/2]

◆ cellCompressor() [2/2]