[inferbo] Give a widening threshold for array offset

Reviewed By: mbouaziz

Differential Revision: D13859243

fbshipit-source-id: 9a81505cc

infer/src/bufferoverrun/arrayBlk.ml

@@ -50,8 +50,14 @@ module ArrInfo = struct
       match (prev, next) with
       | ( C {offset= offset1; size= size1; stride= stride1}
         , C {offset= offset2; size= size2; stride= stride2} ) ->
+          let offset =
+            let thresholds =
+              if Itv.eq size1 size2 then Option.to_list (Itv.is_const size1) else []
+            in
+            Itv.widen_thresholds ~thresholds ~prev:offset1 ~next:offset2 ~num_iters
+          in
           C
-            { offset= Itv.widen ~prev:offset1 ~next:offset2 ~num_iters
+            { offset
             ; size= Itv.widen ~prev:size1 ~next:size2 ~num_iters
             ; stride= Itv.widen ~prev:stride1 ~next:stride2 ~num_iters }
       | Java {length= length1}, Java {length= length2} ->

infer/src/bufferoverrun/bounds.ml

@@ -641,8 +641,44 @@ module Bound = struct
 
   let zero : t = Linear (Z.zero, SymLinear.zero)
 
-  let widen_l : t -> t -> t =
+  module Thresholds : sig
-   fun x y ->
+    type bound = t
+
+    type t
+
+    val make_inc : Z.t list -> t
+
+    val make_dec : Z.t list -> t
+
+    val widen :
+      cond:(threshold:bound -> bound -> bool) -> default:bound -> bound -> bound -> t -> bound
+  end = struct
+    type bound = t
+
+    type t = bound list
+
+    let default_thresholds = [Z.zero]
+
+    let make ~compare thresholds =
+      List.dedup_and_sort ~compare (default_thresholds @ thresholds) |> List.map ~f:of_big_int
+
+
+    (* It makes a list of thresholds that will be applied with the increasing order. *)
+    let make_inc = make ~compare:Z.compare
+
+    (* It makes a list of thresholds that will be applied with the decreasing order. *)
+    let make_dec = make ~compare:(fun x y -> -Z.compare x y)
+
+    let rec widen ~cond ~default x y = function
+      | [] ->
+          default
+      | threshold :: thresholds ->
+          if cond ~threshold x && cond ~threshold y then threshold
+          else widen ~default ~cond x y thresholds
+  end
+
+  let widen_l_thresholds : thresholds:Z.t list -> t -> t -> t =
+   fun ~thresholds x y ->
     match (x, y) with
     | PInf, _ | _, PInf ->
         L.(die InternalError) "Lower bound cannot be +oo."
@@ -653,11 +689,16 @@ module Bound = struct
       when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
         y
     | _ ->
-        if le x y then x else if le zero x && le zero y then zero else MInf
+        if le x y then x
+        else
+          let cond ~threshold x = le threshold x in
+          Thresholds.widen ~cond ~default:MInf x y (Thresholds.make_dec thresholds)
 
 
-  let widen_u : t -> t -> t =
+  let widen_l : t -> t -> t = fun x y -> widen_l_thresholds ~thresholds:[] x y
-   fun x y ->
+
+  let widen_u_thresholds : thresholds:Z.t list -> t -> t -> t =
+   fun ~thresholds x y ->
     match (x, y) with
     | MInf, _ | _, MInf ->
         L.(die InternalError) "Upper bound cannot be -oo."
@@ -668,8 +709,13 @@ module Bound = struct
       when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
         y
     | _ ->
-        if le y x then x else if le x zero && le y zero then zero else PInf
+        if le y x then x
+        else
+          let cond ~threshold x = le x threshold in
+          Thresholds.widen ~cond ~default:PInf x y (Thresholds.make_inc thresholds)
+
 
+  let widen_u : t -> t -> t = fun x y -> widen_u_thresholds ~thresholds:[] x y
 
   let one : t = Linear (Z.one, SymLinear.zero)
 

infer/src/bufferoverrun/bounds.mli

@@ -77,8 +77,12 @@ module Bound : sig
 
   val widen_l : t -> t -> t
 
+  val widen_l_thresholds : thresholds:Z.t list -> t -> t -> t
+
   val widen_u : t -> t -> t
 
+  val widen_u_thresholds : thresholds:Z.t list -> t -> t -> t
+
   val zero : t
 
   val one : t

infer/src/bufferoverrun/itv.ml

@@ -94,6 +94,11 @@ module ItvPure = struct
    fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> (Bound.widen_l l1 l2, Bound.widen_u u1 u2)
 
 
+  let widen_thresholds : thresholds:Z.t list -> prev:t -> next:t -> num_iters:int -> t =
+   fun ~thresholds ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ ->
+    (Bound.widen_l_thresholds ~thresholds l1 l2, Bound.widen_u_thresholds ~thresholds u1 u2)
+
+
   let pp_mark : markup:bool -> F.formatter -> t -> unit =
    fun ~markup fmt (l, u) ->
     if Bound.equal l u then Bound.pp_mark ~markup fmt l
@@ -437,6 +442,20 @@ end
 
 include AbstractDomain.BottomLifted (ItvPure)
 
+let widen_thresholds ~thresholds ~prev:prev0 ~next:next0 ~num_iters =
+  if phys_equal prev0 next0 then prev0
+  else
+    match (prev0, next0) with
+    | Bottom, _ ->
+        next0
+    | _, Bottom ->
+        prev0
+    | NonBottom prev, NonBottom next ->
+        PhysEqual.optim2
+          ~res:(NonBottom (ItvPure.widen_thresholds ~thresholds ~prev ~next ~num_iters))
+          prev0 next0
+
+
 let compare : t -> t -> int =
  fun x y ->
   match (x, y) with

infer/src/bufferoverrun/itv.mli

@@ -102,6 +102,8 @@ end
 
 include module type of AbstractDomain.BottomLifted (ItvPure)
 
+val widen_thresholds : thresholds:Z.t list -> prev:t -> next:t -> num_iters:int -> t
+
 val compare : t -> t -> int
 
 val bot : t

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

@@ -78,9 +78,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, no_buc
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,<Offset trace>,Parameter `i`,<Length trace>,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector_access_at` ]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter1_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
-codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: [0, +oo] Size: 5]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
-codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: [0, +oo] Size: 11]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_front_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]

infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp

@@ -68,8 +68,7 @@ void array_iter1_Bad() {
   a[a[0]] = 0;
 }
 
-// TODO: Inferbo should give a preciser widening threshold.
+void array_iter2_Good() {
-void array_iter2_Good_FP() {
   std::array<int, 11> a;
   for (auto it = a.begin(); it != a.end(); ++it) {
     *it = 10;