Fix evm's make_symbolic_address (#1318)

* Fix evm's make_symbolic_address

The code that created a constrain for created symbolic address was
unreachable.

* Add testcase for make_symbolic_address

manticore/ethereum/manticore.py

@@ -134,21 +134,31 @@ def make_symbolic_value(self, nbits=256, name=None):
         return self.constraints.new_bitvec(nbits, name=name, avoid_collisions=avoid_collisions)
 
     def make_symbolic_address(self, name=None, select='both'):
+        """
+        Creates a symbolic address and constrains it to pre-existing addresses or the 0 address.
+
+        :param name: Name of the symbolic variable. Defaults to 'TXADDR' and later to 'TXADDR_<number>'
+        :param select: Whether to select contracts or normal accounts. Not implemented for now.
+        :return: Symbolic address in form of a BitVecVariable.
+        """
         if select not in ('both', 'normal', 'contract'):
             raise EthereumError('Wrong selection type')
         if select in ('normal', 'contract'):
             # FIXME need to select contracts or normal accounts
             raise NotImplemented
+
         avoid_collisions = False
         if name is None:
             name = 'TXADDR'
             avoid_collisions = True
-        return self.constraints.new_bitvec(160, name=name, avoid_collisions=avoid_collisions)
+
+        symbolic_address = self.constraints.new_bitvec(160, name=name, avoid_collisions=avoid_collisions)
 
         constraint = symbolic_address == 0
-        for contract_account_i in map(int, self._accounts.values()):
-            constraint = Operators.OR(symbolic_address == contract_account_i, constraint)
+        for account in self._accounts.values():
+            constraint = Operators.OR(symbolic_address == int(account), constraint)
         self.constrain(constraint)
+
         return symbolic_address
 
     def constrain(self, constraint):

tests/eth_general.py

@@ -759,11 +759,59 @@ def test_call_with_concretized_args(self):
         owner = m.create_account(balance=10**10)
         contract = m.solidity_create_contract(contract_src, owner=owner)
         receiver = m.create_account(0)
+
         symbolic_address = m.make_symbolic_address()
+
         m.constrain(symbolic_address == receiver.address)
         contract.transferHalfTo(symbolic_address, caller=owner, value=m.make_symbolic_value())
+
+        running_states = list(m.running_states)
+
+        self.assertEqual(len(running_states), 2)
         self.assertTrue(any(state.can_be_true(state.platform.get_balance(receiver.address) > 0)
-                                for state in m.running_states))
+                                for state in running_states))
+
+    def test_make_symbolic_address(self):
+        def get_state():
+            """Returns one state and asserts that there is ONLY ONE."""
+            states = list(self.mevm.running_states)
+            self.assertEqual(len(states), 1)
+            return states[0]
+
+        init_state = get_state()
+
+        symbolic_address1 = self.mevm.make_symbolic_address()
+        self.assertEqual(symbolic_address1.name, 'TXADDR')
+
+        # sanity check: creating a symbolic address should not create a new state
+        self.assertIs(get_state(), init_state)
+
+        # TEST 1: the 1st symbolic address should be constrained only to 0 (as there are no other accounts yet!)
+        possible_addresses1 = init_state.solve_n(symbolic_address1, 10)
+        self.assertEqual(possible_addresses1, [0])
+
+        owner = self.mevm.create_account(balance=1)
+
+        # TEST 2: the 2nd symbolic address should be constrained to OR(owner_address, 0)
+        symbolic_address2 = self.mevm.make_symbolic_address()
+        self.assertEqual(symbolic_address2.name, 'TXADDR_1')
+
+        self.assertEqual(get_state().solve_n(symbolic_address2, 10), [int(owner), 0])
+
+        contract = self.mevm.solidity_create_contract('contract C {}', owner=owner)
+
+        # TEST 3: the 3rd symbolic address should be constrained to OR(contract_address, 0, owner_address)
+        symbolic_address3 = self.mevm.make_symbolic_address()
+        self.assertEqual(symbolic_address3.name, 'TXADDR_2')
+
+        state = get_state()
+
+        self.assertEqual(state.solve_n(symbolic_address3, 10), [int(contract), 0, int(owner)])
+
+        # NOTE: The 1st and 2nd symbolic addresses are still constrained to 0 and OR(owner_address, 0)
+        # as the constrains are not reevaluated. They are created/assigned only once: when we create symbolic address.
+        self.assertEqual(state.solve_n(symbolic_address1, 10), [0])
+        self.assertEqual(state.solve_n(symbolic_address2, 10), [int(owner), 0])
 
     def test_end_instruction_trace(self):
         """