{- |
    Module: EVM.Solvers
    Description: Solver orchestration
-}
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 Data.Char (isSpace)
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe (fromMaybe)
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(..))
import Witch (into)

import EVM.SMT
import EVM.Types (W256, Expr(AbstractBuf), internalError)

-- | Supported solvers
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


-- | A running solver instance
data SolverInstance = SolverInstance
  { SolverInstance -> Solver
solvertype :: Solver
  , SolverInstance -> Handle
stdin      :: Handle
  , SolverInstance -> Handle
stdout     :: Handle
  , SolverInstance -> Handle
stderr     :: Handle
  , SolverInstance -> ProcessHandle
process    :: ProcessHandle
  }

-- | A channel representing a group of solvers
newtype SolverGroup = SolverGroup (Chan Task)

-- | A script to be executed, a list of models to be extracted in the case of a sat result, and a channel where the result should be written
data Task = Task
  { Task -> SMT2
script :: SMT2
  , Task -> Chan CheckSatResult
resultChan :: Chan CheckSatResult
  }

-- | The result of a call to (check-sat)
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
  -- prepare result channel
  Chan CheckSatResult
resChan <- IO (Chan CheckSatResult)
forall a. IO (Chan a)
newChan
  -- send task to solver group
  Chan Task -> Task -> IO ()
forall a. Chan a -> a -> IO ()
writeChan Chan Task
taskQueue (SMT2 -> Chan CheckSatResult -> Task
Task SMT2
script Chan CheckSatResult
resChan)
  -- collect result
  Chan CheckSatResult -> IO CheckSatResult
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
  -- spawn solvers
  [SolverInstance]
