From 7da6bd957ea87e5876f1f071bc064f6b611b3100 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 13 Jan 2025 18:04:22 +0100 Subject: [PATCH] Multi-solution now --- src/EVM.hs | 2 +- src/EVM/Fetch.hs | 2 +- src/EVM/Types.hs | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/EVM.hs b/src/EVM.hs index a55eb270a..7298c68e2 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -2988,7 +2988,7 @@ instance VMOps Symbolic where manySolutions ewordExpr isAddr continue = do pathconds <- use #constraints - query $ PleaseGetSol ewordExpr isAddr pathconds $ \case + query $ PleaseGetSols ewordExpr isAddr pathconds $ \case Just concVals -> do assign #result Nothing case (length concVals) of diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index d10a19bd7..687de2cef 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -214,7 +214,7 @@ oracle solvers info q = do -- Is is possible to satisfy the condition? continue <$> checkBranch solvers (branchcondition ./= (Lit 0)) pathconds - PleaseGetSol symExpr isAddr pathconditions continue -> do + PleaseGetSols symExpr isAddr pathconditions continue -> do let pathconds = foldl' PAnd (PBool True) pathconditions continue <$> getSolutions solvers symExpr isAddr pathconds diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index f3aa1c021..c18648db8 100644 --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -594,7 +594,7 @@ data Query t s where PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s - PleaseGetSol :: Expr EWord -> Bool -> [Prop] -> (Maybe [W256] -> EVM Symbolic s ()) -> Query Symbolic s + PleaseGetSols :: Expr EWord -> Bool -> [Prop] -> (Maybe [W256] -> EVM Symbolic s ()) -> Query Symbolic s PleaseDoFFI :: [String] -> Map String String -> (ByteString -> EVM t s ()) -> Query t s PleaseReadEnv :: String -> (String -> EVM t s ()) -> Query t s @@ -618,7 +618,7 @@ instance Show (Query t s) where (("") ++) - PleaseGetSol expr isAddr constraints _ -> + PleaseGetSols expr isAddr constraints _ -> (("