{-# LANGUAGE ImplicitParams #-}

module EVM.UnitTest where

import EVM
import EVM.ABI
import EVM.SMT
import EVM.Solvers
import EVM.Dapp
import EVM.Effects
import EVM.Exec
import EVM.Expr qualified as Expr
import EVM.FeeSchedule (feeSchedule)
import EVM.Fetch qualified as Fetch
import EVM.Format
import EVM.Solidity
import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isUnknown, isError, groupIssues)
import EVM.Types
import EVM.Transaction (initTx)
import EVM.Stepper (Stepper)
import EVM.Stepper qualified as Stepper

import Control.Monad (void, when, forM, forM_)
import Control.Monad.ST (RealWorld, ST, stToIO)
import Control.Monad.State.Strict (execState, get, put, liftIO)
import Optics.Core
import Optics.State
import Optics.State.Operators
import Data.Binary.Get (runGet)
import Data.ByteString (ByteString)
import Data.ByteString.Char8 qualified as BS
import Data.ByteString.Lazy qualified as BSLazy
import Data.Decimal (DecimalRaw(..))
import Data.Foldable (toList)
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe
import Data.Text (isPrefixOf, stripSuffix, intercalate, Text, pack, unpack)
import Data.Text qualified as Text
import Data.Text.Encoding (encodeUtf8)
import Data.Text.IO qualified as Text
import Data.Word (Word64)
import GHC.Natural
import System.IO (hFlush, stdout)
import Witch (unsafeInto, into)

data UnitTestOptions s = UnitTestOptions
  { forall {k} (s :: k). UnitTestOptions s -> RpcInfo
rpcInfo     :: Fetch.RpcInfo
  , forall {k} (s :: k). UnitTestOptions s -> SolverGroup
solvers     :: SolverGroup
  , forall {k} (s :: k). UnitTestOptions s -> Maybe Int
verbose     :: Maybe Int
  , forall {k} (s :: k). UnitTestOptions s -> Maybe Integer
maxIter     :: Maybe Integer
  , forall {k} (s :: k). UnitTestOptions s -> Integer
askSmtIters :: Integer
  , forall {k} (s :: k). UnitTestOptions s -> Maybe Natural
smtTimeout  :: Maybe Natural
  , forall {k} (s :: k). UnitTestOptions s -> Maybe Text
solver      :: Maybe Text
  , forall {k} (s :: k). UnitTestOptions s -> Text
match       :: Text
  , forall {k} (s :: k). UnitTestOptions s -> DappInfo
dapp        :: DappInfo
  , forall {k} (s :: k). UnitTestOptions s -> TestVMParams
testParams  :: TestVMParams
  , forall {k} (s :: k). UnitTestOptions s -> Bool
ffiAllowed  :: Bool
  , forall {k} (s :: k). UnitTestOptions s -> Bool
checkFailBit:: Bool
  }

data TestVMParams = TestVMParams
  { TestVMParams -> Expr 'EAddr
address       :: Expr EAddr
  , TestVMParams -> Expr 'EAddr
caller        :: Expr EAddr
  , TestVMParams -> Expr 'EAddr
origin        :: Expr EAddr
  , TestVMParams -> Word64
gasCreate     :: Word64
  , TestVMParams -> Word64
gasCall       :: Word64
  , TestVMParams -> W256
baseFee       :: W256
  , TestVMParams -> W256
priorityFee   :: W256
  , TestVMParams -> W256
balanceCreate :: W256
  , TestVMParams -> Expr 'EAddr
coinbase      :: Expr EAddr
  , TestVMParams -> W256
number        :: W256
  , TestVMParams -> W256
timestamp     :: W256
  , TestVMParams -> Word64
gaslimit      :: Word64
  , TestVMParams -> W256
gasprice      :: W256
  , TestVMParams -> W256
maxCodeSize   :: W256
  , TestVMParams -> W256
prevrandao    :: W256
  , TestVMParams -> W256
chainId       :: W256
  }

defaultGasForCreating :: Word64
defaultGasForCreating :: Word64
defaultGasForCreating = Word64
0xffffffffffff

defaultGasForInvoking :: Word64
defaultGasForInvoking :: Word64
defaultGasForInvoking = Word64
0xffffffffffff

defaultBalanceForTestContract :: W256
defaultBalanceForTestContract :: W256
defaultBalanceForTestContract = W256
0xffffffffffffffffffffffff

defaultMaxCodeSize :: W256
defaultMaxCodeSize :: W256
defaultMaxCodeSize = W256
0xffffffff

type ABIMethod = Text

-- | Used in various places for dumping traces
writeTraceDapp :: App m => DappInfo -> VM t RealWorld -> m ()
writeTraceDapp :: forall (m :: * -> *) (t :: VMType).
App m =>
DappInfo -> VM t RealWorld -> m ()
writeTraceDapp DappInfo
dapp VM t RealWorld
vm = do
  Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
  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
$ Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.dumpTrace (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Text -> IO ()
Text.writeFile FilePath
"VM.trace" (DappInfo -> VM t RealWorld -> Text
forall (t :: VMType) s. DappInfo -> VM t s -> Text
showTraceTree DappInfo
dapp VM t RealWorld
vm)

writeTrace :: App m => VM t RealWorld -> m ()
writeTrace :: forall (m :: * -> *) (t :: VMType). App m => VM t RealWorld -> m ()
writeTrace VM t RealWorld
vm = do
  Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
  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
$ Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.dumpTrace (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeFile FilePath
"VM.trace" (Forest Trace -> FilePath
forall a. Show a => a -> FilePath
show (Forest Trace -> FilePath) -> Forest Trace -> FilePath
forall a b. (a -> b) -> a -> b
$ VM t RealWorld -> Forest Trace
forall (t :: VMType) s. VM t s -> Forest Trace
traceForest VM t RealWorld
vm)

-- | Generate VeriOpts from UnitTestOptions
makeVeriOpts :: UnitTestOptions s -> VeriOpts
makeVeriOpts :: forall {k} (s :: k). UnitTestOptions s -> VeriOpts
makeVeriOpts UnitTestOptions s
opts =
   VeriOpts
defaultVeriOpts { maxIter = opts.maxIter
                   , askSmtIters = opts.askSmtIters
                   , rpcInfo = opts.rpcInfo
                   }

-- | Top level CLI endpoint for hevm test
unitTest :: App m => UnitTestOptions RealWorld -> Contracts -> m Bool
unitTest :: forall (m :: * -> *).
App m =>
UnitTestOptions RealWorld -> Contracts -> m Bool
unitTest UnitTestOptions RealWorld
opts (Contracts Map Text SolcContract
cs) = do
  let unitTestContrs :: [(Text, [Sig])]
unitTestContrs = Text -> [SolcContract] -> [(Text, [Sig])]
findUnitTests UnitTestOptions RealWorld
opts.match ([SolcContract] -> [(Text, [Sig])])
-> [SolcContract] -> [(Text, [Sig])]
forall a b. (a -> b) -> a -> b
$ Map Text SolcContract -> [SolcContract]
forall k a. Map k a -> [a]
Map.elems Map Text SolcContract
cs
  Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.debug (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
    FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Found " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show ([(Text, [Sig])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Text, [Sig])]
unitTestContrs) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" unit test contract(s) to test:"
    let x :: [Text]
x = ((Text, [Sig]) -> Text) -> [(Text, [Sig])] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\(Text
a,[Sig]
b) -> Text
"  --> " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"  ---  functions: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (FilePath -> Text
Text.pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ [Sig] -> FilePath
forall a. Show a => a -> FilePath
show [Sig]
b)) [(Text, [Sig])]
unitTestContrs
    FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ (Text -> FilePath) -> [Text] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Text -> FilePath
Text.unpack [Text]
x
  [Bool]
results <- ((Text, [Sig]) -> m [Bool]) -> [(Text, [Sig])] -> m [Bool]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (UnitTestOptions RealWorld
-> Map Text SolcContract -> (Text, [Sig]) -> m [Bool]
forall (m :: * -> *).
App m =>
UnitTestOptions RealWorld
-> Map Text SolcContract -> (Text, [Sig]) -> m [Bool]
runUnitTestContract UnitTestOptions RealWorld
opts Map Text SolcContract
cs) [(Text, [Sig])]
unitTestContrs
  Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
results

