GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-01 04:14:24 +03:00
Code Issues Projects Releases Wiki Activity

Implement signed right shift uniformly

Browse Source
This commit is contained in:
Rob Dockins 2021-03-31 00:16:34 -07:00
parent 9d4183975e
commit 7c3f1ac67b
9 changed files with 58 additions and 87 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/Cryptol/Backend.hs
View File

@ -538,6 +538,17 @@ class MonadIO (SEval sym) => Backend sym where
SWord sym {- ^ amount to shift by -} ->
SEval sym (SWord sym)
-- | Shift a bitvector right by the specified amount. This is an
-- arithmetic shift, which shifts in copies of the high bit on the
-- left. The shift amount is considered as an unsigned
-- value. Shifting by more than the word length results in filling
-- the bitvector with the high bit.
wordSignedShiftRight ::
sym ->
SWord sym {- ^ value to shift -} ->
SWord sym {- ^ amount to shift by -} ->
SEval sym (SWord sym)
wordRotateLeft ::
sym ->
SWord sym {- ^ value to rotate -} ->
@ -550,6 +561,8 @@ class MonadIO (SEval sym) => Backend sym where
SWord sym {- ^ amount to rotate by -} ->
SEval sym (SWord sym)
-- | 2's complement negation of bitvectors
wordNegate ::
sym ->

7
src/Cryptol/Backend/Concrete.hs
View File

