[inferbo] Suppress intended integer underflow of unsigned integer

Summary: Sometimes programmers use integer underflow to get a maximum number of that type.  This diff assumes that integer underflows from the syntactical form `(unsigned 0) - constant` is intended by the programmer, and suppresses the alarms of which.

Reviewed By: ezgicicek

Differential Revision: D16560639

fbshipit-source-id: 206f30dbc

infer/src/IR/Exp.ml

@@ -77,6 +77,8 @@ let is_this = function Lvar pvar -> Pvar.is_this pvar | _ -> false
 
 let is_zero = function Const (Cint n) -> IntLit.iszero n | _ -> false
 
+let rec is_const = function Const _ -> true | Cast (_, x) -> is_const x | _ -> false
+
 (** {2 Utility Functions for Expressions} *)
 
 (** Turn an expression representing a type into the type it represents

infer/src/IR/Exp.mli

@@ -63,6 +63,8 @@ val is_this : t -> bool
 
 val is_zero : t -> bool
 
+val is_const : t -> bool
+
 (** {2 Utility Functions for Expressions} *)
 
 val texp_to_typ : Typ.t option -> t -> Typ.t

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -202,6 +202,9 @@ let check_expr_for_array_access :
 
 let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set =
   match bop with
+  | Binop.MinusA (Some typ) when Typ.ikind_is_unsigned typ && Exp.is_zero lhs && Exp.is_const rhs
+    ->
+      cond_set
   | Binop.PlusA (Some _) | Binop.MinusA (Some _) | Binop.Mult (Some _) ->
       let lhs_v = Sem.eval integer_type_widths lhs mem in
       let rhs_v = Sem.eval integer_type_widths rhs mem in

infer/tests/codetoanalyze/c/bufferoverrun/arith.c

@@ -540,3 +540,9 @@ void shift_right_zero_Bad(int x) {
   int arr[1];
   arr[1 + (0 >> x)] = 1;
 }
+
+#define INTENDED_INTEGER_UNDERFLOW (0ULL - 2)
+
+void use_intended_integer_underflow_Good() {
+  unsigned long long x = INTENDED_INTEGER_UNDERFLOW;
+}