[pulse][objc][nullptr] A special case for objc nil messaging for unknown call

Summary: To support objc nil messaging for unknown function calls we prune `self` to be positive in the `normal` specification and add additional specification to handle nil case.

Reviewed By: skcho

Differential Revision: D27360757

fbshipit-source-id: 119999b30

infer/src/pulse/PulseCallOperations.ml

@@ -189,58 +189,86 @@ let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate)
   AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate
 
 
+let call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc exec_states
+    (astate : AbductiveDomain.t) =
+  let formals =
+    Procdesc.get_formals callee_proc_desc
+    |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
+  in
+  let captured_vars =
+    Procdesc.get_captured callee_proc_desc
+    |> List.map ~f:(fun {CapturedVar.name; capture_mode} ->
+           let pvar = Pvar.mk name callee_pname in
+           (Var.of_pvar pvar, capture_mode) )
+  in
+  let<*> astate, captured_vars_with_actuals =
+    match actuals with
+    | (actual_closure, _) :: _
+      when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) ->
+        (* Assumption: the first parameter will be a closure *)
+        PulseOperations.get_captured_actuals call_loc ~captured_vars ~actual_closure astate
+    | _ ->
+        Ok (astate, [])
+  in
+  let should_keep_at_most_one_disjunct =
+    Option.exists Config.pulse_cut_to_one_path_procedures_pattern ~f:(fun regex ->
+        Str.string_match regex (Procname.to_string callee_pname) 0 )
+  in
+  if should_keep_at_most_one_disjunct then
+    L.d_printfln "Will keep at most one disjunct because %a is in blacklist" Procname.pp
+      callee_pname ;
+  (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *)
+  List.fold ~init:[] exec_states ~f:(fun posts callee_exec_state ->
+      if should_keep_at_most_one_disjunct && not (List.is_empty posts) then posts
+      else
+        (* apply all pre/post specs *)
+        match
+          apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
+            ~captured_vars_with_actuals ~formals ~actuals ~ret astate
+        with
+        | Unsat ->
+            (* couldn't apply pre/post pair *)
+            posts
+        | Sat post ->
+            post :: posts )
+
+
 let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc
     callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) =
   let get_arg_values () = List.map actuals ~f:(fun ((value, _), _) -> value) in
+  (* a special case for objc nil messaging *)
+  let unknown_objc_nil_messaging astate_unknown procdesc =
+    let result_unknown =
+      let<+> astate_unknown =
+        PulseObjectiveCSummary.append_objc_actual_self_positive procdesc (List.hd actuals)
+          astate_unknown
+      in
+      astate_unknown
+    in
+    let result_unknown_nil =
+      PulseObjectiveCSummary.mk_objc_method_nil_summary tenv procdesc
+        (ExecutionDomain.mk_initial tenv procdesc)
+      |> Option.value_map ~default:[] ~f:(fun nil_summary ->
+             let<*> nil_astate = nil_summary in
+             call_aux tenv caller_proc_desc call_loc callee_pname ret actuals procdesc
+               ([ContinueProgram nil_astate] :> ExecutionDomain.t list)
+               astate )
+    in
+    result_unknown @ result_unknown_nil
+  in
   match callee_data with
   | Some (callee_proc_desc, exec_states) ->
-      let formals =
-        Procdesc.get_formals callee_proc_desc
-        |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
-      in
-      let captured_vars =
-        Procdesc.get_captured callee_proc_desc
-        |> List.map ~f:(fun {CapturedVar.name; capture_mode} ->
-               let pvar = Pvar.mk name callee_pname in
-               (Var.of_pvar pvar, capture_mode) )
-      in
-      let<*> astate, captured_vars_with_actuals =
-        match actuals with
-        | (actual_closure, _) :: _
-          when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) ->
-            (* Assumption: the first parameter will be a closure *)
-            PulseOperations.get_captured_actuals call_loc ~captured_vars ~actual_closure astate
-        | _ ->
-            Ok (astate, [])
-      in
-      let should_keep_at_most_one_disjunct =
-        Option.exists Config.pulse_cut_to_one_path_procedures_pattern ~f:(fun regex ->
-            Str.string_match regex (Procname.to_string callee_pname) 0 )
-      in
-      if should_keep_at_most_one_disjunct then
-        L.d_printfln "Will keep at most one disjunct because %a is in blacklist" Procname.pp
-          callee_pname ;
-      (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *)
-      List.fold ~init:[]
+      call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc
         (exec_states :> ExecutionDomain.t list)
-        ~f:(fun posts callee_exec_state ->
-          if should_keep_at_most_one_disjunct && not (List.is_empty posts) then posts
-          else
-            (* apply all pre/post specs *)
-            match
-              apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
-                ~captured_vars_with_actuals ~formals ~actuals ~ret astate
-            with
-            | Unsat ->
-                (* couldn't apply pre/post pair *)
-                posts
-            | Sat post ->
-                post :: posts )
+        astate
   | None ->
       (* no spec found for some reason (unknown function, ...) *)
       L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ;
-      let astate =
+      let astate_unknown =
         conservatively_initialize_args (get_arg_values ()) astate
         |> unknown_call tenv call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt
       in
-      [Ok (ContinueProgram astate)]
+      let callee_procdesc_opt = AnalysisCallbacks.get_proc_desc callee_pname in
+      Option.value_map callee_procdesc_opt
+        ~default:[Ok (ContinueProgram astate_unknown)]
+        ~f:(unknown_objc_nil_messaging astate_unknown)

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -56,7 +56,7 @@ let mk_objc_method_nil_summary_aux tenv proc_desc astate =
       PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:self_value astate
 
 
-let mk_objc_method_nil_summary {InterproceduralAnalysis.tenv; proc_desc; err_log} initial =
+let mk_objc_method_nil_summary tenv proc_desc initial =
   let proc_name = Procdesc.get_proc_name proc_desc in
   match (initial, proc_name) with
   | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod}
@@ -66,8 +66,7 @@ let mk_objc_method_nil_summary {InterproceduralAnalysis.tenv; proc_desc; err_log
          We create a nil summary to avoid reporting NPE in this case.
          However, there is an exception in the case where the return type is non-POD.
          In that case it's UB and we want to report an error. *)
-      let result = mk_objc_method_nil_summary_aux tenv proc_desc astate in
-      Some (PulseReport.report_result tenv proc_desc err_log result)
+      Some (mk_objc_method_nil_summary_aux tenv proc_desc astate)
   | ContinueProgram _, _
   | ExitProgram _, _
   | AbortProgram _, _
@@ -95,11 +94,20 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log}
       [astate]
 
 
-let update_objc_method_posts analysis_data ~initial_astate ~posts =
-  let nil_summary = mk_objc_method_nil_summary analysis_data initial_astate in
-  match nil_summary with
-  | None ->
-      posts
-  | Some nil_summary ->
-      let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in
-      nil_summary @ posts
+let append_objc_actual_self_positive procdesc self_actual astate =
+  let procname = Procdesc.get_proc_name procdesc in
+  match procname with
+  | Procname.ObjC_Cpp {kind= ObjCInstanceMethod} when Procdesc.is_ret_type_pod procdesc ->
+      Option.value_map self_actual ~default:(Ok astate) ~f:(fun ((self, _), _) ->
+          PulseArithmetic.prune_positive self astate )
+  | _ ->
+      Ok astate
+
+
+let update_objc_method_posts ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data)
+    ~initial_astate ~posts =
+  mk_objc_method_nil_summary tenv proc_desc initial_astate
+  |> Option.value_map ~default:posts ~f:(function result ->
+         let nil_summary = PulseReport.report_result tenv proc_desc err_log result in
+         let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in
+         nil_summary @ posts )

infer/src/pulse/PulseObjectiveCSummary.mli

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+open PulseBasicInterface
 open PulseDomainInterface
 
 val update_objc_method_posts :
@@ -15,3 +16,12 @@ val update_objc_method_posts :
   -> ExecutionDomain.t list
 (** For ObjC instance methods: adds path condition `self > 0` to given posts and appends additional
     nil summary. Does nothing to posts for other kinds of methods *)
+
+val append_objc_actual_self_positive :
+     Procdesc.t
+  -> ((AbstractValue.t * ValueHistory.t) * Typ.t) option
+  -> AbductiveDomain.t
+  -> AbductiveDomain.t AccessResult.t
+
+val mk_objc_method_nil_summary :
+  Tenv.t -> Procdesc.t -> ExecutionDomain.t -> AbductiveDomain.t AccessResult.t option

infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm

@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  */
 
-#import <Foundation/NSObject.h>
+#import <Foundation/Foundation.h>
 #include <memory>
 
 @interface SomeObject : NSObject
@@ -27,6 +27,8 @@
 
 - (SomeObject*)get;
 
++ (NSString*)returnsStringNil;
+
 @end
 
 @implementation SomeObject
@@ -56,6 +58,10 @@
   return o;
 }
 
++ (NSString*)returnsStringNil {
+  return nil;
+}
+
 @end
 
 int dereferenceNilBad() {
@@ -136,3 +142,11 @@ int testTraceBad() {
   int* ptr = [obj getXPtr];
   return *ptr;
 }
+
+void testUnknownNilSpecOk() {
+  NSString* const str = [SomeObject returnsStringNil];
+  if (str.length == 0) {
+    return;
+  };
+  NSDictionary* dict = @{@"helloString" : str};
+}