Documentation

This is the type we use to index nodes in the data-flow graph.

The connection between syntactic things (e.g. Ids) and Nodes is made implicitly in code in analysis templates through an appropriate allocation mechanism as in NodeAllocator.

Models a data-flow problem, where each Node is mapped to its denoting LiftedFunc and a means to detect when the iterated transfer function reached a fixed-point through a ChangeDetector.

A monad with a single impure primitive dependOn that expresses a dependency on a Node of a data-flow graph.

The associated Domain type is the abstract domain in which we denote Nodes.

Think of it like memoization on steroids. You can represent dynamic programs with this quite easily:

>>> :{
  transferFib :: forall m . (MonadDependency m, Domain m ~ Int) => Node -> LiftedFunc Int m
  transferFib (Node 0) = return 0
  transferFib (Node 1) = return 1
  transferFib (Node n) = (+) <$> dependOn @m (Node (n-1)) <*> dependOn @m (Node (n-2))
  -- sparing the negative n error case
:}

We can construct a description of a DataFlowProblem with this transferFib function:

>>> :{
  dataFlowProblem :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowProblem m
  dataFlowProblem = DFP transferFib (const (eqChangeDetector @(Domain m)))
:}

We regard the ordinary fib function a solution to the recurrence modeled by transferFib:

>>> :{
  fib :: Int -> Int
  fib 0 = 0
  fib 1 = 1
  fib n = fib (n-1) + fib (n - 2)
:}

E.g., under the assumption of fib being total (which is true on the domain of natural numbers), it computes the same results as the least fixed-point of the series of iterations of the transfer function transferFib.

Ostensibly, the nth iteration of transferFib substitutes each dependOn with transferFib repeatedly for n times and finally substitutes all remaining dependOns with a call to error.

Computing a solution by fixed-point iteration in a declarative manner is the purpose of this library. There potentially are different approaches to computing a solution, but in Datafix.Worklist we offer an approach based on a worklist algorithm, trying to find a smart order in which nodes in the data-flow graph are reiterated.

The concrete MonadDependency depends on the solution algorithm, which is in fact the reason why there is no satisfying data type in this module: We are only concerned with declaring data-flow problems here.

The distinguishing feature of data-flow graphs is that they are not necessarily acyclic (data-flow graphs of dynamic programs always are!), but under certain conditions even have solutions when there are cycles.

Cycles occur commonly in data-flow problems of static analyses for programming languages, introduced through loops or recursive functions. Thus, this library mostly aims at making the life of compiler writers easier.