crucible-0.7.1: Crucible is a library for language-agnostic symbolic simulation
Copyright(c) Galois Inc 2015
LicenseBSD3
MaintainerTristan Ravitch <tristan@galois.com>
Stabilityprovisional 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 HaskellSafe-Inferred
LanguageHaskell2010

Lang.Crucible.Analysis.Fixpoint

Description

 
Synopsis

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 #

forwardFixpoint' 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

data ScopedReg where Source #

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.

Constructors

ScopedReg :: BlockID blocks ctx1 -> Reg ctx2 tp -> ScopedReg 

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

Instances details
Show a => ShowF (Ignore a :: k -> Type) Source # 
Instance details

Defined in Lang.Crucible.Analysis.Fixpoint

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.Fixpoint

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.Fixpoint

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.Fixpoint

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 #

Abstract Domains

data Domain (dom :: CrucibleType -> Type) Source #

A domain of abstract values, parameterized by a term type

Constructors

Domain 

Fields

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

Instances details
ShowF dom => ShowF (PointAbstraction blocks dom :: Ctx CrucibleType -> Type) Source # 
Instance details

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 # 
Instance details

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

Constructors

Top :: Pointed a tp 
Pointed :: dom tp -> Pointed dom tp 
Bottom :: Pointed dom tp 

Instances

Instances details
ShowF dom => ShowF (Pointed dom :: CrucibleType -> Type) Source # 
Instance details

Defined in Lang.Crucible.Analysis.Fixpoint

Methods

withShow :: forall p q (tp :: k) a. p (Pointed dom) -> q tp -> (Show (Pointed dom tp) => a) -> a #

showF :: forall (tp :: k). Pointed dom tp -> String #

showsPrecF :: forall (tp :: k). Int -> Pointed dom tp -> String -> String #

ShowF dom => Show (Pointed dom tp) Source # 
Instance details

Defined in Lang.Crucible.Analysis.Fixpoint

Methods

showsPrec :: Int -> Pointed dom tp -> ShowS #

show :: Pointed dom tp -> String #

showList :: [Pointed dom tp] -> ShowS #

Eq (dom tp) => Eq (Pointed dom tp) Source # 
Instance details

Defined in Lang.Crucible.Analysis.Fixpoint

Methods

(==) :: Pointed dom tp -> Pointed dom tp -> Bool #

(/=) :: Pointed dom tp -> Pointed dom tp -> Bool #

pointed Source #

Arguments

:: (forall tp. dom tp -> dom tp -> Pointed dom tp)

Join of contained domain elements

-> (forall tp. dom tp -> dom tp -> Bool)

Equality for domain elements

-> IterationStrategy (Pointed dom) 
-> Domain (Pointed dom) 

Construct a Pointed Domain from a pointed join function and an equality test.