diff --git a/CHANGES b/CHANGES index de7dbbb2..49c03731 100644 --- a/CHANGES +++ b/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 ) + version 1.8, October 4, 2011 ---------------------------- o removed ocamlyacc shift/reduce conflict in dot_parser.mly diff --git a/Makefile.in b/Makefile.in index c1adfa3f..d3160bac 100644 --- a/Makefile.in +++ b/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) diff --git a/src/fixpoint.ml b/src/fixpoint.ml new file mode 100644 index 00000000..02b4c771 --- /dev/null +++ b/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 + * 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 diff --git a/src/fixpoint.mli b/src/fixpoint.mli new file mode 100644 index 00000000..61b87ca6 --- /dev/null +++ b/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 + * 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 diff --git a/src/pack.ml b/src/pack.ml index 50b5c97f..fffd705c 100644 --- a/src/pack.ml +++ b/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