Documentation

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.

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

A constraint synonym for the constraints m and its associated Domain have to suffice.

This is actually a lot less scary than you might think. Assuming we got quantified class constraints, Datafixable is a specialized version of this:

type Datafixable m =
  ( forall r. Currying (ParamTypes (Domain m)) r
  , MonoMapKey (Products (ParamTypes (Domain m)))
  , BoundedJoinSemiLattice (ReturnType (Domain m))
  )

Now, let's assume a concrete Domain m ~ String -> Bool -> Int, so that ParamTypes (String -> Bool -> Int) expands to the type-level list '[String, Bool] and Products '[String, Bool] reduces to (String, Bool).

Then this constraint makes sure we are able to

1. Curry the domain of String -> Bool -> r for all r to e.g. (String, Bool) -> r. See Currying. This constraint should always be discharged automatically by the type-checker as soon as ParamTypes and ReturnTypes reduce for the Domain argument, which happens when the concrete MonadDependency m is known.

   (Actually, we do this for multiple concrete r because of the missing support for quantified class constraints)

2. We want to use a monotone map of (String, Bool) to Int (the ReturnType (Domain m)). This is ensured by the MonoMapKey (String, Bool) constraint.

   This constraint has to be discharged manually, but should amount to a single line of boiler-plate in most cases, see MonoMapKey.

   Note that the monotonicity requirement means we have to pull non-monotone arguments in Domain m into the Node portion of the DataFlowProblem.

3. For fixed-point iteration to work at all, the values which we iterate naturally have to be instances of BoundedJoinSemiLattice. That type-class allows us to start iteration from a most-optimistic bottom value and successively iterate towards a conservative approximation using the '(/)' operator.

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

evalDenotation denot ib returns a value in domain that is described by the denotation denot.

It does so by building up the DataFlowProblem corresponding to denot and solving the resulting problem with solveProblem, the documentation of which describes in detail how to arrive at a stable denotation and what the IterationBound ib is for.