[inferbo] Suppress intended integer overflow

Summary:
It suppresses intended integer overflows that generate hash values or random numbers.  For judging that the intention of integer overflow, it applies a heuristics: checking if traces of issues include a whitelisted words, e.g., "rand" or "seed".

While we would be able to suppress all integer overflows of unsigned integers since they have defined behaviors, we don't want to miss unintended integer overflows, e.g., that on unsigned index value.

Depends on D13595958

Reviewed By: mbouaziz

Differential Revision: D13595967

fbshipit-source-id: 8d3aca5a7

infer/src/bufferoverrun/absLoc.ml

@@ -208,6 +208,10 @@ module Loc = struct
         Allocsite.represents_multiple_values allocsite
     | Field (l, _) ->
         represents_multiple_values l
+
+
+  let exists_str ~f l =
+    Option.exists (get_path l) ~f:(fun path -> Symb.SymbolPath.exists_str_partial ~f path)
 end
 
 module PowLoc = struct
@@ -240,6 +244,9 @@ module PowLoc = struct
 
   let subst x (eval_locpath : eval_locpath) =
     fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty
+
+
+  let exists_str ~f x = exists (fun l -> Loc.exists_str ~f l) x
 end
 
 let always_strong_update = false

infer/src/bufferoverrun/bounds.ml

@@ -180,6 +180,9 @@ module SymLinear = struct
         Some (Symb.Symbol.path s1)
     | _ ->
         None
+
+
+  let exists_str ~f x = M.exists (fun k _ -> Symb.Symbol.exists_str ~f k) x
 end
 
 module Bound = struct
@@ -943,6 +946,15 @@ module Bound = struct
         SymLinear.is_same_symbol se1 se2
     | _ ->
         None
+
+
+  let exists_str ~f = function
+    | MInf | PInf ->
+        false
+    | Linear (_, s) ->
+        SymLinear.exists_str ~f s
+    | MinMax (_, _, _, _, s) ->
+        Symb.Symbol.exists_str ~f s
 end
 
 type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop

infer/src/bufferoverrun/bounds.mli

@@ -116,6 +116,8 @@ module Bound : sig
   val simplify_bound_ends_from_paths : t -> t
 
   val is_same_symbol : t -> t -> Symb.SymbolPath.t option
+
+  val exists_str : f:(string -> bool) -> t -> bool
 end
 
 type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -74,6 +74,8 @@ module ConditionTrace = struct
 
   let has_risky ct = ValTrace.Issue.has_risky ct.val_traces
 
+  let exists_str ~f ct = ValTrace.Issue.exists_str ~f ct.val_traces
+
   let check ~issue_type_u5 ~issue_type_r2 : _ t0 -> IssueType.t option =
    fun ct ->
     if has_risky ct then Some issue_type_r2
@@ -515,8 +517,19 @@ module BinaryOperationCondition = struct
     (not cannot_underflow, not cannot_overflow)
 
 
-  let check ({binop; typ; integer_widths; lhs; rhs} as c) =
-    if is_mult_one binop lhs rhs then {report_issue_type= NotIssue; propagate= false}
+  let is_deliberate_integer_overflow =
+    let whitelist = ["lfsr"; "prng"; "rand"; "seed"] in
+    let f x =
+      List.exists whitelist ~f:(fun whitelist -> String.is_substring x ~substring:whitelist)
+    in
+    fun {typ; lhs; rhs} ct ->
+      Typ.ikind_is_unsigned typ
+      && (ConditionTrace.exists_str ~f ct || ItvPure.exists_str ~f lhs || ItvPure.exists_str ~f rhs)
+
+
+  let check ({binop; typ; integer_widths; lhs; rhs} as c) (trace : ConditionTrace.t) =
+    if is_mult_one binop lhs rhs || is_deliberate_integer_overflow c trace then
+      {report_issue_type= NotIssue; propagate= false}
     else
       let v =
         match binop with
@@ -658,13 +671,14 @@ module Condition = struct
         BinaryOperationCondition.pp_description ~markup fmt c
 
 
-  let check = function
+  let check cond trace =
+    match cond with
     | AllocSize c ->
         AllocSizeCondition.check c
     | ArrayAccess c ->
         ArrayAccessCondition.check c
     | BinaryOperation c ->
-        BinaryOperationCondition.check c
+        BinaryOperationCondition.check c trace
 
 
   let forget_locs locs x =
@@ -750,7 +764,7 @@ module ConditionWithTrace = struct
 
 
   let check cwt =
-    let ({report_issue_type; propagate} as checked) = Condition.check cwt.cond in
+    let ({report_issue_type; propagate} as checked) = Condition.check cwt.cond cwt.trace in
     match report_issue_type with
     | NotIssue | SymbolicIssue ->
         checked

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -105,6 +105,25 @@ module BoTrace = struct
 
   let has_risky = final_exists ~f:(function UnknownFrom _ -> false | RiskyLibCall _ -> true)
 
+  let exists_str ~f =
+    let rec helper = function
+      | Empty | Final _ ->
+          false
+      | Elem {kind= elem; from} ->
+          ( match elem with
+          | Assign locs ->
+              PowLoc.exists_str ~f locs
+          | Parameter l ->
+              Loc.exists_str ~f l
+          | _ ->
+              false )
+          || helper from
+      | Call {caller; callee} ->
+          helper caller || helper callee
+    in
+    helper
+
+
   let final_err_desc = function
     | UnknownFrom pname_opt ->
         F.asprintf "Unknown value from: %a" pp_pname_opt pname_opt
@@ -187,6 +206,8 @@ module Set = struct
 
   let has_risky t = exists BoTrace.has_risky t
 
