Repository: a16z/halmos

Issue:
SWAPn/DUPn instructions don't handle stack underflows correctly
e.g. if you DUP1 from an empty stack:

```sh
ERROR    IndexError: list index out of range                                                   
Traceback (most recent call last):
  File "/home/mk/.local/share/uv/tools/halmos/lib/python3.12/site-packages/halmos/__main__.py", line 906, in run_sequential
    test_result = run(setup_ex, run_args.abi, fun_info, test_config, solver)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/mk/.local/share/uv/tools/halmos/lib/python3.12/site-packages/halmos/__main__.py", line 694, in run
    for idx, ex in enumerate(exs):
  File "/home/mk/.local/share/uv/tools/halmos/lib/python3.12/site-packages/halmos/sevm.py", line 2667, in run
    yield from self._run(ex0, status)
  File "/home/mk/.local/share/uv/tools/halmos/lib/python3.12/site-packages/halmos/sevm.py", line 3141, in _run
    ex.st.dup(opcode - EVM.DUP1 + 1)
  File "/home/mk/.local/share/uv/tools/halmos/lib/python3.12/site-packages/halmos/sevm.py", line 452, in dup
    self.stack.append(self.stack[-n])
                      ~~~~~~~~~~^^^^
```

h/t @m4k2

Hints from issue comments:

Solution patch:
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index 4265934..ac5ce97 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -452,9 +452,15 @@ class State:
         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:


Test patch:
diff --git a/tests/test_sevm.py b/tests/test_sevm.py
index 7c39ef7..eabfd21 100644
--- a/tests/test_sevm.py
+++ b/tests/test_sevm.py
@@ -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)