Added constant-folding support for shifting

Reviewed By: jeremydubreil

Differential Revision: D5485475

fbshipit-source-id: 424a88a

infer/src/IR/IntLit.ml

@@ -103,6 +103,24 @@ let lognot i = lift1 Int64.bit_not i
 
 let sub i1 i2 = add i1 (neg i2)
 
+let shift_left (unsigned1, i1, ptr1) (_, i2, _) =
+  match Int64.to_int i2 with
+  | None
+   -> failwithf "Shifting failed with operand %a" Int64.pp i2
+  | Some i2
+   -> if i2 < 0 || i2 >= 64 then failwithf "Oversized shift: %d" i2 ;
+      let res = Int64.shift_left i1 i2 in
+      (unsigned1, res, ptr1)
+
+let shift_right (unsigned1, i1, ptr1) (_, i2, _) =
+  match Int64.to_int i2 with
+  | None
+   -> failwithf "Shifting failed with operand %a" Int64.pp i2
+  | Some i2
+   -> if i2 < 0 || i2 >= 64 then failwithf "Oversized shift: %d" i2 ;
+      let res = Int64.shift_right i1 i2 in
+      (unsigned1, res, ptr1)
+
 let pp f (unsigned, n, ptr) =
   if ptr && Int64.equal n 0L then F.fprintf f "null"
   else if unsigned then F.fprintf f "%Lu" n

infer/src/IR/IntLit.mli

@@ -78,6 +78,15 @@ val pp : F.formatter -> t -> unit
 
 val rem : t -> t -> t
 
+val shift_left : t -> t -> t
+
+(* shift_right performs arithmetic shift, for the following reasons: *)
+(* In C++, whether right shift is logical or arithmetical is implementation defined.
+ * Usually an arithmetic shift is implemented. *)
+(* In Java, the current frontend refuses to translate logical right shift. *)
+
+val shift_right : t -> t -> t
+
 val sub : t -> t -> t
 
 val to_int : t -> int

infer/src/backend/prop.ml

@@ -992,9 +992,33 @@ module Normalize = struct
           | _
            -> if abs then Exp.get_undefined false else BinOp (Mod, e1', e2') )
       | BinOp (Shiftlt, e1, e2)
-       -> if abs then Exp.get_undefined false else BinOp (Shiftlt, eval e1, eval e2)
+       -> (
+          if abs then Exp.get_undefined false
+          else
+            match (e1, e2) with
+            | Const Cint n, Const Cint m
+             -> Exp.int (IntLit.shift_left n m)
+            | _, Const Cint m when IntLit.iszero m
+             -> eval e1
+            | _, Const Cint m when IntLit.isone m
+             -> eval (Exp.BinOp (PlusA, e1, e1))
+            | Const Cint m, _ when IntLit.iszero m
+             -> e1
+            | _
+             -> BinOp (Shiftlt, eval e1, eval e2) )
       | BinOp (Shiftrt, e1, e2)
-       -> if abs then Exp.get_undefined false else BinOp (Shiftrt, eval e1, eval e2)
+       -> (
+          if abs then Exp.get_undefined false
+          else
+            match (e1, e2) with
+            | Const Cint n, Const Cint m
+             -> Exp.int (IntLit.shift_right n m)
+            | _, Const Cint m when IntLit.iszero m
+             -> eval e1
+            | Const Cint m, _ when IntLit.iszero m
+             -> e1
+            | _
+             -> BinOp (Shiftrt, eval e1, eval e2) )
       | BinOp (BAnd, e1, e2)
        -> (
           let e1' = eval e1 in

infer/tests/codetoanalyze/c/biabduction/Makefile

@@ -9,7 +9,7 @@ TESTS_DIR = ../../..
 
 ANALYZER = checkers
 CLANG_OPTIONS = -c
-INFER_OPTIONS = --biabduction --project-root $(TESTS_DIR)
+INFER_OPTIONS = --biabduction --debug-exceptions --project-root $(TESTS_DIR)
 
 INFERPRINT_OPTIONS = --issues-tests
 

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

@@ -1,3 +1,7 @@
+codetoanalyze/c/biabduction/abduce.c, FN_set_ptr_param_array_get_null_bad, 3, PRECONDITION_NOT_MET, [start of procedure FN_set_ptr_param_array_get_null_bad()]
+codetoanalyze/c/biabduction/example.c, bar, 2, DIVIDE_BY_ZERO, [start of procedure bar()]
 codetoanalyze/c/biabduction/example.c, foo, 2, NULL_DEREFERENCE, [start of procedure foo()]
 codetoanalyze/c/biabduction/example.c, global_addr_alias_bad, 3, NULL_DEREFERENCE, [start of procedure global_addr_alias_bad(),Condition is true]
 codetoanalyze/c/biabduction/example.c, local_addr_noalias_bad, 4, NULL_DEREFERENCE, [start of procedure local_addr_noalias_bad(),Condition is true]
+codetoanalyze/c/biabduction/shift.c, return_null_deref1_bad, 2, NULL_DEREFERENCE, [start of procedure return_null_deref1_bad(),start of procedure return_depends_on_lshift(),Condition is true,return from a call to return_depends_on_lshift]
+codetoanalyze/c/biabduction/shift.c, return_null_deref2_bad, 2, NULL_DEREFERENCE, [start of procedure return_null_deref2_bad(),start of procedure return_depends_on_rshift(),Condition is true,return from a call to return_depends_on_rshift]

infer/tests/codetoanalyze/c/biabduction/shift.c

@@ -0,0 +1,41 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+int* return_depends_on_lshift(int x, int* p) {
+  if (x < (1 << 7))
+    return 0;
+  else
+    return p;
+}
+
+int return_nonnull_deref1_ok() {
+  int y = 0;
+  return *return_depends_on_lshift(1000, &y);
+}
+
+int return_null_deref1_bad() {
+  int y = 0;
+  return *return_depends_on_lshift(0, &y);
+}
+
+int* return_depends_on_rshift(int x, int* p) {
+  if (x < (4 >> 2))
+    return 0;
+  else
+    return p;
+}
+
+int return_nonnull_deref2_ok() {
+  int y = 0;
+  return *return_depends_on_rshift(2, &y);
+}
+
+int return_null_deref2_bad() {
+  int y = 0;
+  return *return_depends_on_rshift(0, &y);
+}