From b62bdc46b682d0149e49a8b8298c908fe8dfe7a6 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Sat, 5 Mar 2016 09:11:48 -0800 Subject: [PATCH] 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 | 26 +++--- infer/src/checkers/registerCheckers.ml | 4 - infer/src/checkers/scheduler.ml | 105 +++++++++++++++++++++++++ infer/src/unit/inferunit.ml | 2 +- infer/src/unit/schedulerTests.ml | 105 +++++++++++++++++++++++++ 5 files changed, 226 insertions(+), 16 deletions(-) create mode 100644 infer/src/checkers/scheduler.ml create mode 100644 infer/src/unit/schedulerTests.ml diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index d74a24c07..1cf5967f8 100644 --- a/infer/src/checkers/procCfg.ml +++ b/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) diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 42931d817..caafea4c8 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/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 diff --git a/infer/src/checkers/scheduler.ml b/infer/src/checkers/scheduler.ml new file mode 100644 index 000000000..460637dac --- /dev/null +++ b/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 diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml index db0d12f0e..159bb7813 100644 --- a/infer/src/unit/inferunit.ml +++ b/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 diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml new file mode 100644 index 000000000..ac72b59ac --- /dev/null +++ b/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