Add tests for round-trip verification of printing and parsing.
Kevin Quick
7 years ago
| 19 | 19 | build-type: Simple |
| 20 | 20 | cabal-version: >=1.10 |
| 21 | 21 | bug-reports: https://github.com/aisamanra/s-cargot/issues |
| 22 | ||
| 23 | ||
| 24 | extra-source-files: test/big-sample.sexp | |
| 25 | , test/med-sample.sexp | |
| 26 | , test/med2-sample.sexp | |
| 27 | , test/small-sample.sexp | |
| 22 | 28 | |
| 23 | 29 | source-repository head |
| 24 | 30 | type: git |
| 72 | 78 | parsec >=3.1 && <4, |
| 73 | 79 | QuickCheck >=2.8 && <3, |
| 74 | 80 | text >=1.2 && <2 |
| 81 | ||
| 82 | test-suite s-cargot-printparse | |
| 83 | default-language: Haskell2010 | |
| 84 | type: exitcode-stdio-1.0 | |
| 85 | hs-source-dirs: test | |
| 86 | main-is: SCargotPrintParse.hs | |
| 87 | build-depends: s-cargot, | |
| 88 | base >=4.7 && <5, | |
| 89 | parsec >=3.1 && <4, | |
| 90 | HUnit >=1.6 && <1.7, | |
| 91 | text >=1.2 && <2 | |
| 1 | {-# LANGUAGE OverloadedStrings #-} | |
| 2 | {-# LANGUAGE LambdaCase #-} | |
| 3 | ||
| 4 | module Main where | |
| 5 | ||
| 6 | import Data.Either | |
| 7 | import Data.SCargot | |
| 8 | import Data.SCargot.Comments | |
| 9 | import Data.SCargot.Repr | |
| 10 | import Data.Semigroup | |
| 11 | import qualified Data.Text as T | |
| 12 | import qualified Data.Text.IO as TIO | |
| 13 | import System.Exit | |
| 14 | import Test.HUnit | |
| 15 | import Text.Parsec as P | |
| 16 | import Text.Parsec.Text (Parser) | |
| 17 | import Text.Printf ( printf ) | |
| 18 | ||
| 19 | ||
| 20 | main = do | |
| 21 | putStrLn "Parsing a large S-expression" | |
| 22 | srcs <- mapM (\n -> (,) n <$> TIO.readFile n) [ "test/small-sample.sexp" | |
| 23 | , "test/med-sample.sexp" | |
| 24 | , "test/med2-sample.sexp" | |
| 25 | , "test/big-sample.sexp" | |
| 26 | ] | |
| 27 | counts <- runTestTT $ TestList | |
| 28 | [ TestLabel "basic checks" $ TestList | |
| 29 | [ TestLabel "flat print" $ TestList | |
| 30 | [ TestLabel "flatprint SNil" $ "()" ~=? printSExpr SNil | |
| 31 | , TestLabel "flatprint SAtom" $ "hi" ~=? printSExpr (SAtom (AIdent "hi")) | |
| 32 | , TestLabel "flatprint pair" $ "(hi . world)" ~=? | |
| 33 | printSExpr (SCons (SAtom (AIdent "hi")) (SAtom (AIdent "world"))) | |
| 34 | , TestLabel "flatprint list of 1" $ "(hi)" ~=? | |
| 35 | printSExpr (SCons (SAtom (AIdent "hi")) SNil) | |
| 36 | , TestLabel "flatprint list of 2" $ "(hi world)" ~=? | |
| 37 | printSExpr (SCons (SAtom (AIdent "hi")) | |
| 38 | (SCons (SAtom (AIdent "world")) | |
| 39 | SNil)) | |
| 40 | , TestLabel "flatprint list of 2 pairs" $ "((hi . hallo) (world . welt))" ~=? | |
| 41 | printSExpr (SCons (SCons (SAtom (AIdent "hi")) | |
| 42 | (SAtom (AIdent "hallo"))) | |
| 43 | (SCons (SAtom (AIdent "world")) | |
| 44 | (SAtom (AIdent "welt")))) | |
| 45 | , TestLabel "flatprint list of 3 ending in a pair" $ "(hi world (hallo . welt))" ~=? | |
| 46 | printSExpr (SCons (SAtom (AIdent "hi")) | |
| 47 | (SCons (SAtom (AIdent "world")) | |
| 48 | (SCons (SAtom (AIdent "hallo")) | |
| 49 | (SAtom (AIdent "welt"))))) | |
| 50 | , TestLabel "flatprint list of 3" $ "(hi world hallo)" ~=? | |
| 51 | printSExpr (SCons (SAtom (AIdent "hi")) | |
| 52 | (SCons (SAtom (AIdent "world")) | |
| 53 | (SCons (SAtom (AIdent "hallo")) | |
| 54 | SNil))) | |
| 55 | ] | |
| 56 | , TestLabel "pretty print" $ | |
| 57 | let pprintIt = pprintSExpr 40 Swing in TestList | |
| 58 | [ TestLabel "pretty print SNil" $ "()\n" ~=? pprintIt SNil | |
| 59 | , TestLabel "pretty print SAtom" $ "hi\n" ~=? pprintIt (SAtom (AIdent "hi")) | |
| 60 | , TestLabel "pretty print pair" $ "(hi . world)\n" ~=? | |
| 61 | pprintIt (SCons (SAtom (AIdent "hi")) (SAtom (AIdent "world"))) | |
| 62 | , TestLabel "pretty print list of 1" $ "(hi)\n" ~=? | |
| 63 | pprintIt (SCons (SAtom (AIdent "hi")) SNil) | |
| 64 | , TestLabel "pretty print list of 2" $ "(hi world)\n" ~=? | |
| 65 | pprintIt (SCons (SAtom (AIdent "hi")) | |
| 66 | (SCons (SAtom (AIdent "world")) | |
| 67 | SNil)) | |
| 68 | , TestLabel "pretty print list of 2 pairs" $ | |
| 69 | "((hi . hallo) (world . welt))\n" ~=? | |
| 70 | pprintIt (SCons (SCons (SAtom (AIdent "hi")) | |
| 71 | (SAtom (AIdent "hallo"))) | |
| 72 | (SCons (SAtom (AIdent "world")) | |
| 73 | (SAtom (AIdent "welt")))) | |
| 74 | , TestLabel "pretty print list of 3 ending in a pair" $ | |
| 75 | "(hi world (hallo . welt))\n" ~=? | |
| 76 | pprintIt (SCons (SAtom (AIdent "hi")) | |
| 77 | (SCons (SAtom (AIdent "world")) | |
| 78 | (SCons (SAtom (AIdent "hallo")) | |
| 79 | (SAtom (AIdent "welt"))))) | |
| 80 | , TestLabel "pretty print list of 3" $ "(hi world hallo)\n" ~=? | |
| 81 | pprintIt (SCons (SAtom (AIdent "hi")) | |
| 82 | (SCons (SAtom (AIdent "world")) | |
| 83 | (SCons (SAtom (AIdent "hallo")) | |
| 84 | SNil))) | |
| 85 | ] | |
| 86 | ] | |
| 87 | , TestLabel "round-trip" $ TestList $ | |
| 88 | concatMap (\t -> map t srcs) $ | |
| 89 | [ testParsePrint | |
| 90 | ] | |
| 91 | ] | |
| 92 | if errors counts + failures counts > 0 | |
| 93 | then exitFailure | |
| 94 | else exitSuccess | |
| 95 | ||
| 96 | ||
| 97 | testParsePrint :: (String, T.Text) -> Test | |
| 98 | testParsePrint (n,s) = TestList | |
| 99 | [ testParseFlatPrint n s | |
| 100 | ||
| 101 | , testParsePPrint 80 Swing n s | |
| 102 | , testParsePPrint 60 Swing n s | |
| 103 | , testParsePPrint 40 Swing n s | |
| 104 | , testParsePPrint 20 Swing n s | |
| 105 | , testParsePPrint 15 Swing n s | |
| 106 | , testParsePPrint 10 Swing n s | |
| 107 | ||
| 108 | , testParsePPrint 80 Align n s | |
| 109 | , testParsePPrint 40 Align n s | |
| 110 | , testParsePPrint 10 Align n s | |
| 111 | ] | |
| 112 | ||
| 113 | ||
| 114 | testParseFlatPrint testName src = | |
| 115 | testRoundTrip (testName <> " flat print") | |
| 116 | (fromRight (error "Failed parse") . parseSExpr) | |
| 117 | printSExpr | |
| 118 | stripAllText | |
| 119 | src | |
| 120 | ||
| 121 | testParsePPrint width indentStyle testName src = | |
| 122 | testRoundTrip (testName <> " pretty print") | |
| 123 | (fromRight (error "Failed parse") . parseSExpr) | |
| 124 | (pprintSExpr width indentStyle) | |
| 125 | stripAllText | |
| 126 | src | |
| 127 | ||
| 128 | stripAllText = T.unwords . concatMap T.words . T.lines | |
| 129 | ||
| 130 | testRoundTrip nm there back prep src = TestList | |
| 131 | [ TestLabel (nm <> " round trip") $ | |
| 132 | TestCase $ (prep src) @=? (prep $ back $ there src) | |
| 133 | ||
| 134 | , TestLabel (nm <> " round trip twice") $ | |
| 135 | TestCase $ (prep src) @=? (prep $ back $ there $ back $ there src) | |
| 136 | ] | |
| 137 | ||
| 138 | ||
| 139 | ------------------------------------------------------------------------ | |
| 140 | ||
| 141 | data FAtom = AIdent String | |
| 142 | | AQuoted String | |
| 143 | | AString String | |
| 144 | | AInt Integer | |
| 145 | | ABV Int Integer | |
| 146 | deriving (Eq, Show) | |
| 147 | ||
| 148 | ||
| 149 | string :: String -> SExpr FAtom | |
| 150 | string = SAtom . AString | |
| 151 | ||
| 152 | -- | Lift an unquoted identifier. | |
| 153 | ident :: String -> SExpr FAtom | |
| 154 | ident = SAtom . AIdent | |
| 155 | ||
| 156 | -- | Lift a quoted identifier. | |
| 157 | quoted :: String -> SExpr FAtom | |
| 158 | quoted = SAtom . AQuoted | |
| 159 | ||
| 160 | -- | Lift an integer. | |
| 161 | int :: Integer -> SExpr FAtom | |
| 162 | int = SAtom . AInt | |
| 163 | ||
| 164 | ||
| 165 | printAtom :: FAtom -> T.Text | |
| 166 | printAtom a = | |
| 167 | case a of | |
| 168 | AIdent s -> T.pack s | |
| 169 | AQuoted s -> T.pack ('\'' : s) | |
| 170 | AString s -> T.pack (show s) | |
| 171 | AInt i -> T.pack (show i) | |
| 172 | ABV w val -> formatBV w val | |
| 173 | ||
| 174 | ||
| 175 | printSExpr :: SExpr FAtom -> T.Text | |
| 176 | printSExpr = encodeOne (flatPrint printAtom) | |
| 177 | ||
| 178 | pprintSExpr :: Int -> Indent -> SExpr FAtom -> T.Text | |
| 179 | pprintSExpr w i = encodeOne (setIndentStrategy (const i) $ | |
| 180 | setMaxWidth w $ | |
| 181 | setIndentAmount 1 $ | |
| 182 | basicPrint printAtom) | |
| 183 | ||
| 184 | getIdent :: FAtom -> Maybe String | |
| 185 | getIdent (AIdent s) = Just s | |
| 186 | getIdent _ = Nothing | |
| 187 | ||
| 188 | formatBV :: Int -> Integer -> T.Text | |
| 189 | formatBV w val = T.pack (prefix ++ printf fmt val) | |
| 190 | where | |
| 191 | (prefix, fmt) | |
| 192 | | w `rem` 4 == 0 = ("#x", "%0" ++ show (w `div` 4) ++ "x") | |
| 193 | | otherwise = ("#b", "%0" ++ show w ++ "b") | |
| 194 | ||
| 195 | parseIdent :: Parser String | |
| 196 | parseIdent = (:) <$> first <*> P.many rest | |
| 197 | where first = P.letter P.<|> P.oneOf "+-=<>_" | |
| 198 | rest = P.letter P.<|> P.digit P.<|> P.oneOf "+-=<>_" | |
| 199 | ||
| 200 | parseString :: Parser String | |
| 201 | parseString = do | |
| 202 | _ <- P.char '"' | |
| 203 | s <- P.many (P.noneOf ['"']) | |
| 204 | _ <- P.char '"' | |
| 205 | return s | |
| 206 | ||
| 207 | parseBV :: Parser (Int, Integer) | |
| 208 | parseBV = P.char '#' >> ((P.char 'b' >> parseBin) P.<|> (P.char 'x' >> parseHex)) | |
| 209 | where parseBin = P.oneOf "10" >>= \d -> parseBin' (1, if d == '1' then 1 else 0) | |
| 210 | ||
| 211 | parseBin' :: (Int, Integer) -> Parser (Int, Integer) | |
| 212 | parseBin' (bits, x) = do | |
| 213 | P.optionMaybe (P.oneOf "10") >>= \case | |
| 214 | Just d -> parseBin' (bits + 1, x * 2 + (if d == '1' then 1 else 0)) | |
| 215 | Nothing -> return (bits, x) | |
| 216 | ||
| 217 | parseHex = (\s -> (length s * 4, read ("0x" ++ s))) <$> P.many1 P.hexDigit | |
| 218 | ||
| 219 | parseAtom :: Parser FAtom | |
| 220 | parseAtom | |
| 221 | = AIdent <$> parseIdent | |
| 222 | P.<|> AQuoted <$> (P.char '\'' >> parseIdent) | |
| 223 | P.<|> AString <$> parseString | |
| 224 | P.<|> AInt . read <$> P.many1 P.digit | |
| 225 | P.<|> uncurry ABV <$> parseBV | |
| 226 | ||
| 227 | parserLL :: SExprParser FAtom (SExpr FAtom) | |
| 228 | parserLL = withLispComments (mkParser parseAtom) | |
| 229 | ||
| 230 | parseSExpr :: T.Text -> Either String (SExpr FAtom) | |
| 231 | parseSExpr = decodeOne parserLL |
| 1 | ((operands ((rD . 'GPR) (setcc . 'Cc_out) (predBits . 'Pred) (mimm . 'Mod_imm) (rN . 'GPR))) (in (mimm setcc rN 'CPSR 'PC)) (defs (('PC (ite ((_ call "arm.is_r15") rD) (ite (bveq #b0 ((_ extract 0 0) ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000))))) (bvand #xfffffffe ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000)))) (ite (bveq #b0 ((_ extract 1 1) ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000))))) (bvand #xfffffffd ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000)))) ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000))))) (bvadd 'PC #x00000004))) ('CPSR (ite (ite (andp (bveq #b1 ((_ extract 0 0) predBits)) (bvne predBits #xf)) (notp (ite (bveq ((_ extract 3 1) predBits) #b000) (bveq #b1 ((_ extract 30 30) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b001) (bveq #b1 ((_ extract 29 29) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b010) (bveq #b1 ((_ extract 31 31) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b011) (bveq #b1 ((_ extract 28 28) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b100) (andp (bveq #b1 ((_ extract 29 29) 'CPSR)) (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) (ite (bveq ((_ extract 3 1) predBits) #b101) (bveq ((_ extract 31 31) 'CPSR) ((_ extract 28 28) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b110) (andp (bveq ((_ extract 31 31) 'CPSR) ((_ extract 28 28) 'CPSR)) (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) (bveq #b0 #b0))))))))) (ite (bveq ((_ extract 3 1) predBits) #b000) (bveq #b1 ((_ extract 30 30) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b001) (bveq #b1 ((_ extract 29 29) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b010) (bveq #b1 ((_ extract 31 31) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b011) (bveq #b1 ((_ extract 28 28) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b100) (andp (bveq #b1 ((_ extract 29 29) 'CPSR)) (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) (ite (bveq ((_ extract 3 1) predBits) #b101) (bveq ((_ extract 31 31) 'CPSR) ((_ extract 28 28) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b110) (andp (bveq ((_ extract 31 31) 'CPSR) ((_ extract 28 28) 'CPSR)) (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) (bveq #b0 #b0))))))))) (ite (andp (bveq setcc #b1) (notp ((_ call "arm.is_r15") rD))) (concat (concat ((_ extract 31 31) ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000)))) (concat (ite (bveq ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000))) #x00000000) #b1 #b0) (concat ((_ extract 32 32) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000))) (bvand ((_ extract 31 31) ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000)))) ((_ extract 32 32) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000))))))) ((_ extract 27 0) (ite ((_ call "arm.is_r15") rD) (ite (bveq #b0 ((_ extract 0 0) ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000))))) (bvand #xfeffffff (bvor #x00000020 'CPSR)) 'CPSR) 'CPSR))) (ite ((_ call "arm.is_r15") rD) (ite (bveq #b0 ((_ extract 0 0) ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000))))) (bvand #xfeffffff (bvor #x00000020 'CPSR)) 'CPSR) 'CPSR)) 'CPSR)) (rD (ite (ite (andp (bveq #b1 ((_ extract 0 0) predBits)) (bvne predBits #xf)) (notp (ite (bveq ((_ extract 3 1) predBits) #b000) (bveq #b1 ((_ extract 30 30) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b001) (bveq #b1 ((_ extract 29 29) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b010) (bveq #b1 ((_ extract 31 31) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b011) (bveq #b1 ((_ extract 28 28) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b100) (andp (bveq #b1 ((_ extract 29 29) 'CPSR)) (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) (ite (bveq ((_ extract 3 1) predBits) #b101) (bveq ((_ extract 31 31) 'CPSR) ((_ extract 28 28) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b110) (andp (bveq ((_ extract 31 31) 'CPSR) ((_ extract 28 28) 'CPSR)) (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) (bveq #b0 #b0))))))))) (ite (bveq ((_ extract 3 1) predBits) #b000) (bveq #b1 ((_ extract 30 30) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b001) (bveq #b1 ((_ extract 29 29) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b010) (bveq #b1 ((_ extract 31 31) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b011) (bveq #b1 ((_ extract 28 28) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b100) (andp (bveq #b1 ((_ extract 29 29) 'CPSR)) (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) (ite (bveq ((_ extract 3 1) predBits) #b101) (bveq ((_ extract 31 31) 'CPSR) ((_ extract 28 28) 'CPSR)) (ite (bveq ((_ extract 3 1) predBits) #b110) (andp (bveq ((_ extract 31 31) 'CPSR) ((_ extract 28 28) 'CPSR)) (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) (bveq #b0 #b0))))))))) (ite ((_ call "arm.is_r15") rD) rD ((_ extract 31 0) (bvadd (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (ite (bveq (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) #x00000000) ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) (bvor (bvshl (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvsub #x00000020 (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020))) (bvlshr (bvshl #x00000001 ((_ zero_extend 28) ((_ call "a32.modimm_rot") mimm))) (bvurem ((_ zero_extend 24) ((_ call "a32.modimm_imm") mimm)) #x00000020)))))) ((_ zero_extend 1) #x00000000)))) rD)))))⏎ |
| 1 | ((operands ((rA . 'Gprc) (rS . 'Gprc) (rB . 'Gprc))) | |
| 2 | (in ('XER 'CR rB rS 'IP)) | |
| 3 | (defs | |
| 4 | (('CR | |
| 5 | (bvor | |
| 6 | (bvand | |
| 7 | 'CR | |
| 8 | (bvnot (bvshl #x0000000f (bvmul ((_ zero_extend 29) #b000) #x00000004)))) | |
| 9 | (bvshl | |
| 10 | ((_ zero_extend 28) | |
| 11 | (concat | |
| 12 | (ite | |
| 13 | (bvslt (bvxor rS rB) #x00000000) | |
| 14 | #b100 | |
| 15 | (ite (bvsgt (bvxor rS rB) #x00000000) #b010 #b001)) | |
| 16 | ((_ extract 0 0) 'XER))) | |
| 17 | (bvmul ((_ zero_extend 29) #b000) #x00000004)))) (rA (bvxor rS rB)) ('IP (bvadd 'IP #x00000004)))))⏎ |
| 1 | ((operands | |
| 2 | ((rD . 'GPR) | |
| 3 | (setcc . 'Cc_out) | |
| 4 | (predBits . 'Pred) | |
| 5 | (rM . 'GPR) | |
| 6 | (rN . 'GPR))) | |
| 7 | (in (setcc rN rM 'CPSR 'PC)) | |
| 8 | (defs | |
| 9 | (('PC | |
| 10 | (ite | |
| 11 | ((_ call "arm.is_r15") rD) | |
| 12 | (ite | |
| 13 | (bveq | |
| 14 | #b0 | |
| 15 | ((_ extract 0 0) | |
| 16 | ((_ extract 31 0) | |
| 17 | (bvadd | |
| 18 | (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM))) | |
| 19 | ((_ zero_extend 1) #x00000001))))) | |
| 20 | (bvand | |
| 21 | #xfffffffe | |
| 22 | ((_ extract 31 0) | |
| 23 | (bvadd | |
| 24 | (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM))) | |
| 25 | ((_ zero_extend 1) #x00000001)))) | |
| 26 | (ite | |
| 27 | (bveq | |
| 28 | #b0 | |
| 29 | ((_ extract 1 1) | |
| 30 | ((_ extract 31 0) | |
| 31 | (bvadd | |
| 32 | (bvadd | |
| 33 | ((_ zero_extend 1) rN) | |
| 34 | ((_ zero_extend 1) (bvnot rM))) | |
| 35 | ((_ zero_extend 1) #x00000001))))) | |
| 36 | (bvand | |
| 37 | #xfffffffd | |
| 38 | ((_ extract 31 0) | |
| 39 | (bvadd | |
| 40 | (bvadd | |
| 41 | ((_ zero_extend 1) rN) | |
| 42 | ((_ zero_extend 1) (bvnot rM))) | |
| 43 | ((_ zero_extend 1) #x00000001)))) | |
| 44 | ((_ extract 31 0) | |
| 45 | (bvadd | |
| 46 | (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM))) | |
| 47 | ((_ zero_extend 1) #x00000001))))) | |
| 48 | (bvadd 'PC #x00000004))) | |
| 49 | ('CPSR | |
| 50 | (ite | |
| 51 | (ite | |
| 52 | (andp (bveq #b1 ((_ extract 0 0) predBits)) (bvne predBits #xf)) | |
| 53 | (notp | |
| 54 | (ite | |
| 55 | (bveq ((_ extract 3 1) predBits) #b000) | |
| 56 | (bveq #b1 ((_ extract 30 30) 'CPSR)) | |
| 57 | (ite | |
| 58 | (bveq ((_ extract 3 1) predBits) #b001) | |
| 59 | (bveq #b1 ((_ extract 29 29) 'CPSR)) | |
| 60 | (ite | |
| 61 | (bveq ((_ extract 3 1) predBits) #b010) | |
| 62 | (bveq #b1 ((_ extract 31 31) 'CPSR)) | |
| 63 | (ite | |
| 64 | (bveq ((_ extract 3 1) predBits) #b011) | |
| 65 | (bveq #b1 ((_ extract 28 28) 'CPSR)) | |
| 66 | (ite | |
| 67 | (bveq ((_ extract 3 1) predBits) #b100) | |
| 68 | (andp | |
| 69 | (bveq #b1 ((_ extract 29 29) 'CPSR)) | |
| 70 | (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) | |
| 71 | (ite | |
| 72 | (bveq ((_ extract 3 1) predBits) #b101) | |
| 73 | (bveq | |
| 74 | ((_ extract 31 31) 'CPSR) | |
| 75 | ((_ extract 28 28) 'CPSR)) | |
| 76 | (ite | |
| 77 | (bveq ((_ extract 3 1) predBits) #b110) | |
| 78 | (andp | |
| 79 | (bveq | |
| 80 | ((_ extract 31 31) 'CPSR) | |
| 81 | ((_ extract 28 28) 'CPSR)) | |
| 82 | (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) | |
| 83 | (bveq #b0 #b0))))))))) | |
| 84 | (ite | |
| 85 | (bveq ((_ extract 3 1) predBits) #b000) | |
| 86 | (bveq #b1 ((_ extract 30 30) 'CPSR)) | |
| 87 | (ite | |
| 88 | (bveq ((_ extract 3 1) predBits) #b001) | |
| 89 | (bveq #b1 ((_ extract 29 29) 'CPSR)) | |
| 90 | (ite | |
| 91 | (bveq ((_ extract 3 1) predBits) #b010) | |
| 92 | (bveq #b1 ((_ extract 31 31) 'CPSR)) | |
| 93 | (ite | |
| 94 | (bveq ((_ extract 3 1) predBits) #b011) | |
| 95 | (bveq #b1 ((_ extract 28 28) 'CPSR)) | |
| 96 | (ite | |
| 97 | (bveq ((_ extract 3 1) predBits) #b100) | |
| 98 | (andp | |
| 99 | (bveq #b1 ((_ extract 29 29) 'CPSR)) | |
| 100 | (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) | |
| 101 | (ite | |
| 102 | (bveq ((_ extract 3 1) predBits) #b101) | |
| 103 | (bveq | |
| 104 | ((_ extract 31 31) 'CPSR) | |
| 105 | ((_ extract 28 28) 'CPSR)) | |
| 106 | (ite | |
| 107 | (bveq ((_ extract 3 1) predBits) #b110) | |
| 108 | (andp | |
| 109 | (bveq | |
| 110 | ((_ extract 31 31) 'CPSR) | |
| 111 | ((_ extract 28 28) 'CPSR)) | |
| 112 | (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) | |
| 113 | (bveq #b0 #b0))))))))) | |
| 114 | (ite | |
| 115 | (andp (bveq setcc #b1) (notp ((_ call "arm.is_r15") rD))) | |
| 116 | (concat | |
| 117 | (concat | |
| 118 | ((_ extract 31 31) | |
| 119 | ((_ extract 31 0) | |
| 120 | (bvadd | |
| 121 | (bvadd | |
| 122 | ((_ zero_extend 1) rN) | |
| 123 | ((_ zero_extend 1) (bvnot rM))) | |
| 124 | ((_ zero_extend 1) #x00000001)))) | |
| 125 | (concat | |
| 126 | (ite | |
| 127 | (bveq | |
| 128 | ((_ extract 31 0) | |
| 129 | (bvadd | |
| 130 | (bvadd | |
| 131 | ((_ zero_extend 1) rN) | |
| 132 | ((_ zero_extend 1) (bvnot rM))) | |
| 133 | ((_ zero_extend 1) #x00000001))) | |
| 134 | #x00000000) | |
| 135 | #b1 | |
| 136 | #b0) | |
| 137 | (concat | |
| 138 | ((_ extract 32 32) | |
| 139 | (bvadd | |
| 140 | (bvadd | |
| 141 | ((_ zero_extend 1) rN) | |
| 142 | ((_ zero_extend 1) (bvnot rM))) | |
| 143 | ((_ zero_extend 1) #x00000001))) | |
| 144 | (bvand | |
| 145 | ((_ extract 31 31) | |
| 146 | ((_ extract 31 0) | |
| 147 | (bvadd | |
| 148 | (bvadd | |
| 149 | ((_ zero_extend 1) rN) | |
| 150 | ((_ zero_extend 1) (bvnot rM))) | |
| 151 | ((_ zero_extend 1) #x00000001)))) | |
| 152 | ((_ extract 32 32) | |
| 153 | (bvadd | |
| 154 | (bvadd | |
| 155 | ((_ zero_extend 1) rN) | |
| 156 | ((_ zero_extend 1) (bvnot rM))) | |
| 157 | ((_ zero_extend 1) #x00000001))))))) | |
| 158 | ((_ extract 27 0) | |
| 159 | (ite | |
| 160 | ((_ call "arm.is_r15") rD) | |
| 161 | (ite | |
| 162 | (bveq | |
| 163 | #b0 | |
| 164 | ((_ extract 0 0) | |
| 165 | ((_ extract 31 0) | |
| 166 | (bvadd | |
| 167 | (bvadd | |
| 168 | ((_ zero_extend 1) rN) | |
| 169 | ((_ zero_extend 1) (bvnot rM))) | |
| 170 | ((_ zero_extend 1) #x00000001))))) | |
| 171 | (bvand #xfeffffff (bvor #x00000020 'CPSR)) | |
| 172 | 'CPSR) | |
| 173 | 'CPSR))) | |
| 174 | (ite | |
| 175 | ((_ call "arm.is_r15") rD) | |
| 176 | (ite | |
| 177 | (bveq | |
| 178 | #b0 | |
| 179 | ((_ extract 0 0) | |
| 180 | ((_ extract 31 0) | |
| 181 | (bvadd | |
| 182 | (bvadd | |
| 183 | ((_ zero_extend 1) rN) | |
| 184 | ((_ zero_extend 1) (bvnot rM))) | |
| 185 | ((_ zero_extend 1) #x00000001))))) | |
| 186 | (bvand #xfeffffff (bvor #x00000020 'CPSR)) | |
| 187 | 'CPSR) | |
| 188 | 'CPSR)) | |
| 189 | 'CPSR)) | |
| 190 | (rD | |
| 191 | (ite | |
| 192 | (ite | |
| 193 | (andp (bveq #b1 ((_ extract 0 0) predBits)) (bvne predBits #xf)) | |
| 194 | (notp | |
| 195 | (ite | |
| 196 | (bveq ((_ extract 3 1) predBits) #b000) | |
| 197 | (bveq #b1 ((_ extract 30 30) 'CPSR)) | |
| 198 | (ite | |
| 199 | (bveq ((_ extract 3 1) predBits) #b001) | |
| 200 | (bveq #b1 ((_ extract 29 29) 'CPSR)) | |
| 201 | (ite | |
| 202 | (bveq ((_ extract 3 1) predBits) #b010) | |
| 203 | (bveq #b1 ((_ extract 31 31) 'CPSR)) | |
| 204 | (ite | |
| 205 | (bveq ((_ extract 3 1) predBits) #b011) | |
| 206 | (bveq #b1 ((_ extract 28 28) 'CPSR)) | |
| 207 | (ite | |
| 208 | (bveq ((_ extract 3 1) predBits) #b100) | |
| 209 | (andp | |
| 210 | (bveq #b1 ((_ extract 29 29) 'CPSR)) | |
| 211 | (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) | |
| 212 | (ite | |
| 213 | (bveq ((_ extract 3 1) predBits) #b101) | |
| 214 | (bveq | |
| 215 | ((_ extract 31 31) 'CPSR) | |
| 216 | ((_ extract 28 28) 'CPSR)) | |
| 217 | (ite | |
| 218 | (bveq ((_ extract 3 1) predBits) #b110) | |
| 219 | (andp | |
| 220 | (bveq | |
| 221 | ((_ extract 31 31) 'CPSR) | |
| 222 | ((_ extract 28 28) 'CPSR)) | |
| 223 | (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) | |
| 224 | (bveq #b0 #b0))))))))) | |
| 225 | (ite | |
| 226 | (bveq ((_ extract 3 1) predBits) #b000) | |
| 227 | (bveq #b1 ((_ extract 30 30) 'CPSR)) | |
| 228 | (ite | |
| 229 | (bveq ((_ extract 3 1) predBits) #b001) | |
| 230 | (bveq #b1 ((_ extract 29 29) 'CPSR)) | |
| 231 | (ite | |
| 232 | (bveq ((_ extract 3 1) predBits) #b010) | |
| 233 | (bveq #b1 ((_ extract 31 31) 'CPSR)) | |
| 234 | (ite | |
| 235 | (bveq ((_ extract 3 1) predBits) #b011) | |
| 236 | (bveq #b1 ((_ extract 28 28) 'CPSR)) | |
| 237 | (ite | |
| 238 | (bveq ((_ extract 3 1) predBits) #b100) | |
| 239 | (andp | |
| 240 | (bveq #b1 ((_ extract 29 29) 'CPSR)) | |
| 241 | (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) | |
| 242 | (ite | |
| 243 | (bveq ((_ extract 3 1) predBits) #b101) | |
| 244 | (bveq | |
| 245 | ((_ extract 31 31) 'CPSR) | |
| 246 | ((_ extract 28 28) 'CPSR)) | |
| 247 | (ite | |
| 248 | (bveq ((_ extract 3 1) predBits) #b110) | |
| 249 | (andp | |
| 250 | (bveq | |
| 251 | ((_ extract 31 31) 'CPSR) | |
| 252 | ((_ extract 28 28) 'CPSR)) | |
| 253 | (notp (bveq #b1 ((_ extract 30 30) 'CPSR)))) | |
| 254 | (bveq #b0 #b0))))))))) | |
| 255 | (ite | |
| 256 | ((_ call "arm.is_r15") rD) | |
| 257 | rD | |
| 258 | ((_ extract 31 0) | |
| 259 | (bvadd | |
| 260 | (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM))) | |
| 261 | ((_ zero_extend 1) #x00000001)))) | |
| 262 | rD))))) |
| 1 | ((operands ((rT . 'Gprc) (rA . 'Gprc))) (in (rA 'IP)) (defs ((rT rA) ('IP (bvadd 'IP #x00000004)))))⏎ |