Merge pull request #614 from goblint/cfg-optimize-pick

Optimize CFG construction

src/framework/cfgTools.ml

@@ -31,8 +31,8 @@ let find_loop_heads_fun (module Cfg:CfgForward) (fd:Cil.fundec): unit NH.t =
 
   loop_heads
 
-let find_backwards_reachable (module Cfg:CfgBackward) (node:node): unit NH.t =
-  let reachable = NH.create 100 in
+let find_backwards_reachable ~initial_size (module Cfg:CfgBackward) (node:node): unit NH.t =
+  let reachable = NH.create initial_size in
 
   (* DFS, copied from Control is_sink *)
   let rec iter_node node =
@@ -53,8 +53,8 @@ module SCC =
 struct
   type t = {
     nodes: unit NH.t; (** Set of nodes in SCC, mutated during [computeSCCs]. *)
-    next: (edges * node) NH.t; (** Successor edges from this SCC to another SCC, mutated during [computeSCCs]. *)
-    prev: (edges * node) NH.t; (** Predecessor edges from another SCC to this SCC, mutated during [computeSCCs]. *)
+    next: (edges * node) list NH.t; (** Successor edges from this SCC to another SCC, mutated during [computeSCCs]. *)
+    prev: (edges * node) list NH.t; (** Predecessor edges from another SCC to this SCC, mutated during [computeSCCs]. *)
   }
   (* Identity by physical equality. *)
   let equal = (==)
@@ -64,10 +64,11 @@ end
 (** Compute strongly connected components (SCCs) of [nodes] in [Cfg].
     Returns list of SCCs and a mapping from nodes to those SCCs. *)
 let computeSCCs (module Cfg: CfgBidir) nodes =
+  let nodes_length = List.length nodes in
   (* Kosaraju's algorithm *)
   let finished_rev =
     (* first DFS to construct list of nodes in reverse finished order *)
-    let visited = NH.create 100 in
+    let visited = NH.create nodes_length in
 
     let rec dfs_inner node finished_rev =
       if not (NH.mem visited node) then (
@@ -89,7 +90,7 @@ let computeSCCs (module Cfg: CfgBidir) nodes =
   let open SCC in (* open for SCC.t constructors *)
   let (sccs, node_scc) as r =
     (* second DFS to construct SCCs on transpose graph *)
-    let node_scc = NH.create 100 in (* like visited, but values are assigned SCCs *)
+    let node_scc = NH.create nodes_length in (* like visited, but values are assigned SCCs *)
 
     let rec dfs_inner node scc =
       (* assumes: not (NH.mem node_scc node) *)
@@ -101,8 +102,8 @@ let computeSCCs (module Cfg: CfgBidir) nodes =
           else if not (NH.mem scc.nodes prev_node) then (
             (* prev_node has been visited, but not in current SCC, therefore is backwards edge to predecessor scc *)
             if Messages.tracing then Messages.trace "cfg" "SCC edge: %s -> %s\n" (Node.show_id prev_node) (Node.show_id node);
-            NH.add scc.prev node (edges, prev_node);
-            NH.add (NH.find node_scc prev_node).next prev_node (edges, node);
+            NH.modify_def [] node (List.cons (edges, prev_node)) scc.prev;
+            NH.modify_def [] prev_node (List.cons (edges, node)) (NH.find node_scc prev_node).next;
           )
         ) (Cfg.prev node) (* implicitly transpose graph by moving backwards *)
     in
@@ -111,10 +112,10 @@ let computeSCCs (module Cfg: CfgBidir) nodes =
     let sccs = List.fold_left (fun sccs node ->
         if not (NH.mem node_scc node) then
           let scc = {
-              nodes = NH.create 25;
-              next = NH.create 5;
-              prev = NH.create 5
-            }
+            nodes = NH.create 1;
+            next = NH.create 1;
+            prev = NH.create 1
+          }
           in
           dfs_inner node scc;
           scc :: sccs
@@ -136,6 +137,8 @@ let computeSCCs (module Cfg: CfgBidir) nodes =
   );
   r
 
+let computeSCCs x = Stats.time "computeSCCs" (computeSCCs x)
+
 let rec pretty_edges () = function
   | [] -> Pretty.dprintf ""
   | [_,x] -> Edge.pretty_plain () x
@@ -171,8 +174,8 @@ let createCFG (file: file) =
         Node.pretty_trace toNode;
     NH.replace fd_nodes fromNode ();
     NH.replace fd_nodes toNode ();
-    H.add cfgB toNode (edges,fromNode);
-    H.add cfgF fromNode (edges,toNode);
+    H.modify_def [] toNode (List.cons (edges,fromNode)) cfgB;
+    H.modify_def [] fromNode (List.cons (edges,toNode)) cfgF;
     if Messages.tracing then Messages.trace "cfg" "done\n\n"
   in
   let addEdge fromNode edge toNode = addEdges fromNode [edge] toNode in
@@ -380,16 +383,16 @@ let createCFG (file: file) =
           | ComputedGoto _ ->
             failwith "MyCFG.createCFG: unsupported stmt"
         in
-        List.iter handle fd.sallstmts;
+        Stats.time "handle" (List.iter handle) fd.sallstmts;
 
         if Messages.tracing then Messages.trace "cfg" "Over\n";
 
         (* Connect remaining infinite loops (e.g made using goto) to end of function
          * via pseudo return node for demand driven solvers *)
         let module TmpCfg: CfgBidir =
         struct
-          let next = H.find_all cfgF
-          let prev = H.find_all cfgB
+          let next n = H.find_default cfgF n []
+          let prev n = H.find_default cfgB n []
         end
         in
 
@@ -400,7 +403,7 @@ let createCFG (file: file) =
 
           (* DFS over SCCs starting from FunctionEntry SCC *)
           let module SH = Hashtbl.Make (SCC) in
-          let visited_scc = SH.create 13 in
+          let visited_scc = SH.create (List.length sccs) in
           let rec iter_scc scc =
             if not (SH.mem visited_scc scc) then (
               SH.replace visited_scc scc ();
@@ -443,8 +446,10 @@ let createCFG (file: file) =
                 )
               )
               else
-                NH.iter (fun _ (_, toNode) ->
-                    iter_scc (NH.find node_scc toNode)
+                NH.iter (fun _ nexts ->
+                    List.iter (fun (_, toNode) ->
+                        iter_scc (NH.find node_scc toNode)
+                      ) nexts
                   ) scc.next
             )
           in
@@ -453,47 +458,52 @@ let createCFG (file: file) =
           if !added_connect then
             iter_connect () (* added connect edge might have made a cycle of SCCs, have to recompute SCCs to see if it needs connecting *)
           else
