{-# Language DataKinds #-}
{-# Language GADTs #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
module EVM.Solvers where
import Prelude hiding (LT, GT)
import GHC.Natural
import Control.Monad
import GHC.IO.Handle (Handle, hFlush, hSetBuffering, BufferMode(..))
import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
import Control.Concurrent (forkIO, killThread)
import Control.Monad.State.Strict
import Data.Char (isSpace)
import Data.Maybe (fromMaybe)
import Data.Text.Lazy (Text)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Text as TS
import qualified Data.Text.Lazy as T
import qualified Data.Text.Lazy.IO as T
import Data.Text.Lazy.Builder
import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))
import EVM.SMT
import EVM.Types
data Solver
= Z3
| CVC5
| Bitwuzla
| Custom Text
instance Show Solver where
show :: Solver -> String
show Solver
Z3 = String
"z3"
show Solver
CVC5 = String
"cvc5"
show Solver
Bitwuzla = String
"bitwuzla"
show (Custom Text
s) = Text -> String
T.unpack Text
s
data SolverInstance = SolverInstance
{ SolverInstance -> Solver
solvertype :: Solver
, SolverInstance -> Handle
stdin :: Handle
, SolverInstance -> Handle
stdout :: Handle
, SolverInstance -> Handle
stderr :: Handle
, SolverInstance -> ProcessHandle
process :: ProcessHandle
}
newtype SolverGroup = SolverGroup (Chan Task)
data Task = Task
{ Task -> SMT2
script :: SMT2
, Task -> Chan CheckSatResult
resultChan :: Chan CheckSatResult
}
data CheckSatResult
= Sat SMTCex
| Unsat
| Unknown
| Error TS.Text
deriving (Int -> CheckSatResult -> ShowS
[CheckSatResult] -> ShowS
CheckSatResult -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CheckSatResult] -> ShowS
$cshowList :: [CheckSatResult] -> ShowS
show :: CheckSatResult -> String
$cshow :: CheckSatResult -> String
showsPrec :: Int -> CheckSatResult -> ShowS
$cshowsPrec :: Int -> CheckSatResult -> ShowS
Show, CheckSatResult -> CheckSatResult -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CheckSatResult -> CheckSatResult -> Bool
$c/= :: CheckSatResult -> CheckSatResult -> Bool
== :: CheckSatResult -> CheckSatResult -> Bool
$c== :: CheckSatResult -> CheckSatResult -> Bool
Eq)
isSat :: CheckSatResult -> Bool
isSat :: CheckSatResult -> Bool
isSat (Sat SMTCex
_) = Bool
True
isSat CheckSatResult
_ = Bool
False
isErr :: CheckSatResult -> Bool
isErr :: CheckSatResult -> Bool
isErr (Error Text
_) = Bool
True
isErr CheckSatResult
_ = Bool
False
isUnsat :: CheckSatResult -> Bool
isUnsat :: CheckSatResult -> Bool
isUnsat CheckSatResult
Unsat = Bool
True
isUnsat CheckSatResult
_ = Bool
False
checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
checkSat (SolverGroup Chan Task
taskQueue) SMT2
script = do
Chan CheckSatResult
resChan <- forall a. IO (Chan a)
newChan
forall a. Chan a -> a -> IO ()
writeChan Chan Task
taskQueue (SMT2 -> Chan CheckSatResult -> Task
Task SMT2
script Chan CheckSatResult
resChan)
forall a. Chan a -> IO a
readChan Chan CheckSatResult
resChan
withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers :: forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
solver Natural
count Maybe Natural
timeout SolverGroup -> IO a
cont = do
[SolverInstance]
instances <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Solver -> Maybe Natural -> IO SolverInstance
spawnSolver Solver
solver Maybe Natural
timeout) [Natural
1..Natural
count]
Chan Task
taskQueue <- forall a. IO (Chan a)
newChan
Chan SolverInstance
availableInstances <- forall a. IO (Chan a)
newChan
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SolverInstance]
instances (forall a. Chan a -> a -> IO ()
writeChan Chan SolverInstance
availableInstances)
ThreadId
orchestrateId <- IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ forall {b}. Chan Task -> Chan SolverInstance -> IO b
orchestrate Chan Task
taskQueue Chan SolverInstance
availableInstances
a
res <- SolverGroup -> IO a
cont (Chan Task -> SolverGroup
SolverGroup Chan Task
taskQueue)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SolverInstance -> IO ()
stopSolver [SolverInstance]
instances
ThreadId -> IO ()
killThread ThreadId
orchestrateId
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
res
where
orchestrate :: Chan Task -> Chan SolverInstance -> IO b
orchestrate Chan Task
queue Chan SolverInstance
avail = do
Task
task <- forall a. Chan a -> IO a
readChan Chan Task
queue
SolverInstance
inst <- forall a. Chan a -> IO a
readChan Chan SolverInstance
avail
ThreadId
_ <- IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ Task -> SolverInstance -> Chan SolverInstance -> IO ()
runTask Task
task SolverInstance
inst Chan SolverInstance
avail
Chan Task -> Chan SolverInstance -> IO b
orchestrate Chan Task
queue Chan SolverInstance
avail
runTask :: Task -> SolverInstance -> Chan SolverInstance -> IO ()
runTask (Task (SMT2 [Builder]
cmds CexVars
cexvars) Chan CheckSatResult
r) SolverInstance
inst Chan SolverInstance
availableInstances = do
Either Text ()
out <- SolverInstance -> SMT2 -> IO (Either Text ())
sendScript SolverInstance
inst ([Builder] -> CexVars -> SMT2
SMT2 (Builder
"(reset)" forall a. a -> [a] -> [a]
: [Builder]
cmds) CexVars
cexvars)
case Either Text ()
out of
Left Text
e -> forall a. Chan a -> a -> IO ()
writeChan Chan CheckSatResult
r (Text -> CheckSatResult
Error (Text
"error while writing SMT to solver: " forall a. Semigroup a => a -> a -> a
<> Text -> Text
T.toStrict Text
e))
Right () -> do
Text
sat <- SolverInstance -> Text -> IO Text
sendLine SolverInstance
inst Text
"(check-sat)"
CheckSatResult
res <- case Text
sat of
Text
"sat" -> SMTCex -> CheckSatResult
Sat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverInstance -> CexVars -> IO SMTCex
getModel SolverInstance
inst CexVars
cexvars
Text
"unsat" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unsat
Text
"timeout" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unknown
Text
"unknown" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unknown
Text
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> CheckSatResult
Error forall a b. (a -> b) -> a -> b
$ Text -> Text
T.toStrict forall a b. (a -> b) -> a -> b
$ Text
"Unable to parse solver output: " forall a. Semigroup a => a -> a -> a
<> Text
sat
forall a. Chan a -> a -> IO ()
writeChan Chan CheckSatResult
r CheckSatResult
res
forall a. Chan a -> a -> IO ()
writeChan Chan SolverInstance
availableInstances SolverInstance
inst
getModel :: SolverInstance -> CexVars -> IO SMTCex
getModel :: SolverInstance -> CexVars -> IO SMTCex
getModel SolverInstance
inst CexVars
cexvars = do
SMTCex
initialModel <- IO SMTCex
getRaw
Map Text W256
hints <- Map Text W256 -> Map Text W256
capHints forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> IO Text) -> Map Text (Expr 'EWord) -> IO (Map Text W256)
queryMaxReads (SolverInstance -> Text -> IO Text
getValue SolverInstance
inst) CexVars
cexvars.buffers
if SMTCex -> Bool
bufsUsable SMTCex
initialModel
then do
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMTCex -> SMTCex
mkConcrete SMTCex
initialModel)
else SMTCex -> SMTCex
mkConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Map Text W256 -> StateT SMTCex IO ()
shrinkModel Map Text W256
hints) SMTCex
initialModel
where
getRaw :: IO SMTCex
getRaw :: IO SMTCex
getRaw = do
Map (Expr 'EWord) W256
vars <- (Text -> Expr 'EWord)
-> (Text -> IO Text) -> [Text] -> IO (Map (Expr 'EWord) W256)
getVars Text -> Expr 'EWord
parseVar (SolverInstance -> Text -> IO Text
getValue SolverInstance
inst) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict CexVars
cexvars.calldata)
Map (Expr 'Buf) BufModel
buffers <- (Text -> IO Text) -> [Text] -> IO (Map (Expr 'Buf) BufModel)
getBufs (SolverInstance -> Text -> IO Text
getValue SolverInstance
inst) (forall k a. Map k a -> [k]
Map.keys CexVars
cexvars.buffers)
Map W256 (Map W256 W256)
storage <- (Text -> IO Text)
-> [(Expr 'EWord, Expr 'EWord)] -> IO (Map W256 (Map W256 W256))
getStore (SolverInstance -> Text -> IO Text
getValue SolverInstance
inst) CexVars
cexvars.storeReads
Map (Expr 'EWord) W256
blockctx <- (Text -> Expr 'EWord)
-> (Text -> IO Text) -> [Text] -> IO (Map (Expr 'EWord) W256)
getVars Text -> Expr 'EWord
parseBlockCtx (SolverInstance -> Text -> IO Text
getValue SolverInstance
inst) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict CexVars
cexvars.blockContext)
Map (Expr 'EWord) W256
txctx <- (Text -> Expr 'EWord)
-> (Text -> IO Text) -> [Text] -> IO (Map (Expr 'EWord) W256)
getVars Text -> Expr 'EWord
parseFrameCtx (SolverInstance -> Text -> IO Text
getValue SolverInstance
inst) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict CexVars
cexvars.txContext)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Map (Expr 'EWord) W256
-> Map (Expr 'Buf) BufModel
-> Map W256 (Map W256 W256)
-> Map (Expr 'EWord) W256
-> Map (Expr 'EWord) W256
-> SMTCex
SMTCex Map (Expr 'EWord) W256
vars Map (Expr 'Buf) BufModel
buffers Map W256 (Map W256 W256)
storage Map (Expr 'EWord) W256
blockctx Map (Expr 'EWord) W256
txctx
capHints :: Map Text W256 -> Map Text W256
capHints :: Map Text W256 -> Map Text W256
capHints = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Ord a => a -> a -> a
min W256
1024)
shrinkModel :: Map Text W256 -> StateT SMTCex IO ()
shrinkModel :: Map Text W256 -> StateT SMTCex IO ()
shrinkModel Map Text W256
hints = do
SMTCex
m <- forall s (m :: * -> *). MonadState s m => m s
get
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [k]
Map.keys SMTCex
m.buffers) forall a b. (a -> b) -> a -> b
$ \case
AbstractBuf Text
b -> do
let name :: Text
name = Text -> Text
T.fromStrict Text
b
hint :: W256
hint = forall a. a -> Maybe a -> a
fromMaybe
(forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: Could not find hint for buffer: " forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
name)
(forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
name Map Text W256
hints)
Text -> W256 -> StateT SMTCex IO ()
shrinkBuf Text
name W256
hint
Expr 'Buf
_ -> forall a. HasCallStack => String -> a
error String
"Internal Error: Received model from solver for non AbstractBuf"
shrinkBuf :: Text -> W256 -> StateT SMTCex IO ()
shrinkBuf :: Text -> W256 -> StateT SMTCex IO ()
shrinkBuf Text
buf W256
hint = do
let encBound :: Text
encBound = Text
"(_ bv" forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show (forall a b. (Integral a, Num b) => a -> b
num W256
hint :: Integer)) forall a. Semigroup a => a -> a -> a
<> Text
" 256)"
Text
sat <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
SolverInstance -> Text -> IO ()
sendLine' SolverInstance
inst Text
"(push)"
SolverInstance -> Text -> IO ()
sendLine' SolverInstance
inst forall a b. (a -> b) -> a -> b
$ Text
"(assert (bvule " forall a. Semigroup a => a -> a -> a
<> Text
buf forall a. Semigroup a => a -> a -> a
<> Text
"_length " forall a. Semigroup a => a -> a -> a
<> Text
encBound forall a. Semigroup a => a -> a -> a
<> Text
"))"
SolverInstance -> Text -> IO Text
sendLine SolverInstance
inst Text
"(check-sat)"
case Text
sat of
Text
"sat" -> do
SMTCex
model <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO SMTCex
getRaw
forall s (m :: * -> *). MonadState s m => s -> m ()
put SMTCex
model
Text
"unsat" -> do
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SolverInstance -> Text -> IO ()
sendLine' SolverInstance
inst Text
"(pop)"
Text -> W256 -> StateT SMTCex IO ()
shrinkBuf Text
buf (if W256
hint forall a. Eq a => a -> a -> Bool
== W256
0 then W256
hint forall a. Num a => a -> a -> a
+ W256
1 else W256
hint forall a. Num a => a -> a -> a
* W256
2)
Text
_ -> forall a. HasCallStack => String -> a
error String
"TODO: HANDLE ERRORS"
mkConcrete :: SMTCex -> SMTCex
mkConcrete :: SMTCex -> SMTCex
mkConcrete SMTCex
c = forall a. a -> Maybe a -> a
fromMaybe
(forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: counterexample contains buffers that are too large to be represented as a ByteString: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show SMTCex
c)
(SMTCex -> Maybe SMTCex
flattenBufs SMTCex
c)
bufsUsable :: SMTCex -> Bool
bufsUsable :: SMTCex -> Bool
bufsUsable SMTCex
model = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (BufModel -> Bool
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall k a. Map k a -> [(k, a)]
Map.toList SMTCex
model.buffers)
where
go :: BufModel -> Bool
go (Flat ByteString
_) = Bool
True
go (Comp CompressedBuf
c) = case CompressedBuf
c of
(Base Word8
_ W256
sz) -> W256
sz forall a. Ord a => a -> a -> Bool
<= W256
1024
(Write Word8
_ W256
idx CompressedBuf
next) -> W256
idx forall a. Ord a => a -> a -> Bool
<= W256
1024 Bool -> Bool -> Bool
&& BufModel -> Bool
go (CompressedBuf -> BufModel
Comp CompressedBuf
next)
mkTimeout :: Maybe Natural -> Text
mkTimeout :: Maybe Natural -> Text
mkTimeout Maybe Natural
t = String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ (Natural
1000 *)forall a b. (a -> b) -> a -> b
$ case Maybe Natural
t of
Maybe Natural
Nothing -> Natural
300 :: Natural
Just Natural
t' -> Natural
t'
solverArgs :: Solver -> Maybe Natural -> [Text]
solverArgs :: Solver -> Maybe Natural -> [Text]
solverArgs Solver
solver Maybe Natural
timeout = case Solver
solver of
Solver
Bitwuzla -> forall a. HasCallStack => String -> a
error String
"TODO: Bitwuzla args"
Solver
Z3 ->
[ Text
"-in" ]
Solver
CVC5 ->
[ Text
"--lang=smt"
, Text
"--no-interactive"
, Text
"--produce-models"
, Text
"--tlimit-per=" forall a. Semigroup a => a -> a -> a
<> Maybe Natural -> Text
mkTimeout Maybe Natural
timeout
]
Custom Text
_ -> []
spawnSolver :: Solver -> Maybe (Natural) -> IO SolverInstance
spawnSolver :: Solver -> Maybe Natural -> IO SolverInstance
spawnSolver Solver
solver Maybe Natural
timeout = do
let cmd :: CreateProcess
cmd = (String -> [String] -> CreateProcess
proc (forall a. Show a => a -> String
show Solver
solver) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Solver -> Maybe Natural -> [Text]
solverArgs Solver
solver Maybe Natural
timeout)) { std_in :: StdStream
std_in = StdStream
CreatePipe, std_out :: StdStream
std_out = StdStream
CreatePipe, std_err :: StdStream
std_err = StdStream
CreatePipe }
(Just Handle
stdin, Just Handle
stdout, Just Handle
stderr, ProcessHandle
process) <- CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess CreateProcess
cmd
Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdin (Maybe Int -> BufferMode
BlockBuffering (forall a. a -> Maybe a
Just Int
1000000))
let solverInstance :: SolverInstance
solverInstance = Solver
-> Handle -> Handle -> Handle -> ProcessHandle -> SolverInstance
SolverInstance Solver
solver Handle
stdin Handle
stdout Handle
stderr ProcessHandle
process
case Solver
solver of
Solver
CVC5 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
Solver
_ -> do
()
_ <- SolverInstance -> Text -> IO ()
sendLine' SolverInstance
solverInstance forall a b. (a -> b) -> a -> b
$ Text
"(set-option :timeout " forall a. Semigroup a => a -> a -> a
<> Maybe Natural -> Text
mkTimeout Maybe Natural
timeout forall a. Semigroup a => a -> a -> a
<> Text
")"
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
stopSolver :: SolverInstance -> IO ()
stopSolver :: SolverInstance -> IO ()
stopSolver (SolverInstance Solver
_ Handle
stdin Handle
stdout Handle
stderr ProcessHandle
process) = (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle) -> IO ()
cleanupProcess (forall a. a -> Maybe a
Just Handle
stdin, forall a. a -> Maybe a
Just Handle
stdout, forall a. a -> Maybe a
Just Handle
stderr, ProcessHandle
process)
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
sendScript SolverInstance
solver (SMT2 [Builder]
cmds CexVars
_) = do
SolverInstance -> Text -> IO ()
sendLine' SolverInstance
solver ([Text] -> Text
T.unlines forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
cmds)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right()
sendCommand :: SolverInstance -> Text -> IO Text
sendCommand :: SolverInstance -> Text -> IO Text
sendCommand SolverInstance
inst Text
cmd = do
let cmd' :: Text
cmd' = (Char -> Bool) -> Text -> Text
T.dropWhile Char -> Bool
isSpace Text
cmd
case Text -> String
T.unpack Text
cmd' of
String
"" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"success"
Char
';' : String
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"success"
String
_ -> SolverInstance -> Text -> IO Text
sendLine SolverInstance
inst Text
cmd'
sendLine :: SolverInstance -> Text -> IO Text
sendLine :: SolverInstance -> Text -> IO Text
sendLine (SolverInstance Solver
_ Handle
stdin Handle
stdout Handle
_ ProcessHandle
_) Text
cmd = do
Handle -> Text -> IO ()
T.hPutStr Handle
stdin (Text -> Text -> Text
T.append Text
cmd Text
"\n")
Handle -> IO ()
hFlush Handle
stdin
Handle -> IO Text
T.hGetLine Handle
stdout
sendLine' :: SolverInstance -> Text -> IO ()
sendLine' :: SolverInstance -> Text -> IO ()
sendLine' (SolverInstance Solver
_ Handle
stdin Handle
_ Handle
_ ProcessHandle
_) Text
cmd = do
Handle -> Text -> IO ()
T.hPutStr Handle
stdin (Text -> Text -> Text
T.append Text
cmd Text
"\n")
Handle -> IO ()
hFlush Handle
stdin
getValue :: SolverInstance -> Text -> IO Text
getValue :: SolverInstance -> Text -> IO Text
getValue (SolverInstance Solver
_ Handle
stdin Handle
stdout Handle
_ ProcessHandle
_) Text
var = do
Handle -> Text -> IO ()
T.hPutStr Handle
stdin (Text -> Text -> Text
T.append (Text -> Text -> Text
T.append Text
"(get-value (" Text
var) Text
"))\n")
Handle -> IO ()
hFlush Handle
stdin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Text] -> Text
T.unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse) (Handle -> IO [Text]
readSExpr Handle
stdout)
readSExpr :: Handle -> IO [Text]
readSExpr :: Handle -> IO [Text]
readSExpr Handle
h = Int64 -> Int64 -> [Text] -> IO [Text]
go Int64
0 Int64
0 []
where
go :: Int64 -> Int64 -> [Text] -> IO [Text]
go Int64
0 Int64
0 [Text]
_ = do
Text
line <- Handle -> IO Text
T.hGetLine Handle
h
let ls :: Int64
ls = Text -> Int64
T.length forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (forall a. Eq a => a -> a -> Bool
== Char
'(') Text
line
rs :: Int64
rs = Text -> Int64
T.length forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (forall a. Eq a => a -> a -> Bool
== Char
')') Text
line
if Int64
ls forall a. Eq a => a -> a -> Bool
== Int64
rs
then forall (f :: * -> *) a. Applicative f => a -> f a
pure [Text
line]
else Int64 -> Int64 -> [Text] -> IO [Text]
go Int64
ls Int64
rs [Text
line]
go Int64
ls Int64
rs [Text]
prev = do
Text
line <- Handle -> IO Text
T.hGetLine Handle
h
let ls' :: Int64
ls' = Text -> Int64
T.length forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (forall a. Eq a => a -> a -> Bool
== Char
'(') Text
line
rs' :: Int64
rs' = Text -> Int64
T.length forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (forall a. Eq a => a -> a -> Bool
== Char
')') Text
line
if (Int64
ls forall a. Num a => a -> a -> a
+ Int64
ls') forall a. Eq a => a -> a -> Bool
== (Int64
rs forall a. Num a => a -> a -> a
+ Int64
rs')
then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Text
line forall a. a -> [a] -> [a]
: [Text]
prev
else Int64 -> Int64 -> [Text] -> IO [Text]
go (Int64
ls forall a. Num a => a -> a -> a
+ Int64
ls') (Int64
rs forall a. Num a => a -> a -> a
+ Int64
rs') (Text
line forall a. a -> [a] -> [a]
: [Text]
prev)