From 0639ef82b7ebdf8d6ef4c31d6d92191c83882b42 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Mon, 25 Jun 2018 07:06:50 -0700
Subject: [PATCH] Cost: also take into account arguments in range

Reviewed By: ddino

Differential Revision: D7956770

fbshipit-source-id: 71e0582
---
 infer/src/checkers/cost.ml                      | 11 ++---------
 .../c/performance/compound_loop_guard.c         |  3 ++-
 .../codetoanalyze/c/performance/cost_test.c     | 17 +++++++++++++++++
 .../codetoanalyze/c/performance/instantiate.c   |  4 ++++
 .../codetoanalyze/c/performance/issues.exp      |  5 +++++
 .../c/performance/two_loops_symbolic.c          |  2 ++
 .../java/performance/ArrayCost.java             |  2 ++
 7 files changed, 34 insertions(+), 10 deletions(-)

diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml
index a3f046996..611ba7054 100644
--- a/infer/src/checkers/cost.ml
+++ b/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
-                      ~filter_loc:(filter_loc formal_pvars control_vars)
+                    BufferOverrunDomain.MemReach.heap_range ~filter_loc:(filter_loc control_vars)
                       mem
               in
               L.(debug Analysis Medium)
diff --git a/infer/tests/codetoanalyze/c/performance/compound_loop_guard.c b/infer/tests/codetoanalyze/c/performance/compound_loop_guard.c
index a31d9b058..119a9989f 100644
--- a/infer/tests/codetoanalyze/c/performance/compound_loop_guard.c
+++ b/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;
diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c
index fd9183718..0e3cba0b5 100644
--- a/infer/tests/codetoanalyze/c/performance/cost_test.c
+++ b/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); }
diff --git a/infer/tests/codetoanalyze/c/performance/instantiate.c b/infer/tests/codetoanalyze/c/performance/instantiate.c
index c4cf5c649..29094e14e 100644
--- a/infer/tests/codetoanalyze/c/performance/instantiate.c
+++ b/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);
diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp
index bd4668d9b..6b370980b 100644
--- a/infer/tests/codetoanalyze/c/performance/issues.exp
+++ b/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]
diff --git a/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c b/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c
index ce25660e0..aa84d8fb8 100644
--- a/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c
+++ b/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++) {
diff --git a/infer/tests/codetoanalyze/java/performance/ArrayCost.java b/infer/tests/codetoanalyze/java/performance/ArrayCost.java
index b007808dc..21907f404 100644
--- a/infer/tests/codetoanalyze/java/performance/ArrayCost.java
+++ b/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;