From 8602b709effc360e2bc94bd8e0f7ad7490731577 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Thu, 1 Apr 2021 10:24:45 -0700
Subject: [PATCH] [pulse][arith] change bit shifts by a constant factor into
 multiplications

Summary:
When we don't know the value being shifted it may help to translate
bit-shifting into multiplication by a constant as it might surface
linear terms, eg `x<<1` is `2*x`.

Reviewed By: skcho

Differential Revision: D27464847

fbshipit-source-id: 9b3b5f0d0
---
 infer/src/pulse/PulseFormula.ml                | 18 ++++++++++++++++++
 infer/tests/codetoanalyze/cpp/pulse/values.cpp | 14 ++++++++++++++
 2 files changed, 32 insertions(+)

diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml
index 89de14d4d..5d98babb8 100644
--- a/infer/src/pulse/PulseFormula.ml
+++ b/infer/src/pulse/PulseFormula.ml
@@ -647,6 +647,24 @@ module Term = struct
         zero
     | (BitShiftLeft (t1, t2) | BitShiftRight (t1, t2)) when is_zero t2 ->
         t1
+    | BitShiftLeft (t', Const q) | BitShiftRight (t', Const q) -> (
+      match Q.to_int q with
+      | None ->
+          (* overflows or otherwise undefined, propagate puzzlement *)
+          Const Q.undef
+      | Some i -> (
+          if i >= 64 then (* assume 64-bit or fewer architecture *) zero
+          else if i < 0 then (* this is undefined, maybe we should report a bug here *)
+            Const Q.undef
+          else
+            let factor = Const Q.(of_int 1 lsl i) in
+            match[@warning "-8"] t with
+            | BitShiftLeft _ ->
+                simplify_shallow_ (Mult (t', factor))
+            | BitShiftRight _ ->
+                simplify_shallow_ (Div (t', factor)) ) )
+    | (BitShiftLeft (t1, t2) | BitShiftRight (t1, t2)) when is_zero t2 ->
+        t1
     | And (t1, t2) when is_zero t1 || is_zero t2 ->
         (* [false ∧ t = t ∧ false = false] *) zero
     | And (t1, t2) when is_non_zero_const t1 ->
diff --git a/infer/tests/codetoanalyze/cpp/pulse/values.cpp b/infer/tests/codetoanalyze/cpp/pulse/values.cpp
index 283d30d85..5d428749a 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/values.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/values.cpp
@@ -155,3 +155,17 @@ void FP_ints_are_not_rationals_ok() {
     *p = 42;
   }
 }
+
+void shift_equal_mult_by_power_of_two_ok(int x) {
+  if (x << 1 != mult(2, x)) {
+    int* p = nullptr;
+    *p = 42;
+  }
+}
+
+void shift_by_too_much_ok(int x) {
+  if (x << 64 != 0 || x >> 4000 != 0) {
+    int* p = nullptr;
+    *p = 42;
+  }
+}