{-# Language OverloadedStrings #-} {-# Language ViewPatterns #-} {-# Language ScopedTypeVariables #-} {-# Language LambdaCase #-} {-# Language QuasiQuotes #-} {-# Language FlexibleInstances #-} {-# Language GeneralizedNewtypeDeriving #-} {-# Language DataKinds #-} {-# Language StandaloneDeriving #-} module Main where import Data.Text (Text) import Data.ByteString (ByteString) import Prelude hiding (fail) import qualified Data.Text as Text import qualified Data.ByteString as BS import qualified Data.ByteString.Lazy as BS (fromStrict) import qualified Data.ByteString.Base16 as Hex import Test.Tasty import Test.Tasty.QuickCheck import Test.Tasty.HUnit import Test.Tasty.Runners import Control.Monad.State.Strict (execState, runState) import Control.Lens hiding (List, pre, (.>)) import qualified Data.Vector as Vector import Data.String.Here import Control.Monad.Fail import Data.Binary.Put (runPut) import Data.SBV hiding ((===), forAll, sList) import Data.SBV.Control import qualified Data.Map as Map import Data.Binary.Get (runGetOrFail) import EVM hiding (Query) import EVM.SymExec import EVM.ABI import EVM.Exec import qualified EVM.Patricia as Patricia import EVM.Precompiled import EVM.RLP import EVM.Solidity import EVM.Types instance MonadFail Query where fail = io . fail main :: IO () main = defaultMain tests -- | run a subset of tests in the repl. p is a tasty pattern: -- https://github.com/UnkindPartition/tasty/tree/ee6fe7136fbcc6312da51d7f1b396e1a2d16b98a#patterns runSubSet :: String -> IO () runSubSet p = defaultMain . applyPattern p $ tests tests :: TestTree tests = testGroup "hevm" [ testGroup "ABI" [ testProperty "Put/get inverse" $ \x -> case runGetOrFail (getAbi (abiValueType x)) (runPut (putAbi x)) of Right ("", _, x') -> x' == x _ -> False ] , testGroup "Solidity expressions" [ testCase "Trivial" $ SolidityCall "x = 3;" [] ===> AbiUInt 256 3 , testCase "Arithmetic" $ do SolidityCall "x = a + 1;" [AbiUInt 256 1] ===> AbiUInt 256 2 SolidityCall "unchecked { x = a - 1; }" [AbiUInt 8 0] ===> AbiUInt 8 255 , testCase "keccak256()" $ SolidityCall "x = uint(keccak256(abi.encodePacked(a)));" [AbiString ""] ===> AbiUInt 256 0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470 , 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 AbiTuple (Vector.toList -> [solidityEncoded]) = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) 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 AbiTuple (Vector.toList -> [solidityEncoded]) = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) 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) ] , testGroup "Precompiled contracts" [ testGroup "Example (reverse)" [ testCase "success" $ assertEqual "example contract reverses" (execute 0xdeadbeef "foobar" 6) (Just "raboof") , testCase "failure" $ assertEqual "example contract fails on length mismatch" (execute 0xdeadbeef "foobar" 5) Nothing ] , testGroup "ECRECOVER" [ testCase "success" $ do let r = hex "c84e55cee2032ea541a32bf6749e10c8b9344c92061724c4e751600f886f4732" s = hex "1542b6457e91098682138856165381453b3d0acae2470286fd8c8a09914b1b5d" v = hex "000000000000000000000000000000000000000000000000000000000000001c" h = hex "513954cf30af6638cb8f626bd3f8c39183c26784ce826084d9d267868a18fb31" a = hex "0000000000000000000000002d5e56d45c63150d937f2182538a0f18510cb11f" assertEqual "successful recovery" (Just a) (execute 1 (h <> v <> r <> s) 32) , testCase "fail on made up values" $ do let r = hex "c84e55cee2032ea541a32bf6749e10c8b9344c92061724c4e751600f886f4731" s = hex "1542b6457e91098682138856165381453b3d0acae2470286fd8c8a09914b1b5d" v = hex "000000000000000000000000000000000000000000000000000000000000001c" h = hex "513954cf30af6638cb8f626bd3f8c39183c26784ce826084d9d267868a18fb31" assertEqual "fail because bit flip" Nothing (execute 1 (h <> v <> r <> s) 32) ] ] , testGroup "Byte/word manipulations" [ testProperty "padLeft length" $ \n (Bytes bs) -> BS.length (padLeft n bs) == max n (BS.length bs) , testProperty "padLeft identity" $ \(Bytes bs) -> padLeft (BS.length bs) bs == bs , testProperty "padRight length" $ \n (Bytes bs) -> BS.length (padLeft n bs) == max n (BS.length bs) , testProperty "padRight identity" $ \(Bytes bs) -> padLeft (BS.length bs) bs == bs , testProperty "padLeft zeroing" $ \(NonNegative n) (Bytes bs) -> let x = BS.take n (padLeft (BS.length bs + n) bs) y = BS.replicate n 0 in x == y ] , testGroup "Unresolved link detection" [ testCase "holes detected" $ do let code' = "608060405234801561001057600080fd5b5060405161040f38038061040f83398181016040528101906100329190610172565b73__$f3cbc3eb14e5bd0705af404abcf6f741ec$__63ab5c1ffe826040518263ffffffff1660e01b81526004016100699190610217565b60206040518083038186803b15801561008157600080fd5b505af4158015610095573d6000803e3d6000fd5b505050506040513d601f19601f820116820180604052508101906100b99190610145565b50506103c2565b60006100d36100ce84610271565b61024c565b9050828152602081018484840111156100ef576100ee610362565b5b6100fa8482856102ca565b509392505050565b600081519050610111816103ab565b92915050565b600082601f83011261012c5761012b61035d565b5b815161013c8482602086016100c0565b91505092915050565b60006020828403121561015b5761015a61036c565b5b600061016984828501610102565b91505092915050565b6000602082840312156101885761018761036c565b5b600082015167ffffffffffffffff8111156101a6576101a5610367565b5b6101b284828501610117565b91505092915050565b60006101c6826102a2565b6101d081856102ad565b93506101e08185602086016102ca565b6101e981610371565b840191505092915050565b60006102016003836102ad565b915061020c82610382565b602082019050919050565b6000604082019050818103600083015261023181846101bb565b90508181036020830152610244816101f4565b905092915050565b6000610256610267565b905061026282826102fd565b919050565b6000604051905090565b600067ffffffffffffffff82111561028c5761028b61032e565b5b61029582610371565b9050602081019050919050565b600081519050919050565b600082825260208201905092915050565b60008115159050919050565b60005b838110156102e85780820151818401526020810190506102cd565b838111156102f7576000848401525b50505050565b61030682610371565b810181811067ffffffffffffffff821117156103255761032461032e565b5b80604052505050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052604160045260246000fd5b600080fd5b600080fd5b600080fd5b600080fd5b6000601f19601f8301169050919050565b7f6261720000000000000000000000000000000000000000000000000000000000600082015250565b6103b4816102be565b81146103bf57600080fd5b50565b603f806103d06000396000f3fe6080604052600080fdfea26469706673582212207d03b26e43dc3d116b0021ddc9817bde3762a3b14315351f11fc4be384fd14a664736f6c63430008060033" assertBool "linker hole not detected" (containsLinkerHole code'), testCase "no false positives" $ do let code' = "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fea265627a7a723158205d775f914dcb471365a430b5f5b2cfe819e615cbbb5b2f1ccc7da1fd802e43c364736f6c634300050b0032" assertBool "false positive" (not . containsLinkerHole $ code') ] , testGroup "metadata stripper" [ testCase "it strips the metadata for solc => 0.6" $ do let code' = hexText "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fea265627a7a723158205d775f914dcb471365a430b5f5b2cfe819e615cbbb5b2f1ccc7da1fd802e43c364736f6c634300050b0032" stripped = stripBytecodeMetadata code' assertEqual "failed to strip metadata" (show (ByteStringS stripped)) "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fe" , testCase "it strips the metadata and constructor args" $ do let srccode = [i| contract A { uint y; constructor(uint x) public { y = x; } } |] (json, path') <- solidity' srccode let Just (solc', _, _) = readJSON json initCode :: ByteString Just initCode = solc' ^? ix (path' <> ":A") . creationCode -- add constructor arguments assertEqual "constructor args screwed up metadata stripping" (stripBytecodeMetadata (initCode <> encodeAbiValue (AbiUInt 256 1))) (stripBytecodeMetadata initCode) ] , testGroup "RLP encodings" [ testProperty "rlp decode is a retraction (bytes)" $ \(Bytes bs) -> -- withMaxSuccess 100000 $ rlpdecode (rlpencode (BS bs)) == Just (BS bs) , testProperty "rlp encode is a partial inverse (bytes)" $ \(Bytes bs) -> -- withMaxSuccess 100000 $ case rlpdecode bs of Just r -> rlpencode r == bs Nothing -> True , testProperty "rlp decode is a retraction (RLP)" $ \(RLPData r) -> -- withMaxSuccess 100000 $ rlpdecode (rlpencode r) == Just r ] , testGroup "Merkle Patricia Trie" [ testProperty "update followed by delete is id" $ \(Bytes r, Bytes s, Bytes t) -> whenFail (putStrLn ("r:" <> (show (ByteStringS r))) >> putStrLn ("s:" <> (show (ByteStringS s))) >> putStrLn ("t:" <> (show (ByteStringS t)))) $ -- withMaxSuccess 100000 $ Patricia.insertValues [(r, BS.pack[1]), (s, BS.pack[2]), (t, BS.pack[3]), (r, mempty), (s, mempty), (t, mempty)] === (Just $ Patricia.Literal Patricia.Empty) ] , testGroup "Symbolic execution" [ -- Somewhat tautological since we are asserting the precondition -- on the same form as the actual "requires" clause. testCase "SafeAdd success case" $ do Just safeAdd <- solcRuntime "SafeAdd" [i| contract SafeAdd { function add(uint x, uint y) public pure returns (uint z) { require((z = x + y) >= x); } } |] let pre preVM = let [x, y] = getStaticAbiArgs preVM in x .<= x + y .&& view (state . callvalue) preVM .== 0 post = Just $ \(prestate, poststate) -> let [x, y] = getStaticAbiArgs prestate in case view result poststate of Just (VMSuccess (SymbolicBuffer out)) -> (fromBytes out) .== x + y _ -> sFalse (Qed res, _) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "x == y => x + y == 2 * y" $ do Just safeAdd <- solcRuntime "SafeAdd" [i| contract SafeAdd { function add(uint x, uint y) public pure returns (uint z) { require((z = x + y) >= x); } } |] let pre preVM = let [x, y] = getStaticAbiArgs preVM in (x .<= x + y) .&& (x .== y) .&& view (state . callvalue) preVM .== 0 post (prestate, poststate) = let [_, y] = getStaticAbiArgs prestate in case view result poststate of Just (VMSuccess (SymbolicBuffer out)) -> fromBytes out .== 2 * y _ -> sFalse (Qed res, _) <- runSMTWith z3 $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post) putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "summary storage writes" $ do Just c <- solcRuntime "A" [i| contract A { uint x; function f(uint256 y) public { unchecked { x += y; x += y; } } } |] let pre vm = 0 .== view (state . callvalue) vm post = Just $ \(prestate, poststate) -> let [y] = getStaticAbiArgs prestate this = view (state . codeContract) prestate Just preC = view (env.contracts . at this) prestate Just postC = view (env.contracts . at this) poststate Symbolic _ prestore = _storage preC Symbolic _ poststore = _storage postC prex = readArray prestore 0 postx = readArray poststore 0 in case view result poststate of Just (VMSuccess _) -> prex + 2 * y .== postx _ -> sFalse (Qed res, _) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post putStrLn $ "successfully explored: " <> show (length res) <> " paths" , -- tests how whiffValue handles Neg via application of the triple IsZero simplification rule -- regression test for: https://github.com/dapphub/dapptools/pull/698 testCase "Neg" $ do let src = [i| object "Neg" { code { // Deploy the contract datacopy(0, dataoffset("runtime"), datasize("runtime")) return(0, datasize("runtime")) } object "runtime" { code { let v := calldataload(4) if iszero(iszero(and(v, not(0xffffffffffffffffffffffffffffffffffffffff)))) { invalid() } } } } |] Just c <- yulRuntime "Neg" src (Qed res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("hello(address)", [AbiAddressType])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , -- Inspired by these `msg.sender == to` token bugs -- which break linearity of totalSupply. testCase "catch storage collisions" $ do Just c <- solcRuntime "A" [i| contract A { function f(uint x, uint y) public { assembly { let newx := sub(sload(x), 1) let newy := add(sload(y), 1) sstore(x,newx) sstore(y,newy) } } } |] let pre vm = 0 .== view (state . callvalue) vm post (prestate, poststate) = let [x,y] = getStaticAbiArgs prestate this = view (state . codeContract) prestate (Just preC, Just postC) = both' (view (env.contracts . at this)) (prestate, poststate) --Just postC = view (env.contracts . at this) poststate (Symbolic _ prestore, Symbolic _ poststore) = both' (view storage) (preC, postC) (prex, prey) = both' (readArray prestore) (x, y) (postx, posty) = both' (readArray poststore) (x, y) in case view result poststate of Just (VMSuccess _) -> prex + prey .== postx + (posty :: SWord 256) _ -> sFalse bs <- runSMT $ query $ do (Cex _, vm) <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post) case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected" let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs assertEqual "Catch storage collisions" x y , testCase "Deposit contract loop (z3)" $ do Just c <- solcRuntime "Deposit" [i| contract Deposit { function deposit(uint256 deposit_count) external pure { require(deposit_count < 2**32 - 1); ++deposit_count; bool found = false; for (uint height = 0; height < 32; height++) { if ((deposit_count & 1) == 1) { found = true; break; } deposit_count = deposit_count >> 1; } assert(found); } } |] (Qed res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "Deposit contract loop (cvc4)" $ do Just c <- solcRuntime "Deposit" [i| contract Deposit { function deposit(uint256 deposit_count) external pure { require(deposit_count < 2**32 - 1); ++deposit_count; bool found = false; for (uint height = 0; height < 32; height++) { if ((deposit_count & 1) == 1) { found = true; break; } deposit_count = deposit_count >> 1; } assert(found); } } |] (Qed res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "Deposit contract loop (error version)" $ do Just c <- solcRuntime "Deposit" [i| contract Deposit { function deposit(uint8 deposit_count) external pure { require(deposit_count < 2**32 - 1); ++deposit_count; bool found = false; for (uint height = 0; height < 32; height++) { if ((deposit_count & 1) == 1) { found = true; break; } deposit_count = deposit_count >> 1; } assert(found); } } |] bs <- runSMT $ query $ do (Cex _, vm) <- checkAssert allPanicCodes c (Just ("deposit(uint8)", [AbiUIntType 8])) [] case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected" let [deposit] = decodeAbiValues [AbiUIntType 8] bs assertEqual "overflowing uint8" deposit (AbiUInt 8 255) , testCase "explore function dispatch" $ do Just c <- solcRuntime "A" [i| contract A { function f(uint x) public pure returns (uint) { return x; } } |] (Qed res, _) <- runSMTWith z3 $ do setTimeOut 5000 query $ checkAssert defaultPanicCodes c Nothing [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "injectivity of keccak (32 bytes)" $ do Just c <- solcRuntime "A" [i| contract A { function f(uint x, uint y) public pure { if (keccak256(abi.encodePacked(x)) == keccak256(abi.encodePacked(y))) assert(x == y); } } |] (Qed res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "injectivity of keccak (32 bytes)" $ do Just c <- solcRuntime "A" [i| contract A { function f(uint x, uint y) public pure { if (keccak256(abi.encodePacked(x)) == keccak256(abi.encodePacked(y))) assert(x == y); } } |] (Qed res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "injectivity of keccak (64 bytes)" $ do Just c <- solcRuntime "A" [i| contract A { function f(uint x, uint y, uint w, uint z) public pure { assert (keccak256(abi.encodePacked(x,y)) != keccak256(abi.encodePacked(w,z))); } } |] bs <- runSMTWith z3 $ query $ do (Cex _, vm) <- checkAssert defaultPanicCodes c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) [] case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected" let [AbiUInt 256 x, AbiUInt 256 y, AbiUInt 256 w, AbiUInt 256 z] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256, AbiUIntType 256] bs assertEqual "x == w" x w assertEqual "y == z" y z , testCase "calldata beyond calldatasize is 0 (z3)" $ do Just c <- solcRuntime "A" [i| contract A { function f() public pure { uint y; assembly { let x := calldatasize() y := calldataload(x) } assert(y == 0); } } |] Qed res <- runSMTWith z3 $ do setTimeOut 5000 query $ fst <$> checkAssert defaultPanicCodes c Nothing [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "keccak soundness" $ do Just c <- solcRuntime "C" [i| contract C { mapping (uint => mapping (uint => uint)) maps; function f(uint x, uint y) public view { assert(maps[y][0] == maps[x][0]); } } |] -- should find a counterexample Cex _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn "found counterexample:" , testCase "multiple contracts" $ do let code' = [i| contract C { uint x; A constant a = A(0x35D1b3F3D7966A1DFe207aa4514C12a259A0492B); function call_A() public view { // should fail since a.x() can be anything assert(a.x() == x); } } contract A { uint public x; } |] aAddr = Addr 0x35D1b3F3D7966A1DFe207aa4514C12a259A0492B Just c <- solcRuntime "C" code' Just a <- solcRuntime "A" code' Cex _ <- runSMT $ query $ do vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS store <- freshArray (show aAddr) Nothing let vm = vm0 & set (state . callvalue) 0 & over (env . contracts) (Map.insert aAddr (initialContract (RuntimeCode $ ConcreteBuffer a) & set EVM.storage (EVM.Symbolic [] store))) verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "found counterexample:" , testCase "calling unique contracts (read from storage)" $ do let code' = [i| contract C { uint x; A a; function call_A() public { a = new A(); // should fail since x can be anything assert(a.x() == x); } } contract A { uint public x; } |] Just c <- solcRuntime "C" code' Cex _ <- runSMT $ query $ do vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS let vm = vm0 & set (state . callvalue) 0 verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "found counterexample:" , testCase "keccak concrete and sym agree" $ do let code' = [i| contract C { function kecc(uint x) public pure { if (x == 0) { assert(keccak256(abi.encode(x)) == keccak256(abi.encode(0))); } } } |] Just c <- solcRuntime "C" code' Qed _ <- runSMT $ query $ do vm0 <- abstractVM (Just ("kecc(uint256)", [AbiUIntType 256])) [] c SymbolicS let vm = vm0 & set (state . callvalue) 0 verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "found counterexample:" , testCase "safemath distributivity (yul)" $ do Qed _ <- runSMTWith cvc4 $ query $ do let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b" vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] yulsafeDistributivity SymbolicS verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "Proven" , testCase "safemath distributivity (sol)" $ do let code' = [i| contract C { function distributivity(uint x, uint y, uint z) public { assert(mul(x, add(y, z)) == add(mul(x, y), mul(x, z))); } function add(uint x, uint y) internal pure returns (uint z) { unchecked { require((z = x + y) >= x, "ds-math-add-overflow"); } } function mul(uint x, uint y) internal pure returns (uint z) { unchecked { require(y == 0 || (z = x * y) / y == x, "ds-math-mul-overflow"); } } } |] Just c <- solcRuntime "C" code' Qed _ <- runSMTWith cvc4 $ query $ do vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] c SymbolicS verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "Proven" ] , testGroup "Equivalence checking" [ testCase "yul optimized" $ do -- These yul programs are not equivalent: (try --calldata $(seth --to-uint256 2) for example) Just aPrgm <- yul "" [i| { calldatacopy(0, 0, 32) switch mload(0) case 0 { } case 1 { } default { invalid() } } |] Just bPrgm <- yul "" [i| { calldatacopy(0, 0, 32) switch mload(0) case 0 { } case 2 { } default { invalid() } } |] runSMTWith z3 $ query $ do Cex _ <- equivalenceCheck aPrgm bPrgm Nothing Nothing Nothing return () ] ] where (===>) = assertSolidityComputation runSimpleVM :: ByteString -> ByteString -> Maybe ByteString runSimpleVM x ins = case loadVM x of Nothing -> Nothing Just vm -> let calldata' = (ConcreteBuffer ins, w256lit $ num $ BS.length ins) in case runState (assign (state.calldata) calldata' >> exec) vm of (VMSuccess (ConcreteBuffer bs), _) -> Just bs _ -> Nothing loadVM :: ByteString -> Maybe VM loadVM x = case runState exec (vmForEthrunCreation x) of (VMSuccess (ConcreteBuffer targetCode), vm1) -> do let target = view (state . contract) vm1 vm2 = execState (replaceCodeOfSelf (RuntimeCode (ConcreteBuffer targetCode))) vm1 return $ snd $ flip runState vm2 (do resetState assign (state . gas) 0xffffffffffffffff -- kludge loadContract target) _ -> Nothing hex :: ByteString -> ByteString hex s = case Hex.decode s of Right x -> x Left e -> error e singleContract :: Text -> Text -> IO (Maybe ByteString) singleContract x s = solidity x [i| pragma experimental ABIEncoderV2; contract ${x} { ${s} } |] defaultDataLocation :: AbiType -> Text defaultDataLocation t = if (case t of AbiBytesDynamicType -> True AbiStringType -> True AbiArrayDynamicType _ -> True AbiArrayType _ _ -> True _ -> False) then "memory" else "" runFunction :: Text -> ByteString -> IO (Maybe ByteString) runFunction c input = do Just x <- singleContract "X" c return $ runSimpleVM x input runStatements :: Text -> [AbiValue] -> AbiType -> IO (Maybe ByteString) runStatements stmts args t = do let params = Text.intercalate ", " (map (\(x, c) -> abiTypeSolidity (abiValueType x) <> " " <> defaultDataLocation (abiValueType x) <> " " <> Text.pack [c]) (zip args "abcdefg")) s = "foo(" <> Text.intercalate "," (map (abiTypeSolidity . abiValueType) args) <> ")" runFunction [i| function foo(${params}) public pure returns (${abiTypeSolidity t} ${defaultDataLocation t} x) { ${stmts} } |] (abiMethod s (AbiTuple $ Vector.fromList args)) getStaticAbiArgs :: VM -> [SWord 256] getStaticAbiArgs vm = let cd = view (state . calldata . _1) vm bs = case cd of ConcreteBuffer bs' -> ConcreteBuffer $ BS.drop 4 bs' SymbolicBuffer bs' -> SymbolicBuffer $ drop 4 bs' args = decodeStaticArgs bs in fmap (\(S _ v) -> v) args -- includes shaving off 4 byte function sig decodeAbiValues :: [AbiType] -> ByteString -> [AbiValue] decodeAbiValues types bs = let AbiTuple xy = decodeAbiValue (AbiTupleType $ Vector.fromList types) (BS.fromStrict (BS.drop 4 bs)) in Vector.toList xy newtype Bytes = Bytes ByteString deriving Eq instance Show Bytes where showsPrec _ (Bytes x) _ = show (BS.unpack x) instance Arbitrary Bytes where arbitrary = fmap (Bytes . BS.pack) arbitrary newtype RLPData = RLPData RLP deriving (Eq, Show) -- bias towards bytestring to try to avoid infinite recursion instance Arbitrary RLPData where arbitrary = frequency [(5, do Bytes bytes <- arbitrary return $ RLPData $ BS bytes) , (1, do k <- choose (0,10) ls <- vectorOf k arbitrary return $ RLPData $ List [r | RLPData r <- ls]) ] data Invocation = SolidityCall Text [AbiValue] deriving Show assertSolidityComputation :: Invocation -> AbiValue -> IO () assertSolidityComputation (SolidityCall s args) x = do y <- runStatements s args (abiValueType x) assertEqual (Text.unpack s) (fmap Bytes (Just (encodeAbiValue x))) (fmap Bytes y) bothM :: (Monad m) => (a -> m b) -> (a, a) -> m (b, b) bothM f (a, a') = do b <- f a b' <- f a' return (b, b') applyPattern :: String -> TestTree -> TestTree applyPattern p = localOption (TestPattern (parseExpr p))