From ff1b02652abd806beaac4daedcdb2ead93f3a0e0 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Tue, 13 Feb 2024 11:25:12 -0800 Subject: [PATCH] Support N'h notation --- Golds/decode6.gold | 120 ++++++++++++++++++++++++++++++++++++++ src/CrackNum/Main.hs | 32 +++++++--- src/CrackNum/TestSuite.hs | 3 +- 3 files changed, 145 insertions(+), 10 deletions(-) create mode 100644 Golds/decode6.gold diff --git a/Golds/decode6.gold b/Golds/decode6.gold new file mode 100644 index 0000000..9ca3b29 --- /dev/null +++ b/Golds/decode6.gold @@ -0,0 +1,120 @@ +Arguments: -fhp -l8 128'hffffffffffffffffbdffaaffdc71fc60 +Exit code: ExitSuccess +== Lane 7 ============================================================ +Satisfiable. Model: + DECODED = NaN :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 1 11111 1111111111 + Hex layout: FFFF + Precision: Half (5 exponent bits, 10 significand bits.) + Sign: Negative + Exponent: 16 (Stored: 31, Bias: 15) + Classification: FP_NAN (Quiet) + Value: NaN + Note: Representation for NaN's is not unique +== Lane 6 ============================================================ +Satisfiable. Model: + DECODED = NaN :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 1 11111 1111111111 + Hex layout: FFFF + Precision: Half (5 exponent bits, 10 significand bits.) + Sign: Negative + Exponent: 16 (Stored: 31, Bias: 15) + Classification: FP_NAN (Quiet) + Value: NaN + Note: Representation for NaN's is not unique +== Lane 5 ============================================================ +Satisfiable. Model: + DECODED = NaN :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 1 11111 1111111111 + Hex layout: FFFF + Precision: Half (5 exponent bits, 10 significand bits.) + Sign: Negative + Exponent: 16 (Stored: 31, Bias: 15) + Classification: FP_NAN (Quiet) + Value: NaN + Note: Representation for NaN's is not unique +== Lane 4 ============================================================ +Satisfiable. Model: + DECODED = NaN :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 1 11111 1111111111 + Hex layout: FFFF + Precision: Half (5 exponent bits, 10 significand bits.) + Sign: Negative + Exponent: 16 (Stored: 31, Bias: 15) + Classification: FP_NAN (Quiet) + Value: NaN + Note: Representation for NaN's is not unique +== Lane 3 ============================================================ +Satisfiable. Model: + DECODED = -1.499 :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 1 01111 0111111111 + Hex layout: BDFF + Precision: Half (5 exponent bits, 10 significand bits.) + Sign: Negative + Exponent: 0 (Stored: 15, Bias: 15) + Classification: FP_NORMAL + Binary: -0b1.0111111111 + Octal: -0o1.3774 + Decimal: -1.499 + Hex: -0x1.7fc +== Lane 2 ============================================================ +Satisfiable. Model: + DECODED = -0.054657 :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 1 01010 1011111111 + Hex layout: AAFF + Precision: Half (5 exponent bits, 10 significand bits.) + Sign: Negative + Exponent: -5 (Stored: 10, Bias: 15) + Classification: FP_NORMAL + Binary: -0b1.1011111111p-5 + Octal: -0o3.377p-6 + Decimal: -0.054657 + Hex: -0xd.fep-8 +== Lane 1 ============================================================ +Satisfiable. Model: + DECODED = -284.25 :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 1 10111 0001110001 + Hex layout: DC71 + Precision: Half (5 exponent bits, 10 significand bits.) + Sign: Negative + Exponent: 8 (Stored: 23, Bias: 15) + Classification: FP_NORMAL + Binary: -0b1.0001110001p8 + Octal: -0o4.342p6 + Decimal: -284.25 + Hex: -0x1.1c4p8 +== Lane 0 ============================================================ +Satisfiable. Model: + DECODED = NaN :: FloatingPoint 5 11 + 1 0 + 5 43210 9876543210 + S -E5-- ---S10---- + Binary layout: 1 11111 0001100000 + Hex layout: FC60 + 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 diff --git a/src/CrackNum/Main.hs b/src/CrackNum/Main.hs index 3165094..d0f6129 100644 --- a/src/CrackNum/Main.hs +++ b/src/CrackNum/Main.hs @@ -245,7 +245,12 @@ crack pn argv = case getOpt Permute pgmOptions argv of _ -> do usage pn exitFailure - let decode = any (`isPrefixOf` arg) ["0x", "0b"] + let decode = case arg of + '0':'x':_ -> True + '0':'b':_ -> True + _ -> case break (`elem` "'h") arg of + (pre@(_:_), '\'':'h':_) -> all isDigit pre + _ -> False if decode then decodeAllLanes lanes kind arg else encodeLane lanes kind rm arg @@ -299,12 +304,15 @@ parseToBits :: String -> IO [Bool] parseToBits inp = do let isSkippable c = c `elem` "_-" || isSpace c - (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) - ] + (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) + ] let cvtBin '1' = pure [True] cvtBin '0' = pure [False] @@ -321,7 +329,13 @@ parseToBits inp = do cvt i | isHex = concat <$> mapM cvtHex i | True = concat <$> mapM cvtBin i - cvt stream + res <- cvt stream + + let pad = case mbPadTo of + Nothing -> [] + Just n -> replicate (n - length res) False + + pure $ pad ++ res -- | Decoding decodeLane :: [Bool] -> NKind -> IO () @@ -434,7 +448,7 @@ encodeLane lanes num rm inp 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 index 82cb8ae..1fed032 100644 --- a/src/CrackNum/TestSuite.hs +++ b/src/CrackNum/TestSuite.hs @@ -63,7 +63,8 @@ tests = testGroup "CrackNum" [ , gold "decode2" ["-f3+4", "0b0111001"] , gold "decode3" ["-fbp", "0x000F"] , gold "decode4" ["-fdp", "0x8000000000000000"] - , gold "decode5" ["-fhp", "0x7c01"] + , gold "decode5" ["-fhp", "0x7c01"] + , gold "decode6" ["-fhp", "-l8", "128'hffffffffffffffffbdffaaffdc71fc60"] ] , testGroup "Bad" [ gold "badInvocation0" ["-f3+4", "0b01"]