Fix control variable imprecision in do while loops

Reviewed By: ddino

Differential Revision: D8608040

fbshipit-source-id: 13a9048

infer/src/IR/Procdesc.ml

@@ -98,6 +98,14 @@ module Node = struct
   (** Get the predecessors of the node *)
   let get_preds node = node.preds
 
+  (** Get siblings *)
+  let get_siblings node =
+    get_preds node
+    |> List.fold_left ~init:[] ~f:(fun acc parent ->
+           let siblings = get_succs parent |> List.filter ~f:(fun n -> not (equal node n)) in
+           List.rev_append siblings acc )
+
+
   (** Get the node kind *)
   let get_kind node = node.kind
 

infer/src/IR/Procdesc.mli

@@ -84,6 +84,9 @@ module Node : sig
   val get_preds : t -> t list
   (** Get the predecessor nodes of the current node *)
 
+  val get_siblings : t -> t list
+  (** Get siblings of the current node *)
+
   val get_proc_name : t -> Typ.Procname.t
   (** Get the name of the procedure the node belongs to *)
 

infer/src/checkers/loop_control.ml

@@ -92,6 +92,22 @@ let is_prune node =
   match Procdesc.Node.get_kind node with Procdesc.Node.Prune_node _ -> true | _ -> false
 
 
+(* Remove pairs of prune nodes that are for the same condition,
+   i.e. sibling of the same parent. This is necessary to prevent
+   picking unnecessary control variables in do-while like loops *)
+let remove_prune_node_pairs exit_nodes guard_nodes =
+  let exit_nodes = Control.GuardNodes.of_list exit_nodes in
+  let except_exit_nodes = Control.GuardNodes.diff guard_nodes exit_nodes in
+  L.(debug Analysis Medium) "Except exit nodes: [%a]\n" Control.GuardNodes.pp except_exit_nodes ;
+  except_exit_nodes
+  |> Control.GuardNodes.filter (fun node ->
+         is_prune node
+         && Procdesc.Node.get_siblings node |> List.hd
+            |> Option.value_map ~default:false ~f:(fun sibling ->
+                   not (Control.GuardNodes.mem sibling except_exit_nodes) ) )
+  |> Control.GuardNodes.union exit_nodes
+
+
 (* 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
@@ -119,7 +135,8 @@ let get_control_maps cfg =
       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 loop_head exit_nodes |> Control.GuardNodes.filter is_prune
+        get_all_nodes_upwards_until loop_head exit_nodes |> remove_prune_node_pairs exit_nodes
+        |> Control.GuardNodes.filter is_prune
       in
       let exit_map' =
         (List.fold_left ~init:exit_map ~f:(fun exit_map_acc exit_node ->

infer/tests/codetoanalyze/c/performance/issues.exp

@@ -91,6 +91,11 @@ codetoanalyze/c/performance/invariant.c, while_infinite_FN, 2, CONDITION_ALWAYS_
 codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2002]
 codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2002]
 codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2004]
+codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 225]
+codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 225]
+codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 225]
+codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 225]
+codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226]
 codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 320]
 codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 320]
 codetoanalyze/c/performance/loops.c, if_in_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 320]

infer/tests/codetoanalyze/c/performance/loops.c

@@ -36,6 +36,18 @@ int if_out_loop(int t) {
   return p;
 }
 
+int do_while_independent_of_p(int p) {
+  int a = 0;
+  do {
+    if (p == 15) {
+      p = p + 1;
+    }
+    a++;
+  } while (a < 25);
+
+  return 0;
+}
+
 void larger_state_FN() {
 
   int i = 0, k = 0;

infer/tests/codetoanalyze/java/performance/Loops.java

@@ -0,0 +1,38 @@
+/*
+ * 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 Loops{
+
+  static int do_while_independent_of_p (int p) {
+   int a = 0;
+   do {
+         if( p == 15) {
+            p = p + 1;
+         }
+         a++;
+   } while( a < 25 );
+
+   return 0;
+  }
+
+  /* can't handle nested loops yet, but control vars of both loops must
+     be {a, b} */
+  static void nested_do_while_FP (int p) {
+    int a = 10;
+    int b = 0;
+    do {
+      do{
+        if( p == 15) {
+            p = p + 1;
+         }
+        b++;
+      }while ( b < 10);
+      a++;
+    } while( a < 20 );
+  }
+}

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -59,6 +59,10 @@ 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/Loops.java, int Loops.do_while_independent_of_p(int), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 249]
+codetoanalyze/java/performance/Loops.java, int Loops.do_while_independent_of_p(int), 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250]
+codetoanalyze/java/performance/Loops.java, int Loops.do_while_independent_of_p(int), 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 249]
+codetoanalyze/java/performance/Loops.java, void Loops.nested_do_while_FP(int), 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]