[inferbo] More precise min/max

Reviewed By: skcho

Differential Revision: D10386539

fbshipit-source-id: 15efa602d

infer/src/bufferoverrun/bounds.ml

@@ -198,6 +198,8 @@ module Bound = struct
 
     let eval_big_int x i1 i2 = match x with Plus -> Z.(i1 + i2) | Minus -> Z.(i1 - i2)
 
+    let eval_neg_if_minus x i = match x with Plus -> i | Minus -> Z.neg i
+
     let pp ~need_plus : F.formatter -> t -> unit =
      fun fmt -> function
       | Plus ->
@@ -306,10 +308,10 @@ module Bound = struct
   let big_int_ub_of_minmax = function
     | MinMax (c, Plus, Min, d, _) ->
         Some Z.(c + d)
-    | MinMax (c, Minus, Max, d, s) when Symb.Symbol.is_unsigned s ->
-        Some Z.(min c (c - d))
     | MinMax (c, Minus, Max, d, _) ->
         Some Z.(c - d)
+    | MinMax (c, Minus, Min, _, s) when Symb.Symbol.is_unsigned s ->
+        Some c
     | MinMax _ ->
         None
     | MInf | PInf | Linear _ ->
@@ -317,12 +319,12 @@ module Bound = struct
 
 
   let big_int_lb_of_minmax = function
-    | MinMax (c, Plus, Max, d, s) when Symb.Symbol.is_unsigned s ->
-        Some Z.(max c (c + d))
     | MinMax (c, Plus, Max, d, _) ->
         Some Z.(c + d)
     | MinMax (c, Minus, Min, d, _) ->
         Some Z.(c - d)
+    | MinMax (c, Plus, Min, _, s) when Symb.Symbol.is_unsigned s ->
+        Some c
     | MinMax _ ->
         None
     | MInf | PInf | Linear _ ->
@@ -446,23 +448,30 @@ module Bound = struct
 
   let xcompare = PartialOrder.of_le ~le
 
-  let remove_max_int : t -> t =
-   fun x ->
-    match x with
-    | MinMax (c, Plus, Max, _, s) ->
-        Linear (c, SymLinear.singleton_one s)
-    | MinMax (c, Minus, Min, _, s) ->
-        Linear (c, SymLinear.singleton_minus_one s)
+  let is_const : t -> bool = function
+    | Linear (_, se) when SymLinear.is_zero se ->
+        true
     | _ ->
-        x
+        false
 
 
-  let rec lb : default:t -> t -> t -> t =
-   fun ~default x y ->
-    if le x y then x
-    else if le y x then y
+  let neg : t -> t = function
+    | MInf ->
+        PInf
+    | PInf ->
+        MInf
+    | Linear (c, x) ->
+        Linear (Z.neg c, SymLinear.neg x)
+    | MinMax (c, sign, min_max, d, x) ->
+        mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x)
+
+
+  let exact_min : otherwise:(t -> t -> t) -> t -> t -> t =
+   fun ~otherwise b1 b2 ->
+    if le b1 b2 then b1
+    else if le b2 b1 then b2
     else
-      match (x, y) with
+      match (b1, b2) with
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 ->
           mk_MinMax (c2, Plus, Min, Z.(c1 - c2), SymLinear.get_one_symbol x2)
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 ->
@@ -473,70 +482,168 @@ module Bound = struct
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2
         ->
           mk_MinMax (c1, Minus, Max, Z.(c1 - c2), SymLinear.get_mone_symbol x1)
-      | MinMax (c1, Plus, Min, d1, s), Linear (c2, se)
-      | Linear (c2, se), MinMax (c1, Plus, Min, d1, s)
-        when SymLinear.is_zero se ->
-          mk_MinMax (c1, Plus, Min, Z.(min d1 (c2 - c1)), s)
-      | MinMax (c1, Plus, Max, _, s), Linear (c2, se)
-      | Linear (c2, se), MinMax (c1, Plus, Max, _, s)
+      | MinMax (c1, (Plus as sign), (Min as minmax), _, s), Linear (c2, se)
+      | Linear (c2, se), MinMax (c1, (Plus as sign), (Min as minmax), _, s)
+      | MinMax (c1, (Minus as sign), (Max as minmax), _, s), Linear (c2, se)
+      | Linear (c2, se), MinMax (c1, (Minus as sign), (Max as minmax), _, s)
         when SymLinear.is_zero se ->
