Fix shift/rotate by amounts greater than 2^63 in evaluator

Also added regression tests. This should fix issue #306.

src/Cryptol/Prims/Eval.hs

@@ -26,7 +26,8 @@ import Cryptol.Utils.Panic (panic)
 import Cryptol.ModuleSystem.Name (asPrim)
 import Cryptol.Utils.Ident (Ident,mkIdent)
 
-import Data.List (sortBy,transpose,genericTake,genericReplicate,genericSplitAt,genericIndex)
+import Data.List (sortBy, transpose, genericTake, genericDrop,
+                  genericReplicate, genericSplitAt, genericIndex)
 import Data.Ord (comparing)
 import Data.Bits (Bits(..))
 
@@ -546,10 +547,10 @@ logicUnary op = loop
     | otherwise = evalPanic "logicUnary" ["invalid logic type"]
 
 
-logicShift :: (Integer -> Integer -> Int -> Integer)
+logicShift :: (Integer -> Integer -> Integer -> Integer)
               -- ^ The function may assume its arguments are masked.
               -- It is responsible for masking its result if needed.
-           -> (TValue -> TValue -> [Value] -> Int -> [Value])
+           -> (TValue -> TValue -> [Value] -> Integer -> [Value])
            -> Value
 logicShift opW opS
   = tlam $ \ a ->
@@ -560,62 +561,61 @@ logicShift opW opS
         if isTBit c
           then -- words
             let BV w i  = fromVWord l
-            in VWord (BV w (opW w i (fromInteger (fromWord r))))
+            in VWord (BV w (opW w i (fromWord r)))
 
-          else toSeq a c (opS a c (fromSeq l) (fromInteger (fromWord r)))
+          else toSeq a c (opS a c (fromSeq l) (fromWord r))
 
 -- Left shift for words.
-shiftLW :: Integer -> Integer -> Int -> Integer
+shiftLW :: Integer -> Integer -> Integer -> Integer
 shiftLW w ival by
-  | toInteger by >= w = 0
-  | otherwise         = mask w (shiftL ival by)
+  | by >= w   = 0
+  | otherwise = mask w (shiftL ival (fromInteger by))
 
-shiftLS :: TValue -> TValue -> [Value] -> Int -> [Value]
+shiftLS :: TValue -> TValue -> [Value] -> Integer -> [Value]
 shiftLS w ety vs by =
   case numTValue w of
     Nat len
-      | toInteger by < len -> genericTake len (drop by vs ++ repeat (zeroV ety))
-      | otherwise          -> genericReplicate len (zeroV ety)
-    Inf                    -> drop by vs
+      | by < len  -> genericTake len (genericDrop by vs ++ repeat (zeroV ety))
+      | otherwise -> genericReplicate len (zeroV ety)
+    Inf           -> genericDrop by vs
 
-shiftRW :: Integer -> Integer -> Int -> Integer
+shiftRW :: Integer -> Integer -> Integer -> Integer
 shiftRW w i by
-  | toInteger by >= w = 0
-  | otherwise         = shiftR i by
+  | by >= w   = 0
+  | otherwise = shiftR i (fromInteger by)
 
-shiftRS :: TValue -> TValue -> [Value] -> Int -> [Value]
+shiftRS :: TValue -> TValue -> [Value] -> Integer -> [Value]
 shiftRS w ety vs by =
   case numTValue w of
     Nat len
-      | toInteger by < len -> genericTake len (replicate by (zeroV ety) ++ vs)
-      | otherwise          -> genericReplicate len (zeroV ety)
-    Inf                    -> replicate by (zeroV ety) ++ vs
+      | by < len  -> genericTake len (genericReplicate by (zeroV ety) ++ vs)
+      | otherwise -> genericReplicate len (zeroV ety)
+    Inf           -> genericReplicate by (zeroV ety) ++ vs
 
 -- XXX integer doesn't implement rotateL, as there's no bit bound
-rotateLW :: Integer -> Integer -> Int -> Integer
+rotateLW :: Integer -> Integer -> Integer -> Integer
 rotateLW 0 i _  = i
 rotateLW w i by = mask w $ (i `shiftL` b) .|. (i `shiftR` (fromInteger w - b))
-  where b = by `mod` fromInteger w
+  where b = fromInteger (by `mod` w)
 
-
-rotateLS :: TValue -> TValue -> [Value] -> Int -> [Value]
+rotateLS :: TValue -> TValue -> [Value] -> Integer -> [Value]
 rotateLS w _ vs at =
   case numTValue w of
-    Nat len -> let at'     = toInteger at `mod` len
+    Nat len -> let at'     = at `mod` len
                    (ls,rs) = genericSplitAt at' vs
                 in rs ++ ls
     _ -> panic "Cryptol.Eval.Prim.rotateLS" [ "unexpected infinite sequence" ]
 
 -- XXX integer doesn't implement rotateR, as there's no bit bound
-rotateRW :: Integer -> Integer -> Int -> Integer
+rotateRW :: Integer -> Integer -> Integer -> Integer
 rotateRW 0 i _  = i
 rotateRW w i by = mask w $ (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))
-  where b = by `mod` fromInteger w
+  where b = fromInteger (by `mod` w)
 
-rotateRS :: TValue -> TValue -> [Value] -> Int -> [Value]
+rotateRS :: TValue -> TValue -> [Value] -> Integer -> [Value]
 rotateRS w _ vs at =
   case numTValue w of
-    Nat len -> let at'     = toInteger at `mod` len
+    Nat len -> let at'     = at `mod` len
                    (ls,rs) = genericSplitAt (len - at') vs
                 in rs ++ ls
     _ -> panic "Cryptol.Eval.Prim.rotateRS" [ "unexpected infinite sequence" ]

tests/issues/issue306.icry

@@ -0,0 +1,6 @@
+:exhaust \(x:[6]) -> x <<< (0x10000000000000000 : [68]) == x <<< 4
+:exhaust \(x:[6]) -> x >>> (0x10000000000000000 : [68]) == x >>> 4
+:exhaust \(x:[8]) -> x << (0x10000000000000000 : [68]) == 0
+:exhaust \(x:[8]) -> x >> (0x10000000000000000 : [68]) == 0
+:exhaust \(x:[8]) -> x << (0x8000000000000000 : [64]) == 0
+:exhaust \(x:[8]) -> x >> (0x8000000000000000 : [64]) == 0

tests/issues/issue306.icry.stdout

@@ -0,0 +1,19 @@
+Loading module Cryptol
+Using exhaustive testing.
+testing...passed 64 tests.
+Q.E.D.
+Using exhaustive testing.
+testing...passed 64 tests.
+Q.E.D.
+Using exhaustive testing.
+testing...passed 256 tests.
+Q.E.D.
+Using exhaustive testing.
+testing...passed 256 tests.
+Q.E.D.
+Using exhaustive testing.
+testing...passed 256 tests.
+Q.E.D.
+Using exhaustive testing.
+testing...passed 256 tests.
+Q.E.D.