{-# Language GADTs #-}
{-# Language StandaloneDeriving #-}
{-# Language LambdaCase #-}

module EVM.Fetch where

import Prelude hiding (Word)

import EVM.ABI
import EVM.Types    (Addr, w256, W256, hexText, Word, Buffer(..))
import EVM.Symbolic (litWord)
import EVM          (IsUnique(..), EVM, Contract, Block, initialContract, nonce, balance, external)
import qualified EVM.FeeSchedule as FeeSchedule

import qualified EVM

import Control.Lens hiding ((.=))
import Control.Monad.Reader
import Control.Monad.Trans.Maybe
import Data.SBV.Trans.Control
import qualified Data.SBV.Internals as SBV
import Data.SBV.Trans hiding (Word)
import Data.Aeson
import Data.Aeson.Lens
import qualified Data.ByteString as BS
import Data.Text (Text, unpack, pack)

import qualified Data.Vector as RegularVector
import Network.Wreq
import Network.Wreq.Session (Session)
import System.Process

import qualified Network.Wreq.Session as Session

-- | Abstract representation of an RPC fetch request
data RpcQuery a where
  QueryCode    :: Addr         -> RpcQuery BS.ByteString
  QueryBlock   ::                 RpcQuery Block
  QueryBalance :: Addr         -> RpcQuery W256
  QueryNonce   :: Addr         -> RpcQuery W256
  QuerySlot    :: Addr -> W256 -> RpcQuery W256
  QueryChainId ::                 RpcQuery W256

data BlockNumber = Latest | BlockNumber W256

deriving instance Show (RpcQuery a)

rpc :: String -> [Value] -> Value
rpc :: String -> [Value] -> Value
rpc String
method [Value]
args = [Pair] -> Value
object
  [ Text
"jsonrpc" Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= (String
"2.0" :: String)
  , Text
"id"      Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Scientific -> Value
Number Scientific
1
  , Text
"method"  Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String
method
  , Text
"params"  Text -> [Value] -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= [Value]
args
  ]

class ToRPC a where
  toRPC :: a -> Value

instance ToRPC Addr where
  toRPC :: Addr -> Value
toRPC = Text -> Value
String (Text -> Value) -> (Addr -> Text) -> Addr -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack (String -> Text) -> (Addr -> String) -> Addr -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Addr -> String
forall a. Show a => a -> String
show

instance ToRPC W256 where
  toRPC :: W256 -> Value
toRPC = Text -> Value
String (Text -> Value) -> (W256 -> Text) -> W256 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack (String -> Text) -> (W256 -> String) -> W256 -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> String
forall a. Show a => a -> String
show

instance ToRPC Bool where
  toRPC :: Bool -> Value
toRPC = Bool -> Value
Bool

instance ToRPC BlockNumber where
  toRPC :: BlockNumber -> Value
toRPC BlockNumber
Latest          = Text -> Value
String Text
"latest"
  toRPC (BlockNumber W256
n) = Text -> Value
String (Text -> Value) -> (String -> Text) -> String -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ W256 -> String
forall a. Show a => a -> String
show W256
n

readText :: Read a => Text -> a
readText :: Text -> a
readText = String -> a
forall a. Read a => String -> a
read (String -> a) -> (Text -> String) -> Text -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
unpack

fetchQuery
  :: Show a
  => BlockNumber
  -> (Value -> IO (Maybe Value))
  -> RpcQuery a
  -> IO (Maybe a)
fetchQuery :: BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
fetchQuery BlockNumber
n Value -> IO (Maybe Value)
f RpcQuery a
q = do
  Maybe a
x <- case RpcQuery a
q of
    QueryCode Addr
addr -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc String
"eth_getCode" [Addr -> Value
forall a. ToRPC a => a -> Value
toRPC Addr
addr, BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe ByteString -> IO (Maybe ByteString)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ByteString -> IO (Maybe ByteString))
-> Maybe ByteString -> IO (Maybe ByteString)
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
hexText (Text -> ByteString) -> (Value -> Text) -> Value -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> ByteString) -> Maybe Value -> Maybe ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
    QueryNonce Addr
addr -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc String
"eth_getTransactionCount" [Addr -> Value
forall a. ToRPC a => a -> Value
toRPC Addr
addr, BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe W256 -> IO (Maybe W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe W256 -> IO (Maybe W256)) -> Maybe W256 -> IO (Maybe W256)
forall a b. (a -> b) -> a -> b
$ Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> (Value -> Text) -> Value -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> W256) -> Maybe Value -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
    RpcQuery a
QueryBlock -> do
      Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc String
"eth_getBlockByNumber" [BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n, Bool -> Value
forall a. ToRPC a => a -> Value
toRPC Bool
False])
      Maybe Block -> IO (Maybe Block)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Block -> IO (Maybe Block))
