adding scheduler abstraction and reverse postorder scheduler

Reviewed By: dkgi

Differential Revision: D2975916

fb-gh-sync-id: 0b9a8bf
shipit-source-id: 0b9a8bf

infer/src/checkers/procCfg.ml

@@ -13,16 +13,22 @@ module F = Format
 (** control-flow graph for a single procedure (as opposed to cfg.ml, which represents a cfg for a
     file). *)
 
-(* wrapper that allows us to do tricks like turn a forward cfg to into a backward one *)
-module type Wrapper = sig
+module type Base = sig
   type t
   type node
   type node_id
 
   val node_id : node -> node_id
+  val node_id_compare : node_id -> node_id -> int
   val succs : t -> node -> node list
-  val exn_succs : t -> node -> node list
   val preds : t -> node -> node list
+end
+
+(* wrapper that allows us to do tricks like turn a forward cfg to into a backward one *)
+module type Wrapper = sig
+  include Base
+
+  val exn_succs : t -> node -> node list
   val start_node : t -> node
   val exit_node : t -> node
   val instrs : node -> Sil.instr list
@@ -32,8 +38,6 @@ module type Wrapper = sig
 
   val from_pdesc : Cfg.Procdesc.t -> t
 
-  val node_id_compare : node_id -> node_id -> int
-
   val pp_node : F.formatter -> node -> unit
   val pp_node_id : F.formatter -> node_id -> unit
 
@@ -79,12 +83,12 @@ module Backward (W : Wrapper) : Wrapper = struct
 
 end
 
