foxdec-0.1.0.0: Formally Verified x86-64 Decompilation
Safe HaskellSafe-Inferred
LanguageHaskell2010

WithNoAbstraction.SymbolicExecution

Description

 
Synopsis

Documentation

type Static bin v = LiftingEntry bin (Sstate SValue SPointer) (FInit SValue SPointer) v Source #

traceTop :: p -> a -> a Source #

mk_top :: String -> SValue Source #

ctry_immediate :: SValue -> Maybe Word64 Source #

cis_deterministic :: SValue -> Bool Source #

mk_concrete :: BinaryClass bin => Static bin v -> String -> NESet SimpleExpr -> SValue Source #

mk_concreteS :: BinaryClass bin => Static bin v -> SimpleExpr -> SValue Source #

mk_saddends :: BinaryClass bin => (bin, Config, L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64) -> NESet SimpleExpr -> SValue Source #

group_immediates :: BinaryClass bin => Static bin v -> NESet SimpleExpr -> NESet SimpleExpr Source #

cimmediate :: (Integral i, BinaryClass bin) => Static bin v -> i -> SValue Source #

cwiden :: BinaryClass bin => Static bin v -> String -> SValue -> SValue Source #

expr_to_addends :: BinaryClass bin => Static bin v -> SimpleExpr -> [SimpleExpr] Source #

cjoin :: BinaryClass bin => (bin, Config, L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64) -> [Char] -> SValue -> SValue -> SValue Source #

cjoin_all :: Foldable t => BinaryClass bin => Static bin v -> String -> t SValue -> SValue Source #

cjoin_pointers :: BinaryClass bin => Static bin v -> [SPointer] -> [SPointer] Source #

mk_expr :: BinaryClass bin => Static bin v -> SimpleExpr -> SimpleExpr Source #

svalue_plus :: BinaryClass bin => Static bin v -> Int -> SValue -> SValue -> SValue Source #

svalue_minus :: BinaryClass bin => Static bin v -> Int -> SValue -> SValue -> SValue Source #

svalue_and :: BinaryClass bin => Static bin v -> Int -> SValue -> SValue -> SValue Source #

svalue_unop :: BinaryClass bin => Static bin v -> String -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue Source #

svalue_takebits :: BinaryClass bin => Static bin v -> Int -> SValue -> SValue Source #

svalue_sextend :: BinaryClass bin => Static bin v -> Int -> Int -> SValue -> SValue Source #

svalue_apply :: BinaryClass bin => Static bin v -> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue Source #

data CSemantics Source #

Constructors

ApplyPlus Int 
ApplyMinus Int 
ApplyNeg Int 
ApplyDec Int 
ApplyInc Int 
ApplyAnd Int 
ApplyMov 
ApplyCMov 
ApplySExtend Int Int 
Apply ([SimpleExpr] -> SimpleExpr) 
SetXX 
SExtension_HI 
NoSemantics 

csemantics :: BinaryClass bin => Static bin v -> String -> SymbolicOperation SValue -> SValue Source #

mnemonic_to_semantics :: Opcode -> Int -> Maybe Int -> CSemantics Source #

replace_rip_in_operand :: Integral a => a -> Operand -> Operand Source #

cflg_semantics :: BinaryClass bin => Static bin v -> a -> Instruction -> FlagStatus -> FlagStatus Source #

try_get_base :: BinaryClass bin => Static bin v -> SimpleExpr -> Maybe SimpleExpr Source #

base_to_expr :: PointerBase -> SimpleExpr Source #

cmk_mem_addresses :: BinaryClass bin => Static bin v -> String -> SValue -> Set SPointer Source #

cmk_init_reg_value :: BinaryClass bin => Static bin v -> Register -> SValue Source #

cmk_init_mem_value :: BinaryClass bin => Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue Source #

cseparate :: BinaryClass bin => Static bin v -> String -> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool Source #

lookup_finit :: Integral a => (a, b, L0 pred finit v, a) -> finit Source #

calias :: (Eq a, Eq a) => p -> a -> a -> a -> a -> Bool Source #

cnecessarily_enclosed :: p -> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool Source #

csensitive :: BinaryClass p => (p, b, c, d) -> SPointer -> Maybe ByteSize -> SValue -> Bool Source #

cread_from_ro_data :: BinaryClass bin => Static bin v -> SPointer -> Maybe ByteSize -> Maybe SValue Source #

cis_local :: BinaryClass bin => (bin, b, c, d) -> SPointer -> Bool Source #

ckeep_for_finit :: BinaryClass bin => (bin, Config, L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64) -> SStatePart SPointer -> SValue -> Maybe (Set SPointer) Source #

is_function_pointer :: BinaryClass p => p -> SValue -> Bool Source #

check_regs_in_postcondition :: BinaryClass bin => Static bin v -> SValue -> SValue -> Bool Source #

