From 88983488fcdf9916eb18342b861b543ca2f8b1e5 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 13 Nov 2014 13:17:31 -0800 Subject: [PATCH] Share more code between interpreter and symbolic simulator Some interpreter/simulator operations are now overloaded using a newly introduced 'BitWord' type class. --- src/Cryptol/Eval/Value.hs | 50 ++++++++++++++++++++--------------- src/Cryptol/Symbolic/Prims.hs | 30 ++++++++++----------- src/Cryptol/Symbolic/Value.hs | 30 +++++++-------------- 3 files changed, 53 insertions(+), 57 deletions(-) diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs index b4727903..28fb6422 100644 --- a/src/Cryptol/Eval/Value.hs +++ b/src/Cryptol/Eval/Value.hs @@ -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 diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs index 7c3cd29f..3747f212 100644 --- a/src/Cryptol/Symbolic/Prims.hs +++ b/src/Cryptol/Symbolic/Prims.hs @@ -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)) diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs index e13a7a42..6278169a 100644 --- a/src/Cryptol/Symbolic/Value.hs +++ b/src/Cryptol/Symbolic/Value.hs @@ -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 ----------------------------------------------------------------------