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..369b65e61 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 (maybeLitWordSimp, maybeLitAddrSimp) data AssertionType = DSTest | Forge deriving (Eq, Show, Read, ParseField) @@ -489,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" @@ -511,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 55b43b1b2..5750ea84f 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 (maybeLitByteSimp, maybeLitWordSimp, maybeLitAddrSimp) import Control.Monad (unless, when) import Control.Monad.ST (ST) @@ -281,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 @@ -296,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 @@ -741,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 @@ -759,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 @@ -914,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 @@ -1178,7 +1176,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 -> @@ -1593,28 +1591,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 @@ -1666,7 +1664,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) @@ -1691,7 +1689,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 @@ -1700,7 +1698,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 @@ -2056,7 +2054,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 @@ -2653,7 +2651,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)) @@ -2692,7 +2690,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) @@ -2717,7 +2715,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) @@ -2745,7 +2743,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/ABI.hs b/src/EVM/ABI.hs index 58d97dcc2..861c40e8f 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 (maybeLitWordSimp) import Control.Applicative ((<|>)) import Control.Monad (replicateM, replicateM_, forM_, void) @@ -511,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 c6e1e4e9f..c415cf0b3 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 (maybeLitByteSimp, maybeLitWordSimp) import Control.Arrow ((>>>), second) import Data.Aeson (Value) @@ -138,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 @@ -153,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 903288258..2351773ff 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) @@ -297,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 @@ -352,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 all 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 @@ -530,7 +531,7 @@ toList buf = case bufLength buf of fromList :: V.Vector (Expr Byte) -> Expr Buf fromList bs = case all 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 @@ -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) @@ -1484,7 +1482,7 @@ padBytesLeft n bs joinBytes :: [Expr Byte] -> Expr EWord joinBytes bs - | all isLitByte bs = Lit . bytesToW256 . (mapMaybe maybeLitByte) $ bs + | all isLitByte bs = Lit . bytesToW256 . (mapMaybe maybeLitByteSimp) $ bs | otherwise = let bytes = padBytesLeft 32 bs in JoinBytes @@ -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 + +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) + _ -> Nothing + +maybeLitAddrSimp :: Expr EAddr -> Maybe Addr +maybeLitAddrSimp e = case (concKeccakSimpExpr e) of + LitAddr a -> Just a + _ -> Nothing + +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 d58b8bb94..53aa2fe55 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(..)) import EVM.Types +import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp) import Control.Arrow ((>>>)) import Optics.Core @@ -218,7 +219,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) -> @@ -236,7 +237,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 -> @@ -281,7 +282,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 -> textValue abiType (ConcreteBuf (word256Bytes w)) _ -> "" @@ -376,7 +377,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/Solidity.hs b/src/EVM/Solidity.hs index 3b48f72aa..2670a55db 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 (maybeLitByteSimp) import Control.Applicative import Control.Monad @@ -729,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/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 9e094f858..95db2849b 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -45,6 +45,7 @@ import EVM.Stepper (Stepper) import EVM.Stepper qualified as Stepper import EVM.Traversals import EVM.Types +import EVM.Expr (maybeConcStoreSimp) import GHC.Conc (getNumProcessors) import GHC.Generics (Generic) import Optics.Core @@ -653,7 +654,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/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 e69e79c19..d8a4e2f24 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 (maybeLitWordSimp) import Control.Monad (void, when, forM, forM_) import Control.Monad.ST (RealWorld, ST, stToIO) @@ -338,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 +415,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 +469,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 f3eb0487e..f7e6bdac8 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 (maybeLitWordSimp, maybeLitAddrSimp) import Optics.Core import Control.Arrow ((***), (&&&)) @@ -235,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 @@ -533,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 diff --git a/test/test.hs b/test/test.hs index aa4cd8346..69027f250 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 (maybeLitByteSimp) testEnv :: Env testEnv = Env { config = defaultConfig { @@ -447,6 +449,24 @@ 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" + 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 "" @@ -1430,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) @@ -4597,3 +4617,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"