ctry_resolve_error_call :: BinaryClass bin => (bin, Config, L0 pred finit v, d) -> Instruction -> SValue -> Maybe Indirection Source #

mapMaybeS :: Ord b => (a -> Maybe b) -> Set a -> Set b Source #

mapMaybeNES :: Ord b => (a -> Maybe b) -> NESet a -> Set b Source #

data ExternalFunctionOutput Source #

Constructors

FreshPointer 
UnknownReturnValue 
Input Register 

data ExternalFunctionBehavior Source #

Constructors

ExternalFunctionBehavior 

Fields

param :: (Eq a, Num a) => a -> Register Source #

pure_and_fresh :: ExternalFunctionBehavior Source #

pure_and_unknown :: ExternalFunctionBehavior Source #

external_function_behavior :: String -> ExternalFunctionBehavior Source #

a list of some function that return a heap-pointer through RAX. The pointer is assumed to be fresh.

transpose_bw_svalue :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> SValue -> SValue Source #

Backward transposition Let p be the current predicate and let the equality sp == v be from the predicate after execution of an internal function. For example, p contains: RSP == RSP0 - 64 RSI == 10

And after execution of the function, we have: *[RSP0+16,8] == RSI0

Transposing this equality produces: *[RSP0-40,8] == 10

transpose_bw_addends :: BinaryClass bin => (bin, Config, L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64) -> Sstate SValue SPointer -> SimpleExpr -> SValue Source #

transpose_bw_spointer :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> SPointer -> Set SPointer Source #

transpose_bw_reg :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> (Register, SValue) -> Maybe (Register, SValue) Source #

transpose_bw_mem :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> ((SPointer, Maybe ByteSize), SValue) -> [((SPointer, Maybe ByteSize), SValue)] Source #

transpose_bw_e :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue Source #

transpose_bw_sp :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> StatePart -> SValue Source #

data FunctionType Source #

Constructors

AnalyzedInternalFunction (Sstate SValue SPointer) 
ExternalFunction 
AnalyzedInternalFunctionTerminates 
AnalyzedInternalFunctionUnknown 

get_function_type :: BinaryClass bin => Static bin v -> Instruction -> String -> FunctionType Source #

call :: BinaryClass bin => Static bin v -> Instruction -> State (Sstate SValue SPointer, VCS SValue) () Source #

Executes semantics for external functions.

is_top_stackframe :: SimpleExpr -> Maybe ByteSize -> Bool Source #

jump :: BinaryClass bin => Static bin v -> Instruction -> State (Sstate SValue SPointer, VCS SValue) () Source #

ctry_jump_targets :: BinaryClass bin => Static bin v -> SValue -> Maybe (Set ResolvedJumpTarget) Source #

Orphan instances

BinaryClass bin => WithAbstractSymbolicValues (Static bin v) SValue SPointer Source # 
Instance details

Methods

sseparate :: Static bin v -> String -> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool Source #

senclosed :: Static bin v -> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool Source #

salias :: Static bin v -> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool Source #

ssensitive :: Static bin v -> SPointer -> Maybe ByteSize -> SValue -> Bool Source #

sread_from_ro_data :: Static bin v -> SPointer -> Maybe ByteSize -> Maybe SValue Source #

smk_mem_addresses :: Static bin v -> String -> SValue -> Set SPointer Source #

sjoin_values :: Foldable t => Static bin v -> String -> t SValue -> SValue Source #

swiden_values :: Static bin v -> String -> SValue -> SValue Source #

sjoin_pointers :: Static bin v -> [SPointer] -> [SPointer] Source #

top :: Static bin v -> String -> SValue Source #

ssemantics :: Static bin v -> String -> SymbolicOperation SValue -> SValue Source #

sflg_semantics :: Static bin v -> SValue -> Instruction -> FlagStatus -> FlagStatus Source #

simmediate :: Integral i => Static bin v -> i -> SValue Source #

smk_init_reg_value :: Static bin v -> Register -> SValue Source #

smk_init_mem_value :: Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue Source #

scall :: Static bin v -> Instruction -> State (Sstate SValue SPointer, VCS SValue) () Source #

sjump :: Static bin v -> Instruction -> State (Sstate SValue SPointer, VCS SValue) () Source #

saddress_has_instruction :: Static bin v -> Word64 -> Bool Source #

skeep_for_finit :: Static bin v -> SStatePart SPointer -> SValue -> Maybe (Set SPointer) Source #

stry_jump_targets :: Static bin v -> SValue -> Maybe (Set ResolvedJumpTarget) Source #

stry_resolve_error_call :: Static bin v -> Instruction -> SValue -> Maybe Indirection Source #

stry_immediate :: Static bin v -> SValue -> Maybe Word64 Source #

sis_deterministic :: Static bin v -> SValue -> Bool Source #

scheck_regs_in_postcondition :: Static bin v -> SValue -> SValue -> Bool Source #