[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

@@ -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
     () ;

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 *)

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 ;
   ()

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

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

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

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

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

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

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, [<Offset trace>,Parameter `x`,Call,Assignment,Assignment,Assignment,Assignment,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 255] Size: 255]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 256] Size: 256]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,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,<Offset trace>,Assignment,<Length trace>,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,<Offset trace>,Parameter `n`,<Length trace>,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]

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();
 }

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;
+}

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, []

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;