diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index 693ec00ca..d67990fa2 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -9,27 +9,33 @@ open! IStd module F = Format module L = Logging (* forward dependency analysis for computing set of variables that - affect the control flow at each program point + affect the looping behavior of the program 1. perform a control flow dependency analysis by getting all the - variables that appear in the control flow path up to that node. + variables that appear in the guards of the loops. 2. for each control dependency per node, find its respective data dependency + + 3. remove invariant vars in the loop from control vars *) module VarSet = AbstractDomain.FiniteSet (Var) -module ControlDepSet = VarSet +module CFG = ProcCfg.Normal +module ControlDepSet = AbstractDomain.FiniteSet (Var) module GuardNodes = AbstractDomain.FiniteSet (Procdesc.Node) +module LoopHeads = Procdesc.NodeSet -(** Map exit node -> prune nodes in the loop guard *) -module ExitNodeToGuardNodes = AbstractDomain.Map (Procdesc.Node) (GuardNodes) +(** Map exit node -> loop head set *) +module ExitNodeToLoopHeads = Procdesc.NodeMap -(** Map loop header node -> prune nodes in the loop guard *) -module LoopHeaderToGuardNodes = AbstractDomain.Map (Procdesc.Node) (GuardNodes) +(** Map loop head -> prune nodes in the loop guard *) +module LoopHeadToGuardNodes = +Procdesc.NodeMap type loop_control_maps = - {exit_map: ExitNodeToGuardNodes.astate; loop_header_map: LoopHeaderToGuardNodes.astate} + { exit_map: LoopHeads.t ExitNodeToLoopHeads.t + ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t } (* forward transfer function for control dependencies *) module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct @@ -40,7 +46,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct let collect_vars_in_exp exp = Var.get_all_vars_in_exp exp - |> Sequence.fold ~init:ControlDepSet.empty ~f:(fun acc var -> ControlDepSet.add var acc) + |> Sequence.fold ~init:ControlDepSet.empty ~f:(fun acc cvar -> ControlDepSet.add cvar acc) let find_vars_in_decl id _ = function @@ -86,25 +92,40 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct (* Each time we pass through - - a loop header, add control variables of its guard nodes + - a loop header, add control variables of its guard nodes, - a loop exit node, remove control variables of its guard nodes This is correct because the CVs are only going to be temporaries. *) - let exec_instr astate {ProcData.extras= {exit_map; loop_header_map}} (node: CFG.Node.t) _ = + let exec_instr astate {ProcData.extras= {exit_map; loop_head_to_guard_nodes}} (node: CFG.Node.t) + _ = let node = CFG.Node.underlying_node node in let astate' = - match LoopHeaderToGuardNodes.find_opt node loop_header_map with + match LoopHeadToGuardNodes.find_opt node loop_head_to_guard_nodes with | Some loop_nodes -> - L.(debug Analysis Medium) "@\n>>> Loop header %a \n" Procdesc.Node.pp node ; Domain.union astate (get_control_vars loop_nodes) | _ -> astate in - match ExitNodeToGuardNodes.find_opt node exit_map with - | Some loop_nodes -> - L.(debug Analysis Medium) - "@\n>>>Exit node %a loop nodes=%a @\n\n" Procdesc.Node.pp node GuardNodes.pp loop_nodes ; - get_control_vars loop_nodes |> Domain.diff astate' + match Procdesc.Node.get_kind node with + | Procdesc.Node.Prune_node _ -> ( + match ExitNodeToLoopHeads.find_opt node exit_map with + | Some loop_heads -> + LoopHeads.fold + (fun loop_head astate_acc -> + match LoopHeadToGuardNodes.find_opt loop_head loop_head_to_guard_nodes with + | Some guard_nodes -> + L.(debug Analysis Medium) + "@\n>>>Exit node %a, Loop head %a, guard nodes=%a @\n\n" Procdesc.Node.pp node + Procdesc.Node.pp loop_head GuardNodes.pp guard_nodes ; + get_control_vars guard_nodes |> Domain.diff astate_acc + | _ -> + (* Every loop head must have a guard node *) + assert false ) + loop_heads astate' + | _ -> + astate' ) | _ -> + (* Exit node must be a prune node *) + assert (not (ExitNodeToLoopHeads.mem node exit_map)) ; astate' @@ -112,22 +133,16 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct F.fprintf fmt "control dependency analysis %a" CFG.Node.pp_id (CFG.Node.id node) end -module CFG = ProcCfg.Normal module ControlDepAnalyzer = AbstractInterpreter.Make (CFG) (TransferFunctionsControlDeps) -let report_control_deps control_map node = - Instrs.iter (Procdesc.Node.get_instrs node) ~f:(fun instr -> - L.(debug Analysis Medium) "@\n>>>Control dependencies of node = %a @\n" Procdesc.Node.pp node ; - List.iter (Sil.instr_get_exps instr) ~f:(fun exp -> - L.(debug Analysis Medium) - "@\n>>>for exp = %a : %a @\n\n" Exp.pp exp ControlDepSet.pp control_map ) ) - - -let compute_all_deps control_invariant_map node = +let compute_control_vars control_invariant_map node = let node_id = CFG.Node.id node in let deps = VarSet.empty in ControlDepAnalyzer.extract_post node_id control_invariant_map |> Option.map ~f:(fun control_deps -> - report_control_deps control_deps node ; + (* loop_inv_map: loop head -> variables that are invariant in the loop *) + L.(debug Analysis Medium) + "@\n>>> Control dependencies of node %a : %a @\n" Procdesc.Node.pp node ControlDepSet.pp + control_deps ; control_deps ) |> Option.value ~default:deps diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index aca630485..d3a68d6a6 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -161,11 +161,11 @@ module BoundMap = struct in match exit_state_opt with | Some entry_mem -> - (* compute all the dependencies, i.e. set of variables that affect the control flow upto the node *) - let all_deps = Control.compute_all_deps control_invariant_map node in + (* compute control vars, i.e. set of variables that affect the execution count *) + let control_vars = Control.compute_control_vars control_invariant_map node in L.(debug Analysis Medium) "@\n>>> All dependencies for node = %a : %a @\n\n" Procdesc.Node.pp node - Control.VarSet.pp all_deps ; + Control.VarSet.pp control_vars ; (* bound = env(v1) *... * env(vn) *) let bound = match entry_mem with @@ -177,7 +177,7 @@ module BoundMap = struct BasicCost.zero | NonBottom mem -> BufferOverrunDomain.MemReach.heap_range - ~filter_loc:(filter_loc formal_pvars all_deps) + ~filter_loc:(filter_loc formal_pvars control_vars) mem in L.(debug Analysis Medium) diff --git a/infer/src/checkers/loop_control.ml b/infer/src/checkers/loop_control.ml index 96668f535..717896c9f 100644 --- a/infer/src/checkers/loop_control.ml +++ b/infer/src/checkers/loop_control.ml @@ -92,39 +92,56 @@ let is_prune node = match Procdesc.Node.get_kind node with Procdesc.Node.Prune_node _ -> true | _ -> false -(* Get a pair of two maps (exit_to_guard_map, loop_header_to_guard_map) where - exit_to_guard_map : exit_node -> guard_nodes - loop_header_to_guard_map : loop_header (i.e. target of the back edge) -> guard_nodes and +(* Get a pair of maps (exit_map, loop_head_to_guard_map) where + exit_map : exit_node -> loop_head set (i.e. target of the back edges) + loop_head_to_guard_map : loop_head -> guard_nodes and guard_nodes contains the nodes that may affect the looping behavior, i.e. occur in the guard of the loop conditional. *) let get_control_maps cfg = - (* get back edges*) - let back_edge_set = get_back_edges cfg in - List.fold_left - ~f:(fun Control.({exit_map; loop_header_map}) {source; target} -> + (* Since there could be multiple back-edges per loop, collect all + source nodes per loop head *) + (* loop_head (target of back-edges) --> source nodes *) + let loop_head_to_source_nodes_map = + get_back_edges cfg + |> List.fold ~init:Procdesc.NodeMap.empty ~f:(fun loop_head_to_source_list {source; target} -> + Procdesc.NodeMap.update target + (function Some source_list -> Some (source :: source_list) | None -> Some [source]) + loop_head_to_source_list ) + in + Procdesc.NodeMap.fold + (fun loop_head source_list Control.({exit_map; loop_head_to_guard_nodes}) -> L.(debug Analysis Medium) - "Back-edge source: %i -> target: %i\n" (nid_int source) (nid_int target) ; - let loop_nodes = get_all_nodes_upwards_until target [source] in + "Back-edge source list : [%a] --> loop_head: %i \n" (Pp.comma_seq Procdesc.Node.pp) + source_list (nid_int loop_head) ; + let loop_nodes = get_all_nodes_upwards_until loop_head source_list in let exit_nodes = get_exit_nodes_in_loop loop_nodes in + L.(debug Analysis Medium) "Exit nodes: [%a]\n" (Pp.comma_seq Procdesc.Node.pp) exit_nodes ; (* find all the prune nodes in the loop guard *) let guard_prune_nodes = - get_all_nodes_upwards_until target exit_nodes |> Control.GuardNodes.filter is_prune + get_all_nodes_upwards_until loop_head exit_nodes |> Control.GuardNodes.filter is_prune in let exit_map' = - (List.fold_left ~init:exit_map ~f:(fun acc exit_node -> - (*Make sure an exit node only belongs to a single loop *) - assert (not (Control.ExitNodeToGuardNodes.mem exit_node acc)) ; - Control.ExitNodeToGuardNodes.add exit_node guard_prune_nodes acc )) + (List.fold_left ~init:exit_map ~f:(fun exit_map_acc exit_node -> + Control.ExitNodeToLoopHeads.update exit_node + (function + | Some existing_loop_heads -> + Some (Control.LoopHeads.add loop_head existing_loop_heads) + | None -> + Some (Control.LoopHeads.singleton loop_head)) + exit_map_acc )) exit_nodes in - let loop_map' = - (*Make sure a loop header only belongs to a single loop *) - assert (not (Control.LoopHeaderToGuardNodes.mem target loop_header_map)) ; - Control.LoopHeaderToGuardNodes.add target guard_prune_nodes loop_header_map + let loop_head_to_guard_nodes' = + Control.LoopHeadToGuardNodes.update loop_head + (function + | Some existing_guard_nodes -> + Some (Control.GuardNodes.union existing_guard_nodes guard_prune_nodes) + | None -> + Some guard_prune_nodes) + loop_head_to_guard_nodes in - Control.{exit_map= exit_map'; loop_header_map= loop_map'} ) - back_edge_set - ~init: - Control. - { exit_map= Control.ExitNodeToGuardNodes.empty - ; loop_header_map= Control.LoopHeaderToGuardNodes.empty } + Control.{exit_map= exit_map'; loop_head_to_guard_nodes= loop_head_to_guard_nodes'} ) + loop_head_to_source_nodes_map + Control. + { exit_map= Control.ExitNodeToLoopHeads.empty + ; loop_head_to_guard_nodes= Control.LoopHeadToGuardNodes.empty } diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 6cff3a80a..d8dedd3e7 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -97,6 +97,13 @@ codetoanalyze/c/performance/loops.c, larger_state_FN, 3, EXPENSIVE_EXECUTION_TIM codetoanalyze/c/performance/loops.c, larger_state_FN, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1003] codetoanalyze/c/performance/loops.c, larger_state_FN, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1003] codetoanalyze/c/performance/loops.c, larger_state_FN, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1003] +codetoanalyze/c/performance/switch_continue.c, test_switch, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 601] +codetoanalyze/c/performance/switch_continue.c, test_switch, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 601] +codetoanalyze/c/performance/switch_continue.c, test_switch, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 601] +codetoanalyze/c/performance/switch_continue.c, test_switch, 17, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 601] +codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 603] +codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * s$1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * s$1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 * s$1] diff --git a/infer/tests/codetoanalyze/c/performance/switch_continue.c b/infer/tests/codetoanalyze/c/performance/switch_continue.c new file mode 100644 index 000000000..ab013ca19 --- /dev/null +++ b/infer/tests/codetoanalyze/c/performance/switch_continue.c @@ -0,0 +1,47 @@ +/* + * 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. + */ +int test_switch() { + int value = 0; + // infinite loop + while (value < 100) { + switch (value) { + // code before the first case statement gets skipped but can be used to + // declare variables + int x = 1; + x = value + 1; + case 0: + break; + case 1: + continue; + case 2: + default: + continue; + } + value++; + } + return 0; +} + +int unroll_loop_FP(int n) { + int ret = 0; + int loop = n + 3 / 4; + switch (n % 8) { + case 0: + do { + ret++; + case 3: + ret++; + if (1) { + case 2: + ret++; + } + case 1: + ret++; + } while (--loop > 0); + } + return ret; +} diff --git a/infer/tests/codetoanalyze/java/performance/Break.java b/infer/tests/codetoanalyze/java/performance/Break.java index 1eff5071f..fc0cad42b 100644 --- a/infer/tests/codetoanalyze/java/performance/Break.java +++ b/infer/tests/codetoanalyze/java/performance/Break.java @@ -27,4 +27,18 @@ private static int break_constant(int p) return break_loop(p, -1); } + +private static void break_outer_loop_FN (int maxI, int maxJ){ + int i = 0 ; + outerloop: + while (i < maxI) { + int j = 0 ; + while (j < maxJ) { + if (i+j > 10) + break outerloop ; + j++ ; + } + i++ ; + }} + } diff --git a/infer/tests/codetoanalyze/java/performance/Continue.java b/infer/tests/codetoanalyze/java/performance/Continue.java new file mode 100644 index 000000000..84a866596 --- /dev/null +++ b/infer/tests/codetoanalyze/java/performance/Continue.java @@ -0,0 +1,21 @@ +/* + * 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. + */ +package codetoanalyze.java.performance; + +public class Continue{ + int continue_outer_loop_FN () +{ + outer: + for (int i = 2; i < 1000; i++) { + for (int j = 2; j < i; j++) { + if (i % j == 0) + continue outer; + } + } + return 0; +} +} diff --git a/infer/tests/codetoanalyze/java/performance/Switch.java b/infer/tests/codetoanalyze/java/performance/Switch.java new file mode 100644 index 000000000..4ef1e84c6 --- /dev/null +++ b/infer/tests/codetoanalyze/java/performance/Switch.java @@ -0,0 +1,44 @@ +/* + * 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. + */ +package codetoanalyze.java.performance; + +public class Switch{ + // Cost 51 + private static void vanilla_switch(int i){ + + for (int p = 0; p < 100; p++) + { + switch (p) { + case 0: + i++; + break; + case 1: case 2: case 3: + break; + default: + return; + } + } + } + //797 + private static int test_switch() { + int value = 0; + // infinite loop + while (value < 100) { + switch (value) { + case 0: + break; + case 1: + continue; + case 2: + default: + continue; + } + value++; + } + return 0; +} +} diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index ec2b1d6a5..5f5db834e 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -7,6 +7,7 @@ codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), codetoanalyze/java/performance/Break.java, int Break.break_constant(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * s$1] codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 7 * s$1] codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * s$1] +codetoanalyze/java/performance/Break.java, void Break.break_outer_loop_FN(int,int), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.compound_while(int), 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.compound_while(int), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * s$1] codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.compound_while(int), 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * s$1] @@ -16,6 +17,7 @@ codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.nested_whil codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.nested_while_and_or(int), 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/java/performance/Compound_loop.java, void Compound_loop.while_and_or(int), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Compound_loop.java, void Compound_loop.while_and_or(int), 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/java/performance/Continue.java, int Continue.continue_outer_loop_FN(), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * s$1] codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 * s$1] codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * (-s$0 + s$1 + 15)] @@ -57,3 +59,7 @@ codetoanalyze/java/performance/JsonUtils.java, StringBuilder JsonUtils.serialize codetoanalyze/java/performance/JsonUtils.java, void JsonUtils.escape(StringBuilder,String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, void JsonUtils.escape(StringBuilder,String), 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/java/performance/JsonUtils.java, void JsonUtils.serialize(StringBuilder,String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/Switch.java, int Switch.test_switch(), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 797] +codetoanalyze/java/performance/Switch.java, int Switch.test_switch(), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798] +codetoanalyze/java/performance/Switch.java, int Switch.test_switch(), 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 797] +codetoanalyze/java/performance/Switch.java, int Switch.test_switch(), 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 797]