fix: concretize calldatacopy

src/halmos/bytevec.py

@@ -5,6 +5,7 @@
 
 from sortedcontainers import SortedDict
 from z3 import BitVecRef, If, eq, is_bool, is_bv, is_bv_value, simplify
+from z3.z3util import is_expr_var
 
 from .utils import (
     Byte,
@@ -610,6 +611,23 @@ def set_word(self, offset: int, value: Word) -> None:
 
         self.set_slice(offset, offset + 32, value)
 
+    def concretize(self, substitution: dict[BitVecRef, BitVecRef]) -> None:
+        """
+        Replace all symbols in the chunks with their corresponding concrete values, if they exist in the given substituion mapping.
+        """
+        for offset, chunk in self.chunks.items():
+            chunk_data = chunk.data
+            if not isinstance(chunk, SymbolicChunk) or not is_expr_var(chunk_data):
+                continue
+
+            concrete_chunk_data = substitution.get(chunk_data)
+            if concrete_chunk_data is None:  # could be zero
+                continue
+
+            self.chunks[offset] = ConcreteChunk(
+                bv_value_to_bytes(concrete_chunk_data), chunk.start, chunk.length
+            )
+
     ### read operations
 
     def slice(self, start: int, stop: int) -> "ByteVec":

src/halmos/sevm.py

@@ -644,8 +644,10 @@ class Concretization:
     In the future, it may be used for other purposes, such as concrete hash reasoning.
     """
 
-    substitution: dict = field(default_factory=dict)  # symbol -> constant
-    candidates: dict = field(default_factory=dict)  # symbol -> set of constants
+    # symbol -> constant
+    substitution: dict[BitVecRef, BitVecRef] = field(default_factory=dict)
+    # symbol -> set of constants
+    candidates: dict[BitVecRef, list[int]] = field(default_factory=dict)
 
     def process_cond(self, cond):
         if not is_eq(cond):
@@ -2863,6 +2865,7 @@ def finalize(ex: Exec):
 
                     if size > 0:
                         data: ByteVec = ex.calldata().slice(offset, offset + size)
+                        data.concretize(ex.path.concretization.substitution)
                         ex.st.memory.set_slice(loc, end_loc, data)
 
                 elif opcode == EVM.CODECOPY: