diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -3,6 +3,14 @@ * Latest Hackage released version: 3.7, 2024-02-15 +### Version 3.8, Not yet released + + * Add support for FP8 formats, as decribed in: https://arxiv.org/pdf/2209.05433.pdf + - E5M2: Which is essentially a synonym for f5+3 + - E4M3: Similar to f4+4, except it does not have infinities and interprets NaN values differently + + * Fix a bug in cracking of arbitrary-sized floats, that yielded wrong values for some NaN cases + ### Version 3.7, 2024-02-15 * Support signaling/quiet indication for decoded NaN values. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -125,15 +125,18 @@ -l lanes Number of lanes to decode -h, -? --help print help, with examples -v --version print version info + -d --debug debug mode, developers only Examples: Encoding: - crackNum -i4 -- -2 -- encode as 4-bit signed integer - crackNum -w4 2 -- encode as 4-bit unsigned integer - crackNum -f3+4 2.5 -- encode as float with 3 bits exponent, 4 bits significand - crackNum -f3+4 2.5 -rRTZ -- encode as above, but use RTZ rounding mode. - crackNum -fbp 2.5 -- encode as a brain-precision float - crackNum -fdp 2.5 -- encode as a double-precision float + crackNum -i4 -- -2 -- encode as 4-bit signed integer + crackNum -w4 2 -- encode as 4-bit unsigned integer + crackNum -f3+4 2.5 -- encode as float with 3 bits exponent, 4 bits significand + crackNum -f3+4 2.5 -rRTZ -- encode as above, but use RTZ rounding mode. + crackNum -fbp 2.5 -- encode as a brain-precision float + crackNum -fdp 2.5 -- encode as a double-precision float + crackNum -fe4m3 2.5 -- encode as an E4M3 FP8 float + crackNum -fe5m2 2.5 -- encode as an E5M2 FP8 float Decoding: crackNum -i4 0b0110 -- decode as 4-bit signed integer, from binary diff --git a/crackNum.cabal b/crackNum.cabal --- a/crackNum.cabal +++ b/crackNum.cabal @@ -1,6 +1,6 @@ Cabal-version : 2.2 Name : crackNum -Version : 3.7 +Version : 3.8 Synopsis : Crack various integer and floating-point data formats Description : Crack IEEE-754 float formats and arbitrary sized words and integers, showing the layout. . @@ -26,7 +26,7 @@ default-language: Haskell2010 hs-source-dirs : src ghc-options : -Wall -Wunused-packages - build-depends : base >= 4.11 && < 5, libBF, sbv >= 10.4 + build-depends : base >= 4.11 && < 5, libBF, sbv >= 10.5 , tasty, tasty-golden, filepath, directory, process other-modules : Paths_crackNum, CrackNum.TestSuite autogen-modules : Paths_crackNum diff --git a/src/CrackNum/Main.hs b/src/CrackNum/Main.hs --- a/src/CrackNum/Main.hs +++ b/src/CrackNum/Main.hs @@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} @@ -19,8 +20,9 @@ import Control.Monad (when) import Data.Char (isDigit, isSpace, toLower) -import Data.List (isPrefixOf, isSuffixOf, unfoldr) +import Data.List (isPrefixOf, isSuffixOf, unfoldr, isInfixOf, intercalate) import Data.Maybe (fromMaybe) + import Text.Read (readMaybe) import System.Environment (getArgs, getProgName, withArgs) import System.Console.GetOpt (ArgOrder(Permute), getOpt, ArgDescr(..), OptDescr(..), usageInfo) @@ -30,11 +32,13 @@ import LibBF import Numeric -import Data.SBV hiding (crack) +import Data.SBV hiding (crack, satCmd) import Data.SBV.Float hiding (FP) -import Data.SBV.Dynamic hiding (satWith) -import Data.SBV.Internals hiding (free) +import Data.SBV.Dynamic hiding (satWith, satCmd) +import Data.SBV.Internals hiding (free, satCmd) +import qualified Data.SBV as SBV + import Data.Version (showVersion) import Paths_crackNum (version) @@ -48,6 +52,8 @@ data FP = SP -- Single precision | DP -- Double precision | FP Int Int -- Arbitrary precision with given exponent and significand sizes + | E5M2 -- Synonym for FP 5 3 (yes, confusing M2->3, but that's the naming) + | E4M3 -- Custom FP8 format with no infinities and limited NaNs deriving (Show, Eq) -- | How many bits does this float occupy @@ -55,6 +61,8 @@ fpSize SP = 32 fpSize DP = 64 fpSize (FP i j) = i+j +fpSize E5M2 = 8 +fpSize E4M3 = 8 -- | Rounding modes we support data RM = RNE -- ^ Round nearest ties to even @@ -88,6 +96,7 @@ | Lanes Int -- ^ How many lanes to decode? | BadFlag [String] -- ^ Bad input | Version -- ^ Version + | Debug -- ^ Run in debug mode. Debugging only. | Help -- ^ Show help deriving (Show, Eq) @@ -101,6 +110,11 @@ isLanes Lanes{} = True isLanes _ = False +-- | Is this the debug flag? +isDebug :: Flag -> Bool +isDebug Debug{} = True +isDebug _ = False + -- | Given an integer flag value, turn it into a flag getSize :: String -> (Int -> Flag) -> String -> Flag getSize flg f n = case readMaybe n of @@ -122,41 +136,45 @@ -- | Given a float flag value, turn it into a flag getFP :: String -> Flag -getFP "hp" = Floating $ FP 5 11 -getFP "bp" = Floating $ FP 8 8 -getFP "sp" = Floating SP -getFP "dp" = Floating DP -getFP "qp" = Floating $ FP 15 113 -getFP ab = case span isDigit ab of - (eb@(_:_), '+':r) -> case span isDigit r of - (sp@(_:_), "") -> mkEBSB (read eb) (read sp) - _ -> bad - _ -> bad - where bad = BadFlag [ "Option " ++ show "-f" ++ " requires one of:" - , "" - , " hp: Half float ( 5 + 11)" - , " bp: Brain float ( 8 + 8)" - , " sp: Single precision ( 8 + 24)" - , " dp: Single precision (11 + 53)" - , " qp: Quad precision (15 + 113)" - , " a+b: Arbitrary precision ( a + b)" - , "" - , "where first number is the number of bits in the exponent" - , "and the second number is the number of bits in the significand, including the implicit bit." - ] - mkEBSB :: Int -> Int -> Flag - mkEBSB eb sb - | eb >= FP_MIN_EB && eb <= FP_MAX_EB - && sb >= FP_MIN_SB && sb <= FP_MAX_SB - = Floating $ FP eb sb - | True - = BadFlag [ "Invalid floating-point precision." - , "" - , " Exponent size must be between " ++ show (FP_MIN_EB :: Int) ++ " to " ++ show (FP_MAX_EB :: Int) - , " Significant size must be between " ++ show (FP_MIN_SB :: Int) ++ " to " ++ show (FP_MAX_SB :: Int) - , "" - , "Received: " ++ show eb ++ " " ++ show sb - ] +getFP "hp" = Floating $ FP 5 11 +getFP "bp" = Floating $ FP 8 8 +getFP "sp" = Floating SP +getFP "dp" = Floating DP +getFP "qp" = Floating $ FP 15 113 +getFP "e5m2" = Floating E5M2 +getFP "e4m3" = Floating E4M3 +getFP ab = case span isDigit ab of + (eb@(_:_), '+':r) -> case span isDigit r of + (sp@(_:_), "") -> mkEBSB (read eb) (read sp) + _ -> bad + _ -> bad + where bad = BadFlag [ "Option " ++ show "-f" ++ " requires one of:" + , "" + , " hp: Half float ( 5 + 11)" + , " bp: Brain float ( 8 + 8)" + , " sp: Single precision ( 8 + 24)" + , " dp: Single precision (11 + 53)" + , " qp: Quad precision (15 + 113)" + , " a+b: Arbitrary IEEE-754 ( a + b)" + , " e5m2: FP8 format (IEEE-754) ( 5 + 3)" + , " e4m3: FP8 format (Alternate) ( 4 + 4)" + , "" + , "In the arbitrary format, the first number is the number of bits in the exponent" + , "and the second number is the number of bits in the significand, including the implicit bit." + ] + mkEBSB :: Int -> Int -> Flag + mkEBSB eb sb + | eb >= FP_MIN_EB && eb <= FP_MAX_EB + && sb >= FP_MIN_SB && sb <= FP_MAX_SB + = Floating $ FP eb sb + | True + = BadFlag [ "Invalid floating-point precision." + , "" + , " Exponent size must be between " ++ show (FP_MIN_EB :: Int) ++ " to " ++ show (FP_MAX_EB :: Int) + , " Significant size must be between " ++ show (FP_MIN_SB :: Int) ++ " to " ++ show (FP_MAX_SB :: Int) + , "" + , "Received: " ++ show eb ++ " " ++ show sb + ] getRM :: String -> Flag getRM "rne" = RMode RNE @@ -183,6 +201,7 @@ , Option "l" [] (ReqArg (getSize "-l" Lanes) "lanes") "Number of lanes to decode" , Option "h?" ["help"] (NoArg Help) "print help, with examples" , Option "v" ["version"] (NoArg Version) "print version info" + , Option "d" ["debug"] (NoArg Debug) "debug mode, developers only" ] -- | Help info @@ -194,12 +213,14 @@ usage pn = putStr $ unlines [ helpStr pn , "Examples:" , " Encoding:" - , " " ++ pn ++ " -i4 -- -2 -- encode as 4-bit signed integer" - , " " ++ pn ++ " -w4 2 -- encode as 4-bit unsigned integer" - , " " ++ pn ++ " -f3+4 2.5 -- encode as float with 3 bits exponent, 4 bits significand" - , " " ++ pn ++ " -f3+4 2.5 -rRTZ -- encode as above, but use RTZ rounding mode." - , " " ++ pn ++ " -fbp 2.5 -- encode as a brain-precision float" - , " " ++ pn ++ " -fdp 2.5 -- encode as a double-precision float" + , " " ++ pn ++ " -i4 -- -2 -- encode as 4-bit signed integer" + , " " ++ pn ++ " -w4 2 -- encode as 4-bit unsigned integer" + , " " ++ pn ++ " -f3+4 2.5 -- encode as float with 3 bits exponent, 4 bits significand" + , " " ++ pn ++ " -f3+4 2.5 -rRTZ -- encode as above, but use RTZ rounding mode." + , " " ++ pn ++ " -fbp 2.5 -- encode as a brain-precision float" + , " " ++ pn ++ " -fdp 2.5 -- encode as a double-precision float" + , " " ++ pn ++ " -fe4m3 2.5 -- encode as an E4M3 FP8 float" + , " " ++ pn ++ " -fe5m2 2.5 -- encode as an E5M2 FP8 float" , "" , " Decoding:" , " " ++ pn ++ " -i4 0b0110 -- decode as 4-bit signed integer, from binary" @@ -244,7 +265,9 @@ arg = dropWhile isSpace $ unwords rs - (kind, eSize) <- case ([b | BadFlag b <- os], filter (\o -> not (isRMode o || isLanes o)) os) of + debug = Debug `elem` os + + (kind, eSize) <- case ([b | BadFlag b <- os], filter (\o -> not (isRMode o || isLanes o || isDebug o)) os) of (e:_, _) -> die e (_, [Signed n]) -> pure (SInt n, n) (_, [Unsigned n]) -> pure (SWord n, n) @@ -274,11 +297,11 @@ | True = lanesGiven if decode - then decodeAllLanes lanes kind arg - else encodeLane lanes kind rm arg + then decodeAllLanes debug lanes kind arg + else encodeLane debug lanes kind rm arg -decodeAllLanes :: Int -> NKind -> String -> IO () -decodeAllLanes lanes kind arg = do +decodeAllLanes :: Bool -> Int -> NKind -> String -> IO () +decodeAllLanes debug lanes kind arg = do when (lanes < 0) $ die ["Number of lanes must be non-negative. Got: " ++ show lanes] @@ -303,7 +326,7 @@ , "" , "Please report this as a bug!" ] - decodeLane (if lanes == 1 then Nothing else Just i) curLaneBits kind + decodeLane debug (if lanes == 1 then Nothing else Just i) curLaneBits kind laneLoop (i-1) remBits laneLoop (lanes - 1) bits -- | Kinds of numbers we understand @@ -360,12 +383,14 @@ pure $ pad ++ res -- | Decoding -decodeLane :: Maybe Int -> [Bool] -> NKind -> IO () -decodeLane mbLane inputBits kind = case kind of - SInt n -> print =<< di True n - SWord n -> print =<< di False n - SFloat s -> df s - where bitString n = do let bits 1 = "one bit" +decodeLane :: Bool -> Maybe Int -> [Bool] -> NKind -> IO () +decodeLane debug mbLane inputBits kind = case kind of + SInt n -> print =<< di True n + SWord n -> print =<< di False n + SFloat s -> df s + where satCmd = satWith z3{crackNum=True, verbose=debug} + + bitString n = do let bits 1 = "one bit" bits b = show b ++ " bits" extra = case mbLane of @@ -379,7 +404,7 @@ di :: Bool -> Int -> IO SatResult di sgn n = do bs <- bitString n - satWith z3{crackNum=True} $ p bs + satCmd $ p bs where p :: [Bool] -> ConstraintSet p bs = do x <- (if sgn then sIntN else sWordN) n "DECODED" mapM_ constrain $ zipWith (.==) (map SBV (svBlastBE x)) (map literal bs) @@ -393,12 +418,15 @@ else sofar) (0 :: Integer) (zip [0..] (reverse allBits)))] + , verbose = debug } case fp of SP -> print =<< satWith config (dFloat bs) DP -> print =<< satWith config (dDouble bs) FP i j -> print =<< satWith config (dFP i j bs) + E5M2 -> fixE5M2Type =<< satWith config (dFP 5 3 bs) + E4M3 -> de4m3 config allBits dFloat :: [SBool] -> ConstraintSet dFloat bs = do x <- sFloat "DECODED" @@ -412,12 +440,62 @@ dFP :: Int -> Int -> [SBool] -> ConstraintSet dFP i j bs = do sx <- svNewVar (KFP i j) "DECODED" - let bits = svBlastBE sx + let bits = svBlastBE $ svFloatingPointAsSWord sx mapM_ constrain $ zipWith (.==) (map SBV bits) bs + -- E4M3 deviates from IEEE, so we have to carefully handle the deviations! + de4m3 config allBits@[sign, True, True, True, True, s1, s2, s3] + | [s1, s2, s3] /= [True, True, True] + = -- Exceptions in the E4M3 format: Exponent is all 1s but significant isn't all ones + -- So, we have to manipulate the output + do res <- satWith config (dFP 4 4 (map literal allBits)) + case res of + SatResult (Satisfiable{}) -> de4m3Model debug (sign, s1, s2, s3) res + _ -> print res + -- Otherwise, it's just FP 4 4 + de4m3 config allBits = print =<< satWith config (dFP 4 4 (map literal allBits)) + +-- Print a model for E5M2, this is the same as dFP 5 3, we just fix the "printed" type +fixE5M2Type :: SatResult -> IO () +fixE5M2Type res = case res of + SatResult (Satisfiable{}) -> mapM_ (putStrLn . fixType) (lines (show res)) + _ -> print res + where fixType :: String -> String + fixType s + | any (`isInfixOf` s) ["ENCODED", "DECODED"] + = takeWhile (/= ':') s ++ ":: E5M2" + | True + = s + +-- Print a deviating model for E4M3: +de4m3Model :: Bool -> (Bool, Bool, Bool, Bool) -> SatResult -> IO () +de4m3Model debug (sign, s1, s2, s3) ieeeResult = do + let ifSet True v = v + ifSet False _ = 0 + + val, sval :: Double + val = 256 + ifSet s1 128 + ifSet s2 64 + ifSet s3 32 + sval + | sign = -val + | True = val + + modifiedResult = SBV.crack debug (literal sval :: SDouble) + + isClassification = ("Classification:" `isInfixOf`) + + fixDecoded l + | "DECODED" `isInfixOf` l + = " DECODED = " ++ show sval ++ " :: E4M3" + | True + = l + + -- Print from the original result upto Classification, rest from the modified result + mapM_ (putStrLn . fixDecoded) $ takeWhile (not . isClassification) (lines (show ieeeResult)) + mapM_ putStrLn $ dropWhile (not . isClassification) (lines modifiedResult) + -- | Encoding -encodeLane :: Int -> NKind -> RM -> String -> IO () -encodeLane lanes num rm inp +encodeLane :: Bool -> Int -> NKind -> RM -> String -> IO () +encodeLane debug lanes num rm inp | lanes /= 1 = die [ "Lanes argument is only valid with decoding values." , "Received: " ++ show lanes @@ -426,10 +504,12 @@ = case num of SInt n -> print =<< ei True n SWord n -> print =<< ei False n - SFloat s -> ef s - where ei :: Bool -> Int -> IO SatResult + SFloat s -> ef s (s == E5M2) + where satCmd = satWith z3{crackNum=True, verbose=debug} + + ei :: Bool -> Int -> IO SatResult ei sgn n = case reads inp of - [(v :: Integer, "")] -> satWith z3{crackNum=True} $ p v + [(v :: Integer, "")] -> satCmd $ p v _ -> die ["Expected an integer value to decode, received: " ++ show inp] where p :: Integer -> Predicate p iv = do let k = KBounded sgn n @@ -442,7 +522,7 @@ Ok -> (v, Nothing) _ -> (v, Just (trim (show s))) where bfOpts = allowSubnormal <> rnd (toLibBFRM rm) <> expBits (fromIntegral i) <> precBits (fromIntegral j) - (v, s) = bfFromString 10 bfOpts inp + (v, s) = bfFromString 10 bfOpts (fixup False inp) trim xs | "[" `isPrefixOf` xs && "]" `isSuffixOf` xs = init (drop 1 xs) | True = xs @@ -452,44 +532,225 @@ Nothing -> putStrLn $ " Note: Conversion from " ++ show inp ++ " was exact. No rounding happened." Just s -> putStrLn $ " Note: Conversion from " ++ show inp ++ " was not faithful. Status: " ++ s ++ "." - ef :: FP -> IO () - ef SP = case reads (fixup inp) of - [(v :: Float, "")] -> do print =<< satWith z3{crackNum=True} (p v) - note $ snd $ convert 8 24 - _ -> ef (FP 8 24) + ef :: FP -> Bool -> IO () + ef SP _ = case reads (fixup True inp) of + [(v :: Float, "")] -> do print =<< satCmd (p v) + note $ snd $ convert 8 24 + _ -> ef (FP 8 24) False where p :: Float -> Predicate p f = do x <- sFloat "ENCODED" pure $ x .=== literal f - ef DP = case reads (fixup inp) of - [(v :: Double, "")] -> do print =<< satWith z3{crackNum=True} (p v) - note $ snd $ convert 11 53 - _ -> ef (FP 11 53) + ef DP _ = case reads (fixup True inp) of + [(v :: Double, "")] -> do print =<< satCmd (p v) + note $ snd $ convert 11 53 + _ -> ef (FP 11 53) False where p :: Double -> Predicate p d = do x <- sDouble "ENCODED" pure $ x .=== literal d - ef (FP i j) = do let (v, mbS) = convert i j - if bfIsNaN v - then die [ "Input does not represent floating point number we recognize." - , "Saw: " ++ inp - , "" - , "For decoding bit-strings, prefix them with 0x, N'h, 0b and" - , "provide a hexadecimal or binary representation of the input." - ] - else do print =<< satWith z3{crackNum=True} (p v) - note mbS - where p :: BigFloat -> Predicate - p bf = do let k = KFP i j - sx <- svNewVar k "ENCODED" - pure $ SBV $ sx `svStrongEqual` SVal k (Left (CV k (CFP (fpFromBigFloat i j bf)))) + ef (FP i j) wasE5M2 = do let (v, mbS) = convert i j + if bfIsNaN v && fixup False inp /= "NaN" + then unrecognized inp + else do res <- satCmd (p v) + if wasE5M2 then fixE5M2Type res + else print res + note mbS + where p :: BigFloat -> Predicate + p bf = do let k = KFP i j + sx <- svNewVar k "ENCODED" + pure $ SBV $ sx `svStrongEqual` SVal k (Left (CV k (CFP (fpFromBigFloat i j bf)))) + ef E5M2 _ = ef (FP 5 3) True -- 3 is intentional; the format ignores the sign storage, but SBV doesn't, following SMTLib + + ef E4M3 _ = encodeE4M3 debug rm inp + -- | Convert certain strings to more understandable format by read -fixup :: String -> String -fixup inp - | linp `elem` ["inf", "infinity"] = "Infinity" - | linp `elem` ["-inf", "-infinity"] = "-Infinity" - | linp == "nan" = "NaN" - | linp == "-nan" = "-NaN" - | True = inp - where linp = map toLower inp +-- If first argument is True, then we're reading using reads, i.e., haskell syntax +-- If first argument is False, then we're using big-float library, which has a different notion for infinity and nans +fixup :: Bool -> String -> String +fixup True inp = case map toLower inp of + linp | linp `elem` ["inf", "infinity"] -> "Infinity" + linp | linp `elem` ["-inf", "-infinity"] -> "-Infinity" + linp | linp == "nan" -> "NaN" + _ -> inp +fixup False inp = case map toLower inp of + linp | linp `elem` ["inf", "infinity"] -> "inf" + linp | linp `elem` ["-inf", "-infinity"] -> "-inf" + linp | linp == "nan" -> "NaN" + _ -> inp + +unrecognized :: String -> IO () +unrecognized inp = die [ "Input does not represent floating point number we recognize." + , "Saw: " ++ inp + , "" + , "For decoding bit-strings, prefix them with 0x, N'h, 0b and" + , "provide a hexadecimal or binary representation of the input." + ] + +-- Bool is True if negative +data ExtraE3M4 = E240 Bool -- Not really extra but can be mapped to + | E256 Bool + | E288 Bool + | E320 Bool + | E352 Bool + | E384 Bool + | E416 Bool + | E448 Bool + deriving Show + +toD :: ExtraE3M4 -> Double +toD (E240 isNeg) = if isNeg then -240 else 240 +toD (E256 isNeg) = if isNeg then -256 else 256 +toD (E288 isNeg) = if isNeg then -288 else 288 +toD (E320 isNeg) = if isNeg then -320 else 320 +toD (E352 isNeg) = if isNeg then -352 else 352 +toD (E384 isNeg) = if isNeg then -384 else 384 +toD (E416 isNeg) = if isNeg then -416 else 416 +toD (E448 isNeg) = if isNeg then -448 else 448 + +neg4 :: Bool -> (String, String, String, String) -> (String, String, String, String) +neg4 True (a, b, c, d) = ('-':a, '-':b, '-':c, '-':d) +neg4 False (a, b, c, d) = (a, b, c, d) + +-- binary, octal, decimal, hex +inBases :: ExtraE3M4 -> (String, String, String, String) +inBases (E240 isNeg) = neg4 isNeg ("0b1.111p+7", "0o3.6p+6", "240.0", "0xFp+4") +inBases (E256 isNeg) = neg4 isNeg ("0b1p+8", "0o4p+6", "256.0", "0x1p+8") +inBases (E288 isNeg) = neg4 isNeg ("0b1.001p+8", "0o4.4p+6", "288.0", "0x1.2p+8") +inBases (E320 isNeg) = neg4 isNeg ("0b1.01p+8", "0o5p+6", "320.0", "0x1.4p+8") +inBases (E352 isNeg) = neg4 isNeg ("0b1.011p+8", "0o5.4p+6", "352.0", "0x1.6p+8") +inBases (E384 isNeg) = neg4 isNeg ("0b1.1p+8", "0o6p+6", "384.0", "0x1.8p+8") +inBases (E416 isNeg) = neg4 isNeg ("0b1.101p+8", "0o6.4p+6", "416.0", "0x1.Ap+8") +inBases (E448 isNeg) = neg4 isNeg ("0b1.11p+8", "0o7p+6", "448.0", "0x1.Cp+8") + +-- Encoding E4M3 is tricky, because of deviation from IEEE. So, we do a case analysis, mostly +encodeE4M3 :: Bool -> RM -> String -> IO () +encodeE4M3 debug rm inp = case reads (fixup True inp) of + [(v :: Double, "")] -> analyze v + _ -> unrecognized inp + where config = z3{ crackNum = True + , verbose = debug + } + + fixEncoded :: SatResult -> String + fixEncoded res@(SatResult (Satisfiable{})) = intercalate "\n" $ map fixType (lines (show res)) + fixEncoded res = show res + + fixType :: String -> String + fixType s + | any (`isInfixOf` s) ["ENCODED", "DECODED"] + = takeWhile (/= ':') s ++ ":: E4M3" + | True + = s + + onEach f = intercalate "\n" . concatMap f . lines + + -- nan representation is unique for E4M3 + fixNaN :: String -> [String] + fixNaN s | "Representation for NaN's is not unique" `isInfixOf` s = [] + | True = [s] + + getNaN = satWith config{crackNumSurfaceVals = [("ENCODED", 0x7F)]} $ + do x :: SFloatingPoint 4 4 <- sFloatingPoint "ENCODED" + constrain $ fpIsNaN x + + analyze :: Double -> IO () + analyze v + -- NaN has two representations, with surface value S.1111.111; we use 0x7F for simplicity + | isNaN v + = getNaN >>= putStrLn . onEach fixNaN . fixEncoded + | isInfinite v + = do getNaN >>= putStrLn . onEach fixNaN . fixEncoded + putStrLn " Note: The input value was infinite, which is not representable in E4M3." + | True + = range v + + -- This list is sorted on the first value. + -- Final bool is True if this value is considered "even" for rounding purposes + extraVals :: [(ExtraE3M4, String, Bool)] + extraVals = [(v True, '1':s, eo) | (v, s, eo) <- reverse pos] + ++ [(v False, '0':s, eo) | (v, s, eo) <- pos] + where pos = [ (E240, "1110111", False) + , (E256, "1111000", True) + , (E288, "1111001", False) + , (E320, "1111010", True) + , (E352, "1111011", False) + , (E384, "1111100", True) + , (E416, "1111101", False) + , (E448, "1111110", True) + ] + + -- Pick the value we land on + pick v = case [p | (d, p) <- dists, d == minVal] of + [x] -> x + [x, y] -> choose v x y + -- The following two can't happen, but just in case: + [] -> error $ "encodeE4M3: Empty list of candidates for " ++ show v -- Can't happen + cands -> error $ "encodeE4M3: More than two candidates for " ++ show v ++ ": " ++ show cands + where dists = [(abs (v - toD ev), p) | p@(ev, _, _) <- extraVals] + minVal = minimum $ map fst dists + + -- choose is called if we're smack in between the two values given. Then, we pick + -- depending on the rounding mode. Note that p1 < p2 is guaranteed here. + choose :: Double -> (ExtraE3M4, String, Bool) -> (ExtraE3M4, String, Bool) -> (ExtraE3M4, String, Bool) + choose v p1@(_, _, eo1) p2@(_, _, eo2) = + let isNegative = v < 0 || isNegativeZero v + in case rm of + RNE -> case (eo1, eo2) of + (True, False) -> p1 + (False, True) -> p2 + _ -> error $ "encodeE4M3: RNE can't pick between values: " ++ show (v, p1, p2) + RNA -> if isNegative then p1 else p2 + RTP -> p2 + RTN -> p1 + RTZ -> if isNegative then p2 else p1 + + range v + | v < -448 || v > 448 -- Out-of-bounds becomes NaN + = do getNaN >>= putStrLn . onEach fixNaN . fixEncoded + putStrLn $ " Note: The input value " ++ show v ++ " is out of bounds, and hence becomes NaN" + putStrLn " The representable range is [-448, 448]" + + | v >= -240 && v <= 240 -- Fits into regular 4+4 format, so just decode + = do res <- satWith config $ do x :: SFloatingPoint 4 4 <- sFloatingPoint "ENCODED" + constrain $ x .== fromSDouble sRNE (literal v) + putStrLn $ fixEncoded res + + -- Otherwise, we're in the range [-448, -240) OR (240, 448] + -- Pick the nearest and display that + | True + = do let (k, bitString, _evenOdd) = pick v + + toInt binDigits = foldr (\(idx, b) sofar -> if b == '0' then sofar + else setBit sofar idx) + (0 :: Integer) + (zip [0..] (reverse binDigits)) + + (signBit, expoBits, binary) = case bitString of + [s, e1, e2, e3, e4, m1, m2, m3] -> + (s == '1', [e1, e2, e3, e4], s : " " ++ e1 : e2 : e3 : e4 : " " ++ m1 : m2 : [m3]) + _ -> error $ "encodee4M3: Unexpected bitstring: " ++ show bitString + + storedExp = toInt expoBits + actualExp = storedExp - 7 + + (bBin, bOct, bDec, bHex) = inBases k + + putStrLn "Satisfiable. Model:" + putStrLn $ " ENCODED = " ++ bDec ++ " :: E4M3" + putStrLn " 7 6543 210" + putStrLn " S -E4- S3-" + putStrLn $ " Binary layout: " ++ binary + putStrLn $ " Hex layout: " ++ showHex (toInt bitString) "" + putStrLn " Precision: 4 exponent bits, 3 significand bits" + putStrLn $ " Sign: " ++ if signBit then "Negative" else "Positive" + putStrLn $ " Exponent: " ++ show actualExp ++ " (Stored: " ++ show storedExp ++ ", Bias: 7)" + putStrLn " Classification: FP_NORMAL" + + putStrLn $ " Binary: " ++ bBin + putStrLn $ " Octal: " ++ bOct + putStrLn $ " Decimal: " ++ bDec + putStrLn $ " Hex: " ++ bHex + putStrLn $ " Rounding mode: " ++ show rm + putStrLn $ " Note: Original value of " ++ show v ++ ", represented as E4M3 special value" diff --git a/src/CrackNum/TestSuite.hs b/src/CrackNum/TestSuite.hs --- a/src/CrackNum/TestSuite.hs +++ b/src/CrackNum/TestSuite.hs @@ -26,14 +26,15 @@ import Data.List (intercalate) -gold :: TestName -> [String] -> TestTree -gold n args = goldenVsFileDiff n diff gf gfTmp (rm gfTmp >> run) +gold :: TestName -> String -> TestTree +gold n as = goldenVsFileDiff n diff gf gfTmp (rm gfTmp >> run) where gf = "Golds" n <.> "gold" gfTmp = gf ++ "_temp" rm f = removeFile f `C.catch` (\(_ :: C.SomeException) -> return ()) - as = unwords args + args = words as + run = do (ec, so, se) <- readProcessWithExitCode "crackNum" args "" writeFile gfTmp $ intercalate "\n" $ [ "Arguments: " ++ as , "Exit code: " ++ show ec @@ -50,24 +51,75 @@ tests :: TestTree tests = testGroup "CrackNum" [ testGroup "Encode" [ - gold "encode0" ["-i4", "--", "-2"] - , gold "encode1" ["-w4", "2"] - , gold "encode2" ["-f3+4", "2.5"] - , gold "encode3" ["-f3+4", "2.5", "-rRTZ"] - , gold "encode4" ["-fbp", "2.5"] - , gold "encode5" ["-fdp", "2.5"] + gold "encode0" "-i4 -- -2" + , gold "encode1" "-w4 2" + , gold "encode2" "-f3+4 2.5" + , gold "encode3" "-f3+4 2.5 -rRTZ" + , gold "encode4" "-fbp 2.5" + , gold "encode5" "-fdp 2.5" + , gold "encode6" "-f3+3 -- -inf" + , gold "encode7" "-f3+3 -- -infinity" + , gold "encode8" "-f3+3 inf" + , gold "encode9" "-f3+3 infinity" + , gold "encode10" "-f3+3 nan" + , gold "encode11" "-fsp -- -inf" + , gold "encode12" "-fsp -- -infinity" + , gold "encode13" "-fsp inf" + , gold "encode14" "-fsp infinity" + , gold "encode15" "-fsp nan" + , gold "encode16" "-fe5m2 2.5" ] + , testGroup "EncodeE4M3" [ + gold "encodeE4M3_nan" "-fe4m3 nan" + , gold "encodeE4M3_+inf" "-fe4m3 inf" + , gold "encodeE4M3_-inf" "-fe4m3 -- -inf" + , gold "encodeE4M3_in1" "-fe4m3 -- -448.0001" + , gold "encodeE4M3_in2" "-fe4m3 -- 448.0001" + , gold "encodeE4M3_bnd1" "-fe4m3 -- -239.9999" + , gold "encodeE4M3_bnd2" "-fe4m3 -- 239.9999" + , gold "encodeE4M3_zero1" "-fe4m3 -- 0" + , gold "encodeE4M3_zero2" "-fe4m3 -- -0" + , gold "encodeE4M3_mr1" "-fe4m3 -- 240" + , gold "encodeE4M3_mr2" "-fe4m3 -- 240.00" + , gold "encodeE4M3_mr3" "-fe4m3 -- -240" + , gold "encodeE4M3_mr4" "-fe4m3 -- -240.00" + ] + , testGroup "EncodeE4M3Special" $ concat [ + [ gold ("encodeE4M3_special_" ++ rm ++ "_+" ++ show i) ("-fe4m3 -r" ++ rm ++ " -- " ++ show i) + , gold ("encodeE4M3_special_" ++ rm ++ "_-" ++ show i) ("-fe4m3 -r" ++ rm ++ " -- -" ++ show i) + ] + | rm <- ["RNE", "RNA", "RTP", "RTN", "RTZ"] + , i :: Double <- [240.01, 248, 419, 432] + ] , testGroup "Decode" [ - gold "decode0" ["-i4", "0b0110"] - , gold "decode1" ["-w4", "0xE"] - , gold "decode2" ["-f3+4", "0b0111001"] - , gold "decode3" ["-fbp", "0x000F"] - , gold "decode4" ["-fdp", "0x8000000000000000"] - , gold "decode5" ["-fhp", "0x7c01"] - , gold "decode6" ["-fhp", "-l8", "128'hffffffffffffffffbdffaaffdc71fc60"] + gold "decode0" "-i4 0b0110" + , gold "decode1" "-w4 0xE" + , gold "decode2" "-f3+4 0b0111001" + , gold "decode3" "-fbp 0x000F" + , gold "decode4" "-fdp 0x8000000000000000" + , gold "decode5" "-fhp 0x7c01" + , gold "decode6" "-fhp -l8 128'hffffffffffffffffbdffaaffdc71fc60" + , gold "decode7" "-fe5m2 0b01111011" ] + , testGroup "DecodeE4M3" [ + gold ("decodeE4M3_" ++ show (if sign then (-val :: Int) else val)) + $ "-fe4m3 0b" ++ (if sign then "1" else "0") ++ "1111" ++ frac + | (val, frac) <- [ (256, "000") + , (288, "001") + , (320, "010") + , (352, "011") + , (384, "100") + , (416, "101") + , (448, "110") + ] + , sign <- [False, True] + ] + , testGroup "DecodeE4M3_NaN" [ + gold "decodeE4M3_+NaN" "-fe4m3 0b_0111_1111" + , gold "decodeE4M3_-NaN" "-fe4m3 0b_1111_1111" + ] , testGroup "Bad" [ - gold "badInvocation0" ["-f3+4", "0b01"] - , gold "badInvocation1" ["-f3+4", "0xFFFF"] + gold "badInvocation0" "-f3+4 0b01" + , gold "badInvocation1" "-f3+4 0xFFFF" ] ]