[pulse] Give semantics of dispatch_sync in ObjC

Summary: This diff gives semantics of dispatch_sync to call the closure parameter.

Reviewed By: jvillard

Differential Revision: D25423175

fbshipit-source-id: a45309073

infer/src/pulse/PulseModels.ml

@@ -208,6 +208,24 @@ module ObjC = struct
     PulseOperations.add_dynamic_type dynamic_type ret_addr astate
     |> PulseArithmetic.and_positive ret_addr
     |> ok_continue
+
+
+  let dispatch_sync args : model =
+   fun {analyze_dependency; proc_desc; err_log} ~callee_procname:_ location ~ret astate ->
+    match List.last args with
+    | None ->
+        Ok [ExecutionDomain.ContinueProgram astate]
+    | Some {ProcnameDispatcher.Call.FuncArg.arg_payload= lambda_ptr_hist} -> (
+        let* astate, (lambda, _) =
+          PulseOperations.eval_access Read location lambda_ptr_hist Dereference astate
+        in
+        match AddressAttributes.get_closure_proc_name lambda astate with
+        | None ->
+            Ok [ExecutionDomain.ContinueProgram astate]
+        | Some callee_proc_name ->
+            PulseOperations.call ~caller_proc_desc:proc_desc err_log
+              ~callee_data:(analyze_dependency callee_proc_name)
+              location callee_proc_name ~ret ~actuals:[] ~formals_opt:None astate )
 end
 
 module Optional = struct
@@ -1248,6 +1266,7 @@ module ProcNameDispatcher = struct
           &:: "nextElement" <>$ capt_arg_payload
           $!--> fun x ->
           StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) )
+        ; -"dispatch_sync" &++> ObjC.dispatch_sync
         ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_create_or_copy
           &--> C.malloc_no_param
         ; +map_context_tenv PatternMatch.ObjectiveC.is_core_foundation_create_or_copy

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

@@ -4,7 +4,7 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  */
-#import <Foundation/NSObject.h>
+#import <Foundation/Foundation.h>
 
 @interface Uninit : NSObject
 @end
@@ -60,4 +60,23 @@
   block();
 }
 
+- (BOOL)dispatch_sync_closure_ok:(dispatch_queue_t)queue {
+  __block BOOL x;
+
+  dispatch_sync(queue, ^() {
+    x = true;
+  });
+  return x;
+}
+
+- (BOOL)dispatch_sync_variable_closure_ok:(dispatch_queue_t)queue {
+  __block BOOL x;
+
+  void (^block)() = ^() {
+    x = true;
+  };
+  dispatch_sync(queue, block);
+  return x;
+}
+
 @end