SymbolicSemantics::MemoryCell< ValueType > Struct Template Reference

#include <SymbolicSemantics.h>

Collaboration diagram for SymbolicSemantics::MemoryCell< ValueType >:

[legend]List of all members.

---

Detailed Description

template<template< size_t > class ValueType>
struct SymbolicSemantics::MemoryCell< ValueType >

Represents one location in memory.

Has an address data and size in bytes.

When a state is created, every register and memory location will be given a unique named value. However, it's not practicle to store a named value for every possible memory address, yet we want the following example to work correctly:

  1: mov eax, ds:[edx]    // first read returns V1
  2: mov eax, ds:[edx]    // subsequent reads from same address also return V1
  3: mov ds:[ecx], eax    // write to unknown address clobbers all memory
  4: mov eax, ds:[edx]    // read from same address as above returns V2
  5: mov eax, ds:[edx]    // subsequent reads from same address also return V2

Furthermore, the read from ds:[edx] at #1 above, retroactively stores V1 in the original memory state. That way if we need to do additional analyses starting from the same initial state it will be available to use.

To summarize: every memory address is given a unique named value. These values are implicit until the memory location is actually read.

See also readMemory() and writeMemory().

Public Member Functions
template<size_t Len>
	MemoryCell (const ValueType< 32 > &address, const ValueType< Len > data, size_t nbytes, SgAsmInstruction *insn)
bool	is_clobbered () const
void	set_clobbered ()
bool	is_written () const
void	set_written ()
bool	may_alias (const MemoryCell &other, SMTSolver *solver) const
	Returns true if this memory value could possibly overlap with the other memory value.
bool	must_alias (const MemoryCell &other, SMTSolver *solver) const
	Returns true if this memory address is the same as the other.
void	print (std::ostream &o, RenameMap *rmap=NULL, const std::string &prefix="") const
	Prints the value of a memory cell on a single line.
Public Attributes
ValueType< 32 >	address
ValueType< 32 >	data
size_t	nbytes
bool	clobbered
bool	written
Friends
std::ostream &	operator<< (std::ostream &o, const MemoryCell &mc)

---

Constructor & Destructor Documentation

template<template< size_t > class ValueType>

template<size_t Len>

SymbolicSemantics::MemoryCell< ValueType >::MemoryCell	(	const ValueType< 32 > &	address,
		const ValueType< Len >	data,
		size_t	nbytes,
		SgAsmInstruction *	insn
	)			[inline]

---

Member Function Documentation

template<template< size_t > class ValueType>

bool SymbolicSemantics::MemoryCell< ValueType >::is_clobbered

(

)

const [inline]

template<template< size_t > class ValueType>

void SymbolicSemantics::MemoryCell< ValueType >::set_clobbered

(

)

[inline]

template<template< size_t > class ValueType>

bool SymbolicSemantics::MemoryCell< ValueType >::is_written

(

)

const [inline]

template<template< size_t > class ValueType>

void SymbolicSemantics::MemoryCell< ValueType >::set_written

(

)

[inline]

template<template< size_t > class ValueType>

bool SymbolicSemantics::MemoryCell< ValueType >::may_alias	(	const MemoryCell< ValueType > &	other,
		SMTSolver *	solver
	)			const [inline]

Returns true if this memory value could possibly overlap with the other memory value.

In other words, returns false only if this memory location cannot overlap with other memory location. Two addresses that are identical alias one another. The solver is optional but recommended (absence of a solver will result in a naive definition).

Address X and Y may alias each other if X+datasize(X)>=Y or X<Y+datasize(Y) where datasize(A) is the number of bytes stored at address A. In other words, if the following expression is satisfiable, then the memory cells might alias one another.

     ((X.addr + X.nbytes > Y.addr) && (X.addr < Y.addr + Y.nbytes)) ||
     ((Y.addr + Y.nbytes > X.addr) && (Y.addr < X.addr + X.nbytes))
  \code

  Or, equivalently written in LISP style

  \code
     (and (or (> (+ X.addr X.nbytes) Y.addr) (< X.addr (+ Y.addr Y.nbytes)))
          (or (> (+ Y.addr Y.nbytes) X.addr) (< Y.addr (+ X.addr X.nbytes))))

template<template< size_t > class ValueType>

bool SymbolicSemantics::MemoryCell< ValueType >::must_alias	(	const MemoryCell< ValueType > &	other,
		SMTSolver *	solver
	)			const [inline]

Returns true if this memory address is the same as the other.

Note that "same" is more strict than "overlap". The solver is optional but recommended (absence of a solver will result in a naive definition).

template<template< size_t > class ValueType>

void SymbolicSemantics::MemoryCell< ValueType >::print	(	std::ostream &	o,
		RenameMap *	rmap = NULL,
		const std::string &	prefix = ""
	)			const [inline]

Prints the value of a memory cell on a single line.

If a rename map is specified then named values will be renamed to have a shorter name. See the ValueType<>::rename() method for details.

---

Friends And Related Function Documentation

template<template< size_t > class ValueType>

std::ostream& operator<<	(	std::ostream &	o,
		const MemoryCell< ValueType > &	mc
	)			[friend]

---

Member Data Documentation

template<template< size_t > class ValueType>

ValueType<32> SymbolicSemantics::MemoryCell< ValueType >::address

template<template< size_t > class ValueType>

ValueType<32> SymbolicSemantics::MemoryCell< ValueType >::data

template<template< size_t > class ValueType>

size_t SymbolicSemantics::MemoryCell< ValueType >::nbytes

template<template< size_t > class ValueType>

bool SymbolicSemantics::MemoryCell< ValueType >::clobbered

template<template< size_t > class ValueType>

bool SymbolicSemantics::MemoryCell< ValueType >::written

---

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

• SymbolicSemantics.h

---