{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImplicitParams #-}

module EVM.UnitTest where

import EVM
import EVM.ABI
import EVM.SMT
import EVM.Solvers
import EVM.Dapp
import EVM.Exec
import EVM.Expr (readStorage')
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, runExpr, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr)
import EVM.Types
import EVM.Transaction (initTx)
import EVM.Stepper (Stepper)
import EVM.Stepper qualified as Stepper

import Control.Monad.ST (RealWorld, ST, stToIO)
import Optics.Core hiding (elements)
import Optics.State
import Optics.State.Operators
import Control.Monad.State.Strict hiding (state)
import Data.ByteString.Lazy qualified as BSLazy
import Data.Binary.Get (runGet)
import Data.ByteString (ByteString)
import Data.Decimal (DecimalRaw(..))
import Data.Either (isRight, rights, lefts)
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 -> Bool
smtDebug    :: Bool
  , 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
  }

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


-- | Generate VeriOpts from UnitTestOptions
makeVeriOpts :: UnitTestOptions s -> VeriOpts
makeVeriOpts :: forall {k} (s :: k). UnitTestOptions s -> VeriOpts
makeVeriOpts UnitTestOptions s
opts =
   VeriOpts
defaultVeriOpts { $sel:debug:VeriOpts :: Bool
debug = UnitTestOptions s
opts.smtDebug
                   , $sel:maxIter:VeriOpts :: Maybe Integer
maxIter = UnitTestOptions s
opts.maxIter
                   , $sel:askSmtIters:VeriOpts :: Integer
askSmtIters = UnitTestOptions s
opts.askSmtIters
                   , $sel:rpcInfo:VeriOpts :: RpcInfo
rpcInfo = UnitTestOptions s
opts.rpcInfo
                   }

-- | Top level CLI endpoint for hevm test
unitTest :: UnitTestOptions RealWorld -> Contracts -> IO Bool
unitTest :: UnitTestOptions RealWorld -> Contracts -> IO Bool
unitTest UnitTestOptions RealWorld
opts (Contracts Map Text SolcContract
cs) = do
  let unitTests :: [(Text, [Sig])]
unitTests = 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
  [Bool]
results <- ((Text, [Sig]) -> IO [Bool]) -> [(Text, [Sig])] -> IO [Bool]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (UnitTestOptions RealWorld
-> Map Text SolcContract -> (Text, [Sig]) -> IO [Bool]
runUnitTestContract UnitTestOptions RealWorld
opts Map Text SolcContract
cs) [(Text, [Sig])]
unitTests
  Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> IO Bool) -> Bool -> IO 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 s ()
