Reviewed By: jberdine Differential Revision: D7783487 fbshipit-source-id: 15b4c84e1master
Mehdi Bouaziz
6 years ago
committed by
Facebook Github Bot
parent
c9b89b54dd
commit
eca0b491d6
@ -0,0 +1,172 @@
|
||||
(*
|
||||
* Copyright (c) 2018-present, Facebook, Inc.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
module F = Format
|
||||
|
||||
module Partition = struct
|
||||
type 'node t =
|
||||
| Empty
|
||||
| Node of {node: 'node; next: 'node t}
|
||||
| Component of {head: 'node; rest: 'node t; next: 'node t}
|
||||
|
||||
let empty = Empty
|
||||
|
||||
let add_node node next = Node {node; next}
|
||||
|
||||
let add_component head rest next = Component {head; rest; next}
|
||||
|
||||
let rec pp ~prefix ~pp_node fmt = function
|
||||
| Empty ->
|
||||
()
|
||||
| Node {node; next} ->
|
||||
F.fprintf fmt "%s%a" prefix pp_node node ;
|
||||
pp ~prefix:" " ~pp_node fmt next
|
||||
| Component {head; rest; next} ->
|
||||
F.fprintf fmt "%s(%a%a)" prefix pp_node head (pp ~prefix:" " ~pp_node) rest ;
|
||||
pp ~prefix:" " ~pp_node fmt next
|
||||
|
||||
|
||||
let pp ~pp_node = pp ~prefix:"" ~pp_node
|
||||
end
|
||||
|
||||
module type S = sig
|
||||
module CFG : ProcCfg.S
|
||||
|
||||
val make : CFG.t -> CFG.Node.t Partition.t
|
||||
end
|
||||
|
||||
module type Make = functor (CFG : ProcCfg.S) -> S with module CFG = CFG
|
||||
|
||||
module Bourdoncle_SCC (CFG : ProcCfg.S) = struct
|
||||
module CFG = CFG
|
||||
|
||||
(**
|
||||
[dfn] contains a DFS pre-order indexing. A node is not in the map if it has never been visited.
|
||||
A node's dfn is +oo if it has been fully visited (head of cross-edges) or we want to hide it
|
||||
for building a subcomponent partition (head of highest back-edges).
|
||||
*)
|
||||
module Dfn = CFG.Node.IdMap
|
||||
|
||||
(*
|
||||
Unlike Bourdoncle's paper version or OCamlGraph implementation, this implementation handles
|
||||
high DFS-depth graphs, which would stack-overflow otherwise.
|
||||
It still doesn't handle high component nesting, but it is pretty unlikely to happen in real
|
||||
code (means a lot of loop nesting).
|
||||
*)
|
||||
|
||||
type stack =
|
||||
{ node: CFG.Node.t
|
||||
; node_id: CFG.Node.id
|
||||
; node_dfn: int
|
||||
; succs: CFG.Node.t list
|
||||
; mutable succs_to_visit: CFG.Node.t list
|
||||
; mutable head: int (** Minimum [dfn] of the nodes accessibles from [node]. *)
|
||||
; mutable component: CFG.Node.id ARList.t
|
||||
(** Nodes in the current strict-connected component. *)
|
||||
; mutable building_component: bool
|
||||
; next: stack option }
|
||||
|
||||
let make cfg =
|
||||
let num = ref 0 in
|
||||
let dfn = ref Dfn.empty in
|
||||
let stack = ref None in
|
||||
let push_on_stack node =
|
||||
let node_id = CFG.Node.id node in
|
||||
incr num ;
|
||||
let node_dfn = !num in
|
||||
dfn := Dfn.add node_id node_dfn !dfn ;
|
||||
let succs = IContainer.to_rev_list ~fold:(CFG.fold_succs cfg) node in
|
||||
stack :=
|
||||
Some
|
||||
{ node
|
||||
; node_id
|
||||
; node_dfn
|
||||
; succs
|
||||
; succs_to_visit= succs
|
||||
; head= Int.max_value
|
||||
; component= ARList.empty
|
||||
; building_component= false
|
||||
; next= !stack }
|
||||
in
|
||||
let record_head ?add_to_component cur_head =
|
||||
let stack_top = Option.value_exn !stack in
|
||||
stack_top.head <- min stack_top.head cur_head ;
|
||||
Option.iter add_to_component ~f:(fun add ->
|
||||
stack_top.component <- ARList.append add stack_top.component )
|
||||
in
|
||||
let visit node =
|
||||
let node_id = CFG.Node.id node in
|
||||
match Dfn.find node_id !dfn with
|
||||
| node_dfn ->
|
||||
(*
|
||||
[node_dfn] is going to be either +oo (see [Dfn] for why), in which case [record_head]
|
||||
will have no effect; or be the [dfn] of the head of a back-edge or cross-edge in the
|
||||
current strictly connected component.
|
||||
*)
|
||||
record_head node_dfn
|
||||
| exception Caml.Not_found ->
|
||||
push_on_stack node
|
||||
| exception Not_found_s _ ->
|
||||
push_on_stack node
|
||||
in
|
||||
let rec process_stack partition =
|
||||
match !stack with
|
||||
| None ->
|
||||
()
|
||||
| Some ({succs_to_visit= succ :: succs_to_visit} as stack_top) ->
|
||||
stack_top.succs_to_visit <- succs_to_visit ;
|
||||
visit succ ;
|
||||
(process_stack [@tailcall]) partition
|
||||
| Some {succs_to_visit= []; building_component= true} ->
|
||||
()
|
||||
| Some
|
||||
{succs_to_visit= []; building_component= false; node_id; node_dfn; head; component; next}
|
||||
when head < node_dfn ->
|
||||
(* [node] is in a strictly connected component but is (locally) not its head. *)
|
||||
stack := next ;
|
||||
record_head head ~add_to_component:(ARList.cons node_id component) ;
|
||||
(process_stack [@tailcall]) partition
|
||||
| Some
|
||||
( { succs_to_visit= []
|
||||
; building_component= false
|
||||
; node
|
||||
; node_id
|
||||
; node_dfn
|
||||
; succs
|
||||
; head
|
||||
; component
|
||||
; next } as stack_top ) ->
|
||||
dfn := Dfn.add node_id Int.max_value !dfn ;
|
||||
if head > node_dfn then
|
||||
(* [node] is not (locally) in a strictly connected component *)
|
||||
partition := Partition.add_node node !partition
|
||||
else (
|
||||
(*
|
||||
head = node_dfn. [node] is (locally) the head of a strictly connected component.
|
||||
[node] is marked as already visited (line dfn := ... above).
|
||||
All nodes in the current [component] are marked as not visited.
|
||||
And we recursively construct a WTO for the component.
|
||||
*)
|
||||
Container.iter component ~fold:ARList.fold_unordered ~f:(fun nid ->
|
||||
dfn := Dfn.remove nid !dfn ) ;
|
||||
let component_partition =
|
||||
let partition = ref Partition.empty in
|
||||
stack_top.building_component <- true ;
|
||||
stack_top.succs_to_visit <- succs ;
|
||||
process_stack partition ;
|
||||
!partition
|
||||
in
|
||||
partition := Partition.add_component node component_partition !partition ) ;
|
||||
stack := next ;
|
||||
(process_stack [@tailcall]) partition
|
||||
in
|
||||
let partition = ref Partition.empty in
|
||||
push_on_stack (CFG.start_node cfg) ;
|
||||
process_stack partition ;
|
||||
!partition
|
||||
end
|
||||
@ -0,0 +1,55 @@
|
||||
(*
|
||||
* Copyright (c) 2018-present, Facebook, Inc.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
module F = Format
|
||||
|
||||
(* The definitions below taken from [Bou] "Efficient chaotic iteration strategies with widenings"
|
||||
by François Bourdoncle.
|
||||
*)
|
||||
|
||||
(**
|
||||
A hierarchical ordering of a set is a well-parenthesized permutation of its elements without two
|
||||
consecutive "(". I defines a total order <= over its elements.
|
||||
The elements between two matching parentheses are called a Component.
|
||||
The first element of a Component is called the head.
|
||||
Let denote by H(v) the set of head of the nested components containing v.
|
||||
*)
|
||||
|
||||
module Partition : sig
|
||||
type 'node t = private
|
||||
| Empty
|
||||
| Node of {node: 'node; next: 'node t}
|
||||
| Component of {head: 'node; rest: 'node t; next: 'node t}
|
||||
|
||||
val pp : pp_node:(F.formatter -> 'node -> unit) -> F.formatter -> 'node t -> unit
|
||||
end
|
||||
|
||||
(**
|
||||
A weak topological ordering (WTO) of a directed graph is a hierarchical ordering of its vertices
|
||||
such that for every edge u -> v,
|
||||
u < v and v is not in H(u) (forward edge)
|
||||
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.
|
||||
*)
|
||||
|
||||
module type S = sig
|
||||
module CFG : ProcCfg.S
|
||||
|
||||
val make : CFG.t -> CFG.Node.t Partition.t
|
||||
end
|
||||
|
||||
module type Make = functor (CFG : ProcCfg.S) -> S with module CFG = CFG
|
||||
|
||||
(**
|
||||
Implementation of Bourdoncle's "Hierarchical decomposition of a directed graph into strongly
|
||||
connected components and subcomponents". See [Bou] Figure 4, page 10.
|
||||
*)
|
||||
module Bourdoncle_SCC : Make
|
||||
@ -0,0 +1,94 @@
|
||||
(*
|
||||
* Copyright (c) 2018-present, Facebook, Inc.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
module MockProcCfg = SchedulerTests.MockProcCfg
|
||||
module WTO = WeakTopologicalOrder.Bourdoncle_SCC (MockProcCfg)
|
||||
|
||||
let inputs_from_scheduler_tests =
|
||||
SchedulerTests.inputs |> List.map ~f:(fun (name, cfg, _, wto) -> (name, cfg, wto))
|
||||
|
||||
|
||||
let inputs =
|
||||
inputs_from_scheduler_tests
|
||||
@ [ ( "bourdoncle_fig1"
|
||||
, [(1, [2]); (2, [3; 8]); (3, [4]); (4, [5; 7]); (5, [6]); (6, [5; 7]); (7, [3; 8])]
|
||||
, "1 2 (3 4 (5 6) 7) 8" )
|
||||
; ( "bourdoncle_fig2left"
|
||||
, [(1, [2; 4]); (2, [3]); (3, []); (4, [5; 3]); (5, [4])]
|
||||
, "1 2 (4 5) 3" )
|
||||
; ("bourdoncle_fig2right", [(1, [2; 4]); (2, [3]); (3, [1]); (4, [3])], "(1 2 4 3)")
|
||||
; ( "bourdoncle_fig5"
|
||||
, [ (1, [4; 2])
|
||||
; (2, [3])
|
||||
; (3, [6])
|
||||
; (4, [10])
|
||||
; (10, [20; 40])
|
||||
; (40, [1])
|
||||
; (20, [30])
|
||||
; (30, [60])
|
||||
; (60, [5])
|
||||
; (50, [60])
|
||||
; (6, [50])
|
||||
; (5, [6]) ]
|
||||
, "(1 4 10 40) 20 30 2 3 (6 50 60 5)" )
|
||||
; ( "elder_fig1"
|
||||
, [(1, [2]); (2, [3]); (7, [2; 8]); (3, [4]); (6, [7; 3]); (4, [5]); (5, [6; 2])]
|
||||
, "1 (2 (3 4 5 6) 7) 8" )
|
||||
; ( "jjb1" (* corresponds to tests/codetoanalyze/c/frontend/gotostmt/jjb1.c *)
|
||||
, [ (1, [19])
|
||||
; (19, [6])
|
||||
; (6, [7; 8])
|
||||
; (7, [16])
|
||||
; (8, [9])
|
||||
; (16, [13])
|
||||
; (13, [14; 15])
|
||||
; (5 (* no preds, dead node *), [4])
|
||||
; (14, [4])
|
||||
; (15, [12])
|
||||
; (4, [3])
|
||||
; (12, [11])
|
||||
; (3, [2])
|
||||
; (11, [10])
|
||||
; (10, [9])
|
||||
; (9, [18])
|
||||
; (18, [17])
|
||||
; (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)")
|
||||
; ( "nested_loops_two_entries"
|
||||
, [(1, [60; 6]); (60, [5; 50]); (5, [6]); (6, [50]); (50, [60])]
|
||||
, "1 (6 (50 60) 5)" )
|
||||
; ( "nested_loops2"
|
||||
, [ (1, [2])
|
||||
; (2, [9])
|
||||
; (6, [2; 7])
|
||||
; (7, [8; 5])
|
||||
; (5, [7; 6])
|
||||
; (9, [3; 10])
|
||||
; (3, [4])
|
||||
; (4, [5])
|
||||
; (8, [4; 3]) ]
|
||||
, "1 (2 9 (3 (4 (5 6 7) 8))) 10" ) ]
|
||||
|
||||
|
||||
let create_test cfg expected_result _ =
|
||||
let result =
|
||||
let partition = WTO.make cfg in
|
||||
Format.asprintf "%a"
|
||||
(WeakTopologicalOrder.Partition.pp ~pp_node:MockProcCfg.Node.pp_id)
|
||||
partition
|
||||
in
|
||||
OUnit2.assert_equal ~printer:Fn.id expected_result result
|
||||
|
||||
|
||||
let tests =
|
||||
let open OUnit2 in
|
||||
let test_list =
|
||||
inputs |> List.map ~f:(fun (name, test, expected) -> name >:: create_test test expected)
|
||||
in
|
||||
"wto_suite" >::: test_list
|
||||
@ -0,0 +1,30 @@
|
||||
/*
|
||||
* Copyright (c) 2018-present, Facebook, Inc.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*/
|
||||
|
||||
extern void print_int(int);
|
||||
|
||||
int jjb1() {
|
||||
int x, y;
|
||||
|
||||
x++;
|
||||
if (x / 2) {
|
||||
L0:
|
||||
if (x <= 0)
|
||||
goto L3;
|
||||
x--;
|
||||
print_int(x);
|
||||
goto L1;
|
||||
} else {
|
||||
L1:
|
||||
y++;
|
||||
print_int(y);
|
||||
goto L0;
|
||||
}
|
||||
L3:
|
||||
|
||||
return 0;
|
||||
}
|
||||
@ -0,0 +1,80 @@
|
||||
/* @generated */
|
||||
digraph cfg {
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_1" [label="1: Start jjb1\nFormals: \nLocals: y:int x:int \n " color=yellow style=filled]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_1" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_19" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_2" [label="2: Exit jjb1 \n " color=yellow style=filled]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_3" [label="3: Return Stmt \n *&return:int=0 [line 29, column 3]\n " shape="box"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_3" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_2" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_4" [label="4: Skip GotoLabel_L3 \n " color="gray"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_4" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_3" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_5" [label="5: + \n " ]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_5" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_4" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_6" [label="6: BinaryOperatorStmt: Div \n n$1=*&x:int [line 14, column 7]\n " shape="box"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_6" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_7" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_6" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_8" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_7" [label="7: Prune (true branch, if) \n PRUNE((n$1 / 2), true); [line 14, column 7]\n " shape="invhouse"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_7" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_16" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_8" [label="8: Prune (false branch, if) \n PRUNE(!(n$1 / 2), false); [line 14, column 7]\n " shape="invhouse"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_8" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_9" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_9" [label="9: Skip GotoLabel_L1 \n " color="gray"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_9" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_18" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_10" [label="10: Call _fun_print_int \n n$3=*&x:int [line 19, column 15]\n n$4=_fun_print_int(n$3:int) [line 19, column 5]\n " shape="box"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_10" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_9" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_11" [label="11: UnaryOperator \n n$5=*&x:int [line 18, column 5]\n *&x:int=(n$5 - 1) [line 18, column 5]\n " shape="box"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_11" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_10" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_12" [label="12: + \n " ]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_12" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_11" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_13" [label="13: BinaryOperatorStmt: LE \n n$6=*&x:int [line 16, column 9]\n " shape="box"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_13" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_14" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_13" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_15" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_14" [label="14: Prune (true branch, if) \n PRUNE((n$6 <= 0), true); [line 16, column 9]\n " shape="invhouse"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_14" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_4" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_15" [label="15: Prune (false branch, if) \n PRUNE(!(n$6 <= 0), false); [line 16, column 9]\n " shape="invhouse"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_15" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_12" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_16" [label="16: Skip GotoLabel_L0 \n " color="gray"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_16" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_13" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_17" [label="17: Call _fun_print_int \n n$12=*&y:int [line 24, column 15]\n n$13=_fun_print_int(n$12:int) [line 24, column 5]\n " shape="box"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_17" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_16" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_18" [label="18: UnaryOperator \n n$14=*&y:int [line 23, column 5]\n *&y:int=(n$14 + 1) [line 23, column 5]\n " shape="box"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_18" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_17" ;
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_19" [label="19: UnaryOperator \n n$17=*&x:int [line 13, column 3]\n *&x:int=(n$17 + 1) [line 13, column 3]\n " shape="box"]
|
||||
|
||||
|
||||
"jjb1.9d6085e324f8fe61c38e804980fa5cf1_19" -> "jjb1.9d6085e324f8fe61c38e804980fa5cf1_6" ;
|
||||
}
|
||||
Loading…
Reference in new issue