Module type MkFixpoint.S

module type S = sig .. end

module Graph: SHGraph.S

Datatypes

Manager

type ('a, 'b) manager = {

`mutable bottom : Graph.vertex -> 'a;`	`(*`	Create a bottom value	`*)`
`mutable canonical : Graph.vertex -> 'a -> unit;`	`(*`	Make an abstract value canonical	`*)`
`mutable is_bottom : Graph.vertex -> 'a -> bool;`	`(*`	Emptiness test	`*)`
`mutable is_leq : Graph.vertex -> 'a -> 'a -> bool;`	`(*`	Inclusion test	`*)`
`mutable join : Graph.vertex -> 'a -> 'a -> 'a;`
`mutable join_list : Graph.vertex -> 'a list -> 'a;`	`(*`	Binary and n-ary join operation	`*)`
`mutable widening : Graph.vertex -> 'a -> 'a -> 'a;`	`(*`	Apply widening at the given point, with the two arguments	`*)`
`mutable apply : Graph.hedge -> 'a array -> 'b * 'a;`	`(*`	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 arc_init : Graph.hedge -> 'b;`	`(*`	Initial value for arcs	`*)`
`mutable get_init : Graph.vertex -> 'a;`	`(*`	Return the initial value associated to the given vertex	`*)`
`mutable print_abstract : Format.formatter -> 'a -> unit;`
`mutable print_arc : Format.formatter -> 'b -> unit;`
`mutable print_vertex : Format.formatter -> Graph.vertex -> unit;`
`mutable print_hedge : Format.formatter -> Graph.hedge -> unit;`
`mutable widening_first : bool;`	`(*`	When to apply widening from first non bottom value.	`*)`
`mutable widening_start : int;`	`(*`	First widening step	`*)`
`mutable widening_freq : int;`	`(*`	widening every n steps	`*)`
`mutable widening_descend : int;`	`(*`	Maximum nb. of descending steps	`*)`
`mutable print_analysis : bool;`
`mutable print_step : bool;`
`mutable print_state : bool;`
`mutable print_postpre : bool;`

}

Iteration strategies

type strategy_vertex = {

`mutable vertex : Graph.vertex;`
`mutable hedges : Graph.hedge 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 strategy = 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.

Result

type stat = {

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

}

statistics at the end of the analysis

type ('a, 'b) output = ('a, 'b, stat) Graph.t

result of the analysis

Internal datatype

type ('a, 'b) graph

Printing functions

val print_strategy_vertex : ('a, 'b) manager ->
       Format.formatter -> 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

(vertex,[list of
	hedges],boolean)

val print_strategy : ('a, 'b) manager ->
       Format.formatter -> 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_graph : ('a, 'b) manager ->
       Format.formatter -> ('a, 'b) graph -> unit

Prints internal graph.

print_graph man print_arc fmt graph prints an object of (abstract) type ('abstract,'arc) graph, using print_arc for printing the information associated to hyperedges.

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

Prints statistics

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

Prints the result of an analysis.

print_graph man print_arc fmt graph prints an object of type 'arc output, using print_arc for printing the information associated to hyperedges.

Main Functions

val init : ('a, 'b) manager ->
       ('c, 'd, 'e) Graph.t -> Graph.SetV.t -> ('a, 'b) graph

init manager inputgraph sinit creates an internal graph and initializes it.

Only the structure of inputgraph is used.
sinit is the set of vertices with non-bottom initial values. Initial values are obtained by calling the function manager.get_init on these vertices.

val fixpoint : ('a, 'b) manager ->
       ('a, 'b) graph -> strategy -> unit

fixpoint manager graph strategy computes a fixpoint (or a postfixpoint in case of widening) of the system of equation represented by graph. The iteration order (and set of widening points) is specified by the argument strategy.

val descend : ('a, 'b) manager ->
       ('a, 'b) graph -> strategy -> bool

descend manager graph sinit strategy performs several descending steps, depending on the option manager.widening_descend. strategy is used only for the ordering of connex components and the iteration ordering inside them.

val analysis : ('a, 'b) manager ->
       ('c, 'd, 'e) Graph.t ->
       Graph.SetV.t -> strategy -> ('a, 'b) graph

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

val analysis_guided : ?depth:int ->
       ?priority:(Graph.hedge -> int) ->
       ?modify_strategy:(strategy -> strategy) ->
       ('a, 'b) manager ->
       ('c, 'd, 'e) Graph.t -> Graph.SetV.t -> ('a, 'b) graph

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

val output_of_graph : ('a, 'b) graph -> ('a, 'b) output

Getting the result of the analysis.

Utility functions

val strategy_default : ?depth:int ->
       ?priority:(Graph.hedge -> int) ->
       ('a, 'b, 'c) Graph.t -> Graph.SetV.t -> strategy

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

depth: to apply the recursive strategy of Bourdncle'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, wher eone analysis a subgraph of the equation graph.