[inferbo] Do not raise integer overflow when multiplying 1

Summary: We assume multiplication of 1 is safe. It happens sometimes by multiplying `sizeof(char)`.

Reviewed By: mbouaziz

Differential Revision: D10444680

fbshipit-source-id: 2f33be280

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -360,40 +360,46 @@ module BinaryOperationCondition = struct
 
   let pp_description = pp
 
+  let is_mult_one binop lhs rhs =
+    equal_binop binop Mult && (ItvPure.is_one lhs || ItvPure.is_one rhs)
+
+
   let check {binop; typ; integer_widths; lhs; rhs} =
-    let v =
-      match binop with
-      | Plus ->
-          ItvPure.plus lhs rhs
-      | Minus ->
-          ItvPure.minus lhs rhs
-      | Mult ->
-          ItvPure.mult lhs rhs
-    in
-    let v_lb, v_ub = (ItvPure.lb v, ItvPure.ub v) in
-    let typ_lb, typ_ub =
-      let lb, ub = Typ.range_of_ikind integer_widths typ in
-      (Bound.of_big_int lb, Bound.of_big_int ub)
-    in
-    if
-      (* typ_lb <= v_lb and v_ub <= typ_ub, not an error *)
-      Bound.le v_ub typ_ub && Bound.le typ_lb v_lb
-    then {report_issue_type= None; propagate= false}
-    else if
-      (* v_ub < typ_lb or typ_ub < v_lb, definitely an error *)
-      Bound.lt v_ub typ_lb || Bound.lt typ_ub v_lb
-    then {report_issue_type= Some IssueType.integer_overflow_l1; propagate= false}
-    else if
-      (* -oo != v_lb < typ_lb or typ_ub < v_ub != +oo, probably an error *)
-      (Bound.lt v_lb typ_lb && Bound.is_not_infty v_lb)
-      || (Bound.lt typ_ub v_ub && Bound.is_not_infty v_ub)
-    then {report_issue_type= Some IssueType.integer_overflow_l2; propagate= false}
+    if is_mult_one binop lhs rhs then {report_issue_type= None; propagate= false}
     else
-      let is_symbolic = ItvPure.is_symbolic v in
-      let report_issue_type =
-        if Config.bo_debug <= 3 && is_symbolic then None else Some IssueType.integer_overflow_l5
+      let v =
+        match binop with
+        | Plus ->
+            ItvPure.plus lhs rhs
+        | Minus ->
+            ItvPure.minus lhs rhs
+        | Mult ->
+            ItvPure.mult lhs rhs
       in
-      {report_issue_type; propagate= is_symbolic}
+      let v_lb, v_ub = (ItvPure.lb v, ItvPure.ub v) in
+      let typ_lb, typ_ub =
+        let lb, ub = Typ.range_of_ikind integer_widths typ in
+        (Bound.of_big_int lb, Bound.of_big_int ub)
+      in
+      if
+        (* typ_lb <= v_lb and v_ub <= typ_ub, not an error *)
+        Bound.le v_ub typ_ub && Bound.le typ_lb v_lb
+      then {report_issue_type= None; propagate= false}
+      else if
+        (* v_ub < typ_lb or typ_ub < v_lb, definitely an error *)
+        Bound.lt v_ub typ_lb || Bound.lt typ_ub v_lb
+      then {report_issue_type= Some IssueType.integer_overflow_l1; propagate= false}
+      else if
+        (* -oo != v_lb < typ_lb or typ_ub < v_ub != +oo, probably an error *)
+        (Bound.lt v_lb typ_lb && Bound.is_not_infty v_lb)
+        || (Bound.lt typ_ub v_ub && Bound.is_not_infty v_ub)
+      then {report_issue_type= Some IssueType.integer_overflow_l2; propagate= false}
+      else
+        let is_symbolic = ItvPure.is_symbolic v in
+        let report_issue_type =
+          if Config.bo_debug <= 3 && is_symbolic then None else Some IssueType.integer_overflow_l5
+        in
+        {report_issue_type; propagate= is_symbolic}
 
 
   let make integer_widths bop ~lhs ~rhs =

infer/src/bufferoverrun/itv.ml

@@ -568,6 +568,8 @@ module ItvPure = struct
 
   let is_zero : t -> bool = fun (l, u) -> Bound.is_zero l && Bound.is_zero u
 
+  let is_one : t -> bool = fun (l, u) -> Bound.eq l Bound.one && Bound.eq u Bound.one
+
   let is_true : t -> bool = fun (l, u) -> Bound.le Bound.one l || Bound.le u Bound.mone
 
   let is_false : t -> bool = is_zero

infer/src/bufferoverrun/itv.mli

@@ -98,6 +98,8 @@ module ItvPure : sig
 
   val is_top : t -> bool
 
+  val is_one : t -> bool
+
   val ( <= ) : lhs:t -> rhs:t -> bool
 
   val have_similar_bounds : t -> t -> bool

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

@@ -178,3 +178,15 @@ void use_uint64_max_Bad_FN() {
   uint64_t y = UINT64_MAX - 15;
   arr[x - y] = 0;
 }
+
+uint64_t unknown_uint();
+
+void muliply_one_Good() {
+  uint64_t x = unknown_uint();
+  uint64_t y = x * 1;
+}
+
+void muliply_two_Bad() {
+  uint64_t x = unknown_uint();
+  uint64_t y = x * 2;
+}

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

@@ -7,6 +7,7 @@ codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, I
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5]
+codetoanalyze/c/bufferoverrun/arith.c, muliply_two_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([-oo, +oo] * 2):unsigned64]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19]