From 5f4e14d544810c8b3c3755dbf85403ce88cd45e5 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 17 Dec 2024 16:52:45 +0100 Subject: [PATCH 1/4] Performing concKeccakSimpExpr before forcing to concrete value This should alleviate issues with symbolic expression errors --- CHANGELOG.md | 5 +++++ cli/cli.hs | 1 + src/EVM.hs | 1 + src/EVM/ABI.hs | 1 + src/EVM/Dapp.hs | 1 + src/EVM/Expr.hs | 34 ++++++++++++++++++++++------ src/EVM/Format.hs | 1 + src/EVM/Solidity.hs | 3 ++- src/EVM/SymExec.hs | 1 + src/EVM/Types.hs | 18 --------------- src/EVM/UnitTest.hs | 1 + test/EVM/Test/BlockchainTests.hs | 1 + test/test.hs | 38 ++++++++++++++++++++++++++++++++ 13 files changed, 80 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 87c7e608d..fb9e67ff3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,11 @@ All notable changes to this project will be documented in this file. 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). +## Fixed +- We now try to simplify expressions fully before trying to cast them to a concrete value + This should improve issues when "Unexpected Symbolic Arguments to Opcode" was + unnecessarily output + ## [0.54.2] - 2024-12-12 ## Fixed diff --git a/cli/cli.hs b/cli/cli.hs index 516158115..66fa6a8ca 100644 --- a/cli/cli.hs +++ b/cli/cli.hs @@ -46,6 +46,7 @@ import EVM.Types hiding (word, Env, Symbolic) import EVM.Types qualified import EVM.UnitTest import EVM.Effects +import EVM.Expr (maybeLitWord, maybeLitAddr) data AssertionType = DSTest | Forge deriving (Eq, Show, Read, ParseField) diff --git a/src/EVM.hs b/src/EVM.hs index d0549501d..8ab39cdac 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -24,6 +24,7 @@ import EVM.Types qualified as Expr (Expr(Gas)) import EVM.Sign qualified import EVM.Concrete qualified as Concrete import EVM.CheatsTH +import EVM.Expr (maybeLitByte, maybeLitWord, maybeLitAddr) import Control.Monad (unless, when) import Control.Monad.ST (ST) diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs index 58d97dcc2..cb386b447 100644 --- a/src/EVM/ABI.hs +++ b/src/EVM/ABI.hs @@ -60,6 +60,7 @@ module EVM.ABI import EVM.Expr (readWord, isLitWord) import EVM.Types +import EVM.Expr (maybeLitWord) import Control.Applicative ((<|>)) import Control.Monad (replicateM, replicateM_, forM_, void) diff --git a/src/EVM/Dapp.hs b/src/EVM/Dapp.hs index c6e1e4e9f..d421b4e19 100644 --- a/src/EVM/Dapp.hs +++ b/src/EVM/Dapp.hs @@ -4,6 +4,7 @@ import EVM.ABI import EVM.Concrete import EVM.Solidity import EVM.Types +import EVM.Expr (maybeLitByte, maybeLitWord) import Control.Arrow ((>>>), second) import Data.Aeson (Value) diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 7a0c8a9ce..91fc3ac91 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -15,6 +15,7 @@ import Data.ByteString (ByteString) import Data.ByteString qualified as BS import Data.DoubleWord (Int256, Word256(Word256), Word128(Word128)) import Data.List +import Data.Map qualified as LMap import Data.Map.Strict qualified as Map import Data.Maybe (mapMaybe, isJust, fromMaybe) import Data.Semigroup (Any, Any(..), getAny) @@ -1326,13 +1327,10 @@ exprToAddr _ = Nothing -- TODO: make this smarter, probably we will need to use the solver here? wordToAddr :: Expr EWord -> Maybe (Expr EAddr) -wordToAddr = go . simplify - where - go :: Expr EWord -> Maybe (Expr EAddr) - go = \case - WAddr a -> Just a - Lit a -> Just $ LitAddr (truncateToAddr a) - _ -> Nothing +wordToAddr e = case (concKeccakSimpExpr e) of + WAddr a -> Just a + Lit a -> Just $ LitAddr (truncateToAddr a) + _ -> Nothing litCode :: BS.ByteString -> [Expr Byte] litCode bs = fmap LitByte (BS.unpack bs) @@ -1616,3 +1614,25 @@ checkLHSConstProp a = isJust $ mapPropM_ lhsConstHelper a -- Commutative operators should have the constant on the LHS checkLHSConst :: Expr a -> Bool checkLHSConst a = isJust $ mapExprM_ lhsConstHelper a + +maybeLitByte :: Expr Byte -> Maybe Word8 +maybeLitByte e = case (concKeccakSimpExpr e) of + (LitByte x) -> Just x + _ -> Nothing + +maybeLitWord :: Expr EWord -> Maybe W256 +maybeLitWord e = case (concKeccakSimpExpr e) of + (Lit w) -> Just w + (WAddr (LitAddr w)) -> Just (into w) + _ -> Nothing + +maybeLitAddr :: Expr EAddr -> Maybe Addr +maybeLitAddr e = case (concKeccakSimpExpr e) of + (LitAddr a) -> Just a + _ -> Nothing + +maybeConcreteStore :: Expr Storage -> Maybe (LMap.Map W256 W256) +maybeConcreteStore e = case (concKeccakSimpExpr e) of + (ConcreteStore s) -> Just s + _ -> Nothing + diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs index c46c38773..6c0847691 100644 --- a/src/EVM/Format.hs +++ b/src/EVM/Format.hs @@ -40,6 +40,7 @@ import EVM.Dapp (DappContext(..), DappInfo(..), findSrc, showTraceLocation) import EVM.Expr qualified as Expr import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap) import EVM.Types +import EVM.Expr (maybeLitWord, maybeLitAddr) import Control.Arrow ((>>>)) import Optics.Core diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs index 3b48f72aa..7cc23cd59 100644 --- a/src/EVM/Solidity.hs +++ b/src/EVM/Solidity.hs @@ -44,7 +44,8 @@ import EVM.Types hiding (Success) import Optics.Core import Optics.Operators.Unsafe -import EVM.Effects; +import EVM.Effects +import EVM.Expr (maybeLitByte) import Control.Applicative import Control.Monad diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 16c312255..87f488a96 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -44,6 +44,7 @@ import EVM.Stepper (Stepper) import EVM.Stepper qualified as Stepper import EVM.Traversals import EVM.Types +import EVM.Expr (maybeConcreteStore) import GHC.Conc (getNumProcessors) import GHC.Generics (Generic) import Optics.Core diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index 5690ecf02..bb724fb99 100644 --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -1266,24 +1266,6 @@ instance Show Nibble where -- Conversions ------------------------------------------------------------------------------------- -maybeLitByte :: Expr Byte -> Maybe Word8 -maybeLitByte (LitByte x) = Just x -maybeLitByte _ = Nothing - -maybeLitWord :: Expr EWord -> Maybe W256 -maybeLitWord (Lit w) = Just w -maybeLitWord (WAddr (LitAddr w)) = Just (into w) -maybeLitWord _ = Nothing - -maybeLitAddr :: Expr EAddr -> Maybe Addr -maybeLitAddr (LitAddr a) = Just a -maybeLitAddr _ = Nothing - -maybeConcreteStore :: Expr Storage -> Maybe (Map W256 W256) -maybeConcreteStore (ConcreteStore s) = Just s -maybeConcreteStore _ = Nothing - - word256 :: ByteString -> Word256 word256 xs | BS.length xs == 1 = -- optimize one byte pushes diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs index 3a9b87c29..b4275b941 100644 --- a/src/EVM/UnitTest.hs +++ b/src/EVM/UnitTest.hs @@ -19,6 +19,7 @@ import EVM.Types import EVM.Transaction (initTx) import EVM.Stepper (Stepper) import EVM.Stepper qualified as Stepper +import EVM.Expr (maybeLitWord) import Control.Monad (void, when, forM, forM_) import Control.Monad.ST (RealWorld, ST, stToIO) diff --git a/test/EVM/Test/BlockchainTests.hs b/test/EVM/Test/BlockchainTests.hs index f3eb0487e..bcb52b257 100644 --- a/test/EVM/Test/BlockchainTests.hs +++ b/test/EVM/Test/BlockchainTests.hs @@ -10,6 +10,7 @@ import EVM.Transaction import EVM.UnitTest (writeTrace) import EVM.Types hiding (Block, Case, Env) import EVM.Test.Tracing (interpretWithTrace, VMTrace, compareTraces, EVMToolTraceOutput(..), decodeTraceOutputHelper) +import EVM.Expr (maybeLitWord, maybeLitAddr) import Optics.Core import Control.Arrow ((***), (&&&)) diff --git a/test/test.hs b/test/test.hs index aa4cd8346..90ac61b5e 100644 --- a/test/test.hs +++ b/test/test.hs @@ -33,6 +33,7 @@ import Data.Tree (flatten) import Data.Typeable import Data.Vector qualified as V import Data.Word (Word8, Word64) +import Data.Char (digitToInt) import GHC.Conc (getNumProcessors) import System.Directory import System.Environment @@ -72,6 +73,7 @@ import EVM.Traversals import EVM.Types hiding (Env) import EVM.Effects import EVM.UnitTest (writeTrace) +import EVM.Expr (maybeLitByte) testEnv :: Env testEnv = Env { config = defaultConfig { @@ -447,6 +449,14 @@ tests = testGroup "hevm" expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts -- putStrLnM $ T.unpack $ formatExpr expr assertEqualM "Expression is not clean." (badStoresInExpr expr) False + , test "simplify-storage-wordToAddr" $ do + let a = "000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a" + s = ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cf)]) + expr = SLoad (Keccak (ConcreteBuf (hexStringToByteString a))) s + simpExpr = Expr.wordToAddr expr + simpExpr2 = Expr.concKeccakSimpExpr expr + assertEqualM "Expression should simplify to value." simpExpr (Just $ LitAddr 0x5842cf) + assertEqualM "Expression should simplify to value." simpExpr2 (Lit 0x5842cf) ] , testGroup "StorageTests" [ test "read-from-sstore" $ assertEqualM "" @@ -4597,3 +4607,31 @@ expectedConcVals nm val = case val of _ -> internalError $ "unsupported Abi type " <> show nm <> " val: " <> show val <> " val type: " <> showAlter val where mkWord = word . encodeAbiValue + +hexStringToByteString :: String -> BS.ByteString +hexStringToByteString hexStr + | odd (length hexStr) = error "Hex string has an odd length" + | otherwise = case traverse hexPairToByte (pairs hexStr) of + Just bytes -> (BS.pack bytes) + Nothing -> error "Invalid hex string" + where + -- Convert a pair of hex characters to a byte + hexPairToByte :: (Char, Char) -> Maybe Word8 + hexPairToByte (c1, c2) = do + b1 <- hexCharToDigit c1 + b2 <- hexCharToDigit c2 + return $ fromIntegral (b1 * 16 + b2) + + -- Convert a single hex character to its integer value + hexCharToDigit :: Char -> Maybe Int + hexCharToDigit c + | c >= '0' && c <= '9' = Just (digitToInt c) + | c >= 'a' && c <= 'f' = Just (digitToInt c) + | c >= 'A' && c <= 'F' = Just (digitToInt c) + | otherwise = Nothing + + -- Split a string into pairs of characters + pairs :: [a] -> [(a, a)] + pairs [] = [] + pairs (x:y:xs) = (x, y) : pairs xs + pairs _ = error "Unexpected odd length" From ed2a03cbe3751c9359708433cf32c7f5eeabe922 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 18 Dec 2024 12:11:51 +0100 Subject: [PATCH 2/4] Rename functions to better explain what they do --- cli/cli.hs | 6 +++--- src/EVM.hs | 31 ++++++++++++++----------------- src/EVM/ABI.hs | 4 ++-- src/EVM/Dapp.hs | 4 ++-- src/EVM/Expr.hs | 12 ++++++------ src/EVM/Format.hs | 10 +++++----- src/EVM/SymExec.hs | 4 ++-- src/EVM/UnitTest.hs | 8 ++++---- test/EVM/Test/BlockchainTests.hs | 6 +++--- 9 files changed, 41 insertions(+), 44 deletions(-) diff --git a/cli/cli.hs b/cli/cli.hs index 66fa6a8ca..369b65e61 100644 --- a/cli/cli.hs +++ b/cli/cli.hs @@ -46,7 +46,7 @@ import EVM.Types hiding (word, Env, Symbolic) import EVM.Types qualified import EVM.UnitTest import EVM.Effects -import EVM.Expr (maybeLitWord, maybeLitAddr) +import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp) data AssertionType = DSTest | Forge deriving (Eq, Show, Read, ParseField) @@ -490,7 +490,7 @@ vmFromCommand cmd = do putStrLn "Error, must provide at least (rpc + address) or code" exitFailure - let ts' = case maybeLitWord ts of + let ts' = case maybeLitWordSimp ts of Just t -> t Nothing -> internalError "unexpected symbolic timestamp when executing vm test" @@ -512,7 +512,7 @@ vmFromCommand cmd = do then InitCode bs mempty else RuntimeCode (ConcreteRuntimeCode bs) address = if cmd.create - then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddr origin) (W64 $ word64 (.nonce) 0)) + then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddrSimp origin) (W64 $ word64 (.nonce) 0)) else addr (.address) (LitAddr 0xacab) vm0 baseFee miner ts blockNum prevRan c = makeVm $ VMOpts diff --git a/src/EVM.hs b/src/EVM.hs index 8ab39cdac..2d9a01492 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -24,7 +24,7 @@ import EVM.Types qualified as Expr (Expr(Gas)) import EVM.Sign qualified import EVM.Concrete qualified as Concrete import EVM.CheatsTH -import EVM.Expr (maybeLitByte, maybeLitWord, maybeLitAddr) +import EVM.Expr (maybeLitByte, maybeLitWordSimp, maybeLitAddrSimp) import Control.Monad (unless, when) import Control.Monad.ST (ST) @@ -297,12 +297,9 @@ exec1 = do stk = vm.state.stack self = vm.state.contract this = fromMaybe (internalError "state contract") (Map.lookup self vm.env.contracts) - fees@FeeSchedule {..} = vm.block.schedule - doStop = finishFrame (FrameReturned mempty) - - litSelf = maybeLitAddr self + litSelf = maybeLitAddrSimp self if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 0xa then do -- call to precompile @@ -742,7 +739,7 @@ exec1 = do Lit v -> v _ -> 0 storage_cost = - case (maybeLitWord current, maybeLitWord new) of + case (maybeLitWordSimp current, maybeLitWordSimp new) of (Just current', Just new') -> if (current' == new') then g_sload else if (current' == original) && (original == 0) then g_sset @@ -760,7 +757,7 @@ exec1 = do assign (#state % #stack) xs modifying (#env % #contracts % ix self % #storage) (writeStorage x new) - case (maybeLitWord current, maybeLitWord new) of + case (maybeLitWordSimp current, maybeLitWordSimp new) of (Just current', Just new') -> unless (current' == new') $ if current' == original then @@ -915,7 +912,7 @@ exec1 = do output <- readMemory xOffset xSize let codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data") - . maybeLitWord . bufLength $ output + . maybeLitWordSimp . bufLength $ output maxsize = vm.block.maxCodeSize creation = case vm.frames of [] -> vm.tx.isCreate @@ -1177,7 +1174,7 @@ precompiledContract this xGas precompileAddr recipient xValue inOffset inSize ou vm <- get case result' of Nothing -> case stk of - x:_ -> case maybeLitWord x of + x:_ -> case maybeLitWordSimp x of Just 0 -> pure () Just 1 -> @@ -1592,28 +1589,28 @@ forceAddr n msg continue = case wordToAddr n of Just c -> continue c forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s () -forceConcrete n msg continue = case maybeLitWord n of +forceConcrete n msg continue = case maybeLitWordSimp n of Nothing -> do vm <- get partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n]) Just c -> continue c forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s () -forceConcreteAddr n msg continue = case maybeLitAddr n of +forceConcreteAddr n msg continue = case maybeLitAddrSimp n of Nothing -> do vm <- get partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n]) Just c -> continue c forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s () -forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of +forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddrSimp n, maybeLitAddrSimp m) of (Just c, Just d) -> continue (c,d) _ -> do vm <- get partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n, m]) forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s () -forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of +forceConcrete2 (n,m) msg continue = case (maybeLitWordSimp n, maybeLitWordSimp m) of (Just c, Just d) -> continue (c, d) _ -> do vm <- get @@ -1665,7 +1662,7 @@ accessAccountForGas addr = do accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM t s Bool accessStorageForGas addr key = do accessedStrkeys <- use (#tx % #subState % #accessedStorageKeys) - case maybeLitWord key of + case maybeLitWordSimp key of Just litword -> do let accessed = member (addr, litword) accessedStrkeys assign (#tx % #subState % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys) @@ -1690,7 +1687,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do input <- readMemory (Expr.add inOffset (Lit 4)) (Expr.sub inSize (Lit 4)) calldata <- readMemory inOffset inSize abi <- readBytes 4 (Lit 0) <$> readMemory inOffset (Lit 4) - let newContext = CallContext cheatCode cheatCode outOffset outSize (Lit 0) (maybeLitWord abi) calldata vm.env.contracts vm.tx.subState + let newContext = CallContext cheatCode cheatCode outOffset outSize (Lit 0) (maybeLitWordSimp abi) calldata vm.env.contracts vm.tx.subState pushTrace $ FrameTrace newContext next @@ -1699,7 +1696,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do { state = vm1.state { stack = xs } , context = newContext } - case maybeLitWord abi of + case maybeLitWordSimp abi of Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi]) Just (unsafeInto -> abi') -> case Map.lookup abi' cheatActions of @@ -2055,7 +2052,7 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut _ -> do burn' xGas $ do calldata <- readMemory xInOffset xInSize - abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4) + abi <- maybeLitWordSimp . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4) let newContext = CallContext { target = xTo , context = xContext diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs index cb386b447..861c40e8f 100644 --- a/src/EVM/ABI.hs +++ b/src/EVM/ABI.hs @@ -60,7 +60,7 @@ module EVM.ABI import EVM.Expr (readWord, isLitWord) import EVM.Types -import EVM.Expr (maybeLitWord) +import EVM.Expr (maybeLitWordSimp) import Control.Applicative ((<|>)) import Control.Monad (replicateM, replicateM_, forM_, void) @@ -512,7 +512,7 @@ decodeBuf tps buf = else let vs = decodeStaticArgs 0 (length tps) buf - asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs) + asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWordSimp vs) in if not (all isLitWord vs) then SAbi vs else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of diff --git a/src/EVM/Dapp.hs b/src/EVM/Dapp.hs index d421b4e19..6dc4b16a4 100644 --- a/src/EVM/Dapp.hs +++ b/src/EVM/Dapp.hs @@ -4,7 +4,7 @@ import EVM.ABI import EVM.Concrete import EVM.Solidity import EVM.Types -import EVM.Expr (maybeLitByte, maybeLitWord) +import EVM.Expr (maybeLitByte, maybeLitWordSimp) import Control.Arrow ((>>>), second) import Data.Aeson (Value) @@ -139,7 +139,7 @@ srcMap dapp contr opIndex = do findSrc :: Contract -> DappInfo -> Maybe SolcContract findSrc c dapp = do - hash <- maybeLitWord c.codehash + hash <- maybeLitWordSimp c.codehash case Map.lookup hash dapp.solcByHash of Just (_, v) -> Just v Nothing -> lookupCode c.code dapp diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 91fc3ac91..420a5bdde 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -1620,19 +1620,19 @@ maybeLitByte e = case (concKeccakSimpExpr e) of (LitByte x) -> Just x _ -> Nothing -maybeLitWord :: Expr EWord -> Maybe W256 -maybeLitWord e = case (concKeccakSimpExpr e) of +maybeLitWordSimp :: Expr EWord -> Maybe W256 +maybeLitWordSimp e = case (concKeccakSimpExpr e) of (Lit w) -> Just w (WAddr (LitAddr w)) -> Just (into w) _ -> Nothing -maybeLitAddr :: Expr EAddr -> Maybe Addr -maybeLitAddr e = case (concKeccakSimpExpr e) of +maybeLitAddrSimp :: Expr EAddr -> Maybe Addr +maybeLitAddrSimp e = case (concKeccakSimpExpr e) of (LitAddr a) -> Just a _ -> Nothing -maybeConcreteStore :: Expr Storage -> Maybe (LMap.Map W256 W256) -maybeConcreteStore e = case (concKeccakSimpExpr e) of +maybeConcStoreSimp :: Expr Storage -> Maybe (LMap.Map W256 W256) +maybeConcStoreSimp e = case (concKeccakSimpExpr e) of (ConcreteStore s) -> Just s _ -> Nothing diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs index 6c0847691..9f912a0d1 100644 --- a/src/EVM/Format.hs +++ b/src/EVM/Format.hs @@ -40,7 +40,7 @@ import EVM.Dapp (DappContext(..), DappInfo(..), findSrc, showTraceLocation) import EVM.Expr qualified as Expr import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap) import EVM.Types -import EVM.Expr (maybeLitWord, maybeLitAddr) +import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp) import Control.Arrow ((>>>)) import Optics.Core @@ -212,7 +212,7 @@ showTrace trace = [] -> logn firstTopic:restTopics -> - case maybeLitWord firstTopic of + case maybeLitWordSimp firstTopic of Just topic -> case Map.lookup topic dapp.eventMap of Just (Event name _ argInfos) -> @@ -230,7 +230,7 @@ showTrace trace = -- ) anonymous; let sig = unsafeInto $ shiftR topic 224 :: FunctionSelector - usr = case maybeLitWord t2 of + usr = case maybeLitWordSimp t2 of Just w -> pack $ show (unsafeInto w :: Addr) Nothing -> @@ -275,7 +275,7 @@ showTrace trace = where showTopic :: AbiType -> Expr EWord -> Text showTopic abiType topic = - case maybeLitWord (Expr.concKeccakSimpExpr topic) of + case maybeLitWordSimp (Expr.concKeccakSimpExpr topic) of Just w -> head $ textValues [abiType] (ConcreteBuf (word256Bytes w)) _ -> "" @@ -370,7 +370,7 @@ ppAddr addr alwaysShowAddr = case (findSrc contract ?context.info) of Just x -> Just (contractNamePart x.contractName) Nothing -> Nothing - label = case do litAddr <- maybeLitAddr addr + label = case do litAddr <- maybeLitAddrSimp addr Map.lookup litAddr ?context.labels of Nothing -> "" Just l -> "[" <> "\x1b[1m" <> l <> "\x1b[0m" <> "]" diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 87f488a96..ac4965fc2 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -44,7 +44,7 @@ import EVM.Stepper (Stepper) import EVM.Stepper qualified as Stepper import EVM.Traversals import EVM.Types -import EVM.Expr (maybeConcreteStore) +import EVM.Expr (maybeConcStoreSimp) import GHC.Conc (getNumProcessors) import GHC.Generics (Generic) import Optics.Core @@ -653,7 +653,7 @@ verify solvers opts preState maybepost = do expandCex :: VM Symbolic s -> SMTCex -> SMTCex expandCex prestate c = c { store = Map.union c.store concretePreStore } where - concretePreStore = Map.mapMaybe (maybeConcreteStore . (.storage)) + concretePreStore = Map.mapMaybe (maybeConcStoreSimp . (.storage)) . Map.filter (\v -> Expr.containsNode isConcreteStore v.storage) $ (prestate.env.contracts) isConcreteStore = \case diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs index b4275b941..b7e5cf1b8 100644 --- a/src/EVM/UnitTest.hs +++ b/src/EVM/UnitTest.hs @@ -19,7 +19,7 @@ import EVM.Types import EVM.Transaction (initTx) import EVM.Stepper (Stepper) import EVM.Stepper qualified as Stepper -import EVM.Expr (maybeLitWord) +import EVM.Expr (maybeLitWordSimp) import Control.Monad (void, when, forM, forM_) import Control.Monad.ST (RealWorld, ST, stToIO) @@ -339,7 +339,7 @@ formatTestLog :: (?context :: DappContext) => Map W256 Event -> Expr Log -> Mayb formatTestLog _ (LogEntry _ _ []) = Nothing formatTestLog _ (GVar _) = internalError "unexpected global variable" formatTestLog events (LogEntry _ args (topic:_)) = - case maybeLitWord topic >>= \t1 -> (Map.lookup t1 events) of + case maybeLitWordSimp topic >>= \t1 -> (Map.lookup t1 events) of Nothing -> Nothing Just (Event name _ argInfos) -> case (name <> parenthesise (abiTypeSolidity <$> argTypes)) of @@ -414,7 +414,7 @@ makeTxCall params (cd, cdProps) = do assign (#state % #caller) params.caller assign (#state % #gas) (toGas params.gasCall) origin <- fromMaybe (initialContract (RuntimeCode (ConcreteRuntimeCode ""))) <$> use (#env % #contracts % at params.origin) - let insufficientBal = maybe False (\b -> b < params.gasprice * (into params.gasCall)) (maybeLitWord origin.balance) + let insufficientBal = maybe False (\b -> b < params.gasprice * (into params.gasCall)) (maybeLitWordSimp origin.balance) when insufficientBal $ internalError "insufficient balance for gas cost" vm <- get put $ initTx vm @@ -468,7 +468,7 @@ paramsFromRpc rpcinfo = do , gaslimit , baseFee ) - let ts' = fromMaybe (internalError "received unexpected symbolic timestamp via rpc") (maybeLitWord ts) + let ts' = fromMaybe (internalError "received unexpected symbolic timestamp via rpc") (maybeLitWordSimp ts) pure $ TestVMParams -- TODO: make this symbolic! It needs some tweaking to the way that our -- symbolic interpreters work to allow us to symbolically exec constructor initialization diff --git a/test/EVM/Test/BlockchainTests.hs b/test/EVM/Test/BlockchainTests.hs index bcb52b257..f7e6bdac8 100644 --- a/test/EVM/Test/BlockchainTests.hs +++ b/test/EVM/Test/BlockchainTests.hs @@ -10,7 +10,7 @@ import EVM.Transaction import EVM.UnitTest (writeTrace) import EVM.Types hiding (Block, Case, Env) import EVM.Test.Tracing (interpretWithTrace, VMTrace, compareTraces, EVMToolTraceOutput(..), decodeTraceOutputHelper) -import EVM.Expr (maybeLitWord, maybeLitAddr) +import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp) import Optics.Core import Control.Arrow ((***), (&&&)) @@ -236,7 +236,7 @@ checkStateFail x vm (okBal, okNonce, okData, okCode) = do printContracts cs = putStrLn $ Map.foldrWithKey (\k c acc -> acc ++ "-->" <> show k ++ " : " ++ (show $ fromJust c.nonce) ++ " " - ++ (show $ fromJust $ maybeLitWord c.balance) ++ " " + ++ (show $ fromJust $ maybeLitWordSimp c.balance) ++ " " ++ (show $ fromConcrete c.storage) ++ (show $ fromConcrete c.tStorage) ++ "\n") "" cs @@ -534,5 +534,5 @@ vmForCase x = do forceConcreteAddrs :: Map (Expr EAddr) Contract -> Map Addr Contract forceConcreteAddrs cs = Map.mapKeys - (fromMaybe (internalError "Internal Error: unexpected symbolic address") . maybeLitAddr) + (fromMaybe (internalError "Internal Error: unexpected symbolic address") . maybeLitAddrSimp) cs From 6f1ed8532e675e54be255be28088262e3944746b Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 18 Dec 2024 15:23:23 +0100 Subject: [PATCH 3/4] More tests --- test/test.hs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/test/test.hs b/test/test.hs index 90ac61b5e..2e76685e1 100644 --- a/test/test.hs +++ b/test/test.hs @@ -451,12 +451,22 @@ tests = testGroup "hevm" assertEqualM "Expression is not clean." (badStoresInExpr expr) False , test "simplify-storage-wordToAddr" $ do let a = "000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a" - s = ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cf)]) - expr = SLoad (Keccak (ConcreteBuf (hexStringToByteString a))) s + store = ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cf)]) + expr = SLoad (Keccak (ConcreteBuf (hexStringToByteString a))) store simpExpr = Expr.wordToAddr expr simpExpr2 = Expr.concKeccakSimpExpr expr assertEqualM "Expression should simplify to value." simpExpr (Just $ LitAddr 0x5842cf) assertEqualM "Expression should simplify to value." simpExpr2 (Lit 0x5842cf) + , test "simplify-storage-wordToAddr-complex" $ do + let a = "000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a" + store = ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cf)]) + expr = SLoad (Keccak (ConcreteBuf (hexStringToByteString a))) store + writeWChain = WriteWord (Lit 0x32) (Lit 0x72) (WriteWord (Lit 0x0) expr (ConcreteBuf "")) + kecc = Keccak (CopySlice (Lit 0x0) (Lit 0x0) (Lit 0x20) (WriteWord (Lit 0x0) expr (writeWChain)) (ConcreteBuf "")) + keccAnd = (And (Lit 1461501637330902918203684832716283019655932542975) kecc) + outer = And (Lit 1461501637330902918203684832716283019655932542975) (SLoad (keccAnd) (ConcreteStore (Map.fromList[(W256 1184450375068808042203882151692185743185288360635, W256 0xacab)]))) + simp = Expr.concKeccakSimpExpr outer + assertEqualM "Expression should simplify to value." simp (Lit 0xacab) ] , testGroup "StorageTests" [ test "read-from-sstore" $ assertEqualM "" From c377f03a5c04599062b15439cbecfd1322c20428 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 23 Dec 2024 12:44:42 +0100 Subject: [PATCH 4/4] maybeLitByte->maybeLitByteSimp Thanks @blishko for catching this! --- src/EVM.hs | 12 ++++++------ src/EVM/Dapp.hs | 4 ++-- src/EVM/Expr.hs | 22 +++++++++++----------- src/EVM/Solidity.hs | 4 ++-- test/test.hs | 4 ++-- 5 files changed, 23 insertions(+), 23 deletions(-) diff --git a/src/EVM.hs b/src/EVM.hs index 2d9a01492..447036764 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -24,7 +24,7 @@ import EVM.Types qualified as Expr (Expr(Gas)) import EVM.Sign qualified import EVM.Concrete qualified as Concrete import EVM.CheatsTH -import EVM.Expr (maybeLitByte, maybeLitWordSimp, maybeLitAddrSimp) +import EVM.Expr (maybeLitByteSimp, maybeLitWordSimp, maybeLitAddrSimp) import Control.Monad (unless, when) import Control.Monad.ST (ST) @@ -282,7 +282,7 @@ getOpW8 state = case state.code of RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs state.pc RuntimeCode (SymbolicRuntimeCode ops) -> fromMaybe (internalError "could not analyze symbolic code") $ - maybeLitByte $ ops V.! state.pc + maybeLitByteSimp $ ops V.! state.pc getOpName :: forall (t :: VMType) s . FrameState t s -> [Char] getOpName state = intToOpName $ fromEnum $ getOpW8 state @@ -2649,7 +2649,7 @@ isValidJumpDest vm x = let UnknownCode _ -> internalError "Cannot analyze jumpdests for unknown code" InitCode ops _ -> BS.indexMaybe ops x RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x - RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByte + RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByteSimp in case op of Nothing -> False Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! x)) @@ -2688,7 +2688,7 @@ mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops)) let (_, _, _, m) = foldl (go v) (0, 0, 0, pure ()) (stripBytecodeMetadataSym $ V.toList ops) in m >> pure v where - go v (0, !i, !j, !m) x = case maybeLitByte x of + go v (0, !i, !j, !m) x = case maybeLitByteSimp x of Just x' -> if x' >= 0x60 && x' <= 0x7f -- start of PUSH op -- then (x' - 0x60 + 1, i + 1, j, m >> SV.write v i j) @@ -2713,7 +2713,7 @@ vmOp vm = RuntimeCode (ConcreteRuntimeCode xs') -> (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs') RuntimeCode (SymbolicRuntimeCode xs') -> - ( fromMaybe (internalError "unexpected symbolic code") . maybeLitByte $ xs' V.! i , V.toList $ V.drop i xs') + ( fromMaybe (internalError "unexpected symbolic code") . maybeLitByteSimp $ xs' V.! i , V.toList $ V.drop i xs') in if (opslen code' < i) then Nothing else Just (readOp op pushdata) @@ -2741,7 +2741,7 @@ mkCodeOps contractCode = Nothing -> mempty Just (x, xs') -> - let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByte x + let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByteSimp x j = opSize x' in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs) diff --git a/src/EVM/Dapp.hs b/src/EVM/Dapp.hs index 6dc4b16a4..c415cf0b3 100644 --- a/src/EVM/Dapp.hs +++ b/src/EVM/Dapp.hs @@ -4,7 +4,7 @@ import EVM.ABI import EVM.Concrete import EVM.Solidity import EVM.Types -import EVM.Expr (maybeLitByte, maybeLitWordSimp) +import EVM.Expr (maybeLitByteSimp, maybeLitWordSimp) import Control.Arrow ((>>>), second) import Data.Aeson (Value) @@ -154,7 +154,7 @@ lookupCode (RuntimeCode (ConcreteRuntimeCode c)) a = Just x -> pure x Nothing -> snd <$> find (compareCode c . fst) a.solcByCode lookupCode (RuntimeCode (SymbolicRuntimeCode c)) a = let - code = BS.pack $ mapMaybe maybeLitByte $ V.toList c + code = BS.pack $ mapMaybe maybeLitByteSimp $ V.toList c in case snd <$> Map.lookup (keccak' (stripBytecodeMetadata code)) a.solcByHash of Just x -> pure x Nothing -> snd <$> find (compareCode code . fst) a.solcByCode diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 420a5bdde..8f87c2ecb 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -298,7 +298,7 @@ readWordFromBytes (Lit idx) (ConcreteBuf bs) = readWordFromBytes i@(Lit idx) buf = let bytes = [readByte (Lit i') buf | i' <- [idx .. idx + 31]] in if all isLitByte bytes - then Lit (bytesToW256 . mapMaybe maybeLitByte $ bytes) + then Lit (bytesToW256 . mapMaybe maybeLitByteSimp $ bytes) else ReadWord i buf readWordFromBytes idx buf = ReadWord idx buf @@ -353,7 +353,7 @@ copySlice s@(Lit srcOffset) d@(Lit dstOffset) sz@(Lit size) src ds@(ConcreteBuf sl = [readByte (Lit i) src | i <- [srcOffset .. srcOffset + (size - 1)]] tl = BS.drop (unsafeInto dstOffset + unsafeInto size) dst in if Prelude.and . (fmap isLitByte) $ sl - then ConcreteBuf $ hd <> (BS.pack . (mapMaybe maybeLitByte) $ sl) <> tl + then ConcreteBuf $ hd <> (BS.pack . (mapMaybe maybeLitByteSimp) $ sl) <> tl else CopySlice s d sz src ds | otherwise = CopySlice s d sz src ds @@ -531,7 +531,7 @@ toList buf = case bufLength buf of fromList :: V.Vector (Expr Byte) -> Expr Buf fromList bs = case Prelude.and (fmap isLitByte bs) of - True -> ConcreteBuf . BS.pack . V.toList . V.mapMaybe maybeLitByte $ bs + True -> ConcreteBuf . BS.pack . V.toList . V.mapMaybe maybeLitByteSimp $ bs -- we want to minimize the size of the resulting expression, so we do two passes: -- 1. write all concrete bytes to some base buffer -- 2. write all symbolic writes on top of this buffer @@ -1482,7 +1482,7 @@ padBytesLeft n bs joinBytes :: [Expr Byte] -> Expr EWord joinBytes bs - | Prelude.and . (fmap isLitByte) $ bs = Lit . bytesToW256 . (mapMaybe maybeLitByte) $ bs + | Prelude.and . (fmap isLitByte) $ bs = Lit . bytesToW256 . (mapMaybe maybeLitByteSimp) $ bs | otherwise = let bytes = padBytesLeft 32 bs in JoinBytes @@ -1615,24 +1615,24 @@ checkLHSConstProp a = isJust $ mapPropM_ lhsConstHelper a checkLHSConst :: Expr a -> Bool checkLHSConst a = isJust $ mapExprM_ lhsConstHelper a -maybeLitByte :: Expr Byte -> Maybe Word8 -maybeLitByte e = case (concKeccakSimpExpr e) of - (LitByte x) -> Just x +maybeLitByteSimp :: Expr Byte -> Maybe Word8 +maybeLitByteSimp e = case (concKeccakSimpExpr e) of + LitByte x -> Just x _ -> Nothing maybeLitWordSimp :: Expr EWord -> Maybe W256 maybeLitWordSimp e = case (concKeccakSimpExpr e) of - (Lit w) -> Just w - (WAddr (LitAddr w)) -> Just (into w) + Lit w -> Just w + WAddr (LitAddr w) -> Just (into w) _ -> Nothing maybeLitAddrSimp :: Expr EAddr -> Maybe Addr maybeLitAddrSimp e = case (concKeccakSimpExpr e) of - (LitAddr a) -> Just a + LitAddr a -> Just a _ -> Nothing maybeConcStoreSimp :: Expr Storage -> Maybe (LMap.Map W256 W256) maybeConcStoreSimp e = case (concKeccakSimpExpr e) of - (ConcreteStore s) -> Just s + ConcreteStore s -> Just s _ -> Nothing diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs index 7cc23cd59..2670a55db 100644 --- a/src/EVM/Solidity.hs +++ b/src/EVM/Solidity.hs @@ -45,7 +45,7 @@ import EVM.Types hiding (Success) import Optics.Core import Optics.Operators.Unsafe import EVM.Effects -import EVM.Expr (maybeLitByte) +import EVM.Expr (maybeLitByteSimp) import Control.Applicative import Control.Monad @@ -730,7 +730,7 @@ stripBytecodeMetadataSym :: [Expr Byte] -> [Expr Byte] stripBytecodeMetadataSym b = let concretes :: [Maybe Word8] - concretes = maybeLitByte <$> b + concretes = maybeLitByteSimp <$> b bzzrs :: [[Maybe Word8]] bzzrs = fmap (Just) . BS.unpack <$> knownBzzrPrefixes candidates = (flip Data.List.isInfixOf concretes) <$> bzzrs diff --git a/test/test.hs b/test/test.hs index 2e76685e1..69027f250 100644 --- a/test/test.hs +++ b/test/test.hs @@ -73,7 +73,7 @@ import EVM.Traversals import EVM.Types hiding (Env) import EVM.Effects import EVM.UnitTest (writeTrace) -import EVM.Expr (maybeLitByte) +import EVM.Expr (maybeLitByteSimp) testEnv :: Env testEnv = Env { config = defaultConfig { @@ -1450,7 +1450,7 @@ tests = testGroup "hevm" , test "jump-into-symbolic-region" $ do let -- our initCode just jumps directly to the end - code = BS.pack . mapMaybe maybeLitByte $ V.toList $ assemble + code = BS.pack . mapMaybe maybeLitByteSimp $ V.toList $ assemble [ OpPush (Lit 0x85) , OpJump , OpPush (Lit 1)