foxdec-0.1.0.0: Formally Verified x86-64 Decompilation
Safe HaskellNone
LanguageHaskell2010

Data.SValue

Description

 
Synopsis

Documentation

data PtrOffset Source #

A `pointer value` may have a `pointer offset` that is either a known fixed immediate or unknown

Constructors

PtrOffset Word64 
UnknownOffset 

Instances

Instances details
Eq PtrOffset Source # 
Instance details

Defined in Data.SValue

Methods

(==) :: PtrOffset -> PtrOffset -> Bool #

(/=) :: PtrOffset -> PtrOffset -> Bool #

Ord PtrOffset Source # 
Instance details

Defined in Data.SValue

Methods

compare :: PtrOffset -> PtrOffset -> Ordering #

(<) :: PtrOffset -> PtrOffset -> Bool #

(<=) :: PtrOffset -> PtrOffset -> Bool #

(>) :: PtrOffset -> PtrOffset -> Bool #

(>=) :: PtrOffset -> PtrOffset -> Bool #

max :: PtrOffset -> PtrOffset -> PtrOffset #

min :: PtrOffset -> PtrOffset -> PtrOffset #

Show PtrOffset Source # 
Instance details

Defined in Data.SValue

Methods

showsPrec :: Int -> PtrOffset -> ShowS #

show :: PtrOffset -> String #

showList :: [PtrOffset] -> ShowS #

Generic PtrOffset Source # 
Instance details

Defined in Data.SValue

Associated Types

type Rep PtrOffset :: Type -> Type #

Methods

from :: PtrOffset -> Rep PtrOffset x #

to :: Rep PtrOffset x -> PtrOffset #

ToJSON PtrOffset Source # 
Instance details

Defined in OutputGeneration.JSON

Methods

toJSON :: PtrOffset -> Value #

toEncoding :: PtrOffset -> Encoding #

toJSONList :: [PtrOffset] -> Value #

toEncodingList :: [PtrOffset] -> Encoding #

Serialize PtrOffset Source #

A `symbolic value` is either a `pointer value` (high certainty that it is actually a pointer), or a non-deterministic set of concrete expressions, or computed from a set of possible addends. data SValue = SPointer (NES.NESet PtrValue) | SConcrete (NES.NESet SimpleExpr) | SAddends (NES.NESet SAddend) | Top deriving (Eq,Ord,Generic)

Instance details

Defined in Data.SValue

Methods

put :: Putter PtrOffset #

get :: Get PtrOffset #

NFData PtrOffset Source # 
Instance details

Defined in Data.SValue

Methods

rnf :: PtrOffset -> () #

type Rep PtrOffset Source # 
Instance details

Defined in Data.SValue

type Rep PtrOffset = D1 ('MetaData "PtrOffset" "Data.SValue" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "PtrOffset" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Word64)) :+: C1 ('MetaCons "UnknownOffset" 'PrefixI 'False) (U1 :: Type -> Type))

data SPointer Source #

A `pointer value` consists of a `pointer base` and a `pointer offset`

Constructors

Base_StackPointer String PtrOffset

The stackpointer of the given function

Base_Immediate Word64 PtrOffset

An immediate pointer

Base_Malloc (Maybe Word64) (Maybe String) PtrOffset

A malloc return value

Base_FunctionPtr Word64 String PtrOffset

A function pointer (external)

Base_ReturnAddr String

The return address of the given function

Base_TLS PtrOffset

The Thread Local Storage

Base_StatePart StatePart PtrOffset

The value initially stored in some statepart

Base_FunctionReturn String PtrOffset

The return value of a function

Instances

Instances details
Eq SPointer Source # 
Instance details

Defined in Data.SValue

Methods

(==) :: SPointer -> SPointer -> Bool #

(/=) :: SPointer -> SPointer -> Bool #

Ord SPointer Source # 
Instance details

Defined in Data.SValue

Methods

compare :: SPointer -> SPointer -> Ordering #

(<) :: SPointer -> SPointer -> Bool #

