[inferbo] Suppress integer overflow in hash functions

Summary: This diff suppresses integer overflow issues in functions that includes "hash" in its name.

Reviewed By: jvillard

Differential Revision: D19942654

fbshipit-source-id: d86fa4f00

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -198,7 +198,7 @@ let check_expr_for_array_access :
         cond_set
 
 
-let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set =
+let check_binop_for_integer_overflow integer_type_widths pname 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
@@ -206,32 +206,32 @@ let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location
       let lhs_v = Sem.eval integer_type_widths lhs mem in
       let rhs_v = Sem.eval integer_type_widths rhs mem in
       let latest_prune = Dom.Mem.get_latest_prune mem in
-      BoUtils.Check.binary_operation integer_type_widths bop ~lhs:lhs_v ~rhs:rhs_v ~latest_prune
-        location cond_set
+      BoUtils.Check.binary_operation integer_type_widths pname bop ~lhs:lhs_v ~rhs:rhs_v
+        ~latest_prune location cond_set
   | _ ->
       cond_set
 
 
-let rec check_expr_for_integer_overflow integer_type_widths exp location mem cond_set =
+let rec check_expr_for_integer_overflow integer_type_widths pname exp location mem cond_set =
   match exp with
   | Exp.UnOp (_, e, _)
   | Exp.Exn e
   | Exp.Lfield (e, _, _)
   | Exp.Cast (_, e)
   | Exp.Sizeof {dynamic_length= Some e} ->
-      check_expr_for_integer_overflow integer_type_widths e location mem cond_set
+      check_expr_for_integer_overflow integer_type_widths pname e location mem cond_set
   | Exp.BinOp (bop, lhs, rhs) ->
       cond_set
-      |> check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem
-      |> check_expr_for_integer_overflow integer_type_widths lhs location mem
-      |> check_expr_for_integer_overflow integer_type_widths rhs location mem
+      |> check_binop_for_integer_overflow integer_type_widths pname bop ~lhs ~rhs location mem
+      |> check_expr_for_integer_overflow integer_type_widths pname lhs location mem
+      |> check_expr_for_integer_overflow integer_type_widths pname rhs location mem
   | Exp.Lindex (e1, e2) ->
       cond_set
-      |> check_expr_for_integer_overflow integer_type_widths e1 location mem
-      |> check_expr_for_integer_overflow integer_type_widths e2 location mem
+      |> check_expr_for_integer_overflow integer_type_widths pname e1 location mem
+      |> check_expr_for_integer_overflow integer_type_widths pname e2 location mem
   | Exp.Closure {captured_vars} ->
       List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) ->
-          check_expr_for_integer_overflow integer_type_widths e location mem cond_set )
+          check_expr_for_integer_overflow integer_type_widths pname e location mem cond_set )
   | Exp.Var _ | Exp.Const _ | Exp.Lvar _ | Exp.Sizeof {dynamic_length= None} ->
       cond_set
 
@@ -275,17 +275,17 @@ let check_instr :
   | Sil.Load {e= exp; loc= location} ->
       cond_set
       |> check_expr_for_array_access integer_type_widths exp location mem
-      |> check_expr_for_integer_overflow integer_type_widths exp location mem
+      |> check_expr_for_integer_overflow integer_type_widths pname exp location mem
   | Sil.Store {e1= lexp; e2= rexp; loc= location} ->
       cond_set
       |> check_expr_for_array_access integer_type_widths lexp location mem
       |> check_expr_for_array_access ~sub_expr_only:true integer_type_widths rexp location mem
-      |> check_expr_for_integer_overflow integer_type_widths lexp location mem
-      |> check_expr_for_integer_overflow integer_type_widths rexp location mem
+      |> check_expr_for_integer_overflow integer_type_widths pname lexp location mem
+      |> check_expr_for_integer_overflow integer_type_widths pname rexp location mem
   | Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> (
       let cond_set =
         List.fold params ~init:cond_set ~f:(fun cond_set (exp, _) ->
-            check_expr_for_integer_overflow integer_type_widths exp location mem cond_set )
+            check_expr_for_integer_overflow integer_type_widths pname exp location mem cond_set )
       in
       let fun_arg_list =
         List.map params ~f:(fun (exp, typ) ->
@@ -310,7 +310,7 @@ let check_instr :
           | _, _ ->
               (* unknown call / no inferbo payload *) cond_set ) )
   | Sil.Prune (exp, location, _, _) ->
-      check_expr_for_integer_overflow integer_type_widths exp location mem cond_set
+      check_expr_for_integer_overflow integer_type_widths pname exp location mem cond_set
   | _ ->
       cond_set
 

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -436,7 +436,8 @@ module BinaryOperationCondition = struct
     ; typ: Typ.ikind
     ; integer_widths: Typ.IntegerWidths.t
     ; lhs: ItvPure.t
-    ; rhs: ItvPure.t }
+    ; rhs: ItvPure.t
+    ; pname: Procname.t }
   [@@deriving compare]
 
   let get_symbols c = Symb.SymbolSet.union (ItvPure.get_symbols c.lhs) (ItvPure.get_symbols c.rhs)
