mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 13:01:31 +03:00
Use more efficent algorithms based on barrel-shifters for implementing
shifts and rotates in the symbolic backend. Fixes #376
This commit is contained in:
Robert Dockins
parent
14af3690c6
commit
a048690e3a
@ -29,7 +29,8 @@ import Cryptol.Eval.Monad (Eval(..), ready, invalidIndex)
|
||||
import Cryptol.Eval.Type (finNat', TValue(..))
|
||||
import Cryptol.Eval.Value (BitWord(..), EvalPrims(..), enumerateSeqMap, SeqMap(..),
|
||||
reverseSeqMap, wlam, nlam, WordValue(..),
|
||||
asWordVal, asBitsVal, fromWordVal, updateSeqMap, lookupSeqMap )
|
||||
asWordVal, asBitsVal, fromWordVal,
|
||||
updateSeqMap, lookupSeqMap, memoMap )
|
||||
import Cryptol.Prims.Eval (binary, unary, arithUnary,
|
||||
arithBinary, Binary, BinArith,
|
||||
logicBinary, logicUnary, zeroV,
|
||||
@ -236,6 +237,17 @@ iteWord :: SBool
|
||||
-> Eval (WordValue SBool SWord)
|
||||
iteWord c x y = mergeWord True c <$> x <*> y
|
||||
|
||||
|
||||
-- | Barrel-shifter algorithm. Takes a list of bits in big-endian order.
|
||||
shifter :: Monad m => (SBool -> a -> a -> m a) -> (a -> Integer -> m a) -> a -> [SBool] -> m a
|
||||
shifter mux op = go
|
||||
where
|
||||
go x [] = return x
|
||||
go x (b : bs) = do
|
||||
x' <- op x (2 ^ length bs)
|
||||
y <- mux b x' x
|
||||
go y bs
|
||||
|
||||
logicShift :: String
|
||||
-> (SWord -> SWord -> SWord)
|
||||
-> (Nat' -> Integer -> Integer -> Maybe Integer)
|
||||
@ -249,26 +261,33 @@ logicShift nm wop reindex =
|
||||
idx <- fromWordVal "logicShift" =<< y
|
||||
|
||||
xs >>= \case
|
||||
VWord w x -> return $ VWord w $ do
|
||||
x >>= \case
|
||||
WordVal x' -> WordVal . wop x' <$> asWordVal idx
|
||||
BitsVal bs -> selectV iteWord idx $ \shft -> return $
|
||||
BitsVal $ Seq.fromFunction (Seq.length bs) $ \i ->
|
||||
VWord w x ->
|
||||
return $ VWord w $ do
|
||||
x >>= \case
|
||||
WordVal x' -> WordVal . wop x' <$> asWordVal idx
|
||||
wv ->
|
||||
do idx_bits <- sequence $ Fold.toList $ asBitsVal idx
|
||||
let op bs shft = return $ Seq.fromFunction (Seq.length bs) $ \i ->
|
||||
case reindex (Nat w) (toInteger i) shft of
|
||||
Nothing -> return $ bitLit False
|
||||
Just i' -> Seq.index bs (fromInteger i')
|
||||
BitsVal <$> shifter (\c x y -> return $ mergeBits True c x y) op (asBitsVal wv) idx_bits
|
||||
|
||||
VSeq w vs -> selectV iteValue idx $ \shft -> return $
|
||||
VSeq w $ IndexSeqMap $ \i ->
|
||||
case reindex (Nat w) i shft of
|
||||
Nothing -> return $ zeroV a
|
||||
Just i' -> lookupSeqMap vs i'
|
||||
VSeq w vs0 ->
|
||||
do idx_bits <- sequence $ Fold.toList $ asBitsVal idx
|
||||
let op vs shft = memoMap $ IndexSeqMap $ \i ->
|
||||
case reindex (Nat w) i shft of
|
||||
Nothing -> return $ zeroV a
|
||||
Just i' -> lookupSeqMap vs i'
|
||||
VSeq w <$> shifter (\c x y -> return $ mergeSeqMap True c x y) op vs0 idx_bits
|
||||
|
||||
VStream vs -> selectV iteValue idx $ \shft -> return $
|
||||
VStream $ IndexSeqMap $ \i ->
|
||||
case reindex Inf i shft of
|
||||
Nothing -> return $ zeroV a
|
||||
Just i' -> lookupSeqMap vs i'
|
||||
VStream vs0 ->
|
||||
do idx_bits <- sequence $ Fold.toList $ asBitsVal idx
|
||||
let op vs shft = memoMap $ IndexSeqMap $ \i ->
|
||||
case reindex Inf i shft of
|
||||
Nothing -> return $ zeroV a
|
||||
Just i' -> lookupSeqMap vs i'
|
||||
VStream <$> shifter (\c x y -> return $ mergeSeqMap True c x y) op vs0 idx_bits
|
||||
|
||||
_ -> evalPanic "expected sequence value in shift operation" [nm]
|
||||
|
||||
|
||||
@ -24,7 +24,7 @@ module Cryptol.Symbolic.Value
|
||||
, fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
|
||||
, fromSeq, fromVWord
|
||||
, evalPanic
|
||||
, iteSValue, mergeValue, mergeWord, mergeBit
|
||||
, iteSValue, mergeValue, mergeWord, mergeBit, mergeBits, mergeSeqMap
|
||||
)
|
||||
where
|
||||
|
||||
@ -35,6 +35,7 @@ import Data.SBV.Dynamic
|
||||
|
||||
--import Cryptol.Eval.Monad
|
||||
import Cryptol.Eval.Type (TValue(..), isTBit, tvSeq)
|
||||
import Cryptol.Eval.Monad (Eval)
|
||||
import Cryptol.Eval.Value ( GenValue(..), BitWord(..), lam, tlam, toStream,
|
||||
toFinSeq, toSeq, WordValue(..), asBitsVal,
|
||||
fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
|
||||
@ -94,8 +95,14 @@ mergeWord :: Bool
|
||||
-> WordValue SBool SWord
|
||||
mergeWord f c (WordVal w1) (WordVal w2) =
|
||||
WordVal $ svSymbolicMerge (kindOf w1) f c w1 w2
|
||||
mergeWord f c w1 w2 =
|
||||
BitsVal $ Seq.zipWith mergeBit' (asBitsVal w1) (asBitsVal w2)
|
||||
mergeWord f c w1 w2 = BitsVal $ mergeBits f c (asBitsVal w1) (asBitsVal w2)
|
||||
|
||||
mergeBits :: Bool
|
||||
-> SBool
|
||||
-> Seq.Seq (Eval SBool)
|
||||
-> Seq.Seq (Eval SBool)
|
||||
-> Seq.Seq (Eval SBool)
|
||||
mergeBits f c bs1 bs2 = Seq.zipWith mergeBit' bs1 bs2
|
||||
where mergeBit' b1 b2 = mergeBit f c <$> b1 <*> b2
|
||||
|
||||
mergeValue :: Bool -> SBool -> Value -> Value -> Value
|
||||
@ -105,8 +112,8 @@ mergeValue f c v1 v2 =
|
||||
(VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (\x y -> mergeValue f c <$> x <*> y) vs1 vs2
|
||||
(VBit b1 , VBit b2 ) -> VBit $ mergeBit f c b1 b2
|
||||
(VWord n1 w1, VWord n2 w2 ) | n1 == n2 -> VWord n1 (mergeWord f c <$> w1 <*> w2)
|
||||
(VSeq n1 vs1, VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 $ mergeSeqMap vs1 vs2
|
||||
(VStream vs1, VStream vs2) -> VStream $ mergeSeqMap vs1 vs2
|
||||
(VSeq n1 vs1, VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 $ mergeSeqMap f c vs1 vs2
|
||||
(VStream vs1, VStream vs2) -> VStream $ mergeSeqMap f c vs1 vs2
|
||||
(VFun f1 , VFun f2 ) -> VFun $ \x -> mergeValue f c <$> (f1 x) <*> (f2 x)
|
||||
(VPoly f1 , VPoly f2 ) -> VPoly $ \x -> mergeValue f c <$> (f1 x) <*> (f2 x)
|
||||
(_ , _ ) -> panic "Cryptol.Symbolic.Value"
|
||||
@ -116,8 +123,11 @@ mergeValue f c v1 v2 =
|
||||
| n1 == n2 = (n1, mergeValue f c <$> x1 <*> x2)
|
||||
| otherwise = panic "Cryptol.Symbolic.Value"
|
||||
[ "mergeValue.mergeField: incompatible values" ]
|
||||
mergeSeqMap x y =
|
||||
IndexSeqMap $ \i -> mergeValue f c <$> lookupSeqMap x i <*> lookupSeqMap y i
|
||||
|
||||
|
||||
mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord -> SeqMap SBool SWord -> SeqMap SBool SWord
|
||||
mergeSeqMap f c x y =
|
||||
IndexSeqMap $ \i -> mergeValue f c <$> lookupSeqMap x i <*> lookupSeqMap y i
|
||||
|
||||
-- Symbolic Big-endian Words -------------------------------------------------------
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user