[pulse][objc] Special case for calling objc dispatch methods

Summary: Objective-C dispatch methods are not specialized, but have a special case during symbolic execution in biabduction. Reuse the same approach for Pulse: retrieve the given block name and its arguments and call it.

Reviewed By: skcho

Differential Revision: D28550468

fbshipit-source-id: 5017bb71e

infer/src/pulse/Pulse.ml

@@ -129,6 +129,19 @@ module PulseTransferFunctions = struct
 
   let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) ret
       call_exp actuals call_loc flags astate =
+    let<*> astate, callee_pname = PulseOperations.eval_proc_name call_loc call_exp astate in
+    (* special case for objc dispatch models *)
+    let callee_pname, actuals =
+      match callee_pname with
+      | Some callee_pname when ObjCDispatchModels.is_model callee_pname -> (
+        match ObjCDispatchModels.get_dispatch_closure_opt actuals with
+        | Some (block_name, args) ->
+            (Some block_name, args)
+        | None ->
+            (Some callee_pname, actuals) )
+      | _ ->
+          (callee_pname, actuals)
+    in
     (* evaluate all actuals *)
     let<*> astate, rev_func_args =
       List.fold_result actuals ~init:(astate, [])
@@ -140,7 +153,6 @@ module PulseTransferFunctions = struct
             :: rev_func_args ) )
     in
     let func_args = List.rev rev_func_args in
-    let<*> astate, callee_pname = PulseOperations.eval_proc_name call_loc call_exp astate in
     let model =
       match callee_pname with
       | Some callee_pname ->

infer/tests/codetoanalyze/objc/pulse/NPEBlocks.m

@@ -19,8 +19,7 @@ void dispatch(MyBlock block) { block(); }
 
 @implementation Singleton
 
-// Common FP in Pulse NPEs, this requires block specialization
-- (int)dispatch_once_no_npe_good_FP {
+- (int)dispatch_once_no_npe_good {
   static Singleton* a = nil;
   static dispatch_once_t onceToken;
   dispatch_once(&onceToken, ^{
@@ -29,6 +28,17 @@ void dispatch(MyBlock block) { block(); }
   return a->_x;
 }
 
+- (int)dispatch_once_captured_vars_bad {
+  static dispatch_once_t onceToken;
+  int* x = NULL;
+  int val = 5;
+  __block int* y = &val;
+  dispatch_once(&onceToken, ^{
+    y = x;
+  });
+  return *y;
+}
+
 - (int)dispatch_no_npe_good {
   static Singleton* a = nil;
   static dispatch_once_t onceToken;

infer/tests/codetoanalyze/objc/pulse/issues.exp

@@ -7,8 +7,8 @@ codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.no_bridge_leak_bad, 2, MEMOR
 codetoanalyze/objc/pulse/MemoryLeaks.m, call_bridge_interproc_leak_ok_FP, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `CFLocaleCreate` here,memory becomes unreachable here]
 codetoanalyze/objc/pulse/MemoryLeaks.m, call_cfrelease_interproc_leak_ok_FP, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `CFLocaleCreate` here,memory becomes unreachable here]
 codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m, block_captured_var_leak_bad, 7, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc_no_fail` here,memory becomes unreachable here]
-codetoanalyze/objc/pulse/NPEBlocks.m, Singleton.dispatch_once_no_npe_good_FP, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
-codetoanalyze/objc/pulse/NPEBlocks.m, captured_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `objc_blockcaptured_npe_bad_3` here,parameter `x` of objc_blockcaptured_npe_bad_3,invalid access occurs here]
+codetoanalyze/objc/pulse/NPEBlocks.m, Singleton.dispatch_once_captured_vars_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,in call to `objc_blockSingleton.dispatch_once_captured_vars_bad_2`,parameter `x` of objc_blockSingleton.dispatch_once_captured_vars_bad_2,assigned,return from call to `objc_blockSingleton.dispatch_once_captured_vars_bad_2`,invalid access occurs here]
+codetoanalyze/objc/pulse/NPEBlocks.m, captured_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `objc_blockcaptured_npe_bad_4` here,parameter `x` of objc_blockcaptured_npe_bad_4,invalid access occurs here]
 codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.assignNilBad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramAssignNilBad:, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramReassignNilBad:, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,assigned,invalid access occurs here]