From 1263bfa899a728bbe0c004b2b3dc307e3c08bcb3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= <ezgi@fb.com>
Date: Wed, 16 May 2018 11:16:34 -0700
Subject: [PATCH] Add tests for cost analysis

Reviewed By: mbouaziz

Differential Revision: D8024669

fbshipit-source-id: 479517e
---
 .../c/performance/compound_loop_guard.c       | 66 +++++++++++++++++++
 .../codetoanalyze/c/performance/issues.exp    | 21 ++++++
 .../c/performance/two_loops_symbolic.c        | 36 ++++++++++
 3 files changed, 123 insertions(+)
 create mode 100644 infer/tests/codetoanalyze/c/performance/compound_loop_guard.c
 create mode 100644 infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c

diff --git a/infer/tests/codetoanalyze/c/performance/compound_loop_guard.c b/infer/tests/codetoanalyze/c/performance/compound_loop_guard.c
new file mode 100644
index 000000000..3214b2c34
--- /dev/null
+++ b/infer/tests/codetoanalyze/c/performance/compound_loop_guard.c
@@ -0,0 +1,66 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+/* while loop that contains && in the guard. It gives the correct bound  */
+int compound_while(int m) {
+  int i = 0;
+  int j = 3 * i;
+  while (j == 0 && i < m) {
+    i++;
+  }
+  return j;
+}
+
+/* B will be in the loop and executed ~100 times-- we get infinity due to
+ * control variable problem with gotos */
+int simulated_while_with_and(int p) {
+  int k = 0;
+  int j = 0;
+B:
+  j++;
+  if (k == 0 && j < 100) {
+    goto B; // continue;
+  }
+  return k;
+}
+
+/* shortcut in the conditional, hence we won't loop, and get constant cost */
+int simulated_while_shortcut(int p) {
+  int k = 0;
+  int j = 0;
+B:
+  j++;
+  if (k == 1 && j < 100) {
+    goto B; // continue;
+  }
+  return k;
+}
+
+/* p should be in control vars */
+void while_and_or(int p) {
+  int i = 0;
+  while (p == 1 || (i < 30 && i > 0)) {
+    i++;
+  }
+}
+
+// should be constant cost, but due to p occuring in control vars, we would get
+// +oo for p
+int nested_while_and_or(int p) {
+  int i = 0;
+  int j = 3 * i;
+  while (p == 1 || (i < 30 && i > 0)) {
+    while (p == 1 || (j < 5 && j > 0)) {
+
+      return j;
+    }
+    i++;
+  }
+  return j;
+}
diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp
index 50c4aaa38..8ac0d8dc0 100644
--- a/infer/tests/codetoanalyze/c/performance/issues.exp
+++ b/infer/tests/codetoanalyze/c/performance/issues.exp
@@ -1,3 +1,14 @@
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, CONDITION_ALWAYS_TRUE, WARNING, []
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 7 + 7 * s$1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 7 + 7 * s$1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 7 + 7 * s$1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 10 + 7 * s$1]
+codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
+codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_FALSE, WARNING, []
+codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, WARNING, []
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_shortcut, 5, CONDITION_ALWAYS_FALSE, WARNING, []
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 5, CONDITION_ALWAYS_TRUE, WARNING, []
+codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1004]
@@ -38,3 +49,13 @@ codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TI
 codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 6 * s$1]
 codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 5 + 5 * s$1^2]
 codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 5 + 5 * s$1^2]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6 + 6 * s$1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6 + 6 * s$1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 8 + 6 * s$1 + 6 * s$3]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 8 + 6 * s$1 + 6 * s$3]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 10 + 6 * s$1 + 6 * s$3]
diff --git a/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c b/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c
new file mode 100644
index 000000000..81584c22b
--- /dev/null
+++ b/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c
@@ -0,0 +1,36 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+void nop() { int k = 0; }
+
+/* we report infinity after the first loop, due to the problem in prune node.
+ * Instead, we should obtain the appropriate bounds for the two loops */
+int two_loops_symb(int m) {
+  int p = 10;
+
+  for (int i = 0; i < m; i++) {
+    nop();
+  }
+  for (int j = 0; j < m; j++) {
+    nop();
+  }
+  return p;
+}
+
+/* we report the appropriate bounds for the two loops if the loops are over two
+ * different arguments */
+int two_loops_symb_diff(int m, int k) {
+  int p = 10;
+  for (int i = 0; i < m; i++) {
+    nop();
+  }
+  for (int j = 0; j < k; j++) {
+    nop();
+  }
+  return p;
+}