crackNum 3.29 → 3.30
raw patch · 12 files changed
+1768/−1453 lines, 12 files
Files
- CHANGES.md +35/−1
- GUI/tclGUI/crackNum.tcl +102/−30
- crackNum.cabal +11/−2
- src/CrackNum/Decode.hs +190/−0
- src/CrackNum/Encode.hs +538/−0
- src/CrackNum/Formats.hs +106/−0
- src/CrackNum/GUI.hs +140/−0
- src/CrackNum/Main.hs +119/−1420
- src/CrackNum/Options.hs +130/−0
- src/CrackNum/Output.hs +188/−0
- src/CrackNum/Types.hs +114/−0
- src/CrackNum/Utils.hs +95/−0
CHANGES.md view
@@ -1,7 +1,41 @@ * Hackage: <http://hackage.haskell.org/package/crackNum> * GitHub: <http://github.com/LeventErkok/crackNum/> -* Latest Hackage released version: 3.29, 2026-08-21+* Latest Hackage released version: 3.30, 2026-08-21++### Version 3.30, 2026-08-21++ * The GUIs now group the floating-point formats by provenance instead of listing all+ twelve of them in one flat "Float" section. The formats that exist because of machine+ learning -- FP4 (E2M1), FP4 (E0M3), FP8 (E4M3), FP8 (E5M2), FP8 (E8M0), Brain, and+ TF32 -- come first under "AI formats", followed by the IEEE-754 ones (Half, Single,+ Double, Quad, and Custom) under "IEEE-754". Integers now precede words, so the+ sidebar reads AI formats, IEEE-754, Integer (Signed), Word (Unsigned). Both the+ macOS (Swift) and the Tcl/Tk GUI are grouped identically. No format was added,+ removed, or renamed, and the command line is unaffected.++ * The "Custom parameters" box in the GUIs is now titled "Custom IEEE-754 float:", and+ its heading lines up flush left with "Rounding mode" above it rather than being+ indented past it. The "(exponent width applies to custom floats)" note is gone, the+ new title having made it redundant. Note that the "Total width" field also applies+ to the Custom entries under Integer (Signed) and Word (Unsigned), which take a width+ but no exponent.++ * The format list in the Tcl/Tk GUI now has a vertical scrollbar. With four sections+ it is taller than the sidebar at the default window size, and without a scrollbar the+ formats past the bottom were not merely off-screen but unreachable. (The macOS GUI+ needed no equivalent change; its list already scrolled.)++ * Scrollbars in the Tcl/Tk GUI now appear only when there is something to scroll to,+ rather than always taking up room. This covers the output pane's pair as well as the+ new one on the format list.++ * Internally, `Main.hs` has been split into per-topic modules -- `CrackNum.Types`,+ `.Formats`, `.Options`, `.Utils`, `.Output`, `.GUI`, `.Decode`, and `.Encode` --+ leaving `Main` with just the argument dispatch. It had grown to some 1400 lines+ holding everything from option parsing to the hand-rolled layouts for the formats+ that have no IEEE look-alike. This is purely a reorganization: every definition+ moved verbatim, so there is no change in behavior or output. ### Version 3.29, 2026-08-21
GUI/tclGUI/crackNum.tcl view
@@ -30,29 +30,30 @@ # Each entry: {id label flag_kind flag_arg} # flag_kind = fixed | customFloat | word | customWord | int | customInt # flag_arg = the flag suffix for "fixed", or bit-count for "word"/"int"+#+# The floats are grouped by provenance rather than by width: first the formats that+# exist because of machine learning (the narrow FP4/FP8 ones, plus bfloat16 and+# TF32), then the IEEE-754 ones. Order here is the order the sidebar shows. The ids+# are what parseArgs maps -f/-w/-i onto, so they stay put even when a format moves+# from one group to another. set FORMAT_SECTIONS {- {"Float" {+ {"AI formats" { {ffp4 "FP4 (E2M1)" fixed fp4} {ffp4e0m3 "FP4 (E0M3)" fixed fp4e0m3} {fe4m3 "FP8 (E4M3)" fixed e4m3} {fe5m2 "FP8 (E5M2)" fixed e5m2} {fe8m0 "FP8 (E8M0)" fixed e8m0}- {fhp "Half" fixed hp} {fbp "Brain" fixed bp} {ftf32 "TF32" fixed tf32}+ }}+ {"IEEE-754" {+ {fhp "Half" fixed hp} {fsp "Single" fixed sp} {fdp "Double" fixed dp} {fqp "Quad" fixed qp} {fcs "Custom" customFloat {}} }}- {"Word (Unsigned)" {- {w8 "8-bit" word 8}- {w16 "16-bit" word 16}- {w32 "32-bit" word 32}- {w64 "64-bit" word 64}- {wcs "Custom" customWord {}}- }} {"Integer (Signed)" { {i8 "8-bit" int 8} {i16 "16-bit" int 16}@@ -60,6 +61,13 @@ {i64 "64-bit" int 64} {ics "Custom" customInt {}} }}+ {"Word (Unsigned)" {+ {w8 "8-bit" word 8}+ {w16 "16-bit" word 16}+ {w32 "32-bit" word 32}+ {w64 "64-bit" word 64}+ {wcs "Custom" customWord {}}+ }} } set ROUNDING_MODES {RNE RNA RTP RTN RTZ}@@ -355,34 +363,62 @@ ttk::style configure Treeview -rowheight 22 ttk::style configure Treeview.Item -padding {4 0} -ttk::treeview .main.side.lb -selectmode browse -show tree -height 18-pack .main.side.lb -fill both -expand yes+# Tk has no auto-hiding scrollbar, so do it by hand: unpack it while the whole list+# fits, and pack it back when it does not. -before keeps it to the right of the+# treeview when it returns, matching how it was packed originally.+#+# NB. Safe against the oscillation that auto-hiding is prone to, because hiding a+# *vertical* scrollbar only makes the treeview wider, which cannot change the vertical+# fractions that decide whether it should be shown. That reasoning does not carry over+# to a horizontal/vertical pair, where each one's visibility feeds the other's.+proc autoScroll {sb tv first last} {+ if {$first <= 0.0 && $last >= 1.0} {+ if {[winfo manager $sb] ne ""} { pack forget $sb }+ } elseif {[winfo manager $sb] eq ""} {+ pack $sb -side right -fill y -before $tv+ }+ $sb set $first $last+} -.main.side.lb tag configure hdr -font {TkDefaultFont 9 bold}-.main.side.lb tag configure item -font {TkDefaultFont 9}+# The format list is taller than the sidebar at the default window size, so it needs+# a scrollbar: without one the rows past the bottom are not merely off-screen, they+# are unreachable. Treeview and scrollbar live in their own frame so the widgets+# packed below (rounding, custom parameters) are unaffected by the side-by-side+# packing used here.+frame .main.side.fmts+pack .main.side.fmts -fill both -expand yes +ttk::treeview .main.side.fmts.lb -selectmode browse -show tree -height 18 \+ -yscrollcommand {autoScroll .main.side.fmts.sy .main.side.fmts.lb}+ttk::scrollbar .main.side.fmts.sy -orient vertical -command {.main.side.fmts.lb yview}+pack .main.side.fmts.sy -side right -fill y+pack .main.side.fmts.lb -side left -fill both -expand yes++.main.side.fmts.lb tag configure hdr -font {TkDefaultFont 9 bold}+.main.side.fmts.lb tag configure item -font {TkDefaultFont 9}+ # Populate treeview; build item-id <-> format-id mappings array set ITEM_FMT {} ;# treeview item id -> format id array set FMT_ITEM {} ;# format id -> treeview item id foreach section $FORMAT_SECTIONS { set title [lindex $section 0]- set sid [.main.side.lb insert {} end -text $title -open yes -tags hdr]+ set sid [.main.side.fmts.lb insert {} end -text $title -open yes -tags hdr] foreach fmt [lindex $section 1] { set fid [lindex $fmt 0]- set iid [.main.side.lb insert $sid end -text [lindex $fmt 1] -tags item]+ set iid [.main.side.fmts.lb insert $sid end -text [lindex $fmt 1] -tags item] set ITEM_FMT($iid) $fid set FMT_ITEM($fid) $iid } } -bind .main.side.lb <<TreeviewSelect>> {- set sel [.main.side.lb selection]+bind .main.side.fmts.lb <<TreeviewSelect>> {+ set sel [.main.side.fmts.lb selection] if {$sel ne "" && [info exists ITEM_FMT($sel)]} { set state(selection) $ITEM_FMT($sel) crack } else {- .main.side.lb selection remove $sel+ .main.side.fmts.lb selection remove $sel } } @@ -410,10 +446,16 @@ crack } -# Custom parameters-labelframe .main.side.custom -text "Custom parameters" -padx 4 -pady 4-pack .main.side.custom -fill x -pady {8 0}+# Custom parameters. The heading is a separate label above the box rather than the+# labelframe's own -text: that keeps the framed/shaded container while letting the+# heading line up flush left with "Rounding mode:" above it, instead of being+# indented past it by the frame's title inset.+label .main.side.customLbl -text "Custom IEEE-754 float:" -anchor w+pack .main.side.customLbl -fill x -pady {8 2} +labelframe .main.side.custom -padx 4 -pady 4+pack .main.side.custom -fill x+ frame .main.side.custom.bw pack .main.side.custom.bw -fill x -pady 2 label .main.side.custom.bw.l -text "Total width:"@@ -432,20 +474,50 @@ pack .main.side.custom.ew.e -side right bind .main.side.custom.ew.e <Return> crack -label .main.side.custom.note \- -text "(exponent width applies to custom floats)" \- -font {TkDefaultFont 8} -foreground gray -wraplength 200 -justify left-pack .main.side.custom.note -fill x -pady {4 0}- # Output pane frame .main.out pack .main.out -side left -fill both -expand yes +# Auto-hiding for the output pane's pair. Unlike the format list's lone vertical bar,+# these two feed each other: dropping the horizontal bar makes the text taller, which+# can change the vertical fractions, and dropping the vertical one makes it wider,+# which can change the horizontal ones. A naive toggle can therefore oscillate when+# the content sits right at the boundary. Three guards:+#+# * track visibility ourselves rather than re-deriving it from the widget, so the+# decision does not depend on geometry that is still settling;+# * act only on an actual change of visibility;+# * defer the change to an idle callback, so a burst of scrollcommand calls during+# one geometry pass collapses into a single decision.+#+# 'grid remove' (rather than 'grid forget') keeps the row/column options, so restoring+# it is a bare 'grid'.+array set SB_VIS {} ;# scrollbar -> 1 when currently gridded+array set SB_PENDING {} ;# scrollbar -> 1 when an idle update is already queued++proc autoScrollGrid {sb first last} {+ global SB_VIS SB_PENDING+ $sb set $first $last+ if {![info exists SB_VIS($sb)]} { set SB_VIS($sb) 1 }+ set want [expr {($first <= 0.0 && $last >= 1.0) ? 0 : 1}]+ if {$want == $SB_VIS($sb) || [info exists SB_PENDING($sb)]} return+ set SB_PENDING($sb) 1+ after idle [list applyScrollVis $sb $want]+}++proc applyScrollVis {sb want} {+ global SB_VIS SB_PENDING+ unset -nocomplain SB_PENDING($sb)+ if {$want == $SB_VIS($sb)} return+ if {$want} { grid $sb } else { grid remove $sb }+ set SB_VIS($sb) $want+}+ text .output -state disabled -wrap none \ -font [list $MONO $state(fontSize)] \ -padx 8 -pady 8 \- -xscrollcommand {.main.out.sx set} \- -yscrollcommand {.main.out.sy set}+ -xscrollcommand {autoScrollGrid .main.out.sx} \+ -yscrollcommand {autoScrollGrid .main.out.sy} scrollbar .main.out.sy -orient vertical -command {.output yview} scrollbar .main.out.sx -orient horizontal -command {.output xview} @@ -517,8 +589,8 @@ # Sync treeview selection highlight if {$state(selection) ne "" && [info exists FMT_ITEM($state(selection))]} { set iid $FMT_ITEM($state(selection))- .main.side.lb selection set $iid- .main.side.lb see $iid+ .main.side.fmts.lb selection set $iid+ .main.side.fmts.lb see $iid } # Sync rounding combo label. Must happen even when no format was given:
crackNum.cabal view
@@ -1,6 +1,6 @@ Cabal-version : 2.2 Name : crackNum-Version : 3.29+Version : 3.30 Synopsis : Crack various integer and floating-point data formats Description : Crack IEEE-754 and other float formats and arbitrary sized words and integers, showing the layout. .@@ -32,5 +32,14 @@ ghc-options : -Wall -Wunused-packages build-depends : base >= 4.11 && < 5, libBF, ghc, sbv >= 11.0 , tasty, tasty-golden, filepath, directory, process, deepseq- other-modules : Paths_crackNum, CrackNum.TestSuite+ other-modules : Paths_crackNum+ , CrackNum.Types+ , CrackNum.Formats+ , CrackNum.Options+ , CrackNum.Utils+ , CrackNum.Output+ , CrackNum.GUI+ , CrackNum.Decode+ , CrackNum.Encode+ , CrackNum.TestSuite autogen-modules : Paths_crackNum
+ src/CrackNum/Decode.hs view
@@ -0,0 +1,190 @@+---------------------------------------------------------------------------+-- |+-- Module : CrackNum.Decode+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Decoding: from a bit-pattern to the value it stands for+-----------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module CrackNum.Decode(+ decodeAllLanes+ ) where++import Control.Monad (when)+++import Data.SBV hiding (crack, satCmd)+import Data.SBV.Dynamic hiding (satWith, satCmd)+import Data.SBV.Internals hiding (free, satCmd)++import CrackNum.Types+import CrackNum.Utils+import CrackNum.Output++decodeAllLanes :: Bool -> Bool -> Int -> NKind -> String -> IO ()+decodeAllLanes isVerilog debug lanes kind arg = do+ when (lanes < 0) $ die+ ["Number of lanes must be non-negative. Got: " ++ show lanes]++ unalteredBits <- parseToBits arg++ bits <- if not isVerilog+ then pure unalteredBits+ else do let needed = lanes * kSize kind+ have = length unalteredBits+ case needed `compare` have of+ EQ -> pure unalteredBits+ LT -> -- we have too much, drop but only if they're all False:+ let (pre, post) = splitAt (have - needed) unalteredBits+ in if all not pre+ then pure post+ else die [ "Needed " ++ show needed ++ " bits, got " ++ show have ++ " bits, " ++ show (have - needed) ++ " extra bits."+ , "But these bits are not all zeros! So, dropping isn't safe."+ , "They are: " ++ map (\d -> if d then '1' else '0') pre+ ]+ GT -> -- we don't have enough. Add enough bits to satisfy+ pure $ replicate (needed - have) False ++ unalteredBits++ let l = length bits+ bitsPerLane = l `div` lanes++ header i | lanes == 1 = pure ()+ | True = putStrLn $ "== Lane " ++ show i ++ " " ++ replicate 60 '='++ when (l `rem` lanes /= 0) $ die+ ["Number of lanes is not a divisor of the bit-length: " ++ show (l, lanes)]++ let laneLoop (-1) [] = pure ()+ laneLoop i curBits = do header i+ let (curLaneBits, remBits) = splitAt bitsPerLane curBits+ when (length curLaneBits /= bitsPerLane) $ die+ [ "INTERNAL ERROR: Missing lane bits: "+ , " Current lane bits: " ++ show curLaneBits+ , " Needed : " ++ show bitsPerLane+ , ""+ , "Please report this as a bug!"+ ]+ decodeLane debug (if lanes == 1 then Nothing else Just i) curLaneBits kind+ laneLoop (i-1) remBits+ laneLoop (lanes - 1) bits++-- | Decoding+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+ Nothing -> ""+ Just i -> "Lane " ++ show i ++ " "++ case length inputBits `compare` n of+ EQ -> pure inputBits+ LT -> die [extra ++ "Input needs to be " ++ show n ++ " bits wide, it's too short by " ++ bits (n - length inputBits)]+ GT -> die [extra ++ "Input needs to be " ++ show n ++ " bits wide, it's too long by " ++ bits (length inputBits - n)]++ di :: Bool -> Int -> IO SatResult+ di sgn n = do bs <- bitString n+ 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)++ df :: FP -> IO ()+ df fp = do allBits <- bitString (fpSize fp)++ let bs = map literal allBits+ config = z3{ crackNum = True+ , crackNumSurfaceVals = [("DECODED", foldr (\(idx, b) sofar -> if b then setBit sofar idx+ 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 -> printAs E5M2 =<< satWith config (dFP 5 3 bs)+ E4M3 -> de4m3 config allBits+ FP4 -> dFP4 config allBits+ FP4E0M3 -> decodeFP4E0M3 allBits+ E8M0 -> decodeE8M0 debug allBits++ dFloat :: [SBool] -> ConstraintSet+ dFloat bs = do x <- sFloat "DECODED"+ let (s, e, m) = blastSFloat x+ mapM_ constrain $ zipWith (.==) (s : e ++ m) bs++ dDouble :: [SBool] -> ConstraintSet+ dDouble bs = do x <- sDouble "DECODED"+ let (s, e, m) = blastSDouble x+ mapM_ constrain $ zipWith (.==) (s : e ++ m) bs++ dFP :: Int -> Int -> [SBool] -> ConstraintSet+ dFP i j bs = do sx <- svNewVar (KFP i j) "DECODED"+ 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+ _ -> printAs E4M3 res+ -- Otherwise, it's just FP 4 4+ de4m3 config allBits = printAs E4M3 =<< satWith config (dFP 4 4 (map literal allBits))++ -- 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+ _ -> printAs FP4 res++ -- Otherwise, it's just FP 2 2+ dFP4 config allBits = printAs FP4 =<< satWith config (dFP 2 2 (map literal allBits))++-- Print a deviating model for E4M3:+de4m3Model :: Bool -> (Bool, Bool, Bool, Bool) -> SatResult -> IO ()+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++ 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++-- | Decoding FP4E0M3: the sign bit and the magnitude are simply read off.+decodeFP4E0M3 :: [Bool] -> IO ()+decodeFP4E0M3 (sign : mag@[_, _, _]) = putStr $ unlines $ fp4e0m3Layout "DECODED" sign (foldl (\sofar b -> 2 * sofar + (if b then 1 else 0)) 0 mag)+decodeFP4E0M3 bs = error $ "decodeFP4E0M3: Unexpected bits: " ++ show bs -- Can't happen; the caller checks the width++-- | Decoding E8M0: the entire byte is the stored exponent.+decodeE8M0 :: Bool -> [Bool] -> IO ()+decodeE8M0 debug bs@[_, _, _, _, _, _, _, _] = putStr $ unlines $ e8m0Layout debug "DECODED" (foldl (\sofar b -> 2 * sofar + (if b then 1 else 0)) 0 bs)+decodeE8M0 _ bs = error $ "decodeE8M0: Unexpected bits: " ++ show bs -- Can't happen; the caller checks the width
+ src/CrackNum/Encode.hs view
@@ -0,0 +1,538 @@+---------------------------------------------------------------------------+-- |+-- Module : CrackNum.Encode+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Encoding: from a value to the bit-pattern it turns into+-----------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module CrackNum.Encode(+ encodeLane+ ) where++import Control.DeepSeq (rnf)+import Data.List (isPrefixOf, isSuffixOf, intercalate)++import qualified Control.Exception as C++import GHC.Utils.Misc (readHexRational)+import GHC.Real (Ratio((:%)))++import LibBF+import Numeric++import Data.SBV hiding (crack, satCmd)+import Data.SBV.Float hiding (FP)+import Data.SBV.Dynamic hiding (satWith, satCmd)+import Data.SBV.Internals hiding (free, satCmd)++import CrackNum.Types+import CrackNum.Utils+import CrackNum.Output++-- | Encoding+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+ ]+ | True+ = case num of+ SInt n -> print =<< ei True n+ SWord n -> print =<< ei False n+ SFloat s -> ef s (s == E5M2)+ where cfg = z3{crackNum=True, verbose=debug, isNonModelVar = (/= "ENCODED")}+ satCmd = satWith cfg++ -- SMTLib's FloatingPoint sort has exactly one NaN value: the solver answers+ -- with the abstract (_ NaN eb sb), so the concrete bit-pattern we display is+ -- picked when that abstract value is materialized, and is not stable across+ -- solver/library upgrades. Pin it to the canonical quiet NaN, the same way+ -- the E4M3 path does. (We still note that the representation isn't unique.)+ satCmdNaN :: Int -> Int -> Predicate -> IO SatResult+ satCmdNaN eb sb = satWith cfg{crackNumSurfaceVals = [("ENCODED", canonicalNaN eb sb)]}++ ei :: Bool -> Int -> IO SatResult+ ei sgn n = case reads inp of+ [(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+ v = SVal k $ Left $ mkConstCV k iv+ x <- (if sgn then sIntN else sWordN) n "ENCODED"+ pure $ SBV (x `svEqual` v)++ convert :: Int -> Int -> (BigFloat, Maybe String)+ convert i j = case s of+ 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 (fixup False inp)+ trim xs | "[" `isPrefixOf` xs && "]" `isSuffixOf` xs = init (drop 1 xs)+ | True = xs++ note :: Maybe String -> IO ()+ note mbs = do putStrLn $ " Rounding mode: " ++ show rm+ case mbs of+ 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 -> Bool -> IO ()+ ef SP _ = case reads (fixup True inp) of+ [(v :: Float, "")] -> do print =<< run v (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++ run f | isNaN f = satCmdNaN 8 24+ | True = satCmd++ ef DP _ = case reads (fixup True inp) of+ [(v :: Double, "")] -> do print =<< run v (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++ run d | isNaN d = satCmdNaN 11 53+ | True = satCmd++ ef (FP i j) wasE5M2 = do let (v, mbS) = convert i j+ if bfIsNaN v && fixup False inp /= "NaN"+ then -- maybe it's a hexfloat?+ do let hr = readHexRational inp+ () <- (rnf hr `seq` return ()) `C.catch` (\(_ :: C.SomeException) -> unrecognized inp)+ res <- satCmd (pRat hr)+ if wasE5M2 then printAs E5M2 res+ else print res+ else do let run | bfIsNaN v = satCmdNaN i j+ | True = satCmd+ res <- run (p v)+ if wasE5M2 then printAs E5M2 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))))++ pRat :: Rational -> Predicate+ pRat (a :% b) = do let k = KFP i j+ sx <- svNewVar k "ENCODED"+ sr <- sReal_+ let top, bot :: SReal+ top = sFromIntegral (literal a)+ bot = sFromIntegral (literal b)+ val = top / bot+ r st = do msv <- sbvToSV st (toSBVRM rm)+ xsv <- sbvToSV st sr+ newExpr st k (SBVApp (IEEEFP (FP_Cast KReal k msv)) [xsv])+ pure $ sr .== val+ .&& SBV (sx `svEqual` SVal k (Right (cache r)))++ 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++ ef FP4 _ = encodeFP4 debug rm inp++ ef FP4E0M3 _ = encodeFP4E0M3 rm inp++ ef E8M0 _ = encodeE8M0 debug rm inp++-- 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+ _ -> -- maybe it's a hexfloat?+ do let hr = readHexRational inp+ (rnf hr `seq` analyze (fromRational hr))+ `C.catch` (\(_ :: C.SomeException) -> unrecognized inp)+ where config = z3{ crackNum = True+ , verbose = debug+ }++ fixEncoded :: SatResult -> String+ fixEncoded = retype E4M3++ -- nan representation is unique for E4M3+ fixNaN :: String -> String+ fixNaN = intercalate "\n" . dropNaNUniquenessNote . lines++ 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 . fixNaN . fixEncoded+ | isInfinite v+ = do getNaN >>= putStrLn . 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 . 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"++-- 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 ++ "."++-- | Encoding FP4E0M3. The representable values are just the integers -7 to 7, so we round+-- the magnitude by hand, saturating anything that doesn't fit.+encodeFP4E0M3 :: RM -> String -> IO ()+encodeFP4E0M3 rm inp = case reads (fixup True inp) of+ [(v :: Double, "")] -> analyze v+ _ -> -- maybe it's a hexfloat? As in encodeFP4, the catch must+ -- scope 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 analyze :: Double -> IO ()+ analyze v+ | isNaN v+ = die [ "FP4E0M3 has no representation for NaN." ]+ | isInfinite v+ = die [ "FP4E0M3 has no representation for infinity."+ , "The representable range is [-7, 7]."+ ]+ | True+ = do let isNeg = v < 0 || isNegativeZero v+ mag = roundMag isNeg (abs v)++ putStr $ unlines $ fp4e0m3Layout "ENCODED" isNeg mag+ trailer v isNeg mag++ -- Round the magnitude to one of 0 .. 7, 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 >= 7 -- Larger than we can represent; saturate+ = 7+ | m == fromIntegral lo -- Exactly representable+ = lo+ | 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 = floor 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) (fromIntegral (lo + hi)) of+ LT -> lo+ GT -> hi+ EQ -> tie++ -- Since FP4E0M3 has no infinities, out-of-range values saturate to the largest magnitude.+ trailer :: Double -> Bool -> Int -> IO ()+ trailer v isNeg mag = do putStrLn $ " Rounding mode: " ++ show rm+ note+ where t = (if isNeg then "-" else "") ++ show mag++ note+ | abs v > 7+ = do putStrLn $ " Note: Original value of " ++ show v ++ " is out of range, saturated to " ++ t ++ "."+ putStrLn " The representable range is [-7, 7]."+ | abs v == fromIntegral mag+ = putStrLn $ " Note: Conversion from " ++ show inp ++ " was exact. No rounding happened."+ | True+ = putStrLn $ " Note: Original value of " ++ show v ++ " was rounded to " ++ t ++ "."++-- | Encoding E8M0. The representable values are the powers of two from 2^-127 to 2^127,+-- plus NaN, so we round the exponent by hand. Rounding is always between two adjacent+-- powers of two; we split them at the arithmetic midpoint (1.5 * 2^e, not the geometric+-- one) and break RNE ties toward the even /stored/ exponent. Both follow 'encodeFP4',+-- which ties on the parity of the encoding index rather than of the value's exponent.+encodeE8M0 :: Bool -> RM -> String -> IO ()+encodeE8M0 debug rm inp = case reads (fixup True inp) of+ [(v :: Double, "")] -> analyze v+ _ -> -- maybe it's a hexfloat? As in encodeFP4, the catch must+ -- scope 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 smallest, largest :: Double+ smallest = e8m0Value 0+ largest = e8m0Value 254++ analyze :: Double -> IO ()+ analyze v+ -- NaN is representable, and uniquely so.+ | isNaN v+ = out 255+ -- A negative is not an out-of-range magnitude: with no sign bit there is no+ -- direction to saturate towards, and clamping would quietly make it positive.+ | v < 0 || isNegativeZero v+ = die [ "E8M0 has no representation for negative values."+ , "The representable range is [2^-127, 2^127], plus NaN."+ ]+ -- Infinity is the limiting overflow, so it saturates along with anything else+ -- that is too large.+ | isInfinite v || v > largest+ = out 254+ -- The bottom of the range is a hard cliff: there is no zero and no subnormal+ -- below 2^-127, so zero and everything under it saturates up to it.+ | v < smallest+ = out 0+ | True+ = out (e8m0Bias + roundExp v)+ where out stored = do putStr $ unlines $ e8m0Layout debug "ENCODED" stored+ trailer v stored++ -- The exponent we land on, for a v already known to be in range. 'exponent'+ -- returns the e with v = m * 2^e and 0.5 <= m < 1, so lo is the exponent whose+ -- power of two sits at or just below v.+ roundExp :: Double -> Int+ roundExp v+ | v == twoTo lo -- Exactly representable+ = lo+ | True+ = case rm of+ RTZ -> lo -- Every value is positive, so RTZ and RTN necessarily agree+ RTN -> lo+ RTP -> hi+ RNE -> nearest (if even (lo + e8m0Bias) then lo else hi)+ RNA -> nearest hi+ where lo = exponent v - 1+ hi = lo + 1++ twoTo :: Int -> Double+ twoTo = encodeFloat 1++ -- Ties are broken by the given choice; note that comparing against the sum+ -- avoids any rounding of its own, since 2*v and 3*2^lo are both exact here.+ nearest tie = case compare (2 * v) (twoTo lo + twoTo hi) of+ LT -> lo+ GT -> hi+ EQ -> tie++ trailer :: Double -> Int -> IO ()+ trailer v stored = do putStrLn $ " Rounding mode: " ++ show rm+ note+ where t = e8m0Value stored++ note+ | isNaN v+ = exact+ | isInfinite v || v > largest || v < smallest+ = do putStrLn $ " Note: Original value of " ++ show v ++ " is out of range, saturated to " ++ show t ++ "."+ putStrLn " The representable range is [2^-127, 2^127]."+ | v == t+ = exact+ | True+ = putStrLn $ " Note: Original value of " ++ show v ++ " was rounded to " ++ show t ++ "."++ exact = putStrLn $ " Note: Conversion from " ++ show inp ++ " was exact. No rounding happened."
+ src/CrackNum/Formats.hs view
@@ -0,0 +1,106 @@+---------------------------------------------------------------------------+-- |+-- Module : CrackNum.Formats+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- The table of floating-point formats, and parsing the -f flag+-----------------------------------------------------------------------------++{-# LANGUAGE CPP #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module CrackNum.Formats(+ fpFormats, fpFormatNames, fpFormatsHelp, getFP+ ) where++import Data.Char (isDigit)++import CrackNum.Types++#include "MachDeps.h"++#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+#else+#define FP_MAX_EB 29+#define FP_MAX_SB 1073741822+#endif++-- | The floating-point formats we support, in the order we present them: the name to+-- pass to -f, what it is, and its (exponent + significand) sizes. The arbitrary format+-- stands in for any a+b pair rather than naming a format of its own, which is what the+-- final field records: only the named ones can be listed as choices.+fpFormats :: [(String, String, String, Bool)]+fpFormats = [ ("hp", "Half float", "( 5 + 11)", True )+ , ("bp", "Brain float", "( 8 + 8)", True )+ , ("tf32", "TensorFloat-32", "( 8 + 11)", True )+ , ("sp", "Single precision", "( 8 + 24)", True )+ , ("dp", "Double precision", "(11 + 53)", True )+ , ("qp", "Quad precision", "(15 + 113)", True )+ , ("a+b", "Arbitrary IEEE-754", "( a + b)", False)+ , ("e5m2", "FP8 format (IEEE-754)", "( 5 + 3)", True )+ , ("e4m3", "FP8 format (Alternate)", "( 4 + 4)", True )+ , ("fp4", "FP4 format (E2M1)", "( 2 + 2)", True )+ , ("fp4e0m3", "FP4 format (E0M3)", "( 0 + 3)", True )+ , ("e8m0", "FP8 format (MX scale)", "( 8 + 0)", True )+ ]++-- | The formats that can actually be named, i.e., everything but the arbitrary a+b+-- placeholder. This is what --list-formats prints, one per line.+fpFormatNames :: [String]+fpFormatNames = [n | (n, _, _, True) <- fpFormats]++-- | Floating-point formats we support, as a table for use in help/error messages.+fpFormatsHelp :: [String]+fpFormatsHelp = [rjust n ++ ": " ++ ljust d ++ " " ++ sz | (n, d, sz, _) <- fpFormats]+ where nw = maximum [length n | (n, _, _, _) <- fpFormats]+ dw = maximum [length d | (_, d, _, _) <- fpFormats]+ rjust x = replicate (nw - length x) ' ' ++ x+ ljust x = x ++ replicate (dw - length x) ' '++-- | 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 "tf32" = Floating $ FP 8 11+getFP "sp" = Floating SP+getFP "dp" = Floating DP+getFP "qp" = Floating $ FP 15 113+getFP "e5m2" = Floating E5M2+getFP "e4m3" = Floating E4M3+getFP "fp4" = Floating FP4+getFP "fp4e0m3" = Floating FP4E0M3+getFP "e8m0" = Floating E8M0+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:"+ , ""+ ]+ ++ fpFormatsHelp+ ++ [ ""+ , "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+ ]
+ src/CrackNum/GUI.hs view
@@ -0,0 +1,140 @@+---------------------------------------------------------------------------+-- |+-- Module : CrackNum.GUI+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Locating and launching the graphical interface+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall -Werror #-}++module CrackNum.GUI(+ launchGUI+ ) where++import System.Directory (findExecutable, doesFileExist)+import System.Environment (lookupEnv, getExecutablePath)+import System.Exit (ExitCode(..))+import System.FilePath (takeDirectory, (</>))+import System.Process (rawSystem)+import qualified System.Info as Info++import Paths_crackNum (getDataFileName)++import CrackNum.Utils (die)++-- | Where the Tcl/Tk GUI script lives relative to the package root; also its+-- location within the installed data-directory. (See Data-files in the cabal file.)+tclRelPath :: FilePath+tclRelPath = "GUI/tclGUI/crackNum.tcl"++-- | Locate the Tcl/Tk GUI script. Normally it is installed together with the+-- binary, so this just works; we look in four places, in order:+--+-- 1. $CRACKNUM_TCL, if set: an explicit override, mirroring $CRACKNUM_GUI on macOS.+-- 2. The PATH, so a source checkout can shadow the installed copy while hacking.+-- 3. Next to the executable itself. This is what makes a relocatable binary+-- distribution work: in one the data-directory below was baked in on the+-- build machine, and names a path that does not exist on the user's.+-- 4. The copy cabal installed in our data-directory.+locateTcl :: IO FilePath+locateTcl = do mbEnv <- lookupEnv "CRACKNUM_TCL"+ case mbEnv of+ Just p -> do ok <- doesFileExist p+ if ok+ then pure p+ else die [ "The CRACKNUM_TCL environment variable is set, but does not name a file:"+ , ""+ , " " ++ p+ ]+ Nothing -> do beside <- besideExe+ installed <- getDataFileName tclRelPath+ mbPath <- findExecutable "crackNum.tcl"+ case mbPath of+ Just p -> pure p+ Nothing -> search [beside, installed] (noTcl beside installed)+ where -- NB. getExecutablePath resolves symlinks, so this finds the script even+ -- when the binary is reached through a link from elsewhere on the PATH.+ besideExe = do exe <- getExecutablePath+ pure (takeDirectory exe </> "crackNum.tcl")++ search [] onFail = die onFail+ search (c:cs) onFail = do ok <- doesFileExist c+ if ok then pure c else search cs onFail++ noTcl beside installed =+ [ "Cannot find the CrackNum GUI script (crackNum.tcl)."+ , ""+ , "Looked in:"+ , " $CRACKNUM_TCL (not set)"+ , " crackNum.tcl on your PATH (not found)"+ , " " ++ beside+ , " " ++ installed+ , ""+ , "This script is normally installed along with crackNum, so seeing this"+ , "means the installed copy is missing or the binary has been moved."+ , ""+ , "If you have a source checkout, point at it directly:"+ , ""+ , " export CRACKNUM_TCL=/path/to/crackNum/" ++ tclRelPath+ , ""+ , "Otherwise, get a copy of the sources with either of:"+ , ""+ , " cabal get crackNum"+ , " git clone http://github.com/LeventErkok/crackNum.git"+ ]++-- | Launch the graphical interface, forwarding all remaining arguments+-- (format flags, rounding mode, and/or the value to crack) so the GUI can preselect+-- them. The GUI itself calls back into this executable to do the actual cracking.+--+-- On macOS the GUI is a Swift/AppKit app; CRACKNUM_GUI can override the .app bundle+-- location. On Linux the GUI is a Tcl/Tk script; 'wish' is located via PATH, and+-- 'crackNum.tcl' via 'locateTcl'.+launchGUI :: [String] -> IO ()+launchGUI vals+ | Info.os == "darwin"+ = do mbApp <- lookupEnv "CRACKNUM_GUI"+ let args = case mbApp of+ Just p -> ["-n", p, "--args"] ++ vals+ Nothing -> ["-n", "-a", "CrackNum", "--args"] ++ vals+ ec <- rawSystem "open" args+ case ec of+ ExitSuccess -> pure ()+ ExitFailure _ -> die [ "Unable to launch the CrackNum GUI application."+ , ""+ , "The CrackNum GUI app does not seem to be installed. To install it,"+ , "get the crackNum sources and build the GUI (macOS 13+, Swift toolchain):"+ , ""+ , " git clone http://github.com/LeventErkok/crackNum.git"+ , " cd crackNum/GUI/swiftGUI"+ , " make install # builds and copies CrackNum.app into /Applications"+ , ""+ , "Then re-run: crackNum --gui" ++ (if null vals then "" else ' ' : unwords vals)+ ]+ | Info.os == "linux"+ = do mbWish <- findExecutable "wish"+ wish <- case mbWish of+ Just w -> pure w+ Nothing -> die [ "Cannot find 'wish' on your PATH."+ , "Install Tcl/Tk to get wish, e.g.:"+ , ""+ , " nix profile install nixpkgs#tk"+ , " sudo apt install tk # Debian/Ubuntu"+ , " sudo dnf install tk # RHEL/Fedora"+ ]+ tcl <- locateTcl+ ec <- rawSystem wish (tcl : vals)+ case ec of+ ExitSuccess -> pure ()+ ExitFailure _ -> die [ "Unable to launch the CrackNum GUI."+ , ""+ , "Tried: " ++ wish ++ " " ++ tcl+ ]+ | True+ = die [ "The --gui option is not supported on this platform (" ++ Info.os ++ ")."+ , "Use crackNum directly from the command line."+ ]
src/CrackNum/Main.hs view
@@ -9,1423 +9,122 @@ -- Main entry point for the crackNum executable ----------------------------------------------------------------------------- -{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TupleSections #-}--{-# OPTIONS_GHC -Wall -Werror #-}--module Main(main) where--import Control.Monad (when)-import Control.DeepSeq (rnf)-import Data.Char (intToDigit, isDigit, isSpace, toLower, toUpper)-import Data.List (isPrefixOf, isSuffixOf, unfoldr, isInfixOf, intercalate)-import Data.Maybe (fromMaybe)--import GHC.Utils.Misc (readHexRational)-import GHC.Real (Ratio((:%)))--import qualified Control.Exception as C--import Text.Read (readMaybe)-import System.Environment (getArgs, getProgName, withArgs, lookupEnv, getExecutablePath)-import System.Console.GetOpt (ArgOrder(Permute), getOpt, ArgDescr(..), OptDescr(..), usageInfo)-import System.Exit (exitFailure, ExitCode(..))-import System.IO (hPutStr, stderr)-import System.Directory (findExecutable, doesFileExist)-import System.FilePath (takeDirectory, (</>))-import System.Process (rawSystem)-import qualified System.Info as Info--import LibBF-import Numeric--import Data.SBV hiding (crack, satCmd)-import Data.SBV.Float hiding (FP)-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, getDataFileName)--import CrackNum.TestSuite---- | Copyright info-copyRight :: String-copyRight = "(c) Levent Erkok. Released with a BSD3 license."---- | Various precisions we support-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- | FP4 -- NVIDIA FP4 (E2M1) format with no infinities and no NaNs- | FP4E0M3 -- 4-bit sign-magnitude integer format; no exponent at all- | E8M0 -- OCP MX scale format; no sign and no significand at all- deriving (Show, Eq)---- | How many bits does this float occupy-fpSize :: FP -> Int-fpSize SP = 32-fpSize DP = 64-fpSize (FP i j) = i+j-fpSize E5M2 = 8-fpSize E4M3 = 8-fpSize FP4 = 4-fpSize FP4E0M3 = 4-fpSize E8M0 = 8--kSize :: NKind -> Int-kSize (SInt i) = i-kSize (SWord i) = i-kSize (SFloat f) = fpSize f---- | Rounding modes we support-data RM = RNE -- ^ Round nearest ties to even- | RNA -- ^ Round nearest ties to away- | RTP -- ^ Round towards positive infinity- | RTN -- ^ Round towards negative infinity- | RTZ -- ^ Round towards zero- deriving (Eq, Enum, Bounded)---- | Show instance for RM, for descriptive purposes-instance Show RM where- show RNE = "RNE: Round nearest ties to even."- show RNA = "RNA: Round nearest ties to away."- show RTP = "RTP: Round towards positive infinity."- show RTN = "RTN: Round towards negative infinity."- show RTZ = "RTZ: Round towards zero."---- Convert to LibBF rounding mode-toLibBFRM :: RM -> RoundMode-toLibBFRM RNE = NearEven-toLibBFRM RNA = NearAway-toLibBFRM RTP = ToPosInf-toLibBFRM RTN = ToNegInf-toLibBFRM RTZ = ToZero---- Convert to SBV rounding mode-toSBVRM :: RM -> SRoundingMode-toSBVRM RNE = sRNE-toSBVRM RNA = sRNA-toSBVRM RTP = sRTP-toSBVRM RTN = sRTN-toSBVRM RTZ = sRTZ---- | Options accepted by the executable-data Flag = Signed Int -- ^ Crack as a signed word with the given number of bits- | Unsigned Int -- ^ Crack as an unsigned word with the given number of bits- | Floating FP -- ^ Crack as the corresponding floating-point type- | RMode RM -- ^ Rounding mode to use- | Lanes Int -- ^ How many lanes to decode?- | BadFlag [String] -- ^ Bad input- | Version -- ^ Version- | Debug -- ^ Run in debug mode. Debugging only.- | GUI -- ^ Launch the graphical interface- | Formats -- ^ List the floating-point formats we support- | Help -- ^ Show help- deriving (Show, Eq)---- | Is this a rounding flag?-isRMode :: Flag -> Bool-isRMode RMode{} = True-isRMode _ = False---- | Is this lanes flag-isLanes :: Flag -> Bool-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- Just i | i > 0 -> f i- | True -> BadFlag ["Option " ++ show flg ++ " requires an integer >= 1. Received: " ++ show n]- Nothing -> BadFlag ["Option " ++ show flg ++ " requires an integer argument. Received: " ++ show n]--#include "MachDeps.h"--#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-#else-#define FP_MAX_EB 29-#define FP_MAX_SB 1073741822-#endif---- | The floating-point formats we support, in the order we present them: the name to--- pass to -f, what it is, and its (exponent + significand) sizes. The arbitrary format--- stands in for any a+b pair rather than naming a format of its own, which is what the--- final field records: only the named ones can be listed as choices.-fpFormats :: [(String, String, String, Bool)]-fpFormats = [ ("hp", "Half float", "( 5 + 11)", True )- , ("bp", "Brain float", "( 8 + 8)", True )- , ("tf32", "TensorFloat-32", "( 8 + 11)", True )- , ("sp", "Single precision", "( 8 + 24)", True )- , ("dp", "Double precision", "(11 + 53)", True )- , ("qp", "Quad precision", "(15 + 113)", True )- , ("a+b", "Arbitrary IEEE-754", "( a + b)", False)- , ("e5m2", "FP8 format (IEEE-754)", "( 5 + 3)", True )- , ("e4m3", "FP8 format (Alternate)", "( 4 + 4)", True )- , ("fp4", "FP4 format (E2M1)", "( 2 + 2)", True )- , ("fp4e0m3", "FP4 format (E0M3)", "( 0 + 3)", True )- , ("e8m0", "FP8 format (MX scale)", "( 8 + 0)", True )- ]---- | The formats that can actually be named, i.e., everything but the arbitrary a+b--- placeholder. This is what --list-formats prints, one per line.-fpFormatNames :: [String]-fpFormatNames = [n | (n, _, _, True) <- fpFormats]---- | Floating-point formats we support, as a table for use in help/error messages.-fpFormatsHelp :: [String]-fpFormatsHelp = [rjust n ++ ": " ++ ljust d ++ " " ++ sz | (n, d, sz, _) <- fpFormats]- where nw = maximum [length n | (n, _, _, _) <- fpFormats]- dw = maximum [length d | (_, d, _, _) <- fpFormats]- rjust x = replicate (nw - length x) ' ' ++ x- ljust x = x ++ replicate (dw - length x) ' '---- | 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 "tf32" = Floating $ FP 8 11-getFP "sp" = Floating SP-getFP "dp" = Floating DP-getFP "qp" = Floating $ FP 15 113-getFP "e5m2" = Floating E5M2-getFP "e4m3" = Floating E4M3-getFP "fp4" = Floating FP4-getFP "fp4e0m3" = Floating FP4E0M3-getFP "e8m0" = Floating E8M0-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:"- , ""- ]- ++ fpFormatsHelp- ++ [ ""- , "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-getRM "rna" = RMode RNA-getRM "rtp" = RMode RTP-getRM "rtn" = RMode RTN-getRM "rtz" = RMode RTZ-getRM m = BadFlag $ [ "Invalid rounding mode."- , ""- , " Must be one of:"- ]- ++ [ " " ++ show r | r <- [minBound .. maxBound::RM]]- ++ [ ""- , "Received: " ++ m- ]---- | Options we accept-pgmOptions :: [OptDescr Flag]-pgmOptions = [- Option "i" [] (ReqArg (getSize "-i" Signed) "N" ) "Signed integer of N-bits"- , Option "w" [] (ReqArg (getSize "-w" Unsigned) "N" ) "Unsigned integer of N-bits"- , Option "f" [] (ReqArg getFP "fp") "Floating point format fp"- , Option "r" [] (ReqArg (getRM . map toLower) "rm") "Rounding mode to use. If not given, Nearest-ties-to-Even."- , 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"- , Option "" ["gui"] (NoArg GUI) "launch the graphical interface"- , Option "" ["list-formats"] (NoArg Formats) "list the formats supported by -f, one per line"- ]---- | Help info-helpStr :: String -> String-helpStr pn = usageInfo ("Usage: " ++ pn ++ " value OR binary/hex-pattern") pgmOptions---- | Print usage info and examples.-usage :: String -> IO ()-usage pn = putStr $ unlines $ [ helpStr pn- , "Supported floating-point formats (for use with -f):"- , ""- ]- ++ map (" " ++) fpFormatsHelp- ++ [ ""- , "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 ++ " -ftf32 2.5 -- encode as a TensorFloat-32 float"- , " " ++ pn ++ " -fdp 2.5 -- encode as a double-precision float"- , " " ++ pn ++ " -fqp 2.5 -- encode as a quad-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 ++ " -ffp4e0m3 3.5 -- encode as an FP4 (E0M3) sign-magnitude integer"- , " " ++ pn ++ " -fe8m0 2.5 -- encode as an E8M0 MX scale (power of two)"- , " " ++ pn ++ " -fsp 0x3.2p5 -- encode as single-precision from hex-float"- , ""- , " Decoding:"- , " " ++ pn ++ " -i4 0b0110 -- decode as 4-bit signed integer, from binary"- , " " ++ pn ++ " -w4 0xE -- decode as 4-bit unsigned integer, from hex"- , " " ++ pn ++ " -f3+4 0b0111001 -- decode as float with 3 bits exponent, 4 bits significand"- , " " ++ pn ++ " -fbp 0x000F -- decode as a brain-precision float"- , " " ++ pn ++ " -ftf32 19\\'h0000F -- decode as a TensorFloat-32 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 ++ " -ffp4e0m3 0b1101 -- decode as an FP4 (E0M3) sign-magnitude integer"- , " " ++ pn ++ " -fe8m0 0x7F -- decode as an E8M0 MX scale (power of two)"- , " " ++ pn ++ " -l4 -fhp 64\\'hbdffaaffdc71fc60 -- decode as half-precision float over 4 lanes using verilog notation"- , ""- , " GUI:"- , " " ++ pn ++ " --gui -- launch the graphical interface"- , " " ++ pn ++ " --gui 0xdeadbeef -- launch the GUI, pre-filled with the given value"- , " " ++ pn ++ " --gui -fsp 0xdeadbeef -- launch the GUI, using the given format"- , ""- , " Notes:"- , " - For encoding:"- , " - 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."- , " - FP4 (E0M3) is a sign-magnitude integer: a sign bit and a 3-bit magnitude,"- , " covering -7 to 7, with both a positive and a negative zero. It has no NaN"- , " and no Inf either, and values outside [-7, 7] saturate to the end-point."- , " - E8M0 (MX scale) is all exponent: no sign bit and no significand at all,"- , " so every value is a power of two, from 2^-127 to 2^127. It has no zero"- , " and no Inf, and 0xFF is its only NaN. Negative inputs are rejected;"- , " values outside the range 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."- , " - You can use _,- or space as a digit to improve readability for the pattern to be decoded"- , " - With -lN parameter, you can decode multiple lanes of data."- , " - If you use verilog input format, then we will infer the number of lanes unless you provide it."- ]---- | Terminate early-die :: [String] -> IO a-die xs = do hPutStr stderr $ unlines $ "ERROR:" : map (" " ++) xs- exitFailure---- | Where the Tcl/Tk GUI script lives relative to the package root; also its--- location within the installed data-directory. (See Data-files in the cabal file.)-tclRelPath :: FilePath-tclRelPath = "GUI/tclGUI/crackNum.tcl"---- | Locate the Tcl/Tk GUI script. Normally it is installed together with the--- binary, so this just works; we look in four places, in order:------ 1. $CRACKNUM_TCL, if set: an explicit override, mirroring $CRACKNUM_GUI on macOS.--- 2. The PATH, so a source checkout can shadow the installed copy while hacking.--- 3. Next to the executable itself. This is what makes a relocatable binary--- distribution work: in one the data-directory below was baked in on the--- build machine, and names a path that does not exist on the user's.--- 4. The copy cabal installed in our data-directory.-locateTcl :: IO FilePath-locateTcl = do mbEnv <- lookupEnv "CRACKNUM_TCL"- case mbEnv of- Just p -> do ok <- doesFileExist p- if ok- then pure p- else die [ "The CRACKNUM_TCL environment variable is set, but does not name a file:"- , ""- , " " ++ p- ]- Nothing -> do beside <- besideExe- installed <- getDataFileName tclRelPath- mbPath <- findExecutable "crackNum.tcl"- case mbPath of- Just p -> pure p- Nothing -> search [beside, installed] (noTcl beside installed)- where -- NB. getExecutablePath resolves symlinks, so this finds the script even- -- when the binary is reached through a link from elsewhere on the PATH.- besideExe = do exe <- getExecutablePath- pure (takeDirectory exe </> "crackNum.tcl")-- search [] onFail = die onFail- search (c:cs) onFail = do ok <- doesFileExist c- if ok then pure c else search cs onFail-- noTcl beside installed =- [ "Cannot find the CrackNum GUI script (crackNum.tcl)."- , ""- , "Looked in:"- , " $CRACKNUM_TCL (not set)"- , " crackNum.tcl on your PATH (not found)"- , " " ++ beside- , " " ++ installed- , ""- , "This script is normally installed along with crackNum, so seeing this"- , "means the installed copy is missing or the binary has been moved."- , ""- , "If you have a source checkout, point at it directly:"- , ""- , " export CRACKNUM_TCL=/path/to/crackNum/" ++ tclRelPath- , ""- , "Otherwise, get a copy of the sources with either of:"- , ""- , " cabal get crackNum"- , " git clone http://github.com/LeventErkok/crackNum.git"- ]---- | Launch the graphical interface, forwarding all remaining arguments--- (format flags, rounding mode, and/or the value to crack) so the GUI can preselect--- them. The GUI itself calls back into this executable to do the actual cracking.------ On macOS the GUI is a Swift/AppKit app; CRACKNUM_GUI can override the .app bundle--- location. On Linux the GUI is a Tcl/Tk script; 'wish' is located via PATH, and--- 'crackNum.tcl' via 'locateTcl'.-launchGUI :: [String] -> IO ()-launchGUI vals- | Info.os == "darwin"- = do mbApp <- lookupEnv "CRACKNUM_GUI"- let args = case mbApp of- Just p -> ["-n", p, "--args"] ++ vals- Nothing -> ["-n", "-a", "CrackNum", "--args"] ++ vals- ec <- rawSystem "open" args- case ec of- ExitSuccess -> pure ()- ExitFailure _ -> die [ "Unable to launch the CrackNum GUI application."- , ""- , "The CrackNum GUI app does not seem to be installed. To install it,"- , "get the crackNum sources and build the GUI (macOS 13+, Swift toolchain):"- , ""- , " git clone http://github.com/LeventErkok/crackNum.git"- , " cd crackNum/GUI/swiftGUI"- , " make install # builds and copies CrackNum.app into /Applications"- , ""- , "Then re-run: crackNum --gui" ++ (if null vals then "" else ' ' : unwords vals)- ]- | Info.os == "linux"- = do mbWish <- findExecutable "wish"- wish <- case mbWish of- Just w -> pure w- Nothing -> die [ "Cannot find 'wish' on your PATH."- , "Install Tcl/Tk to get wish, e.g.:"- , ""- , " nix profile install nixpkgs#tk"- , " sudo apt install tk # Debian/Ubuntu"- , " sudo dnf install tk # RHEL/Fedora"- ]- tcl <- locateTcl- ec <- rawSystem wish (tcl : vals)- case ec of- ExitSuccess -> pure ()- ExitFailure _ -> die [ "Unable to launch the CrackNum GUI."- , ""- , "Tried: " ++ wish ++ " " ++ tcl- ]- | True- = die [ "The --gui option is not supported on this platform (" ++ Info.os ++ ")."- , "Use crackNum directly from the command line."- ]----- | main entry point to crackNum-crack :: String -> [String] -> IO ()-crack pn argv = case getOpt Permute pgmOptions argv of- (_, _, errs@(_:_)) -> die $ errs ++ lines (helpStr pn)- (os, rs, [])- | Version `elem` os -> putStrLn $ pn ++ " v" ++ showVersion version ++ ", " ++ copyRight- -- NB. Machine readable, one name per line: this is what the editor- -- integrations use so they need not hardcode the list of formats.- | Formats `elem` os -> mapM_ putStrLn fpFormatNames- | Help `elem` os -> usage pn- -- NB. Check for bad flags before launching: otherwise a typo like- -- "-ft32" would silently bring the GUI up with nothing selected.- | GUI `elem` os -> case [b | BadFlag b <- os] of- (e:_) -> die e- [] -> launchGUI (filter (/= "--gui") argv)- | True -> do let rm = case reverse [r | RMode r <- os] of- (r:_) -> r- _ -> RNE-- (tryInfer, lanesGiven) = case reverse [l | Lanes l <- os] of- (l:_) -> (False, l)- _ -> (True, 1)-- arg = dropWhile isSpace $ unwords rs-- 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)- (_, [Floating s]) -> pure (SFloat s, fpSize s)- _ -> do usage pn- exitFailure-- let inferLanes :: Int -> IO (Maybe Int)- inferLanes prefix- | prefix `rem` eSize == 0 = pure $ Just (prefix `div` eSize)- | True = die [ "Verilog notation size mismatch:"- , " Input length: " ++ show prefix- , " Element size: " ++ show eSize- , "Length must be an exact multiple of the element size."- ]-- (decode, isVerilog, lanesInferred) <-- case arg of- '0':'x':r -> if any (`elem` ".p") r- then pure (False, False, Nothing)- else pure (True, False, Nothing)- '0':'b':_ -> pure (True, False, Nothing)- _ -> case break (`elem` "'h") arg of- (pre@(_:_), '\'':'h':_)- | all isDigit pre -> (True, True, ) <$> inferLanes (read pre)- _ -> pure (False, False, Nothing)-- let lanes- | tryInfer = fromMaybe lanesGiven lanesInferred- | True = lanesGiven-- let act | decode = decodeAllLanes isVerilog debug lanes kind arg- | True = encodeLane debug lanes kind rm arg-- act `C.catch` solverLimitation kind---- | We accept exponent/significand sizes down to 1 bit, but SMTLib's FloatingPoint--- sort (and hence z3) requires at least 2 of each. Rather than letting such a format--- surface as a raw solver exception with a backtrace, report it as a plain error.--- Anything else is re-thrown untouched.-solverLimitation :: NKind -> SBVException -> IO a-solverLimitation kind e = case kind of- SFloat (FP eb sb) | eb < 2 || sb < 2 -> die [ "The solver does not support this format:"- , " " ++ plural eb "exponent bit" ++ ", " ++ plural sb "significand bit"- , "z3 requires at least 2 of each."- ]- _ -> C.throwIO e- where plural :: Int -> String -> String- plural 1 what = "1 " ++ what- plural n what = show n ++ " " ++ what ++ "s"--decodeAllLanes :: Bool -> Bool -> Int -> NKind -> String -> IO ()-decodeAllLanes isVerilog debug lanes kind arg = do- when (lanes < 0) $ die- ["Number of lanes must be non-negative. Got: " ++ show lanes]-- unalteredBits <- parseToBits arg-- bits <- if not isVerilog- then pure unalteredBits- else do let needed = lanes * kSize kind- have = length unalteredBits- case needed `compare` have of- EQ -> pure unalteredBits- LT -> -- we have too much, drop but only if they're all False:- let (pre, post) = splitAt (have - needed) unalteredBits- in if all not pre- then pure post- else die [ "Needed " ++ show needed ++ " bits, got " ++ show have ++ " bits, " ++ show (have - needed) ++ " extra bits."- , "But these bits are not all zeros! So, dropping isn't safe."- , "They are: " ++ map (\d -> if d then '1' else '0') pre- ]- GT -> -- we don't have enough. Add enough bits to satisfy- pure $ replicate (needed - have) False ++ unalteredBits-- let l = length bits- bitsPerLane = l `div` lanes-- header i | lanes == 1 = pure ()- | True = putStrLn $ "== Lane " ++ show i ++ " " ++ replicate 60 '='-- when (l `rem` lanes /= 0) $ die- ["Number of lanes is not a divisor of the bit-length: " ++ show (l, lanes)]-- let laneLoop (-1) [] = pure ()- laneLoop i curBits = do header i- let (curLaneBits, remBits) = splitAt bitsPerLane curBits- when (length curLaneBits /= bitsPerLane) $ die- [ "INTERNAL ERROR: Missing lane bits: "- , " Current lane bits: " ++ show curLaneBits- , " Needed : " ++ show bitsPerLane- , ""- , "Please report this as a bug!"- ]- 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-data NKind = SInt Int -- ^ Signed integer of n bits- | SWord Int -- ^ Unsigned integer of n bits- | SFloat FP -- ^ Floating point with precision---- | main entry point to crackNum-main :: IO ()-main = do argv <- getArgs- pn <- getProgName-- let rt = "--runTests"-- if rt `elem` argv- then withArgs (filter (`notElem` [rt, "--"]) argv) runTests- else crack pn argv--parseToBits :: String -> IO [Bool]-parseToBits inp = do- let isSkippable c = c `elem` "_-" || isSpace c-- cleanInput = map toLower (filter (not . isSkippable) inp)-- (mbPadTo, isHex, stream) <- case cleanInput of- '0':'x':rest -> pure (Nothing, True, rest)- '0':'b':rest -> pure (Nothing, False, rest)- _ ->- case break (`elem` "'h") cleanInput of- (pre@(_:_), '\'' : 'h' : rest) | all isDigit pre -> pure (Just (read pre), True, rest)- _ -> die [ "Input string must start with 0b, 0x, or N'h for decoding."- , "Received prefix: " ++ show (take 2 cleanInput)- ]-- let cvtBin '1' = pure [True]- cvtBin '0' = pure [False]- cvtBin c = die ["Input has a non-binary digit: " ++ show c]-- cvtHex c = case readHex [c] of- [(v, "")] -> pure $ pad- $ map (== (1::Int))- $ reverse- $ unfoldr (\x -> if x == 0 then Nothing else Just (x `rem` 2, x `div` 2)) v- _ -> die ["Input has a non-hexadecimal digit: " ++ show c]- where pad p = replicate (4 - length p) False ++ p-- cvt i | isHex = concat <$> mapM cvtHex i- | True = concat <$> mapM cvtBin i-- res <- cvt stream-- let pad = case mbPadTo of- Nothing -> []- Just n -> replicate (n - length res) False-- pure $ pad ++ res---- | Decoding-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- Nothing -> ""- Just i -> "Lane " ++ show i ++ " "-- case length inputBits `compare` n of- EQ -> pure inputBits- LT -> die [extra ++ "Input needs to be " ++ show n ++ " bits wide, it's too short by " ++ bits (n - length inputBits)]- GT -> die [extra ++ "Input needs to be " ++ show n ++ " bits wide, it's too long by " ++ bits (length inputBits - n)]-- di :: Bool -> Int -> IO SatResult- di sgn n = do bs <- bitString n- 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)-- df :: FP -> IO ()- df fp = do allBits <- bitString (fpSize fp)-- let bs = map literal allBits- config = z3{ crackNum = True- , crackNumSurfaceVals = [("DECODED", foldr (\(idx, b) sofar -> if b then setBit sofar idx- 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 -> printAs E5M2 =<< satWith config (dFP 5 3 bs)- E4M3 -> de4m3 config allBits- FP4 -> dFP4 config allBits- FP4E0M3 -> decodeFP4E0M3 allBits- E8M0 -> decodeE8M0 debug allBits-- dFloat :: [SBool] -> ConstraintSet- dFloat bs = do x <- sFloat "DECODED"- let (s, e, m) = blastSFloat x- mapM_ constrain $ zipWith (.==) (s : e ++ m) bs-- dDouble :: [SBool] -> ConstraintSet- dDouble bs = do x <- sDouble "DECODED"- let (s, e, m) = blastSDouble x- mapM_ constrain $ zipWith (.==) (s : e ++ m) bs-- dFP :: Int -> Int -> [SBool] -> ConstraintSet- dFP i j bs = do sx <- svNewVar (KFP i j) "DECODED"- 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- _ -> printAs E4M3 res- -- Otherwise, it's just FP 4 4- de4m3 config allBits = printAs E4M3 =<< satWith config (dFP 4 4 (map literal allBits))-- -- 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- _ -> printAs FP4 res-- -- Otherwise, it's just FP 2 2- dFP4 config allBits = printAs FP4 =<< 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 ++ ":: " ++ show fmt- | True- = s-retype _ res = show res---- Print a model for one of the non-IEEE formats: the look-alike does all the work,--- we merely fix the type name it prints.-printAs :: FP -> SatResult -> IO ()-printAs fmt = putStrLn . retype fmt---- Print a deviating model for E4M3:-de4m3Model :: Bool -> (Bool, Bool, Bool, Bool) -> SatResult -> IO ()-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-- 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)-- 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 . fixVal) $ takeWhile (not . isClassification) (lines (show ieeeResult))- mapM_ putStrLn $ dropWhile (not . isClassification) (lines modifiedResult)---- | The line SBV's cracker prints the classification on. Everything from here down--- describes the value itself rather than its layout, which is the split the formats--- that deviate from IEEE need: they take the layout from the look-alike (or lay it--- out by hand) and the rest from the value they actually mean.-isClassification :: String -> Bool-isClassification = ("Classification:" `isInfixOf`)---- | SBV notes that a NaN's representation is not unique. That holds for IEEE formats,--- but not for the ones here that have exactly one NaN pattern (E4M3 and E8M0), so drop--- the note for those rather than claim an ambiguity the format does not have.-dropNaNUniquenessNote :: [String] -> [String]-dropNaNUniquenessNote = filter (not . ("Representation for NaN's is not unique" `isInfixOf`))---- | The canonical quiet-NaN pattern for a float with @eb@ exponent bits and @sb@--- significand bits (including the implicit one): sign 0, all-ones exponent, and only--- the leading stored significand bit set. For single-precision this is 0x7FC00000.-canonicalNaN :: Int -> Int -> Integer-canonicalNaN eb sb = (2 ^ eb - 1) * 2 ^ (sb - 1) + 2 ^ (sb - 2)---- | Encoding-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- ]- | True- = case num of- SInt n -> print =<< ei True n- SWord n -> print =<< ei False n- SFloat s -> ef s (s == E5M2)- where cfg = z3{crackNum=True, verbose=debug, isNonModelVar = (/= "ENCODED")}- satCmd = satWith cfg-- -- SMTLib's FloatingPoint sort has exactly one NaN value: the solver answers- -- with the abstract (_ NaN eb sb), so the concrete bit-pattern we display is- -- picked when that abstract value is materialized, and is not stable across- -- solver/library upgrades. Pin it to the canonical quiet NaN, the same way- -- the E4M3 path does. (We still note that the representation isn't unique.)- satCmdNaN :: Int -> Int -> Predicate -> IO SatResult- satCmdNaN eb sb = satWith cfg{crackNumSurfaceVals = [("ENCODED", canonicalNaN eb sb)]}-- ei :: Bool -> Int -> IO SatResult- ei sgn n = case reads inp of- [(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- v = SVal k $ Left $ mkConstCV k iv- x <- (if sgn then sIntN else sWordN) n "ENCODED"- pure $ SBV (x `svEqual` v)-- convert :: Int -> Int -> (BigFloat, Maybe String)- convert i j = case s of- 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 (fixup False inp)- trim xs | "[" `isPrefixOf` xs && "]" `isSuffixOf` xs = init (drop 1 xs)- | True = xs-- note :: Maybe String -> IO ()- note mbs = do putStrLn $ " Rounding mode: " ++ show rm- case mbs of- 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 -> Bool -> IO ()- ef SP _ = case reads (fixup True inp) of- [(v :: Float, "")] -> do print =<< run v (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-- run f | isNaN f = satCmdNaN 8 24- | True = satCmd-- ef DP _ = case reads (fixup True inp) of- [(v :: Double, "")] -> do print =<< run v (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-- run d | isNaN d = satCmdNaN 11 53- | True = satCmd-- ef (FP i j) wasE5M2 = do let (v, mbS) = convert i j- if bfIsNaN v && fixup False inp /= "NaN"- then -- maybe it's a hexfloat?- do let hr = readHexRational inp- () <- (rnf hr `seq` return ()) `C.catch` (\(_ :: C.SomeException) -> unrecognized inp)- res <- satCmd (pRat hr)- if wasE5M2 then printAs E5M2 res- else print res- else do let run | bfIsNaN v = satCmdNaN i j- | True = satCmd- res <- run (p v)- if wasE5M2 then printAs E5M2 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))))-- pRat :: Rational -> Predicate- pRat (a :% b) = do let k = KFP i j- sx <- svNewVar k "ENCODED"- sr <- sReal_- let top, bot :: SReal- top = sFromIntegral (literal a)- bot = sFromIntegral (literal b)- val = top / bot- r st = do msv <- sbvToSV st (toSBVRM rm)- xsv <- sbvToSV st sr- newExpr st k (SBVApp (IEEEFP (FP_Cast KReal k msv)) [xsv])- pure $ sr .== val- .&& SBV (sx `svEqual` SVal k (Right (cache r)))-- 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-- ef FP4 _ = encodeFP4 debug rm inp-- ef FP4E0M3 _ = encodeFP4E0M3 rm inp-- ef E8M0 _ = encodeE8M0 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-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- _ -> -- maybe it's a hexfloat?- do let hr = readHexRational inp- (rnf hr `seq` analyze (fromRational hr))- `C.catch` (\(_ :: C.SomeException) -> unrecognized inp)- where config = z3{ crackNum = True- , verbose = debug- }-- fixEncoded :: SatResult -> String- fixEncoded = retype E4M3-- -- nan representation is unique for E4M3- fixNaN :: String -> String- fixNaN = intercalate "\n" . dropNaNUniquenessNote . lines-- 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 . fixNaN . fixEncoded- | isInfinite v- = do getNaN >>= putStrLn . 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 . 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"---- 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 ++ "."---- FP4E0M3 is a 4-bit sign-magnitude integer: a sign bit and a 3-bit magnitude, covering--- -7 to 7, with both a positive and a negative zero. Having no exponent at all, it has no--- IEEE look-alike we could lean on, so we lay the bits out by hand; the shape follows what--- crackNum prints for the plain integer formats, which is what this format really is.-fp4e0m3Layout :: String -> Bool -> Int -> [String]-fp4e0m3Layout tag isNeg mag =- [ "Satisfiable. Model:"- , " " ++ tag ++ " = " ++ sign ++ show mag ++ " :: " ++ show FP4E0M3- , " 3 210"- , " S -M-"- , " Binary layout: " ++ (if isNeg then '1' else '0') : ' ' : pad 3 (inBase 2 mag)- , " Hex layout: " ++ map toUpper (inBase 16 ((if isNeg then 8 else 0) + mag))- , " Type: 4-bit sign-magnitude integer"- , " Sign: " ++ (if isNeg then "Negative" else "Positive")- , " Binary: " ++ sign ++ "0b" ++ inBase 2 mag- , " Octal: " ++ sign ++ "0o" ++ inBase 8 mag- , " Decimal: " ++ sign ++ show mag- , " Hex: " ++ sign ++ "0x" ++ inBase 16 mag- ]- where sign = if isNeg then "-" else ""-- inBase b v = showIntAtBase b intToDigit v ""-- pad n s = replicate (n - length s) '0' ++ s---- | Decoding FP4E0M3: the sign bit and the magnitude are simply read off.-decodeFP4E0M3 :: [Bool] -> IO ()-decodeFP4E0M3 (sign : mag@[_, _, _]) = putStr $ unlines $ fp4e0m3Layout "DECODED" sign (foldl (\sofar b -> 2 * sofar + (if b then 1 else 0)) 0 mag)-decodeFP4E0M3 bs = error $ "decodeFP4E0M3: Unexpected bits: " ++ show bs -- Can't happen; the caller checks the width---- | Encoding FP4E0M3. The representable values are just the integers -7 to 7, so we round--- the magnitude by hand, saturating anything that doesn't fit.-encodeFP4E0M3 :: RM -> String -> IO ()-encodeFP4E0M3 rm inp = case reads (fixup True inp) of- [(v :: Double, "")] -> analyze v- _ -> -- maybe it's a hexfloat? As in encodeFP4, the catch must- -- scope 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 analyze :: Double -> IO ()- analyze v- | isNaN v- = die [ "FP4E0M3 has no representation for NaN." ]- | isInfinite v- = die [ "FP4E0M3 has no representation for infinity."- , "The representable range is [-7, 7]."- ]- | True- = do let isNeg = v < 0 || isNegativeZero v- mag = roundMag isNeg (abs v)-- putStr $ unlines $ fp4e0m3Layout "ENCODED" isNeg mag- trailer v isNeg mag-- -- Round the magnitude to one of 0 .. 7, 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 >= 7 -- Larger than we can represent; saturate- = 7- | m == fromIntegral lo -- Exactly representable- = lo- | 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 = floor 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) (fromIntegral (lo + hi)) of- LT -> lo- GT -> hi- EQ -> tie-- -- Since FP4E0M3 has no infinities, out-of-range values saturate to the largest magnitude.- trailer :: Double -> Bool -> Int -> IO ()- trailer v isNeg mag = do putStrLn $ " Rounding mode: " ++ show rm- note- where t = (if isNeg then "-" else "") ++ show mag-- note- | abs v > 7- = do putStrLn $ " Note: Original value of " ++ show v ++ " is out of range, saturated to " ++ t ++ "."- putStrLn " The representable range is [-7, 7]."- | abs v == fromIntegral mag- = putStrLn $ " Note: Conversion from " ++ show inp ++ " was exact. No rounding happened."- | True- = putStrLn $ " Note: Original value of " ++ show v ++ " was rounded to " ++ t ++ "."---- | E8M0 is the OCP Microscaling (MX) scale format: the value that scales a block of--- MXFP8/MXFP6/MXFP4 elements. All 8 bits are exponent -- there is no sign bit and no--- significand at all -- so every value is the power of two 2^(E-127), and 0xFF is its--- one and only NaN. Having no significand, it has no zero and no subnormals either:--- with nothing for the E=0 encoding to mean, it simply denotes 2^-127.-e8m0Bias :: Int-e8m0Bias = 127---- | The value a stored E8M0 exponent denotes. All 254 finite values are exactly--- representable as a Double, since 2^(+/-127) is nowhere near its range limits; note--- that 'encodeFloat' builds them exactly, which @2 **@ would not be guaranteed to do.-e8m0Value :: Int -> Double-e8m0Value 255 = 0/0-e8m0Value e = encodeFloat 1 (e - e8m0Bias)---- | Lay out an E8M0 value. With no sign and no significand there is no IEEE look-alike--- to lean on, so the layout is built by hand, following the shape crackNum prints for--- the other formats. Everything from the classification down describes the value rather--- than its layout, so that part comes from cracking the equivalent Double -- the same--- division of labor 'modOut' uses for the E4M3 and FP4 deviations.-e8m0Layout :: Bool -> String -> Int -> [String]-e8m0Layout debug tag stored =- [ "Satisfiable. Model:"- , " " ++ tag ++ " = " ++ show v ++ " :: " ++ show E8M0- , " 76543210"- , " ---E8---"- , " Binary layout: " ++ pad 8 (inBase 2 stored)- , " Hex layout: " ++ map toUpper (pad 2 (inBase 16 stored))- , " Precision: 8 exponent bits, no significand"- -- NB. There is no sign bit: bit 7 is the exponent's MSB. We print the line anyway,- -- so the block keeps the same shape as every other format, but say outright that- -- it can never read anything else.- , " Sign: Positive (always)"- , " Exponent: " ++ show (stored - e8m0Bias) ++ " (Stored: " ++ show stored ++ ", Bias: " ++ show e8m0Bias ++ ")"- ]- ++ dropNaNUniquenessNote (dropWhile (not . isClassification) (lines (SBV.crack debug (literal v :: SDouble))))- where v = e8m0Value stored-- inBase b x = showIntAtBase b intToDigit x ""-- pad n x = replicate (n - length x) '0' ++ x---- | Decoding E8M0: the entire byte is the stored exponent.-decodeE8M0 :: Bool -> [Bool] -> IO ()-decodeE8M0 debug bs@[_, _, _, _, _, _, _, _] = putStr $ unlines $ e8m0Layout debug "DECODED" (foldl (\sofar b -> 2 * sofar + (if b then 1 else 0)) 0 bs)-decodeE8M0 _ bs = error $ "decodeE8M0: Unexpected bits: " ++ show bs -- Can't happen; the caller checks the width---- | Encoding E8M0. The representable values are the powers of two from 2^-127 to 2^127,--- plus NaN, so we round the exponent by hand. Rounding is always between two adjacent--- powers of two; we split them at the arithmetic midpoint (1.5 * 2^e, not the geometric--- one) and break RNE ties toward the even /stored/ exponent. Both follow 'encodeFP4',--- which ties on the parity of the encoding index rather than of the value's exponent.-encodeE8M0 :: Bool -> RM -> String -> IO ()-encodeE8M0 debug rm inp = case reads (fixup True inp) of- [(v :: Double, "")] -> analyze v- _ -> -- maybe it's a hexfloat? As in encodeFP4, the catch must- -- scope 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 smallest, largest :: Double- smallest = e8m0Value 0- largest = e8m0Value 254-- analyze :: Double -> IO ()- analyze v- -- NaN is representable, and uniquely so.- | isNaN v- = out 255- -- A negative is not an out-of-range magnitude: with no sign bit there is no- -- direction to saturate towards, and clamping would quietly make it positive.- | v < 0 || isNegativeZero v- = die [ "E8M0 has no representation for negative values."- , "The representable range is [2^-127, 2^127], plus NaN."- ]- -- Infinity is the limiting overflow, so it saturates along with anything else- -- that is too large.- | isInfinite v || v > largest- = out 254- -- The bottom of the range is a hard cliff: there is no zero and no subnormal- -- below 2^-127, so zero and everything under it saturates up to it.- | v < smallest- = out 0- | True- = out (e8m0Bias + roundExp v)- where out stored = do putStr $ unlines $ e8m0Layout debug "ENCODED" stored- trailer v stored-- -- The exponent we land on, for a v already known to be in range. 'exponent'- -- returns the e with v = m * 2^e and 0.5 <= m < 1, so lo is the exponent whose- -- power of two sits at or just below v.- roundExp :: Double -> Int- roundExp v- | v == twoTo lo -- Exactly representable- = lo- | True- = case rm of- RTZ -> lo -- Every value is positive, so RTZ and RTN necessarily agree- RTN -> lo- RTP -> hi- RNE -> nearest (if even (lo + e8m0Bias) then lo else hi)- RNA -> nearest hi- where lo = exponent v - 1- hi = lo + 1-- twoTo :: Int -> Double- twoTo = encodeFloat 1-- -- Ties are broken by the given choice; note that comparing against the sum- -- avoids any rounding of its own, since 2*v and 3*2^lo are both exact here.- nearest tie = case compare (2 * v) (twoTo lo + twoTo hi) of- LT -> lo- GT -> hi- EQ -> tie-- trailer :: Double -> Int -> IO ()- trailer v stored = do putStrLn $ " Rounding mode: " ++ show rm- note- where t = e8m0Value stored-- note- | isNaN v- = exact- | isInfinite v || v > largest || v < smallest- = do putStrLn $ " Note: Original value of " ++ show v ++ " is out of range, saturated to " ++ show t ++ "."- putStrLn " The representable range is [2^-127, 2^127]."- | v == t- = exact- | True- = putStrLn $ " Note: Original value of " ++ show v ++ " was rounded to " ++ show t ++ "."-- exact = putStrLn $ " Note: Conversion from " ++ show inp ++ " was exact. No rounding happened."+{-# LANGUAGE TupleSections #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Main(main) where++import Data.Char (isDigit, isSpace)+import Data.Maybe (fromMaybe)++import qualified Control.Exception as C++import System.Environment (getArgs, getProgName, withArgs)+import System.Console.GetOpt (ArgOrder(Permute), getOpt)+import System.Exit (exitFailure)++import Data.SBV (SBVException)++import Data.Version (showVersion)+import Paths_crackNum (version)++import CrackNum.Types+import CrackNum.Formats (fpFormatNames)+import CrackNum.Options (pgmOptions, helpStr, usage)+import CrackNum.Utils (copyRight, die)+import CrackNum.GUI (launchGUI)+import CrackNum.Decode (decodeAllLanes)+import CrackNum.Encode (encodeLane)++import CrackNum.TestSuite++-- | main entry point to crackNum+main :: IO ()+main = do argv <- getArgs+ pn <- getProgName++ let rt = "--runTests"++ if rt `elem` argv+ then withArgs (filter (`notElem` [rt, "--"]) argv) runTests+ else crack pn argv++-- | main entry point to crackNum+crack :: String -> [String] -> IO ()+crack pn argv = case getOpt Permute pgmOptions argv of+ (_, _, errs@(_:_)) -> die $ errs ++ lines (helpStr pn)+ (os, rs, [])+ | Version `elem` os -> putStrLn $ pn ++ " v" ++ showVersion version ++ ", " ++ copyRight+ -- NB. Machine readable, one name per line: this is what the editor+ -- integrations use so they need not hardcode the list of formats.+ | Formats `elem` os -> mapM_ putStrLn fpFormatNames+ | Help `elem` os -> usage pn+ -- NB. Check for bad flags before launching: otherwise a typo like+ -- "-ft32" would silently bring the GUI up with nothing selected.+ | GUI `elem` os -> case [b | BadFlag b <- os] of+ (e:_) -> die e+ [] -> launchGUI (filter (/= "--gui") argv)+ | True -> do let rm = case reverse [r | RMode r <- os] of+ (r:_) -> r+ _ -> RNE++ (tryInfer, lanesGiven) = case reverse [l | Lanes l <- os] of+ (l:_) -> (False, l)+ _ -> (True, 1)++ arg = dropWhile isSpace $ unwords rs++ 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)+ (_, [Floating s]) -> pure (SFloat s, fpSize s)+ _ -> do usage pn+ exitFailure++ let inferLanes :: Int -> IO (Maybe Int)+ inferLanes prefix+ | prefix `rem` eSize == 0 = pure $ Just (prefix `div` eSize)+ | True = die [ "Verilog notation size mismatch:"+ , " Input length: " ++ show prefix+ , " Element size: " ++ show eSize+ , "Length must be an exact multiple of the element size."+ ]++ (decode, isVerilog, lanesInferred) <-+ case arg of+ '0':'x':r -> if any (`elem` ".p") r+ then pure (False, False, Nothing)+ else pure (True, False, Nothing)+ '0':'b':_ -> pure (True, False, Nothing)+ _ -> case break (`elem` "'h") arg of+ (pre@(_:_), '\'':'h':_)+ | all isDigit pre -> (True, True, ) <$> inferLanes (read pre)+ _ -> pure (False, False, Nothing)++ let lanes+ | tryInfer = fromMaybe lanesGiven lanesInferred+ | True = lanesGiven++ let act | decode = decodeAllLanes isVerilog debug lanes kind arg+ | True = encodeLane debug lanes kind rm arg++ act `C.catch` solverLimitation kind++-- | We accept exponent/significand sizes down to 1 bit, but SMTLib's FloatingPoint+-- sort (and hence z3) requires at least 2 of each. Rather than letting such a format+-- surface as a raw solver exception with a backtrace, report it as a plain error.+-- Anything else is re-thrown untouched.+solverLimitation :: NKind -> SBVException -> IO a+solverLimitation kind e = case kind of+ SFloat (FP eb sb) | eb < 2 || sb < 2 -> die [ "The solver does not support this format:"+ , " " ++ plural eb "exponent bit" ++ ", " ++ plural sb "significand bit"+ , "z3 requires at least 2 of each."+ ]+ _ -> C.throwIO e+ where plural :: Int -> String -> String+ plural 1 what = "1 " ++ what+ plural n what = show n ++ " " ++ what ++ "s"
+ src/CrackNum/Options.hs view
@@ -0,0 +1,130 @@+---------------------------------------------------------------------------+-- |+-- Module : CrackNum.Options+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Command-line options, and the help text+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall -Werror #-}++module CrackNum.Options(+ getSize, getRM, pgmOptions, helpStr, usage+ ) where++import Data.Char (toLower)+import Text.Read (readMaybe)++import System.Console.GetOpt (ArgDescr(..), OptDescr(..), usageInfo)++import CrackNum.Types+import CrackNum.Formats++-- | Given an integer flag value, turn it into a flag+getSize :: String -> (Int -> Flag) -> String -> Flag+getSize flg f n = case readMaybe n of+ Just i | i > 0 -> f i+ | True -> BadFlag ["Option " ++ show flg ++ " requires an integer >= 1. Received: " ++ show n]+ Nothing -> BadFlag ["Option " ++ show flg ++ " requires an integer argument. Received: " ++ show n]++getRM :: String -> Flag+getRM "rne" = RMode RNE+getRM "rna" = RMode RNA+getRM "rtp" = RMode RTP+getRM "rtn" = RMode RTN+getRM "rtz" = RMode RTZ+getRM m = BadFlag $ [ "Invalid rounding mode."+ , ""+ , " Must be one of:"+ ]+ ++ [ " " ++ show r | r <- [minBound .. maxBound::RM]]+ ++ [ ""+ , "Received: " ++ m+ ]++-- | Options we accept+pgmOptions :: [OptDescr Flag]+pgmOptions = [+ Option "i" [] (ReqArg (getSize "-i" Signed) "N" ) "Signed integer of N-bits"+ , Option "w" [] (ReqArg (getSize "-w" Unsigned) "N" ) "Unsigned integer of N-bits"+ , Option "f" [] (ReqArg getFP "fp") "Floating point format fp"+ , Option "r" [] (ReqArg (getRM . map toLower) "rm") "Rounding mode to use. If not given, Nearest-ties-to-Even."+ , 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"+ , Option "" ["gui"] (NoArg GUI) "launch the graphical interface"+ , Option "" ["list-formats"] (NoArg Formats) "list the formats supported by -f, one per line"+ ]++-- | Help info+helpStr :: String -> String+helpStr pn = usageInfo ("Usage: " ++ pn ++ " value OR binary/hex-pattern") pgmOptions++-- | Print usage info and examples.+usage :: String -> IO ()+usage pn = putStr $ unlines $ [ helpStr pn+ , "Supported floating-point formats (for use with -f):"+ , ""+ ]+ ++ map (" " ++) fpFormatsHelp+ ++ [ ""+ , "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 ++ " -ftf32 2.5 -- encode as a TensorFloat-32 float"+ , " " ++ pn ++ " -fdp 2.5 -- encode as a double-precision float"+ , " " ++ pn ++ " -fqp 2.5 -- encode as a quad-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 ++ " -ffp4e0m3 3.5 -- encode as an FP4 (E0M3) sign-magnitude integer"+ , " " ++ pn ++ " -fe8m0 2.5 -- encode as an E8M0 MX scale (power of two)"+ , " " ++ pn ++ " -fsp 0x3.2p5 -- encode as single-precision from hex-float"+ , ""+ , " Decoding:"+ , " " ++ pn ++ " -i4 0b0110 -- decode as 4-bit signed integer, from binary"+ , " " ++ pn ++ " -w4 0xE -- decode as 4-bit unsigned integer, from hex"+ , " " ++ pn ++ " -f3+4 0b0111001 -- decode as float with 3 bits exponent, 4 bits significand"+ , " " ++ pn ++ " -fbp 0x000F -- decode as a brain-precision float"+ , " " ++ pn ++ " -ftf32 19\\'h0000F -- decode as a TensorFloat-32 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 ++ " -ffp4e0m3 0b1101 -- decode as an FP4 (E0M3) sign-magnitude integer"+ , " " ++ pn ++ " -fe8m0 0x7F -- decode as an E8M0 MX scale (power of two)"+ , " " ++ pn ++ " -l4 -fhp 64\\'hbdffaaffdc71fc60 -- decode as half-precision float over 4 lanes using verilog notation"+ , ""+ , " GUI:"+ , " " ++ pn ++ " --gui -- launch the graphical interface"+ , " " ++ pn ++ " --gui 0xdeadbeef -- launch the GUI, pre-filled with the given value"+ , " " ++ pn ++ " --gui -fsp 0xdeadbeef -- launch the GUI, using the given format"+ , ""+ , " Notes:"+ , " - For encoding:"+ , " - 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."+ , " - FP4 (E0M3) is a sign-magnitude integer: a sign bit and a 3-bit magnitude,"+ , " covering -7 to 7, with both a positive and a negative zero. It has no NaN"+ , " and no Inf either, and values outside [-7, 7] saturate to the end-point."+ , " - E8M0 (MX scale) is all exponent: no sign bit and no significand at all,"+ , " so every value is a power of two, from 2^-127 to 2^127. It has no zero"+ , " and no Inf, and 0xFF is its only NaN. Negative inputs are rejected;"+ , " values outside the range 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."+ , " - You can use _,- or space as a digit to improve readability for the pattern to be decoded"+ , " - With -lN parameter, you can decode multiple lanes of data."+ , " - If you use verilog input format, then we will infer the number of lanes unless you provide it."+ ]
+ src/CrackNum/Output.hs view
@@ -0,0 +1,188 @@+---------------------------------------------------------------------------+-- |+-- Module : CrackNum.Output+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Massaging the output, and laying out the formats that have no IEEE look-alike+-----------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module CrackNum.Output(+ retype, printAs, modOut, isClassification, dropNaNUniquenessNote, canonicalNaN,+ ExtraE3M4(..), toD, inBases, fp4e0m3Layout, e8m0Bias, e8m0Value, e8m0Layout+ ) where++import Data.Char (intToDigit, toUpper)+import Data.List (intercalate, isInfixOf)++import Numeric (showIntAtBase)++import Data.SBV+import qualified Data.SBV as SBV++import CrackNum.Types++-- 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 ++ ":: " ++ show fmt+ | True+ = s+retype _ res = show res++-- Print a model for one of the non-IEEE formats: the look-alike does all the work,+-- we merely fix the type name it prints.+printAs :: FP -> SatResult -> IO ()+printAs fmt = putStrLn . retype fmt++-- 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)++ 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 . fixVal) $ takeWhile (not . isClassification) (lines (show ieeeResult))+ mapM_ putStrLn $ dropWhile (not . isClassification) (lines modifiedResult)++-- | The line SBV's cracker prints the classification on. Everything from here down+-- describes the value itself rather than its layout, which is the split the formats+-- that deviate from IEEE need: they take the layout from the look-alike (or lay it+-- out by hand) and the rest from the value they actually mean.+isClassification :: String -> Bool+isClassification = ("Classification:" `isInfixOf`)++-- | SBV notes that a NaN's representation is not unique. That holds for IEEE formats,+-- but not for the ones here that have exactly one NaN pattern (E4M3 and E8M0), so drop+-- the note for those rather than claim an ambiguity the format does not have.+dropNaNUniquenessNote :: [String] -> [String]+dropNaNUniquenessNote = filter (not . ("Representation for NaN's is not unique" `isInfixOf`))++-- | The canonical quiet-NaN pattern for a float with @eb@ exponent bits and @sb@+-- significand bits (including the implicit one): sign 0, all-ones exponent, and only+-- the leading stored significand bit set. For single-precision this is 0x7FC00000.+canonicalNaN :: Int -> Int -> Integer+canonicalNaN eb sb = (2 ^ eb - 1) * 2 ^ (sb - 1) + 2 ^ (sb - 2)++-- 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")++-- FP4E0M3 is a 4-bit sign-magnitude integer: a sign bit and a 3-bit magnitude, covering+-- -7 to 7, with both a positive and a negative zero. Having no exponent at all, it has no+-- IEEE look-alike we could lean on, so we lay the bits out by hand; the shape follows what+-- crackNum prints for the plain integer formats, which is what this format really is.+fp4e0m3Layout :: String -> Bool -> Int -> [String]+fp4e0m3Layout tag isNeg mag =+ [ "Satisfiable. Model:"+ , " " ++ tag ++ " = " ++ sign ++ show mag ++ " :: " ++ show FP4E0M3+ , " 3 210"+ , " S -M-"+ , " Binary layout: " ++ (if isNeg then '1' else '0') : ' ' : pad 3 (inBase 2 mag)+ , " Hex layout: " ++ map toUpper (inBase 16 ((if isNeg then 8 else 0) + mag))+ , " Type: 4-bit sign-magnitude integer"+ , " Sign: " ++ (if isNeg then "Negative" else "Positive")+ , " Binary: " ++ sign ++ "0b" ++ inBase 2 mag+ , " Octal: " ++ sign ++ "0o" ++ inBase 8 mag+ , " Decimal: " ++ sign ++ show mag+ , " Hex: " ++ sign ++ "0x" ++ inBase 16 mag+ ]+ where sign = if isNeg then "-" else ""++ inBase b v = showIntAtBase b intToDigit v ""++ pad n s = replicate (n - length s) '0' ++ s++-- | E8M0 is the OCP Microscaling (MX) scale format: the value that scales a block of+-- MXFP8/MXFP6/MXFP4 elements. All 8 bits are exponent -- there is no sign bit and no+-- significand at all -- so every value is the power of two 2^(E-127), and 0xFF is its+-- one and only NaN. Having no significand, it has no zero and no subnormals either:+-- with nothing for the E=0 encoding to mean, it simply denotes 2^-127.+e8m0Bias :: Int+e8m0Bias = 127++-- | The value a stored E8M0 exponent denotes. All 254 finite values are exactly+-- representable as a Double, since 2^(+/-127) is nowhere near its range limits; note+-- that 'encodeFloat' builds them exactly, which @2 **@ would not be guaranteed to do.+e8m0Value :: Int -> Double+e8m0Value 255 = 0/0+e8m0Value e = encodeFloat 1 (e - e8m0Bias)++-- | Lay out an E8M0 value. With no sign and no significand there is no IEEE look-alike+-- to lean on, so the layout is built by hand, following the shape crackNum prints for+-- the other formats. Everything from the classification down describes the value rather+-- than its layout, so that part comes from cracking the equivalent Double -- the same+-- division of labor 'modOut' uses for the E4M3 and FP4 deviations.+e8m0Layout :: Bool -> String -> Int -> [String]+e8m0Layout debug tag stored =+ [ "Satisfiable. Model:"+ , " " ++ tag ++ " = " ++ show v ++ " :: " ++ show E8M0+ , " 76543210"+ , " ---E8---"+ , " Binary layout: " ++ pad 8 (inBase 2 stored)+ , " Hex layout: " ++ map toUpper (pad 2 (inBase 16 stored))+ , " Precision: 8 exponent bits, no significand"+ -- NB. There is no sign bit: bit 7 is the exponent's MSB. We print the line anyway,+ -- so the block keeps the same shape as every other format, but say outright that+ -- it can never read anything else.+ , " Sign: Positive (always)"+ , " Exponent: " ++ show (stored - e8m0Bias) ++ " (Stored: " ++ show stored ++ ", Bias: " ++ show e8m0Bias ++ ")"+ ]+ ++ dropNaNUniquenessNote (dropWhile (not . isClassification) (lines (SBV.crack debug (literal v :: SDouble))))+ where v = e8m0Value stored++ inBase b x = showIntAtBase b intToDigit x ""++ pad n x = replicate (n - length x) '0' ++ x
+ src/CrackNum/Types.hs view
@@ -0,0 +1,114 @@+---------------------------------------------------------------------------+-- |+-- Module : CrackNum.Types+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Core types: the formats, kinds, and rounding modes we understand+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall -Werror #-}++module CrackNum.Types(+ FP(..), fpSize, NKind(..), kSize, RM(..), toLibBFRM, toSBVRM, Flag(..), isRMode, isLanes, isDebug+ ) where++-- NB. LibBF's rounding modes (NearEven etc.) are pattern synonyms rather than+-- constructors, so RoundMode(..) does not bring them into scope; import wholesale.+import LibBF+import Data.SBV (SRoundingMode, sRNE, sRNA, sRTP, sRTN, sRTZ)++-- | Various precisions we support+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+ | FP4 -- NVIDIA FP4 (E2M1) format with no infinities and no NaNs+ | FP4E0M3 -- 4-bit sign-magnitude integer format; no exponent at all+ | E8M0 -- OCP MX scale format; no sign and no significand at all+ deriving (Show, Eq)++-- | How many bits does this float occupy+fpSize :: FP -> Int+fpSize SP = 32+fpSize DP = 64+fpSize (FP i j) = i+j+fpSize E5M2 = 8+fpSize E4M3 = 8+fpSize FP4 = 4+fpSize FP4E0M3 = 4+fpSize E8M0 = 8++-- | Kinds of numbers we understand+data NKind = SInt Int -- ^ Signed integer of n bits+ | SWord Int -- ^ Unsigned integer of n bits+ | SFloat FP -- ^ Floating point with precision++kSize :: NKind -> Int+kSize (SInt i) = i+kSize (SWord i) = i+kSize (SFloat f) = fpSize f++-- | Rounding modes we support+data RM = RNE -- ^ Round nearest ties to even+ | RNA -- ^ Round nearest ties to away+ | RTP -- ^ Round towards positive infinity+ | RTN -- ^ Round towards negative infinity+ | RTZ -- ^ Round towards zero+ deriving (Eq, Enum, Bounded)++-- | Show instance for RM, for descriptive purposes+instance Show RM where+ show RNE = "RNE: Round nearest ties to even."+ show RNA = "RNA: Round nearest ties to away."+ show RTP = "RTP: Round towards positive infinity."+ show RTN = "RTN: Round towards negative infinity."+ show RTZ = "RTZ: Round towards zero."++-- Convert to LibBF rounding mode+toLibBFRM :: RM -> RoundMode+toLibBFRM RNE = NearEven+toLibBFRM RNA = NearAway+toLibBFRM RTP = ToPosInf+toLibBFRM RTN = ToNegInf+toLibBFRM RTZ = ToZero++-- Convert to SBV rounding mode+toSBVRM :: RM -> SRoundingMode+toSBVRM RNE = sRNE+toSBVRM RNA = sRNA+toSBVRM RTP = sRTP+toSBVRM RTN = sRTN+toSBVRM RTZ = sRTZ++-- | Options accepted by the executable+data Flag = Signed Int -- ^ Crack as a signed word with the given number of bits+ | Unsigned Int -- ^ Crack as an unsigned word with the given number of bits+ | Floating FP -- ^ Crack as the corresponding floating-point type+ | RMode RM -- ^ Rounding mode to use+ | Lanes Int -- ^ How many lanes to decode?+ | BadFlag [String] -- ^ Bad input+ | Version -- ^ Version+ | Debug -- ^ Run in debug mode. Debugging only.+ | GUI -- ^ Launch the graphical interface+ | Formats -- ^ List the floating-point formats we support+ | Help -- ^ Show help+ deriving (Show, Eq)++-- | Is this a rounding flag?+isRMode :: Flag -> Bool+isRMode RMode{} = True+isRMode _ = False++-- | Is this lanes flag+isLanes :: Flag -> Bool+isLanes Lanes{} = True+isLanes _ = False++-- | Is this the debug flag?+isDebug :: Flag -> Bool+isDebug Debug{} = True+isDebug _ = False
+ src/CrackNum/Utils.hs view
@@ -0,0 +1,95 @@+---------------------------------------------------------------------------+-- |+-- Module : CrackNum.Utils+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Small helpers: dying, parsing bit-patterns, and input fixups+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall -Werror #-}++module CrackNum.Utils(+ copyRight, die, parseToBits, fixup, unrecognized+ ) where++import Data.Char (isDigit, isSpace, toLower)+import Data.List (unfoldr)++import Numeric (readHex)++import System.Exit (exitFailure)+import System.IO (hPutStr, stderr)++-- | Copyright info+copyRight :: String+copyRight = "(c) Levent Erkok. Released with a BSD3 license."++-- | Terminate early+die :: [String] -> IO a+die xs = do hPutStr stderr $ unlines $ "ERROR:" : map (" " ++) xs+ exitFailure++parseToBits :: String -> IO [Bool]+parseToBits inp = do+ let isSkippable c = c `elem` "_-" || isSpace c++ cleanInput = map toLower (filter (not . isSkippable) inp)++ (mbPadTo, isHex, stream) <- case cleanInput of+ '0':'x':rest -> pure (Nothing, True, rest)+ '0':'b':rest -> pure (Nothing, False, rest)+ _ ->+ case break (`elem` "'h") cleanInput of+ (pre@(_:_), '\'' : 'h' : rest) | all isDigit pre -> pure (Just (read pre), True, rest)+ _ -> die [ "Input string must start with 0b, 0x, or N'h for decoding."+ , "Received prefix: " ++ show (take 2 cleanInput)+ ]++ let cvtBin '1' = pure [True]+ cvtBin '0' = pure [False]+ cvtBin c = die ["Input has a non-binary digit: " ++ show c]++ cvtHex c = case readHex [c] of+ [(v, "")] -> pure $ pad+ $ map (== (1::Int))+ $ reverse+ $ unfoldr (\x -> if x == 0 then Nothing else Just (x `rem` 2, x `div` 2)) v+ _ -> die ["Input has a non-hexadecimal digit: " ++ show c]+ where pad p = replicate (4 - length p) False ++ p++ cvt i | isHex = concat <$> mapM cvtHex i+ | True = concat <$> mapM cvtBin i++ res <- cvt stream++ let pad = case mbPadTo of+ Nothing -> []+ Just n -> replicate (n - length res) False++ pure $ pad ++ res++-- | 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+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."+ ]