Merge branch 'sail2' into rmem_interpreter

1 files changed, 19 insertions, 8 deletions

diff --git a/src/graph.ml b/src/graph.ml
index e3af0b97..703deba9 100644
--- a/src/graph.ml
+++ b/src/graph.ml
@@ -69,6 +69,15 @@ module type S =
     val add_edge : node -> node -> graph -> graph
     val add_edges : node -> node list -> graph -> graph
 
+    (** Add edges to the graph, but may leave the internal structure
+       of the graph in a non-normalized state. Fix leaves repairs any
+       such issue in the graph. These additional functions are much
+       faster than those above, but it is important to call fix_leaves
+       before calling reachable, prune, or any other function. *)
+    val add_edge' : node -> node -> graph -> graph
+    val add_edges' : node -> node list -> graph -> graph
+    val fix_leaves : graph -> graph
+
     val children : graph -> node -> node list
 
     (** Return the set of nodes that are reachable from the first set
@@ -119,19 +128,21 @@ module Make(Ord: OrderedType) = struct
   let fix_leaves cg =
     NS.fold (fun leaf cg -> if NM.mem leaf cg then cg else NM.add leaf NS.empty cg) (leaves cg) cg
 
-  (* FIXME: don't use fix_leaves because this is inefficient *)
-  let add_edge caller callee cg =
+  let add_edge' caller callee cg =
     try
-      fix_leaves (NM.add caller (NS.add callee (NM.find caller cg)) cg)
+      NM.add caller (NS.add callee (NM.find caller cg)) cg
     with
-    | Not_found -> fix_leaves (NM.add caller (NS.singleton callee) cg)
+    | Not_found -> NM.add caller (NS.singleton callee) cg
 
-  let add_edges caller callees cg =
+  let add_edges' caller callees cg =
     let callees = List.fold_left (fun s c -> NS.add c s) NS.empty callees in
     try
-      fix_leaves (NM.add caller (NS.union callees (NM.find caller cg)) cg)
+      NM.add caller (NS.union callees (NM.find caller cg)) cg
     with
-    | Not_found -> fix_leaves (NM.add caller callees cg)
+    | Not_found -> NM.add caller callees cg
+
+  let add_edge caller callee cg = fix_leaves (add_edge' caller callee cg)
+  let add_edges caller callees cg = fix_leaves (add_edges' caller callees cg)
 
   let reachable roots cuts cg =
     let visited = ref NS.empty in
@@ -223,6 +234,6 @@ module Make(Ord: OrderedType) = struct
     NM.bindings graph |> List.iter (fun (from_node, _) -> make_node from_node);
     NM.bindings graph |> List.iter (fun (from_node, to_nodes) -> NS.iter (make_line from_node) to_nodes);
     output_string out_chan "}\n";
-    Util.opt_colors := true;
+    Util.opt_colors := true
 
 end