@@ -529,13 +530,15 @@ module BinaryOperationCondition = struct
 
 
   let is_deliberate_integer_overflow =
-    let whitelist = ["lfsr"; "prng"; "rand"; "seed"] in
+    let whitelist = ["hash"; "lfsr"; "prng"; "rand"; "seed"] in
     let f x =
+      let x = String.lowercase x in
       List.exists whitelist ~f:(fun whitelist -> String.is_substring x ~substring:whitelist)
     in
-    fun {typ; lhs; rhs} ct ->
+    fun {typ; lhs; rhs; pname} ct ->
       Typ.ikind_is_unsigned typ
-      && (ConditionTrace.exists_str ~f ct || ItvPure.exists_str ~f lhs || ItvPure.exists_str ~f rhs)
+      && ( ConditionTrace.exists_str ~f ct || ItvPure.exists_str ~f lhs || ItvPure.exists_str ~f rhs
+         || f (Procname.to_simplified_string pname) )
 
 
   let check ({binop; typ; integer_widths; lhs; rhs} as c) (trace : ConditionTrace.t) =
@@ -580,7 +583,7 @@ module BinaryOperationCondition = struct
         {report_issue_type; propagate= is_symbolic}
 
 
-  let make integer_widths bop ~lhs ~rhs =
+  let make integer_widths pname bop ~lhs ~rhs =
     if ItvPure.is_invalid lhs || ItvPure.is_invalid rhs then None
     else
       let binop, typ =
@@ -595,7 +598,7 @@ module BinaryOperationCondition = struct
             L.(die InternalError)
               "Unexpected type %s is given to BinaryOperationCondition." (Binop.str Pp.text bop)
       in
-      Some {binop; typ; integer_widths; lhs; rhs}
+      Some {binop; typ; integer_widths; lhs; rhs; pname}
 end
 
 module Condition = struct
@@ -923,9 +926,9 @@ module ConditionSet = struct
     |> add_opt location (ValTrace.Issue.alloc location val_traces) latest_prune condset
 
 
-  let add_binary_operation integer_type_widths location bop ~lhs ~rhs ~lhs_traces ~rhs_traces
+  let add_binary_operation integer_type_widths location pname bop ~lhs ~rhs ~lhs_traces ~rhs_traces
       ~latest_prune condset =
-    BinaryOperationCondition.make integer_type_widths bop ~lhs ~rhs
+    BinaryOperationCondition.make integer_type_widths pname bop ~lhs ~rhs
     |> Condition.make_binary_operation
     |> add_opt location
          (ValTrace.Issue.(binary location Binop) lhs_traces rhs_traces)

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -58,6 +58,7 @@ module ConditionSet : sig
   val add_binary_operation :
        Typ.IntegerWidths.t
     -> Location.t
+    -> Procname.t
     -> Binop.t
     -> lhs:ItvPure.t
     -> rhs:ItvPure.t

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -318,7 +318,7 @@ module Check = struct
     array_access_byte ~arr ~idx ~is_plus:true ~last_included ~latest_prune location cond_set
 
 
-  let binary_operation integer_type_widths bop ~lhs ~rhs ~latest_prune location cond_set =
+  let binary_operation integer_type_widths pname bop ~lhs ~rhs ~latest_prune location cond_set =
     let lhs_itv = Dom.Val.get_itv lhs in
     let rhs_itv = Dom.Val.get_itv rhs in
     match (lhs_itv, rhs_itv) with
@@ -326,7 +326,7 @@ module Check = struct
         L.(debug BufferOverrun Verbose)
           "@[<v 2>Add condition :@,bop:%s@,  lhs: %a@,  rhs: %a@,@]@." (Binop.str Pp.text bop)
           Itv.ItvPure.pp lhs_itv Itv.ItvPure.pp rhs_itv ;
-        PO.ConditionSet.add_binary_operation integer_type_widths location bop ~lhs:lhs_itv
+        PO.ConditionSet.add_binary_operation integer_type_widths location pname bop ~lhs:lhs_itv
           ~rhs:rhs_itv ~lhs_traces:(Dom.Val.get_traces lhs) ~rhs_traces:(Dom.Val.get_traces rhs)
           ~latest_prune cond_set
     | _, _ ->

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -84,6 +84,7 @@ module Check : sig
 
   val binary_operation :
        Typ.IntegerWidths.t
+    -> Procname.t
     -> Binop.t
     -> lhs:Dom.Val.t
     -> rhs:Dom.Val.t

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

@@ -117,6 +117,12 @@ uint32_t integer_overflow_param_2(uint32_t x) { return x - 1; }
 
 void call_integer_overflow_param_2_Bad() { integer_overflow_param_2(0); }
 
+// "HaSh" (not "hash") is fot checking case-insensitive comparison.
+void whitelisted_HaSh_Good() {
+  uint32_t x = -1;
+  uint32_t y = x * 8;
+}
+
 void mod_ub(const char* msg, size_t leng) {
   size_t rem = leng % 32;
   if (rem == 15) {