(<=) :: SPointer -> SPointer -> Bool #

(>) :: SPointer -> SPointer -> Bool #

(>=) :: SPointer -> SPointer -> Bool #

max :: SPointer -> SPointer -> SPointer #

min :: SPointer -> SPointer -> SPointer #

Show SPointer Source # 
Instance details

Defined in Data.SValue

Methods

showsPrec :: Int -> SPointer -> ShowS #

show :: SPointer -> String #

showList :: [SPointer] -> ShowS #

Generic SPointer Source # 
Instance details

Defined in Data.SValue

Associated Types

type Rep SPointer :: Type -> Type #

Methods

from :: SPointer -> Rep SPointer x #

to :: Rep SPointer x -> SPointer #

ToJSON SPointer Source # 
Instance details

Defined in OutputGeneration.JSON

Methods

toJSON :: SPointer -> Value #

toEncoding :: SPointer -> Encoding #

toJSONList :: [SPointer] -> Value #

toEncodingList :: [SPointer] -> Encoding #

Serialize SPointer Source # 
Instance details

Defined in Data.SValue

Methods

put :: Putter SPointer #

get :: Get SPointer #

NFData SPointer Source # 
Instance details

Defined in Data.SValue

Methods

rnf :: SPointer -> () #

Propagator FContext Predicate Source # 
Instance details

Defined in Instantiation.SymbolicPropagation

Methods

tau :: FContext -> [Instruction] -> Maybe [Instruction] -> Predicate -> (Predicate, Set VerificationCondition) Source #

join :: FContext -> String -> Predicate -> Predicate -> Predicate Source #

implies :: FContext -> Predicate -> Predicate -> Bool Source #

SymbolicExecutable FContext SValue SPointer Source # 
Instance details

Defined in Instantiation.SymbolicPropagation

Methods

sseparate :: FContext -> String -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

senclosed :: FContext -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

salias :: FContext -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

ssensitive :: FContext -> SPointer -> RegionSize -> SValue -> Bool Source #

sread_from_ro_data :: FContext -> SPointer -> RegionSize -> Maybe SValue Source #

smk_mem_addresses :: FContext -> String -> SValue -> Set SPointer Source #

sjoin_values :: Foldable t => FContext -> String -> t SValue -> SValue Source #

swiden_values :: FContext -> String -> SValue -> SValue Source #

sjoin_pointers :: FContext -> [SPointer] -> [SPointer] Source #

top :: FContext -> String -> SValue Source #

ssemantics :: FContext -> String -> SymbolicOperation SValue -> SValue Source #

sflg_semantics :: FContext -> SValue -> Instruction -> FlagStatus -> FlagStatus Source #

simmediate :: Integral i => FContext -> i -> SValue Source #

smk_init_reg_value :: FContext -> Register -> SValue Source #

smk_init_mem_value :: FContext -> String -> SPointer -> RegionSize -> SValue Source #

scall :: FContext -> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) () Source #

sjump :: FContext -> Instruction -> State (Sstate SValue SPointer, VCS) () Source #

stry_jump_targets :: FContext -> SValue -> Maybe (Set ResolvedJumpTarget) Source #

stry_immediate :: FContext -> SValue -> Maybe Word64 Source #

stry_deterministic :: FContext -> SValue -> Maybe SimpleExpr Source #

stry_relocation :: FContext -> SPointer -> RegionSize -> Maybe SValue Source #

saddress_has_instruction :: FContext -> Word64 -> Bool Source #

type Rep SPointer Source # 
Instance details

Defined in Data.SValue

