From 54eaaa9573c04a91ea3ea18888478c48481d0c39 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Tue, 15 Aug 2017 23:56:34 -0700 Subject: [PATCH] [infer][biabduction] remove the check for null test after dereference on Java Summary: This check is not possible in Java as it natirally happens in the totally legit case of the `try ... finally`. Reviewed By: sblackshear Differential Revision: D5568802 fbshipit-source-id: 24ca074 --- infer/src/backend/symExec.ml | 3 ++- .../tests/codetoanalyze/java/infer/issues.exp | 20 ------------------- 2 files changed, 2 insertions(+), 21 deletions(-) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index c4289eb52..374624b12 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1165,7 +1165,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path | _ -> () in - if not Config.tracing then check_already_dereferenced tenv current_pname cond prop__ ; + if not (Config.tracing || Typ.Procname.is_java current_pname) then + check_already_dereferenced tenv current_pname cond prop__ ; check_condition_always_true_false () ; let n_cond, prop = check_arith_norm_exp tenv current_pname cond prop__ in ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop)) diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index 2c39a05d5..9cb03a8ba 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -40,12 +40,9 @@ codetoanalyze/java/infer/CursorLeaks.java, int CursorLeaks.completeDownloadNotCl codetoanalyze/java/infer/CursorLeaks.java, int CursorLeaks.cursorNotClosed(SQLiteDatabase), 4, RESOURCE_LEAK, [start of procedure cursorNotClosed(...),Skipped call: function or method not found] codetoanalyze/java/infer/CursorLeaks.java, int CursorLeaks.getBucketCountNotClosed(), 10, RESOURCE_LEAK, [start of procedure getBucketCountNotClosed(),Taking false branch,Taking false branch] codetoanalyze/java/infer/CursorLeaks.java, int CursorLeaks.getImageCountHelperNotClosed(String), 13, RESOURCE_LEAK, [start of procedure getImageCountHelperNotClosed(...),Taking true branch,Skipped call: function or method not found] -codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.loadPrefsFromContentProviderClosed(), 3, NULL_TEST_AFTER_DEREFERENCE, [start of procedure loadPrefsFromContentProviderClosed(),Taking false branch] -codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.loadPrefsFromContentProviderNotClosed(), 3, NULL_TEST_AFTER_DEREFERENCE, [start of procedure loadPrefsFromContentProviderNotClosed(),Taking false branch] codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.loadPrefsFromContentProviderNotClosed(), 11, RESOURCE_LEAK, [start of procedure loadPrefsFromContentProviderNotClosed(),Taking false branch,Taking true branch] codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.queryUVMLegacyDbNotClosed(), 4, RESOURCE_LEAK, [start of procedure queryUVMLegacyDbNotClosed(),Skipped call: function or method not found,Taking true branch] codetoanalyze/java/infer/CursorNPEs.java, int CursorNPEs.cursorFromDownloadManagerNPE(DownloadManager), 5, NULL_DEREFERENCE, [start of procedure cursorFromDownloadManagerNPE(...)] -codetoanalyze/java/infer/CursorNPEs.java, void CursorNPEs.cursorFromContentProviderClient(), 3, NULL_TEST_AFTER_DEREFERENCE, [start of procedure cursorFromContentProviderClient(),Taking false branch] codetoanalyze/java/infer/CursorNPEs.java, void CursorNPEs.cursorFromContentResolverNPE(String), 12, NULL_DEREFERENCE, [start of procedure cursorFromContentResolverNPE(...)] codetoanalyze/java/infer/CursorNPEs.java, void CursorNPEs.cursorFromMediaNPE(), 3, NULL_DEREFERENCE, [start of procedure cursorFromMediaNPE()] codetoanalyze/java/infer/DivideByZero.java, int DivideByZero.callDivideByZeroInterProc(), 1, DIVIDE_BY_ZERO, [start of procedure callDivideByZeroInterProc(),start of procedure divideByZeroInterProc(...)] @@ -68,26 +65,16 @@ codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeak codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.gzipInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure gzipInputStreamNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.inflaterInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure inflaterInputStreamNotClosedAfterRead(),Skipped call: function or method not found,exception java.io.IOException] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.pushbackInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure pushbackInputStreamNotClosedAfterRead(),Skipped call: function or method not found,exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.bufferedOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure bufferedOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.bufferedOutputStreamNotClosedAfterWrite(), 8, RESOURCE_LEAK, [start of procedure bufferedOutputStreamNotClosedAfterWrite(),exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.checkedOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure checkedOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.checkedOutputStreamNotClosedAfterWrite(), 8, RESOURCE_LEAK, [start of procedure checkedOutputStreamNotClosedAfterWrite(),exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.cipherOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure cipherOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.cipherOutputStreamNotClosedAfterWrite(), 8, RESOURCE_LEAK, [start of procedure cipherOutputStreamNotClosedAfterWrite(),exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.dataOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure dataOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.dataOutputStreamNotClosedAfterWrite(), 8, RESOURCE_LEAK, [start of procedure dataOutputStreamNotClosedAfterWrite(),exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.deflaterOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure deflaterOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.deflaterOutputStreamNotClosedAfterWrite(), 8, RESOURCE_LEAK, [start of procedure deflaterOutputStreamNotClosedAfterWrite(),exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.digestOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure digestOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.digestOutputStreamNotClosedAfterWrite(), 8, RESOURCE_LEAK, [start of procedure digestOutputStreamNotClosedAfterWrite(),exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.filterOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure filterOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.filterOutputStreamNotClosedAfterWrite(), 8, RESOURCE_LEAK, [start of procedure filterOutputStreamNotClosedAfterWrite(),exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.gzipOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure gzipOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.gzipOutputStreamNotClosedAfterFlush(), 4, RESOURCE_LEAK, [start of procedure gzipOutputStreamNotClosedAfterFlush()] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.gzipOutputStreamNotClosedAfterFlush(), 7, RESOURCE_LEAK, [start of procedure gzipOutputStreamNotClosedAfterFlush(),exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.inflaterOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure inflaterOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.inflaterOutputStreamNotClosedAfterWrite(), 8, RESOURCE_LEAK, [start of procedure inflaterOutputStreamNotClosedAfterWrite(),exception java.io.IOException] -codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.printStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure printStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.printStreamNotClosedAfterWrite(), 6, RESOURCE_LEAK, [start of procedure printStreamNotClosedAfterWrite()] codetoanalyze/java/infer/GuardedByExample.java, Object GuardedByExample.byRefTrickyBad(), 5, UNSAFE_GUARDED_BY_ACCESS, [start of procedure byRefTrickyBad()] codetoanalyze/java/infer/GuardedByExample.java, String GuardedByExample$3.readFromInnerClassBad1(), 2, UNSAFE_GUARDED_BY_ACCESS, [start of procedure readFromInnerClassBad1()] @@ -157,7 +144,6 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions. codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.stringConstantEqualsFalseNotNPE_FP(), 10, NULL_DEREFERENCE, [start of procedure stringConstantEqualsFalseNotNPE_FP(),Taking false branch] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.stringVarEqualsFalseNPE(), 5, NULL_DEREFERENCE, [start of procedure stringVarEqualsFalseNPE(),start of procedure getString2(),return from a call to String NullPointerExceptions.getString2(),Skipped call: function or method not found,Taking true branch] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.testSystemGetPropertyReturn(), 2, NULL_DEREFERENCE, [start of procedure testSystemGetPropertyReturn()] -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(), 6, RESOURCE_LEAK, [start of procedure bufferedReaderNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.fileReaderNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure fileReaderNotClosedAfterRead(),Skipped call: function or method not found,exception java.io.IOException] codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.inputStreamReaderNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure inputStreamReaderNotClosedAfterRead(),Skipped call: function or method not found,exception java.io.IOException] @@ -174,8 +160,6 @@ codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.readConfigNotClos codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.NoResourceLeakWarningAfterCheckState(File,int), 2, PRECONDITION_NOT_MET, [start of procedure NoResourceLeakWarningAfterCheckState(...),Taking false branch] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.activityObtainTypedArrayAndLeak(Activity), 2, RESOURCE_LEAK, [start of procedure activityObtainTypedArrayAndLeak(...),start of procedure ignore(...),return from a call to void ResourceLeaks.ignore(Object)] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.contextObtainTypedArrayAndLeak(Context), 2, RESOURCE_LEAK, [start of procedure contextObtainTypedArrayAndLeak(...),start of procedure ignore(...),return from a call to void ResourceLeaks.ignore(Object)] -codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.copyFileLeak(File,File), 6, NULL_TEST_AFTER_DEREFERENCE, [start of procedure copyFileLeak(...),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] -codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.copyFileLeak(File,File), 8, NULL_TEST_AFTER_DEREFERENCE, [start of procedure copyFileLeak(...),exception java.io.IOException,Switch condition is true. Entering switch case,Taking true branch,Taking false branch] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.copyFileLeak(File,File), 11, RESOURCE_LEAK, [start of procedure copyFileLeak(...),exception java.io.FileNotFoundException] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.copyFileLeak(File,File), 11, RESOURCE_LEAK, [start of procedure copyFileLeak(...),exception java.io.IOException,Switch condition is true. Entering switch case,Taking true branch,exception java.io.IOException] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.deflaterLeak(), 1, RESOURCE_LEAK, [start of procedure deflaterLeak()] @@ -192,19 +176,15 @@ codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.nestedBad1(), 1, codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.nestedBad2(), 1, RESOURCE_LEAK, [start of procedure nestedBad2()] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.nestedBadJarInputStream(File), 1, RESOURCE_LEAK, [start of procedure nestedBadJarInputStream(...)] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.nestedBadJarOutputStream(), 1, RESOURCE_LEAK, [start of procedure nestedBadJarOutputStream()] -codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectInputStreamClosed(), 8, NULL_TEST_AFTER_DEREFERENCE, [start of procedure objectInputStreamClosed(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectInputStreamClosedNestedBad(), 3, RESOURCE_LEAK, [start of procedure objectInputStreamClosedNestedBad()] -codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectInputStreamClosedNestedBad(), 7, NULL_TEST_AFTER_DEREFERENCE, [start of procedure objectInputStreamClosedNestedBad(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectInputStreamNotClosedAfterRead(), 3, RESOURCE_LEAK, [start of procedure objectInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectInputStreamNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure objectInputStreamNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectOutputStreamClosedNestedBad(), 3, RESOURCE_LEAK, [start of procedure objectOutputStreamClosedNestedBad()] -codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectOutputStreamClosedNestedBad(), 7, NULL_TEST_AFTER_DEREFERENCE, [start of procedure objectOutputStreamClosedNestedBad(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectOutputStreamNotClosedAfterWrite(), 4, RESOURCE_LEAK, [start of procedure objectOutputStreamNotClosedAfterWrite()] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectOutputStreamNotClosedAfterWrite(), 7, RESOURCE_LEAK, [start of procedure objectOutputStreamNotClosedAfterWrite(),exception java.io.IOException] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.openHttpURLConnectionNotDisconnected(), 7, RESOURCE_LEAK, [start of procedure openHttpURLConnectionNotDisconnected()] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.openHttpsURLConnectionNotDisconnected(), 3, RESOURCE_LEAK, [start of procedure openHttpsURLConnectionNotDisconnected()] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.parseFromInputStreamAndLeak(JsonFactory), 5, RESOURCE_LEAK, [start of procedure parseFromInputStreamAndLeak(...)] -codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.parseFromInputStreamAndLeak(JsonFactory), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure parseFromInputStreamAndLeak(...),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.parseFromStringAndNotClose(JsonFactory), 4, RESOURCE_LEAK, [start of procedure parseFromStringAndNotClose(...)] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.pipedInputStreamNotClosedAfterRead(PipedOutputStream), 6, RESOURCE_LEAK, [start of procedure pipedInputStreamNotClosedAfterRead(...),exception java.io.IOException] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.pipedOutputStreamNotClosedAfterWrite(), 7, RESOURCE_LEAK, [start of procedure pipedOutputStreamNotClosedAfterWrite(),exception java.io.IOException]