From 21e1bd46e13080e9a1b02cadb604d88da9ef41b9 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Mon, 22 Jan 2024 17:22:06 -0800 Subject: [PATCH] Fix eager jumpdest parsing We used to parse valid jumpdests on the fly, we now do it eagerly once and cache the results. This exposes an issue with jumpdest parsing for contracts with symbolic arguments at the end -- in this case we assume that symbolic arguments are data and don't contain potentially valid jumpdests (technically they could, but we don't normally attempt to deal with symbolic bytecode) --- src/halmos/sevm.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 1b16e995..0ee49a69 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -562,7 +562,7 @@ def from_hexcode(hexcode: str): raise ValueError(f"{e} (hexcode={hexcode})") def decode_instruction(self, pc: int) -> Instruction: - opcode = int_of(self[pc]) + opcode = int_of(self[pc], f"symbolic opcode at pc={pc}") if EVM.PUSH1 <= opcode <= EVM.PUSH32: operand = self.slice(pc + 1, pc + opcode - EVM.PUSH0 + 1) @@ -592,10 +592,9 @@ def slice(self, start, stop) -> UnionType[bytes, BitVecRef]: return bytes(data) @cache - def __getitem__(self, offset: int) -> UnionType[int, BitVecRef]: + def __getitem__(self, key: int) -> UnionType[int, BitVecRef]: """Returns the byte at the given offset.""" - if not isinstance(offset, int): - raise ValueError("unexpected program offset {offset!r}") + offset = int_of(key, "symbolic index into contract bytecode {offset!r}") # support for negative indexing, e.g. contract[-1] if offset < 0: @@ -641,6 +640,9 @@ def __next__(self) -> Instruction: if self.pc >= len(self.contract): raise StopIteration + if self.is_symbolic and is_bv(self.contract[self.pc]): + raise StopIteration + insn = self.contract.decode_instruction(self.pc) self.pc += len(insn)