From a94fab55e831a3a915b807959f167498b58ecf9e Mon Sep 17 00:00:00 2001
From: Cristiano Calcagno <cristianoc@fb.com>
Date: Wed, 8 Jul 2015 16:24:48 -0200
Subject: [PATCH] [Eradicate] Fix issue where direct throw instructions were
 not handled like method calls that trow exceptions.

---
 infer/src/backend/cfg.ml                      |  2 ++
 infer/src/backend/cfg.mli                     |  3 +++
 infer/src/checkers/typeCheck.ml               |  8 ++++++-
 infer/src/java/jTrans.ml                      |  3 +--
 .../java/eradicate/ReturnNotNullable.java     | 23 +++++++++++++++++++
 .../java/eradicate/ReturnNotNullableTest.java | 12 ++++++++--
 6 files changed, 46 insertions(+), 5 deletions(-)

diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml
index 557e1fb4d..2e77d45e8 100644
--- a/infer/src/backend/cfg.ml
+++ b/infer/src/backend/cfg.ml
@@ -54,6 +54,8 @@ module Node = struct
 
   let exn_handler_kind = Stmt_node "exception handler"
   let exn_sink_kind = Stmt_node "exceptions sink"
+  let throw_kind = Stmt_node "throw"
+
 
   type cfg = (** data type for the control flow graph *)
     { node_id : int ref;
diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli
index 2dfddca99..b20197b35 100644
--- a/infer/src/backend/cfg.mli
+++ b/infer/src/backend/cfg.mli
@@ -145,6 +145,9 @@ module Node : sig
   (** kind of Stmt_node for an exceptions sink. *)
   val exn_sink_kind : nodekind
 
+  (** kind of Stmt_node for a throw instruction. *)
+  val throw_kind : nodekind
+
   (** Append the instructions and temporaries to the list of instructions to execute *)
   val append_instrs_temps : t -> Sil.instr list -> Ident.t list -> unit
 
diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml
index 05664a864..3f02535f5 100644
--- a/infer/src/checkers/typeCheck.ml
+++ b/infer/src/checkers/typeCheck.ml
@@ -938,13 +938,19 @@ let typecheck_node
   let typestates_exn = ref [] in
   let handle_exceptions typestate instr = match instr with
     | Sil.Call (_, Sil.Const (Sil.Cfun callee_pname), _, _, _) ->
+    (* check if the call might throw an exception *)
         let exceptions =
           match get_proc_desc callee_pname with
           | Some callee_pdesc ->
               (Specs.proc_get_attributes callee_pname callee_pdesc).Sil.exceptions
           | None -> [] in
         if exceptions <> [] then
-          typestates_exn := typestate :: !typestates_exn;
+          typestates_exn := typestate :: !typestates_exn
+    | Sil.Set (Sil.Lvar pv, _, _, _) when
+    Sil.pvar_is_return pv &&
+    Cfg.Node.get_kind node = Cfg.Node.throw_kind ->
+    (* throw instruction *)
+        typestates_exn := typestate :: !typestates_exn
     | _ -> () in
 
   let canonical_node = find_canonical_duplicate node in
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index 1e093d8bb..59d1bfc5a 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -936,11 +936,10 @@ let rec instruction context pc instr : translation =
         else
           Prune (prune_node_true, prune_node_false)
     | JBir.Throw expr ->
-        let node_kind = Cfg.Node.Stmt_node "throw" in
         let (ids, instrs, sil_expr) = expression context pc expr in
         let sil_exn = Sil.Const (Sil.Cexn sil_expr) in
         let sil_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
-        let node = create_node node_kind ids (instrs @ [sil_instr]) in
+        let node = create_node Cfg.Node.throw_kind ids (instrs @ [sil_instr]) in
         JContext.add_goto_jump context pc JContext.Exit;
         Instr node
     | JBir.New (var, cn, constr_type_list, constr_arg_list) ->
diff --git a/infer/tests/codetoanalyze/java/eradicate/ReturnNotNullable.java b/infer/tests/codetoanalyze/java/eradicate/ReturnNotNullable.java
index ad6b5e974..f26104f23 100644
--- a/infer/tests/codetoanalyze/java/eradicate/ReturnNotNullable.java
+++ b/infer/tests/codetoanalyze/java/eradicate/ReturnNotNullable.java
@@ -88,4 +88,27 @@ public class ReturnNotNullable {
   String testOptional(Optional<String> os) {
     return os.orNull();
   }
+
+  class E extends Exception {
+  }
+
+  String return_null_in_catch() {
+    try {
+      throw new E();
+    } catch (E e) {
+      return null;
+    }
+  }
+
+  String return_null_in_catch_after_throw() {
+    try {
+      try {
+        throw new E();
+      } catch (E e) {
+        throw e;
+      }
+    } catch (E e) {
+      return null;
+    }
+  }
 }
diff --git a/infer/tests/endtoend/java/eradicate/ReturnNotNullableTest.java b/infer/tests/endtoend/java/eradicate/ReturnNotNullableTest.java
index bd376f3a8..afa5c202a 100644
--- a/infer/tests/endtoend/java/eradicate/ReturnNotNullableTest.java
+++ b/infer/tests/endtoend/java/eradicate/ReturnNotNullableTest.java
@@ -49,13 +49,21 @@ public class ReturnNotNullableTest {
       throws IOException, InterruptedException, InferException {
 
 
-    String[] nullableMethods = {"returnNull", "returnNullable"};
+    String[] nullableMethods = {
+        "returnNull",
+        "returnNullable",
+        "return_null_in_catch",
+        "return_null_in_catch_after_throw",
+    };
     List<ErrorPattern> errorPatterns = createPatterns(
         RETURN_NOT_NULLABLE,
         SOURCE_FILE,
         nullableMethods);
 
-    String[] redundantMethods = {"redundantEq", "redundantNeq"};
+    String[] redundantMethods = {
+        "redundantEq",
+        "redundantNeq",
+    };
     errorPatterns.addAll(
         createPatterns(
             CONDITION_REDUNDANT_NONNULL,