Skip to content

Commit

Permalink
Support for multiple-lane decoding
Browse files Browse the repository at this point in the history
  • Loading branch information
@LeventErkok
LeventErkok committed Feb 13, 2024
1 parent dfea4c5 commit a9f54fa
Show file tree
Hide file tree
Showing 2 changed files with 113 additions and 72 deletions.
184 changes: 112 additions & 72 deletions src/CrackNum/Main.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,15 +16,14 @@

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 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
Expand Down Expand Up @@ -232,19 +231,54 @@ crack pn argv = case getOpt Permute pgmOptions argv of
(r:_) -> r
_ -> RNE

ls = case reverse [l | Lanes l <- os] of
(l:_) -> l
_ -> 1
lanes = case reverse [l | Lanes l <- os] of
(l:_) -> l
_ -> 1

arg = dropWhile isSpace $ unwords rs

case ([b | BadFlag b <- os], filter (\o -> not (isRMode o || isLanes o)) os) of
(e:_, _) -> die e
(_, [Signed n]) -> process ls (SInt n) rm arg
(_, [Unsigned n]) -> process ls (SWord n) rm arg
(_, [Floating s]) -> process ls (SFloat s) rm arg
_ -> usage pn

kind <- case ([b | BadFlag b <- os], filter (\o -> not (isRMode o || isLanes o)) os) of
(e:_, _) -> die e
(_, [Signed n]) -> pure $ SInt n
(_, [Unsigned n]) -> pure $ SWord n
(_, [Floating s]) -> pure $ SFloat s
_ -> do usage pn
exitFailure

let decode = any (`isPrefixOf` arg) ["0x", "0b"]
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 ()

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

View workflow job for this annotation

GitHub Actions / hlint 

Suggestion in decodeAllLanes in module Main: Use otherwise ▫︎ Found: "header i\n | lanes == 1 = pure ()\n | True = putStrLn $ \"== Lane \" ++ show i ++ \" \" ++ replicate 60 '='" ▫︎ Perhaps: "header i\n | lanes == 1 = pure ()\n | otherwise\n = putStrLn $ \"== Lane \" ++ show i ++ \" \" ++ replicate 60 '='"
| 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 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
Expand All @@ -261,53 +295,47 @@ main = do argv <- getArgs
then withArgs (filter (`notElem` [rt, "--"]) argv) runTests
else crack pn argv

-- | Perform the encoding/decoding
process :: Int -> NKind -> RM -> String -> IO ()
process lanes num rm inp
| not decode && lanes > 1
= die [ "Encoding requested with number of lanes = " ++ show lanes
, "Lanes are only supported for decoding values."
]
| True
= 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"]

bitString n = 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)
]

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

cvt i | isHex = concat <$> mapM cvtHex i
| True = concat <$> mapM cvtBin i

encoded <- cvt stream

let bits 1 = "one bit"
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)
]

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

cvt i | isHex = concat <$> mapM cvtHex i

Check warning on line 321 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

