From e353b86bf06ce799b3b4a9e97bba097959c15a46 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Tue, 8 Sep 2020 17:04:27 +0200 Subject: [PATCH] allow calldata to be either a buffer or pseudodynamic (old approach) --- src/hevm/src/EVM.hs | 40 ++++++++++++++---- src/hevm/src/EVM/Exec.hs | 4 +- src/hevm/src/EVM/SymExec.hs | 57 ++++++++++++++++--------- src/hevm/src/EVM/Symbolic.hs | 29 ++++++++++++- src/hevm/src/EVM/TTY.hs | 8 +++- src/hevm/src/EVM/UnitTest.hs | 4 +- src/hevm/src/EVM/VMTest.hs | 6 +-- src/hevm/test/test.hs | 80 ++++++++++++++++++------------------ 8 files changed, 150 insertions(+), 78 deletions(-) diff --git a/src/hevm/src/EVM.hs b/src/hevm/src/EVM.hs index 22cc7d187..9102c2db6 100644 --- a/src/hevm/src/EVM.hs +++ b/src/hevm/src/EVM.hs @@ -16,6 +16,7 @@ module EVM where import Prelude hiding (log, Word, exponent) import Data.SBV hiding (Word, output, Unknown) +import Data.SBV.List (implode, subList) import Data.Proxy (Proxy(..)) import EVM.ABI import EVM.Types @@ -170,7 +171,7 @@ data Cache = Cache -- | A way to specify an initial VM state data VMOpts = VMOpts { vmoptContract :: Contract - , vmoptCalldata :: Buffer -- maximum size of uint32 as per eip 1985 + , vmoptCalldata :: Calldata , vmoptValue :: SymWord , vmoptAddress :: Addr , vmoptCaller :: SAddr @@ -225,7 +226,7 @@ data FrameState = FrameState , _stack :: [SymWord] , _memory :: Buffer , _memorySize :: SWord 32 - , _calldata :: Buffer + , _calldata :: Calldata , _callvalue :: SymWord , _caller :: SAddr , _gas :: Word @@ -312,6 +313,14 @@ data StorageModel instance ParseField StorageModel +-- | Calldata can either by a normal buffer, or a custom "pseudo dynamic" encoding. See EVM.Symbolic for details +data CalldataModel + = BufferCD + | BoundedCD + deriving (Read, Show) + +instance ParseField CalldataModel + -- | Various environmental data data Env = Env { _contracts :: Map Addr Contract @@ -342,7 +351,7 @@ blankState = FrameState , _stack = mempty , _memory = mempty , _memorySize = 0 - , _calldata = mempty + , _calldata = CalldataBuffer mempty , _callvalue = 0 , _caller = 0 , _gas = 0 @@ -501,8 +510,8 @@ exec1 = do -- call to precompile let ?op = 0x00 -- dummy value - copyBytesToMemory (the state calldata) (len $ the state calldata) 0 0 - executePrecompile self (the state gas) 0 (len $ the state calldata) 0 0 [] + copyCalldataToMemory (the state calldata) (cdlen $ the state calldata) 0 0 + executePrecompile self (the state gas) 0 (cdlen $ the state calldata) 0 0 [] vmx <- get case view (state.stack) vmx of (x:_) -> case maybeLitWord x of @@ -712,12 +721,14 @@ exec1 = do -- op: CALLDATALOAD 0x35 -> stackOp1 (const g_verylow) $ - flip readSWord (the state calldata) + case the state calldata of + CalldataBuffer bf -> flip readSWord bf + CalldataDynamic bf -> \(S _ i) -> readStaticWordWithBound (sFromIntegral i) bf -- op: CALLDATASIZE 0x36 -> limitStack 1 . burn g_base $ - next >> pushSym (len $ the state calldata) + next >> pushSym (cdlen $ the state calldata) -- op: CALLDATACOPY 0x37 -> @@ -727,7 +738,7 @@ exec1 = do accessUnboundedMemoryRange fees xTo xSize $ do next assign (state . stack) xs - copyBytesToMemory (the state calldata) xSize xFrom xTo + copyCalldataToMemory (the state calldata) xSize xFrom xTo _ -> underrun -- op: CODESIZE @@ -1909,7 +1920,7 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut assign memory mempty assign memorySize 0 assign returndata mempty - assign calldata (readMemory xInOffset xInSize vm0) + assign calldata (CalldataBuffer $ readMemory xInOffset xInSize vm0) continue @@ -2195,6 +2206,17 @@ accessMemoryWord :: FeeSchedule Word -> SymWord -> EVM () -> EVM () accessMemoryWord fees x = accessMemoryRange fees x 32 +copyCalldataToMemory + :: Calldata -> SymWord -> SymWord -> SymWord -> EVM () +copyCalldataToMemory (CalldataBuffer bf) size xOffset yOffset = + copyBytesToMemory bf size xOffset yOffset +copyCalldataToMemory (CalldataDynamic (b, l)) size xOffset yOffset = + case (maybeLitWord size, maybeLitWord xOffset, maybeLitWord yOffset) of + (Just size', Just xOffset', Just yOffset') -> + copyBytesToMemory (StaticSymBuffer [ite (i .<= l) x 0 | (x, i) <- zip b [1..]]) size' xOffset' yOffset' + _ -> + copyBytesToMemory (DynamicSymBuffer (subList (implode b) 0 (sFromIntegral l))) size xOffset yOffset + copyBytesToMemory :: Buffer -> SymWord -> SymWord -> SymWord -> EVM () copyBytesToMemory bs size xOffset yOffset = diff --git a/src/hevm/src/EVM/Exec.hs b/src/hevm/src/EVM/Exec.hs index d960b87ea..0fede87b7 100644 --- a/src/hevm/src/EVM/Exec.hs +++ b/src/hevm/src/EVM/Exec.hs @@ -2,7 +2,7 @@ module EVM.Exec where import EVM import EVM.Concrete (createAddress) -import EVM.Symbolic (litAddr) +import EVM.Symbolic (litAddr, Calldata(..)) import EVM.Types import qualified EVM.FeeSchedule as FeeSchedule @@ -22,7 +22,7 @@ vmForEthrunCreation :: ByteString -> VM vmForEthrunCreation creationCode = (makeVm $ VMOpts { vmoptContract = initialContract (InitCode creationCode) - , vmoptCalldata = mempty + , vmoptCalldata = CalldataBuffer mempty , vmoptValue = 0 , vmoptAddress = createAddress ethrunAddress 1 , vmoptCaller = litAddr ethrunAddress diff --git a/src/hevm/src/EVM/SymExec.hs b/src/hevm/src/EVM/SymExec.hs index bbdb14b93..66febd08e 100644 --- a/src/hevm/src/EVM/SymExec.hs +++ b/src/hevm/src/EVM/SymExec.hs @@ -16,7 +16,7 @@ import EVM.Stepper (Stepper) import qualified EVM.Stepper as Stepper import qualified Control.Monad.Operational as Operational import EVM.Types hiding (Word) -import EVM.Symbolic (litBytes, SymWord(..), sw256, Buffer(..)) +import EVM.Symbolic (litBytes, SymWord(..), sw256, Buffer(..), Calldata(..)) import EVM.Concrete (createAddress, Word) import qualified EVM.FeeSchedule as FeeSchedule import Data.SBV.Trans.Control @@ -93,19 +93,28 @@ staticCalldata sig typesignature concreteArgs = sig' = litBytes $ selector sig -abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> Query VM -abstractVM typesignature concreteArgs x storagemodel = do +-- | Construct a VM out of a type signature, possibly with specialized concrete arguments +-- ,bytecode, storagemodel and calldata structure. +abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> CalldataModel -> Query VM +abstractVM typesignature concreteArgs x storagemodel calldatamodel = do (cd',pathCond) <- case typesignature of - Nothing -> do list <- freshVar_ - return (DynamicSymBuffer list, - -- due to some current z3 shenanegans (possibly related to: https://github.com/Z3Prover/z3/issues/4635) - -- we assume the list length to be shorter than max_length both as a bitvector and as an integer. - -- The latter implies the former as long as max_length fits in a bitvector, but assuming it explitly - -- improves z3 (4.8.8) performance. - SList.length list .< 1000 .&& - sw256 (sFromIntegral (SList.length list)) .< sw256 1000) + Nothing -> case calldatamodel of + BufferCD -> do + list <- freshVar_ + return (CalldataBuffer (DynamicSymBuffer list), + -- due to some current z3 shenanegans (possibly related to: https://github.com/Z3Prover/z3/issues/4635) + -- we assume the list length to be shorter than max_length both as a bitvector and as an integer. + -- The latter implies the former as long as max_length fits in a bitvector, but assuming it explitly + -- improves z3 (4.8.8) performance. + SList.length list .< 1000 .&& + sw256 (sFromIntegral (SList.length list)) .< sw256 1000) + + BoundedCD -> do + cd <- sbytes256 + len <- freshVar_ + return (CalldataDynamic (cd, len), len .<= 256) Just (name, typs) -> do symbytes <- staticCalldata name typs concreteArgs - return (StaticSymBuffer symbytes, sTrue) + return (CalldataBuffer (StaticSymBuffer symbytes), sTrue) symstore <- case storagemodel of SymbolicS -> Symbolic <$> freshArray_ Nothing @@ -116,7 +125,7 @@ abstractVM typesignature concreteArgs x storagemodel = do return $ loadSymVM (RuntimeCode x) symstore storagemodel c value' cd' & over pathConditions (<> [pathCond]) -loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> Buffer -> VM +loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> Calldata -> VM loadSymVM x initStore model addr callvalue' calldata' = (makeVm $ VMOpts { vmoptContract = contractWithStore x initStore @@ -196,17 +205,21 @@ maxIterationsReached vm (Just maxIter) = type Precondition = VM -> SBool type Postcondition = (VM, VM) -> SBool +checkAssertBuffer :: ByteString -> Query (Either (VM, [VM]) VM) +checkAssertBuffer c = verifyContract c Nothing [] SymbolicS BufferCD (const sTrue) (Just checkAssertions) + + checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM) -checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions) +checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS BoundedCD (const sTrue) (Just checkAssertions) checkAssertions :: Postcondition checkAssertions (_, out) = case view result out of Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> sFalse _ -> sTrue -verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM) -verifyContract theCode signature' concreteArgs storagemodel pre maybepost = do - preStateRaw <- abstractVM signature' concreteArgs theCode storagemodel +verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> CalldataModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM) +verifyContract theCode signature' concreteArgs storagemodel calldatamodel pre maybepost = do + preStateRaw <- abstractVM signature' concreteArgs theCode storagemodel calldatamodel -- add the pre condition to the pathconditions to ensure that we are only exploring valid paths let preState = over pathConditions ((++) [pre preStateRaw]) preStateRaw verify preState Nothing Nothing maybepost @@ -247,7 +260,7 @@ verify preState maxIter rpcinfo maybepost = do -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states. equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM) equivalenceCheck bytecodeA bytecodeB maxiter signature' = do - preStateA <- abstractVM signature' [] bytecodeA SymbolicS + preStateA <- abstractVM signature' [] bytecodeA SymbolicS BoundedCD let preself = preStateA ^. state . contract precaller = preStateA ^. state . caller @@ -310,8 +323,12 @@ showCounterexample vm maybesig = do SAddr caller' = view (EVM.state . EVM.caller) vm -- cdlen' <- num <$> getValue cdlen calldatainput <- case calldata' of - StaticSymBuffer cd -> mapM (getValue.fromSized) cd >>= return . pack - ConcreteBuffer cd -> return $ cd + CalldataDynamic (cd, cdlen) -> do + cdlen' <- num <$> getValue cdlen + mapM (getValue.fromSized) (take cdlen' cd) >>= return . pack + CalldataBuffer (StaticSymBuffer cd) -> mapM (getValue.fromSized) cd >>= return . pack + CalldataBuffer (ConcreteBuffer cd) -> return $ cd + CalldataBuffer (DynamicSymBuffer cd) -> (fmap fromSized) <$> getValue cd >>= return . pack callvalue' <- num <$> getValue cvalue caller'' <- num <$> getValue caller' io $ do diff --git a/src/hevm/src/EVM/Symbolic.hs b/src/hevm/src/EVM/Symbolic.hs index e5ae1a480..0f7192373 100644 --- a/src/hevm/src/EVM/Symbolic.hs +++ b/src/hevm/src/EVM/Symbolic.hs @@ -206,7 +206,6 @@ readByteOrZero'' i bs = (bs .!! (sFromIntegral i)) (literal 0) - -- pad up to 1000 bytes sslice :: SymWord -> SymWord -> SList (WordN 8) -> SList (WordN 8) sslice (S _ o) (S _ l) bs = case (unliteral $ SL.length bs, unliteral (o + l)) of @@ -299,12 +298,26 @@ instance Semigroup Buffer where instance Monoid Buffer where mempty = ConcreteBuffer mempty +-- | Althogh calldata can be modeled perfectly well directly as a Buffer, +-- we allow for it to take on a special form; the pair ([SWord 8], SWord 32) +-- where the second argument is understood as the length of the list. +-- This allows us to 'fake' dynamically sized calldata arrays in a way +-- that has proven more efficient than `SList`. +data Calldata + = CalldataBuffer Buffer + | CalldataDynamic ([SWord 8], SWord 32) + deriving Show + -- a whole foldable instance seems overkill, but length is always good to have! len :: Buffer -> SymWord --SWord 32 len (DynamicSymBuffer a) = sw256 $ sFromIntegral $ SL.length a len (StaticSymBuffer bs) = litWord . num $ length bs len (ConcreteBuffer bs) = litWord . num $ BS.length bs +cdlen :: Calldata -> SymWord +cdlen (CalldataBuffer bf) = len bf +cdlen (CalldataDynamic (_, a)) = sw256 $ sFromIntegral a + grab :: Int -> Buffer -> Buffer grab n (StaticSymBuffer bs) = StaticSymBuffer $ take n bs grab n (ConcreteBuffer bs) = ConcreteBuffer $ BS.take n bs @@ -393,6 +406,20 @@ readSWord i bf = case (maybeLitWord i, bf) of (Just i', ConcreteBuffer x) -> num $ Concrete.readMemoryWord i' x _ -> readSWord'' i (dynamize bf) + +select' :: (Ord b, Num b, SymVal b, Mergeable a) => [a] -> a -> SBV b -> a +select' xs err ind = walk xs ind err + where walk [] _ acc = acc + walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc) + +-- Generates a ridiculously large set of constraints (roughly 25k) when +-- the index is symbolic, but it still seems (kind of) manageable +-- for the solvers. +readStaticWordWithBound :: SWord 32 -> ([SWord 8], SWord 32) -> SymWord +readStaticWordWithBound ind (xs, bound) = + let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]] + in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]] + -- | Custom instances for SymWord, many of which have direct -- analogues for concrete words defined in Concrete.hs diff --git a/src/hevm/src/EVM/TTY.hs b/src/hevm/src/EVM/TTY.hs index 8ffcdfaea..0a2679046 100644 --- a/src/hevm/src/EVM/TTY.hs +++ b/src/hevm/src/EVM/TTY.hs @@ -12,7 +12,7 @@ import Brick.Widgets.List import EVM import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi) -import EVM.Symbolic (SymWord(..), Buffer(..)) +import EVM.Symbolic (SymWord(..), Buffer(..), Calldata(..)) import EVM.SymExec (maxIterationsReached) import EVM.Dapp (DappInfo, dappInfo) import EVM.Dapp (dappUnitTests, unitTestMethods, dappSolcByName, dappSolcByHash, dappSources) @@ -868,12 +868,16 @@ prettyIfConcrete (StaticSymBuffer x) = show x prettyIfConcrete (DynamicSymBuffer x) = show x prettyIfConcrete (ConcreteBuffer x) = prettyHex 40 x +prettyIfConcreteCd :: Calldata -> String +prettyIfConcreteCd (CalldataBuffer bf) = prettyIfConcrete bf +prettyIfConcreteCd (CalldataDynamic (x, l)) = show x + drawTracePane :: UiVmState -> UiWidget drawTracePane s = case view uiShowMemory s of True -> hBorderWithLabel (txt "Calldata") - <=> str (prettyIfConcrete $ view (uiVm . state . calldata) s) + <=> str (prettyIfConcreteCd $ view (uiVm . state . calldata) s) <=> hBorderWithLabel (txt "Returndata") <=> str (prettyIfConcrete (view (uiVm . state . returndata) s)) <=> hBorderWithLabel (txt "Output") diff --git a/src/hevm/src/EVM/UnitTest.hs b/src/hevm/src/EVM/UnitTest.hs index 6f9a7d015..0a02bf3e6 100644 --- a/src/hevm/src/EVM/UnitTest.hs +++ b/src/hevm/src/EVM/UnitTest.hs @@ -553,7 +553,7 @@ setupCall TestVMParams{..} sig args = do use (env . contracts) >>= assign (tx . txReversion) assign (tx . isCreate) False loadContract testAddress - assign (state . calldata) (ConcreteBuffer $ abiMethod sig args) + assign (state . calldata) (CalldataBuffer (ConcreteBuffer $ abiMethod sig args)) assign (state . caller) (litAddr testCaller) assign (state . gas) (w256 testGasCall) @@ -563,7 +563,7 @@ initialUnitTestVm (UnitTestOptions {..}) theContract = TestVMParams {..} = testParams vm = makeVm $ VMOpts { vmoptContract = initialContract (InitCode (view creationCode theContract)) - , vmoptCalldata = mempty + , vmoptCalldata = CalldataBuffer mempty , vmoptValue = 0 , vmoptAddress = testAddress , vmoptCaller = litAddr testCaller diff --git a/src/hevm/src/EVM/VMTest.hs b/src/hevm/src/EVM/VMTest.hs index b31d4a10d..6212e93ae 100644 --- a/src/hevm/src/EVM/VMTest.hs +++ b/src/hevm/src/EVM/VMTest.hs @@ -255,7 +255,7 @@ parseVmOpts v = (JSON.Object env, JSON.Object exec) -> EVM.VMOpts <$> (dataField exec "code" >>= pure . EVM.initialContract . EVM.RuntimeCode) - <*> (dataField exec "data" >>= pure . ConcreteBuffer) + <*> (dataField exec "data" >>= pure . CalldataBuffer . ConcreteBuffer) <*> (w256lit <$> wordField exec "value") <*> addrField exec "address" <*> (litAddr <$> addrField exec "caller") @@ -376,7 +376,7 @@ fromCreateBlockchainCase block tx preState postState = in Right $ Case (EVM.VMOpts { vmoptContract = EVM.initialContract (EVM.InitCode (txData tx)) - , vmoptCalldata = mempty + , vmoptCalldata = CalldataBuffer mempty , vmoptValue = w256lit $ txValue tx , vmoptAddress = createdAddr , vmoptCaller = (litAddr origin) @@ -415,7 +415,7 @@ fromNormalBlockchainCase block tx preState postState = (_, _, Just origin, Just checkState) -> Right $ Case (EVM.VMOpts { vmoptContract = EVM.initialContract theCode - , vmoptCalldata = ConcreteBuffer $ txData tx + , vmoptCalldata = CalldataBuffer $ ConcreteBuffer $ txData tx , vmoptValue = litWord (EVM.w256 $ txValue tx) , vmoptAddress = toAddr , vmoptCaller = (litAddr origin) diff --git a/src/hevm/test/test.hs b/src/hevm/test/test.hs index 81f2ed005..c22174945 100644 --- a/src/hevm/test/test.hs +++ b/src/hevm/test/test.hs @@ -273,33 +273,35 @@ main = defaultMain $ testGroup "hevm" in case view result poststate of Just (VMSuccess (StaticSymBuffer out)) -> (fromBytes out) .== x + y _ -> sFalse - Left (_, res) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post + Left (_, res) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS BoundedCD 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 (StaticSymBuffer out)) -> fromBytes out .== 2 * y - -- _ -> sFalse - -- Left (_, res) <- runSMTWith z3 $ query $ - -- verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post) - -- putStrLn $ "successfully explored: " <> show (length res) <> " paths" - -- , + 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 (StaticSymBuffer out)) -> fromBytes out .== 2 * y + _ -> sFalse + Left (_, res) <- runSMTWith z3 $ query $ + verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS BoundedCD pre (Just post) + putStrLn $ "successfully explored: " <> show (length res) <> " paths" + + , + testCase "factorize 973013" $ do Just factor <- solcRuntime "PrimalityCheck" [i| @@ -312,8 +314,8 @@ main = defaultMain $ testGroup "hevm" |] bs <- runSMTWith cvc4 $ query $ do Right vm <- checkAssert factor (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] - case view (state . calldata . _1) vm of - StaticSymBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs + case view (state . calldata) vm of + CalldataBuffer (StaticSymBuffer bs) -> BS.pack <$> mapM (getValue.fromSized) bs _ -> error "unexpected" let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs @@ -344,7 +346,7 @@ main = defaultMain $ testGroup "hevm" in case view result poststate of Just (VMSuccess _) -> prex + 2 * y .== postx _ -> sFalse - Left (_, res) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post + Left (_, res) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS BoundedCD pre post putStrLn $ "successfully explored: " <> show (length res) <> " paths" , -- Inspired by these `msg.sender == to` token bugs @@ -376,9 +378,9 @@ main = defaultMain $ testGroup "hevm" Just (VMSuccess _) -> prex + prey .== postx + (posty :: SWord 256) _ -> sFalse bs <- runSMT $ query $ do - Right vm <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post) - case view (state . calldata . _1) vm of - StaticSymBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs + Right vm <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS BoundedCD pre (Just post) + case view (state . calldata) vm of + CalldataBuffer (StaticSymBuffer bs) -> BS.pack <$> mapM (getValue.fromSized) bs _ -> error "unexpected" let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs @@ -449,8 +451,8 @@ main = defaultMain $ testGroup "hevm" |] bs <- runSMT $ query $ do Right vm <- checkAssert c (Just ("deposit(uint8)", [AbiUIntType 8])) [] - case view (state . calldata . _1) vm of - StaticSymBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs + case view (state . calldata) vm of + CalldataBuffer (StaticSymBuffer bs) -> BS.pack <$> mapM (getValue.fromSized) bs _ -> error "unexpected" let [deposit] = decodeAbiValues [AbiUIntType 8] bs @@ -507,8 +509,8 @@ main = defaultMain $ testGroup "hevm" |] bs <- runSMTWith z3 $ query $ do Right vm <- checkAssert c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) [] - case view (state . calldata . _1) vm of - StaticSymBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs + case view (state . calldata) vm of + CalldataBuffer (StaticSymBuffer bs) -> BS.pack <$> mapM (getValue.fromSized) bs _ -> error "unexpected" let [AbiUInt 256 x, @@ -578,7 +580,7 @@ main = defaultMain $ testGroup "hevm" Just c <- solcRuntime "C" code Just a <- solcRuntime "A" code Right cex <- runSMT $ query $ do - vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS + vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS BoundedCD store <- freshArray (show aAddr) Nothing let vm = vm0 & set (state . callvalue) 0 @@ -625,7 +627,7 @@ main = defaultMain $ testGroup "hevm" -- should find a counterexample Left (_, res) <- runSMTWith z3{verbose=True} $ do -- setTimeOut 20000 - query $ checkAssert c Nothing [] + query $ checkAssertBuffer c putStrLn $ "successfully explored: " <> show (length res) <> " paths" ] , testGroup "Equivalence checking" @@ -642,7 +644,7 @@ main = defaultMain $ testGroup "hevm" -- } } let aPrgm = hex "602060006000376000805160008114601d5760018114602457fe6029565b8191506029565b600191505b50600160015250" bPrgm = hex "6020600060003760005160008114601c5760028114602057fe6021565b6021565b5b506001600152" - runSMTWith z3 $ query $ do + runSMTWith cvc4 $ query $ do Right counterexample <- equivalenceCheck aPrgm bPrgm Nothing Nothing return () @@ -656,7 +658,7 @@ runSimpleVM :: ByteString -> ByteString -> Maybe ByteString runSimpleVM x ins = case loadVM x of Nothing -> Nothing Just vm -> - case runState (assign (state.calldata) (ConcreteBuffer ins) >> exec) vm of + case runState (assign (state.calldata) (CalldataBuffer $ ConcreteBuffer ins) >> exec) vm of (VMSuccess (ConcreteBuffer bs), _) -> Just bs _ -> Nothing @@ -722,8 +724,8 @@ runStatements stmts args t = do getStaticAbiArgs :: VM -> [SWord 256] getStaticAbiArgs vm = - let SymbolicBuffer bs = ditch 4 $ view (state . calldata . _1) vm - in fmap (\i -> fromBytes $ take 32 (drop (i*32) bs)) [0..((length bs) `div` 32 - 1)] + let CalldataBuffer (StaticSymBuffer bs) = view (state . calldata) vm + in fmap (\i -> fromBytes $ take 32 (drop (i*32) (drop 4 bs))) [0..((length (drop 4 bs)) `div` 32 - 1)] -- includes shaving off 4 byte function sig decodeAbiValues :: [AbiType] -> ByteString -> [AbiValue]