-            NH.iter (NH.add node_scc_global) node_scc; (* there's no merge inplace *)
+            NH.iter (NH.replace node_scc_global) node_scc; (* there's no merge inplace *)
         in
-        iter_connect ();
+        Stats.time "iter_connect" iter_connect ();
 
         (* Verify that function is now connected *)
-        let reachable_return' = find_backwards_reachable (module TmpCfg) (Function fd) in
+        let reachable_return' = find_backwards_reachable ~initial_size:(NH.keys fd_nodes |> BatEnum.hard_count) (module TmpCfg) (Function fd) in
         (* TODO: doesn't check that all branches are connected, but only that there exists one which is *)
         if not (NH.mem reachable_return' (FunctionEntry fd)) then
           raise (Not_connect fd)
       | _ -> ()
     );
   if Messages.tracing then Messages.trace "cfg" "CFG building finished.\n\n";
+  if get_bool "dbg.verbose" then
+    ignore (Pretty.eprintf "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB));
   cfgF, cfgB
 
+let createCFG = Stats.time "createCFG" createCFG
+
 
 let minimizeCFG (fw,bw) =
-  let keep = H.create 113 in
+  let keep = H.create (H.length bw) in
   let comp_keep t (_,f) =
-    if (List.compare_length_with (H.find_all bw t) 1 <> 0) || (List.compare_length_with (H.find_all fw t) 1 <> 0) then
+    if (List.compare_length_with (H.find_default bw t []) 1 <> 0) || (List.compare_length_with (H.find_default fw t []) 1 <> 0) then
       H.replace keep t ();
-    if (List.compare_length_with (H.find_all bw f) 1 <> 0) || (List.compare_length_with (H.find_all fw f) 1 <> 0) then
+    if (List.compare_length_with (H.find_default bw f []) 1 <> 0) || (List.compare_length_with (H.find_default fw f []) 1 <> 0) then
       H.replace keep f ()
   in
+  let comp_keep t es = List.iter (comp_keep t) es in
   H.iter comp_keep bw;
   (* H.iter comp_keep fw; *)
-  let cfgB = H.create 113 in
-  let cfgF = H.create 113 in
-  let ready = H.create 113 in
+  let cfgB = H.create (H.length bw) in
+  let cfgF = H.create (H.length fw) in
+  let ready = H.create (H.length bw) in
   let rec add a b t (e,f)=
     if H.mem keep f then begin
-      H.add cfgB b (e@a,f);
-      H.add cfgF f (e@a,b);
+      H.modify_def [] b (List.cons (e@a,f)) cfgB;
+      H.modify_def [] f (List.cons (e@a,b)) cfgF;
       if H.mem ready b then begin
         H.replace ready f ();
-        List.iter (add [] f f) (H.find_all bw f)
+        List.iter (add [] f f) (H.find_default bw f [])
       end
     end else begin
-      List.iter (add (e@a) b f) (H.find_all bw f)
+      List.iter (add (e@a) b f) (H.find_default bw f [])
     end
   in
-  H.iter (fun k _ -> List.iter (add [] k k) (H.find_all bw k)) keep;
+  H.iter (fun k _ -> List.iter (add [] k k) (H.find_default bw k [])) keep;
   H.clear ready;
   H.clear keep;
   cfgF, cfgB
@@ -585,7 +595,7 @@ let fprint_hash_dot cfg  =
   end
   in
   let out = open_out "cfg.dot" in
-  let iter_edges f = H.iter f cfg in
+  let iter_edges f = H.iter (fun n es -> List.iter (f n) es) cfg in
   fprint_dot (module CfgPrinters (NoExtraNodeStyles)) iter_edges out
 
 
@@ -598,7 +608,7 @@ let getCFG (file: file) : cfg * cfg =
       (cfgF, cfgB)
   in
   if get_bool "justcfg" then fprint_hash_dot cfgB;
-  H.find_all cfgF, H.find_all cfgB
+  (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n [])
 
 
 (* TODO: unused *)

src/framework/constraints.ml

@@ -717,7 +717,7 @@ struct
         | Some scc when NodeH.mem scc.prev v && NodeH.length scc.prev = 1 ->
           (* Limited to loops with only one entry node. Otherwise unsound as is. *)
           (* TODO: Is it possible to do soundly for multi-entry loops? *)
-          let stricts = NodeH.find_all scc.prev v in
+          let stricts = NodeH.find_default scc.prev v [] in
           let xs_stricts = List.map tf' stricts in
           if List.for_all S.D.is_bot xs_stricts then
             S.D.bot ()

src/util/gobHashtbl.ml

@@ -0,0 +1,7 @@
+let magic_stats h =
+  let h: _ Hashtbl.t = Obj.magic h in (* Batteries Hashtables don't expose stats yet...: https://github.com/ocaml-batteries-team/batteries-included/pull/1079 *)
+  Hashtbl.stats h
+
+let pretty_statistics () (s: Hashtbl.statistics) =
+  let load_factor = float_of_int s.num_bindings /. float_of_int s.num_buckets in
+  Pretty.dprintf "bindings=%d buckets=%d max_length=%d histo=%a load=%f" s.num_bindings s.num_buckets s.max_bucket_length (Pretty.docList (Pretty.dprintf "%d")) (Array.to_list s.bucket_histogram) load_factor