#include <SymbolicSemantics.h>
Collaboration diagram for SymbolicSemantics::Policy< State, ValueType >:
See documentation for the SymbolicSemantics namespace.
Public Types | |
| MRT_STACK_PTR | |
| MRT_FRAME_PTR | |
| MRT_OTHER_PTR | |
| enum | MemRefType { MRT_STACK_PTR, MRT_FRAME_PTR, MRT_OTHER_PTR } |
| See memory_reference_type(). More... | |
Public Member Functions | |
| Policy () | |
| Constructs a new policy without an SMT solver. | |
| Policy (SMTSolver *solver) | |
| Constructs a new policy with an SMT solver. | |
| void | init () |
| Initialize undefined policy. | |
| void | set_solver (SMTSolver *s) |
| Sets the satisfiability modulo theory (SMT) solver to use for certain operations. | |
| SMTSolver * | get_solver () const |
| Returns the solver that is currently being used. | |
| const State< ValueType > & | get_state () const |
| Returns the current state. | |
| State< ValueType > & | get_state () |
| const State< ValueType > & | get_orig_state () const |
| Returns the original state. | |
| State< ValueType > & | get_orig_state () |
| const ValueType< 32 > & | get_ip () const |
| Returns the current instruction pointer. | |
| const ValueType< 32 > & | get_orig_ip () const |
| Returns the original instruction pointer. | |
| Memory | memory_for_equality (const State< ValueType > &) const |
| Returns a copy of the state after removing memory that is not pertinent to an equal_states() comparison. | |
| Memory | memory_for_equality () const |
| Returns a copy of the current state after removing memory that is not pertinent to an equal_states() comparison. | |
| bool | equal_states (const State< ValueType > &, const State< ValueType > &) const |
| Compares two states for equality. | |
| void | print (std::ostream &o, RenameMap *rmap=NULL) const |
| Print the current state of this policy. | |
| bool | on_stack (const ValueType< 32 > &value) const |
| Returns true if the specified value exists in memory and is provably at or above the stack pointer. | |
| void | set_discard_popped_memory (bool b) |
| Changes how the policy treats the stack. | |
| bool | get_discard_popped_memory () const |
| Returns the current setting for the property that determines how the stack behaves. | |
| void | print_diff (std::ostream &, const State< ValueType > &, const State< ValueType > &, RenameMap *rmap=NULL) const |
| Print only the differences between two states. | |
| void | print_diff (std::ostream &o, const State< ValueType > &state, RenameMap *rmap=NULL) const |
| Print the difference between a state and the initial state. | |
| void | print_diff (std::ostream &o, RenameMap *rmap=NULL) const |
| Print the difference between the current state and the initial state. | |
| std::string | SHA1 () const |
| Returns the SHA1 hash of the difference between the current state and the original state. | |
| template<size_t FromLen, size_t ToLen> | |
| ValueType< ToLen > | unsignedExtend (const ValueType< FromLen > &a) const |
Extend (or shrink) from FromLen bits to ToLen bits by adding or removing high-order bits from the input. | |
| template<size_t FromLen, size_t ToLen> | |
| ValueType< ToLen > | signedExtend (const ValueType< FromLen > &a) const |
Sign extend from FromLen bits to ToLen bits. | |
| template<size_t BeginAt, size_t EndAt, size_t Len> | |
| ValueType< EndAt-BeginAt > | extract (const ValueType< Len > &a) const |
| Extracts certain bits from the specified value and shifts them to the low-order positions in the result. | |
| template<size_t Len> | |
| ValueType< Len > | mem_read (State< ValueType > &state, const ValueType< 32 > &addr) const |
| Reads a value from memory in a way that always returns the same value provided there are not intervening writes that would clobber the value either directly or by aliasing. | |
| MemRefType | memory_reference_type (const State< ValueType > &state, const ValueType< 32 > &addr) const |
| Determines if the specified address is related to the current stack or frame pointer. | |
| template<size_t Len> | |
| void | mem_write (State< ValueType > &state, const ValueType< 32 > &addr, const ValueType< Len > &data) |
| Writes a value to memory. | |
| const RegisterDictionary * | get_register_dictionary () const |
| Returns the register dictionary. | |
| void | set_register_dictionary (const RegisterDictionary *regdict) |
| Sets the register dictionary. | |
| void | startInstruction (SgAsmInstruction *insn) |
| void | finishInstruction (SgAsmInstruction *) |
| ValueType< 1 > | true_ () const |
| True value. | |
| ValueType< 1 > | false_ () const |
| False value. | |
| ValueType< 1 > | undefined_ () const |
| Undefined Boolean. | |
| template<size_t Len> | |
| ValueType< Len > | number (uint64_t n) const |
| Used to build a known constant. | |
| ValueType< 32 > | filterCallTarget (const ValueType< 32 > &a) const |
| Called only for CALL instructions before assigning new value to IP register. | |
| ValueType< 32 > | filterReturnTarget (const ValueType< 32 > &a) const |
| Called only for RET instructions before adjusting the IP register. | |
| ValueType< 32 > | filterIndirectJumpTarget (const ValueType< 32 > &a) const |
| Called only for JMP instructions before adjusting the IP register. | |
| void | hlt () |
| Called only for the HLT instruction. | |
| void | cpuid () |
| Called only for the CPUID instruction. | |
| ValueType< 64 > | rdtsc () |
| Called only for the RDTSC instruction. | |
| void | interrupt (uint8_t num) |
| Called only for the INT instruction. | |
| void | sysenter () |
| Called for SYSENTER instruction. | |
| template<size_t Len> | |
| ValueType< Len > | add (const ValueType< Len > &a, const ValueType< Len > &b) const |
| Adds two values. | |
| template<size_t Len> | |
| ValueType< Len > | addWithCarries (const ValueType< Len > &a, const ValueType< Len > &b, const ValueType< 1 > &c, ValueType< Len > &carry_out) const |
| Add two values of equal size and a carry bit. | |
| template<size_t Len> | |
| ValueType< Len > | and_ (const ValueType< Len > &a, const ValueType< Len > &b) const |
| Computes bit-wise AND of two values. | |
| template<size_t Len> | |
| ValueType< 1 > | equalToZero (const ValueType< Len > &a) const |
| Returns true_, false_, or undefined_ depending on whether argument is zero. | |
| template<size_t Len> | |
| ValueType< Len > | invert (const ValueType< Len > &a) const |
| One's complement. | |
| template<size_t Len1, size_t Len2> | |
| ValueType< Len1+Len2 > | concat (const ValueType< Len1 > &a, const ValueType< Len2 > &b) const |
Concatenate the values of a and b so that the result has b in the high-order bits and a in the low order bits. | |
| template<size_t Len> | |
| ValueType< Len > | ite (const ValueType< 1 > &sel, const ValueType< Len > &ifTrue, const ValueType< Len > &ifFalse) const |
| Returns second or third arg depending on value of first arg. | |
| template<size_t Len> | |
| ValueType< Len > | leastSignificantSetBit (const ValueType< Len > &a) const |
| Returns position of least significant set bit; zero when no bits are set. | |
| template<size_t Len> | |
| ValueType< Len > | mostSignificantSetBit (const ValueType< Len > &a) const |
| Returns position of most significant set bit; zero when no bits are set. | |
| template<size_t Len> | |
| ValueType< Len > | negate (const ValueType< Len > &a) const |
| Two's complement. | |
| template<size_t Len> | |
| ValueType< Len > | or_ (const ValueType< Len > &a, const ValueType< Len > &b) const |
| Computes bit-wise OR of two values. | |
| template<size_t Len, size_t SALen> | |
| ValueType< Len > | rotateLeft (const ValueType< Len > &a, const ValueType< SALen > &sa) const |
| Rotate bits to the left. | |
| template<size_t Len, size_t SALen> | |
| ValueType< Len > | rotateRight (const ValueType< Len > &a, const ValueType< SALen > &sa) const |
| Rotate bits to the right. | |
| template<size_t Len, size_t SALen> | |
| ValueType< Len > | shiftLeft (const ValueType< Len > &a, const ValueType< SALen > &sa) const |
| Returns arg shifted left. | |
| template<size_t Len, size_t SALen> | |
| ValueType< Len > | shiftRight (const ValueType< Len > &a, const ValueType< SALen > &sa) const |
| Returns arg shifted right logically (no sign bit). | |
| template<size_t Len, size_t SALen> | |
| ValueType< Len > | shiftRightArithmetic (const ValueType< Len > &a, const ValueType< SALen > &sa) const |
| Returns arg shifted right arithmetically (with sign bit). | |
| template<size_t From, size_t To> | |
| ValueType< To > | signExtend (const ValueType< From > &a) |
| Sign extends a value. | |
| template<size_t Len1, size_t Len2> | |
| ValueType< Len1 > | signedDivide (const ValueType< Len1 > &a, const ValueType< Len2 > &b) const |
| Divides two signed values. | |
| template<size_t Len1, size_t Len2> | |
| ValueType< Len2 > | signedModulo (const ValueType< Len1 > &a, const ValueType< Len2 > &b) const |
| Calculates modulo with signed values. | |
| template<size_t Len1, size_t Len2> | |
| ValueType< Len1+Len2 > | signedMultiply (const ValueType< Len1 > &a, const ValueType< Len2 > &b) const |
| Multiplies two signed values. | |
| template<size_t Len1, size_t Len2> | |
| ValueType< Len1 > | unsignedDivide (const ValueType< Len1 > &a, const ValueType< Len2 > &b) const |
| Divides two unsigned values. | |
| template<size_t Len1, size_t Len2> | |
| ValueType< Len2 > | unsignedModulo (const ValueType< Len1 > &a, const ValueType< Len2 > &b) const |
| Calculates modulo with unsigned values. | |
| template<size_t Len1, size_t Len2> | |
| ValueType< Len1+Len2 > | unsignedMultiply (const ValueType< Len1 > &a, const ValueType< Len2 > &b) const |
| Multiply two unsigned values. | |
| template<size_t Len> | |
| ValueType< Len > | xor_ (const ValueType< Len > &a, const ValueType< Len > &b) const |
| Computes bit-wise XOR of two values. | |
| const RegisterDescriptor & | findRegister (const std::string ®name, size_t nbits=0) |
| Finds a register by name. | |
| template<size_t Len> | |
| ValueType< Len > | readRegister (const char *regname) |
| Reads from a named register. | |
| template<size_t Len> | |
| void | writeRegister (const char *regname, const ValueType< Len > &value) |
| Writes to a named register. | |
| template<size_t Len> | |
| ValueType< Len > | readRegister (const RegisterDescriptor ®) |
| Generic register read. | |
| template<size_t Len> | |
| void | writeRegister (const RegisterDescriptor ®, const ValueType< Len > &value) |
| Generic register write. | |
| template<size_t Len> | |
| ValueType< Len > | readMemory (X86SegmentRegister segreg, const ValueType< 32 > &addr, const ValueType< 1 > &cond) const |
| Reads a value from memory. | |
| template<size_t Len> | |
| void | writeMemory (X86SegmentRegister segreg, const ValueType< 32 > &addr, const ValueType< Len > &data, const ValueType< 1 > &cond) |
| Writes a value to memory. | |
Protected Types | |
| typedef State< ValueType >::Memory | Memory |
Protected Attributes | |
| SgAsmInstruction * | cur_insn |
| Set by startInstruction(), cleared by finishInstruction(). | |
| State< ValueType > | orig_state |
| Original machine state, initialized by constructor and mem_write. | |
| State< ValueType > | cur_state |
| Current machine state updated by each processInstruction(). | |
| bool | p_discard_popped_memory |
| Property that determines how the stack behaves. | |
| size_t | ninsns |
| Total number of instructions processed. | |
| SMTSolver * | solver |
| The solver to use for Satisfiability Modulo Theory, or NULL. | |
| const RegisterDictionary * | regdict |
| Registers stored in the various State objects for this Policy. | |
Friends | |
| std::ostream & | operator<< (std::ostream &o, const Policy &p) |
Classes | |
| struct | Exception |
typedef State<ValueType>::Memory SymbolicSemantics::Policy< State, ValueType >::Memory [protected] |
| enum SymbolicSemantics::Policy::MemRefType |
| SymbolicSemantics::Policy< State, ValueType >::Policy | ( | ) | [inline] |
Constructs a new policy without an SMT solver.
| SymbolicSemantics::Policy< State, ValueType >::Policy | ( | SMTSolver * | solver | ) | [inline] |
Constructs a new policy with an SMT solver.
| void SymbolicSemantics::Policy< State, ValueType >::init | ( | ) | [inline] |
Initialize undefined policy.
Used by constructors so initialization is in one location.
| void SymbolicSemantics::Policy< State, ValueType >::set_solver | ( | SMTSolver * | s | ) | [inline] |
Sets the satisfiability modulo theory (SMT) solver to use for certain operations.
| SMTSolver* SymbolicSemantics::Policy< State, ValueType >::get_solver | ( | ) | const [inline] |
Returns the solver that is currently being used.
| const State<ValueType>& SymbolicSemantics::Policy< State, ValueType >::get_state | ( | ) | const [inline] |
Returns the current state.
| State<ValueType>& SymbolicSemantics::Policy< State, ValueType >::get_state | ( | ) | [inline] |
| const State<ValueType>& SymbolicSemantics::Policy< State, ValueType >::get_orig_state | ( | ) | const [inline] |
Returns the original state.
The original state is initialized to be equal to the current state twice: once by the constructor, and then again when the first instruction is processed.
| State<ValueType>& SymbolicSemantics::Policy< State, ValueType >::get_orig_state | ( | ) | [inline] |
| const ValueType<32>& SymbolicSemantics::Policy< State, ValueType >::get_ip | ( | ) | const [inline] |
Returns the current instruction pointer.
| const ValueType<32>& SymbolicSemantics::Policy< State, ValueType >::get_orig_ip | ( | ) | const [inline] |
Returns the original instruction pointer.
See also get_orig_state().
| Memory SymbolicSemantics::Policy< State, ValueType >::memory_for_equality | ( | const State< ValueType > & | ) | const |
Returns a copy of the state after removing memory that is not pertinent to an equal_states() comparison.
| Memory SymbolicSemantics::Policy< State, ValueType >::memory_for_equality | ( | ) | const [inline] |
Returns a copy of the current state after removing memory that is not pertinent to an equal_states() comparison.
| bool SymbolicSemantics::Policy< State, ValueType >::equal_states | ( | const State< ValueType > & | , | |
| const State< ValueType > & | ||||
| ) | const |
Compares two states for equality.
The comarison looks at all register values and the memory locations that are different than their original value (but excluding differences due to clobbering). It does not compare memory that has only been read.
| void SymbolicSemantics::Policy< State, ValueType >::print | ( | std::ostream & | o, | |
| RenameMap * | rmap = NULL | |||
| ) | const [inline] |
Print the current state of this policy.
If a rename map is specified then named values will be renamed to have a shorter name. See the ValueType<>::rename() method for details.
| bool SymbolicSemantics::Policy< State, ValueType >::on_stack | ( | const ValueType< 32 > & | value | ) | const |
Returns true if the specified value exists in memory and is provably at or above the stack pointer.
The stack pointer need not have a known value.
| void SymbolicSemantics::Policy< State, ValueType >::set_discard_popped_memory | ( | bool | b | ) | [inline] |
Changes how the policy treats the stack.
See the p_discard_popped_memory property data member for details.
| bool SymbolicSemantics::Policy< State, ValueType >::get_discard_popped_memory | ( | ) | const [inline] |
Returns the current setting for the property that determines how the stack behaves.
See the p_set_discard_popped_memory property data member for details.
| void SymbolicSemantics::Policy< State, ValueType >::print_diff | ( | std::ostream & | , | |
| const State< ValueType > & | , | |||
| const State< ValueType > & | , | |||
| RenameMap * | rmap = NULL | |||
| ) | const |
Print only the differences between two states.
If a rename map is specified then named values will be renamed to have a shorter name. See the ValueType<>::rename() method for details.
| void SymbolicSemantics::Policy< State, ValueType >::print_diff | ( | std::ostream & | o, | |
| const State< ValueType > & | state, | |||
| RenameMap * | rmap = NULL | |||
| ) | const [inline] |
Print the difference between a state and the initial state.
If a rename map is specified then named values will be renamed to have a shorter name. See the ValueType<>::rename() method for details.
| void SymbolicSemantics::Policy< State, ValueType >::print_diff | ( | std::ostream & | o, | |
| RenameMap * | rmap = NULL | |||
| ) | const [inline] |
Print the difference between the current state and the initial state.
If a rename map is specified then named values will be renamed to have a shorter name. See the ValueType<>::rename() method for details.
| std::string SymbolicSemantics::Policy< State, ValueType >::SHA1 | ( | ) | const |
Returns the SHA1 hash of the difference between the current state and the original state.
If libgcrypt is not available then the return value will be an empty string.
| ValueType<ToLen> SymbolicSemantics::Policy< State, ValueType >::unsignedExtend | ( | const ValueType< FromLen > & | a | ) | const [inline] |
Extend (or shrink) from FromLen bits to ToLen bits by adding or removing high-order bits from the input.
Added bits are always zeros.
| ValueType<ToLen> SymbolicSemantics::Policy< State, ValueType >::signedExtend | ( | const ValueType< FromLen > & | a | ) | const [inline] |
Sign extend from FromLen bits to ToLen bits.
| ValueType<EndAt-BeginAt> SymbolicSemantics::Policy< State, ValueType >::extract | ( | const ValueType< Len > & | a | ) | const [inline] |
Extracts certain bits from the specified value and shifts them to the low-order positions in the result.
The bits of the result include bits from BeginAt (inclusive) through EndAt (exclusive). The lsb is numbered zero.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::mem_read | ( | State< ValueType > & | state, | |
| const ValueType< 32 > & | addr | |||
| ) | const [inline] |
Reads a value from memory in a way that always returns the same value provided there are not intervening writes that would clobber the value either directly or by aliasing.
Also, if appropriate, the value is added to the original memory state (thus changing the value at that address from an implicit named value to an explicit named value).
It is safe to call this function and supply the policy's original state as the state argument.
The documentation for MemoryCell has an example that demonstrates the desired behavior of mem_read() and mem_write().
| MemRefType SymbolicSemantics::Policy< State, ValueType >::memory_reference_type | ( | const State< ValueType > & | state, | |
| const ValueType< 32 > & | addr | |||
| ) | const [inline] |
Determines if the specified address is related to the current stack or frame pointer.
This is used by mem_write() when we're operating under the assumption that memory written via stack pointer is different than memory written via frame pointer, and that memory written by either pointer is different than all other memory.
| void SymbolicSemantics::Policy< State, ValueType >::mem_write | ( | State< ValueType > & | state, | |
| const ValueType< 32 > & | addr, | |||
| const ValueType< Len > & | data | |||
| ) | [inline] |
Writes a value to memory.
If the address written to is an alias for other addresses then the other addresses will be clobbered. Subsequent reads from clobbered addresses will return new values. See also, mem_read().
| const RegisterDictionary* SymbolicSemantics::Policy< State, ValueType >::get_register_dictionary | ( | ) | const [inline] |
Returns the register dictionary.
| void SymbolicSemantics::Policy< State, ValueType >::set_register_dictionary | ( | const RegisterDictionary * | regdict | ) | [inline] |
Sets the register dictionary.
| void SymbolicSemantics::Policy< State, ValueType >::startInstruction | ( | SgAsmInstruction * | insn | ) | [inline] |
| void SymbolicSemantics::Policy< State, ValueType >::finishInstruction | ( | SgAsmInstruction * | ) | [inline] |
| ValueType<1> SymbolicSemantics::Policy< State, ValueType >::true_ | ( | ) | const [inline] |
True value.
| ValueType<1> SymbolicSemantics::Policy< State, ValueType >::false_ | ( | ) | const [inline] |
False value.
| ValueType<1> SymbolicSemantics::Policy< State, ValueType >::undefined_ | ( | ) | const [inline] |
Undefined Boolean.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::number | ( | uint64_t | n | ) | const [inline] |
Used to build a known constant.
| ValueType<32> SymbolicSemantics::Policy< State, ValueType >::filterCallTarget | ( | const ValueType< 32 > & | a | ) | const [inline] |
Called only for CALL instructions before assigning new value to IP register.
| ValueType<32> SymbolicSemantics::Policy< State, ValueType >::filterReturnTarget | ( | const ValueType< 32 > & | a | ) | const [inline] |
Called only for RET instructions before adjusting the IP register.
| ValueType<32> SymbolicSemantics::Policy< State, ValueType >::filterIndirectJumpTarget | ( | const ValueType< 32 > & | a | ) | const [inline] |
Called only for JMP instructions before adjusting the IP register.
| void SymbolicSemantics::Policy< State, ValueType >::hlt | ( | ) | [inline] |
Called only for the HLT instruction.
| void SymbolicSemantics::Policy< State, ValueType >::cpuid | ( | ) | [inline] |
Called only for the CPUID instruction.
| ValueType<64> SymbolicSemantics::Policy< State, ValueType >::rdtsc | ( | ) | [inline] |
Called only for the RDTSC instruction.
| void SymbolicSemantics::Policy< State, ValueType >::interrupt | ( | uint8_t | num | ) | [inline] |
Called only for the INT instruction.
| void SymbolicSemantics::Policy< State, ValueType >::sysenter | ( | ) | [inline] |
Called for SYSENTER instruction.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::add | ( | const ValueType< Len > & | a, | |
| const ValueType< Len > & | b | |||
| ) | const [inline] |
Adds two values.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::addWithCarries | ( | const ValueType< Len > & | a, | |
| const ValueType< Len > & | b, | |||
| const ValueType< 1 > & | c, | |||
| ValueType< Len > & | carry_out | |||
| ) | const [inline] |
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.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::and_ | ( | const ValueType< Len > & | a, | |
| const ValueType< Len > & | b | |||
| ) | const [inline] |
Computes bit-wise AND of two values.
| ValueType<1> SymbolicSemantics::Policy< State, ValueType >::equalToZero | ( | const ValueType< Len > & | a | ) | const [inline] |
Returns true_, false_, or undefined_ depending on whether argument is zero.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::invert | ( | const ValueType< Len > & | a | ) | const [inline] |
One's complement.
| ValueType<Len1+Len2> SymbolicSemantics::Policy< State, ValueType >::concat | ( | const ValueType< Len1 > & | a, | |
| const ValueType< Len2 > & | b | |||
| ) | const [inline] |
Concatenate the values of a and b so that the result has b in the high-order bits and a in the low order bits.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::ite | ( | const ValueType< 1 > & | sel, | |
| const ValueType< Len > & | ifTrue, | |||
| const ValueType< Len > & | ifFalse | |||
| ) | const [inline] |
Returns second or third arg depending on value of first arg.
"ite" means "if-then-else".
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::leastSignificantSetBit | ( | const ValueType< Len > & | a | ) | const [inline] |
Returns position of least significant set bit; zero when no bits are set.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::mostSignificantSetBit | ( | const ValueType< Len > & | a | ) | const [inline] |
Returns position of most significant set bit; zero when no bits are set.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::negate | ( | const ValueType< Len > & | a | ) | const [inline] |
Two's complement.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::or_ | ( | const ValueType< Len > & | a, | |
| const ValueType< Len > & | b | |||
| ) | const [inline] |
Computes bit-wise OR of two values.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::rotateLeft | ( | const ValueType< Len > & | a, | |
| const ValueType< SALen > & | sa | |||
| ) | const [inline] |
Rotate bits to the left.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::rotateRight | ( | const ValueType< Len > & | a, | |
| const ValueType< SALen > & | sa | |||
| ) | const [inline] |
Rotate bits to the right.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::shiftLeft | ( | const ValueType< Len > & | a, | |
| const ValueType< SALen > & | sa | |||
| ) | const [inline] |
Returns arg shifted left.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::shiftRight | ( | const ValueType< Len > & | a, | |
| const ValueType< SALen > & | sa | |||
| ) | const [inline] |
Returns arg shifted right logically (no sign bit).
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::shiftRightArithmetic | ( | const ValueType< Len > & | a, | |
| const ValueType< SALen > & | sa | |||
| ) | const [inline] |
Returns arg shifted right arithmetically (with sign bit).
| ValueType<To> SymbolicSemantics::Policy< State, ValueType >::signExtend | ( | const ValueType< From > & | a | ) | [inline] |
Sign extends a value.
| ValueType<Len1> SymbolicSemantics::Policy< State, ValueType >::signedDivide | ( | const ValueType< Len1 > & | a, | |
| const ValueType< Len2 > & | b | |||
| ) | const [inline] |
Divides two signed values.
| ValueType<Len2> SymbolicSemantics::Policy< State, ValueType >::signedModulo | ( | const ValueType< Len1 > & | a, | |
| const ValueType< Len2 > & | b | |||
| ) | const [inline] |
Calculates modulo with signed values.
| ValueType<Len1+Len2> SymbolicSemantics::Policy< State, ValueType >::signedMultiply | ( | const ValueType< Len1 > & | a, | |
| const ValueType< Len2 > & | b | |||
| ) | const [inline] |
Multiplies two signed values.
| ValueType<Len1> SymbolicSemantics::Policy< State, ValueType >::unsignedDivide | ( | const ValueType< Len1 > & | a, | |
| const ValueType< Len2 > & | b | |||
| ) | const [inline] |
Divides two unsigned values.
| ValueType<Len2> SymbolicSemantics::Policy< State, ValueType >::unsignedModulo | ( | const ValueType< Len1 > & | a, | |
| const ValueType< Len2 > & | b | |||
| ) | const [inline] |
Calculates modulo with unsigned values.
| ValueType<Len1+Len2> SymbolicSemantics::Policy< State, ValueType >::unsignedMultiply | ( | const ValueType< Len1 > & | a, | |
| const ValueType< Len2 > & | b | |||
| ) | const [inline] |
Multiply two unsigned values.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::xor_ | ( | const ValueType< Len > & | a, | |
| const ValueType< Len > & | b | |||
| ) | const [inline] |
Computes bit-wise XOR of two values.
| const RegisterDescriptor& SymbolicSemantics::Policy< State, ValueType >::findRegister | ( | const std::string & | regname, | |
| size_t | nbits = 0 | |||
| ) | [inline] |
Finds a register by name.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::readRegister | ( | const char * | regname | ) | [inline] |
Reads from a named register.
| void SymbolicSemantics::Policy< State, ValueType >::writeRegister | ( | const char * | regname, | |
| const ValueType< Len > & | value | |||
| ) | [inline] |
Writes to a named register.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::readRegister | ( | const RegisterDescriptor & | reg | ) | [inline] |
Generic register read.
| void SymbolicSemantics::Policy< State, ValueType >::writeRegister | ( | const RegisterDescriptor & | reg, | |
| const ValueType< Len > & | value | |||
| ) | [inline] |
Generic register write.
| ValueType<Len> SymbolicSemantics::Policy< State, ValueType >::readMemory | ( | X86SegmentRegister | segreg, | |
| const ValueType< 32 > & | addr, | |||
| const ValueType< 1 > & | cond | |||
| ) | const [inline] |
Reads a value from memory.
| void SymbolicSemantics::Policy< State, ValueType >::writeMemory | ( | X86SegmentRegister | segreg, | |
| const ValueType< 32 > & | addr, | |||
| const ValueType< Len > & | data, | |||
| const ValueType< 1 > & | cond | |||
| ) | [inline] |
Writes a value to memory.
| std::ostream& operator<< | ( | std::ostream & | o, | |
| const Policy< State, ValueType > & | p | |||
| ) | [friend] |
SgAsmInstruction* SymbolicSemantics::Policy< State, ValueType >::cur_insn [protected] |
Set by startInstruction(), cleared by finishInstruction().
State<ValueType> SymbolicSemantics::Policy< State, ValueType >::orig_state [mutable, protected] |
Original machine state, initialized by constructor and mem_write.
This data member is mutable because a mem_read() operation, although conceptually const, may cache the value that was read so that subsquent reads from the same address will return the same value. This member is initialized by the first call to startInstruction() (as called by X86InstructionSemantics::processInstruction()) which allows the user to initialize the original conditions using the same interface that's used to process instructions. In other words, if one wants the stack pointer to contain a specific original value, then one may initialize the stack pointer by calling writeGPR() before processing the first instruction.
State<ValueType> SymbolicSemantics::Policy< State, ValueType >::cur_state [mutable, protected] |
Current machine state updated by each processInstruction().
The instruction pointer is updated before we process each instruction. This data member is mutable because a mem_read() operation, although conceptually const, may cache the value that was read so that subsequent reads from the same address will return the same value.
bool SymbolicSemantics::Policy< State, ValueType >::p_discard_popped_memory [protected] |
Property that determines how the stack behaves.
When set, any time the stack pointer is adjusted, memory below the stack pointer and having the same address name as the stack pointer is removed (the memory location becomes undefined). The default is false, that is, no special treatment for the stack.
size_t SymbolicSemantics::Policy< State, ValueType >::ninsns [protected] |
Total number of instructions processed.
This is incremented by startInstruction(), which is the first thing called by X86InstructionSemantics::processInstruction().
SMTSolver* SymbolicSemantics::Policy< State, ValueType >::solver [protected] |
The solver to use for Satisfiability Modulo Theory, or NULL.
const RegisterDictionary* SymbolicSemantics::Policy< State, ValueType >::regdict [protected] |
Registers stored in the various State objects for this Policy.
This dictionary is used by the X86InstructionSemantics class to translate register names to register descriptors. For instance, to read from the "eax" register, the semantics will look up "eax" in the policy's register dictionary and then pass that descriptor to the policy's readRegister() method. Register descriptors are also stored in instructions then the instruction is disassembled, so the disassembler and policy should probably be using the same dictionary.
1.4.7