Module UniversalFlow

Provides predicates for proving data flow properties that hold for all paths, that is, reachability is computed using universal quantification over the step relation.

Regular data flow search for the existence of a path, that is, reachability using existential quantification over the step relation. Hence, this library computes the dual reachability predicate that states that a certain property always holds for a given node regardless of the path taken.

As a simple comparison, the computed predicate is essentially equivalent to the folllowing:

  predicate hasProperty(FlowNode n, Prop t) {
    basecase(n, t)
    or
    forex(FlowNode mid | step(mid, n) | hasProperty(mid, t))
  }

More complex property propagation is supported, and strongly connected components in the flow graph are handled.

As an initial such property calculation, the library computes the set of nodes that are always null. These are then subtracted from the graph such that subsequently calculated properties hold under the assumption that the value is not null.