diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 92d9f013d..cfaad3ecf 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/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, diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayMember.java b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayMember.java new file mode 100644 index 000000000..cbe362329 --- /dev/null +++ b/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; + } + } +} diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index b3a8a5d60..390bcf080 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/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, [,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, [,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, [,Parameter `this.buf[*]`,Assignment,,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, [,Assignment,,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32] diff --git a/infer/tests/codetoanalyze/java/hoisting/issues.exp b/infer/tests/codetoanalyze/java/hoisting/issues.exp index 59dc93126..22574bb99 100644 --- a/infer/tests/codetoanalyze/java/hoisting/issues.exp +++ b/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[])] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index f1ad181d0..a16e22b79 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/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, [,Parameter `a[*]`,,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, [,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]