diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index dbb8eb135..4a45526b4 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -409,7 +409,13 @@ module PowLoc = struct type eval_locpath = Symb.SymbolPath.partial -> t let subst_loc l (eval_locpath : eval_locpath) = - match Loc.get_param_path l with None -> singleton l | Some path -> eval_locpath path + match Loc.get_param_path l with + | None -> + singleton l + | Some path when Language.curr_language_is Java && Symb.SymbolPath.is_global_partial path -> + singleton l + | Some path -> + eval_locpath path let subst x (eval_locpath : eval_locpath) = diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 68104a9c9..0f208c6fb 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -978,11 +978,14 @@ module Bound = struct in fun ~subst_pos x eval_sym -> let get s bound_position = - match eval_sym s bound_position with - | NonBottom x when Symb.Symbol.is_unsigned s -> - NonBottom (approx_max subst_pos x zero) - | x -> - x + if Language.curr_language_is Java && Symb.Symbol.is_global s then + NonBottom (of_sym (SymLinear.singleton_one s)) + else + match eval_sym s bound_position with + | NonBottom x when Symb.Symbol.is_unsigned s -> + NonBottom (approx_max subst_pos x zero) + | x -> + x in let get_mult_const s coeff = let bound_position = diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 9a5a98b30..ea03dea6c 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -249,6 +249,18 @@ module SymbolPath = struct BufferOverrunField.is_cpp_vector_elem fn | _ -> false + + + let rec is_global_partial = function + | Pvar pvar -> + Pvar.is_global pvar + | Deref (_, x) | Field {prefix= x} | StarField {prefix= x} -> + is_global_partial x + | Callsite _ -> + false + + + let is_global = function Normal p | Offset {p} | Length {p} | Modeled p -> is_global_partial p end module Symbol = struct @@ -326,6 +338,11 @@ module Symbol = struct let is_non_int : t -> bool = function OneValue {non_int} | BoundEnd {non_int} -> non_int + let is_global : t -> bool = function + | OneValue {path} | BoundEnd {path} -> + SymbolPath.is_global path + + let path = function OneValue {path} | BoundEnd {path} -> path (* NOTE: This may not be satisfied in the cost checker for simplifying its results. *) diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 634a5bac5..57c835f11 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -89,6 +89,8 @@ module SymbolPath : sig val is_void_ptr_path : t -> bool val is_cpp_vector_elem : partial -> bool + + val is_global_partial : partial -> bool end module Symbol : sig @@ -102,6 +104,8 @@ module Symbol : sig val is_non_int : t -> bool + val is_global : t -> bool + val pp_mark : markup:bool -> F.formatter -> t -> unit val equal : t -> t -> bool diff --git a/infer/tests/codetoanalyze/java/performance/Cost_test.java b/infer/tests/codetoanalyze/java/performance/Cost_test.java index 40c843014..aa8a9339f 100644 --- a/infer/tests/codetoanalyze/java/performance/Cost_test.java +++ b/infer/tests/codetoanalyze/java/performance/Cost_test.java @@ -190,4 +190,16 @@ public class Cost_test { total += r; } } + + static int global; + + int get_global() { + return global; + } + + /* It instantiates the return value of `get_global` (= `global`, the value of which is unknown) to + the `global` symbol, instead of top, in order to avoid useless top-cost results. */ + void loop_on_unknown_global_linear() { + for (int i = 0; i < get_global(); i++) {} + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index dd7a17c74..95c878103 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -94,6 +94,7 @@ codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Co codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1202, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop1_bad():int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1303, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop3(int):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 237, O(1), degree = 0] +codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop_on_unknown_global_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ codetoanalyze.java.performance.Cost_test.global + 5 ⋅ (1+max(0, codetoanalyze.java.performance.Cost_test.global)), O(codetoanalyze.java.performance.Cost_test.global), degree = 1,{1+max(0, codetoanalyze.java.performance.Cost_test.global)},Loop at line 203,{codetoanalyze.java.performance.Cost_test.global},Loop at line 203] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.main_bad():int, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 205, O(1), degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 613, O(1), degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 201, O(1), degree = 0]