Description

Base class for semantic values.

A semantic value represents a datum from the specimen being analyzed. The datum could be from memory, it could be something stored in a register, it could be the result of some computation, etc. The datum in the specimen has a datum type that might be only partially known; the datum value could, for instance, be 32-bits but unknown whether it is integer or floating point.

The various semantic domains will define SValue subclasses that are appropriate for that domain–a concrete domain will define an SValue that specimen data in a concrete form, an interval domain will define an SValue that represents specimen data in intervals, etc.

Semantics value objects are allocated on the heap and reference counted. The BaseSemantics::SValue is an abstract class that defines the interface. See the Rose::BinaryAnalysis::InstructionSemantics2 namespace for an overview of how the parts fit together.

Definition at line 46 of file SValue.h.

#include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics/SValue.h>

Inheritance diagram for Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue:

[legend]

Classes
class	WithFormatter
	SValue with formatter. More...

Public Types
using	Ptr = SValuePtr
	Shared-ownership pointer for an SValue object. More...

Public Member Functions
virtual SValuePtr	undefined_ (size_t nbits) const =0
	Create a new undefined semantic value. More...

virtual SValuePtr	unspecified_ (size_t nbits) const =0
	Create a new unspecified semantic value. More...

virtual SValuePtr	bottom_ (size_t nBits) const =0
	Data-flow bottom value. More...

virtual SValuePtr	number_ (size_t nbits, uint64_t number) const =0
	Create a new concrete semantic value. More...

virtual SValuePtr	boolean_ (bool value) const
	Create a new, Boolean value. More...

virtual SValuePtr	copy (size_t new_width=0) const =0
	Create a new value from an existing value, changing the width if `new_width` is non-zero. More...

virtual Sawyer::Optional< SValuePtr >	createOptionalMerge (const SValuePtr &other, const MergerPtr &merger, const SmtSolverPtr &solver) const =0
	Possibly create a new value by merging two existing values. More...

SValuePtr	createMerged (const SValuePtr &other, const MergerPtr &merger, const SmtSolverPtr &solver) const
	Create a new value by merging two existing values. More...

size_t	nBits () const
	Property: value width. More...

virtual bool	isBottom () const =0
	Determines whether a value is a data-flow bottom. More...

bool	isConcrete () const
	Determines if the value is a concrete number. More...

Sawyer::Optional< uint64_t >	toUnsigned () const
	Converts a concrete value to a native unsigned integer. More...

Sawyer::Optional< int64_t >	toSigned () const
	Converts a concrete value to a native signed integer. More...

