Copyright  (c) Sebastian Graf 20172020 

License  ISC 
Maintainer  sgraf1337@gmail.com 
Portability  portable 
Safe Haskell  None 
Language  Haskell2010 
Internal module, does not follow the PVP. Breaking changes may happen at any minor version.
Synopsis
 newtype DependencyM graph domain a = DM (ReaderT (Env graph domain) IO a)
 data Env graph domain = Env {
 problem :: !(DataFlowFramework (DependencyM graph domain))
 iterationBound :: !(IterationBound domain)
 callStack :: !(IntArgsMonoSet (Products (ParamTypes domain)))
 graph :: !(graph domain)
 referencedPoints :: !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))
 unstable :: !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))
 initialEnv :: IntArgsMonoSet (Products (ParamTypes domain)) > DataFlowFramework (DependencyM graph domain) > IterationBound domain > IO (graph domain) > IO (Env graph domain)
 data Density graph where
 type AbortionFunction domain = Arrows (ParamTypes domain) (ReturnType domain > ReturnType domain)
 abortWithTop :: forall domain. Currying (ParamTypes domain) (ReturnType domain > ReturnType domain) => BoundedMeetSemiLattice (ReturnType domain) => AbortionFunction domain
 data IterationBound domain
 = NeverAbort
  AbortAfter Int (AbortionFunction domain)
 zoomIORef :: State s a > ReaderT (IORef s) IO a
 zoomReferencedPoints :: State (IntArgsMonoSet (Products (ParamTypes domain))) a > ReaderT (Env graph domain) IO a
 zoomUnstable :: State (IntArgsMonoSet (Products (ParamTypes domain))) a > ReaderT (Env graph domain) IO a
 enqueueUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int > k > ReaderT (Env graph domain) IO ()
 deleteUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int > k > ReaderT (Env graph domain) IO ()
 highestPriorityUnstableNode :: k ~ Products (ParamTypes domain) => MonoMapKey k => ReaderT (Env graph domain) IO (Maybe (Int, k))
 withCall :: Datafixable domain => Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO a > ReaderT (Env graph domain) IO a
 recompute :: forall domain graph dom cod depm. dom ~ ParamTypes domain => cod ~ ReturnType domain => depm ~ DependencyM graph domain => GraphRef graph => Datafixable domain => Int > Products dom > ReaderT (Env graph domain) IO cod
 dependOn :: forall domain graph depm. depm ~ DependencyM graph domain => Datafixable domain => GraphRef graph => Node > LiftedFunc domain depm
 optimisticApproximation :: GraphRef graph => Datafixable domain => Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain)
 scheme1 :: GraphRef graph => Datafixable domain => Maybe (ReturnType domain) > Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain)
 scheme2 :: GraphRef graph => Datafixable domain => Maybe (ReturnType domain) > Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain)
 whileJust_ :: Monad m => m (Maybe a) > (a > m b) > m ()
 work :: GraphRef graph => Datafixable domain => ReaderT (Env graph domain) IO ()
 solveProblem :: forall domain graph a. GraphRef graph => Datafixable domain => DataFlowFramework (DependencyM graph domain) > Density graph > IterationBound domain > DependencyM graph domain a > a
