diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index 687de2cef..ecbdf5824 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -30,6 +30,7 @@ import Control.Monad.IO.Class import Control.Monad (when) import EVM.Effects import qualified EVM.Expr as Expr +import Numeric (showHex) -- | Abstract representation of an RPC fetch request data RpcQuery a where @@ -263,10 +264,12 @@ getSolutions solvers symExpr isAddr pathconditions = do checkSat solvers (assertProps conf [(PEq (Var "addrQuery") symExpr) .&& conds]) >>= \case Sat (SMTCex vars _ _ _ _ _) -> case (Map.lookup (Var "addrQuery") vars) of Just v -> do - let cond = if isAddr then (And symExpr (Lit 0xffffffffffffffffffffffffffffffffffffffff)) ./= Lit (fromIntegral (truncateToAddr v)) + let truncated = truncateToAddr v + cond = if isAddr then (And symExpr (Lit 0xffffffffffffffffffffffffffffffffffffffff)) ./= Lit (fromIntegral truncated) else symExpr ./= Lit v newConds = Expr.simplifyProp $ PAnd conds cond - when conf.debug $ putStrLn $ "Got one solution to symbolic query:" <> show v <> " now have " <> + showedVal = if isAddr then "addr: 0x" <> (showHex truncated "") else ("value: 0x" <> showHex v "") + when conf.debug $ putStrLn $ "Got one solution to symbolic query," <> showedVal <> " now have " <> show (length vals + 1) <> " solution(s), max is: " <> show maxSols collectSolutions (v:vals) maxSols newConds conf _ -> internalError "No solution to symbolic query"