From f2ae438cce6f945de0380fba79eec900df0f219d Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Fri, 11 Oct 2024 18:36:30 -0700 Subject: [PATCH] fix: hash value range assumption only for symbolic ones --- src/halmos/sevm.py | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 39338e9f..cae904e5 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -1156,6 +1156,16 @@ def sha3_data(self, data: Bytes) -> Word: if sha3_hash is not None: self.path.append(sha3_expr == bytes_to_bv_value(sha3_hash)) + # ensure the hash value is within the safe range assumed below + sha3_hash_int = int.from_bytes(sha3_hash, "big") + if sha3_hash_int == 0 or sha3_hash_int > 2**256 - 2**64: + raise HalmosException(f"hash value outside expected range: {sha3_hash.hex()}") + + else: + # assume hash values are non-zero and sufficiently small to prevent overflow when adding reasonable offsets + self.path.append(sha3_expr != ZERO) + self.path.append(ULE(sha3_expr, 2**256 - 2**64)) + # assume no hash collision self.assume_sha3_distinct(sha3_expr) @@ -1190,11 +1200,6 @@ def assume_sha3_distinct(self, sha3_expr) -> None: # inputs have different sizes: assume the outputs are different self.path.append(sha3_expr != prev_sha3_expr) - # assume hash values are non-zero and sufficiently smaller than the uint max - # TODO: assume they are sufficiently larger than 0 - self.path.append(sha3_expr != ZERO) - self.path.append(ULE(sha3_expr, 2**256 - 2**64)) - self.sha3s[sha3_expr] = len(self.sha3s) def new_gas_id(self) -> int: