Expose WTO in ProcCfg

Reviewed By: jberdine

Differential Revision: D10376596

fbshipit-source-id: 0162a5cf3

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
 

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 ->
         ()

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

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)

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_nodes cfg ~init ~f =
-    let f init node =
+  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))
-    in
-    Base.fold_nodes cfg ~init ~f
+
+
+  let 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)

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

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 =

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

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)

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)" )