Module Fixpoint

module Fixpoint: sig .. end

Fixpoint analysis of an equation system

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 = ('a, 'b, 'c, 'd) FixpointType.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	`*)`

}

Static equation system

A static equation system is defined by an hypergraph, of type PSHGraph.t, see Fixpoint.analysis_std and Fixpoint.analysis_guided

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 = ('a, 'b) FixpointType.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.

See Fixpoint.make_strategy_default to generate automatically a sound strategy.

Output

type stat = FixpointType.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

Functions

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.

val analysis_std : ('a, 'b, 'c, 'd) manager ->
       ('a, 'b, 'e, 'f, 'g) PSHGraph.t ->
       'a PSette.t -> ('a, 'b) strategy -> ('a, 'b, 'c, 'd) output

Performs initialization, fixpoint analysis and descending, and measures the global analysis time.

analysis_std manager graph sinit strategy takes a graph giving the structure of the equation system, a manager indicating how to interpret the equation system, a (super)set sinit of the variables to be initialized to a non-empty value, and an iteration strategy strategy.

val analysis_guided : ('a, 'b, 'c, 'd) manager ->
       ('a, 'b, 'e, 'f, 'g) PSHGraph.t ->
       'a PSette.t ->
       (('b -> bool) -> ('a, 'b) strategy) ->
       ('a, 'b, 'c, 'd) output

Same as Fixpoint.analysis_std, but with the technique of Gopan and Reps published in Static Anlaysis Symposium, SAS'2007.

analysis_guided manager graph sinit make_strategy: compared to Fixpoint.analysis_std, instead of providing a strategy, one provides a function make_strategy generating strategies, which takes as input a function filtering the edges to be considered. A typical value for the argument make_strategy is (fun p -> make_strategy_default ~priority:(PSHGraph.Filter p) vdummy hdummy graph sinit).

val equation_of_graph : ?filter:('a -> bool) ->
       ('b, 'a, 'c, 'd, 'e) PSHGraph.t -> ('b, 'a) equation

Generate from a graph a function of type

('vertex,
	'hedge) equation

or dynamically exploring the graph. The filter function allows to select a part of the graph.

val graph_of_equation : ('a, 'b) PSHGraph.compare ->
       ?filter:('b -> bool) ->
       make_attrvertex:('a -> 'c) ->
       make_attrhedge:('b -> 'd) ->
       info:'e ->
       ('a, 'b) equation -> 'a PSette.t -> ('a, 'b, 'c, 'd, 'e) PSHGraph.t

Generate from an equation a graph, using make_attrvertex, make_attrhedge and info.

val analysis_dyn : ('a, 'b) SHGraph.compare ->
       guided:bool ->
       ('a, 'b, 'c, 'd) manager ->
       ('a, 'b) equation ->
       'a PSette.t ->
       (('a, 'b, 'c, 'd) FixpointType.graph -> ('a, 'b) strategy) ->
       ('a, 'b, 'c, 'd) output

Dynamic analysis.

Printing Functions

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