[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

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

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]