From 6a8f389c35119030e8d478b351c4a9f8cc41397f Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 1 Jan 2019 21:10:51 -0800 Subject: [PATCH] [inferbo] Prune (p=null) Summary: This diff unset powloc and arrayblk values of p when assume(p==Null). Reviewed By: mbouaziz, jvillard Differential Revision: D13415366 fbshipit-source-id: a491a957f --- .../src/bufferoverrun/bufferOverrunDomain.ml | 10 +++++- .../codetoanalyze/c/bufferoverrun/issues.exp | 5 +++ .../c/bufferoverrun/prune_constant.c | 36 +++++++++++++++++++ .../java/bufferoverrun/Array.java | 36 +++++++++++++++++++ .../java/bufferoverrun/issues.exp | 5 +++ .../java/performance/ArrayListTest.java | 16 +++++++++ .../codetoanalyze/java/performance/issues.exp | 6 ++++ 7 files changed, 113 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 0f8723f6b..f06901b29 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -286,7 +286,15 @@ module Val = struct fun c -> lift_prune2 (Itv.prune_comp c) (ArrayBlk.prune_comp c) - let prune_eq : t -> t -> t = lift_prune2 Itv.prune_eq ArrayBlk.prune_eq + let is_null : t -> bool = + fun x -> Itv.is_false x.itv && PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk + + + let prune_eq : t -> t -> t = + fun x y -> + if is_null y then {x with itv= Itv.zero; powloc= PowLoc.bot; arrayblk= ArrayBlk.bot} + else lift_prune2 Itv.prune_eq ArrayBlk.prune_eq x y + let prune_ne : t -> t -> t = lift_prune2 Itv.prune_ne ArrayBlk.prune_ne diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index d5cc360a2..7d80dd122 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -230,6 +230,11 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BU codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,Assignment,,Array declaration,Array access: Offset: [-28, 16] Size: 17] codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_add2` ] codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_sub2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_sub2` ] +codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning1_Bad, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning1_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning2_Good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c index 9dbf7d8d0..754e69648 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c @@ -128,3 +128,39 @@ void call_prune_sub2_1_Good() { prune_sub2(5); } void call_prune_sub2_2_Bad() { prune_sub2(10); } void call_prune_sub2_3_Good() { prune_sub2(100); } + +void null_pruning1_Good(int* p) { + if (p == 0) { + if (p != 0) { + int a[5]; + a[10] = 1; + } + } +} + +void null_pruning1_Bad(int* p) { + if (p == 0) { + if (p == 0) { + int a[5]; + a[10] = 1; + } + } +} + +void null_pruning2_Good_FP(int* p) { + if (p != 0) { + if (p == 0) { + int a[5]; + a[10] = 1; + } + } +} + +void null_pruning2_Bad(int* p) { + if (p != 0) { + if (p != 0) { + int a[5]; + a[10] = 1; + } + } +} diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java index 019bbecaf..ef6994e28 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java @@ -20,4 +20,40 @@ class Array { b.remove(0); return b; } + + void null_pruning1_Good() { + if (a == null) { + if (a != null) { + int[] arr = {1, 2, 3, 4, 5}; + arr[10] = 1; + } + } + } + + void null_pruning1_Bad() { + if (a == null) { + if (a == null) { + int[] arr = {1, 2, 3, 4, 5}; + arr[10] = 1; + } + } + } + + void null_pruning2_Good_FP() { + if (a != null) { + if (a == null) { + int[] arr = {1, 2, 3, 4, 5}; + arr[10] = 1; + } + } + } + + void null_pruning2_Bad() { + if (a != null) { + if (a != null) { + int[] arr = {1, 2, 3, 4, 5}; + arr[10] = 1; + } + } + } } diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 3bbd85f02..b3a8a5d60 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -1,2 +1,7 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_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_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/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/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index b5120c723..1c7ff247b 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -205,4 +205,20 @@ public class ArrayListTest { private static void call_sortArrayList(ArrayList list) { sortArrayList(list); } + + private ArrayList list = new ArrayList<>(); + + // Since we know the maximum value of boolean [iterator.next().equals(s)] is 1, it is better to be + // excluded from the cost. + // Simplified version of real code https://fburl.com/traceview/tpc0grh2 + public boolean remove_string_from_list(String s) { + Iterator iterator = list.iterator(); + while (iterator.hasNext()) { + if (iterator.next().equals(s)) { + iterator.remove(); + return true; + } + } + return false; + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 10a83e2f9..575eeb89d 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -42,6 +42,12 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_h codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: __cast,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 12 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), degree = 1 + 1⋅log] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, degree = 1] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p, degree = 1]