[inferbo][easy] Shift right zero

Reviewed By: ezgicicek

Differential Revision: D13517435

fbshipit-source-id: fa107fc2c

infer/src/bufferoverrun/itv.ml

@@ -263,15 +263,17 @@ module ItvPure = struct
   (* x >> [-1,-1] does nothing. *)
   let shiftrt : t -> t -> t =
    fun x y ->
-    match is_const y with
+    if is_zero x then x
-    | Some n when Z.(leq n zero) ->
+    else
-        x
+      match is_const y with
-    | Some n when Z.(n >= of_int 64) ->
+      | Some n when Z.(leq n zero) ->
-        zero
+          x
-    | Some n -> (
+      | Some n when Z.(n >= of_int 64) ->
-      match Z.to_int n with n -> div_const x Z.(one lsl n) | exception Z.Overflow -> top )
+          zero
-    | None ->
+      | Some n -> (
-        top
+        match Z.to_int n with n -> div_const x Z.(one lsl n) | exception Z.Overflow -> top )
+      | None ->
+          top
 
 
   let band_sem : t -> t -> t =

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

@@ -530,3 +530,15 @@ int check_addition_overflow_Good(unsigned int x, unsigned int y) {
     return 0;
   }
 }
+
+void shift_right_zero_Good(int x) {
+  int arr[1];
+  arr[0 >> x] = 1;
+}
+
+/* This also exhibits an overapproximation of traces, here [x] doesn't influence
+ * the result */
+void shift_right_zero_Bad(int x) {
+  int arr[1];
+  arr[1 + (0 >> x)] = 1;
+}

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

@@ -35,6 +35,7 @@ codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Bad, 3, INTEGER
 codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Good_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, 9] - 1):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, scan_hex_Good, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/arith.c, scan_hex_Good, 8, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/arith.c, shift_right_zero_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, simple_overflow_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Binary operation: (85 × 4294967295):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, two_safety_conditions2_Bad, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] + [0, 80]):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]