ROSE  0.11.50.0
Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators Class Reference

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:

return arg->copy(); //correct
return arg; //incorrect
}

Definition at line 822 of file SymbolicSemantics.h.

#include <SymbolicSemantics.h>

Inheritance diagram for Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators:
Inheritance graph
[legend]
Collaboration diagram for Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators:
Collaboration graph
[legend]

Public Types

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 BaseSemantics::RiscOperatorsPtr create (const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
 Virtual allocating constructor. More...
 
virtual BaseSemantics::RiscOperatorsPtr create (const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE
 Virtual allocating constructor. More...
 
virtual BaseSemantics::SValuePtr boolean_ (bool b) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr number_ (size_t nbits, uint64_t value) ROSE_OVERRIDE
 
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
 
virtual BaseSemantics::SValuePtr or_ (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr xor_ (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr invert (const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr extract (const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr concat (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr leastSignificantSetBit (const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr mostSignificantSetBit (const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr rotateLeft (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr rotateRight (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr shiftLeft (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr shiftRight (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr shiftRightArithmetic (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr equalToZero (const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr ite (const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr unsignedExtend (const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr signExtend (const BaseSemantics::SValuePtr &a_, size_t new_width) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr add (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) ROSE_OVERRIDE
 
virtual BaseSemantics::SValuePtr addWithCarries (const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, const BaseSemantics::SValuePtr &c_, BaseSemantics::SValuePtr &carry_out) ROSE_OVERRIDE
 Used for printing RISC operators with formatting. 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 readRegister (RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
 Reads a value from a register. More...
 
virtual BaseSemantics::SValuePtr peekRegister (RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
 Obtain a register value without side effects. More...
 
virtual void writeRegister (RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) ROSE_OVERRIDE
 Writes a value to a register. More...
 
virtual BaseSemantics::SValuePtr readMemory (RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE
 Reads a value from memory. More...
 
virtual BaseSemantics::SValuePtr peekMemory (RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE
 Read memory without side effects. More...
 
virtual void writeMemory (RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE
 Writes a value to memory. 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 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.
 
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 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 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())
 

Protected Attributes

bool omit_cur_insn
 
DefinersMode computingDefiners_
 
WritersMode computingMemoryWriters_
 
WritersMode computingRegisterWriters_
 
size_t trimThreshold_
 
bool reinterpretMemoryReads_
 
bool reinterpretRegisterReads_
 

Member Typedef Documentation

Base type.

Definition at line 825 of file SymbolicSemantics.h.

Shared-ownership pointer.

Definition at line 828 of file SymbolicSemantics.h.

Member Function Documentation

static RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::instance ( const RegisterDictionary regdict,
const SmtSolverPtr solver = SmtSolverPtr() 
)
inlinestatic
static RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::instance ( const BaseSemantics::SValuePtr protoval,
const SmtSolverPtr solver = SmtSolverPtr() 
)
inlinestatic

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.

Definition at line 904 of file SymbolicSemantics.h.

References Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators::solver().

static RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::instance ( const BaseSemantics::StatePtr state,
const SmtSolverPtr solver = SmtSolverPtr() 
)
inlinestatic

Instantiates a new RiscOperators object with specified state.

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

Definition at line 910 of file SymbolicSemantics.h.

References Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators::solver().

virtual BaseSemantics::RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::create ( const BaseSemantics::SValuePtr protoval,
const SmtSolverPtr solver = SmtSolverPtr() 
) const
inlinevirtual

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::InstructionSemantics2::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators, and Rose::BinaryAnalysis::InstructionSemantics2::LlvmSemantics::RiscOperators.

Definition at line 917 of file SymbolicSemantics.h.

References instance(), and Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators::solver().

virtual BaseSemantics::RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::create ( const BaseSemantics::StatePtr state,
const SmtSolverPtr solver = SmtSolverPtr() 
) const
inlinevirtual

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::InstructionSemantics2::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators, and Rose::BinaryAnalysis::InstructionSemantics2::LlvmSemantics::RiscOperators.

Definition at line 922 of file SymbolicSemantics.h.

References instance(), and Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators::solver().

static RiscOperatorsPtr Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::promote ( const BaseSemantics::RiscOperatorsPtr x)
inlinestatic

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.

Definition at line 932 of file SymbolicSemantics.h.

void Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::computingDefiners ( DefinersMode  m)
inline

Property: Track which instructions define a semantic value.

Each semantic value (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 1037 of file SymbolicSemantics.h.

DefinersMode Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::computingDefiners ( ) const
inline

Property: Track which instructions define a semantic value.

Each semantic value (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 1038 of file SymbolicSemantics.h.

void Rose::BinaryAnalysis::InstructionSemantics2::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 1059 of file SymbolicSemantics.h.

WritersMode Rose::BinaryAnalysis::InstructionSemantics2::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 1060 of file SymbolicSemantics.h.

void Rose::BinaryAnalysis::InstructionSemantics2::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 1084 of file SymbolicSemantics.h.

WritersMode Rose::BinaryAnalysis::InstructionSemantics2::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 1085 of file SymbolicSemantics.h.

void Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::trimThreshold ( size_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 1097 of file SymbolicSemantics.h.

size_t Rose::BinaryAnalysis::InstructionSemantics2::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 1098 of file SymbolicSemantics.h.

bool Rose::BinaryAnalysis::InstructionSemantics2::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 1108 of file SymbolicSemantics.h.

void Rose::BinaryAnalysis::InstructionSemantics2::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 1109 of file SymbolicSemantics.h.

bool Rose::BinaryAnalysis::InstructionSemantics2::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 1110 of file SymbolicSemantics.h.

void Rose::BinaryAnalysis::InstructionSemantics2::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 1111 of file SymbolicSemantics.h.

virtual void Rose::BinaryAnalysis::InstructionSemantics2::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::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
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;
virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::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.

static SgAsmFloatType* Rose::BinaryAnalysis::InstructionSemantics2::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.

virtual SymbolicExpr::Type Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::sgTypeToSymbolicType ( SgAsmType )
virtual

Convert a SgAsmType to a symbolic type.

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

virtual void Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::RiscOperators::interrupt ( int  majr,
int  minr 
)
virtual

Invoked for instructions that cause 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 minr operand for INT3 is -3 to distinguish it from the one-argument "INT 3" instruction which has slightly different semantics.

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

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

Used for printing RISC operators with formatting.

The usual way to use this is:

RiscOperatorsPtr obj = ...;
Formatter fmt = ...;
std::cout <<"The value is: " <<(*obj+fmt) <<"\n";

Since specifying a line prefix string for indentation purposes is such a common use case, the indentation can be given instead of a format, as in the following code that indents the prefixes each line of the expression with four spaces.

std::cout <<"Machine state:\n" <<*(obj + " ");
@code
@{ */
WithFormatter with_format(Formatter &fmt) { return WithFormatter(shared_from_this(), fmt); }
WithFormatter operator+(Formatter &fmt) { return with_format(fmt); }
WithFormatter operator+(const std::string &linePrefix);
virtual size_t nInsns() const { return nInsns_; }
virtual void nInsns(size_t n) { nInsns_ = n; }
virtual SgAsmInstruction* currentInstruction() const {
return currentInsn_;
}
virtual void currentInstruction(SgAsmInstruction *insn) {
currentInsn_ = insn;
}
virtual void startInstruction(SgAsmInstruction *insn);
virtual void finishInstruction(SgAsmInstruction *insn);
// Value Construction Operations
// The trailing underscores are necessary for for undefined_() on some machines, so we just add one to the end of all the
// virtual constructors for consistency.
virtual SValuePtr undefined_(size_t nbits);
virtual SValuePtr unspecified_(size_t nbits);
virtual SValuePtr number_(size_t nbits, uint64_t value);
virtual SValuePtr boolean_(bool value);
virtual SValuePtr bottom_(size_t nbits);
// x86-specific Operations (FIXME)
virtual SValuePtr filterCallTarget(const SValuePtr &a);
virtual SValuePtr filterReturnTarget(const SValuePtr &a);
virtual SValuePtr filterIndirectJumpTarget(const SValuePtr &a);
virtual void hlt() {}
virtual void cpuid() {}
virtual SValuePtr rdtsc() { return unspecified_(64); }
// Boolean Operations
virtual SValuePtr and_(const SValuePtr &a, const SValuePtr &b) = 0;
virtual SValuePtr or_(const SValuePtr &a, const SValuePtr &b) = 0;
virtual SValuePtr xor_(const SValuePtr &a, const SValuePtr &b) = 0;
virtual SValuePtr invert(const SValuePtr &a) = 0;
virtual SValuePtr extract(const SValuePtr &a, size_t begin_bit, size_t end_bit) = 0;
virtual SValuePtr concat(const SValuePtr &lowBits, const SValuePtr &highBits) = 0;
virtual SValuePtr concatLoHi(const SValuePtr &lowBits, const SValuePtr &highBits) {
return concat(lowBits, highBits);
}
virtual SValuePtr concatHiLo(const SValuePtr &highBits, const SValuePtr &lowBits) {
return concat(lowBits, highBits);
}
virtual std::pair<SValuePtr /*low*/, SValuePtr /*high*/> split(const SValuePtr &a, size_t splitPoint);
virtual SValuePtr leastSignificantSetBit(const SValuePtr &a) = 0;
virtual SValuePtr mostSignificantSetBit(const SValuePtr &a) = 0;
virtual SValuePtr countLeadingZeros(const SValuePtr &a);
virtual SValuePtr countLeadingOnes(const SValuePtr &a);
virtual SValuePtr rotateLeft(const SValuePtr &a, const SValuePtr &nbits) = 0;
virtual SValuePtr rotateRight(const SValuePtr &a, const SValuePtr &nbits) = 0;
virtual SValuePtr shiftLeft(const SValuePtr &a, const SValuePtr &nbits) = 0;
virtual SValuePtr shiftRight(const SValuePtr &a, const SValuePtr &nbits) = 0;
virtual SValuePtr shiftRightArithmetic(const SValuePtr &a, const SValuePtr &nbits) = 0;
virtual SValuePtr reverseElmts(const SValuePtr &a, size_t elmtNBits);
// Comparison Operations
virtual SValuePtr equalToZero(const SValuePtr &a) = 0;
virtual SValuePtr ite(const SValuePtr &cond, const SValuePtr &a, const SValuePtr &b) = 0;
virtual SValuePtr isEqual(const SValuePtr &a, const SValuePtr &b);
virtual SValuePtr isNotEqual(const SValuePtr &a, const SValuePtr &b);
virtual SValuePtr isUnsignedLessThan(const SValuePtr &a, const SValuePtr &b);
virtual SValuePtr isUnsignedLessThanOrEqual(const SValuePtr &a, const SValuePtr &b);
virtual SValuePtr isUnsignedGreaterThan(const SValuePtr &a, const SValuePtr &b);
virtual SValuePtr isUnsignedGreaterThanOrEqual(const SValuePtr &a, const SValuePtr &b);
virtual SValuePtr isSignedLessThan(const SValuePtr &a, const SValuePtr &b);
virtual SValuePtr isSignedLessThanOrEqual(const SValuePtr &a, const SValuePtr &b);
virtual SValuePtr isSignedGreaterThan(const SValuePtr &a, const SValuePtr &b);
virtual SValuePtr isSignedGreaterThanOrEqual(const SValuePtr &a, const SValuePtr &b);
// Integer Arithmetic Operations
virtual SValuePtr unsignedExtend(const SValuePtr &a, size_t new_width);
virtual SValuePtr signExtend(const SValuePtr &a, size_t new_width) = 0;
virtual SValuePtr add(const SValuePtr &a, const SValuePtr &b) = 0;
virtual SValuePtr addCarry(const SValuePtr &a, const SValuePtr &b,
SValuePtr &carryOut /*out*/, SValuePtr &overflowed /*out*/);
virtual SValuePtr subtract(const SValuePtr &minuend, const SValuePtr &subtrahend);
virtual SValuePtr subtractCarry(const SValuePtr &minuend, const SValuePtr &subtrahend,
SValuePtr &carryOut /*out*/, SValuePtr &overflowed /*out*/);

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::InstructionSemantics2::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators.

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

Two's complement.

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

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators.

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

Divides two signed values.

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

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators.

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

Calculates modulo with signed values.

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

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators.

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

Multiplies two signed values.

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

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators.

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

Divides two unsigned values.

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

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators.

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

Calculates modulo with unsigned values.

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

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators.

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

Multiply two unsigned values.

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

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::RiscOperators.

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

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::InstructionSemantics2::BaseSemantics::RiscOperators.

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

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::InstructionSemantics2::BaseSemantics::RiscOperators.

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

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::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators.

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

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::InstructionSemantics2::BaseSemantics::RiscOperators.

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

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::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators.

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

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::InstructionSemantics2::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators, and Rose::BinaryAnalysis::InstructionSemantics2::LlvmSemantics::RiscOperators.

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

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::InstructionSemantics2::BaseSemantics::RiscOperators.

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

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::InstructionSemantics2::BaseSemantics::RiscOperators.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::RiscOperators, and Rose::BinaryAnalysis::InstructionSemantics2::LlvmSemantics::RiscOperators.


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