From ecc5c80a9bab3298dee5cbe4d9cebe9d82802654 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 13 Nov 2019 02:49:30 -0800 Subject: [PATCH] [inferbo] Fix a bug in SafeInvertedMap.join Summary: `equals1` and `equals2` in `SafeInvertedMap.join` are references that indicate whether given parameters and the result is physically equal or not. This diff fixes a missing update of them. Reviewed By: ezgicicek Differential Revision: D18450680 fbshipit-source-id: bae19cbe9 --- infer/src/absint/AbstractDomain.ml | 5 ++++- .../java/bufferoverrun/ArrayListTest.java | 17 +++++++++++++++++ .../codetoanalyze/java/bufferoverrun/issues.exp | 2 ++ 3 files changed, 23 insertions(+), 1 deletion(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 27b9654b4..1c6e5219d 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -649,7 +649,10 @@ struct match (v1_opt, v2_opt) with | Some v1, Some v2 -> let v = f v1 v2 in - if ValueDomain.is_top v then None + if ValueDomain.is_top v then ( + equals1 := false ; + equals2 := false ; + None ) else ( if not (phys_equal v v1) then equals1 := false ; if not (phys_equal v v2) then equals2 := false ; diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java index 47111dc51..cea94ce55 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java @@ -203,4 +203,21 @@ class ArrayListTest { j = a1.get(b.size() + 1); j = a2.get(b.size() + 1); } + + void alias_join_bad() { + int i; + ArrayList a = new ArrayList<>(); + ArrayList b = new ArrayList<>(); + if (unknown_bool) { + a.add(0); + i = 0; // i = size of b + } else { + b.add(0); + b.add(0); + i = 0; // i = size of a + } + if (i == 0) { + b.get(0); // size of b should be [0, 2] + } + } } diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 1a886e554..89fae33b9 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -14,6 +14,8 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_b codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Array declaration,Assignment,,Parameter `b.elements[*]`,Assignment,Array declaration,Array access: Offset: b.length + 1 Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator2_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Assignment,,Parameter `b.elements[*]`,Array access: Offset: [0, b.length] Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Array declaration,Array access: Offset: b.length + 1 Size: b.length] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 12, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 13, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: [0, 2]] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 2, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.multi_adds_in_loop_iterator_bad(java.util.ArrayList):void, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Array declaration,Array access: Offset: b.length + 1 Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.remove_in_loop_iterator_good_FP(java.util.ArrayList):void, 14, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Parameter `b.elements[*]`,Array access: Offset: b.length Size: b.length]