[inferbo] Check collection constructor size

Reviewed By: mbouaziz

Differential Revision: D14122995

fbshipit-source-id: eeb2fceab

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -653,8 +653,8 @@ module Collection = struct
     let exec {integer_type_widths} ~ret:_ mem =
       let itr = Sem.eval integer_type_widths rhs_exp mem in
       model_by_value itr lhs_id mem
-    in
-    {exec; check= no_check}
+    and check = check_alloc_size rhs_exp in
+    {exec; check}
 
 
   let hasNext iterator =

infer/tests/codetoanalyze/java/bufferoverrun/Array.java

@@ -56,4 +56,16 @@ class Array {
       }
     }
   }
+
+  void negative_alloc_Bad() {
+    a = new ArrayList<>(-1);
+  }
+
+  void zero_alloc_Good_FP() {
+    a = new ArrayList<>(0);
+  }
+
+  void positive_alloc_Good() {
+    a = new ArrayList<>(10);
+  }
 }

infer/tests/codetoanalyze/java/bufferoverrun/issues.exp

@@ -1,8 +1,10 @@
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, 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, 1, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1]
 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, [<Length trace>,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, [<Length trace>,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, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.zero_alloc_Good_FP():void, 1, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Allocation: Length: 0]
 codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,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, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]