instances <- (Natural -> IO SolverInstance) -> [Natural] -> IO [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 (IO SolverInstance -> Natural -> IO SolverInstance
forall a b. a -> b -> a
const (IO SolverInstance -> Natural -> IO SolverInstance)
-> IO SolverInstance -> Natural -> IO SolverInstance
forall a b. (a -> b) -> a -> b
$ Solver -> Maybe Natural -> IO SolverInstance
spawnSolver Solver
solver Maybe Natural
timeout) [Natural
1..Natural
count]
  -- spawn orchestration thread
  Chan Task
taskQueue <- IO (Chan Task)
forall a. IO (Chan a)
newChan
  Chan SolverInstance
availableInstances <- IO (Chan SolverInstance)
forall a. IO (Chan a)
newChan
  [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)
  ThreadId
orchestrateId <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ Chan Task -> Chan SolverInstance -> IO ()
forall {b}. Chan Task -> Chan SolverInstance -> IO b
orchestrate Chan Task
taskQueue Chan SolverInstance
availableInstances

  -- run continuation with task queue
  a
res <- SolverGroup -> IO a
cont (Chan Task -> SolverGroup
SolverGroup Chan Task
taskQueue)

  -- cleanup and return results
  (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
  ThreadId -> IO ()
killThread ThreadId
orchestrateId
  a -> IO a
forall a. a -> IO a
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 <- Chan Task -> IO Task
forall a. Chan a -> IO a
readChan Chan Task
queue
      SolverInstance
inst <- Chan SolverInstance -> IO SolverInstance
forall a. Chan a -> IO a
readChan Chan SolverInstance
avail
      ThreadId
_ <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
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
      -- reset solver and send all lines of provided script
      Either Text ()
out <- SolverInstance -> SMT2 -> IO (Either Text ())
sendScript SolverInstance
inst ([Builder] -> CexVars -> SMT2
SMT2 (Builder
"(reset)" Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
: [Builder]
cmds) CexVars
cexvars)
      case Either Text ()
out of
        -- if we got an error then return it
        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))
        -- otherwise call (check-sat), parse the result, and send it down the result channel
        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 (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
"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
_ -> 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

      -- put the instance back in the list of available instances
      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
  -- get an initial version of the model from the solver
  SMTCex
initialModel <- IO SMTCex
getRaw
  -- get concrete values for each buffers max read index
  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
  -- check the sizes of buffer models and shrink if needed
  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 '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 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) ((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
parseFrameCtx (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 '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

    -- sometimes the solver might give us back a model for the max read index
    -- that is too high to be a useful cex (e.g. in the case of reads from a
    -- symbolic index), so we cap the max value of the starting point to be 1024
    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)

    -- shrink all the buffers in a model
    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
      -- iterate over all the buffers in the model, and shrink each one in turn if needed
      [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"

    -- starting with some guess at the max useful size for a buffer, cap
    -- it's size to that value, and ask the solver to check satisfiability. If
    -- it's still sat with the new constraint, leave that constraint on the
    -- stack and return a new model, if it's unsat, double the size of the hint
    -- and try again.
    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 ()
sendLine' SolverInstance
inst Text
"(push)"
        SolverInstance -> Text -> IO ()
sendLine' 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 ()
sendLine' SolverInstance
inst Text
"(pop)"
          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
_ -> String -> StateT SMTCex IO ()
forall a. HasCallStack => String -> a
internalError String
"SMT solver returned unexpected result (neither sat/unsat), which HEVM currently cannot handle"

    -- Collapses the abstract description of a models buffers down to a bytestring
    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)

    -- we set a pretty arbitrary upper limit (of 1024) to decide if we need to do some shrinking
    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
          -- TODO: do I need to check the write idx here?
          (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'

-- | Arguments used when spawing a solver instance
solverArgs :: Solver -> Maybe Natural -> [Text]
solverArgs :: Solver -> Maybe Natural -> [Text]
solverArgs Solver
solver Maybe Natural
timeout = case Solver
solver of
  Solver
Bitwuzla -> String -> [Text]
forall a. HasCallStack => String -> a
internalError String
"TODO: Bitwuzla args"
  Solver
Z3 ->
    [ Text
"-in" ]
  Solver
CVC5 ->
    [ Text
"--lang=smt"
    , Text
"--produce-models"
    , Text
"--tlimit-per=" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Maybe Natural -> Text
mkTimeout Maybe Natural
timeout
    ]
  Custom Text
_ -> []

-- | Spawns a solver instance, and sets the various global config options that we use for our queries
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 (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 = 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 (Int -> Maybe Int
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 -> SolverInstance -> IO SolverInstance
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
    Solver
_ -> 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
")"
      SolverInstance -> IO SolverInstance
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance

-- | Cleanly shutdown a running solver instnace
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 (Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
stdin, Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
stdout, Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
stderr, ProcessHandle
process)

-- | Sends a list of commands to the solver. Returns the first error, if there was one.
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
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)
  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()

-- | Sends a single command to the solver, returns the first available line from the output buffer
sendCommand :: SolverInstance -> Text -> IO Text
sendCommand :: SolverInstance -> Text -> IO Text
sendCommand SolverInstance
inst Text
cmd = do
  -- trim leading whitespace
  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"      -- ignore blank lines
    Char
';' : String
_ -> Text -> IO Text
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"success" -- ignore comments
    String
_ -> SolverInstance -> Text -> IO Text
sendLine SolverInstance
inst Text
cmd'

-- | Sends a string to the solver and appends a newline, returns the first available line from the output buffer
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

-- | Sends a string to the solver and appends a newline, doesn't return 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

-- | Returns a string representation of the model for the requested variable
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
  ([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)

-- | Reads lines from h until we have a balanced sexpr
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)

-- From a list of lines, take each separate SExpression and put it in
-- its own list, after removing comments.
splitSExpr :: [Text] -> Text
splitSExpr :: [Text] -> Text
splitSExpr [Text]
ls =
  -- split lines, strip comments, and append everything to a single line
  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] -> Text
T.unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (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

-- take the first SExpression and return the rest of the text
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"
    -- find the next left parenthesis
    go Par
LPar Text
line Int64
r [Text]
prev = -- r is how many right parentheses we are missing
      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)
    -- find the next right parenthesis
    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)