Merge pull request #11 from kquick/master

Printing updates: bugfix for flat and speed for pretty

Data/SCargot/Print.hs

@@ -19,6 +19,7 @@ module Data.SCargot.Print
          , flatPrint
          ) where
 
+import           Control.Applicative
 import           Data.Monoid ((<>))
 import           Data.Text (Text)
 import qualified Data.Text as T
@@ -180,10 +181,10 @@ indentSubsequent n (t:ts) = joinLines (t : go ts)
 prettyPrintSExpr :: SExprPrinter a (SExpr a) -> SExpr a -> Text
 prettyPrintSExpr pr@SExprPrinter { .. } expr = case maxWidth of
   Nothing -> flatPrintSExpr (fmap atomPrinter (fromCarrier expr))
-  Just _  -> indentPrintSExpr pr expr
+  Just w  -> indentPrintSExpr2 pr w expr
 
-indentPrintSExpr :: SExprPrinter a (SExpr a) -> SExpr a -> Text
-indentPrintSExpr SExprPrinter { .. } = pHead 0
+indentPrintSExpr :: SExprPrinter a (SExpr a) -> Int -> SExpr a -> Text
+indentPrintSExpr SExprPrinter { .. } _ = pHead 0
   where
     pHead _   SNil         = "()"
     pHead _   (SAtom a)    = atomPrinter a
@@ -218,44 +219,205 @@ indentPrintSExpr SExprPrinter { .. } = pHead 0
               , T.length flat + ind > maxAmt = " " <> indented
               | otherwise = " " <> flat
 
