Safe Haskell	Safe-Inferred
Language	Haskell2010

WithAbstractSymbolicValues.Class

Synopsis

data SymbolicOperation v
- = SO_Op Opcode Int (Maybe Int) [v]
- | SO_Bit Int v
- | SO_SExtend Int Int v
- | SO_Overwrite Int v v
- | SO_Plus v v
- | SO_Minus v v
- | SO_Times v v
data SStatePart p
- = SSP_Reg Register
- | SSP_Mem p Int
data Sstate v p = Sstate {
- sregs :: Map Register v
- smem :: Map (p, Maybe ByteSize) v
- sflags :: FlagStatus
}
data MemRelation
- = Separate
- | Aliassing
- | Unknown
data FInit v p = FInit (Set (SStatePart p, v)) (Map (SStatePart p, SStatePart p) MemRelation)
empty_finit :: FInit v p
unknownSize :: Maybe a
class (Ord v, Eq v, Show v, Eq p, Ord p, Show p) => WithAbstractSymbolicValues ctxt v p | ctxt -> v p where
- sseparate :: ctxt -> String -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
- senclosed :: ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
- salias :: ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
- ssensitive :: ctxt -> p -> Maybe ByteSize -> v -> Bool
- sread_from_ro_data :: ctxt -> p -> Maybe ByteSize -> Maybe v
- smk_mem_addresses :: ctxt -> String -> v -> Set p
- sjoin_values :: Foldable t => ctxt -> String -> t v -> v
- swiden_values :: ctxt -> String -> v -> v
- sjoin_pointers :: ctxt -> [p] -> [p]
- top :: ctxt -> String -> v
- ssemantics :: ctxt -> String -> SymbolicOperation v -> v
- sflg_semantics :: ctxt -> v -> Instruction -> FlagStatus -> FlagStatus
- simmediate :: Integral i => ctxt -> i -> v
- smk_init_reg_value :: ctxt -> Register -> v
- smk_init_mem_value :: ctxt -> String -> p -> Maybe ByteSize -> v
- scall :: ctxt -> Instruction -> State (Sstate v p, VCS v) ()
- sjump :: ctxt -> Instruction -> State (Sstate v p, VCS v) ()
- saddress_has_instruction :: ctxt -> Word64 -> Bool
- skeep_for_finit :: ctxt -> SStatePart p -> v -> Maybe (Set p)
- stry_jump_targets :: ctxt -> v -> Maybe (Set ResolvedJumpTarget)
- stry_resolve_error_call :: ctxt -> Instruction -> v -> Maybe Indirection
- stry_immediate :: ctxt -> v -> Maybe Word64
- sis_deterministic :: ctxt -> v -> Bool
- scheck_regs_in_postcondition :: ctxt -> v -> v -> Bool

Documentation

data SymbolicOperation v Source #

Constructors

SO_Op Opcode Int (Maybe Int) [v]
SO_Bit Int v
SO_SExtend Int Int v
SO_Overwrite Int v v
SO_Plus v v
SO_Minus v v
SO_Times v v

data SStatePart p Source #

A statepart is either a register or a region in memory

Constructors

SSP_Reg Register	A register
SSP_Mem p Int	A region with a symbolic address and an immediate size.

Instances

Instances details

