Description

Type of values manipulated by the SymbolicSemantics domain.

Values of type type are used whenever a value needs to be stored, such as memory addresses, the values stored at those addresses, the values stored in registers, the operands for RISC operations, and the results of those operations.

Taint SValues are symbolic SValues with additional taint information. Taintedness is a set represented by the four possible values of the Taintedness enum. Values can be tainted, untainted, neither, or both. The "neither" case means we don't know anything about the taintedness of the value and is also called "bottom" in dataflow parlance. When data flow merges two values and one is tainted and the other is untainted, then the merged result is both tainted and untainted at the same time, which is called "top" in data flow parlance. Note that the isBottom method inherited from SymbolicSemantics::SValue tests whether the symbolic value is a bottom value, not whether the taintedness is bottom.

Definition at line 59 of file TaintSemantics.h.

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

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

[legend]

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

[legend]

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

using	Ptr = SValuePtr
	Shared-ownership pointer.

Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue
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 value) const override
	Create a new concrete semantic value.

virtual BaseSemantics::SValuePtr	boolean_ (bool value) const override
	Create a new, Boolean 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 void	print (std::ostream &, BaseSemantics::Formatter &) const override
	Print a value to a stream using default format.

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


Taintedness	taintedness () const
	Property: Taintedness.

void	taintedness (Taintedness)
	Property: Taintedness.

Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue
virtual bool	isBottom () const override
	Determines whether a value is a data-flow bottom.

