pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[infer][java] Simplify some of the models of Java resources [1/n]

Browse Source 
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
master
Jeremy Dubreil 8 years ago committed by Facebook Github Bot
parent c67de3e827
commit 574d640af0
6 changed files with 7 additions and 100 deletions
Show Stats Download Patch File Download Diff File

22
infer/models/java/src/java/io/BufferedReader.java
Unescape View File

@ -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();

27
infer/models/java/src/java/io/FileReader.java
Unescape View File

@ -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));
}
}

13
infer/models/java/src/java/io/FilterReader.java
Unescape View File

@ -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();

24
infer/models/java/src/java/io/InputStreamReader.java
Unescape View File

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

15
infer/models/java/src/java/io/PushbackReader.java
Unescape View File

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

6
infer/tests/codetoanalyze/java/infer/issues.exp
Unescape View File

@ -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]

Write Preview
Loading…
Cancel
Save