| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.SimplePred
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 Pred = Predicate (Map StatePart SimpleExpr) FlagStatus
- 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
- rock_bottom :: SimpleExpr
- pp_expr :: SimpleExpr -> [Char]
- pp_pred :: Pred -> String
- expr_size :: SimpleExpr -> Int
Documentation
A symbolic predicate consists of:
- A mapping from stateparts to symbolic expressions.
- The status of the flags.
- A set of verification conditions.
Constructors
| Predicate (Map StatePart SimpleExpr) FlagStatus |
Instances
| Eq Pred Source # | |
| Ord Pred Source # | |
| Show Pred Source # | |
| Generic Pred Source # | |
| Serialize Pred Source # | |
| Propagator FContext Pred Source # | |
| type Rep Pred Source # | |
Defined in Data.SimplePred type Rep Pred = D1 ('MetaData "Pred" "Data.SimplePred" "foxdec-0.1.0.0-KhdyLJGQiCJLT7iSdXA91t" 'False) (C1 ('MetaCons "Predicate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Map StatePart SimpleExpr)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 FlagStatus))) | |
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
| Eq StatePart Source # | |
| Ord StatePart Source # | |
| Show StatePart Source # | |
| Generic StatePart Source # | |
| Serialize StatePart Source # | |
| type Rep StatePart Source # | |
Defined in Data.SimplePred type Rep StatePart = D1 ('MetaData "StatePart" "Data.SimplePred" "foxdec-0.1.0.0-KhdyLJGQiCJLT7iSdXA91t" 'False) (C1 ('MetaCons "SP_StackPointer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String)) :+: (C1 ('MetaCons "SP_Reg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Register)) :+: C1 ('MetaCons "SP_Mem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 SimpleExpr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int)))) | |
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 [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 (Set SimpleExpr) | The expression evaluates to one of the expressions in the set |
| FromPointerBases (Set PointerBase) | The expression is a pointer-computation with known base(s) |
| FromCall String | Return value of a function call |
| FromSources (Set BotSrc) | The expression is some computation based on sources. |
| FromOverlap (Set BotSrc) | A read from two possibly overlapping regions |
| FromMemWrite (Set BotSrc) | A write to two possibly overlapping regions |
| FromSemantics (Set BotSrc) | An instruction with unknown semantics |
| FromBitMode (Set BotSrc) | Should not happen, but if a register writes to a registeralias with unknown bit size |
| FromUninitializedMemory (Set 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 |
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.
Constructors
| Minus Int | |
| Plus Int | |
| Times Int | |
| And Int | |
| Or Int | |
| Xor Int | |
| Not Int | |
| SetXX | |
| Bsr Int | |
| Div_Rem Int | |
| Div Int | |
| Shl Int | |
| Shr Int | |
| Sar Int | |
| Udiv Int | |
| Ror Int | |
| Rol Int | |
| Bswap Int | |
| Pextr Int |
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. |
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 #
Do all occurences of Bottom satisfy the given predicate?
simp :: SimpleExpr -> SimpleExpr Source #
Simplification of symbolic expressions.
Must always produce an expression logically equivalent to the original.
TODO: overwrite(8,Bot[src|RSP_0x1000070ec,malloc100007204()|],b8(Bot[m|RSP_0x1000070ec,malloc100007204()|]))
rock_bottom :: SimpleExpr Source #
The lowest botom element
pp_expr :: SimpleExpr -> [Char] Source #
Pretty print expression, showing Bottom expressions only as Bot
expr_size :: SimpleExpr -> Int Source #