Skip to content

Commit

Permalink
Support N'h notation
Browse files Browse the repository at this point in the history
  • Loading branch information
@LeventErkok
LeventErkok committed Feb 13, 2024
1 parent a9f54fa commit ff1b026
Show file tree
Hide file tree
Showing 3 changed files with 145 additions and 10 deletions.
120 changes: 120 additions & 0 deletions Golds/decode6.gold
View file
Original file line number Diff line number Diff line change
@@ -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
32 changes: 23 additions & 9 deletions src/CrackNum/Main.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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]
Expand All @@ -321,7 +329,13 @@ parseToBits inp = do
cvt i | isHex = concat <$> mapM cvtHex i

Check warning on line 329 in src/CrackNum/Main.hs

View workflow job for this annotation

GitHub Actions / hlint 

Suggestion in parseToBits in module Main: Use otherwise ▫︎ Found: "cvt i\n | isHex = concat <$> mapM cvtHex i\n | True = concat <$> mapM cvtBin i" ▫︎ Perhaps: "cvt i\n | isHex = concat <$> mapM cvtHex i\n | otherwise = concat <$> mapM cvtBin 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 ()
Expand Down Expand Up @@ -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)
Expand Down
3 changes: 2 additions & 1 deletion src/CrackNum/TestSuite.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down

0 comments on commit ff1b026

Please sign in to comment.