-  -- where
-  --   -- this is the base-case that knows how to print empty lists and
-  --   -- atoms
-  --   pHead _   SNil         = B.fromString "()"
-  --   pHead _   (SAtom a)    = B.fromText a
-  --   pHead ind (SCons x xs) = gather ind x xs id 0
-
-  --   -- otherwise, we trawl through the list grabbing every element...
-  --   gather ind h (SCons x xs) k r = gather ind h xs (k . (x:)) (r + T.length x)
-  --   gather ind h end          k r = B.fromString "(" <> hd <> body <> tl <> B.fromString ")"
-  --     where
-  --       tl   = case end of
-  --                SNil      -> mempty
-  --                SAtom a   -> B.fromString " . " <> B.fromText a
-  --                SCons _ _ -> error "[unreachable]"
-  --       hd   = indentSubsequent ind [pHead (ind+1) h]
-  --       lst  = k []
-  --       flat = T.unwords (map (pHead (ind+1)) lst)
-  --       headWidth = T.length hd + 1
-  --       indented =
-  --         case swingIndent h of
-  --           SwingAfter n ->
-  --             let (l, ls) = splitAt n lst
-  --                 t  = T.unwords (map (pHead (ind+1)) l)
-  --                 ts = indentAll (ind + indentAmount)
-  --                                (map (pHead (ind + indentAmount)) ls)
-  --             in t <> ts
-  --           Swing ->
-  --             indentAll (ind + indentAmount)
-  --               (map (pHead (ind + indentAmount)) lst)
-  --           Align ->
-  --             indentSubsequent (ind + headWidth + 1)
-  --               (map (pHead (ind + headWidth + 1)) lst)
-  --       body
-  --         | length lst == 0              = B.fromString ""
-  --         | Just maxAmt <- maxWidth
-  --         , T.length flat + ind > maxAmt = B.fromString " " <> indented
-  --         | otherwise                    = B.fromString " " <> flat
+-- | Pretty-printing for S-Expressions.  The general strategy is that
+-- an SCons tail should either all fit on the current line, or else
+-- each tail item should be placed on its own line with indenting.
+-- Note that a line must print something, so while subsequent elements
+-- will be placed on following lines, it is possible that the first
+-- thing on a line (plus its indentation) may exceed the maxwidth.
+
+type IndentSpec = Int
+type Indenting = Maybe IndentSpec
+
+data PPS = PPS { indentWc :: IndentSpec
+               , remWidth :: Int
+               , numClose :: Int
+               }
+         deriving Show
+
+data SElem = SText Int T.Text
+           | SPair Int SElem SElem
+           | SDecl Int SElem [SElem]
+           | SJoin Int [SElem]
+             deriving (Show, Eq)
+
+sElemSize :: SElem -> Int
+sElemSize (SText n _) = n
+sElemSize (SPair n _ _) = n
+sElemSize (SDecl n _ _) = n
+sElemSize (SJoin n _) = n
+
+indentPrintSExpr2 :: SExprPrinter a (SExpr a) -> Int -> SExpr a -> Text
+indentPrintSExpr2 SExprPrinter { .. } maxW sexpr =
+    let atomTextTree = selems sexpr
+        pretty = fmap addIndent $ fst $ pHead (PPS 0 maxW 0) atomTextTree
+        -- prettyWithDebug = pretty <> ["", (T.pack $ show atomTextTree)]
+    in T.unlines pretty
+  where
+    -- selems converts the (SExpr a) into an SElem, converting
+    -- individual atoms to their text format but not concerned with
+    -- other text formatting.  The resulting SElem tree will be
+    -- iterated over to determine the wrapping strategy to apply.
+    selems SNil = SText 2 "()"
+    selems (SAtom a) = let p = atomPrinter a in SText (T.length p) p
+    selems (SCons l r) =
+        let l' = selems l
+            lsz = sElemSize l'
+            r' = selems r
+            rsz = sElemSize r'
+            bsz = lsz + rsz
+        in case r of
+             SNil -> SJoin lsz [l']
+             SAtom _ -> SPair bsz l' r'
+             _ -> case l of
+                    SAtom _ -> case r' of
+                                 SJoin _ rl' -> SDecl bsz l' rl'
+                                 SDecl _ d dl -> SDecl bsz l' (d:dl)
+                                 _ -> SDecl bsz l' [r']
+                    _ -> SJoin bsz $ prefixOnto l' r'
+
+    prefixOnto e (SJoin _ l) = e:l
+    prefixOnto e (SDecl _ l r) = e:l:r
+    prefixOnto e r = [e,r]
+
+    addIndent (Nothing, t) = t
+    addIndent (Just n, t) = indent n t
+
+    nextIndent = incrIndent indentAmount
+    incrIndent v n = n + v
+
+    pHead :: PPS -> SElem -> ( [(Indenting, Text)], PPS )
+    pHead pps (SText _ t) = ( [(Nothing, t)]
+                            , pps { remWidth = remWidth pps - T.length t})
+    pHead pps (SPair _ e1 e2) =
+        let (t1,pps1) = pHead pps e1
+            (t2,pps2) = pTail ppsNextLine e2
+            (t3,pps3) = pTail ppsSameLine e2  -- same line
+            ppsNextLine = pps { remWidth = remWidth pps - T.length sep }
+            ppsSameLine = pps1 { remWidth = remWidth pps1 - T.length sep }
+            sep = " . "
+            t1h = head t1
+            wrapJoin i l rs = wrapT i (snd l <> sep) rs
+            sameLine l r p = (wrapJoin (indentWc pps) l r, p)
+            separateLines l r p = (wrapTWith False "(" "" (indentWc pps) "" l ++
+                                   wrapTWith True sep ")" (indentWc pps) "" r, p)
+        in if length t1 > 1 || remWidth pps3 < numClose pps + 5
+           then separateLines t1 t2 pps2
+           else sameLine t1h t3 pps3
+    -- An SJoin is a sequence of elements at the same rank.  They are
+    -- either all placed on a single line, or one on each line.
+    pHead pps (SJoin _ []) = ( [], pps )
+    pHead pps (SJoin els others) =
+        let (t1,_) = pHead pps $ head others
+            (t3,pps3) = foldl pTail' ([], pps) others
+            pTail' :: ([(Indenting, Text)], PPS)
+                   -> SElem
+                   -> ([(Indenting, Text)], PPS)
+            pTail' (rl,pp) ne = let (rt,pr) = pTail pp ne
+                                    hrl = head rl
+                                    hrt = head rt
+                                in if length rt == 1
+                                   then case length rl of
+                                          0 -> (rt, pr)
+                                          1 -> ((fst hrl, snd hrl <> " " <> snd hrt):[], pr)
+                                          _ -> (rl <> rt, pr)
+                                   else (rl <> rt, pr)
+            sameLine parts pEnd = (wrapT (indentWc ppsSame) "" parts, pEnd)
+            ppsNext = pps { indentWc = nextIndent (indentWc pps)
+                          , remWidth = remWidth pps - indentAmount
+                          }
+            ppsSame = pps { indentWc = nextIndent (indentWc pps)
+                          , remWidth = remWidth pps - indentAmount
+                          }
+            ppsMulti = pps { indentWc = nextIndent (indentWc pps)
+                           , remWidth = remWidth pps - indentAmount
+                           }
+            pps3' = pps3
+            separateLines elems pEnd =
+                let lr = concatMap (fst . pTail pEnd) elems
+                in (wrapTWith False "(" ")" (indentWc ppsNext) "" lr, pEnd)
+        in if els > remWidth pps3 || length t1 > 1 || remWidth pps3 < numClose pps + 5
+           then separateLines others ppsMulti
+           else sameLine t3 pps3'
+    --  For an SDecl, always put the first element on the line.  If
+    --  *all* other elements fit on the same line, do that, otherwise
+    --  all other elements should appear on subsequent lines with
+    --  indentation.  This will produce left-biased wrapping: wrapping
+    --  will occur near the root of the SExp tree more than at the
+    --  leaves.
+    pHead pps (SDecl els first others) =
+        let (t1,pps1) = pHead pp2 first
+            (to1,_) = pTail pps1 (head others)
+            firstPlusFits = sElemSize first + sElemSize (head others) < (remWidth pps - 4)
+            allFits = els < (remWidth pps - length others - 3)
+            tryFirstArgSameLine = case swingIndent (SCons SNil (SCons SNil SNil)) of
+                                    Align -> True
+                                    _ -> False
+            pp2 = pps { indentWc = nextIndent (indentWc pps)
+                      , remWidth = remWidth pps - 1 - indentAmount
+                      , numClose = numClose pps + 1
+                      }
+            pp2next = pp2
+            pp2solo = pp2
+            t1h = head t1
+            pps1' = pps1 { indentWc = incrIndent (T.length (snd t1h) + 1)
+                                                 (indentWc pps1)
+                         , remWidth = remWidth pps1 - T.length (snd t1h) - 1
+                         }
+            tothers = concatMap (fst . pTail pp2next) others -- multiline
+            tothers' = concatMap (fst . pTail pps1') $ tail others -- multiline from 2nd
+            (others', ppone) = foldl foldPTail ([],pps1) others -- oneline
+            (others'', ppone') = foldl foldPTail ([],pps1') $ tail others -- multiline from 2nd
+            foldPTail (tf,ppf) o = let (ot,opp) = pTail ppf o
+                                       tf1 = head tf
+                                       tr = if length ot == 1
+                                            then case length tf of
+                                                   0 -> ot
+                                                   1 -> [(fst tf1, snd tf1 <> " " <> snd (head ot))]
+                                                   _ -> tf ++ ot
+                                            else tf ++ ot
+                                   in (tr, opp)
+            separateLines l r p =
+                let wr = if null r then []
+                         else wrapTWith True "" ")" (indentWc p) "" r
+                    cl = if null r then ")" else ""
+                in (wrapTWith False "(" cl (indentWc pps) "" l <> wr, pp2)
+            maybeSameLine l (r1,p1) (rn,p2) =
+                if length r1 <= 1 && remWidth p1 > numClose p1
+                then (wrapT (indentWc pps) (snd l <> " ") r1, p1)
+                else separateLines [l] rn p2
+        in if allFits && length t1 < 2
+           then maybeSameLine t1h (others',ppone) (tothers,pp2solo)
+           else if (tryFirstArgSameLine && firstPlusFits &&
+                    length t1 < 2 &&
+                    length to1 < 2 &&
+                    not (null to1) && not (null others))
+                then maybeSameLine (fst t1h,
+                                    snd t1h <> " " <> snd (head to1)) (others'',ppone') (tothers',pps1')
+                else separateLines t1 tothers pp2
+
+
+    pTail = pHead
+
+
+wrapTWith :: Bool -> T.Text -> T.Text -> IndentSpec
+          -> T.Text
+          -> [(Indenting, T.Text)]
+          -> [(Indenting, T.Text)]
+wrapTWith isContinued st en ind hstart ts =
+    let th = head ts
+        tt = last ts
+        tb = init $ tail ts
+        tp l = (fst l <|> Just ind, snd l)
+        fi = if isContinued then Just ind else Nothing
+    in if length ts > 1
+       then (((fi, st <> hstart <> snd th) : map tp tb) ++
+             [ tp $ (fst tt, snd tt <> en) ])
+       else [(fi, st <> hstart <> snd th <> en)]
+
+wrapT :: IndentSpec -> T.Text -> [(Indenting, T.Text)] -> [(Indenting, T.Text)]
+wrapT = wrapTWith False "(" ")"
+
 
 -- if we don't indent anything, then we can ignore a bunch of the
 -- details above
@@ -269,6 +431,8 @@ flatPrintSExpr = TL.toStrict . B.toLazyText . pHead
     pHead SNil         =
       B.fromString "()"
 
+    pTail e@(SCons _ (SAtom _)) =
+        B.fromString " " <> pHead e <> B.fromString ")"
     pTail (SCons x xs) =
       B.fromString " " <> pHead x <> pTail xs
     pTail (SAtom t) =

s-cargot.cabal

@@ -20,6 +20,12 @@ build-type:          Simple
 cabal-version:       >=1.10
 bug-reports:         https://github.com/aisamanra/s-cargot/issues
 
+
+extra-source-files:  test/big-sample.sexp
+                   , test/med-sample.sexp
+                   , test/med2-sample.sexp
+                   , test/small-sample.sexp
+
 source-repository head
   type: git
   location: git://github.com/aisamanra/s-cargot.git
@@ -72,3 +78,14 @@ test-suite s-cargot-qc
                     parsec        >=3.1 && <4,
                     QuickCheck    >=2.8 && <3,
                     text          >=1.2 && <2
+
+test-suite s-cargot-printparse
+  default-language: Haskell2010
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   test
+  main-is:          SCargotPrintParse.hs
+  build-depends:    s-cargot,
+                    base          >=4.7 && <5,
+                    parsec        >=3.1 && <4,
+                    HUnit         >=1.6 && <1.7,
+                    text          >=1.2 && <2

test/SCargotPrintParse.hs

@@ -0,0 +1,231 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Main where
+
+import           Data.Either
+import           Data.SCargot
+import           Data.SCargot.Comments
+import           Data.SCargot.Repr
+import           Data.Semigroup
+import qualified Data.Text as T
+import qualified Data.Text.IO as TIO
+import           System.Exit
+import           Test.HUnit
+import           Text.Parsec as P
+import           Text.Parsec.Text (Parser)
+import           Text.Printf ( printf )
+
+
+main = do
+  putStrLn "Parsing a large S-expression"
+  srcs <- mapM (\n -> (,) n <$> TIO.readFile n) [ "test/small-sample.sexp"
+                                                , "test/med-sample.sexp"
+                                                , "test/med2-sample.sexp"
+                                                , "test/big-sample.sexp"
+                                                ]
+  counts <- runTestTT $ TestList
+            [ TestLabel "basic checks" $ TestList
+              [ TestLabel "flat print" $ TestList
+                [ TestLabel "flatprint SNil" $ "()" ~=? printSExpr SNil
+                , TestLabel "flatprint SAtom" $ "hi" ~=? printSExpr (SAtom (AIdent "hi"))
+                , TestLabel "flatprint pair" $ "(hi . world)" ~=?
+                  printSExpr (SCons (SAtom (AIdent "hi")) (SAtom (AIdent "world")))
+                , TestLabel "flatprint list of 1" $ "(hi)" ~=?
+                  printSExpr (SCons (SAtom (AIdent "hi")) SNil)
+                , TestLabel "flatprint list of 2" $ "(hi world)" ~=?
+                  printSExpr (SCons (SAtom (AIdent "hi"))
+                                    (SCons (SAtom (AIdent "world"))
+                                           SNil))
+                , TestLabel "flatprint list of 2 pairs" $ "((hi . hallo) (world . welt))" ~=?
+                  printSExpr (SCons (SCons (SAtom (AIdent "hi"))
+                                           (SAtom (AIdent "hallo")))
+                                    (SCons (SAtom (AIdent "world"))
+                                           (SAtom (AIdent "welt"))))
+                , TestLabel "flatprint list of 3 ending in a pair" $ "(hi world (hallo . welt))" ~=?
+                  printSExpr (SCons (SAtom (AIdent "hi"))
+                                    (SCons (SAtom (AIdent "world"))
+                                           (SCons (SAtom (AIdent "hallo"))
+                                                  (SAtom (AIdent "welt")))))
+                , TestLabel "flatprint list of 3" $ "(hi world hallo)" ~=?
+                  printSExpr (SCons (SAtom (AIdent "hi"))
+                                    (SCons (SAtom (AIdent "world"))
+                                           (SCons (SAtom (AIdent "hallo"))
+                                                  SNil)))
+                ]
+              , TestLabel "pretty print" $
+                let pprintIt = pprintSExpr 40 Swing in TestList
+                [ TestLabel "pretty print SNil" $ "()\n" ~=? pprintIt SNil
+                , TestLabel "pretty print SAtom" $ "hi\n" ~=? pprintIt (SAtom (AIdent "hi"))
+                , TestLabel "pretty print pair" $ "(hi . world)\n" ~=?
+                  pprintIt (SCons (SAtom (AIdent "hi")) (SAtom (AIdent "world")))
+                , TestLabel "pretty print list of 1" $ "(hi)\n" ~=?
+                  pprintIt (SCons (SAtom (AIdent "hi")) SNil)
+                , TestLabel "pretty print list of 2" $ "(hi world)\n" ~=?
+                  pprintIt (SCons (SAtom (AIdent "hi"))
+                                  (SCons (SAtom (AIdent "world"))
+                                         SNil))
+                , TestLabel "pretty print list of 2 pairs" $
+                  "((hi . hallo) (world . welt))\n" ~=?
+                  pprintIt (SCons (SCons (SAtom (AIdent "hi"))
+                                         (SAtom (AIdent "hallo")))
+                                  (SCons (SAtom (AIdent "world"))
+                                         (SAtom (AIdent "welt"))))
+                , TestLabel "pretty print list of 3 ending in a pair" $
+                  "(hi world (hallo . welt))\n" ~=?
+                  pprintIt (SCons (SAtom (AIdent "hi"))
+                                  (SCons (SAtom (AIdent "world"))
+                                         (SCons (SAtom (AIdent "hallo"))
+                                                (SAtom (AIdent "welt")))))
+                , TestLabel "pretty print list of 3" $ "(hi world hallo)\n" ~=?
+                  pprintIt (SCons (SAtom (AIdent "hi"))
+                                  (SCons (SAtom (AIdent "world"))
+                                         (SCons (SAtom (AIdent "hallo"))
+                                                SNil)))
+                ]
+              ]
+            , TestLabel "round-trip" $ TestList $
+              concatMap (\t -> map t srcs) $
+              [ testParsePrint
+              ]
+            ]
+  if errors counts + failures counts > 0
+  then exitFailure
+  else exitSuccess
+
+
+testParsePrint :: (String, T.Text) -> Test
+testParsePrint (n,s) = TestList
+                       [ testParseFlatPrint n s
+
+                       , testParsePPrint 80 Swing n s
+                       , testParsePPrint 60 Swing n s
+                       , testParsePPrint 40 Swing n s
+                       , testParsePPrint 20 Swing n s
+                       , testParsePPrint 15 Swing n s
+                       , testParsePPrint 10 Swing n s
+
+                       , testParsePPrint 80 Align n s
+                       , testParsePPrint 40 Align n s
+                       , testParsePPrint 10 Align n s
+                       ]
+
+
+testParseFlatPrint testName src =
+    testRoundTrip (testName <> " flat print")
+                      (fromRight (error "Failed parse") . parseSExpr)
+                      printSExpr
+                      stripAllText
+                      src
+
+testParsePPrint width indentStyle testName src =
+    testRoundTrip (testName <> " pretty print")
+                      (fromRight (error "Failed parse") . parseSExpr)
+                      (pprintSExpr width indentStyle)
+                      stripAllText
+                      src
+
+stripAllText = T.unwords . concatMap T.words . T.lines
+
+testRoundTrip nm there back prep src = TestList
+  [ TestLabel (nm <> " round trip") $
+    TestCase $ (prep src) @=? (prep $ back $ there src)
+
+  , TestLabel (nm <> " round trip twice") $
+    TestCase $ (prep src) @=? (prep $ back $ there $ back $ there src)
+  ]
+
+
+------------------------------------------------------------------------
+
+data FAtom = AIdent String
+           | AQuoted String
+           | AString String
+           | AInt Integer
+           | ABV Int Integer
+           deriving (Eq, Show)
+
+
+string :: String -> SExpr FAtom
+string = SAtom . AString
+
+-- | Lift an unquoted identifier.
+ident :: String -> SExpr FAtom
+ident = SAtom . AIdent
+
+-- | Lift a quoted identifier.
+quoted :: String -> SExpr FAtom
+quoted = SAtom . AQuoted
+
+-- | Lift an integer.
+int :: Integer -> SExpr FAtom
+int = SAtom . AInt
+
+
+printAtom :: FAtom -> T.Text
+printAtom a =
+  case a of
+    AIdent s -> T.pack s
+    AQuoted s -> T.pack ('\'' : s)
+    AString s -> T.pack (show s)
+    AInt i -> T.pack (show i)
+    ABV w val -> formatBV w val
+
+
+printSExpr :: SExpr FAtom -> T.Text
+printSExpr = encodeOne (flatPrint printAtom)
+
+pprintSExpr :: Int -> Indent -> SExpr FAtom -> T.Text
+pprintSExpr w i = encodeOne (setIndentStrategy (const i) $
+                             setMaxWidth w $
+                             setIndentAmount 1 $
+                             basicPrint printAtom)
+
+getIdent :: FAtom -> Maybe String
+getIdent (AIdent s) = Just s
+getIdent _ = Nothing
+
+formatBV :: Int -> Integer -> T.Text
+formatBV w val = T.pack (prefix ++ printf fmt val)
+  where
+    (prefix, fmt)
+      | w `rem` 4 == 0 = ("#x", "%0" ++ show (w `div` 4) ++ "x")
+      | otherwise = ("#b", "%0" ++ show w ++ "b")
+
+parseIdent :: Parser String
+parseIdent = (:) <$> first <*> P.many rest
+  where first = P.letter P.<|> P.oneOf "+-=<>_"
+        rest = P.letter P.<|> P.digit P.<|> P.oneOf "+-=<>_"
+
+parseString :: Parser String
+parseString = do
+  _ <- P.char '"'
+  s <- P.many (P.noneOf ['"'])
+  _ <- P.char '"'
+  return s
+
+parseBV :: Parser (Int, Integer)
+parseBV = P.char '#' >> ((P.char 'b' >> parseBin) P.<|> (P.char 'x' >> parseHex))
+  where parseBin = P.oneOf "10" >>= \d -> parseBin' (1, if d == '1' then 1 else 0)
+
+        parseBin' :: (Int, Integer) -> Parser (Int, Integer)
+        parseBin' (bits, x) = do
+          P.optionMaybe (P.oneOf "10") >>= \case
+            Just d -> parseBin' (bits + 1, x * 2 + (if d == '1' then 1 else 0))
+            Nothing -> return (bits, x)
+
+        parseHex = (\s -> (length s * 4, read ("0x" ++ s))) <$> P.many1 P.hexDigit
+
+parseAtom :: Parser FAtom
+parseAtom
+  =   AIdent      <$> parseIdent
+  P.<|> AQuoted     <$> (P.char '\'' >> parseIdent)
+  P.<|> AString     <$> parseString
+  P.<|> AInt . read <$> P.many1 P.digit
+  P.<|> uncurry ABV <$> parseBV
+
+parserLL :: SExprParser FAtom (SExpr FAtom)
+parserLL = withLispComments (mkParser parseAtom)
+
+parseSExpr :: T.Text -> Either String (SExpr FAtom)
+parseSExpr = decodeOne parserLL

test/med-sample.sexp

@@ -0,0 +1,17 @@
+((operands ((rA . 'Gprc) (rS . 'Gprc) (rB . 'Gprc))) 
+  (in ('XER 'CR rB rS 'IP))
+  (defs 
+    (('CR 
+       (bvor 
+         (bvand 
+           'CR
+           (bvnot (bvshl #x0000000f (bvmul ((_ zero_extend 29) #b000) #x00000004))))
+         (bvshl 
+           ((_ zero_extend 28) 
+             (concat 
+               (ite 
+                 (bvslt (bvxor rS rB) #x00000000)
+                 #b100
+                 (ite (bvsgt (bvxor rS rB) #x00000000) #b010 #b001))
+               ((_ extract 0 0) 'XER)))
+           (bvmul ((_ zero_extend 29) #b000) #x00000004)))) (rA (bvxor rS rB)) ('IP (bvadd 'IP #x00000004)))))

test/med2-sample.sexp

@@ -0,0 +1,262 @@
+((operands
+ ((rD . 'GPR)
+ (setcc . 'Cc_out)
+ (predBits . 'Pred)
+ (rM . 'GPR)
+ (rN . 'GPR)))
+(in (setcc rN rM '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) (bvnot rM)))
+      ((_ zero_extend 1) #x00000001)))))
+    (bvand
+     #xfffffffe
+     ((_ extract 31 0)
+     (bvadd
+      (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM)))
+      ((_ zero_extend 1) #x00000001))))
+    (ite
+     (bveq
+      #b0
+      ((_ extract 1 1)
+      ((_ extract 31 0)
+      (bvadd
+       (bvadd
+        ((_ zero_extend 1) rN)
+        ((_ zero_extend 1) (bvnot rM)))
+       ((_ zero_extend 1) #x00000001)))))
+     (bvand
+      #xfffffffd
+      ((_ extract 31 0)
+      (bvadd
+       (bvadd
+        ((_ zero_extend 1) rN)
+        ((_ zero_extend 1) (bvnot rM)))
+       ((_ zero_extend 1) #x00000001))))
+     ((_ extract 31 0)
+     (bvadd
+      (bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM)))
+      ((_ zero_extend 1) #x00000001)))))
+   (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) (bvnot rM)))
+       ((_ zero_extend 1) #x00000001))))
+      (concat
+       (ite
+        (bveq
+         ((_ extract 31 0)
+         (bvadd
+          (bvadd
+           ((_ zero_extend 1) rN)
+           ((_ zero_extend 1) (bvnot rM)))
+          ((_ zero_extend 1) #x00000001)))
+         #x00000000)
+        #b1
+        #b0)
+       (concat
+        ((_ extract 32 32)
+        (bvadd
+         (bvadd
+          ((_ zero_extend 1) rN)
+          ((_ zero_extend 1) (bvnot rM)))
+         ((_ zero_extend 1) #x00000001)))
+        (bvand
+         ((_ extract 31 31)
+         ((_ extract 31 0)
+         (bvadd
+          (bvadd
+           ((_ zero_extend 1) rN)
+           ((_ zero_extend 1) (bvnot rM)))
+          ((_ zero_extend 1) #x00000001))))
+         ((_ extract 32 32)
+         (bvadd
+          (bvadd
+           ((_ zero_extend 1) rN)
+           ((_ zero_extend 1) (bvnot rM)))
+          ((_ zero_extend 1) #x00000001)))))))
+     ((_ 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) (bvnot rM)))
+         ((_ zero_extend 1) #x00000001)))))
+       (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) (bvnot rM)))
+        ((_ zero_extend 1) #x00000001)))))
+      (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) (bvnot rM)))
+     ((_ zero_extend 1) #x00000001))))
+   rD)))))

test/small-sample.sexp

@@ -0,0 +1 @@
+((operands ((rT . 'Gprc) (rA . 'Gprc))) (in (rA 'IP)) (defs ((rT rA) ('IP (bvadd 'IP #x00000004)))))