From c5ab00ae825c4aebdd373ebfc338a085fa50d6bf Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 26 Sep 2019 04:03:42 -0700 Subject: [PATCH] [cost] Avoid giving top to unknown global in Java Summary: This diff avoids giving the top value to unknown globals in Java, because they harm precision of the cost checker. Instead, it doesn't subst the global symbols at function calls. Reviewed By: ezgicicek Differential Revision: D17498714 fbshipit-source-id: d1215b3aa --- infer/src/bufferoverrun/absLoc.ml | 8 +++++++- infer/src/bufferoverrun/bounds.ml | 13 ++++++++----- infer/src/bufferoverrun/symb.ml | 17 +++++++++++++++++ infer/src/bufferoverrun/symb.mli | 4 ++++ .../java/performance/Cost_test.java | 12 ++++++++++++ .../codetoanalyze/java/performance/issues.exp | 1 + 6 files changed, 49 insertions(+), 6 deletions(-) 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]