[inferbo] Fix array member access in Java

Summary: In SIL, Java's array member is a pointer to an array, while C++'s is the array itself.  This diff differentiate them in evaluating abstract locations.

Reviewed By: ezgicicek, mbouaziz

Differential Revision: D14021451

fbshipit-source-id: 00f14fe3b

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -270,7 +270,7 @@ and eval_binop : Typ.IntegerWidths.t -> Binop.t -> Exp.t -> Exp.t -> Mem.t -> Va
 
 
 (**
-  [eval_locs exp mem] is like [eval_locs exp mem |> Val.get_all_locs]
+  [eval_locs exp mem] is like [eval exp mem |> Val.get_all_locs]
   but takes some shortcuts to avoid computing useless and/or problematic intermediate values
 *)
 let rec eval_locs : Exp.t -> Mem.t -> PowLoc.t =
@@ -293,7 +293,8 @@ let rec eval_locs : Exp.t -> Mem.t -> PowLoc.t =
   | Lindex (((Lfield _ | Lindex _) as e), _) ->
       Mem.find_set (eval_locs e mem) mem |> Val.get_all_locs
   | Lindex (e, _) ->
-      eval_locs e mem
+      if Language.curr_language_is Java then Mem.find_set (eval_locs e mem) mem |> Val.get_all_locs
+      else eval_locs e mem
 
 
 (* It returns the array value of the input expression.  For example,

infer/tests/codetoanalyze/java/bufferoverrun/ArrayMember.java

@@ -0,0 +1,27 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+package codetoanalyze.java.bufferoverrun;
+
+public class ArrayMember {
+  public int[] buf;
+
+  public void load_array_member_Good() {
+    int[] a = new int[10];
+    int x = buf[0];
+    if (x == 9) {
+      a[x] = 0;
+    }
+  }
+
+  public void load_array_member_Bad() {
+    int[] a = new int[10];
+    int x = buf[0];
+    if (x == 10) {
+      a[x] = 0;
+    }
+  }
+}

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

@@ -4,4 +4,5 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Good():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
+codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]
 codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]

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

@@ -47,7 +47,6 @@ codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.regionFirst(int[]):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect.regionFirst(int[])]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.return_zero():int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect.return_zero()]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 125 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.tmp_irvar_change_dont_hoist(int[][],int,int[]):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistIndirect.tmp_irvar_change_dont_hoist(int[][],int,int[])]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.unmodified_arg_hoist(int[][],int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.regionFirst(int[]) at line 220 is loop-invariant]
 codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate$Item.while_dont_hoist(HoistInvalidate$Item,HoistInvalidate$Item):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistInvalidate$Item.while_dont_hoist(HoistInvalidate$Item,HoistInvalidate$Item)]
 codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate.get_length(int[]):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistInvalidate.get_length(int[])]

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

@@ -100,6 +100,7 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 ⋅ (length - 1), degree = 1]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length - 1)² + 8 ⋅ length, degree = 2]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `a[*]`,<RHS trace>,Parameter `b[*]`,Binary operation: (a[*] × b[*]):signed64]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 20 + 33 ⋅ x.length, degree = 1]