Skip to content

Commit

Permalink
fix: handle stack underflows in DUPn/SWAPn instructions
Browse files Browse the repository at this point in the history
fixes #438
  • Loading branch information
karmacoma-eth committed Jan 10, 2025
1 parent b276768 commit 134ee80
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 7 deletions.
6 changes: 6 additions & 0 deletions src/halmos/sevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -452,9 +452,15 @@ def peek(self, n: int = 1) -> Word:
return self.stack[-n]

def dup(self, n: int) -> None:
if len(self.stack) < n:
raise StackUnderflowError()

self.stack.append(self.stack[-n])

def swap(self, n: int) -> None:
if len(self.stack) < n + 1:
raise StackUnderflowError()

self.stack[-(n + 1)], self.stack[-1] = self.stack[-1], self.stack[-(n + 1)]

def mloc(self, subst: dict = None) -> int:
Expand Down
19 changes: 12 additions & 7 deletions tests/test_sevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -336,13 +336,18 @@ def test_opcode_stack(hexcode, stack_in, stack_out, sevm: SEVM, solver, storage)
assert output_ex.st.stack == list(reversed(stack_out))


def test_stack_underflow_pop(sevm: SEVM, solver, storage):
# check that we get an exception when popping from an empty stack
ex = mk_ex(o(EVM.POP), sevm, solver, storage, caller, this)

exs: list[Exec] = list(sevm.run(ex))

[output_ex] = exs
@pytest.mark.parametrize(
"opcode",
[
EVM.POP,
*range(EVM.DUP1, EVM.DUP16 + 1),
*range(EVM.SWAP1, EVM.SWAP16 + 1),
],
)
def test_stack_underflow(sevm: SEVM, solver, storage, opcode):
"""Test that operations on empty stack raise StackUnderflowError"""
ex = mk_ex(o(opcode), sevm, solver, storage, caller, this)
[output_ex] = list(sevm.run(ex))
assert isinstance(output_ex.context.output.error, StackUnderflowError)


Expand Down

0 comments on commit 134ee80

Please sign in to comment.