crackNum 3.10 → 3.11
raw patch · 5 files changed
+59/−13 lines, 5 filesdep +deepseqdep +ghcdep ~sbv
Dependencies added: deepseq, ghc
Dependency ranges changed: sbv
Files
- CHANGES.md +4/−0
- README.md +3/−1
- crackNum.cabal +3/−3
- src/CrackNum/Main.hs +46/−9
- src/CrackNum/TestSuite.hs +3/−0
CHANGES.md view
@@ -3,6 +3,10 @@ * Latest Hackage released version: 3.10, 2024-03-01 +### Version 3.11, 2024-04-05++ * Allow for encoding of hexadecimal floats+ ### Version 3.10, 2024-03-01 * More relaxed parsing for verilog input format
README.md view
@@ -137,6 +137,7 @@ crackNum -fdp 2.5 -- encode as a double-precision float crackNum -fe4m3 2.5 -- encode as an E4M3 FP8 float crackNum -fe5m2 2.5 -- encode as an E5M2 FP8 float+ crackNum -fsp 0x3.2p5 -- encode as single-precision from hex-float Decoding: crackNum -i4 0b0110 -- decode as 4-bit signed integer, from binary@@ -150,7 +151,8 @@ 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 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) - For decoding: - Use hexadecimal (0x) binary (0b), or N'h (verilog) notation as input. Input must have one of these prefixes.
crackNum.cabal view
@@ -1,6 +1,6 @@ Cabal-version : 2.2 Name : crackNum-Version : 3.10+Version : 3.11 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.5- , tasty, tasty-golden, filepath, directory, process+ build-depends : base >= 4.11 && < 5, libBF, ghc, sbv >= 10.9+ , tasty, tasty-golden, filepath, directory, process, deepseq other-modules : Paths_crackNum, CrackNum.TestSuite autogen-modules : Paths_crackNum
src/CrackNum/Main.hs view
@@ -18,11 +18,17 @@ module Main(main) where -import Control.Monad (when)-import Data.Char (isDigit, isSpace, toLower)-import Data.List (isPrefixOf, isSuffixOf, unfoldr, isInfixOf, intercalate)-import Data.Maybe (fromMaybe)+import Control.Monad (when)+import Control.DeepSeq (rnf)+import Data.Char (isDigit, isSpace, toLower)+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) import System.Console.GetOpt (ArgOrder(Permute), getOpt, ArgDescr(..), OptDescr(..), usageInfo)@@ -85,7 +91,7 @@ show RTN = "RTN: Round towards negative infinity." show RTZ = "RTZ: Round towards zero." --- Covert to LibBF rounding mode+-- Convert to LibBF rounding mode toLibBFRM :: RM -> RoundMode toLibBFRM RNE = NearEven toLibBFRM RNA = NearAway@@ -93,6 +99,14 @@ 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@@ -226,6 +240,7 @@ , " " ++ pn ++ " -fdp 2.5 -- encode as a double-precision float" , " " ++ pn ++ " -fe4m3 2.5 -- encode as an E4M3 FP8 float" , " " ++ pn ++ " -fe5m2 2.5 -- encode as an E5M2 FP8 float"+ , " " ++ pn ++ " -fsp 0x3.2p5 -- encode as single-precision from hex-float" , "" , " Decoding:" , " " ++ pn ++ " -i4 0b0110 -- decode as 4-bit signed integer, from binary"@@ -239,7 +254,8 @@ , " 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 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)" , " - For decoding:" , " - Use hexadecimal (0x) binary (0b), or N'h (verilog) notation as input." , " Input must have one of these prefixes."@@ -291,7 +307,9 @@ (decode, isVerilog, lanesInferred) <- case arg of- '0':'x':_ -> pure (True, False, Nothing)+ '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':_)@@ -531,7 +549,7 @@ SInt n -> print =<< ei True n SWord n -> print =<< ei False n SFloat s -> ef s (s == E5M2)- where satCmd = satWith z3{crackNum=True, verbose=debug}+ where satCmd = satWith z3{crackNum=True, verbose=debug, isNonModelVar = (/= "ENCODED")} ei :: Bool -> Int -> IO SatResult ei sgn n = case reads inp of@@ -577,7 +595,12 @@ ef (FP i j) wasE5M2 = do let (v, mbS) = convert i j if bfIsNaN v && fixup False inp /= "NaN"- then unrecognized inp+ 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 fixE5M2Type res+ else print res else do res <- satCmd (p v) if wasE5M2 then fixE5M2Type res else print res@@ -586,6 +609,20 @@ 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 .== SBV (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
src/CrackNum/TestSuite.hs view
@@ -68,6 +68,9 @@ , gold "encode14" "-fsp infinity" , gold "encode15" "-fsp nan" , gold "encode16" "-fe5m2 2.5"+ , gold "encode17" "-fsp -- -0x2p3"+ , gold "encode18" "-fdp -- 0x1.3"+ , gold "encode19" "-fhp -- 0x1.3p4" ] , testGroup "EncodeE4M3" [ gold "encodeE4M3_nan" "-fe4m3 nan"