Module Fixpoint

module Fixpoint: sig .. end
Fixpoint analysis of an equation system



The manager parameterizes the fixpoint solver with the following types: and values:
type ('vertex, 'hedge, 'abstract, 'arc) manager = ('vertex, 'hedge, 'abstract, 'arc) FixpointType.manager = {
   mutable bottom :'vertex -> 'abstract; (*Create a bottom value*)
   mutable canonical :'vertex -> 'abstract -> unit; (*Make an abstract value canonical*)
   mutable is_bottom :'vertex -> 'abstract -> bool; (*Emptiness test*)
   mutable is_leq :'vertex -> 'abstract -> 'abstract -> bool; (*Inclusion test*)
   mutable join :'vertex -> 'abstract -> 'abstract -> 'abstract;
   mutable join_list :'vertex -> 'abstract list -> 'abstract; (*Binary and n-ary join operation*)
   mutable widening :'vertex -> 'abstract -> 'abstract -> 'abstract; (*Apply widening at the given point, with the two arguments. Widening will always be applied with first argument being included in the second one.*)
   mutable odiff :('vertex -> 'abstract -> 'abstract -> 'abstract) option; (*Sound approximation of set difference (optional)*)
   mutable abstract_init :'vertex -> 'abstract; (*Return the non-bottom initial value associated to the given vertex*)
   mutable arc_init :'hedge -> 'arc; (*Initial value for arcs*)
   mutable apply :'hedge -> 'abstract array -> 'arc * 'abstract; (*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 -> 'vertex -> unit;
   mutable print_hedge :Format.formatter -> 'hedge -> unit;
   mutable print_abstract :Format.formatter -> 'abstract -> unit;
   mutable print_arc :Format.formatter -> 'arc -> 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 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 -> 'vertex -> unit; (*Print vertex identifiers in DOT format*)
   mutable dot_hedge :Format.formatter -> 'hedge -> 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 -> 'vertex -> unit; (*Print the displayed information in boxes*)
   mutable dot_attrhedge :Format.formatter -> 'hedge -> 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 ('vertex, 'hedge) equation = 'vertex -> ('hedge, 'vertex array * 'vertex) 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 strategy_iteration = FixpointType.strategy_iteration = {
   mutable widening_start :int; (*Nb of initial steps without widening in the current strategy*)
   mutable widening_descend :int; (*Maximum nb. of descending steps in the current strategy*)
   mutable ascending_nb :int; (*For stats*)
   mutable descending_nb :int; (*For stats*)
   mutable descending_stable :bool; (*For stats*)
Widening and Descending Options
type ('vertex, 'hedge) strategy_vertex = ('vertex, 'hedge) FixpointType.strategy_vertex = {
   mutable vertex :'vertex;
   mutable hedges :'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.
type ('vertex, 'hedge) strategy = (strategy_iteration, ('vertex, 'hedge) strategy_vertex)
Type for defining iteration strategies. For instance, [1; [2;3]; 4; [5]; 6] means: Moreover, to each (imbricated) list is associated a record of type strategy_iteration, which indicates when to start the widening, and the maximum number of descending iterations.

Some observations on this example:

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.


type stat_iteration = FixpointType.stat_iteration = {
   mutable nb :int;
   mutable stable :bool;
type stat = FixpointType.stat = {
   mutable time :float;
   mutable ascending :(stat_iteration, unit) Ilist.t;
   mutable descending :(stat_iteration, unit) Ilist.t;
statistics at the end of the analysis
type ('vertex, 'hedge, 'abstract, 'arc) output = ('vertex, 'hedge, 'abstract, 'arc, stat) PSHGraph.t 
result of the analysis


val make_strategy_default : ?depth:int ->
?widening_start:int ->
?widening_descend:int ->
?priority:'hedge PSHGraph.priority ->
vertex_dummy:'vertex ->
hedge_dummy:'hedge ->
('vertex, 'hedge, 'e, 'f, 'g) PSHGraph.t ->
'vertex PSette.t -> ('vertex, 'hedge) strategy
Build a "default" strategy, with the following options:

One known usage for filtering: guided analysis, where one analyse a subgraph of the equation graph.
val analysis_std : ('vertex, 'hedge, 'abstract, 'arc) manager ->
('vertex, 'hedge, 'e, 'f, 'g) PSHGraph.t ->
'vertex PSette.t ->
('vertex, 'hedge) strategy ->
('vertex, 'hedge, 'abstract, 'arc) 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 : ('vertex, 'hedge, 'attr, 'arc) manager ->
('vertex, 'hedge, 'e, 'f, 'g) PSHGraph.t ->
'vertex PSette.t ->
(('hedge -> bool) -> ('vertex, 'hedge) strategy) ->
('vertex, 'hedge, 'attr, 'arc) 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:('hedge -> bool) ->
('vertex, 'hedge, 'attr, 'arc, 'e) PSHGraph.t ->
('vertex, 'hedge) 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 : ('vertex, 'hedge) ->
?filter:('hedge -> bool) ->
make_attrvertex:('vertex -> 'attr) ->
make_attrhedge:('hedge -> 'arc) ->
info:'e ->
('vertex, 'hedge) equation ->
'vertex PSette.t -> ('vertex, 'hedge, 'attr, 'arc, 'e) PSHGraph.t
Generate from an equation a graph, using make_attrvertex, make_attrhedge and info.
val analysis_dyn : ('a, 'b) ->
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 : ('vertex, 'hedge, 'attr, 'arc) manager ->
Format.formatter -> ('vertex, 'hedge, 'attr, 'arc) output -> unit
Prints the result of an analysis.