diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index c2afd7f1d..9d1dc4c55 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -248,8 +248,81 @@ struct let compute_post = make_compute_post ~exec_cfg_internal end +module MakeWithWTO + (WTO : WeakTopologicalOrder.S) + (TransferFunctions : TransferFunctions.SIL with module CFG = WTO.CFG) = +struct + include AbstractInterpreterCommon (TransferFunctions) + + let debug_wto wto node = + let pp_name fmt = + TransferFunctions.pp_session_name node fmt ; + F.pp_print_string fmt " WEAK TOPOLOGICAL ORDER" + in + let underlying_node = Node.underlying_node node in + NodePrinter.start_session ~pp_name underlying_node ; + let pp_node fmt node = node |> Node.id |> Node.pp_id fmt in + L.d_strln (Format.asprintf "%a" (WeakTopologicalOrder.Partition.pp ~pp_node) wto) ; + NodePrinter.finish_session underlying_node + + + let exec_wto_node ~debug cfg proc_data inv_map node ~is_loop_head = + match compute_pre cfg node inv_map with + | Some astate_pre -> + exec_node ~debug proc_data node ~is_loop_head astate_pre inv_map + | None -> + L.(die InternalError) "Could not compute the pre of a node" + + + let rec exec_wto_component ~debug cfg proc_data inv_map head ~is_loop_head rest = + match exec_wto_node ~debug cfg proc_data inv_map head ~is_loop_head with + | inv_map, ReachedFixPoint -> + inv_map + | inv_map, DidNotReachFixPoint -> + let inv_map = exec_wto_partition ~debug cfg proc_data inv_map rest in + exec_wto_component ~debug cfg proc_data inv_map head ~is_loop_head:true rest + + + and exec_wto_partition ~debug cfg proc_data inv_map + (partition : CFG.Node.t WeakTopologicalOrder.Partition.t) = + match partition with + | Empty -> + inv_map + | Node {node; next} -> + let inv_map = exec_wto_node ~debug cfg proc_data inv_map node ~is_loop_head:false |> fst in + exec_wto_partition ~debug cfg proc_data inv_map next + | Component {head; rest; next} -> + let inv_map = + exec_wto_component ~debug cfg proc_data inv_map head ~is_loop_head:false rest + in + exec_wto_partition ~debug cfg proc_data inv_map next + + + let exec_cfg_internal ~debug cfg proc_data ~initial = + match WTO.make cfg with + | Empty -> + InvariantMap.empty (* empty cfg *) + | Node {node= start_node; next} as wto -> + if Config.write_html then debug_wto wto start_node ; + let inv_map, _did_not_reach_fix_point = + exec_node ~debug proc_data start_node ~is_loop_head:false initial InvariantMap.empty + in + exec_wto_partition ~debug cfg proc_data inv_map next + | Component _ -> + L.(die InternalError) "Did not expect the start node to be part of a loop" + + + let exec_cfg = exec_cfg_internal ~debug:Default + + let exec_pdesc = make_exec_pdesc ~exec_cfg_internal + + let compute_post = make_compute_post ~exec_cfg_internal +end + module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> S with module TransferFunctions = TransferFunctions module MakeRPO (T : TransferFunctions.SIL) = MakeWithScheduler (Scheduler.ReversePostorder (T.CFG)) (T) +module MakeWTO (T : TransferFunctions.SIL) = + MakeWithWTO (WeakTopologicalOrder.Bourdoncle_SCC (T.CFG)) (T) diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli index babf3c3db..eab9942a2 100644 --- a/infer/src/absint/AbstractInterpreter.mli +++ b/infer/src/absint/AbstractInterpreter.mli @@ -59,3 +59,6 @@ module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> S (** create an intraprocedural abstract interpreter from transfer functions using the reverse post-order scheduler *) module MakeRPO : Make + +(** create an intraprocedural abstract interpreter from transfer functions using Bourdoncle's strongly connected component weak topological order *) +module MakeWTO : Make diff --git a/infer/src/absint/WeakTopologicalOrder.ml b/infer/src/absint/WeakTopologicalOrder.ml new file mode 100644 index 000000000..815ac18ed --- /dev/null +++ b/infer/src/absint/WeakTopologicalOrder.ml @@ -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 diff --git a/infer/src/absint/WeakTopologicalOrder.mli b/infer/src/absint/WeakTopologicalOrder.mli new file mode 100644 index 000000000..3d75d0d38 --- /dev/null +++ b/infer/src/absint/WeakTopologicalOrder.mli @@ -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 diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 834309b1a..cfc6b170f 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -281,8 +281,9 @@ end module Make (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t) (T : TransferFunctions.MakeSIL) = struct module AI_RPO = MakeMake (AbstractInterpreter.MakeRPO) (CFG) (T) + module AI_WTO = MakeMake (AbstractInterpreter.MakeWTO) (CFG) (T) - let ai_list = [("ai_rpo", AI_RPO.create_test)] + let ai_list = [("ai_rpo", AI_RPO.create_test); ("ai_wto", AI_WTO.create_test)] let create_tests ?(test_pname = Typ.Procname.empty_block) ~initial ?pp_opt extras tests = let open OUnit2 in diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml index 35c25d445..e7ca6e98a 100644 --- a/infer/src/unit/inferunit.ml +++ b/infer/src/unit/inferunit.ml @@ -43,7 +43,8 @@ let () = ; SeverityTests.tests ; StacktraceTests.tests ; TaintTests.tests - ; TraceTests.tests ] + ; TraceTests.tests + ; WeakTopologicalOrderTests.tests ] @ ClangTests.tests ) in let test_suite = "all" >::: tests in diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index cbfc7663c..503df7d9b 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -117,23 +117,26 @@ let create_test test_graph expected_result _ = let inputs = - [ ("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]) + [ ("straightline", [(1, [2]); (2, [3]); (3, [4])], [1; 2; 3; 4], "1 2 3 4") + ; ("if_then_else", [(1, [2; 3]); (2, [4]); (3, [4]); (4, [5])], [1; 2; 3; 4; 5], "1 2 3 4 5") + ; ("if_then", [(1, [2; 4]); (2, [3]); (3, [4]); (4, [5])], [1; 2; 3; 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] ) + , [1; 2; 3; 4; 5; 6; 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] ) + , [1; 2; 3; 4; 5; 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] ) ] + , [1; 2; 3; 7; 11; 10] + , "1 2 3 7 11 10" ) ] let tests = let open OUnit2 in let test_list = - inputs |> List.map ~f:(fun (name, test, expected) -> name >:: create_test test expected) + inputs |> List.map ~f:(fun (name, test, expected, _wto) -> name >:: create_test test expected) in "scheduler_suite" >::: test_list diff --git a/infer/src/unit/weakTopologicalOrderTests.ml b/infer/src/unit/weakTopologicalOrderTests.ml new file mode 100644 index 000000000..edd7238ff --- /dev/null +++ b/infer/src/unit/weakTopologicalOrderTests.ml @@ -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 diff --git a/infer/tests/codetoanalyze/c/frontend/gotostmt/jjb1.c b/infer/tests/codetoanalyze/c/frontend/gotostmt/jjb1.c new file mode 100644 index 000000000..89fa8024d --- /dev/null +++ b/infer/tests/codetoanalyze/c/frontend/gotostmt/jjb1.c @@ -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; +} diff --git a/infer/tests/codetoanalyze/c/frontend/gotostmt/jjb1.c.dot b/infer/tests/codetoanalyze/c/frontend/gotostmt/jjb1.c.dot new file mode 100644 index 000000000..e84a7fef4 --- /dev/null +++ b/infer/tests/codetoanalyze/c/frontend/gotostmt/jjb1.c.dot @@ -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" ; +}