Fix control var analysis for loops with multiple back-edges per loop head

Summary:
I realized that control variable analysis was broken when we had multiple back-edges for the same loop. This is often the case when we have a switch statement combined with continue in a loop (see `test_switch` in `switch_continue.c`) or when we have disjunctive guards in do-while loops.

This diff fixes that by

- defining a loop by its loophead (the target of its backedges) rather than its back-edges. Then it converts back-edge list to a map from loop_head to sources of the loop's back-edges.
- collecting multiple guard nodes that come from potentially multiple exit nodes per loop head

In addition, it also removes the wrong assumption that an exit node belongs to a single loop head.

Reviewed By: mbouaziz

Differential Revision: D8398061

fbshipit-source-id: abaf288

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  *)
+(** Map exit node -> loop head set  *)
-module ExitNodeToGuardNodes = AbstractDomain.Map (Procdesc.Node) (GuardNodes)
+module ExitNodeToLoopHeads = Procdesc.NodeMap
 
-(** Map loop header node -> prune nodes in the loop guard  *)
+(** Map loop head -> prune nodes in the loop guard  *)
-module LoopHeaderToGuardNodes = AbstractDomain.Map (Procdesc.Node) (GuardNodes)
+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
+    match Procdesc.Node.get_kind node with
-    | Some loop_nodes ->
+    | Procdesc.Node.Prune_node _ -> (
-        L.(debug Analysis Medium)
+      match ExitNodeToLoopHeads.find_opt node exit_map with
-          "@\n>>>Exit node %a loop nodes=%a  @\n\n" Procdesc.Node.pp node GuardNodes.pp loop_nodes ;
+      | Some loop_heads ->
-        get_control_vars loop_nodes |> Domain.diff astate'
+          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 =
+let compute_control_vars control_invariant_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 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

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 *)
+              (* compute control vars, i.e. set of variables that affect the execution count *)
-              let all_deps = Control.compute_all_deps control_invariant_map node in
+              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)

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
+(* Get a pair of maps (exit_map, loop_head_to_guard_map) where
-   exit_to_guard_map : exit_node -> guard_nodes
+   exit_map : exit_node -> loop_head set (i.e. target of the back edges) 
-   loop_header_to_guard_map : loop_header (i.e. target of the back edge) -> guard_nodes and
+   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*)
+  (* Since there could be multiple back-edges per loop, collect all
-  let back_edge_set = get_back_edges cfg in
+     source nodes per loop head *)
-  List.fold_left
+  (* loop_head (target of back-edges) --> source nodes *)
-    ~f:(fun Control.({exit_map; loop_header_map}) {source; target} ->
+  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) ;
+        "Back-edge source list : [%a] --> loop_head: %i \n" (Pp.comma_seq Procdesc.Node.pp)
-      let loop_nodes = get_all_nodes_upwards_until target [source] in
+        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 ->
+        (List.fold_left ~init:exit_map ~f:(fun exit_map_acc exit_node ->
-             (*Make sure an exit node only belongs to a single loop *)
+             Control.ExitNodeToLoopHeads.update exit_node
-             assert (not (Control.ExitNodeToGuardNodes.mem exit_node acc)) ;
+               (function
-             Control.ExitNodeToGuardNodes.add exit_node guard_prune_nodes acc ))
+                   | 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' =
+      let loop_head_to_guard_nodes' =
-        (*Make sure a loop header only belongs to a single loop *)
+        Control.LoopHeadToGuardNodes.update loop_head
-        assert (not (Control.LoopHeaderToGuardNodes.mem target loop_header_map)) ;
+          (function
-        Control.LoopHeaderToGuardNodes.add target guard_prune_nodes loop_header_map
+              | 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'} )
+      Control.{exit_map= exit_map'; loop_head_to_guard_nodes= loop_head_to_guard_nodes'} )
-    back_edge_set
+    loop_head_to_source_nodes_map
-    ~init:
+    Control.
-      Control.
+      { exit_map= Control.ExitNodeToLoopHeads.empty
-        { exit_map= Control.ExitNodeToGuardNodes.empty
+      ; loop_head_to_guard_nodes= Control.LoopHeadToGuardNodes.empty }
-        ; loop_header_map= Control.LoopHeaderToGuardNodes.empty }

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]

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;
+}

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++ ;
+    }}
+
 }

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;
+}
+}

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;
+}
+}

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]