virtual SValuePtr	substitute (const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const
	Substitute one value for another throughout a value.

virtual const ExprPtr &	get_expression () const
	Returns the expression stored in this value.

virtual const InsnSet &	get_defining_instructions () const
	Returns the set of instructions that defined this value.

virtual void	defined_by (SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3)
	Adds instructions to the list of defining instructions.

virtual void	defined_by (SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2)
	Adds instructions to the list of defining instructions.

virtual void	defined_by (SgAsmInstruction *insn, const InsnSet &set1)
	Adds instructions to the list of defining instructions.

virtual void	defined_by (SgAsmInstruction *insn)
	Adds instructions to the list of defining instructions.

virtual void	set_expression (const ExprPtr &new_expr)
	Changes the expression stored in the value.

virtual void	set_expression (const SValuePtr &source)
	Changes the expression stored in the value.

virtual size_t	add_defining_instructions (const InsnSet &to_add)
	Adds definitions to the list of defining instructions.

virtual size_t	add_defining_instructions (const SValuePtr &source)
	Adds definitions to the list of defining instructions.

virtual size_t	add_defining_instructions (SgAsmInstruction *insn)
	Adds definitions to the list of defining instructions.

virtual void	set_defining_instructions (const InsnSet &new_defs)
	Set defining instructions.

virtual void	set_defining_instructions (const SValuePtr &source)
	Set defining instructions.

virtual void	set_defining_instructions (SgAsmInstruction *insn)
	Set defining instructions.

Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue
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.

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 specified width.

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

static SValuePtr	instance_integer (size_t nbits, uint64_t value)
	Instantiate a new concrete value.

static SValuePtr	instance_symbolic (const SymbolicExpression::Ptr &value)
	Instantiate a new symbolic value.

static SValuePtr	promote (const BaseSemantics::SValuePtr &v)
	Promote a base value to a TaintSemantics value.

static Taintedness	mergeTaintedness (Taintedness, Taintedness)

Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue
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 specified width.

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

static SValuePtr	instance_integer (size_t nbits, uint64_t value)
	Instantiate a new concrete value.

static SValuePtr	instance_symbolic (const SymbolicExpression::Ptr &value)
	Instantiate a new symbolic value.

static SValuePtr	promote (const BaseSemantics::SValuePtr &)
	Promote a base value to a SymbolicSemantics 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 (ExprPtr expr)

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.

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

	SValue (size_t nbits, uint64_t number)

	SValue (ExprPtr expr)

virtual void	set_width (size_t nbits) override
	Virtual API.

virtual bool	is_number () const override
	Virtual API.

virtual uint64_t	get_number () const override
	Virtual API.

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

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

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

	SValue (const SValue &other)

Additional Inherited Members
Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue
ExprPtr	expr
	The symbolic expression for this value.

InsnSet	defs
	Instructions defining this value.

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

Member Typedef Documentation

◆ Super

using Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::Super = SymbolicSemantics::SValue

Base type.

Definition at line 64 of file TaintSemantics.h.

◆ Ptr

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

Shared-ownership pointer.

Definition at line 67 of file TaintSemantics.h.

Constructor & Destructor Documentation

◆ SValue() [1/4]

Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::SValue ( )

inlineprotected

Definition at line 85 of file TaintSemantics.h.

◆ SValue() [2/4]

Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::SValue ( size_t nbits )

inlineexplicitprotected

Definition at line 87 of file TaintSemantics.h.

◆ SValue() [3/4]

Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::SValue	(	size_t	nbits,
		uint64_t	number
	)

inlineprotected

Definition at line 89 of file TaintSemantics.h.

◆ SValue() [4/4]

Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::SValue ( ExprPtr expr )

inlineprotected

Definition at line 91 of file TaintSemantics.h.

Member Function Documentation

◆ instance()

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

inlinestatic

Instantiate a new prototypical value.

Prototypical values are only used for their virtual constructors.

Definition at line 97 of file TaintSemantics.h.

References Rose::BinaryAnalysis::SymbolicExpression::makeIntegerVariable().

◆ instance_bottom()

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::instance_bottom ( size_t nbits )

inlinestatic

Instantiate a new data-flow bottom value of specified width.

The symbolic value is what is set to bottom in this case. The taintedness is always set to bottom by all the static allocating constructors. If you need a different taintedness then you need to change it with the taintedness property.

Definition at line 106 of file TaintSemantics.h.

References Rose::BinaryAnalysis::SymbolicExpression::Node::BOTTOM, and Rose::BinaryAnalysis::SymbolicExpression::makeIntegerVariable().

Referenced by bottom_().

◆ instance_undefined()

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

inlinestatic

Instantiate a new undefined value of specified width.

Definition at line 111 of file TaintSemantics.h.

References Rose::BinaryAnalysis::SymbolicExpression::makeIntegerVariable().

Referenced by undefined_().

◆ instance_unspecified()

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

inlinestatic

Instantiate a new unspecified value of specified width.

Definition at line 116 of file TaintSemantics.h.

References Rose::BinaryAnalysis::SymbolicExpression::makeIntegerVariable(), and Rose::BinaryAnalysis::SymbolicExpression::Node::UNSPECIFIED.

Referenced by unspecified_().

◆ instance_integer()

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::instance_integer	(	size_t	nbits,
		uint64_t	value
	)

inlinestatic

Instantiate a new concrete value.

Definition at line 121 of file TaintSemantics.h.

References Rose::BinaryAnalysis::SymbolicExpression::makeIntegerConstant().

Referenced by boolean_(), and number_().

◆ instance_symbolic()

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::instance_symbolic ( const SymbolicExpression::Ptr & value )

inlinestatic

Instantiate a new symbolic value.

Definition at line 126 of file TaintSemantics.h.

◆ bottom_()

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

inlineoverridevirtual

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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

Definition at line 134 of file TaintSemantics.h.

References instance_bottom().

◆ undefined_()

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

inlineoverridevirtual

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_

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

Definition at line 143 of file TaintSemantics.h.

References instance_undefined().

◆ unspecified_()

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

inlineoverridevirtual

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_

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

Definition at line 147 of file TaintSemantics.h.

References instance_unspecified().

◆ number_()

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

inlineoverridevirtual

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

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

Definition at line 151 of file TaintSemantics.h.

References instance_integer().

◆ boolean_()

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

inlineoverridevirtual

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 from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

Definition at line 155 of file TaintSemantics.h.

References instance_integer().

◆ copy()

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

inlineoverridevirtual

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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

Definition at line 159 of file TaintSemantics.h.

◆ createOptionalMerge()

virtual Sawyer::Optional< BaseSemantics::SValuePtr > Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

◆ promote()

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

inlinestatic

Promote a base value to a TaintSemantics value.

The value v must have a TaintSemantics::SValue dynamic type.

Definition at line 174 of file TaintSemantics.h.

References Sawyer::SharedPointer< T >::dynamicCast().

◆ print()

virtual void Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::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().

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

◆ hash()

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

overridevirtual

Hash this semantic value.

Hashes the value by appending it to the specified hasher.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

◆ may_equal()

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

overrideprotectedvirtual

Virtual API.

See mayEqual.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

◆ must_equal()

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

overrideprotectedvirtual

Virtual API.

See mustEqual.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.

◆ taintedness() [1/2]

Taintedness Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::taintedness ( ) const

Property: Taintedness.

True if the value is considered to be tainted, and false otherwise.

◆ taintedness() [2/2]

void Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue::taintedness ( Taintedness )

Property: Taintedness.

True if the value is considered to be tainted, and false otherwise.

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

TaintSemantics.h

Description

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Additional Inherited Members

Member Typedef Documentation

◆ Super

◆ Ptr

Constructor & Destructor Documentation

◆ SValue() [1/4]

◆ SValue() [2/4]

◆ SValue() [3/4]

◆ SValue() [4/4]

Member Function Documentation

◆ instance()

◆ instance_bottom()

◆ instance_undefined()

◆ instance_unspecified()

◆ instance_integer()

◆ instance_symbolic()

◆ bottom_()

◆ undefined_()

◆ unspecified_()

◆ number_()

◆ boolean_()

◆ copy()

◆ createOptionalMerge()

◆ promote()

◆ print()

◆ hash()

◆ may_equal()

◆ must_equal()

◆ taintedness() [1/2]

◆ taintedness() [2/2]