Generic (SStatePart p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Associated Types type Rep (SStatePart p) :: Type -> Type # Methods from :: SStatePart p -> Rep (SStatePart p) x # to :: Rep (SStatePart p) x -> SStatePart p #
Show p => Show (SStatePart p) Source #
Instance details Defined in WithAbstractSymbolicValues.FInit Methods showsPrec :: Int -> SStatePart p -> ShowS # show :: SStatePart p -> String # showList :: [SStatePart p] -> ShowS #
Serialize p => Serialize (SStatePart p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods put :: Putter (SStatePart p) # get :: Get (SStatePart p) #
NFData p => NFData (SStatePart p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods rnf :: SStatePart p -> () #
Eq p => Eq (SStatePart p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods (==) :: SStatePart p -> SStatePart p -> Bool # (/=) :: SStatePart p -> SStatePart p -> Bool #
Ord p => Ord (SStatePart p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods compare :: SStatePart p -> SStatePart p -> Ordering # (<) :: SStatePart p -> SStatePart p -> Bool # (<=) :: SStatePart p -> SStatePart p -> Bool # (>) :: SStatePart p -> SStatePart p -> Bool # (>=) :: SStatePart p -> SStatePart p -> Bool # max :: SStatePart p -> SStatePart p -> SStatePart p # min :: SStatePart p -> SStatePart p -> SStatePart p #
type Rep (SStatePart p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class type Rep (SStatePart p) = D1 ('MetaData "SStatePart" "WithAbstractSymbolicValues.Class" "foxdec-0.1.0.0-DGuc5MMkhbvOBLAebyTd5" 'False) (C1 ('MetaCons "SSP_Reg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Register)) :+: C1 ('MetaCons "SSP_Mem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

data Sstate v p Source #

Constructors

Sstate
Fields sregs :: Map Register v smem :: Map (p, Maybe ByteSize) v sflags :: FlagStatus

Instances

Instances details

(Show v, Ord v, BinaryClass bin, WithAbstractSymbolicValues (bin, Config, L0 (Sstate v p) (FInit v p) v, Word64) v p) => WithAbstractPredicates bin (Sstate v p) (FInit v p) v Source #
Instance details Defined in WithAbstractSymbolicValues.InstanceOfAbstractPredicates Methods symbolically_execute :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Bool -> [Instruction] -> Maybe [Instruction] -> State (Sstate v p, VCS v) () Source # verify_postcondition :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Bool Source # finit_to_init_pred :: LiftingEntry bin (Sstate v p) (FInit v p) v -> FInit v p -> Sstate v p Source # pred_to_finit :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> FInit v p Source # resolve_indirection :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> [Instruction] -> Indirections Source # is_weaker_than :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Sstate v p -> Bool Source # join_preds :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Sstate v p -> Sstate v p Source # join_finits :: LiftingEntry bin (Sstate v p) (FInit v p) v -> FInit v p -> FInit v p -> FInit v p Source # new_finit :: Lifting bin (Sstate v p) (FInit v p) v -> FInit v p Source # pp_finit :: Lifting bin (Sstate v p) (FInit v p) v -> FInit v p -> String Source #
Generic (Sstate v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Associated Types type Rep (Sstate v p) :: Type -> Type # Methods from :: Sstate v p -> Rep (Sstate v p) x # to :: Rep (Sstate v p) x -> Sstate v p #
(Show v, Show p) => Show (Sstate v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods showsPrec :: Int -> Sstate v p -> ShowS # show :: Sstate v p -> String # showList :: [Sstate v p] -> ShowS #
(Ord v, Serialize v, Ord p, Serialize p) => Serialize (Sstate v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods put :: Putter (Sstate v p) # get :: Get (Sstate v p) #
(NFData v, NFData p) => NFData (Sstate v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods rnf :: Sstate v p -> () #
(Eq v, Eq p) => Eq (Sstate v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods (==) :: Sstate v p -> Sstate v p -> Bool # (/=) :: Sstate v p -> Sstate v p -> Bool #
(Ord v, Ord p) => Ord (Sstate v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods compare :: Sstate v p -> Sstate v p -> Ordering # (<) :: Sstate v p -> Sstate v p -> Bool # (<=) :: Sstate v p -> Sstate v p -> Bool # (>) :: Sstate v p -> Sstate v p -> Bool # (>=) :: Sstate v p -> Sstate v p -> Bool # max :: Sstate v p -> Sstate v p -> Sstate v p # min :: Sstate v p -> Sstate v p -> Sstate v p #
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 #
type Rep (Sstate v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class type Rep (Sstate v p) = D1 ('MetaData "Sstate" "WithAbstractSymbolicValues.Class" "foxdec-0.1.0.0-DGuc5MMkhbvOBLAebyTd5" 'False) (C1 ('MetaCons "Sstate" 'PrefixI 'True) (S1 ('MetaSel ('Just "sregs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Register v)) :: (S1 ('MetaSel ('Just "smem") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map (p, Maybe ByteSize) v)) :: S1 ('MetaSel ('Just "sflags") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FlagStatus))))

data MemRelation Source #

A function initialisation consists of a mapping of state parts to values, and memory relations

Constructors

Separate
Aliassing
Unknown

Instances

Instances details

Generic MemRelation Source #
Instance details Defined in WithAbstractSymbolicValues.Class Associated Types type Rep MemRelation :: Type -> Type # Methods from :: MemRelation -> Rep MemRelation x # to :: Rep MemRelation x -> MemRelation #
Show MemRelation Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods showsPrec :: Int -> MemRelation -> ShowS # show :: MemRelation -> String # showList :: [MemRelation] -> ShowS #
Serialize MemRelation Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods put :: Putter MemRelation # get :: Get MemRelation #
NFData MemRelation Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods rnf :: MemRelation -> () #
Eq MemRelation Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods (==) :: MemRelation -> MemRelation -> Bool # (/=) :: MemRelation -> MemRelation -> Bool #
Ord MemRelation Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods compare :: MemRelation -> MemRelation -> Ordering # (<) :: MemRelation -> MemRelation -> Bool # (<=) :: MemRelation -> MemRelation -> Bool # (>) :: MemRelation -> MemRelation -> Bool # (>=) :: MemRelation -> MemRelation -> Bool # max :: MemRelation -> MemRelation -> MemRelation # min :: MemRelation -> MemRelation -> MemRelation #
type Rep MemRelation Source #
Instance details Defined in WithAbstractSymbolicValues.Class type Rep MemRelation = D1 ('MetaData "MemRelation" "WithAbstractSymbolicValues.Class" "foxdec-0.1.0.0-DGuc5MMkhbvOBLAebyTd5" 'False) (C1 ('MetaCons "Separate" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Aliassing" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unknown" 'PrefixI 'False) (U1 :: Type -> Type)))

data FInit v p Source #

Constructors

FInit (Set (SStatePart p, v)) (Map (SStatePart p, SStatePart p) MemRelation)

Instances

Instances details

(Show v, Ord v, BinaryClass bin, WithAbstractSymbolicValues (bin, Config, L0 (Sstate v p) (FInit v p) v, Word64) v p) => WithAbstractPredicates bin (Sstate v p) (FInit v p) v Source #
Instance details Defined in WithAbstractSymbolicValues.InstanceOfAbstractPredicates Methods symbolically_execute :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Bool -> [Instruction] -> Maybe [Instruction] -> State (Sstate v p, VCS v) () Source # verify_postcondition :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Bool Source # finit_to_init_pred :: LiftingEntry bin (Sstate v p) (FInit v p) v -> FInit v p -> Sstate v p Source # pred_to_finit :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> FInit v p Source # resolve_indirection :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> [Instruction] -> Indirections Source # is_weaker_than :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Sstate v p -> Bool Source # join_preds :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Sstate v p -> Sstate v p Source # join_finits :: LiftingEntry bin (Sstate v p) (FInit v p) v -> FInit v p -> FInit v p -> FInit v p Source # new_finit :: Lifting bin (Sstate v p) (FInit v p) v -> FInit v p Source # pp_finit :: Lifting bin (Sstate v p) (FInit v p) v -> FInit v p -> String Source #
Generic (FInit v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Associated Types type Rep (FInit v p) :: Type -> Type # Methods from :: FInit v p -> Rep (FInit v p) x # to :: Rep (FInit v p) x -> FInit v p #
(Eq v, Show v, Show p) => Show (FInit v p) Source #	Show function initialisation
Instance details Defined in WithAbstractSymbolicValues.FInit Methods showsPrec :: Int -> FInit v p -> ShowS # show :: FInit v p -> String # showList :: [FInit v p] -> ShowS #
(Serialize v, Serialize p, Ord p, Ord v) => Serialize (FInit v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods put :: Putter (FInit v p) # get :: Get (FInit v p) #
(NFData p, NFData v) => NFData (FInit v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods rnf :: FInit v p -> () #
(Eq p, Eq v) => Eq (FInit v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods (==) :: FInit v p -> FInit v p -> Bool # (/=) :: FInit v p -> FInit v p -> Bool #
(Ord p, Ord v) => Ord (FInit v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class Methods compare :: FInit v p -> FInit v p -> Ordering # (<) :: FInit v p -> FInit v p -> Bool # (<=) :: FInit v p -> FInit v p -> Bool # (>) :: FInit v p -> FInit v p -> Bool # (>=) :: FInit v p -> FInit v p -> Bool # max :: FInit v p -> FInit v p -> FInit v p # min :: FInit v p -> FInit v p -> FInit v p #
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 #
type Rep (FInit v p) Source #
Instance details Defined in WithAbstractSymbolicValues.Class type Rep (FInit v p) = D1 ('MetaData "FInit" "WithAbstractSymbolicValues.Class" "foxdec-0.1.0.0-DGuc5MMkhbvOBLAebyTd5" 'False) (C1 ('MetaCons "FInit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set (SStatePart p, v))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map (SStatePart p, SStatePart p) MemRelation))))