bool	mustEqual (const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const
	Tests two values for equality. More...

bool	mayEqual (const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const
	Tests two values for possible equality. More...

bool	isTrue () const
	Returns true if concrete non-zero. More...

bool	isFalse () const
	Returns true if concrete zero. More...

virtual void	hash (Combinatorics::Hasher &) const =0
	Hash this semantic value. More...

virtual bool	is_number () const =0
	Virtual API. More...

virtual uint64_t	get_number () const =0
	Virtual API. More...

virtual bool	must_equal (const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const =0
	Virtual API. More...

virtual bool	may_equal (const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const =0
	Virtual API. More...


std::string	comment () const
	Property: Comment. More...

void	comment (const std::string &) const
	Property: Comment. More...


void	print (std::ostream &) const
	Print a value to a stream using default format. More...

virtual void	print (std::ostream &, Formatter &) const =0
	Print a value to a stream using default format. More...


WithFormatter	with_format (Formatter &fmt)
	Used for printing values with formatting. More...

WithFormatter	operator+ (Formatter &fmt)
	Used for printing values with formatting. More...

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


virtual size_t	get_width () const
	Virtual API. More...

virtual void	set_width (size_t nbits)
	Virtual API. More...


virtual std::string	get_comment () const
	Some subclasses support the ability to add comments to values. More...

virtual void	set_comment (const std::string &) const
	Some subclasses support the ability to add comments to values. More...

Public Member Functions inherited from Sawyer::SharedObject
	SharedObject ()
	Default constructor. More...

	SharedObject (const SharedObject &)
	Copy constructor. More...

virtual	~SharedObject ()
	Virtual destructor. More...

SharedObject &	operator= (const SharedObject &)
	Assignment. More...

Public Member Functions inherited from Sawyer::SharedFromThis< SValue >
SharedPointer< SValue >	sharedFromThis ()
	Create a shared pointer from `this`. More...

SharedPointer< const SValue >	sharedFromThis () const
	Create a shared pointer from `this`. More...

Static Public Member Functions
static SValuePtr	promote (const SValuePtr &x)

Static Public Member Functions inherited from Sawyer::SmallObject
static SynchronizedPoolAllocator &	poolAllocator ()
	Return the pool allocator for this class. More...

static void *	operator new (size_t size)

static void	operator delete (void *ptr, size_t size)

Protected Member Functions
	SValue (size_t nbits)

	SValue (const SValue &other)

Protected Attributes
size_t	width

Member Typedef Documentation

using Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::Ptr = SValuePtr

Shared-ownership pointer for an SValue object.

See Shared ownership.

Definition at line 49 of file SValue.h.

Member Function Documentation

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::undefined_ ( size_t nbits ) const

pure virtual

Create a new undefined semantic value.

The new semantic value will have the same dynamic type as the value on which this virtual method is called. This is the most common way that a new value is created. The unspecified_ method is closely related.

See also: unspecified_

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::unspecified_ ( size_t nbits ) const

pure virtual

Create a new unspecified semantic value.

The new semantic value will have the same dynamic type as the value on which this virtual method is called. Undefined (undefined_) and unspecified are closely related. Unspecified values are the same as undefined values except they're instantiated as the result of some machine instruction where the ISA documentation indicates that the value is unspecified (e.g., status flags for x86 shift and rotate instructions).

Most semantic domains make no distinction between undefined and unspecified.

See also: undefined_

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::bottom_ ( size_t nBits ) const

pure virtual

Data-flow bottom value.

Returns a new value that represents bottom in a data-flow analysis. If a semantic domain can represent a bottom value then the isBottom predicate is true when invoked on this method's return value. If a semantic domain cannot support a bottom value, then it may return some other value.

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::number_	(	size_t	nbits,
		uint64_t	number
	)		const

pure virtual

Create a new concrete semantic value.

The new value will represent the specified concrete value and have the same dynamic type as the value on which this virtual method is called. This is the most common way that a new constant is created. The number is truncated to contain nbits bits (higher order bits are cleared).

Referenced by boolean_().

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::boolean_ ( bool value ) const

inlinevirtual

Create a new, Boolean value.

The new semantic value will have the same dynamic type as the value on which this virtual method is called. This is how 1-bit flag register values (among others) are created. The base implementation uses number_() to construct a 1-bit value whose bit is zero (false) or one (true).

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue, Rose::BinaryAnalysis::ModelChecker::P2Model::SValue, Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue, and Rose::BinaryAnalysis::InstructionSemantics2::ConcreteSemantics::SValue.

Definition at line 121 of file SValue.h.

References number_().

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::copy ( size_t new_width = 0 ) const

pure virtual

Create a new value from an existing value, changing the width if new_width is non-zero.

Increasing the width logically adds zero bits to the most significant side of the value; decreasing the width logically removes bits from the most significant side of the value.

Referenced by createMerged().

virtual Sawyer::Optional<SValuePtr> Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::createOptionalMerge	(	const SValuePtr &	other,
		const MergerPtr &	merger,
		const SmtSolverPtr &	solver
	)		const

pure virtual

Possibly create a new value by merging two existing values.

This method optionally returns a new semantic value as the data-flow merge of this and other. If the two inputs are "equal" in some sense of the dataflow implementation then nothing is returned, otherwise a new value is returned. Typical usage is like this:

 if (SValuePtr merged = v1->createOptionalMerge(v2).orDefault()) {
     std::cout <<"v1 and v2 were merged to " <<*merged <<"\n";
 } else {
     std::cout <<"no merge is necessary\n";
 }
 or
@code
 SValuePtr merge;
 if (v1->createOptionalMerge(v2).assignTo(merged)) {
     std::cout <<"v1 and v2 were merged to " <<*merged <<"\n";
 } else {
     std::cout <<"v1 and v2 are equal in some sense (no merge necessary)\n";
 }

If you always want a copy regardless of whether the merge is necessary, then use the createMerged convenience function instead.

Referenced by createMerged().

SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::createMerged	(	const SValuePtr &	other,
		const MergerPtr &	merger,
		const SmtSolverPtr &	solver
	)		const

inline

Create a new value by merging two existing values.

This is a convenience wrapper around createOptionalMerge. It always returns a newly constructed semantic value regardless of whether a merge was necessary. In order to determine if a merge was necessary one can compare the return value to this using must_equal, although doing so is more expensive than calling createOptionalMerge.

Definition at line 163 of file SValue.h.

References copy(), and createOptionalMerge().

size_t Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::nBits ( ) const

Property: value width.

Returns the width of the value in bits. One generally doesn't change the width after a value is created.

This function should not be overridden by subclasses. Instead, it calls get_width to do its work.

Referenced by Rose::BinaryAnalysis::InstructionSemantics2::NullSemantics::SValue::print(), Rose::BinaryAnalysis::InstructionSemantics2::MultiSemantics::SValue::set_subvalue(), and Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue::set_width().

virtual bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::isBottom ( ) const

pure virtual

Determines whether a value is a data-flow bottom.

Returns true if this value represents a bottom value for data-flow analysis. Any RiscOperation performed on an operand whose isBottom predicate returns true will itself return a bottom value. This includes operations like "xor x x" which would normally return zero.

Implemented in Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::MultiSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::ConcreteSemantics::SValue, and Rose::BinaryAnalysis::InstructionSemantics2::NullSemantics::SValue.

bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::isConcrete ( ) const

Determines if the value is a concrete number.

Concrete numbers can be created with the number_ and boolean_ methods, virtual constructors, or other means. Some semantic domains have only concrete numbers.

This function should not be overridden by subclasses. Instead, it calls the virtual is_number method to do its work.

Sawyer::Optional<uint64_t> Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::toUnsigned ( ) const

Converts a concrete value to a native unsigned integer.

If this is a concrete value (see isConcrete) and an unsigned integer interpretation of the bits fits in a 64-bit unsigned integer (uint64_t) then that interpretation is returned, otherwise nothing is returned.

This function should not be overridden by subclasses. Instead, it calls get_number to do its work.

Sawyer::Optional<int64_t> Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::toSigned ( ) const

Converts a concrete value to a native signed integer.

If this is a concrete value (see isConcrete) and a signed integer interpretation of the bits fits in a 64-bit signed integer (int64_t) then that interpretation is returned, otherwise nothing is returned.

This function should not be overridden by subclasses. Instead, it calls get_number to do its work.

bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::mustEqual	(	const SValuePtr &	other,
		const SmtSolverPtr &	solver = `SmtSolverPtr()`
	)		const

Tests two values for equality.

Returns true if this value and the other value must be equal, and false if they might not be equal.

This function should not be overridden by subclasses. Instead, it calls must_equal to do its work.

bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::mayEqual	(	const SValuePtr &	other,
		const SmtSolverPtr &	solver = `SmtSolverPtr()`
	)		const

Tests two values for possible equality.

Returns true if this value and the other value might be equal, and false if they cannot be equal.

This function should not be overridden by subclasses. Instead, it calls may_equal to do its work.

bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::isTrue ( ) const

Returns true if concrete non-zero.

This is not virtual since it can be implemented in terms of other functions.

bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::isFalse ( ) const

Returns true if concrete zero.

This is not virtual since it can be implemented in terms of other functions.

std::string Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::comment ( ) const

Property: Comment.

Some subclasses support associating a string comment with a value. If the class does not support comments, then this property will always have an empty value regardless of what's assigned. Since comments do not affect computation, their value is allowed to be changed even for const objects.

This function should not be overridden by subclasses. Instead, it calls get_comment and set_comment to do its work.

void Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::comment ( const std::string & ) const

Property: Comment.

Some subclasses support associating a string comment with a value. If the class does not support comments, then this property will always have an empty value regardless of what's assigned. Since comments do not affect computation, their value is allowed to be changed even for const objects.

This function should not be overridden by subclasses. Instead, it calls get_comment and set_comment to do its work.

virtual void Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::hash ( Combinatorics::Hasher & ) const

pure virtual

Hash this semantic value.

Hashes the value by appending it to the specified hasher.

void Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::print ( std::ostream & ) const

Print a value to a stream using default format.

The value will normally occupy a single line and not contain leading space or line termination. See also, with_format().

virtual void Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::print	(	std::ostream &	,
		Formatter &
	)		const

pure virtual

Print a value to a stream using default format.

The value will normally occupy a single line and not contain leading space or line termination. See also, with_format().

WithFormatter Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::with_format ( Formatter & fmt )

inline

Used for printing values with formatting.

The usual way to use this is:

SValuePtr val = ...;
Formatter fmt = ...;
std::cout <<"The value is: " <<(*val+fmt) <<"\n";

Definition at line 283 of file SValue.h.

Referenced by operator+().

WithFormatter Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::operator+ ( Formatter & fmt )

inline

Used for printing values with formatting.

The usual way to use this is:

SValuePtr val = ...;
Formatter fmt = ...;
std::cout <<"The value is: " <<(*val+fmt) <<"\n";

Definition at line 284 of file SValue.h.

References with_format().

WithFormatter Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::operator+ ( const std::string & linePrefix )

Used for printing values with formatting.

The usual way to use this is:

SValuePtr val = ...;
Formatter fmt = ...;
std::cout <<"The value is: " <<(*val+fmt) <<"\n";

virtual bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::is_number ( ) const

pure virtual

Virtual API.

See isConcrete.

virtual uint64_t Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::get_number ( ) const

pure virtual

Virtual API.

See toUnsigned and toSigned.

virtual size_t Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::get_width ( ) const

inlinevirtual

Virtual API.

See nBits.

Definition at line 302 of file SValue.h.

virtual void Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::set_width ( size_t nbits )

inlinevirtual

Virtual API.

See nBits.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::MultiSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue, and Rose::BinaryAnalysis::InstructionSemantics2::ConcreteSemantics::SValue.

Definition at line 303 of file SValue.h.

Referenced by Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::set_width().

virtual bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::must_equal	(	const SValuePtr &	other,
		const SmtSolverPtr &	solver = `SmtSolverPtr()`
	)		const

pure virtual

Virtual API.

See mustEqual.

virtual bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::may_equal	(	const SValuePtr &	other,
		const SmtSolverPtr &	solver = `SmtSolverPtr()`
	)		const

pure virtual

Virtual API.

See mayEqual.

virtual std::string Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::get_comment ( ) const

inlinevirtual

Some subclasses support the ability to add comments to values.

We define no-op versions of these methods here because it makes things easier. The base class tries to be as small as possible by not storing comments at all. Comments should not affect any computation (comparisons, hash values, etc), and therefore are allowed to be modified even for const objects.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue.

Definition at line 317 of file SValue.h.

virtual void Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::set_comment ( const std::string & ) const

inlinevirtual

Some subclasses support the ability to add comments to values.

We define no-op versions of these methods here because it makes things easier. The base class tries to be as small as possible by not storing comments at all. Comments should not affect any computation (comparisons, hash values, etc), and therefore are allowed to be modified even for const objects.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue.

Definition at line 318 of file SValue.h.

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

SValue.h

Description

Classes

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Member Typedef Documentation

Member Function Documentation