Skip to content

Commit

Permalink
Update
Browse files Browse the repository at this point in the history
  • Loading branch information
msooseth committed Jan 13, 2025
1 parent 7da6bd9 commit 19cf8d8
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions src/EVM/Fetch.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down

0 comments on commit 19cf8d8

Please sign in to comment.