new module Fixpoint

CHANGES

@@ -1,3 +1,8 @@
+
+ o new module Fixpoint to compute fixpoints using the work-list
+   algorithm, e.g. for data flow analysis
+   (contributed by Markus W. Weissmann <[email protected]>)
+
 version 1.8, October 4, 2011
 ----------------------------
  o removed ocamlyacc shift/reduce conflict in dot_parser.mly

Makefile.in

@@ -71,7 +71,7 @@ CMO = 	version util blocks persistent imperative \
 	delaunay builder classic rand oper \
 	path traverse coloring topological components kruskal flow \
         graphviz gml dot_parser dot_lexer dot pack \
-	gmap minsep cliquetree mcs_m md strat
+	gmap minsep cliquetree mcs_m md strat fixpoint
 CMO := $(LIB) $(patsubst %, $(SRCDIR)/%.cmo, $(CMO))
 
 CMX = $(CMO:.cmo=.cmx)

src/fixpoint.ml

@@ -0,0 +1,175 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Ocamlgraph: a generic graph library for OCaml                         *)
+(*  Copyright (C) 2004-2010                                               *)
+(*  Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles        *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Copyright (c) 2010 - 2011 Technische Universitaet Muenchen
+ * Markus W. Weissmann <[email protected]>
+ * All rights reserved. *)
+
+(* maximum fixpoint point calculation with the work list algorithm;
+   to implement a concrete analysis, implement a module that satisfies
+   the Rules signature. Such a module in the Analysis functor gives a
+   complete analysis/optimization module that works on a CFG.
+*)
+
+type direction = Forward | Backward
+
+module type Analysis = sig
+  type data
+  type label
+  type vertex
+  type cfg
+
+  val direction : direction
+  val join : data -> data -> data
+  val equal : data -> data -> bool
+  val analyze : label -> data -> data
+end
+
+(** Minimal graph signature for work list algorithm *)
+module type G = sig
+  type t
+  module V : Sig.COMPARABLE
+  module E : sig
+    type t
+    type label
+    val label : t -> label
+    val dst : t -> V.t
+    val src : t -> V.t
+  end
+  val fold_vertex : (V.t -> 'a -> 'a) -> t -> 'a -> 'a
+  val succ_e : t -> V.t -> E.t list
+  val pred_e : t -> V.t -> E.t list
+  val succ : t -> V.t -> V.t list
+  val pred : t -> V.t -> V.t list
+end
+
+
+module Make
+  (G : G)
+  (A : Analysis with type cfg = G.t with type label = G.E.label
+with type vertex = G.V.t) =
+struct
+
+  module M = Map.Make(G.V)
+  module N = Set.Make(G.V)
+
+  let analyze initial cfg =
+    let (nodes, data) =
+      G.fold_vertex
+        (fun vertex (n, m) ->
+           (N.add vertex n, M.add vertex (initial vertex) m))
+        cfg (N.empty, M.empty)
+    in
+    (* generate an associative map to quickly find the incoming
+     * (outgoing) edges of a node during the anaysis store a pair of
+     * a partially applied analysis function and the corresponding
+     * 'partner' node *)
+    let nodemap : ((A.data -> A.data) * G.V.t) list M.t =
+      let add = match A.direction with
+        | Forward ->
+            (fun n ->
+               let preds = G.pred_e cfg n in
+               List.map
+                 (fun edge -> (A.analyze (G.E.label edge), G.E.src edge))
+                 preds)
+        | Backward ->
+            (fun n ->
+               let succs = G.succ_e cfg n in
+               List.map
+                 (fun edge -> (A.analyze (G.E.label edge), G.E.dst edge))
+                 succs)
+      in
+      G.fold_vertex (fun vertex m -> M.add vertex (add vertex) m) cfg M.empty
+    in
+
+    let rec worklist (data : A.data M.t) (wl : N.t) =
+      (* 'meet' an arbitrary number of data-sets *)
+      let meet ~default = function
+        | [] -> default
+        | [x] -> x
+        | x::xs -> List.fold_left (fun a b -> A.join a b) x xs
+      in
+
+      (* analyze one node, creating a new data-set and node-worklist
+         as necessary *)
+      let analyze_node analysis n d wl =
+        match analysis d n with
+          | None -> (d, wl)
+          | Some d' -> (d', N.add n wl)
+      in
+
+      try
+        (* get some node from the node-set -- this will eventually trigger
+           an exception *)
+        let n = N.choose wl in
+        (* remove the chosen node from the set *)
+        let wl = N.remove n wl in
+
+        let (f, ns) = match A.direction with
+            (* analyze all INCOMING edges of all SUCCESSOR nodes of the
+               node to be processed *)
+          | Forward ->
+              (* process one node: analyze all it's incoming edges
+                 and merge the resulting data;
+                 if the result is different to the previously stored data
+                 for this node, return a new tuple, else None *)
+              let new_node_data (data : A.data M.t) node =
+                let edges = M.find node nodemap in
+                let analysis =
+                  List.map
+                    (fun (f, src) -> f (M.find src data)) edges
+                in
+                let node_data = M.find node data in
+                let node_data' = meet ~default:node_data analysis in
+                if A.equal node_data node_data' then None
+                else Some (M.add node node_data' data)
+              in
+
+              (new_node_data, G.succ cfg n)
+                (* analyze all OUTGOING edges of all PREDECESSOR nodes
+                   of the node to be processed *)
+          | Backward ->
+              let new_node_data (data : A.data M.t) node =
+                let edges = M.find node nodemap in
+                let analysis =
+                  List.map
+                    (fun (f, dst) -> f (M.find dst data)) edges
+                in
+                let node_data = M.find node data in
+                let node_data' = meet ~default:node_data analysis in
+                if A.equal node_data node_data' then None
+                else Some (M.add node node_data' data)
+              in
+
+              (new_node_data, G.pred cfg n)
+        in
+        (* analyze all successor nodes by analyzing all of their
+           predecessor edges *)
+        let (data, wl) =
+          List.fold_left (fun (d, wl) n -> analyze_node f n d wl)
+            (data, wl) ns
+        in
+
+        (* do a recursive call: the recursion will eventually end with a
+         * Not_found exception when no nodes are left in the work list *)
+        worklist data wl
+
+      with Not_found -> data
+    in
+    let data = worklist data nodes in
+    (fun n -> M.find n data)
+end

src/fixpoint.mli

@@ -0,0 +1,77 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Ocamlgraph: a generic graph library for OCaml                         *)
+(*  Copyright (C) 2004-2010                                               *)
+(*  Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles        *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Copyright (c) 2010 - 2011 Technische Universitaet Muenchen
+ * Markus W. Weissmann <[email protected]>
+ * All rights reserved. *)
+
+(** Fixpoint computation implemented using the work list algorithm.
+    This module makes writing data-flow analysis easy. *)
+
+(** Minimal graph signature for work list algorithm *)
+module type G = sig
+  type t
+  module V : Sig.COMPARABLE
+  module E : sig
+    type t
+    type label
+    val label : t -> label
+    val dst : t -> V.t
+    val src : t -> V.t
+  end
+  val fold_vertex : (V.t -> 'a -> 'a) -> t -> 'a -> 'a
+  val succ_e : t -> V.t -> E.t list
+  val pred_e : t -> V.t -> E.t list
+  val succ : t -> V.t -> V.t list
+  val pred : t -> V.t -> V.t list
+end
+
+type direction = Forward | Backward
+(** Type of an analysis *)
+
+module type Analysis = sig
+  type data
+    (** information stored at each vertex *)
+  type label
+    (** the label of edges of the underlying graph *)
+  type vertex
+    (** type of a vertex of the underlying graph *)
+  type cfg
+    (** type of the underlying graph *)
+  val direction : direction
+    (** the direction of the analysis *)
+  val join : data -> data -> data
+    (** operation how to join data when paths meet *)
+  val equal : data -> data -> bool
+    (** predicate to determine the fixpoint *)
+  val analyze : label -> data -> data
+    (** the actual analysis of one label; provided the label and the incoming
+        data, it needs to compute the outgoing data *)
+  end
+
+module Make
+  (G : G)
+  (A : Analysis with type cfg = G.t with type label = G.E.label
+                with type vertex = G.V.t) :
+sig
+  val analyze : (G.V.t -> A.data) -> A.cfg -> G.V.t -> A.data
+  (** [analyze f g] computes the fixpoint on the given graph using the
+      work list algorithm. Beware that a misconstructed Analysis will
+      not terminate! [f] is used to create the initial analysis
+      data. The function returned is a map to see what data was computed
+      for which node. *)
+end

src/pack.ml

@@ -17,17 +17,17 @@
 
 (* $Id: pack.ml,v 1.13 2006-05-12 14:07:16 filliatr Exp $ *)
 
-module Generic(G : Sig.IM with type V.label = int and type E.label = int) = 
+module Generic(G : Sig.IM with type V.label = int and type E.label = int) =
 struct
 
   include G
 
   exception Found of V.t
   let find_vertex g i =
-    try 
+    try
       iter_vertex (fun v -> if V.label v = i then raise (Found v)) g;
       raise Not_found
-    with Found v -> 
+    with Found v ->
       v
 
   module Builder = Builder.I(G)
@@ -42,7 +42,7 @@ struct
 
   module Components = Components.Make(G)
 
-  module W = struct 
+  module W = struct
     type label = int
     type t = int
     let weight x = x
@@ -68,13 +68,13 @@ struct
   end
 
   module FF = Flow.Ford_Fulkerson(G)(F)
-  let ford_fulkerson g = 
-    if not G.is_directed then 
+  let ford_fulkerson g =
+    if not G.is_directed then
       invalid_arg "ford_fulkerson: not a directed graph";
     FF.maxflow g
 
   module Goldberg = Flow.Goldberg(G)(F)
-  let goldberg g = 
+  let goldberg g =
     if not G.is_directed then invalid_arg "goldberg: not a directed graph";
     Goldberg.maxflow g
 
@@ -104,7 +104,7 @@ struct
   module Dot_ = Graphviz.Dot(Display)
   module Neato = Graphviz.Neato(Display)
 
-  let dot_output g f = 
+  let dot_output g f =
     let oc = open_out f in
     if is_directed then Dot_.output_graph oc g else Neato.output_graph oc g;
     close_out oc
@@ -115,11 +115,11 @@ struct
     ignore (Sys.command ("dot -Tps " ^ tmp ^ " | gv -"));
     Sys.remove tmp
 
-  module GmlParser = 
+  module GmlParser =
     Gml.Parse
       (Builder)
-      (struct 
-	 let node l = 
+      (struct
+	 let node l =
 	   try match List.assoc "id" l with Gml.Int n -> n | _ -> -1
 	   with Not_found -> -1
 	 let edge _ =
@@ -134,10 +134,10 @@ struct
       (struct
  	 let nodes = Hashtbl.create 97
 	 let new_node = ref 0
-	 let node (id,_) _ = 
-	   try 
+	 let node (id,_) _ =
+	   try
 	     Hashtbl.find nodes id
-	   with Not_found -> 
+	   with Not_found ->
 	     incr new_node;
 	     Hashtbl.add nodes id !new_node;
 	     !new_node
@@ -166,9 +166,9 @@ struct
 end
 
 module I = struct
-  type t = int 
+  type t = int
   let compare : t -> t -> int = Pervasives.compare
-  let hash = Hashtbl.hash 
+  let hash = Hashtbl.hash
   let equal = (=)
   let default = 0
 end