GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 20:03:27 +03:00
Code Issues Projects Releases Wiki Activity

Share more code between interpreter and symbolic simulator

Browse Source 
Some interpreter/simulator operations are now overloaded using
a newly introduced 'BitWord' type class.
This commit is contained in:
Brian Huffman 2014-11-13 13:17:31 -08:00
parent 6368bcbe38
commit 88983488fc
3 changed files with 53 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
src/Cryptol/Eval/Value.hs
View File

@ -9,6 +9,7 @@
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
module Cryptol.Eval.Value where
@ -188,30 +189,38 @@ ppWord opts (BV width i)
-- Big-endian Words ------------------------------------------------------------
class BitWord b w where
-- | NOTE this assumes that the sequence of bits is big-endian and finite, so the
-- first element of the list will be the most significant bit.
packWord :: [b] -> w
-- | NOTE this produces a list of bits that represent a big-endian word, so the
-- most significant bit is the first element of the list.
unpackWord :: w -> [b]
mask :: Integer -- ^ Bit-width
-> Integer -- ^ Value
-> Integer -- ^ Masked result
mask w i | w >= Arch.maxBigIntWidth = wordTooWide w
| otherwise = i .&. ((1 `shiftL` fromInteger w) - 1)
-- NOTE this assumes that the sequence of bits is big-endian and finite, so the
-- first element of the list will be the most significant bit.
packWord :: [Bool] -> BV
packWord bits = BV (toInteger w) a
where
w = case length bits of
len | toInteger len >= Arch.maxBigIntWidth -> wordTooWide (toInteger len)
| otherwise -> len
a = foldl set 0 (zip [w - 1, w - 2 .. 0] bits)
set acc (n,b) | b = setBit acc n
| otherwise = acc
-- NOTE this produces a list of bits that represent a big-endian word, so the
-- most significant bit is the first element of the list.
unpackWord :: BV -> [Bool]
unpackWord (BV w a) = [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ]
where
w' = fromInteger w
instance BitWord Bool BV where
packWord bits = BV (toInteger w) a
where
w = case length bits of
len | toInteger len >= Arch.maxBigIntWidth -> wordTooWide (toInteger len)
| otherwise -> len
a = foldl set 0 (zip [w - 1, w - 2 .. 0] bits)
set acc (n,b) | b = setBit acc n
| otherwise = acc
unpackWord (BV w a) = [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ]
where
w' = fromInteger w
-- Value Constructors ----------------------------------------------------------
@ -272,7 +281,7 @@ fromVBit val = case val of
_ -> evalPanic "fromVBit" ["not a Bit"]
-- | Extract a sequence.
fromSeq :: Value -> [Value]
fromSeq :: BitWord b w => GenValue b w -> [GenValue b w]
fromSeq val = case val of
VSeq _ vs -> vs
VWord bv -> map VBit (unpackWord bv)
@ -284,12 +293,11 @@ fromStr = map (toEnum . fromInteger . fromWord) . fromSeq
-- | Extract a packed word.
-- Note that this does not clean-up any junk bits in the word.
fromVWord :: Value -> BV
fromVWord :: BitWord b w => GenValue b w -> w
fromVWord val = case val of
VWord bv -> bv -- this should always mask
VSeq isWord bs | isWord -> packWord (map fromVBit bs)
_ -> evalPanic "fromVWord"
["not a word", show $ ppValue defaultPPOpts val]
_ -> evalPanic "fromVWord" ["not a word"]
vWordLen :: Value -> Maybe Integer
vWordLen val = case val of

30
src/Cryptol/Symbolic/Prims.hs
View File

