[cost] Compute range using post state

Reviewed By: ezgicicek

Differential Revision: D8186895

fbshipit-source-id: 679cd4e

infer/src/absint/ProcCfg.ml

@@ -286,9 +286,11 @@ module Backward (Base : S) = struct
   let fold_exceptional_preds = Base.fold_exceptional_succs
 end
 
-module OneInstrPerNode (Base : S with module Node = DefaultNode) :
+module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig
-  S with type t = Base.t and module Node = InstrNode =
+  include S with type t = Base.t and module Node = InstrNode
-struct
+
+  val last_of_underlying_node : Procdesc.Node.t -> Node.t
+end = struct
   type t = Base.t
 
   module Node = InstrNode
@@ -302,6 +304,8 @@ struct
 
   let last_of_node node = (node, max 0 (Instrs.count (Base.instrs node) - 1))
 
+  let last_of_underlying_node = last_of_node
+
   let fold_normal_succs _ _ ~init:_ ~f:_ = (* not used *) assert false
 
   let fold_exceptional_succs _ _ ~init:_ ~f:_ = (* not used *) assert false

infer/src/absint/ProcCfg.mli

@@ -96,7 +96,10 @@ module Exceptional :
 (** Wrapper that reverses the direction of the CFG *)
 module Backward (Base : S) : S with type t = Base.t and module Node = Base.Node
 
-module OneInstrPerNode (Base : S with module Node = DefaultNode) :
+module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig
-  S with type t = Base.t and module Node = InstrNode
+  include S with type t = Base.t and module Node = InstrNode
+
+  val last_of_underlying_node : Procdesc.Node.t -> Node.t
+end
 
 module NormalOneInstrPerNode : module type of OneInstrPerNode (Normal)

infer/src/bufferoverrun/bufferOverrunChecker.mli

@@ -18,3 +18,5 @@ type invariant_map
 val compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t
 
 val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option
+
+val extract_post : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option

infer/src/checkers/cost.ml

@@ -154,11 +154,11 @@ module BoundMap = struct
       | Procdesc.Node.Exit_node _ ->
           Node.IdMap.add node_id BasicCost.one bound_map
       | _ ->
-          let entry_state_opt =
+          let exit_state_opt =
-            let instr_node_id = InstrCFG.Node.of_underlying_node node |> InstrCFG.Node.id in
+            let instr_node_id = InstrCFG.last_of_underlying_node node |> InstrCFG.Node.id in
-            BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map
+            BufferOverrunChecker.extract_post instr_node_id inferbo_invariant_map
           in
-          match entry_state_opt with
+          match exit_state_opt with
           | Some entry_mem ->
               (* compute all the dependencies, i.e. set of variables that affect the control flow upto the node *)
               let all_deps =

infer/tests/codetoanalyze/c/performance/issues.exp

@@ -2,7 +2,7 @@ codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, CONDITION_
 codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * s$1]
 codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * s$1]
 codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * s$1]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 * s$1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 7 * s$1]
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
@@ -49,6 +49,9 @@ codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TI
 codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * s$1]
 codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * s$1^2]
 codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * s$1^2]
+codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2002]
+codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2002]
+codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2004]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * s$1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * s$1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 * s$1]

infer/tests/codetoanalyze/c/performance/jump_inside_loop.c

@@ -0,0 +1,22 @@
+/*
+ * 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.
+ */
+
+int jump_inside_loop(int p) {
+  int i = 0;
+  if (p > 0) {
+    goto Loop;
+  } else {
+    return p;
+  }
+  while (i < 500) {
+  Loop:
+    i++;
+  }
+  return 1;
+}