From a3229fc43a7303e65352dca3495c19b33cf76ba8 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 1 Aug 2019 01:37:55 -0700 Subject: [PATCH] [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 | 2 ++ infer/src/IR/Exp.mli | 2 ++ infer/src/bufferoverrun/bufferOverrunChecker.ml | 3 +++ infer/tests/codetoanalyze/c/bufferoverrun/arith.c | 6 ++++++ 4 files changed, 13 insertions(+) diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml index 495eac6f8..e0d901344 100644 --- a/infer/src/IR/Exp.ml +++ b/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 diff --git a/infer/src/IR/Exp.mli b/infer/src/IR/Exp.mli index f022aa6c4..17b77bd93 100644 --- a/infer/src/IR/Exp.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 49748991d..3f362795e 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index e389fbdaa..0a3ee472e 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/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; +}