extcodehash behave as a symbolic value

[simon-something]

Describe the bug While calling the extcodehash on a concrete address (either eoa or contract), a concrete hash image would be expected. Instead, the returned value behave as a symbolic one.

To Reproduce While running this code snippet as context, in a Counter example repo:

function check_extcodehash() public {
    address firstImplementation = address(new Counter());
    address secondImplementation = address(new Counter());

    bytes32 firstHash;
    bytes32 secondHash;

    assembly {
        firstHash := extcodehash(firstImplementation)
        secondHash := extcodehash(secondImplementation)
    }

the following assertions produce these results: assert(firstHash == secondHash); fails assert(firstHash != secondHash); fails assert(firstHash == secondHash || firstHash != secondHash); passes

This same example can be reproduced with 2 EOA as well.

Environment:

• OS: macOS
• Python version: 3.10.4
• Halmos and other dependency versions: 0.1.13

Additional context This is relevant as extcodehash was used by OpenZeppelin isContract(address) in the Address lib (now removed, but some older repo still rely on it for, for instance, proxy implementation migration)

[simon-something]

Tagging @karmacoma-eth as we discussed it over telegram

[0xkarmacoma]

ok this is unfortunate behavior, but it seems expected atm because extcodehash is modeled as a bare uninterpreted function.

If we log firstHash and secondHash, we get:

[console.log] f_extcodehash(0x00000000000000000000000000000000aaaa0002)
[console.log] f_extcodehash(0x00000000000000000000000000000000aaaa0003)

so as far as the solver is involved, they could be the same, and they could be different.

To fix this, we need to implement the full behavior of extcodehash

[daejunpark]

this should be fixed by #328. please feel free to reopen if the issue persists. thank you!