Handle symbolic balance arg (#1394)

* Handle symbolic balance arg

* Make a call for balance

* Handle additional case for bitvecs

mythril/laser/ethereum/instructions.py

@@ -904,12 +904,14 @@ class Instruction:
         """
         state = global_state.mstate
         address = state.stack.pop()
-
-        account = global_state.world_state.accounts_exist_or_load(
-            address.value, self.dynamic_loader
-        )
-
-        balance = account.balance()
+        if address.symbolic is False:
+            balance = global_state.world_state.accounts_exist_or_load(
+                address, self.dynamic_loader
+            ).balance()
+        else:
+            balance = symbol_factory.BitVecVal(0, 256)
+            for account in global_state.world_state.accounts.values():
+                balance = If(address == account.address, account.balance(), balance)
         state.stack.append(balance)
         return [global_state]
 

mythril/laser/ethereum/state/world_state.py

@@ -87,6 +87,8 @@ class WorldState:
             addr_bitvec = symbol_factory.BitVecVal(addr, 256)
         elif not isinstance(addr, BitVec):
             addr_bitvec = symbol_factory.BitVecVal(int(addr, 16), 256)
+        else:
+            addr_bitvec = addr
 
         if addr_bitvec.value in self.accounts:
             return self.accounts[addr_bitvec.value]