Fix bugs in the signed right shift operation.

Fixes #664.
GaloisInc · Nov 27, 2019 · 56f2638 · 56f2638
1 parent c859570
commit 56f2638
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs
@@ -678,9 +678,8 @@ sshrV =
   wlam $ \y ->
    let signx = testBit x (fromInteger (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
+       x'    = if signx then x - bit (fromInteger i) else x
+    in return . VWord i . ready . WordVal . mkBv i $! x' `shiftR` amt
 
 -- | Signed carry bit.
 scarryV :: Value