ROSE 0.11.145.192
|
Defines RISC operators for the TaintSemantics domain.
These RISC operators depend on functionality introduced into the SValue class hierarchy at the TaintSemantics::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 TaintSemantics::SValue.
Each RISC operator should return a newly allocated semantic value so that the caller can adjust taintedness for the result without affecting any of the inputs. For example, a no-op that returns its argument should be implemented like this:
Definition at line 231 of file TaintSemantics.h.
#include <Rose/BinaryAnalysis/InstructionSemantics/TaintSemantics.h>
Public Types | |
using | Super = SymbolicSemantics::RiscOperators |
Base type. | |
using | Ptr = RiscOperatorsPtr |
Shared-ownership pointer. | |
Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators | |
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 | 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. | |
Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators | |
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 | 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 TaintSemantics. | |
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 Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators | |
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 &) | |
RiscOperators (const BaseSemantics::StatePtr &, const SmtSolverPtr &) | |
Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators | |
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()) | |
Additional Inherited Members | |
Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators | |
bool | omit_cur_insn |
DefinersMode | computingDefiners_ |
WritersMode | computingMemoryWriters_ |
WritersMode | computingRegisterWriters_ |
uint64_t | trimThreshold_ |
bool | reinterpretMemoryReads_ |
bool | reinterpretRegisterReads_ |
size_t | nTrimmed_ = 0 |
using Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators::Super = SymbolicSemantics::RiscOperators |
Base type.
Definition at line 234 of file TaintSemantics.h.
using Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators::Ptr = RiscOperatorsPtr |
Shared-ownership pointer.
Definition at line 237 of file TaintSemantics.h.
|
virtual |
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
|
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.
|
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).
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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).
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
overridevirtual |
One's complement.
The result will be the same size as the operand.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
overridevirtual |
Determines whether a value is equal to zero.
Returns true, false, or undefined (in the semantic domain) depending on whether argument is zero.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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::SymbolicSemantics::RiscOperators.
|
overridevirtual |
Sign extends a value.
The result will be the specified new_width
, which must be at least as large as the original width.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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:
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.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
overridevirtual |
Two's complement.
The return value will have the same width as the operand.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
overridevirtual |
Divides two signed values.
The width of the result will be the same as the width of the dividend
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
overridevirtual |
Calculates modulo with signed values.
The width of the result will be the same as the width of operand b
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
overridevirtual |
Multiplies two signed values.
The width of the result will be the sum of the widths of a
and b
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
overridevirtual |
Divides two unsigned values.
The width of the result is the same as the width of the dividend
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
overridevirtual |
Calculates modulo with unsigned values.
The width of the result is the same as the width of operand b
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
overridevirtual |
Multiply two unsigned values.
The width of the result is the sum of the widths of a
and b
.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::RiscOperators.
|
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::SymbolicSemantics::RiscOperators.
|
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::SymbolicSemantics::RiscOperators.