diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,11 +5,33 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.50.4] - 2023-03-17 + +### Fixed + +- The `--solvers` cli option is now respected (previously we always used Z3) +- The `equivalence` command now fails with the correct status code when counterexamples are found +- The `equivalence` command now respects the given `--sig` argument +- Correct symbolic execution for the `SGT` opcode + +### Changed + +- The `equivalence` command now pretty prints discovered counterexamples + +### Added + +- Implemented a shrinking algorithm for counterexamples +- A new differential fuzzing test harness that compares the concrete semantics, as well as parts of the symbolic semantics against the geth evm implementation +- The `hevm` library can now be built on Windows systems. +- Support for function pointers in ABI +- `equivalence` can now be checked for fully or partially concrete calldata + ## [0.50.3] - 2023-02-17 ### Fixed - `hevm symbolic` exits with status code `1` if counterexamples or timeouts are found +- Calldata reads beyond calldata size are provably equal to zero. ### Added @@ -18,6 +40,9 @@ - Improved simplification for arithmetic expressions - Construction of storage counterexamples based on the model returned by the SMT solver. - Static binaries for macos + +### Changed +- SMT encoding of buffer length without using uninterpreted functions. ## [0.50.2] - 2023-01-06 diff --git a/bench/bench.hs b/bench/bench.hs --- a/bench/bench.hs +++ b/bench/bench.hs @@ -47,7 +47,7 @@ main :: IO () main = defaultMain - [ mkbench erc20 "erc20" Nothing [1, 2, 4, 8, 16] + [ mkbench erc20 "erc20" Nothing [1] , mkbench (pure vat) "vat" Nothing [4] , mkbench (pure deposit) "deposit" (Just 32) [4] , mkbench (pure uniV2Pair) "uniV2" (Just 10) [4] @@ -59,7 +59,7 @@ debugContract :: ByteString -> IO () debugContract c = withSolvers CVC5 4 Nothing $ \solvers -> do - let prestate = abstractVM Nothing [] c Nothing SymbolicS + let prestate = abstractVM (mkCalldata Nothing []) c Nothing SymbolicS void $ TTY.runFromVM solvers Nothing Nothing emptyDapp prestate 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 @@ -15,7 +15,6 @@ import EVM.SymExec import EVM.Debug import qualified EVM.Expr as Expr -import EVM.SMT import EVM.Solvers import qualified EVM.TTY as TTY import EVM.Solidity @@ -36,7 +35,7 @@ import Control.Monad (void, when, forM_, unless) import Control.Monad.State.Strict (execStateT, liftIO) import Data.ByteString (ByteString) -import Data.List (intercalate, isSuffixOf) +import Data.List (intercalate, isSuffixOf, intersperse) import Data.Text (unpack, pack) import Data.Maybe (fromMaybe, mapMaybe) import Data.Version (showVersion) @@ -109,6 +108,8 @@ { 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" + , arg :: w ::: [String] "Values to encode" + , calldata :: w ::: Maybe ByteString "Tx: calldata" , smttimeout :: w ::: Maybe Natural "Timeout given to SMT solver in milliseconds (default: 60000)" , maxIterations :: w ::: Maybe Integer "Number of times we may revisit a particular branching point" , solver :: w ::: Maybe Text "Used SMT solver: z3 (default) or cvc5" @@ -266,7 +267,8 @@ DappTest {} -> withCurrentDirectory root $ do cores <- num <$> getNumProcessors - withSolvers Z3 cores cmd.smttimeout $ \solvers -> do + solver <- getSolver cmd + withSolvers solver cores cmd.smttimeout $ \solvers -> do testFile <- findJsonFile cmd.jsonFile testOpts <- unitTestOptions cmd solvers testFile case (cmd.coverage, optsMode cmd) of @@ -307,19 +309,34 @@ , askSmtIters = cmd.askSmtIterations , rpcInfo = Nothing } - - withSolvers Z3 3 Nothing $ \s -> do - res <- equivalenceCheck s bytecodeA bytecodeB veriOpts Nothing - case not (any isCex res) of + calldata <- buildCalldata cmd + solver <- getSolver cmd + withSolvers solver 3 Nothing $ \s -> do + res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata + case any isCex res of False -> do putStrLn "No discrepancies found" when (any isTimeout res) $ do putStrLn "But timeout(s) occurred" exitFailure True -> do - putStrLn $ "Not equivalent. Counterexample(s):" <> show res + let cexs = mapMaybe getCex res + T.putStrLn . T.unlines $ + [ "Not equivalent. The following inputs result in differing behaviours:" + , "" , "-----", "" + ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (formatCex (AbstractBuf "txdata")) cexs) exitFailure +getSolver :: Command Options.Unwrapped -> IO Solver +getSolver cmd = case cmd.solver of + Nothing -> pure Z3 + Just s -> case T.unpack s of + "z3" -> pure Z3 + "cvc5" -> pure CVC5 + input -> do + putStrLn $ "unrecognised solver: " <> input + exitFailure + getSrcInfo :: Command Options.Unwrapped -> IO DappInfo getSrcInfo cmd = let root = fromMaybe "." cmd.dappRoot @@ -332,42 +349,36 @@ Just (contractMap, sourceCache) -> pure $ dappInfo root contractMap sourceCache --- Although it is tempting to fully abstract calldata and give any hints about --- the nature of the signature doing so results in significant time spent in --- consulting z3 about rather trivial matters. But with cvc5 it is quite --- pleasant! +-- | Builds a buffer representing calldata based on the given cli arguments +buildCalldata :: Command Options.Unwrapped -> IO (Expr Buf, [Prop]) +buildCalldata cmd = case (cmd.calldata, cmd.sig) of + -- fully abstract calldata + (Nothing, Nothing) -> pure $ mkCalldata Nothing [] + -- fully concrete calldata + (Just c, Nothing) -> pure (ConcreteBuf (hexByteString "bytes" . strip0x $ c), []) + -- calldata according to given abi with possible specializations from the `arg` list + (Nothing, Just sig') -> do + method' <- functionAbi sig' + pure $ mkCalldata (Just (Sig method'.methodSignature (snd <$> method'.inputs))) cmd.arg + -- both args provided + (_, _) -> do + putStrLn "incompatible options provided: --calldata and --sig" + exitFailure + + -- If function signatures are known, they should always be given for best results. assert :: Command Options.Unwrapped -> IO () assert cmd = do let block' = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block rpcinfo = (,) block' <$> cmd.rpc - decipher = hexByteString "bytes" . strip0x - calldata' <- case (cmd.calldata, cmd.sig) of - -- fully abstract calldata - (Nothing, Nothing) -> pure - ( AbstractBuf "txdata" - -- assert that the length of the calldata is never more than 2^64 - -- this is way larger than would ever be allowed by the gas limit - -- and avoids spurious counterexamples during abi decoding - -- TODO: can we encode calldata as an array with a smaller length? - , [Expr.bufLength (AbstractBuf "txdata") .< (Lit (2 ^ (64 :: Integer)))] - ) - - -- fully concrete calldata - (Just c, Nothing) -> pure (ConcreteBuf (decipher c), []) - -- calldata according to given abi with possible specializations from the `arg` list - (Nothing, Just sig') -> do - method' <- functionAbi sig' - let typs = snd <$> method'.inputs - pure $ symCalldata method'.methodSignature typs cmd.arg (AbstractBuf "txdata") - _ -> error "incompatible options: calldata and abi" - + calldata' <- buildCalldata cmd preState <- symvmFromCommand cmd calldata' let errCodes = fromMaybe defaultPanicCodes cmd.assertions cores <- num <$> getNumProcessors let solverCount = fromMaybe cores cmd.numSolvers - withSolvers EVM.Solvers.Z3 solverCount cmd.smttimeout $ \solvers -> do + solver <- getSolver cmd + withSolvers solver solverCount cmd.smttimeout $ \solvers -> do if cmd.debug then do srcInfo <- getSrcInfo cmd void $ TTY.runFromVM @@ -381,21 +392,23 @@ (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes) case res of [Qed _] -> putStrLn "\nQED: No reachable property violations discovered\n" - cexs -> do - let counterexamples - | null (getCexs cexs) = [] + _ -> do + let cexs = snd <$> mapMaybe getCex res + timeouts = mapMaybe getTimeout res + counterexamples + | null cexs = [] | otherwise = [ "" , "Discovered the following counterexamples:" , "" - ] <> fmap (formatCex (fst calldata')) (getCexs cexs) + ] <> fmap (formatCex (fst calldata')) cexs unknowns - | null (getTimeouts cexs) = [] + | null timeouts = [] | otherwise = [ "" , "Could not determine reachability of the following end states:" , "" - ] <> fmap (formatExpr) (getTimeouts cexs) + ] <> fmap (formatExpr) timeouts T.putStrLn $ T.unlines (counterexamples <> unknowns) exitFailure when cmd.showTree $ do @@ -412,17 +425,13 @@ ms <- produceModels solvers expr forM_ ms (showModel (fst calldata')) -getCexs :: [VerifyResult] -> [SMTCex] -getCexs = mapMaybe go - where - go (Cex cex) = Just $ snd cex - go _ = Nothing +getCex :: ProofResult a b c -> Maybe b +getCex (Cex c) = Just c +getCex _ = Nothing -getTimeouts :: [VerifyResult] -> [Expr End] -getTimeouts = mapMaybe go - where - go (Timeout leaf) = Just leaf - go _ = Nothing +getTimeout :: ProofResult a b c -> Maybe c +getTimeout (Timeout c) = Just c +getTimeout _ = Nothing dappCoverage :: UnitTestOptions -> Mode -> String -> IO () dappCoverage opts _ solcFile = @@ -480,16 +489,16 @@ let res = case msg of ConcreteBuf bs -> bs _ -> "" - print $ ByteStringS res + putStrLn $ "Revert: " <> (show $ ByteStringS res) exitWith (ExitFailure 2) Just (EVM.VMFailure err) -> do - print err + putStrLn $ "Error: " <> show err exitWith (ExitFailure 2) Just (EVM.VMSuccess buf) -> do let msg = case buf of ConcreteBuf msg' -> msg' _ -> "" - print $ ByteStringS msg + print $ "Return: " <> (show $ ByteStringS msg) case cmd.state of Nothing -> pure () Just path -> diff --git a/hevm.cabal b/hevm.cabal --- a/hevm.cabal +++ b/hevm.cabal @@ -2,7 +2,7 @@ name: hevm version: - 0.50.3 + 0.50.4 synopsis: Ethereum virtual machine evaluator description: @@ -40,6 +40,7 @@ test/contracts/fail/cheatCodes.sol test/contracts/fail/dsProveFail.sol test/contracts/fail/invariantFail.sol + test/scripts/convert_trace_to_json.sh flag ci description: Sets flags for compilation in CI @@ -76,6 +77,7 @@ exposed-modules: EVM, EVM.ABI, + EVM.Assembler, EVM.Concrete, EVM.Dapp, EVM.Debug, @@ -103,22 +105,22 @@ EVM.CSE, EVM.Keccak, EVM.Transaction, - EVM.TTY, - EVM.TTYCenteredList, EVM.Types, EVM.UnitTest, + EVM.Sign, + if !os(windows) + exposed-modules: + EVM.TTY, + EVM.TTYCenteredList other-modules: Paths_hevm autogen-modules: Paths_hevm - if flag(devel) - ghc-options: -Wall -Wno-deprecations -Wno-unticked-promoted-constructors -Wno-orphans -j - else - ghc-options: -Wall -Wno-deprecations -Wno-unticked-promoted-constructors -Wno-orphans + ghc-options: -Wall -Wno-deprecations -Wno-unticked-promoted-constructors -Wno-orphans + if os(linux) || os(windows) + extra-libraries: stdc++ extra-libraries: - secp256k1, ff - if os(linux) - extra-libraries: stdc++ + secp256k1, ff, gmp c-sources: ethjet/tinykeccak.c, ethjet/ethjet.c cxx-sources: @@ -144,13 +146,11 @@ unordered-containers >= 0.2.10 && < 0.3, vector >= 0.12.1 && < 0.13, ansi-wl-pprint >= 0.6.9 && < 0.7, - base16-bytestring >= 1.0.0 && < 2.0, - brick >= 1.4 && < 1.5, + base16 >= 0.3.2.0 && < 0.3.3.0, megaparsec >= 9.0.0 && < 10.0, mtl >= 2.2.2 && < 2.3, directory >= 1.3.3 && < 1.4, filepath >= 1.4.2 && < 1.5, - vty >= 5.37 && < 5.38, cereal >= 0.5.8 && < 0.6, cryptonite >= 0.30 && < 0.31, memory >= 0.16.0 && < 0.20, @@ -180,6 +180,10 @@ spool >= 0.1 && < 0.2, stm >= 2.5.0 && < 2.6.0, spawn >= 0.3 && < 0.4 + if !os(windows) + build-depends: + brick >= 1.4 && < 1.5, + vty >= 5.37 && < 5.38 hs-source-dirs: src @@ -189,10 +193,7 @@ hevm-cli main-is: hevm-cli.hs - if flag(devel) - ghc-options: -Wall -threaded -with-rtsopts=-N -Wno-unticked-promoted-constructors -Wno-orphans -j - else - ghc-options: -Wall -threaded -with-rtsopts=-N -Wno-unticked-promoted-constructors -Wno-orphans + ghc-options: -Wall -threaded -with-rtsopts=-N -Wno-unticked-promoted-constructors -Wno-orphans other-modules: Paths_hevm if os(darwin) @@ -206,7 +207,7 @@ ansi-wl-pprint, async, base, - base16-bytestring, + base16, binary, brick, bytestring, @@ -234,15 +235,14 @@ vty, stm, spawn + if os(windows) + buildable: False --- Test Helpers --- common test-base import: shared - if flag (devel) - ghc-options: -Wall -Wno-unticked-promoted-constructors -Wno-orphans -j - else - ghc-options: -Wall -Wno-unticked-promoted-constructors -Wno-orphans + ghc-options: -Wall -Wno-unticked-promoted-constructors -Wno-orphans hs-source-dirs: test extra-libraries: @@ -257,7 +257,7 @@ quickcheck-instances, aeson, base, - base16-bytestring, + base16, binary, containers, directory, @@ -285,21 +285,29 @@ stm >= 2.5.0, spawn >= 0.3, witherable, - smt2-parser >= 0.1.0.1 + smt2-parser >= 0.1.0.1, + operational library test-utils import: test-base exposed-modules: EVM.TestUtils + if os(windows) + buildable: False common test-common import: test-base + if flag(devel) + ghc-options: -threaded -with-rtsopts=-N build-depends: test-utils other-modules: EVM.TestUtils + EVM.Tracing + if os(windows) + buildable: False if os(darwin) extra-libraries: c++ -- https://gitlab.haskell.org/ghc/ghc/-/issues/11829 diff --git a/src/EVM.hs b/src/EVM.hs --- a/src/EVM.hs +++ b/src/EVM.hs @@ -1,7 +1,6 @@ {-# Language ImplicitParams #-} {-# Language DataKinds #-} {-# Language GADTs #-} -{-# Language StrictData #-} {-# Language TemplateHaskell #-} module EVM where @@ -18,6 +17,7 @@ import EVM.Precompiled qualified import EVM.Solidity import EVM.Types hiding (IllegalOverflow, Error) +import EVM.Sign qualified import Control.Lens hiding (op, (:<), (|>), (.>)) import Control.Monad.State.Strict hiding (state) @@ -49,12 +49,10 @@ import Data.Word (Word8, Word32, Word64) import Options.Generic as Options -import Crypto.Hash (Digest, SHA256, RIPEMD160, digestFromByteString) +import Crypto.Hash (Digest, SHA256, RIPEMD160) import Crypto.Hash qualified as Crypto import Crypto.Number.ModArithmetic (expFast) import Crypto.PubKey.ECC.ECDSA (signDigestWith, PrivateKey(..), Signature(..)) -import Crypto.PubKey.ECC.Generate (generateQ) -import Crypto.PubKey.ECC.Types (getCurveByName, CurveName(..), Point(..)) -- * Data types @@ -83,6 +81,7 @@ | NotUnique (Expr EWord) | SMTTimeout | FFI [AbiValue] + | ReturnDataOutOfBounds | NonceOverflow deriving instance Show Error @@ -104,7 +103,7 @@ , _logs :: [Expr Log] , _traces :: Zipper.TreePos Zipper.Empty Trace , _cache :: Cache - , _burned :: Word64 + , _burned :: {-# UNPACK #-} !Word64 , _iterations :: Map CodeLocation Int , _constraints :: [Prop] , _keccakEqs :: [Prop] @@ -248,14 +247,14 @@ { _contract :: Addr , _codeContract :: Addr , _code :: ContractCode - , _pc :: Int + , _pc :: {-# UNPACK #-} !Int , _stack :: [Expr EWord] , _memory :: Expr Buf , _memorySize :: Word64 , _calldata :: Expr Buf , _callvalue :: Expr EWord , _caller :: Expr EWord - , _gas :: Word64 + , _gas :: {-# UNPACK #-} !Word64 , _returndata :: Expr Buf , _static :: Bool } @@ -391,8 +390,9 @@ , _baseFee :: W256 , _maxCodeSize :: W256 , _schedule :: FeeSchedule Word64 - } deriving Show + } deriving (Show, Generic) + blankState :: FrameState blankState = FrameState { _contract = 0 @@ -610,11 +610,10 @@ fromMaybe (error "could not analyze symbolic code") $ unlitByte $ ops V.! vm._state._pc - case ?op of + case getOp(?op) of - -- op: PUSH - x | x >= 0x60 && x <= 0x7f -> do - let !n = num x - 0x60 + 1 + OpPush n' -> do + let n = fromIntegral n' !xs = case vm._state._code of InitCode conc _ -> Lit $ word $ padRight n $ BS.take n (BS.drop (1 + vm._state._pc) conc) RuntimeCode (ConcreteRuntimeCode bs) -> Lit $ word $ BS.take n $ BS.drop (1 + vm._state._pc) bs @@ -626,10 +625,8 @@ next pushSym xs - -- op: DUP - x | x >= 0x80 && x <= 0x8f -> do - let !i = x - 0x80 + 1 - case preview (ix (num i - 1)) stk of + OpDup i -> + case preview (ix (fromIntegral i - 1)) stk of Nothing -> underrun Just y -> limitStack 1 $ @@ -637,33 +634,29 @@ next pushSym y - -- op: SWAP - x | x >= 0x90 && x <= 0x9f -> do - let i = num (x - 0x90 + 1) - if length stk < i + 1 + OpSwap i -> + if length stk < (fromIntegral i) + 1 then underrun else burn g_verylow $ do next zoom (state . stack) $ do - assign (ix 0) (stk ^?! ix i) - assign (ix i) (stk ^?! ix 0) + assign (ix 0) (stk ^?! ix (fromIntegral i)) + assign (ix (fromIntegral i)) (stk ^?! ix 0) - -- op: LOG - x | x >= 0xa0 && x <= 0xa4 -> + OpLog n -> notStatic $ - let n = (num x - 0xa0) in case stk of (xOffset':xSize':xs) -> - if length xs < n + if length xs < (fromIntegral n) then underrun else forceConcrete2 (xOffset', xSize') "LOG" $ \(xOffset, xSize) -> do - let (topics, xs') = splitAt n xs + let (topics, xs') = splitAt (fromIntegral n) xs bytes = readMemory xOffset' xSize' vm logs' = (LogEntry (litAddr self) bytes topics) : vm._logs burn (g_log + g_logdata * (num xSize) + num n * g_logtopic) $ - accessMemoryRange fees xOffset xSize $ do + accessMemoryRange xOffset xSize $ do traceTopLog logs' next assign (state . stack) xs' @@ -671,74 +664,49 @@ _ -> underrun - -- op: STOP - 0x00 -> doStop + OpStop -> doStop - -- op: ADD - 0x01 -> stackOp2 (const g_verylow) (uncurry Expr.add) - -- op: MUL - 0x02 -> stackOp2 (const g_low) (uncurry Expr.mul) - -- op: SUB - 0x03 -> stackOp2 (const g_verylow) (uncurry Expr.sub) + OpAdd -> stackOp2 g_verylow (uncurry Expr.add) + OpMul -> stackOp2 g_low (uncurry Expr.mul) + OpSub -> stackOp2 g_verylow (uncurry Expr.sub) - -- op: DIV - 0x04 -> stackOp2 (const g_low) (uncurry Expr.div) + OpDiv -> stackOp2 g_low (uncurry Expr.div) - -- op: SDIV - 0x05 -> stackOp2 (const g_low) (uncurry Expr.sdiv) + OpSdiv -> stackOp2 g_low (uncurry Expr.sdiv) - -- op: MOD - 0x06 -> stackOp2 (const g_low) (uncurry Expr.mod) + OpMod-> stackOp2 g_low (uncurry Expr.mod) - -- op: SMOD - 0x07 -> stackOp2 (const g_low) (uncurry Expr.smod) - -- op: ADDMOD - 0x08 -> stackOp3 (const g_mid) (uncurryN Expr.addmod) - -- op: MULMOD - 0x09 -> stackOp3 (const g_mid) (uncurryN Expr.mulmod) + OpSmod -> stackOp2 g_low (uncurry Expr.smod) + OpAddmod -> stackOp3 g_mid (uncurryN Expr.addmod) + OpMulmod -> stackOp3 g_mid (uncurryN Expr.mulmod) - -- op: LT - 0x10 -> stackOp2 (const g_verylow) (uncurry Expr.lt) - -- op: GT - 0x11 -> stackOp2 (const g_verylow) (uncurry Expr.gt) - -- op: SLT - 0x12 -> stackOp2 (const g_verylow) (uncurry Expr.slt) - -- op: SGT - 0x13 -> stackOp2 (const g_verylow) (uncurry Expr.sgt) + OpLt -> stackOp2 g_verylow (uncurry Expr.lt) + OpGt -> stackOp2 g_verylow (uncurry Expr.gt) + OpSlt -> stackOp2 g_verylow (uncurry Expr.slt) + OpSgt -> stackOp2 g_verylow (uncurry Expr.sgt) - -- op: EQ - 0x14 -> stackOp2 (const g_verylow) (uncurry Expr.eq) - -- op: ISZERO - 0x15 -> stackOp1 (const g_verylow) Expr.iszero + OpEq -> stackOp2 g_verylow (uncurry Expr.eq) + OpIszero -> stackOp1 g_verylow Expr.iszero - -- op: AND - 0x16 -> stackOp2 (const g_verylow) (uncurry Expr.and) - -- op: OR - 0x17 -> stackOp2 (const g_verylow) (uncurry Expr.or) - -- op: XOR - 0x18 -> stackOp2 (const g_verylow) (uncurry Expr.xor) - -- op: NOT - 0x19 -> stackOp1 (const g_verylow) Expr.not + OpAnd -> stackOp2 g_verylow (uncurry Expr.and) + OpOr -> stackOp2 g_verylow (uncurry Expr.or) + OpXor -> stackOp2 g_verylow (uncurry Expr.xor) + OpNot -> stackOp1 g_verylow Expr.not - -- op: BYTE - 0x1a -> stackOp2 (const g_verylow) (\(i, w) -> Expr.padByte $ Expr.indexWord i w) + OpByte -> stackOp2 g_verylow (\(i, w) -> Expr.padByte $ Expr.indexWord i w) - -- op: SHL - 0x1b -> stackOp2 (const g_verylow) (uncurry Expr.shl) - -- op: SHR - 0x1c -> stackOp2 (const g_verylow) (uncurry Expr.shr) - -- op: SAR - 0x1d -> stackOp2 (const g_verylow) (uncurry Expr.sar) + OpShl -> stackOp2 g_verylow (uncurry Expr.shl) + OpShr -> stackOp2 g_verylow (uncurry Expr.shr) + OpSar -> stackOp2 g_verylow (uncurry Expr.sar) - -- op: SHA3 -- more accurately refered to as KECCAK - 0x20 -> + OpSha3 -> case stk of (xOffset' : xSize' : xs) -> forceConcrete xOffset' "sha3 offset must be concrete" $ \xOffset -> forceConcrete xSize' "sha3 size must be concrete" $ \xSize -> burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $ - accessMemoryRange fees xOffset xSize $ do + accessMemoryRange xOffset xSize $ do (hash, invMap) <- case readMemory xOffset' xSize' vm of ConcreteBuf bs -> do let hash' = keccak' bs @@ -751,13 +719,11 @@ (env . sha3Crack) <>= invMap _ -> underrun - -- op: ADDRESS - 0x30 -> + OpAddress -> limitStack 1 $ burn g_base (next >> push (num self)) - -- op: BALANCE - 0x31 -> + OpBalance -> case stk of (x':xs) -> forceConcrete x' "BALANCE" $ \x -> accessAndBurn (num x) $ @@ -768,50 +734,42 @@ [] -> underrun - -- op: ORIGIN - 0x32 -> + OpOrigin -> limitStack 1 . burn g_base $ next >> push (num vm._tx._origin) - -- op: CALLER - 0x33 -> + OpCaller -> limitStack 1 . burn g_base $ next >> pushSym vm._state._caller - -- op: CALLVALUE - 0x34 -> + OpCallvalue -> limitStack 1 . burn g_base $ next >> pushSym vm._state._callvalue - -- op: CALLDATALOAD - 0x35 -> stackOp1 (const g_verylow) $ + OpCalldataload -> stackOp1 g_verylow $ \ind -> Expr.readWord ind vm._state._calldata - -- op: CALLDATASIZE - 0x36 -> + OpCalldatasize -> limitStack 1 . burn g_base $ next >> pushSym (bufLength vm._state._calldata) - -- op: CALLDATACOPY - 0x37 -> + OpCalldatacopy -> case stk of (xTo' : xFrom : xSize' : xs) -> forceConcrete2 (xTo', xSize') "CALLDATACOPY" $ \(xTo, xSize) -> burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $ - accessMemoryRange fees xTo xSize $ do + accessMemoryRange xTo xSize $ do next assign (state . stack) xs copyBytesToMemory vm._state._calldata xSize' xFrom xTo' _ -> underrun - -- op: CODESIZE - 0x38 -> + OpCodesize -> limitStack 1 . burn g_base $ next >> pushSym (codelen vm._state._code) - -- op: CODECOPY - 0x39 -> + OpCodecopy -> case stk of (memOffset' : codeOffset : n' : xs) -> forceConcrete2 (memOffset', n') "CODECOPY" $ @@ -821,20 +779,18 @@ Just n'' -> if n'' <= ( (maxBound :: Word64) - g_verylow ) `div` g_copy * 32 then burn (g_verylow + g_copy * ceilDiv (num n) 32) $ - accessMemoryRange fees memOffset n $ do + accessMemoryRange memOffset n $ do next assign (state . stack) xs copyBytesToMemory (toBuf vm._state._code) n' codeOffset memOffset' else vmError IllegalOverflow _ -> underrun - -- op: GASPRICE - 0x3a -> + OpGasprice -> limitStack 1 . burn g_base $ next >> push vm._tx._gasprice - -- op: EXTCODESIZE - 0x3b -> + OpExtcodesize -> case stk of (x':xs) -> case x' of (Lit x) -> if x == num cheatCode @@ -855,8 +811,7 @@ [] -> underrun - -- op: EXTCODECOPY - 0x3c -> + OpExtcodecopy -> case stk of ( extAccount' : memOffset' @@ -868,29 +823,27 @@ acc <- accessAccountForGas (num extAccount) let cost = if acc then g_warm_storage_read else g_cold_account_access burn (cost + g_copy * ceilDiv (num codeSize) 32) $ - accessMemoryRange fees memOffset codeSize $ + accessMemoryRange memOffset codeSize $ fetchAccount (num extAccount) $ \c -> do next assign (state . stack) xs copyBytesToMemory (view bytecode c) codeSize' codeOffset memOffset' _ -> underrun - -- op: RETURNDATASIZE - 0x3d -> + OpReturndatasize -> limitStack 1 . burn g_base $ next >> pushSym (bufLength vm._state._returndata) - -- op: RETURNDATACOPY - 0x3e -> + OpReturndatacopy -> case stk of (xTo' : xFrom : xSize' :xs) -> forceConcrete2 (xTo', xSize') "RETURNDATACOPY" $ \(xTo, xSize) -> burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $ - accessMemoryRange fees xTo xSize $ do + accessMemoryRange xTo xSize $ do next assign (state . stack) xs - let jump True = vmError EVM.InvalidMemoryAccess + let jump True = vmError EVM.ReturnDataOutOfBounds jump False = copyBytesToMemory vm._state._returndata xSize' xFrom xTo' case (xFrom, bufLength vm._state._returndata) of @@ -903,8 +856,7 @@ branch loc (Expr.or oob overflow) jump _ -> underrun - -- op: EXTCODEHASH - 0x3f -> + OpExtcodehash -> case stk of (x':xs) -> forceConcrete x' "EXTCODEHASH" $ \x -> accessAndBurn (num x) $ do @@ -917,97 +869,83 @@ [] -> underrun - -- op: BLOCKHASH - 0x40 -> do + OpBlockhash -> do -- We adopt the fake block hash scheme of the VMTests, -- so that blockhash(i) is the hash of i as decimal ASCII. - stackOp1 (const g_blockhash) $ \case + stackOp1 g_blockhash $ \case (Lit i) -> if i + 256 < vm._block._number || i >= vm._block._number then Lit 0 else (num i :: Integer) & show & Char8.pack & keccak' & Lit i -> BlockHash i - -- op: COINBASE - 0x41 -> + OpCoinbase -> limitStack 1 . burn g_base $ next >> push (num vm._block._coinbase) - -- op: TIMESTAMP - 0x42 -> + OpTimestamp -> limitStack 1 . burn g_base $ next >> pushSym vm._block._timestamp - -- op: NUMBER - 0x43 -> + OpNumber -> limitStack 1 . burn g_base $ next >> push vm._block._number - -- op: PREVRANDAO - 0x44 -> do + OpPrevRandao -> do limitStack 1 . burn g_base $ next >> push vm._block._prevRandao - -- op: GASLIMIT - 0x45 -> + OpGaslimit -> limitStack 1 . burn g_base $ next >> push (num vm._block._gaslimit) - -- op: CHAINID - 0x46 -> + OpChainid -> limitStack 1 . burn g_base $ next >> push vm._env._chainId - -- op: SELFBALANCE - 0x47 -> + OpSelfbalance -> limitStack 1 . burn g_low $ next >> push this._balance - -- op: BASEFEE - 0x48 -> + OpBaseFee -> limitStack 1 . burn g_base $ next >> push vm._block._baseFee - -- op: POP - 0x50 -> + OpPop -> case stk of (_:xs) -> burn g_base (next >> assign (state . stack) xs) _ -> underrun - -- op: MLOAD - 0x51 -> + OpMload -> case stk of (x':xs) -> forceConcrete x' "MLOAD" $ \x -> burn g_verylow $ - accessMemoryWord fees x $ do + accessMemoryWord x $ do next assign (state . stack) (readWord (Lit x) mem : xs) _ -> underrun - -- op: MSTORE - 0x52 -> + OpMstore -> case stk of (x':y:xs) -> forceConcrete x' "MSTORE index" $ \x -> burn g_verylow $ - accessMemoryWord fees x $ do + accessMemoryWord x $ do next assign (state . memory) (writeWord (Lit x) y mem) assign (state . stack) xs _ -> underrun - -- op: MSTORE8 - 0x53 -> + OpMstore8 -> case stk of (x':y:xs) -> forceConcrete x' "MSTORE8" $ \x -> burn g_verylow $ - accessMemoryRange fees x 1 $ do + accessMemoryRange x 1 $ do let yByte = indexWord (Lit 31) y next modifying (state . memory) (writeByte (Lit x) yByte) assign (state . stack) xs _ -> underrun - -- op: SLOAD - 0x54 -> + OpSload -> case stk of (x:xs) -> do acc <- accessStorageForGas self x @@ -1018,8 +956,7 @@ assign (state . stack) (y:xs) _ -> underrun - -- op: SSTORE - 0x55 -> + OpSstore -> notStatic $ case stk of (x:new:xs) -> @@ -1071,8 +1008,7 @@ _ -> noop _ -> underrun - -- op: JUMP - 0x56 -> + OpJump -> case stk of (x:xs) -> burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' -> @@ -1081,8 +1017,7 @@ Just i -> checkJump i xs _ -> underrun - -- op: JUMPI - 0x57 -> do + OpJumpi -> do case stk of (x:y:xs) -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' -> burn g_high $ @@ -1099,26 +1034,21 @@ branch loc y jump _ -> underrun - -- op: PC - 0x58 -> + OpPc -> limitStack 1 . burn g_base $ next >> push (num vm._state._pc) - -- op: MSIZE - 0x59 -> + OpMsize -> limitStack 1 . burn g_base $ next >> push (num vm._state._memorySize) - -- op: GAS - 0x5a -> + OpGas -> limitStack 1 . burn g_base $ next >> push (num (vm._state._gas - g_base)) - -- op: JUMPDEST - 0x5b -> burn g_jumpdest next + OpJumpdest -> burn g_jumpdest next - -- op: EXP - 0x0a -> + OpExp -> -- NOTE: this can be done symbolically using unrolling like this: -- https://hackage.haskell.org/package/sbv-9.0/docs/src/Data.SBV.Core.Model.html#.%5E -- However, it requires symbolic gas, since the gas depends on the exponent @@ -1132,16 +1062,14 @@ state . stack .= Expr.exp base exponent' : xs _ -> underrun - -- op: SIGNEXTEND - 0x0b -> stackOp2 (const g_low) (uncurry Expr.sex) + OpSignextend -> stackOp2 g_low (uncurry Expr.sex) - -- op: CREATE - 0xf0 -> + OpCreate -> notStatic $ case stk of (xValue' : xOffset' : xSize' : xs) -> forceConcrete3 (xValue', xOffset', xSize') "CREATE" $ \(xValue, xOffset, xSize) -> do - accessMemoryRange fees xOffset xSize $ do + accessMemoryRange xOffset xSize $ do availableGas <- use (state . gas) let newAddr = createAddress self this._nonce @@ -1155,8 +1083,7 @@ create self this (num gas') xValue xs newAddr initCode _ -> underrun - -- op: CALL - 0xf1 -> + OpCall -> case stk of ( xGas' : xTo @@ -1181,8 +1108,7 @@ _ -> underrun - -- op: CALLCODE - 0xf2 -> + OpCallcode -> case stk of ( xGas' : xTo @@ -1203,11 +1129,10 @@ _ -> underrun - -- op: RETURN - 0xf3 -> + OpReturn -> case stk of (xOffset' : xSize' :_) -> forceConcrete2 (xOffset', xSize') "RETURN" $ \(xOffset, xSize) -> - accessMemoryRange fees xOffset xSize $ do + accessMemoryRange xOffset xSize $ do let output = readMemory xOffset' xSize' vm codesize = fromMaybe (error "RETURN: cannot return dynamically sized abstract data") @@ -1239,8 +1164,7 @@ finishFrame (FrameReturned output) _ -> underrun - -- op: DELEGATECALL - 0xf4 -> + OpDelegatecall -> case stk of (xGas' :xTo @@ -1254,8 +1178,7 @@ touchAccount self _ -> underrun - -- op: CREATE2 - 0xf5 -> notStatic $ + OpCreate2 -> notStatic $ case stk of (xValue' :xOffset' @@ -1263,7 +1186,7 @@ :xSalt' :xs) -> forceConcrete4 (xValue', xOffset', xSize', xSalt') "CREATE2" $ \(xValue, xOffset, xSize, xSalt) -> - accessMemoryRange fees xOffset xSize $ do + accessMemoryRange xOffset xSize $ do availableGas <- use (state . gas) forceConcreteBuf (readMemory xOffset' xSize' vm) "CREATE2" $ @@ -1275,8 +1198,7 @@ burn (cost - gas') $ create self this gas' xValue xs newAddr (ConcreteBuf initCode) _ -> underrun - -- op: STATICCALL - 0xfa -> + OpStaticcall -> case stk of (xGas' :xTo @@ -1298,8 +1220,7 @@ _ -> underrun - -- op: SELFDESTRUCT - 0xff -> + OpSelfdestruct -> notStatic $ case stk of [] -> underrun @@ -1322,16 +1243,15 @@ doStop else doStop - -- op: REVERT - 0xfd -> + OpRevert -> case stk of (xOffset':xSize':_) -> forceConcrete2 (xOffset', xSize') "REVERT" $ \(xOffset, xSize) -> - accessMemoryRange fees xOffset xSize $ do + accessMemoryRange xOffset xSize $ do let output = readMemory xOffset' xSize' vm finishFrame (FrameReverted output) _ -> underrun - xxx -> + OpUnknown xxx -> vmError (UnrecognizedOpcode xxx) transfer :: Addr -> Addr -> W256 -> EVM () @@ -1350,8 +1270,8 @@ callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue = do vm <- get let fees = vm._block._schedule - accessMemoryRange fees xInOffset xInSize $ - accessMemoryRange fees xOutOffset xOutSize $ do + accessMemoryRange xInOffset xInSize $ + accessMemoryRange xOutOffset xOutSize $ do availableGas <- use (state . gas) let recipientExists = accountExists xContext vm (cost, gas') <- costOfCall fees recipientExists xValue availableGas xGas xTo @@ -1996,51 +1916,28 @@ action "sign(uint256,bytes32)" $ \sig outOffset _ input -> case decodeStaticArgs 0 2 input of [sk, hash] -> - forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> let - curve = getCurveByName SEC_p256k1 - priv = PrivateKey curve (num sk') - digest = digestFromByteString (word256Bytes hash') - in do - case digest of - Nothing -> vmError (BadCheatCode sig) - Just digest' -> do - let s = ethsign priv digest' - -- calculating the V value is pretty annoying if you - -- don't have access to the full X/Y coords of the - -- signature (which we don't get back from cryptonite). - -- Luckily since we use a fixed nonce (to avoid the - -- overhead of bringing randomness into the core EVM - -- semantics), it would appear that every signature we - -- produce has v == 28. Definitely a hack, and also bad - -- for code that somehow depends on the value of v, but - -- that seems acceptable for now. - v = 28 - encoded = encodeAbiValue $ - AbiTuple (RegularVector.fromList - [ AbiUInt 8 v - , AbiBytes 32 (word256Bytes . fromInteger $ sign_r s) - , AbiBytes 32 (word256Bytes . fromInteger $ sign_s s) - ]) - assign (state . returndata) (ConcreteBuf encoded) - copyBytesToMemory (ConcreteBuf encoded) (Lit . num . BS.length $ encoded) (Lit 0) outOffset + forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> do + let (v,r,s) = EVM.Sign.sign hash' (toInteger sk') + encoded = encodeAbiValue $ + AbiTuple (RegularVector.fromList + [ AbiUInt 8 $ num v + , AbiBytes 32 (word256Bytes r) + , AbiBytes 32 (word256Bytes s) + ]) + assign (state . returndata) (ConcreteBuf encoded) + copyBytesToMemory (ConcreteBuf encoded) (Lit . num . BS.length $ encoded) (Lit 0) outOffset _ -> vmError (BadCheatCode sig), action "addr(uint256)" $ \sig outOffset _ input -> case decodeStaticArgs 0 1 input of - [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> let - curve = getCurveByName SEC_p256k1 - pubPoint = generateQ curve (num sk') - encodeInt = encodeAbiValue . AbiUInt 256 . fromInteger - in do - case pubPoint of - PointO -> do vmError (BadCheatCode sig) - Point x y -> do - -- See yellow paper #286 - let - pub = BS.concat [ encodeInt x, encodeInt y ] - addr = Lit . W256 . word256 . BS.drop 12 . BS.take 32 . keccakBytes $ pub - assign (state . returndata . word256At (Lit 0)) addr - assign (state . memory . word256At outOffset) addr + [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> do + let a = EVM.Sign.deriveAddr $ num sk' + case a of + Nothing -> vmError (BadCheatCode sig) + Just address -> do + let expAddr = litAddr address + assign (state . returndata . word256At (Lit 0)) expAddr + assign (state . memory . word256At outOffset) expAddr _ -> vmError (BadCheatCode sig), action "prank(address)" $ @@ -2422,14 +2319,14 @@ -- * Memory helpers accessUnboundedMemoryRange - :: FeeSchedule Word64 - -> Word64 + :: Word64 -> Word64 -> EVM () -> EVM () -accessUnboundedMemoryRange _ _ 0 continue = continue -accessUnboundedMemoryRange fees f l continue = do +accessUnboundedMemoryRange _ 0 continue = continue +accessUnboundedMemoryRange f l continue = do m0 <- num <$> use (state . memorySize) + fees <- gets (._block._schedule) do let m1 = 32 * ceilDiv (max m0 (f + l)) 32 burn (memoryCost fees m1 - memoryCost fees m0) $ do @@ -2437,23 +2334,22 @@ continue accessMemoryRange - :: FeeSchedule Word64 - -> W256 + :: W256 -> W256 -> EVM () -> EVM () -accessMemoryRange _ _ 0 continue = continue -accessMemoryRange fees f l continue = +accessMemoryRange _ 0 continue = continue +accessMemoryRange f l continue = case (,) <$> toWord64 f <*> toWord64 l of Nothing -> vmError IllegalOverflow Just (f64, l64) -> if f64 + l64 < l64 then vmError IllegalOverflow - else accessUnboundedMemoryRange fees f64 l64 continue + else accessUnboundedMemoryRange f64 l64 continue accessMemoryWord - :: FeeSchedule Word64 -> W256 -> EVM () -> EVM () -accessMemoryWord fees x = accessMemoryRange fees x 32 + :: W256 -> EVM () -> EVM () +accessMemoryWord x = accessMemoryRange x 32 copyBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM () @@ -2535,13 +2431,13 @@ stackOp1 :: (?op :: Word8) - => ((Expr EWord) -> Word64) + => Word64 -> ((Expr EWord) -> (Expr EWord)) -> EVM () stackOp1 cost f = use (state . stack) >>= \case (x:xs) -> - burn (cost x) $ do + burn cost $ do next let !y = f x state . stack .= y : xs @@ -2550,13 +2446,13 @@ stackOp2 :: (?op :: Word8) - => (((Expr EWord), (Expr EWord)) -> Word64) + => Word64 -> (((Expr EWord), (Expr EWord)) -> (Expr EWord)) -> EVM () stackOp2 cost f = use (state . stack) >>= \case (x:y:xs) -> - burn (cost (x, y)) $ do + burn cost $ do next state . stack .= f (x, y) : xs _ -> @@ -2564,13 +2460,13 @@ stackOp3 :: (?op :: Word8) - => (((Expr EWord), (Expr EWord), (Expr EWord)) -> Word64) + => Word64 -> (((Expr EWord), (Expr EWord), (Expr EWord)) -> (Expr EWord)) -> EVM () stackOp3 cost f = use (state . stack) >>= \case (x:y:z:xs) -> - burn (cost (x, y, z)) $ do + burn cost $ do next state . stack .= f (x, y, z) : xs _ -> @@ -2692,89 +2588,6 @@ if length (vm ^. state . stack) >= length xs then Map.fromList (zip xs (vm ^. state . stack)) else mempty - --- | Reads -readOp :: Word8 -> [Expr Byte] -> Op -readOp x _ | x >= 0x80 && x <= 0x8f = OpDup (x - 0x80 + 1) -readOp x _ | x >= 0x90 && x <= 0x9f = OpSwap (x - 0x90 + 1) -readOp x _ | x >= 0xa0 && x <= 0xa4 = OpLog (x - 0xa0) -readOp x xs | x >= 0x60 && x <= 0x7f = - let n = num $ x - 0x60 + 1 - in OpPush (readBytes n (Lit 0) (Expr.fromList $ V.fromList xs)) -readOp x _ = case x of - 0x00 -> OpStop - 0x01 -> OpAdd - 0x02 -> OpMul - 0x03 -> OpSub - 0x04 -> OpDiv - 0x05 -> OpSdiv - 0x06 -> OpMod - 0x07 -> OpSmod - 0x08 -> OpAddmod - 0x09 -> OpMulmod - 0x0a -> OpExp - 0x0b -> OpSignextend - 0x10 -> OpLt - 0x11 -> OpGt - 0x12 -> OpSlt - 0x13 -> OpSgt - 0x14 -> OpEq - 0x15 -> OpIszero - 0x16 -> OpAnd - 0x17 -> OpOr - 0x18 -> OpXor - 0x19 -> OpNot - 0x1a -> OpByte - 0x1b -> OpShl - 0x1c -> OpShr - 0x1d -> OpSar - 0x20 -> OpSha3 - 0x30 -> OpAddress - 0x31 -> OpBalance - 0x32 -> OpOrigin - 0x33 -> OpCaller - 0x34 -> OpCallvalue - 0x35 -> OpCalldataload - 0x36 -> OpCalldatasize - 0x37 -> OpCalldatacopy - 0x38 -> OpCodesize - 0x39 -> OpCodecopy - 0x3a -> OpGasprice - 0x3b -> OpExtcodesize - 0x3c -> OpExtcodecopy - 0x3d -> OpReturndatasize - 0x3e -> OpReturndatacopy - 0x3f -> OpExtcodehash - 0x40 -> OpBlockhash - 0x41 -> OpCoinbase - 0x42 -> OpTimestamp - 0x43 -> OpNumber - 0x44 -> OpPrevRandao - 0x45 -> OpGaslimit - 0x46 -> OpChainid - 0x47 -> OpSelfbalance - 0x50 -> OpPop - 0x51 -> OpMload - 0x52 -> OpMstore - 0x53 -> OpMstore8 - 0x54 -> OpSload - 0x55 -> OpSstore - 0x56 -> OpJump - 0x57 -> OpJumpi - 0x58 -> OpPc - 0x59 -> OpMsize - 0x5a -> OpGas - 0x5b -> OpJumpdest - 0xf0 -> OpCreate - 0xf1 -> OpCall - 0xf2 -> OpCallcode - 0xf3 -> OpReturn - 0xf4 -> OpDelegatecall - 0xf5 -> OpCreate2 - 0xfd -> OpRevert - 0xfa -> OpStaticcall - 0xff -> OpSelfdestruct - _ -> OpUnknown x -- Maps operation indicies into a pair of (bytecode index, operation) mkCodeOps :: ContractCode -> RegularVector.Vector (Int, Op) diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs --- a/src/EVM/ABI.hs +++ b/src/EVM/ABI.hs @@ -101,6 +101,7 @@ | AbiArrayDynamic AbiType (Vector AbiValue) | AbiArray Int AbiType (Vector AbiValue) | AbiTuple (Vector AbiValue) + | AbiFunction BS.ByteString deriving (Read, Eq, Ord, Generic) -- | Pretty-print some 'AbiValue'. @@ -118,6 +119,7 @@ "[" ++ intercalate ", " (show <$> Vector.toList v) ++ "]" show (AbiTuple v) = "(" ++ intercalate ", " (show <$> Vector.toList v) ++ ")" + show (AbiFunction b) = show (ByteStringS b) formatString :: ByteString -> String formatString bs = @@ -136,6 +138,7 @@ | AbiArrayDynamicType AbiType | AbiArrayType Int AbiType | AbiTupleType (Vector AbiType) + | AbiFunctionType deriving (Read, Eq, Ord, Generic) instance Show AbiType where @@ -174,6 +177,7 @@ AbiArrayDynamic t _ -> AbiArrayDynamicType t AbiArray n t _ -> AbiArrayType n t AbiTuple v -> AbiTupleType (abiValueType <$> v) + AbiFunction _ -> AbiFunctionType abiTypeSolidity :: AbiType -> Text abiTypeSolidity = \case @@ -187,6 +191,7 @@ AbiArrayDynamicType t -> abiTypeSolidity t <> "[]" AbiArrayType n t -> abiTypeSolidity t <> "[" <> pack (show n) <> "]" AbiTupleType ts -> "(" <> (Text.intercalate "," . Vector.toList $ abiTypeSolidity <$> ts) <> ")" + AbiFunctionType -> "function" getAbi :: AbiType -> Get AbiValue getAbi t = label (Text.unpack (abiTypeSolidity t)) $ @@ -224,6 +229,9 @@ AbiTupleType ts -> AbiTuple <$> getAbiSeq (Vector.length ts) (Vector.toList ts) + AbiFunctionType -> + AbiFunction <$> getBytesWith256BitPadding (24 :: Int) + putAbi :: AbiValue -> Put putAbi = \case AbiUInt _ x -> @@ -256,6 +264,9 @@ AbiTuple v -> putAbiSeq v + AbiFunction b -> do + putAbi (AbiBytes 24 b) + -- | Decode a sequence type (e.g. tuple / array). Will fail for non sequence types getAbiSeq :: Int -> [AbiType] -> Get (Vector AbiValue) getAbiSeq n ts = label "sequence" $ do @@ -308,6 +319,7 @@ AbiBool _ -> 32 AbiTuple v -> sum (abiHeadSize <$> v) AbiArray _ _ xs -> sum (abiHeadSize <$> xs) + AbiFunction _ -> 32 _ -> error "impossible" putAbiSeq :: Vector AbiValue -> Put @@ -370,6 +382,7 @@ , P.string "bytes" $> AbiBytesDynamicType , P.string "tuple" $> AbiTupleType v + , P.string "function" $> AbiFunctionType ] where @@ -430,6 +443,9 @@ replicateM n (scale (`div` 2) (genAbiValue t)) AbiTupleType ts -> AbiTuple <$> mapM genAbiValue ts + AbiFunctionType -> + do xs <- replicateM 24 arbitrary + pure (AbiFunction (BS.pack xs)) where genUInt :: Int -> Gen Word256 genUInt n = arbitraryIntegralWithMax (2^n-1) :: Gen Word256 @@ -471,6 +487,7 @@ AbiBool b -> AbiBool <$> shrink b AbiAddress a -> [AbiAddress 0xacab, AbiAddress 0xdeadbeef, AbiAddress 0xbabeface] <> (AbiAddress <$> shrinkIntegral a) + AbiFunction b -> shrink $ AbiBytes 24 b -- Bool synonym with custom read instance @@ -516,6 +533,8 @@ AbiArray n typ <$> do a <- listP (parseAbiValue typ) return $ Vector.fromList a parseAbiValue (AbiTupleType _) = error "tuple types not supported" +parseAbiValue AbiFunctionType = AbiFunction <$> do ByteStringS bytes <- bytesP + return bytes listP :: ReadP a -> ReadP [a] listP parser = between (char '[') (char ']') ((do skipSpaces @@ -527,7 +546,7 @@ bytesP = do _ <- string "0x" hex <- munch isHexDigit - case BS16.decode (encodeUtf8 (Text.pack hex)) of + case BS16.decodeBase16 (encodeUtf8 (Text.pack hex)) of Right d -> pure $ ByteStringS d Left _ -> pfail diff --git a/src/EVM/Assembler.hs b/src/EVM/Assembler.hs new file mode 100644 --- /dev/null +++ b/src/EVM/Assembler.hs @@ -0,0 +1,109 @@ +{-| +Module : Assembler +Description : Assembler for EVM opcodes used in the HEVM symbolic checker +-} + +{-# LANGUAGE DataKinds #-} + +module EVM.Assembler where + +import EVM.Op +import EVM.Types +import qualified EVM.Expr as Expr + +import qualified Data.Vector as V +import Data.Vector (Vector) + +assemble :: [Op] -> Vector (Expr Byte) +assemble os = V.fromList $ concatMap go os + where + go :: Op -> [Expr Byte] + go = \case + OpStop -> [LitByte 0x00] + OpAdd -> [LitByte 0x01] + OpMul -> [LitByte 0x02] + OpSub -> [LitByte 0x03] + OpDiv -> [LitByte 0x04] + OpSdiv -> [LitByte 0x05] + OpMod -> [LitByte 0x06] + OpSmod -> [LitByte 0x07] + OpAddmod -> [LitByte 0x08] + OpMulmod -> [LitByte 0x09] + OpExp -> [LitByte 0x0A] + OpSignextend -> [LitByte 0x0B] + OpLt -> [LitByte 0x10] + OpGt -> [LitByte 0x11] + OpSlt -> [LitByte 0x12] + OpSgt -> [LitByte 0x13] + OpEq -> [LitByte 0x14] + OpIszero -> [LitByte 0x15] + OpAnd -> [LitByte 0x16] + OpOr -> [LitByte 0x17] + OpXor -> [LitByte 0x18] + OpNot -> [LitByte 0x19] + OpByte -> [LitByte 0x1A] + OpShl -> [LitByte 0x1B] + OpShr -> [LitByte 0x1C] + OpSar -> [LitByte 0x1D] + OpSha3 -> [LitByte 0x20] + OpAddress -> [LitByte 0x30] + OpBalance -> [LitByte 0x31] + OpOrigin -> [LitByte 0x32] + OpCaller -> [LitByte 0x33] + OpCallvalue -> [LitByte 0x34] + OpCalldataload -> [LitByte 0x35] + OpCalldatasize -> [LitByte 0x36] + OpCalldatacopy -> [LitByte 0x37] + OpCodesize -> [LitByte 0x38] + OpCodecopy -> [LitByte 0x39] + OpGasprice -> [LitByte 0x3A] + OpExtcodesize -> [LitByte 0x3B] + OpExtcodecopy -> [LitByte 0x3C] + OpReturndatasize -> [LitByte 0x3D] + OpReturndatacopy -> [LitByte 0x3E] + OpExtcodehash -> [LitByte 0x3F] + OpBlockhash -> [LitByte 0x40] + OpCoinbase -> [LitByte 0x41] + OpTimestamp -> [LitByte 0x42] + OpNumber -> [LitByte 0x43] + OpPrevRandao -> [LitByte 0x44] + OpGaslimit -> [LitByte 0x45] + OpChainid -> [LitByte 0x46] + OpSelfbalance -> [LitByte 0x47] + OpBaseFee -> [LitByte 0x48] + OpPop -> [LitByte 0x50] + OpMload -> [LitByte 0x51] + OpMstore -> [LitByte 0x52] + OpMstore8 -> [LitByte 0x53] + OpSload -> [LitByte 0x54] + OpSstore -> [LitByte 0x55] + OpJump -> [LitByte 0x56] + OpJumpi -> [LitByte 0x57] + OpPc -> [LitByte 0x58] + OpMsize -> [LitByte 0x59] + OpGas -> [LitByte 0x5A] + OpJumpdest -> [LitByte 0x5B] + OpCreate -> [LitByte 0xF0] + OpCall -> [LitByte 0xF1] + OpStaticcall -> [LitByte 0xFA] + OpCallcode -> [LitByte 0xF2] + OpReturn -> [LitByte 0xF3] + OpDelegatecall -> [LitByte 0xF4] + OpCreate2 -> [LitByte 0xF5] + OpRevert -> [LitByte 0xFD] + OpSelfdestruct -> [LitByte 0xFF] + OpDup n -> + if 1 <= n && n <= 16 + then [LitByte (0x80 + (n - 1))] + else error $ "Internal Error: invalid argument to OpDup: " <> show n + OpSwap n -> + if 1 <= n && n <= 16 + then [LitByte (0x90 + (n - 1))] + else error $ "Internal Error: invalid argument to OpSwap: " <> show n + OpLog n -> + if 0 <= n && n <= 4 + then [LitByte (0xA0 + n)] + else error $ "Internal Error: invalid argument to OpLog: " <> show n + -- we just always assemble OpPush into PUSH32 + OpPush wrd -> (LitByte 0x7f) : [Expr.indexWord (Lit i) wrd | i <- [0..31]] + OpUnknown o -> [LitByte o] diff --git a/src/EVM/Concrete.hs b/src/EVM/Concrete.hs --- a/src/EVM/Concrete.hs +++ b/src/EVM/Concrete.hs @@ -1,5 +1,3 @@ -{-# Language StrictData #-} - module EVM.Concrete where import Prelude hiding (Word) diff --git a/src/EVM/Debug.hs b/src/EVM/Debug.hs --- a/src/EVM/Debug.hs +++ b/src/EVM/Debug.hs @@ -1,3 +1,5 @@ +{-# Language DataKinds #-} + module EVM.Debug where import EVM (Contract, nonce, balance, bytecode, codehash) diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -25,6 +25,7 @@ import qualified Data.Vector as V import qualified Data.Vector.Storable as VS import Data.Vector.Storable.ByteString +import Data.Semigroup (Any, Any(..), getAny) -- ** Stack Ops ** --------------------------------------------------------------------------------- @@ -136,7 +137,7 @@ in if sx < sy then 1 else 0) sgt :: Expr EWord -> Expr EWord -> Expr EWord -sgt = op2 SLT (\x y -> +sgt = op2 SGT (\x y -> let sx, sy :: Int256 sx = fromIntegral x sy = fromIntegral y @@ -224,11 +225,9 @@ then readByte (Lit $ x - (dstOffset - srcOffset)) src else readByte i dst readByte i@(Lit x) buf@(CopySlice _ (Lit dstOffset) (Lit size) _ dst) - = if x < dstOffset || x >= dstOffset + size - then readByte i dst - else ReadByte (Lit x) buf -readByte i@(Lit x) buf@(CopySlice _ (Lit dstOffset) _ _ dst) - = if x < dstOffset + -- the byte we are trying to read is compeletely outside of the sliced reegion + -- we check that there is no overflow and that addresses do not wrap around + = if (x < dstOffset || x >= dstOffset + size) && (dstOffset <= dstOffset + size) then readByte i dst else ReadByte (Lit x) buf @@ -262,7 +261,8 @@ -- the region we are trying to read is enclosed in the sliced region | idx >= dstOff && idx + 32 <= dstOff + size = readWord (Lit $ srcOff + (idx - dstOff)) src -- the region we are trying to read is compeletely outside of the sliced reegion - | idx >= dstOff + size || idx + 32 <= dstOff = readWord (Lit idx) dst + -- we check that there is no overflow and that addresses do not wrap around + | (idx >= dstOff + size || idx + 32 <= dstOff) && (dstOff<= dstOff + size) = readWord (Lit idx) dst -- the region we are trying to read partially overlaps the sliced region | otherwise = readWordFromBytes (Lit idx) b readWord i b = readWordFromBytes i b @@ -403,17 +403,24 @@ -- If there are any writes to abstract locations, or CopySlices with an -- abstract size or dstOffset, an abstract expresion will be returned. bufLength :: Expr Buf -> Expr EWord -bufLength buf = case go 0 buf of - Just len -> len - Nothing -> BufLength buf +bufLength = bufLengthEnv mempty False + +bufLengthEnv :: Map.Map Int (Expr Buf) -> Bool -> Expr Buf -> Expr EWord +bufLengthEnv env useEnv buf = go (Lit 0) buf where - go :: W256 -> Expr Buf -> Maybe (Expr EWord) - go l (ConcreteBuf b) = Just . Lit $ max (num . BS.length $ b) l - go l (WriteWord (Lit idx) _ b) = go (max l (idx + 32)) b - go l (WriteByte (Lit idx) _ b) = go (max l (idx + 1)) b - go l (CopySlice _ (Lit dstOffset) (Lit size) _ dst) = go (max (dstOffset + size) l) dst - go _ _ = Nothing + go :: Expr EWord -> Expr Buf -> Expr EWord + go l (ConcreteBuf b) = EVM.Expr.max l (Lit (num . BS.length $ b)) + go l (AbstractBuf b) = Max l (BufLength (AbstractBuf b)) + go l (WriteWord idx _ b) = go (EVM.Expr.max l (add idx (Lit 32))) b + go l (WriteByte idx _ b) = go (EVM.Expr.max l (add idx (Lit 1))) b + go l (CopySlice _ dstOffset size _ dst) = go (EVM.Expr.max l (add dstOffset size)) dst + go l (GVar (BufVar a)) | useEnv = + case Map.lookup a env of + Just b -> go l b + Nothing -> error "Internal error: cannot compute length of open expression" + go l (GVar (BufVar a)) = EVM.Expr.max l (BufLength (GVar (BufVar a))) + -- | If a buffer has a concrete prefix, we return it's length here concPrefix :: Expr Buf -> Maybe Integer concPrefix (CopySlice (Lit srcOff) (Lit _) (Lit _) src (ConcreteBuf "")) = do @@ -423,22 +430,44 @@ go :: W256 -> Expr Buf -> Maybe Integer -- base cases go _ (AbstractBuf _) = Nothing - go l (ConcreteBuf b) = Just . num $ max (num . BS.length $ b) l + go l (ConcreteBuf b) = Just . num $ Prelude.max (num . BS.length $ b) l -- writes to a concrete index - go l (WriteWord (Lit idx) (Lit _) b) = go (max l (idx + 32)) b - go l (WriteByte (Lit idx) (LitByte _) b) = go (max l (idx + 1)) b - go l (CopySlice _ (Lit dstOffset) (Lit size) _ dst) = go (max (dstOffset + size) l) dst + go l (WriteWord (Lit idx) (Lit _) b) = go (Prelude.max l (idx + 32)) b + go l (WriteByte (Lit idx) (LitByte _) b) = go (Prelude.max l (idx + 1)) b + go l (CopySlice _ (Lit dstOffset) (Lit size) _ dst) = go (Prelude.max (dstOffset + size) l) dst -- writes to an abstract index are ignored go l (WriteWord _ _ b) = go l b go l (WriteByte _ _ b) = go l b go _ (CopySlice _ _ _ _ _) = error "Internal Error: cannot compute a concrete prefix length for nested copySlice expressions" - go _ (GVar _) = error "Internal error: cannot calculate minLength of an open expression" + go _ (GVar _) = error "Internal error: cannot calculate a concrete prefix of an open expression" concPrefix (ConcreteBuf b) = Just (num . BS.length $ b) concPrefix e = error $ "Internal error: cannot compute a concrete prefix length for: " <> show e +-- | Return the minimum possible length of a buffer. In the case of an +-- abstract buffer, it is the largest write that is made on a concrete +-- location. Parameterized by an environment for buffer variables. +minLength :: Map.Map Int (Expr Buf) -> Expr Buf -> Maybe Integer +minLength bufEnv = go 0 + where + go :: W256 -> Expr Buf -> Maybe Integer + -- base cases + go l (AbstractBuf _) = if l == 0 then Nothing else Just $ num l + go l (ConcreteBuf b) = Just . num $ Prelude.max (num . BS.length $ b) l + -- writes to a concrete index + go l (WriteWord (Lit idx) _ b) = go (Prelude.max l (idx + 32)) b + go l (WriteByte (Lit idx) _ b) = go (Prelude.max l (idx + 1)) b + go l (CopySlice _ (Lit dstOffset) (Lit size) _ dst) = go (Prelude.max (dstOffset + size) l) dst + -- writes to an abstract index are ignored + go l (WriteWord _ _ b) = go l b + go l (WriteByte _ _ b) = go l b + go l (CopySlice _ _ _ _ b) = go l b + go l (GVar (BufVar a)) = do + b <- Map.lookup a bufEnv + go l b + word256At :: Functor f => Expr EWord -> (Expr EWord -> f (Expr EWord)) @@ -763,6 +792,9 @@ -- Double NOT is a no-op, since it's a bitwise inversion go (EVM.Types.Not (EVM.Types.Not a)) = a + go (Max (Lit 0) a) = a + go (Min (Lit 0) _) = Lit 0 + go a = a @@ -772,6 +804,10 @@ litAddr :: Addr -> Expr EWord litAddr = Lit . num +exprToAddr :: Expr EWord -> Maybe Addr +exprToAddr (Lit x) = Just (num x) +exprToAddr _ = Nothing + litCode :: BS.ByteString -> [Expr Byte] litCode bs = fmap LitByte (BS.unpack bs) @@ -927,12 +963,23 @@ eqByte x y = EqByte x y min :: Expr EWord -> Expr EWord -> Expr EWord -min (Lit x) (Lit y) = if x < y then Lit x else Lit y -min x y = Min x y +min x y = normArgs Min Prelude.min x y +max :: Expr EWord -> Expr EWord -> Expr EWord +max x y = normArgs Max Prelude.max x y + numBranches :: Expr End -> Int numBranches (ITE _ t f) = numBranches t + numBranches f numBranches _ = 1 allLit :: [Expr Byte] -> Bool allLit = Data.List.and . fmap (isLitByte) + +-- | True if the given expression contains any node that satisfies the +-- input predicate +containsNode :: (forall a. Expr a -> Bool) -> Expr b -> Bool +containsNode p = getAny . foldExpr go (Any False) + where + go :: Expr a -> Any + go node | p node = Any True + go _ = Any False diff --git a/src/EVM/Facts.hs b/src/EVM/Facts.hs --- a/src/EVM/Facts.hs +++ b/src/EVM/Facts.hs @@ -102,9 +102,9 @@ load = readMaybe . Char8.unpack instance AsASCII ByteString where - dump x = BS16.encode x <> "\n" + dump x = BS16.encodeBase16' x <> "\n" load x = - case BS16.decode . mconcat . BS.split 10 $ x of + case BS16.decodeBase16 . mconcat . BS.split 10 $ x of Right y -> Just y _ -> Nothing diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs --- a/src/EVM/Format.hs +++ b/src/EVM/Format.hs @@ -27,16 +27,16 @@ import Prelude hiding (Word) import EVM qualified -import EVM (VM, cheatCode, traceForest, Error(..), Trace, - TraceData(..), Query(..), FrameContext(..)) -import EVM.ABI (AbiValue (..), Event (..), AbiType (..), SolError(..), - Indexed(NotIndexed), getAbiSeq, parseTypeName, formatString) +import EVM (VM, cheatCode, traceForest, Error (..), Trace, TraceData(..), Query(..), FrameContext(..)) +import EVM.ABI (AbiValue (..), Event (..), AbiType (..), SolError (..), + Indexed (NotIndexed), getAbiSeq, parseTypeName, formatString) import EVM.Dapp (DappContext(..), DappInfo(..), showTraceLocation) import EVM.Expr qualified as Expr import EVM.Hexdump (prettyHex) -import EVM.Solidity (SolcContract(..), Method(..)) -import EVM.Types (maybeLitWord, W256(..), num, word, Expr(..), EType(..), Addr, +import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap) +import EVM.Types (maybeLitWord, W256(..),num, word, Expr(..), EType(..), Addr, ByteStringS(..), Error(..)) + import Control.Arrow ((>>>)) import Control.Lens (preview, ix, _2) import Data.Binary.Get (runGetOrFail) @@ -366,14 +366,14 @@ prettyError :: EVM.Types.Error -> String prettyError= \case - Invalid -> "Invalid Opcode" + EVM.Types.Invalid -> "Invalid Opcode" EVM.Types.IllegalOverflow -> "Illegal Overflow" - SelfDestruct -> "Self Destruct" + EVM.Types.SelfDestruct -> "Self Destruct" EVM.Types.StackLimitExceeded -> "Stack limit exceeded" EVM.Types.InvalidMemoryAccess -> "Invalid memory access" EVM.Types.BadJumpDestination -> "Bad jump destination" EVM.Types.StackUnderrun -> "Stack underrun" - TmpErr err -> "Temp error: " <> err + EVM.Types.TmpErr err -> "Temp error: " <> err prettyvmresult :: (?context :: DappContext) => Expr End -> String diff --git a/src/EVM/Hexdump.hs b/src/EVM/Hexdump.hs --- a/src/EVM/Hexdump.hs +++ b/src/EVM/Hexdump.hs @@ -28,7 +28,7 @@ -- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -- -module EVM.Hexdump (prettyHex, simpleHex) where +module EVM.Hexdump (prettyHex, simpleHex, paddedShowHex) where import Data.ByteString (ByteString) import qualified Data.ByteString as B (length, unpack) diff --git a/src/EVM/Op.hs b/src/EVM/Op.hs --- a/src/EVM/Op.hs +++ b/src/EVM/Op.hs @@ -1,16 +1,24 @@ {-# LANGUAGE DataKinds #-} module EVM.Op - ( Op (..) + ( Op + , GenericOp (..) , opString + , intToOpName + , getOp + , readOp ) where +import EVM.Expr qualified as Expr import EVM.Types +import Data.Vector qualified as V import Data.Word (Word8) import Numeric (showHex) -data Op +type Op = GenericOp (Expr EWord) + +data GenericOp a = OpStop | OpAdd | OpMul @@ -87,10 +95,165 @@ | OpDup !Word8 | OpSwap !Word8 | OpLog !Word8 - | OpPush (Expr EWord) + | OpPush a | OpUnknown Word8 - deriving (Show, Eq) + deriving (Show, Eq, Functor) +intToOpName:: Int -> String +intToOpName a = + case a of + 0x00-> "STOP" + 0x01-> "ADD" + 0x02-> "MUL" + 0x03-> "SUB" + 0x04-> "DIV" + 0x05-> "SDIV" + 0x06-> "MOD" + 0x07-> "SMOD" + 0x08-> "ADDMOD" + 0x09-> "MULMOD" + 0x0a-> "EXP" + 0x0b-> "SIGNEXTEND" + -- + 0x10 -> "LT" + 0x11 -> "GT" + 0x12 -> "SLT" + 0x13 -> "SGT" + 0x14 -> "EQ" + 0x15 -> "ISZERO" + 0x16 -> "AND" + 0x17 -> "OR" + 0x18 -> "XOR" + 0x19 -> "NOT" + 0x1a -> "BYTE" + 0x1b -> "SHL" + 0x1c -> "SHR" + 0x1d -> "SAR" + 0x20 -> "SHA3" + 0x30 -> "ADDRESS" + -- + 0x31 -> "BALANCE" + 0x32 -> "ORIGIN" + 0x33 -> "CALLER" + 0x34 -> "CALLVALUE" + 0x35 -> "CALLDATALOAD" + 0x36 -> "CALLDATASIZE" + 0x37 -> "CALLDATACOPY" + 0x38 -> "CODESIZE" + 0x39 -> "CODECOPY" + 0x3a -> "GASPRICE" + 0x3b -> "EXTCODESIZE" + 0x3c -> "EXTCODECOPY" + 0x3d -> "RETURNDATASIZE" + 0x3e -> "RETURNDATACOPY" + 0x3f -> "EXTCODEHASH" + 0x40 -> "BLOCKHASH" + 0x41 -> "COINBASE" + 0x42 -> "TIMESTAMP" + 0x43 -> "NUMBER" + 0x44 -> "PREVRANDAO" + 0x45 -> "GASLIMIT" + 0x46 -> "CHAINID" + 0x47 -> "SELFBALANCE" + 0x48 -> "BASEFEE" + 0x50 -> "POP" + 0x51 -> "MLOAD" + 0x52 -> "MSTORE" + 0x53 -> "MSTORE8" + 0x54 -> "SLOAD" + 0x55 -> "SSTORE" + 0x56 -> "JUMP" + 0x57 -> "JUMPI" + 0x58 -> "PC" + 0x59 -> "MSIZE" + 0x5a -> "GAS" + 0x5b -> "JUMPDEST" + -- + 0x60 -> "PUSH1" + 0x61 -> "PUSH2" + 0x62 -> "PUSH3" + 0x63 -> "PUSH4" + 0x64 -> "PUSH5" + 0x65 -> "PUSH6" + 0x66 -> "PUSH7" + 0x67 -> "PUSH8" + 0x68 -> "PUSH9" + 0x69 -> "PUSH10" + 0x6a -> "PUSH11" + 0x6b -> "PUSH12" + 0x6c -> "PUSH13" + 0x6d -> "PUSH14" + 0x6e -> "PUSH15" + 0x6f -> "PUSH16" + 0x70 -> "PUSH17" + 0x71 -> "PUSH18" + 0x72 -> "PUSH19" + 0x73 -> "PUSH20" + 0x74 -> "PUSH21" + 0x75 -> "PUSH22" + 0x76 -> "PUSH23" + 0x77 -> "PUSH24" + 0x78 -> "PUSH25" + 0x79 -> "PUSH26" + 0x7a -> "PUSH27" + 0x7b -> "PUSH28" + 0x7c -> "PUSH29" + 0x7d -> "PUSH30" + 0x7e -> "PUSH31" + 0x7f -> "PUSH32" + -- + 0x80 -> "DUP1" + 0x81 -> "DUP2" + 0x82 -> "DUP3" + 0x83 -> "DUP4" + 0x84 -> "DUP5" + 0x85 -> "DUP6" + 0x86 -> "DUP7" + 0x87 -> "DUP8" + 0x88 -> "DUP9" + 0x89 -> "DUP10" + 0x8a -> "DUP11" + 0x8b -> "DUP12" + 0x8c -> "DUP13" + 0x8d -> "DUP14" + 0x8e -> "DUP15" + 0x8f -> "DUP16" + -- + 0x90 -> "SWAP1" + 0x91 -> "SWAP2" + 0x92 -> "SWAP3" + 0x93 -> "SWAP4" + 0x94 -> "SWAP5" + 0x95 -> "SWAP6" + 0x96 -> "SWAP7" + 0x97 -> "SWAP8" + 0x98 -> "SWAP9" + 0x99 -> "SWAP10" + 0x9a -> "SWAP11" + 0x9b -> "SWAP12" + 0x9c -> "SWAP13" + 0x9d -> "SWAP14" + 0x9e -> "SWAP15" + 0x9f -> "SWAP16" + -- + 0xa0 -> "LOG0" + 0xa1 -> "LOG1" + 0xa2 -> "LOG2" + 0xa3 -> "LOG3" + 0xa4 -> "LOG4" + -- + 0xf0 -> "CREATE" + 0xf1 -> "CALL" + 0xf2 -> "CALLCODE" + 0xf3 -> "RETURN" + 0xf4 -> "DELEGATECALL" + 0xf5 -> "CREATE2" + 0xfa -> "STATICCALL" + 0xfd -> "REVERT" + 0xfe -> "INVALID" + 0xff -> "SELFDESTRUCT" + _ -> "UNKNOWN " + opString :: (Integral a, Show a) => (a, Op) -> String opString (i, o) = let showPc x | x < 0x10 = '0' : showHex x "" | otherwise = showHex x "" @@ -177,3 +340,88 @@ OpUnknown x -> case x of 254 -> "INVALID" _ -> "UNKNOWN " ++ (showHex x "") + +readOp :: Word8 -> [Expr Byte] -> Op +readOp x xs = + (\n -> Expr.readBytes (fromIntegral n) (Lit 0) (Expr.fromList $ V.fromList xs)) <$> getOp x + +getOp :: Word8 -> GenericOp Word8 +getOp x | x >= 0x80 && x <= 0x8f = OpDup (x - 0x80 + 1) +getOp x | x >= 0x90 && x <= 0x9f = OpSwap (x - 0x90 + 1) +getOp x | x >= 0xa0 && x <= 0xa4 = OpLog (x - 0xa0) +getOp x | x >= 0x60 && x <= 0x7f = OpPush (x - 0x60 + 1) +getOp x = case x of + 0x00 -> OpStop + 0x01 -> OpAdd + 0x02 -> OpMul + 0x03 -> OpSub + 0x04 -> OpDiv + 0x05 -> OpSdiv + 0x06 -> OpMod + 0x07 -> OpSmod + 0x08 -> OpAddmod + 0x09 -> OpMulmod + 0x0a -> OpExp + 0x0b -> OpSignextend + 0x10 -> OpLt + 0x11 -> OpGt + 0x12 -> OpSlt + 0x13 -> OpSgt + 0x14 -> OpEq + 0x15 -> OpIszero + 0x16 -> OpAnd + 0x17 -> OpOr + 0x18 -> OpXor + 0x19 -> OpNot + 0x1a -> OpByte + 0x1b -> OpShl + 0x1c -> OpShr + 0x1d -> OpSar + 0x20 -> OpSha3 + 0x30 -> OpAddress + 0x31 -> OpBalance + 0x32 -> OpOrigin + 0x33 -> OpCaller + 0x34 -> OpCallvalue + 0x35 -> OpCalldataload + 0x36 -> OpCalldatasize + 0x37 -> OpCalldatacopy + 0x38 -> OpCodesize + 0x39 -> OpCodecopy + 0x3a -> OpGasprice + 0x3b -> OpExtcodesize + 0x3c -> OpExtcodecopy + 0x3d -> OpReturndatasize + 0x3e -> OpReturndatacopy + 0x3f -> OpExtcodehash + 0x40 -> OpBlockhash + 0x41 -> OpCoinbase + 0x42 -> OpTimestamp + 0x43 -> OpNumber + 0x44 -> OpPrevRandao + 0x45 -> OpGaslimit + 0x46 -> OpChainid + 0x47 -> OpSelfbalance + 0x48 -> OpBaseFee + 0x50 -> OpPop + 0x51 -> OpMload + 0x52 -> OpMstore + 0x53 -> OpMstore8 + 0x54 -> OpSload + 0x55 -> OpSstore + 0x56 -> OpJump + 0x57 -> OpJumpi + 0x58 -> OpPc + 0x59 -> OpMsize + 0x5a -> OpGas + 0x5b -> OpJumpdest + 0xf0 -> OpCreate + 0xf1 -> OpCall + 0xf2 -> OpCallcode + 0xf3 -> OpReturn + 0xf4 -> OpDelegatecall + 0xf5 -> OpCreate2 + 0xfd -> OpRevert + 0xfa -> OpStaticcall + 0xff -> OpSelfdestruct + _ -> OpUnknown x diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -34,20 +34,22 @@ import qualified Data.Text.Lazy as T import Data.Text.Lazy.Builder import Data.Bifunctor (second) -import Data.Semigroup (Any, Any(..), getAny) import EVM.Types import EVM.Traversals import EVM.CSE import EVM.Keccak -import EVM.Expr hiding (copySlice, writeWord, op1, op2, op3, drop) +import EVM.Expr (writeByte, bufLengthEnv, containsNode, bufLength, minLength) +import qualified EVM.Expr as Expr -- ** Encoding ** ---------------------------------------------------------------------------------- + + -- variable names in SMT that we want to get values for data CexVars = CexVars { calldataV :: [Text] - , buffersV :: [Text] + , buffersV :: Map Text (Expr EWord) -- buffers and guesses at their maximum size , storeReads :: [(Expr EWord, Expr EWord)] -- a list of relevant store reads , blockContextV :: [Text] , txContextV :: [Text] @@ -66,16 +68,49 @@ , txContextV = mempty } +-- | A model for a buffer, either in it's compressed form (for storing parsed +-- models from a solver), or as a bytestring (for presentation to users) +data BufModel + = Comp CompressedBuf + | Flat ByteString + deriving (Eq, Show) + +-- | This representation lets us store buffers of arbitrary length without +-- exhausting the available memory, it closely matches the format used by +-- smt-lib when returning models for arrays +data CompressedBuf + = Base { byte :: Word8, length :: W256} + | Write { byte :: Word8, idx :: W256, next :: CompressedBuf } + deriving (Eq, Show) + + +-- | a final post shrinking cex, buffers here are all represented as concrete bytestrings data SMTCex = SMTCex { vars :: Map (Expr EWord) W256 - , buffers :: Map (Expr Buf) ByteString + , buffers :: Map (Expr Buf) BufModel , store :: Map W256 (Map W256 W256) , blockContext :: Map (Expr EWord) W256 , txContext :: Map (Expr EWord) W256 } deriving (Eq, Show) -getVar :: EVM.SMT.SMTCex -> TS.Text -> W256 +flattenBufs :: SMTCex -> Maybe SMTCex +flattenBufs cex = do + bs <- mapM collapse cex.buffers + pure $ cex { buffers = bs} + +-- | Attemps to collapse a compressed buffer representation down to a flattened one +collapse :: BufModel -> Maybe BufModel +collapse model = case toBuf model of + Just (ConcreteBuf b) -> Just $ Flat b + _ -> Nothing + where + toBuf (Comp (Base b sz)) | sz <= 120_000_000 = Just . ConcreteBuf $ BS.replicate (num sz) b + toBuf (Comp (Write b idx next)) = fmap (writeByte (Lit idx) (LitByte b)) (toBuf $ Comp next) + toBuf (Flat b) = Just . ConcreteBuf $ b + toBuf _ = Nothing + +getVar :: SMTCex -> TS.Text -> W256 getVar cex name = fromJust $ Map.lookup (Var name) cex.vars data SMT2 = SMT2 [Builder] CexVars @@ -101,16 +136,18 @@ where compareFst (l, _) (r, _) = compare l r encodeBuf n expr = - fromLazyText ("(define-const buf" <> (T.pack . show $ n) <> " Buf ") <> exprToSMT expr <> ")" + "(define-const buf" <> (fromString . show $ n) <> " Buf " <> exprToSMT expr <> ")\n" <> encodeBufLen n expr + encodeBufLen n expr = + "(define-const buf" <> (fromString . show $ n) <>"_length" <> " (_ BitVec 256) " <> exprToSMT (bufLengthEnv bufs True expr) <> ")" encodeStore n expr = - fromLazyText ("(define-const store" <> (T.pack . show $ n) <> " Storage ") <> exprToSMT expr <> ")" + "(define-const store" <> (fromString . show $ n) <> " Storage " <> exprToSMT expr <> ")" assertProps :: [Prop] -> SMT2 assertProps ps = let encs = map propToSMT ps_elim intermediates = declareIntermediates bufs stores in prelude - <> (declareBufs . nubOrd $ foldl (<>) [] allBufs) + <> (declareBufs ps_elim bufs stores) <> SMT2 [""] mempty <> (declareVars . nubOrd $ foldl (<>) [] allVars) <> SMT2 [""] mempty @@ -121,6 +158,7 @@ <> intermediates <> SMT2 [""] mempty <> keccakAssumes + <> readAssumes <> SMT2 [""] mempty <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty <> SMT2 [] mempty{storeReads = storageReads} @@ -128,7 +166,6 @@ where (ps_elim, bufs, stores) = eliminateProps ps - allBufs = fmap referencedBufs' ps_elim <> fmap referencedBufs bufVals <> fmap referencedBufs storeVals allVars = fmap referencedVars' ps_elim <> fmap referencedVars bufVals <> fmap referencedVars storeVals frameCtx = fmap referencedFrameContext' ps_elim <> fmap referencedFrameContext bufVals <> fmap referencedFrameContext storeVals blockCtx = fmap referencedBlockContext' ps_elim <> fmap referencedBlockContext bufVals <> fmap referencedBlockContext storeVals @@ -142,6 +179,9 @@ = SMT2 ["; keccak assumptions"] mempty <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakAssumptions ps_elim bufVals storeVals)) mempty + readAssumes + = SMT2 ["; read assumptions"] mempty + <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (assertReads ps_elim bufs stores)) mempty referencedBufsGo :: Expr a -> [Builder] referencedBufsGo = \case @@ -154,7 +194,6 @@ referencedBufs' :: Prop -> [Builder] referencedBufs' prop = nubOrd $ foldProp referencedBufsGo [] prop - referencedVarsGo :: Expr a -> [Builder] referencedVarsGo = \case Var s -> [fromText s] @@ -166,7 +205,6 @@ referencedVars' :: Prop -> [Builder] referencedVars' prop = nubOrd $ foldProp referencedVarsGo [] prop - referencedFrameContextGo :: Expr a -> [Builder] referencedFrameContextGo = \case CallValue a -> [fromLazyText $ T.append "callvalue_" (T.pack . show $ a)] @@ -202,14 +240,6 @@ referencedBlockContext' :: Prop -> [Builder] referencedBlockContext' prop = nubOrd $ foldProp referencedBlockContextGo [] prop - -isAbstractStorage :: Expr Storage -> Bool -isAbstractStorage = getAny . foldExpr go (Any False) - where - go :: Expr a -> Any - go AbstractStore = Any True - go _ = Any False - -- | This function overapproximates the reads from the abstract -- storage. Potentially, it can return locations that do not read a -- slot directly from the abstract store but from subsequent writes on @@ -221,19 +251,80 @@ where go :: Expr a -> [(Expr EWord, Expr EWord)] go = \case - SLoad addr slot storage -> [(addr, slot) | isAbstractStorage storage] + SLoad addr slot storage -> [(addr, slot) | containsNode isAbstractStore storage] _ -> [] + isAbstractStore AbstractStore = True + isAbstractStore _ = False -declareBufs :: [Builder] -> SMT2 -declareBufs names = SMT2 ("; buffers" : fmap declareBuf names <> ("; buffer lengths" : fmap declareLength names)) cexvars + +findBufferAccess :: TraversableTerm a => [a] -> [(Expr EWord, Expr EWord, Expr Buf)] +findBufferAccess = foldl (foldTerm go) mempty where - declareBuf n = "(declare-const " <> n <> " (Array (_ BitVec 256) (_ BitVec 8)))" - declareLength n = "(define-const " <> n <> "_length" <> " (_ BitVec 256) (bufLength " <> n <> "))" - cexvars = mempty{buffersV = fmap toLazyText names} + go :: Expr a -> [(Expr EWord, Expr EWord, Expr Buf)] + go = \case + ReadWord idx buf -> [(idx, Lit 32, buf)] + ReadByte idx buf -> [(idx, Lit 1, buf)] + CopySlice srcOff _ size src _ -> [(srcOff, size, src)] + _ -> mempty +-- | Asserts that buffer reads beyond the size of the buffer are equal +-- to zero. Looks for buffer reads in the a list of given predicates +-- and the buffer and storage environments. +assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop] +assertReads props benv senv = concatMap assertRead allReads + where + assertRead :: (Expr EWord, Expr EWord, Expr Buf) -> [Prop] + assertRead (idx, Lit 32, buf) = [PImpl (PGEq idx (bufLength buf)) (PEq (ReadWord idx buf) (Lit 0))] + assertRead (idx, Lit sz, buf) = fmap (\s -> PImpl (PGEq idx (bufLength buf)) (PEq (ReadByte idx buf) (LitByte (num s)))) [(0::Int)..num sz-1] + assertRead (_, _, _) = error "Cannot generate assertions for accesses of symbolic size" --- Given a list of 256b VM variable names, create an SMT2 object with the variables declared + allReads = filter keepRead $ nubOrd $ findBufferAccess props <> findBufferAccess (Map.elems benv) <> findBufferAccess (Map.elems senv) + + -- discard constraints if we can statically determine that read is less than the buffer length + keepRead (Lit idx, Lit size, buf) = + case minLength benv buf of + Just l | num (idx + size) <= l -> False + _ -> True + keepRead _ = True + +-- | Finds the maximum read index for each abstract buffer in the input props +discoverMaxReads :: [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr EWord) +discoverMaxReads props benv senv = bufMap + where + allReads = nubOrd $ findBufferAccess props <> findBufferAccess (Map.elems benv) <> findBufferAccess (Map.elems senv) + -- we can have buffers that are not read from but are still mentioned via BufLength in some branch condition + -- we assign a default read hint of 4 to start with in these cases (since in most cases we will need at least 4 bytes to produce a counterexample) + allBufs = Map.fromList . fmap (, Lit 4) . fmap toLazyText . nubOrd . concat $ fmap referencedBufs' props <> fmap referencedBufs (Map.elems benv) <> fmap referencedBufs (Map.elems senv) + + bufMap = Map.unionWith Expr.max (foldl addBound mempty allReads) allBufs + + addBound m (idx, size, buf) = + case baseBuf buf of + AbstractBuf b -> Map.insertWith Expr.max (T.fromStrict b) (Expr.add idx size) m + _ -> m + + baseBuf :: Expr Buf -> Expr Buf + baseBuf (AbstractBuf b) = AbstractBuf b + baseBuf (ConcreteBuf b) = ConcreteBuf b + baseBuf (GVar (BufVar a)) = + case Map.lookup a benv of + Just b -> baseBuf b + Nothing -> error "Internal error: could not find buffer variable" + baseBuf (WriteByte _ _ b) = baseBuf b + baseBuf (WriteWord _ _ b) = baseBuf b + baseBuf (CopySlice _ _ _ _ dst)= baseBuf dst + +-- | Returns an SMT2 object with all buffers referenced from the input props declared, and with the appropriate cex extraction metadata attached +declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2 +declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs <> ("; buffer lengths" : fmap declareLength allBufs)) cexvars + where + cexvars = mempty{buffersV = discoverMaxReads props bufEnv storeEnv} + allBufs = fmap fromLazyText $ Map.keys cexvars.buffersV + declareBuf n = "(declare-const " <> n <> " (Array (_ BitVec 256) (_ BitVec 8)))" + declareLength n = "(declare-const " <> n <> "_length" <> " (_ BitVec 256))" + +-- Given a list of variable names, create an SMT2 object with the variables declared declareVars :: [Builder] -> SMT2 declareVars names = SMT2 (["; variables"] <> fmap declare names) cexvars where @@ -274,6 +365,8 @@ (declare-fun keccak (Buf) Word) (declare-fun sha256 (Buf) Word) + (define-fun max ((a (_ BitVec 256)) (b (_ BitVec 256))) (_ BitVec 256) (ite (bvult a b) b a)) + ; word indexing (define-fun indexWord31 ((w Word)) Byte ((_ extract 7 0) w)) (define-fun indexWord30 ((w Word)) Byte ((_ extract 15 8) w)) @@ -348,7 +441,6 @@ ) ; buffers - (declare-fun bufLength (Buf) Word) (define-const emptyBuf Buf ((as const Buf) #b00000000)) (define-fun readWord ((idx Word) (buf Buf)) Word @@ -499,12 +591,19 @@ let aenc = exprToSMT a benc = exprToSMT b in "(ite (bvule " <> aenc `sp` benc <> ") " <> aenc `sp` benc <> ")" + Max a b -> + let aenc = exprToSMT a + benc = exprToSMT b in + "(max " <> aenc `sp` benc <> ")" LT a b -> let cond = op2 "bvult" a b in "(ite " <> cond `sp` one `sp` zero <> ")" SLT a b -> let cond = op2 "bvslt" a b in "(ite " <> cond `sp` one `sp` zero <> ")" + SGT a b -> + let cond = op2 "bvsgt" a b in + "(ite " <> cond `sp` one `sp` zero <> ")" GT a b -> let cond = op2 "bvugt" a b in "(ite " <> cond `sp` one `sp` zero <> ")" @@ -575,7 +674,6 @@ ChainId -> "chainid" BaseFee -> "basefee" - -- TODO: make me binary... LitByte b -> fromLazyText $ "(_ bv" <> T.pack (show (num b :: Integer)) <> " 8)" IndexWord idx w -> case idx of Lit n -> if n >= 0 && n < 32 @@ -590,7 +688,9 @@ ConcreteBuf bs -> writeBytes bs mempty AbstractBuf s -> fromText s ReadWord idx prev -> op2 "readWord" idx prev - BufLength b -> op1 "bufLength" b + BufLength (AbstractBuf b) -> fromText b <> "_length" + BufLength (GVar (BufVar n)) -> fromLazyText $ "buf" <> (T.pack . show $ n) <> "_length" + BufLength b -> exprToSMT (bufLength b) WriteByte idx val prev -> let encIdx = exprToSMT idx encVal = exprToSMT val @@ -660,6 +760,10 @@ let aenc = propToSMT a benc = propToSMT b in "(or " <> aenc <> " " <> benc <> ")" + PImpl a b -> + let aenc = propToSMT a + benc = propToSMT b in + "(=> " <> aenc <> " " <> benc <> ")" PBool b -> if b then "true" else "false" where op2 op a b = @@ -677,9 +781,9 @@ copySlice srcOffset dstOffset size@(Lit _) src dst | size == (Lit 0) = dst | otherwise = - let size' = (sub size (Lit 1)) - encDstOff = exprToSMT (add dstOffset size') - encSrcOff = exprToSMT (add srcOffset size') + let size' = (Expr.sub size (Lit 1)) + encDstOff = exprToSMT (Expr.add dstOffset size') + encSrcOff = exprToSMT (Expr.add srcOffset size') child = copySlice srcOffset dstOffset size' src dst in "(store " <> child `sp` encDstOff `sp` "(select " <> src `sp` encSrcOff <> "))" copySlice _ _ _ _ _ = error "TODO: implement copySlice with a symbolically sized region" @@ -733,6 +837,7 @@ -- ** Cex parsing ** -------------------------------------------------------------------------------- + parseW256 :: SpecConstant -> W256 parseW256 = parseSC @@ -791,52 +896,44 @@ r -> parseErr r pure $ Map.insert name val acc -getBufs :: (Text -> IO Text) -> [TS.Text] -> IO (Map (Expr Buf) ByteString) -getBufs getVal names = foldM getBuf mempty names +-- | Queries the solver for models for each of the expressions representing the +-- max read index for a given buffer +queryMaxReads :: (Text -> IO Text) -> Map Text (Expr EWord) -> IO (Map Text W256) +queryMaxReads getVal maxReads = mapM (queryValue getVal) maxReads + +-- | Gets the initial model for each buffer, these will often be much too large for our purposes +getBufs :: (Text -> IO Text) -> [Text] -> IO (Map (Expr Buf) BufModel) +getBufs getVal bufs = foldM getBuf mempty bufs where - getLength :: TS.Text -> IO Int + getLength :: Text -> IO W256 getLength name = do - val <- getVal (T.fromStrict name <> "_length") - len <- case parseCommentFreeFileMsg getValueRes (T.toStrict val) of + val <- getVal (name <> "_length ") + pure $ case parseCommentFreeFileMsg getValueRes (T.toStrict val) of Right (ResSpecific (parsed :| [])) -> case parsed of (TermQualIdentifier (Unqualified (IdSymbol symbol)), (TermSpecConstant sc)) - -> if symbol == (name <> "_length") - then pure $ parseW256 sc + -> if symbol == (T.toStrict $ name <> "_length") + then parseW256 sc else error "Internal Error: solver did not return model for requested value" res -> parseErr res res -> parseErr res - pure $ if len <= num (maxBound :: Int) - then fromIntegral len - else error $ "Internal Error: buffer: " - <> (TS.unpack name) - <> " is too large to be represented in a ByteString. Length: " - <> show len - getBuf :: Map (Expr Buf) ByteString -> TS.Text -> IO (Map (Expr Buf) ByteString) + getBuf :: Map (Expr Buf) BufModel -> Text -> IO (Map (Expr Buf) BufModel) getBuf acc name = do - -- Sometimes the solver gives us back a model for a Buffer that has every - -- element set to some concrete value. This is impossible to represent as - -- a concrete ByteString in haskell (or in any existing computer hardware :D), - -- so we ask the solver to give us back a model for the length of - -- this buffer and then use that to produce a shorter counterexample (by - -- replicating the constant byte up to the length). len <- getLength name - val <- getVal (T.fromStrict name) + val <- getVal name + buf <- case parseCommentFreeFileMsg getValueRes (T.toStrict val) of Right (ResSpecific (valParsed :| [])) -> case valParsed of (TermQualIdentifier (Unqualified (IdSymbol symbol)), term) - -> if symbol == name + -> if (T.fromStrict symbol) == name then pure $ parseBuf len term else error "Internal Error: solver did not return model for requested value" res -> error $ "Internal Error: cannot parse solver response: " <> show res res -> error $ "Internal Error: cannot parse solver response: " <> show res - let bs = case simplify buf of - ConcreteBuf b -> b - _ -> error "Internal Error: unable to parse solver response into a concrete buffer" - pure $ Map.insert (AbstractBuf name) bs acc + pure $ Map.insert (AbstractBuf $ T.toStrict name) buf acc - parseBuf :: Int -> Term -> Expr Buf - parseBuf len = go mempty + parseBuf :: W256 -> Term -> BufModel + parseBuf len = Comp . go mempty where go env = \case -- constant arrays @@ -848,8 +945,8 @@ ) )) ((TermSpecConstant val :| []))) -> case val of - SCHexadecimal "00" -> mempty - v -> ConcreteBuf $ BS.replicate len (parseW8 v) + SCHexadecimal "00" -> Base 0 0 + v -> Base (parseW8 v) len -- writing a byte over some array (TermApplication @@ -859,7 +956,7 @@ pbase = go env base pidx = parseW256 idx pval = parseW8 val - in writeByte (Lit pidx) (LitByte pval) pbase + in Write pval pidx pbase -- binding a new name (TermLet ((VarBinding name bound) :| []) term) -> let @@ -890,8 +987,8 @@ -- then create a map by adding only the locations that are read by the program foldM (\m (addr, slot) -> do - addr' <- queryValue addr - slot' <- queryValue slot + addr' <- queryValue getVal addr + slot' <- queryValue getVal slot pure $ addElem addr' slot' m fun) Map.empty sreads where @@ -903,17 +1000,17 @@ Nothing -> Map.insert addr (Map.singleton slot (fun addr slot)) store - queryValue :: Expr EWord -> IO W256 - queryValue (Lit w) = pure w - queryValue w = do - let expr = toLazyText $ exprToSMT w - raw <- getVal expr - case parseCommentFreeFileMsg getValueRes (T.toStrict raw) of - Right (ResSpecific (valParsed :| [])) -> - case valParsed of - (_, TermSpecConstant sc) -> pure $ parseW256 sc - _ -> error "Internal Error: cannot parse model for storage index" - r -> parseErr r +queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256 +queryValue _ (Lit w) = pure w +queryValue getVal w = do + let expr = toLazyText $ exprToSMT w + raw <- getVal expr + case parseCommentFreeFileMsg getValueRes (T.toStrict raw) of + Right (ResSpecific (valParsed :| [])) -> + case valParsed of + (_, TermSpecConstant sc) -> pure $ parseW256 sc + _ -> error $ "Internal Error: cannot parse model for: " <> show w + r -> parseErr r diff --git a/src/EVM/Sign.hs b/src/EVM/Sign.hs new file mode 100644 --- /dev/null +++ b/src/EVM/Sign.hs @@ -0,0 +1,77 @@ +{-| +Module : Helper functions to sign a transaction and derive address from +Description : for the EVM given a secret key +-} + +module EVM.Sign where + +import qualified Crypto.Hash as Crypto +import Data.Maybe (fromMaybe) +import Crypto.PubKey.ECC.ECDSA (signDigestWith, PrivateKey(..), Signature(..)) +import Crypto.PubKey.ECC.Types (getCurveByName, CurveName(..), Point(..)) +import Crypto.PubKey.ECC.Generate (generateQ) + +import EVM.ABI (encodeAbiValue, AbiValue (..)) +import qualified Data.ByteString as BS +import EVM.Types +import EVM.Expr (exprToAddr) +import EVM.Precompiled +import Data.Word + + +-- Given a secret key, generates the address +deriveAddr :: Integer -> Maybe Addr +deriveAddr sk = case pubPoint of + PointO -> Nothing + Point x y -> + -- See yellow paper #286 + let pub = BS.concat [ encodeInt x, encodeInt y ] + addr = Lit . W256 . word256 . BS.drop 12 . BS.take 32 . keccakBytes $ pub + in exprToAddr addr + where + curve = getCurveByName SEC_p256k1 + pubPoint = generateQ curve (num sk) + encodeInt = encodeAbiValue . AbiUInt 256 . fromInteger + +sign :: W256 -> Integer -> (Word8, W256, W256) +sign hash sk = (v, r, s) + where + -- setup curve params + curve = getCurveByName SEC_p256k1 + priv = PrivateKey curve sk + digest = fromMaybe + (error $ "Internal Error: could produce a digest from " <> show hash) + (Crypto.digestFromByteString (word256Bytes hash)) + + -- sign message + sig = ethsign priv digest + r = num $ sign_r sig + s = num lowS + + -- this is a little bit sad, but cryptonite doesn't give us back a v value + -- so we compute it by guessing one, and then seeing if that gives us the right answer from ecrecover + v = if ecrec 28 r s hash == deriveAddr sk + then 28 + else 27 + + -- we always use the lower S value to conform with EIP2 (re: ECDSA transaction malleability) + -- https://eips.ethereum.org/EIPS/eip-2 + secpOrder = 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141 :: Integer + lowS = if sign_s sig > secpOrder `div` 2 + then secpOrder - sign_s sig + else sign_s sig + +-- | We don't want to introduce the machinery needed to sign with a random nonce, +-- so we just use the same nonce every time (420). This is obviously very +-- insecure, but fine for testing purposes. +ethsign :: PrivateKey -> Crypto.Digest Crypto.Keccak_256 -> Signature +ethsign sk digest = go 420 + where + go k = case signDigestWith k sk digest of + Nothing -> go (k + 1) + Just sig -> sig + +ecrec :: W256 -> W256 -> W256 -> W256 -> Maybe Addr +ecrec v r s e = num . word <$> EVM.Precompiled.execute 1 input 32 + where input = BS.concat (word256Bytes <$> [e, v, r, s]) + diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs --- a/src/EVM/Solidity.hs +++ b/src/EVM/Solidity.hs @@ -1,6 +1,5 @@ {-# Language DeriveAnyClass #-} {-# Language DataKinds #-} -{-# Language StrictData #-} {-# Language QuasiQuotes #-} module EVM.Solidity @@ -178,11 +177,11 @@ deriving (Show, Eq, Ord, Generic) data SrcMap = SM { - srcMapOffset :: {-# UNPACK #-} Int, - srcMapLength :: {-# UNPACK #-} Int, - srcMapFile :: {-# UNPACK #-} Int, + srcMapOffset :: {-# UNPACK #-} !Int, + srcMapLength :: {-# UNPACK #-} !Int, + srcMapFile :: {-# UNPACK #-} !Int, srcMapJump :: JumpType, - srcMapModifierDepth :: {-# UNPACK #-} Int + srcMapModifierDepth :: {-# UNPACK #-} !Int } deriving (Show, Eq, Ord, Generic) data SrcMapParseState @@ -518,11 +517,11 @@ containsLinkerHole = regexMatches "__\\$[a-z0-9]{34}\\$__" toCode :: Text -> ByteString -toCode t = case BS16.decode (encodeUtf8 t) of +toCode t = case BS16.decodeBase16 (encodeUtf8 t) of Right d -> d Left e -> if containsLinkerHole t then error "unlinked libraries detected in bytecode" - else error e + else error $ Text.unpack e solidity' :: Text -> IO (Text, Text) solidity' src = withSystemTempFile "hevm.sol" $ \path handle -> do diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs --- a/src/EVM/Solvers.hs +++ b/src/EVM/Solvers.hs @@ -2,8 +2,6 @@ {-# Language GADTs #-} {-# Language PolyKinds #-} {-# Language ScopedTypeVariables #-} -{-# Language TypeApplications #-} -{-# Language QuasiQuotes #-} {- | Module: EVM.Solvers @@ -18,10 +16,13 @@ import GHC.IO.Handle (Handle, hFlush, hSetBuffering, BufferMode(..)) import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan) import Control.Concurrent (forkIO, killThread) +import Control.Monad.State.Strict import Data.Char (isSpace) import Data.Maybe (fromMaybe) import Data.Text.Lazy (Text) +import Data.Map (Map) +import qualified Data.Map as Map import qualified Data.Text as TS import qualified Data.Text.Lazy as T import qualified Data.Text.Lazy.IO as T @@ -29,6 +30,7 @@ import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..)) import EVM.SMT +import EVM.Types -- | Supported solvers data Solver @@ -128,19 +130,7 @@ Right () -> do sat <- sendLine inst "(check-sat)" res <- case sat of - "sat" -> do - calldatamodels <- getVars parseVar (getValue inst) (fmap T.toStrict cexvars.calldataV) - buffermodels <- getBufs (getValue inst) (fmap T.toStrict cexvars.buffersV) - storagemodels <- getStore (getValue inst) cexvars.storeReads - blockctxmodels <- getVars parseBlockCtx (getValue inst) (fmap T.toStrict cexvars.blockContextV) - txctxmodels <- getVars parseFrameCtx (getValue inst) (fmap T.toStrict cexvars.txContextV) - pure $ Sat $ SMTCex - { vars = calldatamodels - , buffers = buffermodels - , store = storagemodels - , blockContext = blockctxmodels - , txContext = txctxmodels - } + "sat" -> Sat <$> getModel inst cexvars "unsat" -> pure Unsat "timeout" -> pure Unknown "unknown" -> pure Unknown @@ -149,6 +139,85 @@ -- put the instance back in the list of available instances writeChan availableInstances inst + +getModel :: SolverInstance -> CexVars -> IO SMTCex +getModel inst cexvars = do + -- get an initial version of the model from the solver + initialModel <- getRaw + -- get concrete values for each buffers max read index + hints <- capHints <$> queryMaxReads (getValue inst) cexvars.buffersV + -- check the sizes of buffer models and shrink if needed + if bufsUsable initialModel + then do + pure (mkConcrete initialModel) + else mkConcrete . snd <$> runStateT (shrinkModel hints) initialModel + where + getRaw :: IO SMTCex + getRaw = do + vars <- getVars parseVar (getValue inst) (fmap T.toStrict cexvars.calldataV) + buffers <- getBufs (getValue inst) (Map.keys cexvars.buffersV) + storage <- getStore (getValue inst) cexvars.storeReads + blockctx <- getVars parseBlockCtx (getValue inst) (fmap T.toStrict cexvars.blockContextV) + txctx <- getVars parseFrameCtx (getValue inst) (fmap T.toStrict cexvars.txContextV) + pure $ SMTCex vars buffers storage blockctx txctx + + -- sometimes the solver might give us back a model for the max read index + -- that is too high to be a useful cex (e.g. in the case of reads from a + -- symbolic index), so we cap the max value of the starting point to be 1024 + capHints :: Map Text W256 -> Map Text W256 + capHints = fmap (min 1024) + + -- shrink all the buffers in a model + shrinkModel :: Map Text W256 -> StateT SMTCex IO () + shrinkModel hints = do + m <- get + -- iterate over all the buffers in the model, and shrink each one in turn if needed + forM_ (Map.keys m.buffers) $ \case + AbstractBuf b -> do + let name = T.fromStrict b + hint = fromMaybe + (error $ "Internal Error: Could not find hint for buffer: " <> T.unpack name) + (Map.lookup name hints) + shrinkBuf name hint + _ -> error "Internal Error: Received model from solver for non AbstractBuf" + + -- starting with some guess at the max useful size for a buffer, cap + -- it's size to that value, and ask the solver to check satisfiability. If + -- it's still sat with the new constraint, leave that constraint on the + -- stack and return a new model, if it's unsat, double the size of the hint + -- and try again. + shrinkBuf :: Text -> W256 -> StateT SMTCex IO () + shrinkBuf buf hint = do + let encBound = "(_ bv" <> (T.pack $ show (num hint :: Integer)) <> " 256)" + sat <- liftIO $ do + sendLine' inst "(push)" + sendLine' inst $ "(assert (bvule " <> buf <> "_length " <> encBound <> "))" + sendLine inst "(check-sat)" + case sat of + "sat" -> do + model <- liftIO getRaw + put model + "unsat" -> do + liftIO $ sendLine' inst "(pop)" + shrinkBuf buf (if hint == 0 then hint + 1 else hint * 2) + _ -> error "TODO: HANDLE ERRORS" + + -- Collapses the abstract description of a models buffers down to a bytestring + mkConcrete :: SMTCex -> SMTCex + mkConcrete c = fromMaybe + (error $ "Internal Error: counterexample contains buffers that are too large to be represented as a ByteString: " <> show c) + (flattenBufs c) + + -- we set a pretty arbitrary upper limit (of 1024) to decide if we need to do some shrinking + bufsUsable :: SMTCex -> Bool + bufsUsable model = any (go . snd) (Map.toList model.buffers) + where + go (Flat _) = True + go (Comp c) = case c of + (Base _ sz) -> sz <= 1024 + -- TODO: do I need to check the write idx here? + (Write _ idx next) -> idx <= 1024 && go (Comp next) + -- | Arguments used when spawing a solver instance solverArgs :: Solver -> Maybe (Natural) -> [Text] diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -12,7 +12,8 @@ import EVM.Exec import qualified EVM.Fetch as Fetch import EVM.ABI -import EVM.SMT +import EVM.SMT (SMTCex(..), SMT2(..), assertProps, formatSMT2) +import qualified EVM.SMT as SMT import EVM.Solvers import EVM.Traversals import qualified EVM.Expr as Expr @@ -46,6 +47,9 @@ import GHC.Conc (getNumProcessors) import EVM.Format (indent, formatBinary) +-- | A method name, and the (ordered) types of it's arguments +data Sig = Sig Text [AbiType] + data ProofResult a b c = Qed a | Cex b | Timeout c deriving (Show, Eq) type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End) @@ -173,12 +177,9 @@ s -> error $ "unsupported cd fragment: " <> show s -abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> Maybe Precondition -> StorageModel -> VM -abstractVM typesignature concreteArgs contractCode maybepre storagemodel = finalVm +abstractVM :: (Expr Buf, [Prop]) -> ByteString -> Maybe Precondition -> StorageModel -> VM +abstractVM (cd, calldataProps) contractCode maybepre storagemodel = finalVm where - (calldata', calldataProps) = case typesignature of - Nothing -> (AbstractBuf "txdata", [Expr.bufLength (AbstractBuf "txdata") .< (Lit (2 ^ (64 :: Integer)))]) - Just (name, typs) -> symCalldata name typs concreteArgs (AbstractBuf "txdata") store = case storagemodel of SymbolicS -> AbstractStore InitialS -> EmptyStore @@ -186,7 +187,7 @@ caller' = Caller 0 value' = CallValue 0 code' = RuntimeCode (ConcreteRuntimeCode contractCode) - vm' = loadSymVM code' store caller' value' calldata' calldataProps + vm' = loadSymVM code' store caller' value' cd calldataProps precond = case maybepre of Nothing -> [] Just p -> [p vm'] @@ -299,7 +300,7 @@ type Postcondition = VM -> Expr End -> Prop -checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult]) +checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult]) checkAssert solvers errs c signature' concreteArgs opts = verifyContract solvers c signature' concreteArgs opts SymbolicS Nothing (Just $ checkAssertions errs) {- |Checks if an assertion violation has been encountered @@ -338,9 +339,21 @@ panicMsg :: Word256 -> ByteString panicMsg err = (selector "Panic(uint256)") <> (encodeAbiValue $ AbiUInt 256 err) -verifyContract :: SolverGroup -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> StorageModel -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult]) -verifyContract solvers theCode signature' concreteArgs opts storagemodel maybepre maybepost = do - let preState = abstractVM signature' concreteArgs theCode maybepre storagemodel +-- | Builds a buffer representing calldata from the provided method description and concrete arguments +mkCalldata :: Maybe Sig -> [String] -> (Expr Buf, [Prop]) +mkCalldata Nothing _ = + ( AbstractBuf "txdata" + -- assert that the length of the calldata is never more than 2^64 + -- this is way larger than would ever be allowed by the gas limit + -- and avoids spurious counterexamples during abi decoding + -- TODO: can we encode calldata as an array with a smaller length? + , [Expr.bufLength (AbstractBuf "txdata") .< (Lit (2 ^ (64 :: Integer)))] + ) +mkCalldata (Just (Sig name types)) args = symCalldata name types args (AbstractBuf "txdata") + +verifyContract :: SolverGroup -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> StorageModel -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult]) +verifyContract solvers theCode signature concreteArgs opts storagemodel maybepre maybepost = do + let preState = abstractVM (mkCalldata signature concreteArgs) theCode maybepre storagemodel verify solvers opts preState maybepost pruneDeadPaths :: [VM] -> [VM] @@ -518,8 +531,8 @@ -- We do this by asking the solver to find a common input for each pair of endstates that satisfies the path -- conditions for both sides and produces a differing output. If we can find such an input, then we have a clear -- equivalence break, and since we run this check for every pair of end states, the check is exhaustive. -equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> Maybe (Text, [AbiType]) -> IO [EquivResult] -equivalenceCheck solvers bytecodeA bytecodeB opts signature' = do +equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> (Expr Buf, [Prop]) -> IO [EquivResult] +equivalenceCheck solvers bytecodeA bytecodeB opts calldata' = do case bytecodeA == bytecodeB of True -> do putStrLn "bytecodeA and bytecodeB are identical" @@ -563,7 +576,7 @@ getBranches bs = do let bytecode = if BS.null bs then BS.pack [0] else bs - prestate = abstractVM signature' [] bytecode Nothing SymbolicS + prestate = abstractVM calldata' bytecode Nothing SymbolicS expr <- evalStateT (interpret (Fetch.oracle solvers Nothing) opts.maxIter opts.askSmtIters runExpr) prestate let simpl = if opts.simp then (Expr.simplify expr) else expr pure $ flattenExpr simpl @@ -749,8 +762,11 @@ -- | Takes a buffer and a Cex and replaces all abstract values in the buf with concrete ones from the Cex subModel :: SMTCex -> Expr a -> Expr a -subModel c expr = subBufs c.buffers . subVars c.vars . subStore c.store . subVars c.blockContext . subVars c.txContext $ expr +subModel c expr = subBufs (fmap forceFlattened c.buffers) . subVars c.vars . subStore c.store . subVars c.blockContext . subVars c.txContext $ expr where + forceFlattened (SMT.Flat bs) = bs + forceFlattened b@(SMT.Comp _) = forceFlattened $ fromMaybe (error $ "Internal Error: cannot flatten buffer: " <> show b) (SMT.collapse b) + subVars model b = Map.foldlWithKey subVar b model subVar :: Expr a -> Expr EWord -> W256 -> Expr a subVar b var val = mapExpr go b diff --git a/src/EVM/TTY.hs b/src/EVM/TTY.hs --- a/src/EVM/TTY.hs +++ b/src/EVM/TTY.hs @@ -25,7 +25,7 @@ import EVM.Solvers (SolverGroup) import EVM.Op import EVM.Solidity hiding (storageLayout) -import EVM.Types hiding (padRight) +import EVM.Types hiding (padRight, Max) import EVM.UnitTest import EVM.Stepper (Stepper) import EVM.Stepper qualified as Stepper diff --git a/src/EVM/Transaction.hs b/src/EVM/Transaction.hs --- a/src/EVM/Transaction.hs +++ b/src/EVM/Transaction.hs @@ -5,34 +5,44 @@ import qualified EVM import EVM (balance, initialContract) import EVM.FeeSchedule -import EVM.Precompiled (execute) import EVM.RLP import EVM.Types import EVM.Expr (litAddr) - import Control.Lens +import EVM.Sign -import Data.Aeson (FromJSON (..)) import Data.ByteString (ByteString) import Data.Map (Map) import Data.Maybe (fromMaybe, isNothing, fromJust) +import GHC.Generics (Generic) +import Data.Aeson (FromJSON (..)) 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 import Data.Word (Word64) +import Numeric (showHex) data AccessListEntry = AccessListEntry { accessAddress :: Addr, accessStorageKeys :: [W256] -} deriving Show +} deriving (Show, Generic) +instance JSON.ToJSON AccessListEntry + data TxType = LegacyTransaction | AccessListTransaction | EIP1559Transaction - deriving (Show, Eq) + deriving (Show, Eq, Generic) +instance JSON.ToJSON TxType where + toJSON t = case t of + EIP1559Transaction -> "0x2" -- EIP1559 + LegacyTransaction -> "0x1" -- EIP2718 + AccessListTransaction -> "0x1" -- EIP2930 + + data Transaction = Transaction { txData :: ByteString, txGasLimit :: Word64, @@ -46,30 +56,68 @@ txType :: TxType, txAccessList :: [AccessListEntry], txMaxPriorityFeeGas :: Maybe W256, - txMaxFeePerGas :: Maybe W256 -} deriving Show + txMaxFeePerGas :: Maybe W256, + txChainId :: W256 +} deriving (Show, Generic) +instance JSON.ToJSON Transaction where + toJSON t = JSON.object [ ("input", (JSON.toJSON (ByteStringS t.txData))) + , ("gas", (JSON.toJSON $ "0x" ++ showHex (toInteger $ t.txGasLimit) "")) + , ("gasPrice", (JSON.toJSON $ show $ fromJust $ t.txGasPrice)) + , ("v", (JSON.toJSON $ show $ (t.txV)-27)) + , ("r", (JSON.toJSON $ show $ t.txR)) + , ("s", (JSON.toJSON $ show $ t.txS)) + , ("to", (JSON.toJSON $ t.txToAddr)) + , ("nonce", (JSON.toJSON $ show $ t.txNonce)) + , ("value", (JSON.toJSON $ show $ t.txValue)) + , ("type", (JSON.toJSON $ t.txType)) + , ("accessList", (JSON.toJSON $ t.txAccessList)) + , ("maxPriorityFeePerGas", (JSON.toJSON $ show $ fromJust $ t.txMaxPriorityFeeGas)) + , ("maxFeePerGas", (JSON.toJSON $ show $ fromJust $ t.txMaxFeePerGas)) + , ("chainId", (JSON.toJSON $ show t.txChainId)) + ] + +emptyTransaction :: Transaction +emptyTransaction = Transaction { txData = mempty + , txGasLimit = 0 + , txGasPrice = Nothing + , txNonce = 0 + , txR = 0 + , txS = 0 + , txToAddr = Nothing + , txV = 0 + , txValue = 0 + , txType = EIP1559Transaction + , txAccessList = [] + , txMaxPriorityFeeGas = Nothing + , txMaxFeePerGas = Nothing + , txChainId = 1 + } + -- | utility function for getting a more useful representation of accesslistentries -- duplicates only matter for gas computation txAccessMap :: Transaction -> Map Addr [W256] txAccessMap tx = ((Map.fromListWith (++)) . makeTups) tx.txAccessList where makeTups = map (\ale -> (ale.accessAddress , ale.accessStorageKeys )) -ecrec :: W256 -> W256 -> W256 -> W256 -> Maybe Addr -ecrec v r s e = num . word <$> EVM.Precompiled.execute 1 input 32 - where input = BS.concat (word256Bytes <$> [e, v, r, s]) - -sender :: Int -> Transaction -> Maybe Addr -sender chainId tx = ecrec v' tx.txR tx.txS hash - where hash = keccak' (signingData chainId tx) +-- Given Transaction, it recovers the address that sent it +sender :: Transaction -> Maybe Addr +sender tx = ecrec v' tx.txR tx.txS hash + where hash = keccak' (signingData tx) v = tx.txV v' = if v == 27 || v == 28 then v else 27 + v -signingData :: Int -> Transaction -> ByteString -signingData chainId tx = +sign :: Integer -> Transaction -> Transaction +sign sk tx = tx { txV = num v, txR = r, txS = s} + where + hash = keccak' $ signingData tx + (v, r, s) = EVM.Sign.sign hash sk + +signingData :: Transaction -> ByteString +signingData tx = case tx.txType of - LegacyTransaction -> if v == (chainId * 2 + 35) || v == (chainId * 2 + 36) + LegacyTransaction -> if v == (tx.txChainId * 2 + 35) || v == (tx.txChainId * 2 + 36) then eip155Data else normalData AccessListTransaction -> eip2930Data @@ -98,11 +146,11 @@ to', rlpWord256 tx.txValue, BS tx.txData, - rlpWord256 (fromIntegral chainId), + rlpWord256 tx.txChainId, rlpWord256 0x0, rlpWord256 0x0] eip1559Data = cons 0x02 $ rlpList [ - rlpWord256 (fromIntegral chainId), + rlpWord256 tx.txChainId, rlpWord256 tx.txNonce, rlpWord256 maxPrio, rlpWord256 maxFee, @@ -113,7 +161,7 @@ rlpAccessList] eip2930Data = cons 0x01 $ rlpList [ - rlpWord256 (fromIntegral chainId), + rlpWord256 tx.txChainId, rlpWord256 tx.txNonce, rlpWord256 gasPrice, rlpWord256 (num tx.txGasLimit), @@ -165,15 +213,15 @@ value <- wordField val "value" txType <- fmap (read :: String -> Int) <$> (val JSON..:? "type") case txType of - Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing + Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing 1 Just 0x01 -> do accessListEntries <- (val JSON..: "accessList") >>= parseJSONList - return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries Nothing Nothing + return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries Nothing Nothing 1 Just 0x02 -> do accessListEntries <- (val JSON..: "accessList") >>= parseJSONList - return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value EIP1559Transaction accessListEntries maxPrio maxFee + return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value EIP1559Transaction accessListEntries maxPrio maxFee 1 Just _ -> fail "unrecognized custom transaction type" - Nothing -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing + Nothing -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing 1 parseJSON invalid = JSON.typeMismatch "Transaction" invalid diff --git a/src/EVM/Traversals.hs b/src/EVM/Traversals.hs --- a/src/EVM/Traversals.hs +++ b/src/EVM/Traversals.hs @@ -26,6 +26,7 @@ PNeg a -> go a PAnd a b -> go a <> go b POr a b -> go a <> go b + PImpl a b -> go a <> go b -- | Recursively folds a given function over a given expression -- Recursion schemes do this & a lot more, but defining them over GADT's isn't worth the hassle @@ -85,6 +86,7 @@ e@(Exp a b) -> f e <> (go a) <> (go b) e@(SEx a b) -> f e <> (go a) <> (go b) e@(Min a b) -> f e <> (go a) <> (go b) + e@(Max a b) -> f e <> (go a) <> (go b) -- booleans @@ -237,6 +239,7 @@ PNeg a -> PNeg (mapProp f a) PAnd a b -> PAnd (mapProp f a) (mapProp f b) POr a b -> POr (mapProp f a) (mapProp f b) + PImpl a b -> PImpl (mapProp f a) (mapProp f b) -- | Recursively applies a given function to every node in a given expr instance -- Recursion schemes do this & a lot more, but defining them over GADT's isn't worth the hassle @@ -379,6 +382,10 @@ a' <- mapExprM f a b' <- mapExprM f b f (Min a' b') + Max a b -> do + a' <- mapExprM f a + b' <- mapExprM f b + f (Max a' b') -- booleans @@ -642,3 +649,22 @@ a' <- mapPropM f a b' <- mapPropM f b pure $ POr a' b' + PImpl a b -> do + a' <- mapPropM f a + b' <- mapPropM f b + pure $ PImpl a' b' + + +-- | Generic operations over AST terms +class TraversableTerm a where + mapTerm :: (forall b. Expr b -> Expr b) -> a -> a + foldTerm :: forall c. Monoid c => (forall b. Expr b -> c) -> c -> a -> c + + +instance TraversableTerm (Expr a) where + mapTerm = mapExpr + foldTerm = foldExpr + +instance TraversableTerm Prop where + mapTerm = mapProp + foldTerm = foldProp diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -11,40 +11,42 @@ import Prelude hiding (Word, LT, GT) -import Data.Aeson +import Control.Arrow ((>>>)) import Crypto.Hash hiding (SHA256) -import Data.Map (Map) +import Data.Aeson +import Data.Aeson qualified as JSON +import Data.Aeson.Types qualified as JSON import Data.Bifunctor (first) +import Data.Bits (Bits, FiniteBits, shiftR, shift, shiftL, (.&.), (.|.)) +import Data.ByteArray qualified as BA import Data.Char import Data.List (isPrefixOf, foldl') import Data.ByteString (ByteString) -import Data.ByteString.Base16 as BS16 +import Data.ByteString qualified as BS +import Data.ByteString.Base16 qualified as BS16 import Data.ByteString.Builder (byteStringHex, toLazyByteString) +import Data.ByteString.Char8 qualified as Char8 import Data.ByteString.Lazy (toStrict) -import qualified Data.ByteString.Char8 as Char8 import Data.Word (Word8, Word32, Word64) -import Data.Bits (Bits, FiniteBits, shiftR, shift, shiftL, (.&.), (.|.)) import Data.DoubleWord import Data.DoubleWord.TH +import Data.Map (Map) import Data.Maybe (fromMaybe) +import Data.Sequence qualified as Seq +import Data.Serialize qualified as Cereal +import Data.Text qualified as Text +import Data.Text.Encoding qualified as Text +import Data.Vector qualified as V import Numeric (readHex, showHex) import Options.Generic -import Control.Arrow ((>>>)) +import EVM.Hexdump (paddedShowHex) +import Control.Monad -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 Data.Sequence as Seq import qualified Text.Regex.TDFA as Regex import qualified Text.Read -- Some stuff for "generic programming", needed to create Word512 import Data.Data -import qualified Data.Vector as V -- We need a 512-bit word for doing ADDMOD and MULMOD with full precision. mkUnpackedDoubleWord "Word512" ''Word256 "Int512" ''Int256 ''Word256 @@ -144,13 +146,13 @@ -- identifiers - Lit :: W256 -> Expr EWord + Lit :: {-# UNPACK #-} !W256 -> Expr EWord Var :: Text -> Expr EWord GVar :: GVar a -> Expr a -- bytes - LitByte :: Word8 -> Expr Byte + LitByte :: {-# UNPACK #-} !Word8 -> Expr Byte IndexWord :: Expr EWord -> Expr EWord -> Expr Byte EqByte :: Expr Byte -> Expr Byte -> Expr EWord @@ -166,10 +168,10 @@ -> Expr EWord -- control flow - Revert :: [Prop] -> Expr Buf -> Expr End - Failure :: [Prop] -> Error -> Expr End - Return :: [Prop] -> Expr Buf -> Expr Storage -> Expr End - ITE :: Expr EWord -> Expr End -> Expr End -> Expr End + Revert :: [Prop] -> Expr Buf -> Expr End + Failure :: [Prop] -> Error -> Expr End + Return :: [Prop] -> Expr Buf -> Expr Storage -> Expr End + ITE :: Expr EWord -> Expr End -> Expr End -> Expr End -- integers @@ -185,6 +187,7 @@ Exp :: Expr EWord -> Expr EWord -> Expr EWord SEx :: Expr EWord -> Expr EWord -> Expr EWord Min :: Expr EWord -> Expr EWord -> Expr EWord + Max :: Expr EWord -> Expr EWord -> Expr EWord -- booleans @@ -384,6 +387,7 @@ PNeg :: Prop -> Prop PAnd :: Prop -> Prop -> Prop POr :: Prop -> Prop -> Prop + PImpl :: Prop -> Prop -> Prop PBool :: Bool -> Prop deriving instance (Show Prop) @@ -430,6 +434,7 @@ PNeg a == PNeg b = a == b PAnd a b == PAnd c d = a == c && b == d POr a b == POr c d = a == c && b == d + PImpl a b == PImpl c d = a == c && b == d _ == _ = False instance Ord Prop where @@ -445,6 +450,7 @@ PNeg a <= PNeg b = a <= b PAnd a b <= PAnd c d = a <= c && b <= d POr a b <= POr c d = a <= c && b <= d + PImpl a b <= PImpl c d = a <= c && b <= d _ <= _ = False @@ -456,7 +462,7 @@ unlitByte (LitByte x) = Just x unlitByte _ = Nothing -newtype ByteStringS = ByteStringS ByteString deriving (Eq) +newtype ByteStringS = ByteStringS ByteString deriving (Eq, Generic) instance Show ByteStringS where show (ByteStringS x) = ("0x" ++) . Text.unpack . fromBinary $ x @@ -464,14 +470,22 @@ fromBinary = Text.decodeUtf8 . toStrict . toLazyByteString . byteStringHex +instance JSON.FromJSON ByteStringS where + parseJSON (JSON.String x) = case BS16.decodeBase16' x of + Left _ -> mzero + Right bs -> pure (ByteStringS bs) + parseJSON _ = mzero + instance JSON.ToJSON ByteStringS where - toJSON = JSON.String . Text.pack . show + toJSON (ByteStringS x) = JSON.String (Text.pack $ "0x" ++ (concatMap (paddedShowHex 2) . BS.unpack $ x)) newtype Addr = Addr { addressWord160 :: Word160 } deriving ( Num, Integral, Real, Ord, Enum , Eq, Generic, Bits, FiniteBits ) +instance JSON.ToJSON Addr where + toJSON = JSON.String . Text.pack . show maybeLitWord :: Expr EWord -> Maybe W256 maybeLitWord (Lit w) = Just w @@ -485,8 +499,28 @@ showsPrec _ s = ("0x" ++) . showHex s instance JSON.ToJSON W256 where - toJSON = JSON.String . Text.pack . show + toJSON x = JSON.String $ Text.pack ("0x" ++ pad ++ cutshow) + where + cutshow = drop 2 $ show x + pad = replicate (64 - length (cutshow)) '0' +newtype W64 = W64 Data.Word.Word64 + deriving + ( Num, Integral, Real, Ord, Generic + , Bits , FiniteBits, Enum, Eq , Bounded + ) +instance JSON.FromJSON W64 + +instance Read W64 where + readsPrec _ "0x" = [(0, "")] + readsPrec n s = first W64 <$> readsPrec n s + +instance Show W64 where + showsPrec _ s = ("0x" ++) . showHex s + +instance JSON.ToJSON W64 where + toJSON x = JSON.String $ Text.pack $ show x + instance Read Addr where readsPrec _ ('0':'x':s) = readHex s readsPrec _ s = readHex s @@ -497,6 +531,14 @@ str = replicate (40 - length hex) '0' ++ hex in "0x" ++ toChecksumAddress str ++ drop 40 str +instance JSON.ToJSONKey Addr where + toJSONKey = JSON.toJSONKeyText (addrKey) + where + addrKey :: Addr -> Text + addrKey addr = Text.pack $ replicate (40 - length hex) '0' ++ hex + where + hex = show addr + -- https://eips.ethereum.org/EIPS/eip-55 toChecksumAddress :: String -> String toChecksumAddress addr = zipWith transform nibbles addr @@ -552,13 +594,13 @@ hexByteString :: String -> ByteString -> ByteString hexByteString msg bs = - case BS16.decode bs of + case BS16.decodeBase16 bs of Right x -> x _ -> error ("invalid hex bytestring for " ++ msg) hexText :: Text -> ByteString hexText t = - case BS16.decode (Text.encodeUtf8 (Text.drop 2 t)) of + case BS16.decodeBase16 (Text.encodeUtf8 (Text.drop 2 t)) of Right x -> x _ -> error ("invalid hex bytestring " ++ show t) @@ -597,9 +639,6 @@ padLeft :: Int -> ByteString -> ByteString padLeft n xs = BS.replicate (n - BS.length xs) 0 <> xs -padLeftStr :: Int -> String -> String -padLeftStr n xs = replicate (n - length xs) '0' <> xs - padRight :: Int -> ByteString -> ByteString padRight n xs = xs <> BS.replicate (n - BS.length xs) 0 @@ -616,6 +655,9 @@ padLeft' n xs = V.replicate (n - length xs) (LitByte 0) <> xs word256 :: ByteString -> Word256 +word256 xs | BS.length xs == 1 = + -- optimize one byte pushes + Word256 (Word128 0 0) (Word128 0 (fromIntegral $ BS.head xs)) word256 xs = case Cereal.runGet m (padLeft 32 xs) of Left _ -> error "internal error" Right x -> x @@ -624,14 +666,11 @@ b <- Cereal.getWord64be c <- Cereal.getWord64be d <- Cereal.getWord64be - return $ fromHiAndLo (fromHiAndLo a b) (fromHiAndLo c d) + pure $ Word256 (Word128 a b) (Word128 c d) word :: ByteString -> W256 word = W256 . word256 -byteAt :: (Bits a, Bits b, Integral a, Num b) => a -> Int -> b -byteAt x j = num (x `shiftR` (j * 8)) .&. 0xff - fromBE :: (Integral a) => ByteString -> a fromBE xs = if xs == mempty then 0 else 256 * fromBE (BS.init xs) @@ -643,10 +682,12 @@ <> BS.pack [num $ x `mod` 256] word256Bytes :: W256 -> ByteString -word256Bytes x = BS.pack [byteAt x (31 - i) | i <- [0..31]] +word256Bytes (W256 (Word256 (Word128 a b) (Word128 c d))) = + Cereal.encode a <> Cereal.encode b <> Cereal.encode c <> Cereal.encode d word160Bytes :: Addr -> ByteString -word160Bytes x = BS.pack [byteAt x.addressWord160 (19 - i) | i <- [0..19]] +word160Bytes (Addr (Word160 a (Word128 b c))) = + Cereal.encode a <> Cereal.encode b <> Cereal.encode c newtype Nibble = Nibble Word8 deriving ( Num, Integral, Real, Ord, Enum, Eq, Bounded, Generic) @@ -724,3 +765,23 @@ regex = Regex.makeRegexOpts compOpts execOpts (Text.unpack regexSource) in Regex.matchTest regex . Seq.fromList . Text.unpack + +data VMTrace = + VMTrace + { tracePc :: Int + , traceOp :: Int + , traceStack :: [W256] + , traceMemSize :: Data.Word.Word64 + , traceDepth :: Int + , traceGas :: Data.Word.Word64 + , traceError :: Maybe String + } deriving (Generic, Show) +instance JSON.ToJSON VMTrace where + toEncoding = JSON.genericToEncoding JSON.defaultOptions +instance JSON.FromJSON VMTrace + +bsToHex :: ByteString -> String +bsToHex bs = concatMap (paddedShowHex 2) (BS.unpack bs) + +bssToBs :: ByteStringS -> ByteString +bssToBs (ByteStringS bs) = bs diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs --- a/src/EVM/UnitTest.hs +++ b/src/EVM/UnitTest.hs @@ -926,10 +926,6 @@ _ -> Nothing _ -> Just "" - -word32Bytes :: Word32 -> ByteString -word32Bytes x = BS.pack [byteAt x (3 - i) | i <- [0..3]] - abiCall :: TestVMParams -> Either (Text, AbiValue) ByteString -> EVM () abiCall params args = let cd = case args of diff --git a/test/BlockchainTests.hs b/test/BlockchainTests.hs --- a/test/BlockchainTests.hs +++ b/test/BlockchainTests.hs @@ -352,7 +352,7 @@ -> Either BlockchainError Case fromBlockchainCase' block tx preState postState = let isCreate = isNothing tx.txToAddr in - case (sender 1 tx, checkTx tx block preState) of + case (sender tx, checkTx tx block preState) of (Nothing, _) -> Left SignatureUnverified (_, Nothing) -> Left (if isCreate then FailedCreate else InvalidTx) (Just origin, Just checkState) -> Right $ Case @@ -420,7 +420,7 @@ validateTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe () validateTx tx block cs = do let cs' = Map.map fst cs - origin <- sender 1 tx + origin <- sender tx originBalance <- (view balance) <$> view (at origin) cs' originNonce <- (view nonce) <$> view (at origin) cs' let gasDeposit = (effectiveprice tx block.blockBaseFee) * (num tx.txGasLimit) @@ -431,7 +431,7 @@ checkTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe (Map Addr (EVM.Contract, Storage)) checkTx tx block prestate = do - origin <- sender 1 tx + origin <- sender tx validateTx tx block prestate let isCreate = isNothing tx.txToAddr senderNonce = view (accountAt origin . nonce) (Map.map fst prestate) diff --git a/test/EVM/Tracing.hs b/test/EVM/Tracing.hs new file mode 100644 --- /dev/null +++ b/test/EVM/Tracing.hs @@ -0,0 +1,870 @@ +{-| +Module : Tracing +Description : Tests to fuzz concrete tracing, and symbolic execution + +Functions here are used to generate traces for the concrete +execution of HEVM and check that against evmtool from go-ehereum. Re-using some +of this code, we also generate a symbolic expression then evaluate it +concretely through Expr.simplify, then check that against evmtool's output. +-} + +{-# Language DataKinds #-} +{-# Language DuplicateRecordFields #-} +{-# LANGUAGE DeriveGeneric #-} + +module EVM.Tracing where + +import Data.ByteString (ByteString) +import System.Directory +import System.IO +import qualified Data.Word +import GHC.Generics +import Numeric (showHex) +import qualified Paths_hevm as Paths + +import Prelude hiding (fail, LT, GT) + +import qualified Data.ByteString as BS +import Data.Maybe +import Data.List qualified (length) +import Test.Tasty +import Test.Tasty.QuickCheck hiding (Failure) +import Test.QuickCheck.Instances.Text() +import Test.QuickCheck.Instances.Natural() +import Test.QuickCheck.Instances.ByteString() +import Test.QuickCheck (elements) +import Test.Tasty.HUnit +import qualified Data.Aeson as JSON +import Data.Aeson ((.:), (.:?)) +import Data.ByteString.Char8 qualified as Char8 + +import qualified Control.Monad (when) +import qualified Control.Monad.Operational as Operational (view, ProgramViewT(..), ProgramView) +import Control.Monad.State.Strict hiding (state) +import Control.Monad.State.Strict qualified as State +import Control.Lens hiding (List, pre, (.>), re, op) + +import qualified Data.Vector as Vector +import qualified Data.Map.Strict as Map + +import EVM hiding (allowFFI) +import EVM.SymExec +import EVM.Assembler +import EVM.Op hiding (getOp) +import EVM.Exec +import EVM.Types +import EVM.Traversals +import EVM.Concrete (createAddress) +import qualified EVM.FeeSchedule as FeeSchedule +import EVM.Solvers +import qualified EVM.Expr as Expr +import qualified Data.Text.IO as T +import qualified EVM.Stepper as Stepper +import qualified EVM.Fetch as Fetch +import System.Process +import qualified EVM.Transaction +import EVM.Format (formatBinary) +import EVM.Sign (deriveAddr) +import GHC.IO.Exception (ExitCode(ExitSuccess)) + +data VMTraceResult = + VMTraceResult + { out :: ByteStringS + , gasUsed :: Data.Word.Word64 + } deriving (Generic, Show) + +instance JSON.ToJSON VMTraceResult where + toEncoding = JSON.genericToEncoding JSON.defaultOptions + +data EVMToolTrace = + EVMToolTrace + { pc :: Int + , op :: Int + , gas :: W256 + , memSize :: Integer + , depth :: Int + , refund :: Int + , opName :: String + , stack :: [W256] + , error :: Maybe String + } deriving (Generic, Show) + +instance JSON.FromJSON EVMToolTrace where + parseJSON = JSON.withObject "EVMToolTrace" $ \v -> EVMToolTrace + <$> v .: "pc" + <*> v .: "op" + <*> v .: "gas" + <*> v .: "memSize" + <*> v .: "depth" + <*> v .: "refund" + <*> v .: "opName" + <*> v .: "stack" + <*> v .:? "error" + +mkBlockHash:: Int -> Expr 'EWord +mkBlockHash x = (num x :: Integer) & show & Char8.pack & EVM.Types.keccak' & Lit + +blockHashesDefault :: Map.Map Int W256 +blockHashesDefault = Map.fromList [(x, forceLit $ mkBlockHash x) | x<- [1..256]] + +data EVMToolOutput = + EVMToolOutput + { output :: ByteStringS + , gasUsed :: W256 + , time :: Integer + } deriving (Generic, Show) + +instance JSON.FromJSON EVMToolOutput + +data EVMToolTraceOutput = + EVMToolTraceOutput + { trace :: [EVMToolTrace] + , output :: EVMToolOutput + } deriving (Generic, Show) + +instance JSON.FromJSON EVMToolTraceOutput + +data EVMToolEnv = EVMToolEnv + { coinbase :: Addr + , timestamp :: Expr EWord + , number :: W256 + , prevRandao :: W256 + , gasLimit :: Data.Word.Word64 + , baseFee :: W256 + , maxCodeSize :: W256 + , schedule :: FeeSchedule.FeeSchedule Data.Word.Word64 + , blockHashes :: Map.Map Int W256 + } deriving (Show, Generic) + +instance JSON.ToJSON EVMToolEnv where + toJSON b = JSON.object [ ("currentCoinBase" , (JSON.toJSON $ b.coinbase)) + , ("currentDifficulty", (JSON.toJSON $ b.prevRandao)) + , ("currentGasLimit" , (JSON.toJSON ("0x" ++ showHex (toInteger $ b.gasLimit) ""))) + , ("currentNumber" , (JSON.toJSON $ b.number)) + , ("currentTimestamp" , (JSON.toJSON tstamp)) + , ("currentBaseFee" , (JSON.toJSON $ b.baseFee)) + , ("blockHashes" , (JSON.toJSON $ b.blockHashes)) + ] + where + tstamp :: W256 + tstamp = case (b.timestamp) of + Lit a -> a + _ -> error "Timestamp needs to be a Lit" + +emptyEvmToolEnv :: EVMToolEnv +emptyEvmToolEnv = EVMToolEnv { coinbase = 0 + , timestamp = Lit 0 + , number = 0 + , prevRandao = 42069 + , gasLimit = 0xffffffffffffffff + , baseFee = 0 + , maxCodeSize= 0xffffffff + , schedule = FeeSchedule.berlin + , blockHashes = mempty + } + +data EVMToolReceipt = + EVMToolReceipt + { _type :: String + , root :: String + , status :: String + , cumulativeGasUsed :: String + , logsBloom :: String + , logs :: Maybe String + , transactionHash :: String + , contractAddress :: String + , gasUsed :: String + , blockHash :: String + , transactionIndex :: String + } deriving (Generic, Show) + +instance JSON.FromJSON EVMToolReceipt where + parseJSON = JSON.withObject "EVMReceipt" $ \v -> EVMToolReceipt + <$> v .: "type" + <*> v .: "root" + <*> v .: "status" + <*> v .: "cumulativeGasUsed" + <*> v .: "logsBloom" + <*> v .: "logs" + <*> v .: "transactionHash" + <*> v .: "contractAddress" + <*> v .: "gasUsed" + <*> v .: "blockHash" + <*> v .: "transactionIndex" + +data EVMToolResult = + EVMToolResult + { stateRoot :: String + , txRoot :: String + , receiptsRoot :: String + , logsHash :: String + , logsBloom :: String + , receipts :: [EVMToolReceipt] + , currentDifficulty :: String + , gasUsed :: String + , rejected :: Maybe [EVMRejected] + } deriving (Generic, Show) + +instance JSON.FromJSON EVMToolResult + +data EVMRejected = + EVMRejected + { index :: Int + , err :: String + } deriving (Generic, Show) + +instance JSON.FromJSON EVMRejected where + parseJSON = JSON.withObject "EVMRejected" $ \v -> EVMRejected + <$> v .: "index" + <*> v .: "error" + +data EVMToolAlloc = + EVMToolAlloc + { balance :: W256 + , code :: ByteString + , nonce :: W64 + } deriving (Generic) + +instance JSON.ToJSON EVMToolAlloc where + toJSON b = JSON.object [ ("balance" , (JSON.toJSON $ show b.balance)) + , ("code", (JSON.toJSON $ ByteStringS b.code)) + , ("nonce", (JSON.toJSON $ b.nonce)) + ] + +emptyEVMToolAlloc :: EVMToolAlloc +emptyEVMToolAlloc = EVMToolAlloc { balance = 0 + , code = mempty + , nonce = 0 + } +-- Sets up common parts such as TX, origin contract, and environment that can +-- later be used to create & execute either an evmtool (from go-ethereum) or an +-- HEVM transaction. Some elements here are hard-coded such as the secret key, +-- which are currently not being fuzzed. +evmSetup :: OpContract -> ByteString -> Int -> (EVM.Transaction.Transaction, EVMToolEnv, EVMToolAlloc, Addr, Addr, Integer) +evmSetup contr txData gaslimitExec = (txn, evmEnv, contrAlloc, fromAddress, toAddress, sk) + where + contrLits = assemble $ getOpData contr + toW8fromLitB :: Expr 'Byte -> Data.Word.Word8 + toW8fromLitB (LitByte a) = a + toW8fromLitB _ = error "Cannot convert non-litB" + + bitcode = BS.pack . Vector.toList $ toW8fromLitB <$> contrLits + contrAlloc = EVMToolAlloc{ balance = 0xa493d65e20984bc + , code = bitcode + , nonce = 0x48 + } + txn = EVM.Transaction.Transaction + { txData = txData + , txGasLimit = fromIntegral gaslimitExec + , txGasPrice = Just 1 + , txNonce = 172 + , txToAddr = Just 0x8A8eAFb1cf62BfBeb1741769DAE1a9dd47996192 + , txR = 0 -- will be fixed when we sign + , txS = 0 -- will be fixed when we sign + , txV = 0 -- will be fixed when we sign + , txValue = 0 -- setting this > 0 fails because HEVM doesn't handle value sent in toplevel transaction + , txType = EVM.Transaction.EIP1559Transaction + , txAccessList = [] + , txMaxPriorityFeeGas = Just 1 + , txMaxFeePerGas = Just 1 + , txChainId = 1 + } + evmEnv = EVMToolEnv { coinbase = 0xff + , timestamp = Lit 0x3e8 + , number = 0x0 + , prevRandao = 0x0 + , gasLimit = fromIntegral gaslimitExec + , baseFee = 0x0 + , maxCodeSize = 0xfffff + , schedule = FeeSchedule.berlin + , blockHashes = blockHashesDefault + } + sk = 0xDC38EE117CAE37750EB1ECC5CFD3DE8E85963B481B93E732C5D0CB66EE6B0C9D + fromAddress :: Addr + fromAddress = fromJust $ deriveAddr sk + toAddress :: Addr + toAddress = 0x8A8eAFb1cf62BfBeb1741769DAE1a9dd47996192 + +getHEVMRet :: OpContract -> ByteString -> Int -> IO (Either (EVM.Error, [VMTrace]) (Expr 'End, [VMTrace], VMTraceResult)) +getHEVMRet contr txData gaslimitExec = do + let (txn, evmEnv, contrAlloc, fromAddress, toAddress, _) = evmSetup contr txData gaslimitExec + hevmRun <- runCodeWithTrace Nothing evmEnv contrAlloc txn (fromAddress, toAddress) + return hevmRun + +getEVMToolRet :: OpContract -> ByteString -> Int -> IO (Maybe EVMToolResult) +getEVMToolRet contr txData gaslimitExec = do + let (txn, evmEnv, contrAlloc, fromAddress, toAddress, sk) = evmSetup contr txData gaslimitExec + txs = [EVM.Transaction.sign sk txn] + walletAlloc = EVMToolAlloc{ balance = 0x5ffd4878be161d74 + , code = BS.empty + , nonce = 0xac + } + alloc :: Map.Map Addr EVMToolAlloc + alloc = Map.fromList ([ (fromAddress, walletAlloc), (toAddress, contrAlloc)]) + JSON.encodeFile "txs.json" txs + JSON.encodeFile "alloc.json" alloc + JSON.encodeFile "env.json" evmEnv + (exitCode, evmtoolStdout, evmtoolStderr) <- readProcessWithExitCode "evm" [ "transition" + ,"--input.alloc" , "alloc.json" + , "--input.env" , "env.json" + , "--input.txs" , "txs.json" + , "--output.alloc" , "alloc-out.json" + , "--trace.returndata=true" + , "--trace" , "trace.json" + , "--output.result", "result.json" + ] "" + Control.Monad.when (exitCode /= ExitSuccess) $ do + putStrLn $ "evmtool exited with code " <> show exitCode + putStrLn $ "evmtool stderr output:" <> show evmtoolStderr + putStrLn $ "evmtool stdout output:" <> show evmtoolStdout + evmtoolResult <- JSON.decodeFileStrict "result.json" :: IO (Maybe EVMToolResult) + return evmtoolResult + +-- Compares traces of evmtool (from go-ethereum) and HEVM +compareTraces :: [VMTrace] -> [EVMToolTrace] -> IO (Bool) +compareTraces hevmTrace evmTrace = go hevmTrace evmTrace + where + go :: [VMTrace] -> [EVMToolTrace] -> IO (Bool) + go [] [] = pure True + go (a:ax) (b:bx) = do + let aOp = a.traceOp + bOp = b.op + aPc = a.tracePc + bPc = b.pc + aStack = a.traceStack + bStack = b.stack + aGas = fromIntegral a.traceGas + bGas = b.gas + if aGas /= bGas then do + putStrLn "GAS doesn't match:" + putStrLn $ "HEVM's gas : " <> (show aGas) + putStrLn $ "evmtool's gas: " <> (show bGas) + else + -- putStrLn $ "Gas match : " <> (show aGas) + return () + if aOp /= bOp || aPc /= bPc then + putStrLn $ "HEVM: " <> (intToOpName aOp) <> " (pc " <> (show aPc) <> ") --- evmtool " <> (intToOpName bOp) <> " (pc " <> (show bPc) <> ")" + else + -- putStrLn $ "trace element match. " <> (intToOpName aOp) <> " pc: " <> (show aPc) + return () + + Control.Monad.when (isJust b.error) $ do + putStrLn $ "Error by evmtool: " <> (show b.error) + putStrLn $ "Error by HEVM : " <> (show a.traceError) + + Control.Monad.when (aStack /= bStack) $ do + putStrLn "stacks don't match:" + putStrLn $ "HEVM's stack : " <> (show aStack) + putStrLn $ "evmtool's stack: " <> (show bStack) + if aOp == bOp && aStack == bStack && aPc == bPc && aGas == bGas then go ax bx + else pure False + + + go a@(_:_) [] = do + putStrLn $ "Traces don't match. HEVM's trace is longer by:" <> (show a) + pure False + go [] [b] = do + -- evmtool produces ONE more trace element of the error + -- hevm on the other hand stops and doens't produce one more + if isJust b.error then pure True + else do + putStrLn $ "Traces don't match. HEVM's trace is longer by:" <> (show b) + pure False + go [] b@(_:_) = do + putStrLn $ "Traces don't match. evmtool's trace is longer by:" <> (show b) + pure False + +getTraceFileName :: EVMToolResult -> String +getTraceFileName evmtoolResult = traceFileName + where + txName = ((evmtoolResult.receipts) !! 0).transactionHash + traceFileName = "trace-0-" ++ txName ++ ".jsonl" + +getTraceOutput :: Maybe EVMToolResult -> IO (Maybe EVMToolTraceOutput) +getTraceOutput evmtoolResult = + case evmtoolResult of + Nothing -> pure Nothing + Just res -> do + let traceFileName = getTraceFileName res + convertPath <- Paths.getDataFileName "test/scripts/convert_trace_to_json.sh" + (exitcode, _, _) <- readProcessWithExitCode "bash" [convertPath, getTraceFileName res] "" + case exitcode of + ExitSuccess -> JSON.decodeFileStrict (traceFileName ++ ".json") :: IO (Maybe EVMToolTraceOutput) + _ -> pure Nothing + +deleteTraceOutputFiles :: Maybe EVMToolResult -> IO () +deleteTraceOutputFiles evmtoolResult = + case evmtoolResult of + Nothing -> return () + Just res -> do + let traceFileName = getTraceFileName res + System.Directory.removeFile traceFileName + System.Directory.removeFile (traceFileName ++ ".json") + +-- Create symbolic VM from concrete VM +symbolify :: VM -> VM +symbolify vm = vm { _state = vm._state { _calldata = AbstractBuf "calldata" } } + +-- | Takes a runtime code and calls it with the provided calldata +-- Uses evmtool's alloc and transaction to set up the VM correctly +runCodeWithTrace :: Fetch.RpcInfo -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction -> (Addr, Addr) -> IO (Either (EVM.Error, [VMTrace]) ((Expr 'End, [VMTrace], VMTraceResult))) +runCodeWithTrace rpcinfo evmEnv alloc txn (fromAddr, toAddress) = withSolvers Z3 0 Nothing $ \solvers -> do + let origVM = vmForRuntimeCode code' calldata' evmEnv alloc txn (fromAddr, toAddress) + calldata' = ConcreteBuf txn.txData + code' = alloc.code + buildExpr :: SolverGroup -> VM -> IO (Expr End) + buildExpr s vm = evalStateT (interpret (Fetch.oracle s Nothing) Nothing Nothing runExpr) vm + + expr <- buildExpr solvers $ symbolify origVM + (res, (vm, trace)) <- runStateT (interpretWithTrace (Fetch.oracle solvers rpcinfo) Stepper.execFully) (origVM, []) + case res of + Left x -> pure $ Left (x, trace) + Right _ -> pure $ Right (expr, trace, vmres vm) + +vmForRuntimeCode :: ByteString -> Expr Buf -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction -> (Addr, Addr) -> VM +vmForRuntimeCode runtimecode calldata' evmToolEnv alloc txn (fromAddr, toAddress) = + let contr = initialContract (RuntimeCode (ConcreteRuntimeCode runtimecode)) + contrWithBal = contr { _balance = alloc.balance } + in + (makeVm $ VMOpts + { vmoptContract = contrWithBal + , vmoptCalldata = (calldata', []) + , vmoptValue = Lit txn.txValue + , vmoptStorageBase = Concrete + , vmoptAddress = toAddress + , vmoptCaller = Expr.litAddr fromAddr + , vmoptOrigin = fromAddr + , vmoptCoinbase = evmToolEnv.coinbase + , vmoptNumber = evmToolEnv.number + , vmoptTimestamp = evmToolEnv.timestamp + , vmoptGasprice = fromJust txn.txGasPrice + , vmoptGas = txn.txGasLimit - fromIntegral (EVM.Transaction.txGasCost evmToolEnv.schedule txn) + , vmoptGaslimit = txn.txGasLimit + , vmoptBlockGaslimit = evmToolEnv.gasLimit + , vmoptPrevRandao = evmToolEnv.prevRandao + , vmoptBaseFee = evmToolEnv.baseFee + , vmoptPriorityFee = fromJust txn.txMaxPriorityFeeGas + , vmoptMaxCodeSize = evmToolEnv.maxCodeSize + , vmoptSchedule = evmToolEnv.schedule + , vmoptChainId = txn.txChainId + , vmoptCreate = False + , vmoptTxAccessList = mempty + , vmoptAllowFFI = False + }) & set (EVM.env . contracts . at ethrunAddress) + (Just (initialContract (RuntimeCode (ConcreteRuntimeCode BS.empty)))) + & set (state . calldata) calldata' + +runCode :: Fetch.RpcInfo -> ByteString -> Expr Buf -> IO (Maybe (Expr Buf)) +runCode rpcinfo code' calldata' = withSolvers Z3 0 Nothing $ \solvers -> do + let origVM = vmForRuntimeCode code' calldata' emptyEvmToolEnv emptyEVMToolAlloc EVM.Transaction.emptyTransaction (ethrunAddress, createAddress ethrunAddress 1) + res <- evalStateT (Stepper.interpret (Fetch.oracle solvers rpcinfo) Stepper.execFully) origVM + pure $ case res of + Left _ -> Nothing + Right b -> Just b + +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 = Control.Lens.view (f . g) vm + memsize = the state memorySize + in VMTrace { tracePc = the state EVM.pc + , traceOp = num $ getOp vm + , traceGas = the state EVM.gas + , traceMemSize = memsize + -- increment to match geth format + , traceDepth = 1 + length (Control.Lens.view frames vm) + -- reverse to match geth format + , traceStack = reverse $ forceLit <$> the state EVM.stack + , traceError = readoutError vm._result + } + where + readoutError :: Maybe VMResult -> Maybe String + readoutError Nothing = Nothing + readoutError (Just (VMSuccess _)) = Nothing + readoutError (Just (VMFailure e)) = case e of + -- NOTE: error text made to closely match go-ethereum's errors.go file + OutOfGas {} -> Just "out of gas" + -- TODO "contract creation code storage out of gas" not handled + CallDepthLimitReached -> Just "max call depth exceeded" + BalanceTooLow {} -> Just "insufficient balance for transfer" + -- TODO "contract address collision" not handled + EVM.Revert {} -> Just "execution reverted" + -- TODO "max initcode size exceeded" not handled + MaxCodeSizeExceeded {} -> Just "max code size exceeded" + EVM.BadJumpDestination -> Just "invalid jump destination" + StateChangeWhileStatic -> Just "write protection" + ReturnDataOutOfBounds -> Just "return data out of bounds" + EVM.IllegalOverflow -> Just "gas uint64 overflow" + UnrecognizedOpcode op -> Just $ "invalid opcode: " <> show op + EVM.NonceOverflow -> Just "nonce uint64 overflow" + EVM.StackUnderrun -> Just "stack underflow" + EVM.StackLimitExceeded -> Just "stack limit reached" + EVM.InvalidMemoryAccess -> Just "write protection" + err -> Just $ "HEVM error: " <> show err + +vmres :: VM -> VMTraceResult +vmres vm = + let + gasUsed' = Control.Lens.view (tx . txgaslimit) vm - Control.Lens.view (state . EVM.gas) vm + res = case Control.Lens.view result vm of + Just (VMSuccess (ConcreteBuf b)) -> (ByteStringS b) + Just (VMSuccess x) -> error $ "unhandled: " <> (show x) + Just (VMFailure (EVM.Revert (ConcreteBuf b))) -> (ByteStringS b) + Just (VMFailure _) -> ByteStringS mempty + _ -> ByteStringS mempty + in VMTraceResult + { out = res + , gasUsed = gasUsed' + } + +type TraceState = (VM, [VMTrace]) + +execWithTrace :: StateT TraceState IO VMResult +execWithTrace = do + _ <- runWithTrace + fromJust <$> use (_1 . result) + +runWithTrace :: StateT TraceState IO VM +runWithTrace = do + -- This is just like `exec` except for every instruction evaluated, + -- we also increment a counter indexed by the current code location. + vm0 <- use _1 + case vm0._result of + Nothing -> do + State.modify (\(a, b) -> (a, b ++ [vmtrace vm0])) + zoom _1 (State.state (runState exec1)) + runWithTrace + Just (VMSuccess _) -> pure vm0 + Just (VMFailure _) -> do + -- Update error text for last trace element + (a, b) <- State.get + let updatedElem = (last b) {traceError = (vmtrace vm0).traceError} + updatedTraces = take ((Data.List.length b)-1) b ++ [updatedElem] + State.put (a, updatedTraces) + pure vm0 + +interpretWithTrace + :: Fetch.Fetcher + -> Stepper.Stepper a + -> StateT TraceState IO a +interpretWithTrace fetcher = + eval . Operational.view + + where + eval + :: Operational.ProgramView Stepper.Action a + -> StateT TraceState IO a + + eval (Operational.Return x) = + pure x + + eval (action Operational.:>>= k) = + case action of + Stepper.Exec -> + execWithTrace >>= interpretWithTrace fetcher . k + Stepper.Run -> + runWithTrace >>= interpretWithTrace fetcher . k + Stepper.Wait q -> + do m <- liftIO (fetcher q) + zoom _1 (State.state (runState m)) >> interpretWithTrace fetcher (k ()) + Stepper.Ask _ -> + error "cannot make choice in this interpreter" + Stepper.IOAct q -> + zoom _1 (StateT (runStateT q)) >>= interpretWithTrace fetcher . k + Stepper.EVM m -> + zoom _1 (State.state (runState m)) >>= interpretWithTrace fetcher . k + +data OpContract = OpContract [Op] +instance Show OpContract where + show (OpContract a) = "OpContract " ++ (show a) + +getOpData :: OpContract-> [Op] +getOpData (OpContract x) = x + +instance Arbitrary OpContract where + arbitrary = fmap OpContract (sized genContract) + +removeExtcalls :: OpContract -> OpContract +removeExtcalls (OpContract ops) = OpContract (filter (noStorageNoExtcalls) ops) + where + noStorageNoExtcalls :: Op -> Bool + noStorageNoExtcalls o = case o of + -- Extrenal info functions + OpExtcodecopy -> False + OpExtcodehash -> False + OpExtcodesize -> False + OpAddress -> False + OpOrigin -> False + OpCaller -> False + OpCoinbase -> False + OpCreate -> False + OpCreate2 -> False + -- External call functions + OpDelegatecall -> False + OpStaticcall -> False + OpCall -> False + OpCallcode -> False + -- Not interesting + OpBalance -> False + OpSelfdestruct -> False + _ -> True + +getJumpDests :: [Op] -> [Int] +getJumpDests ops = go ops 0 [] + where + go :: [Op] -> Int -> [Int] -> [Int] + go [] _ dests = dests + go (a:ax) pos dests = case a of + OpJumpdest -> go ax (pos+1) (pos:dests) + OpPush _ -> go ax (pos+33) dests + -- We'll fix these up later to add a Push in between, hence they are 34 bytes + OpJump -> go ax (pos+34) dests + OpJumpi -> go ax (pos+34) dests + -- everything else is 1 byte + _ -> go ax (pos+1) dests + +fixContractJumps :: OpContract -> IO OpContract +fixContractJumps (OpContract ops) = do + let + addedOps = ops++[OpJumpdest] + jumpDests = getJumpDests addedOps + -- always end on an OpJumpdest so we don't have an issue with a "later" position + ops2 = fixup addedOps 0 [] + -- original set of operations, the set of jumpDests NOW valid, current position, return value + fixup :: [Op] -> Int -> [Op] -> IO [Op] + fixup [] _ ret = pure ret + fixup (a:ax) pos ret = case a of + OpJumpi -> do + let filtDests = (filter (> pos) jumpDests) + rndPos <- randItem filtDests + fixup ax (pos+34) (ret++[(OpPush (Lit (fromInteger (fromIntegral rndPos)))), (OpJumpi)]) + OpJump -> do + let filtDests = (filter (> pos) jumpDests) + rndPos <- randItem filtDests + fixup ax (pos+34) (ret++[(OpPush (Lit (fromInteger (fromIntegral rndPos)))), (OpJump)]) + myop@(OpPush _) -> fixup ax (pos+33) (ret++[myop]) + myop -> fixup ax (pos+1) (ret++[myop]) + fmap OpContract ops2 + +genPush :: Int -> Gen [Op] +genPush n = vectorOf n onePush + where + onePush :: Gen Op + onePush = do + p <- chooseInt (1, 10) + pure $ OpPush (Lit (fromIntegral p)) + +genContract :: Int -> Gen [Op] +genContract n = do + y <- chooseInt (3, 6) + pushes <- genPush y + normalOps <- vectorOf (3*n+40) genOne + addReturn <- chooseInt (0, 10) + let contr = pushes ++ normalOps + if addReturn < 10 then pure $ contr++[OpPush (Lit 0x40), OpPush (Lit 0x0), OpReturn] + else pure contr + where + genOne :: Gen Op + genOne = frequency [ + -- math ops + (200, frequency [ + (1, pure OpAdd) + , (1, pure OpMul) + , (1, pure OpSub) + , (1, pure OpDiv) + , (1, pure OpSdiv) + , (1, pure OpMod) + , (1, pure OpSmod) + , (1, pure OpAddmod) + , (1, pure OpMulmod) + , (1, pure OpExp) + , (1, pure OpSignextend) + , (1, pure OpLt) + , (1, pure OpGt) + , (1, pure OpSlt) + , (1, pure OpSgt) + , (1, pure OpSha3) + ]) + -- Comparison & binary ops + , (200, frequency [ + (1, pure OpEq) + , (1, pure OpIszero) + , (1, pure OpAnd) + , (1, pure OpOr) + , (1, pure OpXor) + , (1, pure OpNot) + , (1, pure OpByte) + , (1, pure OpShl) + , (1, pure OpShr) + , (1, pure OpSar) + ]) + -- calldata + , (800, pure OpCalldataload) + , (200, pure OpCalldatacopy) + -- Get some info + , (100, frequency [ + (10, pure OpAddress) + , (10, pure OpBalance) + , (10, pure OpOrigin) + , (10, pure OpCaller) + , (10, pure OpCallvalue) + , (10, pure OpCalldatasize) + , (10, pure OpCodesize) + , (10, pure OpGasprice) + , (10, pure OpReturndatasize) + , (10, pure OpReturndatacopy) + , (10, pure OpExtcodehash) + , (10, pure OpBlockhash) + , (10, pure OpCoinbase) + , (10, pure OpTimestamp) + , (10, pure OpNumber) + , (10, pure OpPrevRandao) + , (10, pure OpGaslimit) + , (10, pure OpChainid) + , (10, pure OpSelfbalance) + , (10, pure OpBaseFee) + , (10, pure OpPc) + , (10, pure OpMsize) + , (10, pure OpGas) + , (10, pure OpExtcodesize) + , (10, pure OpCodecopy) + , (10, pure OpExtcodecopy) + ]) + -- memory manip + , (1200, frequency [ + (50, pure OpMload) + , (50, pure OpMstore) + , (1, pure OpMstore8) + ]) + -- storage manip + , (100, frequency [ + (1, pure OpSload) + , (1, pure OpSstore) + ]) + -- Jumping around + , (20, frequency [ + (1, pure OpJump) + , (10, pure OpJumpi) + ]) + -- calling out + , (1, frequency [ + (1, pure OpStaticcall) + , (1, pure OpCall) + , (1, pure OpCallcode) + , (1, pure OpDelegatecall) + , (1, pure OpCreate) + , (1, pure OpCreate2) + , (1, pure OpSelfdestruct) + ]) + -- manipulate stack + , (13000, frequency [ + (1, pure OpPop) + , (400, do + -- x <- arbitrary + large <- chooseInt (0, 100) + x <- if large == 0 then chooseBoundedIntegral (0::W256, (2::W256)^(256::W256)-1) + else chooseBoundedIntegral (0, 10) + pure $ OpPush (Lit (fromIntegral x))) + , (10, do + x <- chooseInt (1, 10) + pure $ OpDup (fromIntegral x)) + , (10, do + x <- chooseInt (1, 10) + pure $ OpSwap (fromIntegral x)) + ])] + -- End states + -- , (1, frequency [ + -- (1, pure OpStop) + -- , (10, pure OpReturn) + -- , (10, pure OpRevert) + -- ]) + +forceLit :: Expr EWord -> W256 +forceLit (Lit x) = x +forceLit _ = undefined + +randItem :: [a] -> IO a +randItem = generate . Test.QuickCheck.elements + +getOp :: VM -> Data.Word.Word8 +getOp vm = + let pcpos = vm ^. state . EVM.pc + code' = vm ^. state . EVM.code + xs = case code' of + InitCode _ _ -> error "InitCode instead of RuntimeCode" + RuntimeCode (ConcreteRuntimeCode xs') -> BS.drop pcpos xs' + RuntimeCode (SymbolicRuntimeCode _) -> error "RuntimeCode is symbolic" + in if xs == BS.empty then 0 + else BS.head xs + +tests :: TestTree +tests = testGroup "contract-quickcheck-run" + [ testProperty "random-contract-concrete-call" $ \(contr :: OpContract) -> ioProperty $ do + txDataRaw <- generate $ sized $ \n -> vectorOf (10*n+5) $ chooseInt (0,255) + gaslimitExec <- generate $ chooseInt (40000, 0xffff) + let txData = BS.pack $ toEnum <$> txDataRaw + -- TODO: By removing external calls, we fuzz less + -- It should work also when we external calls. Removing for now. + contrFixed <- fixContractJumps $ removeExtcalls contr + evmtoolResult <- getEVMToolRet contrFixed txData gaslimitExec + hevmRun <- getHEVMRet contrFixed txData gaslimitExec + (Just evmtoolTraceOutput) <- getTraceOutput evmtoolResult + case hevmRun of + (Right (expr, hevmTrace, hevmTraceResult)) -> do + let + concretize :: Expr a -> Expr Buf -> Expr a + concretize a c = mapExpr go a + where + go :: Expr a -> Expr a + go = \case + AbstractBuf "calldata" -> c + y -> y + concretizedExpr = concretize expr (ConcreteBuf txData) + simplConcExpr = Expr.simplify concretizedExpr + getReturnVal :: Expr End -> Maybe ByteString + getReturnVal (Return _ (ConcreteBuf bs) _) = Just bs + getReturnVal _ = Nothing + simplConcrExprRetval = getReturnVal simplConcExpr + traceOK <- compareTraces hevmTrace (evmtoolTraceOutput.trace) + -- putStrLn $ "HEVM trace : " <> show hevmTrace + -- putStrLn $ "evmtool trace: " <> show (evmtoolTraceOutput.toTrace) + assertEqual "Traces and gas must match" traceOK True + let resultOK = evmtoolTraceOutput.output.output == hevmTraceResult.out + if resultOK then do + putStrLn $ "HEVM & evmtool's outputs match: '" <> (bsToHex $ bssToBs evmtoolTraceOutput.output.output) <> "'" + if isNothing simplConcrExprRetval || (fromJust simplConcrExprRetval) == (bssToBs hevmTraceResult.out) + then do + putStr "OK, symbolic interpretation -> concrete calldata -> Expr.simplify gives the same answer." + if isNothing simplConcrExprRetval then putStrLn ", but it was a Nothing, so not strong equivalence" + else putStrLn "" + else do + putStrLn $ "concretized expr : " <> (show concretizedExpr) + putStrLn $ "simplified concretized expr: " <> (show simplConcExpr) + putStrLn $ "return value computed : " <> (show simplConcrExprRetval) + putStrLn $ "evmtool's return value : " <> (show hevmTraceResult.out) + assertEqual "Simplified, concretized expression must match evmtool's output." True False + else do + putStrLn $ "Name of trace file: " <> (getTraceFileName $ fromJust evmtoolResult) + putStrLn $ "HEVM result :" <> (show hevmTraceResult) + T.putStrLn $ "HEVM result: " <> (formatBinary $ bssToBs hevmTraceResult.out) + T.putStrLn $ "evm result : " <> (formatBinary $ bssToBs evmtoolTraceOutput.output.output) + putStrLn $ "HEVM result len: " <> (show (BS.length $ bssToBs hevmTraceResult.out)) + putStrLn $ "evm result len: " <> (show (BS.length $ bssToBs evmtoolTraceOutput.output.output)) + assertEqual "Contract exec successful. HEVM & evmtool's outputs must match" resultOK True + Left (evmerr, hevmTrace) -> do + putStrLn $ "HEVM contract exec issue: " <> (show evmerr) + -- putStrLn $ "evmtool result was: " <> show (fromJust evmtoolResult) + -- putStrLn $ "output by evmtool is: '" <> bsToHex evmtoolTraceOutput.toOutput.output <> "'" + traceOK <- compareTraces hevmTrace (evmtoolTraceOutput.trace) + assertEqual "Traces and gas must match" traceOK True + System.Directory.removeFile "txs.json" + System.Directory.removeFile "alloc-out.json" + System.Directory.removeFile "alloc.json" + System.Directory.removeFile "result.json" + System.Directory.removeFile "env.json" + deleteTraceOutputFiles evmtoolResult + ] + diff --git a/test/scripts/convert_trace_to_json.sh b/test/scripts/convert_trace_to_json.sh new file mode 100644 --- /dev/null +++ b/test/scripts/convert_trace_to_json.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +num=$(wc -l "$1" | cut -d " " -f 1) +awk -v ll="$num" 'BEGIN {print "{\"trace\": [" } {if (NR!=ll) {print $0; if (NR!=ll-1) {print ","}} else {print "], \"output\":" $0}} END{print "}"}' "$1" > "$1.json" diff --git a/test/test.hs b/test/test.hs --- a/test/test.hs +++ b/test/test.hs @@ -1,7 +1,7 @@ -{-# Language GADTs #-} -{-# Language NumericUnderscores #-} {-# Language QuasiQuotes #-} {-# Language DataKinds #-} +{-# Language DuplicateRecordFields #-} +{-# LANGUAGE DeriveGeneric #-} module Main where @@ -9,8 +9,8 @@ import Data.ByteString (ByteString) import Data.Bits hiding (And, Xor) import System.Directory +import System.IO import GHC.Natural -import Control.Monad import Text.RE.TDFA.String import Text.RE.Replace import Data.Time @@ -19,10 +19,10 @@ import Prelude hiding (fail, LT, GT) import qualified Data.ByteString as BS -import qualified Data.ByteString.Base16 as Hex +import qualified Data.ByteString.Base16 as BS16 import Data.Maybe import Data.Typeable -import Data.List (elemIndex) +import Data.List qualified (elemIndex) import Data.DoubleWord import Test.Tasty import Test.Tasty.QuickCheck hiding (Failure) @@ -32,9 +32,10 @@ import Test.Tasty.HUnit import Test.Tasty.Runners hiding (Failure) import Test.Tasty.ExpectedFailure +import EVM.Tracing qualified -import Control.Monad.State.Strict (execState, runState) -import Control.Lens hiding (List, pre, (.>), re) +import Control.Monad.State.Strict hiding (state) +import Control.Lens hiding (List, pre, (.>), re, op) import qualified Data.Vector as Vector import Data.String.Here @@ -43,7 +44,7 @@ import Data.Binary.Put (runPut) import Data.Binary.Get (runGetOrFail) -import EVM +import EVM hiding (allowFFI) import EVM.SymExec import EVM.ABI import EVM.Exec @@ -72,7 +73,9 @@ tests :: TestTree tests = testGroup "hevm" - [ testGroup "StorageTests" + [ + EVM.Tracing.tests + , testGroup "StorageTests" [ testCase "read-from-sstore" $ assertEqual "" (Lit 0xab) (Expr.readStorage' (Lit 0x0) (Lit 0x0) (SStore (Lit 0x0) (Lit 0x0) (Lit 0xab) AbstractStore)) @@ -355,29 +358,37 @@ , testProperty "abi encoding vs. solidity" $ withMaxSuccess 20 $ forAll (arbitrary >>= genAbiValue) $ \y -> ioProperty $ do - -- traceM ("encoding: " ++ (show y) ++ " : " ++ show (abiValueType y)) Just encoded <- runStatements [i| x = abi.encode(a);|] [y] AbiBytesDynamicType let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of AbiTuple (Vector.toList -> [e]) -> e _ -> error "AbiTuple expected" let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [y]) - -- traceM ("encoded (solidity): " ++ show solidityEncoded) - -- traceM ("encoded (hevm): " ++ show (AbiBytesDynamic hevmEncoded)) assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded) , testProperty "abi encoding vs. solidity (2 args)" $ withMaxSuccess 20 $ forAll (arbitrary >>= bothM genAbiValue) $ \(x', y') -> ioProperty $ do - -- traceM ("encoding: " ++ (show x') ++ ", " ++ (show y') ++ " : " ++ show (abiValueType x') ++ ", " ++ show (abiValueType y')) Just encoded <- runStatements [i| x = abi.encode(a, b);|] [x', y'] AbiBytesDynamicType let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of AbiTuple (Vector.toList -> [e]) -> e _ -> error "AbiTuple expected" let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [x',y']) - -- traceM ("encoded (solidity): " ++ show solidityEncoded) - -- traceM ("encoded (hevm): " ++ show (AbiBytesDynamic hevmEncoded)) assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded) + + -- we need a separate test for this because the type of a function is "function() external" in solidity but just "function" in the abi: + , testProperty "abi encoding vs. solidity (function pointer)" $ withMaxSuccess 20 $ forAll (genAbiValue AbiFunctionType) $ + \y -> ioProperty $ do + Just encoded <- runFunction [i| + function foo(function() external a) public pure returns (bytes memory x) { + x = abi.encode(a); + } + |] (abiMethod "foo(function)" (AbiTuple (Vector.singleton y))) + let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of + AbiTuple (Vector.toList -> [e]) -> e + _ -> error "AbiTuple expected" + let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [y]) + assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded) ] , testGroup "Precompiled contracts" @@ -456,7 +467,7 @@ (json, path') <- solidity' srccode let (solc', _, _) = fromJust $ readJSON json initCode :: ByteString - initCode = (fromJust $ solc' ^? ix (path' <> ":A")).creationCode + initCode = (solc' ^?! ix (path' <> ":A")).creationCode -- add constructor arguments assertEqual "constructor args screwed up metadata stripping" (stripBytecodeMetadata (initCode <> encodeAbiValue (AbiUInt 256 1))) (stripBytecodeMetadata initCode) ] @@ -499,7 +510,7 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts assertEqual "Must be 0" 0 $ getVar ctr "arg1" putStrLn $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1") , @@ -512,7 +523,7 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x11] c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x11] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts let x = getVar ctr "arg1" let y = getVar ctr "arg2" @@ -529,10 +540,22 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x12] c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x12] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts assertEqual "Division by 0 needs b=0" (getVar ctr "arg2") 0 putStrLn "expected counterexample found" , + testCase "unused-args-fail" $ do + Just c <- solcRuntime "C" + [i| + contract C { + function fun(uint256 a) public pure { + assert(false); + } + } + |] + (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] debugVeriOpts + putStrLn "expected counterexample found" + , testCase "enum-conversion-fail" $ do Just c <- solcRuntime "MyContract" [i| @@ -543,7 +566,7 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x21] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x21] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts assertBool "Enum is only defined for 0 and 1" $ (getVar ctr "arg1") > 1 putStrLn "expected counterexample found" , @@ -564,7 +587,7 @@ } } |] - a <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x31] c (Just ("fun(uint8)", [AbiUIntType 8])) [] defaultVeriOpts + a <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x31] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts print $ length a print $ show a putStrLn "expected counterexample found" @@ -581,8 +604,8 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x32] c (Just ("fun(uint8)", [AbiUIntType 8])) [] defaultVeriOpts - assertBool "Access must be beyond element 2" $ (getVar ctr "arg1") > 1 + (_, [Cex (_, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x32] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts + -- assertBool "Access must be beyond element 2" $ (getVar ctr "arg1") > 1 putStrLn "expected counterexample found" , -- TODO the system currently does not allow for symbolic array size allocation @@ -595,7 +618,7 @@ } } |] - (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x41] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x41] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "expected counterexample found" , -- TODO the system currently does not allow for symbolic JUMP @@ -615,7 +638,7 @@ } } |] - (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x51] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x51] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "expected counterexample found" ] @@ -675,7 +698,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256)", [AbiIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256)" [AbiIntType 256])) [] defaultVeriOpts putStrLn "Require works as expected" , testCase "ITE-with-bitwise-AND" $ do @@ -695,7 +718,7 @@ } |] -- should find a counterexample - (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "expected counterexample found" , testCase "ITE-with-bitwise-OR" $ do @@ -713,7 +736,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "this should always be true, due to bitwise OR with positive value" , -- CopySlice check @@ -747,7 +770,7 @@ , askSmtIters = Nothing , rpcInfo = Nothing } - calldata' = Just ("checkval(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256]) + calldata' = Just (Sig "checkval(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256]) (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c calldata' [] opts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" @@ -767,7 +790,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256,int256)", [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts putStrLn "SAR works as expected" , testCase "opcode-sar-pos" $ do @@ -784,7 +807,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256,int256)", [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts putStrLn "SAR works as expected" , testCase "opcode-sar-fixedval-pos" $ do @@ -801,7 +824,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256,int256)", [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts putStrLn "SAR works as expected" , testCase "opcode-sar-fixedval-neg" $ do @@ -818,7 +841,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256,int256)", [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts putStrLn "SAR works as expected" , testCase "opcode-div-zero-1" $ do @@ -835,7 +858,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "sdiv works as expected" , testCase "opcode-div-zero-2" $ do @@ -852,7 +875,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "sdiv works as expected" , testCase "opcode-sdiv-zero-1" $ do @@ -869,7 +892,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "sdiv works as expected" , testCase "opcode-sdiv-zero-2" $ do @@ -886,9 +909,22 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "sdiv works as expected" , + testCase "signed-overflow-checks" $ do + Just c <- solcRuntime "C" + [i| + contract C { + function fun(uint160 a) external { + int256 j = int256(uint256(a)) + 1; + assert(false); + } + } + |] + (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint160)" [AbiUIntType 160])) [] defaultVeriOpts + putStrLn "expected cex discovered" + , testCase "opcode-signextend-neg" $ do Just c <- solcRuntime "MyContract" [i| @@ -908,7 +944,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "signextend works as expected" , testCase "opcode-signextend-pos-nochop" $ do @@ -926,7 +962,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint8)", [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts putStrLn "signextend works as expected" , testCase "opcode-signextend-pos-chopped" $ do @@ -944,7 +980,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint8)", [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts putStrLn "signextend works as expected" , -- when b is too large, value is unchanged @@ -962,7 +998,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint8)", [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts putStrLn "signextend works as expected" , testCase "opcode-shl" $ do @@ -980,7 +1016,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts putStrLn "SAR works as expected" , testCase "opcode-xor-cancel" $ do @@ -997,7 +1033,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts putStrLn "XOR works as expected" , testCase "opcode-xor-reimplement" $ do @@ -1013,7 +1049,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts putStrLn "XOR works as expected" , testCase "opcode-addmod-no-overflow" $ do @@ -1036,7 +1072,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint8,uint8,uint8)", [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint8,uint8,uint8)" [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts putStrLn "ADDMOD is fine on NON overflow values" , testCase "opcode-mulmod-no-overflow" $ do @@ -1059,7 +1095,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint8,uint8,uint8)", [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint8,uint8,uint8)" [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts putStrLn "MULMOD is fine on NON overflow values" , testCase "opcode-div-res-zero-on-div-by-zero" $ do @@ -1076,7 +1112,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint16)", [AbiUIntType 16])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] defaultVeriOpts putStrLn "DIV by zero is zero" , -- Somewhat tautological since we are asserting the precondition @@ -1094,15 +1130,16 @@ [x', y'] -> (x', y') _ -> error "expected 2 args" in (x .<= Expr.add x y) + -- TODO check if it's needed .&& view (state . callvalue) preVM .== Lit 0 post prestate leaf = let (x, y) = case getStaticAbiArgs 2 prestate of [x', y'] -> (x', y') _ -> error "expected 2 args" in case leaf of - Return _ b _ -> (ReadWord (Lit 0) b) .== (Add x y) + EVM.Types.Return _ b _ -> (ReadWord (Lit 0) b) .== (Add x y) _ -> PBool True - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , @@ -1120,16 +1157,16 @@ _ -> error "expected 2 args" in (x .<= Expr.add x y) .&& (x .== y) - .&& view (state . callvalue) preVM .== Lit 0 + .&& Control.Lens.view (state . callvalue) preVM .== Lit 0 post prestate leaf = let (_, y) = case getStaticAbiArgs 2 prestate of [x', y'] -> (x', y') _ -> error "expected 2 args" in case leaf of - Return _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y) + EVM.Types.Return _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y) _ -> PBool True (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> - verifyContract s safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) + verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , testCase "summary storage writes" $ do @@ -1145,17 +1182,17 @@ } } |] - let pre vm = Lit 0 .== view (state . callvalue) vm + let pre vm = Lit 0 .== Control.Lens.view (state . callvalue) vm post prestate leaf = let y = case getStaticAbiArgs 1 prestate of [y'] -> y' _ -> error "expected 1 arg" - this = Expr.litAddr $ view (state . codeContract) prestate - prex = Expr.readStorage' this (Lit 0) (view (env . storage) prestate) + this = Expr.litAddr $ Control.Lens.view (state . codeContract) prestate + prex = Expr.readStorage' this (Lit 0) (Control.Lens.view (EVM.env . EVM.storage) prestate) in case leaf of - Return _ _ postStore -> Expr.add prex (Expr.mul (Lit 2) y) .== (Expr.readStorage' this (Lit 0) postStore) + EVM.Types.Return _ _ postStore -> Expr.add prex (Expr.mul (Lit 2) y) .== (Expr.readStorage' this (Lit 0) postStore) _ -> PBool True - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just ("f(uint256)", [AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , -- tests how whiffValue handles Neg via application of the triple IsZero simplification rule @@ -1180,7 +1217,7 @@ } |] Just c <- yulRuntime "Neg" src - (res, [Qed _]) <- withSolvers Z3 4 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("hello(address)", [AbiAddressType])) [] defaultVeriOpts + (res, [Qed _]) <- withSolvers Z3 4 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "hello(address)" [AbiAddressType])) [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , testCase "catch-storage-collisions-noproblem" $ do @@ -1199,22 +1236,22 @@ } } |] - let pre vm = (Lit 0) .== view (state . callvalue) vm + let pre vm = (Lit 0) .== Control.Lens.view (state . callvalue) vm post prestate poststate = let (x,y) = case getStaticAbiArgs 2 prestate of [x',y'] -> (x',y') _ -> error "expected 2 args" - this = Expr.litAddr $ view (state . codeContract) prestate - prestore = view (env . storage) prestate + this = Expr.litAddr $ Control.Lens.view (state . codeContract) prestate + prestore = Control.Lens.view (EVM.env . EVM.storage) prestate prex = Expr.readStorage' this x prestore prey = Expr.readStorage' this y prestore in case poststate of - Return _ _ poststore -> let + EVM.Types.Return _ _ poststore -> let postx = Expr.readStorage' this x poststore posty = Expr.readStorage' this y poststore in Expr.add prex prey .== Expr.add postx posty _ -> PBool True - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) putStrLn "Correct, this can never fail" , -- Inspired by these `msg.sender == to` token bugs @@ -1233,22 +1270,22 @@ } } |] - let pre vm = (Lit 0) .== view (state . callvalue) vm + let pre vm = (Lit 0) .== Control.Lens.view (state . callvalue) vm post prestate poststate = let (x,y) = case getStaticAbiArgs 2 prestate of [x',y'] -> (x',y') _ -> error "expected 2 args" - this = Expr.litAddr $ view (state . codeContract) prestate - prestore = view (env . storage) prestate + this = Expr.litAddr $ Control.Lens.view (state . codeContract) prestate + prestore = Control.Lens.view (EVM.env . EVM.storage) prestate prex = Expr.readStorage' this x prestore prey = Expr.readStorage' this y prestore in case poststate of - Return _ _ poststore -> let + EVM.Types.Return _ _ poststore -> let postx = Expr.readStorage' this x poststore posty = Expr.readStorage' this y poststore in Expr.add prex prey .== Expr.add postx posty _ -> PBool True - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post) let x = getVar ctr "arg1" let y = getVar ctr "arg2" putStrLn $ "y:" <> show y @@ -1265,7 +1302,7 @@ } } |] - (_, [Cex (l, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo()", [])) [] defaultVeriOpts + (_, [Cex (l, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo()" [])) [] defaultVeriOpts assertEqual "incorrect revert msg" l (EVM.Types.Revert [] (ConcreteBuf $ panicMsg 0x01)) , testCase "simple-assert-2" $ do @@ -1277,7 +1314,7 @@ } } |] - (_, [(Cex (_, ctr))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [(Cex (_, ctr))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts assertEqual "Must be 10" 10 $ getVar ctr "arg1" putStrLn "Got 10 Cex, as expected" , @@ -1291,9 +1328,9 @@ } } |] - (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts let ints = map (flip getVar "arg1") [a,b] - assertBool "0 must be one of the Cex-es" $ isJust $ elemIndex 0 ints + assertBool "0 must be one of the Cex-es" $ isJust $ Data.List.elemIndex 0 ints putStrLn "expected 2 counterexamples found, one Cex is the 0 value" , testCase "assert-fail-notequal" $ do @@ -1306,7 +1343,7 @@ } } |] - (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts let x = getVar a "arg1" let y = getVar b "arg1" assertBool "At least one has to be 0, to go through the first assert" (x == 0 || y == 0) @@ -1322,7 +1359,7 @@ } } |] - (_, [Cex _, Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex _, Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts putStrLn "expected 2 counterexamples found" , testCase "assert-2nd-arg" $ do @@ -1334,7 +1371,7 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts assertEqual "Must be 666" 666 $ getVar ctr "arg2" putStrLn "Found arg2 Ctx to be 666" , @@ -1351,7 +1388,7 @@ } } |] - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , -- We zero out everything but the LSB byte. However, byte(31,x) takes the LSB byte @@ -1368,7 +1405,7 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts assertBool "last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff) > 0 putStrLn "Expected counterexample found" , @@ -1386,7 +1423,7 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts assertBool "second to last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff00) > 0 putStrLn "Expected counterexample found" , @@ -1405,7 +1442,7 @@ } } |] - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , -- Bitwise OR operation test @@ -1421,7 +1458,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "When OR-ing with full 1's we should get back full 1's" , -- Bitwise OR operation test @@ -1438,7 +1475,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "When OR-ing with a byte of 1's, we should get 1's back there" , testCase "Deposit contract loop (z3)" $ do @@ -1460,7 +1497,7 @@ } } |] - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "deposit(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , testCase "Deposit-contract-loop-error-version" $ do @@ -1482,7 +1519,7 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s allPanicCodes c (Just ("deposit(uint8)", [AbiUIntType 8])) [] defaultVeriOpts + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s allPanicCodes c (Just (Sig "deposit(uint8)" [AbiUIntType 8])) [] defaultVeriOpts assertEqual "Must be 255" 255 $ getVar ctr "arg1" putStrLn $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1") , @@ -1544,7 +1581,7 @@ } } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn "div/mod/sdiv/smod by zero works as expected during constant propagation" , testCase "check-asm-byte-oob" $ do @@ -1571,7 +1608,7 @@ } } |] - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , testCase "injectivity of keccak all pairs (32 bytes)" $ do @@ -1589,7 +1626,7 @@ } } |] - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , testCase "injectivity of keccak contrapositive (32 bytes)" $ do @@ -1602,7 +1639,7 @@ } } |] - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , testCase "injectivity of keccak (64 bytes)" $ do @@ -1614,7 +1651,7 @@ } } |] - (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) [] defaultVeriOpts + (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256,uint256,uint256)" (replicate 4 (AbiUIntType 256)))) [] defaultVeriOpts let x = getVar ctr "arg1" let y = getVar ctr "arg2" let w = getVar ctr "arg3" @@ -1623,7 +1660,7 @@ assertEqual "w==z for hash collision" w z putStrLn "expected counterexample found" , - expectFail $ testCase "calldata beyond calldatasize is 0 (z3)" $ do + testCase "calldata beyond calldatasize is 0 (symbolic calldata)" $ do Just c <- solcRuntime "A" [i| contract A { @@ -1640,6 +1677,43 @@ (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , + testCase "calldata beyond calldatasize is 0 (concrete dalldata prefix)" $ do + Just c <- solcRuntime "A" + [i| + contract A { + function f(uint256 z) public pure { + uint y; + assembly { + let x := calldatasize() + y := calldataload(x) + } + assert(y == 0); + } + } + |] + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts + putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" + , + testCase "calldata symbolic access" $ do + Just c <- solcRuntime "A" + [i| + contract A { + function f(uint256 z) public pure { + uint x; uint y; + assembly { + y := calldatasize() + } + require(z >= y); + assembly { + x := calldataload(z) + } + assert(x == 0); + } + } + |] + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts + putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" + , testCase "keccak soundness" $ do Just c <- solcRuntime "C" [i| @@ -1653,7 +1727,7 @@ |] -- should find a counterexample - (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts putStrLn "expected counterexample found" , testCase "multiple-contracts" $ do @@ -1676,10 +1750,10 @@ Just c <- solcRuntime "C" code' Just a <- solcRuntime "A" code' (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $ \s -> do - let vm0 = abstractVM (Just ("call_A()", [])) [] c Nothing SymbolicS + let vm0 = abstractVM (mkCalldata (Just (Sig "call_A()" [])) []) c Nothing SymbolicS let vm = vm0 & set (state . callvalue) (Lit 0) - & over (env . contracts) + & over (EVM.env . contracts) (Map.insert aAddr (initialContract (RuntimeCode (ConcreteRuntimeCode a)))) verify s defaultVeriOpts vm (Just $ checkAssertions defaultPanicCodes) @@ -1713,7 +1787,7 @@ uint public x; } |] - (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("call_A()", [])) [] defaultVeriOpts + (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "call_A()" [])) [] defaultVeriOpts putStrLn "expected counterexample found" , testCase "keccak concrete and sym agree" $ do @@ -1727,7 +1801,7 @@ } } |] - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("kecc(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "kecc(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , testCase "keccak concrete and sym injectivity" $ do @@ -1739,12 +1813,12 @@ } } |] - (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" , ignoreTest $ testCase "safemath distributivity (yul)" $ do let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b" - let vm = abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] yulsafeDistributivity Nothing SymbolicS + let vm = abstractVM (mkCalldata (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) []) yulsafeDistributivity Nothing SymbolicS (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verify s defaultVeriOpts vm (Just $ checkAssertions defaultPanicCodes) putStrLn "Proven" , @@ -1770,7 +1844,7 @@ } |] - (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts + (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts putStrLn "Proven" , testCase "storage-cex-1" $ do @@ -1784,7 +1858,7 @@ } } |] - (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts let addr = W256 $ num $ createAddress ethrunAddress 1 testCex = Map.size cex.store == 1 && case Map.lookup addr cex.store of @@ -1807,7 +1881,7 @@ } } |] - (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts + (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts let addr = W256 $ num $ createAddress ethrunAddress 1 a = getVar cex "arg1" testCex = Map.size cex.store == 1 && @@ -1831,7 +1905,7 @@ } } |] - (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts ConcreteS Nothing (Just $ checkAssertions [0x01]) + (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts ConcreteS Nothing (Just $ checkAssertions [0x01]) let testCex = Map.null cex.store assertBool "Did not find expected storage cex" testCex putStrLn "Expected counterexample found" @@ -1860,7 +1934,7 @@ } |] withSolvers Z3 3 Nothing $ \s -> do - a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts Nothing + a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) assertBool "Must have a difference" (any isCex a) , testCase "eq-sol-exp-qed" $ do @@ -1885,7 +1959,7 @@ } |] withSolvers Z3 3 Nothing $ \s -> do - a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts Nothing + a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) assertEqual "Must have no difference" [Qed ()] a return () , @@ -1913,7 +1987,7 @@ |] withSolvers Z3 3 Nothing $ \s -> do let myVeriOpts = VeriOpts{ simp = True, debug = False, maxIter = Just 2, askSmtIters = Just 2, rpcInfo = Nothing} - a <- equivalenceCheck s aPrgm bPrgm myVeriOpts Nothing + a <- equivalenceCheck s aPrgm bPrgm myVeriOpts (mkCalldata Nothing []) assertEqual "Must be different" (any isCex a) True return () , testCase "eq-all-yul-optimization-tests" $ do @@ -2176,7 +2250,7 @@ Just bPrgm <- yul "" $ T.pack $ unlines filteredBSym procs <- getNumProcessors withSolvers CVC5 (num procs) (Just 100) $ \s -> do - res <- equivalenceCheck s aPrgm bPrgm myVeriOpts Nothing + res <- equivalenceCheck s aPrgm bPrgm myVeriOpts (mkCalldata Nothing []) end <- getCurrentTime case any isCex res of False -> do @@ -2211,7 +2285,9 @@ Sat _ -> False Error _ -> False +-- | Takes a runtime code and calls it with the provided calldata +-- | Takes a creation code and some calldata, runs the creation code, and calls the resulting contract with the provided calldata runSimpleVM :: ByteString -> ByteString -> Maybe ByteString runSimpleVM x ins = case loadVM x of Nothing -> Nothing @@ -2220,23 +2296,24 @@ (VMSuccess (ConcreteBuf bs), _) -> Just bs _ -> Nothing +-- | Takes a creation code and returns a vm with the result of executing the creation code loadVM :: ByteString -> Maybe VM loadVM x = case runState exec (vmForEthrunCreation x) of (VMSuccess (ConcreteBuf targetCode), vm1) -> do - let target = view (state . contract) vm1 + let target = Control.Lens.view (state . contract) vm1 vm2 = execState (replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode targetCode))) vm1 return $ snd $ flip runState vm2 (do resetState - assign (state . gas) 0xffffffffffffffff -- kludge + assign (state . EVM.gas) 0xffffffffffffffff -- kludge loadContract target) _ -> Nothing hex :: ByteString -> ByteString hex s = - case Hex.decode s of + case BS16.decodeBase16 s of Right x -> x - Left e -> error e + Left e -> error $ T.unpack e singleContract :: Text -> Text -> IO (Maybe ByteString) singleContract x s = @@ -2283,7 +2360,7 @@ getStaticAbiArgs :: Int -> VM -> [Expr EWord] getStaticAbiArgs n vm = - let cd = view (state . calldata) vm + let cd = Control.Lens.view (state . calldata) vm in decodeStaticArgs 4 n cd -- includes shaving off 4 byte function sig @@ -2378,13 +2455,13 @@ genEnd :: Int -> Gen (Expr End) genEnd 0 = oneof - [ pure $ Failure [] Invalid + [ pure $ Failure [] EVM.Types.Invalid , pure $ Failure [] EVM.Types.IllegalOverflow - , pure $ Failure [] SelfDestruct + , pure $ Failure [] EVM.Types.SelfDestruct ] genEnd sz = oneof [ fmap (EVM.Types.Revert []) subBuf - , liftM3 Return (return []) subBuf subStore + , liftM3 EVM.Types.Return (return []) subBuf subStore , liftM3 ITE subWord subEnd subEnd ] where