Simplify before solve

ethereum · Jan 15, 2025 · c32f353 · c32f353
1 parent 603b5af
commit c32f353
Showing 1 changed file with 7 additions and 5 deletions.
diff --git 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."