-- | Assuming a constructor is loaded, this stepper will run the constructor
-- to create the test contract, give it an initial balance, and run `setUp()'.
initializeUnitTest :: UnitTestOptions s -> SolcContract -> Stepper Concrete s ()
initializeUnitTest :: forall s.
UnitTestOptions s -> SolcContract -> Stepper 'Concrete s ()
initializeUnitTest UnitTestOptions s
opts SolcContract
theContract = do
  let addr :: Index (Map (Expr 'EAddr) Contract)
addr = UnitTestOptions s
opts.testParams.address

  EVM 'Concrete s () -> Stepper 'Concrete s ()
forall (t :: VMType) s a. EVM t s a -> Stepper t s a
Stepper.evm (EVM 'Concrete s () -> Stepper 'Concrete s ())
-> EVM 'Concrete s () -> Stepper 'Concrete s ()
forall a b. (a -> b) -> a -> b
$ do
    -- Make a trace entry for running the constructor
    TraceData -> EVM 'Concrete s ()
forall (t :: VMType) s. TraceData -> EVM t s ()
pushTrace (Text -> TraceData
EntryTrace Text
"constructor")

  -- Constructor is loaded; run until it returns code
  ProgramT
  (Action 'Concrete s) Identity (Either EvmError (Expr 'Buf))
-> Stepper 'Concrete s ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ProgramT
  (Action 'Concrete s) Identity (Either EvmError (Expr 'Buf))
forall s. Stepper 'Concrete s (Either EvmError (Expr 'Buf))
Stepper.execFully

  EVM 'Concrete s () -> Stepper 'Concrete s ()
forall (t :: VMType) s a. EVM t s a -> Stepper t s a
Stepper.evm (EVM 'Concrete s () -> Stepper 'Concrete s ())
-> EVM 'Concrete s () -> Stepper 'Concrete s ()
forall a b. (a -> b) -> a -> b
$ do
    -- Give a balance to the test target
    #env % #contracts % ix addr % #balance %= (`Expr.add` (Lit opts.testParams.balanceCreate))

    -- call setUp(), if it exists, to initialize the test contract
    let theAbi = theContract.abiMap
        setUp  = abiKeccak (encodeUtf8 "setUp()")
    when (isJust (Map.lookup setUp theAbi)) $ do
      abiCall opts.testParams (Left ("setUp()", emptyAbi))
      popTrace
      pushTrace (EntryTrace "setUp()")

  -- Let `setUp()' run to completion
  Either EvmError (Expr 'Buf)
res <- ProgramT
  (Action 'Concrete s) Identity (Either EvmError (Expr 'Buf))
forall s. Stepper 'Concrete s (Either EvmError (Expr 'Buf))
Stepper.execFully
  EVM 'Concrete s () -> Stepper 'Concrete s ()
