feat: branching over symbolic call addresses

[daejunpark]

When a call target address may be aliased with multiple existing addresses, or may be non-existent, explicitly branching into multiple paths for each potential alias or non-existent address.

Although this change may increase the number of potential paths, it eliminates the time needed to solve must-alias conditions, which can take up to 1s each. Also, the path branching is unlikely to exponentially grow, unless there are many duplicated instances of contracts with similar interfaces, because most paths will immediately revert due to unimplemented selectors. In such cases, the time saved by reducing solver overhead outweighs the cost of increased path branching.

As a result, "unknown calls" no longer exist, and the related options, --uninterpreted-unknown-calls and --return-size-of-unknown-calls, are no longer needed and have been deprecated.

[daejunpark]

is this correct?

[karmacoma-eth]

there's a weird nuance around dead/empty accounts for which this returns 0

[karmacoma-eth]

py-evm does this:

    if state.account_is_empty(account):
        computation.stack_push_bytes(constants.NULL_BYTE)
    else:
        computation.stack_push_bytes(state.get_code_hash(account))

with

    def account_is_empty(self, address: Address) -> bool:
        return (
            not self.account_has_code_or_nonce(address)
            and self.get_balance(address) == 0
        )

weird but this passes in foundry:

    function test_extcodehash_empty() external {
        address emptyCodeAddr = address(new Empty());
        assertEq(emptyCodeAddr.code.length, 0, "Empty contract should have no code");

        bytes32 codehash;
        bytes32 nextCodehash;
        assembly {
            codehash := extcodehash(emptyCodeAddr)
            nextCodehash := extcodehash(add(emptyCodeAddr, 1))
        }

        assertEq(codehash, keccak256(""), "Expected codehash of the empty string");
        assertEq(nextCodehash, 0, "Expected 0");
    }

[daejunpark]

what? so, extcodehash of a contract account with empty code is different from that of a non-existing account?

so, here we should return 0, based on the current implementation of vms?

[karmacoma-eth]

what? so, extcodehash of a contract account with empty code is different from that of a non-existing account?

yes, https://github.com/ethereum/EIPs/blob/master/EIPS/eip-1052.md#specification is a bit more explicit

The EXTCODEHASH of the account without code is c5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470 what is the keccack256 hash of empty data.
The EXTCODEHASH of non-existent account is 0.
The EXTCODEHASH of a precompiled contract is either c5d246... or 0.

[karmacoma-eth]

so, here we should return 0, based on the current implementation of vms?

we need to have a more proper is_empty check for the account, which is also affected by the balance. This needs to pass:

    function testAccountWithOrWithoutBalance() public {
        address a = address(0x42);
        assertEq(extcodehash(a), bytes32(0), "empty account has extcodehash 0");

        vm.deal(a, 1 ether);
        assertEq(extcodehash(a), 0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470, "account with balance has extcodehash keccak('')");
    }

[karmacoma-eth]

full test:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.18;

import "forge-std/Test.sol";

contract Empty {
    constructor() {
        assembly {
            return(0, 0)
        }
    }
}

contract EmptyDeployerTest is Test {
    function extcodehash(address _addr) public view returns (bytes32) {
        bytes32 hash;
        assembly {
            hash := extcodehash(_addr)
        }
        return hash;
    }

    function testEmptyDeployer() public {
        address a = vm.computeCreateAddress(address(this), vm.getNonce(address(this)));
        assertEq(extcodehash(a), bytes32(0), "empty account has extcodehash 0");
        assertEq(vm.getNonce(a), 0);

        // do deploy
        new Empty();

        assertEq(a.code.length, 0);
        assertEq(extcodehash(a), keccak256(""));
        assertEq(vm.getNonce(a), 1);
    }


    function testAccountWithOrWithoutBalance() public {
        address a = address(0x42);
        assertEq(extcodehash(a), bytes32(0), "empty account has extcodehash 0");

        vm.deal(a, 1 ether);
        assertEq(extcodehash(a), keccak256(""), "account with balance has extcodehash keccak('')");
    }
}

in our case if we don't want to model nonces, we can probably differentiate between not being in code, vs being in code with empty bytecode

[karmacoma-eth]

tangential but related, do you think this test should pass?

    function check_unknown_initial_balance(address addr) public {
        assertEq(addr.balance, 0);
    }

[daejunpark]

tangential but related, do you think this test should pass?

    function check_unknown_initial_balance(address addr) public {
        assertEq(addr.balance, 0);
    }

eventually yes, but in a separate pr. this pr is only for handling code of symbolic addresses.

[karmacoma-eth]

there's a weird nuance around dead/empty accounts for which this returns 0

[karmacoma-eth]

py-evm does this:

    if state.account_is_empty(account):
        computation.stack_push_bytes(constants.NULL_BYTE)
    else:
        computation.stack_push_bytes(state.get_code_hash(account))

with

    def account_is_empty(self, address: Address) -> bool:
        return (
            not self.account_has_code_or_nonce(address)
            and self.get_balance(address) == 0
        )

weird but this passes in foundry:

    function test_extcodehash_empty() external {
        address emptyCodeAddr = address(new Empty());
        assertEq(emptyCodeAddr.code.length, 0, "Empty contract should have no code");

        bytes32 codehash;
        bytes32 nextCodehash;
        assembly {
            codehash := extcodehash(emptyCodeAddr)
            nextCodehash := extcodehash(add(emptyCodeAddr, 1))
        }

        assertEq(codehash, keccak256(""), "Expected codehash of the empty string");
        assertEq(nextCodehash, 0, "Expected 0");
    }