crackNum 3.7 → 3.8
raw patch · 5 files changed
+446/−122 lines, 5 filesdep ~sbv
Dependency ranges changed: sbv
Files
- CHANGES.md +8/−0
- README.md +9/−6
- crackNum.cabal +2/−2
- src/CrackNum/Main.hs +357/−96
- src/CrackNum/TestSuite.hs +70/−18
CHANGES.md view
@@ -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.
README.md view
@@ -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
crackNum.cabal view
@@ -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
src/CrackNum/Main.hs view
@@ -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"
src/CrackNum/TestSuite.hs view
@@ -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" ] ]