From 8abfcfb50489e63ef893625c8416624e19ee299e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 8 Oct 2019 11:38:36 -0700
Subject: [PATCH] [sledge] Simplify normalization of shift operations

Summary:
Remove the guards that prevent normalizing in some cases where the
corresponding instruction in LLVM would produce a poison
value. Usefully tracking poison values will be more involved.

Reviewed By: ngorogiannis

Differential Revision: D17665230

fbshipit-source-id: 59fb25042
---
 sledge/src/symbheap/term.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/sledge/src/symbheap/term.ml b/sledge/src/symbheap/term.ml
index 55874aa2c..049c96088 100644
--- a/sledge/src/symbheap/term.ml
+++ b/sledge/src/symbheap/term.ml
@@ -998,8 +998,7 @@ let simp_xor x y =
 let simp_shl x y =
   match (x, y) with
   (* i shl j *)
-  | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
-    when Z.sign j >= 0 && Z.lt j (Z.of_int bits) ->
+  | Integer {data= i; typ}, Integer {data= j} when Z.sign j >= 0 ->
       integer (Z.shift_left i (Z.to_int j)) typ
   (* e shl 0 ==> e *)
   | e, Integer {data} when Z.equal Z.zero data -> e
@@ -1008,8 +1007,7 @@ let simp_shl x y =
 let simp_lshr x y =
   match (x, y) with
   (* i lshr j *)
-  | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
-    when Z.sign j >= 0 && Z.lt j (Z.of_int bits) ->
+  | Integer {data= i; typ}, Integer {data= j} when Z.sign j >= 0 ->
       integer (Z.shift_right_trunc i (Z.to_int j)) typ
   (* e lshr 0 ==> e *)
   | e, Integer {data} when Z.equal Z.zero data -> e
@@ -1018,8 +1016,7 @@ let simp_lshr x y =
 let simp_ashr x y =
   match (x, y) with
   (* i ashr j *)
-  | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
-    when Z.sign j >= 0 && Z.lt j (Z.of_int bits) ->
+  | Integer {data= i; typ}, Integer {data= j} when Z.sign j >= 0 ->
       integer (Z.shift_right i (Z.to_int j)) typ
   (* e ashr 0 ==> e *)
   | e, Integer {data} when Z.equal Z.zero data -> e