Performing concKeccakSimpExpr before forcing to concrete value

This should alleviate issues with symbolic expression errors

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 (maybeLitWord, maybeLitAddr)
 
 data AssertionType = DSTest | Forge
   deriving (Eq, Show, Read, ParseField)

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)

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)

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)

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
+

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

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

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

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

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)

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 ((***), (&&&))

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"