From 574d640af03871058e37aa77d7cf9f8a81fec591 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Thu, 9 Feb 2017 12:34:43 -0800 Subject: [PATCH] [infer][java] Simplify some of the models of Java resources [1/n] Summary: The Java models for resources are way to complex. The main issue I am facing with these models is that small changes in the analysis can affect the generation of the models in some weird ways. For instance, I get different specs for some of the models between my devserver and my devvm, which seems to be mostly related with the backend treatment of `instanceof`. The objective here is to simplify the models as much as possible in order to: 1) make debugging regressions easier 2) get simpler specs and less modeled methods shipped in `models.jar` Reviewed By: sblackshear Differential Revision: D4536115 fbshipit-source-id: 577183a --- .../java/src/java/io/BufferedReader.java | 22 +-------------- infer/models/java/src/java/io/FileReader.java | 27 ------------------- .../models/java/src/java/io/FilterReader.java | 13 +-------- .../java/src/java/io/InputStreamReader.java | 24 +++-------------- .../java/src/java/io/PushbackReader.java | 15 +---------- .../tests/codetoanalyze/java/infer/issues.exp | 6 ----- 6 files changed, 7 insertions(+), 100 deletions(-) delete mode 100644 infer/models/java/src/java/io/FileReader.java diff --git a/infer/models/java/src/java/io/BufferedReader.java b/infer/models/java/src/java/io/BufferedReader.java index a55541543..3d50101ff 100644 --- a/infer/models/java/src/java/io/BufferedReader.java +++ b/infer/models/java/src/java/io/BufferedReader.java @@ -11,27 +11,7 @@ package java.io; import com.facebook.infer.builtins.InferUndefined; -public class BufferedReader extends Reader { - - private Reader in; - - public BufferedReader(Reader in, int sz) { - this.in = in; - } - - public BufferedReader(Reader in) { - this.in = in; - } - - public void close() throws IOException { - if (in instanceof InputStreamReader) { - ((InputStreamReader) in).close(); - } else if (in instanceof BufferedReader) { - ((BufferedReader) in).close(); - } else { - in.close(); - } - } +public abstract class BufferedReader { public int read() throws IOException { return InferUndefined.can_throw_ioexception_int(); diff --git a/infer/models/java/src/java/io/FileReader.java b/infer/models/java/src/java/io/FileReader.java deleted file mode 100644 index 349810840..000000000 --- a/infer/models/java/src/java/io/FileReader.java +++ /dev/null @@ -1,27 +0,0 @@ -/* - * Copyright (c) 2013 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - */ - -package java.io; - - -public class FileReader extends InputStreamReader { - - public FileReader(String fileName) throws FileNotFoundException { - super(new FileInputStream(fileName)); - } - - public FileReader(File file) throws FileNotFoundException { - super(new FileInputStream(file)); - } - - public FileReader(FileDescriptor fd) { - super(new FileInputStream(fd)); - } - -} diff --git a/infer/models/java/src/java/io/FilterReader.java b/infer/models/java/src/java/io/FilterReader.java index 57ff943e7..6cf9a2aa7 100644 --- a/infer/models/java/src/java/io/FilterReader.java +++ b/infer/models/java/src/java/io/FilterReader.java @@ -11,18 +11,7 @@ package java.io; import com.facebook.infer.builtins.InferUndefined; -public abstract class FilterReader extends Reader { - - protected Reader in; - - protected FilterReader(Reader in) { - this.in = in; - } - - public void close() throws IOException { - if (in instanceof InputStreamReader) - ((InputStreamReader) in).close(); - } +public abstract class FilterReader { public int read() throws IOException { return InferUndefined.can_throw_ioexception_int(); diff --git a/infer/models/java/src/java/io/InputStreamReader.java b/infer/models/java/src/java/io/InputStreamReader.java index ab677bb9e..092534d31 100644 --- a/infer/models/java/src/java/io/InputStreamReader.java +++ b/infer/models/java/src/java/io/InputStreamReader.java @@ -9,42 +9,26 @@ package java.io; +import com.facebook.infer.builtins.InferBuiltins; import com.facebook.infer.builtins.InferUndefined; import com.facebook.infer.builtins.InferUtils; import java.nio.charset.Charset; import java.nio.charset.CharsetDecoder; -public class InputStreamReader extends Reader { - - private InputStream in; - - public InputStreamReader(InputStream in) { - this.in = in; - } +public abstract class InputStreamReader { public InputStreamReader(InputStream in, String charsetName) throws UnsupportedEncodingException { if (charsetName == null) throw new NullPointerException("charsetName"); else if (InferUtils.isValidCharset(charsetName)) { - this.in = in; + InferBuiltins.__set_mem_attribute(in); + InferBuiltins.__set_file_attribute(this); } else throw new UnsupportedEncodingException(); } - public InputStreamReader(InputStream in, Charset cs) { - this.in = in; - } - - public InputStreamReader(InputStream in, CharsetDecoder dec) { - this.in = in; - } - - public void close() throws IOException { - in.close(); - } - public int read() throws IOException { return InferUndefined.can_throw_ioexception_int(); } diff --git a/infer/models/java/src/java/io/PushbackReader.java b/infer/models/java/src/java/io/PushbackReader.java index 1ef6ffd3d..9728f1094 100644 --- a/infer/models/java/src/java/io/PushbackReader.java +++ b/infer/models/java/src/java/io/PushbackReader.java @@ -11,19 +11,7 @@ package java.io; import com.facebook.infer.builtins.InferUndefined; -public class PushbackReader extends FilterReader { - - public PushbackReader(Reader in, int size) { - super(in); - } - - public PushbackReader(Reader in) { - super(in); - } - - public void close() throws IOException { - super.close(); - } +public abstract class PushbackReader { public int read() throws IOException { return InferUndefined.can_throw_ioexception_int(); @@ -61,5 +49,4 @@ public class PushbackReader extends FilterReader { InferUndefined.can_throw_ioexception_void(); } - } diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index 152c6ecf1..e16fadf16 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -198,15 +198,12 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions. codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.testSystemGetPropertyReturn(), 2, NULL_DEREFERENCE, [start of procedure testSystemGetPropertyReturn()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.testSystemGetPropertyReturn(), 2, RETURN_VALUE_IGNORED, [start of procedure testSystemGetPropertyReturn()] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.bufferedReaderClosed(), 4, RETURN_VALUE_IGNORED, [start of procedure bufferedReaderClosed()] -codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.bufferedReaderClosed(), 7, NULL_TEST_AFTER_DEREFERENCE, [start of procedure bufferedReaderClosed(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.bufferedReaderNotClosedAfterRead(), 4, RETURN_VALUE_IGNORED, [start of procedure bufferedReaderNotClosedAfterRead()] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.bufferedReaderNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure bufferedReaderNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.fileReaderClosed(), 4, RETURN_VALUE_IGNORED, [start of procedure fileReaderClosed()] -codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.fileReaderClosed(), 7, NULL_TEST_AFTER_DEREFERENCE, [start of procedure fileReaderClosed(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.fileReaderNotClosedAfterRead(), 4, RETURN_VALUE_IGNORED, [start of procedure fileReaderNotClosedAfterRead()] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.fileReaderNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure fileReaderNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.inputStreamReaderClosed(), 4, RETURN_VALUE_IGNORED, [start of procedure inputStreamReaderClosed()] -codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.inputStreamReaderClosed(), 7, NULL_TEST_AFTER_DEREFERENCE, [start of procedure inputStreamReaderClosed(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.inputStreamReaderNotClosedAfterRead(), 4, RETURN_VALUE_IGNORED, [start of procedure inputStreamReaderNotClosedAfterRead()] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.inputStreamReaderNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure inputStreamReaderNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pipedReaderClosed(PipedWriter), 5, RETURN_VALUE_IGNORED, [start of procedure pipedReaderClosed(...)] @@ -217,14 +214,11 @@ codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pipedReaderNotClosed codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pipedReaderNotClosedAfterConstructedWithWriter(), 6, RETURN_VALUE_IGNORED, [start of procedure pipedReaderNotClosedAfterConstructedWithWriter()] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pipedReaderNotClosedAfterConstructedWithWriter(), 8, RESOURCE_LEAK, [start of procedure pipedReaderNotClosedAfterConstructedWithWriter(),exception java.io.IOException] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pushbackReaderClosed(), 4, RETURN_VALUE_IGNORED, [start of procedure pushbackReaderClosed()] -codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pushbackReaderClosed(), 7, NULL_TEST_AFTER_DEREFERENCE, [start of procedure pushbackReaderClosed(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pushbackReaderNotClosedAfterRead(), 4, RETURN_VALUE_IGNORED, [start of procedure pushbackReaderNotClosedAfterRead()] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pushbackReaderNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure pushbackReaderNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.readerClosed(), 4, RETURN_VALUE_IGNORED, [start of procedure readerClosed()] -codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.readerClosed(), 8, NULL_TEST_AFTER_DEREFERENCE, [start of procedure readerClosed(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.readerNotClosedAfterRead(), 4, RETURN_VALUE_IGNORED, [start of procedure readerNotClosedAfterRead()] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.readerNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure readerNotClosedAfterRead(),exception java.io.IOException] -codetoanalyze/java/infer/ResourceLeaks.java, InputStreamReader ResourceLeaks.withCharset(URLConnection), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure withCharset(...),Taking false branch] codetoanalyze/java/infer/ResourceLeaks.java, String ResourceLeaks.readInstallationFileBad(File), 6, RESOURCE_LEAK, [start of procedure readInstallationFileBad(...),exception java.io.IOException] codetoanalyze/java/infer/ResourceLeaks.java, boolean ResourceLeaks.jarFileNotClosed(), 3, RESOURCE_LEAK, [start of procedure jarFileNotClosed()] codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.fileOutputStreamTwoLeaks1(boolean), 3, RESOURCE_LEAK, [start of procedure fileOutputStreamTwoLeaks1(...),Taking true branch]