From 97ba078d5544ddd50d65ca9db79fcc7e5fe21a18 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Thu, 16 Jan 2020 02:49:20 -0800
Subject: [PATCH] [inferbo] Revise getting size of array block

Summary:
This diff avoids that `array_sizeof` returns bottom value when given Java enum values, which
introduced unreachable code inadvertently.

Reviewed By: ngorogiannis

Differential Revision: D19409077

fbshipit-source-id: 2816fd995
---
 infer/src/bufferoverrun/bufferOverrunDomain.ml      |  4 +++-
 .../codetoanalyze/java/bufferoverrun/Array.java     | 13 +++++++++++++
 .../codetoanalyze/java/bufferoverrun/issues.exp     |  1 +
 3 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index dd2d4d607..b7f836987 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -468,7 +468,9 @@ module Val = struct
     {x with traces}
 
 
-  let array_sizeof {arrayblk} = ArrayBlk.get_size arrayblk
+  let array_sizeof {arrayblk} =
+    if ArrayBlk.is_bot arrayblk then Itv.top else ArrayBlk.get_size arrayblk
+
 
   let set_array_length : Location.t -> length:t -> t -> t =
    fun location ~length v ->
diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java
index 959599241..4665bdb1a 100644
--- a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java
+++ b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java
@@ -122,4 +122,17 @@ class Array {
       arr[idx] = 0;
     }
   }
+
+  enum MyEnum {
+    MyEnumA
+  };
+
+  void array_length_Bad() {
+    int[] arr = new int[5];
+    if (MyEnum.values().length == 0) {
+      arr[10] = 0;
+    } else {
+      arr[10] = 0;
+    }
+  }
 }
diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
index 8af85a6bd..df3c97f86 100644
--- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
@@ -1,3 +1,4 @@
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.array_length_Bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.call_iterate_collection_Bad():void, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Through,Through,Through,Through,Through,Call,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5 by call to `void Array.iterate_collection_Bad(ArrayList)` ]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.negative_alloc_Bad():void, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1]