forall (t :: VMType) s a. EVM t s a -> Stepper t s a
Stepper.evm (EVM 'Concrete s () -> Stepper 'Concrete s ())
-> EVM 'Concrete s () -> Stepper 'Concrete s ()
forall a b. (a -> b) -> a -> b
$ case Either EvmError (Expr 'Buf)
res of
    Left EvmError
e -> TraceData -> EVM 'Concrete s ()
forall (t :: VMType) s. TraceData -> EVM t s ()
pushTrace (EvmError -> TraceData
ErrorTrace EvmError
e)
    Either EvmError (Expr 'Buf)
_ -> EVM 'Concrete s ()
forall (t :: VMType) s. EVM t s ()
popTrace

runUnitTestContract
  :: App m
  => UnitTestOptions RealWorld
  -> Map Text SolcContract
  -> (Text, [Sig])
  -> m [Bool]
runUnitTestContract :: forall (m :: * -> *).
App m =>
UnitTestOptions RealWorld
-> Map Text SolcContract -> (Text, [Sig]) -> m [Bool]
runUnitTestContract
  opts :: UnitTestOptions RealWorld
opts@(UnitTestOptions {Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
DappInfo
SolverGroup
TestVMParams
$sel:rpcInfo:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> RpcInfo
$sel:solvers:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> SolverGroup
$sel:verbose:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Int
$sel:maxIter:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Integer
$sel:askSmtIters:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Integer
$sel:smtTimeout:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Natural
$sel:solver:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Text
$sel:match:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Text
$sel:dapp:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> DappInfo
$sel:testParams:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> TestVMParams
$sel:ffiAllowed:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$sel:checkFailBit:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
checkFailBit :: Bool
..}) Map Text SolcContract
contractMap (Text
name, [Sig]
testSigs) = do

  -- Print a header
  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
$ FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Checking " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show ([Sig] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sig]
testSigs) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" function(s) in contract " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Text -> FilePath
unpack Text
name

  -- Look for the wanted contract by name from the Solidity info
  case Text -> Map Text SolcContract -> Maybe SolcContract
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
name Map Text SolcContract
contractMap of
    Maybe SolcContract
Nothing ->
      -- Fail if there's no such contract
      FilePath -> m [Bool]
forall a. HasCallStack => FilePath -> a
internalError (FilePath -> m [Bool]) -> FilePath -> m [Bool]
forall a b. (a -> b) -> a -> b
$ FilePath
"Contract " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Text -> FilePath
unpack Text
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" not found"

    Just SolcContract
theContract -> do
      -- Construct the initial VM and begin the contract's constructor
      VM 'Concrete RealWorld
vm0 :: VM Concrete RealWorld <- IO (VM 'Concrete RealWorld) -> m (VM 'Concrete RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (VM 'Concrete RealWorld) -> m (VM 'Concrete RealWorld))
-> IO (VM 'Concrete RealWorld) -> m (VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld (VM 'Concrete RealWorld)
-> IO (VM 'Concrete RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (VM 'Concrete RealWorld)
 -> IO (VM 'Concrete RealWorld))
-> ST RealWorld (VM 'Concrete RealWorld)
-> IO (VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ UnitTestOptions RealWorld
-> SolcContract -> ST RealWorld (VM 'Concrete RealWorld)
forall (t :: VMType) s.
VMOps t =>
UnitTestOptions s -> SolcContract -> ST s (VM t s)
initialUnitTestVm UnitTestOptions RealWorld
opts SolcContract
theContract
      VM 'Concrete RealWorld
vm1 <- Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld
-> Stepper 'Concrete RealWorld (VM 'Concrete RealWorld)
-> m (VM 'Concrete RealWorld)
forall (m :: * -> *) a.
App m =>
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
Stepper.interpret (SolverGroup -> RpcInfo -> Fetcher 'Concrete m RealWorld
forall (t :: VMType) (m :: * -> *) s.
SolverGroup -> RpcInfo -> Fetcher t m s
Fetch.oracle SolverGroup
solvers RpcInfo
rpcInfo) VM 'Concrete RealWorld
vm0 (Stepper 'Concrete RealWorld (VM 'Concrete RealWorld)
 -> m (VM 'Concrete RealWorld))
-> Stepper 'Concrete RealWorld (VM 'Concrete RealWorld)
-> m (VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ do
        Text -> Stepper 'Concrete RealWorld ()
forall (t :: VMType) s. Text -> Stepper t s ()
Stepper.enter Text
name
        UnitTestOptions RealWorld
-> SolcContract -> Stepper 'Concrete RealWorld ()
forall s.
UnitTestOptions s -> SolcContract -> Stepper 'Concrete s ()
initializeUnitTest UnitTestOptions RealWorld
opts SolcContract
theContract
        EVM 'Concrete RealWorld (VM 'Concrete RealWorld)
-> Stepper 'Concrete RealWorld (VM 'Concrete RealWorld)
forall (t :: VMType) s a. EVM t s a -> Stepper t s a
Stepper.evm EVM 'Concrete RealWorld (VM 'Concrete RealWorld)
forall s (m :: * -> *). MonadState s m => m s
get

      DappInfo -> VM 'Concrete RealWorld -> m ()
forall (m :: * -> *) (t :: VMType).
App m =>
DappInfo -> VM t RealWorld -> m ()
writeTraceDapp DappInfo
dapp VM 'Concrete RealWorld
vm1
      case VM 'Concrete RealWorld
vm1.result of
        Just (VMFailure EvmError
_) -> IO [Bool] -> m [Bool]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Bool] -> m [Bool]) -> IO [Bool] -> m [Bool]
forall a b. (a -> b) -> a -> b
$ do
          Text -> IO ()
Text.putStrLn Text
"\x1b[31m[BAIL]\x1b[0m setUp() "
          Text -> IO ()
tick (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ VM 'Concrete RealWorld -> UnitTestOptions RealWorld -> Text -> Text
forall (t :: VMType) s. VM t s -> UnitTestOptions s -> Text -> Text
failOutput VM 'Concrete RealWorld
vm1 UnitTestOptions RealWorld
opts Text
"setUp()"
          [Bool] -> IO [Bool]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Bool
False]
        Just (VMSuccess Expr 'Buf
_) -> do
          [Sig] -> (Sig -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Sig]
testSigs ((Sig -> m Bool) -> m [Bool]) -> (Sig -> m Bool) -> m [Bool]
forall a b. (a -> b) -> a -> b
$ \Sig
s -> UnitTestOptions RealWorld
-> VM 'Concrete RealWorld -> Sig -> m Bool
forall (m :: * -> *).
App m =>
UnitTestOptions RealWorld
-> VM 'Concrete RealWorld -> Sig -> m Bool
symRun UnitTestOptions RealWorld
opts VM 'Concrete RealWorld
vm1 Sig
s
        Maybe (VMResult 'Concrete RealWorld)
_ -> FilePath -> m [Bool]
forall a. HasCallStack => FilePath -> a
internalError FilePath
"setUp() did not end with a result"

-- | Define the thread spawner for symbolic tests
symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m Bool
symRun :: forall (m :: * -> *).
App m =>
UnitTestOptions RealWorld
-> VM 'Concrete RealWorld -> Sig -> m Bool
symRun opts :: UnitTestOptions RealWorld
opts@UnitTestOptions{Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
DappInfo
SolverGroup
TestVMParams
$sel:rpcInfo:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> RpcInfo
$sel:solvers:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> SolverGroup
$sel:verbose:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Int
$sel:maxIter:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Integer
$sel:askSmtIters:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Integer
$sel:smtTimeout:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Natural
$sel:solver:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Text
$sel:match:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Text
$sel:dapp:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> DappInfo
$sel:testParams:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> TestVMParams
$sel:ffiAllowed:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$sel:checkFailBit:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
checkFailBit :: Bool
..} VM 'Concrete RealWorld
vm (Sig Text
testName [AbiType]
types) = do
    let callSig :: Text
callSig = Text
testName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (Text -> [Text] -> Text
Text.intercalate Text
"," ((AbiType -> Text) -> [AbiType] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map AbiType -> Text
abiTypeSolidity [AbiType]
types)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
    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
$ FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"\x1b[96m[RUNNING]\x1b[0m " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Text -> FilePath
Text.unpack Text
callSig
    let cd :: (Expr 'Buf, [Prop])
cd = Text -> [AbiType] -> [FilePath] -> Expr 'Buf -> (Expr 'Buf, [Prop])
symCalldata Text
callSig [AbiType]
types [] (Text -> Expr 'Buf
AbstractBuf Text
"txdata")
        shouldFail :: Bool
shouldFail = Text
"proveFail" Text -> Text -> Bool
`isPrefixOf` Text
callSig

    -- define postcondition depending on `shouldFail`
    let testContract :: Map (Expr 'EAddr) (Expr 'EContract) -> Expr 'EContract
testContract Map (Expr 'EAddr) (Expr 'EContract)
store = Expr 'EContract -> Maybe (Expr 'EContract) -> Expr 'EContract
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> Expr 'EContract
forall a. HasCallStack => FilePath -> a
internalError FilePath
"test contract not found in state") (Expr 'EAddr
-> Map (Expr 'EAddr) (Expr 'EContract) -> Maybe (Expr 'EContract)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VM 'Concrete RealWorld
vm.state.contract Map (Expr 'EAddr) (Expr 'EContract)
store)
        failed :: Map (Expr 'EAddr) (Expr 'EContract) -> Prop
failed Map (Expr 'EAddr) (Expr 'EContract)
store = case Expr 'EAddr
-> Map (Expr 'EAddr) (Expr 'EContract) -> Maybe (Expr 'EContract)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr 'EAddr
cheatCode Map (Expr 'EAddr) (Expr 'EContract)
store of
          Just Expr 'EContract
cheatContract -> Expr 'EWord -> Expr 'Storage -> Expr 'EWord
Expr.readStorage' (W256 -> Expr 'EWord
Lit W256
0x6661696c65640000000000000000000000000000000000000000000000000000) Expr 'EContract
cheatContract.storage Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
.== W256 -> Expr 'EWord
Lit W256
1
          Maybe (Expr 'EContract)
Nothing -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
And (Expr 'EWord -> Expr 'Storage -> Expr 'EWord
Expr.readStorage' (W256 -> Expr 'EWord
Lit W256
0) (Map (Expr 'EAddr) (Expr 'EContract) -> Expr 'EContract
testContract Map (Expr 'EAddr) (Expr 'EContract)
store).storage) (W256 -> Expr 'EWord
Lit W256
2) Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
.== W256 -> Expr 'EWord
Lit W256
2
        postcondition :: VM 'Symbolic RealWorld -> Expr 'End -> Prop
postcondition = ((VM 'Symbolic RealWorld, Expr 'End) -> Prop)
-> VM 'Symbolic RealWorld -> Expr 'End -> Prop
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((VM 'Symbolic RealWorld, Expr 'End) -> Prop)
 -> VM 'Symbolic RealWorld -> Expr 'End -> Prop)
-> ((VM 'Symbolic RealWorld, Expr 'End) -> Prop)
-> VM 'Symbolic RealWorld
-> Expr 'End
-> Prop
forall a b. (a -> b) -> a -> b
$ case Bool
shouldFail of
          Bool
True -> \(VM 'Symbolic RealWorld
_, Expr 'End
post) -> case Expr 'End
post of
            Success [Prop]
_ TraceContext
_ Expr 'Buf
_ Map (Expr 'EAddr) (Expr 'EContract)
store -> if UnitTestOptions RealWorld
opts.checkFailBit then Map (Expr 'EAddr) (Expr 'EContract) -> Prop
failed Map (Expr 'EAddr) (Expr 'EContract)
store else Bool -> Prop
PBool Bool
False
            Expr 'End
_ -> Bool -> Prop
PBool Bool
True
          Bool
False -> \(VM 'Symbolic RealWorld
_, Expr 'End
post) -> case Expr 'End
post of
            Success [Prop]
_ TraceContext
_ Expr 'Buf
_ Map (Expr 'EAddr) (Expr 'EContract)
store -> if UnitTestOptions RealWorld
opts.checkFailBit then Prop -> Prop
PNeg (Map (Expr 'EAddr) (Expr 'EContract) -> Prop
failed Map (Expr 'EAddr) (Expr 'EContract)
store) else Bool -> Prop
PBool Bool
True
            Failure [Prop]
_ TraceContext
_ (Revert Expr 'Buf
msg) -> case Expr 'Buf
msg of
              ConcreteBuf ByteString
b ->
                if (ByteString -> ByteString -> Bool
BS.isPrefixOf (Text -> ByteString
selector Text
"Error(string)") ByteString
b) Bool -> Bool -> Bool
|| ByteString
b ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== Word256 -> ByteString
panicMsg Word256
0x01 then Bool -> Prop
PBool Bool
False
                else Bool -> Prop
PBool Bool
True
              Expr 'Buf
b -> Expr 'Buf
b Expr 'Buf -> Expr 'Buf -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= ByteString -> Expr 'Buf
ConcreteBuf (Word256 -> ByteString
panicMsg Word256
0x01)
            Failure [Prop]
_ TraceContext
_ EvmError
_ -> Bool -> Prop
PBool Bool
True
            Partial [Prop]
_ TraceContext
_ PartialExec
_ -> Bool -> Prop
PBool Bool
True
            Expr 'End
_ -> FilePath -> Prop
forall a. HasCallStack => FilePath -> a
internalError FilePath
"Invalid leaf node"

    VM 'Concrete RealWorld
vm' <- Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld
-> Stepper 'Concrete RealWorld (VM 'Concrete RealWorld)
-> m (VM 'Concrete RealWorld)
forall (m :: * -> *) a.
App m =>
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
Stepper.interpret (SolverGroup -> RpcInfo -> Fetcher 'Concrete m RealWorld
forall (t :: VMType) (m :: * -> *) s.
SolverGroup -> RpcInfo -> Fetcher t m s
Fetch.oracle SolverGroup
solvers RpcInfo
rpcInfo) VM 'Concrete RealWorld
vm (Stepper 'Concrete RealWorld (VM 'Concrete RealWorld)
 -> m (VM 'Concrete RealWorld))
-> Stepper 'Concrete RealWorld (VM 'Concrete RealWorld)
-> m (VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$
      EVM 'Concrete RealWorld (VM 'Concrete RealWorld)
-> Stepper 'Concrete RealWorld (VM 'Concrete RealWorld)
forall (t :: VMType) s a. EVM t s a -> Stepper t s a
Stepper.evm (EVM 'Concrete RealWorld (VM 'Concrete RealWorld)
 -> Stepper 'Concrete RealWorld (VM 'Concrete RealWorld))
-> EVM 'Concrete RealWorld (VM 'Concrete RealWorld)
-> Stepper 'Concrete RealWorld (VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ do
        TraceData -> EVM 'Concrete RealWorld ()
