Description

Defines RISC operators for the SymbolicSemantics domain.

These RISC operators depend on functionality introduced into the SValue class hierarchy at the SymbolicSemantics::SValue level. Therefore, the prototypical value supplied to the constructor or present in the supplied state object must have a dynamic type which is a SymbolicSemantics::SValue.

The RiscOperators object also controls whether use-def information is computed and stored in the SValues. The default is to not compute this information. The set_compute_usedef() method can be used to enable this feature.

Each RISC operator should return a newly allocated semantic value so that the caller can adjust definers for the result without affecting any of the inputs. For example, a no-op that returns its argument should be implemented like this:

BaseSemantics::SValuePtr noop(const BaseSemantics::SValuePtr &arg) {
    return arg->copy();     //correct
    return arg;             //incorrect
}

Definition at line 738 of file SymbolicSemantics.h.

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

Inheritance diagram for Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators:

[legend]

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

using	Ptr = RiscOperatorsPtr
	Shared-ownership pointer.

Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators
enum class	IteStatus { NEITHER , A , B , BOTH }
	Status for iteWithStatus operation. More...

using	Ptr = RiscOperatorsPtr
	Shared-ownership pointer.

Public Member Functions
virtual BaseSemantics::RiscOperatorsPtr	create (const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
	Virtual allocating constructor.

virtual BaseSemantics::RiscOperatorsPtr	create (const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr()) const override
	Virtual allocating constructor.

virtual BaseSemantics::SValuePtr	boolean_ (bool b) override
	Returns a Boolean value.

virtual BaseSemantics::SValuePtr	number_ (size_t nbits, uint64_t value) override
	Returns a number of the specified bit width.

SValuePtr	svalueExpr (const ExprPtr &expr, const InsnSet &defs=InsnSet())

bool	getset_omit_cur_insn (bool b)

virtual void	substitute (const SValuePtr &from, const SValuePtr &to)
	Substitute all occurrences of `from` with `to` in the current state.

virtual BaseSemantics::SValuePtr	filterResult (const BaseSemantics::SValuePtr &)
	Filters results from RISC operators.

virtual SymbolicExpression::Type	sgTypeToSymbolicType (SgAsmType *)
	Convert a SgAsmType to a symbolic type.

virtual void	interrupt (int majr, int minr) override
	Unconditionally raise an interrupt.

virtual BaseSemantics::SValuePtr	and_ (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Computes bit-wise AND of two values.

virtual BaseSemantics::SValuePtr	or_ (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Computes bit-wise OR of two values.

virtual BaseSemantics::SValuePtr	xor_ (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Computes bit-wise XOR of two values.

virtual BaseSemantics::SValuePtr	invert (const BaseSemantics::SValuePtr &a_) override
	One's complement.

virtual BaseSemantics::SValuePtr	extract (const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) override
	Extracts bits from a value.

virtual BaseSemantics::SValuePtr	concat (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Concatenates the bits of two values.

virtual BaseSemantics::SValuePtr	leastSignificantSetBit (const BaseSemantics::SValuePtr &a_) override
	Returns position of least significant set bit; zero when no bits are set.

virtual BaseSemantics::SValuePtr	mostSignificantSetBit (const BaseSemantics::SValuePtr &a_) override
	Returns position of most significant set bit; zero when no bits are set.

virtual BaseSemantics::SValuePtr	rotateLeft (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
	Rotate bits to the left.

virtual BaseSemantics::SValuePtr	rotateRight (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
	Rotate bits to the right.

virtual BaseSemantics::SValuePtr	shiftLeft (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
	Returns arg shifted left.

virtual BaseSemantics::SValuePtr	shiftRight (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
	Returns arg shifted right logically (no sign bit).

virtual BaseSemantics::SValuePtr	shiftRightArithmetic (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
	Returns arg shifted right arithmetically (with sign bit).

virtual BaseSemantics::SValuePtr	equalToZero (const BaseSemantics::SValuePtr &a_) override
	Determines whether a value is equal to zero.

virtual BaseSemantics::SValuePtr	iteWithStatus (const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, IteStatus &) override
	If-then-else with status.

virtual BaseSemantics::SValuePtr	unsignedExtend (const BaseSemantics::SValuePtr &a_, size_t new_width) override
	Extend (or shrink) operand `a` so it is `nbits` wide by adding or removing high-order bits.

virtual BaseSemantics::SValuePtr	signExtend (const BaseSemantics::SValuePtr &a_, size_t new_width) override
	Sign extends a value.

virtual BaseSemantics::SValuePtr	add (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Adds two integers of equal size.

virtual BaseSemantics::SValuePtr	addWithCarries (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, const BaseSemantics::SValuePtr &c_, BaseSemantics::SValuePtr &carry_out) override
	Add two values of equal size and a carry bit.

virtual BaseSemantics::SValuePtr	negate (const BaseSemantics::SValuePtr &a_) override
	Two's complement.

virtual BaseSemantics::SValuePtr	signedDivide (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Divides two signed values.

virtual BaseSemantics::SValuePtr	signedModulo (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Calculates modulo with signed values.

virtual BaseSemantics::SValuePtr	signedMultiply (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Multiplies two signed values.

virtual BaseSemantics::SValuePtr	unsignedDivide (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Divides two unsigned values.

virtual BaseSemantics::SValuePtr	unsignedModulo (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Calculates modulo with unsigned values.

virtual BaseSemantics::SValuePtr	unsignedMultiply (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
	Multiply two unsigned values.

virtual BaseSemantics::SValuePtr	fpConvert (const BaseSemantics::SValuePtr &a, SgAsmFloatType aType, SgAsmFloatType retType) override
	Convert from one floating-point type to another.

virtual BaseSemantics::SValuePtr	reinterpret (const BaseSemantics::SValuePtr &, SgAsmType *) override
	Reinterpret an expression as a different type.

virtual BaseSemantics::SValuePtr	readRegister (RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) override
	Reads a value from a register.

virtual BaseSemantics::SValuePtr	peekRegister (RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) override
	Obtain a register value without side effects.

virtual void	writeRegister (RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) override
	Writes a value to a register.

virtual BaseSemantics::SValuePtr	readMemory (RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, const BaseSemantics::SValuePtr &cond) override
	Reads a value from memory.

virtual BaseSemantics::SValuePtr	peekMemory (RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) override
	Read memory without side effects.

virtual void	writeMemory (RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) override
	Writes a value to memory.

BaseSemantics::SValuePtr	readOrPeekMemory (RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, AllowSideEffects::Flag)


void	computingDefiners (DefinersMode m)
	Property: Track which instructions define a semantic value.

DefinersMode	computingDefiners () const
	Property: Track which instructions define a semantic value.


void	computingMemoryWriters (WritersMode m)
	Property: Track which instructions write to each memory location.

WritersMode	computingMemoryWriters () const
	Property: Track which instructions write to each memory location.


void	computingRegisterWriters (WritersMode m)
	Property: Track latest writer to each register.

WritersMode	computingRegisterWriters () const
	Property: Track latest writer to each register.


void	trimThreshold (uint64_t n)
	Property: Maximum size of expressions.

uint64_t	trimThreshold () const
	Property: Maximum size of expressions.


size_t	nTrimmed () const
	Property: Number of symbolic expressions trimmed.

void	nTrimmed (size_t n)
	Property: Number of symbolic expressions trimmed.


bool	reinterpretMemoryReads () const
	Property: Reinterpret data as unsigned integers when reading from memory or registers.

void	reinterpretMemoryReads (bool b)
	Property: Reinterpret data as unsigned integers when reading from memory or registers.

bool	reinterpretRegisterReads () const
	Property: Reinterpret data as unsigned integers when reading from memory or registers.

void	reinterpretRegisterReads (bool b)
	Property: Reinterpret data as unsigned integers when reading from memory or registers.

Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators
virtual SValuePtr	protoval () const
	Property: Prototypical semantic value.

virtual void	hash (Combinatorics::Hasher &)
	Compute hash of current state.

virtual void	startInstruction (SgAsmInstruction *insn)
	Called at the beginning of every instruction.

virtual void	finishInstruction (SgAsmInstruction *insn)
	Called at the end of every instruction.

virtual void	comment (const std::string &)
	Inject a line comment into debugging streams.

virtual SValuePtr	bottom_ (size_t nbits)
	Returns a data-flow bottom value.

virtual SValuePtr	filterCallTarget (const SValuePtr &a)
	Invoked to filter call targets.

virtual SValuePtr	filterReturnTarget (const SValuePtr &a)
	Invoked to filter return targets.

virtual SValuePtr	filterIndirectJumpTarget (const SValuePtr &a)
	Invoked to filter indirect jumps.

virtual void	hlt ()
	Invoked for the x86 HLT instruction.

virtual void	cpuid ()
	Invoked for the x86 CPUID instruction.

virtual SValuePtr	rdtsc ()
	Invoked for the x86 RDTSC instruction.

virtual std::pair< SValuePtr, SValuePtr >	split (const SValuePtr &a, size_t splitPoint)
	Split a value into two narrower values.

virtual SValuePtr	countLeadingZeros (const SValuePtr &a)
	Count leading zero bits.

virtual SValuePtr	countLeadingOnes (const SValuePtr &a)
	Count leading one bits.

virtual SValuePtr	reverseElmts (const SValuePtr &a, size_t elmtNBits)
	Reverse parts of a value.

virtual SValuePtr	ite (const SValuePtr &cond, const SValuePtr &a, const SValuePtr &b) final
	If-then-else.

virtual SValuePtr	addCarry (const SValuePtr &a, const SValuePtr &b, SValuePtr &carryOut, SValuePtr &overflowed)
	Adds two integers of equal size and carry.

virtual SValuePtr	subtract (const SValuePtr &minuend, const SValuePtr &subtrahend)
	Subtract one value from another.

virtual SValuePtr	subtractCarry (const SValuePtr &minuend, const SValuePtr &subtrahend, SValuePtr &carryOut, SValuePtr &overflowed)
	Subtract one value from another and carry.

virtual void	interrupt (const SValuePtr &majr, const SValuePtr &minr, const SValuePtr &raise)
	Invoked for instructions that cause an interrupt.

virtual void	raiseInterrupt (unsigned majorNumber, unsigned minorNumber, const SValuePtr &raise)
	Conditionally raise an interrupt.

virtual SValuePtr	fpFromInteger (const SValuePtr &intValue, SgAsmFloatType *fpType)
	Construct a floating-point value from an integer value.

virtual SValuePtr	fpToInteger (const SValuePtr &fpValue, SgAsmFloatType *fpType, const SValuePtr &dflt)
	Construct an integer value from a floating-point value.

virtual SValuePtr	fpIsNan (const SValuePtr &fpValue, SgAsmFloatType *fpType)
	Whether a floating-point value is a special not-a-number bit pattern.

virtual SValuePtr	fpIsDenormalized (const SValuePtr &fpValue, SgAsmFloatType *fpType)
	Whether a floating-point value is denormalized.

virtual SValuePtr	fpIsZero (const SValuePtr &fpValue, SgAsmFloatType *fpType)
	Whether a floating-point value is equal to zero.

virtual SValuePtr	fpIsInfinity (const SValuePtr &fpValue, SgAsmFloatType *fpType)
	Whether a floating-point value is infinity.

virtual SValuePtr	fpSign (const SValuePtr &fpValue, SgAsmFloatType *fpType)
	Sign of floating-point value.

virtual SValuePtr	fpEffectiveExponent (const SValuePtr &fpValue, SgAsmFloatType *fpType)
	Exponent of floating-point value.

virtual SValuePtr	fpAdd (const SValuePtr &a, const SValuePtr &b, SgAsmFloatType *fpType)
	Add two floating-point values.

virtual SValuePtr	fpSubtract (const SValuePtr &a, const SValuePtr &b, SgAsmFloatType *fpType)
	Subtract one floating-point value from another.

virtual SValuePtr	fpMultiply (const SValuePtr &a, const SValuePtr &b, SgAsmFloatType *fpType)
	Multiply two floating-point values.

virtual SValuePtr	fpDivide (const SValuePtr &a, const SValuePtr &b, SgAsmFloatType *fpType)
	Divide one floating-point value by another.

virtual SValuePtr	fpSquareRoot (const SValuePtr &a, SgAsmFloatType *fpType)
	Square root.

virtual SValuePtr	fpRoundTowardZero (const SValuePtr &a, SgAsmFloatType *fpType)
	Round toward zero.

virtual SValuePtr	convert (const SValuePtr &a, SgAsmType srcType, SgAsmType dstType)
	Convert value from one type to another.

virtual SmtSolverPtr	solver () const
	Property: Satisfiability module theory (SMT) solver.

virtual void	solver (const SmtSolverPtr &s)
	Property: Satisfiability module theory (SMT) solver.

const HotPatch &	hotPatch () const
	Property: Post-instruction hot patches.

HotPatch &	hotPatch ()
	Property: Post-instruction hot patches.

void	hotPatch (const HotPatch &hp)
	Property: Post-instruction hot patches.

virtual StatePtr	currentState () const
	Property: Current semantic state.

virtual void	currentState (const StatePtr &s)
	Property: Current semantic state.

virtual StatePtr	initialState () const
	Property: Optional lazily updated initial state.

virtual void	initialState (const StatePtr &s)
	Property: Optional lazily updated initial state.

virtual const std::string &	name () const
	Property: Name used for debugging.

virtual void	name (const std::string &s)
	Property: Name used for debugging.

void	print (std::ostream &stream, const std::string prefix="") const
	Print multi-line output for this object.

virtual void	print (std::ostream &stream, Formatter &fmt) const
	Print multi-line output for this object.

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

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

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

virtual size_t	nInsns () const
	Property: Number of instructions processed.

virtual void	nInsns (size_t n)
	Property: Number of instructions processed.

virtual SgAsmInstruction *	currentInstruction () const
	Property: Current instruction.

virtual void	currentInstruction (SgAsmInstruction *insn)
	Property: Current instruction.

virtual bool	isNoopRead () const
	Property: No-op read.

virtual void	isNoopRead (bool b)
	Property: No-op read.

virtual SValuePtr	undefined_ (size_t nbits)
	Returns a new undefined value.

virtual SValuePtr	unspecified_ (size_t nbits)
	Returns a new undefined value.

virtual SValuePtr	concatLoHi (const SValuePtr &lowBits, const SValuePtr &highBits)
	Aliases for concatenation.

virtual SValuePtr	concatHiLo (const SValuePtr &highBits, const SValuePtr &lowBits)
	Aliases for concatenation.

virtual SValuePtr	isEqual (const SValuePtr &a, const SValuePtr &b)
	Equality comparison.

virtual SValuePtr	isNotEqual (const SValuePtr &a, const SValuePtr &b)
	Equality comparison.

virtual SValuePtr	isUnsignedLessThan (const SValuePtr &a, const SValuePtr &b)
	Comparison for unsigned values.

virtual SValuePtr	isUnsignedLessThanOrEqual (const SValuePtr &a, const SValuePtr &b)
	Comparison for unsigned values.

virtual SValuePtr	isUnsignedGreaterThan (const SValuePtr &a, const SValuePtr &b)
	Comparison for unsigned values.

virtual SValuePtr	isUnsignedGreaterThanOrEqual (const SValuePtr &a, const SValuePtr &b)
	Comparison for unsigned values.

virtual SValuePtr	isSignedLessThan (const SValuePtr &a, const SValuePtr &b)
	Comparison for signed values.

virtual SValuePtr	isSignedLessThanOrEqual (const SValuePtr &a, const SValuePtr &b)
	Comparison for signed values.

virtual SValuePtr	isSignedGreaterThan (const SValuePtr &a, const SValuePtr &b)
	Comparison for signed values.

virtual SValuePtr	isSignedGreaterThanOrEqual (const SValuePtr &a, const SValuePtr &b)
	Comparison for signed values.

virtual SValuePtr	readRegister (RegisterDescriptor reg)
	Reads a value from a register.

SValuePtr	peekRegister (RegisterDescriptor reg)
	Obtain a register value without side effects.

Static Public Member Functions
static RiscOperatorsPtr	instanceFromRegisters (const RegisterDictionaryPtr &, const SmtSolverPtr &solver=SmtSolverPtr())
	Instantiates a new RiscOperators object and configures it to use semantic values and states that are defaults for SymbolicSemantics.

static RiscOperatorsPtr	instanceFromProtoval (const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
	Instantiates a new RiscOperators object with specified prototypical values.

static RiscOperatorsPtr	instanceFromState (const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr())
	Instantiates a new RiscOperators object with specified state.

static RiscOperatorsPtr	promote (const BaseSemantics::RiscOperatorsPtr &)
	Run-time promotion of a base RiscOperators pointer to symbolic operators.

static SgAsmFloatType *	sgIsIeee754 (SgAsmType *)
	Tests whether a SgAsmType is an IEEE-754 floating-point type.

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

Protected Member Functions
	RiscOperators (const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver)

	RiscOperators (const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver)

SValuePtr	svalueUndefined (size_t nbits)

SValuePtr	svalueBottom (size_t nbits)

SValuePtr	svalueUnspecified (size_t nbits)

SValuePtr	svalueNumber (size_t nbits, uint64_t value)

SValuePtr	svalueBoolean (bool b)

Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators
	RiscOperators (const SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())

	RiscOperators (const StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr())

Protected Attributes
bool	omit_cur_insn

DefinersMode	computingDefiners_

WritersMode	computingMemoryWriters_

WritersMode	computingRegisterWriters_

uint64_t	trimThreshold_

bool	reinterpretMemoryReads_

bool	reinterpretRegisterReads_

size_t	nTrimmed_ = 0

Member Typedef Documentation

◆ Super

using Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::Super = BaseSemantics::RiscOperators

Base type.

Definition at line 741 of file SymbolicSemantics.h.

◆ Ptr

using Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::Ptr = RiscOperatorsPtr

Shared-ownership pointer.

Definition at line 744 of file SymbolicSemantics.h.

Constructor & Destructor Documentation

◆ ~RiscOperators()

Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::~RiscOperators ( )

virtual

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Member Function Documentation

◆ instanceFromProtoval()

static RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::instanceFromProtoval	(	const BaseSemantics::SValuePtr &	protoval,
		const SmtSolverPtr &	solver = `SmtSolverPtr()`
	)

static

Instantiates a new RiscOperators object with specified prototypical values.

An SMT solver may be specified as the second argument for convenience. See solver for details.

◆ instanceFromState()

static RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::instanceFromState	(	const BaseSemantics::StatePtr &	,
		const SmtSolverPtr &	solver = `SmtSolverPtr()`
	)

static

Instantiates a new RiscOperators object with specified state.

An SMT solver may be specified as the second argument for convenience. See solver for details.

◆ create() [1/2]

virtual BaseSemantics::RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::create	(	const BaseSemantics::SValuePtr &	protoval,
		const SmtSolverPtr &	solver = `SmtSolverPtr()`
	)		const

overridevirtual

Virtual allocating constructor.

The protoval is a prototypical semantic value that is used as a factory to create additional values as necessary via its virtual constructors. The state upon which the RISC operations operate must be set by modifying the currentState property. An optional SMT solver may be specified (see solver).

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::LlvmSemantics::RiscOperators, Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators, and Rose::BinaryAnalysis::Partitioner2::Semantics::RiscOperators.

◆ create() [2/2]

virtual BaseSemantics::RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::create	(	const BaseSemantics::StatePtr &	state,
		const SmtSolverPtr &	solver = `SmtSolverPtr()`
	)		const

overridevirtual

Virtual allocating constructor.

The supplied state is that upon which the RISC operations operate and is also used to define the prototypical semantic value. Other states can be supplied by setting currentState. The prototypical semantic value is used as a factory to create additional values as necessary via its virtual constructors. An optional SMT solver may be specified (see solver).

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators, Rose::BinaryAnalysis::InstructionSemantics::LlvmSemantics::RiscOperators, and Rose::BinaryAnalysis::Partitioner2::Semantics::RiscOperators.

◆ promote()

static RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::promote ( const BaseSemantics::RiscOperatorsPtr & )

static

Run-time promotion of a base RiscOperators pointer to symbolic operators.

This is a checked conversion–it will fail if x does not point to a SymbolicSemantics::RiscOperators object.

◆ boolean_()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::boolean_ ( bool value )

overridevirtual

Returns a Boolean value.

Uses the prototypical value to virtually construct a new value.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

◆ number_()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::number_	(	size_t	nbits,
		uint64_t	value
	)

overridevirtual

Returns a number of the specified bit width.

Uses the prototypical value to virtually construct a new value.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

◆ computingDefiners() [1/2]

void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::computingDefiners ( DefinersMode m )

inline

Property: Track which instructions define a semantic value.

Each semantic value (SymbolicSemantics::SValue) is capable of storing a set of instruction addresses. This property controls how operations that produce new semantic values adjust those definers-sets in the new value.

TRACK_NO_DEFINERS: Each new semantic value will have a default-constructed definers-set (probably empty). Using this setting makes the definers-set available for other uses.

TRACK_LATEST_DEFINER: The new values will have the default-constructed definers-set unioned with the address of the current instruction (if there is a current instruction).

TRACK_ALL_DEFINERS: The new values will have a default-constructed definers-set unioned with the address of the current instruciton (if there is one), and the addresses of the definers-sets of the operands. Certain operations are able to simplify these sets. For example, an exclusive-or whose two operands are equal will return a zero result whose only definer is the current instruction.

Definition at line 856 of file SymbolicSemantics.h.

◆ computingDefiners() [2/2]

DefinersMode Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::computingDefiners ( ) const

inline

Property: Track which instructions define a semantic value.

Each semantic value (SymbolicSemantics::SValue) is capable of storing a set of instruction addresses. This property controls how operations that produce new semantic values adjust those definers-sets in the new value.

TRACK_NO_DEFINERS: Each new semantic value will have a default-constructed definers-set (probably empty). Using this setting makes the definers-set available for other uses.

TRACK_LATEST_DEFINER: The new values will have the default-constructed definers-set unioned with the address of the current instruction (if there is a current instruction).

TRACK_ALL_DEFINERS: The new values will have a default-constructed definers-set unioned with the address of the current instruciton (if there is one), and the addresses of the definers-sets of the operands. Certain operations are able to simplify these sets. For example, an exclusive-or whose two operands are equal will return a zero result whose only definer is the current instruction.

Definition at line 857 of file SymbolicSemantics.h.

◆ computingMemoryWriters() [1/2]

void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::computingMemoryWriters ( WritersMode m )

inline

Property: Track which instructions write to each memory location.

Each memory location stores a set of addresses that represent the instructions that wrote to that location. This property controls how each writeMemory operation updates that set.

TRACK_NO_WRITERS: Does not update the memory state's writers information. Using this setting will make that data structure available for other purposes. The data structure can store a set of addresses independently for each memory cell.

TRACK_LATEST_WRITER: Each write operation clobbers all previous write information for the affected memory address and stores the address of the current instruction (if there is one).

TRACK_ALL_WRITERS: Each write operation inserts the instruction address into the set of addresses stored for the affected memory cell without removing any addresses that are already associated with that cell. While this works well for analysis over a small region of code (like a single function), it might cause the writer sets to become very large when the same memory state is used over large regions (like a whole program).

Definition at line 878 of file SymbolicSemantics.h.

◆ computingMemoryWriters() [2/2]

WritersMode Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::computingMemoryWriters ( ) const

inline

Property: Track which instructions write to each memory location.

Each memory location stores a set of addresses that represent the instructions that wrote to that location. This property controls how each writeMemory operation updates that set.

TRACK_NO_WRITERS: Does not update the memory state's writers information. Using this setting will make that data structure available for other purposes. The data structure can store a set of addresses independently for each memory cell.

TRACK_LATEST_WRITER: Each write operation clobbers all previous write information for the affected memory address and stores the address of the current instruction (if there is one).

TRACK_ALL_WRITERS: Each write operation inserts the instruction address into the set of addresses stored for the affected memory cell without removing any addresses that are already associated with that cell. While this works well for analysis over a small region of code (like a single function), it might cause the writer sets to become very large when the same memory state is used over large regions (like a whole program).

Definition at line 879 of file SymbolicSemantics.h.

◆ computingRegisterWriters() [1/2]

void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::computingRegisterWriters ( WritersMode m )

inline

Property: Track latest writer to each register.

Controls whether each writeRegister operation updates the list of writers. The following values are allowed for this property:

TRACK_NO_WRITERS: Does not update the register state's writers information. Using this setting will make that data structure available for other purposes. The data structure can store a set of addresses independently for each bit of each register.

TRACK_LATEST_WRITER: Each write operation clobbers all previous write information for the affected register. This information is stored per bit so that if instruction 1 writes to EAX and then instruction 2 writes to AX then the high-order 16 bits of EAX will have {1} as the writer set while the low order bits will have {2} as its writer set.

TRACK_ALL_WRITERS: Each write operation inserts the instruction address into the set of addresses stored for the affected register (or register part) without removing any addresses that are already associated with that register. While this works well for analysis over a small region of code (like a single function), it might cause the writer sets to become very large when the same register state is used over large regions (like a whole program).

Definition at line 903 of file SymbolicSemantics.h.

◆ computingRegisterWriters() [2/2]

WritersMode Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::computingRegisterWriters ( ) const

inline

Property: Track latest writer to each register.

Controls whether each writeRegister operation updates the list of writers. The following values are allowed for this property:

TRACK_NO_WRITERS: Does not update the register state's writers information. Using this setting will make that data structure available for other purposes. The data structure can store a set of addresses independently for each bit of each register.

TRACK_LATEST_WRITER: Each write operation clobbers all previous write information for the affected register. This information is stored per bit so that if instruction 1 writes to EAX and then instruction 2 writes to AX then the high-order 16 bits of EAX will have {1} as the writer set while the low order bits will have {2} as its writer set.

TRACK_ALL_WRITERS: Each write operation inserts the instruction address into the set of addresses stored for the affected register (or register part) without removing any addresses that are already associated with that register. While this works well for analysis over a small region of code (like a single function), it might cause the writer sets to become very large when the same register state is used over large regions (like a whole program).

Definition at line 904 of file SymbolicSemantics.h.

◆ getset_omit_cur_insn()

bool Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::getset_omit_cur_insn ( bool b )

inline

Definition at line 908 of file SymbolicSemantics.h.

◆ trimThreshold() [1/2]

void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::trimThreshold ( uint64_t n )

inline

Property: Maximum size of expressions.

Symbolic expressions can get very large very quickly. This property controls how large a symbolic expression can grow before it's substituted with a new variable. The default, zero, means to never limit the size of expressions.

Definition at line 916 of file SymbolicSemantics.h.

◆ trimThreshold() [2/2]

uint64_t Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::trimThreshold ( ) const

inline

Property: Maximum size of expressions.

Symbolic expressions can get very large very quickly. This property controls how large a symbolic expression can grow before it's substituted with a new variable. The default, zero, means to never limit the size of expressions.

Definition at line 917 of file SymbolicSemantics.h.

◆ nTrimmed() [1/2]

size_t Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::nTrimmed ( ) const

inline

Property: Number of symbolic expressions trimmed.

Each time the trim threshold causes an expression to be replaced by a new variable, this property is incremented. The counter starts at zero when this object is created, but can be adjusted (usually back to zero) by the user.

Definition at line 926 of file SymbolicSemantics.h.

◆ nTrimmed() [2/2]

void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::nTrimmed ( size_t n )

inline

Property: Number of symbolic expressions trimmed.

Each time the trim threshold causes an expression to be replaced by a new variable, this property is incremented. The counter starts at zero when this object is created, but can be adjusted (usually back to zero) by the user.

Definition at line 927 of file SymbolicSemantics.h.

◆ reinterpretMemoryReads() [1/2]

bool Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::reinterpretMemoryReads ( ) const

inline

Property: Reinterpret data as unsigned integers when reading from memory or registers.

If this property is set, then a call to reinterpret is used to convert the return value to an unsigned integer if necessary. This property should normally be enabled because many of the older parts of ROSE assume that memory only contains integers.

Definition at line 937 of file SymbolicSemantics.h.

◆ reinterpretMemoryReads() [2/2]

void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::reinterpretMemoryReads ( bool b )

inline

Property: Reinterpret data as unsigned integers when reading from memory or registers.

If this property is set, then a call to reinterpret is used to convert the return value to an unsigned integer if necessary. This property should normally be enabled because many of the older parts of ROSE assume that memory only contains integers.

Definition at line 938 of file SymbolicSemantics.h.

◆ reinterpretRegisterReads() [1/2]

bool Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::reinterpretRegisterReads ( ) const

inline

Property: Reinterpret data as unsigned integers when reading from memory or registers.

If this property is set, then a call to reinterpret is used to convert the return value to an unsigned integer if necessary. This property should normally be enabled because many of the older parts of ROSE assume that memory only contains integers.

Definition at line 939 of file SymbolicSemantics.h.

◆ reinterpretRegisterReads() [2/2]

void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::reinterpretRegisterReads ( bool b )

inline

Property: Reinterpret data as unsigned integers when reading from memory or registers.

If this property is set, then a call to reinterpret is used to convert the return value to an unsigned integer if necessary. This property should normally be enabled because many of the older parts of ROSE assume that memory only contains integers.

Definition at line 940 of file SymbolicSemantics.h.

◆ substitute()

virtual void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::substitute	(	const SValuePtr &	from,
		const SValuePtr &	to
	)

virtual

Substitute all occurrences of from with to in the current state.

For instance, in functions that use a frame pointer set up with "push ebp; mov ebp, esp", it is convenient to see stack offsets in terms of the function's stack frame rather than in terms of the original esp value. This convenience comes from the fact that compilers tend to emit stack accessing code where the addresses are offsets from the function's stack frame.

For instance, after the "push ebp; mov ebp, esp" prologue, the machine state is:

registers:
  esp    = (add[32] esp_0[32] -4[32])
  ebp    = (add[32] esp_0[32] -4[32])
  eip    = 0x080480a3[32]
memory:
  addr=(add[32] esp_0[32] -1[32]) value=(extract[8] 24[32] 32[32] ebp_0[32])
  addr=(add[32] esp_0[32] -2[32]) value=(extract[8] 16[32] 24[32] ebp_0[32])
  addr=(add[32] esp_0[32] -3[32]) value=(extract[8] 8[32] 16[32] ebp_0[32])
  addr=(add[32] esp_0[32] -4[32]) value=(extract[8] 0[32] 8[32] ebp_0[32])

If we create a new variable called "stack_frame" where

stack_frame = esp_0 - 4

Solving for esp_0:

esp_0 = stack_frame + 4

Then replacing the lhs (esp_0) with the rhs (stack_frame + 4) in the machine state causes the expressions to be rewritten in terms of stack_frame instead of esp_0:

registers:
  esp    = stack_frame[32]
  ebp    = stack_frame[32]
  eip    = 0x080480a3[32]
memory:
  addr=(add[32] stack_frame[32] 3[32]) value=(extract[8] 24[32] 32[32] ebp_0[32])
  addr=(add[32] stack_frame[32] 2[32]) value=(extract[8] 16[32] 24[32] ebp_0[32])
  addr=(add[32] stack_frame[32] 1[32]) value=(extract[8] 8[32] 16[32] ebp_0[32])
  addr=stack_frame[32] value=(extract[8] 0[32] 8[32] ebp_0[32])

Here's the source code for that substitution:

SymbolicSemantics::RiscOperatorsPtr operators = ...;
SymbolicSemantics::SValuePtr original_esp = ...; //probably read from the initial state
BaseSemantics::SValuePtr stack_frame = operators->undefined_(32);
stack_frame->comment("stack_frame"); //just so output looks nice
SymbolicSemantics::SValuePtr rhs = SymbolicSemantics::SValue::promote(
    operators->add(stack_frame, operators->number_(32, 4))
);
 
std::cerr <<"Prior to state:\n" <<*operators;
operators->substitute(original_esp, rhs);
std::cerr <<"Substituted state:\n" <<*operators;

◆ filterResult()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::filterResult ( const BaseSemantics::SValuePtr & )

virtual

Filters results from RISC operators.

Checks that the size of the specified expression doesn't exceed the trimThreshold. If not (or the threshold is zero), returns the argument, otherwise returns a new variable.

◆ sgIsIeee754()

static SgAsmFloatType * Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::sgIsIeee754 ( SgAsmType * )

static

Tests whether a SgAsmType is an IEEE-754 floating-point type.

If the argument is an IEEE-754 floating-point type then returns the argument dynamically cast to a SgAsmFloatType, otherwise returns NULL. Not all SgAsmFloatType objects are IEEE-754 floating-point types.

◆ sgTypeToSymbolicType()

virtual SymbolicExpression::Type Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::sgTypeToSymbolicType ( SgAsmType * )

virtual

Convert a SgAsmType to a symbolic type.

If the SgAsmType cannot be converted to a SymbolicExpression::Type then throws Exception.

◆ interrupt()

virtual void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::interrupt	(	int	majorNumber,
		int	minorNumber
	)

overridevirtual

Unconditionally raise an interrupt.

The major and minor numbers are architecture specific. For instance, an x86 INT instruction uses major number zero and the minor number is the interrupt number (e.g., 0x80 for Linux system calls), while an x86 SYSENTER instruction uses major number one.

The base implementation does one of two things. If the current state has an interrupt sub-state then the specified interrupt is raised in that state by setting that interrupt to true. Otherwise, the base implementation does nothing.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

◆ and_()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::and_	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b
	)

overridevirtual

Computes bit-wise AND of two values.

The operands must both have the same width; the result must be the same width as the operands.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ or_()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::or_	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b
	)

overridevirtual

Computes bit-wise OR of two values.

The operands a and b must have the same width; the return value width will be the same as a and b.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ xor_()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::xor_	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b
	)

overridevirtual

Computes bit-wise XOR of two values.

The operands a and b must have the same width; the result will be the same width as a and b.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ invert()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::invert ( const BaseSemantics::SValuePtr & a )

overridevirtual

One's complement.

The result will be the same size as the operand.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ extract()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::extract	(	const BaseSemantics::SValuePtr &	a,
		size_t	begin_bit,
		size_t	end_bit
	)

overridevirtual

Extracts bits from a value.

The specified bits from begin_bit (inclusive) through end_bit (exclusive) are copied into the low-order bits of the return value (other bits in the return value are cleared). The least significant bit is number zero. The begin_bit and end_bit values must be valid for the width of a.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ concat()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::concat	(	const BaseSemantics::SValuePtr &	lowBits,
		const BaseSemantics::SValuePtr &	highBits
	)

overridevirtual

Concatenates the bits of two values.

The bits of lowBits and highBits are concatenated so that the result has lowBits in the low-order bits and highBits in the high order bits. The width of the return value is the sum of the widths of lowBits and highBits.

Note that the order of arguments for this method is the reverse of the SymbolicExpression concatenation function.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ leastSignificantSetBit()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::leastSignificantSetBit ( const BaseSemantics::SValuePtr & a )

overridevirtual

Returns position of least significant set bit; zero when no bits are set.

The return value will have the same width as the operand, although this can be safely truncated to the log-base-2 + 1 width.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ mostSignificantSetBit()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::mostSignificantSetBit ( const BaseSemantics::SValuePtr & a )

overridevirtual

Returns position of most significant set bit; zero when no bits are set.

The return value will have the same width as the operand, although this can be safely truncated to the log-base-2 + 1 width.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ rotateLeft()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::rotateLeft	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	nbits
	)

overridevirtual

Rotate bits to the left.

The return value will have the same width as operand a. The nbits is interpreted as unsigned. The behavior is modulo the width of a regardless of whether the implementation makes that a special case or handles it naturally.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ rotateRight()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::rotateRight	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	nbits
	)

overridevirtual

Rotate bits to the right.

The return value will have the same width as operand a. The nbits is interpreted as unsigned. The behavior is modulo the width of a regardless of whether the implementation makes that a special case or handles it naturally.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ shiftLeft()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::shiftLeft	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	nbits
	)

overridevirtual

Returns arg shifted left.

The return value will have the same width as operand a. The nbits is interpreted as unsigned. New bits shifted into the value are zero. If nbits is equal to or larger than the width of a then the result is zero.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ shiftRight()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::shiftRight	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	nbits
	)

overridevirtual

Returns arg shifted right logically (no sign bit).

The return value will have the same width as operand a. The nbits is interpreted as unsigned. New bits shifted into the value are zero. If nbits is equal to or larger than the width of a then the result is zero.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ shiftRightArithmetic()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::shiftRightArithmetic	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	nbits
	)

overridevirtual

Returns arg shifted right arithmetically (with sign bit).

The return value will have the same width as operand a. The nbits is interpreted as unsigned. New bits shifted into the value are the same as the most significant bit (the "sign bit"). If nbits is equal to or larger than the width of a then the result has all bits cleared or all bits set depending on whether the most significant bit was originally clear or set.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ equalToZero()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::equalToZero ( const BaseSemantics::SValuePtr & a )

overridevirtual

Determines whether a value is equal to zero.

Returns true, false, or undefined (in the semantic domain) depending on whether argument is zero.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ iteWithStatus()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::iteWithStatus	(	const BaseSemantics::SValuePtr &	cond,
		const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b,
		IteStatus &	status
	)

overridevirtual

If-then-else with status.

Returns operand a if cond is true, operand b if cond is false, or some other value if the condition is unknown. The condition must be one bit wide; the widths of a and b must be equal; the return value width will be the same as a and b.

The status is an output that indicates how the main return value was determined.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ unsignedExtend()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::unsignedExtend	(	const BaseSemantics::SValuePtr &	a,
		size_t	new_width
	)

overridevirtual

Extend (or shrink) operand a so it is nbits wide by adding or removing high-order bits.

Added bits are always zeros. The result will be the specified new_width.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ signExtend()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::signExtend	(	const BaseSemantics::SValuePtr &	a,
		size_t	new_width
	)

overridevirtual

Sign extends a value.

The result will be the specified new_width, which must be at least as large as the original width.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ add()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::add	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b
	)

overridevirtual

Adds two integers of equal size.

The width of a and b must be equal; the return value will have the same width as a and b.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ addWithCarries()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::addWithCarries	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b,
		const BaseSemantics::SValuePtr &	c,
		BaseSemantics::SValuePtr &	carry_out
	)

overridevirtual

Add two values of equal size and a carry bit.

Carry information is returned via carry_out argument. The carry_out value is the tick marks that are written above the first addend when doing long arithmetic like a 2nd grader would do (of course, they'd probably be adding two base-10 numbers). For instance, when adding 00110110 and 11100100:

 '''..'..         <-- carry tick marks: '=carry .=no carry
  00110110
+ 11100100
----------
 100011010

The carry_out value is 11100100.

The width of a and b must be equal; c must have a width of one bit; the return value and carry_out will be the same width as a and b. The carry_out value is allocated herein.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ negate()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::negate ( const BaseSemantics::SValuePtr & a )

overridevirtual

Two's complement.

The return value will have the same width as the operand.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ signedDivide()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::signedDivide	(	const BaseSemantics::SValuePtr &	dividend,
		const BaseSemantics::SValuePtr &	divisor
	)

overridevirtual

Divides two signed values.

The width of the result will be the same as the width of the dividend.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ signedModulo()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::signedModulo	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b
	)

overridevirtual

Calculates modulo with signed values.

The width of the result will be the same as the width of operand b.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ signedMultiply()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::signedMultiply	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b
	)

overridevirtual

Multiplies two signed values.

The width of the result will be the sum of the widths of a and b.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ unsignedDivide()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::unsignedDivide	(	const BaseSemantics::SValuePtr &	dividend,
		const BaseSemantics::SValuePtr &	divisor
	)

overridevirtual

Divides two unsigned values.

The width of the result is the same as the width of the dividend.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ unsignedModulo()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::unsignedModulo	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b
	)

overridevirtual

Calculates modulo with unsigned values.

The width of the result is the same as the width of operand b.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ unsignedMultiply()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::unsignedMultiply	(	const BaseSemantics::SValuePtr &	a,
		const BaseSemantics::SValuePtr &	b
	)

overridevirtual

Multiply two unsigned values.

The width of the result is the sum of the widths of a and b.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ fpConvert()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::fpConvert	(	const BaseSemantics::SValuePtr &	a,
		SgAsmFloatType *	aType,
		SgAsmFloatType *	retType
	)

overridevirtual

Convert from one floating-point type to another.

Converts the floating-point value a having type aType to the return value having retType.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ reinterpret()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::reinterpret	(	const BaseSemantics::SValuePtr &	a,
		SgAsmType *	retType
	)

overridevirtual

Reinterpret an expression as a different type.

For semantic domains whose values don't carry type information this is a no-op. For other domains, this creates a new value having the same bits as the original value but a new type. The old and new types must be the same size. This is similar to a C++ reinterpret_cast.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators.

◆ readRegister()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::readRegister	(	RegisterDescriptor	reg,
		const BaseSemantics::SValuePtr &	dflt
	)

overridevirtual

Reads a value from a register.

The base implementation simply delegates to the current semantic State, which probably delegates to a register state, but subclasses are welcome to override this behavior at any level.

A register state will typically implement storage for hardware registers, but higher layers (the State, RiscOperators, Dispatcher, ...) should not be concerned about the size of the register they're trying to read. For example, a register state for a 32-bit x86 architecture will likely have a storage location for the 32-bit EAX register, but it should be possible to ask readRegister to return the value of AX (the low-order 16-bits). In order to accomplish this, some level of the readRegister delegations needs to invoke extract to obtain the low 16 bits. The RiscOperators object is passed along the delegation path for this purpose. The inverse concat operation will be needed at some level when we ask readRegister to return a value that comes from multiple storage locations in the register state (such as can happen if an x86 register state holds individual status flags and we ask for the 32-bit EFLAGS register).

If the register state can distinguish between a register that has never been accessed and a register that has only been read, then the dflt value is stored into the register the first time it's read. This ensures that reading the register a second time with no intervening write will return the same value as the first read. If a dflt is not provided then one is constructed by invoking undefined_.

There needs to be a certain level of cooperation between the RiscOperators, State, and register state classes to decide which layer should invoke the extract or concat (or whatever other RISC operations might be necessary).

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

◆ peekRegister()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::peekRegister	(	RegisterDescriptor	,
		const BaseSemantics::SValuePtr &	dflt
	)

overridevirtual

Obtain a register value without side effects.

This is a lower-level operation than readRegister in that it doesn't cause the register to be marked as having been read. It is typically used in situations where the register is being accessed for analysis purposes rather than as part of an instruction emulation.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

◆ writeRegister()

virtual void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::writeRegister	(	RegisterDescriptor	reg,
		const BaseSemantics::SValuePtr &	a
	)

overridevirtual

Writes a value to a register.

The base implementation simply delegates to the current semantic State, which probably delegates to a register state, but subclasses are welcome to override this behavior at any level.

As with readRegister, writeRegister may need to perform various RISC operations in order to accomplish the task of writing a value to the specified register when the underlying register state doesn't actually store a value for that specific register. The RiscOperations object is passed along for that purpose. See readRegister for more details.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

◆ readMemory()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::readMemory	(	RegisterDescriptor	segreg,
		const BaseSemantics::SValuePtr &	addr,
		const BaseSemantics::SValuePtr &	dflt,
		const BaseSemantics::SValuePtr &	cond
	)

overridevirtual

Reads a value from memory.

The implementation (in subclasses) will typically delegate much of the work to the current state's readMemory method.

A MemoryState will implement storage for memory locations and might impose certain restrictions, such as "all memory values must be eight bits". However, the readMemory should not have these constraints so that it can be called from a variety of Dispatcher subclass (e.g., the DispatcherX86 class assumes that readMemory is capable of reading 32-bit values from little-endian memory). The designers of the MemoryState, State, and RiscOperators should collaborate to decide which layer (RiscOperators, State, or MemoryState) is reponsible for combining individual memory locations into larger values. A RiscOperators object is passed along the chain of delegations for this purpose. The RiscOperators might also contain other data that's important during the process, such as an SMT solver.

The segreg argument is an optional segment register. Most architectures have a flat virtual address space and will pass a default-constructed register descriptor whose is_valid() method returns false.

The cond argument is a Boolean value that indicates whether this is a true read operation. If cond can be proven to be false then the read is a no-op and returns an arbitrary value.

The dflt argument determines the size of the value to be read. This argument is also passed along to the lower layers so that they can, if they desire, use it to initialize memory that has never been read or written before.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::LlvmSemantics::RiscOperators.

◆ peekMemory()

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::peekMemory	(	RegisterDescriptor	segreg,
		const BaseSemantics::SValuePtr &	addr,
		const BaseSemantics::SValuePtr &	dflt
	)

overridevirtual

Read memory without side effects.

This is a lower-level operation than readMemory in that it doesn't cause any side effects in the memory state. In all other respects, it's similar to readMemory.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

◆ writeMemory()

virtual void Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::writeMemory	(	RegisterDescriptor	segreg,
		const BaseSemantics::SValuePtr &	addr,
		const BaseSemantics::SValuePtr &	data,
		const BaseSemantics::SValuePtr &	cond
	)

overridevirtual

Writes a value to memory.

The implementation (in subclasses) will typically delegate much of the work to the current state's writeMemory method.

The segreg argument is an optional segment register. Most architectures have a flat virtual address space and will pass a default-constructed register descriptor whose is_valid() method returns false.

The cond argument is a Boolean value that indicates whether this is a true write operation. If cond can be proved to be false then writeMemory is a no-op.

Implements Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::InstructionSemantics::LlvmSemantics::RiscOperators.

Member Data Documentation

◆ omit_cur_insn

bool Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::omit_cur_insn

protected

Definition at line 747 of file SymbolicSemantics.h.

◆ computingDefiners_

DefinersMode Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::computingDefiners_

protected

Definition at line 748 of file SymbolicSemantics.h.

◆ computingMemoryWriters_

WritersMode Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::computingMemoryWriters_

protected

Definition at line 749 of file SymbolicSemantics.h.

◆ computingRegisterWriters_

WritersMode Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::computingRegisterWriters_

protected

Definition at line 750 of file SymbolicSemantics.h.

◆ trimThreshold_

uint64_t Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::trimThreshold_

protected

Definition at line 751 of file SymbolicSemantics.h.

◆ reinterpretMemoryReads_

bool Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::reinterpretMemoryReads_

protected

Definition at line 752 of file SymbolicSemantics.h.

◆ reinterpretRegisterReads_

bool Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::reinterpretRegisterReads_

protected

Definition at line 753 of file SymbolicSemantics.h.

◆ nTrimmed_

size_t Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators::nTrimmed_ = 0

protected

Definition at line 754 of file SymbolicSemantics.h.

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

SymbolicSemantics.h

Description

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Member Typedef Documentation

◆ Super

◆ Ptr

Constructor & Destructor Documentation

◆ ~RiscOperators()

Member Function Documentation

◆ instanceFromProtoval()

◆ instanceFromState()

◆ create() [1/2]

◆ create() [2/2]

◆ promote()

◆ boolean_()

◆ number_()

◆ computingDefiners() [1/2]

◆ computingDefiners() [2/2]

◆ computingMemoryWriters() [1/2]

◆ computingMemoryWriters() [2/2]

◆ computingRegisterWriters() [1/2]

◆ computingRegisterWriters() [2/2]

◆ getset_omit_cur_insn()

◆ trimThreshold() [1/2]

◆ trimThreshold() [2/2]

◆ nTrimmed() [1/2]

◆ nTrimmed() [2/2]

◆ reinterpretMemoryReads() [1/2]

◆ reinterpretMemoryReads() [2/2]

◆ reinterpretRegisterReads() [1/2]

◆ reinterpretRegisterReads() [2/2]

◆ substitute()

◆ filterResult()

◆ sgIsIeee754()

◆ sgTypeToSymbolicType()

◆ interrupt()

◆ and_()

◆ or_()

◆ xor_()

◆ invert()

◆ extract()

◆ concat()

◆ leastSignificantSetBit()

◆ mostSignificantSetBit()

◆ rotateLeft()

◆ rotateRight()

◆ shiftLeft()

◆ shiftRight()

◆ shiftRightArithmetic()

◆ equalToZero()

◆ iteWithStatus()

◆ unsignedExtend()

◆ signExtend()

◆ add()

◆ addWithCarries()

◆ negate()

◆ signedDivide()

◆ signedModulo()

◆ signedMultiply()

◆ unsignedDivide()

◆ unsignedModulo()

◆ unsignedMultiply()

◆ fpConvert()

◆ reinterpret()

◆ readRegister()

◆ peekRegister()

◆ writeRegister()

◆ readMemory()

◆ peekMemory()

◆ writeMemory()

Member Data Documentation

◆ omit_cur_insn

◆ computingDefiners_

◆ computingMemoryWriters_

◆ computingRegisterWriters_

◆ trimThreshold_

◆ reinterpretMemoryReads_