From 2888a90e2a34a1a84f9480c6e2c9f8b8d657fe87 Mon Sep 17 00:00:00 2001
From: Radu Grigore <rgrigore@fb.com>
Date: Wed, 26 Feb 2020 07:33:39 -0800
Subject: [PATCH] [topl] Added tests for inefficient iteration

Summary:
The test shows what that TOPL can express, in addition to bugs,
efficiency properties. However, there seems to be an underlying problem
in biabdaction that prevents this particular problem from being caught.

Reviewed By: ngorogiannis

Differential Revision: D20005404

fbshipit-source-id: 466f79050
---
 .../codetoanalyze/java/topl/slowIter/Makefile | 13 +++++++
 .../java/topl/slowIter/SlowIterTests.java     | 34 +++++++++++++++++++
 .../java/topl/slowIter/slowIter.topl          |  8 +++++
 3 files changed, 55 insertions(+)
 create mode 100644 infer/tests/codetoanalyze/java/topl/slowIter/Makefile
 create mode 100644 infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java
 create mode 100644 infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl

diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile
new file mode 100644
index 000000000..b36e06160
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile
@@ -0,0 +1,13 @@
+# Copyright (c) Facebook, Inc. and its affiliates.
+#
+# This source code is licensed under the MIT license found in the
+# LICENSE file in the root directory of this source tree.
+
+TESTS_DIR = ../../../..
+
+INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 20000 --topl-properties slowIter.topl --biabduction-only
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make
diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java b/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java
new file mode 100644
index 000000000..465566a22
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java
@@ -0,0 +1,34 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+import java.util.Map;
+
+class SlowIterTests {
+  // T62611635
+  static <K, V> void FN_aBad(Map<K, V> m) {
+    for (K k : m.keySet()) {
+      System.out.printf("%s -> %s\n", k, m.get(k));
+    }
+  }
+
+  static <K, V> void aOk(Map<K, V> m) {
+    for (Map.Entry<K, V> e : m.entrySet()) {
+      System.out.printf("%s -> %s\n", e.getKey(), e.getValue());
+    }
+  }
+
+  // Inter-procedural variant of aBad.
+  static <K, V> void FN_bBad(Map<K, V> m) {
+    for (K k : m.keySet()) {
+      print(k, m);
+    }
+  }
+
+  static <K, V> void print(K k, Map<K, V> m) {
+    System.out.printf("%s -> %s\n", k, m.get(k));
+  }
+}
diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl b/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl
new file mode 100644
index 000000000..54500efe0
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl
@@ -0,0 +1,8 @@
+property ShouldUseEntries
+  nondet (start iteratingKeys)
+  start -> start: *
+  start -> gotKeys: S = "Map.keySet"(M)
+  gotKeys -> iteratingKeys: I = "Set.iterator"(s)
+  iteratingKeys -> iteratingKeys: *
+  iteratingKeys -> gotOneKey: K = "Iterator.next"(i)
+  gotOneKey -> error: ".*Map.get"(m, k)