From 0e3d2daa2c347931f55d7f6beccac864477754ce Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Thu, 27 Mar 2025 17:40:26 -0700 Subject: [PATCH 1/2] fix: we do support empty bytes now --- tests/regression/test/Sha3.t.sol | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/tests/regression/test/Sha3.t.sol b/tests/regression/test/Sha3.t.sol index 054c58396..793e0f41e 100644 --- a/tests/regression/test/Sha3.t.sol +++ b/tests/regression/test/Sha3.t.sol @@ -37,9 +37,8 @@ contract Sha3Test is Test, SymTest { function check_empty_hash_value() public { assertEq(keccak256(""), EMPTY_HASH); - // TODO: uncomment when we support empty bytes - // bytes memory data = svm.createBytes(0, "data"); - // assertEq(keccak256(data), EMPTY_HASH); + bytes memory data = svm.createBytes(0, "data"); + assertEq(keccak256(data), EMPTY_HASH); } function check_only_empty_bytes_matches_empty_hash(bytes memory data) public { From 518857ef0ff0402943159c573431c973e7c5e775 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Thu, 27 Mar 2025 17:41:24 -0700 Subject: [PATCH 2/2] fix: apply preimage handling both PUSH and MLOAD --- src/halmos/sevm.py | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index ef0802a99..82f4bfec0 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -1785,6 +1785,18 @@ def assume_sha3_distinct(self, sha3_expr: BitVecRef) -> None: self.sha3s[sha3_expr] = len(self.sha3s) + def try_preimage_sha3_hash(self, val): + if val.is_concrete: + if (inverse := sha3_inv.get(val.value)) is not None: + # restore precomputed hashes + return BV(self.sha3_data(con(inverse)), size=256) + + # TODO: support more commonly used concrete keccak values + elif val.value == EMPTY_KECCAK: + return BV(self.sha3_data(b""), size=256) + + return val + def new_gas_id(self) -> int: self.cnts["gas"] += 1 return self.cnts["gas"] @@ -3307,21 +3319,8 @@ def finalize(ex: Exec): elif opcode == OP_PUSH32: val = insn.operand assert val.size == 256 - - # Special handling for PUSH32 with concrete values - if val.is_concrete: - if (inverse := sha3_inv.get(val.value)) is not None: - # restore precomputed hashes - state.push_any(ex.sha3_data(con(inverse))) - - # TODO: support more commonly used concrete keccak values - elif val.value == EMPTY_KECCAK: - state.push_any(ex.sha3_data(b"")) - else: - state.push(val) - else: - # Symbolic value - state.push(val) + val = ex.try_preimage_sha3_hash(val) + state.push(val) elif opcode == OP_POP: state.pop() @@ -3408,7 +3407,9 @@ def finalize(ex: Exec): elif opcode == OP_MLOAD: loc: int = ex.mloc(check_size=True) - state.push_any(state.memory.get_word(loc)) + val = BV(state.memory.get_word(loc), size=256) + val = ex.try_preimage_sha3_hash(val) + state.push(val) elif opcode == OP_PUSH0: state.push(ZERO)