Module FixpointType

module FixpointType: sig .. end

Fixpoint analysis of an equation system: types

Public datatypes

Manager

The manager parameterizes the fixpoint solver with the following types:

'vertex: type of vertex/variable (identifier) in the hypergraph describing the equation system;
'hedge: type of hyperedge/function (identifier) in the hypergraph describing the equation system;
'abstract: type of abstract values associated to vertices/variables;
'arc: type of information associated to hyperedges/functions;

and values:

Lattice operations on abstract values; the argument of type 'vertex indicates to which vertex the result of the function is associated (useful when abstract values are typed by an environment, for instance)
Functions to initialize variables and to interpret hyperedges/functions;
Printing functions for type parameters;
Options, mainly about widening;
Debugging options, for text output on the formatter print_fmt;
Printing functions for DOT output on the optional formatter dot_fmt.

type ('a, 'b, 'c, 'd) manager = {

`mutable bottom : 'a -> 'c;`	`(*`	Create a bottom value	`*)`
`mutable canonical : 'a -> 'c -> unit;`	`(*`	Make an abstract value canonical	`*)`
`mutable is_bottom : 'a -> 'c -> bool;`	`(*`	Emptiness test	`*)`
`mutable is_leq : 'a -> 'c -> 'c -> bool;`	`(*`	Inclusion test	`*)`
`mutable join : 'a -> 'c -> 'c -> 'c;`
`mutable join_list : 'a -> 'c list -> 'c;`	`(*`	Binary and n-ary join operation	`*)`
`mutable widening : 'a -> 'c -> 'c -> 'c;`	`(*`	Apply widening at the given point, with the two arguments	`*)`
`mutable abstract_init : 'a -> 'c;`	`(*`	Return the non-bottom initial value associated to the given vertex	`*)`
`mutable arc_init : 'b -> 'd;`	`(*`	Initial value for arcs	`*)`
`mutable apply : 'b -> 'c array -> 'd * 'c;`	`(*`	Apply the function indexed by `hedge` to the array of arguments. It returns the new abstract value, but also a user-defined information that will be associated to the hyperedge in the result.	`*)`
`mutable print_vertex : Format.formatter -> 'a -> unit;`
`mutable print_hedge : Format.formatter -> 'b -> unit;`
`mutable print_abstract : Format.formatter -> 'c -> unit;`
`mutable print_arc : Format.formatter -> 'd -> unit;`	`(*`	Printing functions	`*)`
`mutable accumulate : bool;`	`(*`	If true, during ascending phase, compute the union of old reachable value with growing incoming hyperedges. If false, recompute all incoming hyperedges.	`*)`
`mutable widening_first : bool;`	`(*`	Apply widening from first non bottom value ?	`*)`
`mutable widening_start : int;`	`(*`	First widening step in a strategy	`*)`
`mutable widening_freq : int;`	`(*`	widening every n steps in a strategy	`*)`
`mutable widening_descend : int;`	`(*`	Maximum nb. of descending steps	`*)`
`mutable print_fmt : Format.formatter;`	`(*`	Typically equal to `Format.std_formatter`	`*)`
`mutable print_analysis : bool;`
`mutable print_component : bool;`
`mutable print_step : bool;`
`mutable print_state : bool;`
`mutable print_postpre : bool;`
`mutable print_workingsets : bool;`	`(*`	Printing Options	`*)`
`mutable dot_fmt : Format.formatter option;`	`(*`	`Some fmt` enables DOT output. You can set dummy values to the fields below if you always set `None` and you do not want DOT output.	`*)`
`mutable dot_vertex : Format.formatter -> 'a -> unit;`	`(*`	Print vertex identifiers in DOT format	`*)`
`mutable dot_hedge : Format.formatter -> 'b -> unit;`	`(*`	Print hyperedge identifiers in DOT format (vertices and hyperedges identifiers should be different, as they are represented by DOT vertices	`*)`
`mutable dot_attrvertex : Format.formatter -> 'a -> unit;`	`(*`	Print the displayed information in boxes	`*)`
`mutable dot_attrhedge : Format.formatter -> 'b -> unit;`	`(*`	Print the displayed information for hyperedges	`*)`

}

Dynamically explored equation system

type ('a, 'b) equation = 'a -> ('b, 'a array * 'a) PMappe.t

Function that explores dynamically an equation system. equation vertex returns a map hat associates to each successor hyperedge a pair of composed of the set of predecessor vertices, and the successor vertex.

Iteration strategies

type ('a, 'b) strategy_vertex = {

`mutable vertex : 'a;`
`mutable hedges : 'b list;`	`(*`	Order in which the incoming hyperedges will be applied	`*)`
`mutable widen : bool;`	`(*`	Should this vertex be a widening point ?	`*)`

}

Strategy to be applied for the vertex vertex.

hedges is a list of incoming hyperedges. The effect of hyperedges are applied "in parallel" and the destination vertex is updated. Be cautious: if an incoming hyperedge is forgotten in this list, it won't be taken into account in the analysis.

widen specifies whether the vertex is a widening point or not.

type ('a, 'b) strategy = ('a, 'b) strategy_vertex Ilist.t

