From c32f35319e82dca225f4e3e21723fdb609e034f8 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 15 Jan 2025 19:26:46 +0100
Subject: [PATCH] Simplify before solve

---
 src/EVM/Fetch.hs | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
index c51510a1b..fc31c2cbb 100644
--- a/src/EVM/Fetch.hs
+++ b/src/EVM/Fetch.hs
@@ -248,10 +248,12 @@ oracle solvers info q = do
 type Fetcher t m s = App m => Query t s -> m (EVM t s ())
 
 getSolutions :: forall m . App m => SolverGroup -> Expr EWord -> Int -> Prop -> m (Maybe [W256])
-getSolutions solvers symExpr numBytes pathconditions = do
+getSolutions solvers symExprPreSimp numBytes pathconditions = do
   conf <- readConfig
   liftIO $ do
-    ret <- collectSolutions [] 100 pathconditions conf
+    let symExpr = Expr.concKeccakSimpExpr symExprPreSimp
+    when conf.debug $ putStrLn $ "Collecting solutions to symbolic query: " <> show symExpr
+    ret <- collectSolutions [] 100 symExpr pathconditions conf
     case ret of
       Nothing -> pure Nothing
       Just r -> case length r of
@@ -261,8 +263,8 @@ getSolutions solvers symExpr numBytes pathconditions = do
       createHexValue k =
           let hexString = concat (replicate k "ff")
           in fst . head $ readHex hexString
-      collectSolutions :: [W256] -> Int -> Prop -> Config -> IO (Maybe [W256])
-      collectSolutions vals maxSols conds conf = do
+      collectSolutions :: [W256] -> Int -> Expr EWord -> Prop -> Config -> IO (Maybe [W256])
+      collectSolutions vals maxSols symExpr conds conf = do
         if (length vals > maxSols) then pure Nothing
         else
           checkSat solvers (assertProps conf [(PEq (Var "addrQuery") symExpr) .&& conds]) >>= \case
@@ -275,7 +277,7 @@ getSolutions solvers symExpr numBytes pathconditions = do
                     showedVal = "val: 0x" <> (showHex maskedVal "")
                 when conf.debug $ putStrLn $ "Got one solution to symbolic query," <> showedVal <> " now have " <>
                   show (length vals + 1) <> " solution(s), max is: " <> show maxSols
-                collectSolutions (maskedVal:vals) maxSols newConds conf
+                collectSolutions (maskedVal:vals) maxSols symExpr newConds conf
               _ -> internalError "No solution to symbolic query"
             Unsat -> do
               when conf.debug $ putStrLn "No more solution(s) to symbolic query."