initializeUnitTest :: forall s. UnitTestOptions s -> SolcContract -> Stepper s ()
initializeUnitTest UnitTestOptions s
opts SolcContract
theContract = do

  let addr :: Index (Map (Expr 'EAddr) Contract)
addr = UnitTestOptions s
opts.testParams.address

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

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

  EVM s () -> Stepper s ()
forall s a. EVM s a -> Stepper s a
Stepper.evm (EVM s () -> Stepper s ()) -> EVM s () -> Stepper 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 s) Identity (Either EvmError (Expr 'Buf))
forall s. Stepper s (Either EvmError (Expr 'Buf))
Stepper.execFully
  EVM s () -> Stepper s ()
forall s a. EVM s a -> Stepper s a
Stepper.evm (EVM s () -> Stepper s ()) -> EVM s () -> Stepper s ()
forall a b. (a -> b) -> a -> b
$ case Either EvmError (Expr 'Buf)
res of
    Left EvmError
e -> TraceData -> EVM s ()
forall s. TraceData -> EVM s ()
pushTrace (EvmError -> TraceData
ErrorTrace EvmError
e)
    Either EvmError (Expr 'Buf)
_ -> EVM s ()
forall s. EVM s ()
popTrace

runUnitTestContract
  :: UnitTestOptions RealWorld
  -> Map Text SolcContract
  -> (Text, [Sig])
  -> IO [Bool]
runUnitTestContract :: UnitTestOptions RealWorld
-> Map Text SolcContract -> (Text, [Sig]) -> IO [Bool]
runUnitTestContract
  opts :: UnitTestOptions RealWorld
opts@(UnitTestOptions {Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
SolverGroup
DappInfo
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:smtDebug:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$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
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtDebug :: Bool
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
..}) Map Text SolcContract
contractMap (Text
name, [Sig]
testSigs) = do

  -- Print a header
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Running " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([Sig] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sig]
testSigs) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" tests for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
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
      [Char] -> IO [Bool]
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> IO [Bool]) -> [Char] -> IO [Bool]
forall a b. (a -> b) -> a -> b
$ [Char]
"Contract " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
unpack Text
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" not found"

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

      case VM RealWorld
vm1.result of
        Just (VMFailure EvmError
_) -> IO [Bool] -> IO [Bool]
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Bool] -> IO [Bool]) -> IO [Bool] -> IO [Bool]
forall a b. (a -> b) -> a -> b
$ do
          Text -> IO ()
Text.putStrLn Text
"\x1b[31m[BAIL]\x1b[0m setUp() "
          Text -> IO ()
tick Text
"\n"
          Text -> IO ()
tick (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ VM RealWorld -> UnitTestOptions RealWorld -> Text -> Text
forall s. VM s -> UnitTestOptions s -> Text -> Text
failOutput VM 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
          let

          -- Run all the test cases and print their status
          [Either Text Text]
details <- [Sig] -> (Sig -> IO (Either Text Text)) -> IO [Either Text Text]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Sig]
testSigs ((Sig -> IO (Either Text Text)) -> IO [Either Text Text])
-> (Sig -> IO (Either Text Text)) -> IO [Either Text Text]
forall a b. (a -> b) -> a -> b
$ \Sig
s -> do
            (Text
result, Either Text Text
detail) <- UnitTestOptions RealWorld
-> VM RealWorld -> Sig -> IO (Text, Either Text Text)
symRun UnitTestOptions RealWorld
opts VM RealWorld
vm1 Sig
s
            Text -> IO ()
Text.putStrLn Text
result
            Either Text Text -> IO (Either Text Text)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either Text Text
detail

          let running :: [Text]
running = [Either Text Text] -> [Text]
forall a b. [Either a b] -> [b]
rights [Either Text Text]
details
              bailing :: [Text]
bailing = [Either Text Text] -> [Text]
forall a b. [Either a b] -> [a]
lefts [Either Text Text]
details

          Text -> IO ()
tick Text
"\n"
          Text -> IO ()
tick ([Text] -> Text
Text.unlines ((Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Text -> Bool) -> Text -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
Text.null) [Text]
running))
          Text -> IO ()
tick ([Text] -> Text
Text.unlines [Text]
bailing)

          [Bool] -> IO [Bool]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Bool] -> IO [Bool]) -> [Bool] -> IO [Bool]
forall a b. (a -> b) -> a -> b
$ (Either Text Text -> Bool) -> [Either Text Text] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either Text Text -> Bool
forall a b. Either a b -> Bool
isRight [Either Text Text]
details
        Maybe (VMResult RealWorld)
_ -> [Char] -> IO [Bool]
forall a. HasCallStack => [Char] -> a
internalError [Char]
"setUp() did not end with a result"


-- | Define the thread spawner for symbolic tests
symRun :: UnitTestOptions RealWorld -> VM RealWorld -> Sig -> IO (Text, Either Text Text)
symRun :: UnitTestOptions RealWorld
-> VM RealWorld -> Sig -> IO (Text, Either Text Text)
symRun opts :: UnitTestOptions RealWorld
opts@UnitTestOptions{Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
SolverGroup
DappInfo
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:smtDebug:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$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
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtDebug :: Bool
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
..} VM RealWorld
vm (Sig Text
testName [AbiType]
types) = do
    let cd :: (Expr 'Buf, [Prop])
cd = Text -> [AbiType] -> [[Char]] -> Expr 'Buf -> (Expr 'Buf, [Prop])
symCalldata Text
testName [AbiType]
types [] (Text -> Expr 'Buf
AbstractBuf Text
"txdata")
        shouldFail :: Bool