-          mk_MinMax (c1, Plus, Min, Z.(c2 - c1), s)
-      | MinMax (c1, Minus, Min, _, s), Linear (c2, se)
-      | Linear (c2, se), MinMax (c1, Minus, Min, _, s)
-        when SymLinear.is_zero se ->
-          mk_MinMax (c1, Minus, Max, Z.(c1 - c2), s)
-      | MinMax (c1, Minus, Max, d1, s), Linear (c2, se)
-      | Linear (c2, se), MinMax (c1, Minus, Max, d1, s)
+          let d = Sign.eval_neg_if_minus sign Z.(c2 - c1) in
+          mk_MinMax (c1, sign, minmax, d, s)
+      | MinMax (c1, (Minus as sign), (Max as minmax), d1, s1), MinMax (c2, Minus, Max, d2, s2)
+      | MinMax (c1, (Plus as sign), (Min as minmax), d1, s1), MinMax (c2, Plus, Min, d2, s2)
+        when Symb.Symbol.equal s1 s2 ->
+          let v1 = Sign.eval_big_int sign c1 d1 in
+          let v2 = Sign.eval_big_int sign c2 d2 in
+          let c = Z.min c1 c2 in
+          let v = MinMax.eval_big_int minmax v1 v2 in
+          let d = Sign.eval_neg_if_minus sign Z.(v - c) in
+          mk_MinMax (c, sign, minmax, d, s1)
+      | b1, b2 ->
+          otherwise b1 b2
+
+
+  let rec underapprox_min b1 b2 =
+    exact_min b1 b2 ~otherwise:(fun b1 b2 ->
+        match (b1, b2) with
+        | MinMax (c1, sign, _, d1, _s), Linear (_c2, se)
+        | Linear (_c2, se), MinMax (c1, sign, _, d1, _s)
           when SymLinear.is_zero se ->
-          mk_MinMax (c1, Minus, Max, Z.(max d1 (c1 - c2)), s)
-      | MinMax (_, Plus, Min, _, _), MinMax (_, Plus, Max, _, _)
-      | MinMax (_, Plus, Min, _, _), MinMax (_, Minus, Min, _, _)
-      | MinMax (_, Minus, Max, _, _), MinMax (_, Plus, Max, _, _)
-      | MinMax (_, Minus, Max, _, _), MinMax (_, Minus, Min, _, _) ->
-          lb ~default x (remove_max_int y)
-      | MinMax (_, Plus, Max, _, _), MinMax (_, Plus, Min, _, _)
-      | MinMax (_, Minus, Min, _, _), MinMax (_, Plus, Min, _, _)
-      | MinMax (_, Plus, Max, _, _), MinMax (_, Minus, Max, _, _)
-      | MinMax (_, Minus, Min, _, _), MinMax (_, Minus, Max, _, _) ->
-          lb ~default (remove_max_int x) y
-      | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, _) ->
-          Linear (Z.(min (c1 + d1) (c2 + d2)), SymLinear.zero)
-      | _, _ ->
-          default
+            Linear (Sign.eval_big_int sign c1 d1, SymLinear.zero)
+            (*
+              There is no best abstraction, we could also use:
+              For Plus, Max: mk_MinMax (c1, Plus, Min, Z.(c2 - c1), s)
+              For Minus, Min: mk_MinMax (c1, Minus, Max, Z.(c1 - c2), s)
+            *)
+        | MinMax (_, Minus, Max, _, _), MinMax (_, Plus, Min, _, _)
+        | MinMax (_, Plus, Min, _, _), MinMax (_, Minus, Max, _, _) ->
+            fallback_underapprox_min b1 b2
+        | MinMax (c1, (Plus as sign1), Max, d1, _), MinMax (c2, (Minus as sign2), Min, d2, _)
+        | MinMax (c1, (Minus as sign1), Min, d1, _), MinMax (c2, (Plus as sign2), Max, d2, _) ->
+            let v1 = Sign.eval_big_int sign1 c1 d1 in
+            let v2 = Sign.eval_big_int sign2 c2 d2 in
+            Linear (Z.min v1 v2, SymLinear.zero)
+        | MinMax (c1, (Plus as sign), (Max as minmax), d1, s1), MinMax (c2, Plus, Max, d2, s2)
+        | MinMax (c1, (Minus as sign), (Min as minmax), d1, s1), MinMax (c2, Minus, Min, d2, s2)
+          when Symb.Symbol.equal s1 s2 ->
+            let v1 = Sign.eval_big_int sign c1 d1 in
+            let v2 = Sign.eval_big_int sign c2 d2 in
+            let v = Z.min v1 v2 in
+            let c = Z.min c1 c2 in
+            let d = Sign.eval_neg_if_minus sign Z.(v - c) in
+            mk_MinMax (c, sign, minmax, d, s1)
+        | ( MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1)
+          , MinMax (c2, (Plus as sign2), Max, d2, s2) )
+        | ( MinMax (c2, (Plus as sign2), Max, d2, s2)
+          , MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1) )
+        | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1)
+          , MinMax (c2, (Minus as sign2), Min, d2, s2) )
+        | ( MinMax (c2, (Minus as sign2), Min, d2, s2)
+          , MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1) )
+        | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1)
+          , MinMax (c2, (Plus as sign2), Max, d2, s2) )
+        | ( MinMax (c2, (Plus as sign2), (Max as minmax1), d2, s2)
+          , MinMax (c1, (Minus as sign1), Max, d1, s1) )
+        | ( MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1)
+          , MinMax (c2, (Minus as sign2), Min, d2, s2) )
+        | ( MinMax (c2, (Minus as sign2), (Min as minmax1), d2, s2)
+          , MinMax (c1, (Plus as sign1), Min, d1, s1) )
+          when Symb.Symbol.equal s1 s2 ->
+            let v1 = Sign.eval_big_int sign1 c1 d1 in
+            let v2 = Sign.eval_big_int sign2 c2 d2 in
+            let v = Z.min v1 v2 in
+            let d = Sign.eval_neg_if_minus sign1 Z.(v - c1) in
+            mk_MinMax (c1, sign1, minmax1, d, s1)
+        | b1, b2 ->
+            fallback_underapprox_min b1 b2 )
+
+
+  and fallback_underapprox_min b1 b2 =
+    match big_int_lb b2 with
+    | Some v2 when not (is_const b2) ->
+        underapprox_min b1 (Linear (v2, SymLinear.zero))
+    | _ -> (
+      match big_int_lb b1 with
+      | Some v1 when not (is_const b1) ->
+          underapprox_min (Linear (v1, SymLinear.zero)) b2
+      | _ ->
+          MInf )
 
 
-  (** underapproximation of min b1 b2 *)
-  let min_l b1 b2 = lb ~default:MInf b1 b2
+  let overapprox_min original_b1 b2 =
+    let rec overapprox_min b1 b2 =
+      exact_min b1 b2 ~otherwise:(fun b1 b2 ->
+          match (b1, b2) with
+          | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1)
+            , MinMax (c2, (Plus as sign2), Min, d2, s2) )
+          | ( MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1)
+            , MinMax (c2, (Minus as sign2), Max, d2, s2) )
+            when Symb.Symbol.equal s1 s2 ->
+              let v1 = Sign.eval_big_int sign1 c1 d1 in
+              let v2 = Sign.eval_big_int sign2 c2 d2 in
+              let vmeet = Z.(shift_right (c1 + c2 + one) 1) in
+              let v = Z.(min vmeet (min v1 v2)) in
+              let d = Sign.eval_neg_if_minus sign1 Z.(v - c1) in
+              mk_MinMax (c1, sign1, minmax1, d, s1)
+          | MinMax (c1, (Minus as sign1), Max, d1, s1), MinMax (c2, (Plus as sign2), Min, d2, s2)
+          | MinMax (c1, (Minus as sign1), Min, d1, s1), MinMax (c2, (Plus as sign2), Max, d2, s2)
+          | MinMax (c1, (Plus as sign1), Min, d1, s1), MinMax (c2, (Minus as sign2), Max, d2, s2)
+          | MinMax (c1, (Plus as sign1), Max, d1, s1), MinMax (c2, (Minus as sign2), Min, d2, s2)
+            when Symb.Symbol.equal s1 s2 ->
+              let v1 = Sign.eval_big_int sign1 c1 d1 in
+              let v2 = Sign.eval_big_int sign2 c2 d2 in
+              let vmeet = Z.(shift_right (c1 + c2 + one) 1) in
+              Linear (Z.(max vmeet (max v1 v2)), SymLinear.zero)
+          | (MinMax (_, Plus, Min, _, s1) as b), MinMax (_, Plus, Max, _, s2)
+          | MinMax (_, Plus, Max, _, s2), (MinMax (_, Plus, Min, _, s1) as b)
+          | (MinMax (_, Minus, Min, _, s1) as b), MinMax (_, Minus, Max, _, s2)
+          | MinMax (_, Minus, Max, _, s2), (MinMax (_, Minus, Min, _, s1) as b)
+            when Symb.Symbol.equal s1 s2 ->
+              b
+          | MinMax (c1, Plus, Max, _, s1), MinMax (c2, Plus, Max, _, s2)
+          | MinMax (c1, Minus, Min, _, s1), MinMax (c2, Minus, Min, _, s2)
+            when Symb.Symbol.equal s1 s2 ->
+              if Z.leq c1 c2 then b1 else b2
+          | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1)
+            , MinMax (c2, (Plus as sign2), Max, d2, s2) )
+          | ( MinMax (c2, (Plus as sign2), (Max as minmax1), d2, s2)
+            , MinMax (c1, (Minus as sign1), Max, d1, s1) )
+          | ( MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1)
+            , MinMax (c2, (Minus as sign2), Min, d2, s2) )
+          | ( MinMax (c2, (Minus as sign2), (Min as minmax1), d2, s2)
+            , MinMax (c1, (Plus as sign1), Min, d1, s1) )
+            when Symb.Symbol.equal s1 s2 ->
+              let v1 = Sign.eval_big_int sign1 c1 d1 in
+              let v2 = Sign.eval_big_int sign2 c2 d2 in
+              let vmin, vmax = if Z.leq v1 v2 then (v1, v2) else (v2, v1) in
+              let vmeet = Z.(shift_right (c1 + c2 + one) 1) in
+              let v = if Z.leq vmin vmeet && Z.leq vmeet vmax then vmeet else vmax in
+              let d = Sign.eval_neg_if_minus sign1 Z.(v - c1) in
+              mk_MinMax (c1, sign1, minmax1, d, s1)
+          | _ -> (
+            match big_int_ub b2 with
+            | Some v2 when not (is_const b2) ->
+                overapprox_min b1 (Linear (v2, SymLinear.zero))
+            | _ -> (
+              match big_int_ub b1 with
+              | Some v1 when not (is_const b1) ->
+                  overapprox_min (Linear (v1, SymLinear.zero)) b2
+              | _ ->
+                  (* When the result is not representable, our best effort is to return the first original argument. Any other deterministic heuristics would work too. *)
+                  original_b1 ) ) )
+    in
+    overapprox_min original_b1 b2
 
-  (** overapproximation of min b1 b2 *)
-  let min_u b1 b2 =
-    lb
-      ~default:
-        (* When the result is not representable, our best effort is to return the first argument. Any other deterministic heuristics would work too. *)
-        b1 b1 b2
 
+  let underapprox_max b1 b2 = neg (overapprox_min (neg b1) (neg b2))
 
-  let ub : default:t -> t -> t -> t =
-   fun ~default x y ->
-    if le x y then y
-    else if le y x then x
-    else
-      match (x, y) with
-      | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 ->
-          mk_MinMax (c2, Plus, Max, Z.(c1 - c2), SymLinear.get_one_symbol x2)
-      | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 ->
-          mk_MinMax (c1, Plus, Max, Z.(c2 - c1), SymLinear.get_one_symbol x1)
-      | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2
-        ->
-          mk_MinMax (c2, Minus, Min, Z.(c2 - c1), SymLinear.get_mone_symbol x2)
-      | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2
-        ->
-          mk_MinMax (c1, Minus, Min, Z.(c1 - c2), SymLinear.get_mone_symbol x1)
-      | _, _ ->
-          default
+  let overapprox_max b1 b2 = neg (underapprox_min (neg b1) (neg b2))
 
+  let approx_max = function
+    | Symb.BoundEnd.LowerBound ->
+        underapprox_max
+    | Symb.BoundEnd.UpperBound ->
+        overapprox_max
 
-  let max_u : t -> t -> t = ub ~default:PInf
 
   let widen_l : t -> t -> t =
    fun x y ->
@@ -656,17 +763,6 @@ module Bound = struct
 
   let mult_const_u = mult_const Symb.BoundEnd.UpperBound
 
-  let neg : t -> t = function
-    | MInf ->
-        PInf
-    | PInf ->
-        MInf
-    | Linear (c, x) ->
-        Linear (Z.neg c, SymLinear.neg x)
-    | MinMax (c, sign, min_max, d, x) ->
-        mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x)
-
-
   let div_const : t -> NonZeroInt.t -> t option =
    fun x n ->
     match x with
@@ -727,7 +823,7 @@ module Bound = struct
     let get s =
       match eval_sym s with
       | NonBottom x when Symb.Symbol.is_unsigned s ->
-          NonBottom (ub ~default:x zero x)
+          NonBottom (approx_max subst_pos x zero)
       | x ->
           x
     in
@@ -745,7 +841,8 @@ module Bound = struct
               Bottom )
         | NonBottom x ->
             let x = mult_const subst_pos coeff x in
-            if Symb.Symbol.is_unsigned s then NonBottom (ub ~default:x zero x) else NonBottom x
+            if Symb.Symbol.is_unsigned s then NonBottom (approx_max subst_pos x zero)
+            else NonBottom x
     in
     match x with
     | MInf | PInf ->

infer/src/bufferoverrun/bounds.mli

@@ -81,11 +81,11 @@ module Bound : sig
 
   val xcompare : t PartialOrder.xcompare
 
-  val min_l : t -> t -> t
+  val underapprox_min : t -> t -> t
 
-  val min_u : t -> t -> t
+  val overapprox_min : t -> t -> t
 
-  val max_u : t -> t -> t
+  val overapprox_max : t -> t -> t
 
   val widen_l : t -> t -> t
 

infer/src/bufferoverrun/itv.ml

@@ -501,7 +501,9 @@ module ItvPure = struct
         `RightSubsumesLeft
 
 
-  let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.min_l l1 l2, Bound.max_u u1 u2)
+  let join : t -> t -> t =
+   fun (l1, u1) (l2, u2) -> (Bound.underapprox_min l1 l2, Bound.overapprox_max u1 u2)
+
 
   let widen : prev:t -> next:t -> num_iters:int -> t =
    fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> (Bound.widen_l l1 l2, Bound.widen_u u1 u2)
@@ -729,7 +731,9 @@ module ItvPure = struct
     else Boolean.Top
 
 
-  let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.min_l l1 l2, Bound.min_u u1 u2)
+  let min_sem : t -> t -> t =
+   fun (l1, u1) (l2, u2) -> (Bound.underapprox_min l1 l2, Bound.overapprox_min u1 u2)
+
 
   let is_invalid : t -> bool = function
     | Bound.PInf, _ | _, Bound.MInf ->

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

@@ -105,6 +105,9 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVE
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
+codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
+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.lb), -1] Size: 1]
+codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, []
 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]
@@ -153,9 +156,8 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 7, CONDITION_AL
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 11, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
-codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [0, +oo] Size: 17]
-codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Return,Assignment,Binop: ([-1, +oo] + 1):signed32]
-codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex_200_Good_FP, 4, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [0, +oo] Size: 16]
+codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [-28, 16] Size: 17]
+codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [-28, 16] Size: 17]
 codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1]

infer/tests/codetoanalyze/c/bufferoverrun/minmax.c

@@ -0,0 +1,40 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int exact_min_minus_min_linear_CAF(int x) {
+  int size1[1];
+  int y = 28;
+  if (x < 5)
+    y = x + 10;
+  // y = [10 + min(18, x), 28]
+  if (y > 28) {
+    size1[-1] = 0;
+  }
+  return y;
+}
+
+int underapprox_min_minus_min_linear_CAF(int x) {
+  int size1[1];
+  int y = 10;
+  if (x < 5)
+    y = x + 20;
+  // y = [20 + min(-10, x), 24]
+  if (y > 24) {
+    size1[-1] = 0;
+  }
+  return y;
+}
+
+void exact_min_plus_min_plus_min_UNDERRUN(int x, int b) {
+  int size1[1];
+  int y = exact_min_minus_min_linear_CAF(x);
+  if (b)
+    y = underapprox_min_minus_min_linear_CAF(x);
+  y -= 29;
+  // [-19 + min(0, x), -1]
+  size1[y] = 0;
+}

infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c

@@ -61,7 +61,7 @@ void call_fromHex_sym_Good(char c) {
   }
 }
 
-void call_fromHex_200_Good_FP() {
+void call_fromHex_200_Good() {
   char arr[16];
   int idx = fromHex(200);
   if (idx >= 0) {
@@ -69,7 +69,7 @@ void call_fromHex_200_Good_FP() {
   }
 }
 
-void call_fromHex2_sym_Good(char c) {
+void call_fromHex2_sym_Good_FP(char c) {
   char arr[17];
   int idx = fromHex(c);
   arr[idx + 1] = 'H';