diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,41 @@ * Hackage: * GitHub: -* 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 diff --git a/GUI/tclGUI/crackNum.tcl b/GUI/tclGUI/crackNum.tcl --- a/GUI/tclGUI/crackNum.tcl +++ b/GUI/tclGUI/crackNum.tcl @@ -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 <> { - set sel [.main.side.lb selection] +bind .main.side.fmts.lb <> { + 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 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: diff --git a/crackNum.cabal b/crackNum.cabal --- a/crackNum.cabal +++ b/crackNum.cabal @@ -1,6 +1,6 @@ Cabal-version : 2.2 Name : crackNum -Version : 3.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 diff --git a/src/CrackNum/Decode.hs b/src/CrackNum/Decode.hs new file mode 100644 --- /dev/null +++ b/src/CrackNum/Decode.hs @@ -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 diff --git a/src/CrackNum/Encode.hs b/src/CrackNum/Encode.hs new file mode 100644 --- /dev/null +++ b/src/CrackNum/Encode.hs @@ -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." diff --git a/src/CrackNum/Formats.hs b/src/CrackNum/Formats.hs new file mode 100644 --- /dev/null +++ b/src/CrackNum/Formats.hs @@ -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 + ] diff --git a/src/CrackNum/GUI.hs b/src/CrackNum/GUI.hs new file mode 100644 --- /dev/null +++ b/src/CrackNum/GUI.hs @@ -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." + ] diff --git a/src/CrackNum/Main.hs b/src/CrackNum/Main.hs --- a/src/CrackNum/Main.hs +++ b/src/CrackNum/Main.hs @@ -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" diff --git a/src/CrackNum/Options.hs b/src/CrackNum/Options.hs new file mode 100644 --- /dev/null +++ b/src/CrackNum/Options.hs @@ -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." + ] diff --git a/src/CrackNum/Output.hs b/src/CrackNum/Output.hs new file mode 100644 --- /dev/null +++ b/src/CrackNum/Output.hs @@ -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 diff --git a/src/CrackNum/Types.hs b/src/CrackNum/Types.hs new file mode 100644 --- /dev/null +++ b/src/CrackNum/Types.hs @@ -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 diff --git a/src/CrackNum/Utils.hs b/src/CrackNum/Utils.hs new file mode 100644 --- /dev/null +++ b/src/CrackNum/Utils.hs @@ -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." + ]