From fadd8cb541c7138e820e74d3afa06d82769ee3b0 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Fri, 23 Aug 2019 03:45:18 -0700
Subject: [PATCH] [inferbo] Prune array size in Java

Summary: This diff prunes array sizes in Java by adding the size alias on the `get_array_length` function calls.

Reviewed By: ezgicicek

Differential Revision: D16983501

fbshipit-source-id: a924af09d
---
 .../src/bufferoverrun/bufferOverrunModels.ml  | 25 ++++++++++---------
 .../java/performance/PreconditionTest.java    | 12 +++++++++
 2 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 421c87ae1..cd6bdb38c 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -419,11 +419,20 @@ let eval_array_locs_length arr_locs mem =
     Dom.Val.of_itv ~traces length
 
 
+let load_size_alias id arr_locs mem =
+  match PowLoc.is_singleton_or_more arr_locs with
+  | IContainer.Singleton loc ->
+      Dom.Mem.load_size_alias id loc mem
+  | IContainer.Empty | IContainer.More ->
+      mem
+
+
 (* Java only *)
 let get_array_length array_exp =
   let exec _ ~ret:(ret_id, _) mem =
-    let result = eval_array_locs_length (Sem.eval_locs array_exp mem) mem in
-    model_by_value result ret_id mem
+    let arr_locs = Sem.eval_locs array_exp mem in
+    let result = eval_array_locs_length arr_locs mem in
+    model_by_value result ret_id mem |> load_size_alias ret_id arr_locs
   in
   {exec; check= no_check}
 
@@ -695,11 +704,7 @@ module StdVector = struct
     let exec model_env ~ret:(id, _) mem =
       let arr_locs = deref_of model_env elt_typ vec_arg mem in
       let mem = Dom.Mem.add_stack (Loc.of_id id) (eval_array_locs_length arr_locs mem) mem in
-      match PowLoc.is_singleton_or_more arr_locs with
-      | IContainer.Singleton loc ->
-          Dom.Mem.load_size_alias id loc mem
-      | IContainer.Empty | IContainer.More ->
-          mem
+      load_size_alias id arr_locs mem
     in
     {exec; check= no_check}
 end
@@ -893,11 +898,7 @@ module Collection = struct
     let exec _ ~ret:(ret_id, _) mem =
       let result = eval_collection_length coll_exp mem in
       let mem = model_by_value result ret_id mem in
-      match PowLoc.is_singleton_or_more (eval_collection_internal_array_locs coll_exp mem) with
-      | IContainer.Singleton loc ->
-          Dom.Mem.load_size_alias ret_id loc mem
-      | IContainer.Empty | IContainer.More ->
-          mem
+      load_size_alias ret_id (eval_collection_internal_array_locs coll_exp mem) mem
     in
     {exec; check= no_check}
 
diff --git a/infer/tests/codetoanalyze/java/performance/PreconditionTest.java b/infer/tests/codetoanalyze/java/performance/PreconditionTest.java
index efd39eac1..d42e063e0 100644
--- a/infer/tests/codetoanalyze/java/performance/PreconditionTest.java
+++ b/infer/tests/codetoanalyze/java/performance/PreconditionTest.java
@@ -13,4 +13,16 @@ class PreconditionTest {
     Preconditions.checkArgument(list.size() == 2);
     for (int i = 0; i < list.size(); i++) {}
   }
+
+  public class get_five {
+    public static final int FIVE = 5;
+  }
+
+  // should be constant
+  static void constant_array(int[] a) {
+    Preconditions.checkArgument(a.length == get_five.FIVE);
+    for (int i : a) {
+      Preconditions.checkArgument(i >= 0);
+    }
+  }
 }