From cec8cbeff2535a97625b0fc756340813f930edb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 1 Apr 2020 12:56:13 -0700 Subject: [PATCH] [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 | 16 ++++++ infer/src/backend/preanal.ml | 51 ++++++++++++++++--- .../cpp/liveness/dead_stores.cpp | 46 +++++++++++++++-- .../codetoanalyze/cpp/liveness/issues.exp | 4 +- 4 files changed, 105 insertions(+), 12 deletions(-) create mode 100644 infer/src/backend/NoReturnModels.ml diff --git a/infer/src/backend/NoReturnModels.ml b/infer/src/backend/NoReturnModels.ml new file mode 100644 index 000000000..a7b2ed920 --- /dev/null +++ b/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 ] diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 767bc1733..2817113a2 100644 --- a/infer/src/backend/preanal.ml +++ b/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 ; () diff --git a/infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp b/infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp index b0a34bc99..cd074b393 100644 --- a/infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp +++ b/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; diff --git a/infer/tests/codetoanalyze/cpp/liveness/issues.exp b/infer/tests/codetoanalyze/cpp/liveness/issues.exp index 76a18a95a..8e92340b3 100644 --- a/infer/tests/codetoanalyze/cpp/liveness/issues.exp +++ 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]