-- | Decoding
decodeLane :: [Bool] -> NKind -> IO ()
decodeLane 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)]
case length inputBits `compare` n of
EQ -> pure inputBits
LT -> die ["Input needs to be " ++ show n ++ " bits wide, it's too short by " ++ bits (n - length inputBits)]
GT -> die ["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
Expand All @@ -316,16 +344,6 @@ process lanes num rm inp
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 allBits <- bitString (fpSize fp)

Expand Down Expand Up @@ -357,6 +375,28 @@ process lanes num rm inp
let bits = svBlastBE sx
mapM_ constrain $ zipWith (.==) (map SBV bits) bs

-- | Encoding
encodeLane :: Int -> NKind -> RM -> String -> IO ()
encodeLane lanes num rm inp

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

View workflow job for this annotation

GitHub Actions / hlint 

Suggestion in encodeLane in module Main: Use otherwise ▫︎ Found: "encodeLane lanes num rm inp\n | lanes /= 1\n = die\n [\"Lanes argument is only valid with decoding values.\",\n \"Received: \" ++ show lanes]\n | True\n = case num of\n SInt n -> print =<< ei True n\n SWord n -> print =<< ei False n\n SFloat s -> ef s\n where\n ei :: Bool -> Int -> IO SatResult\n ei sgn n\n = case reads inp of\n [(v :: Integer, \"\")] -> satWith z3 {crackNum = True} $ p v\n _ -> die\n [\"Expected an integer value to decode, received: \" ++ show inp]\n where\n p :: Integer -> Predicate\n p iv\n = do let k = KBounded sgn n\n v = SBV $ SVal k $ Left $ mkConstCV k iv\n x <- (if sgn then sIntN else sWordN) n \"ENCODED\"\n pure $ SBV x .== v\n convert :: Int -> Int -> (BigFloat, Maybe String)\n convert i j\n = case s of\n Ok -> (v, Nothing)\n _ -> (v, Just (trim (show s)))\n where\n bfOpts\n = allowSubnormal\n <>\n rnd (toLibBFRM rm)\n <> expBits (fromIntegral i) <> precBits (fromIntegral j)\n (v, s) = bfFromString 10 bfOpts inp\n trim xs\n | \"[\" `isPrefixOf` xs && \"]\" `isSuffixOf` xs = init (drop 1 xs)\n | True = xs\n note :: Maybe String -> IO ()\n note mbs\n = do putStrLn $ \" Rounding mode: \" ++ show rm\n case mbs of\n Nothing\n -> putStrLn\n $ \" Note: Conversion from \"\n ++ show inp ++ \" was exact. No rounding happened.\"\n Just s\n -> putStrLn\n $ \" Note: Conversion from \"\n ++ show inp ++ \" was not faithful. Status: \" ++ s ++ \".\"\n ef :: FP -> IO ()\n ef SP\n = case reads (fixup inp) of\n [(v :: Float, \"\")]\n -> do print =<< satWith z3 {crackNum = True} (p v)\n note $ snd $ convert 8 24\n _ -> ef (FP 8 24)\n where\n p :: Float -> Predicate\n p f\n = do x <- sFloat \"ENCODED\"\n pure $ x .=== literal f\n ef DP\n = case reads (fixup inp) of\n [(v :: Double, \"\")]\n -> do print =<< satWith z3 {crackNum = True} (p v)\n note $ snd $ convert 11 53\n _ -> ef (FP 11 53)\n where\n p :: Double -> Predicate\n p d\n = do x <- sDouble \"ENCODED\"\n pure $ x .=== literal d\n ef (FP i j)\n = do let (v, mbS) = convert i j\n if bfIsNaN v then\n die\n [\"Input does not represent floating point number we recognize.\",\n \"Saw: \" ++ inp, \"\",\n \"For decoding bit-strings, prefix them with 0x or 0b, and\",\n \"provide a hexadecimal or binary representation of the input.\"]\n else\n do print =<< satWith z3 {crackNum = True} (p v)\n note mbS\n where\n p :: BigFloat -> Predicate\n p bf\n = do let k = KFP i j\n sx <- svNewVar k \"ENCODED\"\n pure\n $ SBV\n $ sx\n `svStrongEqual` SVal k (Left (CV k (CFP (fpFromBigFloat i j bf))))" ▫︎ Perhaps: "encodeLane lanes num rm inp\n | lanes /= 1\n = die\n [\"Lanes argument is only valid with decoding values.\",\n \"Received: \" ++ show lanes]\n | otherwise\n = case num of\n SInt n -> print =<< ei True n\n SWord n -> print =<< ei False n\n SFloat s -> ef s\n where\n ei :: Bool -> Int -> IO SatResult\n ei sgn n\n = case reads inp of\n [(v :: Integer, \"\")] -> satWith z3 {crackNum = True} $ p v\n _ -> die\n [\"Expected an integer value to decode, received: \" ++ show inp]\n where\n p :: Integer -> Predicate\n p iv\n = do let k = KBounded sgn n\n v = SBV $ SVal k $ Left $ mkConstCV k iv\n x <- (if sgn then sIntN else sWordN) n \"ENCODED\"\n pure $ SBV x .== v\n convert :: Int -> Int -> (BigFloat, Maybe String)\n convert i j\n = case s of\n Ok -> (v, Nothing)\n _ -> (v, Just (trim (show s)))\n where\n bfOpts\n = allowSubnormal\n <>\n rnd (toLibBFRM rm)\n <> expBits (fromIntegral i) <> precBits (fromIntegral j)\n (v, s) = bfFromString 10 bfOpts inp\n trim xs\n | \"[\" `isPrefixOf` xs && \"]\" `isSuffixOf` xs = init (drop 1 xs)\n | True = xs\n note :: Maybe String -> IO ()\n note mbs\n = do putStrLn $ \" Rounding mode: \" ++ show rm\n case mbs of\n Nothing\n -> putStrLn\n $ \" Note: Conversion from \"\n ++ show inp ++ \" was exact. No rounding happened.\"\n Just s\n -> putStrLn\n $ \" Note: Conversion from \"\n ++ show inp ++ \" was not faithful. Status: \" ++ s ++ \".\"\n ef :: FP -> IO ()\n ef SP\n = case reads (fixup inp) of\n [(v :: Float, \"\")]\n -> do print =<< satWith z3 {crackNum = True} (p v)\n note $
| 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)
Expand Down
1 change: 1 addition & 0 deletions src/CrackNum/TestSuite.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ tests = testGroup "CrackNum" [
, gold "decode2" ["-f3+4", "0b0111001"]
, gold "decode3" ["-fbp", "0x000F"]
, gold "decode4" ["-fdp", "0x8000000000000000"]
, gold "decode5" ["-fhp", "0x7c01"]
]
, testGroup "Bad" [
gold "badInvocation0" ["-f3+4", "0b01"]
Expand Down

0 comments on commit a9f54fa

Please sign in to comment.