From d79bd90b819ce10fd435468d96eaae613e5a6cb1 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 21 Nov 2019 08:16:49 -0800 Subject: [PATCH] [pdesc] new pre-analysis to diverge after "noreturn" function calls Summary: A plugin update allows infer to know when a function doesn't return according to its attributes. This propagates this info all the way to the attributes of each function, and then use this information in a new pre-analysis that cuts the links to successor nodes of each `Call` instruction to a function that does not return. NOTE: The "no_return" `CallFlag.t` was dead code, following diffs deal with that (by removing it). Reviewed By: dulmarod Differential Revision: D18573922 fbshipit-source-id: 85ec64eca --- infer/src/IR/ProcAttributes.ml | 10 ++++--- infer/src/IR/ProcAttributes.mli | 1 + infer/src/backend/preanal.ml | 27 +++++++++++++++++++ infer/src/clang/CMethodProperties.ml | 8 ++++++ infer/src/clang/CMethodProperties.mli | 2 ++ infer/src/clang/CType_decl.ml | 2 ++ infer/src/clang/cMethodSignature.ml | 6 +++-- infer/src/clang/cMethodSignature.mli | 2 ++ infer/src/clang/cMethod_trans.ml | 1 + .../codetoanalyze/c/bufferoverrun/issues.exp | 2 -- .../c/bufferoverrun/unreachable.c | 2 +- .../null_pointer_dereference.c | 10 +++++++ .../tests/codetoanalyze/cpp/uninit/issues.exp | 1 - .../tests/codetoanalyze/cpp/uninit/uninit.cpp | 2 +- 14 files changed, 66 insertions(+), 10 deletions(-) diff --git a/infer/src/IR/ProcAttributes.ml b/infer/src/IR/ProcAttributes.ml index ca79cb2ca..a294d2377 100644 --- a/infer/src/IR/ProcAttributes.ml +++ b/infer/src/IR/ProcAttributes.ml @@ -50,6 +50,7 @@ type t = ; is_defined: bool (** true if the procedure is defined, and not just declared *) ; is_cpp_noexcept_method: bool (** the procedure is an C++ method annotated with "noexcept" *) ; is_java_synchronized_method: bool (** the procedure is a Java synchronized method *) + ; is_no_return: bool (** the procedure is known not to return *) ; is_specialized: bool (** the procedure is a clone specialized for dynamic dispatch handling *) ; is_synthetic_method: bool (** the procedure is a synthetic method *) ; is_variadic: bool (** the procedure is variadic, only supported for Clang procedures *) @@ -74,8 +75,9 @@ let default translation_unit proc_name = ; is_biabduction_model= false ; is_bridge_method= false ; is_cpp_noexcept_method= false - ; is_java_synchronized_method= false ; is_defined= false + ; is_java_synchronized_method= false + ; is_no_return= false ; is_specialized= false ; is_synthetic_method= false ; is_variadic= false @@ -107,6 +109,7 @@ let pp f ; is_defined ; is_cpp_noexcept_method ; is_java_synchronized_method + ; is_no_return ; is_specialized ; is_synthetic_method ; is_variadic @@ -145,13 +148,14 @@ let pp f (Pp.semicolon_seq ~print_env:Pp.text_break PredSymb.pp_func_attribute) func_attributes ; pp_bool_default ~default:default.is_abstract "is_abstract" is_abstract f () ; + pp_bool_default ~default:default.is_biabduction_model "is_model" is_biabduction_model f () ; pp_bool_default ~default:default.is_bridge_method "is_bridge_method" is_bridge_method f () ; - pp_bool_default ~default:default.is_defined "is_defined" is_defined f () ; pp_bool_default ~default:default.is_cpp_noexcept_method "is_cpp_noexcept_method" is_cpp_noexcept_method f () ; + pp_bool_default ~default:default.is_defined "is_defined" is_defined f () ; pp_bool_default ~default:default.is_java_synchronized_method "is_java_synchronized_method" is_java_synchronized_method f () ; - pp_bool_default ~default:default.is_biabduction_model "is_model" is_biabduction_model f () ; + pp_bool_default ~default:default.is_no_return "is_no_return" is_no_return f () ; pp_bool_default ~default:default.is_specialized "is_specialized" is_specialized f () ; pp_bool_default ~default:default.is_synthetic_method "is_synthetic_method" is_synthetic_method f () ; diff --git a/infer/src/IR/ProcAttributes.mli b/infer/src/IR/ProcAttributes.mli index c310c7b3f..df64623e7 100644 --- a/infer/src/IR/ProcAttributes.mli +++ b/infer/src/IR/ProcAttributes.mli @@ -33,6 +33,7 @@ type t = ; is_defined: bool (** true if the procedure is defined, and not just declared *) ; is_cpp_noexcept_method: bool (** the procedure is an C++ method annotated with "noexcept" *) ; is_java_synchronized_method: bool (** the procedure is a Java synchronized method *) + ; is_no_return: bool (** the procedure is known not to return *) ; is_specialized: bool (** the procedure is a clone specialized for dynamic dispatch handling *) ; is_synthetic_method: bool (** the procedure is a synthetic method *) ; is_variadic: bool (** the procedure is variadic, only supported for Clang procedures *) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index b38cc1822..5a05ef0d2 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -210,6 +210,32 @@ module FunctionPointerSubstitution = struct if updated then Attributes.store ~proc_desc:(Some pdesc) (Procdesc.get_attributes pdesc) 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 = + Procdesc.Node.get_instrs node + |> Instrs.exists ~f:(fun (instr : Sil.instr) -> + match instr with + | Call (_, _, _, _, {cf_noreturn= true}) -> + true + | Call (_, Const (Cfun proc_name), _, _, _) -> ( + match Attributes.load proc_name with + | Some {ProcAttributes.is_no_return= true} -> + true + | _ -> + false ) + | _ -> + false ) + + + let process proc_desc = + Procdesc.iter_nodes + (fun node -> + if has_noreturn_call node then Procdesc.set_succs node ~normal:(Some []) ~exn:None ) + proc_desc +end + let do_preanalysis exe_env pdesc = let summary = Summary.OnDisk.reset pdesc in let tenv = Exe_env.get_tenv exe_env (Procdesc.get_proc_name pdesc) in @@ -219,4 +245,5 @@ let do_preanalysis exe_env pdesc = then FunctionPointerSubstitution.process summary tenv ; Liveness.process summary tenv ; AddAbstractionInstructions.process pdesc ; + NoReturn.process pdesc ; () diff --git a/infer/src/clang/CMethodProperties.ml b/infer/src/clang/CMethodProperties.ml index dcfa3dce5..48076904a 100644 --- a/infer/src/clang/CMethodProperties.ml +++ b/infer/src/clang/CMethodProperties.ml @@ -147,6 +147,14 @@ let is_objc_method method_decl = match method_decl with Clang_ast_t.ObjCMethodDecl _ -> true | _ -> false +let is_no_return method_decl = + match Clang_ast_proj.get_function_decl_tuple method_decl with + | Some (_, _, _, {Clang_ast_t.fdi_is_no_return= true}) -> + true + | _ -> + false + + let is_variadic method_decl = let open Clang_ast_t in match method_decl with diff --git a/infer/src/clang/CMethodProperties.mli b/infer/src/clang/CMethodProperties.mli index b9fc8a7ed..1a5a8371b 100644 --- a/infer/src/clang/CMethodProperties.mli +++ b/infer/src/clang/CMethodProperties.mli @@ -30,6 +30,8 @@ val get_pointer_to_property : Clang_ast_t.decl -> Clang_ast_t.pointer option val is_objc_method : Clang_ast_t.decl -> bool +val is_no_return : Clang_ast_t.decl -> bool + val is_variadic : Clang_ast_t.decl -> bool val get_block_captured_variables : Clang_ast_t.decl -> Clang_ast_t.block_captured_variable list diff --git a/infer/src/clang/CType_decl.ml b/infer/src/clang/CType_decl.ml index 3348e0e08..b4929e31a 100644 --- a/infer/src/clang/CType_decl.ml +++ b/infer/src/clang/CType_decl.ml @@ -165,6 +165,7 @@ module BuildMethodSignature = struct let attributes = decl_info.Clang_ast_t.di_attributes in let is_cpp_virtual = CMethodProperties.is_cpp_virtual method_decl in let is_cpp_nothrow = CMethodProperties.is_cpp_nothrow method_decl in + let is_no_return = CMethodProperties.is_no_return method_decl in let is_variadic = CMethodProperties.is_variadic method_decl in let access = decl_info.Clang_ast_t.di_access in let pointer_to_property_opt = CMethodProperties.get_pointer_to_property method_decl in @@ -179,6 +180,7 @@ module BuildMethodSignature = struct ; method_kind ; is_cpp_virtual ; is_cpp_nothrow + ; is_no_return ; is_variadic ; pointer_to_parent ; pointer_to_property_opt diff --git a/infer/src/clang/cMethodSignature.ml b/infer/src/clang/cMethodSignature.ml index 1b43b6158..54ee6e0d2 100644 --- a/infer/src/clang/cMethodSignature.ml +++ b/infer/src/clang/cMethodSignature.ml @@ -30,6 +30,7 @@ type t = ; method_kind: ClangMethodKind.t ; is_cpp_virtual: bool ; is_cpp_nothrow: bool + ; is_no_return: bool ; is_variadic: bool ; pointer_to_parent: Clang_ast_t.pointer option ; pointer_to_property_opt: Clang_ast_t.pointer option @@ -49,8 +50,8 @@ let is_setter {pointer_to_property_opt; params} = let mk name class_param params ret_type ?(has_added_return_param = false) attributes loc method_kind - ?(is_cpp_virtual = false) ?(is_cpp_nothrow = false) ?(is_variadic = false) pointer_to_parent - pointer_to_property_opt return_param_typ access = + ?(is_cpp_virtual = false) ?(is_cpp_nothrow = false) ?(is_no_return = false) + ?(is_variadic = false) pointer_to_parent pointer_to_property_opt return_param_typ access = { name ; access ; class_param @@ -62,6 +63,7 @@ let mk name class_param params ret_type ?(has_added_return_param = false) attrib ; method_kind ; is_cpp_virtual ; is_cpp_nothrow + ; is_no_return ; is_variadic ; pointer_to_parent ; pointer_to_property_opt diff --git a/infer/src/clang/cMethodSignature.mli b/infer/src/clang/cMethodSignature.mli index c473c8fb4..3e6fb8833 100644 --- a/infer/src/clang/cMethodSignature.mli +++ b/infer/src/clang/cMethodSignature.mli @@ -24,6 +24,7 @@ type t = ; method_kind: ClangMethodKind.t ; is_cpp_virtual: bool ; is_cpp_nothrow: bool + ; is_no_return: bool ; is_variadic: bool ; pointer_to_parent: Clang_ast_t.pointer option ; pointer_to_property_opt: Clang_ast_t.pointer option @@ -45,6 +46,7 @@ val mk : -> ClangMethodKind.t -> ?is_cpp_virtual:bool -> ?is_cpp_nothrow:bool + -> ?is_no_return:bool -> ?is_variadic:bool -> Clang_ast_t.pointer option -> Clang_ast_t.pointer option diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 0c6ede171..0e57634d6 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -257,6 +257,7 @@ let create_local_procdesc ?(set_objc_accessor_attr = false) trans_unit_ctx cfg t ; is_defined= defined ; is_cpp_noexcept_method= is_cpp_nothrow ; is_biabduction_model= Config.biabduction_models_mode + ; is_no_return= ms.CMethodSignature.is_no_return ; is_variadic= ms.CMethodSignature.is_variadic ; loc= loc_start ; clang_method_kind diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 230af7a0d..6e70e3304 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -184,7 +184,6 @@ codetoanalyze/c/bufferoverrun/minmax.c, call_exact_minmax_sym_Bad, 3, BUFFER_OVE codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `x`,Call,Assignment,Assignment,Assignment,Assignment,,Array declaration,Array access: Offset: [-19+min(0, x), -1] Size: 1] codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here] codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 255] Size: 255] codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 256] Size: 256] codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [-1, 255] Size: 10000] @@ -306,7 +305,6 @@ codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_bad, 1, CONDI codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_with_else_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/unreachable.c, infinite_loop_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/unreachable.c, never_loops_bad, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/unreachable.c, unreachable_statement_exit_bad, 1, UNREACHABLE_CODE, no_bucket, ERROR, [Here] codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times2_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,,Assignment,,Array declaration,Array access: Offset: [0, 4] Size: 1 by call to `do_two_times2_Good` ] codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: [0, 4] Size: 1 by call to `do_two_times_Good` ] codetoanalyze/c/bufferoverrun/while_loop.c, diverge_on_narrowing, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c b/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c index 4b9e52c6b..922a16bfe 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c @@ -136,7 +136,7 @@ void FN_unreachable_statement_call_bad() { nop(); } -void unreachable_statement_exit_bad() { +void FN_unreachable_statement_exit_bad() { exit(2); nop(); } diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c b/infer/tests/codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c index 9025d5dd9..022bd0140 100644 --- a/infer/tests/codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c +++ b/infer/tests/codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c @@ -135,3 +135,13 @@ void sizeof_expr_ok(void) { } free(p); } + +void __attribute__((noreturn)) will_not_return(); + +void unreachable_null_ok() { + int* p = NULL; + if (p == NULL) { + will_not_return(); + } + *p = 42; +} diff --git a/infer/tests/codetoanalyze/cpp/uninit/issues.exp b/infer/tests/codetoanalyze/cpp/uninit/issues.exp index 129496cd4..c0064d525 100644 --- a/infer/tests/codetoanalyze/cpp/uninit/issues.exp +++ b/infer/tests/codetoanalyze/cpp/uninit/issues.exp @@ -10,7 +10,6 @@ codetoanalyze/cpp/uninit/members.cpp, access_pointer_members_bad, 5, UNINITIALIZ codetoanalyze/cpp/uninit/struct.cpp, pass_basic_type_field_bad, 3, UNINITIALIZED_VALUE, no_bucket, ERROR, [] codetoanalyze/cpp/uninit/struct.cpp, struct_partial_init_bad, 6, UNINITIALIZED_VALUE, no_bucket, ERROR, [] codetoanalyze/cpp/uninit/struct.cpp, struct_uninit_bad, 3, UNINITIALIZED_VALUE, no_bucket, ERROR, [] -codetoanalyze/cpp/uninit/uninit.cpp, FP_no_warning_noreturn_callee_ok, 7, UNINITIALIZED_VALUE, no_bucket, ERROR, [] codetoanalyze/cpp/uninit/uninit.cpp, FP_pointer_param_void_star_ok, 4, UNINITIALIZED_VALUE, no_bucket, ERROR, [] codetoanalyze/cpp/uninit/uninit.cpp, bad1, 2, UNINITIALIZED_VALUE, no_bucket, ERROR, [] codetoanalyze/cpp/uninit/uninit.cpp, bad2, 2, UNINITIALIZED_VALUE, no_bucket, ERROR, [] diff --git a/infer/tests/codetoanalyze/cpp/uninit/uninit.cpp b/infer/tests/codetoanalyze/cpp/uninit/uninit.cpp index a68b611bd..702e203de 100644 --- a/infer/tests/codetoanalyze/cpp/uninit/uninit.cpp +++ b/infer/tests/codetoanalyze/cpp/uninit/uninit.cpp @@ -257,7 +257,7 @@ int warning_when_throw_in_other_branch_bad(int t) { [[noreturn]] void noreturn_function() {} -int FP_no_warning_noreturn_callee_ok(bool t) { +int no_warning_noreturn_callee_ok(bool t) { int x; if (t) { x = 2;