gdritter repos s-cargot / a4202ea
Added kquick's SCargotPrintParse test suite with extra unconstrained tests Getty Ritter 6 years ago
6 changed file(s) with 571 addition(s) and 0 deletion(s). Collapse all Expand all
7373 parsec >=3.1 && <4,
7474 QuickCheck >=2.8 && <3,
7575 text >=1.2 && <2
76
77 test-suite s-cargot-printparse
78 default-language: Haskell2010
79 type: exitcode-stdio-1.0
80 hs-source-dirs: test
81 main-is: SCargotPrintParse.hs
82 build-depends: s-cargot,
83 base >=4.7 && <5,
84 parsec >=3.1 && <4,
85 HUnit >=1.6 && <1.7,
86 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
57 , TestLabel "pretty print" $
58 let pprintIt = pprintSExpr 40 Swing in TestList
59 [ TestLabel "pretty print SNil" $ "()" ~=? pprintIt SNil
60 , TestLabel "pretty print SAtom" $ "hi" ~=? pprintIt (SAtom (AIdent "hi"))
61 , TestLabel "pretty print pair" $ "(hi . world)" ~=?
62 pprintIt (SCons (SAtom (AIdent "hi")) (SAtom (AIdent "world")))
63 , TestLabel "pretty print list of 1" $ "(hi)" ~=?
64 pprintIt (SCons (SAtom (AIdent "hi")) SNil)
65 , TestLabel "pretty print list of 2" $ "(hi world)" ~=?
66 pprintIt (SCons (SAtom (AIdent "hi"))
67 (SCons (SAtom (AIdent "world"))
68 SNil))
69 , TestLabel "pretty print list of 2 pairs" $
70 "((hi . hallo) world . welt)" ~=?
71 pprintIt (SCons (SCons (SAtom (AIdent "hi"))
72 (SAtom (AIdent "hallo")))
73 (SCons (SAtom (AIdent "world"))
74 (SAtom (AIdent "welt"))))
75 , TestLabel "pretty print list of 3 ending in a pair" $
76 "(hi world hallo . welt)" ~=?
77 pprintIt (SCons (SAtom (AIdent "hi"))
78 (SCons (SAtom (AIdent "world"))
79 (SCons (SAtom (AIdent "hallo"))
80 (SAtom (AIdent "welt")))))
81 , TestLabel "pretty print list of 3" $ "(hi world hallo)" ~=?
82 pprintIt (SCons (SAtom (AIdent "hi"))
83 (SCons (SAtom (AIdent "world"))
84 (SCons (SAtom (AIdent "hallo"))
85 SNil)))
86 ]
87
88 , TestLabel "unconstrained print" $
89 let pprintIt = ucPrintSExpr Swing in TestList
90 [ TestLabel "pretty print SNil" $ "()" ~=? pprintIt SNil
91 , TestLabel "pretty print SAtom" $ "hi" ~=? pprintIt (SAtom (AIdent "hi"))
92 , TestLabel "pretty print pair" $ "(hi . world)" ~=?
93 pprintIt (SCons (SAtom (AIdent "hi")) (SAtom (AIdent "world")))
94 , TestLabel "pretty print list of 1" $ "(hi)" ~=?
95 pprintIt (SCons (SAtom (AIdent "hi")) SNil)
96 , TestLabel "pretty print list of 2" $ "(hi world)" ~=?
97 pprintIt (SCons (SAtom (AIdent "hi"))
98 (SCons (SAtom (AIdent "world"))
99 SNil))
100 , TestLabel "pretty print list of 2 pairs" $
101 "((hi . hallo)\n world\n . welt)" ~=?
102 pprintIt (SCons (SCons (SAtom (AIdent "hi"))
103 (SAtom (AIdent "hallo")))
104 (SCons (SAtom (AIdent "world"))
105 (SAtom (AIdent "welt"))))
106 , TestLabel "pretty print list of 3 ending in a pair" $
107 "(hi world hallo . welt)" ~=?
108 pprintIt (SCons (SAtom (AIdent "hi"))
109 (SCons (SAtom (AIdent "world"))
110 (SCons (SAtom (AIdent "hallo"))
111 (SAtom (AIdent "welt")))))
112 , TestLabel "pretty print list of 3" $ "(hi world hallo)" ~=?
113 pprintIt (SCons (SAtom (AIdent "hi"))
114 (SCons (SAtom (AIdent "world"))
115 (SCons (SAtom (AIdent "hallo"))
116 SNil)))
117 ]
118
119 ]
120 , TestLabel "round-trip" $ TestList $
121 concatMap (\t -> map t srcs) $
122 [ testParsePrint
123 ]
124 ]
125 if errors counts + failures counts > 0
126 then exitFailure
127 else exitSuccess
128
129
130 testParsePrint :: (String, T.Text) -> Test
131 testParsePrint (n,s) = TestList
132 [ testParseFlatPrint n s
133
134 , testParseUnconstrainedPrint Swing n s
135 , testParseUnconstrainedPrint Align n s
136
137 , testParsePPrint 80 Swing n s
138 , testParsePPrint 60 Swing n s
139 , testParsePPrint 40 Swing n s
140 , testParsePPrint 20 Swing n s
141 , testParsePPrint 15 Swing n s
142 , testParsePPrint 10 Swing n s
143
144 , testParsePPrint 80 Align n s
145 , testParsePPrint 40 Align n s
146 , testParsePPrint 10 Align n s
147 ]
148
149
150 testParseFlatPrint testName src =
151 testRoundTrip (testName <> " flat print")
152 (fromRight (error "Failed parse") . parseSExpr)
153 printSExpr
154 stripAllText
155 src
156
157 testParseUnconstrainedPrint indentStyle testName src =
158 testRoundTrip (testName <> " unconstrained print")
159 (fromRight (error "Failed parse") . parseSExpr)
160 (ucPrintSExpr indentStyle)
161 stripAllText
162 src
163
164 testParsePPrint width indentStyle testName src =
165 testRoundTrip (testName <> " pretty print")
166 (fromRight (error "Failed parse") . parseSExpr)
167 (pprintSExpr width indentStyle)
168 stripAllText
169 src
170
171 stripAllText = T.unwords . concatMap T.words . T.lines
172
173 testRoundTrip nm there back prep src = TestList
174 [ TestLabel (nm <> " round trip") $
175 TestCase $ (prep src) @=? (prep $ back $ there src)
176
177 , TestLabel (nm <> " round trip twice") $
178 TestCase $ (prep src) @=? (prep $ back $ there $ back $ there src)
179 ]
180
181
182 ------------------------------------------------------------------------
183
184 data FAtom = AIdent String
185 | AQuoted String
186 | AString String
187 | AInt Integer
188 | ABV Int Integer
189 deriving (Eq, Show)
190
191
192 string :: String -> SExpr FAtom
193 string = SAtom . AString
194
195 -- | Lift an unquoted identifier.
196 ident :: String -> SExpr FAtom
197 ident = SAtom . AIdent
198
199 -- | Lift a quoted identifier.
200 quoted :: String -> SExpr FAtom
201 quoted = SAtom . AQuoted
202
203 -- | Lift an integer.
204 int :: Integer -> SExpr FAtom
205 int = SAtom . AInt
206
207
208 printAtom :: FAtom -> T.Text
209 printAtom a =
210 case a of
211 AIdent s -> T.pack s
212 AQuoted s -> T.pack ('\'' : s)
213 AString s -> T.pack (show s)
214 AInt i -> T.pack (show i)
215 ABV w val -> formatBV w val
216
217
218 printSExpr :: SExpr FAtom -> T.Text
219 printSExpr = encodeOne (flatPrint printAtom)
220
221 pprintSExpr :: Int -> Indent -> SExpr FAtom -> T.Text
222 pprintSExpr w i = encodeOne (setIndentStrategy (const i) $
223 setMaxWidth w $
224 setIndentAmount 1 $
225 basicPrint printAtom)
226
227 ucPrintSExpr :: Indent -> SExpr FAtom -> T.Text
228 ucPrintSExpr i = encodeOne (setIndentStrategy (const i) $
229 setIndentAmount 1 $
230 unconstrainedPrint printAtom)
231
232 getIdent :: FAtom -> Maybe String
233 getIdent (AIdent s) = Just s
234 getIdent _ = Nothing
235
236 formatBV :: Int -> Integer -> T.Text
237 formatBV w val = T.pack (prefix ++ printf fmt val)
238 where
239 (prefix, fmt)
240 | w `rem` 4 == 0 = ("#x", "%0" ++ show (w `div` 4) ++ "x")
241 | otherwise = ("#b", "%0" ++ show w ++ "b")
242
243 parseIdent :: Parser String
244 parseIdent = (:) <$> first <*> P.many rest
245 where first = P.letter P.<|> P.oneOf "+-=<>_"
246 rest = P.letter P.<|> P.digit P.<|> P.oneOf "+-=<>_"
247
248 parseString :: Parser String
249 parseString = do
250 _ <- P.char '"'
251 s <- P.many (P.noneOf ['"'])
252 _ <- P.char '"'
253 return s
254
255 parseBV :: Parser (Int, Integer)
256 parseBV = P.char '#' >> ((P.char 'b' >> parseBin) P.<|> (P.char 'x' >> parseHex))
257 where parseBin = P.oneOf "10" >>= \d -> parseBin' (1, if d == '1' then 1 else 0)
258
259 parseBin' :: (Int, Integer) -> Parser (Int, Integer)
260 parseBin' (bits, x) = do
261 P.optionMaybe (P.oneOf "10") >>= \case
262 Just d -> parseBin' (bits + 1, x * 2 + (if d == '1' then 1 else 0))
263 Nothing -> return (bits, x)
264
265 parseHex = (\s -> (length s * 4, read ("0x" ++ s))) <$> P.many1 P.hexDigit
266
267 parseAtom :: Parser FAtom
268 parseAtom
269 = AIdent <$> parseIdent
270 P.<|> AQuoted <$> (P.char '\'' >> parseIdent)
271 P.<|> AString <$> parseString
272 P.<|> AInt . read <$> P.many1 P.digit
273 P.<|> uncurry ABV <$> parseBV
274
275 parserLL :: SExprParser FAtom (SExpr FAtom)
276 parserLL = withLispComments (mkParser parseAtom)
277
278 parseSExpr :: T.Text -> Either String (SExpr FAtom)
279 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)))))