type Rep SPointer = D1 ('MetaData "SPointer" "Data.SValue" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (((C1 ('MetaCons "Base_StackPointer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 PtrOffset)) :+: C1 ('MetaCons "Base_Immediate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 PtrOffset))) :+: (C1 ('MetaCons "Base_Malloc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Maybe Word64)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Maybe String)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 PtrOffset))) :+: C1 ('MetaCons "Base_FunctionPtr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Word64) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 PtrOffset))))) :+: ((C1 ('MetaCons "Base_ReturnAddr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String)) :+: C1 ('MetaCons "Base_TLS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 PtrOffset))) :+: (C1 ('MetaCons "Base_StatePart" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 StatePart) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 PtrOffset)) :+: C1 ('MetaCons "Base_FunctionReturn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 PtrOffset)))))

data SAddend Source #

A `pointer addend` consists of a `pointer base`, some constant relativ to the initial state, or the return value of some function.

Constructors

SAddend_StackPointer String 
SAddend_Immediate Word64 
SAddend_Malloc (Maybe Word64) (Maybe String) 
SAddend_FunctionPtr Word64 String 
SAddend_ReturnAddr String 
SAddend_TLS 
SAddend_StatePart StatePart 
SAddend_FunctionReturn String 

Instances

Instances details
Eq SAddend Source # 
Instance details

Defined in Data.SValue

Methods

(==) :: SAddend -> SAddend -> Bool #

(/=) :: SAddend -> SAddend -> Bool #

Ord SAddend Source # 
Instance details

Defined in Data.SValue

Methods

compare :: SAddend -> SAddend -> Ordering #

(<) :: SAddend -> SAddend -> Bool #

(<=) :: SAddend -> SAddend -> Bool #

(>) :: SAddend -> SAddend -> Bool #

(>=) :: SAddend -> SAddend -> Bool #

max :: SAddend -> SAddend -> SAddend #

min :: SAddend -> SAddend -> SAddend #

Show SAddend Source # 
Instance details

Defined in Data.SValue

Methods

showsPrec :: Int -> SAddend -> ShowS #

show :: SAddend -> String #

showList :: [SAddend] -> ShowS #

Generic SAddend Source # 
Instance details

Defined in Data.SValue

Associated Types

type Rep SAddend :: Type -> Type #

Methods

from :: SAddend -> Rep SAddend x #

to :: Rep SAddend x -> SAddend #

ToJSON SAddend Source # 
Instance details

Defined in OutputGeneration.JSON

Methods

toJSON :: SAddend -> Value #

toEncoding :: SAddend -> Encoding #

toJSONList :: [SAddend] -> Value #

toEncodingList :: [SAddend] -> Encoding #

Serialize SAddend Source # 
Instance details

Defined in Data.SValue

Methods

put :: Putter SAddend #

get :: Get SAddend #

NFData SAddend Source # 
Instance details

Defined in Data.SValue

Methods

rnf :: SAddend -> () #

type Rep SAddend Source # 
Instance details

Defined in Data.SValue

type Rep SAddend = D1 ('MetaData "SAddend" "Data.SValue" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (((C1 ('MetaCons "SAddend_StackPointer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String)) :+: C1 ('MetaCons "SAddend_Immediate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Word64))) :+: (C1 ('MetaCons "SAddend_Malloc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Maybe Word64)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Maybe String))) :+: C1 ('MetaCons "SAddend_FunctionPtr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String)))) :+: ((C1 ('MetaCons "SAddend_ReturnAddr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String)) :+: C1 ('MetaCons "SAddend_TLS" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SAddend_StatePart" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 StatePart)) :+: C1 ('MetaCons "SAddend_FunctionReturn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String)))))

data SValue Source #

Constructors

SConcrete (NESet SimpleExpr) 
SAddends (NESet (NESet SAddend)) 
Top 

Instances

Instances details
Eq SValue Source # 
Instance details

Defined in Data.SValue

Methods

(==) :: SValue -> SValue -> Bool #

(/=) :: SValue -> SValue -> Bool #

Ord SValue Source # 
Instance details

Defined in Data.SValue

Methods

compare :: SValue -> SValue -> Ordering #

(<) :: SValue -> SValue -> Bool #

(<=) :: SValue -> SValue -> Bool #

(>) :: SValue -> SValue -> Bool #

(>=) :: SValue -> SValue -> Bool #

max :: SValue -> SValue -> SValue #

min :: SValue -> SValue -> SValue #

Show SValue Source # 
Instance details

Defined in Data.SValue

Methods

showsPrec :: Int -> SValue -> ShowS #

show :: SValue -> String #

showList :: [SValue] -> ShowS #

Generic SValue Source # 
Instance details

Defined in Data.SValue

Associated Types

type Rep SValue :: Type -> Type #

Methods

from :: SValue -> Rep SValue x #

to :: Rep SValue x -> SValue #

ToJSON SValue Source # 
Instance details

Defined in OutputGeneration.JSON

Methods

toJSON :: SValue -> Value #

toEncoding :: SValue -> Encoding #

toJSONList :: [SValue] -> Value #

toEncodingList :: [SValue] -> Encoding #

Serialize SValue Source # 
Instance details

Defined in Data.SValue

Methods

put :: Putter SValue #

get :: Get SValue #

NFData SValue Source # 
Instance details

Defined in Data.SValue

Methods

rnf :: SValue -> () #

Propagator FContext Predicate Source # 
Instance details

Defined in Instantiation.SymbolicPropagation

Methods

tau :: FContext -> [Instruction] -> Maybe [Instruction] -> Predicate -> (Predicate, Set VerificationCondition) Source #

join :: FContext -> String -> Predicate -> Predicate -> Predicate Source #

implies :: FContext -> Predicate -> Predicate -> Bool Source #

SymbolicExecutable FContext SValue SPointer Source # 
Instance details

Defined in Instantiation.SymbolicPropagation

Methods

sseparate :: FContext -> String -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

senclosed :: FContext -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

salias :: FContext -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

ssensitive :: FContext -> SPointer -> RegionSize -> SValue -> Bool Source #

sread_from_ro_data :: FContext -> SPointer -> RegionSize -> Maybe SValue Source #

smk_mem_addresses :: FContext -> String -> SValue -> Set SPointer Source #

sjoin_values :: Foldable t => FContext -> String -> t SValue -> SValue Source #

swiden_values :: FContext -> String -> SValue -> SValue Source #

sjoin_pointers :: FContext -> [SPointer] -> [SPointer] Source #

top :: FContext -> String -> SValue Source #

ssemantics :: FContext -> String -> SymbolicOperation SValue -> SValue Source #

sflg_semantics :: FContext -> SValue -> Instruction -> FlagStatus -> FlagStatus Source #

simmediate :: Integral i => FContext -> i -> SValue Source #

smk_init_reg_value :: FContext -> Register -> SValue Source #

smk_init_mem_value :: FContext -> String -> SPointer -> RegionSize -> SValue Source #

scall :: FContext -> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) () Source #

