Description

Purely symbolic memory state.

This memory state stores memory as a symbolic expression consisting of read and/or write operations expressed symbolically. The memory state can be passed to SMT solvers and included in if-then-else symbolic expressions to represent different memory states according to different paths through a specimen.

Definition at line 24 of file SymbolicMemory.h.

#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/SymbolicMemory.h>

Inheritance diagram for Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory:

[legend]

Public Types
using	Super = MemoryState
	Base type.

using	Ptr = SymbolicMemoryPtr
	Shared-ownership pointer.

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

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

virtual MemoryStatePtr	clone () const override
	Virtual allocating copy constructor.

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

virtual void	clear () override
	Clear memory.

virtual SValuePtr	readMemory (const SValuePtr &address, const SValuePtr &dflt, RiscOperators addrOps, RiscOperators valOps) override
	Read a value from memory.

virtual void	writeMemory (const SValuePtr &address, const SValuePtr &value, RiscOperators addrOps, RiscOperators valOps) override
	Write a value to memory.

virtual SValuePtr	peekMemory (const SValuePtr &address, const SValuePtr &dflt, RiscOperators addrOps, RiscOperators valOps) override
	Read a value from memory without side effects.

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.


SymbolicExpression::Ptr	expression () const
	Property: the symbolic expression for the memory.

void	expression (const SymbolicExpression::Ptr &mem)
	Property: the symbolic expression for the memory.

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 SymbolicMemoryPtr	instance (const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
	Instantiate a new empty memory state on the heap.

static SymbolicMemoryPtr	promote (const MemoryStatePtr &x)
	Convert pointer to a SymbolicMemory pointer.

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

Protected Member Functions
	SymbolicMemory (const SValuePtr &addrProtoval, const SValuePtr &valProtoval)

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

	MemoryState (const MemoryStatePtr &other)

Member Typedef Documentation

◆ Super

using Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::Super = MemoryState

Base type.

Definition at line 27 of file SymbolicMemory.h.

◆ Ptr

using Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::Ptr = SymbolicMemoryPtr

Shared-ownership pointer.

Definition at line 30 of file SymbolicMemory.h.

Constructor & Destructor Documentation

◆ SymbolicMemory()

Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::SymbolicMemory	(	const SValuePtr &	addrProtoval,
		const SValuePtr &	valProtoval
	)

inlineexplicitprotected

Definition at line 37 of file SymbolicMemory.h.

Member Function Documentation

◆ instance()

static SymbolicMemoryPtr Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::instance	(	const SValuePtr &	addrProtoval,
		const SValuePtr &	valProtoval
	)

inlinestatic

Instantiate a new empty memory state on the heap.

Definition at line 45 of file SymbolicMemory.h.

Referenced by create().

◆ create()

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

inlineoverridevirtual

Virtual allocating constructor.

Allocates and constructs a new MemoryState object having the same dynamic type as this object. A prototypical SValue must be supplied and will be used to construct any additional SValue objects needed during the operation of a MemoryState. Two prototypical values are supplied, one for addresses and another for values stored at those addresses, although they will almost always be the same.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState.

Definition at line 51 of file SymbolicMemory.h.

References instance().

◆ clone()

virtual MemoryStatePtr Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::clone ( ) const

inlineoverridevirtual

Virtual allocating copy constructor.

Creates a new MemoryState object which is a copy of this object.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState.

Definition at line 56 of file SymbolicMemory.h.

◆ promote()

static SymbolicMemoryPtr Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::promote ( const MemoryStatePtr & x )

inlinestatic

Convert pointer to a SymbolicMemory pointer.

Converts x to a SymbolicMemoryPtr and asserts that it is non-null.

Definition at line 63 of file SymbolicMemory.h.

◆ expression()

SymbolicExpression::Ptr Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::expression ( ) const

inline

Property: the symbolic expression for the memory.

Definition at line 73 of file SymbolicMemory.h.

◆ merge()

virtual bool Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::merge	(	const MemoryStatePtr &	other,
		RiscOperators *	addrOps,
		RiscOperators *	valOps
	)

overridevirtual

Merge memory states for data flow analysis.

Merges the other state into this state, returning true if this state changed.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState.

◆ clear()

virtual void Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::clear ( )

overridevirtual

Clear memory.

Removes all memory cells from this memory state.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState.

◆ readMemory()

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::readMemory	(	const SValuePtr &	address,
		const SValuePtr &	dflt,
		RiscOperators *	addrOps,
		RiscOperators *	valOps
	)

overridevirtual

Read a value from memory.

Consults the memory represented by this MemoryState object and returns a semantic value. Depending on the semantic domain, the value can be a value that is already stored in the memory state, a supplied default value, a new value constructed from some combination of existing values and/or the default value, or anything else. For instance, in a symbolic domain the address could alias multiple existing memory locations and the implementation may choose to return a McCarthy expression. Additional data (such as SMT solvers) may be passed via the RiscOperators argument.

The size of the value being read does not necessarily need to be equal to the size of values stored in the memory state, though it typically is(1). For instance, an implementation may allow reading a 32-bit little endian value from a memory state that stores only bytes. A RiscOperators object is provided for use in these situations.

In order to support cases where an address does not match any existing location, the dflt value can be used to initialize a new memory location. The manner in which the default is used depends on the implementation. In any case, the width of the dflt value determines how much to read.

Footnote 1: A MemoryState::readMemory() call is the last in a sequence of delegations starting with RiscOperators::readMemory(). The designers of the MemoryState, State, and RiscOperators subclasses will need to coordinate to decide which layer should handle concatenating values from individual memory locations.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState.

◆ writeMemory()

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

overridevirtual

Write a value to memory.

Consults the memory represented by this MemoryState object and possibly inserts the specified value. The details of how a value is inserted into a memory state depends entirely on the implementation in a subclass and will probably be different for each semantic domain.

A MemoryState::writeMemory() call is the last in a sequence of delegations starting with RiscOperators::writeMemory(). The designers of the MemoryState, State, and RiscOperators will need to coordinate to decide which layer (if any) should handle splitting a multi-byte value into multiple memory locations.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState.

◆ peekMemory()

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::peekMemory	(	const SValuePtr &	address,
		const SValuePtr &	dflt,
		RiscOperators *	addrOps,
		RiscOperators *	valOps
	)

overridevirtual

Read a value from memory without side effects.

This is similar to readMemory except there are no side effects. The memory state is not modified by this function.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState.

◆ hash()

virtual void Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::hash	(	Combinatorics::Hasher &	,
		RiscOperators *	addrOps,
		RiscOperators *	valOps
	)		const

overridevirtual

Calculate a hash for this memory state.

This hashes the addresses and values stored in memory. The goal is to be able to identify when two memory states are the "same". An analysis might be able to take shortcuts if it encounters a state that it has seen before.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState.

◆ print()

virtual void Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SymbolicMemory::print	(	std::ostream &	,
		Formatter &
	)		const

overridevirtual

Print a memory state to more than one line of output.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::MemoryState.

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

SymbolicMemory.h

Description

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Member Typedef Documentation

◆ Super

◆ Ptr

Constructor & Destructor Documentation

◆ SymbolicMemory()

Member Function Documentation

◆ instance()

◆ create()

◆ clone()

◆ promote()

◆ expression()

◆ merge()

◆ clear()

◆ readMemory()

◆ writeMemory()

◆ peekMemory()

◆ hash()

◆ print()