From ca4f4c332fd014147ba2ec83e1382cc259ee6821 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Fri, 11 Oct 2024 15:11:29 -0700
Subject: [PATCH] support empty keccak

---
 src/halmos/sevm.py               | 16 +++++++++++-----
 src/halmos/utils.py              |  4 ++++
 tests/expected/all.json          | 18 ++++++++++++++++++
 tests/regression/test/Sha3.t.sol |  6 +-----
 4 files changed, 34 insertions(+), 10 deletions(-)

diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index 962edb5b..d4feeb49 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -100,6 +100,7 @@
     f_ecrecover,
     f_sha3_256_name,
     f_sha3_512_name,
+    f_sha3_empty,
     f_sha3_name,
     hexify,
     int_of,
@@ -132,7 +133,6 @@
 
 EMPTY_BYTES = ByteVec()
 EMPTY_KECCAK = 0xC5D2460186F7233C927E7DB2DCC703C0E500B653CA82273B7BFAD8045D85A470
-EMPTY_KECCAK_BV = con(EMPTY_KECCAK)
 ZERO, ONE = con(0), con(1)
 MAX_CALL_DEPTH = 1024
 
@@ -1139,7 +1139,7 @@ def sha3_expr(self, data: Bytes) -> Word:
 
         bitsize = byte_length(data) * 8
         if bitsize == 0:
-            return EMPTY_KECCAK_BV
+            return f_sha3_empty
 
         if isinstance(data, bytes):
             data = bytes_to_bv_value(data)
@@ -3044,9 +3044,15 @@ def finalize(ex: Exec):
                 elif EVM.PUSH1 <= opcode <= EVM.PUSH32:
                     val = unbox_int(insn.operand)
                     if isinstance(val, int):
-                        if opcode == EVM.PUSH32 and val in sha3_inv:
-                            # restore precomputed hashes
-                            ex.st.push(ex.sha3_data(con(sha3_inv[val])))
+                        if opcode == EVM.PUSH32:
+                            if val in sha3_inv:
+                                # restore precomputed hashes
+                                ex.st.push(ex.sha3_data(con(sha3_inv[val])))
+                            # TODO: support more commonly used concrete keccak values
+                            elif val == EMPTY_KECCAK:
+                                ex.st.push(ex.sha3_data(b""))
+                            else:
+                                ex.st.push(val)
                         else:
                             ex.st.push(val)
                     else:
diff --git a/src/halmos/utils.py b/src/halmos/utils.py
index 20f2a1ef..3c486714 100644
--- a/src/halmos/utils.py
+++ b/src/halmos/utils.py
@@ -11,6 +11,7 @@
     Z3_OP_BADD,
     Z3_OP_CONCAT,
     Z3_OP_ULEQ,
+    BitVec,
     BitVecNumRef,
     BitVecRef,
     BitVecSort,
@@ -110,6 +111,9 @@ def f_sha3_name(bitsize: int) -> str:
 f_sha3_256_name = f_sha3_name(256)
 f_sha3_512_name = f_sha3_name(512)
 
+f_sha3_0_name = f_sha3_name(0)
+f_sha3_empty = BitVec(f_sha3_0_name, BitVecSort256)
+
 
 def uid() -> str:
     return uuid.uuid4().hex[:7]
diff --git a/tests/expected/all.json b/tests/expected/all.json
index 36ccfa74..36f1c844 100644
--- a/tests/expected/all.json
+++ b/tests/expected/all.json
@@ -2270,6 +2270,15 @@
                 "time": null,
                 "num_bounded_loops": null
             },
+            {
+                "name": "check_hash_collision_with_empty()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_no_hash_collision_assumption()",
                 "exitcode": 0,
@@ -2278,6 +2287,15 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_only_empty_bytes_matches_empty_hash(bytes)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/SignExtend.t.sol:SignExtendTest": [
diff --git a/tests/regression/test/Sha3.t.sol b/tests/regression/test/Sha3.t.sol
index ad7afd0b..3e49c048 100644
--- a/tests/regression/test/Sha3.t.sol
+++ b/tests/regression/test/Sha3.t.sol
@@ -29,12 +29,10 @@ contract Sha3Test is Test, SymTest {
         assert(data32_1[0] == data32_2[0]);
     }
 
-    /* TODO:
     function check_hash_collision_with_empty() public {
         bytes memory data = svm.createBytes(1, "data");
         assertNotEq(keccak256(data), keccak256(""));
     }
-    */
 
     function check_empty_hash_value() public {
         assertEq(keccak256(""), EMPTY_HASH);
@@ -44,13 +42,11 @@ contract Sha3Test is Test, SymTest {
         // assertEq(keccak256(data), EMPTY_HASH);
     }
 
-    /* TODO:
     function check_only_empty_bytes_matches_empty_hash(bytes memory data) public {
         // empty hash value
         vm.assume(keccak256(data) == EMPTY_HASH);
         assertEq(data.length, 0);
     }
-    */
 
     function check_concrete_keccak_does_not_split_paths() external {
         bytes32 hash = keccak256("data");
@@ -68,7 +64,7 @@ contract Sha3Test is Test, SymTest {
         }
     }
 
-    /* TODO:
+    /* TODO: need lazy concretization
     function check_concrete_keccak_memory_lookup() external {
         bytes32 hash = keccak256(abi.encodePacked(uint256(3)));
         uint256 bit = uint256(hash) & 1;