diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,71 @@ # hevm changelog +## 0.44.1 - 2020-02-02 + +### Changed + +- hevm cheatcodes now accept symbolic arguments, allowing e.g. symbolic jumps in time in unit tests + +## 0.44.0 - 2020-01-26 + +### Added + +- `hevm` now accepts solidity json output built via `--standard-json` as + well as `--combined-json`. +- addresses in the trace output are prefixed with `ContractName@0x...` + if there is a corresponding contract and `@0x...` otherwise. +- More efficient arithmetic overflow checks by translating queries to a more [intelligent form](www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf). + +### Fixed + +- Symbolic execution now generates calldata arguments restricted to the proper ranges, +following the semantics of fuzzing. +- If the `--address` flag is present in `hevm exec` or `hevm symbolic`, + it overrides the contract address at which a contract will be created. +- Address pretty printing +- Updated sbv to `8.9.5` to fix "non-const in array declaration" cvc4 issue with ds-test. + +### Changed + +- Use cvc4 as default smt solver + +## 0.43.2 - 2020-12-10 + +### Changed + +- The default smttimeout has been increased from 20s to 30s + +## 0.43.1 - 2020-12-10 + +### Changed + +- Counterexamples from symbolic tests now show clearer failure reasons + +### Fixed + +- Symbolic tests now work with RPC +- Branch selection is working again in the interactive debugger + +## 0.43.0 - 2020-11-29 + +### Added + +- A `--show-tree` option to `hevm symbolic` which prints the execution tree explored. +- Some symbolic terms are displayed with richer semantic information, instead of the black box ``. +- `hevm dapp-test` now supports symbolic execution of test methods that are prefixed with `prove` or `proveFail` +- The `hevm interactive` alias has been removed, as it is equivalent to `hevm dapp-test --debug` +- `hevm dapp-test --match` now matches on contract name and file path, as well as test name +- Step through the callstack in debug mode using the arrow keys + +### Changed + +- `dapp-test` trace output now detects ds-note events and shows `LogNote` +- create addresses are shown with `@
` in the trace +- `DSTest.setUp()` is only run if it exists, rather than failing +- support new ds-test `log_named_x(string, x)` (previously bytes32 keys) +- return arguments are fully displayed in the trace (previously only a single word) +- return/revert trace will now show the correct source position + ## 0.42.0 - 2020-10-31 ### Changed 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 @@ -6,7 +6,6 @@ {-# Language DeriveGeneric #-} {-# Language GADTs #-} {-# Language LambdaCase #-} -{-# Language NumDecimals #-} {-# Language OverloadedStrings #-} {-# Language TypeOperators #-} {-# Language RecordWildCards #-} @@ -15,15 +14,15 @@ import EVM (StorageModel(..)) import qualified EVM -import EVM.Concrete (createAddress, w256, wordValue) -import EVM.Symbolic (forceLitBytes, litAddr, w256lit, sw256, SymWord(..), len, forceLit, litWord) +import EVM.Concrete (createAddress, wordValue) +import EVM.Symbolic (litWord, forceLitBytes, litAddr, len, forceLit) import qualified EVM.FeeSchedule as FeeSchedule import qualified EVM.Fetch import qualified EVM.Flatten import qualified EVM.Stepper import qualified EVM.TTY import qualified EVM.Emacs -import EVM.Dev (concatMapM) +import EVM.Dev (interpretWithTrace) #if MIN_VERSION_aeson(1, 0, 0) import qualified EVM.VMTest as VMTest @@ -37,8 +36,8 @@ import EVM.UnitTest (UnitTestOptions, coverageReport, coverageForUnitTestContract) import EVM.UnitTest (runUnitTestContract) import EVM.UnitTest (getParametersFromEnvironmentVariables, testNumber) -import EVM.Dapp (findUnitTests, dappInfo, DappInfo) -import EVM.Format (showTraceTree) +import EVM.Dapp (findUnitTests, dappInfo, DappInfo, emptyDapp) +import EVM.Format (showTraceTree, showTree', renderTree, showBranchInfoWithAbi, showLeafInfo) import EVM.RLP (rlpdecode) import qualified EVM.Patricia as Patricia import Data.Map (Map) @@ -47,12 +46,14 @@ import qualified EVM.Facts.Git as Git import qualified EVM.UnitTest +import GHC.IO.Encoding import Control.Concurrent.Async (async, waitCatch) -import Control.Lens hiding (pre) +import Control.Lens hiding (pre, passing) import Control.Monad (void, when, forM_, unless) -import Control.Monad.State.Strict (execStateT) +import Control.Monad.State.Strict (execStateT, liftIO) import Data.ByteString (ByteString) import Data.List (intercalate, isSuffixOf) +import Data.Tree import Data.Text (Text, unpack, pack) import Data.Text.Encoding (encodeUtf8) import Data.Text.IO (hPutStr) @@ -60,9 +61,9 @@ import Data.Version (showVersion) import Data.SBV hiding (Word, solver, verbose, name) import Data.SBV.Control hiding (Version, timeout, create) -import System.IO (hFlush, hPrint, stdout, stderr) +import System.IO (hFlush, stdout, stderr, utf8) import System.Directory (withCurrentDirectory, listDirectory) -import System.Exit (die, exitFailure, exitWith, ExitCode(..)) +import System.Exit (exitFailure, exitWith, ExitCode(..)) import System.Environment (setEnv) import System.Process (callProcess) import qualified Data.Aeson as JSON @@ -72,15 +73,14 @@ import qualified Data.Vector as V import qualified Data.ByteString.Lazy as Lazy +import qualified Data.SBV as SBV import qualified Data.ByteString as ByteString import qualified Data.ByteString.Char8 as Char8 import qualified Data.ByteString.Lazy as LazyByteString import qualified Data.Map as Map -import qualified Data.Sequence as Seq import qualified System.Timeout as Timeout import qualified Paths_hevm as Paths -import qualified Text.Regex.TDFA as Regex import Options.Generic as Options @@ -120,18 +120,21 @@ , arg :: w ::: [String] "Values to encode" , debug :: w ::: Bool "Run interactively" , getModels :: w ::: Bool "Print example testcase for each execution path" - , smttimeout :: w ::: Maybe Integer "Timeout given to SMT solver in milliseconds (default: 20000)" + , showTree :: w ::: Bool "Print branches explored in tree view" + , smttimeout :: w ::: Maybe Integer "Timeout given to SMT solver in milliseconds (default: 30000)" , 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" } | Equivalence -- prove equivalence between two programs { codeA :: w ::: ByteString "Bytecode of the first program" , codeB :: w ::: ByteString "Bytecode of the second program" , sig :: w ::: Maybe Text "Signature of types to decode / encode" - , smttimeout :: w ::: Maybe Integer "Timeout given to SMT solver in milliseconds (default: 20000)" + , smttimeout :: w ::: Maybe Integer "Timeout given to SMT solver in milliseconds (default: 30000)" , 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" , smtoutput :: w ::: Bool "Print verbose smt output" + , smtdebug :: w ::: Bool "Print smt queries sent to the solver" } | Exec -- Execute a given program with specified env & calldata { code :: w ::: Maybe ByteString "Program bytecode" @@ -152,6 +155,7 @@ , difficulty :: w ::: Maybe W256 "Block: difficulty" , chainid :: w ::: Maybe W256 "Env: chainId" , debug :: w ::: Bool "Run interactively" + , jsontrace :: w ::: Bool "Print json trace output at every step" , trace :: w ::: Bool "Dump trace" , state :: w ::: Maybe String "Path to state repository" , cache :: w ::: Maybe String "Path to rpc cache repository" @@ -161,32 +165,30 @@ , dappRoot :: w ::: Maybe String "Path to dapp project root directory (default: . )" } | DappTest -- Run DSTest unit tests - { jsonFile :: w ::: Maybe String "Filename or path to dapp build output (default: out/*.solc.json)" - , dappRoot :: w ::: Maybe String "Path to dapp project root directory (default: . )" - , debug :: w ::: Bool "Run interactively" - , fuzzRuns :: w ::: Maybe Int "Number of times to run fuzz tests" - , 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" - , coverage :: w ::: Bool "Coverage analysis" - , state :: w ::: Maybe String "Path to state repository" - , cache :: w ::: Maybe String "Path to rpc cache repository" - , match :: w ::: Maybe String "Test case filter - only run methods matching regex" - } - | Interactive -- Browse & run unit tests interactively - { jsonFile :: w ::: Maybe String "Filename or path to dapp build output (default: out/*.solc.json)" - , dappRoot :: w ::: Maybe String "Path to dapp project root directory (default: . )" - , rpc :: w ::: Maybe URL "Fetch state from a remote node" - , state :: w ::: Maybe String "Path to state repository" - , cache :: w ::: Maybe String "Path to rpc cache repository" - , replay :: w ::: Maybe (Text, ByteString) "Custom fuzz case to run/debug" + { jsonFile :: w ::: Maybe String "Filename or path to dapp build output (default: out/*.solc.json)" + , dappRoot :: w ::: Maybe String "Path to dapp project root directory (default: . )" + , 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" + , 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" + , coverage :: w ::: Bool "Coverage analysis" + , state :: w ::: Maybe String "Path to state repository" + , cache :: w ::: Maybe String "Path to rpc cache repository" + , match :: w ::: Maybe String "Test case filter - only run methods matching regex" + , smttimeout :: w ::: Maybe Integer "Timeout given to SMT solver in milliseconds (default: 30000)" + , 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" } | BcTest -- Run an Ethereum Blockhain/GeneralState test - { file :: w ::: String "Path to .json test file" - , test :: w ::: [String] "Test case filter - only run specified test method(s)" - , debug :: w ::: Bool "Run interactively" - , diff :: w ::: Bool "Print expected vs. actual state on failure" - , timeout :: w ::: Maybe Int "Execution timeout (default: 10 sec.)" + { file :: w ::: String "Path to .json test file" + , test :: w ::: [String] "Test case filter - only run specified test method(s)" + , debug :: w ::: Bool "Run interactively" + , jsontrace :: w ::: Bool "Print json trace output at every step" + , diff :: w ::: Bool "Print expected vs. actual state on failure" + , timeout :: w ::: Maybe Int "Execution timeout (default: 10 sec.)" } | Compliance -- Run Ethereum Blockhain compliance report { tests :: w ::: String "Path to Ethereum Tests directory" @@ -231,37 +233,38 @@ Options.parseRecordWithModifiers Options.lispCaseModifiers optsMode :: Command Options.Unwrapped -> Mode -optsMode x = if debug x then Debug else Run +optsMode x = if debug x then Debug else if jsontrace x then JsonTrace else Run applyCache :: (Maybe String, Maybe String) -> IO (EVM.VM -> EVM.VM) applyCache (state, cache) = let applyState = flip Facts.apply - applyCache = flip Facts.applyCache + applyCache' = flip Facts.applyCache in case (state, cache) of (Nothing, Nothing) -> do pure id (Nothing, Just cachePath) -> do facts <- Git.loadFacts (Git.RepoAt cachePath) - pure $ applyCache facts + pure $ applyCache' facts (Just statePath, Nothing) -> do facts <- Git.loadFacts (Git.RepoAt statePath) pure $ applyState facts (Just statePath, Just cachePath) -> do cacheFacts <- Git.loadFacts (Git.RepoAt cachePath) stateFacts <- Git.loadFacts (Git.RepoAt statePath) - pure $ (applyState stateFacts) . (applyCache cacheFacts) + pure $ (applyState stateFacts) . (applyCache' cacheFacts) -unitTestOptions :: Command Options.Unwrapped -> String -> IO UnitTestOptions +unitTestOptions :: Command Options.Unwrapped -> String -> Query UnitTestOptions unitTestOptions cmd testFile = do let root = fromMaybe "." (dappRoot cmd) - srcInfo <- readSolc testFile >>= \case + srcInfo <- liftIO $ readSolc testFile >>= \case Nothing -> error "Could not read .sol.json file" Just (contractMap, sourceCache) -> pure $ dappInfo root contractMap sourceCache - vmModifier <- applyCache (state cmd, cache cmd) + vmModifier <- liftIO $ applyCache (state cmd, cache cmd) - params <- getParametersFromEnvironmentVariables (rpc cmd) + params <- liftIO $ getParametersFromEnvironmentVariables (rpc cmd) + state <- queryState let testn = testNumber params @@ -272,12 +275,16 @@ pure EVM.UnitTest.UnitTestOptions { EVM.UnitTest.oracle = case rpc cmd of - Just url -> EVM.Fetch.http block' url - Nothing -> EVM.Fetch.zero + Just url -> EVM.Fetch.oracle (Just state) (Just (block', url)) True + Nothing -> EVM.Fetch.oracle (Just state) Nothing True + , EVM.UnitTest.maxIter = maxIterations cmd + , EVM.UnitTest.smtTimeout = smttimeout cmd + , EVM.UnitTest.solver = solver cmd + , EVM.UnitTest.smtState = Just state , EVM.UnitTest.verbose = verbose cmd - , EVM.UnitTest.match = pack $ fromMaybe "^test" (match cmd) + , EVM.UnitTest.match = pack $ fromMaybe ".*" (match cmd) , EVM.UnitTest.fuzzRuns = fromMaybe 100 (fuzzRuns cmd) - , EVM.UnitTest.replay = do + , EVM.UnitTest.replay = do arg' <- replay cmd return (fst arg', LazyByteString.fromStrict (hexByteString "--replay" $ strip0x $ snd arg')) , EVM.UnitTest.vmModifier = vmModifier @@ -303,19 +310,13 @@ DappTest {} -> withCurrentDirectory root $ do testFile <- findJsonFile (jsonFile cmd) - testOpts <- unitTestOptions cmd testFile - case (coverage cmd, optsMode cmd) of - (False, Run) -> - dappTest testOpts (optsMode cmd) testFile (cache cmd) - (False, Debug) -> - EVM.TTY.main testOpts root testFile - (True, _) -> - dappCoverage testOpts (optsMode cmd) testFile - Interactive {} -> - withCurrentDirectory root $ do - testFile <- findJsonFile (jsonFile cmd) - testOpts <- unitTestOptions cmd testFile - EVM.TTY.main testOpts root testFile + runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do + testOpts <- unitTestOptions cmd testFile + case (coverage cmd, optsMode cmd) of + (False, Run) -> dappTest testOpts testFile (cache cmd) + (False, Debug) -> liftIO $ EVM.TTY.main testOpts root testFile + (False, JsonTrace) -> error "json traces not implemented for dappTest" + (True, _) -> liftIO $ dappCoverage testOpts (optsMode cmd) testFile Compliance {} -> case (group cmd) of Just "Blockchain" -> launchScript "/run-blockchain-tests" cmd @@ -374,41 +375,27 @@ , intercalate ", " xs ] -dappTest :: UnitTestOptions -> Mode -> String -> Maybe String -> IO () -dappTest opts _ solcFile cache = - readSolc solcFile >>= - \case - Just (contractMap, sourceCache) -> do - let matcher = regexMatches (EVM.UnitTest.match opts) - unitTests = (findUnitTests matcher) (Map.elems contractMap) - - results <- concatMapM (runUnitTestContract opts contractMap sourceCache) unitTests - let (passing, vms) = unzip results - - case cache of - Nothing -> - pure () - Just path -> - -- merge all of the post-vm caches and save into the state - let - cache' = mconcat [view EVM.cache vm | vm <- vms] - in - Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts cache') - - unless (all id passing) exitFailure - Nothing -> - error ("Failed to read Solidity JSON for `" ++ solcFile ++ "'") +dappTest :: UnitTestOptions -> String -> Maybe String -> Query () +dappTest opts solcFile cache = do + out <- liftIO $ readSolc solcFile + case out of + Just (contractMap, _) -> do + let unitTests = findUnitTests (EVM.UnitTest.match opts) $ Map.elems contractMap + results <- concatMapM (runUnitTestContract opts contractMap) unitTests + let (passing, vms) = unzip results + case cache of + Nothing -> + pure () + Just path -> + -- merge all of the post-vm caches and save into the state + let + cache' = mconcat [view EVM.cache vm | vm <- vms] + in + liftIO $ Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts cache') -regexMatches :: Text -> Text -> Bool -regexMatches regexSource = - let - compOpts = - Regex.defaultCompOpt { Regex.lastStarGreedy = True } - execOpts = - Regex.defaultExecOpt { Regex.captureGroups = False } - regex = Regex.makeRegexOpts compOpts execOpts (unpack regexSource) - in - Regex.matchTest regex . Seq.fromList . unpack + liftIO $ unless (and passing) exitFailure + Nothing -> + error ("Failed to read Solidity JSON for `" ++ solcFile ++ "'") equivalence :: Command Options.Unwrapped -> IO () equivalence cmd = @@ -419,34 +406,36 @@ Just sig' -> do method' <- functionAbi sig' return $ Just (view methodSignature method', snd <$> view methodInputs method') - void . runSMTWithTimeOut (solver cmd) (smttimeout cmd) . query $ + void . runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) . query $ equivalenceCheck bytecodeA bytecodeB (maxIterations cmd) maybeSignature >>= \case Right vm -> do io $ putStrLn "Not equal!" io $ putStrLn "Counterexample:" showCounterexample vm maybeSignature - io $ exitFailure + io exitFailure Left (postAs, postBs) -> io $ do putStrLn $ "Explored: " <> show (length postAs) <> " execution paths of A and: " <> show (length postBs) <> " paths of B." - putStrLn $ "No discrepancies found." + putStrLn "No discrepancies found." -- cvc4 sets timeout via a commandline option instead of smtlib `(set-option)` -runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Symbolic a -> IO a -runSMTWithTimeOut solver maybeTimeout sym - | solver == Just "cvc4" = do - setEnv "SBV_CVC4_OPTIONS" ("--lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=" <> show timeout) - a <- runSMTWith cvc4 sym - setEnv "SBV_CVC4_OPTIONS" "" - return a +runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Bool -> Symbolic a -> IO a +runSMTWithTimeOut solver maybeTimeout smtdebug symb + | solver == Just "cvc4" = runwithcvc4 | solver == Just "z3" = runwithz3 - | solver == Nothing = runwithz3 + | solver == Nothing = runwithcvc4 | otherwise = error "Unknown solver. Currently supported solvers; z3, cvc4" - where timeout = fromMaybe 20000 maybeTimeout - runwithz3 = runSMTWith z3 $ (setTimeOut timeout) >> sym + where timeout = fromMaybe 30000 maybeTimeout + runwithz3 = runSMTWith z3{SBV.verbose=smtdebug} $ (setTimeOut timeout) >> symb + runwithcvc4 = do + setEnv "SBV_CVC4_OPTIONS" ("--lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=" <> show timeout) + a <- runSMTWith cvc4{SBV.verbose=smtdebug} symb + setEnv "SBV_CVC4_OPTIONS" "" + return a + checkForVMErrors :: [EVM.VM] -> [String] checkForVMErrors [] = [] checkForVMErrors (vm:vms) = @@ -459,18 +448,15 @@ _ -> checkForVMErrors vms -emptyDapp :: DappInfo -emptyDapp = dappInfo "" mempty (SourceCache mempty mempty mempty mempty) - getSrcInfo :: Command Options.Unwrapped -> IO DappInfo getSrcInfo cmd = let root = fromMaybe "." (dappRoot cmd) in case (jsonFile cmd) of Nothing -> - pure $ emptyDapp + pure emptyDapp Just json -> readSolc json >>= \case Nothing -> - pure $ emptyDapp + pure emptyDapp Just (contractMap, sourceCache) -> pure $ dappInfo root contractMap sourceCache @@ -482,10 +468,19 @@ -- If function signatures are known, they should always be given for best results. assert :: Command Options.Unwrapped -> IO () assert cmd = do + srcInfo <- getSrcInfo cmd let block' = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd) rpcinfo = (,) block' <$> rpc cmd - model = fromMaybe (if create cmd then InitialS else SymbolicS) (storageModel cmd) - srcInfo <- getSrcInfo cmd + treeShowing :: Tree BranchInfo -> Query () + treeShowing tree = + when (showTree cmd) $ do + consistentTree tree >>= \case + Nothing -> io $ putStrLn "No consistent paths" -- unlikely + Just tree' -> let + showBranch = showBranchInfoWithAbi srcInfo + renderTree' = renderTree showBranch (showLeafInfo srcInfo) + in io $ setLocaleEncoding utf8 >> putStrLn (showTree' (renderTree' tree')) + maybesig <- case sig cmd of Nothing -> return Nothing @@ -495,27 +490,29 @@ name = view methodSignature method' return $ Just (name,typ) if debug cmd then - runSMTWithTimeOut (solver cmd) (smttimeout cmd) $ query $ do + runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do preState <- symvmFromCommand cmd smtState <- queryState io $ void $ EVM.TTY.runFromVM (maxIterations cmd) srcInfo - (EVM.Fetch.oracle (Just smtState) rpcinfo model True) + (EVM.Fetch.oracle (Just smtState) rpcinfo True) preState else - runSMTWithTimeOut (solver cmd) (smttimeout cmd) $ query $ do + runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do preState <- symvmFromCommand cmd verify preState (maxIterations cmd) rpcinfo (Just checkAssertions) >>= \case - Right _ -> do + Right tree -> do io $ putStrLn "Assertion violation found." showCounterexample preState maybesig + treeShowing tree io $ exitWith (ExitFailure 1) - Left (pre, posts) -> do - io $ putStrLn $ "Explored: " <> show (length posts) + Left tree -> do + io $ putStrLn $ "Explored: " <> show (length tree) <> " branches without assertion violations" - let vmErrs = checkForVMErrors posts + treeShowing tree + let vmErrs = checkForVMErrors $ leaves tree unless (null vmErrs) $ io $ do putStrLn $ "However, " @@ -524,18 +521,21 @@ print vmErrs -- When `--get-models` is passed, we print example vm info for each path when (getModels cmd) $ - forM_ (zip [1..] posts) $ \(i, postVM) -> do + forM_ (zip [(1:: Integer)..] (leaves tree)) $ \(i, postVM) -> do resetAssertions - constrain (sAnd (view EVM.pathConditions postVM)) + constrain (sAnd (fst <$> view EVM.constraints postVM)) io $ putStrLn $ - "-- Branch (" <> show i <> "/" <> show (length posts) <> ") --" + "-- Branch (" <> show i <> "/" <> show (length tree) <> ") --" checkSat >>= \case + DSat _ -> error "assert: unexpected SMT result" Unk -> io $ do putStrLn "Timed out" print $ view EVM.result postVM Unsat -> io $ do putStrLn "Inconsistent path conditions: dead path" print $ view EVM.result postVM Sat -> do - showCounterexample pre maybesig + showCounterexample preState maybesig + io $ putStrLn "-- Pathconditions --" + io $ print $ snd <$> view EVM.constraints postVM case view EVM.result postVM of Nothing -> error "internal error; no EVM result" @@ -561,10 +561,9 @@ readSolc solcFile >>= \case Just (contractMap, sourceCache) -> do - let matcher = regexMatches (EVM.UnitTest.match opts) - let unitTests = (findUnitTests matcher) (Map.elems contractMap) - covs <- mconcat <$> mapM (coverageForUnitTestContract opts contractMap sourceCache) unitTests - + let unitTests = findUnitTests (EVM.UnitTest.match opts) $ Map.elems contractMap + covs <- mconcat <$> mapM + (coverageForUnitTestContract opts contractMap sourceCache) unitTests let dapp = dappInfo "." contractMap sourceCache f (k, vs) = do @@ -618,6 +617,7 @@ Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts (view EVM.cache vm')) Debug -> void $ EVM.TTY.runFromVM Nothing dapp fetcher vm + JsonTrace -> void $ execStateT (interpretWithTrace fetcher EVM.Stepper.runFully) vm where fetcher = maybe EVM.Fetch.zero (EVM.Fetch.http block') (rpc cmd) block' = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd) @@ -688,9 +688,9 @@ (miner,ts,blockNum,diff) <- case rpc cmd of Nothing -> return (0,0,0,0) Just url -> EVM.Fetch.fetchBlockFrom block' url >>= \case - Nothing -> error $ "Could not fetch block" + Nothing -> error "Could not fetch block" Just EVM.Block{..} -> return (_coinbase - , wordValue $ forceLit $ _timestamp + , wordValue $ forceLit _timestamp , wordValue _number , wordValue _difficulty ) @@ -721,7 +721,7 @@ EVM.initialContract (codeType $ hexByteString "--code" $ strip0x c) (_, _, Nothing) -> - error $ "must provide at least (rpc + address) or code" + error "must provide at least (rpc + address) or code" return $ VMTest.initTx $ withCache (vm0 miner ts blockNum diff contract) where @@ -733,12 +733,12 @@ calldata' = ConcreteBuffer $ bytes calldata "" codeType = if create cmd then EVM.InitCode else EVM.RuntimeCode address' = if create cmd - then createAddress origin' (word nonce 0) + then addr address (createAddress origin' (word nonce 0)) else addr address 0xacab vm0 miner ts blockNum diff c = EVM.makeVm $ EVM.VMOpts { EVM.vmoptContract = c - , EVM.vmoptCalldata = (calldata', literal . num $ len calldata') + , EVM.vmoptCalldata = (calldata', litWord (num $ len calldata')) , EVM.vmoptValue = w256lit value' , EVM.vmoptAddress = address' , EVM.vmoptCaller = litAddr caller' @@ -774,24 +774,24 @@ ) caller' <- maybe (SAddr <$> freshVar_) (return . litAddr) (caller cmd) - ts <- maybe (sw256 <$> freshVar_) (return . w256lit) (timestamp cmd) - callvalue' <- maybe (sw256 <$> freshVar_) (return . w256lit) (value cmd) + ts <- maybe (var "Timestamp" <$> freshVar_) (return . w256lit) (timestamp cmd) + callvalue' <- maybe (var "CallValue" <$> freshVar_) (return . w256lit) (value cmd) (calldata', cdlen, pathCond) <- case (calldata cmd, sig cmd) of - -- fully abstract calldata (up to 1024 bytes) + -- fully abstract calldata (up to 256 bytes) (Nothing, Nothing) -> do cd <- sbytes256 - len <- freshVar_ - return (SymbolicBuffer cd, len, len .<= 256) + len' <- freshVar_ + return (SymbolicBuffer cd, var "CALLDATALENGTH" len', (len' .<= 256, Todo "len < 256" [])) -- fully concrete calldata (Just c, Nothing) -> let cd = ConcreteBuffer $ decipher c - in return (cd, num (len cd), sTrue) + in return (cd, litWord (num $ len cd), (sTrue, Todo "" [])) -- calldata according to given abi with possible specializations from the `arg` list (Nothing, Just sig') -> do method' <- io $ functionAbi sig' let typs = snd <$> view methodInputs method' (cd, cdlen) <- symCalldata (view methodSignature method') typs (arg cmd) - return (SymbolicBuffer cd, cdlen, sTrue) + return (SymbolicBuffer cd, litWord (num cdlen), (sTrue, Todo "" [])) _ -> error "incompatible options: calldata and abi" @@ -800,10 +800,10 @@ -- ConcreteS cannot (instead values can be fetched from rpc!) -- Initial defaults to 0 for uninitialized storage slots, -- whereas the values of SymbolicS are unconstrained. - Just InitialS -> EVM.Symbolic <$> freshArray_ (Just 0) + Just InitialS -> EVM.Symbolic [] <$> freshArray_ (Just 0) Just ConcreteS -> return (EVM.Concrete mempty) - Just SymbolicS -> EVM.Symbolic <$> freshArray_ Nothing - Nothing -> EVM.Symbolic <$> freshArray_ (if create cmd then (Just 0) else Nothing) + Just SymbolicS -> EVM.Symbolic [] <$> freshArray_ Nothing + Nothing -> EVM.Symbolic [] <$> freshArray_ (if create cmd then (Just 0) else Nothing) withCache <- io $ applyCache (state cmd, cache cmd) @@ -811,7 +811,7 @@ (Just url, Just addr', _) -> io (EVM.Fetch.fetchContractFrom block' url addr') >>= \case Nothing -> - error $ "contract not found." + error "contract not found." Just contract' -> return contract'' where contract'' = case code cmd of @@ -827,10 +827,10 @@ (_, _, Just c) -> return $ (EVM.initialContract . codeType $ decipher c) (_, _, Nothing) -> - error $ "must provide at least (rpc + address) or code" + error "must provide at least (rpc + address) or code" return $ (VMTest.initTx $ withCache $ vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' contract') - & over EVM.pathConditions (<> [pathCond]) + & over EVM.constraints (<> [pathCond]) & set (EVM.env . EVM.contracts . (ix address') . EVM.storage) store where @@ -839,7 +839,7 @@ origin' = addr origin 0 codeType = if create cmd then EVM.InitCode else EVM.RuntimeCode address' = if create cmd - then createAddress origin' (word nonce 0) + then addr address (createAddress origin' (word nonce 0)) else addr address 0xacab vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts { EVM.vmoptContract = c @@ -895,10 +895,12 @@ action <- async $ case mode of Run -> - Timeout.timeout (1e6 * (fromMaybe 10 timelimit)) $ + Timeout.timeout (1000000 * (fromMaybe 10 timelimit)) $ execStateT (EVM.Stepper.interpret EVM.Fetch.zero . void $ EVM.Stepper.execFully) vm0 Debug -> Just <$> EVM.TTY.runFromVM Nothing emptyDapp EVM.Fetch.zero vm0 + JsonTrace -> + Just <$> execStateT (interpretWithTrace EVM.Fetch.zero EVM.Stepper.runFully) vm0 waitCatch action case result of Right (Just vm1) -> do diff --git a/hevm.cabal b/hevm.cabal --- a/hevm.cabal +++ b/hevm.cabal @@ -2,7 +2,7 @@ name: hevm version: - 0.42.0 + 0.44.1 synopsis: Ethereum virtual machine evaluator description: @@ -48,7 +48,6 @@ EVM.Fetch, EVM.FeeSchedule, EVM.Hexdump, - EVM.Keccak, EVM.Op, EVM.Patricia, EVM.Precompiled, @@ -82,6 +81,7 @@ 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, containers >= 0.6.0 && < 0.7, deepseq >= 1.4.4 && < 1.5, time >= 1.8.0 && < 1.11, @@ -121,7 +121,7 @@ restless-git >= 0.7 && < 0.8, rosezipper >= 0.2 && < 0.3, s-cargot >= 0.1.4 && < 0.2, - sbv >= 8.7.5 && < 8.9, + sbv >= 8.7.5, semver-range >= 0.2.7 && < 0.3, temporary >= 1.3 && < 1.4, text-format >= 0.3.2 && < 0.4, diff --git a/src/EVM.hs b/src/EVM.hs --- a/src/EVM.hs +++ b/src/EVM.hs @@ -13,22 +13,20 @@ module EVM where -import Prelude hiding (log, Word, exponent) +import Prelude hiding (log, Word, exponent, GT, LT) import Data.SBV hiding (Word, output, Unknown) import Data.Proxy (Proxy(..)) import EVM.ABI import EVM.Types import EVM.Solidity -import EVM.Keccak -import EVM.Concrete (Word(..), w256, createAddress, wordValue, keccakBlob, create2Address) +import EVM.Concrete (createAddress, wordValue, keccakBlob, create2Address) import EVM.Symbolic import EVM.Op import EVM.FeeSchedule (FeeSchedule (..)) import Options.Generic as Options import qualified EVM.Precompiled -import Data.Binary.Get (runGetOrFail) import Data.Text (Text) import Data.Word (Word8, Word32) import Control.Lens hiding (op, (:<), (|>), (.>)) @@ -58,8 +56,8 @@ import qualified Data.Vector as RegularVector import Crypto.Number.ModArithmetic (expFast) -import Crypto.Hash (Digest, SHA256, RIPEMD160) import qualified Crypto.Hash as Crypto +import Crypto.Hash (Digest, SHA256, RIPEMD160) -- * Data types @@ -85,6 +83,8 @@ | PrecompileFailure | UnexpectedSymbolicArg | DeadPath + | NotUnique Whiff + | SMTTimeout deriving instance Show Error -- | The possible result states of a VM @@ -106,15 +106,17 @@ , _traces :: Zipper.TreePos Zipper.Empty Trace , _cache :: Cache , _burned :: Word - , _pathConditions :: [SBool] + , _constraints :: [(SBool, Whiff)] , _iterations :: Map CodeLocation Int } + deriving (Show) data Trace = Trace { _traceCodehash :: W256 - , _traceOpIx :: Int + , _traceOpIx :: Maybe Int , _traceData :: TraceData } + deriving (Show) data TraceData = EventTrace Log @@ -123,32 +125,38 @@ | ErrorTrace Error | EntryTrace Text | ReturnTrace Buffer FrameContext + deriving (Show) -- | Queries halt execution until resolved through RPC calls or SMT queries data Query where - PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query - PleaseFetchSlot :: Addr -> Word -> (Word -> EVM ()) -> Query + PleaseFetchContract :: Addr -> StorageModel -> (Contract -> EVM ()) -> Query + PleaseMakeUnique :: SymVal a => SBV a -> [SBool] -> (IsUnique a -> EVM ()) -> Query + PleaseFetchSlot :: Addr -> Word -> (Word -> EVM ()) -> Query PleaseAskSMT :: SBool -> [SBool] -> (BranchCondition -> EVM ()) -> Query data Choose where - PleaseChoosePath :: (Bool -> EVM ()) -> Choose + PleaseChoosePath :: Whiff -> (Bool -> EVM ()) -> Choose instance Show Query where showsPrec _ = \case - PleaseFetchContract addr _ -> + PleaseFetchContract addr _ _ -> (("") ++) PleaseFetchSlot addr slot _ -> (("") ++) - PleaseAskSMT condition pathConditions _ -> + PleaseAskSMT condition constraints _ -> (("") ++) + ++ show constraints ++ ">") ++) + PleaseMakeUnique val constraints _ -> + (("") ++) instance Show Choose where showsPrec _ = \case - PleaseChoosePath _ -> + PleaseChoosePath _ _ -> ((" b @@ -511,11 +531,11 @@ let ?op = 0x00 -- dummy value let calldatasize = snd (the state calldata) - case unliteral calldatasize of + case maybeLitWord calldatasize of Nothing -> vmError UnexpectedSymbolicArg Just calldatasize' -> do copyBytesToMemory (fst $ the state calldata) (num calldatasize') 0 0 - executePrecompile self (the state gas) 0 (num calldatasize') 0 0 [] + executePrecompile self (num $ the state gas) 0 (num calldatasize') 0 0 [] vmx <- get case view (state.stack) vmx of (x:_) -> case maybeLitWord x of @@ -543,8 +563,8 @@ -- op: PUSH x | x >= 0x60 && x <= 0x7f -> do let !n = num x - 0x60 + 1 - !xs = BS.take n (BS.drop (1 + the state pc) - (the state code)) + !xs = padRight n $ BS.take n (BS.drop (1 + the state pc) + (the state code)) limitStack 1 $ burn g_verylow $ do next @@ -587,7 +607,7 @@ bytes = readMemory (num xOffset) (num xSize) vm log = Log self bytes topics - burn (g_log + g_logdata * xSize + num n * g_logtopic) $ + burn (g_log + g_logdata * (num xSize) + num n * g_logtopic) $ accessMemoryRange fees xOffset xSize $ do traceLog log next @@ -614,7 +634,7 @@ stackOp2 (const g_low) (uncurry sdiv) -- op: MOD - 0x06 -> stackOp2 (const g_low) $ \(x, y) -> ite (y .== 0) 0 (x `sMod` y) + 0x06 -> stackOp2 (const g_low) $ \(S a x, S b y) -> S (ITE (IsZero b) (Literal 0) (Mod a b)) (ite (y .== 0) 0 (x `sMod` y)) -- op: SMOD 0x07 -> stackOp2 (const g_low) $ uncurry smod @@ -624,18 +644,18 @@ 0x09 -> stackOp3 (const g_mid) (\(x, y, z) -> mulmod x y z) -- op: LT - 0x10 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .< y) 1 0 + 0x10 -> stackOp2 (const g_verylow) $ \(S a x, S b y) -> iteWhiff (LT a b) (x .< y) 1 0 -- op: GT - 0x11 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .> y) 1 0 + 0x11 -> stackOp2 (const g_verylow) $ \(S a x, S b y) -> iteWhiff (GT a b) (x .> y) 1 0 -- op: SLT 0x12 -> stackOp2 (const g_verylow) $ uncurry slt -- op: SGT 0x13 -> stackOp2 (const g_verylow) $ uncurry sgt -- op: EQ - 0x14 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .== y) 1 0 + 0x14 -> stackOp2 (const g_verylow) $ \(S a x, S b y) -> iteWhiff (Eq a b) (x .== y) 1 0 -- op: ISZERO - 0x15 -> stackOp1 (const g_verylow) $ \x -> ite (x .== 0) 1 0 + 0x15 -> stackOp1 (const g_verylow) $ \(S a x) -> iteWhiff (IsZero a) (x .== 0) 1 0 -- op: AND 0x16 -> stackOp2 (const g_verylow) $ uncurry (.&.) @@ -652,11 +672,11 @@ (n, x) | otherwise -> 0xff .&. shiftR x (8 * (31 - num (forceLit n))) -- op: SHL - 0x1b -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sShiftLeft x n + 0x1b -> stackOp2 (const g_verylow) $ \((S a n), (S b x)) -> S (SHL b a) $ sShiftLeft x n -- op: SHR - 0x1c -> stackOp2 (const g_verylow) $ uncurry shiftRight' + 0x1c -> stackOp2 (const g_verylow) $ \((S a n), (S b x)) -> S (SHR b a) $ sShiftRight x n -- op: SAR - 0x1d -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sSignedShiftArithRight x n + 0x1d -> stackOp2 (const g_verylow) $ \((S a n), (S b x)) -> S (SAR b a) $ sSignedShiftArithRight x n -- op: SHA3 -- more accurately refered to as KECCAK @@ -664,29 +684,38 @@ case stk of (xOffset' : xSize' : xs) -> forceConcrete xOffset' $ - \xOffset -> forceConcrete xSize' $ \xSize -> do - (hash, invMap) <- case readMemory xOffset xSize vm of - ConcreteBuffer bs -> pure (litWord $ keccakBlob bs, Map.singleton (keccakBlob bs) bs) + \xOffset -> forceConcrete xSize' $ \xSize -> + burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $ + accessMemoryRange fees xOffset xSize $ do + (hash@(S _ hash'), invMap, bytes) <- case readMemory xOffset xSize vm of + ConcreteBuffer bs -> do + pure (litWord $ keccakBlob bs, Map.singleton (keccakBlob bs) bs, litBytes bs) + SymbolicBuffer bs -> do + let hash' = symkeccak' bs + return (S (FromKeccak $ SymbolicBuffer bs) hash', mempty, bs) - -- Although we would like to simply assert that the uninterpreted function symkeccak' - -- is injective, this proves to cause a lot of concern for our smt solvers, probably - -- due to the introduction of universal quantifiers into the queries. + -- Although we would like to simply assert that the uninterpreted function symkeccak' + -- is injective, this proves to cause a lot of concern for our smt solvers, probably + -- due to the introduction of universal quantifiers into the queries. - -- Instead, we keep track of all of the particular invocations of symkeccak' we see - -- (similarly to sha3Crack), and simply assert that injectivity holds for these - -- particular invocations. + -- Instead, we keep track of all of the particular invocations of symkeccak' we see + -- (similarly to sha3Crack), and simply assert that injectivity holds for these + -- particular invocations. + -- + -- We additionally make the probabalisitc assumption that the output of symkeccak' + -- is greater than 100. This lets us avoid having to reason about storage collisions + -- between mappings and "normal" slots - SymbolicBuffer bs -> do - let hash' = symkeccak' bs - previousUsed = view (env . keccakUsed) vm - env . keccakUsed <>= [(bs, hash')] - pathConditions <>= fmap (\(preimage, image) -> - image .== hash' .=> preimage .== bs) - previousUsed - return (sw256 hash', mempty) + let previousUsed = view (env . keccakUsed) vm + env . keccakUsed <>= [(bytes, hash')] + constraints <>= (hash' .> 100, Todo "probabilistic keccak assumption" []): + (fmap (\(preimage, image) -> + -- keccak is a function + ((preimage .== bytes .=> image .== hash') .&& + -- which is injective + (image .== hash' .=> preimage .== bytes), Todo "injective keccak assumption" [])) + previousUsed) - burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $ - accessMemoryRange fees xOffset xSize $ do next assign (state . stack) (hash : xs) (env . sha3Crack) <>= invMap @@ -717,7 +746,10 @@ -- op: CALLER 0x33 -> limitStack 1 . burn g_base $ - let toSymWord = sw256 . sFromIntegral . saddressWord160 + let toSymWord :: SAddr -> SymWord + toSymWord (SAddr x) = case unliteral x of + Just s -> litWord $ num s + Nothing -> var "CALLER" $ sFromIntegral x in next >> pushSym (toSymWord (the state caller)) -- op: CALLVALUE @@ -727,23 +759,23 @@ -- op: CALLDATALOAD 0x35 -> stackOp1 (const g_verylow) $ - \(S _ x) -> uncurry (readSWordWithBound (sFromIntegral x)) (the state calldata) + \ind -> uncurry (readSWordWithBound ind) (the state calldata) -- op: CALLDATASIZE 0x36 -> limitStack 1 . burn g_base $ - next >> pushSym (sw256 . zeroExtend . snd $ (the state calldata)) + next >> pushSym (snd (the state calldata)) -- op: CALLDATACOPY 0x37 -> case stk of (xTo' : xFrom' : xSize' : xs) -> forceConcrete3 (xTo',xFrom',xSize') $ \(xTo,xFrom,xSize) -> - burn (g_verylow + g_copy * ceilDiv xSize 32) $ + burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $ accessUnboundedMemoryRange fees xTo xSize $ do next assign (state . stack) xs case the state calldata of - (SymbolicBuffer cd, cdlen) -> copyBytesToMemory (SymbolicBuffer [ite (i .<= cdlen) x 0 | (x, i) <- zip cd [1..]]) xSize xFrom xTo + (SymbolicBuffer cd, (S _ cdlen)) -> copyBytesToMemory (SymbolicBuffer [ite (i .<= cdlen) x 0 | (x, i) <- zip cd [1..]]) xSize xFrom xTo -- when calldata is concrete, -- the bound should always be equal to the bytestring length (cd, _) -> copyBytesToMemory cd xSize xFrom xTo @@ -774,7 +806,7 @@ -- op: EXTCODESIZE 0x3b -> case stk of - (x':xs) -> forceConcrete x' $ \x -> + (x':xs) -> makeUnique x' $ \x -> if x == num cheatCode then do next @@ -818,7 +850,7 @@ case stk of (xTo' : xFrom' : xSize' :xs) -> forceConcrete3 (xTo', xFrom', xSize') $ \(xTo, xFrom, xSize) -> - burn (g_verylow + g_copy * ceilDiv xSize 32) $ + burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $ accessUnboundedMemoryRange fees xTo xSize $ do next assign (state . stack) xs @@ -945,12 +977,12 @@ accessStorage self x $ \current -> do availableGas <- use (state . gas) - if availableGas <= g_callstipend - then finishFrame (FrameErrored (OutOfGas availableGas g_callstipend)) + if num availableGas <= g_callstipend + then finishFrame (FrameErrored (OutOfGas availableGas (num g_callstipend))) else do let original = case view storage this of Concrete _ -> fromMaybe 0 (Map.lookup (forceLit x) (view origStorage this)) - Symbolic _ -> 0 -- we don't use this value anywhere anyway + Symbolic _ _ -> 0 -- we don't use this value anywhere anyway cost = case (maybeLitWord current, maybeLitWord new) of (Just current', Just new') -> if (current' == new') then g_sload @@ -999,7 +1031,7 @@ -- op: JUMPI 0x57 -> do case stk of - (x:y:xs) -> forceConcrete x $ \x' -> + (x:y@(S w _):xs) -> forceConcrete x $ \x' -> burn g_high $ let jump :: Bool -> EVM () jump True = assign (state . stack) xs >> next @@ -1007,7 +1039,7 @@ in case maybeLitWord y of Just y' -> jump (0 == y') -- if the jump condition is symbolic, an smt query has to be made. - Nothing -> askSMT (self, the state pc) (0 .== y) jump + Nothing -> askSMT (self, the state pc) (0 .== y, IsZero w) jump _ -> underrun -- op: PC @@ -1023,7 +1055,7 @@ -- op: GAS 0x5a -> limitStack 1 . burn g_base $ - next >> push (the state gas - g_base) + next >> push (the state gas - num g_base) -- op: JUMPDEST 0x5b -> burn g_jumpdest next @@ -1034,16 +1066,16 @@ if exponent == 0 then g_exp else g_exp + g_expbyte * num (ceilDiv (1 + log2 exponent) 8) - in stackOp2 cost $ \((S _ x),(S _ y)) -> sw256 $ x .^ y + in stackOp2 cost $ \((S a x),(S b y)) -> S (Exp a b) (x .^ y) -- op: SIGNEXTEND 0x0b -> - stackOp2 (const g_low) $ \((forceLit -> bytes), w@(S _ x)) -> + stackOp2 (const g_low) $ \((forceLit -> bytes), w@(S a x)) -> if bytes >= 32 then w else let n = num bytes * 8 + 7 in - sw256 $ ite (sTestBit x n) - (x .|. complement (bit n - 1)) - (x .&. (bit n - 1)) + S (Todo "signextend" [a]) $ ite (sTestBit x n) + (x .|. complement (bit n - 1)) + (x .&. (bit n - 1)) -- op: CREATE 0xf0 -> @@ -1057,38 +1089,32 @@ newAddr = createAddress self (wordValue (view nonce this)) (cost, gas') = costOfCreate fees availableGas 0 burn (cost - gas') $ forceConcreteBuffer (readMemory (num xOffset) (num xSize) vm) $ \initCode -> - create self this gas' xValue xs newAddr initCode + create self this (num gas') xValue xs newAddr initCode _ -> underrun -- op: CALL 0xf1 -> case stk of ( xGas' - : xTo' + : S _ xTo : (forceLit -> xValue) : xInOffset' : xInSize' : xOutOffset' : xOutSize' : xs - ) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $ - \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) -> - (if xValue > 0 then notStatic else id) $ - case xTo of - n | n > 0 && n <= 9 -> - precompiledContract this xGas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs - n | num n == cheatCode -> - do - assign (state . stack) xs - cheat (xInOffset, xInSize) (xOutOffset, xOutSize) - _ -> delegateCall this xGas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $ do - zoom state $ do - assign callvalue (litWord xValue) - assign caller (litAddr self) - assign contract xTo - transfer self xTo xValue - touchAccount self - touchAccount xTo + ) -> forceConcrete5 (xGas',xInOffset', xInSize', xOutOffset', xOutSize') $ + \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) -> + (if xValue > 0 then notStatic else id) $ + let target = SAddr $ sFromIntegral xTo in + delegateCall this xGas target target xValue xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do + zoom state $ do + assign callvalue (litWord xValue) + assign caller (litAddr self) + assign contract callee + transfer self callee xValue + touchAccount self + touchAccount callee _ -> underrun @@ -1096,23 +1122,21 @@ 0xf2 -> case stk of ( xGas' - : xTo' + : S _ xTo' : (forceLit -> xValue) : xInOffset' : xInSize' : xOutOffset' : xOutSize' : xs - ) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $ - \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) -> - case xTo of - n | n > 0 && n <= 9 -> - precompiledContract this xGas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs - _ -> delegateCall this xGas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ do - zoom state $ do - assign callvalue (litWord xValue) - assign caller (litAddr self) - touchAccount self + ) -> forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') $ + \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) -> + let target = SAddr $ sFromIntegral xTo' in + delegateCall this xGas target (litAddr self) xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do + zoom state $ do + assign callvalue (litWord xValue) + assign caller (litAddr self) + touchAccount self _ -> underrun @@ -1133,7 +1157,7 @@ then finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize)) else - burn (g_codedeposit * codesize) $ + burn (g_codedeposit * num codesize) $ finishFrame (FrameReturned output) False -> finishFrame (FrameReturned output) @@ -1146,7 +1170,7 @@ then finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize)) else - burn (g_codedeposit * codesize) $ + burn (g_codedeposit * num codesize) $ finishFrame (FrameReturned output) CallContext {} -> finishFrame (FrameReturned output) @@ -1156,22 +1180,16 @@ 0xf4 -> case stk of (xGas' - :xTo' + :S _ xTo :xInOffset' :xInSize' :xOutOffset' :xOutSize' - :xs) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $ - \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) -> - case xTo of - n | n > 0 && n <= 9 -> - precompiledContract this xGas xTo self 0 xInOffset xInSize xOutOffset xOutSize xs - n | num n == cheatCode -> do - assign (state . stack) xs - cheat (xInOffset, xInSize) (xOutOffset, xOutSize) - _ -> do - delegateCall this xGas xTo self 0 xInOffset xInSize xOutOffset xOutSize xs $ do - touchAccount self + :xs) -> forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') $ + \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) -> + let target = SAddr $ sFromIntegral xTo in + delegateCall this xGas target (litAddr self) 0 xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do + touchAccount self _ -> underrun -- op: CREATE2 @@ -1190,31 +1208,29 @@ newAddr = create2Address self (num xSalt) initCode (cost, gas') = costOfCreate fees availableGas xSize in burn (cost - gas') $ - create self this gas' xValue xs newAddr initCode + create self this (num gas') xValue xs newAddr initCode _ -> underrun -- op: STATICCALL 0xfa -> case stk of (xGas' - :xTo' + :S _ xTo :xInOffset' :xInSize' :xOutOffset' :xOutSize' - :xs) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $ - \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) -> - case xTo of - n | n > 0 && n <= 9 -> - precompiledContract this xGas xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs - _ -> delegateCall this xGas xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs $ do - zoom state $ do - assign callvalue 0 - assign caller (litAddr self) - assign contract xTo - assign static True - touchAccount self - touchAccount xTo + :xs) -> forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') $ + \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) -> do + let target = SAddr $ sFromIntegral xTo + delegateCall this xGas target target 0 xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do + zoom state $ do + assign callvalue 0 + assign caller (litAddr self) + assign contract callee + assign static True + touchAccount self + touchAccount callee _ -> underrun @@ -1265,8 +1281,8 @@ callChecks :: (?op :: Word8) => Contract -> Word -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] - -- continuation with gas avail for call - -> (Word -> EVM ()) + -- continuation with gas available for call + -> (Integer -> EVM ()) -> EVM () callChecks this xGas xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue = do vm <- get @@ -1287,7 +1303,7 @@ then do assign (state . stack) (0 : xs) assign (state . returndata) mempty - pushTrace $ ErrorTrace $ CallDepthLimitReached + pushTrace $ ErrorTrace CallDepthLimitReached next else continue gas' @@ -1324,7 +1340,7 @@ executePrecompile :: (?op :: Word8) => Addr - -> Word -> Word -> Word -> Word -> Word -> [SymWord] + -> Integer -> Word -> Word -> Word -> Word -> [SymWord] -> EVM () executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs = do vm <- get @@ -1332,12 +1348,12 @@ fees = view (block . schedule) vm cost = costOfPrecompile fees preCompileAddr input notImplemented = error $ "precompile at address " <> show preCompileAddr <> " not yet implemented" - precompileFail = burn (gasCap - cost) $ do + precompileFail = burn (num gasCap - cost) $ do assign (state . stack) (0 : xs) - pushTrace $ ErrorTrace $ PrecompileFailure + pushTrace $ ErrorTrace PrecompileFailure next - if cost > gasCap then - burn gasCap $ do + if cost > num gasCap then + burn (num gasCap) $ do assign (state . stack) (0 : xs) next else @@ -1363,7 +1379,7 @@ 0x2 -> let hash = case input of - ConcreteBuffer input' -> ConcreteBuffer $ BS.pack $ BA.unpack $ (Crypto.hash input' :: Digest SHA256) + ConcreteBuffer input' -> ConcreteBuffer $ BS.pack $ BA.unpack (Crypto.hash input' :: Digest SHA256) SymbolicBuffer input' -> SymbolicBuffer $ symSHA256 input' in do assign (state . stack) (1 : xs) @@ -1407,9 +1423,9 @@ truncpadlit (num lenm) (asBE (0 :: Int)) False -> let - b = asInteger $ lazySlice 96 lenb $ input' - e = asInteger $ lazySlice (96 + lenb) lene $ input' - m = asInteger $ lazySlice (96 + lenb + lene) lenm $ input' + b = asInteger $ lazySlice 96 lenb input' + e = asInteger $ lazySlice (96 + lenb) lene input' + m = asInteger $ lazySlice (96 + lenb + lene) lenm input' in padLeft (num lenm) (asBE (expFast b e m)) in do @@ -1521,9 +1537,23 @@ getCodeLocation :: VM -> CodeLocation getCodeLocation vm = (view (state . contract) vm, view (state . pc) vm) +-- | Ask the SMT solver to provide a concrete model for val iff a unique model exists +makeUnique :: SymWord -> (Word -> EVM ()) -> EVM () +makeUnique sw@(S w val) cont = case maybeLitWord sw of + Nothing -> do + conditions <- use constraints + assign result . Just . VMFailure . Query $ PleaseMakeUnique val (fst <$> conditions) $ \case + Unique a -> do + assign result Nothing + cont (C w $ fromSizzle a) + InconsistentU -> vmError $ DeadPath + TimeoutU -> vmError $ SMTTimeout + Multiple -> vmError $ NotUnique w + Just a -> cont a + -- | Construct SMT Query and halt execution until resolved -askSMT :: CodeLocation -> SBool -> (Bool -> EVM ()) -> EVM () -askSMT codeloc condition continue = do +askSMT :: CodeLocation -> (SBool, Whiff) -> (Bool -> EVM ()) -> EVM () +askSMT codeloc (condition, whiff) continue = do -- We keep track of how many times we have come across this particular -- (contract, pc) combination in the `iteration` mapping. iteration <- use (iterations . at codeloc . non 0) @@ -1535,20 +1565,22 @@ Just w -> choosePath (Case w) -- If this is a new query, run the query, cache the result -- increment the iterations and select appropriate path - Nothing -> do pathconds <- use pathConditions + Nothing -> do pathconds <- use constraints assign result . Just . VMFailure . Query $ PleaseAskSMT - condition pathconds choosePath + condition' (fst <$> pathconds) choosePath - where -- Only one path is possible + where condition' = simplifyCondition condition whiff + -- Only one path is possible + choosePath :: BranchCondition -> EVM () choosePath (Case v) = do assign result Nothing - pushTo pathConditions (if v then condition else sNot condition) + pushTo constraints $ if v then (condition', whiff) else (sNot condition', IsZero whiff) iteration <- use (iterations . at codeloc . non 0) assign (cache . path . at (codeloc, iteration)) (Just v) assign (iterations . at codeloc) (Just (iteration + 1)) continue v -- Both paths are possible; we ask for more input - choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath $ choosePath . Case + choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath whiff $ choosePath . Case -- None of the paths are possible; fail this branch choosePath Inconsistent = vmError DeadPath @@ -1562,9 +1594,10 @@ Just c -> do assign (env . contracts . at addr) (Just c) continue c - Nothing -> - assign result . Just . VMFailure . Query $ - PleaseFetchContract addr + Nothing -> do + model <- use (env . storageModel) + assign result . Just . VMFailure $ Query $ + PleaseFetchContract addr model (\c -> do assign (cache . fetched . at addr) (Just c) assign (env . contracts . at addr) (Just c) assign result Nothing @@ -1576,11 +1609,11 @@ else continue c readStorage :: Storage -> SymWord -> Maybe (SymWord) -readStorage (Symbolic s) (S _ loc) = Just . sw256 $ readArray s loc +readStorage (Symbolic _ s) (S w loc) = Just $ S (FromStorage w s) $ readArray s loc readStorage (Concrete s) loc = Map.lookup (forceLit loc) s writeStorage :: SymWord -> SymWord -> Storage -> Storage -writeStorage (S _ loc) (S _ val) (Symbolic s) = Symbolic (writeArray s loc val) +writeStorage k@(S _ loc) v@(S _ val) (Symbolic xs s) = Symbolic ((k,v):xs) (writeArray s loc val) writeStorage loc val (Concrete s) = Concrete (Map.insert (forceLit loc) val s) accessStorage @@ -1635,7 +1668,6 @@ finalize :: EVM () finalize = do let - burnRemainingGas = use (state . gas) >>= flip burn noop revertContracts = use (tx . txReversion) >>= assign (env . contracts) revertSubstate = assign (tx . substate) (SubState mempty mempty mempty) @@ -1646,7 +1678,8 @@ revertContracts revertSubstate Just (VMFailure _) -> do - burnRemainingGas + -- burn remaining gas + assign (state . gas) 0 revertContracts revertSubstate Just (VMSuccess output) -> do @@ -1662,14 +1695,14 @@ txOrigin <- use (tx . origin) sumRefunds <- (sum . (snd <$>)) <$> (use (tx . substate . refunds)) miner <- use (block . coinbase) - blockReward <- r_block <$> (use (block . schedule)) + blockReward <- num . r_block <$> (use (block . schedule)) gasPrice <- use (tx . gasprice) gasLimit <- use (tx . txgaslimit) gasRemaining <- use (state . gas) let gasUsed = gasLimit - gasRemaining - cappedRefund = min (quot gasUsed 2) sumRefunds + cappedRefund = min (quot gasUsed 2) (num sumRefunds) originPay = (gasRemaining + cappedRefund) * gasPrice minerPay = gasPrice * (gasUsed - cappedRefund) @@ -1735,16 +1768,22 @@ else continue -- | Burn gas, failing if insufficient gas is available -burn :: Word -> EVM () -> EVM () -burn n continue = do - available <- use (state . gas) - if n <= available - then do - state . gas -= n - burned += n - continue - else - vmError (OutOfGas available n) +-- We use the `Integer` type to avoid overflows in intermediate +-- calculations and throw if the value won't fit into a uint64 +burn :: Integer -> EVM () -> EVM () +burn n' continue = + if n' > (2 :: Integer) ^ (64 :: Integer) - 1 + then vmError IllegalOverflow + else do + let n = num n' + available <- use (state . gas) + if n <= available + then do + state . gas -= n + burned += n + continue + else + vmError (OutOfGas available n) forceConcreteAddr :: SAddr -> (Addr -> EVM ()) -> EVM () forceConcreteAddr n continue = case maybeLitAddr n of @@ -1788,12 +1827,12 @@ forceConcreteBuffer (ConcreteBuffer b) continue = continue b -- * Substate manipulation -refund :: Word -> EVM () +refund :: Integer -> EVM () refund n = do self <- use (state . contract) pushTo (tx . substate . refunds) (self, n) -unRefund :: Word -> EVM () +unRefund :: Integer -> EVM () unRefund n = do self <- use (state . contract) refs <- use (tx . substate . refunds) @@ -1831,101 +1870,110 @@ case Map.lookup abi' cheatActions of Nothing -> vmError (BadCheatCode (Just abi')) - Just (argTypes, action) -> - case input of - SymbolicBuffer _ -> vmError UnexpectedSymbolicArg - ConcreteBuffer input' -> - case runGetOrFail - (getAbiSeq (length argTypes) argTypes) - (LS.fromStrict input') of - Right ("", _, args) -> do - action outOffset outSize (toList args) - next - push 1 - _ -> - vmError (BadCheatCode (Just abi')) + Just action -> do + action outOffset outSize input + next + push 1 -type CheatAction = ([AbiType], Word -> Word -> [AbiValue] -> EVM ()) +type CheatAction = Word -> Word -> Buffer -> EVM () cheatActions :: Map Word32 CheatAction cheatActions = Map.fromList - [ action "warp(uint256)" [AbiUIntType 256] $ - \_ _ [AbiUInt 256 x] -> - assign (block . timestamp) (sw256 $ num x), - action "roll(uint256)" [AbiUIntType 256] $ - \_ _ [AbiUInt 256 x] -> - assign (block . number) (w256 (W256 x)), - action "store(address,bytes32,bytes32)" [AbiAddressType, AbiBytesType 32, AbiBytesType 32] $ - \_ _ [AbiAddress a, AbiBytes 32 x, AbiBytes 32 y] -> do - let slot = w256lit $ word x - new = w256lit $ word y - fetchAccount a $ \_ -> do - modifying (env . contracts . ix a . storage) (writeStorage slot new), - action "load(address,bytes32)" [AbiAddressType, AbiBytesType 32] $ - \outOffset _ [AbiAddress a, AbiBytes 32 x] -> do - let slot = w256lit $ word x - accessStorage a slot $ \res -> do - assign (state . returndata . word256At 0) res - assign (state . memory . word256At outOffset) res + [ action "warp(uint256)" $ + \sig _ _ input -> case decodeStaticArgs input of + [x] -> assign (block . timestamp) (mksym x) + _ -> vmError (BadCheatCode sig), + + action "roll(uint256)" $ + \sig _ _ input -> case decodeStaticArgs input of + [x] -> forceConcrete (mksym x) (assign (block . number)) + _ -> vmError (BadCheatCode sig), + + action "store(address,bytes32,bytes32)" $ + \sig _ _ input -> case decodeStaticArgs input of + [a, slot, new] -> + makeUnique (mksym $ sFromIntegral a) $ \(C _ (num -> a')) -> + fetchAccount a' $ \_ -> do + modifying (env . contracts . ix a' . storage) (writeStorage (mksym slot) (mksym new)) + _ -> vmError (BadCheatCode sig), + + action "load(address,bytes32)" $ + \sig outOffset _ input -> case decodeStaticArgs input of + [a, slot] -> + makeUnique (mksym $ sFromIntegral a) $ \(C _ (num -> a'))-> + accessStorage a' (mksym slot) $ \res -> do + assign (state . returndata . word256At 0) res + assign (state . memory . word256At outOffset) res + _ -> vmError (BadCheatCode sig) ] where - action s ts f = (abiKeccak s, (ts, f)) + action s f = (abiKeccak s, f (Just $ abiKeccak s)) + mksym x = S (Todo "abidecode" []) x -- * General call implementation ("delegateCall") delegateCall :: (?op :: Word8) - => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] - -> EVM () + => Contract -> Word -> SAddr -> SAddr -> Word -> Word -> Word -> Word -> Word -> [SymWord] + -> (Addr -> EVM ()) -> EVM () -delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue = - callChecks this gasGiven xContext xValue xInOffset xInSize xOutOffset xOutSize xs $ - \xGas -> do - vm0 <- get - fetchAccount xTo . const $ - preuse (env . contracts . ix xTo) >>= \case - Nothing -> - vmError (NoSuchContract xTo) - Just target -> - burn xGas $ do - let newContext = CallContext - { callContextTarget = xTo - , callContextContext = xContext - , callContextOffset = xOutOffset - , callContextSize = xOutSize - , callContextCodehash = view codehash target - , callContextReversion = view (env . contracts) vm0 - , callContextSubState = view (tx . substate) vm0 - , callContextAbi = - if xInSize >= 4 - then case unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0) - of Nothing -> Nothing - Just abi -> Just . w256 $ num abi - else Nothing - , callContextData = (readMemory (num xInOffset) (num xInSize) vm0) - } +delegateCall this gasGiven (SAddr xTo) (SAddr xContext) xValue xInOffset xInSize xOutOffset xOutSize xs continue = + makeUnique (S (Todo "xTo" []) $ sFromIntegral xTo) $ \(C _ (num -> xTo')) -> + makeUnique (S (Todo "xcontext" []) $ sFromIntegral xContext) $ \(C _ (num -> xContext')) -> + if xTo' > 0 && xTo' <= 9 + then precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs + else if num xTo' == cheatCode then + do + assign (state . stack) xs + cheat (xInOffset, xInSize) (xOutOffset, xOutSize) + else + callChecks this gasGiven xContext' xValue xInOffset xInSize xOutOffset xOutSize xs $ + \xGas -> do + vm0 <- get + fetchAccount xTo' . const $ + preuse (env . contracts . ix xTo') >>= \case + Nothing -> + vmError (NoSuchContract xTo') + Just target -> do + burn xGas $ do + let newContext = CallContext + { callContextTarget = xTo' + , callContextContext = xContext' + , callContextOffset = xOutOffset + , callContextSize = xOutSize + , callContextCodehash = view codehash target + , callContextReversion = view (env . contracts) vm0 + , callContextSubState = view (tx . substate) vm0 + , callContextAbi = + if xInSize >= 4 + then case unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0) + of Nothing -> Nothing + Just abi -> Just . w256 $ num abi + else Nothing + , callContextData = (readMemory (num xInOffset) (num xInSize) vm0) + } - pushTrace (FrameTrace newContext) - next - vm1 <- get + pushTrace (FrameTrace newContext) + next + vm1 <- get - pushTo frames $ Frame - { _frameState = (set stack xs) (view state vm1) - , _frameContext = newContext - } + pushTo frames $ Frame + { _frameState = (set stack xs) (view state vm1) + , _frameContext = newContext + } - zoom state $ do - assign gas xGas - assign pc 0 - assign code (view bytecode target) - assign codeContract xTo - assign stack mempty - assign memory mempty - assign memorySize 0 - assign returndata mempty - assign calldata (readMemory (num xInOffset) (num xInSize) vm0, literal (num xInSize)) + zoom state $ do + assign gas (num xGas) + assign pc 0 + assign code (view bytecode target) + assign codeContract xTo' + assign stack mempty + assign memory mempty + assign memorySize 0 + assign returndata mempty + assign calldata (readMemory (num xInOffset) (num xInSize) vm0, w256lit (num xInSize)) - continue + continue xTo' -- -- * Contract creation @@ -1938,8 +1986,9 @@ create :: (?op :: Word8) => Addr -> Contract -> Word -> Word -> [SymWord] -> Addr -> ByteString -> EVM () -create self this xGas xValue xs newAddr initCode = do +create self this xGas' xValue xs newAddr initCode = do vm0 <- get + let xGas = num xGas' if xValue > view balance this then do assign (state . stack) (0 : xs) @@ -1958,46 +2007,47 @@ modifying (env . contracts . ix self . nonce) succ next else burn xGas $ do - touchAccount self - touchAccount newAddr - let - store = case view (env . storageModel) vm0 of - ConcreteS -> Concrete mempty - SymbolicS -> Symbolic $ sListArray 0 [] - InitialS -> Symbolic $ sListArray 0 [] - newContract = - initialContract (InitCode initCode) & set storage store - newContext = - CreationContext { creationContextCodehash = view codehash newContract - , creationContextReversion = view (env . contracts) vm0 - , creationContextSubstate = view (tx . substate) vm0 - } + touchAccount self + touchAccount newAddr + let + store = case view (env . storageModel) vm0 of + ConcreteS -> Concrete mempty + SymbolicS -> Symbolic [] $ sListArray 0 [] + InitialS -> Symbolic [] $ sListArray 0 [] + newContract = + initialContract (InitCode initCode) & set storage store + newContext = + CreationContext { creationContextAddress = newAddr + , creationContextCodehash = view codehash newContract + , creationContextReversion = view (env . contracts) vm0 + , creationContextSubstate = view (tx . substate) vm0 + } - zoom (env . contracts) $ do - oldAcc <- use (at newAddr) - let oldBal = maybe 0 (view balance) oldAcc + zoom (env . contracts) $ do + oldAcc <- use (at newAddr) + let oldBal = maybe 0 (view balance) oldAcc - assign (at newAddr) (Just (newContract & balance .~ oldBal)) - modifying (ix self . nonce) succ + assign (at newAddr) (Just (newContract & balance .~ oldBal)) + modifying (ix self . nonce) succ - transfer self newAddr xValue + transfer self newAddr xValue - pushTrace (FrameTrace newContext) - next - vm1 <- get - pushTo frames $ Frame - { _frameContext = newContext - , _frameState = (set stack xs) (view state vm1) - } + pushTrace (FrameTrace newContext) + next + vm1 <- get + pushTo frames $ Frame + { _frameContext = newContext + , _frameState = (set stack xs) (view state vm1) + } - assign state $ - blankState - & set contract newAddr - & set codeContract newAddr - & set code initCode - & set callvalue (litWord xValue) - & set caller (litAddr self) - & set gas xGas + assign state $ + blankState + & set contract newAddr + & set codeContract newAddr + & set code initCode + & set callvalue (litWord xValue) + & set caller (litAddr self) + & set gas xGas' -- | Replace a contract's code, like when CREATE returns -- from the constructor code. @@ -2065,10 +2115,6 @@ -- Are there some remaining frames? nextFrame : remainingFrames -> do - -- Pop the top frame. - assign frames remainingFrames - -- Install the state of the frame to which we shall return. - assign state (view frameState nextFrame) -- Insert a debug trace. insertTrace $ case how of @@ -2083,6 +2129,11 @@ -- Pop to the previous level of the debug trace stack. popTrace + -- Pop the top frame. + assign frames remainingFrames + -- Install the state of the frame to which we shall return. + assign state (view frameState nextFrame) + -- When entering a call, the gas allowance is counted as burned -- in advance; this unburns the remainder and adds it to the -- parent frame. @@ -2127,9 +2178,8 @@ revertSubstate assign (state . returndata) mempty push 0 - -- Or were we creating? - CreationContext _ reversion substate' -> do + CreationContext _ _ reversion substate' -> do creator <- use (state . contract) let createe = view (state . contract) oldVm @@ -2167,7 +2217,7 @@ -- * Memory helpers accessUnboundedMemoryRange - :: FeeSchedule Word + :: FeeSchedule Integer -> Word -> Word -> EVM () @@ -2182,7 +2232,7 @@ continue accessMemoryRange - :: FeeSchedule Word + :: FeeSchedule Integer -> Word -> Word -> EVM () @@ -2194,7 +2244,7 @@ else accessUnboundedMemoryRange fees f l continue accessMemoryWord - :: FeeSchedule Word -> Word -> EVM () -> EVM () + :: FeeSchedule Integer -> Word -> EVM () -> EVM () accessMemoryWord fees x = accessMemoryRange fees x 32 copyBytesToMemory @@ -2234,11 +2284,11 @@ vm <- get let Just this = - preview (env . contracts . ix (view (state . codeContract) vm)) vm + currentContract vm pure Trace { _traceData = x , _traceCodehash = view codehash this - , _traceOpIx = (view opIxMap this) Vector.! (view (state . pc) vm) + , _traceOpIx = (view opIxMap this) Vector.!? (view (state . pc) vm) } pushTrace :: TraceData -> EVM () @@ -2286,7 +2336,7 @@ stackOp1 :: (?op :: Word8) - => ((SymWord) -> Word) + => ((SymWord) -> Integer) -> ((SymWord) -> (SymWord)) -> EVM () stackOp1 cost f = @@ -2301,7 +2351,7 @@ stackOp2 :: (?op :: Word8) - => (((SymWord), (SymWord)) -> Word) + => (((SymWord), (SymWord)) -> Integer) -> (((SymWord), (SymWord)) -> (SymWord)) -> EVM () stackOp2 cost f = @@ -2315,7 +2365,7 @@ stackOp3 :: (?op :: Word8) - => (((SymWord), (SymWord), (SymWord)) -> Word) + => (((SymWord), (SymWord), (SymWord)) -> Integer) -> (((SymWord), (SymWord), (SymWord)) -> (SymWord)) -> EVM () stackOp3 cost f = @@ -2334,13 +2384,15 @@ theCode <- use (state . code) self <- use (state . codeContract) theCodeOps <- use (env . contracts . ix self . codeOps) + theOpIxMap <- use (env . contracts . ix self . opIxMap) if x < num (BS.length theCode) && BS.index theCode (num x) == 0x5b then - case RegularVector.find (\(i, op) -> i == num x && op == OpJumpdest) theCodeOps of - Nothing -> vmError BadJumpDestination - _ -> do - state . stack .= xs - state . pc .= num x + if OpJumpdest == snd (theCodeOps RegularVector.! (theOpIxMap Vector.! num x)) + then do + state . stack .= xs + state . pc .= num x + else + vmError BadJumpDestination else vmError BadJumpDestination opSize :: Word8 -> Int @@ -2507,12 +2559,14 @@ -- Gas cost function for CALL, transliterated from the Yellow Paper. costOfCall - :: FeeSchedule Word + :: FeeSchedule Integer -> Bool -> Word -> Word -> Word - -> (Word, Word) -costOfCall (FeeSchedule {..}) recipientExists xValue availableGas xGas = + -> (Integer, Integer) +costOfCall (FeeSchedule {..}) recipientExists xValue availableGas' xGas' = (c_gascap + c_extra, c_callgas) where + availableGas = num availableGas' + xGas = num xGas' c_extra = num g_call + c_xfer + c_new c_xfer = @@ -2530,17 +2584,18 @@ -- Gas cost of create, including hash cost if needed costOfCreate - :: FeeSchedule Word - -> Word -> Word -> (Word, Word) -costOfCreate (FeeSchedule {..}) availableGas hashSize = + :: FeeSchedule Integer + -> Word -> Word -> (Integer, Integer) +costOfCreate (FeeSchedule {..}) availableGas' hashSize = (createCost + initGas, initGas) where + availableGas = num availableGas' createCost = g_create + hashCost - hashCost = g_sha3word * ceilDiv (hashSize) 32 + hashCost = g_sha3word * ceilDiv (num hashSize) 32 initGas = allButOne64th (availableGas - createCost) -- Gas cost of precompiles -costOfPrecompile :: FeeSchedule Word -> Addr -> Buffer -> Word +costOfPrecompile :: FeeSchedule Integer -> Addr -> Buffer -> Integer costOfPrecompile (FeeSchedule {..}) precompileAddr input = case precompileAddr of -- ECRECOVER @@ -2584,7 +2639,7 @@ _ -> error ("unimplemented precompiled contract " ++ show precompileAddr) -- Gas cost of memory expansion -memoryCost :: FeeSchedule Word -> Word -> Word +memoryCost :: FeeSchedule Integer -> Integer -> Integer memoryCost FeeSchedule{..} byteCount = let wordCount = ceilDiv byteCount 32 @@ -2592,32 +2647,6 @@ quadraticCost = div (wordCount * wordCount) 512 in linearCost + quadraticCost - --- * Uninterpreted functions - -symSHA256N :: SInteger -> SInteger -> SWord 256 -symSHA256N = uninterpret "sha256" - -symkeccakN :: SInteger -> SInteger -> SWord 256 -symkeccakN = uninterpret "keccak" - -toSInt :: [SWord 8] -> SInteger -toSInt bs = sum $ zipWith (\a i -> sFromIntegral a * 256 ^ i) bs [0..] - --- | Although we'd like to define this directly as an uninterpreted function, --- we cannot because [a] is not a symbolic type. We must convert the list into a suitable --- symbolic type first. The only important property of this conversion is that it is injective. --- We embedd the bytestring as a pair of symbolic integers, this is a fairly easy solution. -symkeccak' :: [SWord 8] -> SWord 256 -symkeccak' bytes = case length bytes of - 0 -> literal $ toSizzle $ keccak "" - n -> symkeccakN (num n) (toSInt bytes) - -symSHA256 :: [SWord 8] -> [SWord 8] -symSHA256 bytes = case length bytes of - 0 -> litBytes $ BS.pack $ BA.unpack $ (Crypto.hash BS.empty :: Digest SHA256) - n -> toBytes $ symSHA256N (num n) (toSInt bytes) - -- * Arithmetic diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs --- a/src/EVM/ABI.hs +++ b/src/EVM/ABI.hs @@ -26,6 +26,7 @@ -} {-# Language StrictData #-} +{-# Language DataKinds #-} module EVM.ABI ( AbiValue (..) @@ -46,28 +47,31 @@ , emptyAbi , encodeAbiValue , decodeAbiValue + , decodeStaticArgs + , formatString , parseTypeName , makeAbiValue , parseAbiValue , selector ) where -import EVM.Keccak (abiKeccak) import EVM.Types import Control.Monad (replicateM, replicateM_, forM_, void) -import Data.Binary.Get (Get, runGet, label, getWord8, getWord32be, skip) +import Data.Binary.Get (Get, runGet, runGetOrFail, label, getWord8, getWord32be, skip) import Data.Binary.Put (Put, runPut, putWord8, putWord32be) import Data.Bits (shiftL, shiftR, (.&.)) import Data.ByteString (ByteString) import Data.DoubleWord (Word256, Int256, signedWord) import Data.Functor (($>)) import Data.Monoid ((<>)) -import Data.Text (Text, pack) -import Data.Text.Encoding (encodeUtf8) -import Data.Vector (Vector) +import Data.Text (Text, pack, unpack) +import Data.Text.Encoding (encodeUtf8, decodeUtf8') +import Data.Vector (Vector, toList) import Data.Word (Word32) import Data.List (intercalate) +import Data.SBV (SWord, fromBytes, sFromIntegral, literal) +import Data.Maybe import GHC.Generics import Test.QuickCheck hiding ((.&.), label) @@ -104,7 +108,7 @@ show (AbiBool b) = if b then "true" else "false" show (AbiBytes _ b) = show (ByteStringS b) show (AbiBytesDynamic b) = show (ByteStringS b) - show (AbiString s) = show s + show (AbiString s) = formatString s show (AbiArrayDynamic _ v) = "[" ++ intercalate ", " (show <$> Vector.toList v) ++ "]" show (AbiArray _ _ v) = @@ -112,6 +116,12 @@ show (AbiTuple v) = "(" ++ intercalate ", " (show <$> Vector.toList v) ++ ")" +formatString :: ByteString -> String +formatString bs = + case decodeUtf8' (fst (BS.spanEnd (== 0) bs)) of + Right s -> "\"" <> unpack s <> "\"" + Left _ -> "❮utf8 decode failed❯: " <> (show $ ByteStringS bs) + data AbiType = AbiUIntType Int | AbiIntType Int @@ -183,7 +193,7 @@ AbiIntType n -> asUInt n (AbiInt n) AbiAddressType -> asUInt 256 AbiAddress - AbiBoolType -> asUInt 256 (AbiBool . (== (1 :: Int))) + AbiBoolType -> asUInt 256 (AbiBool . (> (0 :: Integer))) AbiBytesType n -> AbiBytes n <$> getBytesWith256BitPadding n @@ -194,8 +204,9 @@ >>= label "bytes data" . getBytesWith256BitPadding) AbiStringType -> do - AbiBytesDynamic x <- getAbi AbiBytesDynamicType - pure (AbiString x) + AbiString <$> + (label "string length prefix" getWord256 + >>= label "string data" . getBytesWith256BitPadding) AbiArrayType n t' -> AbiArray n t' <$> getAbiSeq n (repeat t') @@ -497,17 +508,17 @@ makeAbiValue :: AbiType -> String -> AbiValue makeAbiValue typ str = case readP_to_S (parseAbiValue typ) str of - [] -> error "could not parse abi arguments" - ((val,_):_) -> val + [(val,"")] -> val + _ -> error $ "could not parse abi argument: " ++ str ++ " : " ++ show typ parseAbiValue :: AbiType -> ReadP AbiValue -parseAbiValue (AbiUIntType n) = do W256 w256 <- readS_to_P reads - return $ AbiUInt n w256 -parseAbiValue (AbiIntType n) = do W256 w256 <- readS_to_P reads - return $ AbiInt n (num w256) +parseAbiValue (AbiUIntType n) = do W256 w <- readS_to_P reads + return $ AbiUInt n w +parseAbiValue (AbiIntType n) = do W256 w <- readS_to_P reads + return $ AbiInt n (num w) parseAbiValue AbiAddressType = AbiAddress <$> readS_to_P reads -parseAbiValue AbiBoolType = (do W256 w256 <- readS_to_P reads - return $ AbiBool (w256 /= 0)) +parseAbiValue AbiBoolType = (do W256 w <- readS_to_P reads + 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 @@ -529,6 +540,12 @@ skipSpaces return a) `sepBy` (char ',')) +decodeStaticArgs :: Buffer -> [SWord 256] +decodeStaticArgs buffer = let + bs = case buffer of + ConcreteBuffer b -> litBytes b + SymbolicBuffer b -> b + in fmap (\i -> fromBytes $ take 32 (drop (i*32) bs)) [0..((length bs) `div` 32 - 1)] -- A modification of 'arbitrarySizedBoundedIntegral' quickcheck library -- which takes the maxbound explicitly rather than relying on a Bounded instance. diff --git a/src/EVM/Concrete.hs b/src/EVM/Concrete.hs --- a/src/EVM/Concrete.hs +++ b/src/EVM/Concrete.hs @@ -5,12 +5,11 @@ import Prelude hiding (Word) -import EVM.Keccak (keccak) import EVM.RLP -import EVM.Types (Addr, W256 (..), num, word, padRight, word160Bytes, word256Bytes, Buffer) +import EVM.Types import Control.Lens ((^?), ix) -import Data.Bits (Bits (..), FiniteBits (..), shiftL, shiftR) +import Data.Bits (Bits (..), shiftL, shiftR) import Data.ByteString (ByteString) import Data.Maybe (fromMaybe) import Data.Semigroup ((<>)) @@ -36,21 +35,7 @@ let bs' = BS.take size (BS.drop offset bs) in bs' <> BS.replicate (size - BS.length bs') 0 --- | This type can give insight into the provenance of a term -data Whiff = Dull - | FromKeccak ByteString - | Var String - | FromBytes Buffer - | InfixBinOp String Whiff Whiff - | BinOp String Whiff Whiff - | UnOp String Whiff - deriving Show -w256 :: W256 -> Word -w256 = C Dull - -data Word = C Whiff W256 --maybe to remove completely in the future - wordValue :: Word -> W256 wordValue (C _ x) = x @@ -76,12 +61,14 @@ readMemoryWord :: Word -> ByteString -> Word readMemoryWord (C _ i) m = + if i > (num $ BS.length m) then 0 else let go !a (-1) = a go !a !n = go (a + shiftL (num $ readByteOrZero (num i + n) m) (8 * (31 - n))) (n - 1) + w = go (0 :: W256) (31 :: Int) in {-# SCC "readMemoryWord" #-} - w256 $ go (0 :: W256) (31 :: Int) + C (Literal w) w readMemoryWord32 :: Word -> ByteString -> Word readMemoryWord32 (C _ i) m = @@ -100,81 +87,8 @@ setMemoryByte (C _ i) x = writeMemory (BS.singleton x) 1 0 (num i) -readBlobWord :: Word -> ByteString -> Word -readBlobWord (C _ i) x = - if i > num (BS.length x) - then 0 - else w256 (wordAt (num i) x) - -blobSize :: ByteString -> Word -blobSize x = w256 (num (BS.length x)) - keccakBlob :: ByteString -> Word -keccakBlob x = C (FromKeccak x) (keccak x) - -instance Show Word where - show (C Dull x) = show x - show (C (Var var) x) = var ++ ": " ++ show x - show (C (InfixBinOp symbol x y) z) = show x ++ symbol ++ show y ++ ": " ++ show z - show (C (BinOp symbol x y) z) = symbol ++ show x ++ show y ++ ": " ++ show z - show (C (UnOp symbol x) z) = symbol ++ show x ++ ": " ++ show z - show (C whiff x) = show whiff ++ ": " ++ show x - -instance Read Word where - readsPrec n s = - case readsPrec n s of - [(x, r)] -> [(C Dull x, r)] - _ -> [] - -instance Bits Word where - (C _ x) .&. (C _ y) = w256 (x .&. y) - (C _ x) .|. (C _ y) = w256 (x .|. y) - (C _ x) `xor` (C _ y) = w256 (x `xor` y) - complement (C _ x) = w256 (complement x) - shift (C _ x) i = w256 (shift x i) - rotate (C _ x) i = w256 (rotate x i) - bitSize (C _ x) = bitSize x - bitSizeMaybe (C _ x) = bitSizeMaybe x - isSigned (C _ x) = isSigned x - testBit (C _ x) = testBit x - bit i = w256 (bit i) - popCount (C _ x) = popCount x - -instance FiniteBits Word where - finiteBitSize (C _ x) = finiteBitSize x - countLeadingZeros (C _ x) = countLeadingZeros x - countTrailingZeros (C _ x) = countTrailingZeros x - -instance Bounded Word where - minBound = w256 minBound - maxBound = w256 maxBound - -instance Eq Word where - (C _ x) == (C _ y) = x == y - -instance Enum Word where - toEnum i = w256 (toEnum i) - fromEnum (C _ x) = fromEnum x - -instance Integral Word where - quotRem (C _ x) (C _ y) = - let (a, b) = quotRem x y - in (w256 a, w256 b) - toInteger (C _ x) = toInteger x - -instance Num Word where - (C _ x) + (C _ y) = w256 (x + y) - (C _ x) * (C _ y) = w256 (x * y) - abs (C _ x) = w256 (abs x) - signum (C _ x) = w256 (signum x) - fromInteger x = w256 (fromInteger x) - negate (C _ x) = w256 (negate x) - -instance Real Word where - toRational (C _ x) = toRational x - -instance Ord Word where - compare (C _ x) (C _ y) = compare x y +keccakBlob x = C (FromKeccak (ConcreteBuffer x)) (keccak x) -- Copied from the standard library just to get specialization. -- We also use bit operations instead of modulo and multiply. diff --git a/src/EVM/Dapp.hs b/src/EVM/Dapp.hs --- a/src/EVM/Dapp.hs +++ b/src/EVM/Dapp.hs @@ -1,54 +1,70 @@ {-# Language TemplateHaskell #-} +{-# Language OverloadedStrings #-} module EVM.Dapp where -import EVM (Trace, traceCodehash, traceOpIx) +import EVM (Trace, traceCodehash, traceOpIx, Env) import EVM.ABI (Event, AbiType) import EVM.Debug (srcMapCodePos) -import EVM.Keccak (abiKeccak) -import EVM.Solidity (SolcContract, CodeType (..), SourceCache, SrcMap) +import EVM.Solidity (SolcContract, CodeType (..), SourceCache (..), SrcMap, Method) import EVM.Solidity (contractName, methodInputs) import EVM.Solidity (runtimeCodehash, creationCodehash, abiMap) -import EVM.Solidity (runtimeSrcmap, creationSrcmap, eventMap) -import EVM.Solidity (methodSignature, contractAst, astIdMap, astSrcMap) -import EVM.Types (W256) +import EVM.Solidity (runtimeSrcmap, sourceAsts, creationSrcmap, eventMap) +import EVM.Solidity (methodSignature, astIdMap, astSrcMap) +import EVM.Types (W256, abiKeccak) import Data.Aeson (Value) -import Data.Text (Text, isPrefixOf, pack) +import Data.Bifunctor (first) +import Data.Text (Text, isPrefixOf, pack, unpack) import Data.Text.Encoding (encodeUtf8) -import Data.Map (Map) +import Data.Map (Map, toList) import Data.Monoid ((<>)) +import Data.Maybe (isJust, fromJust) import Data.Word (Word32) import Control.Applicative ((<$>)) import Control.Arrow ((>>>)) import Control.Lens -import qualified Data.Map as Map +import qualified Data.Map as Map +import qualified Data.Sequence as Seq +import qualified Text.Regex.TDFA as Regex data DappInfo = DappInfo { _dappRoot :: FilePath , _dappSolcByName :: Map Text SolcContract , _dappSolcByHash :: Map W256 (CodeType, SolcContract) , _dappSources :: SourceCache - , _dappUnitTests :: [(Text, [(Text, [AbiType])])] + , _dappUnitTests :: [(Text, [(Test, [AbiType])])] + , _dappAbiMap :: Map Word32 Method , _dappEventMap :: Map W256 Event , _dappAstIdMap :: Map Int Value , _dappAstSrcMap :: SrcMap -> Maybe Value } +data DappContext = DappContext + { _contextInfo :: DappInfo + , _contextEnv :: Env + } + +data Test = ConcreteTest Text | SymbolicTest Text + makeLenses ''DappInfo +makeLenses ''DappContext +instance Show Test where + show t = unpack $ extractSig t + dappInfo :: FilePath -> Map Text SolcContract -> SourceCache -> DappInfo dappInfo root solcByName sources = let solcs = Map.elems solcByName - astIds = astIdMap (map (view contractAst) solcs) + astIds = astIdMap $ snd <$> toList (view sourceAsts sources) in DappInfo { _dappRoot = root - , _dappUnitTests = findUnitTests ("test" `isPrefixOf`) solcs + , _dappUnitTests = findAllUnitTests solcs , _dappSources = sources , _dappSolcByName = solcByName , _dappSolcByHash = @@ -59,35 +75,78 @@ (f runtimeCodehash Runtime) (f creationCodehash Creation) - , _dappEventMap = - -- Sum up the event ABI maps from all the contracts. - mconcat (map (view eventMap) solcs) + -- Sum up the ABI maps from all the contracts. + , _dappAbiMap = mconcat (map (view abiMap) solcs) + , _dappEventMap = mconcat (map (view eventMap) solcs) , _dappAstIdMap = astIds , _dappAstSrcMap = astSrcMap astIds } +emptyDapp :: DappInfo +emptyDapp = dappInfo "" mempty (SourceCache mempty mempty mempty) + +-- Dapp unit tests are detected by searching within abi methods +-- that begin with "test" or "prove", that are in a contract with +-- the "IS_TEST()" abi marker, for a given regular expression. +-- +-- The regex is matched on the full test method name, including path +-- and contract, i.e. "path/to/file.sol:TestContract.test_name()". +-- +-- Tests beginning with "test" are interpreted as concrete tests, whereas +-- tests beginning with "prove" are interpreted as symbolic tests. + unitTestMarkerAbi :: Word32 unitTestMarkerAbi = abiKeccak (encodeUtf8 "IS_TEST()") -findUnitTests :: (Text -> Bool) -> ([SolcContract] -> [(Text, [(Text, [AbiType])])]) -findUnitTests matcher = +findAllUnitTests :: [SolcContract] -> [(Text, [(Test, [AbiType])])] +findAllUnitTests = findUnitTests ".*:.*\\.(test|prove).*" + +mkTest :: Text -> Maybe Test +mkTest sig + | "test" `isPrefixOf` sig = Just (ConcreteTest sig) + | "prove" `isPrefixOf` sig = Just (SymbolicTest sig) + | otherwise = Nothing + +regexMatches :: Text -> Text -> Bool +regexMatches regexSource = + let + compOpts = + Regex.defaultCompOpt { Regex.lastStarGreedy = True } + execOpts = + Regex.defaultExecOpt { Regex.captureGroups = False } + regex = Regex.makeRegexOpts compOpts execOpts (unpack regexSource) + in + Regex.matchTest regex . Seq.fromList . unpack + +findUnitTests :: Text -> ([SolcContract] -> [(Text, [(Test, [AbiType])])]) +findUnitTests match = concatMap $ \c -> case preview (abiMap . ix unitTestMarkerAbi) c of Nothing -> [] Just _ -> - let testNames = unitTestMethodsFiltered matcher c - in ([(view contractName c, testNames) | not (null testNames)]) + let testNames = unitTestMethodsFiltered (regexMatches match) c + in [(view contractName c, testNames) | not (null testNames)] -unitTestMethodsFiltered :: (Text -> Bool) -> (SolcContract -> [(Text, [AbiType])]) -unitTestMethodsFiltered matcher c = filter (matcher . fst) $ unitTestMethods c +unitTestMethodsFiltered :: (Text -> Bool) -> (SolcContract -> [(Test, [AbiType])]) +unitTestMethodsFiltered matcher c = + let + testName method = (view contractName c) <> "." <> (extractSig (fst method)) + in + filter (matcher . testName) (unitTestMethods c) -unitTestMethods :: SolcContract -> [(Text, [AbiType])] -unitTestMethods = view abiMap - >>> Map.elems - >>> map (\f -> (view methodSignature f, - snd <$> view methodInputs f)) +unitTestMethods :: SolcContract -> [(Test, [AbiType])] +unitTestMethods = + view abiMap + >>> Map.elems + >>> map (\f -> (mkTest $ view methodSignature f, snd <$> view methodInputs f)) + >>> filter (isJust . fst) + >>> fmap (first fromJust) +extractSig :: Test -> Text +extractSig (ConcreteTest sig) = sig +extractSig (SymbolicTest sig) = sig + traceSrcMap :: DappInfo -> Trace -> Maybe SrcMap traceSrcMap dapp trace = let @@ -97,9 +156,9 @@ Nothing -> Nothing Just (Creation, solc) -> - preview (creationSrcmap . ix i) solc + i >>= \i' -> preview (creationSrcmap . ix i') solc Just (Runtime, solc) -> - preview (runtimeSrcmap . ix i) solc + i >>= \i' -> preview (runtimeSrcmap . ix i') solc showTraceLocation :: DappInfo -> Trace -> Either Text Text showTraceLocation dapp trace = diff --git a/src/EVM/Debug.hs b/src/EVM/Debug.hs --- a/src/EVM/Debug.hs +++ b/src/EVM/Debug.hs @@ -15,7 +15,7 @@ import Text.PrettyPrint.ANSI.Leijen -data Mode = Debug | Run deriving (Eq, Show) +data Mode = Debug | Run | JsonTrace deriving (Eq, Show) object :: [(Doc, Doc)] -> Doc object xs = @@ -101,34 +101,6 @@ -- Just x -> Just x -- Nothing -> -- vm ^? env . solcByCreationHash . ix hash - --- currentSolc :: VM -> Maybe SolcContract --- currentSolc vm = --- let --- c = vm ^?! env . contracts . ix (vm ^. state . contract) --- theCodehash = view codehash c --- in --- case vm ^? env . solcByRuntimeHash . ix theCodehash of --- Just x -> --- Just x --- Nothing -> --- vm ^? env . solcByCreationHash . ix theCodehash - --- currentSrcMap :: VM -> Maybe SrcMap --- currentSrcMap vm = --- let --- c = vm ^?! env . contracts . ix (vm ^. state . contract) --- theOpIx = (c ^. opIxMap) Vector.! (vm ^. state . pc) --- theCodehash = view codehash c --- (isRuntime, solc) = --- case vm ^? env . solcByRuntimeHash . ix theCodehash of --- Just x -> --- (True, Just x) --- Nothing -> --- (False, vm ^? env . solcByCreationHash . ix theCodehash) --- srcmapLens = if isRuntime then runtimeSrcmap else creationSrcmap --- in --- join (fmap (preview (srcmapLens . ix theOpIx)) solc) srcMapCodePos :: SourceCache -> SrcMap -> Maybe (Text, Int) srcMapCodePos cache sm = diff --git a/src/EVM/Dev.hs b/src/EVM/Dev.hs --- a/src/EVM/Dev.hs +++ b/src/EVM/Dev.hs @@ -1,11 +1,17 @@ +{-# LANGUAGE DeriveAnyClass #-} module EVM.Dev where import System.Directory +import Prelude hiding (Word) + +import EVM.Types import EVM.Dapp import EVM.Solidity import EVM.UnitTest +import EVM.Symbolic +import EVM hiding (path) import qualified EVM.Fetch import qualified EVM.TTY import qualified EVM.Emacs @@ -14,31 +20,37 @@ import qualified EVM.Stepper import qualified EVM.VMTest as VMTest +import Data.SBV hiding (Word) +import qualified Data.Aeson as JSON +import Options.Generic +import Data.SBV.Trans.Control import Control.Monad.State.Strict (execStateT) -import Data.Text (isPrefixOf) import qualified Data.Map as Map import qualified Data.ByteString.Lazy as LazyByteString - -concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] -concatMapM op = foldr f (pure []) - where f x xs = do x <- op x; if null x then xs else do xs <- xs; pure $ x++xs +import qualified Data.ByteString as BS +import qualified Data.ByteString.Lazy.Char8 as B +import qualified Control.Monad.State.Class as State +import Control.Monad.State.Strict (runState, liftIO, StateT, get) +import Control.Lens hiding (op, passing) +import Control.Monad.Operational (ProgramViewT(..), ProgramView) +import qualified Control.Monad.Operational as Operational loadDappInfo :: String -> String -> IO DappInfo loadDappInfo path file = withCurrentDirectory path $ readSolc file >>= \case - Just (contractMap, cache) -> - pure (dappInfo "." contractMap cache) + Just (contractMap, sourcecache) -> + pure (dappInfo "." contractMap sourcecache) _ -> error "nope, sorry" ghciTest :: String -> String -> Maybe String -> IO [Bool] -ghciTest root path state = +ghciTest root path statePath = withCurrentDirectory root $ do loadFacts <- - case state of + case statePath of Nothing -> pure id Just repoPath -> do @@ -50,17 +62,21 @@ { oracle = EVM.Fetch.zero , verbose = Nothing , maxIter = Nothing + , smtTimeout = Nothing + , smtState = Nothing + , solver = Nothing , match = "" , fuzzRuns = 100 , replay = Nothing , vmModifier = loadFacts + , dapp = emptyDapp , testParams = params } readSolc path >>= \case - Just (contractMap, cache) -> do - let unitTests = findUnitTests ("test" `isPrefixOf`) (Map.elems contractMap) - results <- concatMapM (runUnitTestContract opts contractMap cache) unitTests + Just (contractMap, _) -> do + let unitTests = findAllUnitTests (Map.elems contractMap) + results <- runSMT $ query $ concatMapM (runUnitTestContract opts contractMap) unitTests let (passing, _) = unzip results pure passing @@ -71,9 +87,9 @@ runBCTest (name, x) = do let vm0 = VMTest.vmForCase x putStr (name ++ " ") - result <- - execStateT (EVM.Stepper.interpret EVM.Fetch.zero EVM.Stepper.execFully) vm0 - ok <- VMTest.checkExpectation False x result + out <- + execStateT (EVM.Stepper.interpret EVM.Fetch.zero EVM.Stepper.execFully) vm0 + ok <- VMTest.checkExpectation False x out putStrLn (if ok then "ok" else "") return ok @@ -88,10 +104,10 @@ mapM_ runBCTest (Map.toList allTests) ghciTty :: String -> String -> Maybe String -> IO () -ghciTty root path state = +ghciTty root path statePath = withCurrentDirectory root $ do loadFacts <- - case state of + case statePath of Nothing -> pure id Just repoPath -> do @@ -102,10 +118,15 @@ testOpts = UnitTestOptions { oracle = EVM.Fetch.zero , verbose = Nothing + , maxIter = Nothing + , smtTimeout = Nothing + , smtState = Nothing + , solver = Nothing , match = "" , fuzzRuns = 100 , replay = Nothing , vmModifier = loadFacts + , dapp = emptyDapp , testParams = params } EVM.TTY.main testOpts root path @@ -116,3 +137,110 @@ foo :: IO () foo = ghciEmacs + +data VMTrace = + VMTrace + { pc :: Int + , op :: Int + , stack :: [Word] + , memSize :: Int + , depth :: Int + , gas :: Word + } deriving (Generic, JSON.ToJSON) + +data VMTraceResult = + VMTraceResult + { output :: String + , gasUsed :: Word + } deriving (Generic, JSON.ToJSON) + +getOp :: VM -> Word8 +getOp vm = + if BS.length (view (state . code) vm) <= view (state . EVM.pc) vm + then 0 + else fromIntegral $ BS.index (view (state . code) vm) (view (state . EVM.pc) vm) + + +vmtrace :: VM -> VMTrace +vmtrace vm = + let + -- Convenience function to access parts of the current VM state. + -- Arcane type signature needed to avoid monomorphism restriction. + the :: (b -> VM -> Const a VM) -> ((a -> Const a a) -> b) -> a + the f g = view (f . g) vm + memsize = the state memorySize + in VMTrace { pc = the state EVM.pc + , op = num $ getOp vm + , gas = the state EVM.gas + , memSize = memsize + -- increment to match geth format + , depth = 1 + length (view frames vm) + -- reverse to match geth format + , stack = reverse $ forceLit <$> the state EVM.stack + } + +vmres :: VM -> VMTraceResult +vmres vm = + let + gasUsed' = view (tx . txgaslimit) vm - view (state . EVM.gas) vm + res = case view result vm of + Just (VMSuccess out) -> forceBuffer out + Just (VMFailure (Revert out)) -> out + _ -> mempty + in VMTraceResult + -- more oddities to comply with geth + { output = drop 2 $ show $ ByteStringS res + , gasUsed = gasUsed' + } + +interpretWithTrace :: EVM.Fetch.Fetcher -> EVM.Stepper.Stepper a -> StateT VM IO a +interpretWithTrace fetcher = + eval . Operational.view + + where + eval + :: ProgramView EVM.Stepper.Action a + -> StateT VM IO a + + eval (Return x) = do + vm <- get + liftIO $ B.putStrLn $ JSON.encode $ vmres vm + pure x + + eval (action :>>= k) = do + vm <- get + case action of + EVM.Stepper.Run -> do + -- Have we reached the final result of this action? + use result >>= \case + Just _ -> do + -- Yes, proceed with the next action. + interpretWithTrace fetcher (k vm) + Nothing -> do + liftIO $ B.putStrLn $ JSON.encode $ vmtrace vm + + -- No, keep performing the current action + State.state (runState exec1) + interpretWithTrace fetcher (EVM.Stepper.run >>= k) + + -- Stepper wants to keep executing? + EVM.Stepper.Exec -> do + -- Have we reached the final result of this action? + use result >>= \case + Just r -> do + -- Yes, proceed with the next action. + interpretWithTrace fetcher (k r) + Nothing -> do + liftIO $ B.putStrLn $ JSON.encode $ vmtrace vm + + -- No, keep performing the current action + State.state (runState exec1) + interpretWithTrace fetcher (EVM.Stepper.exec >>= k) + EVM.Stepper.Wait q -> + do m <- liftIO (fetcher q) + State.state (runState m) >> interpretWithTrace fetcher (k ()) + EVM.Stepper.Ask _ -> + error "cannot make choices with this interpretWithTraceer" + 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 @@ -21,7 +21,6 @@ import Data.SBV hiding (Word, output) import EVM import EVM.ABI -import EVM.Concrete import EVM.Symbolic import EVM.Dapp import EVM.Debug (srcMapCodePos) @@ -86,10 +85,8 @@ eval (action Operational.:>>= k) = case action of - -- Stepper wants to keep executing? Stepper.Exec -> do - let -- When pausing during exec, we should later restart -- the exec with the same continuation. @@ -420,7 +417,7 @@ sexp = id instance SDisplay Storage where - sexp (Symbolic _) = error "idk" + sexp (Symbolic _ _) = error "idk" sexp (Concrete d) = sexp d instance SDisplay VM where @@ -521,10 +518,14 @@ { oracle = Fetch.zero , verbose = Nothing , maxIter = Nothing + , smtTimeout = Nothing + , smtState = Nothing + , solver = Nothing , match = "" , fuzzRuns = 100 , replay = Nothing , vmModifier = id + , dapp = emptyDapp , testParams = params } @@ -538,13 +539,14 @@ script = do Stepper.evm . pushTrace . EntryTrace $ "test " <> testName <> " (" <> contractPath <> ")" - initializeUnitTest opts + initializeUnitTest opts testContract void (runUnitTest opts testName (AbiTuple mempty)) ui0 = UiVmState { _uiVm = vm0 , _uiVmNextStep = script , _uiVmSolc = Just testContract + , _uiVmDapp = Nothing , _uiVmStepCount = 0 , _uiVmFirstState = undefined , _uiVmFetcher = oracle diff --git a/src/EVM/Facts.hs b/src/EVM/Facts.hs --- a/src/EVM/Facts.hs +++ b/src/EVM/Facts.hs @@ -36,10 +36,9 @@ ) where import EVM (VM, Contract, Cache) -import EVM.Concrete (Word) -import EVM.Symbolic (litWord, SymWord, forceLit) +import EVM.Symbolic (litWord, forceLit) import EVM (balance, nonce, storage, bytecode, env, contracts, contract, state, cache, fetched) -import EVM.Types (Addr) +import EVM.Types (Addr, Word, SymWord) import qualified EVM @@ -121,7 +120,7 @@ storageFacts :: Addr -> Contract -> [Fact] storageFacts a x = case view storage x of - EVM.Symbolic _ -> [] + EVM.Symbolic _ _ -> [] EVM.Concrete s -> map f (Map.toList s) where f :: (Word, SymWord) -> Fact diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -6,10 +6,9 @@ import Prelude hiding (Word) -import EVM.Types (Addr, W256, hexText) -import EVM.Concrete (Word, w256) +import EVM.Types (Addr, w256, W256, hexText, Word) import EVM.Symbolic (litWord) -import EVM (EVM, Contract, Block, StorageModel, initialContract, nonce, balance, external) +import EVM (IsUnique(..), EVM, Contract, Block, initialContract, nonce, balance, external) import qualified EVM.FeeSchedule as FeeSchedule import qualified EVM @@ -79,31 +78,31 @@ x <- case q of QueryCode addr -> do m <- f (rpc "eth_getCode" [toRPC addr, toRPC n]) - return $ hexText <$> view _String <$> m + return $ hexText . view _String <$> m QueryNonce addr -> do m <- f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n]) - return $ readText <$> view _String <$> m + return $ readText . view _String <$> m QueryBlock -> do m <- f (rpc "eth_getBlockByNumber" [toRPC n, toRPC False]) return $ m >>= parseBlock QueryBalance addr -> do m <- f (rpc "eth_getBalance" [toRPC addr, toRPC n]) - return $ readText <$> view _String <$> m + return $ readText . view _String <$> m QuerySlot addr slot -> do m <- f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n]) - return $ readText <$> view _String <$> m + return $ readText . view _String <$> m QueryChainId -> do m <- f (rpc "eth_chainId" [toRPC n]) - return $ readText <$> view _String <$> m + return $ readText . view _String <$> m return x parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block -parseBlock json = do - coinbase <- readText <$> json ^? key "miner" . _String - timestamp <- litWord <$> readText <$> json ^? key "timestamp" . _String - number <- readText <$> json ^? key "number" . _String - difficulty <- readText <$> json ^? key "difficulty" . _String +parseBlock j = do + coinbase <- readText <$> j ^? key "miner" . _String + timestamp <- litWord . readText <$> j ^? key "timestamp" . _String + number <- readText <$> j ^? key "number" . _String + difficulty <- readText <$> j ^? key "difficulty" . _String -- default codesize, default gas limit, default feescedule return $ EVM.Block coinbase timestamp number difficulty 0xffffffff 0xffffffff FeeSchedule.istanbul @@ -156,11 +155,14 @@ (\s -> fetchSlotWithSession n url s addr slot) http :: BlockNumber -> Text -> Fetcher -http n url = oracle Nothing (Just (n, url)) EVM.ConcreteS True +http n url = oracle Nothing (Just (n, url)) True +zero :: Fetcher +zero = oracle Nothing Nothing True + -- smtsolving + (http or zero) -oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> StorageModel -> Bool -> Fetcher -oracle smtstate info model ensureConsistency q = do +oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher +oracle smtstate info ensureConsistency q = do case q of EVM.PleaseAskSMT branchcondition pathconditions continue -> case smtstate of @@ -172,7 +174,7 @@ -- if we are using a symbolic storage model, -- we generate a new array to the fetched contract here - EVM.PleaseFetchContract addr continue -> do + EVM.PleaseFetchContract addr model continue -> do contract <- case info of Nothing -> return $ Just $ initialContract (EVM.RuntimeCode mempty) Just (n, url) -> fetchContractFrom n url addr @@ -180,19 +182,35 @@ Just x -> case model of EVM.ConcreteS -> return $ continue x EVM.InitialS -> return $ continue $ x - & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 []) + & set EVM.storage (EVM.Symbolic [] $ SBV.sListArray 0 []) EVM.SymbolicS -> case smtstate of Nothing -> return (continue $ x - & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 [])) + & set EVM.storage (EVM.Symbolic [] $ SBV.sListArray 0 [])) Just state -> flip runReaderT state $ SBV.runQueryT $ do store <- freshArray_ Nothing return $ continue $ x - & set EVM.storage (EVM.Symbolic store) + & set EVM.storage (EVM.Symbolic [] store) Nothing -> error ("oracle error: " ++ show q) - --- for other queries (there's only slot left right now) we default to zero or http + EVM.PleaseMakeUnique val pathconditions continue -> + case smtstate of + Nothing -> return $ continue Multiple + Just state -> flip runReaderT state $ SBV.runQueryT $ do + constrain $ sAnd $ pathconditions <> [val .== val] -- dummy proposition just to make sure `val` is defined when we do `getValue` later. + checkSat >>= \case + Sat -> do + val' <- getValue val + s <- checksat (val ./= literal val') + case s of + Unsat -> pure $ continue $ Unique val' + _ -> pure $ continue Multiple + Unsat -> pure $ continue InconsistentU + Unk -> pure $ continue TimeoutU + DSat _ -> error "unexpected DSAT" + + EVM.PleaseFetchSlot addr slot continue -> case info of Nothing -> return (continue 0) @@ -202,9 +220,6 @@ Nothing -> error ("oracle error: " ++ show q) -zero :: Fetcher -zero = oracle Nothing Nothing EVM.ConcreteS True - type Fetcher = EVM.Query -> IO (EVM ()) checksat :: SBool -> Query CheckSatResult @@ -235,8 +250,10 @@ Sat -> return EVM.Unknown -- Explore both branches in case of timeout Unk -> return EVM.Unknown + DSat _ -> error "checkBranch: unexpected SMT result" -- If the query times out, we simply explore both paths Unk -> return EVM.Unknown + DSat _ -> error "checkBranch: unexpected SMT result" checkBranch pathconds branchcondition True = do constrain pathconds @@ -250,6 +267,7 @@ Sat -> return $ EVM.Case False -- Assume the negated condition is still possible. Unk -> return $ EVM.Case False + DSat _ -> error "checkBranch: unexpected SMT result" -- Sat means its possible for condition to hold Sat -> -- is its negation also possible? checksat (sNot branchcondition) >>= \case @@ -259,6 +277,8 @@ Sat -> return EVM.Unknown -- Explore both branches in case of timeout Unk -> return EVM.Unknown + DSat _ -> error "checkBranch: unexpected SMT result" -- If the query times out, we simply explore both paths Unk -> return EVM.Unknown + DSat _ -> error "Internal Error: unexpected SMT result" diff --git a/src/EVM/Flatten.hs b/src/EVM/Flatten.hs --- a/src/EVM/Flatten.hs +++ b/src/EVM/Flatten.hs @@ -50,6 +50,13 @@ -- Define an alias for FGL graphs with text nodes and unlabeled edges. type FileGraph = Fgl.Gr Text () +-- | Get field either inside 'attributes' object (combined-json format) +-- or directly. +getAttribute :: Text -> Value -> Maybe Value +getAttribute s v = case preview (key "attributes" . key s) v of + Nothing -> preview (key s) v + Just r -> Just r + -- Given the AST of a source file, resolve all its imported paths. importsFrom :: Value -> [Text] importsFrom ast = @@ -63,11 +70,14 @@ -- and if so, return its resolved import path. resolveImport :: Value -> Maybe Text resolveImport node = - case preview (key "name") node of - Just (String "ImportDirective") -> - preview (key "attributes" . key "absolutePath" . _String) node + case preview (key "nodeType") node of + Just (String "ImportDirective") -> view _String <$> getAttribute "absolutePath" node _ -> - Nothing + case preview (key "name") node of + Just (String "ImportDirective") -> + view _String <$> getAttribute "absolutePath" node + _ -> + Nothing -- Now we just try to resolve import paths at all subnodes. in mapMaybe resolveImport allNodes @@ -112,10 +122,10 @@ Map.fromList $ indexed [ x | x <- xs, (snd x) `elem` xs' ] where - xs = mconcat $ fmap f $ Map.elems asts + xs = concatMap f $ Map.elems asts xs' = repeated $ fmap snd xs - scope = preview (key "attributes" . key "scope" . _Integer) - name = preview (key "attributes" . key "name" . _String) + scope x = getAttribute "scope" x >>= preview _Integer + name x = getAttribute "name" x >>= preview _String id' = preview (key "id" . _Integer) p x = (nodeIs "ContractDefinition" x || nodeIs "StructDefinition" x) && (fromJust' "no contract/struct scope" $ scope x) `elem` topScopeIds @@ -130,11 +140,11 @@ contractStructs :: [(Integer, (Integer, Text))] contractStructs = mconcat $ fmap f $ Map.elems asts where - scope = preview (key "attributes" . key "scope" . _Integer) - cname = preview (key "attributes" . key "canonicalName" . _String) + scope x = getAttribute "scope" x >>= preview _Integer + cname x = getAttribute "canonicalName" x >>= preview _String id' = preview (key "id" . _Integer) p x = (nodeIs "StructDefinition" x) - && (fromJust' "line:137 nested struct" $ scope x) `Map.member` contractsAndStructsToRename + && (fromJust' "nested struct" $ scope x) `Map.member` contractsAndStructsToRename f ast = [ let id'' = fromJust' "no id for nested struct" $ id' node @@ -194,8 +204,8 @@ putStrLn (unpack pragma) BS.putStr (mconcat sources) --- Construct a new Solidity version pragma for the highest mentioned version --- given a list of source file ASTs. +-- | Construct a new Solidity version pragma for the highest mentioned version +-- given a list of source file ASTs. maximalPragma :: [Value] -> Text maximalPragma asts = ( case mapMaybe versions asts of @@ -218,10 +228,8 @@ where isVersionPragma :: [Value] -> Bool - isVersionPragma = - \case - String "solidity" : _ -> True - _ -> False + isVersionPragma (String "solidity" : _) = True + isVersionPragma _ = False pragmaComponents :: Value -> [[Value]] pragmaComponents ast = components @@ -230,8 +238,9 @@ ps = filter (nodeIs "PragmaDirective") (universe ast) components :: [[Value]] - components = catMaybes $ fmap - ((fmap toList) . preview (key "attributes" . key "literals" . _Array)) + components = catMaybes $ + fmap + ((fmap toList) . (\x -> getAttribute "literals" x >>= preview _Array)) ps -- Simple way to combine many SemVer ranges. We don't actually @@ -272,6 +281,7 @@ isJust (preview (key "src") x) hasRightName = Just t == preview (key "name" . _String) x + || Just t == preview (key "nodeType" . _String) x stripImportsAndPragmas :: (ByteString, Int) -> Value -> (ByteString, Int) stripImportsAndPragmas bso ast = stripAstNodes bso ast p @@ -305,8 +315,8 @@ prefixContractAst castr cs bso ast = prefixAstNodes where bs = fst bso - refDec = preview (key "attributes" . key "referencedDeclaration" . _Integer) - name = preview (key "attributes" . key "name" . _String) + refDec x = getAttribute "referencedDeclaration" x >>= preview _Integer + name x = getAttribute "name" x >>= preview _String id' = preview (key "id" . _Integer) -- Is node top level defined type (contract/interface/struct) @@ -316,7 +326,7 @@ -- Is node identifier that is referencing top level defined type p' x = (nodeIs "Identifier" x || nodeIs "UserDefinedTypeName" x) - && (fromJust' "refDec of ident/userdef" $ refDec x) `Map.member` castr + && (isJust $ refDec x) && (fromJust' "refDec of ident/userdef" $ refDec x) `Map.member` castr -- Is node identifier that is referencing a struct nested in a top level -- defined contract/interface @@ -362,10 +372,8 @@ where (start, end) = sourceRange v - x :: Maybe (Int, Integer) - x = case preview (key "name" . _String) v of - Just t - | t `elem` ["ContractDefinition", "StructDefinition"] -> + f :: Text -> Maybe (Int, Integer) + f t | t `elem` ["ContractDefinition", "StructDefinition"] = let name' = encodeUtf8 $ fromJust' "no name for contract/struct" $ name v bs' = snd $ BS.splitAt (start + snd bso) bs @@ -374,12 +382,18 @@ + (BS.length name') in fmap ((,) pos) $ id' v - | t `elem` ["UserDefinedTypeName", "Identifier"] -> + | t `elem` ["UserDefinedTypeName", "Identifier"] = fmap ((,) end) $ refDec v - | otherwise -> + | otherwise = + error $ "internal error: not a contract reference: " ++ show t + + x :: Maybe (Int, Integer) + x = case preview (key "nodeType" . _String) v of + Just t -> f t + Nothing -> case preview (key "name" . _String) v of + Just t -> f t + Nothing -> error "internal error: not a contract reference" - Nothing -> - error "internal error: not a contract reference" -- Prefix a set of non-overlapping ranges from a bytestring -- by commenting them out. diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs --- a/src/EVM/Format.hs +++ b/src/EVM/Format.hs @@ -1,24 +1,29 @@ {-# Language DataKinds #-} -{-# LANGUAGE OverloadedStrings #-} +{-# Language ImplicitParams #-} +{-# Language TemplateHaskell #-} module EVM.Format where import Prelude hiding (Word) - -import EVM (VM, cheatCode, traceForest, traceData, Error (..)) -import EVM (Trace, TraceData (..), Log (..), Query (..), FrameContext (..)) -import EVM.Dapp (DappInfo, dappSolcByHash, dappSolcByName, showTraceLocation, dappEventMap) -import EVM.Concrete (Word (..), wordValue) -import EVM.Symbolic (maybeLitWord, len) -import EVM.Types (W256 (..), num, Buffer(..)) +import qualified EVM +import EVM.Dapp (DappInfo (..), dappSolcByHash, dappAbiMap, showTraceLocation, dappEventMap) +import EVM.Dapp (DappContext (..), contextInfo, contextEnv) +import EVM.Concrete ( wordValue ) +import EVM (VM, VMResult(..), cheatCode, traceForest, traceData, Error (..), result) +import EVM (Trace, TraceData (..), Log (..), Query (..), FrameContext (..), Storage(..)) +import EVM.SymExec +import EVM.Symbolic (len, litWord) +import EVM.Types (maybeLitWord, Word (..), Whiff(..), SymWord(..), W256 (..), num) +import EVM.Types (Addr, Buffer(..), ByteStringS(..)) import EVM.ABI (AbiValue (..), Event (..), AbiType (..)) -import EVM.ABI (Indexed (NotIndexed), getAbiSeq, getAbi) -import EVM.ABI (parseTypeName) -import EVM.Solidity (SolcContract, contractName, abiMap) +import EVM.ABI (Indexed (NotIndexed), getAbiSeq) +import EVM.ABI (parseTypeName, formatString) +import EVM.Solidity (SolcContract(..), contractName, abiMap) import EVM.Solidity (methodOutput, methodSignature, methodName) import Control.Arrow ((>>>)) -import Control.Lens (view, preview, ix, _2, to, _Just) +import Control.Lens (view, preview, ix, _2, to, makeLenses, over, each, (^?!)) import Data.Binary.Get (runGetOrFail) +import Data.Bits (shiftR) import Data.ByteString (ByteString) import Data.ByteString.Builder (byteStringHex, toLazyByteString) import Data.ByteString.Lazy (toStrict, fromStrict) @@ -29,10 +34,10 @@ import Data.Text (Text, pack, unpack, intercalate) import Data.Text (dropEnd, splitOn) import Data.Text.Encoding (decodeUtf8, decodeUtf8') +import Data.Tree (Tree (Node)) import Data.Tree.View (showTree) -import Data.Vector (Vector, fromList) - -import Numeric (showHex) +import Data.Vector (Vector) +import Data.Word (Word32) import qualified Data.ByteString as BS import qualified Data.Char as Char @@ -61,13 +66,9 @@ showWordExplanation :: W256 -> DappInfo -> Text showWordExplanation w _ | w > 0xffffffff = showDec Unsigned w showWordExplanation w dapp = - let - fullAbiMap = - mconcat (map (view abiMap) (Map.elems (view dappSolcByName dapp))) - in - case Map.lookup (fromIntegral w) fullAbiMap of - Nothing -> showDec Unsigned w - Just x -> "keccak(\"" <> view methodSignature x <> "\")" + case Map.lookup (fromIntegral w) (view dappAbiMap dapp) of + Nothing -> showDec Unsigned w + Just x -> "keccak(\"" <> view methodSignature x <> "\")" humanizeInteger :: (Num a, Integral a, Show a) => a -> Text humanizeInteger = @@ -79,64 +80,82 @@ . Text.pack . show --- TODO: make polymorphic -showAbiValues :: Vector AbiValue -> Text -showAbiValues vs = - "(" <> intercalate ", " (toList (fmap showAbiValue vs)) <> ")" +showAbiValue :: (?context :: DappContext) => AbiValue -> Text +showAbiValue (AbiBytes _ bs) = + formatBytes bs -- opportunistically decodes recognisable strings +showAbiValue (AbiAddress addr) = + let dappinfo = view contextInfo ?context + contracts = view (contextEnv . EVM.contracts) ?context + name = case (Map.lookup addr contracts) of + Nothing -> "" + Just contract -> + let hash = view EVM.codehash contract + solcContract = (preview (dappSolcByHash . ix hash . _2) dappinfo) + in maybeContractName' solcContract + in + name <> "@" <> (pack $ show addr) +showAbiValue v = pack $ show v -showAbiArray :: Vector AbiValue -> Text -showAbiArray vs = - "[" <> intercalate ", " (toList (fmap showAbiValue vs)) <> "]" +showAbiValues :: (?context :: DappContext) => Vector AbiValue -> Text +showAbiValues vs = parenthesise (textAbiValues vs) -showAbiValue :: AbiValue -> Text -showAbiValue (AbiUInt _ w) = - pack $ show w -showAbiValue (AbiInt _ w) = - pack $ show w -showAbiValue (AbiBool b) = - pack $ show b -showAbiValue (AbiAddress w160) = - pack $ "0x" ++ (showHex w160 "") -showAbiValue (AbiBytes _ bs) = - formatBytes bs -showAbiValue (AbiBytesDynamic bs) = - formatBinary bs -showAbiValue (AbiString bs) = - formatQString bs -showAbiValue (AbiArray _ _ xs) = - showAbiArray xs -showAbiValue (AbiArrayDynamic _ xs) = - showAbiArray xs -showAbiValue (AbiTuple v) = - showAbiValues v +textAbiValues :: (?context :: DappContext) => Vector AbiValue -> [Text] +textAbiValues vs = toList (fmap showAbiValue vs) +textValues :: (?context :: DappContext) => [AbiType] -> Buffer -> [Text] +textValues ts (SymbolicBuffer _) = [pack $ show t | t <- ts] +textValues ts (ConcreteBuffer bs) = + case runGetOrFail (getAbiSeq (length ts) ts) (fromStrict bs) of + Right (_, _, xs) -> textAbiValues xs + Left (_, _, _) -> [formatBinary bs] + +parenthesise :: [Text] -> Text +parenthesise ts = "(" <> intercalate ", " ts <> ")" + +showValues :: (?context :: DappContext) => [AbiType] -> Buffer -> Text +showValues ts b = parenthesise $ textValues ts b + +showValue :: (?context :: DappContext) => AbiType -> Buffer -> Text +showValue t b = head $ textValues [t] b + +showCall :: (?context :: DappContext) => [AbiType] -> Buffer -> Text +showCall ts (SymbolicBuffer bs) = showValues ts $ SymbolicBuffer (drop 4 bs) +showCall ts (ConcreteBuffer bs) = showValues ts $ ConcreteBuffer (BS.drop 4 bs) + +showError :: (?context :: DappContext) => ByteString -> Text +showError bs = case BS.take 4 bs of + -- Method ID for Error(string) + "\b\195y\160" -> showCall [AbiStringType] (ConcreteBuffer bs) + _ -> formatBinary bs + + +-- the conditions under which bytes will be decoded and rendered as a string isPrintable :: ByteString -> Bool isPrintable = decodeUtf8' >>> - either (const False) - (Text.all (not . Char.isControl)) + either + (const False) + (Text.all (\c-> Char.isPrint c && (not . Char.isControl) c)) formatBytes :: ByteString -> Text formatBytes b = let (s, _) = BS.spanEnd (== 0) b in if isPrintable s - then formatQString s + then formatBString s else formatBinary b formatSBytes :: Buffer -> Text formatSBytes (SymbolicBuffer b) = "<" <> pack (show (length b)) <> " symbolic bytes>" formatSBytes (ConcreteBuffer b) = formatBytes b -formatQString :: ByteString -> Text -formatQString = pack . show - -formatString :: ByteString -> Text -formatString bs = decodeUtf8 (fst (BS.spanEnd (== 0) bs)) +-- a string that came from bytes, displayed with special quotes +formatBString :: ByteString -> Text +formatBString b = mconcat [ "«", Text.dropAround (=='"') (pack $ formatString b), "»" ] formatSString :: Buffer -> Text formatSString (SymbolicBuffer bs) = "<" <> pack (show (length bs)) <> " symbolic bytes (string)>" -formatSString (ConcreteBuffer bs) = formatString bs +formatSString (ConcreteBuffer bs) = pack $ formatString bs formatBinary :: ByteString -> Text formatBinary = @@ -147,63 +166,93 @@ formatSBinary (ConcreteBuffer bs) = formatBinary bs showTraceTree :: DappInfo -> VM -> Text -showTraceTree dapp = - traceForest - >>> fmap (fmap (unpack . showTrace dapp)) - >>> concatMap showTree - >>> pack +showTraceTree dapp vm = + let forest = traceForest vm + traces = fmap (fmap (unpack . showTrace dapp vm)) forest + in pack $ concatMap showTree traces -showTrace :: DappInfo -> Trace -> Text -showTrace dapp trace = - let +unindexed :: [(AbiType, Indexed)] -> [AbiType] +unindexed ts = [t | (t, NotIndexed) <- ts] + +showTrace :: DappInfo -> VM -> Trace -> Text +showTrace dapp vm trace = + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + in let pos = case showTraceLocation dapp trace of - Left x -> " \x1b[90m" <> x <> "\x1b[0m" - Right x -> " \x1b[90m(" <> x <> ")\x1b[0m" - fullAbiMap = - mconcat (map (view abiMap) (Map.elems (view dappSolcByName dapp))) + Left x -> " \x1b[1m" <> x <> "\x1b[0m" + Right x -> " \x1b[1m(" <> x <> ")\x1b[0m" + fullAbiMap = view dappAbiMap dapp in case view traceData trace of EventTrace (Log _ bytes topics) -> - case topics of - [] -> - mconcat + let logn = mconcat [ "\x1b[36m" - , "log0(" - , formatSBinary bytes - , ")" + , "log" <> (pack (show (length topics))) + , parenthesise ((map (pack . show) topics) ++ [formatSBinary bytes]) , "\x1b[0m" ] <> pos - (topic:_) -> - let unknownTopic = -- todo: catch ds-note - mconcat - [ "\x1b[36m" - , "log" <> (pack (show (length topics))) <> "(" - , formatSBinary bytes <> ", " - , intercalate ", " (map (pack . show) topics) <> ")" - , "\x1b[0m" - ] <> pos - - in case maybeLitWord topic of - Just top -> case Map.lookup (wordValue top) (view dappEventMap dapp) of - Just (Event name _ types) -> - mconcat - [ "\x1b[36m" - , name - , showValues [t | (t, NotIndexed) <- types] bytes - -- todo: show indexed - , "\x1b[0m" - ] <> pos - Nothing -> unknownTopic - Nothing -> unknownTopic + knownTopic name types = mconcat + [ "\x1b[36m" + , name + , showValues (unindexed types) bytes + -- todo: show indexed + , "\x1b[0m" + ] <> pos + lognote sig usr = mconcat + [ "\x1b[36m" + , "LogNote" + , parenthesise [sig, usr, "..."] + , "\x1b[0m" + ] <> pos + in case topics of + [] -> + logn + (t1:_) -> + case maybeLitWord t1 of + Just topic -> + case Map.lookup (wordValue topic) (view dappEventMap dapp) of + Just (Event name _ types) -> + knownTopic name types + Nothing -> + case topics of + [_, t2, _, _] -> + -- check for ds-note logs.. possibly catching false positives + -- event LogNote( + -- bytes4 indexed sig, + -- address indexed usr, + -- bytes32 indexed arg1, + -- bytes32 indexed arg2, + -- bytes data + -- ) anonymous; + let + sig = fromIntegral $ shiftR (wordValue topic) 224 :: Word32 + usr = case maybeLitWord t2 of + Just w -> + pack $ show $ (fromIntegral w :: Addr) + Nothing -> + "" + in + case Map.lookup sig (view dappAbiMap dapp) of + Just m -> + lognote (view methodSignature m) usr + Nothing -> + logn + _ -> + logn + Nothing -> + logn QueryTrace q -> case q of - PleaseFetchContract addr _ -> + PleaseFetchContract addr _ _ -> "fetch contract " <> pack (show addr) <> pos PleaseFetchSlot addr slot _ -> "fetch storage slot " <> pack (show slot) <> " from " <> pack (show addr) <> pos PleaseAskSMT _ _ _ -> "ask smt" <> pos + PleaseMakeUnique _ _ _ -> + "make unique value" <> pos + ErrorTrace e -> case e of Revert out -> @@ -211,21 +260,17 @@ _ -> "\x1b[91merror\x1b[0m " <> pack (show e) <> pos - ReturnTrace out (CallContext _ _ _ _ hash (Just abi) _ _ _) -> - case getAbiMethodOutput dapp hash abi of - Nothing -> - "← " <> - case Map.lookup (fromIntegral abi) fullAbiMap of - Just m -> - case (view methodOutput m) of - Just (_, t) -> - pack (show t) <> " " <> showValue t out - Nothing -> - formatSBinary out - Nothing -> + ReturnTrace out (CallContext _ _ _ _ _ (Just abi) _ _ _) -> + "← " <> + case Map.lookup (fromIntegral abi) fullAbiMap of + Just m -> + case unzip (view methodOutput m) of + ([], []) -> formatSBinary out - Just (_, t) -> - "← " <> pack (show t) <> " " <> showValue t out + (_, ts) -> + showValues ts out + Nothing -> + formatSBinary out ReturnTrace out (CallContext {}) -> "← " <> formatSBinary out ReturnTrace out (CreationContext {}) -> @@ -233,8 +278,11 @@ EntryTrace t -> t - FrameTrace (CreationContext hash _ _ ) -> - "create " <> maybeContractName (preview (dappSolcByHash . ix hash . _2) dapp) <> pos + FrameTrace (CreationContext addr hash _ _ ) -> + "create " + <> maybeContractName (preview (dappSolcByHash . ix hash . _2) dapp) + <> "@" <> pack (show addr) + <> pos FrameTrace (CallContext target context _ _ hash abi calldata _ _) -> let calltype = if target == context then "call " @@ -246,7 +294,9 @@ <> pack "::" <> case Map.lookup (fromIntegral (fromMaybe 0x00 abi)) fullAbiMap of Just m -> - view methodName m + "\x1b[1m" + <> view methodName m + <> "\x1b[0m" <> showCall (catMaybes (getAbiTypes (view methodSignature m))) calldata Nothing -> formatSBinary calldata @@ -266,16 +316,6 @@ <> "\x1b[0m" <> pos -getAbiMethodOutput - :: DappInfo -> W256 -> Word -> Maybe (Text, AbiType) -getAbiMethodOutput dapp hash abi = - -- Some typical ugly lens code. :'( - preview - ( dappSolcByHash . ix hash . _2 . abiMap - . ix (fromIntegral abi) . methodOutput . _Just - ) - dapp - getAbiTypes :: Text -> [Maybe AbiType] getAbiTypes abi = map (parseTypeName mempty) types where @@ -283,34 +323,14 @@ filter (/= "") $ splitOn "," (dropEnd 1 (last (splitOn "(" abi))) -showCall :: [AbiType] -> Buffer -> Text -showCall ts (SymbolicBuffer bs) = showValues ts $ SymbolicBuffer (drop 4 bs) -showCall ts (ConcreteBuffer bs) = showValues ts $ ConcreteBuffer (BS.drop 4 bs) - -showError :: ByteString -> Text -showError bs = case BS.take 4 bs of - -- Method ID for Error(string) - "\b\195y\160" -> showCall [AbiStringType] (ConcreteBuffer bs) - _ -> formatBinary bs - -showValues :: [AbiType] -> Buffer -> Text -showValues ts (SymbolicBuffer _) = "symbolic: " <> (pack . show $ AbiTupleType (fromList ts)) -showValues ts (ConcreteBuffer bs) = - case runGetOrFail (getAbiSeq (length ts) ts) (fromStrict bs) of - Right (_, _, xs) -> showAbiValues xs - Left (_, _, _) -> formatBinary bs - -showValue :: AbiType -> Buffer -> Text -showValue t (SymbolicBuffer _) = "symbolic: " <> (pack $ show t) -showValue t (ConcreteBuffer bs) = - case runGetOrFail (getAbi t) (fromStrict bs) of - Right (_, _, x) -> showAbiValue x - Left (_, _, _) -> formatBinary bs - maybeContractName :: Maybe SolcContract -> Text maybeContractName = maybe "" (view (contractName . to contractNamePart)) +maybeContractName' :: Maybe SolcContract -> Text +maybeContractName' = + maybe "" (view (contractName . to contractNamePart)) + maybeAbiName :: SolcContract -> Word -> Maybe Text maybeAbiName solc abi = preview (abiMap . ix (fromIntegral abi) . methodSignature) solc @@ -319,3 +339,113 @@ contractPathPart :: Text -> Text contractPathPart x = Text.split (== ':') x !! 0 + +prettyvmresult :: (?context :: DappContext) => VMResult -> String +prettyvmresult (EVM.VMFailure (EVM.Revert "")) = "Revert" +prettyvmresult (EVM.VMFailure (EVM.Revert msg)) = "Revert" ++ (unpack $ showError msg) +prettyvmresult (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) = "Assertion violation" +prettyvmresult (EVM.VMFailure err) = "Failed: " <> show err +prettyvmresult (EVM.VMSuccess (ConcreteBuffer msg)) = + if BS.null msg + then "Stop" + else "Return: " <> show (ByteStringS msg) +prettyvmresult (EVM.VMSuccess (SymbolicBuffer msg)) = + "Return: " <> show (length msg) <> " symbolic bytes" + +currentSolc :: DappInfo -> VM -> Maybe SolcContract +currentSolc dapp vm = + let + this = vm ^?! EVM.env . EVM.contracts . ix (view (EVM.state . EVM.contract) vm) + h = view EVM.codehash this + in + preview (dappSolcByHash . ix h . _2) dapp + +-- TODO: display in an 'act' format + +-- TreeLine describes a singe line of the tree +-- it contains the indentation which is prefixed to it +-- and its content which contains the rest +data TreeLine = TreeLine { + _indent :: String, + _content :: String + } + +makeLenses ''TreeLine + +-- SHOW TREE + +showTreeIndentSymbol :: Bool -- ^ isLastChild + -> Bool -- ^ isTreeHead + -> String +showTreeIndentSymbol True True = "\x2514" -- └ +showTreeIndentSymbol False True = "\x251c" -- ├ +showTreeIndentSymbol True False = " " +showTreeIndentSymbol False False = "\x2502" -- │ + +flattenTree :: Int -> -- total number of cases + Int -> -- case index + Tree [String] -> + [TreeLine] +-- this case should never happen for our use case, here for generality +flattenTree _ _ (Node [] _) = [] + +flattenTree totalCases i (Node (x:xs) cs) = let + isLastCase = i + 1 == totalCases + indenthead = showTreeIndentSymbol isLastCase True <> " " <> show i <> " " + indentchild = showTreeIndentSymbol isLastCase False <> " " + in TreeLine indenthead x + : ((TreeLine indentchild <$> xs) ++ over (each . indent) ((<>) indentchild) (flattenForest cs)) + +flattenForest :: [Tree [String]] -> [TreeLine] +flattenForest forest = concat $ zipWith (flattenTree (length forest)) [0..] forest + +leftpad :: Int -> String -> String +leftpad n = (<>) $ replicate n ' ' + +showTree' :: Tree [String] -> String +showTree' (Node s []) = unlines s +showTree' (Node _ children) = + let + treeLines = flattenForest children + maxIndent = 2 + maximum (length . _indent <$> treeLines) + showTreeLine (TreeLine colIndent colContent) = + let indentSize = maxIndent - length colIndent + in colIndent <> leftpad indentSize colContent + in unlines $ showTreeLine <$> treeLines + + +-- RENDER TREE + +showStorage :: [(SymWord, SymWord)] -> [String] +showStorage = fmap (\(k, v) -> show k <> " => " <> show v) + +showLeafInfo :: DappInfo -> BranchInfo -> [String] +showLeafInfo srcInfo (BranchInfo vm _) = let + ?context = DappContext { _contextInfo = srcInfo, _contextEnv = vm ^?! EVM.env } + in let + self = view (EVM.state . EVM.contract) vm + updates = case view (EVM.env . EVM.contracts) vm ^?! ix self . EVM.storage of + Symbolic v _ -> v + Concrete x -> [(litWord k,v) | (k, v) <- Map.toList x] + showResult = [prettyvmresult res | Just res <- [view result vm]] + in showResult + ++ showStorage updates + ++ [""] + +showBranchInfoWithAbi :: DappInfo -> BranchInfo -> [String] +showBranchInfoWithAbi _ (BranchInfo _ Nothing) = [""] +showBranchInfoWithAbi srcInfo (BranchInfo vm (Just y)) = + case y of + (IsZero (Eq (Literal x) _)) -> + let + abimap = view abiMap <$> currentSolc srcInfo vm + method = abimap >>= Map.lookup (num x) + in [maybe (show y) (show . view methodSignature) method] + y' -> [show y'] + +renderTree :: (a -> [String]) + -> (a -> [String]) + -> Tree a + -> Tree [String] +renderTree showBranch showLeaf (Node b []) = Node (showBranch b ++ showLeaf b) [] +renderTree showBranch showLeaf (Node b cs) = Node (showBranch b) (renderTree showBranch showLeaf <$> cs) diff --git a/src/EVM/Keccak.hs b/src/EVM/Keccak.hs deleted file mode 100644 --- a/src/EVM/Keccak.hs +++ /dev/null @@ -1,38 +0,0 @@ -module EVM.Keccak (keccak, abiKeccak) where - -import EVM.Types - -import Control.Arrow ((>>>)) - -import Data.Bits -import Data.ByteString (ByteString) - -import qualified Data.ByteString as BS -import Data.Word - -import Crypto.Hash -import qualified Data.ByteArray as BA - -keccakBytes :: ByteString -> ByteString -keccakBytes = - (hash :: ByteString -> Digest Keccak_256) - >>> BA.unpack - >>> BS.pack - - -word32 :: [Word8] -> Word32 -word32 xs = sum [ fromIntegral x `shiftL` (8*n) - | (n, x) <- zip [0..] (reverse xs) ] - -keccak :: ByteString -> W256 -keccak = - keccakBytes - >>> BS.take 32 - >>> word - -abiKeccak :: ByteString -> Word32 -abiKeccak = - keccakBytes - >>> BS.take 4 - >>> BS.unpack - >>> word32 diff --git a/src/EVM/Patricia.hs b/src/EVM/Patricia.hs --- a/src/EVM/Patricia.hs +++ b/src/EVM/Patricia.hs @@ -4,9 +4,8 @@ module EVM.Patricia where -import EVM.Keccak import EVM.RLP -import EVM.Types +import EVM.Types hiding (Literal) import Control.Monad.Free import Control.Monad.State diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs --- a/src/EVM/Solidity.hs +++ b/src/EVM/Solidity.hs @@ -21,6 +21,7 @@ , methodOutput , abiMap , eventMap + , storageLayout , contractName , constructorInputs , creationCode @@ -28,18 +29,21 @@ , makeSrcMaps , readSolc , readJSON + , readStdJSON + , readCombinedJSON , runtimeCode - , snippetCache , runtimeCodehash , creationCodehash , runtimeSrcmap , creationSrcmap - , contractAst , sourceFiles , sourceLines , sourceAsts , stripBytecodeMetadata , signature + , solc + , Language(..) + , stdjson , parseMethodInput , lineSubrange , astIdMap @@ -47,15 +51,16 @@ ) where import EVM.ABI -import EVM.Keccak import EVM.Types import Control.Applicative -import Control.Lens hiding (Indexed) -import Data.Aeson (Value (..)) +import Control.Monad +import Control.Lens hiding (Indexed, (.=)) +import Data.Aeson (Value (..), ToJSON(..), (.=), object, encode) import Data.Aeson.Lens import Data.Scientific import Data.ByteString (ByteString) +import Data.ByteString.Lazy (toStrict) import Data.Char (isDigit) import Data.Foldable import Data.Map.Strict (Map) @@ -65,7 +70,7 @@ import Data.Semigroup import Data.Sequence (Seq) import Data.Text (Text, pack, intercalate) -import Data.Text.Encoding (encodeUtf8) +import Data.Text.Encoding (encodeUtf8, decodeUtf8) import Data.Text.IO (readFile, writeFile) import Data.Vector (Vector) import Data.Word @@ -82,13 +87,14 @@ import qualified Data.Map.Strict as Map import qualified Data.Text as Text import qualified Data.Vector as Vector +import Data.List (sort) data StorageItem = StorageItem { _type :: SlotType, _offset :: Int, _slot :: Int } deriving (Show, Eq) - + data SlotType -- Note that mapping keys can only be elementary; -- that excludes arrays, contracts, and mappings. @@ -99,19 +105,15 @@ instance Show SlotType where show (StorageValue t) = show t - show (StorageMapping (s NonEmpty.:| ss) t) = - "mapping(" - <> show s - <> " => " - <> foldr - (\x y -> - "mapping(" - <> show x - <> " => " - <> y - <> ")") - (show t) ss - <> ")" + show (StorageMapping s t) = + foldr + (\x y -> + "mapping(" + <> show x + <> " => " + <> y + <> ")") + (show t) s instance Read SlotType where readsPrec _ ('m':'a':'p':'p':'i':'n':'g':'(':s) = @@ -134,19 +136,17 @@ , _storageLayout :: Maybe (Map Text StorageItem) , _runtimeSrcmap :: Seq SrcMap , _creationSrcmap :: Seq SrcMap - , _contractAst :: Value } deriving (Show, Eq, Generic) data Method = Method - { _methodOutput :: Maybe (Text, AbiType) + { _methodOutput :: [(Text, AbiType)] , _methodInputs :: [(Text, AbiType)] , _methodName :: Text , _methodSignature :: Text } deriving (Show, Eq, Ord, Generic) data SourceCache = SourceCache - { _snippetCache :: Map (Int, Int) ByteString - , _sourceFiles :: Map Int (Text, ByteString) + { _sourceFiles :: Map Int (Text, ByteString) , _sourceLines :: Map Int (Vector ByteString) , _sourceAsts :: Map Text Value } deriving (Show, Eq, Generic) @@ -155,7 +155,7 @@ _ <> _ = error "lol" instance Monoid SourceCache where - mempty = SourceCache mempty mempty mempty mempty + mempty = SourceCache mempty mempty mempty data JumpType = JumpInto | JumpFrom | JumpRegular deriving (Show, Eq, Ord, Generic) @@ -232,13 +232,14 @@ go c (xs, state, p) = (xs, error ("srcmap: y u " ++ show c ++ " in state" ++ show state ++ "?!?"), p) -makeSourceCache :: [Text] -> Map Text Value -> IO SourceCache +makeSourceCache :: [(Text, Maybe ByteString)] -> Map Text Value -> IO SourceCache makeSourceCache paths asts = do - xs <- mapM (BS.readFile . Text.unpack) paths + let f (_, Just content) = return content + f (fp, Nothing) = BS.readFile $ Text.unpack fp + xs <- mapM f paths return $! SourceCache - { _snippetCache = mempty - , _sourceFiles = - Map.fromList (zip [0..] (zip paths xs)) + { _sourceFiles = + Map.fromList (zip [0..] (zip (fst <$> paths) xs)) , _sourceLines = Map.fromList (zip [0 .. length paths - 1] (map (Vector.fromList . BS.split 0xa) xs)) @@ -270,43 +271,46 @@ solidity :: Text -> Text -> IO (Maybe ByteString) solidity contract src = do (json, path) <- solidity' src - let Just (solc, _, _) = readJSON json - return (solc ^? ix (path <> ":" <> contract) . creationCode) + let Just (sol, _, _) = readJSON json + return (sol ^? ix (path <> ":" <> contract) . creationCode) solcRuntime :: Text -> Text -> IO (Maybe ByteString) solcRuntime contract src = do (json, path) <- solidity' src - let Just (solc, _, _) = readJSON json - return (solc ^? ix (path <> ":" <> contract) . runtimeCode) + let Just (sol, _, _) = readJSON json + return (sol ^? ix (path <> ":" <> contract) . runtimeCode) functionAbi :: Text -> IO Method functionAbi f = do (json, path) <- solidity' ("contract ABI { function " <> f <> " public {}}") - let Just (solc, _, _) = readJSON json - case Map.toList $ solc ^?! ix (path <> ":ABI") . abiMap of + let Just (sol, _, _) = readJSON json + case Map.toList $ sol ^?! ix (path <> ":ABI") . abiMap of [(_,b)] -> return b _ -> error "hevm internal error: unexpected abi format" force :: String -> Maybe a -> a force s = fromMaybe (error s) -readJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [Text]) -readJSON json = do - contracts <- - f <$> (json ^? key "contracts" . _Object) - <*> (fmap (fmap (^. _String)) $ json ^? key "sourceList" . _Array) +readJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) +readJSON json = case json ^? key "sourceList" of + Nothing -> readStdJSON json + _ -> readCombinedJSON json + +readCombinedJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) +readCombinedJSON json = do + contracts <- f <$> (json ^? key "contracts" . _Object) sources <- toList . fmap (view _String) <$> json ^? key "sourceList" . _Array - return (contracts, Map.fromList (HMap.toList asts), sources) + return (contracts, Map.fromList (HMap.toList asts), [ (x, Nothing) | x <- sources]) where asts = fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" . _Object) - f x y = Map.fromList . map (g y) . HMap.toList $ x - g _ (s, x) = + f x = Map.fromList . HMap.toList $ HMap.mapWithKey g x + g s x = let theRuntimeCode = toCode (x ^?! key "bin-runtime" . _String) theCreationCode = toCode (x ^?! key "bin" . _String) abis = toList ((x ^?! key "abi" . _String) ^?! _Array) - in (s, SolcContract { + in SolcContract { _runtimeCode = theRuntimeCode, _creationCode = theCreationCode, _runtimeCodehash = keccak (stripBytecodeMetadata theRuntimeCode), @@ -314,72 +318,109 @@ _runtimeSrcmap = force "internal error: srcmap-runtime" (makeSrcMaps (x ^?! key "srcmap-runtime" . _String)), _creationSrcmap = force "internal error: srcmap" (makeSrcMaps (x ^?! key "srcmap" . _String)), _contractName = s, - _contractAst = - fromMaybe - (error "JSON lacks abstract syntax trees.") - (preview (ix (head (Text.split (== ':') s)) . key "AST") asts), + _constructorInputs = mkConstructor abis, + _abiMap = mkAbiMap abis, + _eventMap = mkEventMap abis, + _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String + } - _constructorInputs = - let - isConstructor y = - "constructor" == y ^?! key "type" . _String - in - case filter isConstructor abis of - [abi] -> map parseMethodInput (toList (abi ^?! key "inputs" . _Array)) - [] -> [] -- default constructor has zero inputs - _ -> error "strange: contract has multiple constructors", +readStdJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) +readStdJSON json = do + contracts <- json ^? key "contracts" ._Object + -- TODO: support the general case of "urls" and "content" in the standard json + sources <- json ^? key "sources" . _Object + let asts = force "JSON lacks abstract syntax trees." . preview (key "ast") <$> sources + contractMap = f contracts + contents src = (src, encodeUtf8 <$> HMap.lookup src (mconcat $ Map.elems $ snd <$> contractMap)) + return (fst <$> contractMap, Map.fromList (HMap.toList asts), contents <$> (sort $ HMap.keys sources)) + where + 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) = + 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 + srcContents :: Maybe (HMap.HashMap Text Text) + srcContents = do metadata <- x ^? key "metadata" . _String + srcs <- metadata ^? key "sources" . _Object + return $ (view (key "content" . _String)) <$> (HMap.filter (isJust . preview (key "content")) srcs) + abis = force ("abi key not found in " <> show x) $ + toList <$> x ^? key "abi" . _Array + in (s <> ":" <> c, (SolcContract { + _runtimeCode = theRuntimeCode, + _creationCode = theCreationCode, + _runtimeCodehash = keccak (stripBytecodeMetadata theRuntimeCode), + _creationCodehash = keccak (stripBytecodeMetadata theCreationCode), + _runtimeSrcmap = force "internal error: srcmap-runtime" (makeSrcMaps (runtime ^?! key "sourceMap" . _String)), + _creationSrcmap = force "internal error: srcmap" (makeSrcMaps (creation ^?! key "sourceMap" . _String)), + _contractName = s <> ":" <> c, + _constructorInputs = mkConstructor abis, + _abiMap = mkAbiMap abis, + _eventMap = mkEventMap abis, + _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String + }, fromMaybe mempty srcContents)) - _abiMap = Map.fromList $ - let - relevant = - filter (\y -> "function" == y ^?! key "type" . _String) abis - in flip map relevant $ - \abi -> ( - abiKeccak (encodeUtf8 (signature abi)), - Method - { _methodName = abi ^?! key "name" . _String - , _methodSignature = signature abi - , _methodInputs = - map parseMethodInput - (toList (abi ^?! key "inputs" . _Array)) - , _methodOutput = - fmap parseMethodInput - (abi ^? key "outputs" . _Array . ix 0) - } - ), - _eventMap = Map.fromList $ - flip map (filter (\y -> "event" == y ^?! key "type" . _String) - . toList $ (x ^?! key "abi" . _String) ^?! _Array) $ - \abi -> - ( keccak (encodeUtf8 (signature abi)) - , Event - (abi ^?! key "name" . _String) - (case abi ^?! key "anonymous" . _Bool of - True -> Anonymous - False -> NotAnonymous) - (map (\y -> ( force "internal error: type" (parseTypeName' y) - , if y ^?! key "indexed" . _Bool - then Indexed - else NotIndexed )) - (toList $ abi ^?! key "inputs" . _Array)) - ), - _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String - }) +mkAbiMap :: [Value] -> Map Word32 Method +mkAbiMap abis = Map.fromList $ + let + relevant = filter (\y -> "function" == y ^?! key "type" . _String) abis + f abi = + (abiKeccak (encodeUtf8 (signature abi)), + Method { _methodName = abi ^?! key "name" . _String + , _methodSignature = signature abi + , _methodInputs = map parseMethodInput + (toList (abi ^?! key "inputs" . _Array)) + , _methodOutput = map parseMethodInput + (toList (abi ^?! key "outputs" . _Array)) + }) + in f <$> relevant +mkEventMap :: [Value] -> Map W256 Event +mkEventMap abis = Map.fromList $ + let + relevant = filter (\y -> "event" == y ^?! key "type" . _String) abis + f abi = + ( keccak (encodeUtf8 (signature abi)) + , Event + (abi ^?! key "name" . _String) + (case abi ^?! key "anonymous" . _Bool of + True -> Anonymous + False -> NotAnonymous) + (map (\y -> ( force "internal error: type" (parseTypeName' y) + , if y ^?! key "indexed" . _Bool + then Indexed + else NotIndexed )) + (toList $ abi ^?! key "inputs" . _Array)) + ) + in f <$> relevant + +mkConstructor :: [Value] -> [(Text, AbiType)] +mkConstructor abis = + let + isConstructor y = + "constructor" == y ^?! key "type" . _String + in + case filter isConstructor abis of + [abi] -> map parseMethodInput (toList (abi ^?! key "inputs" . _Array)) + [] -> [] -- default constructor has zero inputs + _ -> error "strange: contract has multiple constructors" + mkStorageLayout :: Maybe Text -> Maybe (Map Text StorageItem) mkStorageLayout Nothing = Nothing -mkStorageLayout (Just json) = do items <- json ^? key "storage" . _Array - types <- json ^? key "types" - Map.fromList <$> mapM - (\item -> do name <- item ^? key "label" . _String - offset <- item ^? key "offset" . _Number >>= toBoundedInteger - slot <- item ^? key "slot" . _String - typ <- item ^? key "type" . _String - slotType <- types ^?! key typ ^? key "label" . _String - return (name, StorageItem (read $ Text.unpack slotType) offset (read $ Text.unpack slot)) - - ) - (Vector.toList items) +mkStorageLayout (Just json) = do + items <- json ^? key "storage" . _Array + types <- json ^? key "types" + 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 + typ <- item ^? key "type" . _String + slotType <- types ^?! key typ ^? key "label" . _String + return (name, StorageItem (read $ Text.unpack slotType) offset (read $ Text.unpack slot))) signature :: AsValue s => s -> Text signature abi = @@ -423,6 +464,52 @@ "" return (x, pack path) +solc :: Language -> Text -> IO Text +solc lang src = + withSystemTempFile "hevm.sol" $ \path handle -> do + hClose handle + writeFile path (stdjson lang src) + Text.pack <$> readProcess + "solc" + ["--standard-json", path] + "" + +data Language = Solidity | Yul + deriving (Show) + +data StandardJSON = StandardJSON Language Text +-- more options later perhaps + +instance ToJSON StandardJSON where + toJSON (StandardJSON lang src) = + object [ "language" .= show lang + , "sources" .= object ["hevm.sol" .= + object ["content" .= src]] + , "settings" .= + object [ "outputSelection" .= + object ["*" .= + object ["*" .= (toJSON + ["metadata" :: String, + "evm.bytecode", + "evm.deployedBytecode", + "abi", + "storageLayout", + "evm.bytecode.sourceMap", + "evm.bytecode.linkReferences", + "evm.bytecode.generatedSources", + "evm.deployedBytecode.sourceMap", + "evm.deployedBytecode.linkReferences", + "evm.deployedBytecode.generatedSources" + ]), + "" .= (toJSON ["ast" :: String]) + ] + ] + ] + ] + +stdjson :: Language -> Text -> Text +stdjson lang src = decodeUtf8 $ toStrict $ encode $ StandardJSON lang src + -- When doing CREATE and passing constructor arguments, Solidity loads -- the argument data via the creation bytecode, since there is no "calldata" -- for CREATE. @@ -478,15 +565,10 @@ tmp = Map.fromList . mapMaybe - (\v -> - case preview (key "src" . _String) v of - Just src -> - case map (readMaybe . Text.unpack) (Text.split (== ':') src) of - [Just i, Just n, Just f] -> - Just ((i, n, f), v) - _ -> - error "strange formatting of src field" - _ -> - Nothing) + (\v -> do + src <- preview (key "src" . _String) v + [i, n, f] <- mapM (readMaybe . Text.unpack) (Text.split (== ':') src) + return ((i, n, f), v) + ) . Map.elems $ astIds diff --git a/src/EVM/Stepper.hs b/src/EVM/Stepper.hs --- a/src/EVM/Stepper.hs +++ b/src/EVM/Stepper.hs @@ -6,6 +6,7 @@ , Stepper , exec , execFully + , run , runFully , wait , ask @@ -26,23 +27,17 @@ import Prelude hiding (fail) -import Control.Monad.Operational (Program(..), singleton, view, ProgramViewT(..), ProgramView) +import Control.Monad.Operational (Program, singleton, view, ProgramViewT(..), ProgramView) import Control.Monad.State.Strict (runState, liftIO, StateT) import qualified Control.Monad.State.Class as State import qualified EVM.Exec -import Control.Lens (use) -import Data.Binary.Get (runGetOrFail) import Data.Text (Text) import EVM.Types (Buffer) import EVM (EVM, VM, VMResult (VMFailure, VMSuccess), Error (Query, Choose), Query, Choose) import qualified EVM -import EVM.ABI (AbiType, AbiValue, getAbi) import qualified EVM.Fetch as Fetch - -import Data.ByteString (ByteString) -import qualified Data.ByteString.Lazy as LazyByteString -- | The instruction type of the operational monad data Action a where diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -9,58 +9,68 @@ import Control.Lens hiding (pre) import EVM hiding (Query, push) +import qualified EVM import EVM.Exec import qualified EVM.Fetch as Fetch import EVM.ABI import EVM.Stepper (Stepper) import qualified EVM.Stepper as Stepper import qualified Control.Monad.Operational as Operational -import EVM.Types hiding (Word) -import EVM.Symbolic (SymWord(..), sw256) -import EVM.Concrete (createAddress, Word) +import Control.Monad.State.Strict hiding (state) +import Data.Maybe (catMaybes, fromMaybe) +import EVM.Types +import EVM.Concrete (createAddress) import qualified EVM.FeeSchedule as FeeSchedule import Data.SBV.Trans.Control import Data.SBV.Trans hiding (distinct, Word) import Data.SBV hiding (runSMT, newArray_, addAxiom, distinct, sWord8s, Word) import Data.Vector (toList, fromList) +import Data.Tree -import Control.Monad.IO.Class -import qualified Control.Monad.State.Class as State 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 (runStateT, runState, StateT, get, put, zipWithM) +import Control.Monad.State.Strict (runState, get, put, zipWithM) +import qualified Control.Monad.State.Class as State import Control.Applicative -- | Convenience functions for generating large symbolic byte strings -sbytes32, sbytes256, sbytes512, sbytes1024 :: Query ([SWord 8]) +sbytes32, sbytes128, sbytes256, sbytes512, sbytes1024 :: Query ([SWord 8]) sbytes32 = toBytes <$> freshVar_ @ (WordN 256) sbytes128 = toBytes <$> freshVar_ @ (WordN 1024) sbytes256 = liftA2 (++) sbytes128 sbytes128 sbytes512 = liftA2 (++) sbytes256 sbytes256 sbytes1024 = liftA2 (++) sbytes512 sbytes512 +mkByte :: Query [SWord 8] +mkByte = do x <- freshVar_ + return [x] + -- | Abstract calldata argument generation --- We don't assume input types are restricted to their proper range here; --- such assumptions should instead be given as preconditions. --- This could catch some interesting calldata mismanagement errors. -symAbiArg :: AbiType -> Query ([SWord 8], SWord 32) -symAbiArg (AbiUIntType n) | n `mod` 8 == 0 && n <= 256 = do x <- sbytes32 - return (x, 32) +symAbiArg :: AbiType -> Query ([SWord 8], W256) +symAbiArg (AbiUIntType n) | n `mod` 8 == 0 && n <= 256 = + do x <- concatMapM (const mkByte) [0..(n `div` 8) - 1] + return (padLeft' 32 x, 32) | otherwise = error "bad type" -symAbiArg (AbiIntType n) | n `mod` 8 == 0 && n <= 256 = do x <- sbytes32 - return (x, 32) +symAbiArg (AbiIntType n) | n `mod` 8 == 0 && n <= 256 = + do x <- concatMapM (const mkByte) [(0 :: Int) ..(n `div` 8) - 1] + return (padLeft' 32 x, 32) + | otherwise = error "bad type" -symAbiArg AbiBoolType = do x <- sbytes32 - return (x, 32) +symAbiArg AbiBoolType = + do x <- mkByte + return (padLeft' 32 x, 32) -symAbiArg AbiAddressType = do x <- sbytes32 - return (x, 32) +symAbiArg AbiAddressType = + do x <- concatMapM (const mkByte) [(0 :: Int)..19] + return (padLeft' 32 x, 32) -symAbiArg (AbiBytesType n) | n <= 32 = do x <- sbytes32 - return (x, 32) +symAbiArg (AbiBytesType n) | n <= 32 = + do x <- concatMapM (const mkByte) [0..n - 1] + return (padLeft' 32 x, 32) + | otherwise = error "bad type" -- TODO: is this encoding correct? @@ -81,7 +91,7 @@ -- with concrete arguments. -- Any argument given as "" or omitted at the tail of the list are -- kept symbolic. -symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], SWord 32) +symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], W256) symCalldata sig typesignature concreteArgs = let args = concreteArgs <> replicate (length typesignature - length concreteArgs) "" mkArg typ "" = symAbiArg typ @@ -97,18 +107,18 @@ case typesignature of Nothing -> do cd <- sbytes256 len <- freshVar_ - return (cd, len, len .<= 256) + return (cd, var "calldataLength" len, (len .<= 256, Todo "calldatalength < 256" [])) Just (name, typs) -> do (cd, cdlen) <- symCalldata name typs concreteArgs - return (cd, cdlen, sTrue) + return (cd, S (Literal cdlen) (literal $ num cdlen), (sTrue, Todo "Trivial" [])) symstore <- case storagemodel of - SymbolicS -> Symbolic <$> freshArray_ Nothing - InitialS -> Symbolic <$> freshArray_ (Just 0) + SymbolicS -> Symbolic [] <$> freshArray_ Nothing + InitialS -> Symbolic [] <$> freshArray_ (Just 0) ConcreteS -> return $ Concrete mempty c <- SAddr <$> freshVar_ - value' <- sw256 <$> freshVar_ - return $ loadSymVM (RuntimeCode x) symstore storagemodel c value' (SymbolicBuffer cd', cdlen) & over pathConditions ((<>) [cdconstraint]) + value' <- var "CALLVALUE" <$> freshVar_ + return $ loadSymVM (RuntimeCode x) symstore storagemodel c value' (SymbolicBuffer cd', cdlen) & over constraints ((<>) [cdconstraint]) -loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SWord 32) -> VM +loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SymWord) -> VM loadSymVM x initStore model addr callvalue' calldata' = (makeVm $ VMOpts { vmoptContract = contractWithStore x initStore @@ -133,7 +143,52 @@ }) & set (env . contracts . at (createAddress ethrunAddress 1)) (Just (contractWithStore x initStore)) +data BranchInfo = BranchInfo + { _vm :: VM, + _branchCondition :: Maybe Whiff + } +doInterpret :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo) +doInterpret fetcher maxIter vm = let + f (vm', cs) = Node (BranchInfo (if length cs == 0 then vm' else vm) Nothing) cs + in f <$> interpret' fetcher maxIter vm + +interpret' :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (VM, [(Tree BranchInfo)]) +interpret' fetcher maxIter vm = let + cont s = interpret' fetcher maxIter $ execState s vm + in case view EVM.result vm of + + Nothing -> cont exec1 + + Just (VMFailure (EVM.Query q@(PleaseAskSMT _ _ continue))) -> let + codelocation = getCodeLocation vm + iteration = num $ fromMaybe 0 $ view (iterations . at codelocation) vm + -- as an optimization, we skip consulting smt + -- if we've been at the location less than 5 times + in if iteration < (max (fromMaybe 0 maxIter) 5) + then cont $ continue EVM.Unknown + else io (fetcher q) >>= cont + + Just (VMFailure (EVM.Query q)) -> io (fetcher q) >>= cont + + Just (VMFailure (Choose (EVM.PleaseChoosePath whiff continue))) + -> case maxIterationsReached vm maxIter of + Nothing -> let + lvm = execState (continue True) vm + rvm = execState (continue False) vm + in do + push 1 + (leftvm, left) <- interpret' fetcher maxIter lvm + pop 1 + push 1 + (rightvm, right) <- interpret' fetcher maxIter rvm + pop 1 + return (vm, [Node (BranchInfo leftvm (Just whiff)) left, Node (BranchInfo rightvm (Just whiff)) right]) + Just n -> cont $ continue (not n) + + Just _ + -> return (vm, []) + -- | Interpreter which explores all paths at -- | branching points. -- | returns a list of possible final evm states @@ -159,34 +214,38 @@ exec >>= interpret fetcher maxIter . k Stepper.Run -> run >>= interpret fetcher maxIter . k - Stepper.Ask (EVM.PleaseChoosePath continue) -> do + Stepper.Ask (EVM.PleaseChoosePath _ continue) -> do vm <- get case maxIterationsReached vm maxIter of - Nothing -> do push 1 - a <- interpret fetcher maxIter (Stepper.evm (continue True) >>= k) - put vm - pop 1 - push 1 - b <- interpret fetcher maxIter (Stepper.evm (continue False) >>= k) - pop 1 - return $ a <> b - Just n -> interpret fetcher maxIter (Stepper.evm (continue (not n)) >>= k) + Nothing -> do + push 1 + a <- interpret fetcher maxIter (Stepper.evm (continue True) >>= k) + put vm + pop 1 + push 1 + b <- interpret fetcher maxIter (Stepper.evm (continue False) >>= k) + pop 1 + return $ a <> b + Just n -> + interpret fetcher maxIter (Stepper.evm (continue (not n)) >>= k) Stepper.Wait q -> do - let performQuery = - do m <- liftIO (fetcher q) - interpret fetcher maxIter (Stepper.evm m >>= k) + let performQuery = do + m <- liftIO (fetcher q) + interpret fetcher maxIter (Stepper.evm m >>= k) case q of PleaseAskSMT _ _ continue -> do codelocation <- getCodeLocation <$> get - iters <- use (iterations . at codelocation) - case iters of - -- if this is the first time we are branching at this point, - -- explore both branches without consulting SMT. - -- Exploring too many branches is a lot cheaper than - -- consulting our SMT solver. - Nothing -> interpret fetcher maxIter (Stepper.evm (continue EVM.Unknown) >>= k) - _ -> performQuery + iteration <- num <$> fromMaybe 0 <$> use (iterations . at codelocation) + + -- if this is the first time we are branching at this point, + -- explore both branches without consulting SMT. + -- Exploring too many branches is a lot cheaper than + -- consulting our SMT solver. + if iteration < (max (fromMaybe 0 maxIter) 5) + then interpret fetcher maxIter (Stepper.evm (continue EVM.Unknown) >>= k) + else performQuery + _ -> performQuery Stepper.EVM m -> @@ -204,7 +263,7 @@ type Precondition = VM -> SBool type Postcondition = (VM, VM) -> SBool -checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM) +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) checkAssertions :: Postcondition @@ -212,12 +271,13 @@ Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> sFalse _ -> sTrue -verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM) +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 -- add the pre condition to the pathconditions to ensure that we are only exploring valid paths - let preState = over pathConditions ((++) [pre preStateRaw]) preStateRaw - verify preState Nothing Nothing maybepost + let preState = over constraints ((++) [(pre preStateRaw, Todo "assumptions" [])]) preStateRaw + v <- verify preState Nothing Nothing maybepost + return (v, preState) pruneDeadPaths :: [VM] -> [VM] pruneDeadPaths = @@ -225,19 +285,45 @@ Just (VMFailure DeadPath) -> False _ -> True +consistentPath :: VM -> Query (Maybe VM) +consistentPath vm = do + resetAssertions + constrain $ sAnd $ fst <$> view constraints vm + checkSat >>= \case + Sat -> return $ Just vm + Unk -> return $ Just vm -- the path may still be consistent + Unsat -> return Nothing + DSat _ -> error "unexpected DSAT" + +consistentTree :: Tree BranchInfo -> Query (Maybe (Tree BranchInfo)) +consistentTree (Node (BranchInfo vm w) []) = do + consistentPath vm >>= \case + Nothing -> return Nothing + Just vm' -> return $ Just $ Node (BranchInfo vm' w) [] +consistentTree (Node b xs) = do + consistentChildren <- catMaybes <$> forM xs consistentTree + if null consistentChildren then + return Nothing + else + return $ Just (Node b consistentChildren) + + +leaves :: Tree BranchInfo -> [VM] +leaves (Node x []) = [_vm x] +leaves (Node _ xs) = concatMap leaves xs + -- | Symbolically execute the VM and check all endstates against the postcondition, if available. --- Returns `Right VM` if the postcondition can be violated, where `VM` is a prestate counterexample, --- or `Left (VM, [VM])`, a pair of `prestate` and post vm states. -verify :: VM -> Maybe Integer -> Maybe (Fetch.BlockNumber, Text) -> Maybe Postcondition -> Query (Either (VM, [VM]) VM) +-- Returns `Right (Tree BranchInfo)` if the postcondition can be violated, or +-- or `Left (Tree BranchInfo)`, if the postcondition holds for all endstates. +verify :: VM -> Maybe Integer -> Maybe (Fetch.BlockNumber, Text) -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo)) verify preState maxIter rpcinfo maybepost = do - let model = view (env . storageModel) preState smtState <- queryState - results <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) rpcinfo model False) maxIter Stepper.runFully) preState + tree <- doInterpret (Fetch.oracle (Just smtState) rpcinfo False) maxIter preState case maybepost of (Just post) -> do - let livePaths = pruneDeadPaths results + let livePaths = pruneDeadPaths $ leaves tree -- can also do these queries individually (even concurrently!). Could save time and report multiple violations - postC = sOr $ fmap (\postState -> (sAnd (view pathConditions postState)) .&& sNot (post (preState, postState))) livePaths + postC = sOr $ fmap (\postState -> (sAnd (fst <$> view constraints postState)) .&& sNot (post (preState, postState))) livePaths -- is there any path which can possibly violate -- the postcondition? resetAssertions @@ -245,13 +331,14 @@ io $ putStrLn "checking postcondition..." checkSat >>= \case Unk -> do io $ putStrLn "postcondition query timed out" - return $ Left (preState, livePaths) + return $ Left tree Unsat -> do io $ putStrLn "Q.E.D." - return $ Left (preState, livePaths) - Sat -> return $ Right preState + return $ Left tree + Sat -> return $ Right tree + DSat _ -> error "unexpected DSAT" Nothing -> do io $ putStrLn "Nothing to check" - return $ Left (preState, pruneDeadPaths results) + return $ Left tree -- | 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) @@ -263,24 +350,24 @@ callvalue' = preStateA ^. state . callvalue prestorage = preStateA ^?! env . contracts . ix preself . storage (calldata', cdlen) = view (state . calldata) preStateA - pathconds = view pathConditions preStateA - preStateB = loadSymVM (RuntimeCode bytecodeB) prestorage SymbolicS precaller callvalue' (calldata', cdlen) & set pathConditions pathconds + pathconds = view constraints preStateA + preStateB = loadSymVM (RuntimeCode bytecodeB) prestorage SymbolicS precaller callvalue' (calldata', cdlen) & set constraints pathconds smtState <- queryState push 1 - aVMs <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) Nothing SymbolicS False) maxiter Stepper.runFully) preStateA + aVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter preStateA pop 1 push 1 - bVMs <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) Nothing SymbolicS False) maxiter Stepper.runFully) preStateB + bVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter preStateB pop 1 -- Check each pair of endstates for equality: - let differingEndStates = uncurry distinct <$> [(a,b) | a <- pruneDeadPaths aVMs, b <- pruneDeadPaths bVMs] + let differingEndStates = uncurry distinct <$> [(a,b) | a <- pruneDeadPaths (leaves aVMs), b <- pruneDeadPaths (leaves bVMs)] distinct a b = - let (aPath, bPath) = both' (view pathConditions) (a, b) + let (aPath, bPath) = both' (view constraints) (a, b) (aSelf, bSelf) = both' (view (state . contract)) (a, b) (aEnv, bEnv) = both' (view (env . contracts)) (a, b) (aResult, bResult) = both' (view result) (a, b) - (Symbolic aStorage, Symbolic bStorage) = (view storage (aEnv ^?! ix aSelf), view storage (bEnv ^?! ix bSelf)) + (Symbolic _ aStorage, Symbolic _ bStorage) = (view storage (aEnv ^?! ix aSelf), view storage (bEnv ^?! ix bSelf)) differingResults = case (aResult, bResult) of (Just (VMSuccess aOut), Just (VMSuccess bOut)) -> @@ -296,9 +383,9 @@ (Just _, Just _) -> sTrue - _ -> error "Internal error during symbolic execution (should not be possible)" + errormsg -> error $ show errormsg - in sAnd aPath .&& sAnd bPath .&& differingResults + in sAnd (fst <$> aPath) .&& sAnd (fst <$> bPath) .&& differingResults -- If there exists a pair of endstates where this is not the case, -- the following constraint is satisfiable constrain $ sOr differingEndStates @@ -306,21 +393,22 @@ checkSat >>= \case Unk -> error "solver said unknown!" Sat -> return $ Right preStateA - Unsat -> return $ Left (pruneDeadPaths aVMs, pruneDeadPaths bVMs) + Unsat -> return $ Left (leaves aVMs, leaves bVMs) + DSat _ -> error "unexpected DSAT" both' :: (a -> b) -> (a, a) -> (b, b) both' f (x, y) = (f x, f y) showCounterexample :: VM -> Maybe (Text, [AbiType]) -> Query () showCounterexample vm maybesig = do - let (calldata', cdlen) = view (EVM.state . EVM.calldata) vm + let (calldata', S _ cdlen) = view (EVM.state . EVM.calldata) vm S _ cvalue = view (EVM.state . EVM.callvalue) vm SAddr caller' = view (EVM.state . EVM.caller) vm cdlen' <- num <$> getValue cdlen calldatainput <- case calldata' of SymbolicBuffer cd -> mapM (getValue.fromSized) (take cdlen' cd) >>= return . pack ConcreteBuffer cd -> return $ BS.take cdlen' cd - callvalue' <- num <$> getValue cvalue + callvalue' <- getValue cvalue caller'' <- num <$> getValue caller' io $ do putStrLn "Calldata:" diff --git a/src/EVM/Symbolic.hs b/src/EVM/Symbolic.hs --- a/src/EVM/Symbolic.hs +++ b/src/EVM/Symbolic.hs @@ -2,52 +2,40 @@ {-# Language DataKinds #-} {-# Language OverloadedStrings #-} {-# Language TypeApplications #-} +{-# Language ScopedTypeVariables #-} module EVM.Symbolic where -import Prelude hiding (Word) +import Prelude hiding (Word, LT, GT) import qualified Data.ByteString as BS import Data.ByteString (ByteString) import Control.Lens hiding (op, (:<), (|>), (.>)) import Data.Maybe (fromMaybe, fromJust) import EVM.Types -import EVM.Concrete (Word (..), Whiff(..)) import qualified EVM.Concrete as Concrete +import qualified Data.ByteArray as BA import Data.SBV hiding (runSMT, newArray_, addAxiom, Word) - - --- | Symbolic words of 256 bits, possibly annotated with additional --- "insightful" information -data SymWord = S Whiff (SWord 256) - --- | Convenience functions transporting between the concrete and symbolic realm -sw256 :: SWord 256 -> SymWord -sw256 = S Dull +import Data.SBV.Tools.Overflow +import Crypto.Hash (Digest, SHA256) +import qualified Crypto.Hash as Crypto -litWord :: Word -> (SymWord) +litWord :: Word -> SymWord litWord (C whiff a) = S whiff (literal $ toSizzle a) -w256lit :: W256 -> SymWord -w256lit = S Dull . literal . toSizzle - litAddr :: Addr -> SAddr litAddr = SAddr . literal . toSizzle -maybeLitWord :: SymWord -> Maybe Word -maybeLitWord (S whiff a) = fmap (C whiff . fromSizzle) (unliteral a) - maybeLitAddr :: SAddr -> Maybe Addr maybeLitAddr (SAddr a) = fmap fromSizzle (unliteral a) maybeLitBytes :: [SWord 8] -> Maybe ByteString maybeLitBytes xs = fmap (\x -> BS.pack (fmap fromSized x)) (mapM unliteral xs) --- | Note: these forms are crude and in general, +-- | Note: the (force*) functions are crude and in general, -- the continuation passing style `forceConcrete` -- alternatives should be prefered for better error -- handling when used during EVM execution - forceLit :: SymWord -> Word forceLit (S whiff a) = case unliteral a of Just c -> C whiff (fromSizzle c) @@ -60,48 +48,42 @@ forceBuffer (ConcreteBuffer b) = b forceBuffer (SymbolicBuffer b) = forceLitBytes b --- | Arithmetic operations on SymWord - sdiv :: SymWord -> SymWord -> SymWord -sdiv (S _ x) (S _ y) = let sx, sy :: SInt 256 +sdiv (S a x) (S b y) = let sx, sy :: SInt 256 sx = sFromIntegral x sy = sFromIntegral y - in sw256 $ sFromIntegral (sx `sQuot` sy) + in S (Div a b) (sFromIntegral (sx `sQuot` sy)) smod :: SymWord -> SymWord -> SymWord -smod (S _ x) (S _ y) = let sx, sy :: SInt 256 +smod (S a x) (S b y) = let sx, sy :: SInt 256 sx = sFromIntegral x sy = sFromIntegral y - in sw256 $ ite (y .== 0) 0 (sFromIntegral (sx `sRem` sy)) + in S (Mod a b) $ ite (y .== 0) 0 (sFromIntegral (sx `sRem` sy)) addmod :: SymWord -> SymWord -> SymWord -> SymWord -addmod (S _ x) (S _ y) (S _ z) = let to512 :: SWord 256 -> SWord 512 +addmod (S a x) (S b y) (S c z) = let to512 :: SWord 256 -> SWord 512 to512 = sFromIntegral - in sw256 $ sFromIntegral $ ((to512 x) + (to512 y)) `sMod` (to512 z) + in S (Todo "addmod" [a, b, c]) $ sFromIntegral $ ((to512 x) + (to512 y)) `sMod` (to512 z) mulmod :: SymWord -> SymWord -> SymWord -> SymWord -mulmod (S _ x) (S _ y) (S _ z) = let to512 :: SWord 256 -> SWord 512 +mulmod (S a x) (S b y) (S c z) = let to512 :: SWord 256 -> SWord 512 to512 = sFromIntegral - in sw256 $ sFromIntegral $ ((to512 x) * (to512 y)) `sMod` (to512 z) + in S (Todo "mulmod" [a, b, c]) $ sFromIntegral $ ((to512 x) * (to512 y)) `sMod` (to512 z) +-- | Signed less than slt :: SymWord -> SymWord -> SymWord -slt (S _ x) (S _ y) = - sw256 $ ite (sFromIntegral x .< (sFromIntegral y :: (SInt 256))) 1 0 +slt (S xw x) (S yw y) = + iteWhiff (SLT xw yw) (sFromIntegral x .< (sFromIntegral y :: (SInt 256))) 1 0 +-- | Signed greater than sgt :: SymWord -> SymWord -> SymWord -sgt (S _ x) (S _ y) = - sw256 $ ite (sFromIntegral x .> (sFromIntegral y :: (SInt 256))) 1 0 - -shiftRight' :: SymWord -> SymWord -> SymWord -shiftRight' (S _ a') b@(S _ b') = case (num <$> unliteral a', b) of - (Just n, (S (FromBytes (SymbolicBuffer a)) _)) | n `mod` 8 == 0 && n <= 256 -> - let bs = replicate (n `div` 8) 0 <> (take ((256 - n) `div` 8) a) - in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs) - _ -> sw256 $ sShiftRight b' a' +sgt (S xw x) (S yw y) = + iteWhiff (SGT xw yw) (sFromIntegral x .> (sFromIntegral y :: (SInt 256))) 1 0 --- | Operations over symbolic memory (list of symbolic bytes) +-- * Operations over symbolic memory (list of symbolic bytes) swordAt :: Int -> [SWord 8] -> SymWord -swordAt i bs = sw256 . fromBytes $ truncpad 32 $ drop i bs +swordAt i bs = let bs' = truncpad 32 $ drop i bs + in S (FromBytes (SymbolicBuffer bs')) (fromBytes bs') readByteOrZero' :: Int -> [SWord 8] -> SWord 8 readByteOrZero' i bs = fromMaybe 0 (bs ^? ix i) @@ -122,7 +104,9 @@ a <> a' <> c <> b' readMemoryWord' :: Word -> [SWord 8] -> SymWord -readMemoryWord' (C _ i) m = sw256 $ fromBytes $ truncpad 32 (drop (num i) m) +readMemoryWord' (C _ i) m = + let bs = truncpad 32 (drop (num i) m) + in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs) readMemoryWord32' :: Word -> [SWord 8] -> SWord 32 readMemoryWord32' (C _ i) m = fromBytes $ truncpad 4 (drop (num i) m) @@ -147,39 +131,36 @@ where walk [] _ acc = acc walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc) --- Generates a ridiculously large set of constraints (roughly 25k) when --- the index is symbolic, but it still seems (kind of) manageable --- for the solvers. -readSWordWithBound :: SWord 32 -> Buffer -> SWord 32 -> SymWord -readSWordWithBound ind (SymbolicBuffer xs) bound = case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of +-- | Read 32 bytes from index from a bounded list of bytes. +readSWordWithBound :: SymWord -> Buffer -> SymWord -> SymWord +readSWordWithBound sind@(S _ ind) (SymbolicBuffer xs) (S _ bound) = case (num <$> maybeLitWord sind, num <$> fromSizzle <$> unliteral bound) of (Just i, Just b) -> let bs = truncpad 32 $ drop i (take b xs) in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs) - _ -> - let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]] - in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]] + _ -> + -- Generates a ridiculously large set of constraints (roughly 25k) when + -- the index is symbolic, but it still seems (kind of) manageable + -- for the solvers. -readSWordWithBound ind (ConcreteBuffer xs) bound = - case fromSized <$> unliteral ind of - Nothing -> readSWordWithBound ind (SymbolicBuffer (litBytes xs)) bound - Just x' -> + -- The proper solution here is to use smt arrays instead. + + let boundedList = [ite (i .<= bound) x' 0 | (x', i) <- zip xs [1..]] + res = [select' boundedList 0 (ind + j) | j <- [0..31]] + in S (FromBytes $ SymbolicBuffer res) $ fromBytes res + +readSWordWithBound sind (ConcreteBuffer xs) bound = + case maybeLitWord sind of + Nothing -> readSWordWithBound sind (SymbolicBuffer (litBytes xs)) bound + Just x' -> -- INVARIANT: bound should always be length xs for concrete bytes -- so we should be able to safely ignore it here - litWord $ Concrete.readMemoryWord (num x') xs + litWord $ Concrete.readMemoryWord x' xs -- a whole foldable instance seems overkill, but length is always good to have! len :: Buffer -> Int len (SymbolicBuffer bs) = length bs len (ConcreteBuffer bs) = BS.length bs -grab :: Int -> Buffer -> Buffer -grab n (SymbolicBuffer bs) = SymbolicBuffer $ take n bs -grab n (ConcreteBuffer bs) = ConcreteBuffer $ BS.take n bs - -ditch :: Int -> Buffer -> Buffer -ditch n (SymbolicBuffer bs) = SymbolicBuffer $ drop n bs -ditch n (ConcreteBuffer bs) = ConcreteBuffer $ BS.drop n bs - readByteOrZero :: Int -> Buffer -> SWord 8 readByteOrZero i (SymbolicBuffer bs) = readByteOrZero' i bs readByteOrZero i (ConcreteBuffer bs) = num $ Concrete.readByteOrZero i bs @@ -222,65 +203,115 @@ readSWord i (SymbolicBuffer x) = readSWord' i x readSWord i (ConcreteBuffer x) = num $ Concrete.readMemoryWord i x --- | Custom instances for SymWord, many of which have direct --- analogues for concrete words defined in Concrete.hs +-- * Uninterpreted functions -instance Show SymWord where - show s@(S Dull _) = case maybeLitWord s of - Nothing -> "" - Just w -> show w - show (S (Var var) x) = var ++ ": " ++ show x - show (S (InfixBinOp symbol x y) z) = show x ++ symbol ++ show y ++ ": " ++ show z - show (S (BinOp symbol x y) z) = symbol ++ show x ++ show y ++ ": " ++ show z - show (S (UnOp symbol x) z) = symbol ++ show x ++ ": " ++ show z - show (S whiff x) = show whiff ++ ": " ++ show x +symSHA256N :: SInteger -> SInteger -> SWord 256 +symSHA256N = uninterpret "sha256" -instance EqSymbolic SymWord where - (.==) (S _ x) (S _ y) = x .== y +symkeccakN :: SInteger -> SInteger -> SWord 256 +symkeccakN = uninterpret "keccak" -instance Num SymWord where - (S _ x) + (S _ y) = sw256 (x + y) - (S _ x) * (S _ y) = sw256 (x * y) - abs (S _ x) = sw256 (abs x) - signum (S _ x) = sw256 (signum x) - fromInteger x = sw256 (fromInteger x) - negate (S _ x) = sw256 (negate x) +toSInt :: [SWord 8] -> SInteger +toSInt bs = sum $ zipWith (\a (i :: Integer) -> sFromIntegral a * 256 ^ i) bs [0..] -instance Bits SymWord where - (S _ x) .&. (S _ y) = sw256 (x .&. y) - (S _ x) .|. (S _ y) = sw256 (x .|. y) - (S _ x) `xor` (S _ y) = sw256 (x `xor` y) - complement (S _ x) = sw256 (complement x) - shift (S _ x) i = sw256 (shift x i) - rotate (S _ x) i = sw256 (rotate x i) - bitSize (S _ x) = bitSize x - bitSizeMaybe (S _ x) = bitSizeMaybe x - isSigned (S _ x) = isSigned x - testBit (S _ x) i = testBit x i - bit i = sw256 (bit i) - popCount (S _ x) = popCount x -instance SDivisible SymWord where - sQuotRem (S _ x) (S _ y) = let (a, b) = x `sQuotRem` y - in (sw256 a, sw256 b) - sDivMod (S _ x) (S _ y) = let (a, b) = x `sDivMod` y - in (sw256 a, sw256 b) +-- | Although we'd like to define this directly as an uninterpreted function, +-- we cannot because [a] is not a symbolic type. We must convert the list into a suitable +-- symbolic type first. The only important property of this conversion is that it is injective. +-- We embedd the bytestring as a pair of symbolic integers, this is a fairly easy solution. +symkeccak' :: [SWord 8] -> SWord 256 +symkeccak' bytes = case length bytes of + 0 -> literal $ toSizzle $ keccak "" + n -> symkeccakN (num n) (toSInt bytes) -instance Mergeable SymWord where - symbolicMerge a b (S _ x) (S _ y) = sw256 $ symbolicMerge a b x y - select xs (S _ x) b = let ys = fmap (\(S _ y) -> y) xs - in sw256 $ select ys x b +symSHA256 :: [SWord 8] -> [SWord 8] +symSHA256 bytes = case length bytes of + 0 -> litBytes $ BS.pack $ BA.unpack $ (Crypto.hash BS.empty :: Digest SHA256) + n -> toBytes $ symSHA256N (num n) (toSInt bytes) -instance Bounded SymWord where - minBound = sw256 minBound - maxBound = sw256 maxBound +rawVal :: SymWord -> SWord 256 +rawVal (S _ v) = v -instance Eq SymWord where - (S _ x) == (S _ y) = x == y +-- | Reconstruct the smt/sbv value from a whiff +-- Should satisfy (rawVal x .== whiffValue x) +whiffValue :: Whiff -> SWord 256 +whiffValue w = case w of + w'@(Todo _ _) -> error $ "unable to get value of " ++ show w' + And x y -> whiffValue x .&. whiffValue y + Or x y -> whiffValue x .|. whiffValue y + Eq x y -> ite (whiffValue x .== whiffValue y) 1 0 + LT x y -> ite (whiffValue x .< whiffValue y) 1 0 + GT x y -> ite (whiffValue x .> whiffValue y) 1 0 + ITE b x y -> ite (whiffValue b .== 1) (whiffValue x) (whiffValue y) + SLT x y -> rawVal $ slt (S x (whiffValue x)) (S y (whiffValue y)) + SGT x y -> rawVal $ sgt (S x (whiffValue x)) (S y (whiffValue y)) + IsZero x -> ite (whiffValue x .== 0) 1 0 + SHL x y -> sShiftLeft (whiffValue x) (whiffValue y) + SHR x y -> sShiftRight (whiffValue x) (whiffValue y) + SAR x y -> sSignedShiftArithRight (whiffValue x) (whiffValue y) + Add x y -> whiffValue x + whiffValue y + Sub x y -> whiffValue x - whiffValue y + Mul x y -> whiffValue x * whiffValue y + Div x y -> whiffValue x `sDiv` whiffValue y + Mod x y -> whiffValue x `sMod` whiffValue y + Exp x y -> whiffValue x .^ whiffValue y + Neg x -> negate $ whiffValue x + Var _ v -> v + FromKeccak (ConcreteBuffer bstr) -> literal $ num $ keccak bstr + FromKeccak (SymbolicBuffer buf) -> symkeccak' buf + Literal x -> literal $ num $ x + FromBytes buf -> rawVal $ readMemoryWord 0 buf + FromStorage ind arr -> readArray arr (whiffValue ind) -instance Enum SymWord where - toEnum i = sw256 (toEnum i) - fromEnum (S _ x) = fromEnum x +-- | Special cases that have proven useful in practice +simplifyCondition :: SBool -> Whiff -> SBool +simplifyCondition _ (IsZero (IsZero (IsZero a))) = whiffValue a .== 0 -instance OrdSymbolic SymWord where - (.<) (S _ x) (S _ y) = (.<) x y + + +-- | Overflow safe math can be difficult for smt solvers to deal with, +-- especially for 256-bit words. When we recognize terms arising from +-- overflow checks, we translate our queries into a more bespoke form, +-- outlined in: +-- Modular Bug-finding for Integer Overflows in the Large: +-- Sound, Efficient, Bit-precise Static Analysis +-- www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf +-- +-- Addition overflow. +-- Written as +-- require (x <= (x + y)) +-- or require (y <= (x + y)) +-- or require (!(y < (x + y))) +simplifyCondition b (IsZero (IsZero (LT (Add x y) z))) = + let x' = whiffValue x + y' = whiffValue y + z' = whiffValue z + (_, overflow) = bvAddO x' y' + in + ite (x' .== z' .|| + y' .== z') + overflow + b + +-- Multiplication overflow. +-- Written as +-- require (y == 0 || x * y / y == x) +-- or require (y == 0 || x == x * y / y) + +-- proveWith cvc4 $ \x y z -> ite (y .== (z :: SWord 8)) (((x * y) `sDiv` z ./= x) .<=> (snd (bvMulO x y) .|| (z .== 0 .&& x .> 0))) (sTrue) +-- Q.E.D. +simplifyCondition b (IsZero (Eq x (Div (Mul y z) w))) = + simplifyCondition b (IsZero (Eq (Div (Mul y z) w) x)) +simplifyCondition b (IsZero (Eq (Div (Mul y z) w) x)) = + let x' = whiffValue x + y' = whiffValue y + z' = whiffValue z + w' = whiffValue w + (_, overflow) = bvMulO y' z' + in + ite + ((y' .== x' .&& z' .== w') .|| + (z' .== x' .&& y' .== w')) + (overflow .|| (w' .== 0 .&& x' ./= 0)) + b +simplifyCondition b _ = b diff --git a/src/EVM/TTY.hs b/src/EVM/TTY.hs --- a/src/EVM/TTY.hs +++ b/src/EVM/TTY.hs @@ -12,9 +12,8 @@ import EVM import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi) -import EVM.Symbolic (SymWord(..)) -import EVM.SymExec (maxIterationsReached) -import EVM.Dapp (DappInfo, dappInfo) +import EVM.SymExec (maxIterationsReached, symCalldata) +import EVM.Dapp (DappInfo, dappInfo, Test, extractSig, Test(..)) import EVM.Dapp (dappUnitTests, unitTestMethods, dappSolcByName, dappSolcByHash, dappSources) import EVM.Dapp (dappAstSrcMap) import EVM.Debug @@ -22,10 +21,9 @@ import EVM.Format (contractNamePart, contractPathPart, showTraceTree) import EVM.Hexdump (prettyHex) import EVM.Op -import EVM.Solidity +import EVM.Solidity hiding (storageLayout) import EVM.Types hiding (padRight) -import EVM.UnitTest (UnitTestOptions (..)) -import EVM.UnitTest (initialUnitTestVm, initializeUnitTest, runUnitTest) +import EVM.UnitTest import EVM.StorageLayout import EVM.Stepper (Stepper) @@ -35,6 +33,7 @@ import EVM.Fetch (Fetcher) import Control.Lens +import Control.Monad.Trans.Reader import Control.Monad.State.Strict hiding (state) import Data.Aeson.Lens @@ -44,10 +43,11 @@ import Data.Monoid ((<>)) import Data.Text (Text, pack) import Data.Text.Encoding (decodeUtf8) -import Data.List (sort, lookup) +import Data.List (sort, find) import Data.Version (showVersion) import Data.SBV hiding (solver) +import qualified Data.SBV.Internals as SBV import qualified Data.ByteString as BS import qualified Data.Map as Map import qualified Data.Text as Text @@ -78,13 +78,7 @@ , _uiStep :: Int , _uiSnapshots :: Map Int (VM, Stepper ()) , _uiStepper :: Stepper () - , _uiStackList :: List Name (Int, (SymWord)) - , _uiBytecodeList :: List Name (Int, Op) - , _uiTraceList :: List Name Text - , _uiSolidityList :: List Name (Int, ByteString) - , _uiMessage :: Maybe String , _uiShowMemory :: Bool - , _uiSolc :: Maybe SolcContract , _uiTestOpts :: UnitTestOptions } @@ -152,9 +146,19 @@ eval (action Operational.:>>= k) = case action of + Stepper.Run -> do + -- Have we reached the final result of this action? + use (uiVm . result) >>= \case + Just _ -> do + -- Yes, proceed with the next action. + vm <- use uiVm + interpret mode (k vm) + Nothing -> do + -- No, keep performing the current action + keepExecuting mode (Stepper.run >>= k) + -- Stepper wants to keep executing? Stepper.Exec -> do - -- Have we reached the final result of this action? use (uiVm . result) >>= \case Just r -> @@ -162,32 +166,10 @@ interpret mode (k r) Nothing -> do -- No, keep performing the current action - let restart = Stepper.exec >>= k - - case mode of - Step 0 -> do - -- We come here when we've continued while stepping, - -- either from a query or from a return; - -- we should pause here and wait for the user. - pure (Continue restart) - - Step i -> do - -- Run one instruction and recurse - stepOneOpcode restart - interpret (Step (i - 1)) restart - - StepUntil p -> do - vm <- use uiVm - case p vm of - True -> - interpret (Step 0) restart - False -> do - -- Run one instruction and recurse - stepOneOpcode restart - interpret (StepUntil p) restart + keepExecuting mode (Stepper.exec >>= k) -- Stepper is waiting for user input from a query - Stepper.Ask (EVM.PleaseChoosePath cont) -> do + Stepper.Ask (PleaseChoosePath _ cont) -> do -- ensure we aren't stepping past max iterations vm <- use uiVm case maxIterationsReached vm ?maxIter of @@ -206,6 +188,33 @@ assign uiVm vm1 interpret mode (Stepper.exec >> (k r)) +keepExecuting :: (?fetcher :: Fetcher + , ?maxIter :: Maybe Integer) + => StepMode + -> Stepper a + -> StateT UiVmState IO (Continuation a) +keepExecuting mode restart = case mode of + Step 0 -> do + -- We come here when we've continued while stepping, + -- either from a query or from a return; + -- we should pause here and wait for the user. + pure (Continue restart) + + Step i -> do + -- Run one instruction and recurse + stepOneOpcode restart + interpret (Step (i - 1)) restart + + StepUntil p -> do + vm <- use uiVm + if p vm + then + interpret (Step 0) restart + else do + -- Run one instruction and recurse + stepOneOpcode restart + interpret (StepUntil p) restart + isUnitTestContract :: Text -> DappInfo -> Bool isUnitTestContract name dapp = elem name (map fst (view dappUnitTests dapp)) @@ -224,6 +233,9 @@ { oracle = oracle' , verbose = Nothing , maxIter = maxIter' + , smtTimeout = Nothing + , smtState = Nothing + , solver = Nothing , match = "" , fuzzRuns = 1 , replay = error "irrelevant" @@ -242,18 +254,11 @@ initUiVmState :: VM -> UnitTestOptions -> Stepper () -> UiVmState initUiVmState vm0 opts script = - renderVm $ UiVmState { _uiVm = vm0 , _uiStepper = script - , _uiStackList = undefined - , _uiBytecodeList = undefined - , _uiTraceList = undefined - , _uiSolidityList = undefined - , _uiSolc = currentSolc (dapp opts) vm0 , _uiStep = 0 , _uiSnapshots = singleton 0 (vm0, script) - , _uiMessage = Just "Creating unit test contract" , _uiShowMemory = False , _uiTestOpts = opts } @@ -261,13 +266,16 @@ -- filters out fuzztests, unless they have -- explicitly been given an argument by `replay` -concreteTests :: UnitTestOptions -> (Text, [(Text, [AbiType])]) -> [(Text, Text)] -concreteTests UnitTestOptions{..} (contractname, tests) = case replay of - Nothing -> [(contractname, fst x) | x <- tests, - null $ snd x] - Just (sig, _) -> [(contractname, fst x) | x <- tests, - null (snd x) || fst x == sig] +debuggableTests :: UnitTestOptions -> (Text, [(Test, [AbiType])]) -> [(Text, Text)] +debuggableTests UnitTestOptions{..} (contractname, tests) = case replay of + Nothing -> [(contractname, extractSig $ fst x) | x <- tests, not $ isFuzzTest x] + Just (sig, _) -> [(contractname, extractSig $ fst x) | x <- tests, not (isFuzzTest x) || extractSig (fst x) == sig] +isFuzzTest :: (Test, [AbiType]) -> Bool +isFuzzTest (SymbolicTest _, _) = False +isFuzzTest (ConcreteTest _, []) = False +isFuzzTest (ConcreteTest _, _) = True + main :: UnitTestOptions -> FilePath -> FilePath -> IO () main opts root jsonFilePath = readSolc jsonFilePath >>= @@ -283,7 +291,7 @@ TestPickerPane (Vec.fromList (concatMap - (concreteTests opts) + (debuggableTests opts) (view dappUnitTests dapp))) 1 , _testPickerDapp = dapp @@ -307,14 +315,53 @@ continue (ViewVm (ui' & set uiStepper steps)) where m = interpret mode (view uiStepper ui) - nxt = runStateT (m <* modify renderVm) ui + nxt = runStateT m ui +backstepUntil + :: (?fetcher :: Fetcher + ,?maxIter :: Maybe Integer) + => (UiVmState -> Pred VM) -> UiVmState -> EventM n (Next UiState) +backstepUntil p s = + case view uiStep s of + 0 -> continue (ViewVm s) + n -> do + s1 <- backstep s + let + -- find a previous vm that satisfies the predicate + snapshots' = Data.Map.filter (p s1 . fst) (view uiSnapshots s1) + case lookupLT n snapshots' of + -- If no such vm exists, go to the beginning + Nothing -> + let + (step', (vm', stepper')) = fromJust $ lookupLT (n - 1) (view uiSnapshots s) + s2 = s1 + & set uiVm vm' + & set (uiVm . cache) (view (uiVm . cache) s1) + & set uiStep step' + & set uiStepper stepper' + in takeStep s2 (Step 0) + -- step until the predicate doesn't hold + Just (step', (vm', stepper')) -> + let + s2 = s1 + & set uiVm vm' + & set (uiVm . cache) (view (uiVm . cache) s1) + & set uiStep step' + & set uiStepper stepper' + in takeStep s2 (StepUntil (not . p s1)) + backstep :: (?fetcher :: Fetcher ,?maxIter :: Maybe Integer) => UiVmState -> EventM n UiVmState backstep s = case view uiStep s of + -- We're already at the first step; ignore command. 0 -> return s + -- To step backwards, we revert to the previous snapshot + -- and execute n - 1 `mod` snapshotInterval steps from there. + + -- We keep the current cache so we don't have to redo + -- any blocking queries, and also the memory view. n -> let (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s) @@ -357,7 +404,7 @@ let opts = view uiTestOpts s dapp' = dapp (view uiTestOpts s) tests = concatMap - (concreteTests opts) + (debuggableTests opts) (view dappUnitTests dapp') in case tests of [] -> halt st @@ -408,25 +455,32 @@ suspendAndResume $ Readline.runInputT Readline.defaultSettings loop +-- todo refactor to zipper step forward -- Vm Overview: n - step appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'n') [])) = - case view (uiVm . result) s of - Just _ -> continue (ViewVm s) - _ -> takeStep s (Step 1) + if isJust $ view (uiVm . result) s + then continue (ViewVm s) + else takeStep s (Step 1) -- Vm Overview: N - step appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'N') [])) = - takeStep s - (StepUntil (isNextSourcePosition s)) + if isJust $ view (uiVm . result) s + then continue (ViewVm s) + else takeStep s + (StepUntil (isNextSourcePosition s)) -- Vm Overview: C-n - step appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'n') [V.MCtrl])) = - takeStep s + if isJust $ view (uiVm . result) s + then continue (ViewVm s) + else takeStep s (StepUntil (isNextSourcePositionWithoutEntering s)) -- Vm Overview: e - step appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'e') [])) = - takeStep s + if isJust $ view (uiVm . result) s + then continue (ViewVm s) + else takeStep s (StepUntil (isExecutionHalted s)) -- Vm Overview: a - step @@ -452,88 +506,32 @@ n -> do -- To step backwards, we revert to the previous snapshot -- and execute n - 1 `mod` snapshotInterval steps from there. - -- + -- We keep the current cache so we don't have to redo -- any blocking queries, and also the memory view. let (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s) s1 = s - & set uiVm vm - & set (uiVm . cache) (view (uiVm . cache) s) + & set uiVm vm -- set the vm to the one from the snapshot + & set (uiVm . cache) (view (uiVm . cache) s) -- persist the cache & set uiStep step & set uiStepper stepper stepsToTake = n - step - 1 takeStep s1 (Step stepsToTake) --- Vm Overview: P - backstep -appEvent st@(ViewVm s) (VtyEvent (V.EvKey (V.KChar 'P') [])) = - case view uiStep s of - 0 -> - -- We're already at the first step; ignore command. - continue st - n -> do - s1 <- backstep s - let - -- find a vm with a different source location than s1 - snapshots' = Data.Map.filter (isNextSourcePosition s1 . fst) (view uiSnapshots s1) - case lookupLT n snapshots' of - -- s2 source position is the first one. Go to the beginning. - Nothing -> - let - (step', (vm', stepper')) = fromJust $ lookupLT (n - 1) (view uiSnapshots s) - s2 = s1 - & set uiVm vm' - & set (uiVm . cache) (view (uiVm . cache) s1) - & set uiStep step' - & set uiStepper stepper' - in takeStep s2 (Step 0) - -- step until we reach the source location of s1 - Just (step', (vm', stepper')) -> - let - s2 = s1 - & set uiVm vm' - & set (uiVm . cache) (view (uiVm . cache) s1) - & set uiStep step' - & set uiStepper stepper' - in takeStep s2 (StepUntil (not . isNextSourcePosition s1)) +-- Vm Overview: P - backstep to previous source +appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'P') [])) = + backstepUntil isNextSourcePosition s --- Vm Overview: c-p - backstep -appEvent st@(ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [V.MCtrl])) = - case view uiStep s of - 0 -> - -- We're already at the first step; ignore command. - continue st - n -> do - s1 <- backstep s - let - -- find a vm with a different source location than s1 - snapshots' = Data.Map.filter (isNextSourcePositionWithoutEntering s1 . fst) (view uiSnapshots s1) - case lookupLT n snapshots' of - -- s2 source position is the first one. Go to the beginning. - Nothing -> - let - (step', (vm', stepper')) = fromJust $ lookupLT (n - 1) (view uiSnapshots s) - s2 = s1 - & set uiVm vm' - & set (uiVm . cache) (view (uiVm . cache) s1) - & set uiStep step' - & set uiStepper stepper' - in takeStep s2 (Step 0) - -- step until we reach the source location of s1 - Just (step', (vm', stepper')) -> - let - s2 = s1 - & set uiVm vm' - & set (uiVm . cache) (view (uiVm . cache) s1) - & set uiStep step' - & set uiStepper stepper' - in takeStep s2 (StepUntil (not . isNextSourcePosition s1)) +-- Vm Overview: c-p - backstep to previous source avoiding CALL and CREATE +appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [V.MCtrl])) = + backstepUntil isNextSourcePositionWithoutEntering s -- Vm Overview: 0 - choose no jump appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '0') [])) = case view (uiVm . result) s of - Just (VMFailure (Choose (PleaseChoosePath contin))) -> + Just (VMFailure (Choose (PleaseChoosePath _ contin))) -> takeStep (s & set uiStepper (Stepper.evm (contin True) >> (view uiStepper s))) (Step 1) _ -> continue (ViewVm s) @@ -541,7 +539,7 @@ -- Vm Overview: 1 - choose jump appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '1') [])) = case view (uiVm . result) s of - Just (VMFailure (Choose (PleaseChoosePath contin))) -> + Just (VMFailure (Choose (PleaseChoosePath _ contin))) -> takeStep (s & set uiStepper (Stepper.evm (contin False) >> (view uiStepper s))) (Step 1) _ -> continue (ViewVm s) @@ -560,10 +558,9 @@ appEvent (ViewPicker s) (VtyEvent (V.EvKey V.KEnter [])) = case listSelectedElement (view testPickerList s) of Nothing -> error "nothing selected" - Just (_, x) -> - continue . ViewVm $ - initialUiVmStateForTest (view testOpts s) x --- (view testPickerDapp s) x + Just (_, x) -> do + initVm <- liftIO $ initialUiVmStateForTest (view testOpts s) x + continue . ViewVm $ initVm -- UnitTest Picker: (main) - render list appEvent (ViewPicker s) (VtyEvent e) = do @@ -574,12 +571,21 @@ continue (ViewPicker s') -- Page: Down - scroll -appEvent s (VtyEvent (V.EvKey V.KDown [])) = - vScrollBy (viewportScroll TracePane) 1 >> continue s +appEvent (ViewVm s) (VtyEvent (V.EvKey V.KDown [])) = + if view uiShowMemory s then + vScrollBy (viewportScroll TracePane) 1 >> continue (ViewVm s) + else + if isJust $ view (uiVm . result) s + then continue (ViewVm s) + else takeStep s + (StepUntil (isNewTraceAdded s)) -- Page: Up - scroll -appEvent s (VtyEvent (V.EvKey V.KUp [])) = - vScrollBy (viewportScroll TracePane) (-1) >> continue s +appEvent (ViewVm s) (VtyEvent (V.EvKey V.KUp [])) = + if view uiShowMemory s then + vScrollBy (viewportScroll TracePane) (-1) >> continue (ViewVm s) + else + backstepUntil isNewTraceAdded s -- Page: C-f - Page down appEvent s (VtyEvent (V.EvKey (V.KChar 'f') [V.MCtrl])) = @@ -607,23 +613,29 @@ initialUiVmStateForTest :: UnitTestOptions -> (Text, Text) - -> UiVmState -initialUiVmStateForTest opts@UnitTestOptions{..} (theContractName, theTestName) = - ui + -> IO UiVmState +initialUiVmStateForTest opts@UnitTestOptions{..} (theContractName, theTestName) = do + let state' = fromMaybe (error "Internal Error: missing smtState") smtState + (buf, len) <- flip runReaderT state' $ SBV.runQueryT $ symCalldata theTestName types [] + let script = do + Stepper.evm . pushTrace . EntryTrace $ + "test " <> theTestName <> " (" <> theContractName <> ")" + initializeUnitTest opts testContract + case test of + ConcreteTest _ -> do + let args = case replay of + Nothing -> emptyAbi + Just (sig, callData) -> + if theTestName == sig + then decodeAbiValue (AbiTupleType (Vec.fromList types)) callData + else emptyAbi + 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))) + pure $ initUiVmState vm0 opts script where - Just typesig = lookup theTestName (unitTestMethods testContract) - args = case replay of - Nothing -> emptyAbi - Just (sig, callData) -> - if theTestName == sig - then decodeAbiValue (AbiTupleType (Vec.fromList typesig)) callData - else emptyAbi - script = do - Stepper.evm . pushTrace . EntryTrace $ - "test " <> theTestName <> " (" <> theContractName <> ")" - initializeUnitTest opts - void (runUnitTest opts theTestName args) - ui = initUiVmState vm0 opts script + Just (test, types) = find (\(test',_) -> extractSig test' == theTestName) $ unitTestMethods testContract Just testContract = view (dappSolcByName . at theContractName) dapp vm0 = @@ -661,8 +673,8 @@ "m Toggle memory pane\n" <> "0 Choose the branch which does not jump \n" <> "1 Choose the branch which does jump \n" <> - "Down Scroll memory pane fwds\n" <> - "Up Scroll memory pane back\n" <> + "Down Step to next entry in the callstack / Scroll memory pane\n" <> + "Up Step to previous entry in the callstack / Scroll memory pane\n" <> "C-f Page memory pane fwds\n" <> "C-b Page memory pane back\n\n" <> "Enter Contracts browser" @@ -711,27 +723,27 @@ , txt ("Storage: " <> storageDisplay (view storage c)) ] ] - Just solc -> + Just sol -> hBox [ borderWithLabel (txt "Contract information") . padBottom Max . padRight (Pad 2) $ vBox - [ txt "Name: " <+> txt (contractNamePart (view contractName solc)) - , txt "File: " <+> txt (contractPathPart (view contractName solc)) + [ txt "Name: " <+> txt (contractNamePart (view contractName sol)) + , txt "File: " <+> txt (contractPathPart (view contractName sol)) , txt " " , txt "Constructor inputs:" - , vBox . flip map (view constructorInputs solc) $ + , vBox . flip map (view constructorInputs sol) $ \(name, abiType) -> txt (" " <> name <> ": " <> abiTypeSolidity abiType) , txt "Public methods:" - , vBox . flip map (sort (Map.elems (view abiMap solc))) $ + , vBox . flip map (sort (Map.elems (view abiMap sol))) $ \method -> txt (" " <> view methodSignature method) , txt ("Storage:" <> storageDisplay (view storage c)) ] , borderWithLabel (txt "Storage slots") . padBottom Max . padRight Max $ vBox - (map txt (storageLayout dapp' solc)) + (map txt (storageLayout dapp' sol)) ] ] ] where storageDisplay (Concrete s) = pack ( show ( Map.toList s)) - storageDisplay (Symbolic _) = pack "" + storageDisplay (Symbolic v _) = pack $ show v dapp' = dapp (view (browserVm . uiTestOpts) ui) Just (_, (_, c)) = listSelectedElement (view browserContractList ui) -- currentContract = view (dappSolcByHash . ix ) dapp @@ -794,6 +806,13 @@ modifying uiVm (execState exec1) modifying uiStep (+ 1) +isNewTraceAdded + :: UiVmState -> Pred VM +isNewTraceAdded ui vm = + let + currentTraceTree = length <$> traceForest (view uiVm ui) + newTraceTree = length <$> traceForest vm + in currentTraceTree /= newTraceTree isNextSourcePosition :: UiVmState -> Pred VM @@ -833,82 +852,24 @@ currentSrcMap :: DappInfo -> VM -> Maybe SrcMap currentSrcMap dapp vm = let - this = vm ^?! env . contracts . ix (view (state . codeContract) vm) + Just this = currentContract vm i = (view opIxMap this) SVec.! (view (state . pc) vm) h = view codehash this in case preview (dappSolcByHash . ix h) dapp of Nothing -> Nothing - Just (Creation, solc) -> - preview (creationSrcmap . ix i) solc - Just (Runtime, solc) -> - preview (runtimeSrcmap . ix i) solc - -currentSolc :: DappInfo -> VM -> Maybe SolcContract -currentSolc dapp vm = - let - this = vm ^?! env . contracts . ix (view (state . contract) vm) - h = view codehash this - in - preview (dappSolcByHash . ix h . _2) dapp - -renderVm :: UiVmState -> UiVmState -renderVm ui = updateUiVmState ui (view uiVm ui) - -updateUiVmState :: UiVmState -> VM -> UiVmState -updateUiVmState ui vm = - let - move = maybe id listMoveTo (vmOpIx vm) - address = view (state . contract) vm - message = - case view result vm of - Just (VMSuccess (ConcreteBuffer msg)) -> - Just ("VMSuccess: " <> (show $ ByteStringS msg)) - Just (VMSuccess (SymbolicBuffer msg)) -> - Just ("VMSuccess: " <> (show msg)) - Just (VMFailure (Revert msg)) -> - Just ("VMFailure: " <> (show . ByteStringS $ msg)) - Just (VMFailure err) -> - Just ("VMFailure: " <> show err) - Nothing -> - Just ("Executing EVM code in " <> show address) - in ui - & set uiVm vm - & set uiStackList - (list StackPane (Vec.fromList $ zip [1..] (view (state . stack) vm)) 2) - & set uiBytecodeList - (move $ list BytecodePane - (view codeOps (fromJust (currentContract vm))) - 1) - & set uiMessage message - & set uiTraceList - (list - TracePane - (Vec.fromList - . Text.lines - . showTraceTree dapp' - $ vm) - 1) - & set uiSolidityList - (list SolidityPane - (case currentSrcMap dapp' vm of - Nothing -> mempty - Just x -> - view (dappSources - . sourceLines - . ix (srcMapFile x) - . to (Vec.imap (,))) - dapp') - 1) - where - dapp' = dapp (view uiTestOpts ui) + Just (Creation, sol) -> + preview (creationSrcmap . ix i) sol + Just (Runtime, sol) -> + preview (runtimeSrcmap . ix i) sol drawStackPane :: UiVmState -> UiWidget drawStackPane ui = let gasText = showWordExact (view (uiVm . state . gas) ui) labelText = txt ("Gas available: " <> gasText <> "; stack:") + stackList = list StackPane (Vec.fromList $ zip [(1 :: Int)..] (view (uiVm . state . stack) ui)) 2 in hBorderWithLabel labelText <=> renderList (\_ (i, x@(S _ w)) -> @@ -920,18 +881,40 @@ Just u -> showWordExplanation (fromSizzle u) $ dapp (view uiTestOpts ui))) ]) False - (view uiStackList ui) + stackList +message :: VM -> String +message vm = + case view result vm of + Just (VMSuccess (ConcreteBuffer msg)) -> + "VMSuccess: " <> (show $ ByteStringS msg) + Just (VMSuccess (SymbolicBuffer msg)) -> + "VMSuccess: " <> (show msg) + Just (VMFailure (Revert msg)) -> + "VMFailure: " <> (show . ByteStringS $ msg) + Just (VMFailure err) -> + "VMFailure: " <> show err + Nothing -> + "Executing EVM code in " <> show (view (state . contract) vm) + + drawBytecodePane :: UiVmState -> UiWidget drawBytecodePane ui = - hBorderWithLabel (case view uiMessage ui of { Nothing -> str ""; Just s -> str s }) <=> + let + vm = view uiVm ui + move = maybe id listMoveTo $ vmOpIx vm + in + hBorderWithLabel (str $ message vm) <=> Centered.renderList (\active x -> if not active then withDefAttr dimAttr (opWidget x) else withDefAttr boldAttr (opWidget x)) False - (view uiBytecodeList ui) + (move $ list BytecodePane + (view codeOps (fromJust (currentContract vm))) + 1) + dim :: Widget n -> Widget n dim = withDefAttr dimAttr @@ -945,30 +928,57 @@ drawTracePane :: UiVmState -> UiWidget drawTracePane s = - case view uiShowMemory s of + let vm = view uiVm s + dapp' = dapp (view uiTestOpts s) + traceList = + list + TracePane + (Vec.fromList + . Text.lines + . showTraceTree dapp' + $ vm) + 1 + + in case view uiShowMemory s of True -> hBorderWithLabel (txt "Calldata") - <=> str (prettyIfConcrete $ fst (view (uiVm . state . calldata) s)) + <=> str (prettyIfConcrete $ fst (view (state . calldata) vm)) <=> hBorderWithLabel (txt "Returndata") - <=> str (prettyIfConcrete (view (uiVm . state . returndata) s)) + <=> str (prettyIfConcrete (view (state . returndata) vm)) <=> hBorderWithLabel (txt "Output") - <=> str (maybe "" show (view (uiVm . result) s)) + <=> str (maybe "" show (view result vm)) <=> hBorderWithLabel (txt "Cache") - <=> str (show (view (uiVm . cache . path) s)) + <=> str (show (view (cache . path) vm)) + <=> hBorderWithLabel (txt "Path Conditions") + <=> (str $ show $ snd <$> view constraints vm) <=> hBorderWithLabel (txt "Memory") <=> viewport TracePane Vertical - (str (prettyIfConcrete (view (uiVm . state . memory) s))) + (str (prettyIfConcrete (view (state . memory) vm))) False -> hBorderWithLabel (txt "Trace") <=> renderList (\_ x -> txt x) False - (view uiTraceList s) + (listMoveTo (length traceList) traceList) +solidityList :: VM -> DappInfo -> List Name (Int, ByteString) +solidityList vm dapp' = + list SolidityPane + (case currentSrcMap dapp' vm of + Nothing -> mempty + Just x -> + view (dappSources + . sourceLines + . ix (srcMapFile x) + . to (Vec.imap (,))) + dapp') + 1 + drawSolidityPane :: UiVmState -> UiWidget drawSolidityPane ui = let dapp' = dapp (view uiTestOpts ui) - in case currentSrcMap dapp' (view uiVm ui) of + 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 @@ -976,6 +986,8 @@ Just rows -> let subrange = lineSubrange rows (srcMapOffset sm, srcMapLength sm) + fileName :: Maybe Text + fileName = preview (dappSources . sourceFiles . ix (srcMapFile sm) . _1) dapp' lineNo = (snd . fromJust $ (srcMapCodePos @@ -983,8 +995,7 @@ sm)) - 1 in vBox [ hBorderWithLabel $ - txt (maybe "" contractPathPart - (preview (uiSolc . _Just . contractName) ui)) + txt (fromMaybe "" fileName) <+> str (":" ++ show lineNo) -- Show the AST node type if present @@ -1007,7 +1018,7 @@ ]) False (listMoveTo lineNo - (view uiSolidityList ui)) + (solidityList vm dapp')) ] ifTallEnough :: Int -> Widget n -> Widget n -> Widget n diff --git a/src/EVM/Transaction.hs b/src/EVM/Transaction.hs --- a/src/EVM/Transaction.hs +++ b/src/EVM/Transaction.hs @@ -2,20 +2,26 @@ import Prelude hiding (Word) -import EVM.Concrete +import qualified EVM +import EVM (balance, initialContract) import EVM.FeeSchedule -import EVM.Keccak (keccak) 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.Maybe (isNothing) +import Data.Map (Map) +import Data.Maybe (fromMaybe, isNothing, isJust) import qualified Data.Aeson as JSON import qualified Data.Aeson.Types as JSON import qualified Data.ByteString as BS +import qualified Data.Map as Map data Transaction = Transaction { txData :: ByteString, @@ -65,7 +71,7 @@ rlpWord256 0x0, rlpWord256 0x0] -txGasCost :: FeeSchedule Word -> Transaction -> Word +txGasCost :: FeeSchedule Integer -> Transaction -> Integer txGasCost fs tx = let calldata = txData tx zeroBytes = BS.count 0 calldata @@ -90,3 +96,55 @@ return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value parseJSON invalid = JSON.typeMismatch "Transaction" invalid + +accountAt :: Addr -> Getter (Map Addr EVM.Contract) EVM.Contract +accountAt a = (at a) . (to $ fromMaybe newAccount) + +touchAccount :: Addr -> Map Addr EVM.Contract -> Map Addr EVM.Contract +touchAccount a = Map.insertWith (flip const) a newAccount + +newAccount :: EVM.Contract +newAccount = initialContract $ EVM.RuntimeCode mempty + +-- | Increments origin nonce and pays gas deposit +setupTx :: Addr -> Addr -> Word -> Word -> Map Addr EVM.Contract -> Map Addr EVM.Contract +setupTx origin coinbase gasPrice gasLimit prestate = + let gasCost = gasPrice * gasLimit + in (Map.adjust ((over EVM.nonce (+ 1)) + . (over balance (subtract gasCost))) origin) + . touchAccount origin + . touchAccount coinbase $ prestate + +-- | Given a valid tx loaded into the vm state, +-- subtract gas payment from the origin, increment the nonce +-- and pay receiving address +initTx :: EVM.VM -> EVM.VM +initTx vm = let + toAddr = view (EVM.state . EVM.contract) vm + origin = view (EVM.tx . EVM.origin) vm + gasPrice = view (EVM.tx . EVM.gasprice) vm + gasLimit = view (EVM.tx . EVM.txgaslimit) vm + coinbase = view (EVM.block . EVM.coinbase) vm + value = view (EVM.state . EVM.callvalue) vm + toContract = initialContract (EVM.InitCode (view (EVM.state . EVM.code) vm)) + preState = setupTx origin coinbase gasPrice gasLimit $ view (EVM.env . EVM.contracts) vm + oldBalance = view (accountAt toAddr . balance) preState + creation = view (EVM.tx . EVM.isCreate) vm + initState = + (if isJust (maybeLitWord value) + then (Map.adjust (over balance (subtract (forceLit value))) origin) + . (Map.adjust (over balance (+ (forceLit value))) toAddr) + else id) + . (if creation + then Map.insert toAddr (toContract & balance .~ oldBalance) + else touchAccount toAddr) + $ preState + + touched = if creation + then [origin] + else [origin, toAddr] + + in + vm & EVM.env . EVM.contracts .~ initState + & EVM.tx . EVM.txReversion .~ preState + & EVM.tx . EVM.substate . EVM.touchedAccounts .~ touched diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -7,21 +7,28 @@ module EVM.Types where +import Prelude hiding (Word, LT, GT) + import Data.Aeson (FromJSON (..), (.:)) #if MIN_VERSION_aeson(1, 0, 0) import Data.Aeson (FromJSONKey (..), FromJSONKeyFunction (..)) +import Data.Aeson #endif -import Data.SBV +import Crypto.Hash +import Data.SBV hiding (Word) import Data.Kind import Data.Monoid ((<>)) 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) import Data.ByteString.Lazy (toStrict) +import Control.Monad.State.Strict (liftM) import qualified Data.ByteString.Char8 as Char8 import Data.DoubleWord import Data.DoubleWord.TH @@ -29,13 +36,15 @@ import Data.Word (Word8) import Numeric (readHex, showHex) import Options.Generic +import Control.Arrow ((>>>)) -import qualified Data.Aeson as JSON -import qualified Data.Aeson.Types as JSON -import qualified Data.ByteString as BS -import qualified Data.Serialize.Get as Cereal -import qualified Data.Text as Text -import qualified Data.Text.Encoding as Text +import qualified Data.ByteArray as BA +import qualified Data.Aeson as JSON +import qualified Data.Aeson.Types as JSON +import qualified Data.ByteString as BS +import qualified Data.Serialize.Get as Cereal +import qualified Data.Text as Text +import qualified Data.Text.Encoding as Text import qualified Text.Read -- Some stuff for "generic programming", needed to create Word512 @@ -45,31 +54,239 @@ mkUnpackedDoubleWord "Word512" ''Word256 "Int512" ''Int256 ''Word256 [''Typeable, ''Data, ''Generic] + +data Buffer + = ConcreteBuffer ByteString + | SymbolicBuffer [SWord 8] + newtype W256 = W256 Word256 deriving ( Num, Integral, Real, Ord, Enum, Eq , Bits, FiniteBits, Bounded, Generic ) --- | convert between (WordN 256) and Word256 -type family ToSizzle (t :: Type) :: Type where - ToSizzle W256 = (WordN 256) - ToSizzle Addr = (WordN 160) +data Word = C Whiff W256 --maybe to remove completely in the future --- | Conversion from a fixed-sized BV to a sized bit-vector. -class ToSizzleBV a where - -- | Convert a fixed-sized bit-vector to the corresponding sized bit-vector, - toSizzle :: a -> ToSizzle a +instance Show Word where + show (C _ x) = show x - default toSizzle :: (Num (ToSizzle a), Integral a) => (a -> ToSizzle a) - toSizzle = fromIntegral +instance Read Word where + readsPrec n s = + case readsPrec n s of + [(x, r)] -> [(C (Literal x) x, r)] + _ -> [] +w256 :: W256 -> Word +w256 w = C (Literal w) w + +instance Bits Word where + (C a x) .&. (C b y) = C (And a b) (x .&. y) + (C a x) .|. (C b y) = C (Or a b) (x .|. y) + (C a x) `xor` (C b y) = C (Todo "xor" [a, b]) (x `xor` y) + complement (C a x) = C (Neg a) (complement x) + shiftL (C a x) i = C (SHL a (Literal $ fromIntegral i)) (shiftL x i) + shiftR (C a x) i = C (SHR a (Literal $ fromIntegral i)) (shiftR x i) + rotate (C a x) i = C (Todo "rotate " [a]) (rotate x i) -- unused. + bitSize (C _ x) = bitSize x + bitSizeMaybe (C _ x) = bitSizeMaybe x + isSigned (C _ x) = isSigned x + testBit (C _ x) i = testBit x i + bit i = w256 (bit i) + popCount (C _ x) = popCount x + +instance FiniteBits Word where + finiteBitSize (C _ x) = finiteBitSize x + countLeadingZeros (C _ x) = countLeadingZeros x + countTrailingZeros (C _ x) = countTrailingZeros x + +instance Bounded Word where + minBound = w256 minBound + maxBound = w256 maxBound + +instance Eq Word where + (C _ x) == (C _ y) = x == y + +instance Enum Word where + toEnum i = w256 (toEnum i) + fromEnum (C _ x) = fromEnum x + +instance Integral Word where + quotRem (C _ x) (C _ y) = + let (a, b) = quotRem x y + in (w256 a, w256 b) + toInteger (C _ x) = toInteger x + +instance Num Word where + (C a x) + (C b y) = C (Add a b) (x + y) + (C a x) * (C b y) = C (Mul a b) (x * y) + abs (C a x) = C (Todo "abs" [a]) (abs x) + signum (C a x) = C (Todo "signum" [a]) (signum x) + fromInteger x = C (Literal (fromInteger x)) (fromInteger x) + negate (C a x) = C (Sub (Literal 0) a) (negate x) + +instance Real Word where + toRational (C _ x) = toRational x + +instance Ord Word where + compare (C _ x) (C _ y) = compare x y + +newtype ByteStringS = ByteStringS ByteString deriving (Eq) + +instance Show ByteStringS where + show (ByteStringS x) = ("0x" ++) . Text.unpack . fromBinary $ x + where + 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 + +-- | Symbolic words of 256 bits, possibly annotated with additional +-- "insightful" information +data SymWord = S Whiff (SWord 256) + +instance Show SymWord where + show (S w _) = show w + +var :: String -> SWord 256 -> SymWord +var name x = S (Var name x) x + +-- | Custom instances for SymWord, many of which have direct +-- analogues for concrete words defined in Concrete.hs +instance EqSymbolic SymWord where + (.==) (S _ x) (S _ y) = x .== y + +instance Num SymWord where + (S a x) + (S b y) = S (Add a b) (x + y) + (S a x) * (S b y) = S (Mul a b) (x * y) + abs (S a x) = S (Todo "abs" [a]) (abs x) + signum (S a x) = S (Todo "signum" [a]) (signum x) + fromInteger x = S (Literal (fromInteger x)) (fromInteger x) + negate (S a x) = S (Neg a) (negate x) + +instance Bits SymWord where + (S a x) .&. (S b y) = S (And a b) (x .&. y) + (S a x) .|. (S b y) = S (Or a b) (x .|. y) + (S a x) `xor` (S b y) = S (Todo "xor" [a, b]) (x `xor` y) + complement (S a x) = S (Neg a) (complement x) + shiftL (S a x) i = S (SHL a (Literal $ fromIntegral i)) (shiftL x i) + shiftR (S a x) i = S (SHR a (Literal $ fromIntegral i)) (shiftR x i) + rotate (S a x) i = S (Todo "rotate " [a]) (rotate x i) -- unused. + bitSize (S _ x) = bitSize x + bitSizeMaybe (S _ x) = bitSizeMaybe x + isSigned (S _ x) = isSigned x + testBit (S _ x) i = testBit x i + bit i = w256lit (bit i) + popCount (S _ x) = popCount x + +-- sQuotRem and sDivMod are identical for SWord 256 +-- prove $ \x y -> x `sQuotRem` (y :: SWord 256) .== x `sDivMod` y +-- Q.E.D. +instance SDivisible SymWord where + sQuotRem (S x' x) (S y' y) = let (a, b) = x `sQuotRem` y + in (S (Div x' y') a, S (Mod x' y') b) + sDivMod = sQuotRem + +-- | Instead of supporting a Mergeable instance directly, +-- we use one which carries the Whiff around: +iteWhiff :: Whiff -> SBool -> SWord 256 -> SWord 256 -> SymWord +iteWhiff w b x y = S w (ite b x y) + +instance Bounded SymWord where + minBound = w256lit minBound + maxBound = w256lit maxBound + +instance Eq SymWord where + (S _ x) == (S _ y) = x == y + +instance Enum SymWord where + toEnum i = w256lit (toEnum i) + fromEnum (S _ x) = fromEnum x + +-- | This type can give insight into the provenance of a term +-- which is useful, both for the aesthetic purpose of printing +-- terms in a richer way, but also do optimizations on the AST +-- instead of letting the SMT solver do all the heavy lifting. +data Whiff = + Todo String [Whiff] + -- booleans / bits + | And Whiff Whiff + | Or Whiff Whiff + | Eq Whiff Whiff + | LT Whiff Whiff + | GT Whiff Whiff + | SLT Whiff Whiff + | SGT Whiff Whiff + | IsZero Whiff + | ITE Whiff Whiff Whiff + -- bits + | SHL Whiff Whiff + | SHR Whiff Whiff + | SAR Whiff Whiff + + -- integers + | Add Whiff Whiff + | Sub Whiff Whiff + | Mul Whiff Whiff + | Div Whiff Whiff + | Mod Whiff Whiff + | Exp Whiff Whiff + | Neg Whiff + | FromKeccak Buffer + | FromBytes Buffer + | FromStorage Whiff (SArray (WordN 256) (WordN 256)) + | Literal W256 + | Var String (SWord 256) + +instance Show Whiff where + show w = + let + infix' s x y = show x ++ s ++ show y + in case w of + Todo s args -> s ++ "(" ++ (intercalate "," (show <$> args)) ++ ")" + And x y -> infix' " and " x y + Or x y -> infix' " or " x y + ITE b x y -> "if " ++ show b ++ " then " ++ show x ++ " else " ++ show y + Eq x y -> infix' " == " x y + LT x y -> infix' " < " x y + GT x y -> infix' " > " x y + SLT x y -> infix' " s< " x y + SGT x y -> infix' " s> " x y + IsZero x -> "IsZero(" ++ show x ++ ")" + SHL x y -> infix' " << " x y + SHR x y -> infix' " << " x y + SAR x y -> infix' " a<< " x y + Add x y -> infix' " + " x y + Sub x y -> infix' " - " x y + Mul x y -> infix' " * " x y + Div x y -> infix' " / " x y + Mod x y -> infix' " % " x y + Exp x y -> infix' " ** " x y + Neg x -> "not " ++ show x + Var v _ -> v + FromKeccak buf -> "keccak(" ++ show buf ++ ")" + Literal x -> show x + FromBytes buf -> "FromBuffer " ++ show buf + FromStorage l _ -> "SLOAD(" ++ show l ++ ")" + +newtype Addr = Addr { addressWord160 :: Word160 } + deriving (Num, Integral, Real, Ord, Enum, Eq, Bits, Generic) + +newtype SAddr = SAddr { saddressWord160 :: SWord 160 } + deriving (Num) + -- | Capture the correspondence between sized and fixed-sized BVs +-- (This is blatant copypasta of `FromSized` from sbv, which just +-- happens to be defined up to 64 bits) type family FromSizzle (t :: Type) :: Type where FromSizzle (WordN 256) = W256 FromSizzle (WordN 160) = Addr - -- | Conversion from a sized BV to a fixed-sized bit-vector. class FromSizzleBV a where -- | Convert a sized bit-vector to the corresponding fixed-sized bit-vector, @@ -78,12 +295,32 @@ default fromSizzle :: (Num (FromSizzle a), Integral a) => a -> FromSizzle a fromSizzle = fromIntegral - + + +maybeLitWord :: SymWord -> Maybe Word +maybeLitWord (S whiff a) = fmap (C whiff . fromSizzle) (unliteral a) + +-- | convert between (WordN 256) and Word256 +type family ToSizzle (t :: Type) :: Type where + ToSizzle W256 = (WordN 256) + ToSizzle Addr = (WordN 160) + +-- | Conversion from a fixed-sized BV to a sized bit-vector. +class ToSizzleBV a where + -- | Convert a fixed-sized bit-vector to the corresponding sized bit-vector, + toSizzle :: a -> ToSizzle a + + default toSizzle :: (Num (ToSizzle a), Integral a) => (a -> ToSizzle a) + toSizzle = fromIntegral + + instance (ToSizzleBV W256) instance (FromSizzleBV (WordN 256)) instance (ToSizzleBV Addr) instance (FromSizzleBV (WordN 160)) +w256lit :: W256 -> SymWord +w256lit x = S (Literal x) $ literal $ toSizzle x litBytes :: ByteString -> [SWord 8] litBytes bs = fmap (toSized . literal) (BS.unpack bs) @@ -92,11 +329,11 @@ -- | A buffer is a list of bytes. For concrete execution, this is simply `ByteString`. -- In symbolic settings, it is a list of symbolic bitvectors of size 8. -data Buffer - = ConcreteBuffer ByteString - | SymbolicBuffer [SWord 8] - deriving (Show) +instance Show Buffer where + show (ConcreteBuffer b) = show $ ByteStringS b + show (SymbolicBuffer b) = show (length b) ++ " bytes" + instance Semigroup Buffer where ConcreteBuffer a <> ConcreteBuffer b = ConcreteBuffer (a <> b) ConcreteBuffer a <> SymbolicBuffer b = SymbolicBuffer (litBytes a <> b) @@ -112,12 +349,7 @@ SymbolicBuffer a .== ConcreteBuffer b = a .== litBytes b SymbolicBuffer a .== SymbolicBuffer b = a .== b -newtype Addr = Addr { addressWord160 :: Word160 } - deriving (Num, Integral, Real, Ord, Enum, Eq, Bits, Generic) -newtype SAddr = SAddr { saddressWord160 :: SWord 160 } - deriving (Num) - instance Read W256 where readsPrec _ "0x" = [(0, "")] readsPrec n s = first W256 <$> readsPrec n s @@ -125,36 +357,37 @@ instance Show W256 where showsPrec _ s = ("0x" ++) . showHex s +instance JSON.ToJSON W256 where + toJSON = JSON.String . Text.pack . show + +instance JSON.ToJSON Word where + toJSON (C _ x) = toJSON x + instance Read Addr where readsPrec _ ('0':'x':s) = readHex s readsPrec _ s = readHex s instance Show Addr where - showsPrec _ s a = - let h = showHex s a - in "0x" ++ replicate (40 - length h) '0' ++ h + showsPrec _ addr next = + let hex = showHex addr next + str = replicate (40 - length hex) '0' ++ hex + in "0x" ++ toChecksumAddress str instance Show SAddr where show (SAddr a) = case unliteral a of Nothing -> "" - Just c -> show c + Just c -> show $ fromSizzle c +-- https://eips.ethereum.org/EIPS/eip-55 +toChecksumAddress :: String -> String +toChecksumAddress addr = zipWith transform nibbles addr + where + nibbles = unpackNibbles . BS.take 20 $ keccakBytes (Char8.pack addr) + transform nibble = if nibble >= 8 then toUpper else id + strip0x :: ByteString -> ByteString strip0x bs = if "0x" `Char8.isPrefixOf` bs then Char8.drop 2 bs else bs -newtype ByteStringS = ByteStringS ByteString deriving (Eq) - -instance Show ByteStringS where - show (ByteStringS x) = ("0x" ++) . Text.unpack . fromBinary $ x - where - fromBinary = - Text.decodeUtf8 . toStrict . toLazyByteString . byteStringHex - -instance Read ByteStringS where - readsPrec _ ('0':'x':x) = [(ByteStringS $ fst bytes, Text.unpack . Text.decodeUtf8 $ snd bytes)] - where bytes = BS16.decode (Text.encodeUtf8 (Text.pack x)) - readsPrec _ _ = [] - instance FromJSON W256 where parseJSON v = do s <- Text.unpack <$> parseJSON v @@ -242,11 +475,15 @@ padRight :: Int -> ByteString -> ByteString padRight n xs = xs <> BS.replicate (n - BS.length xs) 0 +-- | Right padding / truncating truncpad :: Int -> [SWord 8] -> [SWord 8] truncpad n xs = if m > n then take n xs else mappend xs (replicate (n - m) 0) where m = length xs +padLeft' :: (Num a) => Int -> [a] -> [a] +padLeft' n xs = replicate (n - length xs) 0 <> xs + word256 :: ByteString -> Word256 word256 xs = case Cereal.runGet m (padLeft 32 xs) of Left _ -> error "internal error" @@ -303,4 +540,33 @@ packNibbles :: [Nibble] -> ByteString packNibbles [] = mempty packNibbles (n1:n2:ns) = BS.singleton (toByte n1 n2) <> packNibbles ns -packNibbles _ = error "cant pack odd number of nibbles" +packNibbles _ = error "can't pack odd number of nibbles" + +-- Keccak hashing + +keccakBytes :: ByteString -> ByteString +keccakBytes = + (hash :: ByteString -> Digest Keccak_256) + >>> BA.unpack + >>> BS.pack + +word32 :: [Word8] -> Word32 +word32 xs = sum [ fromIntegral x `shiftL` (8*n) + | (n, x) <- zip [0..] (reverse xs) ] + +keccak :: ByteString -> W256 +keccak = + keccakBytes + >>> BS.take 32 + >>> word + +abiKeccak :: ByteString -> Word32 +abiKeccak = + keccakBytes + >>> BS.take 4 + >>> BS.unpack + >>> word32 + + +concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] +concatMapM f xs = liftM concat (mapM f xs) diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs --- a/src/EVM/UnitTest.hs +++ b/src/EVM/UnitTest.hs @@ -1,4 +1,6 @@ {-# Language LambdaCase #-} +{-# Language DataKinds #-} +{-# Language ImplicitParams #-} module EVM.UnitTest where @@ -13,8 +15,9 @@ import EVM.Exec import EVM.Format import EVM.Solidity +import EVM.SymExec import EVM.Types -import EVM.VMTest +import EVM.Transaction (initTx) import qualified EVM.Fetch import qualified EVM.FeeSchedule as FeeSchedule @@ -31,14 +34,20 @@ import Control.Monad.Par.IO (runParIO) import qualified Data.ByteString.Lazy as BSLazy +import qualified Data.SBV.Trans.Control as SBV (Query, getValue, resetAssertions) +import qualified Data.SBV.Internals as SBV (State) +import Data.Binary.Get (runGet) import Data.ByteString (ByteString) import Data.SBV hiding (verbose) -import Data.Either (isRight) +import Data.SBV.Control (CheckSatResult(..), checkSat) +import Data.Decimal (DecimalRaw(..)) +import Data.Either (isRight, lefts) import Data.Foldable (toList) import Data.Map (Map) import Data.Maybe (fromMaybe, catMaybes, fromJust, isJust, fromMaybe, mapMaybe) import Data.Monoid ((<>)) import Data.Text (isPrefixOf, stripSuffix, intercalate, Text, pack, unpack) +import Data.Text.Encoding (encodeUtf8) import Data.Word (Word32) import System.Environment (lookupEnv) import System.IO (hFlush, stdout) @@ -62,9 +71,12 @@ import Test.QuickCheck hiding (verbose) data UnitTestOptions = UnitTestOptions - { oracle :: Query -> IO (EVM ()) + { oracle :: EVM.Query -> IO (EVM ()) , verbose :: Maybe Int , maxIter :: Maybe Integer + , smtTimeout :: Maybe Integer + , smtState :: Maybe SBV.State + , solver :: Maybe Text , match :: Text , fuzzRuns :: Int , replay :: Maybe (Text, BSLazy.ByteString) @@ -110,8 +122,8 @@ -- | Assuming a constructor is loaded, this stepper will run the constructor -- to create the test contract, give it an initial balance, and run `setUp()'. -initializeUnitTest :: UnitTestOptions -> Stepper () -initializeUnitTest UnitTestOptions { .. } = do +initializeUnitTest :: UnitTestOptions -> SolcContract -> Stepper () +initializeUnitTest UnitTestOptions { .. } theContract = do let addr = testAddress testParams @@ -124,15 +136,19 @@ -- Constructor is loaded; run until it returns code void Stepper.execFully - -- Give a balance to the test target Stepper.evm $ do + -- Give a balance to the test target env . contracts . ix addr . balance += w256 (testBalanceCreate testParams) - -- Initialize the test contract - setupCall testParams "setUp()" emptyAbi - popTrace - pushTrace (EntryTrace "initialize test") + -- call setUp(), if it exists, to initialize the test contract + let theAbi = view abiMap theContract + setUp = abiKeccak (encodeUtf8 "setUp()") + when (isJust (Map.lookup setUp theAbi)) $ do + abiCall testParams "setUp()" emptyAbi + popTrace + pushTrace (EntryTrace "setUp()") + -- Let `setUp()' run to completion res <- Stepper.execFully Stepper.evm $ case res of @@ -145,13 +161,13 @@ runUnitTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool runUnitTest a method args = do x <- execTest a method args - checkFailures a method args x + checkFailures a method x execTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool execTest UnitTestOptions { .. } method args = do -- Set up the call to the test method Stepper.evm $ do - setupCall testParams method args + abiCall testParams method args pushTrace (EntryTrace method) -- Try running the test method Stepper.execFully >>= \case @@ -159,8 +175,8 @@ Left e -> Stepper.evm (pushTrace (ErrorTrace e)) >> pure True _ -> pure False -checkFailures :: UnitTestOptions -> ABIMethod -> AbiValue -> Bool -> Stepper Bool -checkFailures UnitTestOptions { .. } method args bailed = do +checkFailures :: UnitTestOptions -> ABIMethod -> Bool -> Stepper Bool +checkFailures UnitTestOptions { .. } method bailed = do -- Decide whether the test is supposed to fail or succeed let shouldFail = "testFail" `isPrefixOf` method if bailed then @@ -169,8 +185,8 @@ -- Ask whether any assertions failed Stepper.evm $ do popTrace - setupCall testParams "failed()" args - res <- Stepper.execFully -- >>= \(ConcreteBuffer bs) -> (Stepper.decode AbiBoolType bs) + abiCall testParams "failed()" emptyAbi + res <- Stepper.execFully case res of Right (ConcreteBuffer r) -> let AbiBool failed = decodeAbiValue AbiBoolType (BSLazy.fromStrict r) @@ -181,7 +197,7 @@ fuzzTest :: UnitTestOptions -> Text -> [AbiType] -> VM -> Property fuzzTest opts sig types vm = forAllShow (genAbiValue (AbiTupleType $ Vector.fromList types)) (show . ByteStringS . encodeAbiValue) $ \args -> ioProperty $ - fst <$> runStateT (interpret (oracle opts) (runUnitTest opts sig args)) vm + fst <$> runStateT (EVM.Stepper.interpret (oracle opts) (runUnitTest opts sig args)) vm tick :: Text -> IO () tick x = Text.putStr x >> hFlush stdout @@ -196,12 +212,12 @@ srcMapForOpLocation dapp (OpLocation hash opIx) = case preview (dappSolcByHash . ix hash) dapp of Nothing -> Nothing - Just (codeType, solc) -> + Just (codeType, sol) -> let vec = case codeType of - Runtime -> view runtimeSrcmap solc - Creation -> view creationSrcmap solc + Runtime -> view runtimeSrcmap sol + Creation -> view creationSrcmap sol in preview (ix opIx) vec @@ -314,10 +330,10 @@ :: UnitTestOptions -> Map Text SolcContract -> SourceCache - -> (Text, [(Text, [AbiType])]) + -> (Text, [(Test, [AbiType])]) -> IO (MultiSet SrcMap) coverageForUnitTestContract - opts@(UnitTestOptions {..}) contractMap sources (name, testNames) = do + opts@(UnitTestOptions {..}) contractMap _ (name, testNames) = do -- Look for the wanted contract by name from the Solidity info case preview (ix name) contractMap of @@ -331,20 +347,20 @@ (vm1, cov1) <- execStateT (interpretWithCoverage opts - (Stepper.enter name >> initializeUnitTest opts)) + (Stepper.enter name >> initializeUnitTest opts theContract)) (vm0, mempty) -- Define the thread spawner for test cases let - runOne (testName, _) = spawn_ . liftIO $ do - (x, (_, cov)) <- + runOne' (test, _) = spawn_ . liftIO $ do + (_, (_, cov)) <- runStateT - (interpretWithCoverage opts (runUnitTest opts testName emptyAbi)) + (interpretWithCoverage opts (runUnitTest opts (extractSig test) emptyAbi)) (vm1, mempty) pure cov -- Run all the test cases in parallel and gather their coverages covs <- - runParIO (mapM runOne testNames >>= mapM Par.get) + runParIO (mapM runOne' testNames >>= mapM Par.get) -- Sum up all the coverage counts let cov2 = MultiSet.unions (cov1 : covs) @@ -354,14 +370,13 @@ runUnitTestContract :: UnitTestOptions -> Map Text SolcContract - -> SourceCache - -> (Text, [(Text, [AbiType])]) - -> IO [(Bool, VM)] + -> (Text, [(Test, [AbiType])]) + -> SBV.Query [(Bool, VM)] runUnitTestContract - opts@(UnitTestOptions {..}) contractMap sources (name, testSigs) = do + opts@(UnitTestOptions {..}) contractMap (name, testSigs) = do -- Print a header - putStrLn $ "Running " ++ show (length testSigs) ++ " tests for " + liftIO $ putStrLn $ "Running " ++ show (length testSigs) ++ " tests for " ++ unpack name -- Look for the wanted contract by name from the Solidity info @@ -374,25 +389,25 @@ -- Construct the initial VM and begin the contract's constructor let vm0 = initialUnitTestVm opts theContract vm1 <- - execStateT - (interpret oracle - (Stepper.enter name >> initializeUnitTest opts)) + liftIO $ execStateT + (EVM.Stepper.interpret oracle + (Stepper.enter name >> initializeUnitTest opts theContract)) vm0 case view result vm1 of Nothing -> error "internal error: setUp() did not end with a result" - Just (VMFailure _) -> do - Text.putStrLn "\x1b[31m[FAIL]\x1b[0m setUp()" + Just (VMFailure _) -> liftIO $ do + Text.putStrLn "\x1b[31m[BAIL]\x1b[0m setUp() " tick "\n" tick $ failOutput vm1 opts "setUp()" pure [(False, vm1)] Just (VMSuccess _) -> do let - runCache :: ([(Either Text Text, VM)], VM) -> (Text, [AbiType]) - -> IO ([(Either Text Text, VM)], VM) - runCache (results, vm) (testName, types) = do - (t, r, vm') <- runTest opts vm (testName, types) - Text.putStrLn t + runCache :: ([(Either Text Text, VM)], VM) -> (Test, [AbiType]) + -> SBV.Query ([(Either Text Text, VM)], VM) + runCache (results, vm) (test, types) = do + (t, r, vm') <- runTest opts vm (test, types) + liftIO $ Text.putStrLn t let vmCached = vm & set (cache . fetched) (view (cache . fetched) vm') pure (((r, vm'): results), vmCached) @@ -403,17 +418,17 @@ let running = [x | (Right x, _) <- details] let bailing = [x | (Left x, _) <- details] - tick "\n" - tick (Text.unlines (filter (not . Text.null) running)) - tick (Text.unlines (filter (not . Text.null) bailing)) + liftIO $ do + tick "\n" + tick (Text.unlines (filter (not . Text.null) running)) + tick (Text.unlines (filter (not . Text.null) bailing)) pure [(isRight r, vm) | (r, vm) <- details] - -runTest :: UnitTestOptions -> VM -> (Text, [AbiType]) -> IO (Text, Either Text Text, VM) -runTest opts@UnitTestOptions{..} vm (testName, []) = runOne opts vm testName emptyAbi -runTest opts@UnitTestOptions{..} vm (testName, types) = case replay of +runTest :: UnitTestOptions -> VM -> (Test, [AbiType]) -> SBV.Query (Text, Either Text Text, VM) +runTest opts@UnitTestOptions{..} vm (ConcreteTest testName, []) = liftIO $ runOne opts vm testName emptyAbi +runTest opts@UnitTestOptions{..} vm (ConcreteTest testName, types) = liftIO $ case replay of Nothing -> fuzzRun opts vm testName types Just (sig, callData) -> @@ -421,18 +436,19 @@ then runOne opts vm testName $ decodeAbiValue (AbiTupleType (Vector.fromList types)) callData else fuzzRun opts vm testName types +runTest opts vm (SymbolicTest testName, types) = symRun opts vm testName types --- | Define the thread spawner for normal test cases +-- | 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 - (interpret oracle (execTest opts testName args)) + (EVM.Stepper.interpret oracle (execTest opts testName args)) vm (success, vm'') <- runStateT - (interpret oracle (checkFailures opts testName args bailed)) vm' + (EVM.Stepper.interpret oracle (checkFailures opts testName bailed)) vm' if success then let gasSpent = num (testGasCall testParams) - view (state . gas) vm' @@ -444,8 +460,15 @@ , Right (passOutput vm'' opts testName) , vm'' ) - else + else if bailed then pure + ("\x1b[31m[BAIL]\x1b[0m " + <> testName <> argInfo + , Left (failOutput vm'' opts testName) + , vm'' + ) + else + pure ("\x1b[31m[FAIL]\x1b[0m " <> testName <> argInfo , Left (failOutput vm'' opts testName) @@ -476,7 +499,7 @@ ppOutput = pack $ show abiValue in do -- Run the failing test again to get a proper trace - vm' <- execStateT (interpret oracle (runUnitTest opts testName abiValue)) vm + vm' <- execStateT (EVM.Stepper.interpret oracle (runUnitTest opts testName abiValue)) vm pure ("\x1b[31m[FAIL]\x1b[0m " <> testName <> ". Counterexample: " <> ppOutput <> "\nRun:\n dapp test --replay '(\"" <> testName <> "\",\"" @@ -491,8 +514,124 @@ , vm ) +-- | Define the thread spawner for symbolic tests +-- TODO: return a list of VM's +symRun :: UnitTestOptions -> VM -> Text -> [AbiType] -> SBV.Query (Text, Either Text Text, VM) +symRun opts@UnitTestOptions{..} concreteVm testName types = do + SBV.resetAssertions + let vm = symbolify concreteVm + (cd, cdlen) <- symCalldata testName types [] + let cd' = (SymbolicBuffer cd, w256lit cdlen) + shouldFail = "proveFail" `isPrefixOf` testName + -- get all posible postVMs for the test method + allPaths <- fst <$> runStateT + (EVM.SymExec.interpret oracle maxIter (execSymTest opts testName cd')) vm + let consistentPaths = flip filter allPaths $ + \(_, vm') -> case view result vm' of + Just (VMFailure DeadPath) -> False + _ -> True + results <- forM consistentPaths $ + -- If the vm execution succeeded, check if the vm is reachable, + -- and if any ds-test assertions were triggered + -- Report a failure depending on the prefix of the test name + -- If the vm execution failed, check if the vm is reachable, and if so, + -- report a failure unless the test is supposed to fail. + + \(bailed, vm') -> do + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + SBV.resetAssertions + constrain $ sAnd (fst <$> view EVM.constraints vm') + unless bailed $ + case view result vm' of + Just (VMSuccess (SymbolicBuffer buf)) -> + constrain $ litBytes (encodeAbiValue $ AbiBool $ not shouldFail) .== buf + r -> error $ "unexpected return value: " ++ show r + checkSat >>= \case + Sat -> do + prettyCd <- prettyCalldata cd' testName types + let explorationFailed = case view result vm' of + Just (VMFailure e) -> case e of + NotUnique _ -> True + UnexpectedSymbolicArg -> True + _ -> False + _ -> False + return $ + if shouldFail && bailed && not explorationFailed + then Right () + else Left (vm', prettyCd) + Unsat -> return $ Right () + Unk -> return $ Left (vm', "unknown; query timeout") + DSat _ -> error "Unexpected DSat" + + if null $ lefts results + then + return ("\x1b[32m[PASS]\x1b[0m " <> testName, Right "", vm) + else + return ("\x1b[31m[FAIL]\x1b[0m " <> testName, Left $ symFailure opts testName (lefts results), vm) + +symFailure :: UnitTestOptions -> Text -> [(VM, Text)] -> Text +symFailure UnitTestOptions {..} testName failures' = mconcat + [ "Failure: " + , testName + , "\n\n" + , intercalate "\n" $ indentLines 2 . mkMsg <$> failures' + ] + where + showRes vm = let Just res = view result vm in + case res of + VMFailure _ -> + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + in prettyvmresult res + VMSuccess _ -> if "proveFail" `isPrefixOf` testName + then "Successful execution" + else "Failed: DSTest Assertion Violation" + mkMsg (vm, cd) = pack $ unlines + ["Counterexample:" + ,"" + ," result: " <> showRes vm + ," calldata: " <> unpack cd + , case verbose of + Just _ -> unlines + [ "" + , unpack $ indentLines 2 (showTraceTree dapp vm) + ] + _ -> "" + ] + +prettyCalldata :: (?context :: DappContext) => (Buffer, SymWord) -> Text -> [AbiType]-> SBV.Query Text +prettyCalldata (buffer, S _ cdlen) sig types = do + cdlen' <- num <$> SBV.getValue cdlen + cd <- case buffer of + SymbolicBuffer cd -> mapM (SBV.getValue . fromSized) (take cdlen' cd) <&> BS.pack + ConcreteBuffer cd -> return $ BS.take cdlen' cd + pure $ (head (Text.splitOn "(" sig)) <> showCall types (ConcreteBuffer cd) + +execSymTest :: UnitTestOptions -> ABIMethod -> (Buffer, SymWord) -> Stepper (Bool, VM) +execSymTest opts@UnitTestOptions{ .. } method cd = do + -- Set up the call to the test method + Stepper.evm $ do + makeTxCall testParams cd + pushTrace (EntryTrace method) + -- Try running the test method + Stepper.runFully >>= \vm' -> case view result vm' of + Just (VMFailure err) -> + -- If we failed, put the error in the trace. + Stepper.evm (pushTrace (ErrorTrace err)) >> (pure (True, vm')) + Just (VMSuccess _) -> do + postVm <- checkSymFailures opts + pure (False, postVm) + Nothing -> error "Internal Error: execSymTest: vm has not completed execution!" + +checkSymFailures :: UnitTestOptions -> Stepper VM +checkSymFailures UnitTestOptions { .. } = do + -- Ask whether any assertions failed + Stepper.evm $ do + popTrace + abiCall testParams "failed()" emptyAbi + Stepper.runFully + indentLines :: Int -> Text -> Text indentLines n s = let p = Text.replicate n " " @@ -500,92 +639,122 @@ passOutput :: VM -> UnitTestOptions -> Text -> Text passOutput vm UnitTestOptions { .. } testName = - case verbose of - Just 2 -> - mconcat - [ "Success: " - , fromMaybe "" (stripSuffix "()" testName) - , "\n" - , indentLines 2 (formatTestLogs (view dappEventMap dapp) (view logs vm)) - , indentLines 2 (showTraceTree dapp vm) - , "\n" - ] - _ -> - "" + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + in let v = fromMaybe 0 verbose + in if (v > 1) then + mconcat + [ "Success: " + , fromMaybe "" (stripSuffix "()" testName) + , "\n" + , if (v > 2) then indentLines 2 (showTraceTree dapp vm) else "" + , indentLines 2 (formatTestLogs (view dappEventMap dapp) (view logs vm)) + , "\n" + ] + else "" failOutput :: VM -> UnitTestOptions -> Text -> Text -failOutput vm UnitTestOptions { .. } testName = mconcat +failOutput vm UnitTestOptions { .. } testName = + let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env } + in mconcat [ "Failure: " , fromMaybe "" (stripSuffix "()" testName) , "\n" - , indentLines 2 (formatTestLogs (view dappEventMap dapp) (view logs vm)) , case verbose of Just _ -> indentLines 2 (showTraceTree dapp vm) _ -> "" - + , indentLines 2 (formatTestLogs (view dappEventMap dapp) (view logs vm)) + , "\n" ] -formatTestLogs :: Map W256 Event -> Seq.Seq Log -> Text +formatTestLogs :: (?context :: DappContext) => Map W256 Event -> Seq.Seq Log -> Text formatTestLogs events xs = case catMaybes (toList (fmap (formatTestLog events) xs)) of [] -> "\n" ys -> "\n" <> intercalate "\n" ys <> "\n\n" -formatTestLog :: Map W256 Event -> Log -> Maybe Text +-- Here we catch and render some special logs emitted by ds-test, +-- with the intent to then present them in a separate view to the +-- regular trace output. +formatTestLog :: (?context :: DappContext) => Map W256 Event -> Log -> Maybe Text formatTestLog _ (Log _ _ []) = Nothing formatTestLog events (Log _ args (topic:_)) = - case maybeLitWord topic of + case maybeLitWord topic >>= \t1 -> (Map.lookup (wordValue t1) events) of Nothing -> Nothing - Just t -> case (Map.lookup (wordValue t) events) of - Nothing -> Nothing - Just (Event name _ _) -> case name of - "log_bytes32" -> - Just $ formatSBytes args + Just (Event name _ types) -> + case (name <> parenthesise (abiTypeSolidity <$> (unindexed types))) of + "log(string)" -> Just $ unquote $ showValue AbiStringType args - "log_named_bytes32" -> - let key = grab 32 args - val = ditch 32 args - in Just $ formatSString key <> ": " <> formatSBytes val + -- log_named_x(string, x) + "log_named_bytes32(string, bytes32)" -> log_named + "log_named_address(string, address)" -> log_named + "log_named_int(string, int256)" -> log_named + "log_named_uint(string, uint256)" -> log_named + "log_named_bytes(string, bytes)" -> log_named + "log_named_string(string, string)" -> log_named - "log_named_address" -> - let key = grab 32 args - val = ditch 44 args - in Just $ formatSString key <> ": " <> formatSBinary val + -- log_named_decimal_x(string, uint, x) + "log_named_decimal_int(string, int256, uint256)" -> log_named_decimal + "log_named_decimal_uint(string, uint256, uint256)" -> log_named_decimal - "log_named_int" -> - let key = grab 32 args - val = case maybeLitWord (readMemoryWord 32 args) of - Just c -> showDec Signed (wordValue c) - Nothing -> "" - in Just $ formatSString key <> ": " <> val + -- log_x(x) + "log_bytes32(bytes32)" -> log_unnamed + "log_address(address)" -> log_unnamed + "log_int(int256)" -> log_unnamed + "log_uint(uint256)" -> log_unnamed + "log_bytes(bytes)" -> log_unnamed + "log_string(string)" -> log_unnamed - "log_named_uint" -> - let key = grab 32 args - val = case maybeLitWord (readMemoryWord 32 args) of - Just c -> showDec Unsigned (wordValue c) - Nothing -> "" - in Just $ formatSString key <> ": " <> val + -- log_named_x(bytes32, x), as used in older versions of ds-test. + -- bytes32 are opportunistically represented as strings in Format.hs + "log_named_bytes32(bytes32, bytes32)" -> log_named + "log_named_address(bytes32, address)" -> log_named + "log_named_int(bytes32, int256)" -> log_named + "log_named_uint(bytes32, uint256)" -> log_named --- TODO: event logs (bytes); --- TODO: event log_named_decimal_int (bytes32 key, int val, uint decimals); --- TODO: event log_named_decimal_uint (bytes32 key, uint val, uint decimals); + _ -> Nothing - _ -> Nothing + where + ts = unindexed types + unquote = Text.dropAround (\c -> c == '"' || c == '«' || c == '»') + log_unnamed = + Just $ showValue (head ts) args + log_named = + let [key, val] = take 2 (textValues ts args) + in Just $ unquote key <> ": " <> val + showDecimal dec val = + pack $ show $ Decimal (num dec) val + log_named_decimal = + case args of + (ConcreteBuffer b) -> + case toList $ runGet (getAbiSeq (length ts) ts) (BSLazy.fromStrict b) of + [key, (AbiUInt 256 val), (AbiUInt 256 dec)] -> + Just $ (unquote (showAbiValue key)) <> ": " <> showDecimal dec val + [key, (AbiInt 256 val), (AbiUInt 256 dec)] -> + Just $ (unquote (showAbiValue key)) <> ": " <> showDecimal dec val + _ -> Nothing + (SymbolicBuffer _) -> Just "" + word32Bytes :: Word32 -> ByteString word32Bytes x = BS.pack [byteAt x (3 - i) | i <- [0..3]] -setupCall :: TestVMParams -> Text -> AbiValue -> EVM () -setupCall TestVMParams{..} sig args = do +abiCall :: TestVMParams -> Text -> AbiValue -> EVM () +abiCall params sig args = + let cd = abiMethod sig args + l = num . BS.length $ cd + in makeTxCall params (ConcreteBuffer cd, litWord l) + +makeTxCall :: TestVMParams -> (Buffer, SymWord) -> EVM () +makeTxCall TestVMParams{..} cd = do resetState assign (tx . isCreate) False loadContract testAddress - assign (state . calldata) (ConcreteBuffer $ abiMethod sig args, literal . num . BS.length $ abiMethod sig args) + assign (state . calldata) cd assign (state . caller) (litAddr testCaller) assign (state . gas) (w256 testGasCall) origin' <- fromMaybe (initialContract (RuntimeCode mempty)) <$> use (env . contracts . at testOrigin) let originBal = view balance origin' - when (originBal <= (w256 testGasprice) * (w256 testGasCall)) $ error "insufficient balance for gas cost" + when (originBal < (w256 testGasprice) * (w256 testGasCall)) $ error "insufficient balance for gas cost" vm <- get put $ initTx vm @@ -604,7 +773,7 @@ , vmoptGaslimit = testGasCreate , vmoptCoinbase = testCoinbase , vmoptNumber = testNumber - , vmoptTimestamp = litWord $ w256 $ testTimestamp + , vmoptTimestamp = litWord $ w256 testTimestamp , vmoptBlockGaslimit = testGaslimit , vmoptGasprice = testGasprice , vmoptMaxCodeSize = testMaxCodeSize @@ -612,7 +781,7 @@ , vmoptSchedule = FeeSchedule.istanbul , vmoptChainId = testChainId , vmoptCreate = True - , vmoptStorageModel = ConcreteS + , vmoptStorageModel = ConcreteS -- TODO: support RPC } creator = initialContract (RuntimeCode mempty) @@ -622,22 +791,31 @@ & set (env . contracts . at ethrunAddress) (Just creator) -maybeM :: (Monad m) => b -> (a -> b) -> m (Maybe a) -> m b -maybeM def f mayb = do - may <- mayb - return $ maybe def f may +-- | takes a concrete VM and makes all storage symbolic +symbolify :: VM -> VM +symbolify vm = + vm & over (env . contracts . each . storage) mkSymStorage + & set (env . storageModel) InitialS + where + mkSymStorage :: Storage -> Storage + mkSymStorage (Symbolic _ _) = error "should not happen" + mkSymStorage (Concrete s) = + let + list = [(literal $ toSizzle k, v) | (C _ k, S _ v) <- Map.toList s] + symlist = [(litWord k, v) | (k, v) <- Map.toList s] + in Symbolic symlist $ sListArray 0 list getParametersFromEnvironmentVariables :: Maybe Text -> IO TestVMParams getParametersFromEnvironmentVariables rpc = do - block' <- maybeM EVM.Fetch.Latest (EVM.Fetch.BlockNumber . read) (lookupEnv "DAPP_TEST_NUMBER") + block' <- maybe EVM.Fetch.Latest (EVM.Fetch.BlockNumber . read) <$> (lookupEnv "DAPP_TEST_NUMBER") (miner,ts,blockNum,diff) <- case rpc of Nothing -> return (0,0,0,0) Just url -> EVM.Fetch.fetchBlockFrom block' url >>= \case - Nothing -> error $ "Could not fetch block" + Nothing -> error "Could not fetch block" Just EVM.Block{..} -> return ( _coinbase - , wordValue $ forceLit $ _timestamp + , wordValue $ forceLit _timestamp , wordValue _number , wordValue _difficulty ) diff --git a/src/EVM/VMTest.hs b/src/EVM/VMTest.hs --- a/src/EVM/VMTest.hs +++ b/src/EVM/VMTest.hs @@ -12,6 +12,8 @@ , checkExpectation ) where +import Prelude hiding (Word) + import qualified EVM import EVM (contractcode, storage, origStorage, balance, nonce, Storage(..), initialContract) import qualified EVM.Concrete as EVM @@ -21,8 +23,6 @@ import EVM.Transaction import EVM.Types -import Data.SBV - import Control.Arrow ((***), (&&&)) import Control.Lens import Control.Monad @@ -30,7 +30,7 @@ import Data.Aeson ((.:), FromJSON (..)) import Data.Foldable (fold) import Data.Map (Map) -import Data.Maybe (fromMaybe, isNothing, isJust) +import Data.Maybe (fromMaybe, isNothing) import Data.Witherable (Filterable, catMaybes) import qualified Data.Map as Map @@ -63,15 +63,6 @@ , blockchainNetwork :: String } deriving Show -accountAt :: Addr -> Getter (Map Addr EVM.Contract) EVM.Contract -accountAt a = (at a) . (to $ fromMaybe newAccount) - -touchAccount :: Addr -> Map Addr EVM.Contract -> Map Addr EVM.Contract -touchAccount a = Map.insertWith (flip const) a newAccount - -newAccount :: EVM.Contract -newAccount = initialContract $ EVM.RuntimeCode mempty - splitEithers :: (Filterable f) => f (Either a b) -> (f a, f b) splitEithers = (catMaybes *** catMaybes) @@ -99,7 +90,7 @@ check = checkContracts x expected = testExpectation x actual = view (EVM.env . EVM.contracts . to (fmap (clearZeroStorage.clearOrigStorage))) vm - printStorage (EVM.Symbolic c) = show c + printStorage (EVM.Symbolic _ c) = show c printStorage (EVM.Concrete c) = show $ Map.toList c putStr (unwords reason) @@ -145,7 +136,7 @@ clearZeroStorage :: EVM.Contract -> EVM.Contract clearZeroStorage c = case view storage c of - EVM.Symbolic _ -> c + EVM.Symbolic _ _ -> c EVM.Concrete m -> let store = Map.filter (\x -> forceLit x /= 0) m in set EVM.storage (EVM.Concrete store) c @@ -166,16 +157,16 @@ instance FromJSON EVM.Contract where parseJSON (JSON.Object v) = do code <- (EVM.RuntimeCode <$> (hexText <$> v .: "code")) - storage' <- Map.mapKeys EVM.w256 <$> v .: "storage" + storage' <- Map.mapKeys w256 <$> v .: "storage" balance' <- v .: "balance" nonce' <- v .: "nonce" return $ EVM.initialContract code - & balance .~ EVM.w256 balance' - & nonce .~ EVM.w256 nonce' - & storage .~ EVM.Concrete (fmap (litWord . EVM.w256) storage') - & origStorage .~ fmap EVM.w256 storage' + & balance .~ w256 balance' + & nonce .~ w256 nonce' + & storage .~ EVM.Concrete (fmap (litWord . w256) storage') + & origStorage .~ fmap w256 storage' parseJSON invalid = JSON.typeMismatch "Contract" invalid @@ -251,28 +242,28 @@ [] -> Left NoTxs _ -> Left TooManyTxs ([_], _) -> Left OldNetwork - (_, _) -> Left TooManyBlocks + (_, _) -> Left TooManyBlocks fromBlockchainCase' :: Block -> Transaction -> Map Addr EVM.Contract -> Map Addr EVM.Contract -> Either BlockchainError Case fromBlockchainCase' block tx preState postState = let isCreate = isNothing (txToAddr tx) - in case (sender 1 tx, checkTx tx block preState) of + in case (sender 1 tx, checkTx tx preState) of (Nothing, _) -> Left SignatureUnverified (_, Nothing) -> Left (if isCreate then FailedCreate else InvalidTx) (Just origin, Just checkState) -> Right $ Case (EVM.VMOpts { vmoptContract = EVM.initialContract theCode , vmoptCalldata = cd - , vmoptValue = litWord (EVM.w256 $ txValue tx) + , vmoptValue = litWord (w256 $ txValue tx) , vmoptAddress = toAddr , vmoptCaller = litAddr origin , vmoptOrigin = origin , vmoptGas = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx) , vmoptGaslimit = txGasLimit tx , vmoptNumber = blockNumber block - , vmoptTimestamp = litWord $ EVM.w256 $ blockTimestamp block + , vmoptTimestamp = litWord $ w256 $ blockTimestamp block , vmoptCoinbase = blockCoinbase block , vmoptDifficulty = blockDifficulty block , vmoptMaxCodeSize = 24576 @@ -295,7 +286,8 @@ else maybe (EVM.RuntimeCode mempty) (view contractcode) toCode cd = if isCreate then (mempty, 0) - else (ConcreteBuffer $ txData tx, literal . num . BS.length $ txData tx) + else let l = num . BS.length $ txData tx + in (ConcreteBuffer $ txData tx, litWord l) validateTx :: Transaction -> Map Addr EVM.Contract -> Maybe () @@ -303,14 +295,14 @@ origin <- sender 1 tx originBalance <- (view balance) <$> view (at origin) cs originNonce <- (view nonce) <$> view (at origin) cs - let gasDeposit = EVM.w256 $ (txGasPrice tx) * (txGasLimit tx) - if gasDeposit + (EVM.w256 $ txValue tx) <= originBalance - && (EVM.w256 $ txNonce tx) == originNonce + let gasDeposit = w256 $ (txGasPrice tx) * (txGasLimit tx) + if gasDeposit + (w256 $ txValue tx) <= originBalance + && (w256 $ txNonce tx) == originNonce then Just () else Nothing -checkTx :: Transaction -> Block -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract) -checkTx tx block prestate = do +checkTx :: Transaction -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract) +checkTx tx prestate = do origin <- sender 1 tx validateTx tx prestate let isCreate = isNothing (txToAddr tx) @@ -330,46 +322,3 @@ & set (EVM.env . EVM.contracts) (checkContracts x) in initTx vm - --- | Increments origin nonce and pays gas deposit -setupTx :: Addr -> Addr -> EVM.Word -> EVM.Word -> Map Addr EVM.Contract -> Map Addr EVM.Contract -setupTx origin coinbase gasPrice gasLimit prestate = - let gasCost = gasPrice * gasLimit - in (Map.adjust ((over nonce (+ 1)) - . (over balance (subtract gasCost))) origin) - . touchAccount origin - . touchAccount coinbase $ prestate - --- | Given a valid tx loaded into the vm state, --- subtract gas payment from the origin, increment the nonce --- and pay receiving address -initTx :: EVM.VM -> EVM.VM -initTx vm = let - toAddr = view (EVM.state . EVM.contract) vm - origin = view (EVM.tx . EVM.origin) vm - gasPrice = view (EVM.tx . EVM.gasprice) vm - gasLimit = view (EVM.tx . EVM.txgaslimit) vm - coinbase = view (EVM.block . EVM.coinbase) vm - value = view (EVM.state . EVM.callvalue) vm - toContract = initialContract (EVM.InitCode (view (EVM.state . EVM.code) vm)) - preState = setupTx origin coinbase gasPrice gasLimit $ view (EVM.env . EVM.contracts) vm - oldBalance = view (accountAt toAddr . balance) preState - creation = view (EVM.tx . EVM.isCreate) vm - initState = - (if isJust (maybeLitWord value) - then (Map.adjust (over balance (subtract (forceLit value))) origin) - . (Map.adjust (over balance (+ (forceLit value))) toAddr) - else id) - . (if creation - then Map.insert toAddr (toContract & balance .~ oldBalance) - else touchAccount toAddr) - $ preState - - touched = if creation - then [origin] - else [origin, toAddr] - - in - vm & EVM.env . EVM.contracts .~ initState - & EVM.tx . EVM.txReversion .~ preState - & EVM.tx . EVM.substate . EVM.touchedAccounts .~ touched diff --git a/test/test.hs b/test/test.hs --- a/test/test.hs +++ b/test/test.hs @@ -1,4 +1,5 @@ {-# Language OverloadedStrings #-} +{-# Language ScopedTypeVariables #-} {-# Language LambdaCase #-} {-# Language QuasiQuotes #-} {-# Language TypeSynonymInstances #-} @@ -20,13 +21,14 @@ import Test.Tasty.HUnit import Control.Monad.State.Strict (execState, runState, when) -import Control.Lens hiding (List, pre) +import Control.Lens hiding (List, pre, (.<), (.>)) import qualified Data.Vector as Vector import Data.String.Here import Control.Monad.Fail import Debug.Trace +import Data.SBV.Tools.Overflow import Data.Binary.Put (runPut) import Data.SBV hiding ((===), forAll, sList) @@ -40,10 +42,9 @@ import EVM hiding (Query) import EVM.SymExec import EVM.Symbolic -import EVM.Concrete (w256) import EVM.ABI import EVM.Exec -import EVM.Patricia as Patricia +import qualified EVM.Patricia as Patricia import EVM.Precompiled import EVM.RLP import EVM.Solidity @@ -170,7 +171,7 @@ -- withMaxSuccess 100000 $ Patricia.insertValues [(r, BS.pack[1]), (s, BS.pack[2]), (t, BS.pack[3]), (r, mempty), (s, mempty), (t, mempty)] - === (Just $ Literal Patricia.Empty) + === (Just $ Patricia.Literal Patricia.Empty) ] , testGroup "Symbolic execution" @@ -194,7 +195,7 @@ in case view result poststate of Just (VMSuccess (SymbolicBuffer out)) -> (fromBytes out) .== x + y _ -> sFalse - Left (_, res) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post + (Left res, _) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post putStrLn $ "successfully explored: " <> show (length res) <> " paths" , @@ -216,7 +217,7 @@ in case view result poststate of Just (VMSuccess (SymbolicBuffer out)) -> fromBytes out .== 2 * y _ -> sFalse - Left (_, res) <- runSMTWith z3 $ query $ + (Left res, _) <- runSMTWith z3 $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post) putStrLn $ "successfully explored: " <> show (length res) <> " paths" , @@ -231,7 +232,7 @@ } |] bs <- runSMTWith cvc4 $ query $ do - Right vm <- checkAssert factor (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] + (Right _, vm) <- checkAssert 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" @@ -257,14 +258,14 @@ this = view (state . codeContract) prestate Just preC = view (env.contracts . at this) prestate Just postC = view (env.contracts . at this) poststate - Symbolic prestore = _storage preC - Symbolic poststore = _storage postC + Symbolic _ prestore = _storage preC + Symbolic _ poststore = _storage postC prex = readArray prestore 0 postx = readArray poststore 0 in case view result poststate of Just (VMSuccess _) -> prex + 2 * y .== postx _ -> sFalse - Left (_, res) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post + (Left res, _) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post putStrLn $ "successfully explored: " <> show (length res) <> " paths" , -- Inspired by these `msg.sender == to` token bugs @@ -289,14 +290,14 @@ this = view (state . codeContract) prestate (Just preC, Just postC) = both' (view (env.contracts . at this)) (prestate, poststate) --Just postC = view (env.contracts . at this) poststate - (Symbolic prestore, Symbolic poststore) = both' (view storage) (preC, postC) + (Symbolic _ prestore, Symbolic _ poststore) = both' (view storage) (preC, postC) (prex, prey) = both' (readArray prestore) (x, y) (postx, posty) = both' (readArray poststore) (x, y) in case view result poststate of Just (VMSuccess _) -> prex + prey .== postx + (posty :: SWord 256) _ -> sFalse bs <- runSMT $ query $ do - Right vm <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post) + (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" @@ -323,7 +324,7 @@ } } |] - Left (_, res) <- runSMTWith z3 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) [] + (Left res, _) <- runSMTWith z3 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "Deposit contract loop (cvc4)" $ do @@ -345,7 +346,7 @@ } } |] - Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) [] + (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "Deposit contract loop (error version)" $ do @@ -368,7 +369,7 @@ } |] bs <- runSMT $ query $ do - Right vm <- checkAssert c (Just ("deposit(uint8)", [AbiUIntType 8])) [] + (Right _, vm) <- checkAssert c (Just ("deposit(uint8)", [AbiUIntType 8])) [] case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected" @@ -385,7 +386,7 @@ } } |] - Left (_, res) <- runSMTWith z3 $ do + (Left res, _) <- runSMTWith z3 $ do setTimeOut 5000 query $ checkAssert c Nothing [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" @@ -400,7 +401,7 @@ } } |] - Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] + (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "injectivity of keccak (32 bytes)" $ do @@ -412,7 +413,7 @@ } } |] - Left (_, res) <- runSMTWith z3 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] + (Left res, _) <- runSMTWith z3 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , @@ -426,11 +427,11 @@ } |] bs <- runSMTWith z3 $ query $ do - Right vm <- checkAssert c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) [] + (Right _, vm) <- checkAssert 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" - + let [AbiUInt 256 x, AbiUInt 256 y, AbiUInt 256 w, @@ -456,9 +457,9 @@ } } |] - Left (_, res) <- runSMTWith z3 $ do + Left res <- runSMTWith z3 $ do setTimeOut 5000 - query $ checkAssert c Nothing [] + query $ fst <$> checkAssert c Nothing [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , @@ -475,7 +476,7 @@ } |] -- should find a counterexample - Right counterexample <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] + Right _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn $ "found counterexample:" @@ -486,7 +487,7 @@ contract C { uint x; A constant a = A(0x35D1b3F3D7966A1DFe207aa4514C12a259A0492B); - + function call_A() public view { // should fail since a.x() can be anything assert(a.x() == x); @@ -506,10 +507,83 @@ & set (state . callvalue) 0 & over (env . contracts) (Map.insert aAddr (initialContract (RuntimeCode a) & - set EVM.storage (Symbolic store))) + set EVM.storage (EVM.Symbolic [] store))) verify vm Nothing Nothing (Just checkAssertions) putStrLn $ "found counterexample:" + , + testCase "calling unique contracts (read from storage)" $ do + let code = + [i| + contract C { + uint x; + A a; + function call_A() public { + a = new A(); + // should fail since x can be anything + assert(a.x() == x); + } + } + contract A { + uint public x; + } + |] + Just c <- solcRuntime "C" code + Right cex <- 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:" + , + + testCase "keccak concrete and sym agree" $ do + let code = + [i| + contract C { + function kecc(uint x) public pure { + if (x == 0) { + assert(keccak256(abi.encode(x)) == keccak256(abi.encode(0))); + } + } + } + |] + Just c <- solcRuntime "C" code + 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:" + + , 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" + + , testCase "safemath distributivity (sol)" $ do + let code = + [i| + contract C { + function distributivity(uint x, uint y, uint z) public { + assert(mul(x, add(y, z)) == add(mul(x, y), mul(x, z))); + } + + function add(uint x, uint y) internal pure returns (uint z) { + 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"); + } + } + |] + Just c <- solcRuntime "C" code + + 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" + ] , testGroup "Equivalence checking" [ @@ -538,7 +612,7 @@ runSimpleVM :: ByteString -> ByteString -> Maybe ByteString runSimpleVM x ins = case loadVM x of Nothing -> Nothing - Just vm -> let calldata' = (ConcreteBuffer ins, literal . num $ BS.length ins) + Just vm -> let calldata' = (ConcreteBuffer ins, w256lit $ num $ BS.length ins) in case runState (assign (state.calldata) calldata' >> exec) vm of (VMSuccess (ConcreteBuffer bs), _) -> Just bs _ -> Nothing @@ -605,8 +679,11 @@ getStaticAbiArgs :: VM -> [SWord 256] getStaticAbiArgs vm = - let SymbolicBuffer bs = ditch 4 $ view (state . calldata . _1) vm - in fmap (\i -> fromBytes $ take 32 (drop (i*32) bs)) [0..((length bs) `div` 32 - 1)] + let cd = view (state . calldata . _1) vm + bs = case cd of + ConcreteBuffer bs' -> ConcreteBuffer $ BS.drop 4 bs' + SymbolicBuffer bs' -> SymbolicBuffer $ drop 4 bs' + in decodeStaticArgs bs -- includes shaving off 4 byte function sig decodeAbiValues :: [AbiType] -> ByteString -> [AbiValue]