Copyright | (c) Galois Inc 2015 |
---|---|
License | BSD3 |
Maintainer | Tristan Ravitch <tristan@galois.com> |
Stability | provisional Abstract interpretation over the Crucible IR Supports widening with an iteration order based on weak topological orderings. Some basic tests on hand-written IR programs are included. |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- forwardFixpoint :: forall ext dom blocks ret init. Domain dom -> Interpretation ext dom -> CFG ext blocks init ret -> MapF GlobalVar dom -> Assignment dom init -> (Assignment (PointAbstraction blocks dom) blocks, dom ret)
- forwardFixpoint' :: forall ext dom blocks ret init. Domain dom -> Interpretation ext dom -> CFG ext blocks init ret -> MapF GlobalVar dom -> Assignment dom init -> (Assignment (PointAbstraction blocks dom) blocks, Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks, dom ret)
- data ScopedReg where
- lookupAbstractScopedRegValue :: ScopedReg -> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks -> Maybe (Some dom)
- lookupAbstractScopedRegValueByIndex :: (Int, Int) -> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks -> Maybe (Some dom)
- newtype Ignore a (b :: k) = Ignore {
- _ignoreOut :: a
- data Domain (dom :: CrucibleType -> Type) = Domain {}
- data IterationStrategy (dom :: CrucibleType -> Type) where
- WTO :: IterationStrategy dom
- WTOWidening :: (Int -> Bool) -> (forall tp. dom tp -> dom tp -> dom tp) -> IterationStrategy dom
- Worklist :: IterationStrategy dom
- data Interpretation ext (dom :: CrucibleType -> Type) = Interpretation {
- interpExpr :: forall blocks ctx tp. ScopedReg -> TypeRepr tp -> Expr ext ctx tp -> PointAbstraction blocks dom ctx -> (Maybe (PointAbstraction blocks dom ctx), dom tp)
- interpExt :: forall blocks ctx tp. ScopedReg -> StmtExtension ext (Reg ctx) tp -> PointAbstraction blocks dom ctx -> (Maybe (PointAbstraction blocks dom ctx), dom tp)
- interpCall :: forall blocks ctx args ret. CtxRepr args -> TypeRepr ret -> Reg ctx (FunctionHandleType args ret) -> dom (FunctionHandleType args ret) -> Assignment dom args -> PointAbstraction blocks dom ctx -> (Maybe (PointAbstraction blocks dom ctx), dom ret)
- interpReadGlobal :: forall blocks ctx tp. GlobalVar tp -> PointAbstraction blocks dom ctx -> (Maybe (PointAbstraction blocks dom ctx), dom tp)
- interpWriteGlobal :: forall blocks ctx tp. GlobalVar tp -> Reg ctx tp -> PointAbstraction blocks dom ctx -> Maybe (PointAbstraction blocks dom ctx)
- interpBr :: forall blocks ctx. Reg ctx BoolType -> dom BoolType -> JumpTarget blocks ctx -> JumpTarget blocks ctx -> PointAbstraction blocks dom ctx -> (Maybe (PointAbstraction blocks dom ctx), Maybe (PointAbstraction blocks dom ctx))
- interpMaybe :: forall blocks ctx tp. TypeRepr tp -> Reg ctx (MaybeType tp) -> dom (MaybeType tp) -> PointAbstraction blocks dom ctx -> (Maybe (PointAbstraction blocks dom ctx), dom tp, Maybe (PointAbstraction blocks dom ctx))
- data PointAbstraction blocks dom ctx = PointAbstraction {
- _paGlobals :: MapF GlobalVar dom
- _paRegisters :: Assignment dom ctx
- _paRefs :: MapF (RefStmtId blocks) dom
- _paRegisterRefs :: Assignment (RefSet blocks) ctx
- data RefSet blocks tp
- emptyRefSet :: RefSet blocks tp
- paGlobals :: Functor f => (MapF GlobalVar dom -> f (MapF GlobalVar dom)) -> PointAbstraction blocks dom ctx -> f (PointAbstraction blocks dom ctx)
- paRegisters :: Functor f => (Assignment dom ctx -> f (Assignment dom ctx)) -> PointAbstraction blocks dom ctx -> f (PointAbstraction blocks dom ctx)
- lookupAbstractRegValue :: PointAbstraction blocks dom ctx -> Reg ctx tp -> dom tp
- modifyAbstractRegValue :: PointAbstraction blocks dom ctx -> Reg ctx tp -> (dom tp -> dom tp) -> PointAbstraction blocks dom ctx
- cfgWeakTopologicalOrdering :: CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))]
- data Pointed dom (tp :: CrucibleType) where
- pointed :: (forall tp. dom tp -> dom tp -> Pointed dom tp) -> (forall tp. dom tp -> dom tp -> Bool) -> IterationStrategy (Pointed dom) -> Domain (Pointed dom)
Entry point
forwardFixpoint :: forall ext dom blocks ret init. Domain dom -> Interpretation ext dom -> CFG ext blocks init ret -> MapF GlobalVar dom -> Assignment dom init -> (Assignment (PointAbstraction blocks dom) blocks, dom ret) Source #
:: forall ext dom blocks ret init. Domain dom | The domain of abstract values |
-> Interpretation ext dom | The transfer functions for each statement type |
-> CFG ext blocks init ret | The function to analyze |
-> MapF GlobalVar dom | Assignments of abstract values to global variables at the function start |
-> Assignment dom init | Assignments of abstract values to the function arguments |
-> (Assignment (PointAbstraction blocks dom) blocks, Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks, dom ret) |
Compute a fixed point via abstract interpretation over a control
flow graph (CFG
) given 1) an interpretation + domain, 2) initial
assignments of domain values to global variables, and 3) initial
assignments of domain values to function arguments.
This is an intraprocedural analysis. To handle function calls, the transfer function for call statements must know how to supply summaries or compute an appropriate conservative approximation.
There are two results from the fixed point computation:
1) For each block in the CFG, the abstraction computed at the *entry* to the block
2) For each block in the CFG, the abstraction computed at the
*exit* from the block. The Assignment
for these "exit"
abstractions ignores the ctx
index on the blocks, since that
context is for *entry* to the blocks.
3) The final abstract value for the value returned by the function
A CFG-scoped SSA temp register.
We don't care about the type params yet, hence the
existential quantification. We may want to look up the instruction
corresponding to a ScopedReg
after analysis though, and we'll
surely want to compare ScopedReg
s for equality, and use them to
look up values in point abstractions after analysis.
lookupAbstractScopedRegValue :: ScopedReg -> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks -> Maybe (Some dom) Source #
Lookup the abstract value of scoped reg in an exit assignment.
lookupAbstractScopedRegValueByIndex :: (Int, Int) -> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks -> Maybe (Some dom) Source #
Lookup the abstract value of scoped reg -- specified by 0-based int indices -- in an exit assignment.
newtype Ignore a (b :: k) Source #
Turn a non paramaterized type into a parameterized type.
For when you want to use a parameterized-utils
style data
structure with a type that doesn't have a parameter.
The same definition as Const
, but with a
different Show
instance.
Ignore | |
|
Instances
Show a => ShowF (Ignore a :: k -> Type) Source # | |
Show a => Show (Ignore a tp) Source # | |
Eq a => Eq (Ignore a b) Source # | |
Ord a => Ord (Ignore a b) Source # | |
Defined in Lang.Crucible.Analysis.Fixpoint |
Abstract Domains
data Domain (dom :: CrucibleType -> Type) Source #
A domain of abstract values, parameterized by a term type
data IterationStrategy (dom :: CrucibleType -> Type) where Source #
The iteration strategies available for computing fixed points.
Algorithmically, the best strategies seem to be based on Weak Topological Orders (WTOs). The WTO approach also naturally supports widening (with a specified widening strategy and widening operator).
A simple worklist approach is also available.
WTO :: IterationStrategy dom | |
WTOWidening :: (Int -> Bool) -> (forall tp. dom tp -> dom tp -> dom tp) -> IterationStrategy dom | |
Worklist :: IterationStrategy dom |
data Interpretation ext (dom :: CrucibleType -> Type) Source #
Transfer functions for each statement type
Interpretation functions for some statement types --
e.g. interpExpr
and interpExt
-- receive ScopedReg
arguments
corresponding to the SSA tmp that the result of the interpreted
statement get assigned to. Some interpretation functions that could
receive this argument do not -- e.g. interpCall
-- because
conathan didn't have a use for that.
Interpretation | |
|
data PointAbstraction blocks dom ctx Source #
This abstraction contains the abstract values of each register at the program point represented by the abstraction. It also contains a map of abstractions for all of the global variables currently known.
PointAbstraction | |
|
Instances
ShowF dom => ShowF (PointAbstraction blocks dom :: Ctx CrucibleType -> Type) Source # | |
Defined in Lang.Crucible.Analysis.Fixpoint withShow :: forall p q (tp :: k) a. p (PointAbstraction blocks dom) -> q tp -> (Show (PointAbstraction blocks dom tp) => a) -> a # showF :: forall (tp :: k). PointAbstraction blocks dom tp -> String # showsPrecF :: forall (tp :: k). Int -> PointAbstraction blocks dom tp -> String -> String # | |
ShowF dom => Show (PointAbstraction blocks dom ctx) Source # | |
Defined in Lang.Crucible.Analysis.Fixpoint showsPrec :: Int -> PointAbstraction blocks dom ctx -> ShowS # show :: PointAbstraction blocks dom ctx -> String # showList :: [PointAbstraction blocks dom ctx] -> ShowS # |
data RefSet blocks tp Source #
This is a wrapper around a set of StmtId
s that name allocation sites of
references. We need the wrapper to correctly position the tp
type
parameter so that we can put them in an Assignment
.
emptyRefSet :: RefSet blocks tp Source #
paGlobals :: Functor f => (MapF GlobalVar dom -> f (MapF GlobalVar dom)) -> PointAbstraction blocks dom ctx -> f (PointAbstraction blocks dom ctx) Source #
paRegisters :: Functor f => (Assignment dom ctx -> f (Assignment dom ctx)) -> PointAbstraction blocks dom ctx -> f (PointAbstraction blocks dom ctx) Source #
lookupAbstractRegValue :: PointAbstraction blocks dom ctx -> Reg ctx tp -> dom tp Source #
Look up the abstract value of a register at a program point
modifyAbstractRegValue :: PointAbstraction blocks dom ctx -> Reg ctx tp -> (dom tp -> dom tp) -> PointAbstraction blocks dom ctx Source #
Modify the abstract value of a register at a program point
cfgWeakTopologicalOrdering :: CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))] Source #
Compute a weak topological order for the CFG.
Pointed domains
The Pointed
type is a wrapper around another Domain
that
provides distinguished Top
and Bottom
elements. Use of this
type is never required (domains can always define their own top and
bottom), but this1 wrapper can save some boring boilerplate.
data Pointed dom (tp :: CrucibleType) where Source #
The Pointed wrapper that adds Top and Bottom elements