[infer][java] fix the translation of the finally branch

Summary: The previous translation was creating unecessary nodes with unecessary `instanceof` checks.

Reviewed By: jberdine

Differential Revision: D5801019

fbshipit-source-id: eb3a543

infer/src/java/jTransExn.ml

@@ -10,7 +10,6 @@
 
 open! IStd
 module Hashtbl = Caml.Hashtbl
-open Javalib_pack
 open Sawja_pack
 module E = Logging
 
@@ -62,69 +61,66 @@ let translate_exceptions (context: JContext.t) exit_nodes get_body_nodes handler
           | []
            -> Location.none context.source_file
         in
-        let exn_type =
+        match handler.JBir.e_catch_type with
-          let class_name =
+        | None
-            match handler.JBir.e_catch_type with
+         -> let finally_node = create_node loc (Procdesc.Node.Stmt_node "Finally branch") [] in
-            | None
+            Procdesc.node_set_succs_exn procdesc finally_node catch_nodes exit_nodes ;
-             -> JBasics.make_cn "java.lang.Exception"
+            [finally_node]
-            | Some cn
+        | Some exn_class_name
-             -> cn
+         -> let exn_type =
-          in
+              match
-          match
+                JTransType.get_class_type context.program (JContext.get_tenv context)
-            JTransType.get_class_type context.program (JContext.get_tenv context) class_name
+                  exn_class_name
-          with
+              with
-          | {Typ.desc= Tptr (typ, _)}
+              | {Typ.desc= Tptr (typ, _)}
-           -> typ
+               -> typ
-          | _
+              | _
-           -> assert false
+               -> assert false
-        in
+            in
-        let id_instanceof = Ident.create_fresh Ident.knormal in
+            let id_instanceof = Ident.create_fresh Ident.knormal in
-        let instr_call_instanceof =
+            let instr_call_instanceof =
-          let instanceof_builtin = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in
+              let instanceof_builtin = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in
-          let args =
+              let args =
-            [ (Exp.Var id_exn_val, Typ.mk (Tptr (exn_type, Typ.Pk_pointer)))
+                [ (Exp.Var id_exn_val, Typ.mk (Tptr (exn_type, Typ.Pk_pointer)))
-            ; ( Exp.Sizeof
+                ; ( Exp.Sizeof
-                  {typ= exn_type; nbytes= None; dynamic_length= None; subtype= Subtype.exact}
+                      {typ= exn_type; nbytes= None; dynamic_length= None; subtype= Subtype.exact}
-              , Typ.mk Tvoid ) ]
+                  , Typ.mk Tvoid ) ]
-          in
+              in
-          Sil.Call
+              Sil.Call
-            ( Some (id_instanceof, Typ.mk (Tint IBool))
+                ( Some (id_instanceof, Typ.mk (Tint IBool))
-            , instanceof_builtin
+                , instanceof_builtin
-            , args
+                , args
-            , loc
+                , loc
-            , CallFlags.default )
+                , CallFlags.default )
-        in
+            in
-        let if_kind = Sil.Ik_switch in
+            let if_kind = Sil.Ik_switch in
-        let instr_prune_true = Sil.Prune (Exp.Var id_instanceof, loc, true, if_kind) in
+            let instr_prune_true = Sil.Prune (Exp.Var id_instanceof, loc, true, if_kind) in
-        let instr_prune_false =
+            let instr_prune_false =
-          Sil.Prune (Exp.UnOp (Unop.LNot, Exp.Var id_instanceof, None), loc, false, if_kind)
+              Sil.Prune (Exp.UnOp (Unop.LNot, Exp.Var id_instanceof, None), loc, false, if_kind)
-        in
+            in
-        let instr_set_catch_var =
+            let instr_set_catch_var =
-          let catch_var = JContext.set_pvar context handler.JBir.e_catch_var ret_type in
+              let catch_var = JContext.set_pvar context handler.JBir.e_catch_var ret_type in
-          Sil.Store (Exp.Lvar catch_var, ret_type, Exp.Var id_exn_val, loc)
+              Sil.Store (Exp.Lvar catch_var, ret_type, Exp.Var id_exn_val, loc)
-        in
+            in
-        let instr_rethrow_exn =
+            let instr_rethrow_exn =
-          Sil.Store (Exp.Lvar ret_var, ret_type, Exp.Exn (Exp.Var id_exn_val), loc)
+              Sil.Store (Exp.Lvar ret_var, ret_type, Exp.Exn (Exp.Var id_exn_val), loc)
-        in
+            in
-        let node_kind_true = Procdesc.Node.Prune_node (true, if_kind, exn_message) in
+            let node_kind_true = Procdesc.Node.Prune_node (true, if_kind, exn_message) in
-        let node_kind_false = Procdesc.Node.Prune_node (false, if_kind, exn_message) in
+            let node_kind_false = Procdesc.Node.Prune_node (false, if_kind, exn_message) in
-        let node_true =
+            let node_true =
-          let instrs_true = [instr_call_instanceof; instr_prune_true; instr_set_catch_var] in
+              let instrs_true = [instr_call_instanceof; instr_prune_true; instr_set_catch_var] in
-          create_node loc node_kind_true instrs_true
+              create_node loc node_kind_true instrs_true
-        in
+            in
-        let node_false =
+            let node_false =
-          let instrs_false =
+              let instrs_false =
-            [instr_call_instanceof; instr_prune_false]
+                [instr_call_instanceof; instr_prune_false]
-            @ if rethrow_exception then [instr_rethrow_exn] else []
+                @ if rethrow_exception then [instr_rethrow_exn] else []
-          in
+              in
-          create_node loc node_kind_false instrs_false
+              create_node loc node_kind_false instrs_false
-        in
+            in
-        Procdesc.node_set_succs_exn procdesc node_true catch_nodes exit_nodes ;
+            Procdesc.node_set_succs_exn procdesc node_true catch_nodes exit_nodes ;
-        Procdesc.node_set_succs_exn procdesc node_false succ_nodes exit_nodes ;
+            Procdesc.node_set_succs_exn procdesc node_false succ_nodes exit_nodes ;
-        let is_finally = is_none handler.JBir.e_catch_type in
+            [node_true; node_false]
-        if is_finally then [node_true]
-          (* TODO (#4759480): clean up the translation so prune nodes are not created at all *)
-        else [node_true; node_false]
       in
       let is_last_handler = ref true in
       let process_handler succ_nodes handler =

infer/tests/build_systems/ant/issues.exp

@@ -135,8 +135,8 @@ codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.fileOutputStreamT
 codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.readConfigNotCloseStream(String), 5, RESOURCE_LEAK, [start of procedure readConfigNotCloseStream(...)]
 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), 11, RESOURCE_LEAK, [start of procedure copyFileLeak(...),Skipping transferTo(...): unknown method,Taking true branch,exception java.io.IOException]
 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()]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileInputStreamNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure fileInputStreamNotClosedAfterRead(),exception java.io.IOException]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileOutputStreamNotClosed(), 1, RESOURCE_LEAK, [start of procedure fileOutputStreamNotClosed()]

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

