Skip to content

Commit

Permalink
feat: functional implementation of EXTCODEHASH and EXTCODECOPY (#328)
Browse files Browse the repository at this point in the history
  • Loading branch information
karmacoma-eth authored Jul 26, 2024
1 parent 32b81ed commit c969bcd
Show file tree
Hide file tree
Showing 3 changed files with 256 additions and 7 deletions.
47 changes: 40 additions & 7 deletions src/halmos/sevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@
Steps = Dict[int, Dict[str, Any]] # execution tree

EMPTY_BYTES = ByteVec()
EMPTY_KECCAK = con(0xC5D2460186F7233C927E7DB2DCC703C0E500B653CA82273B7BFAD8045D85A470)
MAX_CALL_DEPTH = 1024

# TODO: make this configurable
Expand Down Expand Up @@ -844,7 +845,7 @@ def sha3_data(self, data: Bytes) -> Word:
)
sha3_expr = f_sha3(data)
else:
sha3_expr = BitVec("f_sha3_0", BitVecSort256)
sha3_expr = EMPTY_KECCAK

# assume hash values are sufficiently smaller than the uint max
self.path.append(ULE(sha3_expr, 2**256 - 2**64))
Expand Down Expand Up @@ -2311,15 +2312,47 @@ def finalize(ex: Exec):
ex.path.append(codesize > 0)
ex.st.push(codesize)

# TODO: define f_extcodehash for known addresses in advance
elif opcode == EVM.EXTCODECOPY:
account: Address = uint160(ex.st.pop())
loc: int = int_of(ex.st.pop(), "symbolic EXTCODECOPY offset")
offset: int = int_of(ex.st.pop(), "symbolic EXTCODECOPY offset")
size: int = int_of(ex.st.pop(), "symbolic EXTCODECOPY size")

if size > 0:
end_loc = loc + size
if end_loc > MAX_MEMORY_SIZE:
raise HalmosException("EXTCODECOPY > MAX_MEMORY_SIZE")

# TODO: handle the case where account may alias multiple addresses
account_addr = self.resolve_address_alias(ex, account)
if account_addr is None:
# this could be unsound if the solver in resolve_address_alias
# returns unknown, meaning that there is in fact a must-alias
# address, but we didn't find it in time
warn(
f"EXTCODECOPY: unknown address {hexify(account)} "
"is assumed to have empty bytecode"
)

account_code: Contract = ex.code.get(account_addr) or ByteVec()
codeslice: ByteVec = account_code._code.slice(
offset, offset + size
)
ex.st.memory.set_slice(loc, end_loc, codeslice)

elif opcode == EVM.EXTCODEHASH:
account = uint160(ex.st.pop())
account_addr = self.resolve_address_alias(ex, account)
account_addr = uint160(ex.st.pop())
alias_addr = self.resolve_address_alias(ex, account_addr)
addr = alias_addr if alias_addr is not None else account_addr

account_code: Optional[Contract] = ex.code.get(addr, None)

codehash = (
f_extcodehash(account_addr)
if account_addr is not None
else f_extcodehash(account)
f_extcodehash(addr)
if account_code is None
else ex.sha3_data(account_code._code.unwrap())
)

ex.st.push(codehash)

elif opcode == EVM.CODESIZE:
Expand Down
83 changes: 83 additions & 0 deletions tests/expected/all.json
Original file line number Diff line number Diff line change
Expand Up @@ -786,6 +786,89 @@
"num_bounded_loops": null
}
],
"test/Extcodehash.t.sol:ExtcodehashTest": [
{
"name": "check_extcodehash_a1_eq_a2()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_extcodehash_a1_eq_directHash()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_extcodehash_a1_eq_runtimeCodeHash()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_extcodehash_a1_ne_b1()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_extcodehash_after_etch()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_extcodehash_empty()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_extcodehash_eq_directHash()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_extcodehash_unknown_addr_eq_0()",
"exitcode": 1,
"num_models": 1,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_extcodehash_unknown_addr_noteq_0()",
"exitcode": 1,
"num_models": 1,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
}
],
"test/Foundry.t.sol:DeepFailer": [
{
"name": "check_fail_cheatcode()",
Expand Down
133 changes: 133 additions & 0 deletions tests/regression/test/Extcodehash.t.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,133 @@
// SPDX-License-Identifier: AGPL-3.0
pragma solidity >=0.8.0 <0.9.0;

import "forge-std/Test.sol";
import {SymTest} from "halmos-cheatcodes/SymTest.sol";

contract A {}

contract B {
// make sure bytecode is different from A
function beep() public pure {}
}

contract Empty {
// constructor returns 0-length runtime bytecode
constructor() {
assembly {
return(0, 0)
}
}
}

contract ExtcodehashTest is Test, SymTest {
address a1;
bytes32 a1hash;

function setUp() public {
address _a1 = address(new A());
bytes32 _a1hash;

assembly {
_a1hash := extcodehash(_a1)
}

a1 = _a1;
a1hash = _a1hash;
}

function check_extcodehash_a1_eq_a2() external {
address a2 = address(new A());
bytes32 a2hash;
assembly {
a2hash := extcodehash(a2)
}

// extcodehash(a1) == extcodehash(a2)
assertEq(a1hash, a2hash);
}

function check_extcodehash_a1_ne_b1() external {
address b1 = address(new B());
bytes32 b1hash;
assembly {
b1hash := extcodehash(b1)
}

// extcodehash(a1) != extcodehash(b1)
assertNotEq(a1hash, b1hash);
}

function check_extcodehash_a1_eq_directHash() external {
// extcodehash(a1) == keccak256(extcodecopy(a1))
assertEq(a1hash, keccak256(a1.code));
}

function check_extcodehash_a1_eq_runtimeCodeHash() external {
assertEq(a1hash, keccak256(type(A).runtimeCode));
}

function check_extcodehash_eq_directHash() external {
uint256 thisCodeSize;
assembly {
thisCodeSize := codesize()
}

bytes memory thisCode = new bytes(thisCodeSize);
bytes32 thisCodeHash;
assembly {
codecopy(add(thisCode, 0x20), 0, thisCodeSize)
thisCodeHash := extcodehash(address())
}

// extcodehash(address()) == keccak256(codecopy())
assertEq(thisCodeHash, keccak256(thisCode));
}

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

bytes32 codehash;
assembly {
codehash := extcodehash(emptyCodeAddr)
}

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

/// yields a path where it is eq to 0, and a path where it is not
/// so we expect a counterexample for this and also its negation
function check_extcodehash_unknown_addr_eq_0() external {
bytes32 codehash;
assembly {
codehash := extcodehash(0x1337)
}

assertEq(codehash, 0);
}

/// yields a path where it is eq to 0, and a path where it is not
/// so we expect a counterexample for this and also its negation
function check_extcodehash_unknown_addr_noteq_0() external {
bytes32 codehash;
assembly {
codehash := extcodehash(0x1337)
}

assertNotEq(codehash, 0);
}

function check_extcodehash_after_etch() external {
address who = address(0x1337);
bytes memory code = svm.createBytes(42, "code");
vm.etch(who, code);

bytes32 codehash;
assembly {
codehash := extcodehash(who)
}

assertEq(codehash, keccak256(code));
}
}

0 comments on commit c969bcd

Please sign in to comment.