datafix-0.0.1.0: Fixing data-flow problems

Copyright (c) Sebastian Graf 2017-2020 ISC sgraf1337@gmail.com portable None Haskell2010

Datafix.Worklist.Internal

Description

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

Synopsis

# Documentation

newtype DependencyM graph domain a Source #

The concrete MonadDependency for this worklist-based 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.

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. DataFlowFramework (DependencyM s graph domain)) -> ... and have to instead have the isomorphic (forall s r. (Datafixable domain => r) -> r) -> (forall s. DataFlowFramework (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.buildDenotation 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) Source # Instance detailsDefined in Datafix.Worklist.Internal 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) Source # Instance detailsDefined in Datafix.Worklist.Internal Methodsfmap :: (a -> b) -> DependencyM graph domain a -> DependencyM graph domain b #(<\$) :: a -> DependencyM graph domain b -> DependencyM graph domain a # Applicative (DependencyM graph domain) Source # Instance detailsDefined in Datafix.Worklist.Internal Methodspure :: 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 Domain is extracted from a type parameter. Instance detailsDefined in Datafix.Worklist.Internal Associated Typestype Domain (DependencyM graph domain) :: Type Source # (Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) Source # This allows us to solve MonadDependency m => DataFlowFramework m descriptions with solveProblem. Instance detailsDefined in Datafix.Worklist.Internal MethodsdependOn :: Node -> LiftedFunc (Domain (DependencyM graph domain)) (DependencyM graph domain) Source # type Domain (DependencyM graph domain) Source # Instance detailsDefined in Datafix.Worklist.Internal type Domain (DependencyM graph domain) = domain

data Env graph domain Source #

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

Constructors

 Env Fieldsproblem :: !(DataFlowFramework (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)) -> 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 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) 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 constantly 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.

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.

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) 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 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 recomputes the value of one of its unstable points, until the worklist is empty, indicating that a fixed-point has been reached.

Arguments

 :: GraphRef graph => Datafixable domain => DataFlowFramework (DependencyM graph domain) The description of the DataFlowFramework. -> 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. -> DependencyM graph domain a The action for which we want to compute the solution. May reference Nodes from the DataFlowFramework. If you just want to know the value of Node 42, use dependOn @(DependecyM _ domain) (Node 42). -> a

Computes the (pure) solution of the DependencyM action act specified in the last parameter. act may reference (via dependOn) Nodes of the DataFlowFramework dff's fixed-point, specified as the first parameter.

dff's fixed-point is determined by its transfer functions, and solveProblem will make sure that all (relevant) Nodes will have reached their fixed-point 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 data-flow graph and the IterationBound can be specified. Pass Sparse and NeverAbort when in doubt.

If your problem only has finitely many different Nodes , consider using the FrameworkBuilder 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.

See Datafix.Tutorial and the examples/ subfolder for examples.