From 0d4c06efc5d94e9e0f7feaab26b4b4935fd987a5 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 16 Oct 2018 07:27:59 -0700 Subject: [PATCH] WTO: use a partial ProcCfg Reviewed By: jberdine Differential Revision: D10376574 fbshipit-source-id: 09e0f0ca5 --- infer/src/absint/AbstractInterpreter.ml | 4 +++- infer/src/absint/WeakTopologicalOrder.ml | 24 ++++++++++++++++++++--- infer/src/absint/WeakTopologicalOrder.mli | 22 +++++++++++++++++++-- 3 files changed, 44 insertions(+), 6 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index dc02f8b91..d9dbf9cdf 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -260,7 +260,9 @@ end module MakeWithWTO (WTO : WeakTopologicalOrder.S) - (TransferFunctions : TransferFunctions.SIL with module CFG = WTO.CFG) = + (TransferFunctions : TransferFunctions.SIL + with type CFG.t = WTO.CFG.t + and type CFG.Node.t = WTO.CFG.Node.t) = struct include AbstractInterpreterCommon (TransferFunctions) diff --git a/infer/src/absint/WeakTopologicalOrder.ml b/infer/src/absint/WeakTopologicalOrder.ml index 815ac18ed..22f994075 100644 --- a/infer/src/absint/WeakTopologicalOrder.ml +++ b/infer/src/absint/WeakTopologicalOrder.ml @@ -34,15 +34,33 @@ module Partition = struct let pp ~pp_node = pp ~prefix:"" ~pp_node end +module type PreProcCfg = sig + module Node : sig + type t + + type id + + val id : t -> id + + module IdMap : PrettyPrintable.PPMap with type key = id + end + + type t + + val fold_succs : t -> (Node.t, Node.t, 'accum) Container.fold + + val start_node : t -> Node.t +end + module type S = sig - module CFG : ProcCfg.S + module CFG : PreProcCfg val make : CFG.t -> CFG.Node.t Partition.t end -module type Make = functor (CFG : ProcCfg.S) -> S with module CFG = CFG +module type Make = functor (CFG : PreProcCfg) -> S with module CFG = CFG -module Bourdoncle_SCC (CFG : ProcCfg.S) = struct +module Bourdoncle_SCC (CFG : PreProcCfg) = struct module CFG = CFG (** diff --git a/infer/src/absint/WeakTopologicalOrder.mli b/infer/src/absint/WeakTopologicalOrder.mli index 3d75d0d38..97c7fcfb9 100644 --- a/infer/src/absint/WeakTopologicalOrder.mli +++ b/infer/src/absint/WeakTopologicalOrder.mli @@ -29,6 +29,24 @@ module Partition : sig val pp : pp_node:(F.formatter -> 'node -> unit) -> F.formatter -> 'node t -> unit end +module type PreProcCfg = sig + module Node : sig + type t + + type id + + val id : t -> id + + module IdMap : PrettyPrintable.PPMap with type key = id + end + + type t + + val fold_succs : t -> (Node.t, Node.t, 'accum) Container.fold + + val start_node : t -> Node.t +end + (** A weak topological ordering (WTO) of a directed graph is a hierarchical ordering of its vertices such that for every edge u -> v, @@ -41,12 +59,12 @@ end *) module type S = sig - module CFG : ProcCfg.S + module CFG : PreProcCfg val make : CFG.t -> CFG.Node.t Partition.t end -module type Make = functor (CFG : ProcCfg.S) -> S with module CFG = CFG +module type Make = functor (CFG : PreProcCfg) -> S with module CFG = CFG (** Implementation of Bourdoncle's "Hierarchical decomposition of a directed graph into strongly