[topl] Added two (test) properties for ServletResponse.

Summary:
1. One should use either a writer or a stream to send a response, but not both.
2. A response should be forwarded only if it was commited.
Both properties are extracted from API comments on classes in the servlet API.

Reviewed By: jvillard

Differential Revision: D19514568

fbshipit-source-id: 79f0257ed

infer/tests/codetoanalyze/java/topl/Makefile

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

infer/tests/codetoanalyze/java/topl/servlet/Makefile

@@ -5,8 +5,9 @@
 
 TESTS_DIR = ../../../..
 
-INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 10000 --topl-properties tomcat.topl --biabduction-only
+INFER_OPTIONS = --seconds-per-iteration 20 --symops-per-iteration 60000 --topl-properties servlet.topl --biabduction-only
 INFERPRINT_OPTIONS = --issues-tests
+TEST_CLASSPATH = javax.servlet-api-4.0.1.jar
 
 SOURCES = $(wildcard *.java)
 

infer/tests/codetoanalyze/java/topl/servlet/ServletTests.java

@@ -0,0 +1,40 @@
+/*
+ * 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.IOException;
+import java.io.PrintWriter;
+import javax.servlet.RequestDispatcher;
+import javax.servlet.ServletException;
+import javax.servlet.ServletOutputStream;
+import javax.servlet.ServletRequest;
+import javax.servlet.ServletResponse;
+
+class ServletTests {
+  void aBad(ServletResponse response) throws IOException {
+    PrintWriter w = response.getWriter();
+    ServletOutputStream s = response.getOutputStream();
+  }
+
+  void bBad(ServletResponse response) throws IOException {
+    PrintWriter w = response.getWriter();
+    ServletOutputStream s = response.getOutputStream();
+  }
+
+  void cBad(ServletRequest request, ServletResponse response, RequestDispatcher dispatcher)
+      throws IOException, ServletException {
+    PrintWriter w = response.getWriter();
+    dispatcher.forward(request, response);
+  }
+
+  // A bugfix for cBad.
+  void cOk(ServletRequest request, ServletResponse response, RequestDispatcher dispatcher)
+      throws IOException, ServletException {
+    PrintWriter w = response.getWriter();
+    w.flush();
+    dispatcher.forward(request, response);
+  }
+}

infer/tests/codetoanalyze/java/topl/servlet/issues.exp

@@ -0,0 +1,3 @@
+codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.aBad(javax.servlet.ServletResponse):void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.bBad(javax.servlet.ServletResponse):void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.cBad(javax.servlet.ServletRequest,javax.servlet.ServletResponse,javax.servlet.RequestDispatcher):void, 0, TOPL_ERROR, no_bucket, ERROR, []

infer/tests/codetoanalyze/java/topl/servlet/servlet.topl

@@ -0,0 +1,25 @@
+// TODO: Checking any one of {InterleavedResponse, ForwardUncommited} is relatively fast. But,
+// checking both is very slow.
+
+// According to the Servlet API, one should use
+//  - a writer for a textual response
+//  - a stream for a binary response, or for a mixed binary+textual response
+// but never both a writer and a stream.
+property InterleavedResponse
+  message "A ServletResponse was asked for both a writer and a stream."
+  prefix "ServletResponse"
+  nondet (start)
+  start -> start: *
+  start -> gotWriter: getWriter(R)
+  start -> gotStream: getOutputStream(R)
+  gotWriter -> error: getOutputStream(r)
+  gotStream -> error: getWriter(r)
+
+property ForwardUncommitted
+  message "A ServletResponse was forwarded before being committed."
+  nondet (start)
+  start -> start: *
+  start -> gotChannel: C = "ServletResponse.\\(getWriter\\|getOutputStream\\)"(R)
+  gotChannel -> ok: "\\(PrintWriter\\|ServletOutputStream\\).flush.*"(c)
+  gotChannel -> error: "RequestDispatcher.forward"(*, *, r)
+

infer/tests/codetoanalyze/java/topl/servlet/servlet.topl.inactive

@@ -0,0 +1,19 @@
+// A weaker version of InterleavedResponse
+property InterleavedResponseWeak
+  // vertex names: w = got writer; W = used writer; similarly for s, S
+  message "Incompatible methods for putting data into a response were used."
+  prefix "javax.servlet.ServletResponse"
+  nondet (start)
+  start -> start: *
+  start -> w: W = getWriter(R)
+  start -> s: S = getOutputStream(R)
+  w -> sw: S = getOutputStream(r)
+  s -> sw: W = getWriter(r)
+  w -> W: *(w)
+  sw -> sW: *(w)
+  s -> S: *(s)
+  sw -> Sw: *(s)
+  W -> sW: S = getOutputStream(r)
+  S -> Sw: W = getWriter(r)
+  sW -> error: *(s)
+  Sw -> error: *(w)

infer/tests/codetoanalyze/java/topl/tomcat/TomcatFail.java

@@ -1,9 +0,0 @@
-/*
- * 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 TomcatFail {
-  void f() {}
-}

infer/tests/codetoanalyze/java/topl/tomcat/tomcat.topl

@@ -1,52 +0,0 @@
-property ForwardUncommitted
-  message "A ServletResponse was forwarded before being committed."
-  // TODO assume InterleavedResponse_Weak
-  prefix "javax.servlet"
-  prefix "javax.servlet.{ServletOutputStream,ServletResponse}"
-  prefix "java.io.PrintWriter"
-  nondet (start)
-  start -> start: *
-  start -> tracking: R = "ServletResponse.\<init\>"
-  tracking -> ok: flushBuffer(r)
-  tracking -> gotWriter: W = getWriter(r)
-  gotWriter -> ok: flush(w)
-  gotWriter -> ok: flushBuffer(r)
-  tracking -> gotStream: S = getOutputStream(r)
-  gotStream -> ok: flush(s)
-  gotStream -> ok: flushBuffer(r)
-  tracking -> error: "RequestDispatcher.forward"(*, *, r)
-  gotWriter -> error: "RequestDispatcher.forward"(*, *, r)
-  gotStream -> error: "RequestDispatcher.forward"(*, *, r)
-
-// The documentation of ServletResponse.getOutputStream says that "either this
-// method getWriter may be called to write to the body, not both." So,
-// technically, the property is InterleavedResponse1. However, this property is
-// broken, which is why we also have the weaker version InterleavedResponse2.
-property InterleavedResponse1
-  message "A ServletResponse was asked for both a writer and a stream."
-  prefix "javax.servlet.ServletResponse"
-  nondet (start)
-  start -> start: *
-  start -> gotWriter: W = getWriter(R)
-  start -> gotStream: S = getOutputStream(R)
-  gotWriter -> error: getOutputStream(r)
-  gotStream -> error: getWriter(r)
-
-property InterleavedResponse2
-  // vertex names: w = got writer; W = used writer; similarly for s, S
-  message "Incompatible methods for putting data into a response were used."
-  prefix "javax.servlet.ServletResponse"
-  nondet (start)
-  start -> start: *
-  start -> w: W = getWriter(R)
-  start -> s: S = getOutputStream(R)
-  w -> sw: S = getOutputStream(r)
-  s -> sw: W = getWriter(r)
-  w -> W: *(w)
-  sw -> sW: *(w)
-  s -> S: *(s)
-  sw -> Sw: *(s)
-  W -> sW: S = getOutputStream(r)
-  S -> Sw: W = getWriter(r)
-  sW -> error: *(s)
-  Sw -> error: *(w)

infer/tests/java.make

@@ -17,4 +17,4 @@ JSR305 = $(DEPENDENCIES_DIR)/java/jsr-305/jsr305.jar
 INJECT = $(DEPENDENCIES_DIR)/java/jsr-330/javax.inject.jar
 SUNTOOLS = $(DEPENDENCIES_DIR)/java/sun-tools/tools.jar
 
-CLASSPATH=$(ANDROID):$(ANDROIDX_COLLECTION):$(ANDROIDSUPPORT):$(ANNOTATIONS):$(GUAVA):$(JACKSON):$(JSR305):$(INJECT):$(SUNTOOLS):$(JAVA_BUILTINS_DIR):.
+CLASSPATH=$(ANDROID):$(ANDROIDX_COLLECTION):$(ANDROIDSUPPORT):$(ANNOTATIONS):$(GUAVA):$(JACKSON):$(JSR305):$(INJECT):$(SUNTOOLS):$(JAVA_BUILTINS_DIR):$(TEST_CLASSPATH):.