shouldFail = Text
"proveFail" Text -> Text -> Bool
`isPrefixOf` Text
testName
        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 ([Char] -> Expr 'EContract
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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 RealWorld
vm.state.contract Map (Expr 'EAddr) (Expr 'EContract)
store)

    -- define postcondition depending on `shouldFail`
    -- We directly encode the failure conditions from failed() in ds-test since this is easier to encode than a call into failed()
    -- we need to read from slot 0 in the test contract and mask it with 0x10 to get the value of _failed
    -- we don't need to do this when reading the failed from the cheatcode address since we don't do any packing there
    let 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 'EWord -> Expr 'EWord
And (Expr 'EWord -> Expr 'Storage -> Expr 'EWord
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
0x10) Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
.== W256 -> Expr 'EWord
Lit W256
0x10)
                               Prop -> Prop -> Prop
.|| (Expr 'EWord -> Expr 'Storage -> Expr 'EWord
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
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 RealWorld -> Expr 'End -> Prop
postcondition = ((VM RealWorld, Expr 'End) -> Prop)
-> VM RealWorld -> Expr 'End -> Prop
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((VM RealWorld, Expr 'End) -> Prop)
 -> VM RealWorld -> Expr 'End -> Prop)
-> ((VM RealWorld, Expr 'End) -> Prop)
-> VM RealWorld
-> Expr 'End
-> Prop
forall a b. (a -> b) -> a -> b
$ case Bool
shouldFail of
          Bool
True -> \(VM RealWorld
_, Expr 'End
post) -> case Expr 'End
post of
                                  Success [Prop]
_ Traces
_ Expr 'Buf
_ Map (Expr 'EAddr) (Expr 'EContract)
store -> Map (Expr 'EAddr) (Expr 'EContract) -> Prop
failed Map (Expr 'EAddr) (Expr 'EContract)
store
                                  Expr 'End
_ -> Bool -> Prop
PBool Bool
True
          Bool
False -> \(VM RealWorld
_, Expr 'End
post) -> case Expr 'End
post of
                                   Success [Prop]
_ Traces
_ Expr 'Buf
_ Map (Expr 'EAddr) (Expr 'EContract)
store -> Prop -> Prop
PNeg (Map (Expr 'EAddr) (Expr 'EContract) -> Prop
failed Map (Expr 'EAddr) (Expr 'EContract)
store)
                                   Failure [Prop]
_ Traces
_ (Revert Expr 'Buf
msg) -> case Expr 'Buf
msg of
                                     ConcreteBuf ByteString
b -> Bool -> Prop
PBool (Bool -> Prop) -> Bool -> Prop
forall a b. (a -> b) -> a -> b
$ ByteString
b ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= Word256 -> ByteString
panicMsg Word256
0x01
                                     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]
_ Traces
_ EvmError
_ -> Bool -> Prop
PBool Bool
True
                                   Partial [Prop]
_ Traces
_ PartialExec
_ -> Bool -> Prop
PBool Bool
True
                                   Expr 'End
_ -> [Char] -> Prop
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Invalid leaf node"

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

    -- check postconditions against vm
    (Expr 'End
e, [VerifyResult]
results) <- SolverGroup
-> VeriOpts
-> VM RealWorld
-> Maybe (VM RealWorld -> Expr 'End -> Prop)
-> IO (Expr 'End, [VerifyResult])
verify SolverGroup
solvers (UnitTestOptions RealWorld -> VeriOpts
forall {k} (s :: k). UnitTestOptions s -> VeriOpts
makeVeriOpts UnitTestOptions RealWorld
opts) VM RealWorld
vm' ((VM RealWorld -> Expr 'End -> Prop)
-> Maybe (VM RealWorld -> Expr 'End -> Prop)
forall a. a -> Maybe a
Just VM 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

    -- display results
    if (VerifyResult -> Bool) -> [VerifyResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all VerifyResult -> Bool
forall a b c. ProofResult a b c -> Bool
isQed [VerifyResult]
results
    then if Bool
allReverts Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
shouldFail)
         then (Text, Either Text Text) -> IO (Text, Either Text Text)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text
"\x1b[31m[FAIL]\x1b[0m " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
testName, Text -> Either Text Text
forall a b. a -> Either a b
Left (Text -> Either Text Text) -> Text -> Either Text Text
forall a b. (a -> b) -> a -> b
$ Text -> Text
allBranchRev Text
testName)
         else (Text, Either Text Text) -> IO (Text, Either Text Text)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text
"\x1b[32m[PASS]\x1b[0m " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
testName, Text -> Either Text Text
forall a b. b -> Either a b
Right Text
"")
    else do
      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
      (Text, Either Text Text) -> IO (Text, Either Text Text)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text
"\x1b[31m[FAIL]\x1b[0m " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
testName, Text -> Either Text Text
forall a b. a -> Either a b
Left Text
y)

allBranchRev :: Text -> Text
allBranchRev :: Text -> Text
allBranchRev Text
testName = [Text] -> Text
Text.unlines
  [ Text
"Failure: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
testName
  , Text
""
  , Int -> Text -> Text
indentLines Int
2 (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
Text.unlines
      [ 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
SolverGroup
DappInfo
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:smtDebug:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$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
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtDebug :: Bool
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
..} Text
testName Expr 'Buf
cd [AbiType]
types [(Expr 'End, SMTCex)]
failures' =
  [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
    [ Text
"Failure: "
    , Text
testName
    , Text
"\n\n"
    , Text -> [Text] -> Text
intercalate Text
"\n" ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
indentLines Int
2 (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]
_ Traces
_ Expr 'Buf
_ Map (Expr 'EAddr) (Expr 'EContract)
_ -> if Text
"proveFail" Text -> Text -> Bool
`isPrefixOf` Text
testName
                           then Text
"Successful execution"
                           else Text
"Failed: DSTest Assertion Violation"
        Expr 'End
res ->
          let ?context = DappContext { $sel:info:DappContext :: DappInfo
info = DappInfo
dapp, $sel:env:DappContext :: Map (Expr 'EAddr) Contract
env = Expr 'End -> Map (Expr 'EAddr) Contract
traceContext Expr 'End
res}
          in [Char] -> Text
Text.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'End -> [Char]
prettyvmresult Expr 'End
res
      mkMsg :: (Expr 'End, SMTCex) -> Text
mkMsg (Expr 'End
leaf, SMTCex
cex) = [Text] -> Text
Text.unlines
        [Text
"Counterexample:"
        ,Text
""
        ,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 =  DappInfo -> Map (Expr 'EAddr) Contract -> DappContext
DappContext DappInfo
dapp (Expr 'End -> Map (Expr 'EAddr) Contract
traceContext Expr 'End
leaf)
                           in SMTCex -> Expr 'Buf -> Text -> [AbiType] -> Text
prettyCalldata SMTCex
cex Expr 'Buf
cd Text
testName [AbiType]
types
        , case Maybe Int
verbose of
            Just Int
_ -> [Text] -> Text
Text.unlines
              [ Text
""
              , Int -> Text -> Text
indentLines Int
2 (DappInfo -> Expr 'End -> Text
showTraceTree' DappInfo
dapp Expr 'End
leaf)
              ]
            Maybe Int
_ -> Text
""
        ]

execSymTest :: UnitTestOptions RealWorld -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper RealWorld (Expr End)
execSymTest :: UnitTestOptions RealWorld
-> Text -> (Expr 'Buf, [Prop]) -> Stepper RealWorld (Expr 'End)
execSymTest UnitTestOptions{ Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
SolverGroup
DappInfo
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:smtDebug:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$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
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtDebug :: Bool
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
.. } Text
method (Expr 'Buf, [Prop])
cd = do
  -- Set up the call to the test method
  EVM RealWorld () -> Stepper RealWorld ()
forall s a. EVM s a -> Stepper s a
Stepper.evm (EVM RealWorld () -> Stepper RealWorld ())
-> EVM RealWorld () -> Stepper RealWorld ()
forall a b. (a -> b) -> a -> b
$ do
    TestVMParams -> (Expr 'Buf, [Prop]) -> EVM RealWorld ()
forall s. TestVMParams -> (Expr 'Buf, [Prop]) -> EVM s ()
makeTxCall TestVMParams
testParams (Expr 'Buf, [Prop])
cd
    TraceData -> EVM RealWorld ()
forall s. TraceData -> EVM s ()
pushTrace (Text -> TraceData
EntryTrace Text
method)
  -- Try running the test method
  Stepper RealWorld (Expr 'End)
runExpr

checkSymFailures :: UnitTestOptions RealWorld -> Stepper RealWorld (VM RealWorld)
checkSymFailures :: UnitTestOptions RealWorld -> Stepper RealWorld (VM RealWorld)
checkSymFailures UnitTestOptions { Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
SolverGroup
DappInfo
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:smtDebug:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$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
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtDebug :: Bool
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
.. } = do
  -- Ask whether any assertions failed
  EVM RealWorld () -> Stepper RealWorld ()
forall s a. EVM s a -> Stepper s a
Stepper.evm (EVM RealWorld () -> Stepper RealWorld ())
-> EVM RealWorld () -> Stepper RealWorld ()
forall a b. (a -> b) -> a -> b
$ do
    EVM RealWorld ()
forall s. EVM s ()
popTrace
    TestVMParams
-> Either (Text, AbiValue) ByteString -> EVM RealWorld ()
forall s.
TestVMParams -> Either (Text, AbiValue) ByteString -> EVM s ()
abiCall TestVMParams
testParams ((Text, AbiValue) -> Either (Text, AbiValue) ByteString
forall a b. a -> Either a b
Left (Text
"failed()", AbiValue
emptyAbi))
  Stepper RealWorld (VM RealWorld)
forall s. Stepper s (VM s)
Stepper.runFully

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 s -> UnitTestOptions s -> Text -> Text
passOutput :: forall s. VM s -> UnitTestOptions s -> Text -> Text
passOutput VM s
vm UnitTestOptions { Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
SolverGroup
DappInfo
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:smtDebug:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$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
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtDebug :: Bool
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
.. } Text
testName =
  let ?context = DappContext { $sel:info:DappContext :: DappInfo
info = DappInfo
dapp, $sel:env:DappContext :: Map (Expr 'EAddr) Contract
env = VM s
vm.env.contracts }
  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 s -> Text
forall s. DappInfo -> VM s -> Text
showTraceTree DappInfo
dapp VM 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 s
vm.logs)
      , Text
"\n"
      ]
    else Text
""

failOutput :: VM s -> UnitTestOptions s -> Text -> Text
failOutput :: forall s. VM s -> UnitTestOptions s -> Text -> Text
failOutput VM s
vm UnitTestOptions { Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
SolverGroup
DappInfo
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:smtDebug:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$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
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtDebug :: Bool
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
.. } Text
testName =
  let ?context = DappContext { $sel:info:DappContext :: DappInfo
info = DappInfo
dapp, $sel:env:DappContext :: Map (Expr 'EAddr) Contract
env = VM s
vm.env.contracts }
  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 s -> Text
forall s. DappInfo -> VM s -> Text
showTraceTree DappInfo
dapp VM 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 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
_) = [Char] -> Maybe Text
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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)]
types) ->
      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
<$> ([(Text, AbiType, Indexed)] -> [AbiType]
unindexed [(Text, AbiType, Indexed)]
types))) 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
          ts :: [AbiType]
ts = [(Text, AbiType, Indexed)] -> [AbiType]
unindexed [(Text, AbiType, Indexed)]
types
          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]
ts) 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]
ts Expr 'Buf
args) of
                  [Text
k, Text
v] -> (Text
k, Text
v)
                  [Text]
_ -> [Char] -> (Text, Text)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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 =
            [Char] -> Text
pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ DecimalRaw i -> [Char]
forall a. Show a => a -> [Char]
show (DecimalRaw i -> [Char]) -> DecimalRaw i -> [Char]
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]
ts) [AbiType]
ts) (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 :: TestVMParams -> Either (Text, AbiValue) ByteString -> EVM s ()
abiCall :: forall s.
TestVMParams -> Either (Text, AbiValue) ByteString -> EVM 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 s ()
forall s. TestVMParams -> (Expr 'Buf, [Prop]) -> EVM s ()
makeTxCall TestVMParams
params (ByteString -> Expr 'Buf
ConcreteBuf ByteString
cd, [])

makeTxCall :: TestVMParams -> (Expr Buf, [Prop]) -> EVM s ()
makeTxCall :: forall s. TestVMParams -> (Expr 'Buf, [Prop]) -> EVM s ()
makeTxCall TestVMParams
params (Expr 'Buf
cd, [Prop]
cdProps) = do
  EVM s ()
forall s. EVM s ()
resetState
  Optic A_Lens NoIx (VM s) (VM s) Bool Bool -> Bool -> EVM 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 s) (VM s) TxState TxState
#tx Optic A_Lens NoIx (VM s) (VM s) TxState TxState
-> Optic A_Lens NoIx TxState TxState Bool Bool
-> Optic A_Lens NoIx (VM s) (VM 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 s) () -> VM s -> VM s
forall s a. State s a -> s -> s
execState (Expr 'EAddr -> State (VM s) ()
forall s. Expr 'EAddr -> State (VM s) ()
loadContract TestVMParams
params.address) (VM s -> VM s)
-> StateT (VM s) (ST s) (VM s) -> StateT (VM s) (ST s) (VM s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (VM s) (ST s) (VM s)
forall s (m :: * -> *). MonadState s m => m s
get StateT (VM s) (ST s) (VM s) -> (VM s -> EVM s ()) -> EVM s ()
forall a b.
StateT (VM s) (ST s) a
-> (a -> StateT (VM s) (ST s) b) -> StateT (VM s) (ST s) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VM s -> EVM s ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put
  Optic A_Lens NoIx (VM s) (VM s) (Expr 'Buf) (Expr 'Buf)
-> Expr 'Buf -> EVM 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 s) (VM s) (FrameState s) (FrameState s)
#state Optic A_Lens NoIx (VM s) (VM s) (FrameState s) (FrameState s)
-> Optic
     A_Lens NoIx (FrameState s) (FrameState s) (Expr 'Buf) (Expr 'Buf)
-> Optic A_Lens NoIx (VM s) (VM 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 s) (FrameState s) (Expr 'Buf) (Expr 'Buf)
#calldata) Expr 'Buf
cd
  #constraints %= (<> cdProps)
  Optic A_Lens NoIx (VM s) (VM s) (Expr 'EAddr) (Expr 'EAddr)
-> Expr 'EAddr -> EVM 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 s) (VM s) (FrameState s) (FrameState s)
#state Optic A_Lens NoIx (VM s) (VM s) (FrameState s) (FrameState s)
-> Optic
     A_Lens
     NoIx
     (FrameState s)
     (FrameState s)
     (Expr 'EAddr)
     (Expr 'EAddr)
-> Optic A_Lens NoIx (VM s) (VM 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 s)
  (FrameState s)
  (Expr 'EAddr)
  (Expr 'EAddr)
#caller) TestVMParams
params.caller
  Optic A_Lens NoIx (VM s) (VM s) Word64 Word64 -> Word64 -> EVM 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 s) (VM s) (FrameState s) (FrameState s)
#state Optic A_Lens NoIx (VM s) (VM s) (FrameState s) (FrameState s)
-> Optic A_Lens NoIx (FrameState s) (FrameState s) Word64 Word64
-> Optic A_Lens NoIx (VM s) (VM s) Word64 Word64
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 s) (FrameState s) Word64 Word64
#gas) 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 s) (ST s) (Maybe Contract)
-> StateT (VM s) (ST s) Contract
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Optic' A_Lens NoIx (VM s) (Maybe Contract)
-> StateT (VM 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 s) (VM s) Env Env
#env Optic A_Lens NoIx (VM s) (VM s) Env Env
-> Optic
     A_Lens
     NoIx
     Env
     Env
     (Map (Expr 'EAddr) Contract)
     (Map (Expr 'EAddr) Contract)
-> Optic
     A_Lens
     NoIx
     (VM s)
     (VM 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 s)
  (VM 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 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 s () -> EVM s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
insufficientBal (EVM s () -> EVM s ()) -> EVM s () -> EVM s ()
forall a b. (a -> b) -> a -> b
$ [Char] -> EVM s ()
forall a. HasCallStack => [Char] -> a
internalError [Char]
"insufficient balance for gas cost"
  VM s
vm <- StateT (VM s) (ST s) (VM s)
forall s (m :: * -> *). MonadState s m => m s
get
  VM s -> EVM s ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (VM s -> EVM s ()) -> VM s -> EVM s ()
forall a b. (a -> b) -> a -> b
$ VM s -> VM s
forall s. VM s -> VM s
initTx VM s
vm

initialUnitTestVm :: UnitTestOptions s -> SolcContract -> ST s (VM s)
initialUnitTestVm :: forall s. UnitTestOptions s -> SolcContract -> ST s (VM s)
initialUnitTestVm (UnitTestOptions {Bool
Integer
Maybe Int
Maybe Integer
Maybe Natural
RpcInfo
Maybe Text
Text
SolverGroup
DappInfo
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:smtDebug:UnitTestOptions :: forall {k} (s :: k). UnitTestOptions s -> Bool
$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
rpcInfo :: RpcInfo
solvers :: SolverGroup
verbose :: Maybe Int
maxIter :: Maybe Integer
askSmtIters :: Integer
smtDebug :: Bool
smtTimeout :: Maybe Natural
solver :: Maybe Text
match :: Text
dapp :: DappInfo
testParams :: TestVMParams
ffiAllowed :: Bool
..}) SolcContract
theContract = do
  VM s
vm <- VMOpts -> ST s (VM s)
forall s. VMOpts -> ST s (VM s)
makeVm (VMOpts -> ST s (VM s)) -> VMOpts -> ST s (VM 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 :: Word64
gas = 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
           }
  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 s -> ST s (VM s)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VM s -> ST s (VM s)) -> VM s -> ST s (VM s)
forall a b. (a -> b) -> a -> b
$ VM s
vm VM s -> (VM s -> VM s) -> VM s
forall a b. a -> (a -> b) -> b
& Optic
  A_Lens
  NoIx
  (VM s)
  (VM s)
  (Maybe (IxValue (Map (Expr 'EAddr) Contract)))
  (Maybe (IxValue (Map (Expr 'EAddr) Contract)))
-> Maybe (IxValue (Map (Expr 'EAddr) Contract)) -> VM s -> VM 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 s) (VM s) Env Env
#env Optic A_Lens NoIx (VM s) (VM s) Env Env
-> Optic
     A_Lens
     NoIx
     Env
     Env
     (Map (Expr 'EAddr) Contract)
     (Map (Expr 'EAddr) Contract)
-> Optic
     A_Lens
     NoIx
     (VM s)
     (VM 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 s)
  (VM 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 s)
     (VM 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 -> [Char] -> IO (Expr 'EAddr, Expr 'EWord, W256, W256, Word64, W256)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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 ([Char] -> W256
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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