[Inferbo] Extend abstract domain for vector::empty

Summary:
The interval bound of the abstract domain is extended.
`[min|max](int, symbol)` => `int [+|-] [min|max](int, symbol)`

As a result, `vector::empty` can be modelled to return a more precise value: `1 - min(1, size)`.

Reviewed By: mbouaziz

Differential Revision: D5899404

fbshipit-source-id: c8c3f49

infer/models/cpp/include/infer_model/vector_bufferoverrun.h

@@ -27,6 +27,10 @@
 #include <algorithm>
 #endif
 
+extern "C" {
+int __inferbo_min(int, int);
+}
+
 INFER_NAMESPACE_STD_BEGIN
 
 struct bool_ref {
@@ -212,7 +216,7 @@ class vector {
 
   size_type capacity() const noexcept {}
 
-  bool empty() const noexcept { return infer_size == 0; }
+  bool empty() const noexcept { return 1 - __inferbo_min(infer_size, 1); }
   size_type max_size() const noexcept;
   void reserve(size_type __n);
   void shrink_to_fit() noexcept;

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -80,6 +80,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     fun pname ret params node location mem ->
       model_malloc pname ret (List.tl_exn params) node location mem
 
+  let model_min
+      : (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> Location.t -> Dom.Mem.astate
+        -> Dom.Mem.astate =
+    fun ret params location mem ->
+      match (ret, params) with
+      | Some (id, _), [(e1, _); (e2, _)]
+       -> let i1 = Sem.eval e1 mem location |> Dom.Val.get_itv in
+          let i2 = Sem.eval e2 mem location |> Dom.Val.get_itv in
+          let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in
+          mem |> Dom.Mem.add_stack (Loc.of_id id) v
+      | _
+       -> mem
+
   let model_by_value value ret mem =
     match ret with
     | Some (id, _)
@@ -118,6 +131,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         -> CFG.node -> Dom.Mem.astate -> Location.t -> Dom.Mem.astate =
     fun pname ret callee_pname params node mem loc ->
       match Typ.Procname.get_method callee_pname with
+      | "__inferbo_min"
+       -> model_min ret params loc mem
       | "__exit" | "exit"
        -> Dom.Mem.Bottom
       | "fgetc"

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -492,7 +492,7 @@ module Make (CFG : ProcCfg.S) = struct
             if Int.equal coeff 1 then
               (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map)
             else assert false
-        | Itv.Bound.MinMax (Itv.Bound.Max, 0, symbol)
+        | Itv.Bound.MinMax (0, Itv.Bound.Plus, Itv.Bound.Max, 0, symbol)
          -> (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map)
         | _
          -> assert false

infer/src/bufferoverrun/itv.ml

@@ -16,6 +16,8 @@ module L = Logging
 
 let sym_size = ref 0
 
+exception Not_one_symbol
+
 module Symbol = struct
   type t = Typ.Procname.t * int [@@deriving compare]
 
@@ -58,6 +60,8 @@ module SymLinear = struct
 
   let initial : t = empty
 
+  let singleton : Symbol.t -> int -> t = M.singleton
+
   let find : Symbol.t -> t -> int =
     fun s x ->
       try M.find s x
@@ -132,34 +136,63 @@ module SymLinear = struct
 
   let div_const : t -> int -> t = fun x n -> M.map (( / ) n) x
 
-  (* Returns a symbol when the map contains only one symbol s with the
-     coefficient 1. *)
-  let one_symbol : t -> Symbol.t option =
-    fun x ->
+  (* Returns a symbol when the map contains only one symbol s with a
+     given coefficient. *)
+  let one_symbol_of_coeff : int -> t -> Symbol.t option =
+    fun coeff x ->
       let x = M.filter (fun _ v -> v <> 0) x in
       if Int.equal (M.cardinal x) 1 then
         let k, v = M.min_binding x in
-        if Int.equal v 1 then Some k else None
+        if Int.equal v coeff then Some k else None
       else None
 
-  let is_one_symbol : t -> bool = fun x -> match one_symbol x with Some _ -> true | None -> false
+  let get_one_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff 1
+
+  let get_mone_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff (-1)
+
+  let get_one_symbol : t -> Symbol.t =
+    fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_one_symbol
+
+  let get_mone_symbol : t -> Symbol.t =
+    fun x -> match get_mone_symbol_opt x with Some s -> s | None -> raise Not_one_symbol
+
+  let is_one_symbol : t -> bool =
+    fun x -> match get_one_symbol_opt x with Some _ -> true | None -> false
+
+  let is_mone_symbol : t -> bool =
+    fun x -> match get_mone_symbol_opt x with Some _ -> true | None -> false
 
   let get_symbols : t -> Symbol.t list = fun x -> List.map ~f:fst (M.bindings x)
 end
 
 module Bound = struct
+  type sign_t = Plus | Minus [@@deriving compare]
+
+  let sign_equal = [%compare.equal : sign_t]
+
+  let neg_sign = function Plus -> Minus | Minus -> Plus
+
+  type min_max_t = Min | Max [@@deriving compare]
+
+  let min_max_equal = [%compare.equal : min_max_t]
+
+  let neg_min_max = function Min -> Max | Max -> Min
+
+  (* MinMax constructs a bound that is in the "int [+|-] [min|max](int, symbol)" format.
+     e.g. `MinMax (1, Minus, Max, 2, s)` means "1 - max (2, s)". *)
   type t =
     | MInf
     | Linear of int * SymLinear.t
-    | MinMax of min_max_t * int * Symbol.t
+    | MinMax of int * sign_t * min_max_t * int * Symbol.t
     | PInf
     | Bot
     [@@deriving compare]
 
-  and min_max_t = Min | Max
-
   let equal = [%compare.equal : t]
 
+  let pp_sign ~need_plus : F.formatter -> sign_t -> unit =
+    fun fmt -> function Plus -> if need_plus then F.fprintf fmt "+" | Minus -> F.fprintf fmt "-"
+
   let pp_min_max : F.formatter -> min_max_t -> unit =
     fun fmt -> function Min -> F.fprintf fmt "min" | Max -> F.fprintf fmt "max"
 
@@ -176,8 +209,10 @@ module Bound = struct
          -> if SymLinear.le x SymLinear.empty 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 (m, c, x)
-         -> F.fprintf fmt "%a(%d, %a)" pp_min_max m c Symbol.pp x
+        | MinMax (c, sign, m, d, x)
+         -> if Int.equal c 0 then F.fprintf fmt "%a" (pp_sign ~need_plus:false) sign
+            else F.fprintf fmt "%d%a" c (pp_sign ~need_plus:true) sign ;
+            F.fprintf fmt "%a(%d, %a)" pp_min_max m d Symbol.pp x
 
   let of_int : int -> t = fun n -> Linear (n, SymLinear.empty)
 
@@ -203,17 +238,27 @@ module Bound = struct
     fun s ->
       function
         | Linear (c, se)
-         -> Int.equal c 0 && opt_lift Symbol.eq (SymLinear.one_symbol se) (Some s)
+         -> Int.equal c 0 && opt_lift Symbol.eq (SymLinear.get_one_symbol_opt se) (Some s)
         | _
          -> false
 
-  let one_symbol : t -> Symbol.t option = function
-    | Linear (c, se) when Int.equal c 0
-     -> SymLinear.one_symbol se
-    | _
-     -> None
+  let lift_get_one_symbol : (SymLinear.t -> Symbol.t option) -> t -> Symbol.t option =
+    fun f -> function Linear (c, se) when Int.equal c 0 -> f se | _ -> None
+
+  let get_one_symbol_opt : t -> Symbol.t option = lift_get_one_symbol SymLinear.get_one_symbol_opt
+
+  let get_mone_symbol_opt : t -> Symbol.t option =
+    lift_get_one_symbol SymLinear.get_mone_symbol_opt
+
+  let get_one_symbol : t -> Symbol.t =
+    fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_one_symbol
 
-  let is_one_symbol : t -> bool = fun x -> one_symbol x <> None
+  let get_mone_symbol : t -> Symbol.t =
+    fun x -> match get_mone_symbol_opt x with Some s -> s | None -> raise Not_one_symbol
+
+  let is_one_symbol : t -> bool = fun x -> get_one_symbol_opt x <> None
+
+  let is_mone_symbol : t -> bool = fun x -> get_mone_symbol_opt x <> None
 
   let use_symbol : Symbol.t -> t -> bool =
     fun s ->
@@ -222,7 +267,7 @@ module Bound = struct
          -> false
         | Linear (_, se)
          -> SymLinear.find s se <> 0
-        | MinMax (_, _, s')
+        | MinMax (_, _, _, _, s')
          -> Symbol.eq s s'
 
   let subst1 : t -> t -> Symbol.t -> t -> t =
@@ -238,24 +283,50 @@ module Bound = struct
             let se1 = SymLinear.add s 0 se1 in
             let se' = SymLinear.plus se1 (SymLinear.mult_const se2 coeff) in
             Linear (c', se')
-        | MinMax (Min, _, s'), MInf when Symbol.eq s s'
+        | MinMax (_, Plus, Min, _, _), MInf
          -> MInf
-        | MinMax (Max, c, s'), MInf when Symbol.eq s s'
-         -> Linear (c, SymLinear.zero)
-        | MinMax (Max, _, s'), PInf when Symbol.eq s s'
+        | MinMax (_, Minus, Min, _, _), MInf
          -> PInf
-        | MinMax (Min, c, s'), PInf when Symbol.eq s s'
-         -> Linear (c, SymLinear.zero)
-        | MinMax (Min, c1, s'), Linear (c2, se) when Symbol.eq s s' && SymLinear.is_zero se
-         -> Linear (min c1 c2, SymLinear.zero)
-        | MinMax (Max, c1, s'), Linear (c2, se) when Symbol.eq s s' && SymLinear.is_zero se
-         -> Linear (max c1 c2, SymLinear.zero)
-        | MinMax (m, c, s'), _ when Symbol.eq s s' && is_one_symbol y -> (
-          match one_symbol y with Some s'' -> MinMax (m, c, s'') | _ -> assert false )
-        | MinMax (Min, c1, s'), MinMax (Min, c2, s'') when Symbol.eq s s'
-         -> MinMax (Min, min c1 c2, s'')
-        | MinMax (Max, c1, s'), MinMax (Max, c2, s'') when Symbol.eq s s'
-         -> MinMax (Max, max c1 c2, s'')
+        | MinMax (_, Plus, Max, _, _), PInf
+         -> PInf
+        | MinMax (_, Minus, Max, _, _), PInf
+         -> MInf
+        | MinMax (c, Plus, Min, d, _), PInf
+         -> Linear (c + d, SymLinear.zero)
+        | MinMax (c, Minus, Min, d, _), PInf
+         -> Linear (c - d, SymLinear.zero)
+        | MinMax (c, Plus, Max, d, _), MInf
+         -> Linear (c + d, SymLinear.zero)
+        | MinMax (c, Minus, Max, d, _), MInf
+         -> Linear (c - d, SymLinear.zero)
+        | MinMax (c1, Plus, Min, d1, _), Linear (c2, se) when SymLinear.is_zero se
+         -> Linear (c1 + min d1 c2, SymLinear.zero)
+        | MinMax (c1, Minus, Min, d1, _), Linear (c2, se) when SymLinear.is_zero se
+         -> Linear (c1 - min d1 c2, SymLinear.zero)
+        | MinMax (c1, Plus, Max, d1, _), Linear (c2, se) when SymLinear.is_zero se
+         -> Linear (c1 + max d1 c2, SymLinear.zero)
+        | 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)
+        | MinMax (c, sign, m, d, _), _ when is_mone_symbol y
+         -> 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')
+        | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, s')
+         -> 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')
+        | MinMax (c1, Minus, Max, d1, _), MinMax (c2, Plus, Max, d2, s')
+         -> 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')
+        | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Minus, Min, d2, s')
+         -> 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')
+        | MinMax (c1, Minus, Max, d1, _), MinMax (c2, Minus, Min, d2, s')
+         -> MinMax (c1 - c2, Minus, Min, min (-d1 + c2) d2, s')
         | _
          -> default
 
@@ -263,7 +334,54 @@ module Bound = struct
   let subst : t -> t -> t SubstMap.t -> t =
     fun default x map -> SubstMap.fold (fun s y x -> subst1 default x s y) map x
 
-  let le : t -> t -> bool =
+  let int_ub_of_minmax = function
+    | MinMax (c, Plus, Min, d, _)
+     -> Some (c + d)
+    | MinMax (c, Minus, Max, d, _)
+     -> Some (c - d)
+    | MinMax _
+     -> None
+    | MInf | PInf | Linear _ | Bot
+     -> assert false
+
+  let int_lb_of_minmax = function
+    | MinMax (c, Plus, Max, d, _)
+     -> Some (c + d)
+    | MinMax (c, Minus, Min, d, _)
+     -> Some (c - d)
+    | MinMax _
+     -> None
+    | MInf | PInf | Linear _ | Bot
+     -> assert false
+
+  let linear_ub_of_minmax = function
+    | MinMax (c, Plus, Min, _, x)
+     -> Some (Linear (c, SymLinear.singleton x 1))
+    | MinMax (c, Minus, Max, _, x)
+     -> Some (Linear (c, SymLinear.singleton x (-1)))
+    | MinMax _
+     -> None
+    | MInf | PInf | Linear _ | Bot
+     -> assert false
+
+  let linear_lb_of_minmax = function
+    | MinMax (c, Plus, Max, _, x)
+     -> Some (Linear (c, SymLinear.singleton x 1))
+    | MinMax (c, Minus, Min, _, x)
+     -> Some (Linear (c, SymLinear.singleton x (-1)))
+    | MinMax _
+     -> None
+    | MInf | PInf | Linear _ | Bot
+     -> assert false
+
+  let le_minmax_by_int x y =
+    match (int_ub_of_minmax x, int_lb_of_minmax y) with Some n, Some m -> n <= m | _, _ -> false
+
+  let le_opt1 le opt_n m = Option.value_map opt_n ~default:false ~f:(fun n -> le n m)
+
+  let le_opt2 le n opt_m = Option.value_map opt_m ~default:false ~f:(fun m -> le n m)
+
+  let rec le : t -> t -> bool =
     fun x y ->
       assert (x <> Bot && y <> Bot) ;
       match (x, y) with
@@ -273,16 +391,22 @@ module Bound = struct
        -> false
       | Linear (c0, x0), Linear (c1, x1)
        -> c0 <= c1 && SymLinear.eq x0 x1
-      | MinMax (Min, c0, x0), MinMax (Min, c1, x1) | MinMax (Max, c0, x0), MinMax (Max, c1, x1)
-       -> c0 <= c1 && Symbol.eq x0 x1
-      | MinMax (Min, c0, x0), Linear (c1, x1)
-       -> c0 <= c1 && SymLinear.is_zero x1
-          || Int.equal c1 0 && opt_lift Symbol.eq (SymLinear.one_symbol x1) (Some x0)
-      | Linear (c1, x1), MinMax (Max, c0, x0)
-       -> c1 <= c0 && SymLinear.is_zero x1
-          || Int.equal c1 0 && opt_lift Symbol.eq (SymLinear.one_symbol x1) (Some x0)
-      | MinMax (Min, c0, x0), MinMax (Max, c1, x1)
-       -> c0 <= c1 || Symbol.eq 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
+      | MinMax _, MinMax _ when le_minmax_by_int x y
+       -> true
+      | 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
+       -> le_opt1 ( <= ) (int_ub_of_minmax x) c
+      | MinMax _, Linear _
+       -> le_opt1 le (linear_ub_of_minmax x) y
+      | Linear (c, se), MinMax _ when SymLinear.is_zero se
+       -> le_opt2 ( <= ) c (int_lb_of_minmax y)
+      | Linear _, MinMax _
+       -> le_opt2 le x (linear_lb_of_minmax y)
       | _, _
        -> false
 
@@ -292,14 +416,10 @@ module Bound = struct
       match (x, y) with
       | MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf
        -> true
-      | Linear (c0, x0), Linear (c1, x1)
-       -> c0 < c1 && SymLinear.eq x0 x1
-      | MinMax (Min, c0, _), Linear (c1, x1)
-       -> c0 < c1 && SymLinear.is_zero x1
-      | Linear (c1, x1), MinMax (Max, c0, _)
-       -> c1 < c0 && SymLinear.is_zero x1
-      | MinMax (Min, c0, _), MinMax (Max, c1, _)
-       -> c0 < c1
+      | 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
       | _, _
        -> false
 
@@ -311,59 +431,77 @@ module Bound = struct
       else if equal x Bot || equal y Bot then false
       else le x y && le y x
 
-  let min : t -> t -> t =
-    fun x y ->
+  let remove_max_int : t -> t =
+    fun x ->
+      match x with
+      | MinMax (c, Plus, Max, _, s)
+       -> Linear (c, SymLinear.singleton s 1)
+      | MinMax (c, Minus, Min, _, s)
+       -> Linear (c, SymLinear.singleton s (-1))
+      | _
+       -> x
+
+  let rec lb : ?default:t -> t -> t -> t =
+    fun ?(default= MInf) x y ->
       assert (x <> Bot && y <> Bot) ;
       if le x y then x
       else if le y x then y
       else
         match (x, y) with
-        | Linear (c0, x0), Linear (c1, x1)
-          when SymLinear.is_zero x0 && Int.equal c1 0 && SymLinear.is_one_symbol x1 -> (
-          match SymLinear.one_symbol x1 with
-          | Some x'
-           -> MinMax (Min, c0, x')
-          | None
-           -> assert false )
-        | Linear (c0, x0), Linear (c1, x1)
-          when SymLinear.is_zero x1 && Int.equal c0 0 && SymLinear.is_one_symbol x0 -> (
-          match SymLinear.one_symbol x0 with
-          | Some x'
-           -> MinMax (Min, c1, x')
-          | None
-           -> assert false )
-        | MinMax (Max, c0, _), Linear (c1, x1)
-        | Linear (c1, x1), MinMax (Max, c0, _)
-          when SymLinear.is_zero x1 && c0 < c1
-         -> Linear (c0, x1)
+        | 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)
+        | 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)
+        | 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)
+        | 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)
+        | 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)
+        | 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)
+        | 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)
+        | 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)
+        | 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 (min (c1 + d1) (c2 + d2), SymLinear.zero)
         | _, _
-         -> MInf
+         -> default
 
-  let max : t -> t -> t =
+  let ub : t -> t -> t =
     fun x y ->
       assert (x <> Bot && y <> Bot) ;
       if le x y then y
       else if le y x then x
       else
         match (x, y) with
-        | Linear (c0, x0), Linear (c1, x1)
-          when SymLinear.is_zero x0 && Int.equal c1 0 && SymLinear.is_one_symbol x1 -> (
-          match SymLinear.one_symbol x1 with
-          | Some x'
-           -> MinMax (Max, c0, x')
-          | None
-           -> assert false )
-        | Linear (c0, x0), Linear (c1, x1)
-          when SymLinear.is_zero x1 && Int.equal c0 0 && SymLinear.is_one_symbol x0 -> (
-          match SymLinear.one_symbol x0 with
-          | Some x'
-           -> MinMax (Max, c1, x')
-          | None
-           -> assert false )
-        | MinMax (Min, c0, _), Linear (c1, x1)
-        | Linear (c1, x1), MinMax (Min, c0, _)
-          when SymLinear.is_zero x1 && c0 > c1
-         -> Linear (c0, x1)
+        | 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)
+        | 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)
+        | 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)
+        | 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)
         | _, _
          -> PInf
 
@@ -409,8 +547,16 @@ module Bound = struct
        -> x
       | Linear (c1, x1), Linear (c2, x2)
        -> Linear (c1 + c2, SymLinear.plus x1 x2)
-      | MinMax (Max, c1, _), Linear (c2, x2) | Linear (c2, x2), MinMax (Max, c1, _)
-       -> Linear (c1 + c2, x2)
+      | 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)
+      | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2)
+      | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _)
+       -> Linear (c1 + d1 + c2, x2)
+      | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2)
+      | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _)
+       -> Linear (c1 - d1 + c2, x2)
       | _, _
        -> MInf
 
@@ -424,8 +570,16 @@ module Bound = struct
        -> x
       | Linear (c1, x1), Linear (c2, x2)
        -> Linear (c1 + c2, SymLinear.plus x1 x2)
-      | MinMax (Min, c1, _), Linear (c2, x2) | Linear (c2, x2), MinMax (Min, c1, _)
-       -> Linear (c1 + c2, x2)
+      | 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)
+      | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2)
+      | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _)
+       -> Linear (c1 + d1 + c2, x2)
+      | MinMax (c1, Minus, Max, d1, _), Linear (c2, x2)
+      | Linear (c2, x2), MinMax (c1, Minus, Max, d1, _)
+       -> Linear (c1 - d1 + c2, x2)
       | _, _
        -> PInf
 
@@ -467,34 +621,17 @@ module Bound = struct
      -> Some MInf
     | Linear (c, x)
      -> Some (Linear (-c, SymLinear.neg x))
-    | MinMax _
-     -> None
+    | MinMax (c, sign, min_max, d, x)
+     -> Some (MinMax (-c, neg_sign sign, min_max, d, x))
     | Bot
      -> assert false
 
-  let make_min_max : min_max_t -> t -> t -> t option =
-    fun m x y ->
-      assert (x <> Bot && y <> Bot) ;
-      match (x, y) with
-      | Linear (cx, x'), Linear (cy, y')
-        when Int.equal cy 0 && SymLinear.is_zero x' && SymLinear.is_one_symbol y' -> (
-        match SymLinear.one_symbol y' with Some s -> Some (MinMax (m, cx, s)) | None -> None )
-      | Linear (cx, x'), Linear (cy, y')
-        when Int.equal cx 0 && SymLinear.is_zero y' && SymLinear.is_one_symbol x' -> (
-        match SymLinear.one_symbol x' with Some s -> Some (MinMax (m, cy, s)) | None -> None )
-      | _, _
-       -> None
-
-  let make_min : t -> t -> t option = make_min_max Min
-
-  let make_max : t -> t -> t option = make_min_max Max
-
   let get_symbols : t -> Symbol.t list = function
     | MInf | PInf
      -> []
     | Linear (_, se)
      -> SymLinear.get_symbols se
-    | MinMax (_, _, s)
+    | MinMax (_, _, _, _, s)
      -> [s]
     | Bot
      -> assert false
@@ -525,7 +662,7 @@ module ItvPure = struct
   let ( <= ) : lhs:t -> rhs:t -> bool =
     fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2
 
-  let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.min l1 l2, Bound.max u1 u2)
+  let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.ub 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)
@@ -549,7 +686,8 @@ module ItvPure = struct
   let make_sym : unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t =
     fun ~unsigned pname new_sym_num ->
       let lower =
-        if unsigned then Bound.MinMax (Bound.Max, 0, Symbol.make pname (new_sym_num ()))
+        if unsigned then
+          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
@@ -712,6 +850,8 @@ module ItvPure = struct
       else if is_false x && is_false y then false_sem
       else unknown_bool
 
+  let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2)
+
   let invalid : t -> bool =
     fun (l, u) ->
       Bound.equal l Bound.Bot || Bound.equal u Bound.Bot || Bound.eq l Bound.PInf
@@ -724,25 +864,22 @@ module ItvPure = struct
        -> (l1, u2)
       | (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 -> (
-        match Bound.one_symbol u with
-        | Some s
-         -> (l1, Bound.MinMax (Bound.Min, c, s))
-        | None
-         -> assert false )
-      | (l1, u), (_, Bound.Linear (c, se)) when SymLinear.is_zero se && Bound.is_one_symbol u -> (
-        match Bound.one_symbol u with
-        | Some s
-         -> (l1, Bound.MinMax (Bound.Min, c, s))
-        | None
-         -> assert false )
-      | (l1, Bound.Linear (c1, se)), (_, Bound.MinMax (Bound.Min, c2, se'))
-      | (l1, Bound.MinMax (Bound.Min, c1, se')), (_, Bound.Linear (c2, se))
+      | (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, 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.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, 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.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 (Bound.Min, min c1 c2, se'))
-      | (l1, Bound.MinMax (Bound.Min, c1, se1)), (_, Bound.MinMax (Bound.Min, c2, se2))
-        when Symbol.eq se1 se2
-       -> (l1, Bound.MinMax (Bound.Min, min c1 c2, se1))
+       -> (l1, Bound.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))
       | _
        -> x
 
@@ -753,25 +890,22 @@ module ItvPure = struct
        -> (l2, u1)
       | (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 -> (
-        match Bound.one_symbol l with
-        | Some s
-         -> (Bound.MinMax (Bound.Max, c, s), u1)
-        | None
-         -> assert false )
-      | (l, u1), (Bound.Linear (c, se), _) when SymLinear.is_zero se && Bound.is_one_symbol l -> (
-        match Bound.one_symbol l with
-        | Some s
-         -> (Bound.MinMax (Bound.Max, c, s), u1)
-        | None
-         -> assert false )
-      | (Bound.Linear (c1, se), u1), (Bound.MinMax (Bound.Max, c2, se'), _)
-      | (Bound.MinMax (Bound.Max, c1, se'), u1), (Bound.Linear (c2, se), _)
+      | (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)
+      | (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.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)
+      | (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.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 (Bound.Max, max c1 c2, se'), u1)
-      | (Bound.MinMax (Bound.Max, c1, se1), u1), (Bound.MinMax (Bound.Max, c2, se2), _)
-        when Symbol.eq se1 se2
-       -> (Bound.MinMax (Bound.Max, max c1 c2, se1), u1)
+       -> (Bound.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)
       | _
        -> x
 
@@ -964,6 +1098,8 @@ let land_sem : t -> t -> t = lift2 ItvPure.land_sem
 
 let lor_sem : t -> t -> t = lift2 ItvPure.lor_sem
 
+let min_sem : t -> t -> t = lift2 ItvPure.min_sem
+
 let prune_zero : t -> t = lift1 ItvPure.prune_zero
 
 let prune_comp : Binop.t -> t -> t -> t = fun comp -> lift2_opt (ItvPure.prune_comp comp)

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

@@ -14,6 +14,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Call
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [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, [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/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, call_safe_access4_Good_FP, 2, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Call,Assignment,Return,Call,Assignment,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]]
@@ -21,3 +22,5 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERR
 codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [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, push_back_Bad, 3, BUFFER_OVERRUN, [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, [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, []
+codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_TRUE, []

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

@@ -103,3 +103,21 @@ void just_test_model_FP(void) {
   int y = v3[0];
   int z = v3.at(1);
 }
+
+void safe_access3_Good() {
+  std::vector<int> v;
+  if (!v.empty()) {
+    v[0] = 1;
+  }
+}
+
+void safe_access4(std::vector<int> v) {
+  if (!v.empty()) {
+    v[0] = 1;
+  }
+}
+
+void call_safe_access4_Good_FP() {
+  std::vector<int> v;
+  safe_access4(v);
+}