[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

@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../..
 
-SUBDIRS = hasnext skip tomcat
+SUBDIRS = baos hasnext skip tomcat
 
 test-%:
 	$(MAKE) -C $* test

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();
+  }
+}

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

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)

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, []