first cut: shadow calldata

src/halmos/sevm.py

@@ -58,7 +58,7 @@
 from z3.z3util import is_expr_var
 
 from .bytevec import ByteVec, Chunk, ConcreteChunk, UnwrappedBytes
-from .calldata import FunctionInfo
+from .calldata import FunctionInfo, get_abi, mk_calldata
 from .cheatcodes import Prank, halmos_cheat_code, hevm_cheat_code
 from .config import Config as HalmosConfig
 from .console import console
@@ -2633,6 +2633,92 @@ def create_branch(self, ex: Exec, cond: BitVecRef, target: int) -> Exec:
         )
         return new_ex
 
+    def refine_calldata(self, ex: Exec):
+        calldata = ex.calldata()
+
+        if hasattr(calldata, "shadow_calldata"):
+            return
+
+        if len(calldata) < 4:
+            return
+
+        selector_term = calldata[0:4].unwrap()
+
+        selector = ex.path.concretization.substitution.get(selector_term) if is_bv(selector_term) else selector_term
+
+        if selector is None:
+            if not str(selector_term).startswith("fallback_selector_"):
+                warn(
+                    f"{self.fun_info.sig}: xxx: couldn't concretize the selector: {selector_term}\n"
+#                   f"{ex.path.concretization.substitution}"
+                )
+#               print(ex)
+            return
+
+#       print("selector", hexify(selector_term), hexify(selector))
+
+        selector = int_of(selector, f"{self.fun_info.sig}: xxx: symbolic selector: {selector}")
+
+        contract_name = ex.pgm.contract_name
+        filename = ex.pgm.filename
+
+        if not contract_name:
+            if not eq(ex.this(), con_addr(FOUNDRY_TEST)):
+                warn(
+                    f"{self.fun_info.sig}: xxx: couldn't find contract name for: {hexify(selector)}\n"
+                )
+#               print(ex)
+            return
+
+        contract_json = BuildOut().get_by_name(contract_name, filename)
+        abi = get_abi(contract_json)
+        methodIdentifiers = contract_json["methodIdentifiers"]
+
+        def get_funsig(funselector):
+            selector_dict = contract_json.get("selector_dict")
+
+            if selector_dict is None:
+                selector_dict = {
+                    _funselector: _funsig
+                    for _funsig, _funselector in methodIdentifiers.items()
+                }
+                contract_json["selector_dict"] = selector_dict
+
+            return selector_dict.get(funselector)
+
+        funselector = f"{selector:08x}"
+        funsig = get_funsig(funselector)
+
+        if not funsig:
+            # it's possible for proxy delegate: e.g., see ProxyTest, ERC1967Proxy
+            warn(
+                f"{self.fun_info.sig}: xxx: couldn't find funsig: {hexify(selector)} in {filename}:{contract_name}\n"
+                f"{methodIdentifiers}"
+            )
+            return
+
+        funname = funsig.split("(")[0]
+        funinfo = FunctionInfo(funname, funsig, funselector)
+
+        shadow_calldata, dyn_params = mk_calldata(
+            abi,
+            funinfo,
+            self.options,
+            new_symbol_id=ex.new_symbol_id,
+            max_size=len(calldata),
+        )
+
+#       print(shadow_calldata, dyn_params)
+
+        calldata.shadow_calldata = shadow_calldata
+        calldata.shadow_dyn_params = {
+            d.size_symbol: d.size_choices
+            for d in dyn_params
+        }
+
+#       print(hasattr(calldata, "shadow_calldata"))
+
+
     def calldataload(
         self,
         ex: Exec,
@@ -2648,7 +2734,11 @@ def calldataload(
         """
 
         offset: int = ex.int_of(ex.st.pop(), "symbolic CALLDATALOAD offset")
-        loaded = ex.calldata().get_word(offset)
+        calldata = ex.calldata()
+        loaded = calldata.get_word(offset)
+
+#       print("calldataload", calldata, offset, hexify(loaded))
+#       print(ex)
 
         if is_expr_var(loaded):
             concrete_loaded = ex.path.concretization.substitution.get(loaded)
@@ -2668,6 +2758,39 @@ def calldataload(
                     stack.push(new_ex, step_id)
                 return
 
+        if not is_concrete(loaded):
+
+#           print("refine")
+
+            def get_shadow():
+                self.refine_calldata(ex)
+
+                if not hasattr(calldata, "shadow_calldata"):
+                    return None, None
+
+                shadow_calldata = calldata.shadow_calldata
+#               print(shadow_calldata)
+                shadow_loaded = shadow_calldata.get_word(offset)
+
+                return shadow_loaded, calldata.shadow_dyn_params.get(shadow_loaded)
+
+            shadow_loaded, shadow_loaded_candidates = get_shadow()
+
+#           print(shadow_loaded, shadow_loaded_candidates)
+
+            if shadow_loaded is not None:
+                if is_concrete(shadow_loaded):
+                    ex.path.append(loaded == shadow_loaded)
+                    loaded = shadow_loaded
+
+                if shadow_loaded_candidates is not None:
+                    for candidate in shadow_loaded_candidates:
+                        new_ex = self.create_branch(ex, loaded == candidate, ex.pc)
+                        new_ex.st.push(candidate)
+                        new_ex.advance_pc()
+                        stack.push(new_ex, step_id)
+                    return
+
         ex.st.push(loaded)
         ex.advance_pc()
         stack.push(ex, step_id)
@@ -2863,6 +2986,9 @@ def finalize(ex: Exec):
                         ex.st.push(SignExt(256 - bl, Extract(bl - 1, 0, ex.st.pop())))
 
                 elif opcode == EVM.CALLDATALOAD:
+#                   if not eq(ex.st.peek(), ZERO):
+#                       self.refine_calldata(ex)
+
                     self.calldataload(ex, stack, step_id)
                     continue
 
@@ -3069,6 +3195,8 @@ def finalize(ex: Exec):
                         ex.st.memory.set_slice(loc, end_loc, data)
 
                 elif opcode == EVM.CALLDATACOPY:
+#                   self.refine_calldata(ex)
+
                     loc: int = ex.mloc()
                     offset: int = ex.int_of(ex.st.pop(), "symbolic CALLDATACOPY offset")
                     size: int = ex.int_of(ex.st.pop(), "symbolic CALLDATACOPY size")