module EVM.Solvers where
import Prelude hiding (LT, GT)
import GHC.Natural
import GHC.IO.Handle (Handle, hFlush, hSetBuffering, BufferMode(..))
import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
import Control.Concurrent (forkIO, killThread)
import Control.Monad
import Control.Monad.State.Strict
import Control.Monad.IO.Unlift
import Data.Char (isSpace)
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe (fromMaybe, isJust, fromJust)
import Data.Text qualified as TS
import Data.Text.Lazy (Text)
import Data.Text.Lazy qualified as T
import Data.Text.Lazy.IO qualified as T
import Data.Text.Lazy.Builder
import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..), createPipe)
import Witch (into)
import EVM.Effects
import EVM.Fuzz (tryCexFuzz)
import EVM.SMT
import EVM.Types (W256, Expr(AbstractBuf), internalError)
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 -> 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
(Int -> CheckSatResult -> ShowS)
-> (CheckSatResult -> String)
-> ([CheckSatResult] -> ShowS)
-> Show CheckSatResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CheckSatResult -> ShowS
showsPrec :: Int -> CheckSatResult -> ShowS
$cshow :: CheckSatResult -> String
show :: CheckSatResult -> String
$cshowList :: [CheckSatResult] -> ShowS
showList :: [CheckSatResult] -> ShowS
Show, CheckSatResult -> CheckSatResult -> Bool
(CheckSatResult -> CheckSatResult -> Bool)
-> (CheckSatResult -> CheckSatResult -> Bool) -> Eq CheckSatResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CheckSatResult -> CheckSatResult -> Bool
== :: CheckSatResult -> CheckSatResult -> Bool
$c/= :: CheckSatResult -> CheckSatResult -> Bool
/= :: 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 <- IO (Chan CheckSatResult)
forall a. IO (Chan a)
newChan
Chan Task -> Task -> IO ()
forall a. Chan a -> a -> IO ()
writeChan Chan Task
taskQueue (SMT2 -> Chan CheckSatResult -> Task
Task SMT2
script Chan CheckSatResult
resChan)
Chan CheckSatResult -> IO CheckSatResult
forall a. Chan a -> IO a
readChan Chan CheckSatResult
resChan
writeSMT2File :: SMT2 -> Int -> String -> IO ()
writeSMT2File :: SMT2 -> Int -> String -> IO ()
writeSMT2File SMT2
smt2 Int
count String
abst =
do
let content :: Text
content = SMT2 -> Text
formatSMT2 SMT2
smt2 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\n(check-sat)"
String -> Text -> IO ()
T.writeFile (String
"query-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Int -> String
forall a. Show a => a -> String
show Int
count) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
abst String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
".smt2") Text
content
withSolvers :: App m => Solver -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
withSolvers :: forall (m :: * -> *) a.
App m =>
Solver -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
withSolvers Solver
solver Natural
count Maybe Natural
timeout SolverGroup -> m a
cont = do
[SolverInstance]
instances <- (Natural -> m SolverInstance) -> [Natural] -> m [SolverInstance]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (m SolverInstance -> Natural -> m SolverInstance
forall a b. a -> b -> a
const (m SolverInstance -> Natural -> m SolverInstance)
-> m SolverInstance -> Natural -> m SolverInstance
forall a b. (a -> b) -> a -> b
$ IO SolverInstance -> m SolverInstance
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SolverInstance -> m SolverInstance)
-> IO SolverInstance -> m SolverInstance
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 <- IO (Chan Task) -> m (Chan Task)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (Chan Task)
forall a. IO (Chan a)
newChan
Chan SolverInstance
availableInstances <- IO (Chan SolverInstance) -> m (Chan SolverInstance)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (Chan SolverInstance)
forall a. IO (Chan a)
newChan
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [SolverInstance] -> (SolverInstance -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SolverInstance]
instances (Chan SolverInstance -> SolverInstance -> IO ()
forall a. Chan a -> a -> IO ()
writeChan Chan SolverInstance
availableInstances)
IO ()
orchestrate' <- m () -> m (IO ())
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (IO a)
toIO (m () -> m (IO ())) -> m () -> m (IO ())
forall a b. (a -> b) -> a -> b
$ Chan Task -> Chan SolverInstance -> Int -> m ()
forall (m :: * -> *) b.
App m =>
Chan Task -> Chan SolverInstance -> Int -> m b
orchestrate Chan Task
taskQueue Chan SolverInstance
availableInstances Int
0
ThreadId
orchestrateId <- IO ThreadId -> m ThreadId
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ThreadId -> m ThreadId) -> IO ThreadId -> m ThreadId
forall a b. (a -> b) -> a -> b
$ IO () -> IO ThreadId
forkIO IO ()
orchestrate'
a
res <- SolverGroup -> m a
cont (Chan Task -> SolverGroup
SolverGroup Chan Task
taskQueue)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ (SolverInstance -> IO ()) -> [SolverInstance] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SolverInstance -> IO ()
stopSolver) [SolverInstance]
instances
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ ThreadId -> IO ()
killThread ThreadId
orchestrateId
a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
res
where
orchestrate :: App m => Chan Task -> Chan SolverInstance -> Int -> m b
orchestrate :: forall (m :: * -> *) b.
App m =>
Chan Task -> Chan SolverInstance -> Int -> m b
orchestrate Chan Task
queue Chan SolverInstance
avail Int
fileCounter = do
Task
task <- IO Task -> m Task
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Task -> m Task) -> IO Task -> m Task
forall a b. (a -> b) -> a -> b
$ Chan Task -> IO Task
forall a. Chan a -> IO a
readChan Chan Task
queue
SolverInstance
inst <- IO SolverInstance -> m SolverInstance
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SolverInstance -> m SolverInstance)
-> IO SolverInstance -> m SolverInstance
forall a b. (a -> b) -> a -> b
$ Chan SolverInstance -> IO SolverInstance
forall a. Chan a -> IO a
readChan Chan SolverInstance
avail
IO ()
runTask' <- m () -> m (IO ())
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (IO a)
toIO (m () -> m (IO ())) -> m () -> m (IO ())
forall a b. (a -> b) -> a -> b
$ Task -> SolverInstance -> Chan SolverInstance -> Int -> m ()
forall (m :: * -> *).
(MonadIO m, ReadConfig m) =>
Task -> SolverInstance -> Chan SolverInstance -> Int -> m ()
runTask Task
task SolverInstance
inst Chan SolverInstance
avail Int
fileCounter
ThreadId
_ <- IO ThreadId -> m ThreadId
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ThreadId -> m ThreadId) -> IO ThreadId -> m ThreadId
forall a b. (a -> b) -> a -> b
$ IO () -> IO ThreadId
forkIO IO ()
runTask'
Chan Task -> Chan SolverInstance -> Int -> m b
forall (m :: * -> *) b.
App m =>
Chan Task -> Chan SolverInstance -> Int -> m b
orchestrate Chan Task
queue Chan SolverInstance
avail (Int
fileCounter Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
runTask :: (MonadIO m, ReadConfig m) => Task -> SolverInstance -> Chan SolverInstance -> Int -> m ()
runTask :: forall (m :: * -> *).
(MonadIO m, ReadConfig m) =>
Task -> SolverInstance -> Chan SolverInstance -> Int -> m ()
runTask (Task smt2 :: SMT2
smt2@(SMT2 [Builder]
cmds (RefinementEqs [Builder]
refineEqs [Prop]
refps) CexVars
cexvars [Prop]
ps) Chan CheckSatResult
r) SolverInstance
inst Chan SolverInstance
availableInstances Int
fileCounter = do
Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
let fuzzResult :: Maybe SMTCex
fuzzResult = [Prop] -> Integer -> Maybe SMTCex
tryCexFuzz [Prop]
ps Config
conf.numCexFuzz
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config
conf.dumpQueries) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ SMT2 -> Int -> String -> IO ()
writeSMT2File SMT2
smt2 Int
fileCounter String
"abstracted"
if (Maybe SMTCex -> Bool
forall a. Maybe a -> Bool
isJust Maybe SMTCex
fuzzResult)
then do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config
conf.debug) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Cex found via fuzzing:" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Maybe SMTCex -> String
forall a. Show a => a -> String
show Maybe SMTCex
fuzzResult)
Chan CheckSatResult -> CheckSatResult -> IO ()
forall a. Chan a -> a -> IO ()
writeChan Chan CheckSatResult
r (SMTCex -> CheckSatResult
Sat (SMTCex -> CheckSatResult) -> SMTCex -> CheckSatResult
forall a b. (a -> b) -> a -> b
$ Maybe SMTCex -> SMTCex
forall a. HasCallStack => Maybe a -> a
fromJust Maybe SMTCex
fuzzResult)
else if Bool -> Bool
not Config
conf.onlyCexFuzz then do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config
conf.debug) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Fuzzing failed to find a Cex"
Either Text ()
out <- SolverInstance -> SMT2 -> IO (Either Text ())
sendScript SolverInstance
inst ([Builder] -> RefinementEqs -> CexVars -> [Prop] -> SMT2
SMT2 (Builder
"(reset)" Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
: [Builder]
cmds) RefinementEqs
forall a. Monoid a => a
mempty CexVars
forall a. Monoid a => a
mempty [Prop]
ps)
case Either Text ()
out of
Left Text
e -> Chan CheckSatResult -> CheckSatResult -> IO ()
forall a. Chan a -> a -> IO ()
writeChan Chan CheckSatResult
r (Text -> CheckSatResult
Error (Text
"error while writing SMT to solver: " Text -> Text -> Text
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 <- do
case Text
sat of
Text
"unsat" -> CheckSatResult -> IO CheckSatResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unsat
Text
"timeout" -> CheckSatResult -> IO CheckSatResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unknown
Text
"unknown" -> CheckSatResult -> IO CheckSatResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unknown
Text
"sat" -> if [Builder] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Builder]
refineEqs then SMTCex -> CheckSatResult
Sat (SMTCex -> CheckSatResult) -> IO SMTCex -> IO CheckSatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverInstance -> CexVars -> IO SMTCex
getModel SolverInstance
inst CexVars
cexvars
else do
let refinedSMT2 :: SMT2
refinedSMT2 = [Builder] -> RefinementEqs -> CexVars -> [Prop] -> SMT2
SMT2 [Builder]
refineEqs RefinementEqs
forall a. Monoid a => a
mempty CexVars
forall a. Monoid a => a
mempty ([Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
refps)
SMT2 -> Int -> String -> IO ()
writeSMT2File SMT2
refinedSMT2 Int
fileCounter String
"refined"
Either Text ()
_ <- SolverInstance -> SMT2 -> IO (Either Text ())
sendScript SolverInstance
inst SMT2
refinedSMT2
Text
sat2 <- SolverInstance -> Text -> IO Text
sendLine SolverInstance
inst Text
"(check-sat)"
case Text
sat2 of
Text
"unsat" -> CheckSatResult -> IO CheckSatResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unsat
Text
"timeout" -> CheckSatResult -> IO CheckSatResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unknown
Text
"unknown" -> CheckSatResult -> IO CheckSatResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unknown
Text
"sat" -> SMTCex -> CheckSatResult
Sat (SMTCex -> CheckSatResult) -> IO SMTCex -> IO CheckSatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverInstance -> CexVars -> IO SMTCex
getModel SolverInstance
inst CexVars
cexvars
Text
_ -> CheckSatResult -> IO CheckSatResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckSatResult -> IO CheckSatResult)
-> (Text -> CheckSatResult) -> Text -> IO CheckSatResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> CheckSatResult
Error (Text -> IO CheckSatResult) -> Text -> IO CheckSatResult
forall a b. (a -> b) -> a -> b
$ Text -> Text
T.toStrict (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Text
"Unable to parse solver output: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
sat2
Text
_ -> CheckSatResult -> IO CheckSatResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckSatResult -> IO CheckSatResult)
-> (Text -> CheckSatResult) -> Text -> IO CheckSatResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> CheckSatResult
Error (Text -> IO CheckSatResult) -> Text -> IO CheckSatResult
forall a b. (a -> b) -> a -> b
$ Text -> Text
T.toStrict (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Text
"Unable to parse solver output: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
sat
Chan CheckSatResult -> CheckSatResult -> IO ()
forall a. Chan a -> a -> IO ()
writeChan Chan CheckSatResult
r CheckSatResult
res
else do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config
conf.debug) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Fuzzing failed to find a Cex, not trying SMT due to onlyCexFuzz"
Chan CheckSatResult -> CheckSatResult -> IO ()
forall a. Chan a -> a -> IO ()
writeChan Chan CheckSatResult
r CheckSatResult
Unknown
Chan SolverInstance -> SolverInstance -> IO ()
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 (Map Text W256 -> Map Text W256)
-> IO (Map Text W256) -> IO (Map Text W256)
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
SMTCex -> IO SMTCex
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMTCex -> SMTCex
mkConcrete SMTCex
initialModel)
else SMTCex -> SMTCex
mkConcrete (SMTCex -> SMTCex)
-> (((), SMTCex) -> SMTCex) -> ((), SMTCex) -> SMTCex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((), SMTCex) -> SMTCex
forall a b. (a, b) -> b
snd (((), SMTCex) -> SMTCex) -> IO ((), SMTCex) -> IO SMTCex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SMTCex IO () -> SMTCex -> IO ((), SMTCex)
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) ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict CexVars
cexvars.calldata)
Map (Expr 'EAddr) Addr
addrs <- (Text -> Expr 'EAddr)
-> (Text -> IO Text) -> [Text] -> IO (Map (Expr 'EAddr) Addr)
getAddrs Text -> Expr 'EAddr
parseEAddr (SolverInstance -> Text -> IO Text
getValue SolverInstance
inst) ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict CexVars
cexvars.addrs)
Map (Expr 'Buf) BufModel
buffers <- (Text -> IO Text) -> [Text] -> IO (Map (Expr 'Buf) BufModel)
getBufs (SolverInstance -> Text -> IO Text
getValue SolverInstance
inst) (Map Text (Expr 'EWord) -> [Text]
forall k a. Map k a -> [k]
Map.keys CexVars
cexvars.buffers)
Map (Expr 'EAddr) (Map W256 W256)
storage <- (Text -> IO Text)
-> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
-> IO (Map (Expr 'EAddr) (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) ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
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
parseTxCtx (SolverInstance -> Text -> IO Text
getValue SolverInstance
inst) ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict CexVars
cexvars.txContext)
SMTCex -> IO SMTCex
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMTCex -> IO SMTCex) -> SMTCex -> IO SMTCex
forall a b. (a -> b) -> a -> b
$ Map (Expr 'EWord) W256
-> Map (Expr 'EAddr) Addr
-> Map (Expr 'Buf) BufModel
-> Map (Expr 'EAddr) (Map W256 W256)
-> Map (Expr 'EWord) W256
-> Map (Expr 'EWord) W256
-> SMTCex
SMTCex Map (Expr 'EWord) W256
vars Map (Expr 'EAddr) Addr
addrs Map (Expr 'Buf) BufModel
buffers Map (Expr 'EAddr) (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 = (W256 -> W256) -> Map Text W256 -> Map Text W256
forall a b. (a -> b) -> Map Text a -> Map Text b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (W256 -> W256 -> W256
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 <- StateT SMTCex IO SMTCex
forall s (m :: * -> *). MonadState s m => m s
get
[Expr 'Buf]
-> (Expr 'Buf -> StateT SMTCex IO ()) -> StateT SMTCex IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map (Expr 'Buf) BufModel -> [Expr 'Buf]
forall k a. Map k a -> [k]
Map.keys SMTCex
m.buffers) ((Expr 'Buf -> StateT SMTCex IO ()) -> StateT SMTCex IO ())
-> (Expr 'Buf -> StateT SMTCex IO ()) -> StateT SMTCex IO ()
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 = W256 -> Maybe W256 -> W256
forall a. a -> Maybe a -> a
fromMaybe
(String -> W256
forall a. HasCallStack => String -> a
internalError (String -> W256) -> String -> W256
forall a b. (a -> b) -> a -> b
$ String
"Could not find hint for buffer: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
name)
(Text -> Map Text W256 -> Maybe W256
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
_ -> String -> StateT SMTCex IO ()
forall a. HasCallStack => String -> a
internalError String
"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" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show (W256 -> Integer
forall target source. From source target => source -> target
into W256
hint :: Integer)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" 256)"
Text
sat <- IO Text -> StateT SMTCex IO Text
forall a. IO a -> StateT SMTCex IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Text -> StateT SMTCex IO Text)
-> IO Text -> StateT SMTCex IO Text
forall a b. (a -> b) -> a -> b
$ do
SolverInstance -> Text -> IO ()
checkCommand SolverInstance
inst Text
"(push 1)"
SolverInstance -> Text -> IO ()
checkCommand SolverInstance
inst (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
"(assert (bvule " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
buf Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_length " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
encBound Text -> Text -> Text
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 <- IO SMTCex -> StateT SMTCex IO SMTCex
forall a. IO a -> StateT SMTCex IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO SMTCex
getRaw
SMTCex -> StateT SMTCex IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SMTCex
model
Text
"unsat" -> do
IO () -> StateT SMTCex IO ()
forall a. IO a -> StateT SMTCex IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT SMTCex IO ()) -> IO () -> StateT SMTCex IO ()
forall a b. (a -> b) -> a -> b
$ SolverInstance -> Text -> IO ()
checkCommand SolverInstance
inst Text
"(pop 1)"
Text -> W256 -> StateT SMTCex IO ()
shrinkBuf Text
buf (if W256
hint W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then W256
hint W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
1 else W256
hint W256 -> W256 -> W256
forall a. Num a => a -> a -> a
* W256
2)
Text
e -> String -> StateT SMTCex IO ()
forall a. HasCallStack => String -> a
internalError (String -> StateT SMTCex IO ()) -> String -> StateT SMTCex IO ()
forall a b. (a -> b) -> a -> b
$ String
"Unexpected solver output: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Text -> String
T.unpack Text
e)
mkConcrete :: SMTCex -> SMTCex
mkConcrete :: SMTCex -> SMTCex
mkConcrete SMTCex
c = SMTCex -> Maybe SMTCex -> SMTCex
forall a. a -> Maybe a -> a
fromMaybe
(String -> SMTCex
forall a. HasCallStack => String -> a
internalError (String -> SMTCex) -> String -> SMTCex
forall a b. (a -> b) -> a -> b
$ String
"counterexample contains buffers that are too large to be represented as a ByteString: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> SMTCex -> String
forall a. Show a => a -> String
show SMTCex
c)
(SMTCex -> Maybe SMTCex
flattenBufs SMTCex
c)
bufsUsable :: SMTCex -> Bool
bufsUsable :: SMTCex -> Bool
bufsUsable SMTCex
model = ((Expr 'Buf, BufModel) -> Bool) -> [(Expr 'Buf, BufModel)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (BufModel -> Bool
go (BufModel -> Bool)
-> ((Expr 'Buf, BufModel) -> BufModel)
-> (Expr 'Buf, BufModel)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'Buf, BufModel) -> BufModel
forall a b. (a, b) -> b
snd) (Map (Expr 'Buf) BufModel -> [(Expr 'Buf, BufModel)]
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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
1024
(Write Word8
_ W256
idx CompressedBuf
next) -> W256
idx W256 -> W256 -> Bool
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 (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> Natural -> String
forall a b. (a -> b) -> a -> b
$ (Natural
1000 *)(Natural -> Natural) -> Natural -> Natural
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 ->
[ Text
"--lang=smt2"
, Text
"--produce-models"
, Text
"--time-limit-per=" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Maybe Natural -> Text
mkTimeout Maybe Natural
timeout
, Text
"--bv-solver=preprop"
]
Solver
Z3 ->
[ Text
"-in" ]
Solver
CVC5 ->
[ Text
"--lang=smt"
, Text
"--produce-models"
, Text
"--print-success"
, Text
"--interactive"
, Text
"--incremental"
, Text
"--tlimit-per=" Text -> Text -> Text
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
(Handle
readout, Handle
writeout) <- IO (Handle, Handle)
createPipe
let cmd :: CreateProcess
cmd
= (String -> [String] -> CreateProcess
proc (Solver -> String
forall a. Show a => a -> String
show Solver
solver) ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> String
T.unpack ([Text] -> [String]) -> [Text] -> [String]
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 = Handle -> StdStream
UseHandle Handle
writeout
, std_err :: StdStream
std_err = Handle -> StdStream
UseHandle Handle
writeout
}
(Just Handle
stdin, Maybe Handle
Nothing, Maybe Handle
Nothing, ProcessHandle
process) <- CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess CreateProcess
cmd
Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdin (Maybe Int -> BufferMode
BlockBuffering (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1000000))
let solverInstance :: SolverInstance
solverInstance = Solver -> Handle -> Handle -> ProcessHandle -> SolverInstance
SolverInstance Solver
solver Handle
stdin Handle
readout ProcessHandle
process
case Solver
solver of
Solver
CVC5 -> SolverInstance -> IO SolverInstance
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
Solver
Bitwuzla -> do
Text
_ <- SolverInstance -> Text -> IO Text
sendLine SolverInstance
solverInstance Text
"(set-option :print-success true)"
SolverInstance -> IO SolverInstance
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
Solver
Z3 -> do
()
_ <- SolverInstance -> Text -> IO ()
sendLine' SolverInstance
solverInstance (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
"(set-option :timeout " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Maybe Natural -> Text
mkTimeout Maybe Natural
timeout Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
Text
_ <- SolverInstance -> Text -> IO Text
sendLine SolverInstance
solverInstance Text
"(set-option :print-success true)"
SolverInstance -> IO SolverInstance
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
Custom Text
_ -> SolverInstance -> IO SolverInstance
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
stopSolver :: SolverInstance -> IO ()
stopSolver :: SolverInstance -> IO ()
stopSolver (SolverInstance Solver
_ Handle
stdin Handle
stdout ProcessHandle
process) = (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle) -> IO ()
cleanupProcess (Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
stdin, Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
stdout, Maybe Handle
forall a. Maybe a
Nothing, ProcessHandle
process)
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
sendScript SolverInstance
solver (SMT2 [Builder]
cmds RefinementEqs
_ CexVars
_ [Prop]
_) = do
let sexprs :: [Text]
sexprs = [Text] -> [Text]
splitSExpr ([Text] -> [Text]) -> [Text] -> [Text]
forall a b. (a -> b) -> a -> b
$ (Builder -> Text) -> [Builder] -> [Text]
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
[Text] -> IO (Either Text ())
go [Text]
sexprs
where
go :: [Text] -> IO (Either Text ())
go [] = Either Text () -> IO (Either Text ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Text () -> IO (Either Text ()))
-> Either Text () -> IO (Either Text ())
forall a b. (a -> b) -> a -> b
$ () -> Either Text ()
forall a b. b -> Either a b
Right ()
go (Text
c:[Text]
cs) = do
Text
out <- SolverInstance -> Text -> IO Text
sendCommand SolverInstance
solver Text
c
case Text
out of
Text
"success" -> [Text] -> IO (Either Text ())
go [Text]
cs
Text
e -> Either Text () -> IO (Either Text ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Text () -> IO (Either Text ()))
-> Either Text () -> IO (Either Text ())
forall a b. (a -> b) -> a -> b
$ Text -> Either Text ()
forall a b. a -> Either a b
Left (Text -> Either Text ()) -> Text -> Either Text ()
forall a b. (a -> b) -> a -> b
$ Text
"Solver returned an error:\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
e Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nwhile sending the following line: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
c
checkCommand :: SolverInstance -> Text -> IO ()
checkCommand :: SolverInstance -> Text -> IO ()
checkCommand SolverInstance
inst Text
cmd = do
Text
res <- SolverInstance -> Text -> IO Text
sendCommand SolverInstance
inst Text
cmd
case Text
res of
Text
"success" -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Text
_ -> String -> IO ()
forall a. HasCallStack => String -> a
internalError (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Unexpected solver output: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
res
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
"" -> Text -> IO Text
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"success"
Char
';' : String
_ -> Text -> IO Text
forall a. a -> IO a
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 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
_ 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 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
([Text] -> Text) -> IO [Text] -> IO Text
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Text] -> Text
T.unlines ([Text] -> Text) -> ([Text] -> [Text]) -> [Text] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> [Text]
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 (Text -> Int64) -> Text -> Int64
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'(') Text
line
rs :: Int64
rs = Text -> Int64
T.length (Text -> Int64) -> Text -> Int64
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')') Text
line
if Int64
ls Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== Int64
rs
then [Text] -> IO [Text]
forall a. a -> IO a
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 (Text -> Int64) -> Text -> Int64
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'(') Text
line
rs' :: Int64
rs' = Text -> Int64
T.length (Text -> Int64) -> Text -> Int64
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')') Text
line
if (Int64
ls Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
ls') Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== (Int64
rs Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
rs')
then [Text] -> IO [Text]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Text] -> IO [Text]) -> [Text] -> IO [Text]
forall a b. (a -> b) -> a -> b
$ Text
line Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
prev
else Int64 -> Int64 -> [Text] -> IO [Text]
go (Int64
ls Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
ls') (Int64
rs Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
rs') (Text
line Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
prev)
splitSExpr :: [Text] -> [Text]
splitSExpr :: [Text] -> [Text]
splitSExpr [Text]
ls =
let text :: Text
text = Text -> [Text] -> Text
T.intercalate Text
" " ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
';') (Text -> Text) -> [Text] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> [Text]) -> [Text] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Text -> [Text]
T.lines [Text]
ls in
(Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter (Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= Text
"") ([Text] -> [Text]) -> [Text] -> [Text]
forall a b. (a -> b) -> a -> b
$ Text -> [Text] -> [Text]
go Text
text []
where
go :: Text -> [Text] -> [Text]
go Text
"" [Text]
acc = [Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
acc
go Text
text [Text]
acc =
let (Text
sexpr, Text
text') = Text -> (Text, Text)
getSExpr Text
text in
let (Text
sexpr', Text
rest) = HasCallStack => Text -> Text -> (Text, Text)
Text -> Text -> (Text, Text)
T.breakOnEnd Text
")" Text
sexpr in
Text -> [Text] -> [Text]
go Text
text' ((Text -> Text
T.strip Text
rest)Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:(Text -> Text
T.strip Text
sexpr')Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
acc)
data Par = LPar | RPar
getSExpr :: Text -> (Text, Text)
getSExpr :: Text -> (Text, Text)
getSExpr Text
l = Par -> Text -> Int64 -> [Text] -> (Text, Text)
go Par
LPar Text
l Int64
0 []
where
go :: Par -> Text -> Int64 -> [Text] -> (Text, Text)
go Par
_ Text
text Int64
0 prev :: [Text]
prev@(Text
_:[Text]
_) = (Text -> [Text] -> Text
T.intercalate Text
"" ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
prev), Text
text)
go Par
_ Text
_ Int64
r [Text]
_ | Int64
r Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
< Int64
0 = String -> (Text, Text)
forall a. HasCallStack => String -> a
internalError String
"Unbalanced SExpression"
go Par
_ Text
"" Int64
_ [Text]
_ = String -> (Text, Text)
forall a. HasCallStack => String -> a
internalError String
"Unbalanced SExpression"
go Par
LPar Text
line Int64
r [Text]
prev =
let (Text
before, Text
after) = HasCallStack => Text -> Text -> (Text, Text)
Text -> Text -> (Text, Text)
T.breakOn Text
"(" Text
line in
let rp :: Int64
rp = Text -> Int64
T.length (Text -> Int64) -> Text -> Int64
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')') Text
before in
Par -> Text -> Int64 -> [Text] -> (Text, Text)
go Par
RPar Text
after (Int64
r Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
- Int64
rp) (if Text
before Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"" then [Text]
prev else Text
before Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
prev)
go Par
RPar Text
line Int64
r [Text]
prev =
let (Text
before, Text
after) = HasCallStack => Text -> Text -> (Text, Text)
Text -> Text -> (Text, Text)
T.breakOn Text
")" Text
line in
let lp :: Int64
lp = Text -> Int64
T.length (Text -> Int64) -> Text -> Int64
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'(') Text
before in
Par -> Text -> Int64 -> [Text] -> (Text, Text)
go Par
LPar Text
after (Int64
r Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
lp) (if Text
before Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"" then [Text]
prev else Text
before Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
prev)