ROSE  0.11.51.0
Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | List of all members
Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators Class Reference

Description

RISC operators for model checking.

Definition at line 276 of file P2Model.h.

#include <P2Model.h>

Inheritance diagram for Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators:
Inheritance graph
[legend]
Collaboration diagram for Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators:
Collaboration graph
[legend]

Public Types

using Super = InstructionSemantics2::SymbolicSemantics::RiscOperators
 
using Ptr = RiscOperatorsPtr
 
- Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators
using Super = BaseSemantics::RiscOperators
 Base type. More...
 
using Ptr = RiscOperatorsPtr
 Shared-ownership pointer. More...
 
- Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators
using Ptr = RiscOperatorsPtr
 Shared-ownership pointer for a RiscOperators object. More...
 

Public Member Functions

virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr create (const InstructionSemantics2::BaseSemantics::SValuePtr &, const SmtSolverPtr &) const override
 Virtual allocating constructor. More...
 
virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr create (const InstructionSemantics2::BaseSemantics::StatePtr &, const SmtSolverPtr &) const override
 Virtual allocating constructor. More...
 
const Partitioner2::Partitionerpartitioner () const
 Property: Partitioner. More...
 
void checkNullAccess (const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, IoMode)
 Test whether the specified address is considered to be null. More...
 
void checkOobAccess (const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, IoMode, size_t nBytes)
 Test whether the specified address is out of bounds for variables. More...
 
void pushCallStack (const Partitioner2::FunctionPtr &callee, rose_addr_t initialSp)
 Push a function onto the call stack. More...
 
size_t pruneCallStack ()
 Remove old call stack entries. More...
 
void printCallStack (std::ostream &)
 Print information about the function call stack. More...
 
virtual void startInstruction (SgAsmInstruction *) override
 Called at the beginning of every instruction. More...
 