Type for defining iteration strategies. For instance,

[1; [2;3]; 4;
      [5]; 6]

means:

update 1;
update 2 then 3, and loop until stabilization;
update 4;
update 5 and loop until stabilization;
update 6 and ends the analysis.

Some observations on this example:

The user should specify correctly the strategy. Two vertices belonging to the same connex component should always belong to a loop. Here, if there is an edge from 6 to 2, the loop will not be iterated.
A vertex may appear more than once in the strategy, if it is useful.
Definition of the set of widening point is independent from the order
of application, here. it is alos the user-responsability to ensure that
the computation will end.

So-called stabilization loops can be recursive, like that:

[1; [2;
      [3;4]; [5]]; 6]

, where the loop [3;4] needs to be (temporarily stable) before going on with 5.

val print_strategy_vertex : ('a, 'b, 'c, 'd) manager ->
       Format.formatter -> ('a, 'b) strategy_vertex -> unit

print_strategy_vertex man fmt sv prints an object of type strategy_vertex, using the manager man for printing vertices and hyperedges. The output has the form

(boolean,vertex,[list of list of
	  hedges])

val print_strategy : ('a, 'b, 'c, 'd) manager ->
       Format.formatter -> ('a, 'b) strategy -> unit

print_strategy_vertex man fmt sv prints an object of type strategy, using the manager man for printing vertices and hyperedges.

val make_strategy_default : ?depth:int ->
       ?priority:'a PSHGraph.priority ->
       vertex_dummy:'b ->
       hedge_dummy:'a ->
       ('b, 'a, 'c, 'd, 'e) PSHGraph.t ->
       'b PSette.t -> ('b, 'a) strategy

Build a "default" strategy, with the following options:

depth: to apply the recursive strategy of Bourdoncle's paper. Default value is 2, which means that Strongly Connected Components are stabilized independently: the iteration order looks like (1 2 (3 4 5) 6 (7 8) 9) where 1, 2, 6, 9 are SCC by themselves. A higher value defines a more recursive behavior, like (1 2 (3 (4 5)) 6 (7 (8)) 9).

priority: specify which hedges should be taken into account in the computation of the iteration order and the widening points (the one such that priority h >= 0 and the widening points, and also indicates which hyperedge should be explored first at a point of choice.

One known usage for filtering: guided analysis, where one analyse a subgraph of the equation graph.

Output

type stat = {

	`time : float;`
	`iterations : int;`
	`descendings : int;`
	`stable : bool;`

}

statistics at the end of the analysis

type ('a, 'b, 'c, 'd) output = ('a, 'b, 'c, 'd, stat) PSHGraph.t

result of the analysis

val print_stat : Format.formatter -> stat -> unit

Prints statistics

val print_output : ('a, 'b, 'c, 'd) manager ->
       Format.formatter -> ('a, 'b, 'c, 'd) output -> unit

Prints the result of an analysis.

Internal datatypes

type 'a attr = {

	`mutable reach : 'a;`
	`mutable first : 'a;`
	`mutable empty : bool;`

}
type 'a arc = {

	`mutable arc : 'a;`
	`mutable aempty : bool;`

}
type ('a, 'b) infodyn = {

	`mutable iaddhedge : ('b, 'a array * 'a) PHashhe.t;`
	`iequation : ('a, 'b) equation;`

}
type ('a, 'b) info = {

	`iinit : 'a PSette.t;`
	`itime : float Pervasives.ref;`
	`iiterations : int Pervasives.ref;`
	`idescendings : int Pervasives.ref;`
	`istable : bool Pervasives.ref;`
	`mutable iworkvertex : ('a, unit) PHashhe.t;`
	`mutable iworkhedge : ('b, unit) PHashhe.t;`
	`iinfodyn : ('a, 'b) infodyn option;`

}

type ('a, 'b, 'c, 'd) graph = ('a, 'b, 'c attr, 'd arc,
        ('a, 'b) info)
       PSHGraph.t

val print_attr : ('a, 'b, 'c, 'd) manager ->
       Format.formatter -> 'c attr -> unit

val print_arc : ('a, 'b, 'c, 'd) manager ->
       Format.formatter -> 'd arc -> unit

val print_info : ('a, 'b, 'c, 'd) manager ->
       Format.formatter -> ('a, 'b) info -> unit

val print_workingsets : ('a, 'b, 'c, 'd) manager ->
       Format.formatter -> ('a, 'b, 'c, 'd) graph -> unit

val print_graph : ('a, 'b, 'c, 'd) manager ->
       Format.formatter -> ('a, 'b, 'c, 'd) graph -> unit

Prints internal graph.

DOT output

val dot_graph : ?style:string ->
       ?titlestyle:string ->
       ?vertexstyle:string ->
       ?hedgestyle:string ->
       ?strategy:('a, 'b) strategy ->
       ?vertex:'a ->
       ('a, 'b, 'c, 'd) manager ->
       ('a, 'b, 'c, 'd) graph -> title:string -> unit

Prints internal graph on the (optional) formatter man.dot_fmt, see type FixpointType.manager.