-> Maybe Block -> IO (Maybe Block)
forall a b. (a -> b) -> a -> b
$ Maybe Value
m Maybe Value -> (Value -> Maybe Block) -> Maybe Block
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> Maybe Block
forall s. (AsValue s, Show s) => s -> Maybe Block
parseBlock
    QueryBalance Addr
addr -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc String
"eth_getBalance" [Addr -> Value
forall a. ToRPC a => a -> Value
toRPC Addr
addr, BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe W256 -> IO (Maybe W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe W256 -> IO (Maybe W256)) -> Maybe W256 -> IO (Maybe W256)
forall a b. (a -> b) -> a -> b
$ Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> (Value -> Text) -> Value -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> W256) -> Maybe Value -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
    QuerySlot Addr
addr W256
slot -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc String
"eth_getStorageAt" [Addr -> Value
forall a. ToRPC a => a -> Value
toRPC Addr
addr, W256 -> Value
forall a. ToRPC a => a -> Value
toRPC W256
slot, BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe W256 -> IO (Maybe W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe W256 -> IO (Maybe W256)) -> Maybe W256 -> IO (Maybe W256)
forall a b. (a -> b) -> a -> b
$ Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> (Value -> Text) -> Value -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> W256) -> Maybe Value -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
    RpcQuery a
QueryChainId -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc String
"eth_chainId" [BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe W256 -> IO (Maybe W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe W256 -> IO (Maybe W256)) -> Maybe W256 -> IO (Maybe W256)
forall a b. (a -> b) -> a -> b
$ Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> (Value -> Text) -> Value -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> W256) -> Maybe Value -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
  Maybe a -> IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
x


parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block
parseBlock :: s -> Maybe Block
parseBlock s
j = do
  Addr
coinbase   <- Text -> Addr
forall a. Read a => Text -> a
readText (Text -> Addr) -> Maybe Text -> Maybe Addr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Getting (First Text) s Text -> Maybe Text
forall s a. s -> Getting (First a) s a -> Maybe a
^? Text -> Traversal' s Value
forall t. AsValue t => Text -> Traversal' t Value
key Text
"miner" ((Value -> Const (First Text) Value) -> s -> Const (First Text) s)
-> ((Text -> Const (First Text) Text)
    -> Value -> Const (First Text) Value)
-> Getting (First Text) s Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Const (First Text) Text)
-> Value -> Const (First Text) Value
forall t. AsPrimitive t => Prism' t Text
_String
  SymWord
timestamp  <- Word -> SymWord
litWord (Word -> SymWord) -> (Text -> Word) -> Text -> SymWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Word
forall a. Read a => Text -> a
readText (Text -> SymWord) -> Maybe Text -> Maybe SymWord
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Getting (First Text) s Text -> Maybe Text
forall s a. s -> Getting (First a) s a -> Maybe a
^? Text -> Traversal' s Value
forall t. AsValue t => Text -> Traversal' t Value
key Text
"timestamp" ((Value -> Const (First Text) Value) -> s -> Const (First Text) s)
-> ((Text -> Const (First Text) Text)
    -> Value -> Const (First Text) Value)
-> Getting (First Text) s Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Const (First Text) Text)
-> Value -> Const (First Text) Value
forall t. AsPrimitive t => Prism' t Text
_String
  Word
number     <- Text -> Word
forall a. Read a => Text -> a
readText (Text -> Word) -> Maybe Text -> Maybe Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Getting (First Text) s Text -> Maybe Text
forall s a. s -> Getting (First a) s a -> Maybe a
^? Text -> Traversal' s Value
forall t. AsValue t => Text -> Traversal' t Value
key Text
"number" ((Value -> Const (First Text) Value) -> s -> Const (First Text) s)
-> ((Text -> Const (First Text) Text)
    -> Value -> Const (First Text) Value)
