From bc99e7d7915444e4a3b77c37f7606a692388c3ca Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 17 Mar 2020 15:17:25 -0700 Subject: [PATCH] Take `bitLit` out of the `SEval` monad. The backends all support a non-monadic version of bit literals, and it's somewhat more convenient. --- src/Cryptol/Eval/Backend.hs | 2 +- src/Cryptol/Eval/Concrete.hs | 4 ++-- src/Cryptol/Eval/Concrete/Value.hs | 2 +- src/Cryptol/Eval/Generic.hs | 14 +++++++------- src/Cryptol/Eval/SBV.hs | 8 ++++---- src/Cryptol/Testing/Random.hs | 2 +- 6 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/Cryptol/Eval/Backend.hs b/src/Cryptol/Eval/Backend.hs index cfd20437..4a46d319 100644 --- a/src/Cryptol/Eval/Backend.hs +++ b/src/Cryptol/Eval/Backend.hs @@ -76,7 +76,7 @@ class MonadIO (SEval sym) => Backend sym where wordLen :: sym -> SWord sym -> Integer -- | Construct a literal bit value from a boolean. - bitLit :: sym -> Bool -> SEval sym (SBit sym) + bitLit :: sym -> Bool -> SBit sym -- | Determine if this symbolic bit is a boolean literal bitAsLit :: sym -> SBit sym -> Maybe Bool diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs index 0702ce04..ae89d9b7 100644 --- a/src/Cryptol/Eval/Concrete.hs +++ b/src/Cryptol/Eval/Concrete.hs @@ -108,8 +108,8 @@ primTable :: Map.Map Ident Value primTable = let sym = Concrete in Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v)) [ -- Literals - ("True" , VBit True) - , ("False" , VBit False) + ("True" , VBit (bitLit sym True)) + , ("False" , VBit (bitLit sym False)) , ("number" , {-# SCC "Prelude::number" #-} ecNumberV sym) diff --git a/src/Cryptol/Eval/Concrete/Value.hs b/src/Cryptol/Eval/Concrete/Value.hs index af333b65..fa17b8f9 100644 --- a/src/Cryptol/Eval/Concrete/Value.hs +++ b/src/Cryptol/Eval/Concrete/Value.hs @@ -163,7 +163,7 @@ instance Backend Concrete where ppInteger _ _opts i = integer i - bitLit _ b = pure b + bitLit _ b = b bitAsLit _ b = Just b bitEq _ x y = pure $! x == y diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 90c1f666..7007cf06 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -413,7 +413,7 @@ bitGreaterThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit bitGreaterThan sym x y = bitLessThan sym y x valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym) -valEq sym ty v1 v2 = cmpValue sym fb fw fi fz ty v1 v2 (bitLit sym True) +valEq sym ty v1 v2 = cmpValue sym fb fw fi fz ty v1 v2 (pure $ bitLit sym True) where fb x y k = eqCombine sym (bitEq sym x y) k fw x y k = eqCombine sym (wordEq sym x y) k @@ -421,8 +421,8 @@ valEq sym ty v1 v2 = cmpValue sym fb fw fi fz ty v1 v2 (bitLit sym True) fz m x y k = eqCombine sym (intModEq sym m x y) k valLt :: Backend sym => - sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym) -> SEval sym (SBit sym) -valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 final + sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym) +valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 (pure final) where fb x y k = lexCombine sym (bitLessThan sym x y) (bitEq sym x y) k fw x y k = lexCombine sym (wordLessThan sym x y) (wordEq sym x y) k @@ -430,8 +430,8 @@ valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 final fz m x y k = lexCombine sym (intModLessThan sym m x y) (intModEq sym m x y) k valGt :: Backend sym => - sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym) -> SEval sym (SBit sym) -valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 final + sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym) +valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 (pure final) where fb x y k = lexCombine sym (bitGreaterThan sym y x) (bitEq sym x y) k fw x y k = lexCombine sym (wordGreaterThan sym x y) (wordEq sym x y) k @@ -475,7 +475,7 @@ greaterThanEqV :: Backend sym => sym -> Binary sym greaterThanEqV sym ty v1 v2 = VBit <$> valGt sym ty v1 v2 (bitLit sym True) signedLessThanV :: Backend sym => sym -> Binary sym -signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz ty v1 v2 (bitLit sym False) +signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz ty v1 v2 (pure $ bitLit sym False) where fb _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on bit type"] fw x y k = lexCombine sym (wordSignedLessThan sym x y) (wordEq sym x y) k @@ -508,7 +508,7 @@ zeroV sym ty = case ty of -- bits TVBit -> - VBit <$> bitLit sym False + pure (VBit (bitLit sym False)) -- integers TVInteger -> diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs index cda9509b..a18a6e02 100644 --- a/src/Cryptol/Eval/SBV.hs +++ b/src/Cryptol/Eval/SBV.hs @@ -197,7 +197,7 @@ instance Backend SBV where bitAsLit _ b = svAsBool b - bitLit _ b = pure $! svBool b + bitLit _ b = svBool b wordLit _ n x = pure $! svInteger (KBounded False (fromInteger n)) x integerLit _ x = pure $! svInteger KUnbounded x @@ -387,8 +387,8 @@ primTable :: Map.Map Ident Value primTable = let sym = SBV in Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v)) [ -- Literals - ("True" , VBit SBV.svTrue) - , ("False" , VBit SBV.svFalse) + ("True" , VBit (bitLit sym True)) + , ("False" , VBit (bitLit sym False)) , ("number" , ecNumberV sym) -- Converts a numeric type into its corresponding value. -- { val, rep } (Literal val rep) => rep @@ -566,7 +566,7 @@ logicShift nm wop reindex = do idx_bits <- enumerateWordValue SBV idx let op bs shft = memoMap $ IndexSeqMap $ \i -> case reindex (Nat w) i shft of - Nothing -> VBit <$> bitLit SBV False + Nothing -> pure (VBit (bitLit SBV False)) Just i' -> lookupSeqMap bs i' LargeBitsVal n <$> shifter (mergeSeqMap SBV) op bs0 idx_bits diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index 1f3d6c2d..1e2b2619 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -169,7 +169,7 @@ randomValue sym ty = randomBit :: (Backend sym, RandomGen g) => sym -> Gen g sym randomBit sym _ g = let (b,g1) = random g - in (VBit <$> bitLit sym b, g1) + in (pure (VBit (bitLit sym b)), g1) randomSize :: RandomGen g => Int -> Int -> g -> (Int, g) randomSize k n g