From 1b63cb42b7721eb9a5c138b58bcf70b028db0085 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 1 Jun 2018 12:31:11 -0700 Subject: [PATCH] [cost] Compute range using post state Reviewed By: ezgicicek Differential Revision: D8186895 fbshipit-source-id: 679cd4e --- infer/src/absint/ProcCfg.ml | 10 ++++++--- infer/src/absint/ProcCfg.mli | 7 ++++-- .../bufferoverrun/bufferOverrunChecker.mli | 2 ++ infer/src/checkers/cost.ml | 8 +++---- .../codetoanalyze/c/performance/issues.exp | 5 ++++- .../c/performance/jump_inside_loop.c | 22 +++++++++++++++++++ 6 files changed, 44 insertions(+), 10 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/performance/jump_inside_loop.c diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index bd01c0893..7a99d8fea 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/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) : - S with type t = Base.t and module Node = InstrNode = -struct +module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig + include S with type t = Base.t and module Node = InstrNode + + 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 diff --git a/infer/src/absint/ProcCfg.mli b/infer/src/absint/ProcCfg.mli index 20d1120cb..a9d25c300 100644 --- a/infer/src/absint/ProcCfg.mli +++ b/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) : - S with type t = Base.t and module Node = InstrNode +module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig + 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) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index f09c3576f..b5054dcc0 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/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 diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index b83a256f0..6aaaa0cae 100644 --- a/infer/src/checkers/cost.ml +++ b/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 instr_node_id = InstrCFG.Node.of_underlying_node node |> InstrCFG.Node.id in - BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map + let exit_state_opt = + let instr_node_id = InstrCFG.last_of_underlying_node node |> InstrCFG.Node.id in + 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 = diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 5518c406e..5fe76e685 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/c/performance/jump_inside_loop.c b/infer/tests/codetoanalyze/c/performance/jump_inside_loop.c new file mode 100644 index 000000000..f863a44fa --- /dev/null +++ b/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; +}