Documentation
newtype DependencyM graph domain a Source #
The concrete MonadDependency
for this worklistbased solver.
This essentially tracks the current approximation of the solution to the
DataFlowFramework
as mutable state while solveProblem
makes sure we will eventually
halt with a conservative approximation.
DM (ReaderT (Env graph domain) IO a)  Why does this use This ultimately leaks badly into the exported interface in Also, this means more explicit type signatures as we have to make clear to
the typechecker that So, bottom line: We resort to 
Instances
Monad (DependencyM graph domain) Source #  
Defined in Datafix.Worklist.Internal (>>=) :: DependencyM graph domain a > (a > DependencyM graph domain b) > DependencyM graph domain b # (>>) :: DependencyM graph domain a > DependencyM graph domain b > DependencyM graph domain b # return :: a > DependencyM graph domain a # fail :: String > DependencyM graph domain a #  
Functor (DependencyM graph domain) Source #  
Defined in Datafix.Worklist.Internal fmap :: (a > b) > DependencyM graph domain a > DependencyM graph domain b # (<$) :: a > DependencyM graph domain b > DependencyM graph domain a #  
Applicative (DependencyM graph domain) Source #  
Defined in Datafix.Worklist.Internal pure :: a > DependencyM graph domain a # (<*>) :: DependencyM graph domain (a > b) > DependencyM graph domain a > DependencyM graph domain b # liftA2 :: (a > b > c) > DependencyM graph domain a > DependencyM graph domain b > DependencyM graph domain c # (*>) :: DependencyM graph domain a > DependencyM graph domain b > DependencyM graph domain b # (<*) :: DependencyM graph domain a > DependencyM graph domain b > DependencyM graph domain a #  
Datafixable domain => MonadDomain (DependencyM graph domain) Source #  The 
Defined in Datafix.Worklist.Internal type Domain (DependencyM graph domain) :: Type Source #  
(Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) Source #  This allows us to solve 
Defined in Datafix.Worklist.Internal dependOn :: Node > LiftedFunc (Domain (DependencyM graph domain)) (DependencyM graph domain) Source #  
type Domain (DependencyM graph domain) Source #  
Defined in Datafix.Worklist.Internal 
data Env graph domain Source #
The iteration state of 'DependencyM'/'solveProblem'.
Env  

