Copyright	(c) Galois Inc 2015
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.Analysis.ForwardDataflow

Description

Deprecated: Lang.Crucible.Analysis.Fixpoint is a better implementation of these ideas

This module defines a generic framework for forward dataflow analysis, with some additional control-flow data on the side.

We calculate a fixpoint of a given analysis via the straightforward method of iterating the transfer function until no more updates occur.

Our current method for doing this is quite naive, and more efficient methods exist.

Documentation

Constructors

Instances details

Show SymDom Source #
Instance details Defined in Lang.Crucible.Analysis.ForwardDataflow Methods showsPrec :: Int -> SymDom -> ShowS # show :: SymDom -> String # showList :: [SymDom] -> ShowS #
Eq SymDom Source #
Instance details Defined in Lang.Crucible.Analysis.ForwardDataflow Methods (==) :: SymDom -> SymDom -> Bool # (/=) :: SymDom -> SymDom -> Bool #
Ord SymDom Source #
Instance details Defined in Lang.Crucible.Analysis.ForwardDataflow Methods compare :: SymDom -> SymDom -> Ordering # (<) :: SymDom -> SymDom -> Bool # (<=) :: SymDom -> SymDom -> Bool # (>) :: SymDom -> SymDom -> Bool # (>=) :: SymDom -> SymDom -> Bool # max :: SymDom -> SymDom -> SymDom # min :: SymDom -> SymDom -> SymDom #

data KildallPair (a :: k -> Type) c (tp :: k) Source #

Constructors

KP (a tp) c

Instances details

(ShowF a, Show c) => ShowF (KildallPair a c :: k -> Type) Source #
Instance details Defined in Lang.Crucible.Analysis.ForwardDataflow Methods withShow :: forall p q (tp :: k) a0. p (KildallPair a c) -> q tp -> (Show (KildallPair a c tp) => a0) -> a0 # showF :: forall (tp :: k). KildallPair a c tp -> String # showsPrecF :: forall (tp :: k). Int -> KildallPair a c tp -> String -> String #
(ShowF a, Show c) => Show (KildallPair a c tp) Source #
Instance details Defined in Lang.Crucible.Analysis.ForwardDataflow Methods showsPrec :: Int -> KildallPair a c tp -> ShowS # show :: KildallPair a c tp -> String # showList :: [KildallPair a c tp] -> ShowS #

newtype Ignore a (b :: k) Source #

Constructors

Ignore
Fields ignoreOut :: a

Instances details

Show a => ShowF (Ignore a :: k -> Type) Source #
Instance details Defined in Lang.Crucible.Analysis.ForwardDataflow Methods withShow :: forall p q (tp :: k) a0. p (Ignore a :: k -> Type) -> q tp -> (Show (Ignore a tp) => a0) -> a0 # showF :: forall (tp :: k). Ignore a tp -> String # showsPrecF :: forall (tp :: k). Int -> Ignore a tp -> String -> String #
Show a => Show (Ignore a tp) Source #
Instance details Defined in Lang.Crucible.Analysis.ForwardDataflow Methods showsPrec :: Int -> Ignore a tp -> ShowS # show :: Ignore a tp -> String # showList :: [Ignore a tp] -> ShowS #
Eq a => Eq (Ignore a b) Source #
Instance details Defined in Lang.Crucible.Analysis.ForwardDataflow Methods (==) :: Ignore a b -> Ignore a b -> Bool # (/=) :: Ignore a b -> Ignore a b -> Bool #
Ord a => Ord (Ignore a b) Source #
Instance details Defined in Lang.Crucible.Analysis.ForwardDataflow Methods compare :: Ignore a b -> Ignore a b -> Ordering # (<) :: Ignore a b -> Ignore a b -> Bool # (<=) :: Ignore a b -> Ignore a b -> Bool # (>) :: Ignore a b -> Ignore a b -> Bool # (>=) :: Ignore a b -> Ignore a b -> Bool # max :: Ignore a b -> Ignore a b -> Ignore a b # min :: Ignore a b -> Ignore a b -> Ignore a b #

Constructors

Fields

kfwd_lub :: forall (tp :: CrucibleType). a tp -> a tp -> a tp
kfwd_bot :: forall (tp :: CrucibleType). a tp
kfwd_club :: c -> c -> c
kfwd_cbot :: c
kfwd_same :: forall (tp :: CrucibleType). a tp -> a tp -> Bool
kfwd_csame :: c -> c -> Bool
kfwd_br :: forall (ctx :: Ctx CrucibleType). Reg ctx BoolType -> a BoolType -> c -> (c, c)
kfwd_maybe :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType). TypeRepr tp -> Reg ctx (MaybeType tp) -> a (MaybeType tp) -> c -> (c, a tp, c)
kfwd_reg :: !(forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType). TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp)
kfwd_expr :: !(forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType). TypeRepr tp -> Expr ext ctx tp -> Assignment a ctx -> a tp)
kfwd_call :: forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) (ret :: CrucibleType). CtxRepr args -> TypeRepr ret -> Reg ctx (FunctionHandleType args ret) -> a (FunctionHandleType args ret) -> Assignment a args -> a ret
kfwd_rdglobal :: forall (tp :: CrucibleType). GlobalVar tp -> a tp
kfwd_onentry :: forall (ctx :: Ctx CrucibleType). BlockID blocks ctx -> (Assignment a ctx, c) -> (Assignment a ctx, c)

kildall_transfer :: forall ext a c (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). KildallForward ext blocks a c -> TypeRepr ret -> Block ext blocks ret ctx -> (Assignment a ctx, c) -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks))) Source #

kildall_forward :: forall ext a c (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (init :: Ctx CrucibleType). KildallForward ext blocks a c -> CFG ext blocks init ret -> (Assignment a init, c) -> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) Source #