From a3eed439f6e94f40dd90c2d3d43efd0c658f98f4 Mon Sep 17 00:00:00 2001 From: Phoebe Nichols Date: Tue, 9 Jul 2019 06:06:46 -0700 Subject: [PATCH] Supply caller summary to Ondemand.analyze_proc_desc and Ondemand.analyze_proc_name Summary: Supply the caller `Summary.t` to `Ondemand.analyze_proc_name` and `Ondemand.analyze_proc_desc` instead of the caller `Procdesc.t` This change will enable a later commit to record the procedures that are called by a procedure in its summary Reviewed By: ngorogiannis Differential Revision: D16148677 fbshipit-source-id: cf353e89a --- infer/src/absint/SummaryPayload.ml | 4 +- infer/src/backend/ondemand.ml | 20 +++- infer/src/backend/ondemand.mli | 12 +- infer/src/biabduction/Builtin.ml | 2 +- infer/src/biabduction/Builtin.mli | 2 +- infer/src/biabduction/BuiltinDefn.ml | 104 ++++++++++-------- infer/src/biabduction/SymExec.ml | 78 +++++++------ infer/src/biabduction/SymExec.mli | 2 +- infer/src/biabduction/SymExecBlocks.ml | 6 +- infer/src/biabduction/SymExecBlocks.mli | 2 +- infer/src/biabduction/interproc.ml | 8 +- .../bufferoverrun/bufferOverrunAnalysis.ml | 2 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 2 +- infer/src/checkers/annotationReachability.ml | 8 +- infer/src/checkers/cost.ml | 4 +- infer/src/checkers/hoisting.ml | 4 +- 16 files changed, 141 insertions(+), 119 deletions(-) diff --git a/infer/src/absint/SummaryPayload.ml b/infer/src/absint/SummaryPayload.ml index ebe408aa9..b0b5cdc06 100644 --- a/infer/src/absint/SummaryPayload.ml +++ b/infer/src/absint/SummaryPayload.ml @@ -43,9 +43,7 @@ module Make (P : Payload) : S with type t = P.t = struct let read_all ?caller_summary ~callee_pname = let open Option.Monad_infix in - Ondemand.analyze_proc_name - ?caller_pdesc:(Option.map ~f:Summary.get_proc_desc caller_summary) - callee_pname + Ondemand.analyze_proc_name ?caller_summary callee_pname >>= fun summary -> of_summary summary >>| fun payload -> (Summary.get_proc_desc summary, payload) diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index f3a542dee..f3eefb48e 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -282,7 +282,7 @@ let memcache_set proc_name summ = Summary.SummaryServer.set ~key summ -let analyze_proc_desc ~caller_pdesc callee_pdesc = +let analyze_proc_desc ~caller_summary callee_pdesc = let callee_pname = Procdesc.get_proc_name callee_pdesc in if is_active callee_pname then None else @@ -296,7 +296,11 @@ let analyze_proc_desc ~caller_pdesc callee_pdesc = | None -> let proc_attributes = Procdesc.get_attributes callee_pdesc in if should_be_analyzed proc_attributes then - (Some (run_proc_analysis ~caller_pdesc:(Some caller_pdesc) callee_pdesc), true) + ( Some + (run_proc_analysis + ~caller_pdesc:(Some (Summary.get_proc_desc caller_summary)) + callee_pdesc) + , true ) else (Summary.get callee_pname, true) in if update_memcached then memcache_set callee_pname summary_option ; @@ -312,9 +316,9 @@ let get_proc_desc callee_pname = ; lazy (Topl.get_proc_desc callee_pname) ] -(** analyze_proc_name ?caller_pdesc proc_name performs an on-demand analysis of proc_name triggered - during the analysis of caller_pdesc *) -let analyze_proc_name ?caller_pdesc callee_pname = +(** analyze_proc_name ?caller_summary callee_pname performs an on-demand analysis of callee_pname triggered + during the analysis of caller_summary *) +let analyze_proc_name ?caller_summary callee_pname = if is_active callee_pname then None else let cache = Lazy.force cached_results in @@ -328,7 +332,11 @@ let analyze_proc_name ?caller_pdesc callee_pname = if procedure_should_be_analyzed callee_pname then match get_proc_desc callee_pname with | Some callee_pdesc -> - (Some (run_proc_analysis ~caller_pdesc callee_pdesc), true) + ( Some + (run_proc_analysis + ~caller_pdesc:(Option.map ~f:Summary.get_proc_desc caller_summary) + callee_pdesc) + , true ) | None -> (Summary.get callee_pname, true) else ( diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index d37c59393..f2e5ea44e 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -12,13 +12,13 @@ open! IStd val get_proc_desc : Typ.Procname.t -> Procdesc.t option (** Find a proc desc for the procedure, perhaps loading it from disk. *) -val analyze_proc_desc : caller_pdesc:Procdesc.t -> Procdesc.t -> Summary.t option -(** [analyze_proc_desc ~caller_pdesc callee_pdesc] performs an on-demand analysis of callee_pdesc - triggered during the analysis of caller_pdesc *) +val analyze_proc_desc : caller_summary:Summary.t -> Procdesc.t -> Summary.t option +(** [analyze_proc_desc ~caller_summary callee_pdesc] performs an on-demand analysis of callee_pdesc + triggered during the analysis of caller_summary *) -val analyze_proc_name : ?caller_pdesc:Procdesc.t -> Typ.Procname.t -> Summary.t option -(** [analyze_proc_name ~caller_pdesc proc_name] performs an on-demand analysis of proc_name - triggered during the analysis of caller_pdesc *) +val analyze_proc_name : ?caller_summary:Summary.t -> Typ.Procname.t -> Summary.t option +(** [analyze_proc_name ~caller_summary callee_pname] performs an on-demand analysis of callee_pname + triggered during the analysis of caller_summary *) val set_exe_env : Exe_env.t -> unit (** Set the execution enviroment used during on-demand analysis. *) diff --git a/infer/src/biabduction/Builtin.ml b/infer/src/biabduction/Builtin.ml index 22d5854d3..71b745300 100644 --- a/infer/src/biabduction/Builtin.ml +++ b/infer/src/biabduction/Builtin.ml @@ -11,7 +11,7 @@ module L = Logging (** Module for builtin functions with their symbolic execution handler *) type args = - { pdesc: Procdesc.t + { summary: Summary.t ; instr: Sil.instr ; tenv: Tenv.t ; prop_: Prop.normal Prop.t diff --git a/infer/src/biabduction/Builtin.mli b/infer/src/biabduction/Builtin.mli index e78437574..c86fe1e69 100644 --- a/infer/src/biabduction/Builtin.mli +++ b/infer/src/biabduction/Builtin.mli @@ -10,7 +10,7 @@ open! IStd (** Module for builtin functions with their symbolic execution handler *) type args = - { pdesc: Procdesc.t + { summary: Summary.t ; instr: Sil.instr ; tenv: Tenv.t ; prop_: Prop.normal Prop.t diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index 188de2aae..fb7c46dc1 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -15,12 +15,13 @@ module L = Logging type t = Builtin.registered (** model va_arg as always returning 0 *) -let execute___builtin_va_arg {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} : +let execute___builtin_va_arg {Builtin.summary; tenv; prop_; path; args; loc; exe_env} : Builtin.ret_typ = match args with | [(lexp3, typ3)] -> let instr' = Sil.Store (lexp3, typ3, Exp.zero, loc) in - SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.singleton instr') [(prop_, path)] + SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton instr') + [(prop_, path)] | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -85,7 +86,9 @@ let add_array_to_prop tenv pdesc prop_ lexp typ = (* Add an array in prop if it is not allocated.*) -let execute___require_allocated_array {Builtin.tenv; pdesc; prop_; path; args} : Builtin.ret_typ = +let execute___require_allocated_array {Builtin.tenv; summary; prop_; path; args} : Builtin.ret_typ + = + let pdesc = Summary.get_proc_desc summary in match args with | [(lexp, typ)] -> ( match add_array_to_prop tenv pdesc prop_ lexp typ with @@ -97,11 +100,11 @@ let execute___require_allocated_array {Builtin.tenv; pdesc; prop_; path; args} : raise (Exceptions.Wrong_argument_number __POS__) -let execute___get_array_length {Builtin.tenv; pdesc; prop_; path; ret_id_typ; args} : +let execute___get_array_length {Builtin.tenv; summary; prop_; path; ret_id_typ; args} : Builtin.ret_typ = match args with | [(lexp, typ)] -> ( - match add_array_to_prop tenv pdesc prop_ lexp typ with + match add_array_to_prop tenv (Summary.get_proc_desc summary) prop_ lexp typ with | None -> [] | Some (len, prop) -> @@ -110,7 +113,8 @@ let execute___get_array_length {Builtin.tenv; pdesc; prop_; path; ret_id_typ; ar raise (Exceptions.Wrong_argument_number __POS__) -let execute___set_array_length {Builtin.tenv; pdesc; prop_; path; args} : Builtin.ret_typ = +let execute___set_array_length {Builtin.tenv; summary; prop_; path; args} : Builtin.ret_typ = + let pdesc = Summary.get_proc_desc summary in match args with | [(lexp, typ); (len, _)] -> ( match add_array_to_prop tenv pdesc prop_ lexp typ with @@ -138,9 +142,9 @@ let execute___set_array_length {Builtin.tenv; pdesc; prop_; path; args} : Builti raise (Exceptions.Wrong_argument_number __POS__) -let execute___print_value {Builtin.tenv; pdesc; prop_; path; args} : Builtin.ret_typ = +let execute___print_value {Builtin.tenv; summary; prop_; path; args} : Builtin.ret_typ = L.(debug Analysis Medium) "__print_value: " ; - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let do_arg (lexp, _) = let n_lexp, _ = check_arith_norm_exp tenv pname lexp prop_ in L.(debug Analysis Medium) "%a " Exp.pp n_lexp @@ -211,10 +215,11 @@ let create_type tenv n_lexp typ prop = else null_case @ non_null_case -let execute___get_type_of {Builtin.pdesc; tenv; prop_; path; ret_id_typ; args} : Builtin.ret_typ = +let execute___get_type_of {Builtin.summary; tenv; prop_; path; ret_id_typ; args} : Builtin.ret_typ + = match args with | [(lexp, typ)] -> - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let props = create_type tenv n_lexp typ prop in let aux prop = @@ -256,11 +261,11 @@ let replace_ptsto_texp tenv prop root_e texp = Prop.normalize tenv prop'' -let execute___instanceof_cast ~instof {Builtin.pdesc; tenv; prop_; path; ret_id_typ; args} : +let execute___instanceof_cast ~instof {Builtin.summary; tenv; prop_; path; ret_id_typ; args} : Builtin.ret_typ = match args with | [(val1_, typ1); (texp2_, _)] -> - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in let is_cast_to_reference = @@ -359,10 +364,11 @@ let set_resource_attribute tenv prop path n_lexp loc ra_res = (** Set the attibute of the value as file *) -let execute___set_file_attribute {Builtin.tenv; pdesc; prop_; path; args; loc} : Builtin.ret_typ = +let execute___set_file_attribute {Builtin.tenv; summary; prop_; path; args; loc} : Builtin.ret_typ + = match args with | [(lexp, _)] -> - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in set_resource_attribute tenv prop path n_lexp loc PredSymb.Rfile | _ -> @@ -371,11 +377,11 @@ let execute___set_file_attribute {Builtin.tenv; pdesc; prop_; path; args; loc} : (** Set the resource attribute of the first real argument of method as ignore, the first argument is assumed to be "this" *) -let execute___method_set_ignore_attribute {Builtin.tenv; pdesc; prop_; path; args; loc} : +let execute___method_set_ignore_attribute {Builtin.tenv; summary; prop_; path; args; loc} : Builtin.ret_typ = match args with | [_; (lexp, _)] -> - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in set_resource_attribute tenv prop path n_lexp loc PredSymb.Rignore | _ -> @@ -383,10 +389,10 @@ let execute___method_set_ignore_attribute {Builtin.tenv; pdesc; prop_; path; arg (** Set the attibute of the value as memory *) -let execute___set_mem_attribute {Builtin.tenv; pdesc; prop_; path; args; loc} : Builtin.ret_typ = +let execute___set_mem_attribute {Builtin.tenv; summary; prop_; path; args; loc} : Builtin.ret_typ = match args with | [(lexp, _)] -> - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in set_resource_attribute tenv prop path n_lexp loc (PredSymb.Rmemory PredSymb.Mnew) | _ -> @@ -406,19 +412,20 @@ let delete_attr tenv pdesc prop path exp attr = (** Set attibute att *) -let execute___set_attr attr {Builtin.tenv; pdesc; prop_; path; args} : Builtin.ret_typ = +let execute___set_attr attr {Builtin.tenv; summary; prop_; path; args} : Builtin.ret_typ = match args with | [(lexp, _)] -> - set_attr tenv pdesc prop_ path lexp attr + set_attr tenv (Summary.get_proc_desc summary) prop_ path lexp attr | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Delete the locked attibute of the value*) -let execute___delete_locked_attribute {Builtin.tenv; prop_; pdesc; path; args} : Builtin.ret_typ = +let execute___delete_locked_attribute {Builtin.tenv; prop_; summary; path; args} : Builtin.ret_typ + = match args with | [(lexp, _)] -> - delete_attr tenv pdesc prop_ path lexp PredSymb.Alocked + delete_attr tenv (Summary.get_proc_desc summary) prop_ path lexp PredSymb.Alocked | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -490,11 +497,11 @@ let execute_free_nonzero_ mk ?(mark_as_freed = true) pdesc tenv instr prop lexp raise (Exceptions.Array_of_pointsto __POS__) ) -let execute_free mk ?(mark_as_freed = true) {Builtin.pdesc; instr; tenv; prop_; path; args; loc} : - Builtin.ret_typ = +let execute_free mk ?(mark_as_freed = true) {Builtin.summary; instr; tenv; prop_; path; args; loc} + : Builtin.ret_typ = match args with | [(lexp, typ)] -> - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let prop_nonzero = (* case n_lexp!=0 *) @@ -509,7 +516,7 @@ let execute_free mk ?(mark_as_freed = true) {Builtin.pdesc; instr; tenv; prop_; @ (* model: if 0 then skip else execute_free_nonzero_ *) List.concat_map ~f:(fun p -> - execute_free_nonzero_ mk ~mark_as_freed pdesc tenv instr p + execute_free_nonzero_ mk ~mark_as_freed (Summary.get_proc_desc summary) tenv instr p (Prop.exp_normalize_prop tenv p lexp) typ loc ) prop_nonzero @@ -526,9 +533,9 @@ let execute_free mk ?(mark_as_freed = true) {Builtin.pdesc; instr; tenv; prop_; This should behave correctly most of the time. *) let execute_free_cf mk = execute_free mk ~mark_as_freed:false -let execute_alloc mk can_return_null {Builtin.pdesc; tenv; prop_; path; ret_id_typ; args; loc} : +let execute_alloc mk can_return_null {Builtin.summary; tenv; prop_; path; ret_id_typ; args; loc} : Builtin.ret_typ = - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let rec evaluate_char_sizeof e = match e with | Exp.Var _ -> @@ -600,14 +607,14 @@ let execute_alloc mk can_return_null {Builtin.pdesc; tenv; prop_; path; ret_id_t else [(prop_alloc, path)] -let execute___cxx_typeid ({Builtin.pdesc; tenv; prop_; args; loc; exe_env} as r) : Builtin.ret_typ - = +let execute___cxx_typeid ({Builtin.summary; tenv; prop_; args; loc; exe_env} as r) : + Builtin.ret_typ = match args with | type_info_exp :: rest -> ( let res = execute_alloc PredSymb.Mnew false {r with args= [type_info_exp]} in match rest with | [(field_exp, _); (lexp, typ_)] -> - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let typ = List.find @@ -621,14 +628,14 @@ let execute___cxx_typeid ({Builtin.pdesc; tenv; prop_; args; loc; exe_env} as r) let set_instr = Sil.Store (field_exp, Typ.mk Tvoid, Exp.Const (Const.Cstr typ_string), loc) in - SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.singleton set_instr) res + SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) res | _ -> res ) | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let execute_pthread_create ({Builtin.tenv; pdesc; prop_; path; args; exe_env} as builtin_args) : +let execute_pthread_create ({Builtin.tenv; summary; prop_; path; args; exe_env} as builtin_args) : Builtin.ret_typ = match args with | [_; _; start_routine; arg] -> ( @@ -653,7 +660,7 @@ let execute_pthread_create ({Builtin.tenv; pdesc; prop_; path; args; exe_env} as [(prop_, path)] | Some pname -> ( L.d_printfln "pthread_create: calling function %a" Typ.Procname.pp pname ; - match Ondemand.analyze_proc_name ~caller_pdesc:pdesc pname with + match Ondemand.analyze_proc_name ~caller_summary:summary pname with | None -> (* no precondition to check, skip *) [(prop_, path)] @@ -678,11 +685,11 @@ let execute_scan_function skip_n_arguments ({Builtin.args; ret_id_typ} as call_a raise (Exceptions.Wrong_argument_number __POS__) -let execute__unwrap_exception {Builtin.tenv; pdesc; prop_; path; ret_id_typ; args} : +let execute__unwrap_exception {Builtin.tenv; summary; prop_; path; ret_id_typ; args} : Builtin.ret_typ = match args with | [(ret_exn, _)] -> ( - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let n_ret_exn, prop = check_arith_norm_exp tenv pname ret_exn prop_ in match n_ret_exn with | Exp.Exn exp -> @@ -694,11 +701,11 @@ let execute__unwrap_exception {Builtin.tenv; pdesc; prop_; path; ret_id_typ; arg raise (Exceptions.Wrong_argument_number __POS__) -let execute_return_first_argument {Builtin.tenv; pdesc; prop_; path; ret_id_typ; args} : +let execute_return_first_argument {Builtin.tenv; summary; prop_; path; ret_id_typ; args} : Builtin.ret_typ = match args with | (arg1_, _) :: _ -> - let pname = Procdesc.get_proc_name pdesc in + let pname = Procdesc.get_proc_name (Summary.get_proc_desc summary) in let arg1, prop = check_arith_norm_exp tenv pname arg1_ prop_ in let prop' = return_result tenv arg1 prop ret_id_typ in [(prop', path)] @@ -706,11 +713,11 @@ let execute_return_first_argument {Builtin.tenv; pdesc; prop_; path; ret_id_typ; raise (Exceptions.Wrong_argument_number __POS__) -let execute___split_get_nth {Builtin.tenv; pdesc; prop_; path; ret_id_typ; args} : Builtin.ret_typ - = +let execute___split_get_nth {Builtin.tenv; summary; prop_; path; ret_id_typ; args} : + Builtin.ret_typ = match args with | [(lexp1, _); (lexp2, _); (lexp3, _)] -> ( - let pname = Procdesc.get_proc_name pdesc in + let pname = Summary.get_proc_name summary in let n_lexp1, prop__ = check_arith_norm_exp tenv pname lexp1 prop_ in let n_lexp2, prop___ = check_arith_norm_exp tenv pname lexp2 prop__ in let n_lexp3, prop = check_arith_norm_exp tenv pname lexp3 prop___ in @@ -742,7 +749,8 @@ let execute___infer_assume {Builtin.tenv; prop_; path; args} : Builtin.ret_typ = (* creates a named error state *) -let execute___infer_fail {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} : Builtin.ret_typ = +let execute___infer_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_env} : Builtin.ret_typ + = let error_str = match args with | [(lexp_msg, _)] -> ( @@ -757,12 +765,12 @@ let execute___infer_fail {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} let set_instr = Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) in - SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.singleton set_instr) [(prop_, path)] + SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) [(prop_, path)] (* translate builtin assertion failure *) -let execute___assert_fail {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} : Builtin.ret_typ - = +let execute___assert_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_env} : + Builtin.ret_typ = let error_str = match List.length args with | 4 -> @@ -773,11 +781,11 @@ let execute___assert_fail {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} let set_instr = Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) in - SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.singleton set_instr) [(prop_, path)] + SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) [(prop_, path)] let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt - {Builtin.pdesc; tenv; ret_id_typ; loc; exe_env} = + {Builtin.summary; tenv; ret_id_typ; loc; exe_env} = let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.__objc_alloc_no_fail) in let ptr_typ = Typ.mk (Tptr (typ, Typ.Pk_pointer)) in let sizeof_typ = Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact} in @@ -792,7 +800,7 @@ let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt Sil.Call (ret_id_typ, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) in - SymExec.instrs exe_env tenv pdesc (Instrs.singleton alloc_instr) symb_state + SymExec.instrs exe_env tenv summary (Instrs.singleton alloc_instr) symb_state (* NSArray models *) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 02a46e7e7..98d3b02b5 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -698,17 +698,19 @@ type resolve_and_analyze_result = (** Resolve the procedure name and run the analysis of the resolved procedure if not already analyzed *) -let resolve_and_analyze tenv ~caller_pdesc ?(has_clang_model = false) prop args callee_proc_name +let resolve_and_analyze tenv ~caller_summary ?(has_clang_model = false) prop args callee_proc_name call_flags : resolve_and_analyze_result = (* TODO (#15748878): Fix conflict with method overloading by encoding in the procedure name whether the method is defined or generated by the specialization *) let analyze_ondemand resolved_pname : Procdesc.t option * Summary.t option = if Typ.Procname.equal resolved_pname callee_proc_name then ( Ondemand.get_proc_desc callee_proc_name - , Ondemand.analyze_proc_name ~caller_pdesc callee_proc_name ) + , Ondemand.analyze_proc_name ~caller_summary callee_proc_name ) else (* Create the type specialized procedure description and analyze it directly *) - let analyze specialized_pdesc = Ondemand.analyze_proc_desc ~caller_pdesc specialized_pdesc in + let analyze specialized_pdesc = + Ondemand.analyze_proc_desc ~caller_summary specialized_pdesc + in let resolved_proc_desc_option = match Ondemand.get_proc_desc resolved_pname with | Some _ as resolved_proc_desc -> @@ -724,7 +726,11 @@ let resolve_and_analyze tenv ~caller_pdesc ?(has_clang_model = false) prop args in (resolved_proc_desc_option, Option.bind resolved_proc_desc_option ~f:analyze) in - let resolved_pname = resolve_pname ~caller_pdesc tenv prop args callee_proc_name call_flags in + let resolved_pname = + resolve_pname + ~caller_pdesc:(Summary.get_proc_desc caller_summary) + tenv prop args callee_proc_name call_flags + in let dynamic_dispatch_status = if Typ.Procname.equal callee_proc_name resolved_pname then None else Some EventLogger.Dynamic_dispatch_successful @@ -1092,8 +1098,8 @@ let is_variadic_procname callee_pname = ~default:false -let resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params callee_pname - call_flags = +let resolve_and_analyze_no_dynamic_dispatch current_summary tenv prop_r n_actual_params + callee_pname call_flags = let resolved_pname = match resolve_virtual_pname tenv prop_r n_actual_params callee_pname call_flags with | resolved_pname :: _ -> @@ -1102,7 +1108,7 @@ let resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_p callee_pname in let resolved_summary_opt = - Ondemand.analyze_proc_name ~caller_pdesc:current_pdesc resolved_pname + Ondemand.analyze_proc_name ~caller_summary:current_summary resolved_pname in { resolved_pname ; resolved_procdesc_opt= Ondemand.get_proc_desc resolved_pname @@ -1110,7 +1116,7 @@ let resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_p ; dynamic_dispatch_status= None } -let resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_pname call_flags = +let resolve_and_analyze_clang current_summary tenv prop_r n_actual_params callee_pname call_flags = if Config.dynamic_dispatch && (not (is_variadic_procname callee_pname)) @@ -1121,7 +1127,7 @@ let resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_p try let has_clang_model = Summary.has_model callee_pname in let resolve_and_analyze_result = - resolve_and_analyze tenv ~caller_pdesc:current_pdesc ~has_clang_model prop_r + resolve_and_analyze tenv ~caller_summary:current_summary ~has_clang_model prop_r n_actual_params callee_pname call_flags in (* It could be useful to specialize a model, but also it could cause a failure, @@ -1138,7 +1144,7 @@ let resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_p in if clang_model_specialized_failure then let result = - resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params + resolve_and_analyze_no_dynamic_dispatch current_summary tenv prop_r n_actual_params callee_pname call_flags in { result with @@ -1147,14 +1153,14 @@ let resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_p else resolve_and_analyze_result with SpecializeProcdesc.UnmatchedParameters -> let result = - resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params + resolve_and_analyze_no_dynamic_dispatch current_summary tenv prop_r n_actual_params callee_pname call_flags in { result with dynamic_dispatch_status= Some EventLogger.Dynamic_dispatch_parameters_arguments_mismatch } else - resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params callee_pname - call_flags + resolve_and_analyze_no_dynamic_dispatch current_summary tenv prop_r n_actual_params + callee_pname call_flags let declare_locals_and_ret tenv pdesc (prop_ : Prop.normal Prop.t) = @@ -1190,8 +1196,9 @@ let declare_locals_and_ret tenv pdesc (prop_ : Prop.normal Prop.t) = (** Execute [instr] with a symbolic heap [prop].*) -let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) path : +let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t) path : (Prop.normal Prop.t * Paths.Path.t) list = + let current_pdesc = Summary.get_proc_desc current_summary in let current_pname = Procdesc.get_proc_name current_pdesc in State.set_instr instr_ ; (* mark instruction last seen *) @@ -1231,7 +1238,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) ?callee_attributes ~reason loc Tabulation.CR_skip ; unknown_or_scan_call ~is_scan:false ~reason ret_typ ret_annots Builtin. - { pdesc= current_pdesc + { summary= current_summary ; instr ; tenv ; prop_= prop @@ -1248,7 +1255,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) else skip_res () in let call_args prop_ proc_name args ret_id_typ loc = - { Builtin.pdesc= current_pdesc + { Builtin.summary= current_summary ; instr ; tenv ; prop_ @@ -1314,8 +1321,8 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) norm_args in let resolve_and_analyze_result = - resolve_and_analyze tenv ~caller_pdesc:current_pdesc norm_prop norm_args callee_pname - call_flags + resolve_and_analyze tenv ~caller_summary:current_summary norm_prop norm_args + callee_pname call_flags in let resolved_pname = resolve_and_analyze_result.resolved_pname in match resolve_and_analyze_result.resolved_summary_opt with @@ -1344,7 +1351,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) skip_call ~reason norm_prop path pname ret_annots loc ret_id_typ ret_type url_handled_args in - match Ondemand.analyze_proc_name ~caller_pdesc:current_pdesc pname with + match Ondemand.analyze_proc_name ~caller_summary:current_summary pname with | None -> let ret_typ = Typ.Procname.Java.get_return_typ callee_pname_java in let ret_annots = load_ret_annots callee_pname in @@ -1366,8 +1373,8 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) (* method with block parameters *) let with_block_parameters_summary_opt = if call_flags.CallFlags.cf_with_block_parameters then - SymExecBlocks.resolve_method_with_block_args_and_analyze ~caller_pdesc:current_pdesc - callee_pname actual_params + SymExecBlocks.resolve_method_with_block_args_and_analyze + ~caller_summary:current_summary callee_pname actual_params else None in match with_block_parameters_summary_opt with @@ -1381,7 +1388,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) | None -> (* Generic fun call with known name *) let resolve_and_analyze_result = - resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_pname + resolve_and_analyze_clang current_summary tenv prop_r n_actual_params callee_pname call_flags in let resolved_pname = resolve_and_analyze_result.resolved_pname in @@ -1431,7 +1438,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) | None, true -> (* If it's an alloc model, call alloc rather than skipping *) sym_exec_alloc_model exe_env resolved_pname ret_type tenv ret_id_typ - current_pdesc loc prop path + current_summary loc prop path | None, false -> let is_objc_instance_method = ClangMethodKind.equal attrs.ProcAttributes.clang_method_kind @@ -1470,7 +1477,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) unknown_or_scan_call ~is_scan:false ~reason:"unresolved function pointer" (snd ret_id_typ) Annot.Item.empty Builtin. - { pdesc= current_pdesc + { summary= current_summary ; instr ; tenv ; prop_= prop_r @@ -1521,12 +1528,12 @@ and diverge prop path = (** Symbolic execution of a sequence of instructions. If errors occur and [mask_errors] is true, just treat as skip. *) -and instrs ?(mask_errors = false) exe_env tenv pdesc instrs ppl = +and instrs ?(mask_errors = false) exe_env tenv summary instrs ppl = let exe_instr instr (p, path) = L.d_str "Executing Generated Instruction " ; Sil.d_instr instr ; L.d_ln () ; - try sym_exec exe_env tenv pdesc instr p path + try sym_exec exe_env tenv summary instr p path with exn -> IExn.reraise_if exn ~f:(fun () -> (not mask_errors) || not (SymOp.exn_not_failure exn)) ; let error = Exceptions.recognize_exception exn in @@ -1633,7 +1640,7 @@ and add_constraints_on_actuals_by_ref tenv caller_pdesc prop actuals_by_ref call (** execute a call for an unknown or scan function *) and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots - {Builtin.tenv; pdesc; prop_= pre; path; ret_id_typ; args; proc_name= callee_pname; loc; instr} + {Builtin.tenv; summary; prop_= pre; path; ret_id_typ; args; proc_name= callee_pname; loc; instr} = let remove_file_attribute prop = let do_exp p (e, _) = @@ -1689,6 +1696,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots in let has_nonnull_annot = Annotations.ia_is_nonnull ret_annots in let pre_final = + let pdesc = Summary.get_proc_desc summary in (* in Java, assume that skip functions close resources passed as params *) let pre_1 = if Typ.Procname.is_java callee_pname then remove_file_attribute pre else pre in let pre_2 = @@ -1720,7 +1728,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_pos) - {Builtin.pdesc; tenv; prop_; path; args; proc_name; loc; exe_env} = + {Builtin.summary; tenv; prop_; path; args; proc_name; loc; exe_env} = (* from clang's lib/Sema/SemaExpr.cpp: *) (* "nullPos" is the number of formal parameters at the end which *) (* effectively count as part of the variadic arguments. This is *) @@ -1739,7 +1747,7 @@ and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_po (* simulate a Load for [lexp] *) let tmp_id_deref = Ident.create_fresh Ident.kprimed in let load_instr = Sil.Load (tmp_id_deref, lexp, typ, loc) in - try instrs exe_env tenv pdesc (Instrs.singleton load_instr) result + try instrs exe_env tenv summary (Instrs.singleton load_instr) result with e when SymOp.exn_not_failure e -> IExn.reraise_if e ~f:(fun () -> fails_on_nil) ; let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in @@ -1823,7 +1831,7 @@ and sym_exec_objc_accessor callee_pname property_accesor ret_typ tenv ret_id pde f_accessor ret_typ tenv ret_id pdesc cur_pname loc args prop |> List.map ~f:(fun p -> (p, path)) -and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ pdesc loc prop path : +and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ summary loc prop path : Builtin.ret_typ = let alloc_source_function_arg = (Exp.Const (Const.Cfun pname), Typ.mk Tvoid) in let args = @@ -1836,13 +1844,13 @@ and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ pdesc loc prop pa let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.malloc_no_fail) in let alloc_instr = Sil.Call (ret_id_typ, alloc_fun, args, loc, CallFlags.default) in L.d_strln "No spec found, method should be model as alloc, executing alloc... " ; - instrs exe_env tenv pdesc (Instrs.singleton alloc_instr) [(prop, path)] + instrs exe_env tenv summary (Instrs.singleton alloc_instr) [(prop, path)] (** Perform symbolic execution for a function call *) and proc_call ?dynamic_dispatch exe_env callee_summary - {Builtin.pdesc; tenv; prop_= pre; path; ret_id_typ; args= actual_pars; loc} = - let caller_pname = Procdesc.get_proc_name pdesc in + {Builtin.summary; tenv; prop_= pre; path; ret_id_typ; args= actual_pars; loc} = + let caller_pname = Summary.get_proc_name summary in let callee_attrs = Summary.get_attributes callee_summary in let callee_pname = Summary.get_proc_name callee_summary in check_inherently_dangerous_function caller_pname callee_pname ; @@ -1883,6 +1891,7 @@ and proc_call ?dynamic_dispatch exe_env callee_summary let actual_params = comb actual_pars formal_types in (* In case we call an objc instance method we add an extra spec where the receiver is null and the semantics of the call is nop *) + let pdesc = Summary.get_proc_desc summary in match (!Language.curr_language, callee_attrs.ProcAttributes.clang_method_kind) with | Language.Clang, ClangMethodKind.OBJC_INSTANCE -> handle_objc_instance_method_call actual_pars actual_params pre tenv (fst ret_id_typ) pdesc @@ -1961,8 +1970,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr let res_list = BiabductionConfig.run_with_abs_val_equal_zero (* no exp abstraction during sym exe *) - (fun () -> - sym_exec exe_env tenv (ProcCfg.Exceptional.proc_desc proc_cfg) instr prop' path ) + (fun () -> sym_exec exe_env tenv summary instr prop' path ) () in let res_list_nojunk = diff --git a/infer/src/biabduction/SymExec.mli b/infer/src/biabduction/SymExec.mli index 743d1cb39..94bbbb210 100644 --- a/infer/src/biabduction/SymExec.mli +++ b/infer/src/biabduction/SymExec.mli @@ -28,7 +28,7 @@ val instrs : ?mask_errors:bool -> Exe_env.t -> Tenv.t - -> Procdesc.t + -> Summary.t -> Instrs.not_reversed_t -> (Prop.normal Prop.t * Paths.Path.t) list -> (Prop.normal Prop.t * Paths.Path.t) list diff --git a/infer/src/biabduction/SymExecBlocks.ml b/infer/src/biabduction/SymExecBlocks.ml index 68536fa18..fdc5c22c1 100644 --- a/infer/src/biabduction/SymExecBlocks.ml +++ b/infer/src/biabduction/SymExecBlocks.ml @@ -43,9 +43,9 @@ let get_extended_args_for_method_with_block_analysis act_params = List.map ~f:(fun (exp, _, typ) -> (exp, typ)) args_and_captured -let resolve_method_with_block_args_and_analyze ~caller_pdesc pname act_params = +let resolve_method_with_block_args_and_analyze ~caller_summary pname act_params = let pdesc_opt = - match Ondemand.analyze_proc_name ~caller_pdesc pname with + match Ondemand.analyze_proc_name ~caller_summary pname with | Some summary -> Some (Summary.get_proc_desc summary) | None -> @@ -89,7 +89,7 @@ let resolve_method_with_block_args_and_analyze ~caller_pdesc pname act_params = ) specialized_pdesc ; Logging.(debug Analysis Verbose) "End of instructions@." ; - match Ondemand.analyze_proc_desc ~caller_pdesc specialized_pdesc with + match Ondemand.analyze_proc_desc ~caller_summary specialized_pdesc with | Some summary -> (* Since the closures in the formals were replaced by the captured variables, we do the same with the actual arguments *) diff --git a/infer/src/biabduction/SymExecBlocks.mli b/infer/src/biabduction/SymExecBlocks.mli index df6ee6eba..b9093ac93 100644 --- a/infer/src/biabduction/SymExecBlocks.mli +++ b/infer/src/biabduction/SymExecBlocks.mli @@ -8,7 +8,7 @@ open! IStd val resolve_method_with_block_args_and_analyze : - caller_pdesc:Procdesc.t + caller_summary:Summary.t -> Typ.Procname.t -> (Exp.t * Typ.t) list -> (Summary.t * (Exp.t * Typ.t) list) option diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index fe9967d99..3b09c37ce 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -1221,7 +1221,8 @@ let perform_transition proc_cfg tenv proc_name summary = else summary -let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t = +let analyze_procedure_aux summary exe_env tenv : Summary.t = + let proc_desc = Summary.get_proc_desc summary in let proc_name = Procdesc.get_proc_name proc_desc in let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in let summaryfp = @@ -1250,11 +1251,10 @@ let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t = let analyze_procedure {Callbacks.summary; tenv; exe_env} : Summary.t = - let proc_desc = Summary.get_proc_desc summary in (* make sure models have been registered *) BuiltinDefn.init () ; - if Topl.is_active () then Topl.instrument tenv proc_desc ; - try analyze_procedure_aux summary exe_env tenv proc_desc + if Topl.is_active () then Topl.instrument tenv (Summary.get_proc_desc summary) ; + try analyze_procedure_aux summary exe_env tenv with exn -> IExn.reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ; Reporting.log_error_using_state summary exn ; diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 8ee7732f4..26bf137c0 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -344,7 +344,7 @@ let cached_compute_invariant_map = assert false | None -> let get_proc_summary_and_formals callee_pname = - Ondemand.analyze_proc_name ~caller_pdesc:(Summary.get_proc_desc summary) callee_pname + Ondemand.analyze_proc_name ~caller_summary:summary callee_pname |> Option.bind ~f:(fun summary -> Payload.of_summary summary |> Option.map ~f:(fun payload -> diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 7617e952d..805d260bf 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -433,7 +433,7 @@ let checker : Callbacks.proc_callback_args -> Summary.t = let cfg = CFG.from_pdesc proc_desc in let checks = let get_proc_summary callee_pname = - Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname + Ondemand.analyze_proc_name ~caller_summary:summary callee_pname |> Option.bind ~f:(fun summary -> let analysis_payload = BufferOverrunAnalysis.Payload.of_summary summary in let checker_payload = Payload.of_summary summary in diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 0e7cc131f..cfa9de661 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -113,8 +113,8 @@ let method_has_annot annot tenv pname = let method_overrides_annot annot tenv pname = method_overrides (method_has_annot annot) tenv pname -let lookup_annotation_calls ~caller_pdesc annot pname = - match Ondemand.analyze_proc_name ~caller_pdesc pname with +let lookup_annotation_calls ~caller_summary annot pname = + match Ondemand.analyze_proc_name ~caller_summary pname with | Some {Summary.payloads= {Payloads.annot_map= Some annot_map}} -> ( try AnnotReachabilityDomain.find annot annot_map with Caml.Not_found -> AnnotReachabilityDomain.SinkMap.empty ) @@ -221,7 +221,7 @@ let report_src_snk_path {Callbacks.tenv; summary} sink_map snk_annot src_annot = if method_overrides_annot src_annot tenv proc_name then let f_report = report_annotation_stack src_annot.Annot.class_name snk_annot.Annot.class_name in report_call_stack summary (method_has_annot snk_annot tenv) ~string_of_pname ~call_str:" -> " - (lookup_annotation_calls ~caller_pdesc:proc_desc snk_annot) + (lookup_annotation_calls ~caller_summary:summary snk_annot) f_report (CallSite.make proc_name loc) sink_map @@ -383,7 +383,7 @@ module CxxAnnotationSpecs = struct let sink_map = AnnotReachabilityDomain.find snk_annot annot_map in report_call_stack proc_data.Callbacks.summary snk_pred ~string_of_pname:cxx_string_of_pname ~call_str - (lookup_annotation_calls ~caller_pdesc:proc_desc snk_annot) + (lookup_annotation_calls ~caller_summary:proc_data.Callbacks.summary snk_annot) report_cxx_annotation_stack (CallSite.make proc_name loc) sink_map with Caml.Not_found -> () in diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 1645b137b..4390d57d0 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -807,7 +807,7 @@ let checker {Callbacks.tenv; integer_type_widths; summary} : Summary.t = (* compute loop invariant map for control var analysis *) let loop_inv_map = let get_callee_purity callee_pname = - match Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname with + match Ondemand.analyze_proc_name ~caller_summary:summary callee_pname with | Some {Summary.payloads= {Payloads.purity}} -> purity | _ -> @@ -823,7 +823,7 @@ let checker {Callbacks.tenv; integer_type_widths; summary} : Summary.t = let get_node_nb_exec = compute_get_node_nb_exec node_cfg bound_map in let astate = let get_callee_summary_and_formals callee_pname = - Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname + Ondemand.analyze_proc_name ~caller_summary:summary callee_pname |> Option.bind ~f:(fun summary -> Payload.of_summary summary |> Option.map ~f:(fun payload -> diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index f8abb4e19..100589c1a 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -161,7 +161,7 @@ let checker Callbacks.{tenv; summary; integer_type_widths} : Summary.t = BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths in let get_callee_cost_summary_and_formals callee_pname = - Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname + Ondemand.analyze_proc_name ~caller_summary:summary callee_pname |> Option.bind ~f:(fun summary -> summary.Summary.payloads.Payloads.cost |> Option.map ~f:(fun cost_summary -> @@ -173,7 +173,7 @@ let checker Callbacks.{tenv; summary; integer_type_widths} : Summary.t = else fun _ -> None in let get_callee_purity callee_pname = - match Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname with + match Ondemand.analyze_proc_name ~caller_summary:summary callee_pname with | Some {Summary.payloads= {Payloads.purity}} -> purity | _ ->