hevm-0.55.1: cli/cli.hs
-- Main file of the hevm CLI program
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE OverloadedStrings #-}
module Main where
import Control.Monad (when, forM_, unless)
import Control.Monad.ST (RealWorld, stToIO)
import Control.Monad.IO.Unlift
import Control.Exception (try, IOException)
import Data.ByteString (ByteString)
import qualified Data.ByteString.Lazy as BS
import qualified Data.ByteString.Char8 as BC
import Data.DoubleWord (Word256)
import Data.List (intersperse, intercalate)
import Data.Maybe (fromMaybe, mapMaybe, fromJust, isNothing, isJust)
import Data.Text qualified as T
import Data.Text.IO qualified as T
import Data.Version (showVersion)
import Data.Word (Word64)
import GHC.Conc (getNumProcessors)
import Numeric.Natural (Natural)
import Optics.Core ((&), set)
import Witch (unsafeInto)
import Options.Generic as OptionsGeneric
import Options.Applicative as Options
import Paths_hevm qualified as Paths
import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist, makeAbsolute)
import System.FilePath ((</>))
import System.Exit (exitFailure, exitWith, ExitCode(..))
import Data.List.Split (splitOn)
import Text.Read (readMaybe)
import EVM (initialContract, abstractContract, makeVm)
import EVM.ABI (Sig(..))
import EVM.Dapp (dappInfo, DappInfo, emptyDapp)
import EVM.Expr qualified as Expr
import EVM.Concrete qualified as Concrete
import GitHash
import EVM.FeeSchedule (feeSchedule)
import EVM.Fetch qualified as Fetch
import EVM.Format (hexByteString, strip0x, formatExpr)
import EVM.Solidity
import EVM.Solvers
import EVM.Stepper qualified
import EVM.SymExec
import EVM.Transaction qualified
import EVM.Types hiding (word, Env, Symbolic)
import EVM.Types qualified
import EVM.UnitTest
import EVM.Effects
import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
data AssertionType = DSTest | Forge
deriving (Eq, Show, Read)
projectTypeParser :: Parser ProjectType
projectTypeParser = option auto (long "project-type" <> showDefault <> value Foundry <> help "Is this a CombinedJSON or Foundry project")
sigParser :: Parser (Maybe Text)
sigParser = (optional $ strOption $ long "sig" <> help "Signature of types to decode/encode")
argParser :: Parser [String]
argParser = (many $ strOption $ long "arg" <> help "Value(s) to encode. Can be given multiple times, once for each argument")
createParser :: Parser Bool
createParser = switch $ long "create" <> help "Tx: creation"
rpcParser :: Parser (Maybe URL)
rpcParser = (optional $ strOption $ long "rpc" <> help "Fetch state from a remote node")
data CommonOptions = CommonOptions
{ askSmtIterations ::Integer
, loopDetectionHeuristic ::LoopHeuristic
, noDecompose ::Bool
, solver ::Text
, debug ::Bool
, calldata ::Maybe ByteString
, trace ::Bool
, verb ::Int
, root ::Maybe String
, assertionType ::AssertionType
, solverThreads ::Natural
, smttimeout ::Natural
, smtdebug ::Bool
, numSolvers ::Maybe Natural
, numCexFuzz ::Integer
, maxIterations ::Integer
, promiseNoReent::Bool
, maxBufSize ::Int
, maxWidth ::Int
, maxDepth ::Maybe Int
, noSimplify ::Bool
}
commonOptions :: Parser CommonOptions
commonOptions = CommonOptions
<$> option auto ( long "ask-smt-iterations" <> value 1 <>
help "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability")
<*> option auto (long "loop-detection-heuristic" <> showDefault <> value StackBased <>
help "Which heuristic should be used to determine if we are in a loop: StackBased or Naive")
<*> (switch $ long "no-decompose" <> help "Don't decompose storage slots into separate arrays")
<*> (strOption $ long "solver" <> value "z3" <> help "Used SMT solver: z3, cvc5, or bitwuzla")
<*> (switch $ long "debug" <> help "Debug printing of internal behaviour, and dump internal expressions")
<*> (optional $ strOption $ long "calldata" <> help "Tx: calldata")
<*> (switch $ long "trace" <> help "Dump trace")
<*> (option auto $ long "verb" <> showDefault <> value 1 <> help "Append call trace: {1} failures {2} all")
<*> (optional $ strOption $ long "root" <> help "Path to project root directory")
<*> (option auto $ long "assertion-type" <> showDefault <> value Forge <> help "Assertions as per Forge or DSTest")
<*> (option auto $ long "solver-threads" <> showDefault <> value 1 <> help "Number of threads for each solver instance. Only respected for Z3")
<*> (option auto $ long "smttimeout" <> value 300 <> help "Timeout given to SMT solver in seconds")
<*> (switch $ long "smtdebug" <> help "Print smt queries sent to the solver")
<*> (optional $ option auto $ long "num-solvers" <> help "Number of solver instances to use (default: number of cpu cores)")
<*> (option auto $ long "num-cex-fuzz" <> showDefault <> value 3 <> help "Number of fuzzing tries to do to generate a counterexample")
<*> (option auto $ long "max-iterations" <> showDefault <> value 5 <> help "Number of times we may revisit a particular branching point. For no bound, set -1")
<*> (switch $ long "promise-no-reent" <> help "Promise no reentrancy is possible into the contract(s) being examined")
<*> (option auto $ long "max-buf-size" <> value 64 <> help "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)")
<*> (option auto $ long "max-width" <> showDefault <> value 100 <> help "Max number of concrete values to explore when encountering a symbolic value. This is a form of branch width limitation per symbolic value")
<*> (optional $ option auto $ long "max-depth" <> help "Limit maximum depth of branching during exploration (default: unlimited)")
<*> (switch $ long "no-simplify" <> help "Don't perform simplification of expressions")
data CommonExecOptions = CommonExecOptions
{ address ::Maybe Addr
, caller ::Maybe Addr
, origin ::Maybe Addr
, coinbase ::Maybe Addr
, value ::Maybe W256
, nonce ::Maybe Word64
, gas ::Maybe Word64
, number ::Maybe W256
, timestamp ::Maybe W256
, basefee ::Maybe W256
, priorityFee ::Maybe W256
, gaslimit ::Maybe Word64
, gasprice ::Maybe W256
, maxcodesize ::Maybe W256
, prevRandao ::Maybe W256
, chainid ::Maybe W256
, rpc ::Maybe URL
, block ::Maybe W256
}
commonExecOptions :: Parser CommonExecOptions
commonExecOptions = CommonExecOptions
<$> (optional $ option auto $ long "address" <> help "Tx: address")
<*> (optional $ option auto $ long "caller" <> help "Tx: caller")
<*> (optional $ option auto $ long "origin" <> help "Tx: origin")
<*> (optional $ option auto $ long "coinbase" <> help "Block: coinbase")
<*> (optional $ option auto $ long "value" <> help "Tx: Eth amount")
<*> (optional $ option auto $ long "nonce" <> help "Nonce of origin")
<*> (optional $ option auto $ long "gas" <> help "Tx: gas amount")
<*> (optional $ option auto $ long "number" <> help "Block: number")
<*> (optional $ option auto $ long "timestamp" <> help "Block: timestamp")
<*> (optional $ option auto $ long "basefee" <> help "Block: base fee")
<*> (optional $ option auto $ long "priority-fee" <> help "Tx: priority fee")
<*> (optional $ option auto $ long "gaslimit" <> help "Tx: gas limit")
<*> (optional $ option auto $ long "gasprice" <> help "Tx: gas price")
<*> (optional $ option auto $ long "maxcodesize" <> help "Block: max code size")
<*> (optional $ option auto $ long "prev-randao" <> help "Block: prevRandao")
<*> (optional $ option auto $ long "chainid" <> help "Env: chainId")
<*> rpcParser
<*> (optional $ option auto $ long "block" <> help "Block state is be fetched from")
data CommonFileOptions = CommonFileOptions
{ code ::Maybe ByteString
, codeFile ::Maybe String
}
commonFileOptions :: Parser CommonFileOptions
commonFileOptions = CommonFileOptions
<$> (optional $ strOption $ long "code" <> help "Program bytecode")
<*> (optional $ strOption $ long "code-file" <> help "Program bytecode in a file")
data TestOptions = TestOptions
{ projectType ::ProjectType
, rpc ::Maybe URL
, number ::Maybe W256
, coverage ::Bool
, match ::Maybe String
, prefix ::String
, ffi ::Bool
}
testOptions :: Parser TestOptions
testOptions = TestOptions
<$> projectTypeParser
<*> rpcParser
<*> (optional $ option auto $ long "number" <> help "Block: number")
<*> (switch $ long "coverage" <> help "Coverage analysis")
<*> (optional $ strOption $ long "match" <> help "Test case filter - only run methods matching regex")
<*> (strOption $ long "prefix" <> showDefault <> value "prove" <> help "Prefix for test cases to prove")
<*> (switch $ long "ffi" <> help "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)")
data EqOptions = EqOptions
{ codeA ::Maybe ByteString
, codeB ::Maybe ByteString
, codeAFile ::Maybe String
, codeBFile ::Maybe String
, sig ::Maybe Text
, arg ::[String]
, create ::Bool
}
eqOptions :: Parser EqOptions
eqOptions = EqOptions
<$> (optional $ strOption $ long "code-a" <> help "Bytecode of the first program")
<*> (optional $ strOption $ long "code-b" <> help "Bytecode of the second program")
<*> (optional $ strOption $ long "code-a-file" <> help "First program's bytecode in a file")
<*> (optional $ strOption $ long "code-b-file" <> help "Second program's bytecode in a file")
<*> sigParser
<*> argParser
<*> createParser
data SymbolicOptions = SymbolicOptions
{ projectType ::ProjectType
, initialStorage ::Maybe InitialStorage
, getModels ::Bool
, showTree ::Bool
, showReachableTree ::Bool
, assertions ::Maybe String
, sig ::Maybe Text
, arg ::[String]
, create ::Bool
}
symbolicOptions :: Parser SymbolicOptions
symbolicOptions = SymbolicOptions
<$> projectTypeParser
<*> (optional $ option auto $ long "initial-storage" <> help "Starting state for storage: Empty, Abstract (default Abstract)")
<*> (switch $ long "get-models" <> help "Print example testcase for each execution path")
<*> (switch $ long "show-tree" <> help "Print branches explored in tree view")
<*> (switch $ long "show-reachable-tree" <> showDefault <> help "Print only reachable branches explored in tree view")
<*> (optional $ strOption $ long "assertions" <> help "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)")
<*> sigParser
<*> argParser
<*> createParser
data ExecOptions = ExecOptions
{ projectType ::ProjectType
, create :: Bool
}
execOptions :: Parser ExecOptions
execOptions = ExecOptions
<$> projectTypeParser
<*> createParser
-- Combined options data type
data Command
= Symbolic CommonFileOptions SymbolicOptions CommonExecOptions CommonOptions
| Equal EqOptions CommonOptions
| Test TestOptions CommonOptions
| Exec CommonFileOptions ExecOptions CommonExecOptions CommonOptions
| Version
-- Parser for the subcommands
commandParser :: Parser Command
commandParser = subparser
( command "test"
(info (Test <$> testOptions <*> commonOptions <**> helper)
(progDesc "Prove Foundry unit tests prefixed with `prove` by default"
<> footer "For more help: https://hevm.dev/std-test-tutorial.html" ))
<> command "equivalence"
(info (Equal <$> eqOptions <*> commonOptions <**> helper)
(progDesc "Prove equivalence between two programs"
<> footer "For more help: https://hevm.dev/equivalence-checking-tutorial.html" ))
<> command "symbolic"
(info (Symbolic <$> commonFileOptions <*> symbolicOptions <*> commonExecOptions <*> commonOptions <**> helper)
(progDesc "Symbolically explore an abstract program"
<> footer "For more help, see: https://hevm.dev/symbolic-execution-tutorial.html" ))
<> command "exec"
(info (Exec <$> commonFileOptions <*> execOptions <*> commonExecOptions <*> commonOptions <**> helper)
(progDesc "Concretely execute a given program"
<> footer "For more help, see https://hevm.dev/exec.html" ))
<> command "version"
(info (pure Version)
(progDesc "Show the version of the tool"))
)
type URL = Text
deriving instance OptionsGeneric.ParseField Word256
deriving instance OptionsGeneric.ParseField [Word256]
data InitialStorage
= Empty
| Abstract
deriving (Show, Read, OptionsGeneric.ParseField)
getFullVersion :: [Char]
getFullVersion = showVersion Paths.version <> " [" <> gitVersion <> "]"
where
gitInfo = $$tGitInfoCwdTry
gitVersion = case gitInfo of
Right val -> "git rev " <> giBranch val <> "@" <> giHash val
Left _ -> "no git revision present"
main :: IO ()
main = do
cmd <- execParser $ info (commandParser <**> helper)
( Options.fullDesc
<> progDesc "hevm, a symbolic and concrete EVM bytecode execution framework"
<> footer "See https://hevm.dev for more information"
)
case cmd of
Symbolic cFileOpts symbOpts cExecOpts cOpts -> do
env <- makeEnv cOpts
root <- getRoot cOpts
withCurrentDirectory root $ runEnv env $ symbCheck cFileOpts symbOpts cExecOpts cOpts
Equal eqOpts cOpts -> do
env <- makeEnv cOpts
runEnv env $ equivalence eqOpts cOpts
Test testOpts cOpts -> do
env <- makeEnv cOpts
root <- getRoot cOpts
solver <- getSolver cOpts.solver
cores <- liftIO $ unsafeInto <$> getNumProcessors
let solverCount = fromMaybe cores cOpts.numSolvers
runEnv env $ withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \solvers -> do
buildOut <- readBuildOutput root testOpts.projectType
case buildOut of
Left e -> liftIO $ do
putStrLn $ "Error: " <> e
exitFailure
Right out -> do
-- TODO: which functions here actually require a BuildOutput, and which can take it as a Maybe?
unitTestOpts <- liftIO $ unitTestOptions testOpts cOpts solvers (Just out)
res <- unitTest unitTestOpts out.contracts
liftIO $ unless (uncurry (&&) res) exitFailure
Exec cFileOpts execOpts cExecOpts cOpts-> do
env <- makeEnv cOpts
runEnv env $ launchExec cFileOpts execOpts cExecOpts cOpts
Version {} ->putStrLn getFullVersion
where
makeEnv :: CommonOptions -> IO Env
makeEnv cOpts = do
when (cOpts.maxBufSize > 64) $ do
putStrLn "Error: maxBufSize must be less than or equal to 64. That limits buffers to a size of 2^64, which is more than enough for practical purposes"
exitFailure
when (cOpts.maxBufSize < 0) $ do
putStrLn "Error: maxBufSize must be at least 0. Negative values do not make sense. A value of zero means at most 1 byte long buffers"
exitFailure
pure Env { config = defaultConfig
{ dumpQueries = cOpts.smtdebug
, debug = cOpts.debug
, dumpEndStates = cOpts.debug
, dumpExprs = cOpts.debug
, numCexFuzz = cOpts.numCexFuzz
, dumpTrace = cOpts.trace
, decomposeStorage = Prelude.not cOpts.noDecompose
, promiseNoReent = cOpts.promiseNoReent
, maxBufSize = cOpts.maxBufSize
, maxWidth = cOpts.maxWidth
, maxDepth = cOpts.maxDepth
, verb = cOpts.verb
, simp = Prelude.not cOpts.noSimplify
} }
getCode :: Maybe String -> Maybe ByteString -> IO (Maybe ByteString)
getCode fname code = do
when (isJust fname && isJust code) $ do
putStrLn "Error: Cannot provide both a file and code"
exitFailure
case fname of
Nothing -> pure $ fmap strip code
Just f -> do
result <- try (BS.readFile f) :: IO (Either IOException BS.ByteString)
case result of
Left e -> do
putStrLn $ "Error reading file: " <> show e
exitFailure
Right content -> do
pure $ Just $ strip (BS.toStrict content)
where
strip = BC.filter (\c -> c /= ' ' && c /= '\n' && c /= '\r' && c /= '\t' && c /= '"')
equivalence :: App m => EqOptions -> CommonOptions -> m ()
equivalence eqOpts cOpts = do
bytecodeA' <- liftIO $ getCode eqOpts.codeAFile eqOpts.codeA
bytecodeB' <- liftIO $ getCode eqOpts.codeBFile eqOpts.codeB
let bytecodeA = decipher bytecodeA'
let bytecodeB = decipher bytecodeB'
when (isNothing bytecodeA) $ liftIO $ do
putStrLn "Error: invalid or no bytecode for program A. Provide a valid one with --code-a or --code-a-file"
exitFailure
when (isNothing bytecodeB) $ liftIO $ do
putStrLn "Error: invalid or no bytecode for program B. Provide a valid one with --code-b or --code-b-file"
exitFailure
let veriOpts = VeriOpts { iterConf = IterConfig {
maxIter = parseMaxIters cOpts.maxIterations
, askSmtIters = cOpts.askSmtIterations
, loopHeuristic = cOpts.loopDetectionHeuristic
}
, rpcInfo = Nothing
}
calldata <- buildCalldata cOpts eqOpts.sig eqOpts.arg
solver <- liftIO $ getSolver cOpts.solver
cores <- liftIO $ unsafeInto <$> getNumProcessors
let solverCount = fromMaybe cores cOpts.numSolvers
withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \s -> do
eq <- equivalenceCheck s (fromJust bytecodeA) (fromJust bytecodeB) veriOpts calldata eqOpts.create
let anyIssues = not (null eq.partials) || any (isUnknown . fst) eq.res || any (isError . fst) eq.res
liftIO $ case (any (isCex . fst) eq.res, anyIssues) of
(False, False) -> putStrLn " \x1b[32m[PASS]\x1b[0m Contracts behave equivalently"
(True, _) -> putStrLn " \x1b[31m[FAIL]\x1b[0m Contracts do not behave equivalently"
(_, True) -> putStrLn " \x1b[31m[FAIL]\x1b[0m Contracts may not behave equivalently"
liftIO $ printWarnings eq.partials (map fst eq.res) "the contracts under test"
case any (isCex . fst) eq.res of
False -> liftIO $ do
when anyIssues exitFailure
putStrLn "No discrepancies found"
True -> liftIO $ do
let cexes = mapMaybe getCexP eq.res
T.putStrLn . T.unlines $
[ "Not equivalent. The following inputs result in differing behaviours:"
, "" , "-----", ""
] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap formatCexes cexes)
exitFailure
where
decipher = maybe Nothing (hexByteString . strip0x)
getCexP :: (ProofResult a b, String) -> Maybe (a, String)
getCexP (Cex c, reason) = Just (c, reason)
getCexP _ = Nothing
formatCexes (cex, reason) = formatCex (AbstractBuf "txdata") Nothing cex <> "Difference: " <> T.pack reason
getSolver :: Text -> IO Solver
getSolver s = case T.unpack s of
"z3" -> pure Z3
"cvc5" -> pure CVC5
"bitwuzla" -> pure Bitwuzla
input -> do
putStrLn $ "unrecognised solver: " <> input
exitFailure
getSrcInfo :: App m => ExecOptions -> CommonOptions -> m DappInfo
getSrcInfo execOpts cOpts = do
root <- liftIO $ getRoot cOpts
conf <- readConfig
liftIO $ withCurrentDirectory root $ do
outExists <- doesDirectoryExist (root System.FilePath.</> "out")
if outExists
then do
buildOutput <- runEnv Env {config = conf} $ readBuildOutput root execOpts.projectType
case buildOutput of
Left _ -> pure emptyDapp
Right o -> pure $ dappInfo root o
else pure emptyDapp
getRoot :: CommonOptions -> IO FilePath
getRoot cmd = maybe getCurrentDirectory makeAbsolute cmd.root
parseMaxIters :: Integer -> Maybe Integer
parseMaxIters num = if num < 0 then Nothing else Just num
-- | Builds a buffer representing calldata based on the given cli arguments
buildCalldata :: App m => CommonOptions -> Maybe Text -> [String] -> m (Expr Buf, [Prop])
buildCalldata cOpts sig arg = case (cOpts.calldata, sig) of
-- fully abstract calldata
(Nothing, Nothing) -> mkCalldata Nothing []
-- fully concrete calldata
(Just c, Nothing) -> do
let val = hexByteString $ strip0x c
if (isNothing val) then liftIO $ do
putStrLn $ "Error, invalid calldata: " <> show c
exitFailure
else pure (ConcreteBuf (fromJust val), [])
-- calldata according to given abi with possible specializations from the `arg` list
(Nothing, Just sig') -> do
method' <- liftIO $ functionAbi sig'
mkCalldata (Just (Sig method'.methodSignature (snd <$> method'.inputs))) arg
-- both args provided
(_, _) -> liftIO $ do
putStrLn "incompatible options provided: --calldata and --sig"
exitFailure
-- If function signatures are known, they should always be given for best results.
symbCheck :: App m => CommonFileOptions -> SymbolicOptions -> CommonExecOptions -> CommonOptions -> m ()
symbCheck cFileOpts sOpts cExecOpts cOpts = do
let block' = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
rpcinfo = (,) block' <$> cExecOpts.rpc
calldata <- buildCalldata cOpts sOpts.sig sOpts.arg
preState <- liftIO $ symvmFromCommand cExecOpts sOpts cFileOpts calldata
errCodes <- case sOpts.assertions of
Nothing -> pure defaultPanicCodes
Just s -> case (mapM readMaybe $ splitOn "," s) of
Nothing -> liftIO $ do
putStrLn $ "Error: invalid assertion codes: " <> s
exitFailure
Just codes -> pure codes
when (cOpts.verb > 0) $ liftIO $ putStrLn $ "Using assertion code(s): " <> intercalate "," (map show errCodes)
cores <- liftIO $ unsafeInto <$> getNumProcessors
let solverCount = fromMaybe cores cOpts.numSolvers
solver <- liftIO $ getSolver cOpts.solver
withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \solvers -> do
let veriOpts = VeriOpts { iterConf = IterConfig {
maxIter = parseMaxIters cOpts.maxIterations
, askSmtIters = cOpts.askSmtIterations
, loopHeuristic = cOpts.loopDetectionHeuristic
}
, rpcInfo = rpcinfo
}
(expr, res) <- verify solvers veriOpts preState (Just $ checkAssertions errCodes)
case res of
[Qed] -> do
liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"
showExtras solvers sOpts calldata expr
_ -> do
let cexs = snd <$> mapMaybe getCex res
counterexamples
| null cexs = []
| otherwise =
[ ""
, ("Discovered the following " <> (T.pack $ show (length cexs)) <> " counterexample(s):")
, ""
] <> fmap (formatCex (fst calldata) Nothing) cexs
liftIO $ T.putStrLn $ T.unlines counterexamples
liftIO $ printWarnings [expr] res "symbolically"
showExtras solvers sOpts calldata expr
liftIO exitFailure
showExtras :: App m => SolverGroup ->SymbolicOptions -> (Expr Buf, [Prop]) -> Expr End -> m ()
showExtras solvers sOpts calldata expr = do
when sOpts.showTree $ liftIO $ do
putStrLn "=== Expression ===\n"
T.putStrLn $ formatExpr expr
putStrLn ""
when sOpts.showReachableTree $ do
reached <- reachable solvers expr
liftIO $ do
putStrLn "=== Potentially Reachable Expression ===\n"
T.putStrLn (formatExpr . snd $ reached)
putStrLn ""
when sOpts.getModels $ do
liftIO $ putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ==="
ms <- produceModels solvers expr
liftIO $ forM_ ms (showModel (fst calldata))
isTestOrLib :: Text -> Bool
isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "src/tests/", "lib/"] file
areAnyPrefixOf :: [Text] -> Text -> Bool
areAnyPrefixOf prefixes t = any (flip T.isPrefixOf t) prefixes
launchExec :: App m => CommonFileOptions -> ExecOptions -> CommonExecOptions -> CommonOptions -> m ()
launchExec cFileOpts execOpts cExecOpts cOpts = do
dapp <- getSrcInfo execOpts cOpts
vm <- liftIO $ vmFromCommand cOpts cExecOpts cFileOpts execOpts
let
block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
rpcinfo = (,) block <$> cExecOpts.rpc
-- TODO: we shouldn't need solvers to execute this code
withSolvers Z3 0 1 Nothing $ \solvers -> do
vm' <- EVM.Stepper.interpret (Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully
writeTraceDapp dapp vm'
case vm'.result of
Just (VMFailure (Revert msg)) -> liftIO $ do
let res = case msg of
ConcreteBuf bs -> bs
_ -> "<symbolic>"
putStrLn $ "Revert: " <> (show $ ByteStringS res)
exitWith (ExitFailure 2)
Just (VMFailure err) -> liftIO $ do
putStrLn $ "Error: " <> show err
exitWith (ExitFailure 2)
Just (VMSuccess buf) -> liftIO $ do
let msg = case buf of
ConcreteBuf msg' -> msg'
_ -> "<symbolic>"
print $ "Return: " <> (show $ ByteStringS msg)
_ ->
internalError "no EVM result"
-- | Creates a (concrete) VM from command line options
vmFromCommand :: CommonOptions -> CommonExecOptions -> CommonFileOptions -> ExecOptions -> IO (VM Concrete RealWorld)
vmFromCommand cOpts cExecOpts cFileOpts execOpts= do
(miner,ts,baseFee,blockNum,prevRan) <- case cExecOpts.rpc of
Nothing -> pure (LitAddr 0,Lit 0,0,Lit 0,0)
Just url -> Fetch.fetchBlockFrom block url >>= \case
Nothing -> do
putStrLn $ "Error, Could not fetch block" <> show block <> " from URL: " <> show url
exitFailure
Just Block{..} -> pure ( coinbase
, timestamp
, baseFee
, number
, prevRandao
)
codeWrapped <- getCode cFileOpts.codeFile cFileOpts.code
contract <- case (cExecOpts.rpc, cExecOpts.address, codeWrapped) of
(Just url, Just addr', Just c) -> do
let code = hexByteString $ strip0x c
if isNothing code then do
putStrLn $ "Error, invalid code: " <> show c
exitFailure
else
Fetch.fetchContractFrom block url addr' >>= \case
Nothing -> do
putStrLn $ "Error: contract not found: " <> show address
exitFailure
Just contract ->
-- if both code and url is given,
-- fetch the contract and overwrite the code
pure $
initialContract (mkCode $ fromJust code)
& set #balance (contract.balance)
& set #nonce (contract.nonce)
& set #external (contract.external)
(Just url, Just addr', Nothing) ->
Fetch.fetchContractFrom block url addr' >>= \case
Nothing -> do
putStrLn $ "Error, contract not found: " <> show address
exitFailure
Just contract -> pure contract
(_, _, Just c) -> do
let code = hexByteString $ strip0x c
if (isNothing code) then do
putStrLn $ "Error, invalid code: " <> show c
exitFailure
else pure $ initialContract (mkCode $ fromJust code)
(_, _, Nothing) -> do
putStrLn "Error, must provide at least (rpc + address) or code"
exitFailure
let ts' = case maybeLitWordSimp ts of
Just t -> t
Nothing -> internalError "unexpected symbolic timestamp when executing vm test"
if (isNothing bsCallData) then do
putStrLn $ "Error, invalid calldata: " <> show calldata
exitFailure
else do
vm <- stToIO $ vm0 baseFee miner ts' blockNum prevRan contract
pure $ EVM.Transaction.initTx vm
where
bsCallData = bytes (.calldata) (pure "")
block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
val = word (.value) 0
caller = addr (.caller) (LitAddr 0)
origin = addr (.origin) (LitAddr 0)
calldata = ConcreteBuf $ fromJust bsCallData
decipher = hexByteString . strip0x
mkCode bs = if execOpts.create
then InitCode bs mempty
else RuntimeCode (ConcreteRuntimeCode bs)
address = if execOpts.create
then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddrSimp origin) (W64 $ word64 (.nonce) 0))
else addr (.address) (LitAddr 0xacab)
vm0 baseFee miner ts blockNum prevRan c = makeVm $ VMOpts
{ contract = c
, otherContracts = []
, calldata = (calldata, [])
, value = Lit val
, address = address
, caller = caller
, origin = origin
, gas = word64 (.gas) 0xffffffffffffffff
, baseFee = baseFee
, priorityFee = word (.priorityFee) 0
, gaslimit = word64 (.gaslimit) 0xffffffffffffffff
, coinbase = addr (.coinbase) miner
, number = maybe blockNum Lit cExecOpts.number
, timestamp = Lit $ word (.timestamp) ts
, blockGaslimit = word64 (.gaslimit) 0xffffffffffffffff
, gasprice = word (.gasprice) 0
, maxCodeSize = word (.maxcodesize) 0xffffffff
, prevRandao = word (.prevRandao) prevRan
, schedule = feeSchedule
, chainId = word (.chainid) 1
, create = (.create) execOpts
, baseState = EmptyBase
, txAccessList = mempty -- TODO: support me soon
, allowFFI = False
, freshAddresses = 0
, beaconRoot = 0
}
word f def = fromMaybe def (f cExecOpts)
word64 f def = fromMaybe def (f cExecOpts)
addr f def = maybe def LitAddr (f cExecOpts)
bytes f def = maybe def decipher (f cOpts)
symvmFromCommand :: CommonExecOptions -> SymbolicOptions -> CommonFileOptions -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld)
symvmFromCommand cExecOpts sOpts cFileOpts calldata = do
(miner,blockNum,baseFee,prevRan) <- case cExecOpts.rpc of
Nothing -> pure (SymAddr "miner",Lit 0,0,0)
Just url -> Fetch.fetchBlockFrom block url >>= \case
Nothing -> do
putStrLn $ "Error, Could not fetch block" <> show block <> " from URL: " <> show url
exitFailure
Just Block{..} -> pure ( coinbase
, number
, baseFee
, prevRandao
)
let
caller = maybe (SymAddr "caller") LitAddr cExecOpts.caller
ts = maybe Timestamp Lit cExecOpts.timestamp
callvalue = maybe TxValue Lit cExecOpts.value
storageBase = maybe AbstractBase parseInitialStorage (sOpts.initialStorage)
codeWrapped <- getCode cFileOpts.codeFile cFileOpts.code
contract <- case (cExecOpts.rpc, cExecOpts.address, codeWrapped) of
(Just url, Just addr', _) ->
Fetch.fetchContractFrom block url addr' >>= \case
Nothing -> do
putStrLn "Error, contract not found."
exitFailure
Just contract' -> case codeWrapped of
Nothing -> pure contract'
-- if both code and url is given,
-- fetch the contract and overwrite the code
Just c -> do
let c' = decipher c
if isNothing c' then do
putStrLn $ "Error, invalid code: " <> show c
exitFailure
else pure $ do
initialContract (mkCode $ fromJust c')
& set #origStorage (contract'.origStorage)
& set #balance (contract'.balance)
& set #nonce (contract'.nonce)
& set #external (contract'.external)
(_, _, Just c) -> do
let c' = decipher c
if isNothing c' then do
putStrLn $ "Error, invalid code: " <> show c
exitFailure
else case storageBase of
EmptyBase -> pure (initialContract . mkCode $ fromJust c')
AbstractBase -> pure ((`abstractContract` address) . mkCode $ fromJust c')
(_, _, Nothing) -> do
putStrLn "Error, must provide at least (rpc + address) or code"
exitFailure
vm <- stToIO $ vm0 baseFee miner ts blockNum prevRan calldata callvalue caller contract storageBase
pure $ EVM.Transaction.initTx vm
where
decipher = hexByteString . strip0x
block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
origin = eaddr (.origin) (SymAddr "origin")
mkCode bs = if sOpts.create
then InitCode bs mempty
else RuntimeCode (ConcreteRuntimeCode bs)
address = eaddr (.address) (SymAddr "entrypoint")
vm0 baseFee miner ts blockNum prevRan cd callvalue caller c baseState = makeVm $ VMOpts
{ contract = c
, otherContracts = []
, calldata = cd
, value = callvalue
, address = address
, caller = caller
, origin = origin
, gas = ()
, gaslimit = word64 (.gaslimit) 0xffffffffffffffff
, baseFee = baseFee
, priorityFee = word (.priorityFee) 0
, coinbase = eaddr (.coinbase) miner
, number = maybe blockNum Lit cExecOpts.number
, timestamp = ts
, blockGaslimit = word64 (.gaslimit) 0xffffffffffffffff
, gasprice = word (.gasprice) 0
, maxCodeSize = word (.maxcodesize) 0xffffffff
, prevRandao = word (.prevRandao) prevRan
, schedule = feeSchedule
, chainId = word (.chainid) 1
, create = (.create) sOpts
, baseState = baseState
, txAccessList = mempty
, allowFFI = False
, freshAddresses = 0
, beaconRoot = 0
}
word f def = fromMaybe def (f cExecOpts)
word64 f def = fromMaybe def (f cExecOpts)
eaddr f def = maybe def LitAddr (f cExecOpts)
unitTestOptions :: TestOptions -> CommonOptions -> SolverGroup -> Maybe BuildOutput -> IO (UnitTestOptions RealWorld)
unitTestOptions testOpts cOpts solvers buildOutput = do
root <- getRoot cOpts
let srcInfo = maybe emptyDapp (dappInfo root) buildOutput
let rpcinfo = case (testOpts.number, testOpts.rpc) of
(Just block, Just url) -> Just (Fetch.BlockNumber block, url)
(Nothing, Just url) -> Just (Fetch.Latest, url)
_ -> Nothing
params <- paramsFromRpc rpcinfo
let testn = params.number
block' = if 0 == testn
then Fetch.Latest
else Fetch.BlockNumber testn
pure UnitTestOptions
{ solvers = solvers
, rpcInfo = case testOpts.rpc of
Just url -> Just (block', url)
Nothing -> Nothing
, maxIter = parseMaxIters cOpts.maxIterations
, askSmtIters = cOpts.askSmtIterations
, smtTimeout = Just cOpts.smttimeout
, match = T.pack $ fromMaybe ".*" testOpts.match
, prefix = T.pack testOpts.prefix
, testParams = params
, dapp = srcInfo
, ffiAllowed = testOpts.ffi
, checkFailBit = cOpts.assertionType == DSTest
}
parseInitialStorage :: InitialStorage -> BaseState
parseInitialStorage Empty = EmptyBase
parseInitialStorage Abstract = AbstractBase