diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,6 @@ +# Revision history for s-cargot-letbind + +## 0.1.0.0 -- 2018-02-14 + + * Initial version. + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/s-cargot-letbind.cabal b/s-cargot-letbind.cabal new file mode 100644 --- /dev/null +++ b/s-cargot-letbind.cabal @@ -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 diff --git a/src/Data/SCargot/LetBind.hs b/src/Data/SCargot/LetBind.hs new file mode 100644 --- /dev/null +++ b/src/Data/SCargot/LetBind.hs @@ -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 diff --git a/test/SCargotPrintParseLet.hs b/test/SCargotPrintParseLet.hs new file mode 100644 --- /dev/null +++ b/test/SCargotPrintParseLet.hs @@ -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 diff --git a/test/big-sample.sexp b/test/big-sample.sexp new file mode 100644 --- /dev/null +++ b/test/big-sample.sexp @@ -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))))) diff --git a/test/med-sample.sexp b/test/med-sample.sexp new file mode 100644 --- /dev/null +++ b/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))))) diff --git a/test/med2-sample.sexp b/test/med2-sample.sexp new file mode 100644 --- /dev/null +++ b/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))))) diff --git a/test/small-sample.sexp b/test/small-sample.sexp new file mode 100644 --- /dev/null +++ b/test/small-sample.sexp @@ -0,0 +1,1 @@ +((operands ((rT . 'Gprc) (rA . 'Gprc))) (in (rA 'IP)) (defs ((rT rA) ('IP (bvadd 'IP #x00000004)))))