diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index 9986ac26f..c78b8f267 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/infer/src/bufferoverrun/bufferOverrunChecker.mli @@ -11,6 +11,8 @@ open! IStd val checker : Callbacks.proc_callback_t +module Summary : Summary.S with type payload = BufferOverrunDomain.Summary.t + module CFG = ProcCfg.NormalOneInstrPerNode type invariant_map diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 7fd253e99..795f426dd 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -77,6 +77,8 @@ module Bound : sig val widen : prev:t -> next:t -> num_iters:'a -> t val ( <= ) : lhs:t -> rhs:t -> bool + + val subst_ub : t -> t bottom_lifted SymbolMap.t -> t bottom_lifted end module ItvPure : sig diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index e77ca55c7..09136970b 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -51,17 +51,53 @@ module TransferFunctionsNodesBasicCost = struct let cost_atomic_instruction = Itv.Bound.one - let exec_instr_cost _inferbo_mem (astate: CostDomain.NodeInstructionToCostMap.astate) - {ProcData.pdesc} (node: CFG.node) instr : CostDomain.NodeInstructionToCostMap.astate = + let instantiate_cost ~tenv ~caller_pdesc ~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)" Itv.Bound.pp + callee_cost Typ.Procname.pp callee_pname + | Some callee_pdesc -> + match BufferOverrunChecker.Summary.read_summary caller_pdesc callee_pname with + | None -> + L.(die InternalError) + "Can't instantiate symbolic cost %a from call to %a (can't get summary)" Itv.Bound.pp + callee_cost Typ.Procname.pp callee_pname + | Some inferbo_summary -> + let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in + let callee_entry_mem = BufferOverrunDomain.Summary.get_input inferbo_summary in + let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in + let callee_ret_alias = BufferOverrunDomain.Mem.find_ret_alias callee_exit_mem in + let (subst_map, _), _ = + BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem + callee_entry_mem ~callee_ret_alias + in + match Itv.Bound.subst_ub callee_cost subst_map with + | Bottom -> + L.(die InternalError) + "Instantiation of cost %a from call to %a returned Bottom" Itv.Bound.pp callee_cost + Typ.Procname.pp callee_pname + | NonBottom callee_cost -> + callee_cost + + + let exec_instr_cost inferbo_mem (astate: CostDomain.NodeInstructionToCostMap.astate) + {ProcData.pdesc; tenv} (node: CFG.node) instr : CostDomain.NodeInstructionToCostMap.astate = let key = CFG.id node in let astate' = match instr with - | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), _, _, _) -> ( - match Summary.read_summary pdesc callee_pname with - | Some {post= cost_callee} -> - CostDomain.NodeInstructionToCostMap.add key cost_callee astate - | None -> - CostDomain.NodeInstructionToCostMap.add key cost_atomic_instruction astate ) + | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) -> + let callee_cost = + match Summary.read_summary pdesc callee_pname with + | Some {post= callee_cost} -> + if Itv.Bound.is_symbolic callee_cost then + instantiate_cost ~tenv ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem + ~callee_pname ~params ~callee_cost + else callee_cost + | None -> + cost_atomic_instruction + in + CostDomain.NodeInstructionToCostMap.add key callee_cost astate | Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ -> CostDomain.NodeInstructionToCostMap.add key cost_atomic_instruction astate | _ -> diff --git a/infer/tests/codetoanalyze/c/performance/instantiate.c b/infer/tests/codetoanalyze/c/performance/instantiate.c new file mode 100644 index 000000000..8020fdc96 --- /dev/null +++ b/infer/tests/codetoanalyze/c/performance/instantiate.c @@ -0,0 +1,20 @@ +/* + * Copyright (c) 2018 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +void nop() { int x = 0; } + +void do_n_times(int n) { + for (int i = 0; i < n; i++) { + nop(); + } +} + +void do_2_times_Good() { do_n_times(2); } + +void do_2K_times_Bad() { do_n_times(2000); } diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 236b8f2f5..cd66694e0 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -27,3 +27,6 @@ codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensi codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 545] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 545] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 547] +codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 12004] +codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6xs$1 + 3] +codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6xs$1 + 3]