virtual void finishInstruction (SgAsmInstruction *) override
 Called at the end of every instruction. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr number_ (size_t nBits, uint64_t value) override
 Returns a number of the specified bit width. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr extract (const InstructionSemantics2::BaseSemantics::SValuePtr &, size_t begin, size_t end) override
 Extracts bits from a value. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr concat (const InstructionSemantics2::BaseSemantics::SValuePtr &lowBits, const InstructionSemantics2::BaseSemantics::SValuePtr &highBits) override
 Concatenates the bits of two values. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr shiftLeft (const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override
 Returns arg shifted left. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr shiftRight (const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override
 Returns arg shifted right logically (no sign bit). More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr shiftRightArithmetic (const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override
 Returns arg shifted right arithmetically (with sign bit). More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr unsignedExtend (const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override
 Extend (or shrink) operand a so it is nbits wide by adding or removing high-order bits. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr signExtend (const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override
 Sign extends a value. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr add (const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b) override
 Adds two integers of equal size. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr addCarry (const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b, InstructionSemantics2::BaseSemantics::SValuePtr &carryOut, InstructionSemantics2::BaseSemantics::SValuePtr &overflowed) override
 Adds two integers of equal size and carry. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr subtract (const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b) override
 Subtract one value from another. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr subtractCarry (const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b, InstructionSemantics2::BaseSemantics::SValuePtr &carryOut, InstructionSemantics2::BaseSemantics::SValuePtr &overflowed) override
 Subtract one value from another and carry. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr addWithCarries (const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b, const InstructionSemantics2::BaseSemantics::SValuePtr &c, InstructionSemantics2::BaseSemantics::SValuePtr &carryOut) override
 Add two values of equal size and a carry bit. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr readRegister (RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr &) override
 Reads a value from a register. More...
 
virtual void writeRegister (RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr &) override
 Writes a value to a register. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr readMemory (RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr, const InstructionSemantics2::BaseSemantics::SValuePtr &dflt, const InstructionSemantics2::BaseSemantics::SValuePtr &cond) override
 Reads a value from memory. More...
 
virtual void writeMemory (RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr, const InstructionSemantics2::BaseSemantics::SValuePtr &value, const InstructionSemantics2::BaseSemantics::SValuePtr &cond) override
 Writes a value to memory. More...
 
SmtSolver::Ptr modelCheckerSolver () const
 Property: Model checker SMT solver. More...
 
void modelCheckerSolver (const SmtSolver::Ptr &)
 Property: Model checker SMT solver. More...
 
bool computeMemoryRegions () const
 Property: Compute memory regions for variables. More...
 
void computeMemoryRegions (bool)
 Property: Compute memory regions for variables. More...
 
size_t nInstructions () const
 Property: Number of instructions executed. More...
 
void nInstructions (size_t)
 Property: Number of instructions executed. More...
 
InstructionSemantics2::BaseSemantics::SValuePtr assignRegion (const InstructionSemantics2::BaseSemantics::SValuePtr &result)
 Assign a region to an expression. More...
 
InstructionSemantics2::BaseSemantics::SValuePtr assignRegion (const InstructionSemantics2::BaseSemantics::SValuePtr &result, const InstructionSemantics2::BaseSemantics::SValuePtr &a)
 Assign a region to an expression. More...
 
InstructionSemantics2::BaseSemantics::SValuePtr assignRegion (const InstructionSemantics2::BaseSemantics::SValuePtr &result, const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b)
 Assign a region to an expression. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators
virtual BaseSemantics::SValuePtr boolean_ (bool b) ROSE_OVERRIDE
 Returns a Boolean value. More...
 
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. More...
 
virtual BaseSemantics::SValuePtr filterResult (const BaseSemantics::SValuePtr &)
 Filters results from RISC operators. More...
 
virtual SymbolicExpr::Type sgTypeToSymbolicType (SgAsmType *)
 Convert a SgAsmType to a symbolic type. More...
 
virtual void interrupt (int majr, int minr) ROSE_OVERRIDE
 Invoked for instructions that cause an interrupt. More...
 
virtual BaseSemantics::SValuePtr and_ (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 Computes bit-wise AND of two values. More...
 
virtual BaseSemantics::SValuePtr or_ (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 Computes bit-wise OR of two values. More...
 
virtual BaseSemantics::SValuePtr xor_ (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 Computes bit-wise XOR of two values. More...
 
virtual BaseSemantics::SValuePtr invert (const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 One's complement. More...
 
virtual BaseSemantics::SValuePtr leastSignificantSetBit (const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 Returns position of least significant set bit; zero when no bits are set. More...
 
virtual BaseSemantics::SValuePtr mostSignificantSetBit (const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 Returns position of most significant set bit; zero when no bits are set. More...
 
virtual BaseSemantics::SValuePtr rotateLeft (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
 Rotate bits to the left. More...
 
virtual BaseSemantics::SValuePtr rotateRight (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
 Rotate bits to the right. More...
 
virtual BaseSemantics::SValuePtr equalToZero (const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 Determines whether a value is equal to zero. More...
 
virtual BaseSemantics::SValuePtr ite (const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 If-then-else. More...
 
virtual BaseSemantics::SValuePtr negate (const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 Two's complement. More...
 
virtual BaseSemantics::SValuePtr signedDivide (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 Divides two signed values. More...
 
virtual BaseSemantics::SValuePtr signedModulo (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 Calculates modulo with signed values. More...
 
virtual BaseSemantics::SValuePtr signedMultiply (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 Multiplies two signed values. More...
 
virtual BaseSemantics::SValuePtr unsignedDivide (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 Divides two unsigned values. More...
 
virtual BaseSemantics::SValuePtr unsignedModulo (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 Calculates modulo with unsigned values. More...
 
virtual BaseSemantics::SValuePtr unsignedMultiply (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 Multiply two unsigned values. More...
 
virtual BaseSemantics::SValuePtr fpConvert (const BaseSemantics::SValuePtr &a, SgAsmFloatType *aType, SgAsmFloatType *retType) ROSE_OVERRIDE
 Convert from one floating-point type to another. More...
 
virtual BaseSemantics::SValuePtr reinterpret (const BaseSemantics::SValuePtr &, SgAsmType *) ROSE_OVERRIDE
 Reinterpret an expression as a different type. More...
 
virtual BaseSemantics::SValuePtr peekRegister (RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
 Obtain a register value without side effects. More...
 
virtual BaseSemantics::SValuePtr peekMemory (RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
 Read memory without side effects. More...
 
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. More...
 
DefinersMode computingDefiners () const
 Property: Track which instructions define a semantic value. More...
 
void computingMemoryWriters (WritersMode m)
 Property: Track which instructions write to each memory location. More...
 
WritersMode computingMemoryWriters () const
 Property: Track which instructions write to each memory location. More...
 
void computingRegisterWriters (WritersMode m)
 Property: Track latest writer to each register. More...
 
WritersMode computingRegisterWriters () const
 Property: Track latest writer to each register. More...
 
void trimThreshold (size_t n)
 Property: Maximum size of expressions. More...
 
size_t trimThreshold () const
 Property: Maximum size of expressions. More...
 
bool reinterpretMemoryReads () const
 Property: Reinterpret data as unsigned integers when reading from memory or registers. More...
 
void reinterpretMemoryReads (bool b)
 Property: Reinterpret data as unsigned integers when reading from memory or registers. More...
 
bool reinterpretRegisterReads () const
 Property: Reinterpret data as unsigned integers when reading from memory or registers. More...
 
void reinterpretRegisterReads (bool b)
 Property: Reinterpret data as unsigned integers when reading from memory or registers. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators
virtual SValuePtr protoval () const
 Property: Prototypical semantic value. More...
 
virtual void hash (Combinatorics::Hasher &)
 Compute hash of current state. More...
 
virtual SValuePtr bottom_ (size_t nbits)
 Returns a data-flow bottom value. More...
 
virtual SValuePtr filterCallTarget (const SValuePtr &a)
 Invoked to filter call targets. More...
 
virtual SValuePtr filterReturnTarget (const SValuePtr &a)
 Invoked to filter return targets. More...
 
virtual SValuePtr filterIndirectJumpTarget (const SValuePtr &a)
 Invoked to filter indirect jumps. More...
 
virtual void hlt ()
 Invoked for the x86 HLT instruction. More...
 
virtual void cpuid ()
 Invoked for the x86 CPUID instruction. More...
 
virtual SValuePtr rdtsc ()
 Invoked for the x86 RDTSC instruction. More...
 
virtual std::pair< SValuePtr, SValuePtrsplit (const SValuePtr &a, size_t splitPoint)
 Split a value into two narrower values. More...
 
virtual SValuePtr countLeadingZeros (const SValuePtr &a)
 Count leading zero bits. More...
 
virtual SValuePtr countLeadingOnes (const SValuePtr &a)
 Count leading one bits. More...
 
virtual SValuePtr reverseElmts (const SValuePtr &a, size_t elmtNBits)
 Reverse parts of a value. More...
 
virtual void interrupt (const SValuePtr &majr, const SValuePtr &minr, const SValuePtr &enabled)
 Invoked for instructions that cause an interrupt. More...
 
virtual SValuePtr fpFromInteger (const SValuePtr &intValue, SgAsmFloatType *fpType)
 Construct a floating-point value from an integer value. More...
 
virtual SValuePtr fpToInteger (const SValuePtr &fpValue, SgAsmFloatType *fpType, const SValuePtr &dflt)
 Construct an integer value from a floating-point value. More...
 
virtual SValuePtr fpIsNan (const SValuePtr &fpValue, SgAsmFloatType *fpType)
 Whether a floating-point value is a special not-a-number bit pattern. More...
 
virtual SValuePtr fpIsDenormalized (const SValuePtr &fpValue, SgAsmFloatType *fpType)
 Whether a floating-point value is denormalized. More...
 
virtual SValuePtr fpIsZero (const SValuePtr &fpValue, SgAsmFloatType *fpType)
 Whether a floating-point value is equal to zero. More...
 
virtual SValuePtr fpIsInfinity (const SValuePtr &fpValue, SgAsmFloatType *fpType)
 Whether a floating-point value is infinity. More...
 
virtual SValuePtr fpSign (const SValuePtr &fpValue, SgAsmFloatType *fpType)
 Sign of floating-point value. More...
 
virtual SValuePtr fpEffectiveExponent (const SValuePtr &fpValue, SgAsmFloatType *fpType)
 Exponent of floating-point value. More...
 
virtual SValuePtr fpAdd (const SValuePtr &a, const SValuePtr &b, SgAsmFloatType *fpType)
 Add two floating-point values. More...
 
virtual SValuePtr fpSubtract (const SValuePtr &a, const SValuePtr &b, SgAsmFloatType *fpType)
 Subtract one floating-point value from another. More...
 
virtual SValuePtr fpMultiply (const SValuePtr &a, const SValuePtr &b, SgAsmFloatType *fpType)
 Multiply two floating-point values. More...
 
virtual SValuePtr fpDivide (const SValuePtr &a, const SValuePtr &b, SgAsmFloatType *fpType)
 Divide one floating-point value by another. More...
 
virtual SValuePtr fpSquareRoot (const SValuePtr &a, SgAsmFloatType *fpType)
 Square root. More...
 
virtual SValuePtr fpRoundTowardZero (const SValuePtr &a, SgAsmFloatType *fpType)
 Round toward zero. More...
 
virtual SValuePtr convert (const SValuePtr &a, SgAsmType *srcType, SgAsmType *dstType)
 Convert value from one type to another. More...
 
virtual SmtSolverPtr solver () const
 Property: Satisfiability module theory (SMT) solver. More...
 
virtual void solver (const SmtSolverPtr &s)
 Property: Satisfiability module theory (SMT) solver. More...
 
const HotPatchhotPatch () const
 Property: Post-instruction hot patches. More...
 
HotPatchhotPatch ()
 Property: Post-instruction hot patches. More...
 
void hotPatch (const HotPatch &hp)
 Property: Post-instruction hot patches. More...
 
virtual StatePtr currentState () const
 Property: Current semantic state. More...
 
virtual void currentState (const StatePtr &s)
 Property: Current semantic state. More...
 
virtual StatePtr initialState () const
 Property: Optional lazily updated initial state. More...
 
virtual void initialState (const StatePtr &s)
 Property: Optional lazily updated initial state. More...
 
virtual const std::string & name () const
 Property: Name used for debugging. More...
 
virtual void name (const std::string &s)
 Property: Name used for debugging. More...
 
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. More...
 
WithFormatter operator+ (Formatter &fmt)
 Used for printing RISC operators with formatting. More...
 
WithFormatter operator+ (const std::string &linePrefix)
 Used for printing RISC operators with formatting. More...
 
virtual size_t nInsns () const
 Property: Number of instructions processed. More...
 
virtual void nInsns (size_t n)
 Property: Number of instructions processed. More...
 
virtual SgAsmInstructioncurrentInstruction () const
 Property: Current instruction. More...
 
virtual void currentInstruction (SgAsmInstruction *insn)
 Property: Current instruction. More...
 
virtual SValuePtr undefined_ (size_t nbits)
 Returns a new undefined value. More...
 
virtual SValuePtr unspecified_ (size_t nbits)
 Returns a new undefined value. More...
 
virtual SValuePtr concatLoHi (const SValuePtr &lowBits, const SValuePtr &highBits)
 Aliases for concatenation. More...
 
virtual SValuePtr concatHiLo (const SValuePtr &highBits, const SValuePtr &lowBits)
 Aliases for concatenation. More...
 
virtual SValuePtr isEqual (const SValuePtr &a, const SValuePtr &b)
 Equality comparison. More...
 
virtual SValuePtr isNotEqual (const SValuePtr &a, const SValuePtr &b)
 Equality comparison. More...
 
virtual SValuePtr isUnsignedLessThan (const SValuePtr &a, const SValuePtr &b)
 Comparison for unsigned values. More...
 
virtual SValuePtr isUnsignedLessThanOrEqual (const SValuePtr &a, const SValuePtr &b)
 Comparison for unsigned values. More...
 
virtual SValuePtr isUnsignedGreaterThan (const SValuePtr &a, const SValuePtr &b)
 Comparison for unsigned values. More...
 
virtual SValuePtr isUnsignedGreaterThanOrEqual (const SValuePtr &a, const SValuePtr &b)
 Comparison for unsigned values. More...
 
virtual SValuePtr isSignedLessThan (const SValuePtr &a, const SValuePtr &b)
 Comparison for signed values. More...
 
virtual SValuePtr isSignedLessThanOrEqual (const SValuePtr &a, const SValuePtr &b)
 Comparison for signed values. More...
 
virtual SValuePtr isSignedGreaterThan (const SValuePtr &a, const SValuePtr &b)
 Comparison for signed values. More...
 
virtual SValuePtr isSignedGreaterThanOrEqual (const SValuePtr &a, const SValuePtr &b)
 Comparison for signed values. More...
 
virtual SValuePtr readRegister (RegisterDescriptor reg)
 Reads a value from a register. More...
 
SValuePtr peekRegister (RegisterDescriptor reg)
 Obtain a register value without side effects. More...
 

Static Public Member Functions

static Ptr instance (const Settings &, const Partitioner2::Partitioner &, ModelChecker::SemanticCallbacks *, const InstructionSemantics2::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &, const Variables::VariableFinderPtr &)
 
static Ptr promote (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &x)
 
static std::pair< uint64_t, bool > saturatedAdd (uint64_t base, int64_t delta)
 Saturating addition. More...
 
static AddressInterval shiftAddresses (const AddressInterval &base, int64_t delta, const AddressInterval &limit)
 Offset an interval by a signed amount. More...
 
static AddressInterval shiftAddresses (uint64_t base, const Variables::OffsetInterval &delta, const AddressInterval &limit)
 Offset an interval by a signed amount. More...
 
- Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators
static RiscOperatorsPtr instance (const RegisterDictionary *regdict, const SmtSolverPtr &solver=SmtSolverPtr())
 Instantiates a new RiscOperators object and configures it to use semantic values and states that are defaults for SymbolicSemantics. More...
 
static RiscOperatorsPtr instance (const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
 Instantiates a new RiscOperators object with specified prototypical values. More...
 
static RiscOperatorsPtr instance (const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr())
 Instantiates a new RiscOperators object with specified state. More...
 
static RiscOperatorsPtr promote (const BaseSemantics::RiscOperatorsPtr &x)
 Run-time promotion of a base RiscOperators pointer to symbolic operators. More...
 
static SgAsmFloatTypesgIsIeee754 (SgAsmType *)
 Tests whether a SgAsmType is an IEEE-754 floating-point type. More...
 
- Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators
static RiscOperatorsPtr promote (const RiscOperatorsPtr &x)
 

Protected Member Functions

 RiscOperators (const Settings &, const Partitioner2::Partitioner &, ModelChecker::SemanticCallbacks *, const InstructionSemantics2::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &, const Variables::VariableFinderPtr &)
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators
 RiscOperators (const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
 
 RiscOperators (const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr())
 
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)
 
SValuePtr svalue_number (size_t nbits, uint64_t value) ROSE_DEPRECATED("use svalueNumber instead")
 
SValuePtr svalue_boolean (bool b) ROSE_DEPRECATED("use svalueBoolean instead")
 
SValuePtr svalue_unspecified (size_t nbits) ROSE_DEPRECATED("use svalueUnspecified instead")
 
SValuePtr svalue_bottom (size_t nbits) ROSE_DEPRECATED("use svalueBottom instead")
 
SValuePtr svalue_undefined (size_t nbits) ROSE_DEPRECATED("use svalueUndefined instead")
 
SValuePtr svalue_expr (const ExprPtr &expr, const InsnSet &defs=InsnSet()) ROSE_DEPRECATED("use svalueExpr instead")
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::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::InstructionSemantics2::SymbolicSemantics::RiscOperators
bool omit_cur_insn
 
DefinersMode computingDefiners_
 
WritersMode computingMemoryWriters_
 
WritersMode computingRegisterWriters_
 
size_t trimThreshold_
 
bool reinterpretMemoryReads_
 
bool reinterpretRegisterReads_
 

Member Function Documentation

virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::create ( const InstructionSemantics2::BaseSemantics::SValuePtr protoval,
const SmtSolverPtr solver 
) 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).

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::create ( const InstructionSemantics2::BaseSemantics::StatePtr state,
const SmtSolverPtr solver 
) 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).

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

const Partitioner2::Partitioner& Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::partitioner ( ) const

Property: Partitioner.

The partitioner specified when this object was constructed.

SmtSolver::Ptr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::modelCheckerSolver ( ) const

Property: Model checker SMT solver.

This property holds the solver used for model checking, which can be different or the same as the solver used generally by this object's RISC operators.

void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::modelCheckerSolver ( const SmtSolver::Ptr )

Property: Model checker SMT solver.

This property holds the solver used for model checking, which can be different or the same as the solver used generally by this object's RISC operators.

bool Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::computeMemoryRegions ( ) const

Property: Compute memory regions for variables.

If true, then memory regions are computed and used. Otherwise the SValue memory regions are always empty.

void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::computeMemoryRegions ( bool  )

Property: Compute memory regions for variables.

If true, then memory regions are computed and used. Otherwise the SValue memory regions are always empty.

void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::checkNullAccess ( const InstructionSemantics2::BaseSemantics::SValuePtr addr,
TestMode  ,
IoMode   
)

Test whether the specified address is considered to be null.

An address need not be zero in order to be null. For instance, on Linux the entire first page of memory is generally unmapped in order to increase the chance that a null pointer to a struct/class/array still causes a segmentation fault even when accessing a member other than the first member.

If a null dereference is detected, then a NullDerefTag is thrown.

void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::checkOobAccess ( const InstructionSemantics2::BaseSemantics::SValuePtr addr,
TestMode  ,
IoMode  ,
size_t  nBytes 
)

Test whether the specified address is out of bounds for variables.

If an OOB access is detected, then an OobTag is thrown.

size_t Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::nInstructions ( ) const

Property: Number of instructions executed.

This property contains teh number of instructions executed. It is incremented automatically at the end of each instruction, but the user can reset it to any other value.

void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::nInstructions ( size_t  )

Property: Number of instructions executed.

This property contains teh number of instructions executed. It is incremented automatically at the end of each instruction, but the user can reset it to any other value.

void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::pushCallStack ( const Partitioner2::FunctionPtr callee,
rose_addr_t  initialSp 
)

Push a function onto the call stack.

size_t Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::pruneCallStack ( )

Remove old call stack entries.

Look at the current stack pointer and remove those function call entries that are beyond. In effect, this cleans up those functions that have returned.

Returns the number of items poppped from the call stack.

void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::printCallStack ( std::ostream &  )

Print information about the function call stack.

static std::pair<uint64_t , bool > Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::saturatedAdd ( uint64_t  base,
int64_t  delta 
)
static

Saturating addition.

Add the signed value to the unsigned base, returning an unsigned result. If the result would overflow then return either zero or the maximum unsigned value, depending on the direction of overflow. The return value is a pair that contains the saturated result and a Boolean indicating whether saturation occured.

static AddressInterval Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::shiftAddresses ( const AddressInterval base,
int64_t  delta,
const AddressInterval limit 
)
static

Offset an interval by a signed amount.

The unsigned address interval is shifted lower or higher according to the signed delta value. The endpoints of the returned interval saturate to zero or maximum address if the delta causes the interval to partially overflow. If the interval completely overflows (both its least and greatest values overflow) then the empty interval is returned. Shifting an empty address interval any amount also returns the emtpy interval. The return value is clipped by intersecting it with the specified limit.

static AddressInterval Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::shiftAddresses ( uint64_t  base,
const Variables::OffsetInterval delta,
const AddressInterval limit 
)
static

Offset an interval by a signed amount.

The unsigned address interval is shifted lower or higher according to the signed delta value. The endpoints of the returned interval saturate to zero or maximum address if the delta causes the interval to partially overflow. If the interval completely overflows (both its least and greatest values overflow) then the empty interval is returned. Shifting an empty address interval any amount also returns the emtpy interval. The return value is clipped by intersecting it with the specified limit.

InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::assignRegion ( const InstructionSemantics2::BaseSemantics::SValuePtr result)

Assign a region to an expression.

The region is assigned to the first argument, which is also returned.

If the first argument already has a region, then nothing is done.

Otherwise, if additional arguments are specified and exactly one has a region, then that region is assigned to the result.

Otherwise, we scan the function call stack (stored in the current semantic state) and look for a variable whose addresses include the result value. If such a variable is found, then its memory region is assigned to the result expression.

InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::assignRegion ( const InstructionSemantics2::BaseSemantics::SValuePtr result,
const InstructionSemantics2::BaseSemantics::SValuePtr a 
)

Assign a region to an expression.

The region is assigned to the first argument, which is also returned.

If the first argument already has a region, then nothing is done.

Otherwise, if additional arguments are specified and exactly one has a region, then that region is assigned to the result.

Otherwise, we scan the function call stack (stored in the current semantic state) and look for a variable whose addresses include the result value. If such a variable is found, then its memory region is assigned to the result expression.

InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::assignRegion ( const InstructionSemantics2::BaseSemantics::SValuePtr result,
const InstructionSemantics2::BaseSemantics::SValuePtr a,
const InstructionSemantics2::BaseSemantics::SValuePtr b 
)

Assign a region to an expression.

The region is assigned to the first argument, which is also returned.

If the first argument already has a region, then nothing is done.

Otherwise, if additional arguments are specified and exactly one has a region, then that region is assigned to the result.

Otherwise, we scan the function call stack (stored in the current semantic state) and look for a variable whose addresses include the result value. If such a variable is found, then its memory region is assigned to the result expression.

virtual void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::startInstruction ( SgAsmInstruction insn)
overridevirtual

Called at the beginning of every instruction.

This method is invoked every time the translation object begins processing an instruction. Some policies use this to update a pointer to the current instruction.

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

virtual void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::finishInstruction ( SgAsmInstruction insn)
overridevirtual

Called at the end of every instruction.

This method is invoked whenever the translation object ends processing for an instruction. This is not called if there's an exception during processing.

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

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::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::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::extract ( const InstructionSemantics2::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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::concat ( const InstructionSemantics2::BaseSemantics::SValuePtr lowBits,
const InstructionSemantics2::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 SymbolicExpr concatenation function.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::shiftLeft ( const InstructionSemantics2::BaseSemantics::SValuePtr a,
const InstructionSemantics2::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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::shiftRight ( const InstructionSemantics2::BaseSemantics::SValuePtr a,
const InstructionSemantics2::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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::shiftRightArithmetic ( const InstructionSemantics2::BaseSemantics::SValuePtr a,
const InstructionSemantics2::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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::unsignedExtend ( const InstructionSemantics2::BaseSemantics::SValue::Ptr 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::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::signExtend ( const InstructionSemantics2::BaseSemantics::SValue::Ptr a,
size_t  new_width 
)
overridevirtual

Sign extends a value.

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

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::add ( const InstructionSemantics2::BaseSemantics::SValuePtr a,
const InstructionSemantics2::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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::addCarry ( const InstructionSemantics2::BaseSemantics::SValuePtr a,
const InstructionSemantics2::BaseSemantics::SValuePtr b,
InstructionSemantics2::BaseSemantics::SValuePtr carryOut,
InstructionSemantics2::BaseSemantics::SValuePtr overflowed 
)
overridevirtual

Adds two integers of equal size and carry.

The width of a and b must be the same, and the resulting sum will also have the same width. Returns the sum by value and a carry-out bit by reference. An overflow bit is also returned and is useful when a and b are interpreted as signed values. This method is not pure abstract and is generally not overridden in subclasses because it can be implemented in terms of other operations.

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

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::subtract ( const InstructionSemantics2::BaseSemantics::SValuePtr minuend,
const InstructionSemantics2::BaseSemantics::SValuePtr subtrahend 
)
overridevirtual

Subtract one value from another.

Subtracts the subtrahend from the minuend and returns the result. The two arguments must be the same width and the return value will also be that same width. This method is not pure virtual and is not usually overridden by subclasses because it can be implemented in terms of other operations.

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

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::subtractCarry ( const InstructionSemantics2::BaseSemantics::SValuePtr minuend,
const InstructionSemantics2::BaseSemantics::SValuePtr subtrahend,
InstructionSemantics2::BaseSemantics::SValuePtr carryOut,
InstructionSemantics2::BaseSemantics::SValuePtr overflowed 
)
overridevirtual

Subtract one value from another and carry.

Subtracts the subtrahend from the minuend and returns the result. The two arguments must be the same width and the return value will also be that same width. A carry-out bit and overflow bit are returned by reference. The carry out bit is simply the carry out from adding the minuend and negated subtrahend. The overflow bit is set if the result would overflow the width of the return value, and is calculated as the XOR of the two most significant carray-out bits. This method is not pure virtual and is not usually overridden by subclasses because it can be implemented in terms of other operations.

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

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::addWithCarries ( const InstructionSemantics2::BaseSemantics::SValuePtr a,
const InstructionSemantics2::BaseSemantics::SValuePtr b,
const InstructionSemantics2::BaseSemantics::SValuePtr c,
InstructionSemantics2::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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::readRegister ( RegisterDescriptor  reg,
const InstructionSemantics2::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::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::writeRegister ( RegisterDescriptor  reg,
const InstructionSemantics2::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::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::readMemory ( RegisterDescriptor  segreg,
const InstructionSemantics2::BaseSemantics::SValuePtr addr,
const InstructionSemantics2::BaseSemantics::SValuePtr dflt,
const InstructionSemantics2::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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.

virtual void Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators::writeMemory ( RegisterDescriptor  segreg,
const InstructionSemantics2::BaseSemantics::SValuePtr addr,
const InstructionSemantics2::BaseSemantics::SValuePtr data,
const InstructionSemantics2::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.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators.


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