gdritter repos s-cargot / d86bd85
Merge pull request #13 from aisamanra/revert-11-master Revert "Printing updates: bugfix for flat and speed for pretty" G. D. Ritter authored 6 years ago GitHub committed 6 years ago
7 changed file(s) with 42 addition(s) and 735 deletion(s). Collapse all Expand all
+42
-206
Data/SCargot/Print.hs less more
1919 , flatPrint
2020 ) where
2121
22 import Control.Applicative
2322 import Data.Monoid ((<>))
2423 import Data.Text (Text)
2524 import qualified Data.Text as T
181180 prettyPrintSExpr :: SExprPrinter a (SExpr a) -> SExpr a -> Text
182181 prettyPrintSExpr pr@SExprPrinter { .. } expr = case maxWidth of
183182 Nothing -> flatPrintSExpr (fmap atomPrinter (fromCarrier expr))
184 Just w -> indentPrintSExpr2 pr w expr
185
186 indentPrintSExpr :: SExprPrinter a (SExpr a) -> Int -> SExpr a -> Text
187 indentPrintSExpr SExprPrinter { .. } _ = pHead 0
183 Just _ -> indentPrintSExpr pr expr
184
185 indentPrintSExpr :: SExprPrinter a (SExpr a) -> SExpr a -> Text
186 indentPrintSExpr SExprPrinter { .. } = pHead 0
188187 where
189188 pHead _ SNil = "()"
190189 pHead _ (SAtom a) = atomPrinter a
219218 , T.length flat + ind > maxAmt = " " <> indented
220219 | otherwise = " " <> flat
221220
222 -- | Pretty-printing for S-Expressions. The general strategy is that
223 -- an SCons tail should either all fit on the current line, or else
224 -- each tail item should be placed on its own line with indenting.
225 -- Note that a line must print something, so while subsequent elements
226 -- will be placed on following lines, it is possible that the first
227 -- thing on a line (plus its indentation) may exceed the maxwidth.
228
229 type IndentSpec = Int
230 type Indenting = Maybe IndentSpec
231
232 data PPS = PPS { indentWc :: IndentSpec
233 , remWidth :: Int
234 , numClose :: Int
235 }
236 deriving Show
237
238 data SElem = SText Int T.Text
239 | SPair Int SElem SElem
240 | SDecl Int SElem [SElem]
241 | SJoin Int [SElem]
242 deriving (Show, Eq)
243
244 sElemSize :: SElem -> Int
245 sElemSize (SText n _) = n
246 sElemSize (SPair n _ _) = n
247 sElemSize (SDecl n _ _) = n
248 sElemSize (SJoin n _) = n
249
250 indentPrintSExpr2 :: SExprPrinter a (SExpr a) -> Int -> SExpr a -> Text
251 indentPrintSExpr2 SExprPrinter { .. } maxW sexpr =
252 let atomTextTree = selems sexpr
253 pretty = fmap addIndent $ fst $ pHead (PPS 0 maxW 0) atomTextTree
254 -- prettyWithDebug = pretty <> ["", (T.pack $ show atomTextTree)]
255 in T.unlines pretty
256 where
257 -- selems converts the (SExpr a) into an SElem, converting
258 -- individual atoms to their text format but not concerned with
259 -- other text formatting. The resulting SElem tree will be
260 -- iterated over to determine the wrapping strategy to apply.
261 selems SNil = SText 2 "()"
262 selems (SAtom a) = let p = atomPrinter a in SText (T.length p) p
263 selems (SCons l r) =
264 let l' = selems l
265 lsz = sElemSize l'
266 r' = selems r
267 rsz = sElemSize r'
268 bsz = lsz + rsz
269 in case r of
270 SNil -> SJoin lsz [l']
271 SAtom _ -> SPair bsz l' r'
272 _ -> case l of
273 SAtom _ -> case r' of
274 SJoin _ rl' -> SDecl bsz l' rl'
275 SDecl _ d dl -> SDecl bsz l' (d:dl)
276 _ -> SDecl bsz l' [r']
277 _ -> SJoin bsz $ prefixOnto l' r'
278
279 prefixOnto e (SJoin _ l) = e:l
280 prefixOnto e (SDecl _ l r) = e:l:r
281 prefixOnto e r = [e,r]
282
283 addIndent (Nothing, t) = t
284 addIndent (Just n, t) = indent n t
285
286 nextIndent = incrIndent indentAmount
287 incrIndent v n = n + v
288
289 pHead :: PPS -> SElem -> ( [(Indenting, Text)], PPS )
290 pHead pps (SText _ t) = ( [(Nothing, t)]
291 , pps { remWidth = remWidth pps - T.length t})
292 pHead pps (SPair _ e1 e2) =
293 let (t1,pps1) = pHead pps e1
294 (t2,pps2) = pTail ppsNextLine e2
295 (t3,pps3) = pTail ppsSameLine e2 -- same line
296 ppsNextLine = pps { remWidth = remWidth pps - T.length sep }
297 ppsSameLine = pps1 { remWidth = remWidth pps1 - T.length sep }
298 sep = " . "
299 t1h = head t1
300 wrapJoin i l rs = wrapT i (snd l <> sep) rs
301 sameLine l r p = (wrapJoin (indentWc pps) l r, p)
302 separateLines l r p = (wrapTWith False "(" "" (indentWc pps) "" l ++
303 wrapTWith True sep ")" (indentWc pps) "" r, p)
304 in if length t1 > 1 || remWidth pps3 < numClose pps + 5
305 then separateLines t1 t2 pps2
306 else sameLine t1h t3 pps3
307 -- An SJoin is a sequence of elements at the same rank. They are
308 -- either all placed on a single line, or one on each line.
309 pHead pps (SJoin _ []) = ( [], pps )
310 pHead pps (SJoin els others) =
311 let (t1,_) = pHead pps $ head others
312 (t3,pps3) = foldl pTail' ([], pps) others
313 pTail' :: ([(Indenting, Text)], PPS)
314 -> SElem
315 -> ([(Indenting, Text)], PPS)
316 pTail' (rl,pp) ne = let (rt,pr) = pTail pp ne
317 hrl = head rl
318 hrt = head rt
319 in if length rt == 1
320 then case length rl of
321 0 -> (rt, pr)
322 1 -> ((fst hrl, snd hrl <> " " <> snd hrt):[], pr)
323 _ -> (rl <> rt, pr)
324 else (rl <> rt, pr)
325 sameLine parts pEnd = (wrapT (indentWc ppsSame) "" parts, pEnd)
326 ppsNext = pps { indentWc = nextIndent (indentWc pps)
327 , remWidth = remWidth pps - indentAmount
328 }
329 ppsSame = pps { indentWc = nextIndent (indentWc pps)
330 , remWidth = remWidth pps - indentAmount
331 }
332 ppsMulti = pps { indentWc = nextIndent (indentWc pps)
333 , remWidth = remWidth pps - indentAmount
334 }
335 pps3' = pps3
336 separateLines elems pEnd =
337 let lr = concatMap (fst . pTail pEnd) elems
338 in (wrapTWith False "(" ")" (indentWc ppsNext) "" lr, pEnd)
339 in if els > remWidth pps3 || length t1 > 1 || remWidth pps3 < numClose pps + 5
340 then separateLines others ppsMulti
341 else sameLine t3 pps3'
342 -- For an SDecl, always put the first element on the line. If
343 -- *all* other elements fit on the same line, do that, otherwise
344 -- all other elements should appear on subsequent lines with
345 -- indentation. This will produce left-biased wrapping: wrapping
346 -- will occur near the root of the SExp tree more than at the
347 -- leaves.
348 pHead pps (SDecl els first others) =
349 let (t1,pps1) = pHead pp2 first
350 (to1,_) = pTail pps1 (head others)
351 firstPlusFits = sElemSize first + sElemSize (head others) < (remWidth pps - 4)
352 allFits = els < (remWidth pps - length others - 3)
353 tryFirstArgSameLine = case swingIndent (SCons SNil (SCons SNil SNil)) of
354 Align -> True
355 _ -> False
356 pp2 = pps { indentWc = nextIndent (indentWc pps)
357 , remWidth = remWidth pps - 1 - indentAmount
358 , numClose = numClose pps + 1
359 }
360 pp2next = pp2
361 pp2solo = pp2
362 t1h = head t1
363 pps1' = pps1 { indentWc = incrIndent (T.length (snd t1h) + 1)
364 (indentWc pps1)
365 , remWidth = remWidth pps1 - T.length (snd t1h) - 1
366 }
367 tothers = concatMap (fst . pTail pp2next) others -- multiline
368 tothers' = concatMap (fst . pTail pps1') $ tail others -- multiline from 2nd
369 (others', ppone) = foldl foldPTail ([],pps1) others -- oneline
370 (others'', ppone') = foldl foldPTail ([],pps1') $ tail others -- multiline from 2nd
371 foldPTail (tf,ppf) o = let (ot,opp) = pTail ppf o
372 tf1 = head tf
373 tr = if length ot == 1
374 then case length tf of
375 0 -> ot
376 1 -> [(fst tf1, snd tf1 <> " " <> snd (head ot))]
377 _ -> tf ++ ot
378 else tf ++ ot
379 in (tr, opp)
380 separateLines l r p =
381 let wr = if null r then []
382 else wrapTWith True "" ")" (indentWc p) "" r
383 cl = if null r then ")" else ""
384 in (wrapTWith False "(" cl (indentWc pps) "" l <> wr, pp2)
385 maybeSameLine l (r1,p1) (rn,p2) =
386 if length r1 <= 1 && remWidth p1 > numClose p1
387 then (wrapT (indentWc pps) (snd l <> " ") r1, p1)
388 else separateLines [l] rn p2
389 in if allFits && length t1 < 2
390 then maybeSameLine t1h (others',ppone) (tothers,pp2solo)
391 else if (tryFirstArgSameLine && firstPlusFits &&
392 length t1 < 2 &&
393 length to1 < 2 &&
394 not (null to1) && not (null others))
395 then maybeSameLine (fst t1h,
396 snd t1h <> " " <> snd (head to1)) (others'',ppone') (tothers',pps1')
397 else separateLines t1 tothers pp2
398
399
400 pTail = pHead
401
402
403 wrapTWith :: Bool -> T.Text -> T.Text -> IndentSpec
404 -> T.Text
405 -> [(Indenting, T.Text)]
406 -> [(Indenting, T.Text)]
407 wrapTWith isContinued st en ind hstart ts =
408 let th = head ts
409 tt = last ts
410 tb = init $ tail ts
411 tp l = (fst l <|> Just ind, snd l)
412 fi = if isContinued then Just ind else Nothing
413 in if length ts > 1
414 then (((fi, st <> hstart <> snd th) : map tp tb) ++
415 [ tp $ (fst tt, snd tt <> en) ])
416 else [(fi, st <> hstart <> snd th <> en)]
417
418 wrapT :: IndentSpec -> T.Text -> [(Indenting, T.Text)] -> [(Indenting, T.Text)]
419 wrapT = wrapTWith False "(" ")"
420
221 -- where
222 -- -- this is the base-case that knows how to print empty lists and
223 -- -- atoms
224 -- pHead _ SNil = B.fromString "()"
225 -- pHead _ (SAtom a) = B.fromText a
226 -- pHead ind (SCons x xs) = gather ind x xs id 0
227
228 -- -- otherwise, we trawl through the list grabbing every element...
229 -- gather ind h (SCons x xs) k r = gather ind h xs (k . (x:)) (r + T.length x)
230 -- gather ind h end k r = B.fromString "(" <> hd <> body <> tl <> B.fromString ")"
231 -- where
232 -- tl = case end of
233 -- SNil -> mempty
234 -- SAtom a -> B.fromString " . " <> B.fromText a
235 -- SCons _ _ -> error "[unreachable]"
236 -- hd = indentSubsequent ind [pHead (ind+1) h]
237 -- lst = k []
238 -- flat = T.unwords (map (pHead (ind+1)) lst)
239 -- headWidth = T.length hd + 1
240 -- indented =
241 -- case swingIndent h of
242 -- SwingAfter n ->
243 -- let (l, ls) = splitAt n lst
244 -- t = T.unwords (map (pHead (ind+1)) l)
245 -- ts = indentAll (ind + indentAmount)
246 -- (map (pHead (ind + indentAmount)) ls)
247 -- in t <> ts
248 -- Swing ->
249 -- indentAll (ind + indentAmount)
250 -- (map (pHead (ind + indentAmount)) lst)
251 -- Align ->
252 -- indentSubsequent (ind + headWidth + 1)
253 -- (map (pHead (ind + headWidth + 1)) lst)
254 -- body
255 -- | length lst == 0 = B.fromString ""
256 -- | Just maxAmt <- maxWidth
257 -- , T.length flat + ind > maxAmt = B.fromString " " <> indented
258 -- | otherwise = B.fromString " " <> flat
421259
422260 -- if we don't indent anything, then we can ignore a bunch of the
423261 -- details above
431269 pHead SNil =
432270 B.fromString "()"
433271
434 pTail e@(SCons _ (SAtom _)) =
435 B.fromString " " <> pHead e <> B.fromString ")"
436272 pTail (SCons x xs) =
437273 B.fromString " " <> pHead x <> pTail xs
438274 pTail (SAtom t) =
+0
-17
s-cargot.cabal less more
1919 build-type: Simple
2020 cabal-version: >=1.10
2121 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
2822
2923 source-repository head
3024 type: git
7872 parsec >=3.1 && <4,
7973 QuickCheck >=2.8 && <3,
8074 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
+0
-231
test/SCargotPrintParse.hs less more
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
+0
-1
test/big-sample.sexp less more
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)))))⏎
+0
-17
test/med-sample.sexp less more
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)))))⏎
+0
-262
test/med2-sample.sexp less more
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)))))
+0
-1
test/small-sample.sexp less more
1 ((operands ((rT . 'Gprc) (rA . 'Gprc))) (in (rA 'IP)) (defs ((rT rA) ('IP (bvadd 'IP #x00000004)))))⏎