From 3139ee5d465f7ade8dcc7e394d2fd7b07e8cea88 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 14 Feb 2019 11:25:01 -0800 Subject: [PATCH] [cost] Instantiate costs using formals not pname Summary: Simplifies `instantiate_cost`, call `Ondemand` once per call site. Depends on D14028249 Reviewed By: ddino Differential Revision: D14028281 fbshipit-source-id: 865151fee --- infer/src/checkers/cost.ml | 37 +++++++++++++++++----------------- infer/src/checkers/cost.mli | 2 +- infer/src/checkers/hoisting.ml | 7 ++++--- 3 files changed, 24 insertions(+), 22 deletions(-) diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 31928865d..93a80f250 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -518,19 +518,11 @@ type extras_WCET = ; integer_type_widths: Typ.IntegerWidths.t ; get_node_nb_exec: Node.id -> BasicCost.t } -let instantiate_cost integer_type_widths ~inferbo_caller_mem ~callee_pname ~params ~callee_cost = - match Ondemand.get_proc_desc callee_pname with - | None -> - L.(die InternalError) - "Can't instantiate symbolic cost %a from call to %a (can't get procdesc)" BasicCost.pp - callee_cost Typ.Procname.pp callee_pname - | Some callee_pdesc -> - let callee_formals = Procdesc.get_pvar_formals callee_pdesc in - let eval_sym = - BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_formals params - inferbo_caller_mem - in - BasicCost.subst callee_cost eval_sym +let instantiate_cost integer_type_widths ~inferbo_caller_mem ~callee_formals ~params ~callee_cost = + let eval_sym = + BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_formals params inferbo_caller_mem + in + BasicCost.subst callee_cost eval_sym module InstrBasicCost = struct @@ -539,10 +531,11 @@ module InstrBasicCost = struct For example for basic operation we set it to 1 and for function call we take it from the spec of the function. *) - let callee_OperationCost callee_cost_record integer_type_widths inferbo_mem callee_pname params = + let callee_OperationCost callee_cost_record integer_type_widths inferbo_mem callee_formals params + = let callee_cost = CostDomain.get_operation_cost callee_cost_record in if BasicCost.is_symbolic callee_cost then - instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem ~callee_pname ~params + instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem ~callee_formals ~params ~callee_cost else callee_cost @@ -551,6 +544,14 @@ module InstrBasicCost = struct let callee_IOCost cost_record = CostDomain.get_IO_cost cost_record + let get_callee_summary caller_pdesc callee_pname = + Ondemand.analyze_proc_name ~caller_pdesc callee_pname + |> Option.bind ~f:(fun summary -> + Payload.of_summary summary + |> Option.map ~f:(fun payload -> + (payload, Summary.get_proc_desc summary |> Procdesc.get_pvar_formals) ) ) + + let get_instr_cost_record pdata instr_node instr = match instr with | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) -> ( @@ -565,11 +566,11 @@ module InstrBasicCost = struct | Some model -> CostDomain.set_operation_cost (model inferbo_mem) CostDomain.zero_record | None -> ( - match Payload.read pdesc callee_pname with - | Some {post= callee_cost_record} -> + match get_callee_summary pdesc callee_pname with + | Some ({CostDomain.post= callee_cost_record}, callee_formals) -> let callee_operation_cost = callee_OperationCost callee_cost_record integer_type_widths inferbo_mem - callee_pname params + callee_formals params in let callee_allocation_cost = callee_AllocationCost callee_cost_record in let callee_IO_cost = callee_IOCost callee_cost_record in diff --git a/infer/src/checkers/cost.mli b/infer/src/checkers/cost.mli index b97ed99c6..26975dab2 100644 --- a/infer/src/checkers/cost.mli +++ b/infer/src/checkers/cost.mli @@ -12,7 +12,7 @@ val checker : Callbacks.proc_callback_t val instantiate_cost : Typ.IntegerWidths.t -> inferbo_caller_mem:BufferOverrunDomain.Mem.t - -> callee_pname:Typ.Procname.t + -> callee_formals:(Pvar.t * Typ.t) list -> params:(Exp.t * 'a) list -> callee_cost:CostDomain.BasicCost.t -> CostDomain.BasicCost.t diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index b1d6ff8ae..bee75c557 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -91,16 +91,17 @@ let get_issue_to_report tenv Call.({pname; node; params}) integer_type_widths in || (* only report if function call has expensive/symbolic cost *) match Ondemand.analyze_proc_name pname with - | Some {Summary.payloads= {Payloads.cost= Some {CostDomain.post= cost_record}}} + | Some ({Summary.payloads= {Payloads.cost= Some {CostDomain.post= cost_record}}} as summary) when CostDomain.BasicCost.is_symbolic (CostDomain.get_operation_cost cost_record) -> let instr_node_id = InstrCFG.last_of_underlying_node node |> InstrCFG.Node.id in let inferbo_invariant_map = Lazy.force inferbo_invariant_map in let inferbo_mem = Option.value_exn (BufferOverrunAnalysis.extract_pre instr_node_id inferbo_invariant_map) in + let callee_formals = Summary.get_proc_desc summary |> Procdesc.get_pvar_formals in (* get the cost of the function call *) - Cost.instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem - ~callee_pname:pname ~params + Cost.instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem ~callee_formals + ~params ~callee_cost:(CostDomain.get_operation_cost cost_record) |> CostDomain.BasicCost.is_symbolic | _ ->