-> Getting (First Text) s Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Const (First Text) Text)
-> Value -> Const (First Text) Value
forall t. AsPrimitive t => Prism' t Text
_String
  Word
difficulty <- Text -> Word
forall a. Read a => Text -> a
readText (Text -> Word) -> Maybe Text -> Maybe Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Getting (First Text) s Text -> Maybe Text
forall s a. s -> Getting (First a) s a -> Maybe a
^? Text -> Traversal' s Value
forall t. AsValue t => Text -> Traversal' t Value
key Text
"difficulty" ((Value -> Const (First Text) Value) -> s -> Const (First Text) s)
-> ((Text -> Const (First Text) Text)
    -> Value -> Const (First Text) Value)
-> Getting (First Text) s Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Const (First Text) Text)
-> Value -> Const (First Text) Value
forall t. AsPrimitive t => Prism' t Text
_String
  -- default codesize, default gas limit, default feescedule
  Block -> Maybe Block
forall (m :: * -> *) a. Monad m => a -> m a
return (Block -> Maybe Block) -> Block -> Maybe Block
forall a b. (a -> b) -> a -> b
$ Addr
-> SymWord
-> Word
-> Word
-> Word
-> Word
-> FeeSchedule Integer
-> Block
EVM.Block Addr
coinbase SymWord
timestamp Word
number Word
difficulty Word
0xffffffff Word
0xffffffff FeeSchedule Integer
forall n. Num n => FeeSchedule n
FeeSchedule.berlin

fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession Text
url Session
sess Value
x = do
  Response Value
r <- Response ByteString -> IO (Response Value)
forall (m :: * -> *).
MonadThrow m =>
Response ByteString -> m (Response Value)
asValue (Response ByteString -> IO (Response Value))
-> IO (Response ByteString) -> IO (Response Value)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Session -> String -> Value -> IO (Response ByteString)
forall a.
Postable a =>
Session -> String -> a -> IO (Response ByteString)
Session.post Session
sess (Text -> String
unpack Text
url) Value
x
  Maybe Value -> IO (Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Response Value
r Response Value
-> Getting (First Value) (Response Value) Value -> Maybe Value
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First Value) (Response Value) Value
forall body0 body1.
Lens (Response body0) (Response body1) body0 body1
responseBody Getting (First Value) (Response Value) Value
-> ((Value -> Const (First Value) Value)
    -> Value -> Const (First Value) Value)
-> Getting (First Value) (Response Value) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Traversal' Value Value
forall t. AsValue t => Text -> Traversal' t Value
key Text
"result")

fetchContractWithSession
  :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchContractWithSession :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchContractWithSession BlockNumber
n Text
url Addr
addr Session
sess = MaybeT IO Contract -> IO (Maybe Contract)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO Contract -> IO (Maybe Contract))
-> MaybeT IO Contract -> IO (Maybe Contract)
forall a b. (a -> b) -> a -> b
$ do
  let
    fetch :: Show a => RpcQuery a -> IO (Maybe a)
    fetch :: RpcQuery a -> IO (Maybe a)
fetch = BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
forall a.
Show a =>
BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
fetchQuery BlockNumber
n (Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession Text
url Session
sess)

  ByteString
theCode    <- IO (Maybe ByteString) -> MaybeT IO ByteString
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe ByteString) -> MaybeT IO ByteString)
-> IO (Maybe ByteString) -> MaybeT IO ByteString
forall a b. (a -> b) -> a -> b
$ RpcQuery ByteString -> IO (Maybe ByteString)
forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery ByteString
QueryCode Addr
addr)
  W256
theNonce   <- IO (Maybe W256) -> MaybeT IO W256
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe W256) -> MaybeT IO W256)
-> IO (Maybe W256) -> MaybeT IO W256
forall a b. (a -> b) -> a -> b
$ RpcQuery W256 -> IO (Maybe W256)
forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery W256
QueryNonce Addr
addr)
  W256
theBalance <- IO (Maybe W256) -> MaybeT IO W256
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe W256) -> MaybeT IO W256)
-> IO (Maybe W256) -> MaybeT IO W256
forall a b. (a -> b) -> a -> b
$ RpcQuery W256 -> IO (Maybe W256)
forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery W256
QueryBalance Addr
addr)

  Contract -> MaybeT IO Contract