-module NodeIdMap (W : Wrapper) = Map.Make(struct
-    type t = W.node_id
-    let compare = W.node_id_compare
+module NodeIdMap (B : Base) = Map.Make(struct
+    type t = B.node_id
+    let compare = B.node_id_compare
   end)
 
-module NodeIdSet (W : Wrapper) = Set.Make(struct
-    type t = W.node_id
-    let compare = W.node_id_compare
+module NodeIdSet (B : Base) = Set.Make(struct
+    type t = B.node_id
+    let compare = B.node_id_compare
   end)

infer/src/checkers/registerCheckers.ml

@@ -56,7 +56,3 @@ let register () =
     if active then registry language_opt callback in
   IList.iter (register Callbacks.register_procedure_callback) (active_procedure_checkers ());
   IList.iter (register Callbacks.register_cluster_callback) (active_cluster_checkers ())
-
-module Test (C : ProcCfg.Wrapper) = struct
-
-end

infer/src/checkers/scheduler.ml

@@ -0,0 +1,105 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+module F = Format
+module L = Logging
+
+module type S = functor (C : ProcCfg.Base) -> sig
+  type t
+
+  (* schedule the successors of [node] *)
+  val schedule_succs : t -> C.node -> t
+  (* remove and return the node with the highest priority, the ids of its visited
+     predecessors, and the new schedule *)
+  val pop : t -> C.node * C.node_id list * t
+  val empty : C.t -> t
+
+  exception Empty
+
+end
+
+(* simple scheduler that visits CFG nodes in reverse postorder. fast/precise for straightline code
+   and conditionals; not as good for loops (may visit nodes after a loop multiple times). *)
+module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
+  module M = ProcCfg.NodeIdMap (C)
+  exception Empty
+
+  module WorkUnit = struct
+    module IdSet = ProcCfg.NodeIdSet(C)
+
+    type t = {
+      node : C.node; (* node whose instructions will be analyzed *)
+      visited_preds : IdSet.t ; (* predecessors of [node] we have already visited in current iter *)
+      priority : int; (* |preds| - |visited preds|. *)
+    }
+
+    let node t = t.node
+
+    let visited_preds t = IdSet.elements t.visited_preds
+
+    let priority t = t.priority
+
+    let compute_priority cfg node visited_preds =
+      IList.length (C.preds cfg node) - IdSet.cardinal visited_preds
+
+    let make cfg node =
+      let visited_preds = IdSet.empty in
+      let priority = compute_priority cfg node visited_preds in
+      { node; visited_preds; priority; }
+
+    (* add [node_id] to the visited preds for [t] *)
+    let add_visited_pred cfg t node_id =
+      let visited_preds' = IdSet.add node_id t.visited_preds in
+      let priority' = compute_priority cfg t.node visited_preds' in
+      { t with visited_preds = visited_preds'; priority = priority'; }
+
+  end
+
+  type t = { worklist : WorkUnit.t M.t; cfg : C.t; }
+
+  (* schedule the succs of [node] for analysis *)
+  let schedule_succs t node =
+    let node_id = C.node_id node in
+    (* mark [node] as a visited pred of [node_to_schedule] and schedule it *)
+    let schedule_succ worklist_acc node_to_schedule =
+      let id_to_schedule = C.node_id node_to_schedule in
+      let old_work =
+        try M.find id_to_schedule worklist_acc
+        with Not_found -> WorkUnit.make t.cfg node_to_schedule in
+      let new_work = WorkUnit.add_visited_pred t.cfg old_work node_id in
+      M.add id_to_schedule new_work worklist_acc in
+    let new_worklist = IList.fold_left schedule_succ t.worklist (C.succs t.cfg node) in
+    { t with worklist = new_worklist; }
+
+  (* remove and return the node with the highest priority (note that smaller integers have higher
+     priority), the ids of its visited predecessors, and new schedule *)
+  (* TODO: could do this slightly more efficiently by keeping a list of priority zero nodes for
+     quick popping, and do a linear search only when this list is empty *)
+  let pop t =
+    let max_priority_id, _ =
+      try
+        let init_id, init_work = M.choose t.worklist in
+        let init_priority = WorkUnit.priority init_work in
+        M.fold
+          (fun id work (lowest_id, lowest_priority) ->
+             let priority = WorkUnit.priority work in
+             if priority < lowest_priority
+             then id, priority
+             else lowest_id, lowest_priority)
+          t.worklist
+          (init_id, init_priority)
+      with Not_found -> raise Empty in
+    let max_priority_work = M.find max_priority_id t.worklist in
+    let node = WorkUnit.node max_priority_work in
+    let t' = { t with worklist = M.remove (C.node_id node) t.worklist } in
+    node, WorkUnit.visited_preds max_priority_work, t'
+
+  let empty cfg = { worklist = M.empty; cfg; }
+
+end

infer/src/unit/inferunit.ml

@@ -13,6 +13,6 @@ module L = Logging
 
 let () =
   let open OUnit2 in
-  let tests = [] in
+  let tests = [SchedulerTests.tests] in
   let test_suite = "all" >::: tests in
   OUnit2.run_test_tt_main test_suite

infer/src/unit/schedulerTests.ml

@@ -0,0 +1,105 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+module F = Format
+
+
+(* mock for creating CFG's from adjacency lists *)
+module MockProcCfg = struct
+  type node = int
+  type node_id = int
+  type t = (node * node list) list
+
+  let node_id_compare = int_compare
+
+  let node_id n = n
+
+  let succs t n =
+    try
+      IList.find (fun (node, _) -> node_id_compare node n = 0) t
+      |> snd
+    with Not_found -> []
+
+  let preds t n =
+    try
+      IList.filter
+        (fun (_, succs) -> IList.exists (fun node -> node_id_compare node n = 0) succs) t
+      |> IList.map fst
+    with Not_found -> []
+
+  let from_adjacency_list t = t
+
+end
+
+module S = Scheduler.ReversePostorder (MockProcCfg)
+
+let create_test test_graph expected_result _ =
+  (* keep popping and scheduling until the queue is empty, record the results *)
+  let rec pop_schedule_record q visited_acc =
+    try
+      let n, _, q' = S.pop q in
+      pop_schedule_record (S.schedule_succs q' n) (n :: visited_acc)
+    with S.Empty -> IList.rev visited_acc in
+  let pp_diff fmt (exp, actual) =
+    let pp_sched fmt l =
+      F.pp_print_list ~pp_sep:F.pp_print_space (fun fmt i -> F.fprintf fmt "%d" i) fmt l in
+    F.fprintf fmt "Expected schedule %a but got schedule %a" pp_sched exp pp_sched actual in
+  let cfg = MockProcCfg.from_adjacency_list test_graph in
+  let q = S.schedule_succs (S.empty cfg) 1 in
+  let result = pop_schedule_record q [1] in
+  OUnit2.assert_equal ~pp_diff result expected_result
+
+let tests =
+  let open OUnit2 in
+  let test_list = [
+    ("straightline",
+     [(1, [2]);
+      (2, [3]);
+      (3, [4])],
+     [1; 2; 3; 4]);
+    ("if_then_else",
+     [(1, [2; 3]);
+      (2, [4]);
+      (3, [4]);
+      (4, [5])],
+     [1; 2; 3; 4; 5]);
+    ("if_then",
+     [(1, [2; 4]);
+      (2, [3]);
+      (3, [4]);
+      (4, [5])],
+     [1; 2; 3; 4; 5]);
+    ("diamond",
+     [(1, [2; 3]);
+      (2, [4]);
+      (3, [4]);
+      (4, [5; 6]);
+      (5, [7]);
+      (6, [7]);
+      (7, [8])],
+     [1; 2; 3; 4; 5; 6; 7; 8]);
+    ("switch",
+     [(1, [2; 3; 4; 5;]);
+      (2, [6]);
+      (3, [6]);
+      (4, [6]);
+      (5, [6]);
+      (6, [7])],
+     [1; 2; 3; 4; 5; 6; 7;]);
+    ("nums_order_irrelevant",
+     [(11, [10];);
+      (1, [7; 2]);
+      (2, [3; 11]);
+      (7, [11]);
+      (3, [7]);],
+     [1; 2; 3; 7; 11; 10]);
+  ]
+    |> IList.map
+      (fun (name, test, expected) -> name>::create_test test expected) in
+  "scheduler_suite">:::test_list