From 3483ec72a1fc86461f70bbdf23986a52c4ea90b7 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 26 Apr 2019 12:03:29 -0700 Subject: [PATCH] [sledge] Do not normalize shifts by enough bits to be undefined Summary: Shifting by too many bits is undefined, so do not normalize them. Reviewed By: mbouaziz Differential Revision: D15098812 fbshipit-source-id: 96f4606d7 --- sledge/src/llair/exp.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index cb8b40a64..ea8deefda 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -1054,8 +1054,8 @@ let simp_xor x y = let simp_shl x y = match (x, y) with (* i shl j *) - | Integer {data= i; typ}, Integer {data= j} when Z.fits_int j -> - let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} + when Z.sign j >= 0 && Z.lt j (Z.of_int bits) -> integer (Z.bshift_left ~bits i (Z.to_int j)) typ (* e shl 0 ==> e *) | e, Integer {data} when Z.equal Z.zero data -> e @@ -1064,8 +1064,8 @@ let simp_shl x y = let simp_lshr x y = match (x, y) with (* i lshr j *) - | Integer {data= i; typ}, Integer {data= j} when Z.fits_int j -> - let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} + when Z.sign j >= 0 && Z.lt j (Z.of_int bits) -> integer (Z.bshift_right_trunc ~bits i (Z.to_int j)) typ (* e lshr 0 ==> e *) | e, Integer {data} when Z.equal Z.zero data -> e @@ -1074,8 +1074,8 @@ let simp_lshr x y = let simp_ashr x y = match (x, y) with (* i ashr j *) - | Integer {data= i; typ}, Integer {data= j} when Z.fits_int j -> - let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} + when Z.sign j >= 0 && Z.lt j (Z.of_int bits) -> integer (Z.bshift_right ~bits i (Z.to_int j)) typ (* e ashr 0 ==> e *) | e, Integer {data} when Z.equal Z.zero data -> e