forall (m :: * -> *) a. Monad m => a -> m a
return (Contract -> MaybeT IO Contract) -> Contract -> MaybeT IO Contract
forall a b. (a -> b) -> a -> b
$
    ContractCode -> Contract
initialContract (Buffer -> ContractCode
EVM.RuntimeCode (ByteString -> Buffer
ConcreteBuffer ByteString
theCode))
      Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Word Word -> Word -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Word Word
Lens' Contract Word
nonce    (W256 -> Word
w256 W256
theNonce)
      Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Word Word -> Word -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Word Word
Lens' Contract Word
balance  (W256 -> Word
w256 W256
theBalance)
      Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Bool Bool -> Bool -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Bool Bool
Lens' Contract Bool
external Bool
True

fetchSlotWithSession
  :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe Word)
fetchSlotWithSession :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe Word)
fetchSlotWithSession BlockNumber
n Text
url Session
sess Addr
addr W256
slot =
  (W256 -> Word) -> Maybe W256 -> Maybe Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap W256 -> Word
w256 (Maybe W256 -> Maybe Word) -> IO (Maybe W256) -> IO (Maybe Word)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery W256 -> IO (Maybe W256)
forall a.
Show a =>
BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
fetchQuery BlockNumber
n (Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession Text
url Session
sess) (Addr -> W256 -> RpcQuery W256
QuerySlot Addr
addr W256
slot)

fetchBlockWithSession
  :: BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockWithSession :: BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockWithSession BlockNumber
n Text
url Session
sess =
  BlockNumber
-> (Value -> IO (Maybe Value))
-> RpcQuery Block
-> IO (Maybe Block)
forall a.
Show a =>
BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
fetchQuery BlockNumber
n (Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession Text
url Session
sess) RpcQuery Block
QueryBlock

fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)
fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)
fetchBlockFrom BlockNumber
n Text
url =
  (Session -> IO (Maybe Block)) -> IO (Maybe Block)
forall a. (Session -> IO a) -> IO a
Session.withAPISession
    (BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockWithSession BlockNumber
n Text
url)

fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom BlockNumber
n Text
url Addr
addr =
  (Session -> IO (Maybe Contract)) -> IO (Maybe Contract)
forall a. (Session -> IO a) -> IO a
Session.withAPISession
    (BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchContractWithSession BlockNumber
n Text
url Addr
addr)

fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe Word)
fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe Word)
fetchSlotFrom BlockNumber
n Text
url Addr
addr W256
slot =
  (Session -> IO (Maybe Word)) -> IO (Maybe Word)
forall a. (Session -> IO a) -> IO a
Session.withAPISession
    (\Session
s -> BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe Word)
fetchSlotWithSession BlockNumber
n Text
url Session
s Addr
addr W256
slot)

http :: BlockNumber -> Text -> Fetcher
http :: BlockNumber -> Text -> Fetcher
http BlockNumber
n Text
url = Maybe State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
oracle Maybe State
forall a. Maybe a
Nothing ((BlockNumber, Text) -> Maybe (BlockNumber, Text)
forall a. a -> Maybe a
Just (BlockNumber
n, Text
url)) Bool
True

zero :: Fetcher
zero :: Fetcher
zero = Maybe State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
oracle Maybe State
forall a. Maybe a
Nothing Maybe (BlockNumber, Text)
forall a. Maybe a
Nothing Bool
True

-- smtsolving + (http or zero)
oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
oracle :: Maybe State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
oracle Maybe State
smtstate Maybe (BlockNumber, Text)
info Bool
ensureConsistency Query
q = do
  case Query
q of
    EVM.PleaseDoFFI [String]
vals ByteString -> EVM ()
continue -> case [String]
vals of
       String
cmd : [String]
args -> do
          (ExitCode
_, String
stdout', String
_) <- String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
cmd [String]
args String
""
          EVM () -> IO (EVM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM () -> IO (EVM ()))