initialEnv :: IntArgsMonoSet (Products (ParamTypes domain)) > DataFlowFramework (DependencyM graph domain) > IterationBound domain > IO (graph domain) > IO (Env graph domain) Source #
data Density graph where Source #
Specifies the density of the problem, e.g. whether the domain of
Node
s can be confined to a finite range, in which case solveProblem
tries to use a Data.Vector based graph representation rather than
one based on Data.IntMap.
type AbortionFunction domain = Arrows (ParamTypes domain) (ReturnType domain > ReturnType domain) Source #
A function that computes a sufficiently conservative approximation of a point in the abstract domain for when the solution algorithm decides to have iterated the node often enough.
When domain
is a 'BoundedMeetSemilattice'/'BoundedLattice', the
simplest abortion function would be to constantly return top
.
As is the case for LiftedFunc
and ChangeDetector
, this
carries little semantic meaning if viewed in isolation, so here
are a few examples for how the synonym expands:
AbortionFunction Int ~ Int > Int AbortionFunction (String > Int) ~ String > Int > Int AbortionFunction (a > b > c > PowerSet) ~ a > b > c > PowerSet > PowerSet
E.g., the current value of the point is passed in (the tuple (a, b, c, PowerSet)
)
and the function returns an appropriate conservative approximation in that
point.
abortWithTop :: forall domain. Currying (ParamTypes domain) (ReturnType domain > ReturnType domain) => BoundedMeetSemiLattice (ReturnType domain) => AbortionFunction domain Source #
Aborts iteration of a value by const
antly returning the top
element
of the assumed BoundedMeetSemiLattice
of the ReturnType
.
data IterationBound domain Source #
Expresses that iteration should or shouldn't stop after a point has been iterated a finite number of times.
NeverAbort  Will keep on iterating until a precise, yet conservative approximation
has been reached. Make sure that your 
AbortAfter Int (AbortionFunction domain)  For when your The When your 
zoomReferencedPoints :: State (IntArgsMonoSet (Products (ParamTypes domain))) a > ReaderT (Env graph domain) IO a Source #
zoomUnstable :: State (IntArgsMonoSet (Products (ParamTypes domain))) a > ReaderT (Env graph domain) IO a Source #
enqueueUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int > k > ReaderT (Env graph domain) IO () Source #
deleteUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int > k > ReaderT (Env graph domain) IO () Source #
highestPriorityUnstableNode :: k ~ Products (ParamTypes domain) => MonoMapKey k => ReaderT (Env graph domain) IO (Maybe (Int, k)) Source #
withCall :: Datafixable domain => Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO a > ReaderT (Env graph domain) IO a Source #
recompute :: forall domain graph dom cod depm. dom ~ ParamTypes domain => cod ~ ReturnType domain => depm ~ DependencyM graph domain => GraphRef graph => Datafixable domain => Int > Products dom > ReaderT (Env graph domain) IO cod Source #
The first of the two major functions of this module.
recompute node args
iterates the value of the passed node
at the point args
by invoking its transfer function.
It does so in a way that respects the IterationBound
.
This function is not exported, and is only called by work
and dependOn
, for when the iteration strategy decides that
the node
needs to be (and can be) reiterated.
It performs tracking of which Node
s the transfer function
depended on, do that the worklist algorithm can do its magic.
dependOn :: forall domain graph depm. depm ~ DependencyM graph domain => Datafixable domain => GraphRef graph => Node > LiftedFunc domain depm Source #
optimisticApproximation :: GraphRef graph => Datafixable domain => Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain) Source #
Compute an optimistic approximation for a point of a given node that is as precise as possible, given the other points of that node we already computed.
E.g., it is always valid to return bottom
from this, but in many cases
we can be more precise since we possibly have computed points for the node
that are lower bounds to the current point.
scheme1 :: GraphRef graph => Datafixable domain => Maybe (ReturnType domain) > Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain) Source #
Let the worklist algorithm figure things out.
scheme2 :: GraphRef graph => Datafixable domain => Maybe (ReturnType domain) > Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain) Source #
Descend into \(\bot\) nodes when there is no cycle to discover the set of reachable nodes as quick as possible. Do *not* descend into unstable, non(bot) nodes.
whileJust_ :: Monad m => m (Maybe a) > (a > m b) > m () Source #
As long as the supplied Maybe expression returns "Just _", the loop
body will be called and passed the value contained in the Just
. Results
are discarded.
Taken from whileJust_
.
work :: GraphRef graph => Datafixable domain => ReaderT (Env graph domain) IO () Source #
Defined as 'work = whileJust_ highestPriorityUnstableNode (uncurry recompute)'.
Tries to dequeue the highestPriorityUnstableNode
and recompute
s the value of
one of its unstable
points, until the worklist is empty, indicating that a
fixedpoint has been reached.
:: GraphRef graph  
=> Datafixable domain  
=> DataFlowFramework (DependencyM graph domain)  The description of the 
> Density graph  Describes if the algorithm is free to use a 
> IterationBound domain  Whether the solution algorithm should respect a maximum bound on the
number of iterations per point. Pass 
> DependencyM graph domain a  The action for which we want to compute the solution. May reference

> a 
Computes the (pure) solution of the DependencyM
action act
specified in
the last parameter. act
may reference (via dependOn
) Node
s of the
DataFlowFramework
dff
's fixedpoint, specified as the first parameter.
dff
's fixedpoint is determined by its transfer functions, and
solveProblem
will make sure that all (relevant) Node
s will have reached
their fixedpoint according to their transfer function before computing the
solution for act
.
We try to be smart in saving unnecessary iterations of transfer functions by employing a worklist algorithm. For function domains, where each Node denotes a monotone function, each point's dependencies' will be tracked individually.
Apart from dff
and act
, the Density
of the dataflow graph and the
IterationBound
can be specified. Pass Sparse
and NeverAbort
when in
doubt.
If your problem only has finitely many different Node
s , consider using the
FrameworkBuilder
API (e.g. datafix
+ evalDenotation
) for a higherlevel
API that let's you forget about Node
s and instead let's you focus on
building more complex dataflow frameworks.
See Datafix.Tutorial and the examples/
subfolder for examples.