Cost: instantiate symbolic cost after call

Reviewed By: ddino

Differential Revision: D7397208

fbshipit-source-id: a9647dc

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

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

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
       | _ ->

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); }

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]