sjump :: FContext -> Instruction -> State (Sstate SValue SPointer, VCS) () Source #

stry_jump_targets :: FContext -> SValue -> Maybe (Set ResolvedJumpTarget) Source #

stry_immediate :: FContext -> SValue -> Maybe Word64 Source #

stry_deterministic :: FContext -> SValue -> Maybe SimpleExpr Source #

stry_relocation :: FContext -> SPointer -> RegionSize -> Maybe SValue Source #

saddress_has_instruction :: FContext -> Word64 -> Bool Source #

type Rep SValue Source # 
Instance details

Defined in Data.SValue

type Rep SValue = D1 ('MetaData "SValue" "Data.SValue" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "SConcrete" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (NESet SimpleExpr))) :+: (C1 ('MetaCons "SAddends" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (NESet (NESet SAddend)))) :+: C1 ('MetaCons "Top" 'PrefixI 'False) (U1 :: Type -> Type)))

show_set :: [[Char]] -> [Char] Source #

isImmediateBase :: SAddend -> Bool Source #

isConcrete :: SValue -> Bool Source #

has_unknown_offset :: SPointer -> Bool Source #

liftOffsetMod :: (Word64 -> Word64) -> PtrOffset -> PtrOffset Source #

mod_offset :: (Word64 -> Word64) -> SPointer -> SPointer Source #