[Inferbo] Fix the way pointers to arrays are handled in Java

Reviewed By: mbouaziz

Differential Revision: D9195302

fbshipit-source-id: 83333c0c8

infer/src/IR/Typ.ml

@@ -172,8 +172,6 @@ let is_restrict {is_restrict} = is_restrict
 
 let is_volatile {is_volatile} = is_volatile
 
-let is_array {desc} = match desc with Tarray _ -> true | _ -> false
-
 let mk ?default ?quals desc : t =
   let default_ = {desc; quals= mk_type_quals ()} in
   let mk_aux ?(default= default_) ?(quals= default.quals) desc = {desc; quals} in

infer/src/IR/Typ.mli

@@ -265,8 +265,6 @@ val is_pointer_to_cpp_class : t -> bool
 
 val is_pointer : t -> bool
 
-val is_array : t -> bool
-
 val is_reference : t -> bool
 
 val has_block_prefix : string -> bool

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -239,10 +239,17 @@ module Init = struct
         | Typ.Tfloat _ ->
             let v = Dom.Val.make_sym loc pname symbol_table path new_sym_num location in
             mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
-        | Typ.Tptr (typ, _) when Language.curr_language_is Java && not (Typ.is_array typ) ->
+        | Typ.Tptr (typ, _) when Language.curr_language_is Java -> (
+          match typ with
+          | {desc= Typ.Tarray {elt}} ->
+              BoUtils.Exec.decl_sym_arr
+                ~decl_sym_val:(decl_sym_val ~may_last_field:false)
+                pname symbol_table path tenv ~node_hash location ~depth loc elt ~inst_num
+                ~new_sym_num ~new_alloc_num mem
+          | _ ->
               BoUtils.Exec.decl_sym_java_ptr
                 ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-              pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem
+                pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem )
         | Typ.Tptr (typ, _) ->
             BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname
               symbol_table path tenv ~node_hash location ~depth loc typ ~inst_num ~new_sym_num

infer/tests/codetoanalyze/java/performance/Array.java

@@ -22,4 +22,10 @@ public class Array {
       radii[i * 2 + 2] = radii[i] + 1;
     }
   }
+
+  void array_access_weird_ok(long[] optionNumerators, int length) {
+    for (int j = 0; j < length; ++j) {
+      if (10 < optionNumerators[j] + 1) {}
+    }
+  }
 }

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

@@ -1,4 +1,7 @@
 codetoanalyze/java/performance/Array.java, void Array.array_access_overrun_bad(), 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [2, 8] Size: 8]
+codetoanalyze/java/performance/Array.java, void Array.array_access_weird_ok(long[],int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 15 * length.ub, degree = 1]
+codetoanalyze/java/performance/Array.java, void Array.array_access_weird_ok(long[],int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 * length.ub, degree = 1]
+codetoanalyze/java/performance/Array.java, void Array.array_access_weird_ok(long[],int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 15 * length.ub, degree = 1]
 codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 882, degree = 0]
 codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0]
 codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 882, degree = 0]