forall (t :: VMType) s. TraceData -> EVM t s ()
pushTrace (Text -> TraceData
EntryTrace Text
testName)
        TestVMParams -> (Expr 'Buf, [Prop]) -> EVM 'Concrete RealWorld ()
forall (t :: VMType) s.
VMOps t =>
TestVMParams -> (Expr 'Buf, [Prop]) -> EVM t s ()
makeTxCall TestVMParams
testParams (Expr 'Buf, [Prop])
cd
        EVM 'Concrete RealWorld (VM 'Concrete RealWorld)
forall s (m :: * -> *). MonadState s m => m s
get
    DappInfo -> VM 'Concrete RealWorld -> m ()
forall (m :: * -> *) (t :: VMType).
App m =>
DappInfo -> VM t RealWorld -> m ()
writeTraceDapp DappInfo
dapp VM 'Concrete RealWorld
vm'

    -- check postconditions against vm
    (Expr 'End
e, [VerifyResult]
results) <- SolverGroup
-> VeriOpts
-> VM 'Symbolic RealWorld
-> Maybe (VM 'Symbolic RealWorld -> Expr 'End -> Prop)
-> m (Expr 'End, [VerifyResult])
forall (m :: * -> *).
App m =>
SolverGroup
-> VeriOpts
-> VM 'Symbolic RealWorld
-> Maybe (VM 'Symbolic RealWorld -> Expr 'End -> Prop)
-> m (Expr 'End, [VerifyResult])
verify SolverGroup
solvers (UnitTestOptions RealWorld -> VeriOpts
forall {k} (s :: k). UnitTestOptions s -> VeriOpts
makeVeriOpts UnitTestOptions RealWorld
opts) (VM 'Concrete RealWorld -> VM 'Symbolic RealWorld
forall s. VM 'Concrete s -> VM 'Symbolic s
symbolify VM 'Concrete RealWorld
vm') ((VM 'Symbolic RealWorld -> Expr 'End -> Prop)
-> Maybe (VM 'Symbolic RealWorld -> Expr 'End -> Prop)
forall a. a -> Maybe a
Just VM 'Symbolic RealWorld -> Expr 'End -> Prop
postcondition)
    let allReverts :: Bool
allReverts = Bool -> Bool
not (Bool -> Bool) -> (Expr 'End -> Bool) -> Expr 'End -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'End -> Bool) -> [Expr 'End] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr 'End -> Bool
Expr.isSuccess) ([Expr 'End] -> Bool)
-> (Expr 'End -> [Expr 'End]) -> Expr 'End -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'End -> [Expr 'End]
flattenExpr (Expr 'End -> Bool) -> Expr 'End -> Bool
forall a b. (a -> b) -> a -> b
$ Expr 'End
e

    Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.debug (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ [Expr 'End] -> (Expr 'End -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((Expr 'End -> Bool) -> [Expr 'End] -> [Expr 'End]
forall a. (a -> Bool) -> [a] -> [a]
filter Expr 'End -> Bool
Expr.isFailure (Expr 'End -> [Expr 'End]
flattenExpr Expr 'End
e)) ((Expr 'End -> IO ()) -> IO ()) -> (Expr 'End -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \case
      (Failure [Prop]
_ TraceContext
_ EvmError
a) ->  FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"   -> debug of func: " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Text -> FilePath
Text.unpack Text
testName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" Failure at the end of expr: " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> EvmError -> FilePath
forall a. Show a => a -> FilePath
show EvmError
a;
      Expr 'End
_ -> FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
internalError FilePath
"cannot be, filtered for failure"
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((VerifyResult -> Bool) -> [VerifyResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any VerifyResult -> Bool
forall a b c d. ProofResult a b c d -> Bool
isUnknown [VerifyResult]
results Bool -> Bool -> Bool
|| (VerifyResult -> Bool) -> [VerifyResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any VerifyResult -> Bool
forall a b c d. ProofResult a b c d -> Bool
isError [VerifyResult]
results) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
      FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Text -> FilePath
Text.unpack Text
testName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" due to: ";
      [(Integer, FilePath)] -> ((Integer, FilePath) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([VerifyResult] -> [(Integer, FilePath)]
forall a b c. [ProofResult a b c FilePath] -> [(Integer, FilePath)]
groupIssues ((VerifyResult -> Bool) -> [VerifyResult] -> [VerifyResult]
forall a. (a -> Bool) -> [a] -> [a]
filter VerifyResult -> Bool
forall a b c d. ProofResult a b c d -> Bool
isError [VerifyResult]
results)) (((Integer, FilePath) -> IO ()) -> IO ())
-> ((Integer, FilePath) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Integer
num, FilePath
str) -> FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"      " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
num FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"x -> " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
str
      [(Integer, FilePath)] -> ((Integer, FilePath) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([VerifyResult] -> [(Integer, FilePath)]
forall a b c. [ProofResult a b c FilePath] -> [(Integer, FilePath)]
groupIssues ((VerifyResult -> Bool) -> [VerifyResult] -> [VerifyResult]
forall a. (a -> Bool) -> [a] -> [a]
filter VerifyResult -> Bool
forall a b c d. ProofResult a b c d -> Bool
isUnknown [VerifyResult]
results)) (((Integer, FilePath) -> IO ()) -> IO ())
-> ((Integer, FilePath) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Integer
num, FilePath
str) -> FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"      " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
num FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"x -> " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
str

    -- display results
    if (VerifyResult -> Bool) -> [VerifyResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all VerifyResult -> Bool
forall a b c d. ProofResult a b c d -> Bool
isQed [VerifyResult]
results
    then if Bool
allReverts Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
shouldFail)
         then do
           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
$ FilePath -> IO ()
putStr (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"   \x1b[31m[FAIL]\x1b[0m " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Text -> FilePath
Text.unpack Text
testName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Text -> FilePath
Text.unpack Text
allBranchRev
           Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
         else do
           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
$ FilePath -> IO ()
putStr (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"   \x1b[32m[PASS]\x1b[0m " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Text -> FilePath
Text.unpack Text
testName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"\n"
           Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    else do
      -- not all is Qed
      let x :: [(Expr 'End, SMTCex)]
x = (VerifyResult -> Maybe (Expr 'End, SMTCex))
-> [VerifyResult] -> [(Expr 'End, SMTCex)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe VerifyResult -> Maybe (Expr 'End, SMTCex)
extractCex [VerifyResult]
results
      let y :: Text
y = UnitTestOptions RealWorld
-> Text -> Expr 'Buf -> [AbiType] -> [(Expr 'End, SMTCex)] -> Text
symFailure UnitTestOptions RealWorld
opts Text
testName ((Expr 'Buf, [Prop]) -> Expr 'Buf
forall a b. (a, b) -> a
fst (Expr 'Buf, [Prop])
cd) [AbiType]
types [(Expr 'End, SMTCex)]
x
      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
$ FilePath -> IO ()
putStr (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"   \x1b[31m[FAIL]\x1b[0m " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Text -> FilePath
Text.unpack Text
testName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Text -> FilePath
Text.unpack Text
y
      Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

allBranchRev :: Text
allBranchRev :: Text
allBranchRev = Text -> [Text] -> Text
intercalate Text
"\n"
  [ [Text] -> Text
Text.concat ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
indentLines Int
3 (Text -> Text) -> [Text] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [ Text
"Reason:"
      , Text
"  No reachable assertion violations, but all branches reverted"
      , Text
"  Prefix this testname with `proveFail` if this is expected"
      ]
  ]
symFailure :: UnitTestOptions RealWorld -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> Text
symFailure :: UnitTestOptions RealWorld
-> Text -> Expr 'Buf -> [AbiType] -> [(Expr 'End, SMTCex)] -> Text
symFailure UnitTestOptions {Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
DappInfo
SolverGroup
TestVMParams
$sel:rpcInfo:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> RpcInfo
$sel:solvers:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> SolverGroup
$sel:verbose:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Int
$sel:maxIter:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Integer
$sel:askSmtIters:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Integer
$sel:smtTimeout:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Natural
$sel:solver:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Text
$sel:match:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Text
$sel:dapp:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> DappInfo
$sel:testParams:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> TestVMParams
$sel:ffiAllowed:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$sel:checkFailBit:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
checkFailBit :: Bool
..} Text
testName Expr 'Buf
cd [AbiType]
types [(Expr 'End, SMTCex)]
failures' =
  [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
    [ [Text] -> Text
Text.concat ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
indentLines Int
3 (Text -> Text)
-> ((Expr 'End, SMTCex) -> Text) -> (Expr 'End, SMTCex) -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'End, SMTCex) -> Text
mkMsg ((Expr 'End, SMTCex) -> Text) -> [(Expr 'End, SMTCex)] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Expr 'End, SMTCex)]
failures'
    ]
    where
      showRes :: Expr 'End -> Text
showRes = \case
        Success [Prop]
_ TraceContext
_ Expr 'Buf
_ Map (Expr 'EAddr) (Expr 'EContract)
_ -> if Text
"proveFail" Text -> Text -> Bool
`isPrefixOf` Text
testName
                           then Text
"Successful execution"
                           else Text
"Failed: Test Assertion Violation"
        Expr 'End
res ->
          let ?context = TraceContext -> DappContext
dappContext (Expr 'End -> TraceContext
traceContext Expr 'End
res)
          in FilePath -> Text
Text.pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'End -> FilePath
prettyvmresult Expr 'End
res
      mkMsg :: (Expr 'End, SMTCex) -> Text
mkMsg (Expr 'End
leaf, SMTCex
cex) = Text -> [Text] -> Text
intercalate Text
"\n" ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$
        [Text
"Counterexample:"
        ,Text
"  result:   " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Expr 'End -> Text
showRes Expr 'End
leaf
        ,Text
"  calldata: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> let ?context = TraceContext -> DappContext
dappContext (Expr 'End -> TraceContext
traceContext Expr 'End
leaf)
                           in SMTCex -> Expr 'Buf -> Text -> [AbiType] -> Text
prettyCalldata SMTCex
cex Expr 'Buf
cd Text
testName [AbiType]
types
        ] [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> Expr 'End -> [Text]
verbText Expr 'End
leaf
      verbText :: Expr 'End -> [Text]
verbText Expr 'End
leaf = case Maybe Int
verbose of
            Just Int
_ -> [[Text] -> Text
Text.unlines [ Int -> Text -> Text
indentLines Int
2 (DappInfo -> Expr 'End -> Text
showTraceTree' DappInfo
dapp Expr 'End
leaf)]]
            Maybe Int
_ -> [Text]
forall a. Monoid a => a
mempty
      dappContext :: TraceContext -> DappContext
dappContext TraceContext { Map (Expr 'EAddr) Contract
contracts :: Map (Expr 'EAddr) Contract
$sel:contracts:TraceContext :: TraceContext -> Map (Expr 'EAddr) Contract
contracts, Map Addr Text
labels :: Map Addr Text
$sel:labels:TraceContext :: TraceContext -> Map Addr Text
labels } =
        DappContext { $sel:info:DappContext :: DappInfo
info = DappInfo
dapp, Map (Expr 'EAddr) Contract
contracts :: Map (Expr 'EAddr) Contract
$sel:contracts:DappContext :: Map (Expr 'EAddr) Contract
contracts, Map Addr Text
labels :: Map Addr Text
$sel:labels:DappContext :: Map Addr Text
labels }

indentLines :: Int -> Text -> Text
indentLines :: Int -> Text -> Text
indentLines Int
n Text
s =
  let p :: Text
p = Int -> Text -> Text
Text.replicate Int
n Text
" "
  in [Text] -> Text
Text.unlines ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text
p <>) (Text -> [Text]
Text.lines Text
s))

passOutput :: VM t s -> UnitTestOptions s -> Text -> Text
passOutput :: forall (t :: VMType) s. VM t s -> UnitTestOptions s -> Text -> Text
passOutput VM t s
vm UnitTestOptions { Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
DappInfo
SolverGroup
TestVMParams
$sel:rpcInfo:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> RpcInfo
$sel:solvers:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> SolverGroup
$sel:verbose:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Int
$sel:maxIter:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Integer
$sel:askSmtIters:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Integer
$sel:smtTimeout:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Natural
$sel:solver:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Text
$sel:match:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Text
$sel:dapp:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> DappInfo
$sel:testParams:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> TestVMParams
$sel:ffiAllowed:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$sel:checkFailBit:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
checkFailBit :: Bool
.. } Text
testName =
  let ?context = DappContext { $sel:info:DappContext :: DappInfo
info = DappInfo
dapp
                             , $sel:contracts:DappContext :: Map (Expr 'EAddr) Contract
contracts = VM t s
vm.env.contracts
                             , $sel:labels:DappContext :: Map Addr Text
labels = VM t s
vm.labels }
  in let v :: Int
v = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 Maybe Int
verbose
  in if (Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) then
    [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
      [ Text
"Success: "
      , Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
"" (Text -> Text -> Maybe Text
stripSuffix Text
"()" Text
testName)
      , Text
"\n"
      , if (Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2) then Int -> Text -> Text
indentLines Int
2 (DappInfo -> VM t s -> Text
forall (t :: VMType) s. DappInfo -> VM t s -> Text
showTraceTree DappInfo
dapp VM t s
vm) else Text
""
      , Int -> Text -> Text
indentLines Int
2 ((?context::DappContext) => Map W256 Event -> [Expr 'Log] -> Text
Map W256 Event -> [Expr 'Log] -> Text
formatTestLogs DappInfo
dapp.eventMap VM t s
vm.logs)
      , Text
"\n"
      ]
    else Text
""

failOutput :: VM t s -> UnitTestOptions s -> Text -> Text
failOutput :: forall (t :: VMType) s. VM t s -> UnitTestOptions s -> Text -> Text
failOutput VM t s
vm UnitTestOptions { Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
DappInfo
SolverGroup
TestVMParams
$sel:rpcInfo:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> RpcInfo
$sel:solvers:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> SolverGroup
$sel:verbose:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Int
$sel:maxIter:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Integer
$sel:askSmtIters:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Integer
$sel:smtTimeout:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Natural
$sel:solver:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Text
$sel:match:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Text
$sel:dapp:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> DappInfo
$sel:testParams:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> TestVMParams
$sel:ffiAllowed:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$sel:checkFailBit:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
checkFailBit :: Bool
.. } Text
testName =
  let ?context = DappContext { $sel:info:DappContext :: DappInfo
info = DappInfo
dapp
                             , $sel:contracts:DappContext :: Map (Expr 'EAddr) Contract
contracts = VM t s
vm.env.contracts
                             , $sel:labels:DappContext :: Map Addr Text
labels = VM t s
vm.labels }
  in [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
  [ Text
"Failure: "
  , Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
"" (Text -> Text -> Maybe Text
stripSuffix Text
"()" Text
testName)
  , Text
"\n"
  , case Maybe Int
verbose of
      Just Int
_ -> Int -> Text -> Text
indentLines Int
2 (DappInfo -> VM t s -> Text
forall (t :: VMType) s. DappInfo -> VM t s -> Text
showTraceTree DappInfo
dapp VM t s
vm)
      Maybe Int
_ -> Text
""
  , Int -> Text -> Text
indentLines Int
2 ((?context::DappContext) => Map W256 Event -> [Expr 'Log] -> Text
Map W256 Event -> [Expr 'Log] -> Text
formatTestLogs DappInfo
dapp.eventMap VM t s
vm.logs)
  , Text
"\n"
  ]

formatTestLogs :: (?context :: DappContext) => Map W256 Event -> [Expr Log] -> Text
formatTestLogs :: (?context::DappContext) => Map W256 Event -> [Expr 'Log] -> Text
formatTestLogs Map W256 Event
events [Expr 'Log]
xs =
  case [Maybe Text] -> [Text]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Text] -> [Maybe Text]
forall a. [a] -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ((Expr 'Log -> Maybe Text) -> [Expr 'Log] -> [Maybe Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((?context::DappContext) =>
Map W256 Event -> Expr 'Log -> Maybe Text
Map W256 Event -> Expr 'Log -> Maybe Text
formatTestLog Map W256 Event
events) [Expr 'Log]
xs)) of
    [] -> Text
"\n"
    [Text]
ys -> Text
"\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
intercalate Text
"\n" [Text]
ys Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\n"

-- Here we catch and render some special logs emitted by ds-test,
-- with the intent to then present them in a separate view to the
-- regular trace output.
formatTestLog :: (?context :: DappContext) => Map W256 Event -> Expr Log -> Maybe Text
formatTestLog :: (?context::DappContext) =>
Map W256 Event -> Expr 'Log -> Maybe Text
formatTestLog Map W256 Event
_ (LogEntry Expr 'EWord
_ Expr 'Buf
_ []) = Maybe Text
forall a. Maybe a
Nothing
formatTestLog Map W256 Event
_ (GVar GVar 'Log
_) = FilePath -> Maybe Text
forall a. HasCallStack => FilePath -> a
internalError FilePath
"unexpected global variable"
formatTestLog Map W256 Event
events (LogEntry Expr 'EWord
_ Expr 'Buf
args (Expr 'EWord
topic:[Expr 'EWord]
_)) =
  case Expr 'EWord -> Maybe W256
maybeLitWord Expr 'EWord
topic Maybe W256 -> (W256 -> Maybe Event) -> Maybe Event
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \W256
t1 -> (W256 -> Map W256 Event -> Maybe Event
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup W256
t1 Map W256 Event
events) of
    Maybe Event
Nothing -> Maybe Text
forall a. Maybe a
Nothing
    Just (Event Text
name Anonymity
_ [(Text, AbiType, Indexed)]
argInfos) ->
      case (Text
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
parenthesise (AbiType -> Text
abiTypeSolidity (AbiType -> Text) -> [AbiType] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AbiType]
argTypes)) of
        Text
"log(string)" -> Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Text -> Text
unquote (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ (?context::DappContext) => AbiType -> Expr 'Buf -> Text
AbiType -> Expr 'Buf -> Text
showValue AbiType
AbiStringType Expr 'Buf
args

        -- log_named_x(string, x)
        Text
"log_named_bytes32(string, bytes32)" -> Maybe Text
log_named
        Text
"log_named_address(string, address)" -> Maybe Text
log_named
        Text
"log_named_int(string, int256)"      -> Maybe Text
log_named
        Text
"log_named_uint(string, uint256)"    -> Maybe Text
log_named
        Text
"log_named_bytes(string, bytes)"     -> Maybe Text
log_named
        Text
"log_named_string(string, string)"   -> Maybe Text
log_named

        -- log_named_decimal_x(string, uint, x)
        Text
"log_named_decimal_int(string, int256, uint256)"   -> Maybe Text
log_named_decimal
        Text
"log_named_decimal_uint(string, uint256, uint256)" -> Maybe Text
log_named_decimal

        -- log_x(x)
        Text
"log_bytes32(bytes32)" -> Maybe Text
log_unnamed
        Text
"log_address(address)" -> Maybe Text
log_unnamed
        Text
"log_int(int256)"      -> Maybe Text
log_unnamed
        Text
"log_uint(uint256)"    -> Maybe Text
log_unnamed
        Text
"log_bytes(bytes)"     -> Maybe Text
log_unnamed
        Text
"log_string(string)"   -> Maybe Text
log_unnamed

        -- log_named_x(bytes32, x), as used in older versions of ds-test.
        -- bytes32 are opportunistically represented as strings in Format.hs
        Text
"log_named_bytes32(bytes32, bytes32)" -> Maybe Text
log_named
        Text
"log_named_address(bytes32, address)" -> Maybe Text
log_named
        Text
"log_named_int(bytes32, int256)"      -> Maybe Text
log_named
        Text
"log_named_uint(bytes32, uint256)"    -> Maybe Text
log_named

        Text
_ -> Maybe Text
forall a. Maybe a
Nothing

        where
          argTypes :: [AbiType]
argTypes = [AbiType
argType | (Text
_, AbiType
argType, Indexed
NotIndexed) <- [(Text, AbiType, Indexed)]
argInfos]
          unquote :: Text -> Text
unquote = (Char -> Bool) -> Text -> Text
Text.dropAround (\Char
c -> Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'"' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'«' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'»')
          log_unnamed :: Maybe Text
log_unnamed =
            Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ (?context::DappContext) => AbiType -> Expr 'Buf -> Text
AbiType -> Expr 'Buf -> Text
showValue ([AbiType] -> AbiType
forall a. HasCallStack => [a] -> a
head [AbiType]
argTypes) Expr 'Buf
args
          log_named :: Maybe Text
log_named =
            let (Text
key, Text
val) = case Int -> [Text] -> [Text]
forall a. Int -> [a] -> [a]
take Int
2 ((?context::DappContext) => [AbiType] -> Expr 'Buf -> [Text]
[AbiType] -> Expr 'Buf -> [Text]
textValues [AbiType]
argTypes Expr 'Buf
args) of
                  [Text
k, Text
v] -> (Text
k, Text
v)
                  [Text]
_ -> FilePath -> (Text, Text)
forall a. HasCallStack => FilePath -> a
internalError FilePath
"shouldn't happen"
            in Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Text -> Text
unquote Text
key Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
val
          showDecimal :: source -> i -> Text
showDecimal source
dec i
val =
            FilePath -> Text
pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ DecimalRaw i -> FilePath
forall a. Show a => a -> FilePath
show (DecimalRaw i -> FilePath) -> DecimalRaw i -> FilePath
forall a b. (a -> b) -> a -> b
$ Word8 -> i -> DecimalRaw i
forall i. Word8 -> i -> DecimalRaw i
Decimal (source -> Word8
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto source
dec) i
val
          log_named_decimal :: Maybe Text
log_named_decimal =
            case Expr 'Buf
args of
              (ConcreteBuf ByteString
b) ->
                case Vector AbiValue -> [AbiValue]
forall a. Vector a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Vector AbiValue -> [AbiValue]) -> Vector AbiValue -> [AbiValue]
forall a b. (a -> b) -> a -> b
$ Get (Vector AbiValue) -> ByteString -> Vector AbiValue
forall a. Get a -> ByteString -> a
runGet (Int -> [AbiType] -> Get (Vector AbiValue)
getAbiSeq ([AbiType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AbiType]
argTypes) [AbiType]
argTypes) (ByteString -> ByteString
BSLazy.fromStrict ByteString
b) of
                  [AbiValue
key, (AbiUInt Int
256 Word256
val), (AbiUInt Int
256 Word256
dec)] ->
                    Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ (Text -> Text
unquote ((?context::DappContext) => AbiValue -> Text
AbiValue -> Text
showAbiValue AbiValue
key)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word256 -> Word256 -> Text
forall {i} {source}.
(Integral i, TryFrom source Word8, Show i, Show source,
 Typeable source) =>
source -> i -> Text
showDecimal Word256
dec Word256
val
                  [AbiValue
key, (AbiInt Int
256 Int256
val), (AbiUInt Int
256 Word256
dec)] ->
                    Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ (Text -> Text
unquote ((?context::DappContext) => AbiValue -> Text
AbiValue -> Text
showAbiValue AbiValue
key)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word256 -> Int256 -> Text
forall {i} {source}.
(Integral i, TryFrom source Word8, Show i, Show source,
 Typeable source) =>
source -> i -> Text
showDecimal Word256
dec Int256
val
                  [AbiValue]
_ -> Maybe Text
forall a. Maybe a
Nothing
              Expr 'Buf
_ -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"<symbolic decimal>"

abiCall :: VMOps t => TestVMParams -> Either (Text, AbiValue) ByteString -> EVM t s ()
abiCall :: forall (t :: VMType) s.
VMOps t =>
TestVMParams -> Either (Text, AbiValue) ByteString -> EVM t s ()
abiCall TestVMParams
params Either (Text, AbiValue) ByteString
args =
  let cd :: ByteString
cd = case Either (Text, AbiValue) ByteString
args of
        Left (Text
sig, AbiValue
args') -> Text -> AbiValue -> ByteString
abiMethod Text
sig AbiValue
args'
        Right ByteString
b -> ByteString
b
  in TestVMParams -> (Expr 'Buf, [Prop]) -> EVM t s ()
forall (t :: VMType) s.
VMOps t =>
TestVMParams -> (Expr 'Buf, [Prop]) -> EVM t s ()
makeTxCall TestVMParams
params (ByteString -> Expr 'Buf
ConcreteBuf ByteString
cd, [])

makeTxCall :: VMOps t => TestVMParams -> (Expr Buf, [Prop]) -> EVM t s ()
makeTxCall :: forall (t :: VMType) s.
VMOps t =>
TestVMParams -> (Expr 'Buf, [Prop]) -> EVM t s ()
makeTxCall TestVMParams
params (Expr 'Buf
cd, [Prop]
cdProps) = do
  EVM t s ()
forall (t :: VMType) s. VMOps t => EVM t s ()
resetState
  Optic A_Lens NoIx (VM t s) (VM t s) Bool Bool -> Bool -> EVM t s ()
forall k s (m :: * -> *) (is :: IxList) a b.
(Is k A_Setter, MonadState s m) =>
Optic k is s s a b -> b -> m ()
assign (Optic A_Lens NoIx (VM t s) (VM t s) TxState TxState
#tx Optic A_Lens NoIx (VM t s) (VM t s) TxState TxState
-> Optic A_Lens NoIx TxState TxState Bool Bool
-> Optic A_Lens NoIx (VM t s) (VM t s) Bool Bool
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic A_Lens NoIx TxState TxState Bool Bool
#isCreate) Bool
False
  State (VM t s) () -> VM t s -> VM t s
forall s a. State s a -> s -> s
execState (Expr 'EAddr -> State (VM t s) ()
forall (t :: VMType) s. Expr 'EAddr -> State (VM t s) ()
loadContract TestVMParams
params.address) (VM t s -> VM t s)
-> StateT (VM t s) (ST s) (VM t s)
-> StateT (VM t s) (ST s) (VM t s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (VM t s) (ST s) (VM t s)
forall s (m :: * -> *). MonadState s m => m s
get StateT (VM t s) (ST s) (VM t s)
-> (VM t s -> EVM t s ()) -> EVM t s ()
forall a b.
StateT (VM t s) (ST s) a
-> (a -> StateT (VM t s) (ST s) b) -> StateT (VM t s) (ST s) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VM t s -> EVM t s ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put
  Optic A_Lens NoIx (VM t s) (VM t s) (Expr 'Buf) (Expr 'Buf)
-> Expr 'Buf -> EVM t s ()
forall k s (m :: * -> *) (is :: IxList) a b.
(Is k A_Setter, MonadState s m) =>
Optic k is s s a b -> b -> m ()
assign (Optic
  A_Lens NoIx (VM t s) (VM t s) (FrameState t s) (FrameState t s)
#state Optic
  A_Lens NoIx (VM t s) (VM t s) (FrameState t s) (FrameState t s)
-> Optic
     A_Lens
     NoIx
     (FrameState t s)
     (FrameState t s)
     (Expr 'Buf)
     (Expr 'Buf)
-> Optic A_Lens NoIx (VM t s) (VM t s) (Expr 'Buf) (Expr 'Buf)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  (FrameState t s)
  (FrameState t s)
  (Expr 'Buf)
  (Expr 'Buf)
#calldata) Expr 'Buf
cd
  #constraints %= (<> cdProps)
  Optic A_Lens NoIx (VM t s) (VM t s) (Expr 'EAddr) (Expr 'EAddr)
-> Expr 'EAddr -> EVM t s ()
forall k s (m :: * -> *) (is :: IxList) a b.
(Is k A_Setter, MonadState s m) =>
Optic k is s s a b -> b -> m ()
assign (Optic
  A_Lens NoIx (VM t s) (VM t s) (FrameState t s) (FrameState t s)
#state Optic
  A_Lens NoIx (VM t s) (VM t s) (FrameState t s) (FrameState t s)
-> Optic
     A_Lens
     NoIx
     (FrameState t s)
     (FrameState t s)
     (Expr 'EAddr)
     (Expr 'EAddr)
-> Optic A_Lens NoIx (VM t s) (VM t s) (Expr 'EAddr) (Expr 'EAddr)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  (FrameState t s)
  (FrameState t s)
  (Expr 'EAddr)
  (Expr 'EAddr)
#caller) TestVMParams
params.caller
  Optic A_Lens NoIx (VM t s) (VM t s) (Gas t) (Gas t)
-> Gas t -> EVM t s ()
forall k s (m :: * -> *) (is :: IxList) a b.
(Is k A_Setter, MonadState s m) =>
Optic k is s s a b -> b -> m ()
assign (Optic
  A_Lens NoIx (VM t s) (VM t s) (FrameState t s) (FrameState t s)
#state Optic
  A_Lens NoIx (VM t s) (VM t s) (FrameState t s) (FrameState t s)
-> Optic
     A_Lens NoIx (FrameState t s) (FrameState t s) (Gas t) (Gas t)
-> Optic A_Lens NoIx (VM t s) (VM t s) (Gas t) (Gas t)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic A_Lens NoIx (FrameState t s) (FrameState t s) (Gas t) (Gas t)
#gas) (Word64 -> Gas t
forall (t :: VMType). VMOps t => Word64 -> Gas t
toGas TestVMParams
params.gasCall)
  Contract
origin <- Contract -> Maybe Contract -> Contract
forall a. a -> Maybe a -> a
fromMaybe (ContractCode -> Contract
initialContract (RuntimeCode -> ContractCode
RuntimeCode (ByteString -> RuntimeCode
ConcreteRuntimeCode ByteString
""))) (Maybe Contract -> Contract)
-> StateT (VM t s) (ST s) (Maybe Contract)
-> StateT (VM t s) (ST s) Contract
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Optic' A_Lens NoIx (VM t s) (Maybe Contract)
-> StateT (VM t s) (ST s) (Maybe Contract)
forall k s (m :: * -> *) (is :: IxList) a.
(Is k A_Getter, MonadState s m) =>
Optic' k is s a -> m a
use (Optic A_Lens NoIx (VM t s) (VM t s) Env Env
#env Optic A_Lens NoIx (VM t s) (VM t s) Env Env
-> Optic
     A_Lens
     NoIx
     Env
     Env
     (Map (Expr 'EAddr) Contract)
     (Map (Expr 'EAddr) Contract)
-> Optic
     A_Lens
     NoIx
     (VM t s)
     (VM t s)
     (Map (Expr 'EAddr) Contract)
     (Map (Expr 'EAddr) Contract)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  Env
  Env
  (Map (Expr 'EAddr) Contract)
  (Map (Expr 'EAddr) Contract)
#contracts Optic
  A_Lens
  NoIx
  (VM t s)
  (VM t s)
  (Map (Expr 'EAddr) Contract)
  (Map (Expr 'EAddr) Contract)
-> Optic
     A_Lens
     NoIx
     (Map (Expr 'EAddr) Contract)
     (Map (Expr 'EAddr) Contract)
     (Maybe Contract)
     (Maybe Contract)
-> Optic' A_Lens NoIx (VM t s) (Maybe Contract)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Map (Expr 'EAddr) Contract)
-> Lens'
     (Map (Expr 'EAddr) Contract)
     (Maybe (IxValue (Map (Expr 'EAddr) Contract)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at TestVMParams
params.origin)
  let insufficientBal :: Bool
insufficientBal = Bool -> (W256 -> Bool) -> Maybe W256 -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (\W256
b -> W256
b W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< TestVMParams
params.gasprice W256 -> W256 -> W256
forall a. Num a => a -> a -> a
* (Word64 -> W256
forall target source. From source target => source -> target
into TestVMParams
params.gasCall)) (Expr 'EWord -> Maybe W256
maybeLitWord Contract
origin.balance)
  Bool -> EVM t s () -> EVM t s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
insufficientBal (EVM t s () -> EVM t s ()) -> EVM t s () -> EVM t s ()
forall a b. (a -> b) -> a -> b
$ FilePath -> EVM t s ()
forall a. HasCallStack => FilePath -> a
internalError FilePath
"insufficient balance for gas cost"
  VM t s
vm <- StateT (VM t s) (ST s) (VM t s)
forall s (m :: * -> *). MonadState s m => m s
get
  VM t s -> EVM t s ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (VM t s -> EVM t s ()) -> VM t s -> EVM t s ()
forall a b. (a -> b) -> a -> b
$ VM t s -> VM t s
forall (t :: VMType) s. VM t s -> VM t s
initTx VM t s
vm

initialUnitTestVm :: VMOps t => UnitTestOptions s -> SolcContract -> ST s (VM t s)
initialUnitTestVm :: forall (t :: VMType) s.
VMOps t =>
UnitTestOptions s -> SolcContract -> ST s (VM t s)
initialUnitTestVm (UnitTestOptions {Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
DappInfo
SolverGroup
TestVMParams
$sel:rpcInfo:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> RpcInfo
$sel:solvers:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> SolverGroup
$sel:verbose:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Int
$sel:maxIter:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Integer
$sel:askSmtIters:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Integer
$sel:smtTimeout:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Natural
$sel:solver:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Maybe Text
$sel:match:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Text
$sel:dapp:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> DappInfo
$sel:testParams:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> TestVMParams
$sel:ffiAllowed:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$sel:checkFailBit:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
checkFailBit :: Bool
..}) SolcContract
theContract = do
  VM t s
vm <- VMOpts t -> ST s (VM t s)
forall (t :: VMType) s. VMOps t => VMOpts t -> ST s (VM t s)
makeVm (VMOpts t -> ST s (VM t s)) -> VMOpts t -> ST s (VM t s)
forall a b. (a -> b) -> a -> b
$ VMOpts
           { $sel:contract:VMOpts :: Contract
contract = ContractCode -> Contract
initialContract (ByteString -> Expr 'Buf -> ContractCode
InitCode SolcContract
theContract.creationCode Expr 'Buf
forall a. Monoid a => a
mempty)
           , $sel:otherContracts:VMOpts :: [(Expr 'EAddr, Contract)]
otherContracts = []
           , $sel:calldata:VMOpts :: (Expr 'Buf, [Prop])
calldata = (Expr 'Buf, [Prop])
forall a. Monoid a => a
mempty
           , $sel:value:VMOpts :: Expr 'EWord
value = W256 -> Expr 'EWord
Lit W256
0
           , $sel:address:VMOpts :: Expr 'EAddr
address = TestVMParams
testParams.address
           , $sel:caller:VMOpts :: Expr 'EAddr
caller = TestVMParams
testParams.caller
           , $sel:origin:VMOpts :: Expr 'EAddr
origin = TestVMParams
testParams.origin
           , $sel:gas:VMOpts :: Gas t
gas = Word64 -> Gas t
forall (t :: VMType). VMOps t => Word64 -> Gas t
toGas TestVMParams
testParams.gasCreate
           , $sel:gaslimit:VMOpts :: Word64
gaslimit = TestVMParams
testParams.gasCreate
           , $sel:coinbase:VMOpts :: Expr 'EAddr
coinbase = TestVMParams
testParams.coinbase
           , $sel:number:VMOpts :: W256
number = TestVMParams
testParams.number
           , $sel:timestamp:VMOpts :: Expr 'EWord
timestamp = W256 -> Expr 'EWord
Lit TestVMParams
testParams.timestamp
           , $sel:blockGaslimit:VMOpts :: Word64
blockGaslimit = TestVMParams
testParams.gaslimit
           , $sel:gasprice:VMOpts :: W256
gasprice = TestVMParams
testParams.gasprice
           , $sel:baseFee:VMOpts :: W256
baseFee = TestVMParams
testParams.baseFee
           , $sel:priorityFee:VMOpts :: W256
priorityFee = TestVMParams
testParams.priorityFee
           , $sel:maxCodeSize:VMOpts :: W256
maxCodeSize = TestVMParams
testParams.maxCodeSize
           , $sel:prevRandao:VMOpts :: W256
prevRandao = TestVMParams
testParams.prevrandao
           , $sel:schedule:VMOpts :: FeeSchedule Word64
schedule = FeeSchedule Word64
forall n. Num n => FeeSchedule n
feeSchedule
           , $sel:chainId:VMOpts :: W256
chainId = TestVMParams
testParams.chainId
           , $sel:create:VMOpts :: Bool
create = Bool
True
           , $sel:baseState:VMOpts :: BaseState
baseState = BaseState
EmptyBase
           , $sel:txAccessList:VMOpts :: Map (Expr 'EAddr) [W256]
txAccessList = Map (Expr 'EAddr) [W256]
forall a. Monoid a => a
mempty -- TODO: support unit test access lists???
           , $sel:allowFFI:VMOpts :: Bool
allowFFI = Bool
ffiAllowed
           , $sel:freshAddresses:VMOpts :: Int
freshAddresses = Int
0
           , $sel:beaconRoot:VMOpts :: W256
beaconRoot = W256
0
           }
  let creator :: IxValue (Map (Expr 'EAddr) Contract)
creator =
        ContractCode -> Contract
initialContract (RuntimeCode -> ContractCode
RuntimeCode (ByteString -> RuntimeCode
ConcreteRuntimeCode ByteString
""))
          Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& Optic A_Lens NoIx Contract Contract (Maybe W64) (Maybe W64)
-> Maybe W64 -> Contract -> Contract
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic A_Lens NoIx Contract Contract (Maybe W64) (Maybe W64)
#nonce (W64 -> Maybe W64
forall a. a -> Maybe a
Just W64
1)
          Contract
-> (Contract -> IxValue (Map (Expr 'EAddr) Contract))
-> IxValue (Map (Expr 'EAddr) Contract)
forall a b. a -> (a -> b) -> b
& Optic
  A_Lens
  NoIx
  Contract
  (IxValue (Map (Expr 'EAddr) Contract))
  (Expr 'EWord)
  (Expr 'EWord)
-> Expr 'EWord -> Contract -> IxValue (Map (Expr 'EAddr) Contract)
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic
  A_Lens
  NoIx
  Contract
  (IxValue (Map (Expr 'EAddr) Contract))
  (Expr 'EWord)
  (Expr 'EWord)
#balance (W256 -> Expr 'EWord
Lit TestVMParams
testParams.balanceCreate)
  VM t s -> ST s (VM t s)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VM t s -> ST s (VM t s)) -> VM t s -> ST s (VM t s)
forall a b. (a -> b) -> a -> b
$ VM t s
vm VM t s -> (VM t s -> VM t s) -> VM t s
forall a b. a -> (a -> b) -> b
& Optic
  A_Lens
  NoIx
  (VM t s)
  (VM t s)
  (Maybe (IxValue (Map (Expr 'EAddr) Contract)))
  (Maybe (IxValue (Map (Expr 'EAddr) Contract)))
-> Maybe (IxValue (Map (Expr 'EAddr) Contract)) -> VM t s -> VM t s
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set (Optic A_Lens NoIx (VM t s) (VM t s) Env Env
#env Optic A_Lens NoIx (VM t s) (VM t s) Env Env
-> Optic
     A_Lens
     NoIx
     Env
     Env
     (Map (Expr 'EAddr) Contract)
     (Map (Expr 'EAddr) Contract)
-> Optic
     A_Lens
     NoIx
     (VM t s)
     (VM t s)
     (Map (Expr 'EAddr) Contract)
     (Map (Expr 'EAddr) Contract)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  Env
  Env
  (Map (Expr 'EAddr) Contract)
  (Map (Expr 'EAddr) Contract)
#contracts Optic
  A_Lens
  NoIx
  (VM t s)
  (VM t s)
  (Map (Expr 'EAddr) Contract)
  (Map (Expr 'EAddr) Contract)
-> Lens'
     (Map (Expr 'EAddr) Contract)
     (Maybe (IxValue (Map (Expr 'EAddr) Contract)))
-> Optic
     A_Lens
     NoIx
     (VM t s)
     (VM t s)
     (Maybe (IxValue (Map (Expr 'EAddr) Contract)))
     (Maybe (IxValue (Map (Expr 'EAddr) Contract)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Map (Expr 'EAddr) Contract)
-> Lens'
     (Map (Expr 'EAddr) Contract)
     (Maybe (IxValue (Map (Expr 'EAddr) Contract)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at (Addr -> Expr 'EAddr
LitAddr Addr
ethrunAddress)) (IxValue (Map (Expr 'EAddr) Contract)
-> Maybe (IxValue (Map (Expr 'EAddr) Contract))
forall a. a -> Maybe a
Just IxValue (Map (Expr 'EAddr) Contract)
creator)

paramsFromRpc :: Fetch.RpcInfo -> IO TestVMParams
paramsFromRpc :: RpcInfo -> IO TestVMParams
paramsFromRpc RpcInfo
rpcinfo = do
  (Expr 'EAddr
miner,Expr 'EWord
ts,W256
blockNum,W256
ran,Word64
limit,W256
base) <- case RpcInfo
rpcinfo of
    RpcInfo
Nothing -> (Expr 'EAddr, Expr 'EWord, W256, W256, Word64, W256)
-> IO (Expr 'EAddr, Expr 'EWord, W256, W256, Word64, W256)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Expr 'EAddr
SymAddr Text
"miner", W256 -> Expr 'EWord
Lit W256
0, W256
0, W256
0, Word64
0, W256
0)
    Just (BlockNumber
block, Text
url) -> BlockNumber -> Text -> IO (Maybe Block)
Fetch.fetchBlockFrom BlockNumber
block Text
url IO (Maybe Block)
-> (Maybe Block
    -> IO (Expr 'EAddr, Expr 'EWord, W256, W256, Word64, W256))
-> IO (Expr 'EAddr, Expr 'EWord, W256, W256, Word64, W256)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe Block
Nothing -> FilePath -> IO (Expr 'EAddr, Expr 'EWord, W256, W256, Word64, W256)
forall a. HasCallStack => FilePath -> a
internalError FilePath
"Could not fetch block"
      Just Block{Word64
FeeSchedule Word64
W256
Expr 'EWord
Expr 'EAddr
coinbase :: Expr 'EAddr
timestamp :: Expr 'EWord
number :: W256
prevRandao :: W256
gaslimit :: Word64
baseFee :: W256
maxCodeSize :: W256
schedule :: FeeSchedule Word64
$sel:coinbase:Block :: Block -> Expr 'EAddr
$sel:timestamp:Block :: Block -> Expr 'EWord
$sel:number:Block :: Block -> W256
$sel:prevRandao:Block :: Block -> W256
$sel:gaslimit:Block :: Block -> Word64
$sel:baseFee:Block :: Block -> W256
$sel:maxCodeSize:Block :: Block -> W256
$sel:schedule:Block :: Block -> FeeSchedule Word64
..} -> (Expr 'EAddr, Expr 'EWord, W256, W256, Word64, W256)
-> IO (Expr 'EAddr, Expr 'EWord, W256, W256, Word64, W256)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Expr 'EAddr
coinbase
                             , Expr 'EWord
timestamp
                             , W256
number
                             , W256
prevRandao
                             , Word64
gaslimit
                             , W256
baseFee
                             )
  let ts' :: W256
ts' = W256 -> Maybe W256 -> W256
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> W256
forall a. HasCallStack => FilePath -> a
internalError FilePath
"received unexpected symbolic timestamp via rpc") (Expr 'EWord -> Maybe W256
maybeLitWord Expr 'EWord
ts)
  TestVMParams -> IO TestVMParams
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TestVMParams -> IO TestVMParams)
-> TestVMParams -> IO TestVMParams
forall a b. (a -> b) -> a -> b
$ TestVMParams
    -- TODO: make this symbolic! It needs some tweaking to the way that our
    -- symbolic interpreters work to allow us to symbolically exec constructor initialization
    { $sel:address:TestVMParams :: Expr 'EAddr
address = Addr -> Expr 'EAddr
LitAddr Addr
0xacab
    , $sel:caller:TestVMParams :: Expr 'EAddr
caller = Text -> Expr 'EAddr
SymAddr Text
"caller"
    , $sel:origin:TestVMParams :: Expr 'EAddr
origin = Text -> Expr 'EAddr
SymAddr Text
"origin"
    , $sel:gasCreate:TestVMParams :: Word64
gasCreate = Word64
defaultGasForCreating
    , $sel:gasCall:TestVMParams :: Word64
gasCall = Word64
defaultGasForInvoking
    , $sel:baseFee:TestVMParams :: W256
baseFee = W256
base
    , $sel:priorityFee:TestVMParams :: W256
priorityFee = W256
0
    , $sel:balanceCreate:TestVMParams :: W256
balanceCreate = W256
defaultBalanceForTestContract
    , $sel:coinbase:TestVMParams :: Expr 'EAddr
coinbase = Expr 'EAddr
miner
    , $sel:number:TestVMParams :: W256
number = W256
blockNum
    , $sel:timestamp:TestVMParams :: W256
timestamp = W256
ts'
    , $sel:gaslimit:TestVMParams :: Word64
gaslimit = Word64
limit
    , $sel:gasprice:TestVMParams :: W256
gasprice = W256
0
    , $sel:maxCodeSize:TestVMParams :: W256
maxCodeSize = W256
defaultMaxCodeSize
    , $sel:prevrandao:TestVMParams :: W256
prevrandao = W256
ran
    , $sel:chainId:TestVMParams :: W256
chainId = W256
99
    }

tick :: Text -> IO ()
tick :: Text -> IO ()
tick Text
x = Text -> IO ()
Text.putStr Text
x IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
stdout