Copyright	(c) Galois Inc 2015
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
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 :: Type) (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 :: k0) a0. p (KildallPair a c) -> q tp -> (Show (KildallPair a c tp) => a0) -> a0 # showF :: forall (tp :: k0). KildallPair a c tp -> String # showsPrecF :: forall (tp :: k0). 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 :: k0) a0. p (Ignore a) -> q tp -> (Show (Ignore a tp) => a0) -> a0 # showF :: forall (tp :: k0). Ignore a tp -> String # showsPrecF :: forall (tp :: k0). 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. a tp -> a tp -> a tp
kfwd_bot :: forall tp. a tp
kfwd_club :: c -> c -> c
kfwd_cbot :: c
kfwd_same :: forall tp. a tp -> a tp -> Bool
kfwd_csame :: c -> c -> Bool
kfwd_br :: forall ctx. Reg ctx BoolType -> a BoolType -> c -> (c, c)
kfwd_maybe :: forall ctx tp. TypeRepr tp -> Reg ctx (MaybeType tp) -> a (MaybeType tp) -> c -> (c, a tp, c)
kfwd_reg :: !(forall ctx tp. TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp)
kfwd_expr :: !(forall ctx tp. TypeRepr tp -> Expr ext ctx tp -> Assignment a ctx -> a tp)
kfwd_call :: forall ctx args ret. CtxRepr args -> TypeRepr ret -> Reg ctx (FunctionHandleType args ret) -> a (FunctionHandleType args ret) -> Assignment a args -> a ret
kfwd_rdglobal :: forall tp. GlobalVar tp -> a tp
kfwd_onentry :: forall ctx. BlockID blocks ctx -> (Assignment a ctx, c) -> (Assignment a ctx, c)

kildall_transfer :: forall ext a c blocks ret ctx. 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 ret init. KildallForward ext blocks a c -> CFG ext blocks init ret -> (Assignment a init, c) -> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) Source #