[inferbo] Fix check function for is_collection_add

Summary: It fixes the conditions of the `check` function to address `is_collection_add` cases correctly.

Reviewed By: mbouaziz

Differential Revision: D13081281

fbshipit-source-id: 39ae5ef03

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -250,11 +250,10 @@ module ArrayAccessCondition = struct
        For arrays : we want to check that 0 <= idx < size
        For adding into arraylists: we want to check that 0 <= idx <= size *)
     let real_idx = ItvPure.plus c.offset c.idx in
-    let size = ItvPure.make_positive c.size in
+    let size = ItvPure.make_positive (if is_collection_add then ItvPure.succ c.size else c.size) in
     (* if sl < 0, use sl' = 0 *)
     let not_overrun =
-      if is_collection_add then ItvPure.le_sem real_idx size
+      if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Itv.Boolean.true_
-      else if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Itv.Boolean.true_
       else ItvPure.lt_sem real_idx size
     in
     let not_underrun =

infer/src/bufferoverrun/itv.ml

@@ -626,6 +626,8 @@ module ItvPure = struct
 
   let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2)
 
+  let succ : t -> t = fun x -> plus x one
+
   let mult_const : Z.t -> t -> t =
    fun n ((l, u) as itv) ->
     match NonZeroInt.of_big_int n with

infer/src/bufferoverrun/itv.mli

@@ -146,6 +146,8 @@ module ItvPure : sig
 
   val minus : t -> t -> t
 
+  val succ : t -> t
+
   val mult : t -> t -> t
 end
 

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

@@ -129,6 +129,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_
 codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: x,Call,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [-19+min(0, x), -1] Size: 1]
 codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/models.c, call_memcpy_len2_Good_FP, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Offset: [0, +oo] Size: [0, +oo] by call to `memcpy_len` ]
 codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: 255]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 256] Size: 256]

infer/tests/codetoanalyze/c/bufferoverrun/models.c

@@ -97,6 +97,21 @@ void memcpy_good4() {
   memcpy(dst, src, sizeof(dst));
 }
 
+void memcpy_len(size_t len) {
+  char dst[len];
+  char src[len];
+  memcpy(dst, src, len);
+}
+
+void call_memcpy_len1_Good() { memcpy_len(40); }
+
+extern size_t unknown_uint();
+
+void call_memcpy_len2_Good_FP() {
+  size_t x = unknown();
+  memcpy_len(x);
+}
+
 void memmove_bad1() {
   int arr1[10];
   int arr2[20];