[inferbo] Add symbol for unsigned int

Summary: This commit adds unsigned symbol for preciser analysis results with less number of uses of min/max operators.

Reviewed By: mbouaziz

Differential Revision: D6040437

fbshipit-source-id: 999ca4c

infer/src/bufferoverrun/itv.ml

@@ -18,22 +18,33 @@ module L = Logging
 exception Not_one_symbol
 
 module Symbol = struct
-  type t = Typ.Procname.t * int [@@deriving compare]
+  type t = {pname: Typ.Procname.t; id: int; unsigned: bool} [@@deriving compare]
 
   let eq = [%compare.equal : t]
 
-  let make : Typ.Procname.t -> int -> t = fun pname i -> (pname, i)
+  let make : unsigned:bool -> Typ.Procname.t -> int -> t =
+    fun ~unsigned pname id -> {pname; id; unsigned}
 
   let pp : F.formatter -> t -> unit =
-    fun fmt x ->
+    fun fmt {pname; id; unsigned} ->
-      if Config.bo_debug <= 1 then F.fprintf fmt "s$%d" (snd x)
+      let symbol_name = if unsigned then "u" else "s" in
-      else F.fprintf fmt "%s-s$%d" (fst x |> Typ.Procname.to_string) (snd x)
+      if Config.bo_debug <= 1 then F.fprintf fmt "%s$%d" symbol_name id
+      else F.fprintf fmt "%s-%s$%d" (Typ.Procname.to_string pname) symbol_name id
+
+  let is_unsigned : t -> bool = fun x -> x.unsigned
 end
 
 module SubstMap = Caml.Map.Make (Symbol)
 
 module SymLinear = struct
