Merge pull request #619 from ethereum/better-debug

Fixing missing `concKeccakSimpExpr` for `wordToAddr`, `maybeLitByte`, etc.

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

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

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)
 

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

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

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
+

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))
                 _ -> "<symbolic>"
 
@@ -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" <> "]"