Skip to content

Commit

Permalink
Merge branch 'main' into chore-workflows
Browse files Browse the repository at this point in the history
  • Loading branch information
karmacoma-eth committed Jul 26, 2024
2 parents 440d484 + 29827c4 commit 6ea8f8b
Show file tree
Hide file tree
Showing 4 changed files with 271 additions and 7 deletions.
15 changes: 15 additions & 0 deletions packages/solvers/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,21 @@ done
| Z3 | 4.13.1 | [Z3Prover/z3](https://github.com/Z3Prover/z3) | Includes a [Dockerfile](https://github.com/Z3Prover/z3/blob/master/docker/ubuntu-20-04.Dockerfile) and a package but no `latest` tag |


## Contributing

Everyone is welcome to contribute new solvers or new versions to the image via pull requests. If a solver is competitive at [SMT-COMP](https://smt-comp.github.io), it would be great to have it included in the image.

When possible, we prefer release binaries from an official source like the Github releases for the project to minimize the time it takes to build the image. If you're unsure about a particular solver or how to integrate it, consider reaching out on the [Halmos Dev Chat](https://t.me/+4UhzHduai3MzZmUx).

Before opening the pull request, please test your changes by verifying:

* that you can build the image locally
* that you can correctly invoke the solver as described in the [Quick Start](https://github.com/a16z/halmos/tree/main/packages/solvers#quick-start) section
* update this README with the name, version and source of the solver

Thank you in advance!


## Credit

Based on [EmperorOrokuSaki/solvers](https://github.com/EmperorOrokuSaki/solvers)
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 6ea8f8b

Please sign in to comment.