+  let exists_str ~f t = exists (BoTrace.exists_str ~f) t
+
   let make_err_trace depth set tail =
     if is_empty set then tail else BoTrace.make_err_trace depth (choose_shortest set) tail
 
@@ -232,6 +253,8 @@ module Issue = struct
 
   let has_risky = has_common ~f:Set.has_risky
 
+  let exists_str ~f = has_common ~f:(Set.exists_str ~f)
+
   let binary_labels = function ArrayAccess -> ("Offset", "Length") | Binop -> ("LHS", "RHS")
 
   let pp_elem f = function Alloc -> F.pp_print_string f "Alloc"

infer/src/bufferoverrun/itv.ml

@@ -50,6 +50,8 @@ module ItvPure = struct
 
   let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false
 
+  let exists_str ~f (l, u) = Bound.exists_str ~f l || Bound.exists_str ~f u
+
   let ( <= ) : lhs:t -> rhs:t -> bool =
    fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2
 

infer/src/bufferoverrun/itv.mli

@@ -96,6 +96,8 @@ module ItvPure : sig
   val succ : t -> t
 
   val mult : t -> t -> t
+
+  val exists_str : f:(string -> bool) -> t -> bool
 end
 
 include module type of AbstractDomain.BottomLifted (ItvPure)

infer/src/bufferoverrun/symb.ml

@@ -127,6 +127,20 @@ module SymbolPath = struct
         false
     | Deref (_, p) | Field (_, p) ->
         represents_callsite_sound_partial p
+
+
+  let rec exists_str_partial ~f = function
+    | Pvar pvar ->
+        f (Pvar.to_string pvar)
+    | Deref (_, x) ->
+        exists_str_partial ~f x
+    | Field (fld, x) ->
+        f (Typ.Fieldname.to_string fld) || exists_str_partial ~f x
+    | Callsite _ ->
+        false
+
+
+  let exists_str ~f = function Normal p | Offset p | Length p -> exists_str_partial ~f p
 end
 
 module Symbol = struct
@@ -195,6 +209,9 @@ module Symbol = struct
 
   let assert_bound_end s be =
     match s with OneValue _ -> () | BoundEnd {bound_end} -> assert (BoundEnd.equal be bound_end)
+
+
+  let exists_str ~f = function OneValue {path} | BoundEnd {path} -> SymbolPath.exists_str ~f path
 end
 
 module SymbolSet = struct

infer/src/bufferoverrun/symb.mli

@@ -57,6 +57,8 @@ module SymbolPath : sig
   val represents_multiple_values_sound : partial -> bool
 
   val represents_callsite_sound_partial : partial -> bool
+
+  val exists_str_partial : f:(string -> bool) -> partial -> bool
 end
 
 module Symbol : sig
@@ -81,6 +83,8 @@ module Symbol : sig
   val make_onevalue : unsigned:bool -> SymbolPath.t -> t
 
   val make_boundend : BoundEnd.t -> unsigned:bool -> SymbolPath.t -> t
+
+  val exists_str : f:(string -> bool) -> t -> bool
 end
 
 module SymbolSet : sig

infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp

@@ -4,6 +4,8 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  */
+#include <cstdint>
+
 void sizeof_bool_Good() {
   int a[2];
   int z = sizeof(bool); // z is 1 (byte)
@@ -55,3 +57,61 @@ void bool_overflow2_Good_FP() {
     a[5] = 0;
   }
 }
+
+class RG {
+ public:
+  RG(uint32_t init) {
+    seed = init;
+    x = init;
+  }
+
+  inline uint32_t integer_overflow_rand() {
+    uint32_t max = 4294967295;
+    return (seed = seed * max);
+  }
+
+  inline uint32_t integer_overflow_x() {
+    uint32_t max = 4294967295;
+    return (x = x * max);
+  }
+
+ private:
+  uint32_t seed;
+  uint32_t x;
+};
+
+uint32_t call_integer_overflow_rand_Good() {
+  RG generator(4294967295);
+  return generator.integer_overflow_rand();
+}
+
+uint32_t call_integer_overflow_x_Bad() {
+  RG generator(4294967295);
+  return generator.integer_overflow_x();
+}
+
+struct S_prng_lfsr {
+  uint32_t prng_lfsr;
+};
+
+void integer_overflow_field_Good(struct S_prng_lfsr* c) {
+  c->prng_lfsr = 1;
+  c->prng_lfsr = 0 - c->prng_lfsr;
+}
+
+struct S_x {
+  uint32_t x;
+};
+
+void integer_overflow_field_Bad(struct S_x* c) {
+  c->x = 1;
+  c->x = 0 - c->x;
+}
+
+uint32_t integer_overflow_param_1(uint32_t seed) { return seed - 1; }
+
+void call_integer_overflow_param_1_Good() { integer_overflow_param_1(0); }
+
+uint32_t integer_overflow_param_2(uint32_t x) { return x - 1; }
+
+void call_integer_overflow_param_2_Bad() { integer_overflow_param_2(0); }

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

@@ -8,6 +8,9 @@ codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Bad, 2, CONDITION_ALWAY
 codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/arith.cpp, call_integer_overflow_param_2_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `x`,Binary operation: (0 - 1):unsigned32 by call to `integer_overflow_param_2` ]
+codetoanalyze/cpp/bufferoverrun/arith.cpp, call_integer_overflow_x_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter `init`,Assignment,Call,<LHS trace>,Parameter `this->x`,<RHS trace>,Assignment,Binary operation: (4294967295 × 4294967295):unsigned32 by call to `RG_integer_overflow_x` ]
+codetoanalyze/cpp/bufferoverrun/arith.cpp, integer_overflow_field_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]