diff --git a/infer/src/IR/ObjCDispatchModels.ml b/infer/src/IR/ObjCDispatchModels.ml new file mode 100644 index 000000000..643d5fd76 --- /dev/null +++ b/infer/src/IR/ObjCDispatchModels.ml @@ -0,0 +1,29 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) +open! IStd + +let dispatch_models = + [ "_dispatch_once" + ; "dispatch_async" + ; "dispatch_after" + ; "dispatch_group_async" + ; "dispatch_barrier_async" + ; "dispatch_group_notify" ] + + +let is_model proc_name = List.mem dispatch_models ~equal:String.equal (Procname.to_string proc_name) + +let get_dispatch_closure_opt actual_params = + List.find_map actual_params ~f:(fun (exp, _) -> + match exp with + | Exp.Closure c when Procname.is_objc_block c.name -> + (* We assume that for these modelled functions, the block passed as parameter doesn't + have arguments, so we only pass the captured variables. *) + let args = List.map ~f:(fun (id_exp, _, typ, _) -> (id_exp, typ)) c.captured_vars in + Some (c.name, args) + | _ -> + None ) diff --git a/infer/src/biabduction/ObjCDispatchModels.mli b/infer/src/IR/ObjCDispatchModels.mli similarity index 70% rename from infer/src/biabduction/ObjCDispatchModels.mli rename to infer/src/IR/ObjCDispatchModels.mli index 82e74fbec..d4f1ce292 100644 --- a/infer/src/biabduction/ObjCDispatchModels.mli +++ b/infer/src/IR/ObjCDispatchModels.mli @@ -8,3 +8,5 @@ open! IStd val is_model : Procname.t -> bool + +val get_dispatch_closure_opt : (Exp.t * Typ.t) list -> (Procname.t * (Exp.t * Typ.t) list) option diff --git a/infer/src/biabduction/ObjCDispatchModels.ml b/infer/src/biabduction/ObjCDispatchModels.ml deleted file mode 100644 index 121daa031..000000000 --- a/infer/src/biabduction/ObjCDispatchModels.ml +++ /dev/null @@ -1,18 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) -open! IStd - -let dispatch_models = - [ "_dispatch_once" - ; "dispatch_async" - ; "dispatch_after" - ; "dispatch_group_async" - ; "dispatch_barrier_async" - ; "dispatch_group_notify" ] - - -let is_model proc_name = List.mem dispatch_models ~equal:String.equal (Procname.to_string proc_name) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 6d56124e7..0f0d8eb8d 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1077,11 +1077,6 @@ let declare_locals_and_ret tenv pdesc (prop_ : Prop.normal Prop.t) = prop' -let get_closure_opt actual_params = - List.find_map actual_params ~f:(fun (exp, _) -> - match exp with Exp.Closure c when Procname.is_objc_block c.name -> Some c | _ -> None ) - - (** Execute [instr] with a symbolic heap [prop].*) let rec sym_exec ( {InterproceduralAnalysis.proc_desc= current_pdesc; analyze_dependency; err_log; tenv} as @@ -1109,12 +1104,9 @@ let rec sym_exec let par' = List.map ~f:(fun (id_exp, _, typ, _) -> (id_exp, typ)) c.captured_vars in Sil.Call (ret, proc_exp', par' @ par, loc, call_flags) | Exp.Const (Const.Cfun callee_pname) when ObjCDispatchModels.is_model callee_pname -> ( - match get_closure_opt par with - | Some c -> - (* We assume that for these modelled functions, the block passed as parameter doesn't - have arguments, so we only pass the captured variables. *) - let args = List.map ~f:(fun (id_exp, _, typ, _) -> (id_exp, typ)) c.captured_vars in - Sil.Call (ret, Exp.Const (Const.Cfun c.name), args, loc, call_flags) + match ObjCDispatchModels.get_dispatch_closure_opt par with + | Some (cname, args) -> + Sil.Call (ret, Exp.Const (Const.Cfun cname), args, loc, call_flags) | None -> Sil.Call (ret, exp', par, loc, call_flags) ) | _ ->