Fix definitions of sbvRotate{Left,Right} for large rotation amounts;

Also add regression tests for symbolic rotations.

Fixes #160.

sbv/Data/SBV/BitVectors/Model.hs

@@ -899,20 +899,30 @@ sbvSignedShiftArithRight x i
 -- | Generalization of 'rotateL', when the shift-amount is symbolic. Since Haskell's
 -- 'rotateL' only takes an 'Int' as the shift amount, it cannot be used when we have
 -- a symbolic amount to shift with. The shift amount must be an unsigned quantity.
-sbvRotateLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
+sbvRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a
 sbvRotateLeft x i
-  | isSigned i = error "sbvRotateLeft: shift amount should be unsigned"
-  | True       = select [x `rotateL` k | k <- [0 .. ghcBitSize x - 1]] z i
-    where z = sbvFromInteger (kindOf x) 0
+  | isSigned i             = error "sbvRotateLeft: rotation amount should be unsigned"
+  | bit si <= toInteger sx = select [x `rotateL` k | k <- [0 .. bit si - 1]] z i
+                             -- ^ wrap-around not possible
+  | True                   = select [x `rotateL` k | k <- [0 .. sx - 1]] z (i `sRem` n)
+    where sx = ghcBitSize x
+          si = ghcBitSize i
+          z = sbvFromInteger (kindOf x) 0
+          n = sbvFromInteger (kindOf i) (toInteger sx)
 
 -- | Generalization of 'rotateR', when the shift-amount is symbolic. Since Haskell's
 -- 'rotateR' only takes an 'Int' as the shift amount, it cannot be used when we have
 -- a symbolic amount to shift with. The shift amount must be an unsigned quantity.
-sbvRotateRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
+sbvRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a
 sbvRotateRight x i
-  | isSigned i = error "sbvRotateRight: shift amount should be unsigned"
-  | True       = select [x `rotateR` k | k <- [0 .. ghcBitSize x - 1]] z i
-    where z = sbvFromInteger (kindOf x) 0
+  | isSigned i             = error "sbvRotateRight: rotation amount should be unsigned"
+  | bit si <= toInteger sx = select [x `rotateR` k | k <- [0 .. bit si - 1]] z i
+                             -- ^ wrap-around not possible
+  | True                   = select [x `rotateR` k | k <- [0 .. sx - 1]] z (i `sRem` n)
+    where sx = ghcBitSize x
+          si = ghcBitSize i
+          z = sbvFromInteger (kindOf x) 0
+          n = sbvFromInteger (kindOf i) (toInteger sx)
 
 -- | Full adder. Returns the carry-out from the addition.
 --

tests/issues/issue160.cry

@@ -0,0 +1,17 @@
+thm1 : [16] -> Bit
+property thm1 x = (x <<< 16 == x) && (x >>> 16 == x)
+
+thm2 : [16] -> [16] -> Bit
+property thm2 x i = x >>> i == x >>> (i && 0x000f)
+
+thm3 : [15] -> [8] -> Bit
+property thm3 x i = x <<< i == x <<< (i % 15)
+
+thm4 : [15] -> [15] -> Bit
+property thm4 x i = x <<< i >>> i == x
+
+thm5 : [15] -> [3] -> Bit
+property thm5 x i = x <<< i >>> i == x
+
+thm6 : [8] -> [4] -> [4] -> Bit
+property thm6 x i j = x <<< i >>> j == x <<< (i - j)

tests/issues/issue160.icry

@@ -0,0 +1,2 @@
+:l issue160.cry
+:prove

tests/issues/issue160.icry.stdout

@@ -0,0 +1,9 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+property thm1 Q.E.D.
+property thm2 Q.E.D.
+property thm3 Q.E.D.
+property thm4 Q.E.D.
+property thm5 Q.E.D.
+property thm6 Q.E.D.