Making progress

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
@@ -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

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

@@ -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 {