Take into account if it's an address or not

src/EVM.hs

@@ -1607,7 +1607,7 @@ notStatic continue = do
 
 forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()
 forceAddr n msg continue = case wordToAddr n of
-  Nothing -> manySolutions n $ \case
+  Nothing -> manySolutions n True $ \case
     Just sol -> continue $ LitAddr (truncateToAddr sol)
     Nothing -> fallback
   Just c -> continue c
@@ -1617,15 +1617,15 @@ forceAddr n msg continue = case wordToAddr n of
 
 forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
 forceConcrete n msg continue = case maybeLitWordSimp n of
-  Nothing -> manySolutions n $ maybe fallback continue
+  Nothing -> manySolutions n False $ maybe fallback continue
   Just c -> continue c
   where fallback = do
           vm <- get
           partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])
 
 forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()
 forceConcreteAddr n msg continue = case maybeLitAddrSimp n of
-  Nothing -> manySolutions (WAddr n) $ maybe fallback $ \c -> continue $ unsafeInto c
+  Nothing -> manySolutions (WAddr n) True $ maybe fallback $ \c -> continue (truncateToAddr c)
   Just c -> continue c
   where fallback = do
           vm <- get
@@ -1726,7 +1726,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
                     , context = newContext
                     }
   case maybeLitWordSimp abi of
-    Nothing -> manySolutions abi $ \case
+    Nothing -> manySolutions abi False $ \case
       Just concAbi -> runCheat concAbi input
       Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi])
     Just concAbi -> runCheat concAbi input
@@ -2986,7 +2986,7 @@ instance VMOps Symbolic where
       choosePath loc Unknown =
         choose . PleaseChoosePath condSimp $ choosePath loc . Case
 
-  manySolutions ewordExpr continue = do
+  manySolutions ewordExpr isAddr continue = do
     pathconds <- use #constraints
     query $ PleaseGetSol ewordExpr pathconds $ \case
       Just concVals -> do
@@ -3139,7 +3139,7 @@ instance VMOps Concrete where
   whenSymbolicElse _ a = a
   partial _ = internalError "won't happen during concrete exec"
   branch (forceLit -> cond) continue = continue (cond > 0)
-  manySolutions _ _ = internalError "SMT solver should never be needed in concrete mode"
+  manySolutions _ _ _ = internalError "SMT solver should never be needed in concrete mode"
 
 -- Create symbolic VM from concrete VM
 symbolify :: VM Concrete s -> VM Symbolic s

src/EVM/Fetch.hs

@@ -214,9 +214,9 @@ oracle solvers info q = do
          -- Is is possible to satisfy the condition?
          continue <$> checkBranch solvers (branchcondition ./= (Lit 0)) pathconds
 
-    PleaseGetSol symAddr pathconditions continue -> do
+    PleaseGetSol symExpr isAddr pathconditions continue -> do
          let pathconds = foldl' PAnd (PBool True) pathconditions
-         continue <$> getSolutions solvers symAddr pathconds
+         continue <$> getSolutions solvers symExpr isAddr pathconds
 
     PleaseFetchContract addr base continue -> do
       contract <- case info of
@@ -245,8 +245,8 @@ 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 -> Prop -> m (Maybe [W256])
-getSolutions solvers symAddr pathconditions = do
+getSolutions :: forall m . App m => SolverGroup -> Expr EWord -> Bool -> Prop -> m (Maybe [W256])
+getSolutions solvers symExpr isAddr pathconditions = do
   conf <- readConfig
   liftIO $ do
     ret <- collectSolutions [] 100 pathconditions conf
@@ -257,20 +257,22 @@ getSolutions solvers symAddr pathconditions = do
         _ -> pure $ Just r
     where
       collectSolutions :: [W256] -> Int -> Prop -> Config -> IO (Maybe [W256])
-      collectSolutions addrs maxSols conds conf = do
-        if (length addrs > maxSols) then pure Nothing
+      collectSolutions vals maxSols conds conf = do
+        if (length vals > maxSols) then pure Nothing
         else
-          checkSat solvers (assertProps conf [(PEq (Var "addrQuery") symAddr) .&& conds]) >>= \case
+          checkSat solvers (assertProps conf [(PEq (Var "addrQuery") symExpr) .&& conds]) >>= \case
             Sat (SMTCex vars _ _ _ _ _)  -> case (Map.lookup (Var "addrQuery") vars) of
-              Just addr -> do
-                let newConds = Expr.simplifyProp $ PAnd conds (symAddr ./= Lit addr)
-                when conf.debug $ putStrLn $ "Got one solution to symbolic query:" <> show addr <> " now have "  <>
-                  show (length addrs + 1) <> " solution(s), max is: " <> show maxSols
-                collectSolutions (addr:addrs) maxSols newConds conf
+              Just v -> do
+                let cond = if isAddr then (And symExpr (Lit 0xffffffffffffffffffffffffffffffffffffffff)) ./= Lit (fromIntegral (truncateToAddr v))
+                              else symExpr ./= Lit v
+                    newConds = Expr.simplifyProp $ PAnd conds cond
+                when conf.debug $ putStrLn $ "Got one solution to symbolic query:" <> show v <> " now have "  <>
+                  show (length vals + 1) <> " solution(s), max is: " <> show maxSols
+                collectSolutions (v:vals) maxSols newConds conf
               _ -> internalError "No solution to symbolic query"
             Unsat -> do
               when conf.debug $ putStrLn "No more solution(s) to symbolic query."
-              pure $ Just addrs
+              pure $ Just vals
             -- Error or timeout, we need to be conservative
             res -> do
               when conf.debug $ putStrLn $ "Symbolic query result is neither SAT nor UNSAT:" <> show res

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 -> [Prop] -> (Maybe [W256] -> EVM Symbolic s ()) -> Query Symbolic s
+  PleaseGetSol        :: 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,8 +618,10 @@ instance Show (Query t s) where
       (("<EVM.Query: ask SMT about "
         ++ show condition ++ " in context "
         ++ show constraints ++ ">") ++)
-    PleaseGetSol expr constraints _ ->
-      (("<EVM.Query: ask SMT to get W256 for expression "
+    PleaseGetSol expr isAddr constraints _ ->
+      (("<EVM.Query: ask SMT "
+        ++ if isAddr then "for address " else "for value "
+        ++ "to get W256 for expression "
         ++ show expr ++ " in context "
         ++ show constraints ++ ">") ++)
     PleaseDoFFI cmd env _ ->
@@ -862,7 +864,7 @@ class VMOps (t :: VMType) where
 
   partial :: PartialExec -> EVM t s ()
   branch :: Expr EWord -> (Bool -> EVM t s ()) -> EVM t s ()
-  manySolutions :: Expr EWord -> (Maybe W256 -> EVM t s ()) -> EVM t s ()
+  manySolutions :: Expr EWord -> Bool -> (Maybe W256 -> EVM t s ()) -> EVM t s ()
 
 -- Bytecode Representations ------------------------------------------------------------------------