Description

Type of values manipulated by the IntervalSemantics domain.

Definition at line 33 of file IntervalSemantics.h.

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

Inheritance diagram for Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue:

[legend]

Public Types
using	Super = BaseSemantics::SValue
	Base type.

using	Ptr = SValuePtr
	Shared-ownership pointer.

Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue
using	Ptr = SValuePtr
	Shared-ownership pointer.

Public Member Functions
virtual BaseSemantics::SValuePtr	bottom_ (size_t nbits) const override
	Data-flow bottom value.

virtual BaseSemantics::SValuePtr	undefined_ (size_t nbits) const override
	Create a new undefined semantic value.

virtual BaseSemantics::SValuePtr	unspecified_ (size_t nbits) const override
	Create a new unspecified semantic value.

virtual BaseSemantics::SValuePtr	number_ (size_t nbits, uint64_t number) const override
	Create a new concrete semantic value.

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

virtual Sawyer::Optional< BaseSemantics::SValuePtr >	createOptionalMerge (const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
	Possibly create a new value by merging two existing values.

virtual SValuePtr	create (size_t nbits, uint64_t v1, uint64_t v2)
	Construct a ValueType that's constrained to be between two unsigned values, inclusive.

virtual SValuePtr	create (size_t nbits, const Intervals &)
	Construct a ValueType from a rangemap.

virtual SValuePtr	create_from_bits (size_t nbits, uint64_t possible_bits)
	Generate ranges from bits.

virtual void	hash (Combinatorics::Hasher &) const override
	Hash this semantic value.

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

virtual void	print (std::ostream &output, BaseSemantics::Formatter &) const override
	Print a value to a stream using default format.

virtual bool	may_equal (const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
	Virtual API.

virtual bool	must_equal (const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
	Virtual API.

virtual bool	is_number () const override
	Virtual API.

virtual uint64_t	get_number () const override
	Virtual API.

const Intervals &	get_intervals () const
	Returns the rangemap stored in this value.

void	set_intervals (const Intervals &)
	Changes the rangemap stored in the value.

uint64_t	possible_bits () const
	Returns all possible bits that could be set.

Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue
virtual SValuePtr	boolean_ (bool value) const
	Create a new, Boolean value.

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

size_t	nBits () const
	Property: value width.

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

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

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

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

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

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

bool	isFalse () const
	Returns true if concrete zero.

std::string	toString () const
	Render this symbolic expression as a string.

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

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

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

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

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

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

virtual size_t	get_width () const
	Virtual API.

virtual void	set_width (size_t nbits)
	Virtual API.

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

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

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

	SharedObject (const SharedObject &)
	Copy constructor.

virtual	~SharedObject ()
	Virtual destructor.

SharedObject &	operator= (const SharedObject &)
	Assignment.

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

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

Static Public Member Functions
static SValuePtr	instance ()
	Instantiate a new prototypical value.

static SValuePtr	instance_bottom (size_t nbits)
	Instantiate a new data-flow-bottom value of specified width.

static SValuePtr	instance_undefined (size_t nbits)
	Instantiate a new undefined value of particular width.

static SValuePtr	instance_unspecified (size_t nbits)
	Instantiate a new unspecified value of specific width.

static SValuePtr	instance_integer (size_t nbits, uint64_t number)
	Instantiate a new concrete value of particular width.

static SValuePtr	instance_intervals (size_t nbits, const Intervals &intervals)
	Instantiate a new value from a set of intervals.

static SValuePtr	instance_hull (size_t nbits, uint64_t v1, uint64_t v2)
	Instantiate a new value that's constrained to be between two unsigned values, inclusive.

static SValuePtr	instance_copy (const SValuePtr &)
	Instantiate a new copy of an existing value.

static SValuePtr	instance_from_bits (size_t nbits, uint64_t possible_bits)
	Create a value from a set of possible bits.

static SValuePtr	promote (const BaseSemantics::SValuePtr &)
	Promote a base value to an IntevalSemantics value.

Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue
static SValuePtr	promote (const SValuePtr &x)

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

static void *	operator new (size_t size)

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

Protected Member Functions
	SValue (size_t nbits)

	SValue (size_t nbits, uint64_t number)

	SValue (size_t nbits, uint64_t v1, uint64_t v2)

	SValue (size_t nbits, const Intervals &intervals)

Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue
	SValue (size_t nbits)

	SValue (const SValue &other)

Protected Attributes
Intervals	intervals_

bool	isBottom_

Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue
size_t	width

Member Typedef Documentation

◆ Super

using Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::Super = BaseSemantics::SValue

Base type.

Definition at line 36 of file IntervalSemantics.h.

◆ Ptr

using Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::Ptr = SValuePtr

Shared-ownership pointer.

Definition at line 39 of file IntervalSemantics.h.

Member Function Documentation

◆ instance()

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::instance ( )

static

Instantiate a new prototypical value.

Prototypical values are only used for their virtual constructors.

◆ instance_undefined()

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::instance_undefined ( size_t nbits )

static

Instantiate a new undefined value of particular width.

Currently, there is no distinction between an unspecified value, an undefined value, and an interval that can represent any value of the specified size.

◆ instance_unspecified()

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::instance_unspecified ( size_t nbits )

static

Instantiate a new unspecified value of specific width.

Currently, there is no distinction between an unspecified value, an undefined value, and an interval that can represent any value of the specified size.

◆ promote()

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::promote ( const BaseSemantics::SValuePtr & )

static

Promote a base value to an IntevalSemantics value.

The value v must have an IntervalSemantics::SValue dynamic type.

◆ bottom_()

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

overridevirtual

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.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ undefined_()

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

overridevirtual

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_

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ unspecified_()

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

overridevirtual

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_

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ number_()

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

overridevirtual

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).

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ copy()

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

overridevirtual

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.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ createOptionalMerge()

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

overridevirtual

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.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ create()

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::create	(	size_t	nbits,
		const Intervals &
	)

virtual

Construct a ValueType from a rangemap.

Note that this does not truncate the rangemap to contain only values that would be possible for the ValueType size–see unsignedExtend() for that.

◆ create_from_bits()

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::create_from_bits	(	size_t	nbits,
		uint64_t	possible_bits
	)

virtual

Generate ranges from bits.

Given the set of bits that could be set, generate a range. We have to be careful here because we could end up generating very large rangemaps: a rangemap where the high 31 bits could be set but the zero bit must be cleared would create a rangemap with 2^31 singleton entries.

◆ hash()

virtual void Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::hash ( Combinatorics::Hasher & ) const

overridevirtual

Hash this semantic value.

Hashes the value by appending it to the specified hasher.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ isBottom()

virtual bool Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::isBottom ( ) const

overridevirtual

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.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ print()

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

overridevirtual

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().

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ may_equal()

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

overridevirtual

Virtual API.

See mayEqual.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ must_equal()

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

overridevirtual

Virtual API.

See mustEqual.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ is_number()

virtual bool Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::is_number ( ) const

overridevirtual

Virtual API.

See isConcrete.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

◆ get_number()

virtual uint64_t Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::get_number ( ) const

overridevirtual

Virtual API.

See toUnsigned and toSigned.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue.

Member Data Documentation

◆ intervals_

Intervals Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::intervals_

protected

Definition at line 42 of file IntervalSemantics.h.

◆ isBottom_

bool Rose::BinaryAnalysis::InstructionSemantics::IntervalSemantics::SValue::isBottom_

protected

Definition at line 43 of file IntervalSemantics.h.

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

IntervalSemantics.h

Description

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Member Typedef Documentation

◆ Super

◆ Ptr

Member Function Documentation

◆ instance()

◆ instance_undefined()

◆ instance_unspecified()

◆ promote()

◆ bottom_()

◆ undefined_()

◆ unspecified_()

◆ number_()

◆ copy()

◆ createOptionalMerge()

◆ create()

◆ create_from_bits()

◆ hash()

◆ isBottom()

◆ print()

◆ may_equal()

◆ must_equal()

◆ is_number()

◆ get_number()

Member Data Documentation

◆ intervals_

◆ isBottom_