| 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 |
Lang.Crucible.Analysis.Fixpoint
Description
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 #
Arguments
| :: 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 ScopedRegs for equality, and use them to
look up values in point abstractions after analysis.
Instances
| Show ScopedReg Source # | |
| Eq ScopedReg Source # | |
| Ord ScopedReg Source # | |
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.
Constructors
| Ignore | |
Fields
| |
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.
Constructors
| 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.
Constructors
| Interpretation | |
Fields
| |
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.
Constructors
| PointAbstraction | |
Fields
| |
Instances
| ShowF dom => ShowF (PointAbstraction blocks dom :: Ctx CrucibleType -> Type) Source # | |
Defined in Lang.Crucible.Analysis.Fixpoint Methods 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 Methods 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 StmtIds 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