Functor MkFixpoint.Make


module Make: 
functor (Graph : SHGraph.S) -> S with module Graph = Graph
Parameters:
Graph : SHGraph.S

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

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

One known usage for filtering: guided analysis, wher eone analysis a subgraph of the equation graph.