From b0b96b453bac4d9875288450f8c487bca1838724 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 26 Nov 2018 14:26:44 -0800 Subject: [PATCH] [cost] Do not need to load inferbo summary at calls Reviewed By: skcho Differential Revision: D13190966 fbshipit-source-id: 4e745dac3 --- infer/src/checkers/cost.ml | 30 ++++++++++++------------------ infer/src/checkers/cost.mli | 3 +-- infer/src/checkers/hoisting.ml | 14 ++++++++------ 3 files changed, 21 insertions(+), 26 deletions(-) diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 1512aaf69..ebbadd8f2 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -34,26 +34,18 @@ module Node = ProcCfg.DefaultNode The nodes in the domain of the map are those in the path reaching the current node. *) -let instantiate_cost integer_type_widths ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params - ~callee_cost = +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 -> ( - match BufferOverrunChecker.Payload.read caller_pdesc callee_pname with - | None -> - L.(die InternalError) - "Can't instantiate symbolic cost %a from call to %a (can't get summary)" BasicCost.pp - callee_cost Typ.Procname.pp callee_pname - | Some _ -> - let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in - let eval_sym = - BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_pdesc params - inferbo_caller_mem - in - BasicCost.subst callee_cost eval_sym ) + | Some callee_pdesc -> + let eval_sym = + BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_pdesc params + inferbo_caller_mem + in + BasicCost.subst callee_cost eval_sym module TransferFunctionsNodesBasicCost = struct @@ -77,8 +69,8 @@ module TransferFunctionsNodesBasicCost = struct match Payload.read pdesc callee_pname with | Some {post= callee_cost} -> if BasicCost.is_symbolic callee_cost then - instantiate_cost integer_type_widths ~caller_pdesc:pdesc - ~inferbo_caller_mem:inferbo_mem ~callee_pname ~params ~callee_cost + instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem + ~callee_pname ~params ~callee_cost else callee_cost | None -> cost_atomic_instruction @@ -104,7 +96,9 @@ module TransferFunctionsNodesBasicCost = struct let exec_instr costmap ({ProcData.extras= {inferbo_invariant_map; integer_type_widths}} as pdata) node instr = - let inferbo_mem = BufferOverrunChecker.extract_pre (CFG.Node.id node) inferbo_invariant_map in + let inferbo_mem = + Option.value_exn (BufferOverrunChecker.extract_pre (CFG.Node.id node) inferbo_invariant_map) + in let costmap = exec_instr_cost integer_type_widths inferbo_mem costmap pdata node instr in costmap diff --git a/infer/src/checkers/cost.mli b/infer/src/checkers/cost.mli index 0d0dc3bdd..b97ed99c6 100644 --- a/infer/src/checkers/cost.mli +++ b/infer/src/checkers/cost.mli @@ -11,8 +11,7 @@ val checker : Callbacks.proc_callback_t val instantiate_cost : Typ.IntegerWidths.t - -> caller_pdesc:Procdesc.t - -> inferbo_caller_mem:BufferOverrunDomain.Mem.t option + -> inferbo_caller_mem:BufferOverrunDomain.Mem.t -> callee_pname:Typ.Procname.t -> params:(Exp.t * 'a) list -> callee_cost:CostDomain.BasicCost.t diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index aa91465e2..84aa8c805 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -77,8 +77,8 @@ let do_report summary Call.({pname; loc}) ~issue loop_head_loc = let model_satisfies ~f tenv pname = InvariantModels.Call.dispatch tenv pname [] |> Option.exists ~f -let get_issue_to_report tenv proc_desc Call.({pname; node; params}) integer_type_widths - inferbo_invariant_map = +let get_issue_to_report tenv Call.({pname; node; params}) integer_type_widths inferbo_invariant_map + = (* If a function is modeled as variant for hoisting (like List.size or __cast ), we don't want to report it *) let is_variant_for_hoisting = @@ -93,10 +93,12 @@ let get_issue_to_report tenv proc_desc Call.({pname; node; params}) integer_type when CostDomain.BasicCost.is_symbolic cost -> 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 = BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map in + let inferbo_mem = + Option.value_exn (BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map) + in (* get the cost of the function call *) - Cost.instantiate_cost integer_type_widths ~caller_pdesc:proc_desc - ~inferbo_caller_mem:inferbo_mem ~callee_pname:pname ~params ~callee_cost:cost + Cost.instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem + ~callee_pname:pname ~params ~callee_cost:cost |> CostDomain.BasicCost.is_symbolic | _ -> false @@ -136,7 +138,7 @@ let checker ({Callbacks.tenv; summary; proc_desc; integer_type_widths} as callba let loop_head_loc = Procdesc.Node.get_loc loop_head in HoistCalls.iter (fun call -> - get_issue_to_report tenv proc_desc call integer_type_widths inferbo_invariant_map + get_issue_to_report tenv call integer_type_widths inferbo_invariant_map |> Option.iter ~f:(fun issue -> do_report summary call ~issue loop_head_loc) ) inv_instrs ) loop_head_to_inv_instrs ;