s-cargot-letbind (empty) → 0.1.0.0
raw patch · 10 files changed
+976/−0 lines, 10 filesdep +HUnitdep +basedep +parsecsetup-changed
Dependencies added: HUnit, base, parsec, s-cargot, s-cargot-letbind, text
Files
- ChangeLog.md +6/−0
- LICENSE +13/−0
- Setup.hs +2/−0
- s-cargot-letbind.cabal +66/−0
- src/Data/SCargot/LetBind.hs +351/−0
- test/SCargotPrintParseLet.hs +257/−0
- test/big-sample.sexp +1/−0
- test/med-sample.sexp +17/−0
- test/med2-sample.sexp +262/−0
- test/small-sample.sexp +1/−0
+ ChangeLog.md view
@@ -0,0 +1,6 @@+# Revision history for s-cargot-letbind++## 0.1.0.0 -- 2018-02-14++ * Initial version.+
+ LICENSE view
@@ -0,0 +1,13 @@+Copyright (c) 2018 Kevin Quick++Permission to use, copy, modify, and/or distribute this software for any purpose+with or without fee is hereby granted, provided that the above copyright notice+and this permission notice appear in all copies.++THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH+REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND+FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT,+INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS+OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER+TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF+THIS SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ s-cargot-letbind.cabal view
@@ -0,0 +1,66 @@+name: s-cargot-letbind+version: 0.1.0.0+synopsis: Enables let-binding and let-expansion for s-cargot defined S-expressions.+description:++ This module allows let bindings to be introduced into the S-Expression+ syntax.+ .+ For example, instead of:+ .+ > (concat (if (enabled x) (+ (width x) (width y)) (width y))+ > " meters")+ .+ this can be re-written with let bindings:+ .+ > (let ((wy (width y))+ > (wboth (+ (width x) wy))+ > (wide (if (enabled x) wboth wy))+ > )+ > (concat wide " meters"))+ .+ As S-expressions grow larger, let-binding can help readability for+ those expressions. This module provides the 'discoverLetBindings'+ function that will convert an S-expression into one containing+ let-bound variables, and the inverse function 'letExpand' which will+ expand let-bound variables back into the expression.++homepage: https://github.com/GaloisInc/s-cargot-letbind+license: ISC+license-file: LICENSE+author: Kevin Quick+maintainer: kquick@galois.com+copyright: 2018 Kevin Quick+category: Data+build-type: Simple+extra-source-files: ChangeLog.md+ test/big-sample.sexp+ test/small-sample.sexp+ test/med-sample.sexp+ test/med2-sample.sexp+cabal-version: >=1.10++source-repository head+ type: git+ location: git://github.com/GaloisInc/s-cargot-letbind.git++library+ exposed-modules: Data.SCargot.LetBind+ build-depends: base >=4.10 && <4.11+ , s-cargot >= 0.1.0.0+ , text >=1.2 && <2+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall++test-suite s-cargot-printparselet+ default-language: Haskell2010+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: SCargotPrintParseLet.hs+ build-depends: base >=4.7 && <5+ , parsec >=3.1 && <4+ , HUnit >=1.6 && <1.7+ , s-cargot >= 0.1.0.0+ , s-cargot-letbind+ , text >=1.2 && <2
+ src/Data/SCargot/LetBind.hs view
@@ -0,0 +1,351 @@+-- | This is a helper module that enables the use of let-bound+-- variables in your S-expression.+++{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Data.SCargot.LetBind+ ( -- $intro+ -- * Automatically finding let bindings+ discoverLetBindings+ , DiscoveryGuide(..)+ , nativeGuide+ -- * Expanding+ , letExpand+ )+ where++import Control.Applicative+import qualified Data.Foldable as F+import Data.Function (on)+import Data.List (sortBy)+import Data.Maybe+import Data.Monoid+import Data.SCargot.Repr+import Data.String+import Data.Traversable ( mapAccumL )+import Data.Tuple+++-- | This object provides guidance to the 'discoverLetBindings'+-- function, establishing various parameters for the discovery+-- process.+data DiscoveryGuide a str = Guide+ { maxLetBinds :: Int -> Int+ -- ^ Maximum number of let bindings to generate. Given the+ -- total number discovered as input to allow the maximum number+ -- to be intelligently determined.++ , minExprSize :: Int+ -- ^ Minimum sexpr size to be considered for a let variable+ -- binding. Expressions shorter than this will not be+ -- let-bound.++ , allowRecursion :: Bool+ -- ^ Allow rec bindings, or just direct let bindings?++ , weighting :: SExpr a -> Int -> Int+ -- ^ Given an SExpr sub-expression and the count of occurrences+ -- of that sub-expression, return a weighting value that is used+ -- for sorting the discovered let bindings to choose the most+ -- weighty 'maxLetBinds' for substitution. A sub-expression+ -- with a weight of zero will be ignored (i.e. not let-bound);+ -- one with a weight of 1000000 or more will always be bound.++ , letMaker :: (IsString str) => str -> a+ -- ^ Called to generate the "let" statement token itself.++ , labelMaker :: (IsString str, Monoid str) => str -> SExpr a -> a+ -- ^ Called to generate the binding variable name token given+ -- the name. Passed the suggested name that will be used for+ -- this binding and also the sub-expression that will be+ -- referenced. The return will be placed in an SAtom and used+ -- as the variable to reference the bound sub-expression.++ , extractStr :: (IsString str) => a -> Maybe str+ -- ^ Called to extract a string value. The returned string should+ -- be the string that will be written when the enclosing+ -- S-expression is printed. This is used to verify that the+ -- variables names extracted for let-binding are unique with+ -- respect to all other printed references. A return value of+ -- Nothing permits continuation without uniqueness verification,+ -- but at the risk that variable names will be captured in the+ -- result.+ }+++-- | Returns a default 'DiscoveryGuide'.+nativeGuide :: (str -> a) -> (str -> SExpr a -> a) -> DiscoveryGuide a str+nativeGuide letMk labelMk = Guide { maxLetBinds = const 8+ , minExprSize = 5+ , allowRecursion = False+ , weighting = defaultWeighting+ , letMaker = letMk+ , labelMaker = labelMk+ , extractStr = const Nothing+ }+++-- | Provides a default weighting function for evaluating+-- S-expressions. The general algorithm here is:+--+-- 1. S-expressions beginning with an atom on the left probably use+-- that atom as a function name, and are therefore good+-- candidates for clarity. These sub-expressions get a baseline+-- value of 100.+--+-- 2. The frequency of occurrence matters. It is 4 times more+-- important than the size of the sub-expression.+--+-- 3. Bigger sub-expressions are better candidates than smaller+-- sub-expressions.+defaultWeighting :: SExpr a -> Int -> Int+defaultWeighting subexpr cnt =+ let h = F.length subexpr+ baseline = case subexpr of+ (SCons (SAtom _) _) -> 100+ _ -> 0+ in (baseline + h + (cnt * 4))+++-- | Called to convert a plain S-expression into one with let-bound+-- variables. The let bindings are "discovered" with the assistance+-- of the guide.+discoverLetBindings :: (Monoid str, IsString str, Show str, Eq a) =>+ DiscoveryGuide a str -> SExpr a -> SExpr a+discoverLetBindings guide inp =+ let (inpMap,annotInp) = explore guide startingLoc inp+ -- KWQ: locs rec v.s. let selections?+ locs = bestBindings guide annotInp $ points inpMap+ lbn = assignLBNames guide inp locs+ -- varNameCollisions = verifyNamesUnique guide lbn inp+ letPart = SAtom $ letMaker guide "let"+ (lbvdefs, subsInp) = substLBRefs guide lbn annotInp+ in SCons letPart $ SCons lbvdefs (SCons subsInp SNil)+ -- in if null varNameCollisions+ -- then SCons letPart $ SCons lbvdefs (SCons subsInp SNil)+ -- else error $ "Let-bound variable name collisions: " <> show varNameCollisions++{- $intro++This module allows let bindings to be introduced into the S-Expression+syntax.++For example, instead of:++> (concat (if (enabled x) (+ (width x) (width y)) (width y))+> " meters")++this can be re-written with let bindings:++> (let ((wy (width y))+> (wboth (+ (width x) wy))+> (wide (if (enabled x) wboth wy))+> )+> (concat wide " meters"))++As S-expressions grow larger, let-binding can help readability for+those expressions. This module provides the 'discoverLetBindings'+function that will convert an S-expression into one containing+let-bound variables, and the inverse function 'letExpand' which will+expand let-bound variables back into the expression.++> id = letExpand . discoverLetBindings guide++The typical use is to add let bindings before serializing to+disk, and then expand the bindings after reading from the disk but+before passing to other processing; this process allows the+application using the S-Expressions to be unaware of the let-binding+compression, although it does not obtain corresponding advantages of+the re-use of let-bound variables.++The 'discoverLetBindings' function can be called to automatically+assign let bindings based on a weighting algorithm of discovered+S-expression phrases. The discovery is guided by parameters provided+by the caller in the 'DiscoveryGuide'; this guide also provides the+functions used to create the variables and the top-level let statement+in the language of the current S-expression.++The 'weighting' function of the 'DiscoveryGuide' can be used to assign+weights to various S-expression phrases: the S-expressions with the+highest weights will be let-bound to variables (up to the+'maxLetBinds' limit). A weighting value of 0 will cause the+sub-expression to be ignored (never let-bound) and a value of >=+1000000 will *always* insert a let-binding, ignoring all other limits.++-}++alwaysBindWeight :: Int+alwaysBindWeight = 1000000++bestBindings :: DiscoveryGuide a str -> ExprInfo a -> [Location a] -> [Location a]+bestBindings guide exprs locs = getMaxBest+ where getMaxBest = head $+ -- Sometimes a lengthy binding "swallows"+ -- everything else; skipping over it would+ -- result in more available bindings. Try the+ -- first 3 combinations and take the one+ -- yielding the most bindings.+ sortBy (compare `on` length) $+ fmap getBestSkipping [0..2]+ getBestSkipping n = snd $ snd $ -- extract list of Locations+ -- determine top-set of best bindings to apply+ foldl bestB (n, (maxbinds, [])) $+ -- sorted by heaviest -> lightest+ reverse $+ sortBy (compare `on` fst) $+ filter ((/=) 0 . fst) $ -- remove weights of 0+ -- add weights+ fmap (\l -> (uncurry (weighting guide) $ lwi l, l)) $+ locs+ -- bestB picks the best N bindings, where the bindings are+ -- already sorted by weight, and optionally skipping an+ -- initial count. As an override, any binding whose weight+ -- is 1_000_000 or above is *always* included in the+ -- results.+ bestB :: (Int, (Int, [Location a]))+ -> (Int, Location a)+ -> (Int, (Int, [Location a]))+ -- ^ ((skipcnt, ?), (numRemaining, selectedBinds))+ bestB acc@(_, (numRemaining, binds)) (w,e) =+ let subs = subBindings e binds+ in if numRemaining > 0 &&+ (null subs || allowRecursion guide || w >= alwaysBindWeight)+ then addUnlessSkipping acc w e+ else acc+ subBindings x = catMaybes . fmap (isSub x)+ isSub x startingFrom = do sloc <- findLocation (locId startingFrom) exprs+ findLocation (locId x) sloc+ addUnlessSkipping (skip, (numRemaining, binds)) w e =+ let addE = (minExprSize guide, (numRemaining-1, e:binds))+ skipE = (skip-1, (numRemaining, binds))+ in if w >= alwaysBindWeight+ then addE+ else if numRemaining > 0 && skip == 0+ then addE+ else skipE+ lwi l = (locExpr l, locCount l)+ maxbinds = maxLetBinds guide (length locs)+++type LocationId = Int++data Location a = Location { locExpr :: SExpr a+ , locCount :: Int+ , locId :: LocationId+ }+ deriving Show++data NamedLoc a = NamedLoc { nlocId :: LocationId+ , nlocVar :: SExpr a+ }+ deriving Show++data MyMap a = MyMap { points :: [Location a]+ }++startingLoc :: MyMap a+startingLoc = MyMap []++-- verifyNamesUnique :: IsString str => DiscoveryGuide a str -> [NamedLoc a] -> SExpr a -> [str]+-- verifyNamesUnique guide names sexpr = foldr (checkUnique sexpr) [] names+-- where checkUnique sexpr nloc = maybe [] F. find (extractStr guide)+-- checkf = maybe ? F. find $ extractStr guide++data ExprInfo a = EINil | EIAtom a | EICons LocationId (ExprInfo a) (ExprInfo a)+++explore :: Eq a => DiscoveryGuide a str -> MyMap a -> SExpr a -> (MyMap a, ExprInfo a)+explore _ mymap SNil = (mymap, EINil)+explore _ mymap (SAtom a) = (mymap, EIAtom a)+explore guide mymap h@(SCons l r) =+ let (lc,le) = explore guide mymap l+ (rc,re) = explore guide lc r+ (hm,hi) = updateMap guide h rc+ in (hm, EICons hi le re)+++updateMap :: Eq a => DiscoveryGuide a str -> SExpr a -> MyMap a -> (MyMap a, LocationId)+updateMap guide point mymap =+ let (p, i) = addOrUpdate (points mymap)+ in (mymap { points = p }, i)+ where addOrUpdate [] = ([ Location { locExpr=point, locCount=succCnt(0), locId=lId} ], lId)+ addOrUpdate (p:ps) = let (sm,si) = addOrUpdate ps+ in if locExpr p /= point+ then (p : sm, si)+ else (p { locCount = succCnt(locCount p) } : ps, locId p)+ lId = length (points mymap)+ succCnt n = if F.length point > (minExprSize guide) then n + 1 else n -- ignore short SExprs+++findLocation :: LocationId -> ExprInfo a -> Maybe (ExprInfo a)+findLocation loc = fndLoc+ where fndLoc EINil = Nothing+ fndLoc (EIAtom _) = Nothing+ fndLoc e@(EICons el l r) = if el == loc then Just e else fndLoc l <|> fndLoc r+++assignLBNames :: (Eq a, IsString str, Monoid str) =>+ DiscoveryGuide a str -> SExpr a -> [Location a] -> [NamedLoc a]+assignLBNames guide inp = snd . mapAccumL mkNamedLoc (1::Int)+ where mkNamedLoc i l = let nm = labelMaker guide suggestedName $ locExpr l+ suggestedName = "var" <> fromString (show i)+ in case F.find ((==) nm) inp of+ Nothing -> (i+1, NamedLoc { nlocId = locId l+ , nlocVar = SAtom nm+ })+ Just _ -> mkNamedLoc (i+1) l -- collision, try another varname+++substLBRefs :: Eq a =>+ DiscoveryGuide a str -> [NamedLoc a] -> ExprInfo a+ -> (SExpr a, SExpr a)+ -- ^ (varbindings, exprwithvars)+substLBRefs _ nlocs = swap . fmap declVars . swap . subsRefs []+ where subsRefs b EINil = (b, SNil)+ subsRefs b (EIAtom a) = (b, SAtom a)+ subsRefs b (EICons i l r) = let (b',l') = subsRefs b l+ (c',r') = subsRefs b' r+ here = SCons l' r'+ in case hasBinding i of+ Nothing -> (c', here)+ Just loc -> (((nlocVar loc), here) : c', (SCons (nlocVar loc) SNil))+ hasBinding i = F.find ((==) i . nlocId) nlocs+ declVars = foldl addVar SNil . foldl addVarIfUnique []+ addVarIfUnique vl v@(vn,_) = case lookup vn vl of+ Nothing -> v : vl+ Just _ -> vl+ addVar vl (vn,vv) = SCons (SCons vn (SCons vv SNil)) vl+++-- ----------------------------------------------------------------------++-- | The 'letExpand' function is passed an S-expression that (may)+-- contain let-bound variables and will return an equivalent+-- S-expression that does not contain any let bindings, where let+-- bindings have been expanded into the expression.+letExpand :: (Eq a, Show a, Eq str, IsString str) =>+ (a -> Maybe str) -> SExpr a -> SExpr a+letExpand atomToText = findExpLet+ where findExpLet (SCons (SAtom a) (SCons lbvdefs (SCons subsInp SNil))) =+ if atomToText a == Just "let"+ then expLet lbvdefs subsInp+ else SCons (SAtom a) (SCons (findExpLet lbvdefs) (SCons (findExpLet subsInp) SNil))+ findExpLet e = e+ expLet lb = expandWith (bindings lb)+ bindings = parseVar []+ parseVar vdefs (SCons (SCons vn (SCons vv SNil)) r) = (vn, vv) : parseVar vdefs r+ parseVar vdefs SNil = vdefs+ parseVar _ e = error $ "Expected a var, got: " <> show e+ expandWith _ SNil = SNil+ expandWith vdefs e@(SCons v@(SAtom _) SNil) =+ case lookup v vdefs of+ Nothing -> e+ Just vv -> expandWith vdefs vv+ expandWith vdefs e@(SCons l r) =+ case lookup e vdefs of+ Nothing -> SCons (expandWith vdefs l) (expandWith vdefs r)+ Just vv -> expandWith vdefs vv+ expandWith _ e@(SAtom _) = e
+ test/SCargotPrintParseLet.hs view
@@ -0,0 +1,257 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE LambdaCase #-}++module Main where++import Data.Either+import Data.SCargot+import Data.SCargot.Comments+import Data.SCargot.LetBind+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++ , testParseFlatPrintLetBound False n s+ , testParseFlatPrintLetBound True n s+ , testParsePPrintLetBound 80 Align False n s+ , testParsePPrintLetBound 80 Align True n s+ , testParsePPrintLetBound 40 Swing False n s+ , testParsePPrintLetBound 40 Swing True n s+ , testParsePPrintLetBound 60 Align False n s+ , testParsePPrintLetBound 60 Align True n s+ ]+++testParseFlatPrint testName src =+ testRoundTrip (testName <> " flat print")+ (fromRight (error "Failed parse") . parseSExpr)+ printSExpr+ stripAllText+ src++testParseFlatPrintLetBound recursiveBound testName src =+ let guide = (nativeGuide AIdent (\n _ -> AIdent n)) { allowRecursion = recursiveBound }+ in testRoundTrip (testName <> " flat print")+ (discoverLetBindings guide . fromRight (error "Failed parse") . parseSExpr)+ (printSExpr . letExpand getIdent)+ stripAllText+ src++testParsePPrint width indentStyle testName src =+ testRoundTrip (testName <> " pretty print")+ (fromRight (error "Failed parse") . parseSExpr)+ (pprintSExpr width indentStyle)+ stripAllText+ src++testParsePPrintLetBound width indentStyle recursiveBound testName src =+ let guide = (nativeGuide AIdent (\n _ -> AIdent n)) { allowRecursion = recursiveBound }+ in testRoundTrip (testName <> " pretty print")+ (discoverLetBindings guide . fromRight (error "Failed parse") . parseSExpr)+ (pprintSExpr width indentStyle . letExpand getIdent)+ 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/big-sample.sexp view
@@ -0,0 +1,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)))))
+ test/med-sample.sexp view
@@ -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 view
@@ -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 view
@@ -0,0 +1,1 @@+((operands ((rT . 'Gprc) (rA . 'Gprc))) (in (rA 'IP)) (defs ((rT rA) ('IP (bvadd 'IP #x00000004)))))