Documentation

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.

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

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.

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.

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

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

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.

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.

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.

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.

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

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.

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.