{-# 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)
import EVM.Effects
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
}
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
makeVeriOpts :: UnitTestOptions s -> VeriOpts
makeVeriOpts :: forall {k} (s :: k). UnitTestOptions s -> VeriOpts
makeVeriOpts UnitTestOptions s
opts =
VeriOpts
defaultVeriOpts { $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
}
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 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]) -> 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])]
unitTests
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
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
TraceData -> EVM 'Concrete s ()
forall (t :: VMType) s. TraceData -> EVM t s ()
pushTrace (Text -> TraceData
EntryTrace Text
"constructor")
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
#env % #contracts % ix addr % #balance %= (`Expr.add` (Lit opts.testParams.balanceCreate))
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()")
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
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
..}) Map Text SolcContract
contractMap (Text
name, [Sig]
testSigs) = 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
$ [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
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 ->
[Char] -> m [Bool]
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> m [Bool]) -> [Char] -> m [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
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
"\n"
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
[Either Text Text]
details <- [Sig] -> (Sig -> m (Either Text Text)) -> m [Either Text Text]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Sig]
testSigs ((Sig -> m (Either Text Text)) -> m [Either Text Text])
-> (Sig -> m (Either Text Text)) -> m [Either Text Text]
forall a b. (a -> b) -> a -> b
$ \Sig
s -> do
(Text
result, Either Text Text
detail) <- UnitTestOptions RealWorld
-> VM 'Concrete RealWorld -> Sig -> m (Text, Either Text Text)
forall (m :: * -> *).
App m =>
UnitTestOptions RealWorld
-> VM 'Concrete RealWorld -> Sig -> m (Text, Either Text Text)
symRun UnitTestOptions RealWorld
opts VM 'Concrete RealWorld
vm1 Sig
s
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
$ Text -> IO ()
Text.putStrLn Text
result
Either Text Text -> m (Either Text Text)
forall a. a -> m 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
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
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] -> 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
$ (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 'Concrete RealWorld)
_ -> [Char] -> m [Bool]
forall a. HasCallStack => [Char] -> a
internalError [Char]
"setUp() did not end with a result"
symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m (Text, Either Text Text)
symRun :: forall (m :: * -> *).
App m =>
UnitTestOptions RealWorld
-> VM 'Concrete RealWorld -> Sig -> m (Text, Either Text Text)
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
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
..} VM 'Concrete 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 'Concrete RealWorld
vm.state.contract Map (Expr 'EAddr) (Expr 'EContract)
store)
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 '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 '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]
_ 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 'Symbolic 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 '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'
(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
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) -> m (Text, Either Text Text)
forall a. a -> m 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) -> m (Text, Either Text Text)
forall a. a -> m 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) -> m (Text, Either Text Text)
forall a. a -> m 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
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
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
..} 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 Symbolic RealWorld (Expr End)
execSymTest :: UnitTestOptions RealWorld
-> Text
-> (Expr 'Buf, [Prop])
-> Stepper 'Symbolic RealWorld (Expr 'End)
execSymTest 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
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
.. } Text
method (Expr 'Buf, [Prop])
cd = do
EVM 'Symbolic RealWorld () -> Stepper 'Symbolic RealWorld ()
forall (t :: VMType) s a. EVM t s a -> Stepper t s a
Stepper.evm (EVM 'Symbolic RealWorld () -> Stepper 'Symbolic RealWorld ())
-> EVM 'Symbolic RealWorld () -> Stepper 'Symbolic RealWorld ()
forall a b. (a -> b) -> a -> b
$ do
TestVMParams -> (Expr 'Buf, [Prop]) -> EVM 'Symbolic RealWorld ()
forall (t :: VMType) s.
VMOps t =>
TestVMParams -> (Expr 'Buf, [Prop]) -> EVM t s ()
makeTxCall TestVMParams
testParams (Expr 'Buf, [Prop])
cd
TraceData -> EVM 'Symbolic RealWorld ()
forall (t :: VMType) s. TraceData -> EVM t s ()
pushTrace (Text -> TraceData
EntryTrace Text
method)
Stepper 'Symbolic RealWorld (Expr 'End)
runExpr
checkSymFailures :: VMOps t => UnitTestOptions RealWorld -> Stepper t RealWorld (VM t RealWorld)
checkSymFailures :: forall (t :: VMType).
VMOps t =>
UnitTestOptions RealWorld -> Stepper t RealWorld (VM t RealWorld)
checkSymFailures 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
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
.. } = do
EVM t RealWorld () -> Stepper t RealWorld ()
forall (t :: VMType) s a. EVM t s a -> Stepper t s a
Stepper.evm (EVM t RealWorld () -> Stepper t RealWorld ())
-> EVM t RealWorld () -> Stepper t RealWorld ()
forall a b. (a -> b) -> a -> b
$ do
EVM t RealWorld ()
forall (t :: VMType) s. EVM t s ()
popTrace
TestVMParams
-> Either (Text, AbiValue) ByteString -> EVM t RealWorld ()
forall (t :: VMType) s.
VMOps t =>
TestVMParams -> Either (Text, AbiValue) ByteString -> EVM t s ()
abiCall TestVMParams
testParams ((Text, AbiValue) -> Either (Text, AbiValue) ByteString
forall a b. a -> Either a b
Left (Text
"failed()", AbiValue
emptyAbi))
Stepper t RealWorld (VM t RealWorld)
forall (t :: VMType) s. Stepper t s (VM t 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 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
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
.. } Text
testName =
let ?context = DappContext { $sel:info:DappContext :: DappInfo
info = DappInfo
dapp, $sel:env:DappContext :: Map (Expr 'EAddr) Contract
env = VM t 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 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
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
.. } Text
testName =
let ?context = DappContext { $sel:info:DappContext :: DappInfo
info = DappInfo
dapp, $sel:env:DappContext :: Map (Expr 'EAddr) Contract
env = VM t 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 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"
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)]
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
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
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
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
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]
_ -> [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]
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
$ [Char] -> EVM t s ()
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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
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
..}) 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
, $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 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 -> [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
{ $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