[pre-analysis] Add models for `no_return` and handle throw-catch better

Summary:
- Add `no_return`  models for Java's `exit(...)` methods (can be extended further later on)
- handle throw-catch better by short-cutting throw nodes to not exit node but to all **catch nodes** that are reachable by the node. If there is no catch node, we short-cut to the exit node as before.

This removes a FP from deadstore tests because before we simply were not able to handle CF from throw-> catch nodes at all.

Reviewed By: skcho

Differential Revision: D20769039

fbshipit-source-id: e978f6cdb

infer/src/backend/NoReturnModels.ml

@@ -0,0 +1,16 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+let no_return = true
+
+let dispatch : (Tenv.t, bool, unit) ProcnameDispatcher.ProcName.dispatcher =
+  let open ProcnameDispatcher.ProcName in
+  make_dispatcher
+    [ +PatternMatch.implements_lang "System" &:: "exit" <>--> no_return
+    ; +PatternMatch.implements_lang "Runtime" &:: "exit" <>--> no_return ]

infer/src/backend/preanal.ml

@@ -313,7 +313,7 @@ end
 (** pre-analysis to cut control flow after calls to functions whose type indicates they do not
     return *)
 module NoReturn = struct
-  let has_noreturn_call node =
+  let has_noreturn_call tenv node =
     Procdesc.Node.get_instrs node
     |> Instrs.exists ~f:(fun (instr : Sil.instr) ->
            match instr with
@@ -322,17 +322,54 @@ module NoReturn = struct
              | Some {ProcAttributes.is_no_return= true} ->
                  true
              | _ ->
-                 false )
+                 NoReturnModels.dispatch tenv proc_name |> Option.value ~default:false )
            | _ ->
                false )
 
 
-  let process proc_desc =
+  let has_throw_call node =
+    Procdesc.Node.get_instrs node
+    |> Instrs.exists ~f:(fun (instr : Sil.instr) ->
+           match instr with
+           | Call (_, Const (Cfun proc_name), _, _, _) ->
+               String.equal
+                 (Procname.get_method BuiltinDecl.objc_cpp_throw)
+                 (Procname.get_method proc_name)
+           | _ ->
+               false )
+
+
+  let get_all_reachable_catch_nodes start_node =
+    let rec worklist ~todo ~visited result =
+      if Procdesc.NodeSet.is_empty todo then result
+      else
+        let el = Procdesc.NodeSet.choose todo in
+        let todo = Procdesc.NodeSet.remove el todo in
+        if Procdesc.NodeSet.mem el visited then worklist ~todo ~visited result
+        else
+          let succs = Procdesc.Node.get_succs el |> Procdesc.NodeSet.of_list in
+          let visited = Procdesc.NodeSet.add el visited in
+          worklist
+            ~todo:(Procdesc.NodeSet.union succs todo)
+            ~visited
+            (Procdesc.Node.get_exn el @ result)
+    in
+    worklist ~todo:(Procdesc.NodeSet.singleton start_node) ~visited:Procdesc.NodeSet.empty []
+
+
+  let process tenv proc_desc =
+    let exit_node = Procdesc.get_exit_node proc_desc in
     Procdesc.iter_nodes
       (fun node ->
-        if has_noreturn_call node then
-          let exit_node = Procdesc.get_exit_node proc_desc in
-          Procdesc.set_succs node ~normal:(Some [exit_node]) ~exn:None )
+        if has_noreturn_call tenv node then
+          Procdesc.set_succs node ~normal:(Some [exit_node]) ~exn:None
+        else if has_throw_call node then
+          let catch_nodes = get_all_reachable_catch_nodes node in
+          let catch_or_exit_nodes =
+            if List.is_empty catch_nodes then (* throw with no catch *)
+              [exit_node] else catch_nodes
+          in
+          Procdesc.set_succs node ~normal:(Some catch_or_exit_nodes) ~exn:None )
       proc_desc
 end
 
@@ -345,5 +382,5 @@ let do_preanalysis exe_env pdesc =
     FunctionPointerSubstitution.process summary tenv ;
   Liveness.process summary tenv ;
   AddAbstractionInstructions.process pdesc ;
-  NoReturn.process pdesc ;
+  NoReturn.process tenv pdesc ;
   ()

infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp

@@ -19,6 +19,11 @@ namespace dead_stores {
 
 void easy_bad() { int x = 5; }
 
+void throw_bad() {
+  int i = 20;
+  throw 1;
+}
+
 void reassign_param_bad(int x) { x = 5; }
 
 int dead_then_live_bad() {
@@ -432,9 +437,8 @@ class Exceptions {
     return 0;
   }
 
-  // currently, the only transition to the catch block is at the end of the try
-  // block
-  int FP_read_in_catch_tricky_ok(bool b1, bool b2) {
+  // the transition to the catch block is set at pre-analysis
+  int read_in_catch_tricky_ok(bool b1, bool b2) {
     int i = 1;
     try {
       if (b1) {
@@ -450,6 +454,42 @@ class Exceptions {
     return 0;
   }
 
+  int read_in_loop_tricky_ok(bool b) {
+    int i = 1;
+    for (int p = 0; p <= 5; p++) {
+      try {
+        if (b) {
+          throw std::runtime_error("error");
+        }
+      } catch (...) {
+        return i;
+      }
+    }
+
+    return 0;
+  }
+
+  void read_in_goto_ok(bool b) {
+    int i = 1;
+    try {
+      if (b) {
+        throw std::runtime_error("error");
+
+        goto A;
+      } else {
+
+        goto B;
+      }
+    A:
+      goto B;
+    B:
+      goto A;
+    }
+
+    catch (...) {
+      return i;
+    }
+  }
   int return_in_try1_ok() {
     bool b;
 

infer/tests/codetoanalyze/cpp/liveness/issues.exp

@@ -1,4 +1,3 @@
-codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::Exceptions::FP_read_in_catch_tricky_ok, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::Exceptions::dead_in_catch_bad, 4, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::Exceptions::unreachable_catch_bad, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::FP_assign_array_tricky2_ok, 3, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
@@ -12,11 +11,12 @@ codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::easy_bad, 0, DEAD_STORE
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::init_capture_no_call_bad, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::init_capture_reassign_bad, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::init_in_binop_bad, 0, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
-codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::lambda_bad::lambda_dead_stores.cpp:145:11::operator(), 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
+codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::lambda_bad::lambda_dead_stores.cpp:150:11::operator(), 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::plus_plus1_bad, 2, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::plus_plus2_bad, 2, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::plus_plus3_bad, 2, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::reassign_param_bad, 0, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
+codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::throw_bad, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::unused_blacklisted_clone_bad, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::unused_blacklisted_constructed_bad, 0, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
 codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::unused_blacklisted_unique_ptr_bad, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]