Fix bugs in the signed right shift operation.

However, see the following SBV issue that currently affects
Cryptol behavior when computing signed right shifts with
symbolic index amounts:
LeventErkok/sbv#323

src/Cryptol/Prims/Eval.hs

@@ -91,7 +91,7 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
   , ("$%"         , {-# SCC "Prelude::($%)" #-}
                     liftSigned bvSrem)
   , ("$>>"        , {-# SCC "Prelude::($>>)" #-}
-                    liftWord bvSshr)
+                    sshrV)
   , ("&&"         , {-# SCC "Prelude::(&&)" #-}
                     binary (logicBinary (.&.) (binBV (.&.))))
   , ("||"         , {-# SCC "Prelude::(||)" #-}
@@ -567,10 +567,17 @@ bvSrem :: Integer -> Integer -> Integer -> Eval Value
 bvSrem  _ _ 0 = divideByZero
 bvSrem sz x y = return . VWord sz . ready . WordVal $ mkBv sz (x `rem` y)
 
-bvSshr :: BV -> BV -> Eval Value
-bvSshr (BV i x) y = return . VWord i . ready $ WordVal z
-   where sx = if testBit x (fromIntegral (i-1)) then negate x else x
-         z  = mkBv i (sx `shiftR` (fromInteger (bvVal y)))
+sshrV :: Value
+sshrV =
+  nlam $ \_n ->
+  nlam $ \_k ->
+  wlam $ \(BV i x) -> return $
+  wlam $ \y ->
+   let signx = testBit x (fromIntegral (i-1))
+       amt   = fromInteger (bvVal y)
+       negv  = (((-1) `shiftL` amt) .|. x) `shiftR` amt
+       posv  = x `shiftR` amt
+    in return . VWord i . ready . WordVal . mkBv i $! if signx then negv else posv
 
 -- | Signed carry bit.
 scarryV :: Value

src/Cryptol/Symbolic/Prims.hs

@@ -95,7 +95,7 @@ primTable  = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
   , ("$<"          , liftWord swordSlt)
   , ("$/"          , liftWord swordSdiv)
   , ("$%"          , liftWord swordSrem)
-  , ("$>>"         , liftWord swordSshr)
+  , ("$>>"         , sshrV)
   , ("&&"          , binary (logicBinary SBV.svAnd SBV.svAnd))
   , ("||"          , binary (logicBinary SBV.svOr SBV.svOr))
   , ("^"           , binary (logicBinary SBV.svXOr SBV.svXOr))
@@ -532,10 +532,6 @@ swordSlt :: SWord -> SWord -> Eval Value
 swordSlt x y = return $ VBit lt
   where lt = SBV.svLessThan (SBV.svSign x) (SBV.svSign y)
 
-swordSshr :: SWord -> SWord -> Eval Value
-swordSshr x y = return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
-  where z = SBV.svShiftRight (SBV.svSign x) y
-
 swordSdiv :: SWord -> SWord -> Eval Value
 swordSdiv x y = return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
   where z = SBV.svQuot (SBV.svSign x) (SBV.svSign y)
@@ -544,6 +540,20 @@ swordSrem :: SWord -> SWord -> Eval Value
 swordSrem x y = return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
   where z = SBV.svRem (SBV.svSign x) (SBV.svSign y)
 
+sshrV :: Value
+sshrV =
+  nlam $ \_n ->
+  nlam $ \_k ->
+  wlam $ \x -> return $
+  wlam $ \y ->
+   case SBV.svAsInteger y of
+     Just i ->
+       let z = SBV.svUnsign (SBV.svShr (SBV.svSign x) (fromInteger i))
+        in return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
+     Nothing ->
+       let z = SBV.svUnsign (SBV.svShiftRight (SBV.svSign x) y)
+        in return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
+
 carry :: SWord -> SWord -> Eval Value
 carry x y = return $ VBit c
  where