Cost: also take into account arguments in range

Reviewed By: ddino

Differential Revision: D7956770

fbshipit-source-id: 71e0582

infer/src/checkers/cost.ml

@@ -133,11 +133,9 @@ module BoundMap = struct
     L.(debug Analysis Medium) "@\n******* END Bound Map ITV **** @\n\n"
 
 
-  let filter_loc formal_pvars vars_to_keep = function
+  let filter_loc vars_to_keep = function
     | AbsLoc.Loc.Var (Var.LogicalVar _) ->
         false
-    | AbsLoc.Loc.Var (Var.ProgramVar pvar) when List.mem formal_pvars pvar ~equal:Pvar.equal ->
-        false
     | AbsLoc.Loc.Var var when Control.VarSet.mem var vars_to_keep ->
         true
     | _ ->
@@ -145,10 +143,6 @@ module BoundMap = struct
 
 
   let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map loop_inv_map =
-    let pname = Procdesc.get_proc_name node_cfg in
-    let formal_pvars =
-      Procdesc.get_formals node_cfg |> List.map ~f:(fun (m, _) -> Pvar.mk m pname)
-    in
     let compute_node_upper_bound bound_map node =
       let node_id = NodeCFG.Node.id node in
       match Procdesc.Node.get_kind node with
@@ -178,8 +172,7 @@ module BoundMap = struct
                        unreachable returning cost 0 \n" ;
                     BasicCost.zero
                 | NonBottom mem ->
-                    BufferOverrunDomain.MemReach.heap_range
+                    BufferOverrunDomain.MemReach.heap_range ~filter_loc:(filter_loc control_vars)
-                      ~filter_loc:(filter_loc formal_pvars control_vars)
                       mem
               in
               L.(debug Analysis Medium)

infer/tests/codetoanalyze/c/performance/compound_loop_guard.c

@@ -5,7 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  */
 
-/* while loop that contains && in the guard. It gives the correct bound  */
+/* while loop that contains && in the guard. It gives the correct bound.
+ * Expected: Theta(m)  */
 int compound_while(int m) {
   int i = 0;
   int j = 3 * i;

infer/tests/codetoanalyze/c/performance/cost_test.c

@@ -79,6 +79,7 @@ int loop1_bad() {
   return 0;
 }
 
+// Expected: Theta(k)
 int loop2_bad(int k) {
 
   for (int i = 0; i < k; i++) {
@@ -87,6 +88,7 @@ int loop2_bad(int k) {
   return 0;
 }
 
+// Expected: ~15
 int loop3_bad(int k) {
 
   for (int i = k; i < k + 15; i++) {
@@ -109,3 +111,18 @@ int main_bad() {
   k4 = bar_OK() + foo_OK() + cond_OK(19) * 3;
   return 0;
 }
+
+// Expected: Theta(20-m)
+int while_upto20_bad(int m) {
+  while (m < 20) {
+    int l = 0;
+    m++;
+  }
+  return m;
+}
+
+void call_while_upto20_minus100_bad() { while_upto20_bad(-100); }
+
+void call_while_upto20_10_good() { while_upto20_bad(10); }
+
+void call_while_upto20_unsigned_good_FP(unsigned x) { while_upto20_bad(x); }

infer/tests/codetoanalyze/c/performance/instantiate.c

@@ -7,6 +7,7 @@
 
 void nop() { int x = 0; }
 
+// Expected: Theta(n)
 void do_n_times(int n) {
   for (int i = 0; i < n; i++) {
     nop();
@@ -15,14 +16,17 @@ void do_n_times(int n) {
 
 void do_2_times_Good() { do_n_times(2); }
 
+// Expected: ~2000
 void do_2K_times_Bad() { do_n_times(2000); }
 
+// Expected: Theta(m^2)
 void do_m2_times(int m) {
   for (int i = 0; i < m; i++) {
     do_n_times(m);
   }
 }
 
+// Expected: Theta(m^2)
 void do_half_m2_times(int m) {
   for (int i = 0; i < m; i++) {
     do_n_times(i);

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

@@ -32,6 +32,8 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10,
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * s$1]
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
+codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 604]
+codetoanalyze/c/performance/cost_test.c, call_while_upto20_unsigned_good_FP, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * (-u$0 + 20)]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1002]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1002]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004]
@@ -45,6 +47,9 @@ codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_
 codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * (-s$0 + s$1 + 15)]
 codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 11 * (-s$0 + s$1 + 15)]
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 211]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-s$0 + 20)]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-s$0 + 20)]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * (-s$0 + 20)]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1204]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1204]

infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c

@@ -6,6 +6,7 @@
  */
 void nop() { int k = 0; }
 
+// Expected: Theta(m)
 int two_loops_symb(int m) {
   int p = 10;
 
@@ -18,6 +19,7 @@ int two_loops_symb(int m) {
   return p;
 }
 
+// Expected: Theta(m + k)
 int two_loops_symb_diff(int m, int k) {
   int p = 10;
   for (int i = 0; i < m; i++) {

infer/tests/codetoanalyze/java/performance/ArrayCost.java

@@ -6,6 +6,7 @@
  */
 public class ArrayCost {
 
+  // expected: Theta(mag.length)
   private void ArrayCost(int[] mag) {
 
     int i = 0;
@@ -16,6 +17,7 @@ public class ArrayCost {
     }
   }
 
+  // expected: ~31
   private static boolean isPowOfTwo_FP(int value) {
     int ones = 0;
     int v = value;