diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,14 @@ * Hackage: * GitHub: -* Latest Hackage released version: 3.15, 2024-11-09 +* Latest Hackage released version: 3.17, 2026-08-10 + +### Version 3.17, 2026-08-10 + + * Add support for the FP4 (E2M1) format, via `-ffp4`. Like E4M3, this format + deviates from IEEE-754: The all-ones exponent encodes the values 4 and 6, + instead of infinity and NaN. Consequently, FP4 can represent neither NaN nor + infinity, and finite values outside of [-6, 6] saturate to the end-points. ### Version 3.16, 2026-07-24 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -168,6 +168,7 @@ 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 + crackNum -ffp4 2.5 -- encode as an FP4 (E2M1) float crackNum -fsp 0x3.2p5 -- encode as single-precision from hex-float Decoding: @@ -177,6 +178,7 @@ crackNum -fbp 0x000F -- decode as a brain-precision float crackNum -fdp 0x8000000000000000 -- decode as a double-precision float crackNum -fhp 0x8000 -- decode as a half-precision float + crackNum -ffp4 0b0111 -- decode as an FP4 (E2M1) float crackNum -l4 -fhp 64\'hbdffaaffdc71fc60 -- decode as half-precision float over 4 lanes using verilog notation GUI (macOS): @@ -188,6 +190,8 @@ - Use -- to separate your argument if it's a negative number. - For floats: You can pass in NaN, Inf, -0, -Inf etc as the argument along with a decimal (2.3, -4.1e5) or hexadecimal float (0x2.4p3) + - FP4 (E2M1) has neither NaN nor Inf, so those inputs are rejected. Finite + values outside its range of [-6, 6] saturate to the nearest end-point. - For decoding: - Use hexadecimal (0x) binary (0b), or N'h (verilog) notation as input. Input must have one of these prefixes. 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.16 +Version : 3.17 Synopsis : Crack various integer and floating-point data formats Description : Crack IEEE-754 float formats and arbitrary sized words and integers, showing the layout. . diff --git a/src/CrackNum/Main.hs b/src/CrackNum/Main.hs --- a/src/CrackNum/Main.hs +++ b/src/CrackNum/Main.hs @@ -62,6 +62,7 @@ | 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 + | FP4 -- NVIDIA FP4 (E2M1) format with no infinities and no NaNs deriving (Show, Eq) -- | How many bits does this float occupy @@ -71,6 +72,7 @@ fpSize (FP i j) = i+j fpSize E5M2 = 8 fpSize E4M3 = 8 +fpSize FP4 = 4 kSize :: NKind -> Int kSize (SInt i) = i @@ -146,8 +148,8 @@ #include "MachDeps.h" -#define FP_MIN_EB 2 -#define FP_MIN_SB 2 +#define FP_MIN_EB 1 +#define FP_MIN_SB 1 #if WORD_SIZE_IN_BITS == 64 #define FP_MAX_EB 61 #define FP_MAX_SB 4611686018427387902 @@ -165,6 +167,7 @@ getFP "qp" = Floating $ FP 15 113 getFP "e5m2" = Floating E5M2 getFP "e4m3" = Floating E4M3 +getFP "fp4" = Floating FP4 getFP ab = case span isDigit ab of (eb@(_:_), '+':r) -> case span isDigit r of (sp@(_:_), "") -> mkEBSB (read eb) (read sp) @@ -180,6 +183,7 @@ , " a+b: Arbitrary IEEE-754 ( a + b)" , " e5m2: FP8 format (IEEE-754) ( 5 + 3)" , " e4m3: FP8 format (Alternate) ( 4 + 4)" + , " fp4: FP4 format (E2M1) ( 2 + 2)" , "" , "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." @@ -244,6 +248,7 @@ , " " ++ 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" + , " " ++ pn ++ " -ffp4 2.5 -- encode as an FP4 (E2M1) float" , " " ++ pn ++ " -fsp 0x3.2p5 -- encode as single-precision from hex-float" , "" , " Decoding:" @@ -253,6 +258,7 @@ , " " ++ pn ++ " -fbp 0x000F -- decode as a brain-precision float" , " " ++ pn ++ " -fdp 0x8000000000000000 -- decode as a double-precision float" , " " ++ pn ++ " -fhp 0x8000 -- decode as a half-precision float" + , " " ++ pn ++ " -ffp4 0b0111 -- decode as an FP4 (E2M1) float" , " " ++ pn ++ " -l4 -fhp 64\\'hbdffaaffdc71fc60 -- decode as half-precision float over 4 lanes using verilog notation" , "" , " GUI (macOS):" @@ -264,6 +270,8 @@ , " - Use -- to separate your argument if it's a negative number." , " - For floats: You can pass in NaN, Inf, -0, -Inf etc as the argument" , " along with a decimal (2.3, -4.1e5) or hexadecimal float (0x2.4p3)" + , " - FP4 (E2M1) has neither NaN nor Inf, so those inputs are rejected. Finite" + , " values outside its range of [-6, 6] saturate to the nearest end-point." , " - For decoding:" , " - Use hexadecimal (0x) binary (0b), or N'h (verilog) notation as input." , " Input must have one of these prefixes." @@ -512,6 +520,7 @@ FP i j -> print =<< satWith config (dFP i j bs) E5M2 -> fixE5M2Type =<< satWith config (dFP 5 3 bs) E4M3 -> de4m3 config allBits + FP4 -> dFP4 config allBits dFloat :: [SBool] -> ConstraintSet dFloat bs = do x <- sFloat "DECODED" @@ -540,43 +549,70 @@ -- 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 + -- FP4 also deviates from IEEE. + dFP4 config allBits@[sign, True, True, s1] = + -- normally would be infinity if s1 = 0, and NaN if s1 = 1; but maps to 4/6 instead + do res <- satWith config (dFP 2 2 (map literal allBits)) + case res of + SatResult (Satisfiable{}) -> dFP4Model debug (sign, s1) res + _ -> print res + + -- Otherwise, it's just FP 2 2 + dFP4 config allBits = print =<< satWith config (dFP 2 2 (map literal allBits)) + +-- The non-IEEE formats are all modeled by an IEEE look-alike, so SBV displays the look-alike's +-- type name. Rewrite it to the format the user actually asked for. +retype :: FP -> SatResult -> String +retype fmt res@(SatResult (Satisfiable{})) = intercalate "\n" $ map fixType (lines (show res)) where fixType :: String -> String fixType s | any (`isInfixOf` s) ["ENCODED", "DECODED"] - = takeWhile (/= ':') s ++ ":: E5M2" + = takeWhile (/= ':') s ++ ":: " ++ show fmt | True = s +retype _ res = show res +-- Print a model for E5M2, this is the same as dFP 5 3, we just fix the "printed" type +fixE5M2Type :: SatResult -> IO () +fixE5M2Type = putStrLn . retype E5M2 + -- 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 +de4m3Model debug (sign, s1, s2, s3) = modOut debug sign val E4M3 + where val :: Double + val = 256 + ifSet s1 128 + ifSet s2 64 + ifSet s3 32 - val, sval :: Double - val = 256 + ifSet s1 128 + ifSet s2 64 + ifSet s3 32 - sval - | sign = -val - | True = val + ifSet True v = v + ifSet False _ = 0 +-- Print a deviating model for FP4: +dFP4Model :: Bool -> (Bool, Bool) -> SatResult -> IO () +dFP4Model debug (sign, s1) = modOut debug sign val FP4 + where val :: Double + val | s1 = 6 + | True = 4 + +-- Handle modified output. The bit-layout of these values is precisely what the IEEE look-alike +-- says it is, so we take that part verbatim; but the value itself, and everything that is derived +-- from it, has to come from the double we actually mean. Note that this works for encoding just +-- as well as it does for decoding; the only difference is the label SBV uses. +modOut :: Bool -> Bool -> Double -> FP -> SatResult -> IO () +modOut debug sign val fmt ieeeResult = do + let sval :: Double + 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 + fixVal l = case [tag | tag <- ["ENCODED", "DECODED"], tag `isInfixOf` l] of + tag : _ -> " " ++ tag ++ " = " ++ show sval ++ " :: " ++ show fmt + [] -> 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) + mapM_ (putStrLn . fixVal) $ takeWhile (not . isClassification) (lines (show ieeeResult)) + mapM_ putStrLn $ dropWhile (not . isClassification) (lines modifiedResult) -- | Encoding encodeLane :: Bool -> Int -> NKind -> RM -> String -> IO () @@ -669,6 +705,8 @@ ef E4M3 _ = encodeE4M3 debug rm inp + ef FP4 _ = encodeFP4 debug rm inp + -- | Convert certain strings to more understandable format by read -- 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 @@ -741,15 +779,7 @@ } 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 + fixEncoded = retype E4M3 onEach f = intercalate "\n" . concatMap f . lines @@ -861,3 +891,107 @@ putStrLn $ " Hex: " ++ bHex putStrLn $ " Rounding mode: " ++ show rm putStrLn $ " Note: Original value of " ++ show v ++ ", represented as E4M3 special value" + +-- Likewise encoding FP4 is tricky since it deviates from IEEE. But luckily there aren't too many +-- values to worry about here: There are precisely 8 magnitudes, so we simply round by hand. +encodeFP4 :: Bool -> RM -> String -> IO () +encodeFP4 debug rm inp = case reads (fixup True inp) of + [(v :: Double, "")] -> analyze v + _ -> -- maybe it's a hexfloat? Note that we must scope the + -- catch over the parse only: analyze can legitimately + -- die, and die throws an exit-exception of its own. + do let hr = readHexRational inp + ok <- (rnf hr `seq` pure True) + `C.catch` (\(_ :: C.SomeException) -> pure False) + if ok then analyze (fromRational hr) + else unrecognized inp + where config = z3{ crackNum = True + , verbose = debug + } + + -- The magnitudes FP4 can represent, in increasing order. Note that the index of each + -- magnitude is precisely the value of the low 3 bits of its encoding. The last two + -- (4 and 6) are where FP4 deviates from IEEE, which would call them infinity and NaN. + mags :: [Double] + mags = [0, 0.5, 1, 1.5, 2, 3, 4, 6] + + -- Round the magnitude to the index of one of the representable magnitudes, honoring + -- the rounding mode. Note that rounding a negative value towards +oo is the same thing + -- as rounding its magnitude towards 0; hence the need for the sign here. + roundMag :: Bool -> Double -> Int + roundMag isNeg m + | m >= 6 -- Larger than we can represent; saturate + = 7 + | e : _ <- [i | (i, mv) <- zip [0..] mags, mv == m] -- Exactly representable + = e + | True + = case rm of + RTZ -> lo + RTP -> if isNeg then lo else hi + RTN -> if isNeg then hi else lo + RNE -> nearest (if even lo then lo else hi) + RNA -> nearest hi + where lo = last [i | (i, mv) <- zip [0..] mags, mv < m] + hi = lo + 1 + + -- Ties are broken by the given choice; note that comparing against the sum + -- avoids any rounding of its own, since all the values involved are exact. + nearest tie = case compare (2 * m) (mags !! lo + mags !! hi) of + LT -> lo + GT -> hi + EQ -> tie + + analyze :: Double -> IO () + analyze v + | isNaN v + = die [ "FP4 has no representation for NaN." ] + | isInfinite v + = die [ "FP4 has no representation for infinity." + , "The representable range is [-6, 6]." + ] + | True + = do let isNeg = v < 0 || isNegativeZero v + idx = roundMag isNeg (abs v) + t = (if isNeg then negate else id) (mags !! idx) + + if idx >= 6 then deviant isNeg idx + else regular t + + trailer v t + + -- Everything with magnitude at most 3 is a bona-fide IEEE FP 2 2 value, so let SBV + -- print it; we merely fix the type name it displays. Note that the rounding mode is + -- irrelevant here, since we've already rounded and the value is exactly representable. + regular :: Double -> IO () + regular t = do res <- satWith config $ do x :: SFloatingPoint 2 2 <- sFloatingPoint "ENCODED" + constrain $ x .=== fromSDouble sRNE (literal t) + putStrLn $ retype FP4 res + + -- 4 and 6 sit exactly where IEEE puts infinity and NaN, so we ask SBV for the look-alike + -- and pin the surface bits; that gives us the correct layout without having to guess at + -- SBV's formatting. modOut then replaces the value, and everything derived from it. + deviant :: Bool -> Int -> IO () + deviant isNeg idx = do + let bits :: Integer + bits = (if isNeg then 8 else 0) + (if idx == 7 then 7 else 6) + + res <- satWith config{crackNumSurfaceVals = [("ENCODED", bits)]} $ + do x :: SFloatingPoint 2 2 <- sFloatingPoint "ENCODED" + constrain $ if idx == 7 + then fpIsNaN x -- 6: the NaN slot, whose sign is not observable + else fpIsInfinite x .&& (if isNeg then fpIsNegative x else fpIsPositive x) + + modOut debug isNeg (mags !! idx) FP4 res + + -- Since FP4 has no infinities, out-of-range values saturate to the largest magnitude. + trailer :: Double -> Double -> IO () + trailer v t = do putStrLn $ " Rounding mode: " ++ show rm + note + where note + | abs v > 6 + = do putStrLn $ " Note: Original value of " ++ show v ++ " is out of range, saturated to " ++ show t ++ "." + putStrLn " The representable range is [-6, 6]." + | v == t + = putStrLn $ " Note: Conversion from " ++ show inp ++ " was exact. No rounding happened." + | True + = putStrLn $ " Note: Original value of " ++ show v ++ " was rounded to " ++ show t ++ "." diff --git a/src/CrackNum/TestSuite.hs b/src/CrackNum/TestSuite.hs --- a/src/CrackNum/TestSuite.hs +++ b/src/CrackNum/TestSuite.hs @@ -94,6 +94,30 @@ | rm <- ["RNE", "RNA", "RTP", "RTN", "RTZ"] , i :: Double <- [240.01, 248, 419, 432] ] + , testGroup "EncodeFP4" [ + gold "encodeFP4_nan" "-ffp4 nan" + , gold "encodeFP4_+inf" "-ffp4 inf" + , gold "encodeFP4_-inf" "-ffp4 -- -inf" + , gold "encodeFP4_zero1" "-ffp4 -- 0" + , gold "encodeFP4_zero2" "-ffp4 -- -0" + , gold "encodeFP4_sub" "-ffp4 -- 0.5" -- Subnormal + , gold "encodeFP4_norm" "-ffp4 -- 1.5" + , gold "encodeFP4_dev1" "-ffp4 -- 4" -- Deviates from IEEE: would be +Inf + , gold "encodeFP4_dev2" "-ffp4 -- 6" -- Deviates from IEEE: would be NaN + , gold "encodeFP4_dev3" "-ffp4 -- -6" + , gold "encodeFP4_oob1" "-ffp4 -- 100" -- Saturates + , gold "encodeFP4_oob2" "-ffp4 -- -100" + , gold "encodeFP4_hex" "-ffp4 -- 0x1.8p2" + ] + -- Every value that sits exactly half-way between two representable magnitudes, + -- plus one out-of-range value, over all rounding modes. + , testGroup "EncodeFP4Ties" $ concat [ + [ gold ("encodeFP4_tie_" ++ rm ++ "_+" ++ show i) ("-ffp4 -r" ++ rm ++ " -- " ++ show i) + , gold ("encodeFP4_tie_" ++ rm ++ "_-" ++ show i) ("-ffp4 -r" ++ rm ++ " -- -" ++ show i) + ] + | rm <- ["RNE", "RNA", "RTP", "RTN", "RTZ"] + , i :: Double <- [0.25, 0.75, 1.25, 1.75, 2.5, 3.5, 5, 7] + ] , testGroup "Decode" [ gold "decode0" "-i4 0b0110" , gold "decode1" "-w4 0xE" @@ -121,6 +145,14 @@ , testGroup "DecodeE4M3_NaN" [ gold "decodeE4M3_+NaN" "-fe4m3 0b_0111_1111" , gold "decodeE4M3_-NaN" "-fe4m3 0b_1111_1111" + ] + -- FP4 is small enough that we can simply decode every last one of its 16 patterns. + , testGroup "DecodeFP4" [ + gold ("decodeFP4_" ++ bits) ("-ffp4 0b" ++ bits) + | s <- ["0", "1"] + , e <- ["00", "01", "10", "11"] + , m <- ["0", "1"] + , let bits = s ++ e ++ m ] , testGroup "Bad" [ gold "badInvocation0" "-f3+4 0b01"