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

@@ -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)