-> (AbiValue -> EVM ()) -> AbiValue -> IO (EVM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> EVM ()
continue (ByteString -> EVM ())
-> (AbiValue -> ByteString) -> AbiValue -> EVM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbiValue -> ByteString
encodeAbiValue (AbiValue -> IO (EVM ())) -> AbiValue -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$
            Vector AbiValue -> AbiValue
AbiTuple ([AbiValue] -> Vector AbiValue
forall a. [a] -> Vector a
RegularVector.fromList [ ByteString -> AbiValue
AbiBytesDynamic (ByteString -> AbiValue)
-> (String -> ByteString) -> String -> AbiValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> ByteString
hexText (Text -> ByteString) -> (String -> Text) -> String -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack (String -> AbiValue) -> String -> AbiValue
forall a b. (a -> b) -> a -> b
$ String
stdout'])
       [String]
_ -> String -> IO (EVM ())
forall a. HasCallStack => String -> a
error ([String] -> String
forall a. Show a => a -> String
show [String]
vals)

    EVM.PleaseAskSMT SBool
branchcondition [SBool]
pathconditions BranchCondition -> EVM ()
continue ->
      case Maybe State
smtstate of
        Maybe State
Nothing -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> IO (EVM ())) -> EVM () -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ BranchCondition -> EVM ()
continue BranchCondition
EVM.Unknown
        Just State
state -> (ReaderT State IO (EVM ()) -> State -> IO (EVM ()))
-> State -> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT State IO (EVM ()) -> State -> IO (EVM ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT State
state (ReaderT State IO (EVM ()) -> IO (EVM ()))
-> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall (m :: * -> *) a. QueryT m a -> ReaderT State m a
SBV.runQueryT (QueryT IO (EVM ()) -> ReaderT State IO (EVM ()))
-> QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall a b. (a -> b) -> a -> b
$ do
         let pathconds :: SBool
pathconds = [SBool] -> SBool
sAnd [SBool]
pathconditions
         -- Is is possible to satisfy the condition?
         BranchCondition -> EVM ()
continue (BranchCondition -> EVM ())
-> QueryT IO BranchCondition -> QueryT IO (EVM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBool -> SBool -> Bool -> QueryT IO BranchCondition
checkBranch SBool
pathconds SBool
branchcondition Bool
ensureConsistency

    -- if we are using a symbolic storage model,
    -- we generate a new array to the fetched contract here
    EVM.PleaseFetchContract Addr
addr StorageModel
model Contract -> EVM ()
continue -> do
      Maybe Contract
contract <- case Maybe (BlockNumber, Text)
info of
                    Maybe (BlockNumber, Text)
Nothing -> Maybe Contract -> IO (Maybe Contract)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Contract -> IO (Maybe Contract))
-> Maybe Contract -> IO (Maybe Contract)
forall a b. (a -> b) -> a -> b
$ Contract -> Maybe Contract
forall a. a -> Maybe a
Just (Contract -> Maybe Contract) -> Contract -> Maybe Contract
forall a b. (a -> b) -> a -> b
$ ContractCode -> Contract
initialContract (Buffer -> ContractCode
EVM.RuntimeCode Buffer
forall a. Monoid a => a
mempty)
                    Just (BlockNumber
n, Text
url) -> BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom BlockNumber
n Text
url Addr
addr
      case Maybe Contract
contract of
        Just Contract
x -> case StorageModel
model of
          StorageModel
EVM.ConcreteS -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> IO (EVM ())) -> EVM () -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ Contract -> EVM ()
continue Contract
x
          StorageModel
EVM.InitialS  -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> IO (EVM ())) -> EVM () -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ Contract -> EVM ()
continue (Contract -> EVM ()) -> Contract -> EVM ()
forall a b. (a -> b) -> a -> b
$ Contract
x
             Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Storage Storage
-> Storage -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Storage Storage
Lens' Contract Storage
EVM.storage ([(SymWord, SymWord)] -> SArray (WordN 256) (WordN 256) -> Storage
EVM.Symbolic [] (SArray (WordN 256) (WordN 256) -> Storage)
-> SArray (WordN 256) (WordN 256) -> Storage
forall a b. (a -> b) -> a -> b
$ WordN 256
-> [(SBV (WordN 256), SBV (WordN 256))]
-> SArray (WordN 256) (WordN 256)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, SymVal b) =>
b -> [(SBV a, SBV b)] -> array a b
SBV.sListArray WordN 256
0 [])
          StorageModel
EVM.SymbolicS -> case Maybe State
smtstate of
            Maybe State
Nothing -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Contract -> EVM ()
continue (Contract -> EVM ()) -> Contract -> EVM ()
forall a b. (a -> b) -> a -> b
$ Contract
x
                               Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Storage Storage
