module ChaoticIteration:sig
..end
Fixpoint computation with widenings using weak topological
orderings as defined by François Bourdoncle and implemented
in WeakTopological
.
Fixpoint
is another (simpler) fixpoint computation module, with
general references.
The general idea of fixpoint computation is to iteratively compute the result of the analysis a vertex from the results of its predecessors, until stabilisation is achieved on every vertex. The way to determine, at each step, the next vertex to analyse is called a chaotic iteration strategy. A good strategy can make the analysis much faster. To enforce the termination of the analyse and speed it up when it terminates in too many steps, one can also use a widening, to ensure that there is no infinite (nor too big) sequence of intermediary results for a given vertex. However, it usually results in a loss of precision, which is why choosing a good widening set (the set of points on which the widening will be performed) is mandatory.
This module computes a fixpoint over a graph using weak
topological ordering, which can be used to get both the iteration
strategy and the widening set. The module WeakTopological
aims
to compute weak topological orderings which are known to be
excellent decompositions w.r.t these two critical points.
type 'a
widening_set =
| |
FromWto |
| |
Predicate of |
How to determine which vertices are to be considered as widening points.
FromWto
indicates to use as widening points the heads of the
weak topological ordering given as a parameter of the analysis
function. This will always be a safe choice, and in most cases
it will also be a good one with respect to the precision of the
analysis.Predicate f
indicates to use f
as the characteristic
function of the widening set. Predicate (fun _ -> false)
can
be used if a widening is not needed. This variant can be used
when there is a special knowledge of the graph to achieve
a better precision of the analysis. For instance, if the graph
happens to be the flow graph of a program, the predicate should
be true for control structures heads. In any case, a condition
for a safe widening predicate is that every cycle of the graph
should go through at least one widening point. Otherwise, the
analysis may not terminate. Note that even with a safe
predicate, ensuring the termination does still require a correct
widening definition.module type G =sig
..end
Minimal graph signature for the algorithm.
module type Data =sig
..end
Parameters of the analysis.
module Make: