[pulse] Summary specialization of objc blocks

Summary:
This replaces previous specialisation of blocks with summary specialisation.

- Rather than passing a block variable in a Call expression in the frontend, we now introduce a builtin `__call_objc_block` to handle calling blocks and the specialisation, seems better than continue to overcomplicate the execution of calls in Pulse. Downside is that this builtin needs to be modelled in all checkers, in particular we are missing precision in the performance checkers because of this. Given they are not enabled, we can leave this to be done later if it will be needed again.
- We add a new type name where we can store the block procname to be put in the DynamicType attribute and retrieve it again after.
- The tests mostly are ok. The main problem seems to be that we don't execute correctly when there is aliasing when calling a method that executes a parameter block. This can happen often when then we need to pass self to that method, and the block itself also captures self. We may need to look into combining dynamic type specialisation and alias specialisation in the future.

Reviewed By: davidpichardie

Differential Revision: D52960209

fbshipit-source-id: b0702846f641b649cbc7fb3757604f1a502fa346

infer/src/IR/BuiltinDecl.ml

@@ -74,6 +74,8 @@ let __builtin_offsetof = create_procname "__builtin_offsetof"
 
 let __cast = create_procname "__cast"
 
+let __call_objc_block = create_procname "__call_objc_block"
+
 let __cxx_typeid = create_procname "__cxx_typeid"
 
 let __delete = create_procname "__delete"

infer/src/IR/BuiltinDecl.mli

@@ -94,6 +94,8 @@ val __c11_atomic_fetch_max : Procname.t
 
 val __c11_atomic_fetch_min : Procname.t
 
+val __call_objc_block : Procname.t
+
 val __opencl_atomic_fetch_max : Procname.t
 
 val __opencl_atomic_fetch_min : Procname.t

infer/src/backend/CCallSpecializedWithClosures.ml

@@ -12,7 +12,7 @@ let replace_with_specialize_methods instr =
   | Sil.Call (ret, Exp.Const (Const.Cfun callee_pname), actual_params, loc, flags) -> (
       let args =
         List.map actual_params ~f:(function
-          | Exp.Closure c, _ ->
+          | Exp.Closure c, _ when not (Procname.is_objc_block c.Exp.name) ->
               let captured =
                 List.map c.captured_vars ~f:(fun (_, pvar, typ, capture_mode) ->
                     CapturedVar.{pvar; typ; capture_mode} )

infer/src/clang/cTrans.ml

@@ -281,7 +281,17 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
       if is_inherited_ctor then get_forwarded_params trans_state sil_loc else ([], [])
     in
     let call_instr =
-      Sil.Call (ret_id', function_sil, params @ forwarded_params, sil_loc, call_flags)
+      match function_sil with
+      | Exp.Var _ when call_flags.CallFlags.cf_is_objc_block ->
+          let block_param = (function_sil, Typ.mk Typ.Tfun) in
+          Sil.Call
+            ( ret_id'
+            , Exp.Const (Const.Cfun BuiltinDecl.__call_objc_block)
+            , block_param :: (params @ forwarded_params)
+            , sil_loc
+            , call_flags )
+      | _ ->
+          Sil.Call (ret_id', function_sil, params @ forwarded_params, sil_loc, call_flags)
     in
     mk_trans_result ret_exps
       {empty_control with instrs= forwarded_init_instrs @ [call_instr]; initd_exps}

infer/src/pulse/Pulse.ml

@@ -202,7 +202,7 @@ module PulseTransferFunctions = struct
 
   let interprocedural_call
       ({InterproceduralAnalysis.analyze_dependency; tenv; proc_desc} as analysis_data) path ret
-      callee_pname call_exp func_args call_loc (flags : CallFlags.t) astate non_disj =
+      callee_pname call_exp func_args call_loc astate non_disj =
     let actuals =
       List.map func_args ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} ->
           (ValueOrigin.addr_hist arg_payload, typ) )
@@ -261,34 +261,20 @@ module PulseTransferFunctions = struct
         , non_disj
         , is_known_call )
     | _ ->
-        (* dereference call expression to catch nil issues *)
         ( (let<**> astate, _ =
-             if flags.cf_is_objc_block then
-               (* We are on an unknown block call, meaning that the block was defined
-                  outside the current function and was either passed by the caller
-                  as an argument or retrieved from an object. We do not handle blocks
-                  inside objects yet so we assume we are in the former case. In this
-                  case, we tell the caller that we are missing some information by
-                  setting [need_closure_specialization] in the resulting state and the caller
-                  will then try to specialize the current function with its available
-                  information. *)
-               let astate = AbductiveDomain.set_need_closure_specialization astate in
-               PulseOperations.eval_deref path ~must_be_valid_reason:BlockCall call_loc call_exp
-                 astate
-             else
-               let astate =
-                 if
-                   (* this condition may need refining to check that the function comes
-                      from the function's parameters or captured variables.
-                      The function_pointer_specialization option is there to compensate
-                      this / control the specialization's agressivity *)
-                   Config.function_pointer_specialization
-                   && Language.equal Language.Clang
-                        (Procname.get_language (Procdesc.get_proc_name proc_desc))
-                 then AbductiveDomain.set_need_closure_specialization astate
-                 else astate
-               in
-               PulseOperations.eval_deref path call_loc call_exp astate
+             let astate =
+               if
+                 (* this condition may need refining to check that the function comes
+                    from the function's parameters or captured variables.
+                    The function_pointer_specialization option is there to compensate
+                    this / control the specialization's agressivity *)
+                 Config.function_pointer_specialization
+                 && Language.equal Language.Clang
+                      (Procname.get_language (Procdesc.get_proc_name proc_desc))
+               then AbductiveDomain.set_need_closure_specialization astate
+               else astate
+             in
+             PulseOperations.eval_deref path call_loc call_exp astate
            in
            L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ;
            let astate =
@@ -972,7 +958,7 @@ module PulseTransferFunctions = struct
           PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
           let r =
             interprocedural_call analysis_data path ret callee_pname call_exp func_args call_loc
-              flags astate non_disj
+              astate non_disj
           in
           PerfEvent.(log (fun logger -> log_end_event logger ())) ;
           r

infer/src/pulse/PulseCallOperations.ml

@@ -205,7 +205,8 @@ let unknown_call tenv ({PathContext.timestamp} as path) call_loc (reason : CallE
 
 
 let apply_callee tenv ({PathContext.timestamp} as path) ~caller_proc_desc callee_pname call_loc
-    callee_exec_state ~ret ~captured_formals ~captured_actuals ~formals ~actuals astate =
+    callee_exec_state ~ret ~captured_formals ~captured_actuals ~formals ~actuals ?call_flags astate
+    =
   let open ExecutionDomain in
   let copy_to_caller_return_variable astate return_val_opt =
     (* Copies the return value of the callee into the return register of the caller.
@@ -249,6 +250,15 @@ let apply_callee tenv ({PathContext.timestamp} as path) ~caller_proc_desc callee
         calee_summary
       else callee_summary
     in
+    (* In order to apply summary specialisation, we call blocks with the closure as the first argument,
+       but when we want to call the actual code of the block, we need to remove the closure argument again. *)
+    let actuals =
+      match call_flags with
+      | Some call_flags when call_flags.CallFlags.cf_is_objc_block -> (
+        match actuals with _ :: rest -> rest | [] -> [] )
+      | _ ->
+          actuals
+    in
     let sat_unsat, contradiction =
       PulseInterproc.apply_summary path callee_pname call_loc ~callee_summary ~captured_formals
         ~captured_actuals ~formals
@@ -392,7 +402,7 @@ let apply_callee tenv ({PathContext.timestamp} as path) ~caller_proc_desc callee
 
 let call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals call_kind
     (callee_proc_attrs : ProcAttributes.t) exec_states_callee non_disj_callee
-    (astate_caller : AbductiveDomain.t) non_disj_caller =
+    (astate_caller : AbductiveDomain.t) ?call_flags non_disj_caller =
   let formals =
     List.map callee_proc_attrs.formals ~f:(fun (mangled, typ, _) ->
         (Pvar.mk mangled callee_pname |> Var.of_pvar, typ) )
@@ -429,7 +439,7 @@ let call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals call_k
           Timer.check_timeout () ;
           match
             apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_state
-              ~captured_formals ~captured_actuals ~formals ~actuals ~ret astate
+              ~captured_formals ~captured_actuals ~formals ~actuals ~ret ?call_flags astate
           with
           | Unsat, new_contradiction ->
               (* couldn't apply pre/post pair *)
@@ -441,7 +451,7 @@ let call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals call_k
 
 
 let call_aux_unknown tenv path ~caller_proc_desc call_loc callee_pname ~ret ~actuals ~formals_opt
-    ~call_kind (astate : AbductiveDomain.t) non_disj_caller =
+    ~call_kind (astate : AbductiveDomain.t) ?call_flags non_disj_caller =
   let arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in
   let ( let<**> ) = bind_sat_result (non_disj_caller, None) in
   let<**> astate_unknown =
@@ -471,7 +481,8 @@ let call_aux_unknown tenv path ~caller_proc_desc call_loc callee_pname ~ret ~act
              ~default:([], (NonDisjDomain.bottom, None))
              ~f:(fun nil_summary ->
                call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals call_kind
-                 proc_attrs [nil_summary] NonDisjDomain.Summary.bottom astate non_disj_caller )
+                 proc_attrs [nil_summary] NonDisjDomain.Summary.bottom astate ?call_flags
+                 non_disj_caller )
       in
       ( result_unknown @ result_unknown_nil
       , (NonDisjDomain.join non_disj non_disj_nil, contradiction) )
@@ -564,7 +575,7 @@ let maybe_dynamic_type_specialization_is_needed specialization contradiction ast
 let call tenv path ~caller_proc_desc
     ~(analyze_dependency : ?specialization:Specialization.t -> Procname.t -> PulseSummary.t option)
     call_loc callee_pname ~ret ~actuals ~formals_opt ~call_kind (astate : AbductiveDomain.t)
-    non_disj_caller =
+    ?call_flags non_disj_caller =
   let has_continue_program results =
     let f one_result =
       match one_result with
@@ -578,7 +589,7 @@ let call tenv path ~caller_proc_desc
   let call_as_unknown () =
     let results, (non_disj, contradiction) =
       call_aux_unknown tenv path ~caller_proc_desc call_loc callee_pname ~ret ~actuals ~formals_opt
-        ~call_kind astate non_disj_caller
+        ~call_kind astate ?call_flags non_disj_caller
     in
     if Option.is_some contradiction then (
       L.debug Analysis Verbose
@@ -593,7 +604,7 @@ let call tenv path ~caller_proc_desc
     let results, (non_disj, contradiction) =
       call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals call_kind
         (IRAttributes.load_exn callee_pname)
-        exec_states non_disj_callee astate non_disj_caller
+        exec_states non_disj_callee astate ?call_flags non_disj_caller
     in
     (* When a function call does not have a post of type ContinueProgram, we may want to treat
        the call as unknown to make the analysis continue. This may introduce false positives but
@@ -711,6 +722,6 @@ let call tenv path ~caller_proc_desc
       L.d_printfln_escaped "No spec found for %a@\n" Procname.pp callee_pname ;
       let res, (non_disj, contradiction) =
         call_aux_unknown tenv path ~caller_proc_desc call_loc callee_pname ~ret ~actuals
-          ~formals_opt ~call_kind astate non_disj_caller
+          ~formals_opt ~call_kind astate ?call_flags non_disj_caller
       in
       (res, non_disj, contradiction, `UnknownCall)

infer/src/pulse/PulseCallOperations.mli

@@ -21,6 +21,7 @@ val call :
   -> formals_opt:(Pvar.t * Typ.t) list option
   -> call_kind:PulseOperations.call_kind
   -> AbductiveDomain.t
+  -> ?call_flags:CallFlags.t
   -> NonDisjDomain.t
   -> ExecutionDomain.t AccessResult.t list
      * NonDisjDomain.t

infer/src/pulse/PulseModelsObjC.ml

@@ -12,6 +12,7 @@ open PulseDomainInterface
 open PulseOperationResult.Import
 open PulseModelsImport
 module GenericArrayBackedCollection = PulseModelsGenericArrayBackedCollection
+module FuncArg = ProcnameDispatcher.Call.FuncArg
 
 module CoreFoundation = struct
   let cf_bridging_release access : model_no_non_disj =
@@ -258,6 +259,52 @@ let check_arg_not_nil (value, value_hist) ~desc : model_no_non_disj =
   PulseOperations.write_id ret_id (ret_val, Hist.single_call path location desc) astate
 
 
+let call_objc_block FuncArg.{arg_payload= block_ptr_hist; typ} actuals : model =
+ fun {path; analysis_data= {analyze_dependency; tenv; proc_desc}; location; ret= (ret_id, _) as ret}
+     astate non_disj ->
+  let block = fst block_ptr_hist in
+  let callee_proc_name_opt =
+    match AddressAttributes.get_dynamic_type block astate with
+    | Some {typ= {desc= Typ.Tstruct (ObjcBlock bsig)}} ->
+        Some (Procname.Block bsig)
+    | _ ->
+        None
+  in
+  match callee_proc_name_opt with
+  | Some callee_proc_name ->
+      let actuals =
+        (block_ptr_hist, typ)
+        :: List.map actuals ~f:(fun FuncArg.{arg_payload; typ} -> (arg_payload, typ))
+      in
+      let astate, non_disj, _, _ =
+        PulseCallOperations.call tenv path ~caller_proc_desc:proc_desc ~analyze_dependency location
+          callee_proc_name ~ret ~actuals ~formals_opt:None ~call_kind:`ResolvedProcname astate
+          ~call_flags:{CallFlags.default with cf_is_objc_block= true}
+          non_disj
+      in
+      (astate, non_disj)
+  | _ ->
+      (* we don't know what procname this block resolves to *)
+      let res =
+        (* dereference call expression to catch nil issues *)
+        let<+> astate, _ =
+          PulseOperations.eval_access path Read location ~must_be_valid_reason:BlockCall
+            block_ptr_hist Dereference astate
+        in
+        let desc = Procname.to_string BuiltinDecl.__call_objc_block in
+        let hist = Hist.single_event path (Hist.call_event path location desc) in
+        let astate = PulseOperations.havoc_id ret_id hist astate in
+        let astate = AbductiveDomain.add_need_dynamic_type_specialization block astate in
+        let astate =
+          let unknown_effect = Attribute.UnknownEffect (Model desc, hist) in
+          List.fold actuals ~init:astate ~f:(fun acc FuncArg.{arg_payload= actual, _} ->
+              AddressAttributes.add_one actual unknown_effect acc )
+        in
+        astate
+      in
+      (res, non_disj)
+
+
 let transfer_ownership_matchers : matcher list =
   let open ProcnameDispatcher.Call in
   let transfer_ownership_namespace_matchers =
@@ -296,7 +343,8 @@ let matchers : matcher list =
   let map_context_tenv f (x, _) = f x in
   ( [ -"dispatch_sync" <>$ any_arg $++$--> call
     ; +map_context_tenv (PatternMatch.ObjectiveC.implements "UITraitCollection")
-      &:: "performAsCurrentTraitCollection:" <>$ any_arg $++$--> call ]
+      &:: "performAsCurrentTraitCollection:" <>$ any_arg $++$--> call
+    ; +BuiltinDecl.(match_builtin __call_objc_block) $ capt_arg $++$--> call_objc_block ]
   |> List.map ~f:(ProcnameDispatcher.Call.contramap_arg_payload ~f:ValueOrigin.addr_hist) )
   @ ( [ +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_release
         <>$ capt_arg_payload $--> CoreFoundation.cf_bridging_release

infer/src/pulse/PulseOperations.ml

@@ -173,18 +173,23 @@ let rec eval (path : PathContext.t) mode location exp astate :
   (astate, ValueOrigin.addr_hist value_origin)
 
 
-and record_closure_cpp_lambda astate (path : PathContext.t) loc procname
+and record_closure astate (path : PathContext.t) loc procname
     (captured_vars : (Exp.t * Pvar.t * Typ.t * CapturedVar.capture_mode) list) =
   let assign_event = ValueHistory.Assignment (loc, path.timestamp) in
   let closure_addr_hist = (AbstractValue.mk_fresh (), ValueHistory.singleton assign_event) in
   let astate =
-    match Procname.get_class_type_name procname with
-    | Some typ_name ->
+    match (Procname.get_class_type_name procname, procname) with
+    | Some typ_name, _ when Procname.is_cpp_lambda procname ->
         let typ = Typ.mk (Typ.Tstruct typ_name) in
         AddressAttributes.add_one (fst closure_addr_hist)
           (Attribute.DynamicType {typ; source_file= None})
           astate
-    | None ->
+    | _, Procname.Block bsig ->
+        let typ = Typ.mk (Typ.Tstruct (Typ.ObjcBlock bsig)) in
+        AddressAttributes.add_one (fst closure_addr_hist)
+          (Attribute.DynamicType {typ; source_file= None})
+          astate
+    | _ ->
         astate
   in
   let** astate = PulseArithmetic.and_positive (fst closure_addr_hist) astate in
@@ -229,8 +234,8 @@ and eval_to_value_origin (path : PathContext.t) mode location exp astate :
         (ArrayAccess (StdTyp.void, fst addr_hist_index))
         astate
   | Closure {name; captured_vars} ->
-      if Procname.is_cpp_lambda name then
-        let++ astate, v_hist = record_closure_cpp_lambda astate path location name captured_vars in
+      if Procname.is_cpp_lambda name || Procname.is_objc_block name then
+        let++ astate, v_hist = record_closure astate path location name captured_vars in
         (astate, v_hist)
       else
         let** astate, rev_captured =
@@ -726,7 +731,8 @@ let remove_vars vars location astate =
   Stack.remove_vars vars astate
 
 
-let get_var_captured_actuals path location ~is_lambda ~captured_formals ~actual_closure astate =
+let get_var_captured_actuals path location ~is_lambda_or_block ~captured_formals ~actual_closure
+    astate =
   let+ _, astate, captured_actuals =
     PulseResult.list_fold captured_formals ~init:(0, astate, [])
       ~f:(fun (id, astate, captured) (var, capture_mode, typ) ->
@@ -738,7 +744,7 @@ let get_var_captured_actuals path location ~is_lambda ~captured_formals ~actual_
             in
             let field_name = Fieldname.mk_capture_field_in_closure var_name captured_data in
             let+ astate, captured_actual =
-              if is_lambda then
+              if is_lambda_or_block then
                 eval_deref_access path Read location actual_closure (FieldAccess field_name) astate
               else eval_access path Read location actual_closure (FieldAccess field_name) astate
             in
@@ -773,7 +779,7 @@ type call_kind =
   | `ResolvedProcname ]
 
 let get_captured_actuals procname path location ~captured_formals ~call_kind ~actuals astate =
-  let is_lambda = Procname.is_cpp_lambda procname in
+  let is_lambda_or_block = Procname.is_cpp_lambda procname || Procname.is_objc_block procname in
   if
     Procname.is_objc_block procname
     || Procname.is_specialized_with_function_parameters procname
@@ -784,9 +790,16 @@ let get_captured_actuals procname path location ~captured_formals ~call_kind ~ac
         get_closure_captured_actuals path location ~captured_actuals astate
     | `Var id ->
         let+* astate, actual_closure = eval path Read location (Exp.Var id) astate in
-        get_var_captured_actuals path location ~is_lambda ~captured_formals ~actual_closure astate
-    | `ResolvedProcname ->
-        Sat (Ok (astate, []))
+        get_var_captured_actuals path location ~is_lambda_or_block ~captured_formals ~actual_closure
+          astate
+    | `ResolvedProcname -> (
+      match actuals with
+      | (actual_closure, _) :: _ ->
+          Sat
+            (get_var_captured_actuals path location ~is_lambda_or_block ~captured_formals
+               ~actual_closure astate )
+      | [] ->
+          Sat (Ok (astate, [])) )
   else
     match actuals with
     | (actual_closure, _) :: _ when not (List.is_empty captured_formals) ->
@@ -795,8 +808,8 @@ let get_captured_actuals procname path location ~captured_formals ~call_kind ~ac
            let* astate, actual_closure =
              eval_access path Read location actual_closure Dereference astate
            in
-           get_var_captured_actuals path location ~is_lambda ~captured_formals ~actual_closure
-             astate )
+           get_var_captured_actuals path location ~is_lambda_or_block ~captured_formals
+             ~actual_closure astate )
     | _ ->
         Sat (Ok (astate, []))