From 0fc2769a65f457cada59d5591f648c6fe85e5f73 Mon Sep 17 00:00:00 2001
From: Radu Grigore <rgrigore@fb.com>
Date: Wed, 4 Mar 2020 06:09:12 -0800
Subject: [PATCH] [topl] A test for comparing arguments.

Summary:
This is the kind of property for which the previous syntax forced one to
use spurious registers.

Reviewed By: ngorogiannis

Differential Revision: D20118863

fbshipit-source-id: b49740d33
---
 infer/tests/codetoanalyze/java/topl/Makefile  |  2 +-
 .../java/topl/compareArgs/CompareArgs.java    | 30 +++++++++++++++++++
 .../java/topl/compareArgs/CompareArgs.topl    |  4 +++
 .../java/topl/compareArgs/Makefile            | 13 ++++++++
 .../java/topl/compareArgs/issues.exp          |  2 ++
 5 files changed, 50 insertions(+), 1 deletion(-)
 create mode 100644 infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.java
 create mode 100644 infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.topl
 create mode 100644 infer/tests/codetoanalyze/java/topl/compareArgs/Makefile
 create mode 100644 infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp

diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile
index ec70815b8..fcc22df4f 100644
--- a/infer/tests/codetoanalyze/java/topl/Makefile
+++ b/infer/tests/codetoanalyze/java/topl/Makefile
@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../..
 
-SUBDIRS = baos hasnext skip servlet
+SUBDIRS = baos compareArgs hasnext skip servlet
 
 test-%:
 	$(MAKE) -C $* test
diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.java b/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.java
new file mode 100644
index 000000000..934541b2f
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.java
@@ -0,0 +1,30 @@
+/*
+ * 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.
+ */
+class CompareArgs {
+  static int max(int[] a, int i, int k) {
+    int m = a[i];
+    for (int j = i + 1; j < k; ++j) {
+      m = Math.max(m, a[j]);
+    }
+    return m;
+  }
+
+  static void aBad() {
+    int[] a = new int[10];
+    int x = max(a, 2, 2);
+  }
+
+  static void bOk() {
+    int[] a = new int[10];
+    int x = max(a, 2, 3);
+  }
+
+  static void cBad() {
+    int[] a = new int[10];
+    int x = max(a, 2, 1);
+  }
+}
diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.topl b/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.topl
new file mode 100644
index 000000000..2f640773a
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.topl
@@ -0,0 +1,4 @@
+property MaxArgs
+  nondet (start)
+  start -> start: *
+  start -> error: "CompareArgs.max"(Ignore, I, J, IgnoreRet) when I >= J
diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile
new file mode 100644
index 000000000..625a25205
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/compareArgs/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 4000 --topl-properties CompareArgs.topl --biabduction-only
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make
diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp b/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp
new file mode 100644
index 000000000..521c632e2
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp
@@ -0,0 +1,2 @@
+codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []