From 6e6a33cd01389ca5d4cc4c94dfa9ddd8ead2bb0e Mon Sep 17 00:00:00 2001
From: Radu Grigore <rgrigore@fb.com>
Date: Wed, 22 Jan 2020 08:25:12 -0800
Subject: [PATCH] [topl] Added a test for ByteArrayOutputStream.

Summary:
If data comes from an outer OutputStream, then this outer OutputStream
needs to be flushed before getting the byte array.

Reviewed By: jvillard

Differential Revision: D19514569

fbshipit-source-id: e3e025394
---
 infer/tests/codetoanalyze/java/topl/Makefile  |  2 +-
 .../java/topl/baos/BaosTest.java              | 52 +++++++++++++++++++
 .../codetoanalyze/java/topl/baos/Makefile     | 13 +++++
 .../codetoanalyze/java/topl/baos/baos.topl    | 11 ++++
 .../codetoanalyze/java/topl/baos/issues.exp   |  3 ++
 5 files changed, 80 insertions(+), 1 deletion(-)
 create mode 100644 infer/tests/codetoanalyze/java/topl/baos/BaosTest.java
 create mode 100644 infer/tests/codetoanalyze/java/topl/baos/Makefile
 create mode 100644 infer/tests/codetoanalyze/java/topl/baos/baos.topl
 create mode 100644 infer/tests/codetoanalyze/java/topl/baos/issues.exp

diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile
index de10fc799..97032fb55 100644
--- a/infer/tests/codetoanalyze/java/topl/Makefile
+++ b/infer/tests/codetoanalyze/java/topl/Makefile
@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../..
 
-SUBDIRS = hasnext skip tomcat
+SUBDIRS = baos hasnext skip tomcat
 
 test-%:
 	$(MAKE) -C $* test
diff --git a/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java b/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java
new file mode 100644
index 000000000..5a08ef7f6
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java
@@ -0,0 +1,52 @@
+/*
+ * 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.io.ByteArrayOutputStream;
+import java.io.DataOutputStream;
+import java.io.IOException;
+import java.io.ObjectOutputStream;
+
+class BaosTest {
+  void aBad() throws IOException {
+    ByteArrayOutputStream x = new ByteArrayOutputStream();
+    ObjectOutputStream y = new ObjectOutputStream(x);
+    y.writeObject(1337);
+    byte[] bytes = x.toByteArray(); // This may return partial results.
+  }
+
+  /** Bugfix for aBad. */
+  void a1Ok() throws IOException {
+    ByteArrayOutputStream x = new ByteArrayOutputStream();
+    ObjectOutputStream y = new ObjectOutputStream(x);
+    y.writeObject(1337);
+    y.close();
+    byte[] bytes = x.toByteArray();
+  }
+
+  /** Another bugfix for aBad. */
+  void a2Ok() throws IOException {
+    ByteArrayOutputStream x = new ByteArrayOutputStream();
+    ObjectOutputStream y = new ObjectOutputStream(x);
+    y.writeObject(1337);
+    y.flush();
+    byte[] bytes = x.toByteArray();
+  }
+
+  void bBad() throws IOException {
+    ByteArrayOutputStream x = new ByteArrayOutputStream();
+    ObjectOutputStream y = new ObjectOutputStream(x);
+    y.writeObject(1337);
+    byte[] bytes = x.toByteArray();
+    y.close();
+  }
+
+  void cBad() throws IOException {
+    ByteArrayOutputStream x = new ByteArrayOutputStream();
+    DataOutputStream y = new DataOutputStream(x);
+    y.writeLong(1337);
+    byte[] bytes = x.toByteArray();
+  }
+}
diff --git a/infer/tests/codetoanalyze/java/topl/baos/Makefile b/infer/tests/codetoanalyze/java/topl/baos/Makefile
new file mode 100644
index 000000000..850a34195
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/baos/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 100 --symops-per-iteration 13000 --topl-properties baos.topl --biabduction-only
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make
diff --git a/infer/tests/codetoanalyze/java/topl/baos/baos.topl b/infer/tests/codetoanalyze/java/topl/baos/baos.topl
new file mode 100644
index 000000000..539fc28f2
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/baos/baos.topl
@@ -0,0 +1,11 @@
+property BaosRetrieveWithoutFlush
+  nondet (start)
+  start -> start: *
+  start -> valid: ".*OutputStream"(X, Y)
+  valid -> invalid: ".*OutputStream.write.*"(x, *)
+  valid -> invalid: ".*OutputStream.write.*"(x, *, *)
+  valid -> invalid: ".*OutputStream.write.*"(x, *, *, *)
+  invalid -> valid: ".*OutputStream.flush"(x)
+  invalid -> valid: ".*OutputStream.close"(x)
+  invalid -> error: "ByteArrayOutputStream.toByteArray"(y)
+  invalid -> error: "ByteArrayOutputStream.toString"(y)
diff --git a/infer/tests/codetoanalyze/java/topl/baos/issues.exp b/infer/tests/codetoanalyze/java/topl/baos/issues.exp
new file mode 100644
index 000000000..f1e08c7e0
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/baos/issues.exp
@@ -0,0 +1,3 @@
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.bBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []