[inferbo] Precise symbol instantiation

Summary:
This commit improves precision of symbol instantiations.

When a return value of a callee is `[s1 + s2, _]` and if we want to
instantiate `s1` to `c3 + max(c4, s5)`, the lower bound was
substituted to `-oo` because our domain cannot express `c3 + max(c4,
s5) + s2`.

However, we can have instantiations that are preciser than `-oo`:
(1) `c3 + c4 + s2`
(2) or `c3 + s5 + s2`
because they are smaller than the ideal instantiation, `c3 + max(c4,
s5) + s2` and it is on the lower bound position.

For now, the implementation instantiates to (1) between the two ones,
because constant values introduced by `assert` or `assume`(`if`)
command are often used as safety conditions, e.g., `assert(index >=
0);` can place before array accesses.  (We can change the stratege
later if we find that it doesn't work on some other cases.)

Reviewed By: mbouaziz

Differential Revision: D7020063

fbshipit-source-id: 62fb390

infer/src/bufferoverrun/itv.ml

@@ -264,6 +264,8 @@ module Bound = struct
 
     let neg = function Plus -> Minus | Minus -> Plus
 
+    let eval_int x i1 i2 = match x with Plus -> i1 + i2 | Minus -> i1 - i2
+
     let pp ~need_plus : F.formatter -> t -> unit =
       fun fmt ->
         function Plus -> if need_plus then F.fprintf fmt "+" | Minus -> F.fprintf fmt "-"
@@ -278,6 +280,8 @@ module Bound = struct
 
     let neg = function Min -> Max | Max -> Min
 
+    let eval_int x i1 i2 = match x with Min -> min i1 i2 | Max -> max i1 i2
+
     let pp : F.formatter -> t -> unit =
       fun fmt -> function Min -> F.fprintf fmt "min" | Max -> F.fprintf fmt "max"
   end
@@ -359,8 +363,8 @@ module Bound = struct
   let mk_MinMax (c, sign, m, d, s) =
     if Symbol.is_unsigned s then
       match m with
-      | Min when d <= 0 -> (
+      | Min when d <= 0 ->
-        match sign with Plus -> of_int (c + d) | Minus -> of_int (c - d) )
+          of_int (Sign.eval_int sign c d)
       | Max when d <= 0 -> (
         match sign with
         | Plus ->
@@ -383,27 +387,50 @@ module Bound = struct
             Symbol.equal s s'
 
 
-  (** substitutes [s] with [y0] in [x0], if the result is not expressible, return [default] *)
+  type subst_pos_t = SubstLowerBound | SubstUpperBound
-  let subst1 : default:t -> t bottom_lifted -> Symbol.t -> t bottom_lifted -> t bottom_lifted =
+
-    fun ~default x0 s y0 ->
+  (* [subst1] substitutes [s] in [x0] to [y0].
-      match (x0, y0) with
+
-      | Bottom, _ ->
+     - If the precise result is expressible by the domain, the
-          x0
+     function returns it.
-      | NonBottom x, _ when eq_symbol s x ->
+
-          y0
+     - If the precise result is not expressible, but a compromized
-      | NonBottom x, _ when not (use_symbol s x) ->
+     value, with regard to [subst_pos], is expressible by the domain,
-          x0
+     the function returns the compromized value.
-      | NonBottom _, Bottom ->
+
-          NonBottom default
+     - Otherwise, it returns the default values, -oo for lower bound and
-      | NonBottom x, NonBottom y ->
+     +oo for upper bound.  *)
-          let res =
+  let subst1
-            match (x, y) with
+      : subst_pos:subst_pos_t -> t bottom_lifted -> Symbol.t -> t bottom_lifted -> t bottom_lifted =
-            | Linear (c1, se1), Linear (c2, se2) ->
+    let get_default = function SubstLowerBound -> MInf | SubstUpperBound -> PInf in
+    let subst1_linears c1 se1 s c2 se2 =
       let coeff = SymLinear.find s se1 in
       let c' = c1 + (coeff :> int) * c2 in
       let se1 = SymLinear.remove s se1 in
       let se' = SymLinear.mult_const_plus se2 coeff se1 in
       Linear (c', se')
+    in
+    let subst1_non_bottom ~subst_pos x s y =
+      match (x, y) with
+      | Linear (c1, se1), Linear (c2, se2) ->
+          subst1_linears c1 se1 s c2 se2
+      | Linear (c1, se1), MinMax (c2, sign, min_max, d2, s2) when SymLinear.is_one_symbol se1 ->
+          assert (Symbol.equal (SymLinear.get_one_symbol se1) s) ;
+          MinMax (c1 + c2, sign, min_max, d2, s2)
+      | Linear (c1, se1), MinMax (c2, sign, min_max, d2, s2) when SymLinear.is_mone_symbol se1 ->
+          assert (Symbol.equal (SymLinear.get_mone_symbol se1) s) ;
+          MinMax (c1 - c2, Sign.neg sign, min_max, d2, s2)
+      | Linear (c1, se1), MinMax (c2, bop, min_max, d2, _) ->
+          let coeff = SymLinear.find s se1 in
+          let compromisable =
+            match (subst_pos, min_max) with
+            | SubstLowerBound, Max | SubstUpperBound, Min ->
+                NonZeroInt.is_positive coeff
+            | SubstUpperBound, Max | SubstLowerBound, Min ->
+                NonZeroInt.is_negative coeff
+          in
+          if compromisable then subst1_linears c1 se1 s (Sign.eval_int bop c2 d2) SymLinear.empty
+          else get_default subst_pos
       | MinMax (_, Plus, Min, _, _), MInf ->
           MInf
       | MinMax (_, Minus, Min, _, _), MInf ->
@@ -412,46 +439,39 @@ module Bound = struct
           PInf
       | MinMax (_, Minus, Max, _, _), PInf ->
           MInf
-            | MinMax (c, Plus, Min, d, _), PInf ->
+      | MinMax (c, sign, Min, d, _), PInf | MinMax (c, sign, Max, d, _), MInf ->
-                Linear (c + d, SymLinear.zero)
+          of_int (Sign.eval_int sign c d)
-            | MinMax (c, Minus, Min, d, _), PInf ->
+      | MinMax (c1, sign, min_max, d1, _), Linear (c2, se) when SymLinear.is_zero se ->
-                Linear (c - d, SymLinear.zero)
+          of_int (Sign.eval_int sign c1 (MinMax.eval_int min_max d1 c2))
-            | 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 ->
           mk_MinMax (c, sign, m, d, get_one_symbol y)
       | MinMax (c, sign, m, d, _), _ when is_mone_symbol y ->
           mk_MinMax (c, Sign.neg sign, MinMax.neg m, -d, get_mone_symbol y)
-            | MinMax (c1, Plus, Min, d1, _), MinMax (c2, Plus, Min, d2, s') ->
+      | MinMax (c1, sign1, min_max, d1, _), MinMax (c2, Plus, min_max', d2, s')
-                mk_MinMax (c1 + c2, Plus, Min, min (d1 - c2) d2, s')
+        when MinMax.equal min_max min_max' ->
-            | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, s') ->
+          let c = Sign.eval_int sign1 c1 c2 in
-                mk_MinMax (c1 + c2, Plus, Max, max (d1 - c2) d2, s')
+          let d = MinMax.eval_int min_max (d1 - c2) d2 in
-            | MinMax (c1, Minus, Min, d1, _), MinMax (c2, Plus, Min, d2, s') ->
+          mk_MinMax (c, sign1, min_max, d, s')
-                mk_MinMax (c1 - c2, Minus, Min, min (d1 - c2) d2, s')
+      | MinMax (c1, sign1, min_max, d1, _), MinMax (c2, Minus, min_max', d2, s')
-            | MinMax (c1, Minus, Max, d1, _), MinMax (c2, Plus, Max, d2, s') ->
+        when MinMax.equal (MinMax.neg min_max) min_max' ->
-                mk_MinMax (c1 - c2, Minus, Max, max (d1 - c2) d2, s')
+          let c = Sign.eval_int sign1 c1 c2 in
-            | MinMax (c1, Plus, Min, d1, _), MinMax (c2, Minus, Max, d2, s') ->
+          let d = MinMax.eval_int min_max' (c2 - d1) d2 in
-                mk_MinMax (c1 + c2, Minus, Max, max (-d1 + c2) d2, s')
+          mk_MinMax (c, Sign.neg sign1, min_max', d, s')
-            | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Minus, Min, d2, s') ->
-                mk_MinMax (c1 + c2, Minus, Min, min (-d1 + c2) d2, s')
-            | MinMax (c1, Minus, Min, d1, _), MinMax (c2, Minus, Max, d2, s') ->
-                mk_MinMax (c1 - c2, Minus, Max, max (-d1 + c2) d2, s')
-            | MinMax (c1, Minus, Max, d1, _), MinMax (c2, Minus, Min, d2, s') ->
-                mk_MinMax (c1 - c2, Minus, Min, min (-d1 + c2) d2, s')
       | _ ->
-                default
+          get_default subst_pos
     in
-          NonBottom res
+    fun ~subst_pos x0 s y0 ->
+      match (x0, y0) with
+      | Bottom, _ ->
+          x0
+      | NonBottom x, _ when eq_symbol s x ->
+          y0
+      | NonBottom x, _ when not (use_symbol s x) ->
+          x0
+      | NonBottom _, Bottom ->
+          NonBottom (get_default subst_pos)
+      | NonBottom x, NonBottom y ->
+          NonBottom (subst1_non_bottom ~subst_pos x s y)
 
 
   let int_ub_of_minmax = function
@@ -676,8 +696,8 @@ module Bound = struct
 
 
   (* substitution symbols in ``x'' with respect to ``map'' *)
-  let subst : default:t -> t -> t bottom_lifted SubstMap.t -> t bottom_lifted =
+  let subst : subst_pos:subst_pos_t -> t -> t bottom_lifted SubstMap.t -> t bottom_lifted =
-    fun ~default x map ->
+    fun ~subst_pos x map ->
       let subst_helper s y x =
         let y' =
           match y with
@@ -686,11 +706,15 @@ module Bound = struct
           | NonBottom r ->
               NonBottom (if Symbol.is_unsigned s then ub ~default:r zero r else r)
         in
-        subst1 ~default x s y'
+        subst1 ~subst_pos x s y'
       in
       SubstMap.fold subst_helper map (NonBottom x)
 
 
+  let subst_lb x map = subst ~subst_pos:SubstLowerBound x map
+
+  let subst_ub x map = subst ~subst_pos:SubstUpperBound x map
+
   let plus_l : t -> t -> t =
     fun x y ->
       match (x, y) with
@@ -823,9 +847,7 @@ module ItvPure = struct
 
   let subst : t -> Bound.t bottom_lifted SubstMap.t -> t bottom_lifted =
     fun x map ->
-      match
+      match (Bound.subst_lb (lb x) map, Bound.subst_ub (ub x) map) with
-        (Bound.subst ~default:Bound.MInf (lb x) map, Bound.subst ~default:Bound.PInf (ub x) map)
-      with
       | NonBottom l, NonBottom u ->
           NonBottom (l, u)
       | _ ->

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

@@ -23,6 +23,8 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, [Cal
 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: [u$12, u$13] Size: [u$12, u$13]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, -1] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call `access_minus_one()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, [ArrayDeclaration,Call,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call `access_minus_one()` ]
 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/vector.cpp

@@ -184,3 +184,42 @@ void assert_Bad() {
   assert(v.size() == 5);
   v[6] = 1;
 }
+
+class CharVector {
+ public:
+  CharVector(char* init) : a(init) {}
+
+  char& operator[](int idx) { return a[idx]; }
+
+ private:
+  char* a;
+};
+
+void access_in_sixth(int count, CharVector v) {
+  assert(count >= 0);
+  assert(count < 5);
+  v[count + 1] = '0';
+}
+
+void access_minus_one(int count, CharVector v) {
+  assert(count >= 0);
+  v[count - 1] = '0';
+}
+
+void precise_subst_Good() {
+  char a[10];
+  CharVector v(a);
+  access_in_sixth(0, v);
+}
+
+void precise_subst_Good_FP() {
+  char a[10];
+  CharVector v(a);
+  access_minus_one(1, v);
+}
+
+void precise_subst_Bad() {
+  char a[10];
+  CharVector v(a);
+  access_minus_one(0, v);
+}