-> Storage -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Storage Storage
Lens' Contract Storage
EVM.storage ([(SymWord, SymWord)] -> SArray (WordN 256) (WordN 256) -> Storage
EVM.Symbolic [] (SArray (WordN 256) (WordN 256) -> Storage)
-> SArray (WordN 256) (WordN 256) -> Storage
forall a b. (a -> b) -> a -> b
$ WordN 256
-> [(SBV (WordN 256), SBV (WordN 256))]
-> SArray (WordN 256) (WordN 256)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, SymVal b) =>
b -> [(SBV a, SBV b)] -> array a b
SBV.sListArray WordN 256
0 []))

            Just State
state ->
              (ReaderT State IO (EVM ()) -> State -> IO (EVM ()))
-> State -> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT State IO (EVM ()) -> State -> IO (EVM ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT State
state (ReaderT State IO (EVM ()) -> IO (EVM ()))
-> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall (m :: * -> *) a. QueryT m a -> ReaderT State m a
SBV.runQueryT (QueryT IO (EVM ()) -> ReaderT State IO (EVM ()))
-> QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall a b. (a -> b) -> a -> b
$ do
                SArray (WordN 256) (WordN 256)
store <- Maybe (SBV (WordN 256))
-> QueryT IO (SArray (WordN 256) (WordN 256))
forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
freshArray_ Maybe (SBV (WordN 256))
forall a. Maybe a
Nothing
                EVM () -> QueryT IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ Contract -> EVM ()
continue (Contract -> EVM ()) -> Contract -> EVM ()
forall a b. (a -> b) -> a -> b
$ Contract
x
                  Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Storage Storage
-> Storage -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Storage Storage
Lens' Contract Storage
EVM.storage ([(SymWord, SymWord)] -> SArray (WordN 256) (WordN 256) -> Storage
EVM.Symbolic [] SArray (WordN 256) (WordN 256)
store)
        Maybe Contract
Nothing -> String -> IO (EVM ())
forall a. HasCallStack => String -> a
error (String
"oracle error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Query -> String
forall a. Show a => a -> String
show Query
q)

    EVM.PleaseMakeUnique SBV a
val [SBool]
pathconditions IsUnique a -> EVM ()
continue ->
          case Maybe State
smtstate of
            Maybe State
Nothing -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> IO (EVM ())) -> EVM () -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue IsUnique a
forall a. IsUnique a
Multiple
            Just State
