| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.SymbolicExpression
Description
A datatype for symbolic predicates, tailored to storing information on equalities between the current values stored in state parts (lhs) and constant expressions (rhs).
Synopsis
- data StatePart
- data SimpleExpr
- data FlagStatus
- data BotTyp
- data BotSrc
- data Operator
- data PointerBase
- is_immediate :: SimpleExpr -> Bool
- is_mem_sp :: StatePart -> Bool
- is_reg_sp :: StatePart -> Bool
- contains_bot :: SimpleExpr -> Bool
- contains_bot_sp :: StatePart -> Bool
- all_bot_satisfy :: (BotTyp -> Bool) -> SimpleExpr -> Bool
- simp :: SimpleExpr -> SimpleExpr
- pp_expr :: SimpleExpr -> [Char]
- expr_size :: SimpleExpr -> Int
- sextend_32_64 :: (Bits p, Num p) => p -> p
- sextend_16_64 :: (Bits p, Num p) => p -> p
- sextend_8_64 :: (Bits p, Num p) => p -> p
Documentation
A statepart is either a register or a region in memory
Constructors
| SP_StackPointer String | The stack pointer of the given function |
| SP_Reg Register | A register |
| SP_Mem SimpleExpr Int | A region with a symbolic address and an immediate size. |
Instances
data SimpleExpr Source #
A symbolic expression with as leafs either immediates, variables, live values of stateparts, or malloced addresses. A variable is a constant representing some initial value, e.g., RDI_0, or [RSP_0,8]_0. A statepart evaluates to its current value, e.g., RDI or [RSP,8].
Constructors
| SE_Immediate Word64 | An immediate word |
| SE_Var StatePart | A variable representing the initial value stored in the statepart (e.g., RSP0) |
| SE_StatePart StatePart | The value stored currently in the statepart |
| SE_Malloc (Maybe Word64) (Maybe String) | A malloc return value with possibly an ID |
| SE_Op Operator Int [SimpleExpr] | Application of an |
| SE_Bit Int SimpleExpr | Taking the lower bits of a value |
| SE_SExtend Int Int SimpleExpr | Sign extension |
| SE_Overwrite Int SimpleExpr SimpleExpr | Overwriting certain bits of a value with bits from another value |
| Bottom BotTyp | Bottom (unknown value) |
Instances
data FlagStatus Source #
Symbolically represent the status of all flags in the current state
Constructors
| None | No information known, flags could have any value |
| FS_CMP (Maybe Bool) Operand Operand | The flags are set by the x86 CMP instruction applied to the given operands. |
Instances
Bot represents an unknown (bottom) value. We annotate each occurence of Bot with a BotTyp. This type indicates where the bottom value originates from. The latter six are all equal, we just use them for debugging and information. They indicate that the value is unknown, but was computed using the set of sources.
Constructors
| FromNonDeterminism (NESet SimpleExpr) | The expression evaluates to one of the expressions in the set |
| FromPointerBases (NESet PointerBase) | The expression is a pointer-computation with known base(s) |
| FromCall String | Return value of a function call |
| FromSources (NESet BotSrc) | The expression is some computation based on sources. |
| FromOverlap (NESet BotSrc) | A read from two possibly overlapping regions |
| FromMemWrite (NESet BotSrc) | A write to two possibly overlapping regions |
| FromSemantics (NESet BotSrc) | An instruction with unknown semantics |
| FromBitMode (NESet BotSrc) | Should not happen, but if a register writes to a registeralias with unknown bit size |
| FromUninitializedMemory (NESet BotSrc) | Reading from memory not written to yet |
Instances
Sources that may be used to compute an expression. That is, the inputs to an expression.
Constructors
| Src_Var StatePart | An initial variable, i.e., a constant |
| Src_StackPointer String | The stack pointer of the given function |
| Src_Malloc (Maybe Word64) (Maybe String) | A malloced address |
| Src_ImmediateAddress Word64 | An immediate used in the computation of the pointer |
| Src_Function String | A return value from a function |
| Src_Mem (NESet BotSrc) | reading from memory |
| Src_ImmediateConstants | Some immediate value |
Instances
An operator is a pure operation over bit-vectors, annotated with the bit-size of its operands.
For example, Plus 64 denotes 64-bit addition.
Udiv and Times are operators op type w -> w -> w with all words same length.
Div and Div_Rem are operators of type w -> w -> w -> w performing concatenation of the first two words and then doing division/remainder.
Instances
data PointerBase Source #
A pointerbase is a positive addend of a symbolic expression that may represent a pointer.
Constructors
| StackPointer String | The stack frame of the given function |
| Malloc (Maybe Word64) (Maybe String) | A malloc (at the heap) at a given address (hash is unused for now) |
| GlobalAddress Word64 | A global address in the range of the sections of the binary. |
| PointerToSymbol Word64 String | An address with an associated symbol. |
| ThreadLocalStorage | A pointer to the thread-local-storage (e.g., FS register) |
Instances
is_immediate :: SimpleExpr -> Bool Source #
Returns true iff the expression is an immediate value
contains_bot :: SimpleExpr -> Bool Source #
Returns true iff the expression contains Bot
contains_bot_sp :: StatePart -> Bool Source #
Returns true iff the statepart contains Bot
all_bot_satisfy :: (BotTyp -> Bool) -> SimpleExpr -> Bool Source #
concatMap function p over all bottom values in the expression
simp :: SimpleExpr -> SimpleExpr Source #
Simplification of symbolic expressions.
Must always produce an expression logically equivalent to the original.
pp_expr :: SimpleExpr -> [Char] Source #
Pretty print expression, showing Bottom expressions only as Bot
expr_size :: SimpleExpr -> Int Source #
sextend_32_64 :: (Bits p, Num p) => p -> p Source #
Sign-extension from 32 to 64 bits
sextend_16_64 :: (Bits p, Num p) => p -> p Source #
Sign-extension from 16 to 64 bits
sextend_8_64 :: (Bits p, Num p) => p -> p Source #
Sign-extension from 8 to 64 bits