From 5f4e14d544810c8b3c3755dbf85403ce88cd45e5 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 17 Dec 2024 16:52:45 +0100 Subject: [PATCH] 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"