Datafix.Worklist.Internal

Internal module, does not follow the PVP. Breaking changes may happen at any minor version.

Documentation

newtype DependencyM graph domain a

The concrete MonadDependency for this worklist-based solver.

This essentially tracks the current approximation of the solution to the DataFlowProblem as mutable state while solveProblem makes sure we will eventually halt with a conservative approximation.

Constructors

DM (ReaderT (Env graph domain) IO a)

Why does this use IO? Actually, we only need ST here, but that means we have to carry around the state thread in type signatures.

This ultimately leaks badly into the exported interface in solveProblem: Since we can't have universally quantified instance contexts (yet!), we can' write (forall s. Datafixable domain => (forall s. DataFlowProblem (DependencyM s graph domain)) -> ... and have to instead have the isomorphic (forall s r. (Datafixable domain => r) -> r) -> (forall s. DataFlowProblem (DependencyM s graph domain)) -> ... and urge all call sites to pass a meaningless id parameter.

Also, this means more explicit type signatures as we have to make clear to the type-checker that s is universally quantified in everything that touches it, e.g. Analyses.StrAnal.LetDn.buildProblem from the test suite.

So, bottom line: We resort to IO and unsafePerformIO and promise not to launch missiles. In particular, we don't export DM and also there must never be an instance of MonadIO for this.

Instances

Monad (DependencyM graph domain)

Methods

(>>=) :: 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)

Methods

fmap :: (a -> b) -> DependencyM graph domain a -> DependencyM graph domain b

(<$) :: a -> DependencyM graph domain b -> DependencyM graph domain a

Applicative (DependencyM graph domain)

Methods

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)

The Domain is extracted from a type parameter.

Associated Types

type Domain (DependencyM graph domain :: * -> *) :: *

(Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain)

This allows us to solve MonadDependency m => DataFlowProblem m descriptions with solveProblem.

Methods

dependOn :: Node -> LiftedFunc (Domain (DependencyM graph domain)) (DependencyM graph domain)

type Domain (DependencyM graph domain)

type Domain (DependencyM graph domain) = domain

data Env graph domain

The iteration state of 'DependencyM'/'solveProblem'.

Constructors

Env

Fields

• problem :: !(DataFlowProblem (DependencyM graph domain))

  Constant. The specification of the data-flow problem we ought to solve.

• iterationBound :: !(IterationBound domain)

  Constant. Whether to abort after a number of iterations or not.

• callStack :: !(IntArgsMonoSet (Products (ParamTypes domain)))

  Contextual state. The set of points in the domain of Nodes currently in the call stack.

• graph :: !(graph domain)

  Constant ref to stateful graph. The data-flow graph, modeling dependencies between data-flow Nodes, or rather specific points in the domain of each Node.

• referencedPoints :: !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))

  Constant (but the the wrapped set is stateful). The set of points the currently recomputed node references so far.

• unstable :: !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))

  Constant (but the the wrapped queue is stateful). Unstable nodes that will be recomputed by the worklist algorithm.

initialEnv :: IntArgsMonoSet (Products (ParamTypes domain)) -> DataFlowProblem (DependencyM graph domain) -> IterationBound domain -> IO (graph domain) -> IO (Env graph domain)

data Density graph where

Specifies the density of the problem, e.g. whether the domain of Nodes 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.

Constructors

Sparse :: Density Ref

Dense :: Node -> Density Ref

type AbortionFunction domain = Arrows (ParamTypes domain) (ReturnType domain -> ReturnType domain)

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

Aborts iteration of a value by constantly returning the top element of the assumed BoundedMeetSemiLattice of the ReturnType.

data IterationBound domain

Expresses that iteration should or shouldn't stop after a point has been iterated a finite number of times.

Constructors

NeverAbort

Will keep on iterating until a precise, yet conservative approximation has been reached. Make sure that your domain satisfies the ascending chain condition, e.g. that fixed-point iteration always comes to a halt!

AbortAfter Int (AbortionFunction domain)

For when your domain doesn't satisfy the ascending chain condition or when you are sensitive about solution performance.

The Integer determines the maximum number of iterations of a single point of a Node (with which an entire function with many points may be associated) before iteration aborts in that point by calling the supplied AbortionFunction. The responsibility of the AbortionFunction is to find a sufficiently conservative approximation for the current value at that point.

When your ReturnType is an instance of BoundedMeetSemiLattice, abortWithTop might be a worthwhile option. A more sophisticated solution would trim the current value to a certain cut-off depth, depending on the first parameter, instead.

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

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) re-iterated. It performs tracking of which Nodes 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

optimisticApproximation :: GraphRef graph => Datafixable domain => Int -> Products (ParamTypes domain) -> ReaderT (Env graph domain) IO (ReturnType domain)

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)

scheme 1 (see https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like).

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)

scheme 2 (see https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like).

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 ()

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 ()

Defined as 'work = whileJust_ highestPriorityUnstableNode (uncurry recompute)'.

Tries to dequeue the highestPriorityUnstableNode and recomputes the value of one of its unstable points, until the worklist is empty, indicating that a fixed-point has been reached.

solveProblem

Arguments

:: GraphRef graph

=> Datafixable domain

=> DataFlowProblem (DependencyM graph domain)

The description of the DataFlowProblem to solve.

-> Density graph

Describes if the algorithm is free to use a Dense, Vector-based graph representation or has to go with a Sparse one based on IntMap.

-> IterationBound domain

Whether the solution algorithm should respect a maximum bound on the number of iterations per point. Pass NeverAbort if you don't care.

-> Node

The Node that is initially assumed to be unstable. This should be the Node you are interested in, e.g. Node 42 if you are interested in the value of fib 42 for a hypothetical fibProblem, or the Node denoting the root expression of your data-flow analysis you specified via the DataFlowProblem.

-> domain

Computes a solution to the described DataFlowProblem by iterating transfer functions until a fixed-point is reached.

It does do by employing a worklist algorithm, iterating unstable Nodes only. Nodes become unstable when the point of another Node their transfer function dependOned changed.

The sole initially unstable Node is the last parameter, and if your domain is function-valued (so the returned Arrows expands to a function), then any further parameters specify the exact point in the Nodes transfer function you are interested in.

If your problem only has finitely many different Nodes , consider using the ProblemBuilder API (e.g. datafix + evalDenotation) for a higher-level API that let's you forget about Nodes and instead let's you focus on building more complex data-flow frameworks.