From 7c3f1ac67bca9d3d5a358db3536b338bcb73cb68 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 31 Mar 2021 00:16:34 -0700 Subject: [PATCH] Implement signed right shift uniformly --- src/Cryptol/Backend.hs | 13 +++++++++++ src/Cryptol/Backend/Concrete.hs | 7 ++++++ src/Cryptol/Backend/SBV.hs | 1 + src/Cryptol/Backend/What4.hs | 1 + src/Cryptol/Backend/WordValue.hs | 4 +++- src/Cryptol/Eval/Concrete.hs | 39 ++------------------------------ src/Cryptol/Eval/Generic.hs | 27 ++++++++++++++++++++++ src/Cryptol/Eval/SBV.hs | 25 ++------------------ src/Cryptol/Eval/What4.hs | 28 ++--------------------- 9 files changed, 58 insertions(+), 87 deletions(-) diff --git a/src/Cryptol/Backend.hs b/src/Cryptol/Backend.hs index a74a2714..35dc384e 100644 --- a/src/Cryptol/Backend.hs +++ b/src/Cryptol/Backend.hs @@ -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 -> diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs index 3a3ab42c..385da20c 100644 --- a/src/Cryptol/Backend/Concrete.hs +++ b/src/Cryptol/Backend/Concrete.hs @@ -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)) diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs index 8af04dee..a4e8d663 100644 --- a/src/Cryptol/Backend/SBV.hs +++ b/src/Cryptol/Backend/SBV.hs @@ -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 diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs index f22205af..f60ce18f 100644 --- a/src/Cryptol/Backend/What4.hs +++ b/src/Cryptol/Backend/What4.hs @@ -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 diff --git a/src/Cryptol/Backend/WordValue.hs b/src/Cryptol/Backend/WordValue.hs index a3749b5d..b36bce84 100644 --- a/src/Cryptol/Backend/WordValue.hs +++ b/src/Cryptol/Backend/WordValue.hs @@ -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 diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs index 4bf9c7de..f93cd304 100644 --- a/src/Cryptol/Eval/Concrete.hs +++ b/src/Cryptol/Eval/Concrete.hs @@ -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 --------------------------------------------------------- diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 94b04a5c..9ff16012 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -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 diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs index 2a2074d9..2bd00041 100644 --- a/src/Cryptol/Eval/SBV.hs +++ b/src/Cryptol/Eval/SBV.hs @@ -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 diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs index 1d531a47..5a3b7707 100644 --- a/src/Cryptol/Eval/What4.hs +++ b/src/Cryptol/Eval/What4.hs @@ -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 ->