make_symbolic_address constraints

[disconnect3d]

There is some code in make_symbolic_address which is not reachable:

https://github.com/trailofbits/manticore/blob/master/manticore/ethereum/manticore.py#L136-L152

It seems that the return self.constraints.new_bitvec(160, name=name, avoid_collisions=avoid_collisions) should be in the if condition? return should be a symbolic_address variable instead.

---

EDIT:
The initial issue has been fixed, but there is some discussion and concerns regarding the constraints we apply in make_symbolic_address. TLDR: We should delay those contraints until a moment they are used.

[disconnect3d]

Please see PR #1318.

For now it brings back the constrains for symbolic addresses.

I have one concern for that: we apply a constrain such as OR(0, <account addresses...>) when we create the symbolic address. This means that when we do:

m = ManticoreEVM()

sa1 = m.make_symbolic_address()

owner = m.create_account(balance=1)

sa2 = m.make_symbolic_address()

contract = m.solidity_create_contract(...)

sa3 = m.make_symbolic_address()

The symbolic addresses have such constrains:

• sa1 = 0
• sa2 = OR(0, owner)
• sa3 = OR(0, owner, contract)

This behavior is tested in #1318.

Is this solution good enough for our needs? Maybe the constrain should be applied only if the user explicitly wants it? Or maybe there should be a flag to not apply the constrains? (I bet users might not be that aware to use a flag to explicitly set the constrains).

On the other hand it would probably be good to delay the constrains as much as possible (e.g. when the symbolic address is used). However this may take some effort to implement properly.

[feliam]

The name "make_symbolic_address" may be misleading.
We should check some usecases. For example how this compares with just making a free symbolic 160bitvec?

This constraining thing is a way to hint the values to be used in the concretization.
I'm thinking we could use a free symbolic 160 bitvec as an address and taint it with some specific taints: ADDRESS, USERADDRESS, CONTRACTADDRESS.
Then let the concretization procedure check for it and make it so it ranges over the interesting values. (aka delay the constraint as much as possible)

[disconnect3d]

@feliam I'm putting it as idea and priority-low as I am not sure if we want to focus on this atm.