@ -295,6 +295,13 @@ instance Backend Concrete where
| by > toInteger (maxBound :: Int) = panic "lshr" ["Shift amount too large", show by]
| otherwise = pure $! BV w (shiftR ival (fromInteger by))
wordSignedShiftRight _sym (BV w ival) (BV _ by) =
let by' = min w by in
if by' > toInteger (maxBound :: Int) then
panic "wordSignedShiftRight" ["Shift amount too large", show by]
else
pure $! mkBv w (shiftR (signedValue w ival) (fromInteger by'))
wordRotateRight _sym (BV 0 i) _ = pure (BV 0 i)
wordRotateRight _sym (BV w i) (BV _ by) =
pure . mkBv w $! (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))

1
src/Cryptol/Backend/SBV.hs
View File

@ -266,6 +266,7 @@ instance Backend SBV where
wordShiftRight _ a b = pure $! lshr a b
wordRotateLeft _ a b = pure $! SBV.svRotateLeft a b
wordRotateRight _ a b = pure $! SBV.svRotateRight a b
wordSignedShiftRight _ a b = pure $! ashr a b
wordDiv sym a b =
do let z = literalSWord (intSizeOf b) 0

1
src/Cryptol/Backend/What4.hs
View File

@ -346,6 +346,7 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
wordShiftRight sym x y = w4bvLshr (w4 sym) x y
wordRotateLeft sym x y = w4bvRol (w4 sym) x y
wordRotateRight sym x y = w4bvRor (w4 sym) x y
wordSignedShiftRight sym x y = w4bvAshr (w4 sym) x y
wordDiv sym x y =
do assertBVDivisor sym y

4
src/Cryptol/Backend/WordValue.hs
View File

@ -604,4 +604,6 @@ mergeWord' :: Backend sym =>
SEval sym (WordValue sym) ->
SEval sym (WordValue sym) ->
SEval sym (WordValue sym)
mergeWord' sym = mergeEval sym (mergeWord sym)
mergeWord' sym c x y
| Just b <- bitAsLit sym c = if b then x else y
| otherwise = mergeEval sym (mergeWord sym) c x y

39
src/Cryptol/Eval/Concrete.hs
View File

@ -26,7 +26,6 @@ module Cryptol.Eval.Concrete
) where
import Control.Monad (guard, zipWithM, foldM, mzero)
import Data.Bits (Bits(..))
import Data.Ratio(numerator,denominator)
import Data.Word(Word32, Word64)
import MonadLib( ChoiceT, findOne, lift )
@ -161,11 +160,8 @@ primTable getEOpts = let sym = Concrete in
Map.fromList $ map (\(n, v) -> (prelPrim n, v))
[ (">>$" , {-# SCC "Prelude::(>>$)" #-}
sshrV)
-- Indexing and updates
, ("@" , {-# SCC "Prelude::(@)" #-}
[ -- Indexing and updates
("@" , {-# SCC "Prelude::(@)" #-}
indexPrim sym IndexForward indexFront_int indexFront_segs)
, ("!" , {-# SCC "Prelude::(!)" #-}
indexPrim sym IndexBackward indexFront_int indexFront_segs)
@ -441,37 +437,6 @@ toSHA512Block blk =
(toWord 14) <*>
(toWord 15)
--------------------------------------------------------------------------------
sshrV :: Prim Concrete
sshrV =
PNumPoly \_n ->
PTyPoly \ix ->
PWordFun \(BV w x) ->
PFun \y ->
PPrim
do idx <- (asIndex Concrete ">>$" ix <$> y) >>= \case
Left idx -> pure idx
Right wv -> bvVal <$> asWordVal Concrete wv
if idx < 0 then
VWord w . wordVal <$> concreteShl (BV w x) (BV w (negate idx))
else
return . VWord w . wordVal $! mkBv w $ signedShiftRW w x idx
-- signed right shift for words
signedShiftRW :: Integer -> Integer -> Integer -> Integer
signedShiftRW w ival by =
let by' = min w by in
if by' > toInteger (maxBound :: Int) then
panic "signedShiftRW" ["Shift amount too large", show by]
else
shiftR (signedValue w ival) (fromInteger by')
concreteShl :: BV -> BV -> Eval BV
concreteShl (BV w ival) (BV _ by)
| by >= w = pure $! BV w 0
| by > toInteger (maxBound :: Int) = panic "shl" ["Shift amount too large", show by]
| otherwise = pure $! mkBv w (shiftL ival (fromInteger by))
-- Sequence Primitives ---------------------------------------------------------

27
src/Cryptol/Eval/Generic.hs
View File

@ -1645,6 +1645,30 @@ rotateShrink sym (Nat w) _ x =
do w' <- integerLit sym w
intMod sym x w'
{-# INLINE sshrV #-}
sshrV :: Backend sym => sym -> Prim sym
sshrV sym =
PFinPoly \n ->
PTyPoly \ix ->
PWordFun \x ->
PStrict \y ->
PPrim $
case asIndex sym ">>$" ix y of
Left i ->
do pneg <- intLessThan sym i =<< integerLit sym 0
VWord n <$> mergeWord' sym
pneg
(do i' <- shiftShrink sym (Nat n) ix =<< intNegate sym i
amt <- wordFromInt sym n i'
wordVal <$> wordShiftLeft sym x amt)
(do i' <- shiftShrink sym (Nat n) ix i
amt <- wordFromInt sym n i'
wordVal <$> wordSignedShiftRight sym x amt)
Right wv ->
do amt <- asWordVal sym wv
VWord n . wordVal <$> wordSignedShiftRight sym x amt
-- Miscellaneous ---------------------------------------------------------------
{-# SPECIALIZE errorV ::
@ -2091,6 +2115,9 @@ genericPrimTable sym getEOpts =
(wordRotateRight sym) (wordRotateLeft sym)
rotateRightReindex rotateLeftReindex)
, (">>$" , {-# SCC "Prelude::(>>$)" #-}
sshrV sym)
-- Misc
-- {at,len} (fin len) => [len][8] -> at

25
src/Cryptol/Eval/SBV.hs
View File

@ -54,10 +54,8 @@ primTable sym getEOpts =
Map.union (genericPrimTable sym getEOpts) $
Map.fromList $ map (\(n, v) -> (prelPrim (T.pack n), v))
[ (">>$" , sshrV sym)
-- Indexing and updates
, ("@" , indexPrim sym IndexForward (indexFront sym) (indexFront_segs sym))
[ -- Indexing and updates
("@" , indexPrim sym IndexForward (indexFront sym) (indexFront_segs sym))
, ("!" , indexPrim sym IndexBackward (indexFront sym) (indexFront_segs sym))
, ("update" , updatePrim sym (updateFrontSym_word sym) (updateFrontSym sym))
@ -256,22 +254,3 @@ updateBackSym_word sym (Nat n) eltTy w lridx val =
let bw' = SBV.svAnd bw (SBV.svNot msk)
return $! SBV.svXOr bw' (SBV.svAnd q msk)
sshrV :: SBV -> Prim SBV
sshrV sym =
PNumPoly \n ->
PTyPoly \ix ->
PWordFun \x ->
PStrict \y ->
PPrim $
case asIndex sym ">>$" ix y of
Left idx ->
do let w = toInteger (SBV.intSizeOf x)
let pneg = svLessThan idx (svInteger KUnbounded 0)
zneg <- shl x . svFromInteger w <$> shiftShrink sym n ix (SBV.svUNeg idx)
zpos <- ashr x . svFromInteger w <$> shiftShrink sym n ix idx
let z = svSymbolicMerge (kindOf x) True pneg zneg zpos
return . VWord w . wordVal $ z
Right wv ->
do z <- ashr x <$> asWordVal sym wv
return . VWord (toInteger (SBV.intSizeOf x)) . wordVal $ z

28
src/Cryptol/Eval/What4.hs
View File

@ -70,10 +70,8 @@ primTable sym getEOpts =
Map.fromList $ map (\(n, v) -> (prelPrim n, v))
[ (">>$" , sshrV sym)
-- Indexing and updates
, ("@" , indexPrim sym IndexForward (indexFront_int sym) (indexFront_segs sym))
[ -- Indexing and updates
("@" , indexPrim sym IndexForward (indexFront_int sym) (indexFront_segs sym))
, ("!" , indexPrim sym IndexBackward (indexFront_int sym) (indexFront_segs sym))
, ("update" , updatePrim sym (updateFrontSym_word sym) (updateFrontSym sym))
@ -498,28 +496,6 @@ applyAESStateFunc sym funNm x =
argCtx = W4.knownRepr
sshrV :: W4.IsSymExprBuilder sym => What4 sym -> Prim (What4 sym)
sshrV sym =
PFinPoly \n ->
PTyPoly \ix ->
PWordFun \x ->
PStrict \y ->
PPrim $
case asIndex sym ">>$" ix y of
Left i ->
do pneg <- intLessThan sym i =<< integerLit sym 0
zneg <- do i' <- shiftShrink sym (Nat n) ix =<< intNegate sym i
amt <- wordFromInt sym n i'
w4bvShl (w4 sym) x amt
zpos <- do i' <- shiftShrink sym (Nat n) ix i
amt <- wordFromInt sym n i'
w4bvAshr (w4 sym) x amt
VWord (SW.bvWidth x) . wordVal <$> iteWord sym pneg zneg zpos
Right wv ->
do amt <- asWordVal sym wv
VWord (SW.bvWidth x) . wordVal <$> w4bvAshr (w4 sym) x amt
indexFront_int ::
W4.IsSymExprBuilder sym =>
What4 sym ->