@ -97,7 +97,7 @@ evalECon econ =
VFun $ \xs ->
VFun $ \y ->
case xs of
VWord x -> VWord (SBV.sbvShiftLeft x (fromWord y))
VWord x -> VWord (SBV.sbvShiftLeft x (fromVWord y))
_ -> selectV shl y
where
shl :: Integer -> Value
@ -114,7 +114,7 @@ evalECon econ =
VFun $ \xs ->
VFun $ \y ->
case xs of
VWord x -> VWord (SBV.sbvShiftRight x (fromWord y))
VWord x -> VWord (SBV.sbvShiftRight x (fromVWord y))
_ -> selectV shr y
where
shr :: Integer -> Value
@ -131,7 +131,7 @@ evalECon econ =
VFun $ \xs ->
VFun $ \y ->
case xs of
VWord x -> VWord (SBV.sbvRotateLeft x (fromWord y))
VWord x -> VWord (SBV.sbvRotateLeft x (fromVWord y))
_ -> selectV rol y
where
rol :: Integer -> Value
@ -145,7 +145,7 @@ evalECon econ =
VFun $ \xs ->
VFun $ \y ->
case xs of
VWord x -> VWord (SBV.sbvRotateRight x (fromWord y))
VWord x -> VWord (SBV.sbvRotateRight x (fromVWord y))
_ -> selectV ror y
where
ror :: Integer -> Value
@ -233,13 +233,13 @@ evalECon econ =
ECInfFrom ->
tlam $ \(finTValue -> bits) ->
lam $ \(fromWord -> first) ->
lam $ \(fromVWord -> first) ->
toStream [ VWord (first + SBV.literal (bv (fromInteger bits) i)) | i <- [0 ..] ]
ECInfFromThen -> -- {a} (fin a) => [a] -> [a] -> [inf][a]
tlam $ \_ ->
lam $ \(fromWord -> first) ->
lam $ \(fromWord -> next) ->
lam $ \(fromVWord -> first) ->
lam $ \(fromVWord -> next) ->
toStream (map VWord (iterate (+ (next - first)) first))
-- {at,len} (fin len) => [len][8] -> at
@ -324,8 +324,8 @@ mapV f v =
catV :: Value -> Value -> Value
catV xs (VStream ys) = VStream (fromSeq xs ++ ys)
catV (VWord x) ys = VWord (cat x (fromWord ys))
catV xs (VWord y) = VWord (cat (fromWord xs) y)
catV (VWord x) ys = VWord (cat x (fromVWord ys))
catV xs (VWord y) = VWord (cat (fromVWord xs) y)
catV (VSeq b xs) (VSeq _ ys) = VSeq b (xs ++ ys)
catV _ _ = panic "Cryptol.Symbolic.Prims.catV" [ "non-concatenable value" ]
@ -395,7 +395,7 @@ arithBinary op = loop . toTypeVal
loop ty l r =
case ty of
TVBit -> evalPanic "arithBinop" ["Invalid arguments"]
TVSeq _ TVBit -> VWord (op (fromWord l) (fromWord r))
TVSeq _ TVBit -> VWord (op (fromVWord l) (fromVWord r))
TVSeq _ t -> VSeq False (zipWith (loop t) (fromSeq l) (fromSeq r))
TVStream t -> VStream (zipWith (loop t) (fromSeq l) (fromSeq r))
TVTuple ts -> VTuple (zipWith3 loop ts (fromVTuple l) (fromVTuple r))
@ -409,7 +409,7 @@ arithUnary op = loop . toTypeVal
loop ty v =
case ty of
TVBit -> evalPanic "arithUnary" ["Invalid arguments"]
TVSeq _ TVBit -> VWord (op (fromWord v))
TVSeq _ TVBit -> VWord (op (fromVWord v))
TVSeq _ t -> VSeq False (map (loop t) (fromSeq v))
TVStream t -> VStream (map (loop t) (fromSeq v))
TVTuple ts -> VTuple (zipWith loop ts (fromVTuple v))
@ -451,8 +451,8 @@ cmpValue fb fw = cmp
[ "Functions are not comparable" ]
(VPoly {} , VPoly {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "Polymorphic values are not comparable" ]
(VWord w1 , _ ) -> fw w1 (fromWord v2) k
(_ , VWord w2 ) -> fw (fromWord v1) w2 k
(VWord w1 , _ ) -> fw w1 (fromVWord v2) k
(_ , VWord w2 ) -> fw (fromVWord v1) w2 k
(_ , _ ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "type mismatch" ]
@ -543,7 +543,7 @@ logicBinary bop op = loop . toTypeVal
loop ty l r =
case ty of
TVBit -> VBit (bop (fromVBit l) (fromVBit r))
TVSeq _ TVBit -> VWord (op (fromWord l) (fromWord r))
TVSeq _ TVBit -> VWord (op (fromVWord l) (fromVWord r))
TVSeq _ t -> VSeq False (zipWith (loop t) (fromSeq l) (fromSeq r))
TVStream t -> VStream (zipWith (loop t) (fromSeq l) (fromSeq r))
TVTuple ts -> VTuple (zipWith3 loop ts (fromVTuple l) (fromVTuple r))
@ -556,7 +556,7 @@ logicUnary bop op = loop . toTypeVal
loop ty v =
case ty of
TVBit -> VBit (bop (fromVBit v))
TVSeq _ TVBit -> VWord (op (fromWord v))
TVSeq _ TVBit -> VWord (op (fromVWord v))
TVSeq _ t -> VSeq False (map (loop t) (fromSeq v))
TVStream t -> VStream (map (loop t) (fromSeq v))
TVTuple ts -> VTuple (zipWith loop ts (fromVTuple v))

30
src/Cryptol/Symbolic/Value.hs
View File

@ -8,6 +8,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Cryptol.Symbolic.Value
@ -15,7 +16,7 @@ module Cryptol.Symbolic.Value
, TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq
, GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
, fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
, fromSeq, fromWord
, fromSeq, fromVWord
, evalPanic
)
where
@ -23,8 +24,8 @@ module Cryptol.Symbolic.Value
import Data.Bits (bitSize)
import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq,
GenValue(..), lam, tlam, toStream, toFinSeq, toSeq,
fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord)
GenValue(..), BitWord(..), lam, tlam, toStream, toFinSeq, toSeq, fromSeq,
fromVBit, fromVWord, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord)
import Cryptol.Symbolic.BitVector
import Cryptol.Utils.Panic (panic)
@ -47,8 +48,8 @@ instance Mergeable Value where
(VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2
(VFun f1 , VFun f2 ) -> VFun $ symbolicMerge f c f1 f2
(VPoly f1 , VPoly f2 ) -> VPoly $ symbolicMerge f c f1 f2
(VWord w1 , _ ) -> VWord $ symbolicMerge f c w1 (fromWord v2)
(_ , VWord w2 ) -> VWord $ symbolicMerge f c (fromWord v1) w2
(VWord w1 , _ ) -> VWord $ symbolicMerge f c w1 (fromVWord v2)
(_ , VWord w2 ) -> VWord $ symbolicMerge f c (fromVWord v1) w2
(_ , _ ) -> panic "Cryptol.Symbolic.Value"
[ "symbolicMerge: incompatible values" ]
where
@ -61,22 +62,9 @@ instance Mergeable Value where
-- Big-endian Words ------------------------------------------------------------
unpackWord :: SWord -> [SBool]
unpackWord s = [ sbvTestBit s i | i <- reverse [0 .. bitSize s - 1] ]
-- Constructors and Accessors --------------------------------------------------
fromWord :: Value -> SWord
fromWord (VWord s) = s
fromWord v = Data.SBV.fromBitsBE (map fromVBit (fromSeq v))
-- | Extract a sequence.
fromSeq :: Value -> [Value]
fromSeq v = case v of
VSeq _ vs -> vs
VWord s -> map VBit (unpackWord s)
VStream vs -> vs
_ -> evalPanic "fromSeq" ["not a sequence"]
instance BitWord SBool SWord where
packWord bs = Data.SBV.fromBitsBE bs
unpackWord w = [ sbvTestBit w i | i <- reverse [0 .. bitSize w - 1] ]
-- Errors ----------------------------------------------------------------------