Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.L0

Documentation

data Postcondition pred Source #

Constructors

ReturnsWith pred
HasUnresolvedIndirections [Int]
Terminates
TimeOut
VerificationError [(Int, pred)]

Instances

Instances details

Generic (Postcondition pred) Source #
Instance details Defined in Data.L0 Associated Types type Rep (Postcondition pred) :: Type -> Type # Methods from :: Postcondition pred -> Rep (Postcondition pred) x # to :: Rep (Postcondition pred) x -> Postcondition pred #
Show pred => Show (Postcondition pred) Source #
Instance details Defined in Data.L0 Methods showsPrec :: Int -> Postcondition pred -> ShowS # show :: Postcondition pred -> String # showList :: [Postcondition pred] -> ShowS #
Serialize pred => Serialize (Postcondition pred) Source #
Instance details Defined in Data.L0 Methods put :: Putter (Postcondition pred) # get :: Get (Postcondition pred) #
NFData pred => NFData (Postcondition pred) Source #
Instance details Defined in Data.L0 Methods rnf :: Postcondition pred -> () #
Eq pred => Eq (Postcondition pred) Source #
Instance details Defined in Data.L0 Methods (==) :: Postcondition pred -> Postcondition pred -> Bool # (/=) :: Postcondition pred -> Postcondition pred -> Bool #
type Rep (Postcondition pred) Source #
Instance details Defined in Data.L0 type Rep (Postcondition pred) = D1 ('MetaData "Postcondition" "Data.L0" "foxdec-0.1.0.0-DGuc5MMkhbvOBLAebyTd5" 'False) ((C1 ('MetaCons "ReturnsWith" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 pred)) :+: C1 ('MetaCons "HasUnresolvedIndirections" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int]))) :+: (C1 ('MetaCons "Terminates" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TimeOut" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VerificationError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Int, pred)])))))

data FResult pred v Source #

Constructors

FResult
Fields result_cfg :: CFG result_post :: Postcondition pred result_calls :: Set Word64 result_vcs :: Set (VerificationCondition v) result_pa :: IntMap (PointerAnalysisResult v)

Instances

Instances details

Generic (FResult pred v) Source #
Instance details Defined in Data.L0 Associated Types type Rep (FResult pred v) :: Type -> Type # Methods from :: FResult pred v -> Rep (FResult pred v) x # to :: Rep (FResult pred v) x -> FResult pred v #
(Serialize v, Serialize pred, Ord v) => Serialize (FResult pred v) Source #
Instance details Defined in Data.L0 Methods put :: Putter (FResult pred v) # get :: Get (FResult pred v) #
(NFData v, NFData pred) => NFData (FResult pred v) Source #
Instance details Defined in Data.L0 Methods rnf :: FResult pred v -> () #
type Rep (FResult pred v) Source #
Instance details Defined in Data.L0 type Rep (FResult pred v) = D1 ('MetaData "FResult" "Data.L0" "foxdec-0.1.0.0-DGuc5MMkhbvOBLAebyTd5" 'False) (C1 ('MetaCons "FResult" 'PrefixI 'True) ((S1 ('MetaSel ('Just "result_cfg") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CFG) :: S1 ('MetaSel ('Just "result_post") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Postcondition pred))) :: (S1 ('MetaSel ('Just "result_calls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Word64)) :: (S1 ('MetaSel ('Just "result_vcs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set (VerificationCondition v))) :: S1 ('MetaSel ('Just "result_pa") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IntMap (PointerAnalysisResult v)))))))

data L0 pred finit v Source #

Constructors

L0
Fields l0_functions :: IntMap (finit, Maybe (FResult pred v)) l0_indirections :: IntMap Indirections l0_time :: String

Instances

Instances details

BinaryClass bin => WithAbstractSymbolicValues (Static bin v) SValue SPointer Source #
Instance details Defined in WithNoAbstraction.SymbolicExecution 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 #
Generic (L0 pred finit v) Source #
Instance details Defined in Data.L0 Associated Types type Rep (L0 pred finit v) :: Type -> Type # Methods from :: L0 pred finit v -> Rep (L0 pred finit v) x # to :: Rep (L0 pred finit v) x -> L0 pred finit v #
(Serialize pred, Serialize finit, Serialize v, Ord v) => Serialize (L0 pred finit v) Source #
Instance details Defined in Data.L0 Methods put :: Putter (L0 pred finit v) # get :: Get (L0 pred finit v) #
(NFData pred, NFData finit, NFData v) => NFData (L0 pred finit v) Source #
Instance details Defined in Data.L0 Methods rnf :: L0 pred finit v -> () #
type Rep (L0 pred finit v) Source #
Instance details Defined in Data.L0 type Rep (L0 pred finit v) = D1 ('MetaData "L0" "Data.L0" "foxdec-0.1.0.0-DGuc5MMkhbvOBLAebyTd5" 'False) (C1 ('MetaCons "L0" 'PrefixI 'True) (S1 ('MetaSel ('Just "l0_functions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IntMap (finit, Maybe (FResult pred v)))) :: (S1 ('MetaSel ('Just "l0_indirections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IntMap Indirections)) :: S1 ('MetaSel ('Just "l0_time") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))

l0_insert_new_entry :: Key -> finit -> L0 pred finit v -> L0 pred finit v Source #

l0_adjust_result :: Integral a => a -> Maybe (FResult pred v) -> L0 pred finit v -> L0 pred finit v Source #

l0_lookup_entry :: Integral a => a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)) Source #

l0_lookup_indirection :: Integral a => a -> L0 pred finit v -> Maybe Indirections Source #

l0_insert_indirection :: Integral a => a -> Indirections -> L0 pred finit v -> L0 pred finit v Source #

empty_result :: FResult pred v Source #

l0_get_cfgs :: L0 pred finit v -> IntMap CFG Source #

l0_get_function_entries :: L0 pred finit v -> Set Int Source #

l0_get_pars :: L0 pred finit v -> IntMap (IntMap (PointerAnalysisResult v)) Source #

type Lifting bin pred finit v = (bin, Config, L0 pred finit v) Source #

type LiftingEntry bin pred finit v = (bin, Config, L0 pred finit v, Word64) Source #

show_indirections :: IntMap Indirections -> String Source #