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 ca508ce92..535868991 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 @@ -476,7 +477,7 @@ formatSomeExpr :: SomeExpr -> Text formatSomeExpr (SomeExpr e) = formatExpr e formatSomeExprSimp :: SomeExpr -> Text -formatSomeExprSimp (SomeExpr e) = formatExpr (Expr.simplify e) +formatSomeExprSimp (SomeExpr e) = formatExpr (Expr.concKeccakSimpExpr e) formatExpr :: Expr a -> Text formatExpr = go 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 c12652264..e36dccbb9 100644 --- a/test/test.hs +++ b/test/test.hs @@ -73,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 {