diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,21 @@ # hevm changelog +## 0.47.0 - 2021-07-01 + +- A new test runner for checking invariants against random reachable contract states. +- `hevm symbolic` can search for solc 0.8 style assertion violations, and a new `--assertions` flag + has been added allowing users to customize which assertions should be reported +- A new cheatcode `ffi(string[])` that executes an arbitrary command in the system shell + +### Changed + +- Z3 is once again the default smt solver +- Updated nixpkgs to the `21.05` channel + +### Fixed + +- Sourcemaps for contracts containing `immutable` are now shown in the debug view. + ## 0.46.0 - 2021-04-29 ### Added diff --git a/hevm-cli/hevm-cli.hs b/hevm-cli/hevm-cli.hs --- a/hevm-cli/hevm-cli.hs +++ b/hevm-cli/hevm-cli.hs @@ -2,6 +2,8 @@ {-# Language CPP #-} {-# Language DataKinds #-} +{-# Language StandaloneDeriving #-} +{-# Language DeriveAnyClass #-} {-# Language FlexibleInstances #-} {-# Language DeriveGeneric #-} {-# Language GADTs #-} @@ -60,6 +62,7 @@ import Data.Text.IO (hPutStr) import Data.Maybe (fromMaybe, fromJust) import Data.Version (showVersion) +import Data.DoubleWord (Word256) import Data.SBV hiding (Word, solver, verbose, name) import Data.SBV.Control hiding (Version, timeout, create) import System.IO (hFlush, stdout, stderr) @@ -126,6 +129,7 @@ , maxIterations :: w ::: Maybe Integer "Number of times we may revisit a particular branching point" , solver :: w ::: Maybe Text "Used SMT solver: z3 (default) or cvc4" , smtdebug :: w ::: Bool "Print smt queries sent to the solver" + , assertions :: w ::: Maybe [Word256] "Comma seperated list of solc panic codes to check for (default: everything except arithmetic overflow)" } | Equivalence -- prove equivalence between two programs { codeA :: w ::: ByteString "Bytecode of the first program" @@ -171,6 +175,7 @@ , debug :: w ::: Bool "Run interactively" , jsontrace :: w ::: Bool "Print json trace output at every step" , fuzzRuns :: w ::: Maybe Int "Number of times to run fuzz tests" + , depth :: w ::: Maybe Int "Number of transactions to explore" , replay :: w ::: Maybe (Text, ByteString) "Custom fuzz case to run/debug" , rpc :: w ::: Maybe URL "Fetch state from a remote node" , verbose :: w ::: Maybe Int "Append call trace: {1} failures {2} all" @@ -182,6 +187,7 @@ , maxIterations :: w ::: Maybe Integer "Number of times we may revisit a particular branching point" , solver :: w ::: Maybe Text "Used SMT solver: z3 (default) or cvc4" , smtdebug :: w ::: Bool "Print smt queries sent to the solver" + , ffi :: w ::: Bool "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)" } | BcTest -- Run an Ethereum Blockhain/GeneralState test { file :: w ::: String "Path to .json test file" @@ -229,6 +235,9 @@ -- parseField instance for (Text, ByteString) instance Options.ParseField (Text, ByteString) +deriving instance Options.ParseField Word256 +deriving instance Options.ParseField [Word256] + instance Options.ParseRecord (Command Options.Wrapped) where parseRecord = Options.parseRecordWithModifiers Options.lispCaseModifiers @@ -284,6 +293,7 @@ , EVM.UnitTest.smtState = Just state , EVM.UnitTest.verbose = verbose cmd , EVM.UnitTest.match = pack $ fromMaybe ".*" (match cmd) + , EVM.UnitTest.maxDepth = depth cmd , EVM.UnitTest.fuzzRuns = fromMaybe 100 (fuzzRuns cmd) , EVM.UnitTest.replay = do arg' <- replay cmd @@ -291,6 +301,7 @@ , EVM.UnitTest.vmModifier = vmModifier , EVM.UnitTest.testParams = params , EVM.UnitTest.dapp = srcInfo + , EVM.UnitTest.allowFFI = ffi cmd } main :: IO () @@ -425,7 +436,7 @@ runSMTWithTimeOut solver maybeTimeout smtdebug symb | solver == Just "cvc4" = runwithcvc4 | solver == Just "z3" = runwithz3 - | solver == Nothing = runwithcvc4 + | solver == Nothing = runwithz3 | otherwise = error "Unknown solver. Currently supported solvers; z3, cvc4" where timeout = fromMaybe 30000 maybeTimeout runwithz3 = runSMTWith z3{SBV.verbose=smtdebug} $ (setTimeOut timeout) >> symb @@ -503,7 +514,8 @@ else runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do preState <- symvmFromCommand cmd - verify preState (maxIterations cmd) rpcinfo (Just checkAssertions) >>= \case + let errCodes = fromMaybe defaultPanicCodes (assertions cmd) + verify preState (maxIterations cmd) rpcinfo (Just $ checkAssertions errCodes) >>= \case Right tree -> do io $ putStrLn "Assertion violation found." showCounterexample preState maybesig @@ -757,7 +769,8 @@ , EVM.vmoptChainId = word chainid 1 , EVM.vmoptCreate = create cmd , EVM.vmoptStorageModel = ConcreteS - , EVM.vmoptTxAccessList = mempty -- TODO: support me soon + , EVM.vmoptTxAccessList = mempty -- TODO: support me soon + , EVM.vmoptAllowFFI = False } word f def = fromMaybe def (f cmd) addr f def = fromMaybe def (f cmd) @@ -769,7 +782,7 @@ (miner,blockNum,diff) <- case rpc cmd of Nothing -> return (0,0,0) Just url -> io $ EVM.Fetch.fetchBlockFrom block' url >>= \case - Nothing -> error $ "Could not fetch block" + Nothing -> error "Could not fetch block" Just EVM.Block{..} -> return (_coinbase , wordValue _number , wordValue _difficulty @@ -827,7 +840,7 @@ & set EVM.external (view EVM.external contract') (_, _, Just c) -> - return $ (EVM.initialContract . codeType $ decipher c) + return (EVM.initialContract . codeType $ decipher c) (_, _, Nothing) -> error "must provide at least (rpc + address) or code" @@ -864,6 +877,7 @@ , EVM.vmoptCreate = create cmd , EVM.vmoptStorageModel = fromMaybe SymbolicS (storageModel cmd) , EVM.vmoptTxAccessList = mempty + , EVM.vmoptAllowFFI = False } word f def = fromMaybe def (f cmd) addr f def = fromMaybe def (f cmd) diff --git a/hevm.cabal b/hevm.cabal --- a/hevm.cabal +++ b/hevm.cabal @@ -2,7 +2,7 @@ name: hevm version: - 0.46.0 + 0.47.0 synopsis: Ethereum virtual machine evaluator description: @@ -81,14 +81,14 @@ ethjet/tinykeccak.h, ethjet/ethjet.h, ethjet/ethjet-ff.h, ethjet/blake2.h build-depends: QuickCheck >= 2.13.2 && < 2.15, - Decimal == 0.5.1, + Decimal >= 0.5.1 && < 0.6, containers >= 0.6.0 && < 0.7, deepseq >= 1.4.4 && < 1.5, time >= 1.8.0 && < 1.11, transformers >= 0.5.6 && < 0.6, - tree-view == 0.5, + tree-view >= 0.5 && < 0.6, abstract-par >= 0.3.3 && < 0.4, - aeson >= 1.4.6 && < 1.5, + aeson >= 1.5.6 && < 1.6, bytestring >= 0.10.8 && < 0.11, scientific >= 0.3.6 && < 0.4, binary >= 0.8.6 && < 0.9, @@ -96,20 +96,20 @@ unordered-containers >= 0.2.10 && < 0.3, vector >= 0.12.1 && < 0.13, ansi-wl-pprint >= 0.6.9 && < 0.7, - base16-bytestring >= 0.1.1 && < 0.2, - brick >= 0.47.1 && < 0.56, - megaparsec >= 7.0.5 && < 8.1, + base16-bytestring >= 1.0.0 && < 2.0, + brick >= 0.58 && < 0.63, + megaparsec >= 9.0.0 && < 10.0, mtl >= 2.2.2 && < 2.3, directory >= 1.3.3 && < 1.4, filepath >= 1.4.2 && < 1.5, - vty >= 5.25.1 && < 5.31, + vty >= 5.25.1 && < 5.34, cereal >= 0.5.8 && < 0.6, cryptonite >= 0.27 && < 0.29, memory >= 0.14.18 && < 0.16, data-dword >= 0.3.1 && < 0.4, fgl >= 5.7.0 && < 5.8, free >= 5.1.3 && < 5.2, - haskeline >= 0.7.4 && < 0.8, + haskeline >= 0.8.0 && < 0.9, process >= 1.6.5 && < 1.7, lens >= 4.17.1 && < 4.20, lens-aeson >= 1.0.2 && < 1.2, @@ -125,10 +125,11 @@ semver-range >= 0.2.7 && < 0.3, temporary >= 1.3 && < 1.4, text-format >= 0.3.2 && < 0.4, - witherable >= 0.3.5 && < 0.4, + witherable >= 0.3.5 && < 0.5, wreq >= 0.5.3 && < 0.6, regex-tdfa >= 1.2.3 && < 1.4, - base >= 4.9 && < 5 + base >= 4.9 && < 5, + here >= 1.2.13 && < 1.3, hs-source-dirs: src default-language: diff --git a/src/EVM.hs b/src/EVM.hs --- a/src/EVM.hs +++ b/src/EVM.hs @@ -17,6 +17,9 @@ import Data.SBV hiding (Word, output, Unknown) import Data.Proxy (Proxy(..)) +import Data.Text (unpack) +import Data.Text.Encoding (decodeUtf8, encodeUtf8) +import qualified Data.Vector as V import EVM.ABI import EVM.Types import EVM.Solidity @@ -49,6 +52,7 @@ import qualified Data.Map.Strict as Map import qualified Data.Sequence as Seq import qualified Data.Tree.Zipper as Zipper +import qualified Data.Vector as V import qualified Data.Vector.Storable as Vector import qualified Data.Vector.Storable.Mutable as Vector @@ -87,6 +91,7 @@ | DeadPath | NotUnique Whiff | SMTTimeout + | FFI AbiVals deriving instance Show Error -- | The possible result states of a VM @@ -110,12 +115,13 @@ , _burned :: Word , _constraints :: [(SBool, Whiff)] , _iterations :: Map CodeLocation Int + , _allowFFI :: Bool } deriving (Show) data Trace = Trace - { _traceCodehash :: W256 - , _traceOpIx :: Maybe Int + { _traceOpIx :: Int + , _traceContract :: Contract , _traceData :: TraceData } deriving (Show) @@ -135,6 +141,7 @@ PleaseMakeUnique :: SymVal a => SBV a -> [SBool] -> (IsUnique a -> EVM ()) -> Query PleaseFetchSlot :: Addr -> Word -> (Word -> EVM ()) -> Query PleaseAskSMT :: SBool -> [SBool] -> (BranchCondition -> EVM ()) -> Query + PleaseDoFFI :: [String] -> (ByteString -> EVM ()) -> Query data Choose where PleaseChoosePath :: Whiff -> (Bool -> EVM ()) -> Choose @@ -155,6 +162,8 @@ (("") ++) + PleaseDoFFI cmd _ -> + ((" VM -makeVm o = +makeVm o = let txaccessList = vmoptTxAccessList o txorigin = vmoptOrigin o txtoAddr = vmoptAddress o initialAccessedAddrs = fromList $ [txorigin, txtoAddr] ++ [1..9] ++ (Map.keys txaccessList) initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList) touched = if vmoptCreate o then [txorigin] else [txorigin, txtoAddr] - in + in VM { _result = Nothing , _frames = mempty @@ -485,6 +507,7 @@ , _burned = 0 , _constraints = [] , _iterations = mempty + , _allowFFI = vmoptAllowFFI o } where theCode = case _contractcode (vmoptContract o) of InitCode b -> b RuntimeCode b -> b @@ -1574,8 +1597,8 @@ Unique a -> do assign result Nothing cont (C w $ fromSizzle a) - InconsistentU -> vmError $ DeadPath - TimeoutU -> vmError $ SMTTimeout + InconsistentU -> vmError DeadPath + TimeoutU -> vmError SMTTimeout Multiple -> vmError $ NotUnique w Just a -> cont a @@ -1939,7 +1962,30 @@ cheatActions :: Map Word32 CheatAction cheatActions = Map.fromList - [ action "warp(uint256)" $ + [ action "ffi(string[])" $ + \sig outOffset outSize input -> do + vm <- get + if view EVM.allowFFI vm then + case decodeBuffer [AbiArrayDynamicType AbiStringType] input of + CAbi valsArr -> case valsArr of + [AbiArrayDynamic AbiStringType strsV] -> + let + cmd = (flip fmap) (V.toList strsV) (\case + (AbiString a) -> unpack $ decodeUtf8 a + _ -> "") + cont bs = do + let encoded = ConcreteBuffer bs + assign (state . returndata) encoded + copyBytesToMemory encoded outSize 0 outOffset + assign result Nothing + in assign result (Just . VMFailure . Query $ (PleaseDoFFI cmd cont)) + _ -> vmError (BadCheatCode sig) + _ -> vmError (BadCheatCode sig) + else + let msg = encodeUtf8 "ffi disabled: run again with --ffi if you want to allow tests to call external scripts" + in vmError . Revert $ abiMethod "Error(string)" (AbiTuple . V.fromList $ [AbiString msg]), + + action "warp(uint256)" $ \sig _ _ input -> case decodeStaticArgs input of [x] -> assign (block . timestamp) x _ -> vmError (BadCheatCode sig), @@ -2111,7 +2157,7 @@ then do assign (state . stack) (0 : xs) assign (state . returndata) mempty - pushTrace $ ErrorTrace $ CallDepthLimitReached + pushTrace $ ErrorTrace CallDepthLimitReached next else if collision $ view (env . contracts . at newAddr) vm0 then burn xGas $ do @@ -2271,7 +2317,7 @@ -- In other words, we special case address 0x03 and keep it in the set of touched accounts during revert touched <- use (tx . substate . touchedAccounts) - + let substate'' = over touchedAccounts (maybe id cons (find ((==) 3) touched)) substate' revertContracts = assign (env . contracts) reversion @@ -2408,8 +2454,8 @@ currentContract vm pure Trace { _traceData = x - , _traceCodehash = view codehash this - , _traceOpIx = (view opIxMap this) Vector.!? (view (state . pc) vm) + , _traceContract = this + , _traceOpIx = fromMaybe 0 $ (view opIxMap this) Vector.!? (view (state . pc) vm) } pushTrace :: TraceData -> EVM () diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs --- a/src/EVM/ABI.hs +++ b/src/EVM/ABI.hs @@ -63,6 +63,7 @@ import Data.Binary.Put (Put, runPut, putWord8, putWord32be) import Data.Bits (shiftL, shiftR, (.&.)) import Data.ByteString (ByteString) +import Data.Char (isHexDigit) import Data.DoubleWord (Word256, Int256, signedWord) import Data.Functor (($>)) import Data.Text (Text, pack, unpack) @@ -70,18 +71,19 @@ import Data.Vector (Vector, toList) import Data.Word (Word32) import Data.List (intercalate) -import Data.SBV (SWord, fromBytes) +import Data.SBV (fromBytes) import GHC.Generics import Test.QuickCheck hiding ((.&.), label) import Text.ParserCombinators.ReadP import Control.Applicative -import qualified Data.ByteString as BS -import qualified Data.ByteString.Char8 as Char8 -import qualified Data.ByteString.Lazy as BSLazy -import qualified Data.Text as Text -import qualified Data.Vector as Vector +import qualified Data.ByteString as BS +import qualified Data.ByteString.Base16 as BS16 +import qualified Data.ByteString.Char8 as Char8 +import qualified Data.ByteString.Lazy as BSLazy +import qualified Data.Text as Text +import qualified Data.Vector as Vector import qualified Text.Megaparsec as P import qualified Text.Megaparsec.Char as P @@ -250,6 +252,7 @@ AbiTuple v -> putAbiSeq v +-- | Decode a sequence type (e.g. tuple / array). Will fail for non sequence types getAbiSeq :: Int -> [AbiType] -> Get (Vector AbiValue) getAbiSeq n ts = label "sequence" $ do hs <- label "sequence head" (getAbiHead n ts) @@ -491,9 +494,9 @@ return $ AbiBool (w /= 0)) <|> (do Boolz b <- readS_to_P reads return $ AbiBool b) -parseAbiValue (AbiBytesType n) = AbiBytes n <$> do ByteStringS bytes <- readS_to_P reads +parseAbiValue (AbiBytesType n) = AbiBytes n <$> do ByteStringS bytes <- bytesP return bytes -parseAbiValue AbiBytesDynamicType = AbiBytesDynamic <$> do ByteStringS bytes <- readS_to_P reads +parseAbiValue AbiBytesDynamicType = AbiBytesDynamic <$> do ByteStringS bytes <- bytesP return bytes parseAbiValue AbiStringType = AbiString <$> do Char8.pack <$> readS_to_P reads parseAbiValue (AbiArrayDynamicType typ) = @@ -510,7 +513,16 @@ skipSpaces return a) `sepBy` (char ',')) +bytesP :: ReadP ByteStringS +bytesP = do + string "0x" + hex <- munch isHexDigit + case BS16.decode (encodeUtf8 (Text.pack hex)) of + Right d -> pure $ ByteStringS d + Left d -> pfail + data AbiVals = NoVals | CAbi [AbiValue] | SAbi [SymWord] + deriving (Show) decodeBuffer :: [AbiType] -> Buffer -> AbiVals decodeBuffer tps (ConcreteBuffer b) diff --git a/src/EVM/Dapp.hs b/src/EVM/Dapp.hs --- a/src/EVM/Dapp.hs +++ b/src/EVM/Dapp.hs @@ -3,27 +3,28 @@ module EVM.Dapp where -import EVM (Trace, traceCodehash, traceOpIx, Env) +import EVM (Trace, traceContract, traceOpIx, ContractCode(..), Contract(..), codehash, contractcode) import EVM.ABI (Event, AbiType) import EVM.Debug (srcMapCodePos) -import EVM.Solidity (SolcContract, CodeType (..), SourceCache (..), SrcMap, Method) -import EVM.Solidity (contractName, methodInputs) -import EVM.Solidity (runtimeCodehash, creationCodehash, abiMap) -import EVM.Solidity (runtimeSrcmap, sourceAsts, creationSrcmap, eventMap) -import EVM.Solidity (methodSignature, astIdMap, astSrcMap) -import EVM.Types (W256, abiKeccak) +import EVM.Solidity +import EVM.Types (W256, abiKeccak, keccak, Buffer(..), Addr) +import EVM.Concrete +import Data.ByteString (ByteString) +import qualified Data.ByteString as BS import Data.Aeson (Value) import Data.Bifunctor (first) import Data.Text (Text, isPrefixOf, pack, unpack) import Data.Text.Encoding (encodeUtf8) -import Data.Map (Map, toList) +import Data.Map (Map, toList, elems) +import Data.List (sort) import Data.Maybe (isJust, fromJust) import Data.Word (Word32) import Control.Arrow ((>>>)) import Control.Lens +import Data.List (find) import qualified Data.Map as Map import qualified Data.Sequence as Seq import qualified Text.Regex.TDFA as Regex @@ -32,6 +33,7 @@ { _dappRoot :: FilePath , _dappSolcByName :: Map Text SolcContract , _dappSolcByHash :: Map W256 (CodeType, SolcContract) + , _dappSolcByCode :: [(Code, SolcContract)] -- for contracts with `immutable` vars. , _dappSources :: SourceCache , _dappUnitTests :: [(Text, [(Test, [AbiType])])] , _dappAbiMap :: Map Word32 Method @@ -40,12 +42,20 @@ , _dappAstSrcMap :: SrcMap -> Maybe Value } +-- | bytecode modulo immutables, to identify contracts +data Code = + Code { + raw :: ByteString, + immutableLocations :: [Reference] + } + deriving Show + data DappContext = DappContext { _contextInfo :: DappInfo - , _contextEnv :: Env + , _contextEnv :: Map Addr Contract } -data Test = ConcreteTest Text | SymbolicTest Text +data Test = ConcreteTest Text | SymbolicTest Text | InvariantTest Text makeLenses ''DappInfo makeLenses ''DappContext @@ -59,6 +69,7 @@ let solcs = Map.elems solcByName astIds = astIdMap $ snd <$> toList (view sourceAsts sources) + immutables = filter ((/=) mempty . _immutableReferences) solcs in DappInfo { _dappRoot = root @@ -72,7 +83,9 @@ mappend (f runtimeCodehash Runtime) (f creationCodehash Creation) - + -- contracts with immutable locations can't be id by hash + , _dappSolcByCode = + [(Code (_runtimeCode x) (concat $ elems $ _immutableReferences x), x) | x <- immutables] -- Sum up the ABI maps from all the contracts. , _dappAbiMap = mconcat (map (view abiMap) solcs) , _dappEventMap = mconcat (map (view eventMap) solcs) @@ -98,12 +111,13 @@ unitTestMarkerAbi = abiKeccak (encodeUtf8 "IS_TEST()") findAllUnitTests :: [SolcContract] -> [(Text, [(Test, [AbiType])])] -findAllUnitTests = findUnitTests ".*:.*\\.(test|prove).*" +findAllUnitTests = findUnitTests ".*:.*\\.(test|prove|invariant).*" mkTest :: Text -> Maybe Test mkTest sig | "test" `isPrefixOf` sig = Just (ConcreteTest sig) | "prove" `isPrefixOf` sig = Just (SymbolicTest sig) + | "invariant" `isPrefixOf` sig = Just (InvariantTest sig) | otherwise = Nothing regexMatches :: Text -> Text -> Bool @@ -144,19 +158,46 @@ extractSig :: Test -> Text extractSig (ConcreteTest sig) = sig extractSig (SymbolicTest sig) = sig +extractSig (InvariantTest sig) = sig traceSrcMap :: DappInfo -> Trace -> Maybe SrcMap traceSrcMap dapp trace = let - h = view traceCodehash trace + h = view traceContract trace i = view traceOpIx trace - in case preview (dappSolcByHash . ix h) dapp of - Nothing -> - Nothing - Just (Creation, solc) -> - i >>= \i' -> preview (creationSrcmap . ix i') solc - Just (Runtime, solc) -> - i >>= \i' -> preview (runtimeSrcmap . ix i') solc + in srcMap dapp h i + +srcMap :: DappInfo -> Contract -> Int -> Maybe SrcMap +srcMap dapp contr opIndex = do + sol <- findSrc contr dapp + case view contractcode contr of + (InitCode _) -> + preview (creationSrcmap . ix opIndex) sol + (RuntimeCode _) -> + preview (runtimeSrcmap . ix opIndex) sol + +findSrc :: Contract -> DappInfo -> Maybe SolcContract +findSrc c dapp = case preview (dappSolcByHash . ix (view codehash c)) dapp of + Just (_, v) -> Just v + Nothing -> lookupCode (view contractcode c) dapp + + +lookupCode :: ContractCode -> DappInfo -> Maybe SolcContract +lookupCode (InitCode (SymbolicBuffer _)) _ = Nothing -- TODO: srcmaps for symbolic bytecode +lookupCode (RuntimeCode (SymbolicBuffer _)) _ = Nothing -- TODO: srcmaps for symbolic bytecode +lookupCode (InitCode (ConcreteBuffer c)) a = + snd <$> preview (dappSolcByHash . ix (keccak (stripBytecodeMetadata c))) a +lookupCode (RuntimeCode (ConcreteBuffer c)) a = + case snd <$> preview (dappSolcByHash . ix (keccak (stripBytecodeMetadata c))) a of + Just x -> return x + Nothing -> snd <$> find (compareCode c . fst) (view dappSolcByCode a) + +compareCode :: ByteString -> Code -> Bool +compareCode raw (Code template locs) = + let holes' = sort [(start, len) | (Reference start len) <- locs] + insert at' len' bs = writeMemory (BS.replicate len' 0) (fromIntegral len') 0 (fromIntegral at') bs + refined = foldr (\(start, len) acc -> insert start len acc) raw holes' + in BS.length raw == BS.length template && template == refined showTraceLocation :: DappInfo -> Trace -> Either Text Text showTraceLocation dapp trace = diff --git a/src/EVM/Dev.hs b/src/EVM/Dev.hs --- a/src/EVM/Dev.hs +++ b/src/EVM/Dev.hs @@ -72,6 +72,8 @@ , vmModifier = loadFacts , dapp = emptyDapp , testParams = params + , maxDepth = Nothing + , allowFFI = False } readSolc path >>= \case @@ -129,6 +131,8 @@ , vmModifier = loadFacts , dapp = emptyDapp , testParams = params + , maxDepth = Nothing + , allowFFI = False } EVM.TTY.main testOpts root path @@ -247,6 +251,8 @@ State.state (runState m) >> interpretWithTrace fetcher (k ()) EVM.Stepper.Ask _ -> error "cannot make choices with this interpretWithTraceer" + EVM.Stepper.IOAct m -> + m >>= interpretWithTrace fetcher . k EVM.Stepper.EVM m -> do r <- State.state (runState m) interpretWithTrace fetcher (k r) diff --git a/src/EVM/Emacs.hs b/src/EVM/Emacs.hs --- a/src/EVM/Emacs.hs +++ b/src/EVM/Emacs.hs @@ -289,9 +289,6 @@ case currentSrcMap dapp vm of Nothing -> False Just sm -> - case view (dappSources . sourceFiles . at (srcMapFile sm)) dapp of - Nothing -> False - Just _ -> let (currentFileName, currentLineNumber) = fromJust (srcMapCodePos (view dappSources dapp) sm) @@ -323,7 +320,7 @@ fromMaybe noMap $ do dapp <- view uiVmDapp s sm <- currentSrcMap dapp (view uiVm s) - (fileName, _) <- view (dappSources . sourceFiles . at (srcMapFile sm)) dapp + let (fileName, _) = view (dappSources . sourceFiles) dapp !! srcMapFile sm pure . output $ L [ A "step" , L [A ("vm" :: Text), sexp (view uiVm s)] @@ -520,6 +517,8 @@ , vmModifier = id , dapp = emptyDapp , testParams = params + , maxDepth = Nothing + , allowFFI = False } initialStateForTest diff --git a/src/EVM/Exec.hs b/src/EVM/Exec.hs --- a/src/EVM/Exec.hs +++ b/src/EVM/Exec.hs @@ -41,6 +41,7 @@ , vmoptCreate = False , vmoptStorageModel = ConcreteS , vmoptTxAccessList = mempty + , vmoptAllowFFI = False }) & set (env . contracts . at ethrunAddress) (Just (initialContract (RuntimeCode mempty))) diff --git a/src/EVM/Facts.hs b/src/EVM/Facts.hs --- a/src/EVM/Facts.hs +++ b/src/EVM/Facts.hs @@ -108,12 +108,12 @@ dump x = BS16.encode x <> "\n" load x = case BS16.decode . mconcat . BS.split 10 $ x of - (y, "") -> Just y + Right y -> Just y _ -> Nothing contractFacts :: Addr -> Contract -> [Fact] contractFacts a x = case view bytecode x of - ConcreteBuffer b -> + ConcreteBuffer b -> storageFacts a x ++ [ BalanceFact a (view balance x) , NonceFact a (view nonce x) diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -6,6 +6,7 @@ import Prelude hiding (Word) +import EVM.ABI import EVM.Types (Addr, w256, W256, hexText, Word, Buffer(..)) import EVM.Symbolic (litWord) import EVM (IsUnique(..), EVM, Contract, Block, initialContract, nonce, balance, external) @@ -21,16 +22,19 @@ import Data.SBV.Trans hiding (Word) import Data.Aeson import Data.Aeson.Lens -import Data.ByteString (ByteString) +import qualified Data.ByteString as BS import Data.Text (Text, unpack, pack) + +import qualified Data.Vector as RegularVector import Network.Wreq import Network.Wreq.Session (Session) +import System.Process import qualified Network.Wreq.Session as Session -- | Abstract representation of an RPC fetch request data RpcQuery a where - QueryCode :: Addr -> RpcQuery ByteString + QueryCode :: Addr -> RpcQuery BS.ByteString QueryBlock :: RpcQuery Block QueryBalance :: Addr -> RpcQuery W256 QueryNonce :: Addr -> RpcQuery W256 @@ -164,6 +168,13 @@ oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher oracle smtstate info ensureConsistency q = do case q of + EVM.PleaseDoFFI vals continue -> case vals of + cmd : args -> do + (_, stdout', _) <- readProcessWithExitCode cmd args "" + pure . continue . encodeAbiValue $ + AbiTuple (RegularVector.fromList [ AbiBytesDynamic . hexText . pack $ stdout']) + _ -> error (show vals) + EVM.PleaseAskSMT branchcondition pathconditions continue -> case smtstate of Nothing -> return $ continue EVM.Unknown diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs --- a/src/EVM/Format.hs +++ b/src/EVM/Format.hs @@ -84,7 +84,7 @@ formatBytes bs -- opportunistically decodes recognisable strings showAbiValue (AbiAddress addr) = let dappinfo = view contextInfo ?context - contracts = view (contextEnv . EVM.contracts) ?context + contracts = view contextEnv ?context name = case (Map.lookup addr contracts) of Nothing -> "" Just contract -> @@ -175,7 +175,7 @@ showTrace :: DappInfo -> VM -> Trace -> Text showTrace dapp vm trace = - let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts } in let pos = case showTraceLocation dapp trace of @@ -247,10 +247,12 @@ "fetch contract " <> pack (show addr) <> pos PleaseFetchSlot addr slot _ -> "fetch storage slot " <> pack (show slot) <> " from " <> pack (show addr) <> pos - PleaseAskSMT _ _ _ -> + PleaseAskSMT {} -> "ask smt" <> pos - PleaseMakeUnique _ _ _ -> + PleaseMakeUnique {} -> "make unique value" <> pos + PleaseDoFFI cmd _ -> + "execute ffi " <> pack (show cmd) <> pos ErrorTrace e -> case e of @@ -420,7 +422,7 @@ showLeafInfo :: DappInfo -> BranchInfo -> [String] showLeafInfo srcInfo (BranchInfo vm _) = let - ?context = DappContext { _contextInfo = srcInfo, _contextEnv = vm ^?! EVM.env } + ?context = DappContext { _contextInfo = srcInfo, _contextEnv = vm ^?! EVM.env . EVM.contracts } in let self = view (EVM.state . EVM.contract) vm updates = case view (EVM.env . EVM.contracts) vm ^?! ix self . EVM.storage of diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs --- a/src/EVM/Solidity.hs +++ b/src/EVM/Solidity.hs @@ -3,6 +3,7 @@ {-# Language StrictData #-} {-# Language TemplateHaskell #-} {-# Language OverloadedStrings #-} +{-# Language QuasiQuotes #-} module EVM.Solidity ( solidity @@ -16,10 +17,13 @@ , CodeType (..) , Method (..) , SlotType (..) + , Reference(..) + , Mutability(..) , methodName , methodSignature , methodInputs , methodOutput + , methodMutability , abiMap , eventMap , storageLayout @@ -59,7 +63,9 @@ import Control.Applicative import Control.Monad import Control.Lens hiding (Indexed, (.=)) -import Data.Aeson (Value (..), ToJSON(..), (.=), object, encode) +import qualified Data.String.Here as Here +import Data.Aeson hiding (json) +import Data.Aeson.Types import Data.Aeson.Lens import Data.Scientific import Data.ByteString (ByteString) @@ -76,7 +82,6 @@ import Data.Text.Encoding (encodeUtf8, decodeUtf8) import Data.Text.IO (readFile, writeFile) import Data.Vector (Vector) -import Data.Word import GHC.Generics (Generic) import Prelude hiding (readFile, writeFile) import System.IO hiding (readFile, writeFile) @@ -136,6 +141,7 @@ , _constructorInputs :: [(Text, AbiType)] , _abiMap :: Map Word32 Method , _eventMap :: Map W256 Event + , _immutableReferences :: Map W256 [Reference] , _storageLayout :: Maybe (Map Text StorageItem) , _runtimeSrcmap :: Seq SrcMap , _creationSrcmap :: Seq SrcMap @@ -146,14 +152,34 @@ , _methodInputs :: [(Text, AbiType)] , _methodName :: Text , _methodSignature :: Text + , _methodMutability :: Mutability } deriving (Show, Eq, Ord, Generic) +data Mutability + = Pure -- ^ specified to not read blockchain state + | View -- ^ specified to not modify the blockchain state + | NonPayable -- ^ function does not accept Ether - the default + | Payable -- ^ function accepts Ether + deriving (Show, Eq, Ord, Generic) + data SourceCache = SourceCache - { _sourceFiles :: Map Int (Text, ByteString) - , _sourceLines :: Map Int (Vector ByteString) + { _sourceFiles :: [(Text, ByteString)] + , _sourceLines :: [(Vector ByteString)] , _sourceAsts :: Map Text Value } deriving (Show, Eq, Generic) +data Reference = Reference + { _refStart :: Int, + _refLength :: Int + } deriving (Show, Eq) + +instance FromJSON Reference where + parseJSON (Object v) = Reference + <$> v .: "start" + <*> v .: "length" + parseJSON invalid = + typeMismatch "Transaction" invalid + instance Semigroup SourceCache where _ <> _ = error "lol" @@ -241,13 +267,9 @@ f (fp, Nothing) = BS.readFile $ Text.unpack fp xs <- mapM f paths return $! SourceCache - { _sourceFiles = - Map.fromList (zip [0..] (zip (fst <$> paths) xs)) - , _sourceLines = - Map.fromList (zip [0 .. length paths - 1] - (map (Vector.fromList . BS.split 0xa) xs)) - , _sourceAsts = - asts + { _sourceFiles = zip (fst <$> paths) xs + , _sourceLines = map (Vector.fromList . BS.split 0xa) xs + , _sourceAsts = asts } lineSubrange :: @@ -299,6 +321,7 @@ Nothing -> readStdJSON json _ -> readCombinedJSON json +-- deprecate me soon readCombinedJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) readCombinedJSON json = do contracts <- f <$> (json ^? key "contracts" . _Object) @@ -324,7 +347,8 @@ _constructorInputs = mkConstructor abis, _abiMap = mkAbiMap abis, _eventMap = mkEventMap abis, - _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String + _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String, + _immutableReferences = mempty -- TODO: deprecate combined-json } readStdJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) @@ -340,13 +364,14 @@ f :: (AsValue s) => HMap.HashMap Text s -> (Map Text (SolcContract, (HMap.HashMap Text Text))) f x = Map.fromList . (concatMap g) . HMap.toList $ x g (s, x) = h s <$> HMap.toList (view _Object x) - h s (c, x) = + h :: Text -> (Text, Value) -> (Text, (SolcContract, HMap.HashMap Text Text)) + h s (c, x) = let evmstuff = x ^?! key "evm" runtime = evmstuff ^?! key "deployedBytecode" creation = evmstuff ^?! key "bytecode" - theRuntimeCode = toCode $ runtime ^?! key "object" . _String - theCreationCode = toCode $ creation ^?! key "object" . _String + theRuntimeCode = toCode $ fromMaybe "" $ runtime ^? key "object" . _String + theCreationCode = toCode $ fromMaybe "" $ creation ^? key "object" . _String srcContents :: Maybe (HMap.HashMap Text Text) srcContents = do metadata <- x ^? key "metadata" . _String srcs <- metadata ^? key "sources" . _Object @@ -364,7 +389,12 @@ _constructorInputs = mkConstructor abis, _abiMap = mkAbiMap abis, _eventMap = mkEventMap abis, - _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String + _storageLayout = mkStorageLayout $ x ^? key "storageLayout" . _String, + _immutableReferences = fromMaybe mempty $ + do x' <- runtime ^? key "immutableReferences" + case fromJSON x' of + Success a -> return a + _ -> Nothing }, fromMaybe mempty srcContents)) mkAbiMap :: [Value] -> Map Word32 Method @@ -379,6 +409,8 @@ (toList (abi ^?! key "inputs" . _Array)) , _methodOutput = map parseMethodInput (toList (abi ^?! key "outputs" . _Array)) + , _methodMutability = parseMutability + (abi ^?! key "stateMutability" . _String) }) in f <$> relevant @@ -417,7 +449,7 @@ mkStorageLayout (Just json) = do items <- json ^? key "storage" . _Array types <- json ^? key "types" - fmap Map.fromList $ (forM (Vector.toList items) $ \item -> + fmap Map.fromList (forM (Vector.toList items) $ \item -> do name <- item ^? key "label" . _String offset <- item ^? key "offset" . _Number >>= toBoundedInteger slot <- item ^? key "slot" . _String @@ -446,6 +478,13 @@ (x ^?! key "type" . _String) where parseComponents = fmap $ snd . parseMethodInput +parseMutability :: Text -> Mutability +parseMutability "view" = View +parseMutability "pure" = Pure +parseMutability "nonpayable" = NonPayable +parseMutability "payable" = Payable +parseMutability _ = error "unknown function mutability" + -- This actually can also parse a method output! :O parseMethodInput :: AsValue s => s -> (Text, AbiType) parseMethodInput x = @@ -454,16 +493,53 @@ ) toCode :: Text -> ByteString -toCode = fst . BS16.decode . encodeUtf8 +toCode t = case BS16.decode (encodeUtf8 t) of + Right d -> d + Left e -> error e solidity' :: Text -> IO (Text, Text) solidity' src = withSystemTempFile "hevm.sol" $ \path handle -> do hClose handle - writeFile path ("pragma solidity ^0.6.7;\n" <> src) + writeFile path ("//SPDX-License-Identifier: UNLICENSED\n" <> "pragma solidity ^0.8.6;\n" <> src) + writeFile (path <> ".json") + [Here.i| + { + "language": "Solidity", + "sources": { + ${path}: { + "urls": [ + ${path} + ] + } + }, + "settings": { + "outputSelection": { + "*": { + "*": [ + "metadata", + "evm.bytecode", + "evm.deployedBytecode", + "abi", + "storageLayout", + "evm.bytecode.sourceMap", + "evm.bytecode.linkReferences", + "evm.bytecode.generatedSources", + "evm.deployedBytecode.sourceMap", + "evm.deployedBytecode.linkReferences", + "evm.deployedBytecode.generatedSources" + ], + "": [ + "ast" + ] + } + } + } + } + |] x <- pack <$> readProcess "solc" - ["--combined-json=bin-runtime,bin,srcmap,srcmap-runtime,abi,ast,storage-layout", path] + ["--allow-paths", path, "--standard-json", (path <> ".json")] "" return (x, pack path) @@ -490,7 +566,7 @@ object ["content" .= src]] , "settings" .= object [ "outputSelection" .= - object ["*" .= + object ["*" .= object ["*" .= (toJSON ["metadata" :: String, "evm.bytecode", @@ -502,14 +578,15 @@ "evm.bytecode.generatedSources", "evm.deployedBytecode.sourceMap", "evm.deployedBytecode.linkReferences", - "evm.deployedBytecode.generatedSources" + "evm.deployedBytecode.generatedSources", + "evm.deployedBytecode.immutableReferences" ]), "" .= (toJSON ["ast" :: String]) ] ] ] ] - + stdjson :: Language -> Text -> Text stdjson lang src = decodeUtf8 $ toStrict $ encode $ StandardJSON lang src @@ -536,9 +613,9 @@ stripBytecodeMetadataSym b = let concretes :: [Maybe Word8] - concretes = (fmap fromSized) <$> unliteral <$> b + concretes = (fmap fromSized) . unliteral <$> b bzzrs :: [[Maybe Word8]] - bzzrs = fmap (Just) <$> BS.unpack <$> knownBzzrPrefixes + bzzrs = fmap (Just) . BS.unpack <$> knownBzzrPrefixes candidates = (flip Data.List.isInfixOf concretes) <$> bzzrs in case elemIndex True candidates of Nothing -> b diff --git a/src/EVM/Stepper.hs b/src/EVM/Stepper.hs --- a/src/EVM/Stepper.hs +++ b/src/EVM/Stepper.hs @@ -11,6 +11,7 @@ , wait , ask , evm + , evmIO , entering , enter , interpret @@ -57,6 +58,9 @@ -- | Embed a VM state transformation EVM :: EVM a -> Action a + -- | Perform an IO action + IOAct :: StateT VM IO a -> Action a -- they should all just be this? + -- | Type alias for an operational monad of @Action@ type Stepper a = Program Action a @@ -77,6 +81,9 @@ evm :: EVM a -> Stepper a evm = singleton . EVM +evmIO :: StateT VM IO a -> Stepper a +evmIO = singleton . IOAct + -- | Run the VM until final result, resolving all queries execFully :: Stepper (Either Error Buffer) execFully = @@ -136,6 +143,8 @@ State.state (runState m) >> interpret fetcher (k ()) Ask _ -> error "cannot make choices with this interpreter" + IOAct m -> + do m >>= interpret fetcher . k EVM m -> do r <- State.state (runState m) interpret fetcher (k r) diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -4,7 +4,6 @@ module EVM.SymExec where - import Prelude hiding (Word) import Control.Lens hiding (pre) @@ -26,12 +25,12 @@ import Data.SBV hiding (runSMT, newArray_, addAxiom, distinct, sWord8s, Word) import Data.Vector (toList, fromList) import Data.Tree +import Data.DoubleWord (Word256) import Data.ByteString (ByteString, pack) import qualified Data.ByteString.Lazy as Lazy import qualified Data.ByteString as BS import Data.Text (Text, splitOn, unpack) -import Control.Monad.State.Strict (runState, get, put, zipWithM) import qualified Control.Monad.State.Class as State import Control.Applicative @@ -141,6 +140,7 @@ , vmoptCreate = False , vmoptStorageModel = model , vmoptTxAccessList = mempty + , vmoptAllowFFI = False }) & set (env . contracts . at (createAddress ethrunAddress 1)) (Just (contractWithStore x initStore)) @@ -215,6 +215,8 @@ exec >>= interpret fetcher maxIter . k Stepper.Run -> run >>= interpret fetcher maxIter . k + Stepper.IOAct q -> + mapStateT io q >>= interpret fetcher maxIter . k Stepper.Ask (EVM.PleaseChoosePath _ continue) -> do vm <- get case maxIterationsReached vm maxIter of @@ -264,14 +266,45 @@ type Precondition = VM -> SBool type Postcondition = (VM, VM) -> SBool -checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM) -checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions) +checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM) +checkAssert errs c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just $ checkAssertions errs) -checkAssertions :: Postcondition -checkAssertions (_, out) = case view result out of +{- |Checks if an assertion violation has been encountered + + hevm recognises the following as an assertion violation: + + 1. the invalid opcode (0xfe) (solc < 0.8) + 2. a revert with a reason of the form `abi.encodeWithSelector("Panic(uint256)", code)`, where code is one of the following (solc >= 0.8): + - 0x00: Used for generic compiler inserted panics. + - 0x01: If you call assert with an argument that evaluates to false. + - 0x11: If an arithmetic operation results in underflow or overflow outside of an unchecked { ... } block. + - 0x12; If you divide or modulo by zero (e.g. 5 / 0 or 23 % 0). + - 0x21: If you convert a value that is too big or negative into an enum type. + - 0x22: If you access a storage byte array that is incorrectly encoded. + - 0x31: If you call .pop() on an empty array. + - 0x32: If you access an array, bytesN or an array slice at an out-of-bounds or negative index (i.e. x[i] where i >= x.length or i < 0). + - 0x41: If you allocate too much memory or create an array that is too large. + - 0x51: If you call a zero-initialized variable of internal function type. + + see: https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require +-} +checkAssertions :: [Word256] -> Postcondition +checkAssertions errs (_, out) = case view result out of Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> sFalse + Just (EVM.VMFailure (EVM.Revert msg)) -> if msg `elem` (fmap panicMsg errs) then sFalse else sTrue _ -> sTrue +-- |By default hevm checks for all assertions except those which result from arithmetic overflow +defaultPanicCodes :: [Word256] +defaultPanicCodes = [ 0x00, 0x01, 0x12, 0x21, 0x22, 0x31, 0x32, 0x41, 0x51 ] + +allPanicCodes :: [Word256] +allPanicCodes = [ 0x00, 0x01, 0x11, 0x12, 0x21, 0x22, 0x31, 0x32, 0x41, 0x51 ] + +-- |Produces the revert message for solc >=0.8 assertion violations +panicMsg :: Word256 -> ByteString +panicMsg err = (selector "Panic(uint256)") <> (encodeAbiValue $ AbiUInt 256 err) + verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM) verifyContract theCode signature' concreteArgs storagemodel pre maybepost = do preStateRaw <- abstractVM signature' concreteArgs theCode storagemodel @@ -344,7 +377,7 @@ -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states. equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM) equivalenceCheck bytecodeA bytecodeB maxiter signature' = do - let + let bytecodeA' = if BS.null bytecodeA then BS.pack [0] else bytecodeA bytecodeB' = if BS.null bytecodeB then BS.pack [0] else bytecodeB preStateA <- abstractVM signature' [] bytecodeA' SymbolicS diff --git a/src/EVM/TTY.hs b/src/EVM/TTY.hs --- a/src/EVM/TTY.hs +++ b/src/EVM/TTY.hs @@ -13,7 +13,7 @@ import EVM import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi) import EVM.SymExec (maxIterationsReached, symCalldata) -import EVM.Dapp (DappInfo, dappInfo, Test, extractSig, Test(..)) +import EVM.Dapp (DappInfo, dappInfo, Test, extractSig, Test(..), srcMap) import EVM.Dapp (dappUnitTests, unitTestMethods, dappSolcByName, dappSolcByHash, dappSources) import EVM.Dapp (dappAstSrcMap) import EVM.Debug @@ -24,6 +24,7 @@ import EVM.Solidity hiding (storageLayout) import EVM.Types hiding (padRight) import EVM.UnitTest +import EVM.RLP (RLP(..)) import EVM.StorageLayout import EVM.Stepper (Stepper) @@ -32,7 +33,7 @@ import EVM.Fetch (Fetcher) -import Control.Lens +import Control.Lens hiding (List) import Control.Monad.Trans.Reader import Control.Monad.State.Strict hiding (state) @@ -180,6 +181,10 @@ do m <- liftIO (?fetcher q) interpret mode (Stepper.evm m >>= k) + -- Stepper wants to make a query and wait for the results? + Stepper.IOAct q -> do + zoom uiVm (StateT (runStateT q)) >>= interpret mode . k + -- Stepper wants to modify the VM. Stepper.EVM m -> do vm <- use uiVm @@ -235,12 +240,14 @@ , smtTimeout = Nothing , smtState = Nothing , solver = Nothing + , maxDepth = Nothing , match = "" , fuzzRuns = 1 , replay = error "irrelevant" , vmModifier = id , testParams = error "irrelevant" , dapp = dappinfo + , allowFFI = False } ui0 = initUiVmState vm opts (void Stepper.execFully) @@ -274,6 +281,7 @@ isFuzzTest (SymbolicTest _, _) = False isFuzzTest (ConcreteTest _, []) = False isFuzzTest (ConcreteTest _, _) = True +isFuzzTest (InvariantTest _, _) = True main :: UnitTestOptions -> FilePath -> FilePath -> IO () main opts root jsonFilePath = @@ -631,7 +639,16 @@ void (runUnitTest opts theTestName args) SymbolicTest _ -> do Stepper.evm $ modify symbolify - void (execSymTest opts theTestName (SymbolicBuffer buf, w256lit len)) -- S (Literal $ num len) (literal $ num len))) + void (execSymTest opts theTestName (SymbolicBuffer buf, w256lit len)) + InvariantTest _ -> do + targets <- getTargetContracts opts + let randomRun = explorationStepper opts theTestName [] targets (List []) (fromMaybe 20 maxDepth) + void $ case replay of + Nothing -> randomRun + Just (sig, cd) -> + if theTestName == sig + then explorationStepper opts theTestName (decodeCalls cd) targets (List []) (length (decodeCalls cd)) + else randomRun pure $ initUiVmState vm0 opts script where Just (test, types) = find (\(test',_) -> extractSig test' == theTestName) $ unitTestMethods testContract @@ -851,15 +868,8 @@ currentSrcMap :: DappInfo -> VM -> Maybe SrcMap currentSrcMap dapp vm = do this <- currentContract vm - let - i = (view opIxMap this) SVec.! (view (state . pc) vm) - h = view codehash this - srcmap <- preview (dappSolcByHash . ix h) dapp - case srcmap of - (Creation, sol) -> - preview (creationSrcmap . ix i) sol - (Runtime, sol) -> - preview (runtimeSrcmap . ix i) sol + i <- (view opIxMap this) SVec.!? (view (state . pc) vm) + srcMap dapp this i drawStackPane :: UiVmState -> UiWidget drawStackPane ui = @@ -974,22 +984,22 @@ drawSolidityPane :: UiVmState -> UiWidget drawSolidityPane ui = let dapp' = dapp (view uiTestOpts ui) + dappSrcs = view dappSources dapp' vm = view uiVm ui in case currentSrcMap dapp' vm of Nothing -> padBottom Max (hBorderWithLabel (txt "")) Just sm -> - case view (dappSources . sourceLines . at (srcMapFile sm)) dapp' of - Nothing -> padBottom Max (hBorderWithLabel (txt "")) - Just rows -> let + rows = (_sourceLines dappSrcs) !! srcMapFile sm subrange = lineSubrange rows (srcMapOffset sm, srcMapLength sm) fileName :: Maybe Text fileName = preview (dappSources . sourceFiles . ix (srcMapFile sm) . _1) dapp' - lineNo = - (snd . fromJust $ + lineNo :: Maybe Int + lineNo = maybe Nothing (\a -> Just (a - 1)) + (snd <$> (srcMapCodePos (view dappSources dapp') - sm)) - 1 + sm)) in vBox [ hBorderWithLabel $ txt (fromMaybe "" fileName) @@ -1014,7 +1024,7 @@ , withHighlight False (txt z) ]) False - (listMoveTo lineNo + ((maybe id listMoveTo lineNo) (solidityList vm dapp')) ] diff --git a/src/EVM/Transaction.hs b/src/EVM/Transaction.hs --- a/src/EVM/Transaction.hs +++ b/src/EVM/Transaction.hs @@ -8,15 +8,13 @@ import EVM.Precompiled (execute) import EVM.RLP import EVM.Symbolic (forceLit) -import EVM.Types (keccak) import EVM.Types import Control.Lens import Data.Aeson (FromJSON (..)) import Data.ByteString (ByteString) -import Data.Map (Map, keys) -import Data.Set (fromList) +import Data.Map (Map) import Data.Maybe (fromMaybe, isNothing, isJust) import qualified Data.Aeson as JSON diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -9,7 +9,6 @@ import Prelude hiding (Word, LT, GT) -import Data.Aeson (FromJSONKey (..), FromJSONKeyFunction (..)) import Data.Aeson import Crypto.Hash import Data.SBV hiding (Word) @@ -17,7 +16,6 @@ import Data.Bifunctor (first) import Data.Char import Data.List (intercalate) -import Data.Bifunctor (bimap) import Data.ByteString (ByteString) import Data.ByteString.Base16 as BS16 import Data.ByteString.Builder (byteStringHex, toLazyByteString) @@ -131,11 +129,6 @@ fromBinary = Text.decodeUtf8 . toStrict . toLazyByteString . byteStringHex -instance Read ByteStringS where - readsPrec _ ('0':'x':x) = [bimap ByteStringS (Text.unpack . Text.decodeUtf8) bytes] - where bytes = BS16.decode (Text.encodeUtf8 (Text.pack x)) - readsPrec _ _ = [] - instance JSON.ToJSON ByteStringS where toJSON = JSON.String . Text.pack . show @@ -424,13 +417,13 @@ hexByteString :: String -> ByteString -> ByteString hexByteString msg bs = case BS16.decode bs of - (x, "") -> x + Right x -> x _ -> error ("invalid hex bytestring for " ++ msg) hexText :: Text -> ByteString hexText t = case BS16.decode (Text.encodeUtf8 (Text.drop 2 t)) of - (x, "") -> x + Right x -> x _ -> error ("invalid hex bytestring " ++ show t) readN :: Integral a => String -> a diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs --- a/src/EVM/UnitTest.hs +++ b/src/EVM/UnitTest.hs @@ -18,6 +18,7 @@ import EVM.SymExec import EVM.Types import EVM.Transaction (initTx) +import EVM.RLP import qualified EVM.Fetch import qualified EVM.FeeSchedule as FeeSchedule @@ -26,7 +27,7 @@ import qualified EVM.Stepper as Stepper import qualified Control.Monad.Operational as Operational -import Control.Lens hiding (Indexed) +import Control.Lens hiding (Indexed, elements, List) import Control.Monad.State.Strict hiding (state) import qualified Control.Monad.State.Strict as State @@ -44,7 +45,7 @@ import Data.Either (isRight, lefts) import Data.Foldable (toList) import Data.Map (Map) -import Data.Maybe (fromMaybe, catMaybes, fromJust, isJust, fromMaybe, mapMaybe) +import Data.Maybe (fromMaybe, catMaybes, fromJust, isJust, fromMaybe, mapMaybe, isNothing) import Data.Text (isPrefixOf, stripSuffix, intercalate, Text, pack, unpack) import Data.Text.Encoding (encodeUtf8) import System.Environment (lookupEnv) @@ -72,6 +73,7 @@ { oracle :: EVM.Query -> IO (EVM ()) , verbose :: Maybe Int , maxIter :: Maybe Integer + , maxDepth :: Maybe Int , smtTimeout :: Maybe Integer , smtState :: Maybe SBV.State , solver :: Maybe Text @@ -81,6 +83,7 @@ , vmModifier :: VM -> VM , dapp :: DappInfo , testParams :: TestVMParams + , allowFFI :: Bool } data TestVMParams = TestVMParams @@ -143,7 +146,7 @@ setUp = abiKeccak (encodeUtf8 "setUp()") when (isJust (Map.lookup setUp theAbi)) $ do - abiCall testParams "setUp()" emptyAbi + abiCall testParams (Left ("setUp()", emptyAbi)) popTrace pushTrace (EntryTrace "setUp()") @@ -158,21 +161,39 @@ -- will run the specified test method and return whether it succeeded. runUnitTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool runUnitTest a method args = do - x <- execTest a method args + x <- execTestStepper a method args checkFailures a method x -execTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool -execTest UnitTestOptions { .. } method args = do +execTestStepper :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool +execTestStepper UnitTestOptions { .. } methodName' method = do -- Set up the call to the test method Stepper.evm $ do - abiCall testParams method args - pushTrace (EntryTrace method) + abiCall testParams (Left (methodName', method)) + pushTrace (EntryTrace methodName') -- Try running the test method Stepper.execFully >>= \case -- If we failed, put the error in the trace. - Left e -> Stepper.evm (pushTrace (ErrorTrace e)) >> pure True + Left e -> Stepper.evm (pushTrace (ErrorTrace e) >> popTrace) >> pure True _ -> pure False +exploreStep :: UnitTestOptions -> ByteString -> Stepper Bool +exploreStep UnitTestOptions{..} bs = do + Stepper.evm $ do + cs <- use (env . contracts) + abiCall testParams (Right bs) + let (Method _ inputs sig _ _) = fromMaybe (error "unknown abi call") $ Map.lookup (num $ word $ BS.take 4 bs) (view dappAbiMap dapp) + types = snd <$> inputs + let ?context = DappContext dapp cs + this <- fromMaybe (error "unknown target") <$> (use (env . contracts . at (testAddress testParams))) + let name = maybe "" (contractNamePart . view contractName) $ lookupCode (view contractcode this) dapp + pushTrace (EntryTrace (name <> "." <> sig <> "(" <> intercalate "," ((pack . show) <$> types) <> ")" <> showCall types (ConcreteBuffer bs))) + -- Try running the test method + Stepper.execFully >>= \case + -- If we failed, put the error in the trace. + Left e -> Stepper.evm (pushTrace (ErrorTrace e) >> popTrace) >> pure True + _ -> pure False + + checkFailures :: UnitTestOptions -> ABIMethod -> Bool -> Stepper Bool checkFailures UnitTestOptions { .. } method bailed = do -- Decide whether the test is supposed to fail or succeed @@ -183,7 +204,7 @@ -- Ask whether any assertions failed Stepper.evm $ do popTrace - abiCall testParams "failed()" emptyAbi + abiCall testParams $ Left ("failed()", emptyAbi) res <- Stepper.execFully case res of Right (ConcreteBuffer r) -> @@ -202,22 +223,18 @@ -- | This is like an unresolved source mapping. data OpLocation = OpLocation - { srcCodehash :: !W256 - , srcOpIx :: !Int - } deriving (Eq, Ord, Show) + { srcContract :: Contract + , srcOpIx :: Int + } deriving (Show) +instance Eq OpLocation where + (==) (OpLocation a b) (OpLocation a' b') = b == b' && view contractcode a == view contractcode a' + +instance Ord OpLocation where + compare (OpLocation a b) (OpLocation a' b') = compare (view contractcode a, b) (view contractcode a', b') + srcMapForOpLocation :: DappInfo -> OpLocation -> Maybe SrcMap -srcMapForOpLocation dapp (OpLocation hash opIx) = - case preview (dappSolcByHash . ix hash) dapp of - Nothing -> Nothing - Just (codeType, sol) -> - let - vec = - case codeType of - Runtime -> view runtimeSrcmap sol - Creation -> view creationSrcmap sol - in - preview (ix opIx) vec +srcMapForOpLocation dapp (OpLocation contr opIx) = srcMap dapp contr opIx type CoverageState = (VM, MultiSet OpLocation) @@ -228,7 +245,7 @@ error "internal error: why no contract?" Just c -> OpLocation - (view codehash c) + c (fromMaybe (error "internal error: op ix") (vmOpIx vm)) execWithCoverage :: StateT CoverageState IO VMResult @@ -274,6 +291,8 @@ zoom _1 (State.state (runState m)) >> interpretWithCoverage opts (k ()) Stepper.Ask _ -> error "cannot make choice in this interpreter" + Stepper.IOAct q -> + zoom _1 (StateT (runStateT q)) >>= interpretWithCoverage opts . k Stepper.EVM m -> zoom _1 (State.state (runState m)) >>= interpretWithCoverage opts . k @@ -301,15 +320,12 @@ srcMapCov :: MultiSet (Text, Int) srcMapCov = MultiSet.mapMaybe (srcMapCodePos sources) cov - -- linesByName :: Map Text (Vector ByteString) + linesByName :: Map Text (Vector ByteString) linesByName = - ( Map.fromList - . map - (\(k, v) -> - (fst (fromJust (Map.lookup k (view sourceFiles sources))), v)) - . Map.toList - $ view sourceLines sources - ) + Map.fromList $ zipWith + (\(name, _) lines' -> (name, lines')) + (view sourceFiles sources) + (view sourceLines sources) f :: Text -> Vector ByteString -> Vector (Int, ByteString) f name = @@ -435,15 +451,143 @@ decodeAbiValue (AbiTupleType (Vector.fromList types)) callData else fuzzRun opts vm testName types runTest opts vm (SymbolicTest testName, types) = symRun opts vm testName types +runTest opts@UnitTestOptions{..} vm (InvariantTest testName, []) = liftIO $ case replay of + Nothing -> exploreRun opts vm testName [] + Just (sig, cds) -> + if sig == testName + then exploreRun opts vm testName (decodeCalls cds) + else exploreRun opts vm testName [] +runTest _ _ (InvariantTest _, types) = error $ "invariant testing with arguments: " <> show types <> " is not implemented (yet!)" +type ExploreTx = (Addr, Addr, ByteString, W256) + +decodeCalls :: BSLazy.ByteString -> [ExploreTx] +decodeCalls b = fromMaybe (error "could not decode replay data") $ do + List v <- rlpdecode $ BSLazy.toStrict b + return $ flip fmap v $ \(List [BS caller', BS target, BS cd, BS ts]) -> (num (word caller'), num (word target), cd, word ts) + + +explorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> RLP -> Int -> Stepper (Bool, RLP) +explorationStepper _ _ _ _ history 0 = return (True, history) +explorationStepper opts@UnitTestOptions{..} testName replayData targets (List history) i = do + (caller', target, cd, timestamp') <- + case preview (ix (i - 1)) replayData of + Just v -> return v + Nothing -> + Stepper.evmIO $ do + vm <- get + let cs = view (env . contracts) vm + noCode c = case view contractcode c of + RuntimeCode c' -> len c' == 0 + _ -> False + mutable m = view methodMutability m `elem` [NonPayable, Payable] + knownAbis :: Map Addr SolcContract + knownAbis = + -- exclude contracts without code + Map.filter (not . BS.null . view runtimeCode) $ + -- exclude contracts without state changing functions + Map.filter (not . null . Map.filter mutable . view abiMap) $ + -- exclude testing abis + Map.filter (isNothing . preview (abiMap . ix unitTestMarkerAbi)) $ + -- pick all contracts with known compiler artifacts + fmap fromJust (Map.filter isJust $ Map.fromList [(addr, lookupCode (view contractcode c) dapp) | (addr, c) <- Map.toList cs]) + selected = [(addr, + fromMaybe (error ("no src found for: " <> show addr)) $ lookupCode (view contractcode (fromMaybe (error $ "contract not found: " <> show addr) $ Map.lookup addr cs)) dapp) + | addr <- targets] + -- go to IO and generate a random valid call to any known contract + liftIO $ do + -- select random contract + (target, solcInfo) <- generate $ elements (if null targets then Map.toList knownAbis else selected) + -- choose a random mutable method + (_, (Method _ inputs sig _ _)) <- generate (elements $ Map.toList $ Map.filter mutable $ view abiMap solcInfo) + let types = snd <$> inputs + -- set the caller to a random address with 90% probability, 10% known EOA address + let knownEOAs = Map.keys $ Map.filter noCode cs + AbiAddress caller' <- + if null knownEOAs + then generate $ genAbiValue AbiAddressType + else generate $ frequency + [ (90, genAbiValue AbiAddressType) + , (10, AbiAddress <$> elements knownEOAs) + ] + -- make a call with random valid data to the function + args <- generate $ genAbiValue (AbiTupleType $ Vector.fromList types) + let cd = abiMethod (sig <> "(" <> intercalate "," ((pack . show) <$> types) <> ")") args + -- increment timestamp with random amount + timepassed <- num <$> generate (arbitrarySizedNatural :: Gen Word32) + let ts = fromMaybe (error "symbolic timestamp not supported here") $ maybeLitWord $ view (block . timestamp) vm + return (caller', target, cd, num ts + timepassed) + let opts' = opts { testParams = testParams {testAddress = target, testCaller = caller', testTimestamp = timestamp'}} + thisCallRLP = List [BS $ word160Bytes caller', BS $ word160Bytes target, BS cd, BS $ word256Bytes timestamp'] + -- set the timestamp + Stepper.evm $ assign (block . timestamp) (w256lit timestamp') + -- perform the call + bailed <- exploreStep opts' cd + Stepper.evm popTrace + let newHistory = if bailed then List history else List (thisCallRLP:history) + opts'' = opts {testParams = testParams {testTimestamp = timestamp'}} + carryOn = explorationStepper opts'' testName replayData targets newHistory (i - 1) + -- if we didn't revert, run the test function + if bailed + then carryOn + else + do x <- runUnitTest opts'' testName emptyAbi + if x + then carryOn + else pure (False, List (thisCallRLP:history)) +explorationStepper _ _ _ _ _ _ = error "malformed rlp" + +getTargetContracts :: UnitTestOptions -> Stepper [Addr] +getTargetContracts UnitTestOptions{..} = do + vm <- Stepper.evm $ get + let Just contract = currentContract vm + theAbi = view abiMap $ fromJust $ lookupCode (view contractcode contract) dapp + setUp = abiKeccak (encodeUtf8 "targetContracts()") + case Map.lookup setUp theAbi of + Nothing -> return [] + Just _ -> do + Stepper.evm $ abiCall testParams (Left ("targetContracts()", emptyAbi)) + res <- Stepper.execFully + case res of + Right (ConcreteBuffer r) -> + let AbiTuple vs = decodeAbiValue (AbiTupleType (Vector.fromList [AbiArrayDynamicType AbiAddressType])) (BSLazy.fromStrict r) + [AbiArrayDynamic AbiAddressType targets] = Vector.toList vs + in return $ fmap (\(AbiAddress a) -> a) (Vector.toList targets) + _ -> error "internal error: unexpected failure code" + +exploreRun :: UnitTestOptions -> VM -> ABIMethod -> [ExploreTx] -> IO (Text, Either Text Text, VM) +exploreRun opts@UnitTestOptions{..} initialVm testName replayTxs = do + (targets, _) <- runStateT (EVM.Stepper.interpret oracle (getTargetContracts opts)) initialVm + let depth = fromMaybe 20 maxDepth + ((x, counterex), vm') <- + if null replayTxs + then + foldM (\a@((success, _), _) _ -> + if success + then runStateT (EVM.Stepper.interpret oracle (explorationStepper opts testName [] targets (List []) depth)) initialVm + else pure a) + ((True, (List [])), initialVm) -- no canonical "post vm" + [0..fuzzRuns] + else runStateT (EVM.Stepper.interpret oracle (explorationStepper opts testName replayTxs targets (List []) (length replayTxs))) initialVm + if x + then return ("\x1b[32m[PASS]\x1b[0m " <> testName <> " (runs: " <> (pack $ show fuzzRuns) <>", depth: " <> pack (show depth) <> ")", + Right (passOutput vm' opts testName), vm') -- no canonical "post vm" + else let replayText = if null replayTxs + then "\nReplay data: '(" <> pack (show testName) <> ", " <> pack (show (show (ByteStringS $ rlpencode counterex))) <> ")'" + else " (replayed)" + in return ("\x1b[31m[FAIL]\x1b[0m " <> testName <> replayText, Left (failOutput vm' opts testName), vm') + +execTest :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Bool, VM) +execTest opts@UnitTestOptions{..} vm testName args = + runStateT + (EVM.Stepper.interpret oracle (execTestStepper opts testName args)) + vm + -- | Define the thread spawner for normal test cases runOne :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Text, Either Text Text, VM) runOne opts@UnitTestOptions{..} vm testName args = do let argInfo = pack (if args == emptyAbi then "" else " with arguments: " <> show args) - (bailed, vm') <- - runStateT - (EVM.Stepper.interpret oracle (execTest opts testName args)) - vm + (bailed, vm') <- execTest opts vm testName args (success, vm'') <- runStateT (EVM.Stepper.interpret oracle (checkFailures opts testName bailed)) vm' @@ -538,7 +682,7 @@ -- report a failure unless the test is supposed to fail. \(bailed, vm') -> do - let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts } SBV.resetAssertions constrain $ sAnd (fst <$> view EVM.constraints vm') unless bailed $ @@ -580,7 +724,7 @@ showRes vm = let Just res = view result vm in case res of VMFailure _ -> - let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts} in prettyvmresult res VMSuccess _ -> if "proveFail" `isPrefixOf` testName then "Successful execution" @@ -627,7 +771,7 @@ -- Ask whether any assertions failed Stepper.evm $ do popTrace - abiCall testParams "failed()" emptyAbi + abiCall testParams (Left ("failed()", emptyAbi)) Stepper.runFully indentLines :: Int -> Text -> Text @@ -637,7 +781,7 @@ passOutput :: VM -> UnitTestOptions -> Text -> Text passOutput vm UnitTestOptions { .. } testName = - let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts } in let v = fromMaybe 0 verbose in if (v > 1) then mconcat @@ -652,7 +796,7 @@ failOutput :: VM -> UnitTestOptions -> Text -> Text failOutput vm UnitTestOptions { .. } testName = - let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts} in mconcat [ "Failure: " , fromMaybe "" (stripSuffix "()" testName) @@ -736,9 +880,11 @@ word32Bytes :: Word32 -> ByteString word32Bytes x = BS.pack [byteAt x (3 - i) | i <- [0..3]] -abiCall :: TestVMParams -> Text -> AbiValue -> EVM () -abiCall params sig args = - let cd = abiMethod sig args +abiCall :: TestVMParams -> Either (Text, AbiValue) ByteString -> EVM () +abiCall params args = + let cd = case args of + Left (sig, args') -> abiMethod sig args' + Right b -> b l = num . BS.length $ cd in makeTxCall params (ConcreteBuffer cd, litWord l) @@ -781,6 +927,7 @@ , vmoptCreate = True , vmoptStorageModel = ConcreteS -- TODO: support RPC , vmoptTxAccessList = mempty -- TODO: support unit test access lists??? + , vmoptAllowFFI = allowFFI } creator = initialContract (RuntimeCode mempty) diff --git a/src/EVM/VMTest.hs b/src/EVM/VMTest.hs --- a/src/EVM/VMTest.hs +++ b/src/EVM/VMTest.hs @@ -285,6 +285,7 @@ , vmoptCreate = isCreate , vmoptStorageModel = EVM.ConcreteS , vmoptTxAccessList = txAccessMap tx + , vmoptAllowFFI = False }) checkState postState diff --git a/test/test.hs b/test/test.hs --- a/test/test.hs +++ b/test/test.hs @@ -3,7 +3,6 @@ {-# Language ScopedTypeVariables #-} {-# Language LambdaCase #-} {-# Language QuasiQuotes #-} -{-# Language TypeSynonymInstances #-} {-# Language FlexibleInstances #-} {-# Language GeneralizedNewtypeDeriving #-} {-# Language DataKinds #-} @@ -18,7 +17,7 @@ import qualified Data.Text as Text import qualified Data.ByteString as BS -import qualified Data.ByteString.Lazy as BS (fromStrict, toStrict) +import qualified Data.ByteString.Lazy as BS (fromStrict) import qualified Data.ByteString.Base16 as Hex import Test.Tasty import Test.Tasty.QuickCheck @@ -67,7 +66,7 @@ , testCase "Arithmetic" $ do SolidityCall "x = a + 1;" [AbiUInt 256 1] ===> AbiUInt 256 2 - SolidityCall "x = a - 1;" + SolidityCall "unchecked { x = a - 1; }" [AbiUInt 8 0] ===> AbiUInt 8 255 , testCase "keccak256()" $ @@ -252,7 +251,7 @@ } |] bs <- runSMTWith cvc4 $ query $ do - (Right _, vm) <- checkAssert factor (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] + (Right _, vm) <- checkAssert defaultPanicCodes factor (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected" @@ -267,8 +266,10 @@ contract A { uint x; function f(uint256 y) public { - x += y; - x += y; + unchecked { + x += y; + x += y; + } } } |] @@ -320,7 +321,7 @@ (Right _, vm) <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post) case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs - ConcreteBuffer bs -> error "unexpected" + ConcreteBuffer _ -> error "unexpected" let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs assertEqual "Catch storage collisions" x y @@ -344,7 +345,7 @@ } } |] - (Left res, _) <- runSMTWith z3 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) [] + (Left res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "Deposit contract loop (cvc4)" $ do @@ -366,7 +367,7 @@ } } |] - (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) [] + (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "Deposit contract loop (error version)" $ do @@ -389,7 +390,7 @@ } |] bs <- runSMT $ query $ do - (Right _, vm) <- checkAssert c (Just ("deposit(uint8)", [AbiUIntType 8])) [] + (Right _, vm) <- checkAssert allPanicCodes c (Just ("deposit(uint8)", [AbiUIntType 8])) [] case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected" @@ -408,7 +409,7 @@ |] (Left res, _) <- runSMTWith z3 $ do setTimeOut 5000 - query $ checkAssert c Nothing [] + query $ checkAssert defaultPanicCodes c Nothing [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , @@ -421,7 +422,7 @@ } } |] - (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] + (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "injectivity of keccak (32 bytes)" $ do @@ -433,7 +434,7 @@ } } |] - (Left res, _) <- runSMTWith z3 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] + (Left res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , @@ -447,7 +448,7 @@ } |] bs <- runSMTWith z3 $ query $ do - (Right _, vm) <- checkAssert c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) [] + (Right _, vm) <- checkAssert defaultPanicCodes c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) [] case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected" @@ -479,7 +480,7 @@ |] Left res <- runSMTWith z3 $ do setTimeOut 5000 - query $ fst <$> checkAssert c Nothing [] + query $ fst <$> checkAssert defaultPanicCodes c Nothing [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , @@ -496,8 +497,8 @@ } |] -- should find a counterexample - Right _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] - putStrLn $ "found counterexample:" + Right _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] + putStrLn "found counterexample:" , @@ -520,7 +521,7 @@ aAddr = Addr 0x35D1b3F3D7966A1DFe207aa4514C12a259A0492B Just c <- solcRuntime "C" code Just a <- solcRuntime "A" code - Right cex <- runSMT $ query $ do + Right _ <- runSMT $ query $ do vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS store <- freshArray (show aAddr) Nothing let vm = vm0 @@ -528,8 +529,8 @@ & over (env . contracts) (Map.insert aAddr (initialContract (RuntimeCode $ ConcreteBuffer a) & set EVM.storage (EVM.Symbolic [] store))) - verify vm Nothing Nothing (Just checkAssertions) - putStrLn $ "found counterexample:" + verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes) + putStrLn "found counterexample:" , testCase "calling unique contracts (read from storage)" $ do let code = @@ -549,11 +550,11 @@ } |] Just c <- solcRuntime "C" code - Right cex <- runSMT $ query $ do + Right _ <- runSMT $ query $ do vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS let vm = vm0 & set (state . callvalue) 0 - verify vm Nothing Nothing (Just checkAssertions) - putStrLn $ "found counterexample:" + verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes) + putStrLn "found counterexample:" , testCase "keccak concrete and sym agree" $ do @@ -571,15 +572,15 @@ Left _ <- runSMT $ query $ do vm0 <- abstractVM (Just ("kecc(uint256)", [AbiUIntType 256])) [] c SymbolicS let vm = vm0 & set (state . callvalue) 0 - verify vm Nothing Nothing (Just checkAssertions) - putStrLn $ "found counterexample:" + verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes) + putStrLn "found counterexample:" , testCase "safemath distributivity (yul)" $ do Left _ <- runSMTWith cvc4 $ query $ do let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b" vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] yulsafeDistributivity SymbolicS - verify vm Nothing Nothing (Just checkAssertions) - putStrLn $ "Proven" + verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes) + putStrLn "Proven" , testCase "safemath distributivity (sol)" $ do let code = @@ -590,10 +591,14 @@ } function add(uint x, uint y) internal pure returns (uint z) { - require((z = x + y) >= x, "ds-math-add-overflow"); + unchecked { + require((z = x + y) >= x, "ds-math-add-overflow"); + } } function mul(uint x, uint y) internal pure returns (uint z) { - require(y == 0 || (z = x * y) / y == x, "ds-math-mul-overflow"); + unchecked { + require(y == 0 || (z = x * y) / y == x, "ds-math-mul-overflow"); + } } } |] @@ -601,8 +606,8 @@ Left _ <- runSMTWith z3 $ query $ do vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] c SymbolicS - verify vm Nothing Nothing (Just checkAssertions) - putStrLn $ "Proven" + verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes) + putStrLn "Proven" ] , testGroup "Equivalence checking" @@ -620,7 +625,7 @@ let aPrgm = hex "602060006000376000805160008114601d5760018114602457fe6029565b8191506029565b600191505b50600160015250" bPrgm = hex "6020600060003760005160008114601c5760028114602057fe6021565b6021565b5b506001600152" runSMTWith z3 $ query $ do - Right counterexample <- equivalenceCheck aPrgm bPrgm Nothing Nothing + Right _ <- equivalenceCheck aPrgm bPrgm Nothing Nothing return () ] @@ -652,8 +657,8 @@ hex :: ByteString -> ByteString hex s = case Hex.decode s of - (x, "") -> x - _ -> error "internal error" + Right x -> x + Left e -> error e singleContract :: Text -> Text -> IO (Maybe ByteString) singleContract x s = @@ -753,4 +758,4 @@ b <- f a b' <- f a' return (b, b') - +