state -> (ReaderT State IO (EVM ()) -> State -> IO (EVM ()))
-> State -> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT State IO (EVM ()) -> State -> IO (EVM ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT State
state (ReaderT State IO (EVM ()) -> IO (EVM ()))
-> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall (m :: * -> *) a. QueryT m a -> ReaderT State m a
SBV.runQueryT (QueryT IO (EVM ()) -> ReaderT State IO (EVM ()))
-> QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall a b. (a -> b) -> a -> b
$ do
              SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ [SBool]
pathconditions [SBool] -> [SBool] -> [SBool]
forall a. Semigroup a => a -> a -> a
<> [SBV a
val SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
val] -- dummy proposition just to make sure `val` is defined when we do `getValue` later.
              QueryT IO CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO (EVM ())) -> QueryT IO (EVM ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                CheckSatResult
Sat -> do
                  a
val' <- SBV a -> QueryT IO a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue SBV a
val
                  CheckSatResult
s    <- SBool -> QueryT IO CheckSatResult
checksat (SBV a
val SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
val')
                  case CheckSatResult
s of
                    CheckSatResult
Unsat -> EVM () -> QueryT IO (EVM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue (IsUnique a -> EVM ()) -> IsUnique a -> EVM ()
forall a b. (a -> b) -> a -> b
$ a -> IsUnique a
forall a. a -> IsUnique a
Unique a
val'
                    CheckSatResult
_ -> EVM () -> QueryT IO (EVM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue IsUnique a
forall a. IsUnique a
Multiple
                CheckSatResult
Unsat -> EVM () -> QueryT IO (EVM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue IsUnique a
forall a. IsUnique a
InconsistentU
                CheckSatResult
Unk -> EVM () -> QueryT IO (EVM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue IsUnique a
forall a. IsUnique a
TimeoutU
                DSat Maybe String
_ -> String -> QueryT IO (EVM ())
forall a. HasCallStack => String -> a
error String
"unexpected DSAT"


    EVM.PleaseFetchSlot Addr
addr Word
slot Word -> EVM ()
continue ->
      case Maybe (BlockNumber, Text)
info of
        Maybe (BlockNumber, Text)
Nothing -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Word -> EVM ()
continue Word
0)
        Just (BlockNumber
n, Text
url) ->
         BlockNumber -> Text -> Addr -> W256 -> IO (Maybe Word)
fetchSlotFrom BlockNumber
n Text
url Addr
addr (Word -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
slot) IO (Maybe Word) -> (Maybe Word -> IO (EVM ())) -> IO (EVM ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
           Just Word
x  -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Word -> EVM ()
continue Word
x)
           Maybe Word
Nothing ->
             String -> IO (EVM ())
forall a. HasCallStack => String -> a
error (String
"oracle error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Query -> String
forall a. Show a => a -> String
show Query
q)

type Fetcher = EVM.Query -> IO (EVM ())

checksat :: SBool -> Query CheckSatResult
checksat :: SBool -> QueryT IO CheckSatResult
checksat SBool
b = do Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push Int
1
                SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
b
                CheckSatResult
m <- QueryT IO CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
                Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop Int
1
                CheckSatResult -> QueryT IO CheckSatResult
forall (m :: * -> *) a. Monad m => a -> m a
return CheckSatResult
m

-- | Checks which branches are satisfiable, checking the pathconditions for consistency
-- if the third argument is true.
-- When in debug mode, we do not want to be able to navigate to dead paths,
-- but for normal execution paths with inconsistent pathconditions
-- will be pruned anyway.
checkBranch :: SBool -> SBool -> Bool -> Query EVM.BranchCondition
checkBranch :: SBool -> SBool -> Bool -> QueryT IO BranchCondition
checkBranch SBool
pathconds SBool
branchcondition Bool
False = do
  SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
pathconds
  SBool -> QueryT IO CheckSatResult
checksat SBool
branchcondition QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     -- the condition is unsatisfiable
     CheckSatResult
Unsat -> -- if pathconditions are consistent then the condition must be false
            BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
False
     -- Sat means its possible for condition to hold
     CheckSatResult
Sat -> -- is its negation also possible?
            SBool -> QueryT IO CheckSatResult
checksat (SBool -> SBool
sNot SBool
branchcondition) QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               -- No. The condition must hold
               CheckSatResult
Unsat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
True
               -- Yes. Both branches possible
               CheckSatResult
Sat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               -- Explore both branches in case of timeout
               CheckSatResult
Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               DSat Maybe String
_ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error String
"checkBranch: unexpected SMT result"
     -- If the query times out, we simply explore both paths
     CheckSatResult
Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
     DSat Maybe String
_ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error String
"checkBranch: unexpected SMT result"

checkBranch SBool
pathconds SBool
branchcondition Bool
True = do
  SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
pathconds
  SBool -> QueryT IO CheckSatResult
checksat SBool
branchcondition QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     -- the condition is unsatisfiable
     CheckSatResult
Unsat -> -- are the pathconditions even consistent?
              SBool -> QueryT IO CheckSatResult
checksat (SBool -> SBool
sNot SBool
branchcondition) QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                -- No. We are on an inconsistent path.
                CheckSatResult
Unsat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Inconsistent
                -- Yes. The condition must be false.
                CheckSatResult
Sat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
False
                -- Assume the negated condition is still possible.
                CheckSatResult
Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
False
                DSat Maybe String
_ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error String
"checkBranch: unexpected SMT result"
     -- Sat means its possible for condition to hold
     CheckSatResult
Sat -> -- is its negation also possible?
            SBool -> QueryT IO CheckSatResult
checksat (SBool -> SBool
sNot SBool
branchcondition) QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               -- No. The condition must hold
               CheckSatResult
Unsat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
True
               -- Yes. Both branches possible
               CheckSatResult
Sat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               -- Explore both branches in case of timeout
               CheckSatResult
Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               DSat Maybe String
_ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error String
"checkBranch: unexpected SMT result"

     -- If the query times out, we simply explore both paths
     CheckSatResult
Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
     DSat Maybe String
_ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error String
"Internal Error: unexpected SMT result"