sbv-14.0: Data/SBV/Utils/CrackNum.hs
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Utils.CrackNum
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Crack internal representation for numeric types
-----------------------------------------------------------------------------
{-# LANGUAGE NamedFieldPuns #-}
{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}
module Data.SBV.Utils.CrackNum (
crackNum
) where
import Data.SBV.Core.Concrete
import Data.SBV.Core.Kind
import Data.SBV.Core.SizedFloats
import Data.SBV.Utils.Numeric
import Data.SBV.Utils.PrettyNum (showFloatAtBase)
import Data.Char (intToDigit, toUpper, isSpace)
import Data.Bits
import Data.List
import LibBF hiding (Zero, bfToString)
import Numeric
-- | A class for cracking things deeper, if we know how.
class CrackNum a where
-- | Convert an item to possibly bit-level description, if possible.
crackNum :: a -> Bool -> Maybe Integer -> Maybe String
-- | CVs are easy to crack
instance CrackNum CV where
crackNum cv verbose mbIV = case kindOf cv of
-- Maybe one day we'll have a use for these, currently cracking them
-- any further seems overkill
KVar {} -> Nothing
KBool {} -> Nothing
KUnbounded {} -> Nothing
KReal {} -> Nothing
KApp {} -> Nothing
KADT {} -> Nothing
KChar {} -> Nothing
KString {} -> Nothing
KList {} -> Nothing
KSet {} -> Nothing
KTuple {} -> Nothing
KRational {} -> Nothing
KArray {} -> Nothing
-- Actual crackables
KFloat{} -> Just $ let CFloat f = cvVal cv in float verbose mbIV f
KDouble{} -> Just $ let CDouble d = cvVal cv in float verbose mbIV d
KFP{} -> Just $ let CFP f = cvVal cv in float verbose mbIV f
KBounded sg sz -> Just $ let CInteger i = cvVal cv in int sg sz i
-- How far off the screen we want displayed? Somewhat experimentally found.
tab :: String
tab = replicate 18 ' '
-- Make splits of 4, top one has the remainder
split4 :: Int -> [Int]
split4 n
| m == 0 = rest
| True = m : rest
where (d, m) = n `divMod` 4
rest = replicate d 4
-- Convert bits to the corresponding integer.
getVal :: [Bool] -> Integer
getVal = foldl' (\s b -> 2 * s + if b then 1 else 0) 0
-- Show in hex, but pay attention to how wide a field it should be in
mkHex :: [Bool] -> String
mkHex bin = map toUpper $ showHex (getVal bin) ""
-- | Show a sized word/int in detail
int :: Bool -> Int -> Integer -> String
int signed sz v = intercalate "\n" $ ruler ++ info
where splits = split4 sz
ruler = map (tab ++) $ mkRuler sz splits
bitRep :: [[Bool]]
bitRep = split splits [v `testBit` i | i <- reverse [0 .. sz - 1]]
flatHex = concatMap mkHex bitRep
iprec
| signed = "Signed " ++ show sz ++ "-bit 2's complement integer"
| True = "Unsigned " ++ show sz ++ "-bit word"
signBit = v `testBit` (sz-1)
s | signed && signBit = "-"
| True = ""
av = abs v
info = [ " Binary layout: " ++ unwords [concatMap (\b -> if b then "1" else "0") is | is <- bitRep]
, " Hex layout: " ++ unwords (split (split4 (length flatHex)) flatHex)
, " Type: " ++ iprec
]
++ [ " Sign: " ++ if signBit then "Negative" else "Positive" | signed]
++ [ " Binary: " ++ s ++ "0b" ++ showIntAtBase 2 intToDigit av ""
, " Octal: " ++ s ++ "0o" ++ showOct av ""
, " Decimal: " ++ show v
, " Hex: " ++ s ++ "0x" ++ showHex av ""
]
-- | What kind of Float is this?
data FPKind = Zero Bool -- with sign
| Infty Bool -- with sign
| NaN
| Subnormal
| Normal
deriving Eq
-- | Show instance for Kind, not for reading back!
instance Show FPKind where
show Zero{} = "FP_ZERO"
show Infty{} = "FP_INFINITE"
show NaN = "FP_NAN"
show Subnormal = "FP_SUBNORMAL"
show Normal = "FP_NORMAL"
-- | Find out what kind this float is. We specifically ask
-- the caller to provide if the number is zero, neg-inf, and pos-inf. Why?
-- Because the FP type doesn't have those recognizers that also work with Float/Double.
getKind :: RealFloat a => a -> FPKind
getKind fp
| fp == 0 = Zero (isNegativeZero fp)
| isInfinite fp = Infty (fp < 0)
| isNaN fp = NaN
| isDenormalized fp = Subnormal
| True = Normal
-- Show the value in different bases
showAtBases :: FPKind -> (String, String, String, String) -> Either String (String, String, String, String)
showAtBases k bvs = case k of
Zero False -> Right ("0b0.0", "0o0.0", "0.0", "0x0")
Zero True -> Right ("-0b0.0", "-0o0.0", "-0.0", "-0o0")
Infty False -> Left "Infinity"
Infty True -> Left "-Infinity"
NaN -> Left "NaN"
Subnormal -> Right (dropSuffixes bvs)
Normal -> Right (dropSuffixes bvs)
where dropSuffixes (a, b, c, d) = (bfRemoveRedundantExp a, bfRemoveRedundantExp b, bfRemoveRedundantExp c, bfRemoveRedundantExp d)
-- | Float data for display purposes
data FloatData = FloatData { prec :: String
, eb :: Int
, sb :: Int
, bits :: Integer
, fpKind :: FPKind
, fpVals :: Either String (String, String, String, String)
}
-- | A simple means to organize different bits and pieces of float data
-- for display purposes
class HasFloatData a where
getFloatData :: a -> FloatData
-- | Float instance
instance HasFloatData Float where
getFloatData f = FloatData {
prec = "Single"
, eb = 8
, sb = 24
, bits = fromIntegral (floatToWord f)
, fpKind = k
, fpVals = showAtBases k (showFloatAtBase 2 f "", showFloatAtBase 8 f "", show f, showFloatAtBase 16 f "")
}
where k = getKind f
-- | Double instance
instance HasFloatData Double where
getFloatData d = FloatData {
prec = "Double"
, eb = 11
, sb = 53
, bits = fromIntegral (doubleToWord d)
, fpKind = k
, fpVals = showAtBases k (showFloatAtBase 2 d "", showFloatAtBase 8 d "", show d, showFloatAtBase 16 d "")
}
where k = getKind d
-- | Find the exponent values, (exponent value, exponent as stored, bias)
getExponentData :: FloatData -> (Integer, Integer, Integer)
getExponentData FloatData{eb, sb, bits, fpKind} = (expValue, expStored, bias)
where -- | Bias is 2^(eb-1) - 1
bias :: Integer
bias = (2 :: Integer) ^ ((fromIntegral eb :: Integer) - 1) - 1
-- | Exponent as stored is simply bit extraction
expStored = getVal [bits `testBit` i | i <- reverse [sb-1 .. sb+eb-2]]
-- | Exponent value is stored exponent - bias, unless the number is subnormal. In that case it is 1 - bias
expValue = case fpKind of
Subnormal -> 1 - bias
_ -> expStored - bias
-- | FP instance
instance HasFloatData FP where
getFloatData v@(FP eb sb f) = FloatData {
prec = case (eb, sb) of
( 5, 11) -> "Half (5 exponent bits, 10 significand bits.)"
( 8, 24) -> "Single (8 exponent bits, 23 significand bits.)"
(11, 53) -> "Double (11 exponent bits, 52 significand bits.)"
(15, 113) -> "Quad (15 exponent bits, 112 significand bits.)"
( _, _) -> show eb ++ " exponent bits, " ++ show (sb-1) ++ " significand bit" ++ if sb > 2 then "s" else ""
, eb = eb
, sb = sb
, bits = bfToBits (mkBFOpts eb sb NearEven) f
, fpKind = k
, fpVals = showAtBases k (bfToString 2 True True v, bfToString 8 True True v, bfToString 10 True False v, bfToString 16 True True v)
}
where opts = mkBFOpts eb sb NearEven
k | bfIsZero f = Zero (bfIsNeg f)
| bfIsInf f = Infty (bfIsNeg f)
| bfIsNaN f = NaN
| bfIsSubnormal opts f = Subnormal
| True = Normal
-- | Show a float in detail. mbSurface is the integer equivalent if this is a NaN; so we
-- can represent it faithfully to the original given. Used by crackNum executable.
float :: HasFloatData a => Bool -> Maybe Integer -> a -> String
float verbose mbSurface f = intercalate "\n" $ ruler ++ legend : info
where fd@FloatData{prec, eb, sb, bits = bitsAsStored, fpKind, fpVals} = getFloatData f
nanKind = case fpKind of
Zero{} -> False
Infty{} -> False
NaN -> True
Subnormal -> False
Normal -> False
(nanClassifier, bits, nanChanged)
| nanKind, Just i <- mbSurface = (extraClassifier i, i, i /= bitsAsStored)
| True = ("", bitsAsStored, False)
-- Is this surface representation a signaling NaN or a quiet nan?
-- The test is that the tip bit of the significand is high: If so, quiet. If top bit is low, then signaling.
extraClassifier :: Integer -> String
extraClassifier i
| sb < 2 = "" -- I don't think this can happen, but just in case
| i `testBit` (sb - 2) = " (Quiet)"
| True = " (Signaling)"
splits = [1, eb, sb]
ruler = map (tab ++) $ mkRuler (eb + sb) splits
legend = tab ++ "S " ++ mkTag ('E' : show eb) eb ++ " " ++ mkTag ('S' : show (sb-1)) (sb-1)
mkTag t len = take len $ replicate ((len - length t) `div` 2) '-' ++ t ++ repeat '-'
allBits :: [Bool]
allBits = [bits `testBit` i | i <- reverse [0 .. eb + sb - 1]]
storedBits :: [Bool]
storedBits = [bitsAsStored `testBit` i | i <- reverse [0 .. eb + sb - 1]]
flatHex = concatMap mkHex (split (split4 (eb + sb)) allBits)
sign = bits `testBit` (eb+sb-1)
(exponentVal, storedExponent, bias) = getExponentData fd
esInfo = "Stored: " ++ show storedExponent ++ ", Bias: " ++ show bias
chunks bs = unwords [concatMap (\b -> if b then "1" else "0") is | is <- split splits bs]
isSubNormal = case fpKind of
Subnormal -> True
_ -> False
info = [ " Binary layout: " ++ chunks allBits]
++ [ " Calculated bits: " ++ chunks storedBits ++ " (Surface NaN value differs from calculated)" | verbose && nanChanged]
++ [ " Hex layout: " ++ unwords (split (split4 (length flatHex)) flatHex)
, " Precision: " ++ prec
, " Sign: " ++ if sign then "Negative" else "Positive"
]
++ [ " Exponent: " ++ show exponentVal ++ " (Subnormal, with fixed exponent value. " ++ esInfo ++ ")" | isSubNormal ]
++ [ " Exponent: " ++ show exponentVal ++ " (" ++ esInfo ++ ")" | not isSubNormal]
++ [ " Classification: " ++ show fpKind ++ nanClassifier]
++ (case fpVals of
Left val -> [ " Value: " ++ val]
Right (bval, oval, dval, hval) -> [ " Binary: " ++ bval
, " Octal: " ++ oval
, " Decimal: " ++ dval
, " Hex: " ++ hval
])
++ [ " Note: Representation for NaN's is not unique" | fpKind == NaN]
-- | Build a ruler with given split points
mkRuler :: Int -> [Int] -> [String]
mkRuler n splits = map (trimRight . unwords . split splits . trim Nothing) $ transpose $ map pad $ reverse [0 .. n-1]
where len = length (show (n-1))
pad i = reverse $ take len $ reverse (show i) ++ repeat '0'
trim _ "" = ""
trim mbPrev (c:cs)
| mbPrev == Just c = ' ' : trim mbPrev cs
| True = c : trim (Just c) cs
trimRight = reverse . dropWhile isSpace . reverse
split :: [Int] -> [a] -> [[a]]
split _ [] = []
split [] xs = [xs]
split (i:is) xs = case splitAt i xs of
(pre, []) -> [pre]
(pre, post) -> pre : split is post