[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

@@ -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) =

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
+        if Language.curr_language_is Java && Symb.Symbol.is_global s then
-        | NonBottom x when Symb.Symbol.is_unsigned s ->
+          NonBottom (of_sym (SymLinear.singleton_one s))
-            NonBottom (approx_max subst_pos x zero)
+        else
-        | x ->
+          match eval_sym s bound_position with
-            x
+          | 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 =

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. *)

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

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++) {}
+  }
 }

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]