From b022fcdf0e52cee3f97cb4d4c7314a4ef6c557d1 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Wed, 11 Dec 2024 21:17:23 -0800 Subject: [PATCH] fix test --- src/halmos/sevm.py | 4 ++-- tests/regression/test/Snapshot.t.sol | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 457ac3e2..5ebb8359 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -856,9 +856,9 @@ def __init__(self): self._mapping = defaultdict(lambda: defaultdict(dict)) def digest(self) -> bytes: - # NOTE: 256-bit size is used, as the first key (slot) can be 256-bit. m = hashlib.sha3_256() for keys, val in self._mapping.items(): + # NOTE: 256-bit size is used, as the first key (slot) can be 256-bit. for key in keys: m.update(int.to_bytes(key, length=32)) m.update(int.to_bytes(val.get_id(), length=32)) @@ -871,9 +871,9 @@ def __init__(self): self._mapping = {} def digest(self) -> bytes: - # NOTE: 256-bit size is used for consistency with SolidityStorageData m = hashlib.sha3_256() for key, val in self._mapping.items(): + # NOTE: 256-bit size is used for consistency with SolidityStorageData m.update(int.to_bytes(key, length=32)) m.update(int.to_bytes(val.get_id(), length=32)) return m.digest() diff --git a/tests/regression/test/Snapshot.t.sol b/tests/regression/test/Snapshot.t.sol index b26a6e26..add68b20 100644 --- a/tests/regression/test/Snapshot.t.sol +++ b/tests/regression/test/Snapshot.t.sol @@ -21,6 +21,7 @@ contract SnapshotTest is SymTest, Test { c = new C(); } + /// @custom:halmos --storage-layout solidity function check_snapshot() public { uint storage0 = svm.snapshotStorage(address(c)); uint state0 = vm.snapshotState(); @@ -45,6 +46,7 @@ contract SnapshotTest is SymTest, Test { console.log(storage2); console.log(state2); + // NOTE: failed with the generic storage layout, as the whole storage is an smt array assertEq(storage1, storage2); assertEq(state1, state2); @@ -65,6 +67,7 @@ contract SnapshotTest is SymTest, Test { console.log(storage4); console.log(state4); + // NOTE: failed with the generic storage layout, as the whole storage is an smt array assertEq(storage2, storage4); assertEq(state2, state4); }