[pulse] Change to ExitProgram state when calling noreturn function

Summary:
Since D20736043 (d84fea52ae) is adding edges from the noreturn function node to exit node, analyzers should
handle the state differently to normal states.

Reviewed By: ezgicicek

Differential Revision: D25402576

fbshipit-source-id: a98e41b0c

infer/src/IR/Attributes.ml

@@ -66,6 +66,8 @@ let find =
 
 let load pname = find (Procname.to_unique_id pname)
 
+let is_no_return pname = match load pname with Some {is_no_return} -> is_no_return | _ -> false
+
 let store ~proc_desc (attr : ProcAttributes.t) =
   let pname = attr.proc_name in
   let akind = proc_kind_of_attr attr in

infer/src/IR/Attributes.mli

@@ -19,4 +19,6 @@ val store : proc_desc:Procdesc.t option -> ProcAttributes.t -> unit
 val load : Procname.t -> ProcAttributes.t option
 (** Load the attributes for the procedure from the attributes database. *)
 
+val is_no_return : Procname.t -> bool
+
 val pp_attributes_kind : Format.formatter -> attributes_kind -> unit

infer/src/backend/preanal.ml

@@ -443,12 +443,9 @@ module NoReturn = struct
     Procdesc.Node.get_instrs node
     |> Instrs.exists ~f:(fun (instr : Sil.instr) ->
            match instr with
-           | Call (_, Const (Cfun proc_name), _, _, _) -> (
+           | Call (_, Const (Cfun proc_name), _, _, _) ->
-             match Attributes.load proc_name with
+               Attributes.is_no_return proc_name
-             | Some {ProcAttributes.is_no_return= true} ->
+               || NoReturnModels.dispatch tenv proc_name |> Option.value ~default:false
-                 true
-             | _ ->
-                 NoReturnModels.dispatch tenv proc_name |> Option.value ~default:false )
            | _ ->
                false )
 

infer/src/pulse/Pulse.ml

@@ -9,6 +9,7 @@ open! IStd
 module F = Format
 module L = Logging
 open IResult.Let_syntax
+module IRAttributes = Attributes
 open PulseBasicInterface
 open PulseDomainInterface
 
@@ -147,8 +148,8 @@ module PulseTransferFunctions = struct
     AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate
 
 
-  let dispatch_call ({InterproceduralAnalysis.tenv} as analysis_data) ret call_exp actuals call_loc
+  let dispatch_call ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) ret call_exp
-      flags astate =
+      actuals call_loc flags astate =
     (* evaluate all actuals *)
     let* astate, rev_func_args =
       List.fold_result actuals ~init:(astate, [])
@@ -198,6 +199,7 @@ module PulseTransferFunctions = struct
             (* skip, as above for non-topl *) exec_state_res
       else exec_state_res
     in
+    let+ exec_state =
       match get_out_of_scope_object call_exp actuals flags with
       | Some pvar_typ ->
           L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ;
@@ -207,6 +209,10 @@ module PulseTransferFunctions = struct
           |> Result.all
       | None ->
           exec_state_res
+    in
+    if Option.exists callee_pname ~f:IRAttributes.is_no_return then
+      ExecutionDomain.force_exit_program proc_desc exec_state
+    else exec_state
 
 
   (* [get_dealloc_from_dynamic_types vars_types loc] returns a dealloc procname and vars and

infer/src/pulse/PulseExecutionDomain.ml

@@ -72,7 +72,7 @@ let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_st
 
 type summary = AbductiveDomain.summary base_t [@@deriving yojson_of]
 
-let summary_of_posts pdesc posts =
+let summary_of_posts_common ~continue_program pdesc posts =
   List.filter_mapi posts ~f:(fun i exec_state ->
       L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
       match exec_state with
@@ -81,7 +81,7 @@ let summary_of_posts pdesc posts =
         | Unsat ->
             None
         | Sat astate ->
-            Some (ContinueProgram astate) )
+            Some (continue_program astate) )
       (* already a summary but need to reconstruct the variants to make the type system happy *)
       | AbortProgram astate ->
           Some (AbortProgram astate)
@@ -89,3 +89,11 @@ let summary_of_posts pdesc posts =
           Some (ExitProgram astate)
       | LatentAbortProgram {astate; latent_issue} ->
           Some (LatentAbortProgram {astate; latent_issue}) )
+
+
+let summary_of_posts =
+  summary_of_posts_common ~continue_program:(fun astate -> ContinueProgram astate)
+
+
+let force_exit_program =
+  summary_of_posts_common ~continue_program:(fun astate -> ExitProgram astate)

infer/src/pulse/PulseExecutionDomain.mli

@@ -32,3 +32,5 @@ val is_unsat_cheap : t -> bool
 type summary = AbductiveDomain.summary base_t [@@deriving yojson_of]
 
 val summary_of_posts : Procdesc.t -> t list -> summary list
+
+val force_exit_program : Procdesc.t -> t list -> t list

infer/tests/codetoanalyze/c/pulse/nullptr.c

@@ -6,6 +6,7 @@
  */
 
 #include <stdlib.h>
+#include <stdnoreturn.h>
 
 int* malloc_no_check_bad() {
   int* p = (int*)malloc(sizeof(int));
@@ -77,3 +78,19 @@ void interproc_free_ok() {
   int* p = (int*)malloc(sizeof(int));
   wrap_free(p);
 }
+
+noreturn void no_return();
+
+void wrap_malloc(int** x) {
+  *x = (int*)malloc(sizeof(int));
+  if (!*x) {
+    no_return();
+  }
+}
+
+void call_no_return_good() {
+  int* x = NULL;
+  wrap_malloc(&x);
+  *x = 5;
+  free(x);
+}