[inferbo] Refine <= for MinMax

Reviewed By: skcho

Differential Revision: D10404824

fbshipit-source-id: deacc033f

infer/src/bufferoverrun/bounds.ml

@@ -194,8 +194,6 @@ module Bound = struct
   module Sign = struct
     type t = sign [@@deriving compare]
 
-    let equal = [%compare.equal: t]
-
     let neg = function Plus -> Minus | Minus -> Plus
 
     let eval_big_int x i1 i2 = match x with Plus -> Z.(i1 + i2) | Minus -> Z.(i1 - i2)
@@ -213,8 +211,6 @@ module Bound = struct
   module MinMax = struct
     type t = min_max [@@deriving compare]
 
-    let equal = [%compare.equal: t]
-
     let neg = function Min -> Max | Max -> Min
 
     let eval_big_int x i1 i2 = match x with Min -> Z.min i1 i2 | Max -> Z.max i1 i2
@@ -405,22 +401,30 @@ module Bound = struct
         false
     | Linear (c0, x0), Linear (c1, x1) ->
         c0 <= c1 && SymLinear.le x0 x1
-    | MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2)
-      when Sign.equal sign1 sign2 && MinMax.equal m1 m2 ->
-        c1 <= c2 && Z.equal d1 d2 && Symb.Symbol.equal 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 && Symb.Symbol.equal x1 x2
+    | MinMax (c1, (Plus as sign), Min, d1, s1), MinMax (c2, Plus, Min, d2, s2)
+    | MinMax (c1, (Minus as sign), Min, d1, s1), MinMax (c2, Minus, Min, d2, s2)
+    | MinMax (c1, (Plus as sign), Max, d1, s1), MinMax (c2, Plus, Max, d2, s2)
+    | MinMax (c1, (Minus as sign), Max, d1, s1), MinMax (c2, Minus, Max, d2, s2)
+      when Symb.Symbol.equal s1 s2 ->
+        Z.leq c1 c2
+        &&
+        let v1 = Sign.eval_big_int sign c1 d1 in
+        let v2 = Sign.eval_big_int sign c2 d2 in
+        Z.leq v1 v2
+    | MinMax (c1, Plus, Min, _, s1), MinMax (c2, Plus, Max, _, s2)
+    | MinMax (c1, Minus, Max, _, s1), MinMax (c2, Minus, Min, _, s2)
+      when Symb.Symbol.equal s1 s2 ->
+        Z.leq c1 c2
+    | MinMax _, MinMax _ ->
+        false
     | MinMax _, Linear (c, se) ->
         (SymLinear.is_ge_zero se && le_opt1 Z.leq (big_int_ub_of_minmax x) c)
         || le_opt1 le (linear_ub_of_minmax x) y
     | Linear (c, se), MinMax _ ->
         (SymLinear.is_le_zero se && le_opt2 Z.leq c (big_int_lb_of_minmax y))
         || le_opt2 le x (linear_lb_of_minmax y)
-    | _, _ ->
-        false
 
 
   let lt : t -> t -> bool =

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

@@ -147,6 +147,9 @@ 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, 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/prune_constant.c

@@ -42,3 +42,41 @@ void prune_constant_not_Bad() {
     a[x + 1] = 0;
   }
 }
+
+int fromHex(char c) {
+  if (c < '0' || (c > '9' && (c < 'a' || c > 'f'))) {
+    return -1; // invalid not 0-9a-f hex char
+  }
+  if (c <= '9') {
+    return c - '0';
+  }
+  return c - 'a' + 10;
+}
+
+void call_fromHex_sym_Good(char c) {
+  char arr[16];
+  int idx = fromHex(c);
+  if (idx >= 0) {
+    arr[idx] = 'H';
+  }
+}
+
+void call_fromHex_200_Good_FP() {
+  char arr[16];
+  int idx = fromHex(200);
+  if (idx >= 0) {
+    arr[idx] = 'H';
+  }
+}
+
+void call_fromHex2_sym_Good(char c) {
+  char arr[17];
+  int idx = fromHex(c);
+  arr[idx + 1] = 'H';
+}
+
+void call_fromHex2_200_Good_FP() {
+  char arr[17];
+  int idx = fromHex(200);
+  arr[idx + 1] = 'H';
+}