@@ -148,21 +148,31 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.
 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(),Skipping FileReader(...): unknown method,exception java.io.IOException]
 codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.inputStreamReaderNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure inputStreamReaderNotClosedAfterRead(),Skipping InputStreamReader(...): unknown method,exception java.io.IOException]
+codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.noNeedToCloseBufferReaderWrapperOk(File), 4, UNINITIALIZED_VALUE, [start of procedure noNeedToCloseBufferReaderWrapperOk(...),exception java.io.IOException,Switch condition is true. Entering switch case,exception java.io.IOException]
 codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pipedReaderFalsePositive(), 5, RESOURCE_LEAK, [start of procedure pipedReaderFalsePositive()]
 codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.pipedReaderNotClosedAfterConnect(PipedWriter), 7, RESOURCE_LEAK, [start of procedure pipedReaderNotClosedAfterConnect(...),exception java.io.IOException]
 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.pushbackReaderNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure pushbackReaderNotClosedAfterRead(),Skipping PushbackReader(...): unknown method,exception java.io.IOException]
 codetoanalyze/java/infer/ReaderLeaks.java, void ReaderLeaks.readerNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure readerNotClosedAfterRead(),Skipping FileReader(...): unknown method,exception java.io.IOException]
 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, String ResourceLeaks.readInstallationFileGood(File), 8, UNINITIALIZED_VALUE, [start of procedure readInstallationFileGood(...),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]
 codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.fileOutputStreamTwoLeaks1(boolean), 6, RESOURCE_LEAK, [start of procedure fileOutputStreamTwoLeaks1(...),Taking false branch]
+codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.readConfigCloseStream(String), 8, UNINITIALIZED_VALUE, [start of procedure readConfigCloseStream(...),exception java.io.IOException]
 codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.readConfigNotCloseStream(String), 5, RESOURCE_LEAK, [start of procedure readConfigNotCloseStream(...)]
+codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.tryWithResource(), 3, UNINITIALIZED_VALUE, [start of procedure tryWithResource(),exception java.io.IOException,Switch condition is true. Entering switch case,exception java.io.IOException]
 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.closeNullQuietlyWithCloseables(), 5, UNINITIALIZED_VALUE, [start of procedure closeNullQuietlyWithCloseables(),exception java.io.FileNotFoundException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.closeNullWithCloseables(), 5, UNINITIALIZED_VALUE, [start of procedure closeNullWithCloseables(),exception java.io.FileNotFoundException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.closeWithCloseablesNestedAlloc(), 5, UNINITIALIZED_VALUE, [start of procedure closeWithCloseablesNestedAlloc(),exception java.io.FileNotFoundException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.closedQuietlyWithCloseables(), 5, UNINITIALIZED_VALUE, [start of procedure closedQuietlyWithCloseables(),exception java.io.IOException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.closedWithCloseables(), 5, UNINITIALIZED_VALUE, [start of procedure closedWithCloseables(),exception java.io.IOException]
 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, UNINITIALIZED_VALUE, [start of procedure copyFileLeak(...),exception java.io.IOException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.copyFileLeak(File,File), 11, RESOURCE_LEAK, [start of procedure copyFileLeak(...),Skipping transferTo(...): unknown method,Taking true branch,exception java.io.IOException]
 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()]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileInputStreamNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure fileInputStreamNotClosedAfterRead(),exception java.io.IOException]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileOutputStreamNotClosed(), 1, RESOURCE_LEAK, [start of procedure fileOutputStreamNotClosed()]
@@ -183,6 +193,7 @@ codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectInputStrea
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.objectOutputStreamClosedNestedBad(), 3, RESOURCE_LEAK, [start of procedure objectOutputStreamClosedNestedBad()]
 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.openHttpURLConnectionDisconnected(), 12, UNINITIALIZED_VALUE, [start of procedure openHttpURLConnectionDisconnected(),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(...)]
@@ -191,11 +202,18 @@ codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.pipedInputStream
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.pipedOutputStreamNotClosedAfterWrite(), 7, RESOURCE_LEAK, [start of procedure pipedOutputStreamNotClosedAfterWrite(),exception java.io.IOException]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.scannerNotClosed(), 1, RESOURCE_LEAK, [start of procedure scannerNotClosed()]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.serverSocketNotClosed(), 12, RESOURCE_LEAK, [start of procedure serverSocketNotClosed(),Skipping ServerSocket(...): unknown method,exception java.io.IOException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.serverSocketWithSocketClosed(), 14, UNINITIALIZED_VALUE, [start of procedure serverSocketWithSocketClosed(),Skipping ServerSocket(...): unknown method,exception java.io.IOException]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.socketNotClosed(), 1, RESOURCE_LEAK, [start of procedure socketNotClosed()]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.themeObtainTypedArrayAndLeak(Resources$Theme), 2, RESOURCE_LEAK, [start of procedure themeObtainTypedArrayAndLeak(...),start of procedure ignore(...),return from a call to void ResourceLeaks.ignore(Object)]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResources(), 8, UNINITIALIZED_VALUE, [start of procedure twoResources(),exception java.io.FileNotFoundException]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResources(), 11, RESOURCE_LEAK, [start of procedure twoResources(),Taking true branch,exception java.io.IOException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesCommonFix(), 8, UNINITIALIZED_VALUE, [start of procedure twoResourcesCommonFix(),exception java.io.FileNotFoundException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesHeliosFix(), 9, UNINITIALIZED_VALUE, [start of procedure twoResourcesHeliosFix(),exception java.io.FileNotFoundException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesHeliosFix(), 12, UNINITIALIZED_VALUE, [start of procedure twoResourcesHeliosFix(),exception java.io.FileNotFoundException]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesRandomAccessFile(), 10, RESOURCE_LEAK, [start of procedure twoResourcesRandomAccessFile(),Taking true branch,exception java.io.IOException]
 codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.zipFileLeakExceptionalBranch(), 5, RESOURCE_LEAK, [start of procedure zipFileLeakExceptionalBranch(),exception java.io.IOException,Switch condition is true. Entering switch case]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.zipFileLeakExceptionalBranch(), 8, UNINITIALIZED_VALUE, [start of procedure zipFileLeakExceptionalBranch(),exception java.io.IOException,Switch condition is true. Entering switch case,exception java.io.FileNotFoundException]
+codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.zipFileNoLeak(), 5, UNINITIALIZED_VALUE, [start of procedure zipFileNoLeak(),exception java.io.IOException]
 codetoanalyze/java/infer/SuppressLintExample.java, void SuppressAllWarnigsInTheClass.shouldNotReportNPE(), 2, NULL_DEREFERENCE, [start of procedure shouldNotReportNPE()]
 codetoanalyze/java/infer/SuppressLintExample.java, void SuppressAllWarnigsInTheClass.shouldNotReportResourceLeak(), 2, RESOURCE_LEAK, [start of procedure shouldNotReportResourceLeak()]
 codetoanalyze/java/infer/SuppressLintExample.java, void SuppressLintExample.shouldReportNPE(), 2, NULL_DEREFERENCE, [start of procedure shouldReportNPE()]