From 8ef9bf7641a616fcf57cdff36e42f402ded433de Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 16 Oct 2018 07:37:13 -0700 Subject: [PATCH] Expose WTO in ProcCfg Reviewed By: jberdine Differential Revision: D10376596 fbshipit-source-id: 0162a5cf3 --- infer/src/IR/Procdesc.mli | 4 +- infer/src/IR/WeakTopologicalOrder.ml | 23 ++++++++ infer/src/IR/WeakTopologicalOrder.mli | 12 ++++- infer/src/absint/AbstractInterpreter.ml | 12 ++--- infer/src/absint/ProcCfg.ml | 60 ++++++++++++++++++--- infer/src/absint/ProcCfg.mli | 2 + infer/src/istd/IContainer.ml | 5 ++ infer/src/istd/IContainer.mli | 2 + infer/src/unit/schedulerTests.ml | 12 +++++ infer/src/unit/weakTopologicalOrderTests.ml | 2 + 10 files changed, 114 insertions(+), 20 deletions(-) diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 68aac8d6c..8cda7cd23 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -270,7 +270,9 @@ val set_exit_node : t -> Node.t -> unit val set_start_node : t -> Node.t -> unit val signal_did_preanalysis : t -> unit -(** indicate that we have performed preanalysis on the CFG assoociated with [t] *) +(** indicate that we have performed preanalysis on the CFG associated with [t] *) + +val get_wto : t -> Node.t WeakTopologicalOrder.Partition.t val is_loop_head : t -> Node.t -> bool diff --git a/infer/src/IR/WeakTopologicalOrder.ml b/infer/src/IR/WeakTopologicalOrder.ml index 9df46cb79..60eb6608c 100644 --- a/infer/src/IR/WeakTopologicalOrder.ml +++ b/infer/src/IR/WeakTopologicalOrder.ml @@ -18,6 +18,8 @@ module Partition = struct let add_node node next = Node {node; next} + let prepend_node next node = Node {node; next} + let add_component head rest next = Component {head; rest; next} let rec fold_heads partition ~init ~f = @@ -32,6 +34,27 @@ module Partition = struct (fold_heads [@tailcall]) next ~init ~f + let rec expand ~fold_right partition = + match partition with + | Empty -> + Empty + | Node {node; next} -> + let init = expand ~fold_right next in + fold_right node ~init ~f:prepend_node + | Component {head; rest; next} -> ( + let next = expand ~fold_right next in + let init = expand ~fold_right rest in + match fold_right head ~init ~f:prepend_node with + | Empty | Component _ -> + (* [fold_right] is expected to always provide a non-empty sequence. + Hence the result of [fold_right ~f:prepend_node] will always start with a Node. *) + Logging.(die InternalError) + "WeakTopologicalOrder.Partition.expand: the expansion function fold_right should \ + not return ~init directly" + | Node {node= head; next= rest} -> + Component {head; rest; next} ) + + let rec pp ~prefix ~pp_node fmt = function | Empty -> () diff --git a/infer/src/IR/WeakTopologicalOrder.mli b/infer/src/IR/WeakTopologicalOrder.mli index c1f7f4eb5..3ac06e712 100644 --- a/infer/src/IR/WeakTopologicalOrder.mli +++ b/infer/src/IR/WeakTopologicalOrder.mli @@ -28,6 +28,12 @@ module Partition : sig val fold_heads : ('node t, 'node, _) Container.fold + val expand : fold_right:('a, 'b, 'b t) Container.fold -> 'a t -> 'b t + (** Maps a partition nodes from ['a] to ['b] using the expansion [fold_right]. + [fold_right] should not return its [~init] directly but must always provide + a non-empty sequence. + *) + val pp : pp_node:(F.formatter -> 'node -> unit) -> F.formatter -> 'node t -> unit end @@ -56,8 +62,10 @@ end or v <= u and v is in H(u) (feedback edge) - A WTO of a directed graph is such that the head u of every feedback edge u -> v is the head of a - component containing its tail v. + where H(u) is the set of heads of the nested components containing u. + + A WTO of a directed graph is such that the head v of every feedback edge u -> v is the head of a + component containing its tail u. *) module type S = sig diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 37d9982be..2dcb899f1 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -258,12 +258,7 @@ struct let compute_post = make_compute_post ~exec_cfg_internal end -module MakeWithWTO - (WTO : WeakTopologicalOrder.S) - (TransferFunctions : TransferFunctions.SIL - with type CFG.t = WTO.CFG.t - and type CFG.Node.t = WTO.CFG.Node.t) = -struct +module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct include AbstractInterpreterCommon (TransferFunctions) let debug_wto wto node = @@ -315,7 +310,7 @@ struct let exec_cfg_internal ~debug cfg proc_data ~initial = - match WTO.make cfg with + match CFG.wto cfg with | Empty -> InvariantMap.empty (* empty cfg *) | Node {node= start_node; next} as wto -> @@ -340,5 +335,4 @@ module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> S module MakeRPO (T : TransferFunctions.SIL) = MakeWithScheduler (Scheduler.ReversePostorder (T.CFG)) (T) -module MakeWTO (T : TransferFunctions.SIL) = - MakeWithWTO (WeakTopologicalOrder.Bourdoncle_SCC (T.CFG)) (T) +module MakeWTO (T : TransferFunctions.SIL) = MakeUsingWTO (T) diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index c5da5cc65..013f0c418 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/infer/src/absint/ProcCfg.ml @@ -147,6 +147,8 @@ module type S = sig val from_pdesc : Procdesc.t -> t val is_loop_head : Procdesc.t -> Node.t -> bool + + val wto : t -> Node.t WeakTopologicalOrder.Partition.t end (** Forward CFG with no exceptional control-flow *) @@ -183,6 +185,8 @@ module Normal = struct let from_pdesc pdesc = pdesc let is_loop_head = Procdesc.is_loop_head + + let wto = Procdesc.get_wto end (** Forward CFG with exceptional control-flow *) @@ -266,6 +270,22 @@ module Exceptional = struct let exit_node (pdesc, _) = Procdesc.get_exit_node pdesc let is_loop_head = Procdesc.is_loop_head + + module WTO = WeakTopologicalOrder.Bourdoncle_SCC (struct + module Node = Node + + type t = Procdesc.t + + let fold_succs _cfg n ~init ~f = + (* we do not care about duplicate edges *) + let init = List.fold ~init ~f (Procdesc.Node.get_succs n) in + List.fold ~init ~f (Procdesc.Node.get_exn n) + + + let start_node = Procdesc.get_start_node + end) + + let wto (pdesc, _) = WTO.make pdesc end (** Wrapper that reverses the direction of the CFG *) @@ -293,6 +313,18 @@ module Backward (Base : S with type instrs_dir = Instrs.not_reversed) = struct let fold_exceptional_succs = Base.fold_exceptional_preds let fold_exceptional_preds = Base.fold_exceptional_succs + + module WTO = WeakTopologicalOrder.Bourdoncle_SCC (struct + module Node = Node + + type nonrec t = t + + let fold_succs = fold_succs + + let start_node = start_node + end) + + let wto = WTO.make end module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig @@ -353,20 +385,32 @@ end = struct let proc_desc = Base.proc_desc + let fold_instr_nodes node ~init ~f = + match Base.instrs node |> Instrs.count with + | 0 -> + f init (node, 0) + | nb_instrs -> + IContainer.forto nb_instrs ~init ~f:(fun acc index -> f acc (node, index)) + + let fold_nodes cfg ~init ~f = - let f init node = - match Base.instrs node |> Instrs.count with - | 0 -> - f init (node, 0) - | nb_instrs -> - IContainer.forto nb_instrs ~init ~f:(fun acc index -> f acc (node, index)) - in - Base.fold_nodes cfg ~init ~f + Base.fold_nodes cfg ~init ~f:(fun acc node -> fold_instr_nodes node ~init:acc ~f) let from_pdesc = Base.from_pdesc let is_loop_head pdesc = function node, 0 -> Base.is_loop_head pdesc node | _ -> false + + let fold_right_instr_nodes node ~init ~f = + match Base.instrs node |> Instrs.count with + | 0 -> + f init (node, 0) + | nb_instrs -> + IContainer.forto_right nb_instrs ~init ~f:(fun acc index -> f acc (node, index)) + + + let wto cfg = + Base.wto cfg |> WeakTopologicalOrder.Partition.expand ~fold_right:fold_right_instr_nodes end module NormalOneInstrPerNode = OneInstrPerNode (Normal) diff --git a/infer/src/absint/ProcCfg.mli b/infer/src/absint/ProcCfg.mli index 8f3e4851f..b3d845e81 100644 --- a/infer/src/absint/ProcCfg.mli +++ b/infer/src/absint/ProcCfg.mli @@ -76,6 +76,8 @@ module type S = sig val from_pdesc : Procdesc.t -> t val is_loop_head : Procdesc.t -> Node.t -> bool + + val wto : t -> Node.t WeakTopologicalOrder.Partition.t end module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.Node.id diff --git a/infer/src/istd/IContainer.ml b/infer/src/istd/IContainer.ml index 42ab183d6..36e6707ef 100644 --- a/infer/src/istd/IContainer.ml +++ b/infer/src/istd/IContainer.ml @@ -32,6 +32,11 @@ let forto excl ~init ~f = aux excl ~f init 0 +let forto_right excl ~init ~f = + let rec aux ~f acc i = if i < 0 then acc else aux ~f (f acc i) (i - 1) in + aux ~f init (excl - 1) + + let to_rev_list ~fold t = fold t ~init:[] ~f:(fun tl hd -> hd :: tl) let rev_filter_to_list ~fold t ~f = diff --git a/infer/src/istd/IContainer.mli b/infer/src/istd/IContainer.mli index f30bddd06..237ca4f57 100644 --- a/infer/src/istd/IContainer.mli +++ b/infer/src/istd/IContainer.mli @@ -21,6 +21,8 @@ val mem_nth : fold:('t, _, int) Container.fold -> 't -> int -> bool val forto : (int, int, 'accum) Container.fold +val forto_right : (int, int, 'accum) Container.fold + val to_rev_list : fold:('t, 'a, 'a list) Container.fold -> 't -> 'a list val rev_filter_to_list : fold:('t, 'a, 'a list) Container.fold -> 't -> f:('a -> bool) -> 'a list diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index 503df7d9b..a093eda98 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -93,6 +93,18 @@ module MockProcCfg = struct let from_pdesc _ = assert false let is_loop_head _ = assert false + + module WTO = WeakTopologicalOrder.Bourdoncle_SCC (struct + module Node = Node + + type nonrec t = t + + let fold_succs = fold_succs + + let start_node = start_node + end) + + let wto = WTO.make end module S = Scheduler.ReversePostorder (MockProcCfg) diff --git a/infer/src/unit/weakTopologicalOrderTests.ml b/infer/src/unit/weakTopologicalOrderTests.ml index edd7238ff..4c4bbb628 100644 --- a/infer/src/unit/weakTopologicalOrderTests.ml +++ b/infer/src/unit/weakTopologicalOrderTests.ml @@ -60,6 +60,8 @@ let inputs = ; (17, [16]) ] , "1 19 6 7 8 (9 18 17 16 13 15 12 11 10) 14 4 3 2" ) ; ("self_loop", [(1, [1])], "(1)") + ; ("smallest_nested", [(1, [2]); (2, [1; 2])], "(1 (2))") + ; ("smallest_nested_reversed", [(1, [1; 2]); (2, [1])], "(1 2)") ; ( "nested_loops_two_entries" , [(1, [60; 6]); (60, [5; 50]); (5, [6]); (6, [50]); (50, [60])] , "1 (6 (50 60) 5)" )