crackNum 3.6 → 3.7
raw patch · 5 files changed
+263/−99 lines, 5 filesdep ~sbv
Dependency ranges changed: sbv
Files
- CHANGES.md +16/−1
- README.md +59/−18
- crackNum.cabal +2/−2
- src/CrackNum/Main.hs +184/−78
- src/CrackNum/TestSuite.hs +2/−0
CHANGES.md view
@@ -1,20 +1,35 @@ * Hackage: <http://hackage.haskell.org/package/crackNum> * GitHub: <http://github.com/LeventErkok/crackNum/> -* 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
README.md view
@@ -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
crackNum.cabal view
@@ -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
src/CrackNum/Main.hs view
@@ -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)
src/CrackNum/TestSuite.hs view
@@ -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"]