-  module M = Caml.Map.Make (Symbol)
+  module M = struct
+    include Caml.Map.Make (Symbol)
+
+    let for_all2 : (key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool =
+      fun cond x y ->
+        let merge_function k x y = if cond k x y then None else raise Exit in
+        match merge merge_function x y with _ -> true | exception Exit -> false
+  end
 
   type t = int M.t [@@deriving compare]
 
@@ -60,10 +71,22 @@ module SymLinear = struct
       try M.find s x
       with Not_found -> 0
 
-  let le : t -> t -> bool = fun x y -> M.for_all (fun s v -> v <= find s y) x
+  let is_le_zero : t -> bool =
+    fun x -> M.for_all (fun s v -> Int.equal v 0 || Symbol.is_unsigned s && v <= 0) x
 
+  let is_ge_zero : t -> bool =
+    fun x -> M.for_all (fun s v -> Int.equal v 0 || Symbol.is_unsigned s && v >= 0) x
+
+  let le : t -> t -> bool =
+    fun x y ->
+      let le_one_pair s v1_opt v2_opt =
+        let v1, v2 = (Option.value v1_opt ~default:0, Option.value v2_opt ~default:0) in
+        Int.equal v1 v2 || Symbol.is_unsigned s && v1 <= v2
+      in
+      M.for_all2 le_one_pair x y
 
-  let make : Typ.Procname.t -> int -> t = fun pname i -> M.add (Symbol.make pname i) 1 empty
+  let make : unsigned:bool -> Typ.Procname.t -> int -> t =
+    fun ~unsigned pname i -> M.add (Symbol.make ~unsigned pname i) 1 empty
 
   let eq : t -> t -> bool = fun x y -> le x y && le y x
 
@@ -195,7 +218,7 @@ module Bound = struct
         | PInf
          -> F.fprintf fmt "+oo"
         | Linear (c, x)
-         -> if SymLinear.le x SymLinear.empty then F.fprintf fmt "%d" c
+         -> if SymLinear.is_zero x then F.fprintf fmt "%d" c
             else if Int.equal c 0 then F.fprintf fmt "%a" SymLinear.pp x
             else F.fprintf fmt "%a + %d" SymLinear.pp x c
         | MinMax (c, sign, m, d, x)
@@ -249,6 +272,21 @@ module Bound = struct
 
   let is_mone_symbol : t -> bool = fun x -> get_mone_symbol_opt x <> None
 
+  let mk_MinMax (c, sign, m, d, s) =
+    if Symbol.is_unsigned s then
+      match m with
+      | Min when d <= 0 -> (
+        match sign with Plus -> of_int (c + d) | Minus -> of_int (c - d) )
+      | Max when d <= 0 -> (
+        match sign with
+        | Plus
+         -> Linear (c, SymLinear.singleton s 1)
+        | Minus
+         -> Linear (c, SymLinear.singleton s (-1)) )
+      | _
+       -> MinMax (c, sign, m, d, s)
+    else MinMax (c, sign, m, d, s)
+
   let use_symbol : Symbol.t -> t -> bool =
     fun s ->
       function
@@ -304,37 +342,35 @@ module Bound = struct
             | MinMax (c1, Minus, Max, d1, _), Linear (c2, se) when SymLinear.is_zero se
              -> Linear (c1 - max d1 c2, SymLinear.zero)
             | MinMax (c, sign, m, d, _), _ when is_one_symbol y
-             -> MinMax (c, sign, m, d, get_one_symbol y)
+             -> mk_MinMax (c, sign, m, d, get_one_symbol y)
             | MinMax (c, sign, m, d, _), _ when is_mone_symbol y
-             -> MinMax (c, neg_sign sign, neg_min_max m, -d, get_mone_symbol y)
+             -> mk_MinMax (c, neg_sign sign, neg_min_max m, -d, get_mone_symbol y)
             | MinMax (c1, Plus, Min, d1, _), MinMax (c2, Plus, Min, d2, s')
-             -> MinMax (c1 + c2, Plus, Min, min (d1 - c2) d2, s')
+             -> mk_MinMax (c1 + c2, Plus, Min, min (d1 - c2) d2, s')
             | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, s')
-             -> MinMax (c1 + c2, Plus, Max, max (d1 - c2) d2, s')
+             -> mk_MinMax (c1 + c2, Plus, Max, max (d1 - c2) d2, s')
             | MinMax (c1, Minus, Min, d1, _), MinMax (c2, Plus, Min, d2, s')
-             -> MinMax (c1 - c2, Minus, Min, min (d1 - c2) d2, s')
+             -> mk_MinMax (c1 - c2, Minus, Min, min (d1 - c2) d2, s')
             | MinMax (c1, Minus, Max, d1, _), MinMax (c2, Plus, Max, d2, s')
-             -> MinMax (c1 - c2, Minus, Max, max (d1 - c2) d2, s')
+             -> mk_MinMax (c1 - c2, Minus, Max, max (d1 - c2) d2, s')
             | MinMax (c1, Plus, Min, d1, _), MinMax (c2, Minus, Max, d2, s')
-             -> MinMax (c1 + c2, Minus, Max, max (-d1 + c2) d2, s')
+             -> mk_MinMax (c1 + c2, Minus, Max, max (-d1 + c2) d2, s')
             | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Minus, Min, d2, s')
-             -> MinMax (c1 + c2, Minus, Min, min (-d1 + c2) d2, s')
+             -> mk_MinMax (c1 + c2, Minus, Min, min (-d1 + c2) d2, s')
             | MinMax (c1, Minus, Min, d1, _), MinMax (c2, Minus, Max, d2, s')
-             -> MinMax (c1 - c2, Minus, Max, max (-d1 + c2) d2, s')
+             -> mk_MinMax (c1 - c2, Minus, Max, max (-d1 + c2) d2, s')
             | MinMax (c1, Minus, Max, d1, _), MinMax (c2, Minus, Min, d2, s')
-             -> MinMax (c1 - c2, Minus, Min, min (-d1 + c2) d2, s')
+             -> mk_MinMax (c1 - c2, Minus, Min, min (-d1 + c2) d2, s')
             | _
              -> default
           in
           NonBottom res
 
-  (* substitution symbols in ``x'' with respect to ``map'' *)
-  let subst : default:t -> t -> t bottom_lifted SubstMap.t -> t bottom_lifted =
-    fun ~default x map -> SubstMap.fold (fun s y x -> subst1 ~default x s y) map (NonBottom x)
-
   let int_ub_of_minmax = function
     | MinMax (c, Plus, Min, d, _)
      -> Some (c + d)
+    | MinMax (c, Minus, Max, d, s) when Symbol.is_unsigned s
+     -> Some (min c (c - d))
     | MinMax (c, Minus, Max, d, _)
      -> Some (c - d)
     | MinMax _
@@ -343,6 +379,8 @@ module Bound = struct
      -> assert false
 
   let int_lb_of_minmax = function
+    | MinMax (c, Plus, Max, d, s) when Symbol.is_unsigned s
+     -> Some (max c (c + d))
     | MinMax (c, Plus, Max, d, _)
      -> Some (c + d)
     | MinMax (c, Minus, Min, d, _)
@@ -387,7 +425,7 @@ module Bound = struct
       | _, MInf | PInf, _
        -> false
       | Linear (c0, x0), Linear (c1, x1)
-       -> c0 <= c1 && SymLinear.eq x0 x1
+       -> c0 <= c1 && SymLinear.le x0 x1
       | MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2)
         when sign_equal sign1 sign2 && min_max_equal m1 m2
        -> c1 <= c2 && Int.equal d1 d2 && Symbol.eq x1 x2
@@ -396,14 +434,12 @@ module Bound = struct
       | MinMax (c1, Plus, Min, _, x1), MinMax (c2, Plus, Max, _, x2)
       | MinMax (c1, Minus, Max, _, x1), MinMax (c2, Minus, Min, _, x2)
        -> c1 <= c2 && Symbol.eq x1 x2
-      | MinMax _, Linear (c, se) when SymLinear.is_zero se
+      | MinMax _, Linear (c, se)
-       -> le_opt1 ( <= ) (int_ub_of_minmax x) c
+       -> SymLinear.is_ge_zero se && le_opt1 ( <= ) (int_ub_of_minmax x) c
-      | MinMax _, Linear _
+          || le_opt1 le (linear_ub_of_minmax x) y
-       -> le_opt1 le (linear_ub_of_minmax x) y
+      | Linear (c, se), MinMax _
-      | Linear (c, se), MinMax _ when SymLinear.is_zero se
+       -> SymLinear.is_le_zero se && le_opt2 ( <= ) c (int_lb_of_minmax y)
-       -> le_opt2 ( <= ) c (int_lb_of_minmax y)
+          || le_opt2 le x (linear_lb_of_minmax y)
-      | Linear _, MinMax _
-       -> le_opt2 le x (linear_lb_of_minmax y)
       | _, _
        -> false
 
@@ -415,7 +451,7 @@ module Bound = struct
       | Linear (c, x), _
        -> le (Linear (c + 1, x)) y
       | MinMax (c, sign, min_max, d, x), _
-       -> le (MinMax (c + 1, sign, min_max, d, x)) y
+       -> le (mk_MinMax (c + 1, sign, min_max, d, x)) y
       | _, _
        -> false
 
@@ -453,29 +489,29 @@ module Bound = struct
       else
         match (x, y) with
         | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2
-         -> MinMax (c2, Plus, Min, c1 - c2, SymLinear.get_one_symbol x2)
+         -> mk_MinMax (c2, Plus, Min, c1 - c2, SymLinear.get_one_symbol x2)
         | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2
-         -> MinMax (c1, Plus, Min, c2 - c1, SymLinear.get_one_symbol x1)
+         -> mk_MinMax (c1, Plus, Min, c2 - c1, SymLinear.get_one_symbol x1)
         | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2
-         -> MinMax (c2, Minus, Max, c2 - c1, SymLinear.get_mone_symbol x2)
+         -> mk_MinMax (c2, Minus, Max, c2 - c1, SymLinear.get_mone_symbol x2)
         | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2
-         -> MinMax (c1, Minus, Max, c1 - c2, SymLinear.get_mone_symbol x1)
+         -> mk_MinMax (c1, Minus, Max, 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
-         -> MinMax (c1, Plus, Min, min d1 (c2 - c1), s)
+         -> mk_MinMax (c1, Plus, Min, min d1 (c2 - c1), s)
         | MinMax (c1, Plus, Max, _, s), Linear (c2, se)
         | Linear (c2, se), MinMax (c1, Plus, Max, _, s)
           when SymLinear.is_zero se
-         -> MinMax (c1, Plus, Min, c2 - c1, s)
+         -> mk_MinMax (c1, Plus, Min, c2 - c1, s)
         | MinMax (c1, Minus, Min, _, s), Linear (c2, se)
         | Linear (c2, se), MinMax (c1, Minus, Min, _, s)
           when SymLinear.is_zero se
-         -> MinMax (c1, Minus, Max, c1 - c2, s)
+         -> mk_MinMax (c1, Minus, Max, c1 - c2, s)
         | MinMax (c1, Minus, Max, d1, s), Linear (c2, se)
         | Linear (c2, se), MinMax (c1, Minus, Max, d1, s)
           when SymLinear.is_zero se
-         -> MinMax (c1, Minus, Max, max d1 (c1 - c2), s)
+         -> mk_MinMax (c1, Minus, Max, max d1 (c1 - c2), s)
         | MinMax (_, Plus, Min, _, _), MinMax (_, Plus, Max, _, _)
         | MinMax (_, Plus, Min, _, _), MinMax (_, Minus, Min, _, _)
         | MinMax (_, Minus, Max, _, _), MinMax (_, Plus, Max, _, _)
@@ -491,22 +527,22 @@ module Bound = struct
         | _, _
          -> default
 
-  let ub : t -> t -> t =
+  let ub : ?default:t -> t -> t -> t =
-    fun x y ->
+    fun ?(default= PInf) 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
-         -> MinMax (c2, Plus, Max, c1 - c2, SymLinear.get_one_symbol x2)
+         -> mk_MinMax (c2, Plus, Max, c1 - c2, SymLinear.get_one_symbol x2)
         | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2
-         -> MinMax (c1, Plus, Max, c2 - c1, SymLinear.get_one_symbol x1)
+         -> mk_MinMax (c1, Plus, Max, c2 - c1, SymLinear.get_one_symbol x1)
         | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2
-         -> MinMax (c2, Minus, Min, c2 - c1, SymLinear.get_mone_symbol x2)
+         -> mk_MinMax (c2, Minus, Min, c2 - c1, SymLinear.get_mone_symbol x2)
         | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2
-         -> MinMax (c1, Minus, Min, c1 - c2, SymLinear.get_mone_symbol x1)
+         -> mk_MinMax (c1, Minus, Min, c1 - c2, SymLinear.get_mone_symbol x1)
         | _, _
-         -> PInf
+         -> default
 
   let widen_l : t -> t -> t =
     fun x y ->
@@ -538,6 +574,21 @@ module Bound = struct
   let is_const : t -> int option =
     fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None
 
+  (* substitution symbols in ``x'' with respect to ``map'' *)
+  let subst : default:t -> t -> t bottom_lifted SubstMap.t -> t bottom_lifted =
+    fun ~default x map ->
+      let subst_helper s y x =
+        let y' =
+          match y with
+          | Bottom
+           -> Bottom
+          | NonBottom r
+           -> NonBottom (if Symbol.is_unsigned s then ub ~default:r zero r else r)
+        in
+        subst1 ~default x s y'
+      in
+      SubstMap.fold subst_helper map (NonBottom x)
+
   let plus_l : t -> t -> t =
     fun x y ->
       match (x, y) with
@@ -550,7 +601,7 @@ module Bound = struct
       | MinMax (c1, sign, min_max, d1, x1), Linear (c2, x2)
       | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1)
         when SymLinear.is_zero x2
-       -> MinMax (c1 + c2, sign, min_max, d1, x1)
+       -> mk_MinMax (c1 + c2, sign, min_max, d1, x1)
       | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2)
       | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _)
        -> Linear (c1 + d1 + c2, x2)
@@ -572,7 +623,7 @@ module Bound = struct
       | MinMax (c1, sign, min_max, d1, x1), Linear (c2, x2)
       | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1)
         when SymLinear.is_zero x2
-       -> MinMax (c1 + c2, sign, min_max, d1, x1)
+       -> mk_MinMax (c1 + c2, sign, min_max, d1, x1)
       | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2)
       | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _)
        -> Linear (c1 + d1 + c2, x2)
@@ -619,7 +670,7 @@ module Bound = struct
     | Linear (c, x)
      -> Some (Linear (-c, SymLinear.neg x))
     | MinMax (c, sign, min_max, d, x)
-     -> Some (MinMax (-c, neg_sign sign, min_max, d, x))
+     -> Some (mk_MinMax (-c, neg_sign sign, min_max, d, x))
 
   let get_symbols : t -> Symbol.t list = function
     | MInf | PInf
@@ -724,12 +775,8 @@ module ItvPure = struct
 
   let make_sym : unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t =
     fun ~unsigned pname new_sym_num ->
-      let lower =
+      let lower = Bound.of_sym (SymLinear.make ~unsigned pname (new_sym_num ())) in
-        if unsigned then
+      let upper = Bound.of_sym (SymLinear.make ~unsigned pname (new_sym_num ())) in
-          Bound.MinMax (0, Bound.Plus, Bound.Max, 0, Symbol.make pname (new_sym_num ()))
-        else Bound.of_sym (SymLinear.make pname (new_sym_num ()))
-      in
-      let upper = Bound.of_sym (SymLinear.make pname (new_sym_num ())) in
       (lower, upper)
 
   let m1_255 = (Bound.minus_one, Bound._255)
@@ -911,21 +958,21 @@ module ItvPure = struct
       | (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when SymLinear.eq s1 s2
        -> (l1, Bound.Linear (min c1 c2, s1))
       | (l1, Bound.Linear (c, se)), (_, u) when SymLinear.is_zero se && Bound.is_one_symbol u
-       -> (l1, Bound.MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
+       -> (l1, Bound.mk_MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
       | (l1, u), (_, Bound.Linear (c, se)) when SymLinear.is_zero se && Bound.is_one_symbol u
-       -> (l1, Bound.MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
+       -> (l1, Bound.mk_MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
       | (l1, Bound.Linear (c, se)), (_, u) when SymLinear.is_zero se && Bound.is_mone_symbol u
-       -> (l1, Bound.MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u))
+       -> (l1, Bound.mk_MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u))
       | (l1, u), (_, Bound.Linear (c, se)) when SymLinear.is_zero se && Bound.is_mone_symbol u
-       -> (l1, Bound.MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u))
+       -> (l1, Bound.mk_MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u))
       | (l1, Bound.Linear (c1, se)), (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se'))
       | (l1, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se')), (_, Bound.Linear (c1, se))
         when SymLinear.is_zero se
-       -> (l1, Bound.MinMax (c2, Bound.Plus, Bound.Min, min (c1 - c2) d2, se'))
+       -> (l1, Bound.mk_MinMax (c2, Bound.Plus, Bound.Min, min (c1 - c2) d2, se'))
       | ( (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, d1, se1))
         , (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se2)) )
         when Int.equal c1 c2 && Symbol.eq se1 se2
-       -> (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, min d1 d2, se1))
+       -> (l1, Bound.mk_MinMax (c1, Bound.Plus, Bound.Min, min d1 d2, se1))
       | _
        -> x
 
@@ -937,21 +984,21 @@ module ItvPure = struct
       | (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when SymLinear.eq s1 s2
        -> (Bound.Linear (max c1 c2, s1), u1)
       | (Bound.Linear (c, se), u1), (l, _) when SymLinear.is_zero se && Bound.is_one_symbol l
-       -> (Bound.MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
+       -> (Bound.mk_MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
       | (l, u1), (Bound.Linear (c, se), _) when SymLinear.is_zero se && Bound.is_one_symbol l
-       -> (Bound.MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
+       -> (Bound.mk_MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
       | (Bound.Linear (c, se), u1), (l, _) when SymLinear.is_zero se && Bound.is_mone_symbol l
-       -> (Bound.MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
+       -> (Bound.mk_MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
       | (l, u1), (Bound.Linear (c, se), _) when SymLinear.is_zero se && Bound.is_mone_symbol l
-       -> (Bound.MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
+       -> (Bound.mk_MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
       | (Bound.Linear (c1, se), u1), (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), _)
       | (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), u1), (Bound.Linear (c1, se), _)
         when SymLinear.is_zero se
-       -> (Bound.MinMax (c2, Bound.Plus, Bound.Max, max (c1 - c2) d2, se'), u1)
+       -> (Bound.mk_MinMax (c2, Bound.Plus, Bound.Max, max (c1 - c2) d2, se'), u1)
       | ( (Bound.MinMax (c1, Bound.Plus, Bound.Max, d1, se1), u1)
         , (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se2), _) )
         when Int.equal c1 c2 && Symbol.eq se1 se2
-       -> (Bound.MinMax (c1, Bound.Plus, Bound.Max, max d1 d2, se1), u1)
+       -> (Bound.mk_MinMax (c1, Bound.Plus, Bound.Max, max d1 d2, se1), u1)
       | _
        -> x
 

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

@@ -7,13 +7,15 @@ codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, [Call,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN_L5, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_u_FP, 5, BUFFER_OVERRUN_S2, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1+max(1, s$8), -1+max(1, s$9)] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, [Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ]
-codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
+codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$12, u$13] Size: [u$12, u$13]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, []

infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp

@@ -75,12 +75,12 @@ struct LM {
   typedef LMB<T> B;
   void l(lt& t, const lo& o) { lI(t, o); }
   void tL(lt& t, const lo& o) { lI(t, o); }
-  void u(lt& t, const lo& o) {
+  void u_FP(lt& t, const lo& o) {
     ASSERT(fB(o) == t.bI);
     if (t.bI == kBN) {
       return;
     }
-    uI(t.bI, o);
+    uI_FP(t.bI, o);
     t.bI = kBN;
   }
 
@@ -95,7 +95,7 @@ struct LM {
     }
     t.bI = bi;
   }
-  void uI(BI bi, const lo& o) { b[bi - 1]->u(o); }
+  void uI_FP(BI bi, const lo& o) { b[bi - 1]->u(o); }
   std::vector<std::unique_ptr<B>> b;
 };
 
@@ -105,10 +105,10 @@ typedef TFM LMDM;
 
 static LM<LMDM>* al;
 
-static inline void ral(lt* t, ai a) {
+static inline void ral_FP(lt* t, ai a) {
   ASSERT(t);
   lo o = alo(a);
-  al->u(*t, o);
+  al->u_FP(*t, o);
 }
 
 static inline void gal(lt* t, ai a) {
@@ -135,10 +135,10 @@ struct arh {
   ft i1;
 };
 
-static void am_Good_FP(im* it) {
+static void am_Good(im* it) {
   const arh* ch = (const arh*)it->gKPC();
   const ai a = aft(ch->i1);
   lt at;
   gal(&at, a);
-  ral(&at, a);
+  ral_FP(&at, a);
 }

infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp

@@ -133,3 +133,13 @@ void call_safe_access5_Good() {
   std::vector<int> v;
   safe_access5(v);
 }
+
+void safe_access6(std::vector<int> v) {
+  std::vector<int> v2(2);
+  v2[v.empty()];
+}
+
+void call_safe_access6_Good() {
+  std::vector<int> v;
+  safe_access6(v);
+}