diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,20 +1,35 @@ * Hackage: * GitHub: -* Latest Hackage released version: 3.6, 2024-01-24 +* Latest Hackage released version: 3.7, 2024-02-15 +### Version 3.7, 2024-02-15 + + * Support signaling/quiet indication for decoded NaN values. + + * Add support for decoding over multiple lanes. See the -l option. + + * Add support for verilog bit-vector notation, e.g., 128'hXXX. If + you use this notation, crackNum will automatically infer the + number of lanes to crack based on the width given; unless + explicitly specified. + ### Version 3.6, 2024-01-24 + * Be more clear when the provided input isn't a recognizable float, instead of treating it as NaN implicitly. Thanks to Dmitry Blotsky for pointing out the confusion. ### Version 3.5, 2024-01-11 + * Resolve compilation issues with GHC 9.8 series ### Version 3.4, 2023-04-14 + * Fix compilation in previous build ### Version 3.3, 2023-04-14 + * Allow compilation with newer versions of SBV ### Version 3.2, 2021-06-30 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -80,39 +80,80 @@ Hex: 0xc ``` +### Example: Decode two half-precision floats in two lanes +``` +$ crackNum -l2 -fhp 32\'hfdc71fc6 +== Lane 1 ============================================================ +Satisfiable. Model: + DECODED = NaN :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 1 11111 0111000111 + Hex layout: FDC7 + Precision: Half (5 exponent bits, 10 significand bits.) + Sign: Negative + Exponent: 16 (Stored: 31, Bias: 15) + Classification: FP_NAN (Signaling) + Value: NaN + Note: Representation for NaN's is not unique +== Lane 0 ============================================================ +Satisfiable. Model: + DECODED = 0.0075912 :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 0 00111 1111000110 + Hex layout: 1FC6 + Precision: Half (5 exponent bits, 10 significand bits.) + Sign: Positive + Exponent: -8 (Stored: 7, Bias: 15) + Classification: FP_NORMAL + Binary: 0b1.111100011p-8 + Octal: 0o3.706p-9 + Decimal: 0.0075912 + Hex: 0x1.f18p-8 +``` + ### Usage info ``` Usage: crackNum value OR binary/hex-pattern - -i N Signed integer of N-bits - -w N Unsigned integer of N-bits - -f fp Floating point format fp - -r rm Rounding mode to use. If not given, Nearest-ties-to-Even. - -h, -? --help print help, with examples - -v --version print version info + -i N Signed integer of N-bits + -w N Unsigned integer of N-bits + -f fp Floating point format fp + -r rm Rounding mode to use. If not given, Nearest-ties-to-Even. + -l lanes Number of lanes to decode + -h, -? --help print help, with examples + -v --version print version info Examples: Encoding: - crackNum -i4 -- -2 -- encode as 4-bit signed integer - crackNum -w4 2 -- encode as 4-bit unsigned integer - crackNum -f3+4 2.5 -- encode as float with 3 bits exponent, 4 bits significand - crackNum -f3+4 2.5 -rRTZ -- encode as above, but use RTZ rounding mode. - crackNum -fbp 2.5 -- encode as a brain-precision float - crackNum -fdp 2.5 -- encode as a double-precision float + crackNum -i4 -- -2 -- encode as 4-bit signed integer + crackNum -w4 2 -- encode as 4-bit unsigned integer + crackNum -f3+4 2.5 -- encode as float with 3 bits exponent, 4 bits significand + crackNum -f3+4 2.5 -rRTZ -- encode as above, but use RTZ rounding mode. + crackNum -fbp 2.5 -- encode as a brain-precision float + crackNum -fdp 2.5 -- encode as a double-precision float Decoding: - crackNum -i4 0b0110 -- decode as 4-bit signed integer, from binary - crackNum -w4 0xE -- decode as 4-bit unsigned integer, from hex - crackNum -f3+4 0b0111001 -- decode as float with 3 bits exponent, 4 bits significand - crackNum -fbp 0x000F -- decode as a brain-precision float - crackNum -fdp 0x8000000000000000 -- decode as a double-precision float + crackNum -i4 0b0110 -- decode as 4-bit signed integer, from binary + crackNum -w4 0xE -- decode as 4-bit unsigned integer, from hex + crackNum -f3+4 0b0111001 -- decode as float with 3 bits exponent, 4 bits significand + crackNum -fbp 0x000F -- decode as a brain-precision float + crackNum -fdp 0x8000000000000000 -- decode as a double-precision float + crackNum -fhp 0x8000000000000000 -- decode as a double-precision float + crackNum -l4 -fhp 64\'hbdffaaffdc71fc60 -- decode as half-precision float over 4 lanes using verilog notation 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 float. - For decoding: - - Use hexadecimal (0x) or binary (0b) as input. Input must have one of these prefixes. + - 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. ``` VIM users: You can use the http://github.com/LeventErkok/crackNum/blob/master/crackNum.vim file to 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.6 +Version : 3.7 Synopsis : Crack various integer and floating-point data formats Description : Crack IEEE-754 float formats and arbitrary sized words and integers, showing the layout. . @@ -26,7 +26,7 @@ default-language: Haskell2010 hs-source-dirs : src ghc-options : -Wall -Wunused-packages - build-depends : base >= 4.11 && < 5, libBF, sbv >= 10.3 + build-depends : base >= 4.11 && < 5, libBF, sbv >= 10.4 , tasty, tasty-golden, filepath, directory, process other-modules : Paths_crackNum, CrackNum.TestSuite autogen-modules : Paths_crackNum diff --git a/src/CrackNum/Main.hs b/src/CrackNum/Main.hs --- a/src/CrackNum/Main.hs +++ b/src/CrackNum/Main.hs @@ -11,20 +11,21 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wall -Werror #-} module Main(main) where -import System.Environment (getArgs, getProgName, withArgs) -import Data.Char (isDigit, isSpace, toLower) -import Data.List (isPrefixOf, isSuffixOf, unfoldr) - +import Control.Monad (when) +import Data.Char (isDigit, isSpace, toLower) +import Data.List (isPrefixOf, isSuffixOf, unfoldr) +import Data.Maybe (fromMaybe) +import Text.Read (readMaybe) +import System.Environment (getArgs, getProgName, withArgs) import System.Console.GetOpt (ArgOrder(Permute), getOpt, ArgDescr(..), OptDescr(..), usageInfo) import System.Exit (exitFailure) -import Text.Read (readMaybe) - -import System.IO (hPutStr, stderr) +import System.IO (hPutStr, stderr) import LibBF import Numeric @@ -84,6 +85,7 @@ | 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 | Help -- ^ Show help @@ -94,6 +96,11 @@ isRMode RMode{} = True isRMode _ = False +-- | Is this lanes flag +isLanes :: Flag -> Bool +isLanes Lanes{} = True +isLanes _ = 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 @@ -169,12 +176,13 @@ -- | 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 "h?" ["help"] (NoArg Help) "print help, with examples" - , Option "v" ["version"] (NoArg Version) "print version info" + 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" ] -- | Help info @@ -186,27 +194,32 @@ usage pn = putStr $ unlines [ helpStr pn , "Examples:" , " Encoding:" - , " " ++ pn ++ " -i4 -- -2 -- encode as 4-bit signed integer" - , " " ++ pn ++ " -w4 2 -- encode as 4-bit unsigned integer" - , " " ++ pn ++ " -f3+4 2.5 -- encode as float with 3 bits exponent, 4 bits significand" - , " " ++ pn ++ " -f3+4 2.5 -rRTZ -- encode as above, but use RTZ rounding mode." - , " " ++ pn ++ " -fbp 2.5 -- encode as a brain-precision float" - , " " ++ pn ++ " -fdp 2.5 -- encode as a double-precision float" + , " " ++ pn ++ " -i4 -- -2 -- encode as 4-bit signed integer" + , " " ++ pn ++ " -w4 2 -- encode as 4-bit unsigned integer" + , " " ++ pn ++ " -f3+4 2.5 -- encode as float with 3 bits exponent, 4 bits significand" + , " " ++ pn ++ " -f3+4 2.5 -rRTZ -- encode as above, but use RTZ rounding mode." + , " " ++ pn ++ " -fbp 2.5 -- encode as a brain-precision float" + , " " ++ pn ++ " -fdp 2.5 -- encode as a double-precision float" , "" , " 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 ++ " -fdp 0x8000000000000000 -- decode as a double-precision float" + , " " ++ 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 ++ " -fdp 0x8000000000000000 -- decode as a double-precision float" + , " " ++ pn ++ " -fhp 0x8000000000000000 -- decode as a double-precision float" + , " " ++ pn ++ " -l4 -fhp 64\\'hbdffaaffdc71fc60 -- decode as half-precision float over 4 lanes using verilog notation" , "" , " 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 float." , " - For decoding:" - , " - Use hexadecimal (0x) or binary (0b) as input. Input must have one of these prefixes." + , " - 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 @@ -225,15 +238,74 @@ (r:_) -> r _ -> RNE + (tryInfer, lanesGiven) = case reverse [l | Lanes l <- os] of + (l:_) -> (False, l) + _ -> (True, 1) + arg = dropWhile isSpace $ unwords rs - case ([b | BadFlag b <- os], filter (not . isRMode) os) of - (e:_, _) -> die e - (_, [Signed n]) -> process (SInt n) rm arg - (_, [Unsigned n]) -> process (SWord n) rm arg - (_, [Floating s]) -> process (SFloat s) rm arg - _ -> usage pn + (kind, eSize) <- case ([b | BadFlag b <- os], filter (\o -> not (isRMode o || isLanes 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, lanesInferred) <- case arg of + '0':'x':_ -> pure (True, Nothing) + '0':'b':_ -> pure (True, Nothing) + _ -> case break (`elem` "'h") arg of + (pre@(_:_), '\'':'h':_) + | all isDigit pre -> (True,) <$> inferLanes (read pre) + _ -> pure (False, Nothing) + + let lanes + | tryInfer = fromMaybe lanesGiven lanesInferred + | True = lanesGiven + + if decode + then decodeAllLanes lanes kind arg + else encodeLane lanes kind rm arg + +decodeAllLanes :: Int -> NKind -> String -> IO () +decodeAllLanes lanes kind arg = do + when (lanes < 0) $ die + ["Number of lanes must be non-negative. Got: " ++ show lanes] + + bits <- parseToBits arg + + 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 (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 @@ -250,48 +322,61 @@ then withArgs (filter (`notElem` [rt, "--"]) argv) runTests else crack pn argv --- | Perform the encoding/decoding -process :: NKind -> RM -> String -> IO () -process num rm inp = case num of - SInt n -> print =<< (if decode then di else ei) True n - SWord n -> print =<< (if decode then di else ei) False n - SFloat s -> (if decode then df else ef) s - where decode = any (`isPrefixOf` inp) ["0x", "0b"] +parseToBits :: String -> IO [Bool] +parseToBits inp = do + let isSkippable c = c `elem` "_-" || isSpace c - bitString n = do let isSkippable c = c `elem` "_-" || isSpace c + (mbPadTo, isHex, stream) <- case map toLower (filter (not . isSkippable) inp) of + '0':'x':rest -> pure (Nothing, True, rest) + '0':'b':rest -> pure (Nothing, False, rest) + _ -> + case break (`elem` "'h") inp 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 inp) + ] - (isHex, stream) <- case map toLower (filter (not . isSkippable) inp) of - '0':'x':rest -> pure (True, rest) - '0':'b':rest -> pure (False, rest) - _ -> die [ "Input string must start with 0b or 0x for decoding." - , "Received prefix: " ++ show (take 2 inp) - ] + let cvtBin '1' = pure [True] + cvtBin '0' = pure [False] + cvtBin c = die ["Input has a non-binary digit: " ++ show c] - 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 - 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 - cvt i | isHex = concat <$> mapM cvtHex i - | True = concat <$> mapM cvtBin i + res <- cvt stream - encoded <- cvt stream + let pad = case mbPadTo of + Nothing -> [] + Just n -> replicate (n - length res) False - let bits 1 = "one bit" + pure $ pad ++ res + +-- | Decoding +decodeLane :: Maybe Int -> [Bool] -> NKind -> IO () +decodeLane mbLane inputBits kind = case kind of + SInt n -> print =<< di True n + SWord n -> print =<< di False n + SFloat s -> df s + where bitString n = do let bits 1 = "one bit" bits b = show b ++ " bits" - case length encoded `compare` n of - EQ -> pure encoded - LT -> die ["Input needs to be " ++ show n ++ " bits wide, it's too short by " ++ bits (n - length encoded)] - GT -> die ["Input needs to be " ++ show n ++ " bits wide, it's too long by " ++ bits (length encoded - n)] + 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 satWith z3{crackNum=True} $ p bs @@ -299,22 +384,21 @@ p bs = do x <- (if sgn then sIntN else sWordN) n "DECODED" mapM_ constrain $ zipWith (.==) (map SBV (svBlastBE x)) (map literal bs) - ei :: Bool -> Int -> IO SatResult - ei sgn n = case reads inp of - [(v :: Integer, "")] -> satWith z3{crackNum=True} $ 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 = SBV $ SVal k $ Left $ mkConstCV k iv - x <- (if sgn then sIntN else sWordN) n "ENCODED" - pure $ SBV x .== v - df :: FP -> IO () - df fp = do bs <- map literal <$> bitString (fpSize fp) + 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)))] + } + case fp of - SP -> print =<< satWith z3{crackNum=True} (dFloat bs) - DP -> print =<< satWith z3{crackNum=True} (dDouble bs) - FP i j -> print =<< satWith z3{crackNum=True} (dFP i j bs) + SP -> print =<< satWith config (dFloat bs) + DP -> print =<< satWith config (dDouble bs) + FP i j -> print =<< satWith config (dFP i j bs) dFloat :: [SBool] -> ConstraintSet dFloat bs = do x <- sFloat "DECODED" @@ -331,6 +415,28 @@ let bits = svBlastBE sx mapM_ constrain $ zipWith (.==) (map SBV bits) bs +-- | Encoding +encodeLane :: Int -> NKind -> RM -> String -> IO () +encodeLane 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 + where ei :: Bool -> Int -> IO SatResult + ei sgn n = case reads inp of + [(v :: Integer, "")] -> satWith z3{crackNum=True} $ 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 = SBV $ SVal k $ Left $ mkConstCV k iv + x <- (if sgn then sIntN else sWordN) n "ENCODED" + pure $ SBV x .== v + convert :: Int -> Int -> (BigFloat, Maybe String) convert i j = case s of Ok -> (v, Nothing) @@ -368,7 +474,7 @@ then die [ "Input does not represent floating point number we recognize." , "Saw: " ++ inp , "" - , "For decoding bit-strings, prefix them with 0x or 0b, and" + , "For decoding bit-strings, prefix them with 0x, N'h, 0b and" , "provide a hexadecimal or binary representation of the input." ] else do print =<< satWith z3{crackNum=True} (p v) diff --git a/src/CrackNum/TestSuite.hs b/src/CrackNum/TestSuite.hs --- a/src/CrackNum/TestSuite.hs +++ b/src/CrackNum/TestSuite.hs @@ -63,6 +63,8 @@ , gold "decode2" ["-f3+4", "0b0111001"] , gold "decode3" ["-fbp", "0x000F"] , gold "decode4" ["-fdp", "0x8000000000000000"] + , gold "decode5" ["-fhp", "0x7c01"] + , gold "decode6" ["-fhp", "-l8", "128'hffffffffffffffffbdffaaffdc71fc60"] ] , testGroup "Bad" [ gold "badInvocation0" ["-f3+4", "0b01"]